-- Mathlib/Data/PNat/Xgcd.lean
theorem isSpecial_iff : u.IsSpecial ↔ u.IsSpecial'

Proof state:
case mpr
u : XgcdType
wp x y zp ap bp : ℕ
h : wp * zp + zp + wp = x * y
⊢ wp + zp + wp * zp = wp * zp + zp + wp

Tactic:
ring

Result:
no goals

Proof state:
case mpr
u : XgcdType
wp x y zp ap bp : ℕ
h : (wp + 1) * (zp + 1) = x * y + 1
⊢ wp + zp + wp * zp = x * y

Tactic:
simp [Nat.mul_add, Nat.add_mul, ← Nat.add_assoc] at h

Result:
case mpr
u : XgcdType
wp x y zp ap bp : ℕ
h : wp * zp + zp + wp = x * y
⊢ wp + zp + wp * zp = x * y

Proof state:
u : XgcdType
⊢ u.wp + u.zp + u.wp * u.zp = u.x * u.y ↔ u.w * u.z = (u.x * u.y).succPNat

Tactic:
let ⟨wp, x, y, zp, ap, bp⟩ := u

Result:
u : XgcdType
wp x y zp ap bp : ℕ
⊢ { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp }.wp +
          { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp }.zp +
        { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp }.wp *
          { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp }.zp =
      { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp }.x *
        { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp }.y ↔
    { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp }.w *
        { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp }.z =
      ({ wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp }.x *
          { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp }.y).succPNat

Proof state:
u : XgcdType
⊢ u.IsSpecial ↔ u.IsSpecial'

Tactic:
dsimp [IsSpecial, IsSpecial']

Result:
u : XgcdType
⊢ u.wp + u.zp + u.wp * u.zp = u.x * u.y ↔ u.w * u.z = (u.x * u.y).succPNat

Proof state:
case mp
u : XgcdType
wp x y zp ap bp : ℕ
⊢ (wp + 1) * (zp + 1) = wp + zp + wp * zp + 1

Tactic:
ring

Result:
no goals

Proof state:
case mpr
u : XgcdType
wp x y zp ap bp : ℕ
h : wp * zp + zp + wp = x * y
⊢ wp + zp + wp * zp = x * y

Tactic:
rw [← h]

Result:
case mpr
u : XgcdType
wp x y zp ap bp : ℕ
h : wp * zp + zp + wp = x * y
⊢ wp + zp + wp * zp = wp * zp + zp + wp

Proof state:
u : XgcdType
wp x y zp ap bp : ℕ
⊢ { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp }.wp +
          { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp }.zp +
        { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp }.wp *
          { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp }.zp =
      { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp }.x *
        { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp }.y ↔
    { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp }.w *
        { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp }.z =
      ({ wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp }.x *
          { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp }.y).succPNat

Tactic:
constructor <;> intro h <;> simp only [w, succPNat, succ_eq_add_one, z] at * <;>
  simp only [← coe_inj, mul_coe, mk_coe] at *

Result:
case mp
u : XgcdType
wp x y zp ap bp : ℕ
h : wp + zp + wp * zp = x * y
⊢ (wp + 1) * (zp + 1) = x * y + 1

case mpr
u : XgcdType
wp x y zp ap bp : ℕ
h : (wp + 1) * (zp + 1) = x * y + 1
⊢ wp + zp + wp * zp = x * y

Proof state:
case mp
u : XgcdType
wp x y zp ap bp : ℕ
h : wp + zp + wp * zp = x * y
⊢ (wp + 1) * (zp + 1) = x * y + 1

Tactic:
simp_all [← h]

Result:
case mp
u : XgcdType
wp x y zp ap bp : ℕ
⊢ (wp + 1) * (zp + 1) = wp + zp + wp * zp + 1