Theorem: HTPI.Theorem_7_2_2 (HTPILib/Chap7.lean)

State before:
a b c : ℕ
h1 : c ∣ a * b
h2 : rel_prime a c
⊢ c ∣ b
Tactic:
rewrite [←Int.coe_nat_dvd]
State after:
a b c : ℕ
h1 : c ∣ a * b
h2 : rel_prime a c
⊢ ↑c ∣ ↑b

State before:
a b c : ℕ
h1 : c ∣ a * b
h2 : rel_prime a c
⊢ ↑c ∣ ↑b
Tactic:
define at h1
State after:
a b c : ℕ
h1 : ∃ c_1, a * b = c * c_1
h2 : rel_prime a c
⊢ ↑c ∣ ↑b

State before:
a b c : ℕ
h1 : ∃ c_1, a * b = c * c_1
h2 : rel_prime a c
⊢ ↑c ∣ ↑b
Tactic:
define at h2
State after:
a b c : ℕ
h1 : ∃ c_1, a * b = c * c_1
h2 : gcd a c = 1
⊢ ↑c ∣ ↑b

State before:
a b c : ℕ
h1 : ∃ c_1, a * b = c * c_1
h2 : gcd a c = 1
⊢ ↑c ∣ ↑b
Tactic:
define
State after:
a b c : ℕ
h1 : ∃ c_1, a * b = c * c_1
h2 : gcd a c = 1
⊢ ∃ c_1, ↑b = ↑c * c_1

State before:
a b c : ℕ
h1 : ∃ c_1, a * b = c * c_1
h2 : gcd a c = 1
⊢ ∃ c_1, ↑b = ↑c * c_1
Tactic:
obtain (j : Nat) (h3 : a * b = c * j) from h1
State after:
a b c : ℕ
h1 : ∃ c_1, a * b = c * c_1
h2 : gcd a c = 1
j : ℕ
h3 : a * b = c * j
⊢ ∃ c_1, ↑b = ↑c * c_1

State before:
a b c : ℕ
h1 : ∃ c_1, a * b = c * c_1
h2 : gcd a c = 1
j : ℕ
h3 : a * b = c * j
⊢ ∃ c_1, ↑b = ↑c * c_1
Tactic:
set s : Int := gcd_c1 a c
State after:
a b c : ℕ
h1 : ∃ c_1, a * b = c * c_1
h2 : gcd a c = 1
j : ℕ
h3 : a * b = c * j
s : ℤ := gcd_c1 a c
⊢ ∃ c_1, ↑b = ↑c * c_1

State before:
a b c : ℕ
h1 : ∃ c_1, a * b = c * c_1
h2 : gcd a c = 1
j : ℕ
h3 : a * b = c * j
s : ℤ := gcd_c1 a c
⊢ ∃ c_1, ↑b = ↑c * c_1
Tactic:
set t : Int := gcd_c2 a c
State after:
a b c : ℕ
h1 : ∃ c_1, a * b = c * c_1
h2 : gcd a c = 1
j : ℕ
h3 : a * b = c * j
s : ℤ := gcd_c1 a c
t : ℤ := gcd_c2 a c
⊢ ∃ c_1, ↑b = ↑c * c_1

State before:
a b c : ℕ
h1 : ∃ c_1, a * b = c * c_1
h2 : gcd a c = 1
j : ℕ
h3 : a * b = c * j
s : ℤ := gcd_c1 a c
t : ℤ := gcd_c2 a c
⊢ ∃ c_1, ↑b = ↑c * c_1
Tactic:
have h4 : s * ↑a + t * ↑c = ↑(gcd a c) := gcd_lin_comb c a
State after:
a b c : ℕ
h1 : ∃ c_1, a * b = c * c_1
h2 : gcd a c = 1
j : ℕ
h3 : a * b = c * j
s : ℤ := gcd_c1 a c
t : ℤ := gcd_c2 a c
h4 : s * ↑a + t * ↑c = ↑(gcd a c)
⊢ ∃ c_1, ↑b = ↑c * c_1

State before:
a b c : ℕ
h1 : ∃ c_1, a * b = c * c_1
h2 : gcd a c = 1
j : ℕ
h3 : a * b = c * j
s : ℤ := gcd_c1 a c
t : ℤ := gcd_c2 a c
h4 : s * ↑a + t * ↑c = ↑(gcd a c)
⊢ ∃ c_1, ↑b = ↑c * c_1
Tactic:
rewrite [h2, Nat.cast_one] at h4
State after:
a b c : ℕ
h1 : ∃ c_1, a * b = c * c_1
h2 : gcd a c = 1
j : ℕ
h3 : a * b = c * j
s : ℤ := gcd_c1 a c
t : ℤ := gcd_c2 a c
h4 : s * ↑a + t * ↑c = 1
⊢ ∃ c_1, ↑b = ↑c * c_1

State before:
a b c : ℕ
h1 : ∃ c_1, a * b = c * c_1
h2 : gcd a c = 1
j : ℕ
h3 : a * b = c * j
s : ℤ := gcd_c1 a c
t : ℤ := gcd_c2 a c
h4 : s * ↑a + t * ↑c = 1
⊢ ∃ c_1, ↑b = ↑c * c_1
Tactic:
apply Exists.intro (s * ↑j + t * ↑b)
State after:
a b c : ℕ
h1 : ∃ c_1, a * b = c * c_1
h2 : gcd a c = 1
j : ℕ
h3 : a * b = c * j
s : ℤ := gcd_c1 a c
t : ℤ := gcd_c2 a c
h4 : s * ↑a + t * ↑c = 1
⊢ ↑b = ↑c * (s * ↑j + t * ↑b)

State before:
a b c : ℕ
h1 : ∃ c_1, a * b = c * c_1
h2 : gcd a c = 1
j : ℕ
h3 : a * b = c * j
s : ℤ := gcd_c1 a c
t : ℤ := gcd_c2 a c
h4 : s * ↑a + t * ↑c = 1
⊢ ↑b = ↑c * (s * ↑j + t * ↑b)
Tactic:
show ↑b = ↑c * (s * ↑j + t * ↑b) from
  calc ↑b
    _ = (1 : Int) * ↑b := (one_mul _).symm
    _ = (s * ↑a + t * ↑c) * ↑b := by rw [h4]
    _ = s * (↑a * ↑b) + t * ↑c * ↑b := by ring
    _ = s * (↑c * ↑j) + t * ↑c * ↑b := by
          rw [←Nat.cast_mul a b, h3, Nat.cast_mul c j]
    _ = ↑c * (s * ↑j + t * ↑b) := by ring
State after:
no goals

State before:
a b c : ℕ
h1 : ∃ c_1, a * b = c * c_1
h2 : gcd a c = 1
j : ℕ
h3 : a * b = c * j
s : ℤ := gcd_c1 a c
t : ℤ := gcd_c2 a c
h4 : s * ↑a + t * ↑c = 1
⊢ 1 * ↑b = (s * ↑a + t * ↑c) * ↑b
Tactic:
rw [h4]
State after:
no goals

State before:
a b c : ℕ
h1 : ∃ c_1, a * b = c * c_1
h2 : gcd a c = 1
j : ℕ
h3 : a * b = c * j
s : ℤ := gcd_c1 a c
t : ℤ := gcd_c2 a c
h4 : s * ↑a + t * ↑c = 1
⊢ (s * ↑a + t * ↑c) * ↑b = s * (↑a * ↑b) + t * ↑c * ↑b
Tactic:
ring
State after:
no goals

State before:
a b c : ℕ
h1 : ∃ c_1, a * b = c * c_1
h2 : gcd a c = 1
j : ℕ
h3 : a * b = c * j
s : ℤ := gcd_c1 a c
t : ℤ := gcd_c2 a c
h4 : s * ↑a + t * ↑c = 1
⊢ s * (↑a * ↑b) + t * ↑c * ↑b = s * (↑c * ↑j) + t * ↑c * ↑b
Tactic:
rw [←Nat.cast_mul a b, h3, Nat.cast_mul c j]
State after:
no goals

State before:
a b c : ℕ
h1 : ∃ c_1, a * b = c * c_1
h2 : gcd a c = 1
j : ℕ
h3 : a * b = c * j
s : ℤ := gcd_c1 a c
t : ℤ := gcd_c2 a c
h4 : s * ↑a + t * ↑c = 1
⊢ s * (↑c * ↑j) + t * ↑c * ↑b = ↑c * (s * ↑j + t * ↑b)
Tactic:
ring
State after:
no goals