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

State before:
⊢ ∀ (b a : ℕ), gcd_c1 a b * ↑a + gcd_c2 a b * ↑b = ↑(gcd a b)
Tactic:
by_strong_induc
State after:
⊢ ∀ (b : ℕ),
    (∀ b_1 < b, ∀ (a : ℕ), gcd_c1 a b_1 * ↑a + gcd_c2 a b_1 * ↑b_1 = ↑(gcd a b_1)) →
      ∀ (a : ℕ), gcd_c1 a b * ↑a + gcd_c2 a b * ↑b = ↑(gcd a b)

State before:
⊢ ∀ (b : ℕ),
    (∀ b_1 < b, ∀ (a : ℕ), gcd_c1 a b_1 * ↑a + gcd_c2 a b_1 * ↑b_1 = ↑(gcd a b_1)) →
      ∀ (a : ℕ), gcd_c1 a b * ↑a + gcd_c2 a b * ↑b = ↑(gcd a b)
Tactic:
fix b : Nat
State after:
b : ℕ
⊢ (∀ b_1 < b, ∀ (a : ℕ), gcd_c1 a b_1 * ↑a + gcd_c2 a b_1 * ↑b_1 = ↑(gcd a b_1)) →
    ∀ (a : ℕ), gcd_c1 a b * ↑a + gcd_c2 a b * ↑b = ↑(gcd a b)

State before:
b : ℕ
⊢ (∀ b_1 < b, ∀ (a : ℕ), gcd_c1 a b_1 * ↑a + gcd_c2 a b_1 * ↑b_1 = ↑(gcd a b_1)) →
    ∀ (a : ℕ), gcd_c1 a b * ↑a + gcd_c2 a b * ↑b = ↑(gcd a b)
Tactic:
assume ih : ∀ b_1 < b, ∀ (a : Nat),
  (gcd_c1 a b_1) * ↑a + (gcd_c2 a b_1) * ↑b_1 = ↑(gcd a b_1)
State after:
b : ℕ
ih : ∀ b_1 < b, ∀ (a : ℕ), gcd_c1 a b_1 * ↑a + gcd_c2 a b_1 * ↑b_1 = ↑(gcd a b_1)
⊢ ∀ (a : ℕ), gcd_c1 a b * ↑a + gcd_c2 a b * ↑b = ↑(gcd a b)

State before:
b : ℕ
ih : ∀ b_1 < b, ∀ (a : ℕ), gcd_c1 a b_1 * ↑a + gcd_c2 a b_1 * ↑b_1 = ↑(gcd a b_1)
⊢ ∀ (a : ℕ), gcd_c1 a b * ↑a + gcd_c2 a b * ↑b = ↑(gcd a b)
Tactic:
fix a : Nat
State after:
b : ℕ
ih : ∀ b_1 < b, ∀ (a : ℕ), gcd_c1 a b_1 * ↑a + gcd_c2 a b_1 * ↑b_1 = ↑(gcd a b_1)
a : ℕ
⊢ gcd_c1 a b * ↑a + gcd_c2 a b * ↑b = ↑(gcd a b)

State before:
b : ℕ
ih : ∀ b_1 < b, ∀ (a : ℕ), gcd_c1 a b_1 * ↑a + gcd_c2 a b_1 * ↑b_1 = ↑(gcd a b_1)
a : ℕ
⊢ gcd_c1 a b * ↑a + gcd_c2 a b * ↑b = ↑(gcd a b)
Tactic:
by_cases h1 : b = 0
State after:
case pos
b : ℕ
ih : ∀ b_1 < b, ∀ (a : ℕ), gcd_c1 a b_1 * ↑a + gcd_c2 a b_1 * ↑b_1 = ↑(gcd a b_1)
a : ℕ
h1 : b = 0
⊢ gcd_c1 a b * ↑a + gcd_c2 a b * ↑b = ↑(gcd a b)

case neg
b : ℕ
ih : ∀ b_1 < b, ∀ (a : ℕ), gcd_c1 a b_1 * ↑a + gcd_c2 a b_1 * ↑b_1 = ↑(gcd a b_1)
a : ℕ
h1 : ¬b = 0
⊢ gcd_c1 a b * ↑a + gcd_c2 a b * ↑b = ↑(gcd a b)

State before:
case pos
b : ℕ
ih : ∀ b_1 < b, ∀ (a : ℕ), gcd_c1 a b_1 * ↑a + gcd_c2 a b_1 * ↑b_1 = ↑(gcd a b_1)
a : ℕ
h1 : b = 0
⊢ gcd_c1 a b * ↑a + gcd_c2 a b * ↑b = ↑(gcd a b)
Tactic:
rewrite [h1, gcd_c1_base, gcd_c2_base, gcd_base]
State after:
case pos
b : ℕ
ih : ∀ b_1 < b, ∀ (a : ℕ), gcd_c1 a b_1 * ↑a + gcd_c2 a b_1 * ↑b_1 = ↑(gcd a b_1)
a : ℕ
h1 : b = 0
⊢ 1 * ↑a + 0 * ↑0 = ↑a

State before:
case pos
b : ℕ
ih : ∀ b_1 < b, ∀ (a : ℕ), gcd_c1 a b_1 * ↑a + gcd_c2 a b_1 * ↑b_1 = ↑(gcd a b_1)
a : ℕ
h1 : b = 0
⊢ 1 * ↑a + 0 * ↑0 = ↑a
Tactic:
ring
State after:
no goals

State before:
case neg
b : ℕ
ih : ∀ b_1 < b, ∀ (a : ℕ), gcd_c1 a b_1 * ↑a + gcd_c2 a b_1 * ↑b_1 = ↑(gcd a b_1)
a : ℕ
h1 : ¬b = 0
⊢ gcd_c1 a b * ↑a + gcd_c2 a b * ↑b = ↑(gcd a b)
Tactic:
rewrite [gcd_c1_nonzero a h1, gcd_c2_nonzero a h1, gcd_nonzero a h1]
State after:
case neg
b : ℕ
ih : ∀ b_1 < b, ∀ (a : ℕ), gcd_c1 a b_1 * ↑a + gcd_c2 a b_1 * ↑b_1 = ↑(gcd a b_1)
a : ℕ
h1 : ¬b = 0
⊢ gcd_c2 b (a % b) * ↑a + (gcd_c1 b (a % b) - gcd_c2 b (a % b) * ↑(a / b)) * ↑b = ↑(gcd b (a % b))

State before:
case neg
b : ℕ
ih : ∀ b_1 < b, ∀ (a : ℕ), gcd_c1 a b_1 * ↑a + gcd_c2 a b_1 * ↑b_1 = ↑(gcd a b_1)
a : ℕ
h1 : ¬b = 0
⊢ gcd_c2 b (a % b) * ↑a + (gcd_c1 b (a % b) - gcd_c2 b (a % b) * ↑(a / b)) * ↑b = ↑(gcd b (a % b))
Tactic:
set r : Nat := a % b
State after:
case neg
b : ℕ
ih : ∀ b_1 < b, ∀ (a : ℕ), gcd_c1 a b_1 * ↑a + gcd_c2 a b_1 * ↑b_1 = ↑(gcd a b_1)
a : ℕ
h1 : ¬b = 0
r : ℕ := a % b
⊢ gcd_c2 b r * ↑a + (gcd_c1 b r - gcd_c2 b r * ↑(a / b)) * ↑b = ↑(gcd b r)

State before:
case neg
b : ℕ
ih : ∀ b_1 < b, ∀ (a : ℕ), gcd_c1 a b_1 * ↑a + gcd_c2 a b_1 * ↑b_1 = ↑(gcd a b_1)
a : ℕ
h1 : ¬b = 0
r : ℕ := a % b
⊢ gcd_c2 b r * ↑a + (gcd_c1 b r - gcd_c2 b r * ↑(a / b)) * ↑b = ↑(gcd b r)
Tactic:
set q : Nat := a / b
State after:
case neg
b : ℕ
ih : ∀ b_1 < b, ∀ (a : ℕ), gcd_c1 a b_1 * ↑a + gcd_c2 a b_1 * ↑b_1 = ↑(gcd a b_1)
a : ℕ
h1 : ¬b = 0
r : ℕ := a % b
q : ℕ := a / b
⊢ gcd_c2 b r * ↑a + (gcd_c1 b r - gcd_c2 b r * ↑q) * ↑b = ↑(gcd b r)

State before:
case neg
b : ℕ
ih : ∀ b_1 < b, ∀ (a : ℕ), gcd_c1 a b_1 * ↑a + gcd_c2 a b_1 * ↑b_1 = ↑(gcd a b_1)
a : ℕ
h1 : ¬b = 0
r : ℕ := a % b
q : ℕ := a / b
⊢ gcd_c2 b r * ↑a + (gcd_c1 b r - gcd_c2 b r * ↑q) * ↑b = ↑(gcd b r)
Tactic:
set s : Int := gcd_c1 b r
State after:
case neg
b : ℕ
ih : ∀ b_1 < b, ∀ (a : ℕ), gcd_c1 a b_1 * ↑a + gcd_c2 a b_1 * ↑b_1 = ↑(gcd a b_1)
a : ℕ
h1 : ¬b = 0
r : ℕ := a % b
q : ℕ := a / b
s : ℤ := gcd_c1 b r
⊢ gcd_c2 b r * ↑a + (s - gcd_c2 b r * ↑q) * ↑b = ↑(gcd b r)

State before:
case neg
b : ℕ
ih : ∀ b_1 < b, ∀ (a : ℕ), gcd_c1 a b_1 * ↑a + gcd_c2 a b_1 * ↑b_1 = ↑(gcd a b_1)
a : ℕ
h1 : ¬b = 0
r : ℕ := a % b
q : ℕ := a / b
s : ℤ := gcd_c1 b r
⊢ gcd_c2 b r * ↑a + (s - gcd_c2 b r * ↑q) * ↑b = ↑(gcd b r)
Tactic:
set t : Int := gcd_c2 b r
State after:
case neg
b : ℕ
ih : ∀ b_1 < b, ∀ (a : ℕ), gcd_c1 a b_1 * ↑a + gcd_c2 a b_1 * ↑b_1 = ↑(gcd a b_1)
a : ℕ
h1 : ¬b = 0
r : ℕ := a % b
q : ℕ := a / b
s : ℤ := gcd_c1 b r
t : ℤ := gcd_c2 b r
⊢ t * ↑a + (s - t * ↑q) * ↑b = ↑(gcd b r)

State before:
case neg
b : ℕ
ih : ∀ b_1 < b, ∀ (a : ℕ), gcd_c1 a b_1 * ↑a + gcd_c2 a b_1 * ↑b_1 = ↑(gcd a b_1)
a : ℕ
h1 : ¬b = 0
r : ℕ := a % b
q : ℕ := a / b
s : ℤ := gcd_c1 b r
t : ℤ := gcd_c2 b r
⊢ t * ↑a + (s - t * ↑q) * ↑b = ↑(gcd b r)
Tactic:
have h2 : r < b := mod_nonzero_lt a h1
State after:
case neg
b : ℕ
ih : ∀ b_1 < b, ∀ (a : ℕ), gcd_c1 a b_1 * ↑a + gcd_c2 a b_1 * ↑b_1 = ↑(gcd a b_1)
a : ℕ
h1 : ¬b = 0
r : ℕ := a % b
q : ℕ := a / b
s : ℤ := gcd_c1 b r
t : ℤ := gcd_c2 b r
h2 : r < b
⊢ t * ↑a + (s - t * ↑q) * ↑b = ↑(gcd b r)

State before:
case neg
b : ℕ
ih : ∀ b_1 < b, ∀ (a : ℕ), gcd_c1 a b_1 * ↑a + gcd_c2 a b_1 * ↑b_1 = ↑(gcd a b_1)
a : ℕ
h1 : ¬b = 0
r : ℕ := a % b
q : ℕ := a / b
s : ℤ := gcd_c1 b r
t : ℤ := gcd_c2 b r
h2 : r < b
⊢ t * ↑a + (s - t * ↑q) * ↑b = ↑(gcd b r)
Tactic:
have h3 : s * ↑b + t * ↑r = ↑(gcd b r) := ih r h2 b
State after:
case neg
b : ℕ
ih : ∀ b_1 < b, ∀ (a : ℕ), gcd_c1 a b_1 * ↑a + gcd_c2 a b_1 * ↑b_1 = ↑(gcd a b_1)
a : ℕ
h1 : ¬b = 0
r : ℕ := a % b
q : ℕ := a / b
s : ℤ := gcd_c1 b r
t : ℤ := gcd_c2 b r
h2 : r < b
h3 : s * ↑b + t * ↑r = ↑(gcd b r)
⊢ t * ↑a + (s - t * ↑q) * ↑b = ↑(gcd b r)

State before:
case neg
b : ℕ
ih : ∀ b_1 < b, ∀ (a : ℕ), gcd_c1 a b_1 * ↑a + gcd_c2 a b_1 * ↑b_1 = ↑(gcd a b_1)
a : ℕ
h1 : ¬b = 0
r : ℕ := a % b
q : ℕ := a / b
s : ℤ := gcd_c1 b r
t : ℤ := gcd_c2 b r
h2 : r < b
h3 : s * ↑b + t * ↑r = ↑(gcd b r)
⊢ t * ↑a + (s - t * ↑q) * ↑b = ↑(gcd b r)
Tactic:
have h4 : b * q + r = a := Nat.div_add_mod a b
State after:
case neg
b : ℕ
ih : ∀ b_1 < b, ∀ (a : ℕ), gcd_c1 a b_1 * ↑a + gcd_c2 a b_1 * ↑b_1 = ↑(gcd a b_1)
a : ℕ
h1 : ¬b = 0
r : ℕ := a % b
q : ℕ := a / b
s : ℤ := gcd_c1 b r
t : ℤ := gcd_c2 b r
h2 : r < b
h3 : s * ↑b + t * ↑r = ↑(gcd b r)
h4 : b * q + r = a
⊢ t * ↑a + (s - t * ↑q) * ↑b = ↑(gcd b r)

State before:
case neg
b : ℕ
ih : ∀ b_1 < b, ∀ (a : ℕ), gcd_c1 a b_1 * ↑a + gcd_c2 a b_1 * ↑b_1 = ↑(gcd a b_1)
a : ℕ
h1 : ¬b = 0
r : ℕ := a % b
q : ℕ := a / b
s : ℤ := gcd_c1 b r
t : ℤ := gcd_c2 b r
h2 : r < b
h3 : s * ↑b + t * ↑r = ↑(gcd b r)
h4 : b * q + r = a
⊢ t * ↑a + (s - t * ↑q) * ↑b = ↑(gcd b r)
Tactic:
rewrite [←h3, ←h4]
State after:
case neg
b : ℕ
ih : ∀ b_1 < b, ∀ (a : ℕ), gcd_c1 a b_1 * ↑a + gcd_c2 a b_1 * ↑b_1 = ↑(gcd a b_1)
a : ℕ
h1 : ¬b = 0
r : ℕ := a % b
q : ℕ := a / b
s : ℤ := gcd_c1 b r
t : ℤ := gcd_c2 b r
h2 : r < b
h3 : s * ↑b + t * ↑r = ↑(gcd b r)
h4 : b * q + r = a
⊢ t * ↑(b * q + r) + (s - t * ↑q) * ↑b = s * ↑b + t * ↑r

State before:
case neg
b : ℕ
ih : ∀ b_1 < b, ∀ (a : ℕ), gcd_c1 a b_1 * ↑a + gcd_c2 a b_1 * ↑b_1 = ↑(gcd a b_1)
a : ℕ
h1 : ¬b = 0
r : ℕ := a % b
q : ℕ := a / b
s : ℤ := gcd_c1 b r
t : ℤ := gcd_c2 b r
h2 : r < b
h3 : s * ↑b + t * ↑r = ↑(gcd b r)
h4 : b * q + r = a
⊢ t * ↑(b * q + r) + (s - t * ↑q) * ↑b = s * ↑b + t * ↑r
Tactic:
rewrite [Nat.cast_add, Nat.cast_mul]
State after:
case neg
b : ℕ
ih : ∀ b_1 < b, ∀ (a : ℕ), gcd_c1 a b_1 * ↑a + gcd_c2 a b_1 * ↑b_1 = ↑(gcd a b_1)
a : ℕ
h1 : ¬b = 0
r : ℕ := a % b
q : ℕ := a / b
s : ℤ := gcd_c1 b r
t : ℤ := gcd_c2 b r
h2 : r < b
h3 : s * ↑b + t * ↑r = ↑(gcd b r)
h4 : b * q + r = a
⊢ t * (↑b * ↑q + ↑r) + (s - t * ↑q) * ↑b = s * ↑b + t * ↑r

State before:
case neg
b : ℕ
ih : ∀ b_1 < b, ∀ (a : ℕ), gcd_c1 a b_1 * ↑a + gcd_c2 a b_1 * ↑b_1 = ↑(gcd a b_1)
a : ℕ
h1 : ¬b = 0
r : ℕ := a % b
q : ℕ := a / b
s : ℤ := gcd_c1 b r
t : ℤ := gcd_c2 b r
h2 : r < b
h3 : s * ↑b + t * ↑r = ↑(gcd b r)
h4 : b * q + r = a
⊢ t * (↑b * ↑q + ↑r) + (s - t * ↑q) * ↑b = s * ↑b + t * ↑r
Tactic:
ring
State after:
no goals