-- Mathlib/Data/PNat/Xgcd.lean
theorem gcd_props :
    let d := gcdD a b
    let w := gcdW a b
    let x := gcdX a b
    let y := gcdY a b
    let z := gcdZ a b
    let a' := gcdA' a b
    let b' := gcdB' a b
    w * z = succPNat (x * y) ∧
      a = a' * d ∧
        b = b' * d ∧
          z * a' = succPNat (x * b') ∧
            w * b' = succPNat (y * a') ∧ (z * a : ℕ) = x * b + d ∧ (w * b : ℕ) = y * a + d

Proof state:
case right.right.right
a b : ℕ+
d : ℕ+ := a.gcdD b
w : ℕ+ := a.gcdW b
x : ℕ := a.gcdX b
y : ℕ := a.gcdY b
z : ℕ+ := a.gcdZ b
a' : ℕ+ := a.gcdA' b
b' : ℕ+ := a.gcdB' b
u : XgcdType := XgcdType.start a b
ur : XgcdType := u.reduce
x✝¹ : d = ur.a
hb : d = ur.b
ha' : ↑a' = ↑w + x
hb' : ↑b' = y + ↑z
hdet : w * z = (x * y).succPNat
hdet' : ↑w * ↑z = x * y + 1
x✝ : u.v = (↑a, ↑b)
hv : (↑a' * ↑d, ↑b' * ↑d) = (↑a, ↑b)
ha'' : ↑a = ↑a' * ↑d
hb'' : ↑b = ↑b' * ↑d
hza' : ↑z * ↑a' = x * ↑b' + 1
⊢ z * a' = (x * ↑b').succPNat ∧ w * b' = (y * ↑a').succPNat ∧ ↑z * ↑a = x * ↑b + ↑d ∧ ↑w * ↑b = y * ↑a + ↑d

Tactic:
have hwb' : (w * b' : ℕ) = y * a' + 1 := by
  rw [ha', hb', mul_add, mul_add, hdet']
  ring

Result:
case right.right.right
a b : ℕ+
d : ℕ+ := a.gcdD b
w : ℕ+ := a.gcdW b
x : ℕ := a.gcdX b
y : ℕ := a.gcdY b
z : ℕ+ := a.gcdZ b
a' : ℕ+ := a.gcdA' b
b' : ℕ+ := a.gcdB' b
u : XgcdType := XgcdType.start a b
ur : XgcdType := u.reduce
x✝¹ : d = ur.a
hb : d = ur.b
ha' : ↑a' = ↑w + x
hb' : ↑b' = y + ↑z
hdet : w * z = (x * y).succPNat
hdet' : ↑w * ↑z = x * y + 1
x✝ : u.v = (↑a, ↑b)
hv : (↑a' * ↑d, ↑b' * ↑d) = (↑a, ↑b)
ha'' : ↑a = ↑a' * ↑d
hb'' : ↑b = ↑b' * ↑d
hza' : ↑z * ↑a' = x * ↑b' + 1
hwb' : ↑w * ↑b' = y * ↑a' + 1
⊢ z * a' = (x * ↑b').succPNat ∧ w * b' = (y * ↑a').succPNat ∧ ↑z * ↑a = x * ↑b + ↑d ∧ ↑w * ↑b = y * ↑a + ↑d

Proof state:
case right
a b : ℕ+
d : ℕ+ := a.gcdD b
w : ℕ+ := a.gcdW b
x : ℕ := a.gcdX b
y : ℕ := a.gcdY b
z : ℕ+ := a.gcdZ b
a' : ℕ+ := a.gcdA' b
b' : ℕ+ := a.gcdB' b
u : XgcdType := XgcdType.start a b
ur : XgcdType := u.reduce
x✝¹ : d = ur.a
hb : d = ur.b
ha' : ↑a' = ↑w + x
hb' : ↑b' = y + ↑z
hdet : w * z = (x * y).succPNat
hdet' : ↑w * ↑z = x * y + 1
x✝ : u.v = (↑a, ↑b)
⊢ a = a' * d ∧
    b = b' * d ∧
      z * a' = (x * ↑b').succPNat ∧ w * b' = (y * ↑a').succPNat ∧ ↑z * ↑a = x * ↑b + ↑d ∧ ↑w * ↑b = y * ↑a + ↑d

Tactic:
let hv : Prod.mk (w * d + x * ur.b : ℕ) (y * d + z * ur.b : ℕ) = ⟨a, b⟩ :=
  u.reduce_v.trans (XgcdType.start_v a b)

Result:
case right
a b : ℕ+
d : ℕ+ := a.gcdD b
w : ℕ+ := a.gcdW b
x : ℕ := a.gcdX b
y : ℕ := a.gcdY b
z : ℕ+ := a.gcdZ b
a' : ℕ+ := a.gcdA' b
b' : ℕ+ := a.gcdB' b
u : XgcdType := XgcdType.start a b
ur : XgcdType := u.reduce
x✝¹ : d = ur.a
hb : d = ur.b
ha' : ↑a' = ↑w + x
hb' : ↑b' = y + ↑z
hdet : w * z = (x * y).succPNat
hdet' : ↑w * ↑z = x * y + 1
x✝ : u.v = (↑a, ↑b)
hv : (↑w * ↑d + x * ↑ur.b, y * ↑d + ↑z * ↑ur.b) = (↑a, ↑b) := Eq.trans (XgcdType.reduce_v u) (XgcdType.start_v a b)
⊢ a = a' * d ∧
    b = b' * d ∧
      z * a' = (x * ↑b').succPNat ∧ w * b' = (y * ↑a').succPNat ∧ ↑z * ↑a = x * ↑b + ↑d ∧ ↑w * ↑b = y * ↑a + ↑d

Proof state:
case right.right.right
a b : ℕ+
d : ℕ+ := a.gcdD b
w : ℕ+ := a.gcdW b
x : ℕ := a.gcdX b
y : ℕ := a.gcdY b
z : ℕ+ := a.gcdZ b
a' : ℕ+ := a.gcdA' b
b' : ℕ+ := a.gcdB' b
u : XgcdType := XgcdType.start a b
ur : XgcdType := u.reduce
x✝¹ : d = ur.a
hb : d = ur.b
ha' : ↑a' = ↑w + x
hb' : ↑b' = y + ↑z
hdet : w * z = (x * y).succPNat
hdet' : ↑w * ↑z = x * y + 1
x✝ : u.v = (↑a, ↑b)
hv : (↑a' * ↑d, ↑b' * ↑d) = (↑a, ↑b)
ha'' : ↑a = ↑a' * ↑d
hb'' : ↑b = ↑b' * ↑d
⊢ z * a' = (x * ↑b').succPNat ∧ w * b' = (y * ↑a').succPNat ∧ ↑z * ↑a = x * ↑b + ↑d ∧ ↑w * ↑b = y * ↑a + ↑d

Tactic:
have hza' : (z * a' : ℕ) = x * b' + 1 := by
  rw [ha', hb', mul_add, mul_add, mul_comm (z : ℕ), hdet']
  ring

Result:
case right.right.right
a b : ℕ+
d : ℕ+ := a.gcdD b
w : ℕ+ := a.gcdW b
x : ℕ := a.gcdX b
y : ℕ := a.gcdY b
z : ℕ+ := a.gcdZ b
a' : ℕ+ := a.gcdA' b
b' : ℕ+ := a.gcdB' b
u : XgcdType := XgcdType.start a b
ur : XgcdType := u.reduce
x✝¹ : d = ur.a
hb : d = ur.b
ha' : ↑a' = ↑w + x
hb' : ↑b' = y + ↑z
hdet : w * z = (x * y).succPNat
hdet' : ↑w * ↑z = x * y + 1
x✝ : u.v = (↑a, ↑b)
hv : (↑a' * ↑d, ↑b' * ↑d) = (↑a, ↑b)
ha'' : ↑a = ↑a' * ↑d
hb'' : ↑b = ↑b' * ↑d
hza' : ↑z * ↑a' = x * ↑b' + 1
⊢ z * a' = (x * ↑b').succPNat ∧ w * b' = (y * ↑a').succPNat ∧ ↑z * ↑a = x * ↑b + ↑d ∧ ↑w * ↑b = y * ↑a + ↑d

Proof state:
case right
a b : ℕ+
d : ℕ+ := a.gcdD b
w : ℕ+ := a.gcdW b
x : ℕ := a.gcdX b
y : ℕ := a.gcdY b
z : ℕ+ := a.gcdZ b
a' : ℕ+ := a.gcdA' b
b' : ℕ+ := a.gcdB' b
u : XgcdType := XgcdType.start a b
ur : XgcdType := u.reduce
x✝¹ : d = ur.a
hb : d = ur.b
ha' : ↑a' = ↑w + x
hb' : ↑b' = y + ↑z
hdet : w * z = (x * y).succPNat
hdet' : ↑w * ↑z = x * y + 1
x✝ : u.v = (↑a, ↑b)
hv : (↑a' * ↑d, ↑b' * ↑d) = (↑a, ↑b)
⊢ a = a' * d ∧
    b = b' * d ∧
      z * a' = (x * ↑b').succPNat ∧ w * b' = (y * ↑a').succPNat ∧ ↑z * ↑a = x * ↑b + ↑d ∧ ↑w * ↑b = y * ↑a + ↑d

Tactic:
have ha'' : (a : ℕ) = a' * d := (congr_arg Prod.fst hv).symm

Result:
case right
a b : ℕ+
d : ℕ+ := a.gcdD b
w : ℕ+ := a.gcdW b
x : ℕ := a.gcdX b
y : ℕ := a.gcdY b
z : ℕ+ := a.gcdZ b
a' : ℕ+ := a.gcdA' b
b' : ℕ+ := a.gcdB' b
u : XgcdType := XgcdType.start a b
ur : XgcdType := u.reduce
x✝¹ : d = ur.a
hb : d = ur.b
ha' : ↑a' = ↑w + x
hb' : ↑b' = y + ↑z
hdet : w * z = (x * y).succPNat
hdet' : ↑w * ↑z = x * y + 1
x✝ : u.v = (↑a, ↑b)
hv : (↑a' * ↑d, ↑b' * ↑d) = (↑a, ↑b)
ha'' : ↑a = ↑a' * ↑d
⊢ a = a' * d ∧
    b = b' * d ∧
      z * a' = (x * ↑b').succPNat ∧ w * b' = (y * ↑a').succPNat ∧ ↑z * ↑a = x * ↑b + ↑d ∧ ↑w * ↑b = y * ↑a + ↑d

Proof state:
case right.right.right.left.a
a b : ℕ+
d : ℕ+ := a.gcdD b
w : ℕ+ := a.gcdW b
x : ℕ := a.gcdX b
y : ℕ := a.gcdY b
z : ℕ+ := a.gcdZ b
a' : ℕ+ := a.gcdA' b
b' : ℕ+ := a.gcdB' b
u : XgcdType := XgcdType.start a b
ur : XgcdType := u.reduce
x✝¹ : d = ur.a
hb : d = ur.b
ha' : ↑a' = ↑w + x
hb' : ↑b' = y + ↑z
hdet : w * z = (x * y).succPNat
hdet' : ↑w * ↑z = x * y + 1
x✝ : u.v = (↑a, ↑b)
hv : (↑a' * ↑d, ↑b' * ↑d) = (↑a, ↑b)
ha'' : ↑a = ↑a' * ↑d
hb'' : ↑b = ↑b' * ↑d
hza' : ↑z * ↑a' = x * ↑b' + 1
hwb' : ↑w * ↑b' = y * ↑a' + 1
⊢ ↑(z * a') = ↑(x * ↑b').succPNat

Tactic:
rw [succPNat_coe, Nat.succ_eq_add_one, mul_coe, hza']

Result:
no goals

Proof state:
case right
a b : ℕ+
d : ℕ+ := a.gcdD b
w : ℕ+ := a.gcdW b
x : ℕ := a.gcdX b
y : ℕ := a.gcdY b
z : ℕ+ := a.gcdZ b
a' : ℕ+ := a.gcdA' b
b' : ℕ+ := a.gcdB' b
u : XgcdType := XgcdType.start a b
ur : XgcdType := u.reduce
x✝ : d = ur.a
hb : d = ur.b
ha' : ↑a' = ↑w + x
hb' : ↑b' = y + ↑z
hdet : w * z = (x * y).succPNat
hdet' : ↑w * ↑z = x * y + 1
⊢ a = a' * d ∧
    b = b' * d ∧
      z * a' = (x * ↑b').succPNat ∧ w * b' = (y * ↑a').succPNat ∧ ↑z * ↑a = x * ↑b + ↑d ∧ ↑w * ↑b = y * ↑a + ↑d

Tactic:
have _ : u.v = ⟨a, b⟩ := XgcdType.start_v a b

Result:
case right
a b : ℕ+
d : ℕ+ := a.gcdD b
w : ℕ+ := a.gcdW b
x : ℕ := a.gcdX b
y : ℕ := a.gcdY b
z : ℕ+ := a.gcdZ b
a' : ℕ+ := a.gcdA' b
b' : ℕ+ := a.gcdB' b
u : XgcdType := XgcdType.start a b
ur : XgcdType := u.reduce
x✝¹ : d = ur.a
hb : d = ur.b
ha' : ↑a' = ↑w + x
hb' : ↑b' = y + ↑z
hdet : w * z = (x * y).succPNat
hdet' : ↑w * ↑z = x * y + 1
x✝ : u.v = (↑a, ↑b)
⊢ a = a' * d ∧
    b = b' * d ∧
      z * a' = (x * ↑b').succPNat ∧ w * b' = (y * ↑a').succPNat ∧ ↑z * ↑a = x * ↑b + ↑d ∧ ↑w * ↑b = y * ↑a + ↑d