u : XgcdType
hr : r u = 0
ha : r u + ↑(b u) * q u = ↑(a u) := rq_eq u
⊢ v (finish u) = v u
u : XgcdType
hr : r u = 0
⊢ v (finish u) = v u
let ha : u.r + u.b * u.q = u.a := u.rq_eq
u : XgcdType
hr : r u = 0
ha : ↑(b u) * q u = ↑(a u)
⊢ v (finish u) = v u
u : XgcdType
hr : r u = 0
ha : r u + ↑(b u) * q u = ↑(a u) := rq_eq u
⊢ v (finish u) = v u
rw [hr, zero_add] at ha
case h₁
u : XgcdType
hr : r u = 0
ha : ↑(b u) * q u = ↑(a u)
⊢ (v (finish u)).fst = (v u).fst

case h₂
u : XgcdType
hr : r u = 0
ha : ↑(b u) * q u = ↑(a u)
⊢ (v (finish u)).snd = (v u).snd
u : XgcdType
hr : r u = 0
ha : ↑(b u) * q u = ↑(a u)
⊢ v (finish u) = v u
ext
case h₁
u : XgcdType
hr : r u = 0
ha : ↑(b u) * q u = ↑(a u)
⊢ (u.wp + 1) * ↑(b u) + ((u.wp + 1) * qp u + u.x) * ↑(b u) = ↑(w u) * ↑(a u) + u.x * ↑(b u)
case h₁
u : XgcdType
hr : r u = 0
ha : ↑(b u) * q u = ↑(a u)
⊢ (v (finish u)).fst = (v u).fst
change (u.wp + 1) * u.b + ((u.wp + 1) * u.qp + u.x) * u.b = u.w * u.a + u.x * u.b
case h₁
u : XgcdType
hr : r u = 0
ha : ↑(b u) * q u = ↑(a u)
this : u.wp + 1 = ↑(w u)
⊢ (u.wp + 1) * ↑(b u) + ((u.wp + 1) * qp u + u.x) * ↑(b u) = ↑(w u) * ↑(a u) + u.x * ↑(b u)
case h₁
u : XgcdType
hr : r u = 0
ha : ↑(b u) * q u = ↑(a u)
⊢ (u.wp + 1) * ↑(b u) + ((u.wp + 1) * qp u + u.x) * ↑(b u) = ↑(w u) * ↑(a u) + u.x * ↑(b u)
have : u.wp + 1 = u.w := rfl
case h₁
u : XgcdType
hr : r u = 0
ha : ↑(b u) * q u = ↑(a u)
this : u.wp + 1 = ↑(w u)
⊢ ↑(w u) * ↑(b u) + (↑(w u) * qp u + u.x) * ↑(b u) = ↑(w u) * (↑(b u) * (qp u + 1)) + u.x * ↑(b u)
case h₁
u : XgcdType
hr : r u = 0
ha : ↑(b u) * q u = ↑(a u)
this : u.wp + 1 = ↑(w u)
⊢ (u.wp + 1) * ↑(b u) + ((u.wp + 1) * qp u + u.x) * ↑(b u) = ↑(w u) * ↑(a u) + u.x * ↑(b u)
rw [this, ← ha, u.qp_eq hr]
no goals
case h₁
u : XgcdType
hr : r u = 0
ha : ↑(b u) * q u = ↑(a u)
this : u.wp + 1 = ↑(w u)
⊢ ↑(w u) * ↑(b u) + (↑(w u) * qp u + u.x) * ↑(b u) = ↑(w u) * (↑(b u) * (qp u + 1)) + u.x * ↑(b u)
ring
case h₂
u : XgcdType
hr : r u = 0
ha : ↑(b u) * q u = ↑(a u)
⊢ u.y * ↑(b u) + (u.y * qp u + ↑(z u)) * ↑(b u) = u.y * ↑(a u) + ↑(z u) * ↑(b u)
case h₂
u : XgcdType
hr : r u = 0
ha : ↑(b u) * q u = ↑(a u)
⊢ (v (finish u)).snd = (v u).snd
change u.y * u.b + (u.y * u.qp + u.z) * u.b = u.y * u.a + u.z * u.b
case h₂
u : XgcdType
hr : r u = 0
ha : ↑(b u) * q u = ↑(a u)
⊢ u.y * ↑(b u) + (u.y * qp u + ↑(z u)) * ↑(b u) = u.y * (↑(b u) * (qp u + 1)) + ↑(z u) * ↑(b u)
case h₂
u : XgcdType
hr : r u = 0
ha : ↑(b u) * q u = ↑(a u)
⊢ u.y * ↑(b u) + (u.y * qp u + ↑(z u)) * ↑(b u) = u.y * ↑(a u) + ↑(z u) * ↑(b u)
rw [← ha, u.qp_eq hr]
no goals
case h₂
u : XgcdType
hr : r u = 0
ha : ↑(b u) * q u = ↑(a u)
⊢ u.y * ↑(b u) + (u.y * qp u + ↑(z u)) * ↑(b u) = u.y * (↑(b u) * (qp u + 1)) + ↑(z u) * ↑(b u)
ring