GC000F

crt_is_gcd_coprime_factor_remove

A multiplier coprime to the fixed right input does not change the full relational gcd of the left input.

Alpha v34 checked-use · first admitted v25 · independently kernel and Lean verified; not Stable

Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved. Exact original first-admission records.

Historical partial components only: this chapter proves canonical solutions under successive-merge compatibility and in the pairwise-compatible dominating-last case. G011 is now closed in the separate Alpha-v27 generalized-crt branch for arbitrary pairwise-compatible finite lists, including noncoprime moduli. Full G011 proof · Alpha v27

Exact theorem in conservative defined notation

∀ s. ∀ a. ∀ n. ∀ g. ∀ A. A = s · a → Coprime(s,n) → IsGCD(g,a,n) → IsGCD(g,A,n)

Every linked abbreviation expands hygienically to the identical original native formula.

Definition DAG

Coprime(a,b) · 1IsGCD(g,a,b) · 2

Actual proof prerequisites

is_gcd_dvd_left · checked external prerequisiteis_gcd_dvd_right · checked external prerequisitemul_comm · checked external prerequisitemul_assoc · checked external prerequisitemultiple_refl · checked external prerequisitecrt_coprime_divisor_paircoprime_symm · checked external prerequisitegauss_coprime_cancel · checked external prerequisiteis_gcd_greatest · checked external prerequisite
Original expanded first-order statement 
forall s a n g A. A = s * a -> (forall frp_divisor_gcomp_remove_coprime. (exists frp_left_factor_gcomp_remove_coprime. s = frp_divisor_gcomp_remove_coprime * frp_left_factor_gcomp_remove_coprime) -> (exists frp_right_factor_gcomp_remove_coprime. n = frp_divisor_gcomp_remove_coprime * frp_right_factor_gcomp_remove_coprime) -> frp_divisor_gcomp_remove_coprime = 1) -> ((((exists hag_left_factor_gcomp_remove_source. a = g * hag_left_factor_gcomp_remove_source) /\ (exists hag_right_factor_gcomp_remove_source. n = g * hag_right_factor_gcomp_remove_source)) /\ forall hag_divisor_gcomp_remove_source. (exists hag_common_left_gcomp_remove_source. a = hag_divisor_gcomp_remove_source * hag_common_left_gcomp_remove_source) -> (exists hag_common_right_gcomp_remove_source. n = hag_divisor_gcomp_remove_source * hag_common_right_gcomp_remove_source) -> exists hag_greatest_factor_gcomp_remove_source. g = hag_divisor_gcomp_remove_source * hag_greatest_factor_gcomp_remove_source)) -> ((((exists hag_left_factor_gcomp_remove_result. A = g * hag_left_factor_gcomp_remove_result) /\ (exists hag_right_factor_gcomp_remove_result. n = g * hag_right_factor_gcomp_remove_result)) /\ forall hag_divisor_gcomp_remove_result. (exists hag_common_left_gcomp_remove_result. A = hag_divisor_gcomp_remove_result * hag_common_left_gcomp_remove_result) -> (exists hag_common_right_gcomp_remove_result. n = hag_divisor_gcomp_remove_result * hag_common_right_gcomp_remove_result) -> exists hag_greatest_factor_gcomp_remove_result. g = hag_divisor_gcomp_remove_result * hag_greatest_factor_gcomp_remove_result))

Complete unchanged native tactic proof

All 69 lines are the exact independently kernel-checked original script.

Read the argument

Proof checkpoints

69 script commands · 20 reading checkpoints · 4 local claims

This is a reading aid, not a new proof or a proof-tree certificate. Checkpoint groups are consecutive commands, not inferred branch boundaries. Every step links to the preserved script.

Definition notation is shown below. Open the paired exact edition for the original native formulas. Source pairing is not a new equivalence certificate.

Named ingredients (1)
crt coprime divisor pair
01Fix variables and assumptionsL1–8

Work with arbitrary variables or the premises of the current implication.

  1. L1
    intro s
  2. L2
    intro a
  3. L3
    intro n
  4. L4
    intro g
  5. L5
    intro A
  6. L6
    intro hA
  7. L7
    intro hcoprime
  8. L8
    intro hg
02Separate the logical casesL9–10

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L9
    split
  2. L10
    split
03Use earlier factsL11–13

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L11
    specialize is_gcd_dvd_left g
  2. L12
    specialize is_gcd_dvd_left a
  3. L13
    specialize is_gcd_dvd_left n
04Establish hdividesL14–16

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply is gcd dvd left.

  1. L14
    have hdivides : exists q. a = g * q
  2. L15
    apply is_gcd_dvd_left
  3. L16
    exact hg
05Separate the logical casesL17–17

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L17
    cases hdivides
06Construct an explicit witnessL18–18

Supply the displayed value, then prove that it has the required property.

  1. L18
    exists s * x
07Calculate and transport equalitiesL19–22

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L19
    rewrite hA
  2. L20
    rewrite hdivides_witness
  3. L21
    trans (s * g) * x
  4. L22
    symm
08Use earlier factsL23–23

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L23
    apply mul_assoc
09Calculate and transport equalitiesL24–25

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L24
    trans (g * s) * x
  2. L25
    congr
10Use earlier factsL26–26

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L26
    apply mul_comm
11Calculate and transport equalitiesL27–27

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L27
    refl
12Use earlier factsL28–33

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L28
    apply mul_assoc
  2. L29
    specialize is_gcd_dvd_right g
  3. L30
    specialize is_gcd_dvd_right a
  4. L31
    specialize is_gcd_dvd_right n
  5. L32
    apply is_gcd_dvd_right
  6. L33
    exact hg
13Fix variables and assumptionsL34–36

Work with arbitrary variables or the premises of the current implication.

  1. L34
    intro d
  2. L35
    intro hdA
  3. L36
    intro hdn
14Establish hforwardL37–46

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply crt coprime divisor pair.

  1. L37
    have hforward : forall frp_divisor_gcomp_remove_forward. (exists frp_left_factor_gcomp_remove_forward. s = frp_divisor_gcomp_remove_forward * frp_left_factor_gcomp_remove_forward) -> (exists frp_right_factor_gcomp_remove_forward. d = frp_divisor_gcomp_remove_forward * frp_right_factor_gcomp_remove_forward) -> frp_divisor_gcomp_remove_forward = 1
  2. L38
    specialize crt_coprime_divisor_pair s
  3. L39
    specialize crt_coprime_divisor_pair n
  4. L40
    specialize crt_coprime_divisor_pair s
  5. L41
    specialize crt_coprime_divisor_pair d
  6. L42
    apply crt_coprime_divisor_pair
  7. L43
    exact hcoprime
  8. L44
    specialize multiple_refl s
  9. L45
    exact multiple_refl
  10. L46
    exact hdn
15Establish hreverseL47–51

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply coprime symm.

  1. L47
    have hreverse : forall frp_divisor_gcomp_remove_reverse. (exists frp_left_factor_gcomp_remove_reverse. d = frp_divisor_gcomp_remove_reverse * frp_left_factor_gcomp_remove_reverse) -> (exists frp_right_factor_gcomp_remove_reverse. s = frp_divisor_gcomp_remove_reverse * frp_right_factor_gcomp_remove_reverse) -> frp_divisor_gcomp_remove_reverse = 1
  2. L48
    specialize coprime_symm s
  3. L49
    specialize coprime_symm d
  4. L50
    apply coprime_symm
  5. L51
    exact hforward
16Establish hdaL52–57

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply gauss coprime cancel.

  1. L52
    have hda : exists q. a = d * q
  2. L53
    specialize gauss_coprime_cancel d
  3. L54
    specialize gauss_coprime_cancel s
  4. L55
    specialize gauss_coprime_cancel a
  5. L56
    apply gauss_coprime_cancel
  6. L57
    exact hreverse
17Separate the logical casesL58–58

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L58
    cases hdA
18Construct an explicit witnessL59–59

Supply the displayed value, then prove that it has the required property.

  1. L59
    exists x
19Calculate and transport equalitiesL60–60

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L60
    rewrite hA at hdA_witness
20Use earlier factsL61–69

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L61
    exact hdA_witness
  2. L62
    specialize is_gcd_greatest g
  3. L63
    specialize is_gcd_greatest a
  4. L64
    specialize is_gcd_greatest n
  5. L65
    specialize is_gcd_greatest d
  6. L66
    apply is_gcd_greatest
  7. L67
    exact hg
  8. L68
    exact hda
  9. L69
    exact hdn

Library-wide reading audit

Original defined command ledger · 69 lines
  1. 0001intro s
  2. 0002intro a
  3. 0003intro n
  4. 0004intro g
  5. 0005intro A
  6. 0006intro hA
  7. 0007intro hcoprime
  8. 0008intro hg
  9. 0009split
  10. 0010split
  11. 0011specialize is_gcd_dvd_left g
  12. 0012specialize is_gcd_dvd_left a
  13. 0013specialize is_gcd_dvd_left n
  14. 0014have hdivides : exists q. a = g * q
  15. 0015apply is_gcd_dvd_left
  16. 0016exact hg
  17. 0017cases hdivides
  18. 0018exists s * x
  19. 0019rewrite hA
  20. 0020rewrite hdivides_witness
  21. 0021trans (s * g) * x
  22. 0022symm
  23. 0023apply mul_assoc
  24. 0024trans (g * s) * x
  25. 0025congr
  26. 0026apply mul_comm
  27. 0027refl
  28. 0028apply mul_assoc
  29. 0029specialize is_gcd_dvd_right g
  30. 0030specialize is_gcd_dvd_right a
  31. 0031specialize is_gcd_dvd_right n
  32. 0032apply is_gcd_dvd_right
  33. 0033exact hg
  34. 0034intro d
  35. 0035intro hdA
  36. 0036intro hdn
  37. 0037have hforward : forall frp_divisor_gcomp_remove_forward. (exists frp_left_factor_gcomp_remove_forward. s = frp_divisor_gcomp_remove_forward * frp_left_factor_gcomp_remove_forward) -> (exists frp_right_factor_gcomp_remove_forward. d = frp_divisor_gcomp_remove_forward * frp_right_factor_gcomp_remove_forward) -> frp_divisor_gcomp_remove_forward = 1
  38. 0038specialize crt_coprime_divisor_pair s
  39. 0039specialize crt_coprime_divisor_pair n
  40. 0040specialize crt_coprime_divisor_pair s
  41. 0041specialize crt_coprime_divisor_pair d
  42. 0042apply crt_coprime_divisor_pair
  43. 0043exact hcoprime
  44. 0044specialize multiple_refl s
  45. 0045exact multiple_refl
  46. 0046exact hdn
  47. 0047have hreverse : forall frp_divisor_gcomp_remove_reverse. (exists frp_left_factor_gcomp_remove_reverse. d = frp_divisor_gcomp_remove_reverse * frp_left_factor_gcomp_remove_reverse) -> (exists frp_right_factor_gcomp_remove_reverse. s = frp_divisor_gcomp_remove_reverse * frp_right_factor_gcomp_remove_reverse) -> frp_divisor_gcomp_remove_reverse = 1
  48. 0048specialize coprime_symm s
  49. 0049specialize coprime_symm d
  50. 0050apply coprime_symm
  51. 0051exact hforward
  52. 0052have hda : exists q. a = d * q
  53. 0053specialize gauss_coprime_cancel d
  54. 0054specialize gauss_coprime_cancel s
  55. 0055specialize gauss_coprime_cancel a
  56. 0056apply gauss_coprime_cancel
  57. 0057exact hreverse
  58. 0058cases hdA
  59. 0059exists x
  60. 0060rewrite hA at hdA_witness
  61. 0061exact hdA_witness
  62. 0062specialize is_gcd_greatest g
  63. 0063specialize is_gcd_greatest a
  64. 0064specialize is_gcd_greatest n
  65. 0065specialize is_gcd_greatest d
  66. 0066apply is_gcd_greatest
  67. 0067exact hg
  68. 0068exact hda
  69. 0069exact hdn