u : XgcdType
hr : r u ≠ 0
ha : r u + ↑(b u) * q u = ↑(a u) := rq_eq u
⊢ v (step u) = Prod.swap (v u)
u : XgcdType
hr : r u ≠ 0
⊢ v (step u) = Prod.swap (v u)
let ha : u.r + u.b * u.q = u.a := u.rq_eq
u : XgcdType
hr✝ : r u ≠ 0
ha : r u + ↑(b u) * q u = ↑(a u) := rq_eq u
hr : r u - 1 + 1 = r u := Eq.trans (add_comm (r u - 1) 1) (add_tsub_cancel_of_le (Nat.pos_of_ne_zero hr✝))
⊢ v (step u) = Prod.swap (v u)
u : XgcdType
hr : r u ≠ 0
ha : r u + ↑(b u) * q u = ↑(a u) := rq_eq u
⊢ v (step u) = Prod.swap (v u)
let hr : u.r - 1 + 1 = u.r := (add_comm _ 1).trans (add_tsub_cancel_of_le (Nat.pos_of_ne_zero hr))
case h₁
u : XgcdType
hr✝ : r u ≠ 0
ha : r u + ↑(b u) * q u = ↑(a u) := rq_eq u
hr : r u - 1 + 1 = r u := Eq.trans (add_comm (r u - 1) 1) (add_tsub_cancel_of_le (Nat.pos_of_ne_zero hr✝))
⊢ (v (step u)).fst = (Prod.swap (v u)).fst

case h₂
u : XgcdType
hr✝ : r u ≠ 0
ha : r u + ↑(b u) * q u = ↑(a u) := rq_eq u
hr : r u - 1 + 1 = r u := Eq.trans (add_comm (r u - 1) 1) (add_tsub_cancel_of_le (Nat.pos_of_ne_zero hr✝))
⊢ (v (step u)).snd = (Prod.swap (v u)).snd
u : XgcdType
hr✝ : r u ≠ 0
ha : r u + ↑(b u) * q u = ↑(a u) := rq_eq u
hr : r u - 1 + 1 = r u := Eq.trans (add_comm (r u - 1) 1) (add_tsub_cancel_of_le (Nat.pos_of_ne_zero hr✝))
⊢ v (step u) = Prod.swap (v u)
ext
case h₁
u : XgcdType
hr✝ : r u ≠ 0
ha : r u + ↑(b u) * q u = ↑(a u) := rq_eq u
hr : r u - 1 + 1 = r u := Eq.trans (add_comm (r u - 1) 1) (add_tsub_cancel_of_le (Nat.pos_of_ne_zero hr✝))
⊢ (u.y * q u + ↑(z u)) * ↑(b u) + u.y * (r u - 1 + 1) = u.y * ↑(a u) + ↑(z u) * ↑(b u)
case h₁
u : XgcdType
hr✝ : r u ≠ 0
ha : r u + ↑(b u) * q u = ↑(a u) := rq_eq u
hr : r u - 1 + 1 = r u := Eq.trans (add_comm (r u - 1) 1) (add_tsub_cancel_of_le (Nat.pos_of_ne_zero hr✝))
⊢ (v (step u)).fst = (Prod.swap (v u)).fst
change ((u.y * u.q + u.z) * u.b + u.y * (u.r - 1 + 1) : ℕ) = u.y * u.a + u.z * u.b
case h₁
u : XgcdType
hr✝ : r u ≠ 0
ha : r u + ↑(b u) * q u = ↑(a u) := rq_eq u
hr : r u - 1 + 1 = r u := Eq.trans (add_comm (r u - 1) 1) (add_tsub_cancel_of_le (Nat.pos_of_ne_zero hr✝))
⊢ (u.y * q u + ↑(z u)) * ↑(b u) + u.y * r u = u.y * (r u + ↑(b u) * q u) + ↑(z u) * ↑(b u)
case h₁
u : XgcdType
hr✝ : r u ≠ 0
ha : r u + ↑(b u) * q u = ↑(a u) := rq_eq u
hr : r u - 1 + 1 = r u := Eq.trans (add_comm (r u - 1) 1) (add_tsub_cancel_of_le (Nat.pos_of_ne_zero hr✝))
⊢ (u.y * q u + ↑(z u)) * ↑(b u) + u.y * (r u - 1 + 1) = u.y * ↑(a u) + ↑(z u) * ↑(b u)
rw [← ha, hr]
no goals
case h₁
u : XgcdType
hr✝ : r u ≠ 0
ha : r u + ↑(b u) * q u = ↑(a u) := rq_eq u
hr : r u - 1 + 1 = r u := Eq.trans (add_comm (r u - 1) 1) (add_tsub_cancel_of_le (Nat.pos_of_ne_zero hr✝))
⊢ (u.y * q u + ↑(z u)) * ↑(b u) + u.y * r u = u.y * (r u + ↑(b u) * q u) + ↑(z u) * ↑(b u)
ring
case h₂
u : XgcdType
hr✝ : r u ≠ 0
ha : r u + ↑(b u) * q u = ↑(a u) := rq_eq u
hr : r u - 1 + 1 = r u := Eq.trans (add_comm (r u - 1) 1) (add_tsub_cancel_of_le (Nat.pos_of_ne_zero hr✝))
⊢ (↑(w u) * q u + u.x) * ↑(b u) + ↑(w u) * (r u - 1 + 1) = ↑(w u) * ↑(a u) + u.x * ↑(b u)
case h₂
u : XgcdType
hr✝ : r u ≠ 0
ha : r u + ↑(b u) * q u = ↑(a u) := rq_eq u
hr : r u - 1 + 1 = r u := Eq.trans (add_comm (r u - 1) 1) (add_tsub_cancel_of_le (Nat.pos_of_ne_zero hr✝))
⊢ (v (step u)).snd = (Prod.swap (v u)).snd
change ((u.w * u.q + u.x) * u.b + u.w * (u.r - 1 + 1) : ℕ) = u.w * u.a + u.x * u.b
case h₂
u : XgcdType
hr✝ : r u ≠ 0
ha : r u + ↑(b u) * q u = ↑(a u) := rq_eq u
hr : r u - 1 + 1 = r u := Eq.trans (add_comm (r u - 1) 1) (add_tsub_cancel_of_le (Nat.pos_of_ne_zero hr✝))
⊢ (↑(w u) * q u + u.x) * ↑(b u) + ↑(w u) * r u = ↑(w u) * (r u + ↑(b u) * q u) + u.x * ↑(b u)
case h₂
u : XgcdType
hr✝ : r u ≠ 0
ha : r u + ↑(b u) * q u = ↑(a u) := rq_eq u
hr : r u - 1 + 1 = r u := Eq.trans (add_comm (r u - 1) 1) (add_tsub_cancel_of_le (Nat.pos_of_ne_zero hr✝))
⊢ (↑(w u) * q u + u.x) * ↑(b u) + ↑(w u) * (r u - 1 + 1) = ↑(w u) * ↑(a u) + u.x * ↑(b u)
rw [← ha, hr]
no goals
case h₂
u : XgcdType
hr✝ : r u ≠ 0
ha : r u + ↑(b u) * q u = ↑(a u) := rq_eq u
hr : r u - 1 + 1 = r u := Eq.trans (add_comm (r u - 1) 1) (add_tsub_cancel_of_le (Nat.pos_of_ne_zero hr✝))
⊢ (↑(w u) * q u + u.x) * ↑(b u) + ↑(w u) * r u = ↑(w u) * (r u + ↑(b u) * q u) + u.x * ↑(b u)
ring