case intro.intro.intro.intro.intro.intro
a b : ℕ+
left✝² : gcdW a b * gcdZ a b = succPNat (gcdX a b * gcdY a b)
h₁ : a = gcdA' a b * gcdD a b
h₂ : b = gcdB' a b * gcdD a b
left✝¹ : gcdZ a b * gcdA' a b = succPNat (gcdX a b * ↑(gcdB' a b))
left✝ : gcdW a b * gcdB' a b = succPNat (gcdY a b * ↑(gcdA' a b))
h₅ : ↑(gcdZ a b) * ↑a = gcdX a b * ↑b + ↑(gcdD a b)
right✝ : ↑(gcdW a b) * ↑b = gcdY a b * ↑a + ↑(gcdD a b)
⊢ gcdD a b = gcd a b
a b : ℕ+
⊢ gcdD a b = gcd a b
rcases gcd_props a b with ⟨_, h₁, h₂, _, _, h₅, _⟩
case intro.intro.intro.intro.intro.intro.a
a b : ℕ+
left✝² : gcdW a b * gcdZ a b = succPNat (gcdX a b * gcdY a b)
h₁ : a = gcdA' a b * gcdD a b
h₂ : b = gcdB' a b * gcdD a b
left✝¹ : gcdZ a b * gcdA' a b = succPNat (gcdX a b * ↑(gcdB' a b))
left✝ : gcdW a b * gcdB' a b = succPNat (gcdY a b * ↑(gcdA' a b))
h₅ : ↑(gcdZ a b) * ↑a = gcdX a b * ↑b + ↑(gcdD a b)
right✝ : ↑(gcdW a b) * ↑b = gcdY a b * ↑a + ↑(gcdD a b)
⊢ gcdD a b ∣ gcd a b

case intro.intro.intro.intro.intro.intro.a
a b : ℕ+
left✝² : gcdW a b * gcdZ a b = succPNat (gcdX a b * gcdY a b)
h₁ : a = gcdA' a b * gcdD a b
h₂ : b = gcdB' a b * gcdD a b
left✝¹ : gcdZ a b * gcdA' a b = succPNat (gcdX a b * ↑(gcdB' a b))
left✝ : gcdW a b * gcdB' a b = succPNat (gcdY a b * ↑(gcdA' a b))
h₅ : ↑(gcdZ a b) * ↑a = gcdX a b * ↑b + ↑(gcdD a b)
right✝ : ↑(gcdW a b) * ↑b = gcdY a b * ↑a + ↑(gcdD a b)
⊢ gcd a b ∣ gcdD a b
case intro.intro.intro.intro.intro.intro
a b : ℕ+
left✝² : gcdW a b * gcdZ a b = succPNat (gcdX a b * gcdY a b)
h₁ : a = gcdA' a b * gcdD a b
h₂ : b = gcdB' a b * gcdD a b
left✝¹ : gcdZ a b * gcdA' a b = succPNat (gcdX a b * ↑(gcdB' a b))
left✝ : gcdW a b * gcdB' a b = succPNat (gcdY a b * ↑(gcdA' a b))
h₅ : ↑(gcdZ a b) * ↑a = gcdX a b * ↑b + ↑(gcdD a b)
right✝ : ↑(gcdW a b) * ↑b = gcdY a b * ↑a + ↑(gcdD a b)
⊢ gcdD a b = gcd a b
apply dvd_antisymm
case intro.intro.intro.intro.intro.intro.a.hm
a b : ℕ+
left✝² : gcdW a b * gcdZ a b = succPNat (gcdX a b * gcdY a b)
h₁ : a = gcdA' a b * gcdD a b
h₂ : b = gcdB' a b * gcdD a b
left✝¹ : gcdZ a b * gcdA' a b = succPNat (gcdX a b * ↑(gcdB' a b))
left✝ : gcdW a b * gcdB' a b = succPNat (gcdY a b * ↑(gcdA' a b))
h₅ : ↑(gcdZ a b) * ↑a = gcdX a b * ↑b + ↑(gcdD a b)
right✝ : ↑(gcdW a b) * ↑b = gcdY a b * ↑a + ↑(gcdD a b)
⊢ gcdD a b ∣ a

case intro.intro.intro.intro.intro.intro.a.hn
a b : ℕ+
left✝² : gcdW a b * gcdZ a b = succPNat (gcdX a b * gcdY a b)
h₁ : a = gcdA' a b * gcdD a b
h₂ : b = gcdB' a b * gcdD a b
left✝¹ : gcdZ a b * gcdA' a b = succPNat (gcdX a b * ↑(gcdB' a b))
left✝ : gcdW a b * gcdB' a b = succPNat (gcdY a b * ↑(gcdA' a b))
h₅ : ↑(gcdZ a b) * ↑a = gcdX a b * ↑b + ↑(gcdD a b)
right✝ : ↑(gcdW a b) * ↑b = gcdY a b * ↑a + ↑(gcdD a b)
⊢ gcdD a b ∣ b
case intro.intro.intro.intro.intro.intro.a
a b : ℕ+
left✝² : gcdW a b * gcdZ a b = succPNat (gcdX a b * gcdY a b)
h₁ : a = gcdA' a b * gcdD a b
h₂ : b = gcdB' a b * gcdD a b
left✝¹ : gcdZ a b * gcdA' a b = succPNat (gcdX a b * ↑(gcdB' a b))
left✝ : gcdW a b * gcdB' a b = succPNat (gcdY a b * ↑(gcdA' a b))
h₅ : ↑(gcdZ a b) * ↑a = gcdX a b * ↑b + ↑(gcdD a b)
right✝ : ↑(gcdW a b) * ↑b = gcdY a b * ↑a + ↑(gcdD a b)
⊢ gcdD a b ∣ gcd a b
apply dvd_gcd
case intro.intro.intro.intro.intro.intro.a.hn
a b : ℕ+
left✝² : gcdW a b * gcdZ a b = succPNat (gcdX a b * gcdY a b)
h₁ : a = gcdA' a b * gcdD a b
h₂ : b = gcdB' a b * gcdD a b
left✝¹ : gcdZ a b * gcdA' a b = succPNat (gcdX a b * ↑(gcdB' a b))
left✝ : gcdW a b * gcdB' a b = succPNat (gcdY a b * ↑(gcdA' a b))
h₅ : ↑(gcdZ a b) * ↑a = gcdX a b * ↑b + ↑(gcdD a b)
right✝ : ↑(gcdW a b) * ↑b = gcdY a b * ↑a + ↑(gcdD a b)
⊢ gcdD a b ∣ b
case intro.intro.intro.intro.intro.intro.a.hm
a b : ℕ+
left✝² : gcdW a b * gcdZ a b = succPNat (gcdX a b * gcdY a b)
h₁ : a = gcdA' a b * gcdD a b
h₂ : b = gcdB' a b * gcdD a b
left✝¹ : gcdZ a b * gcdA' a b = succPNat (gcdX a b * ↑(gcdB' a b))
left✝ : gcdW a b * gcdB' a b = succPNat (gcdY a b * ↑(gcdA' a b))
h₅ : ↑(gcdZ a b) * ↑a = gcdX a b * ↑b + ↑(gcdD a b)
right✝ : ↑(gcdW a b) * ↑b = gcdY a b * ↑a + ↑(gcdD a b)
⊢ gcdD a b ∣ a

case intro.intro.intro.intro.intro.intro.a.hn
a b : ℕ+
left✝² : gcdW a b * gcdZ a b = succPNat (gcdX a b * gcdY a b)
h₁ : a = gcdA' a b * gcdD a b
h₂ : b = gcdB' a b * gcdD a b
left✝¹ : gcdZ a b * gcdA' a b = succPNat (gcdX a b * ↑(gcdB' a b))
left✝ : gcdW a b * gcdB' a b = succPNat (gcdY a b * ↑(gcdA' a b))
h₅ : ↑(gcdZ a b) * ↑a = gcdX a b * ↑b + ↑(gcdD a b)
right✝ : ↑(gcdW a b) * ↑b = gcdY a b * ↑a + ↑(gcdD a b)
⊢ gcdD a b ∣ b
exact Dvd.intro (gcdA' a b) (h₁.trans (mul_comm _ _)).symm
no goals
case intro.intro.intro.intro.intro.intro.a.hn
a b : ℕ+
left✝² : gcdW a b * gcdZ a b = succPNat (gcdX a b * gcdY a b)
h₁ : a = gcdA' a b * gcdD a b
h₂ : b = gcdB' a b * gcdD a b
left✝¹ : gcdZ a b * gcdA' a b = succPNat (gcdX a b * ↑(gcdB' a b))
left✝ : gcdW a b * gcdB' a b = succPNat (gcdY a b * ↑(gcdA' a b))
h₅ : ↑(gcdZ a b) * ↑a = gcdX a b * ↑b + ↑(gcdD a b)
right✝ : ↑(gcdW a b) * ↑b = gcdY a b * ↑a + ↑(gcdD a b)
⊢ gcdD a b ∣ b
exact Dvd.intro (gcdB' a b) (h₂.trans (mul_comm _ _)).symm
case intro.intro.intro.intro.intro.intro.a
a b : ℕ+
left✝² : gcdW a b * gcdZ a b = succPNat (gcdX a b * gcdY a b)
h₁ : a = gcdA' a b * gcdD a b
h₂ : b = gcdB' a b * gcdD a b
left✝¹ : gcdZ a b * gcdA' a b = succPNat (gcdX a b * ↑(gcdB' a b))
left✝ : gcdW a b * gcdB' a b = succPNat (gcdY a b * ↑(gcdA' a b))
h₅ : ↑(gcdZ a b) * ↑a = gcdX a b * ↑b + ↑(gcdD a b)
right✝ : ↑(gcdW a b) * ↑b = gcdY a b * ↑a + ↑(gcdD a b)
h₇ : ↑(gcd a b) ∣ ↑(gcdZ a b) * ↑a
⊢ gcd a b ∣ gcdD a b
case intro.intro.intro.intro.intro.intro.a
a b : ℕ+
left✝² : gcdW a b * gcdZ a b = succPNat (gcdX a b * gcdY a b)
h₁ : a = gcdA' a b * gcdD a b
h₂ : b = gcdB' a b * gcdD a b
left✝¹ : gcdZ a b * gcdA' a b = succPNat (gcdX a b * ↑(gcdB' a b))
left✝ : gcdW a b * gcdB' a b = succPNat (gcdY a b * ↑(gcdA' a b))
h₅ : ↑(gcdZ a b) * ↑a = gcdX a b * ↑b + ↑(gcdD a b)
right✝ : ↑(gcdW a b) * ↑b = gcdY a b * ↑a + ↑(gcdD a b)
⊢ gcd a b ∣ gcdD a b
have h₇ : (gcd a b : ℕ) ∣ gcdZ a b * a := (Nat.gcd_dvd_left a b).trans (dvd_mul_left _ _)
case intro.intro.intro.intro.intro.intro.a
a b : ℕ+
left✝² : gcdW a b * gcdZ a b = succPNat (gcdX a b * gcdY a b)
h₁ : a = gcdA' a b * gcdD a b
h₂ : b = gcdB' a b * gcdD a b
left✝¹ : gcdZ a b * gcdA' a b = succPNat (gcdX a b * ↑(gcdB' a b))
left✝ : gcdW a b * gcdB' a b = succPNat (gcdY a b * ↑(gcdA' a b))
h₅ : ↑(gcdZ a b) * ↑a = gcdX a b * ↑b + ↑(gcdD a b)
right✝ : ↑(gcdW a b) * ↑b = gcdY a b * ↑a + ↑(gcdD a b)
h₇ : ↑(gcd a b) ∣ ↑(gcdZ a b) * ↑a
h₈ : ↑(gcd a b) ∣ gcdX a b * ↑b
⊢ gcd a b ∣ gcdD a b
case intro.intro.intro.intro.intro.intro.a
a b : ℕ+
left✝² : gcdW a b * gcdZ a b = succPNat (gcdX a b * gcdY a b)
h₁ : a = gcdA' a b * gcdD a b
h₂ : b = gcdB' a b * gcdD a b
left✝¹ : gcdZ a b * gcdA' a b = succPNat (gcdX a b * ↑(gcdB' a b))
left✝ : gcdW a b * gcdB' a b = succPNat (gcdY a b * ↑(gcdA' a b))
h₅ : ↑(gcdZ a b) * ↑a = gcdX a b * ↑b + ↑(gcdD a b)
right✝ : ↑(gcdW a b) * ↑b = gcdY a b * ↑a + ↑(gcdD a b)
h₇ : ↑(gcd a b) ∣ ↑(gcdZ a b) * ↑a
⊢ gcd a b ∣ gcdD a b
have h₈ : (gcd a b : ℕ) ∣ gcdX a b * b := (Nat.gcd_dvd_right a b).trans (dvd_mul_left _ _)
case intro.intro.intro.intro.intro.intro.a
a b : ℕ+
left✝² : gcdW a b * gcdZ a b = succPNat (gcdX a b * gcdY a b)
h₁ : a = gcdA' a b * gcdD a b
h₂ : b = gcdB' a b * gcdD a b
left✝¹ : gcdZ a b * gcdA' a b = succPNat (gcdX a b * ↑(gcdB' a b))
left✝ : gcdW a b * gcdB' a b = succPNat (gcdY a b * ↑(gcdA' a b))
h₅ : ↑(gcdZ a b) * ↑a = gcdX a b * ↑b + ↑(gcdD a b)
right✝ : ↑(gcdW a b) * ↑b = gcdY a b * ↑a + ↑(gcdD a b)
h₇ : ↑(gcd a b) ∣ gcdX a b * ↑b + ↑(gcdD a b)
h₈ : ↑(gcd a b) ∣ gcdX a b * ↑b
⊢ gcd a b ∣ gcdD a b
case intro.intro.intro.intro.intro.intro.a
a b : ℕ+
left✝² : gcdW a b * gcdZ a b = succPNat (gcdX a b * gcdY a b)
h₁ : a = gcdA' a b * gcdD a b
h₂ : b = gcdB' a b * gcdD a b
left✝¹ : gcdZ a b * gcdA' a b = succPNat (gcdX a b * ↑(gcdB' a b))
left✝ : gcdW a b * gcdB' a b = succPNat (gcdY a b * ↑(gcdA' a b))
h₅ : ↑(gcdZ a b) * ↑a = gcdX a b * ↑b + ↑(gcdD a b)
right✝ : ↑(gcdW a b) * ↑b = gcdY a b * ↑a + ↑(gcdD a b)
h₇ : ↑(gcd a b) ∣ ↑(gcdZ a b) * ↑a
h₈ : ↑(gcd a b) ∣ gcdX a b * ↑b
⊢ gcd a b ∣ gcdD a b
rw [h₅] at h₇
case intro.intro.intro.intro.intro.intro.a
a b : ℕ+
left✝² : gcdW a b * gcdZ a b = succPNat (gcdX a b * gcdY a b)
h₁ : a = gcdA' a b * gcdD a b
h₂ : b = gcdB' a b * gcdD a b
left✝¹ : gcdZ a b * gcdA' a b = succPNat (gcdX a b * ↑(gcdB' a b))
left✝ : gcdW a b * gcdB' a b = succPNat (gcdY a b * ↑(gcdA' a b))
h₅ : ↑(gcdZ a b) * ↑a = gcdX a b * ↑b + ↑(gcdD a b)
right✝ : ↑(gcdW a b) * ↑b = gcdY a b * ↑a + ↑(gcdD a b)
h₇ : ↑(gcd a b) ∣ gcdX a b * ↑b + ↑(gcdD a b)
h₈ : ↑(gcd a b) ∣ gcdX a b * ↑b
⊢ ↑(gcd a b) ∣ ↑(gcdD a b)
case intro.intro.intro.intro.intro.intro.a
a b : ℕ+
left✝² : gcdW a b * gcdZ a b = succPNat (gcdX a b * gcdY a b)
h₁ : a = gcdA' a b * gcdD a b
h₂ : b = gcdB' a b * gcdD a b
left✝¹ : gcdZ a b * gcdA' a b = succPNat (gcdX a b * ↑(gcdB' a b))
left✝ : gcdW a b * gcdB' a b = succPNat (gcdY a b * ↑(gcdA' a b))
h₅ : ↑(gcdZ a b) * ↑a = gcdX a b * ↑b + ↑(gcdD a b)
right✝ : ↑(gcdW a b) * ↑b = gcdY a b * ↑a + ↑(gcdD a b)
h₇ : ↑(gcd a b) ∣ gcdX a b * ↑b + ↑(gcdD a b)
h₈ : ↑(gcd a b) ∣ gcdX a b * ↑b
⊢ gcd a b ∣ gcdD a b
rw [dvd_iff]
no goals
case intro.intro.intro.intro.intro.intro.a
a b : ℕ+
left✝² : gcdW a b * gcdZ a b = succPNat (gcdX a b * gcdY a b)
h₁ : a = gcdA' a b * gcdD a b
h₂ : b = gcdB' a b * gcdD a b
left✝¹ : gcdZ a b * gcdA' a b = succPNat (gcdX a b * ↑(gcdB' a b))
left✝ : gcdW a b * gcdB' a b = succPNat (gcdY a b * ↑(gcdA' a b))
h₅ : ↑(gcdZ a b) * ↑a = gcdX a b * ↑b + ↑(gcdD a b)
right✝ : ↑(gcdW a b) * ↑b = gcdY a b * ↑a + ↑(gcdD a b)
h₇ : ↑(gcd a b) ∣ gcdX a b * ↑b + ↑(gcdD a b)
h₈ : ↑(gcd a b) ∣ gcdX a b * ↑b
⊢ ↑(gcd a b) ∣ ↑(gcdD a b)
exact (Nat.dvd_add_iff_right h₈).mpr h₇