u : XgcdType
⊢ (↑(z u) * ↑(b u) + u.y * ↑(a u), u.x * ↑(b u) + ↑(w u) * ↑(a u)) =
    (u.y * ↑(a u) + ↑(z u) * ↑(b u), ↑(w u) * ↑(a u) + u.x * ↑(b u))
u : XgcdType
⊢ v (flip u) = Prod.swap (v u)
dsimp [v]
case h₁
u : XgcdType
⊢ (↑(z u) * ↑(b u) + u.y * ↑(a u), u.x * ↑(b u) + ↑(w u) * ↑(a u)).fst =
    (u.y * ↑(a u) + ↑(z u) * ↑(b u), ↑(w u) * ↑(a u) + u.x * ↑(b u)).fst

case h₂
u : XgcdType
⊢ (↑(z u) * ↑(b u) + u.y * ↑(a u), u.x * ↑(b u) + ↑(w u) * ↑(a u)).snd =
    (u.y * ↑(a u) + ↑(z u) * ↑(b u), ↑(w u) * ↑(a u) + u.x * ↑(b u)).snd
u : XgcdType
⊢ (↑(z u) * ↑(b u) + u.y * ↑(a u), u.x * ↑(b u) + ↑(w u) * ↑(a u)) =
    (u.y * ↑(a u) + ↑(z u) * ↑(b u), ↑(w u) * ↑(a u) + u.x * ↑(b u))
ext
case h₁
u : XgcdType
⊢ ↑(z u) * ↑(b u) + u.y * ↑(a u) = u.y * ↑(a u) + ↑(z u) * ↑(b u)
case h₁
u : XgcdType
⊢ (↑(z u) * ↑(b u) + u.y * ↑(a u), u.x * ↑(b u) + ↑(w u) * ↑(a u)).fst =
    (u.y * ↑(a u) + ↑(z u) * ↑(b u), ↑(w u) * ↑(a u) + u.x * ↑(b u)).fst
simp only
no goals
case h₁
u : XgcdType
⊢ ↑(z u) * ↑(b u) + u.y * ↑(a u) = u.y * ↑(a u) + ↑(z u) * ↑(b u)
ring
case h₂
u : XgcdType
⊢ u.x * ↑(b u) + ↑(w u) * ↑(a u) = ↑(w u) * ↑(a u) + u.x * ↑(b u)
case h₂
u : XgcdType
⊢ (↑(z u) * ↑(b u) + u.y * ↑(a u), u.x * ↑(b u) + ↑(w u) * ↑(a u)).snd =
    (u.y * ↑(a u) + ↑(z u) * ↑(b u), ↑(w u) * ↑(a u) + u.x * ↑(b u)).snd
simp only
no goals
case h₂
u : XgcdType
⊢ u.x * ↑(b u) + ↑(w u) * ↑(a u) = ↑(w u) * ↑(a u) + u.x * ↑(b u)
ring