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

State before:
d a b : ℕ
h1 : d ∣ a
h2 : d ∣ b
⊢ d ∣ gcd a b
Tactic:
rewrite [←Int.coe_nat_dvd]
State after:
d a b : ℕ
h1 : d ∣ a
h2 : d ∣ b
⊢ ↑d ∣ ↑(gcd a b)

State before:
d a b : ℕ
h1 : d ∣ a
h2 : d ∣ b
⊢ ↑d ∣ ↑(gcd a b)
Tactic:
set s : Int := gcd_c1 a b
State after:
d a b : ℕ
h1 : d ∣ a
h2 : d ∣ b
s : ℤ := gcd_c1 a b
⊢ ↑d ∣ ↑(gcd a b)

State before:
d a b : ℕ
h1 : d ∣ a
h2 : d ∣ b
s : ℤ := gcd_c1 a b
⊢ ↑d ∣ ↑(gcd a b)
Tactic:
set t : Int := gcd_c2 a b
State after:
d a b : ℕ
h1 : d ∣ a
h2 : d ∣ b
s : ℤ := gcd_c1 a b
t : ℤ := gcd_c2 a b
⊢ ↑d ∣ ↑(gcd a b)

State before:
d a b : ℕ
h1 : d ∣ a
h2 : d ∣ b
s : ℤ := gcd_c1 a b
t : ℤ := gcd_c2 a b
⊢ ↑d ∣ ↑(gcd a b)
Tactic:
have h3 : s * ↑a + t * ↑b = ↑(gcd a b) := gcd_lin_comb b a
State after:
d a b : ℕ
h1 : d ∣ a
h2 : d ∣ b
s : ℤ := gcd_c1 a b
t : ℤ := gcd_c2 a b
h3 : s * ↑a + t * ↑b = ↑(gcd a b)
⊢ ↑d ∣ ↑(gcd a b)

State before:
d a b : ℕ
h1 : d ∣ a
h2 : d ∣ b
s : ℤ := gcd_c1 a b
t : ℤ := gcd_c2 a b
h3 : s * ↑a + t * ↑b = ↑(gcd a b)
⊢ ↑d ∣ ↑(gcd a b)
Tactic:
rewrite [←h3]
State after:
d a b : ℕ
h1 : d ∣ a
h2 : d ∣ b
s : ℤ := gcd_c1 a b
t : ℤ := gcd_c2 a b
h3 : s * ↑a + t * ↑b = ↑(gcd a b)
⊢ ↑d ∣ s * ↑a + t * ↑b

State before:
d a b : ℕ
h1 : d ∣ a
h2 : d ∣ b
s : ℤ := gcd_c1 a b
t : ℤ := gcd_c2 a b
h3 : s * ↑a + t * ↑b = ↑(gcd a b)
⊢ ↑d ∣ s * ↑a + t * ↑b
Tactic:
obtain (j : Nat) (h4 : a = d * j) from h1
State after:
d a b : ℕ
h1 : d ∣ a
h2 : d ∣ b
s : ℤ := gcd_c1 a b
t : ℤ := gcd_c2 a b
h3 : s * ↑a + t * ↑b = ↑(gcd a b)
j : ℕ
h4 : a = d * j
⊢ ↑d ∣ s * ↑a + t * ↑b

State before:
d a b : ℕ
h1 : d ∣ a
h2 : d ∣ b
s : ℤ := gcd_c1 a b
t : ℤ := gcd_c2 a b
h3 : s * ↑a + t * ↑b = ↑(gcd a b)
j : ℕ
h4 : a = d * j
⊢ ↑d ∣ s * ↑a + t * ↑b
Tactic:
obtain (k : Nat) (h5 : b = d * k) from h2
State after:
d a b : ℕ
h1 : d ∣ a
h2 : d ∣ b
s : ℤ := gcd_c1 a b
t : ℤ := gcd_c2 a b
h3 : s * ↑a + t * ↑b = ↑(gcd a b)
j : ℕ
h4 : a = d * j
k : ℕ
h5 : b = d * k
⊢ ↑d ∣ s * ↑a + t * ↑b

State before:
d a b : ℕ
h1 : d ∣ a
h2 : d ∣ b
s : ℤ := gcd_c1 a b
t : ℤ := gcd_c2 a b
h3 : s * ↑a + t * ↑b = ↑(gcd a b)
j : ℕ
h4 : a = d * j
k : ℕ
h5 : b = d * k
⊢ ↑d ∣ s * ↑a + t * ↑b
Tactic:
rewrite [h4, h5, Nat.cast_mul, Nat.cast_mul]
State after:
d a b : ℕ
h1 : d ∣ a
h2 : d ∣ b
s : ℤ := gcd_c1 a b
t : ℤ := gcd_c2 a b
h3 : s * ↑a + t * ↑b = ↑(gcd a b)
j : ℕ
h4 : a = d * j
k : ℕ
h5 : b = d * k
⊢ ↑d ∣ s * (↑d * ↑j) + t * (↑d * ↑k)

State before:
d a b : ℕ
h1 : d ∣ a
h2 : d ∣ b
s : ℤ := gcd_c1 a b
t : ℤ := gcd_c2 a b
h3 : s * ↑a + t * ↑b = ↑(gcd a b)
j : ℕ
h4 : a = d * j
k : ℕ
h5 : b = d * k
⊢ ↑d ∣ s * (↑d * ↑j) + t * (↑d * ↑k)
Tactic:
define
State after:
d a b : ℕ
h1 : d ∣ a
h2 : d ∣ b
s : ℤ := gcd_c1 a b
t : ℤ := gcd_c2 a b
h3 : s * ↑a + t * ↑b = ↑(gcd a b)
j : ℕ
h4 : a = d * j
k : ℕ
h5 : b = d * k
⊢ ∃ c, s * (↑d * ↑j) + t * (↑d * ↑k) = ↑d * c

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

State before:
d a b : ℕ
h1 : d ∣ a
h2 : d ∣ b
s : ℤ := gcd_c1 a b
t : ℤ := gcd_c2 a b
h3 : s * ↑a + t * ↑b = ↑(gcd a b)
j : ℕ
h4 : a = d * j
k : ℕ
h5 : b = d * k
⊢ s * (↑d * ↑j) + t * (↑d * ↑k) = ↑d * (s * ↑j + t * ↑k)
Tactic:
ring
State after:
no goals