Theorem: eqn_solvable_iff_divides_gcd (Lectures/WordProblem/Diophantine.lean)

State before:
a b c : ℤ
⊢ (∃ x y, a * x + b * y = c) ↔ ↑(Int.gcd a b) ∣ c
Tactic:
apply Iff.intro
State after:
case mp
a b c : ℤ
⊢ (∃ x y, a * x + b * y = c) → ↑(Int.gcd a b) ∣ c

case mpr
a b c : ℤ
⊢ ↑(Int.gcd a b) ∣ c → ∃ x y, a * x + b * y = c

State before:
case mp
a b c : ℤ
⊢ (∃ x y, a * x + b * y = c) → ↑(Int.gcd a b) ∣ c
Tactic:
intro ⟨x, y, h⟩
State after:
case mp
a b c x y : ℤ
h : a * x + b * y = c
⊢ ↑(Int.gcd a b) ∣ c

State before:
case mp
a b c x y : ℤ
h : a * x + b * y = c
⊢ ↑(Int.gcd a b) ∣ c
Tactic:
rw [← h]
State after:
case mp
a b c x y : ℤ
h : a * x + b * y = c
⊢ ↑(Int.gcd a b) ∣ a * x + b * y

State before:
case mp
a b c x y : ℤ
h : a * x + b * y = c
⊢ ↑(Int.gcd a b) ∣ a * x + b * y
Tactic:
apply dvd_add
State after:
case mp.h₁
a b c x y : ℤ
h : a * x + b * y = c
⊢ ↑(Int.gcd a b) ∣ a * x

case mp.h₂
a b c x y : ℤ
h : a * x + b * y = c
⊢ ↑(Int.gcd a b) ∣ b * y

State before:
case mp.h₁
a b c x y : ℤ
h : a * x + b * y = c
⊢ ↑(Int.gcd a b) ∣ a * x
Tactic:
trans a
State after:
a b c x y : ℤ
h : a * x + b * y = c
⊢ ↑(Int.gcd a b) ∣ a

a b c x y : ℤ
h : a * x + b * y = c
⊢ a ∣ a * x

State before:
a b c x y : ℤ
h : a * x + b * y = c
⊢ ↑(Int.gcd a b) ∣ a
Tactic:
apply Int.gcd_dvd_left
State after:
no goals

State before:
a b c x y : ℤ
h : a * x + b * y = c
⊢ a ∣ a * x
Tactic:
apply Int.dvd_mul_right
State after:
no goals

State before:
case mp.h₂
a b c x y : ℤ
h : a * x + b * y = c
⊢ ↑(Int.gcd a b) ∣ b * y
Tactic:
trans b
State after:
a b c x y : ℤ
h : a * x + b * y = c
⊢ ↑(Int.gcd a b) ∣ b

a b c x y : ℤ
h : a * x + b * y = c
⊢ b ∣ b * y

State before:
a b c x y : ℤ
h : a * x + b * y = c
⊢ ↑(Int.gcd a b) ∣ b
Tactic:
apply Int.gcd_dvd_right
State after:
no goals

State before:
a b c x y : ℤ
h : a * x + b * y = c
⊢ b ∣ b * y
Tactic:
apply Int.dvd_mul_right
State after:
no goals

State before:
case mpr
a b c : ℤ
⊢ ↑(Int.gcd a b) ∣ c → ∃ x y, a * x + b * y = c
Tactic:
intro h
State after:
case mpr
a b c : ℤ
h : ↑(Int.gcd a b) ∣ c
⊢ ∃ x y, a * x + b * y = c

State before:
case mpr
a b c : ℤ
h : ↑(Int.gcd a b) ∣ c
⊢ ∃ x y, a * x + b * y = c
Tactic:
let d := c / Int.gcd a b
State after:
case mpr
a b c : ℤ
h : ↑(Int.gcd a b) ∣ c
d : ℤ := c / ↑(Int.gcd a b)
⊢ ∃ x y, a * x + b * y = c

State before:
case mpr
a b c : ℤ
h : ↑(Int.gcd a b) ∣ c
d : ℤ := c / ↑(Int.gcd a b)
⊢ ∃ x y, a * x + b * y = c
Tactic:
let h' : Int.gcd a b * d = c := by 
  apply Int.mul_ediv_cancel_of_emod_eq_zero
  apply Int.emod_eq_zero_of_dvd
  assumption
State after:
case mpr
a b c : ℤ
h : ↑(Int.gcd a b) ∣ c
d : ℤ := c / ↑(Int.gcd a b)
h' : ↑(Int.gcd a b) * d = c := Int.mul_ediv_cancel_of_emod_eq_zero (Int.emod_eq_zero_of_dvd h)
⊢ ∃ x y, a * x + b * y = c

State before:
case mpr
a b c : ℤ
h : ↑(Int.gcd a b) ∣ c
d : ℤ := c / ↑(Int.gcd a b)
h' : ↑(Int.gcd a b) * d = c := Int.mul_ediv_cancel_of_emod_eq_zero (Int.emod_eq_zero_of_dvd h)
⊢ ∃ x y, a * x + b * y = c
Tactic:
use d * (Int.gcdA a b), d * (Int.gcdB a b)
State after:
case h
a b c : ℤ
h : ↑(Int.gcd a b) ∣ c
d : ℤ := c / ↑(Int.gcd a b)
h' : ↑(Int.gcd a b) * d = c := Int.mul_ediv_cancel_of_emod_eq_zero (Int.emod_eq_zero_of_dvd h)
⊢ a * (d * Int.gcdA a b) + b * (d * Int.gcdB a b) = c

State before:
case h
a b c : ℤ
h : ↑(Int.gcd a b) ∣ c
d : ℤ := c / ↑(Int.gcd a b)
h' : ↑(Int.gcd a b) * d = c := Int.mul_ediv_cancel_of_emod_eq_zero (Int.emod_eq_zero_of_dvd h)
⊢ a * (d * Int.gcdA a b) + b * (d * Int.gcdB a b) = c
Tactic:
rw [← h', Int.gcd_eq_gcd_ab]
State after:
case h
a b c : ℤ
h : ↑(Int.gcd a b) ∣ c
d : ℤ := c / ↑(Int.gcd a b)
h' : ↑(Int.gcd a b) * d = c := Int.mul_ediv_cancel_of_emod_eq_zero (Int.emod_eq_zero_of_dvd h)
⊢ a * (d * Int.gcdA a b) + b * (d * Int.gcdB a b) = (a * Int.gcdA a b + b * Int.gcdB a b) * d

State before:
case h
a b c : ℤ
h : ↑(Int.gcd a b) ∣ c
d : ℤ := c / ↑(Int.gcd a b)
h' : ↑(Int.gcd a b) * d = c := Int.mul_ediv_cancel_of_emod_eq_zero (Int.emod_eq_zero_of_dvd h)
⊢ a * (d * Int.gcdA a b) + b * (d * Int.gcdB a b) = (a * Int.gcdA a b + b * Int.gcdB a b) * d
Tactic:
linarith
State after:
no goals

State before:
a b c : ℤ
h : ↑(Int.gcd a b) ∣ c
d : ℤ := c / ↑(Int.gcd a b)
⊢ ↑(Int.gcd a b) * d = c
Tactic:
apply Int.mul_ediv_cancel_of_emod_eq_zero
State after:
case H
a b c : ℤ
h : ↑(Int.gcd a b) ∣ c
d : ℤ := c / ↑(Int.gcd a b)
⊢ c % ↑(Int.gcd a b) = 0

State before:
case H
a b c : ℤ
h : ↑(Int.gcd a b) ∣ c
d : ℤ := c / ↑(Int.gcd a b)
⊢ c % ↑(Int.gcd a b) = 0
Tactic:
apply Int.emod_eq_zero_of_dvd
State after:
case H.a
a b c : ℤ
h : ↑(Int.gcd a b) ∣ c
d : ℤ := c / ↑(Int.gcd a b)
⊢ ↑(Int.gcd a b) ∣ c

State before:
case H.a
a b c : ℤ
h : ↑(Int.gcd a b) ∣ c
d : ℤ := c / ↑(Int.gcd a b)
⊢ ↑(Int.gcd a b) ∣ c
Tactic:
assumption
State after:
no goals