Theorem: eqn_solvable_divides (PnP2023/Lec_03_08/Diaphontine.lean)

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

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

State before:
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 h₁
a b c x y : ℤ
h : a * x + b * y = c
⊢ ↑(Int.gcd a b) ∣ a * x

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

State before:
case 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 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