awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.PNat.Xgcd
Goal:
u : XgcdType
let :
  ∀ (wp x y zp ap bp : ℕ),
    { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp : XgcdType }.wp +
            { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp : XgcdType }.zp +
          { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp : XgcdType }.wp *
            { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp : XgcdType }.zp =
        { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp : XgcdType }.x *
          { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp : XgcdType }.y ↔
      { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp : XgcdType }.w *
          { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp : XgcdType }.z =
        ({ wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp : XgcdType }.x *
            { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp : XgcdType }.y).succPNat
⊢ 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
-- Module: Mathlib.Data.PNat.Xgcd
Goal:
u : XgcdType
wp x y zp ap bp : ℕ
mp :
  { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp : XgcdType }.wp +
          { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp : XgcdType }.zp +
        { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp : XgcdType }.wp *
          { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp : XgcdType }.zp =
      { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp : XgcdType }.x *
        { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp : XgcdType }.y →
    { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp : XgcdType }.w *
        { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp : XgcdType }.z =
      ({ wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp : XgcdType }.x *
          { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp : XgcdType }.y).succPNat
mpr :
  { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp : XgcdType }.w *
        { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp : XgcdType }.z =
      ({ wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp : XgcdType }.x *
          { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp : XgcdType }.y).succPNat →
    { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp : XgcdType }.wp +
          { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp : XgcdType }.zp +
        { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp : XgcdType }.wp *
          { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp : XgcdType }.zp =
      { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp : XgcdType }.x *
        { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp : XgcdType }.y
⊢ { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp : XgcdType }.wp +
          { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp : XgcdType }.zp +
        { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp : XgcdType }.wp *
          { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp : XgcdType }.zp =
      { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp : XgcdType }.x *
        { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp : XgcdType }.y ↔
    { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp : XgcdType }.w *
        { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp : XgcdType }.z =
      ({ wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp : XgcdType }.x *
          { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp : XgcdType }.y).succPNat

Tactic:
constructor
-- Module: Mathlib.Data.PNat.Xgcd
Goal:
u : XgcdType
wp x y zp ap bp : ℕ
h :
  { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp : XgcdType }.wp +
        { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp : XgcdType }.zp +
      { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp : XgcdType }.wp *
        { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp : XgcdType }.zp =
    { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp : XgcdType }.x *
      { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp : XgcdType }.y
mp :
  Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) (wp + 1) ⋯ * Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) (zp + 1) ⋯ =
    Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) (x * y + 1) ⋯
⊢ { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp : XgcdType }.w *
      { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp : XgcdType }.z =
    ({ wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp : XgcdType }.x *
        { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp : XgcdType }.y).succPNat

Tactic:
simp only [w, succPNat, succ_eq_add_one, z] at *

Premises used: Nat.succ_eq_add_one, PNat.XgcdType.w, Nat.succPNat, PNat.XgcdType.z
-- Module: Mathlib.Data.PNat.Xgcd
Goal:
u : XgcdType
wp x y zp ap bp : ℕ
h :
  { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp : XgcdType }.w *
      { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp : XgcdType }.z =
    ({ wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp : XgcdType }.x *
        { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp : XgcdType }.y).succPNat
mpr : wp + zp + wp * zp = x * y
⊢ { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp : XgcdType }.wp +
        { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp : XgcdType }.zp +
      { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp : XgcdType }.wp *
        { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp : XgcdType }.zp =
    { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp : XgcdType }.x *
      { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp : XgcdType }.y

Tactic:
simp only [w, succPNat, succ_eq_add_one, z] at *

Premises used: Nat.succ_eq_add_one, PNat.XgcdType.w, Nat.succPNat, PNat.XgcdType.z
-- Module: Mathlib.Data.PNat.Xgcd
Goal:
u : XgcdType
wp x y zp ap bp : ℕ
h : wp + zp + wp * zp = x * y
mp : (wp + 1) * (zp + 1) = x * y + 1
⊢ Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) (wp + 1) ⋯ * Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) (zp + 1) ⋯ =
    Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) (x * y + 1) ⋯

Tactic:
simp only [← coe_inj, mul_coe, mk_coe] at *

Premises used: PNat.mul_coe, PNat.coe_inj, PNat.mk_coe
-- Module: Mathlib.Data.PNat.Xgcd
Goal:
u : XgcdType
wp x y zp ap bp : ℕ
h :
  Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) (wp + 1) ⋯ * Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) (zp + 1) ⋯ =
    Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) (x * y + 1) ⋯
⊢ (wp + 1) * (zp + 1) = x * y + 1

Tactic:
simp only [← coe_inj, mul_coe, mk_coe] at *

Premises used: PNat.mul_coe, PNat.coe_inj, PNat.mk_coe
-- Module: Mathlib.Data.PNat.Xgcd
Goal:
u : XgcdType
wp x y zp ap bp : ℕ
h : wp + zp + wp * zp = x * y
mp : (wp + 1) * (zp + 1) = wp + zp + wp * zp + 1
⊢ (wp + 1) * (zp + 1) = x * y + 1

Tactic:
simp_all [← h]
-- Module: Mathlib.Data.PNat.Xgcd
Goal:
u : XgcdType
wp x y zp ap bp : ℕ
⊢ (wp + 1) * (zp + 1) = wp + zp + wp * zp + 1

Tactic:
ring
-- Module: Mathlib.Data.PNat.Xgcd
Goal:
u : XgcdType
wp x y zp ap bp : ℕ
h : (wp + 1) * (zp + 1) = x * y + 1
⊢ wp * zp + zp + wp = x * y

Tactic:
simp only [Nat.mul_add, Nat.add_mul, one_mul, mul_one, ← Nat.add_assoc,
      Nat.add_right_cancel_iff] at h

Premises used: Nat.add_right_cancel_iff, Nat.add_assoc, mul_one, Nat.mul_add, Nat.add_mul, one_mul
-- Module: Mathlib.Data.PNat.Xgcd
Goal:
u : XgcdType
wp x y zp ap bp : ℕ
h : wp * zp + zp + wp = x * y
mpr : wp + zp + wp * zp = wp * zp + zp + wp
⊢ wp + zp + wp * zp = x * y

Tactic:
rw [← h]
-- Module: Mathlib.Data.PNat.Xgcd
Goal:
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
-- Module: Mathlib.Data.PNat.Xgcd
Goal:
u : XgcdType
⊢ u.IsReduced ↔ u.IsReduced'

Tactic:
succPNat_inj.symm

Premises used: PNat.XgcdType.IsReduced', PNat.XgcdType.IsReduced, PNat.XgcdType.a, Nat.succPNat_inj, Iff.symm, PNat.XgcdType.b
-- Module: Mathlib.Data.PNat.Xgcd
Goal:
u : XgcdType
⊢ u.flip.w = u.z

Tactic:
rfl

Premises used: PNat.XgcdType.z, rfl
-- Module: Mathlib.Data.PNat.Xgcd
Goal:
u : XgcdType
⊢ u.flip.x = u.y

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.PNat.Xgcd
Goal:
u : XgcdType
⊢ u.flip.y = u.x

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.PNat.Xgcd
Goal:
u : XgcdType
⊢ u.flip.z = u.w

Tactic:
rfl

Premises used: PNat.XgcdType.w, rfl
-- Module: Mathlib.Data.PNat.Xgcd
Goal:
u : XgcdType
⊢ u.flip.a = u.b

Tactic:
rfl

Premises used: rfl, PNat.XgcdType.b
-- Module: Mathlib.Data.PNat.Xgcd
Goal:
u : XgcdType
⊢ u.flip.b = u.a

Tactic:
rfl

Premises used: PNat.XgcdType.a, rfl
-- Module: Mathlib.Data.PNat.Xgcd
Goal:
u : XgcdType
dsimp : u.bp = u.ap ↔ u.ap = u.bp
⊢ u.flip.IsReduced ↔ u.IsReduced

Tactic:
dsimp [IsReduced, flip]

Premises used: PNat.XgcdType.flip, PNat.XgcdType.IsReduced
-- Module: Mathlib.Data.PNat.Xgcd
Goal:
u : XgcdType
mp : u.bp = u.ap → u.ap = u.bp
mpr : u.ap = u.bp → u.bp = u.ap
⊢ u.bp = u.ap ↔ u.ap = u.bp

Tactic:
constructor
-- Module: Mathlib.Data.PNat.Xgcd
Goal:
u : XgcdType
h : u.bp = u.ap
⊢ u.ap = u.bp

Tactic:
h.symm

Premises used: Eq.symm
-- Module: Mathlib.Data.PNat.Xgcd
Goal:
u : XgcdType
h : u.bp = u.ap
⊢ u.ap = u.bp

Tactic:
exact h.symm

Premises used: Eq.symm
-- Module: Mathlib.Data.PNat.Xgcd
Goal:
u : XgcdType
h : u.ap = u.bp
⊢ u.bp = u.ap

Tactic:
h.symm

Premises used: Eq.symm
-- Module: Mathlib.Data.PNat.Xgcd
Goal:
u : XgcdType
h : u.ap = u.bp
⊢ u.bp = u.ap

Tactic:
exact h.symm

Premises used: Eq.symm
-- Module: Mathlib.Data.PNat.Xgcd
Goal:
u : XgcdType
dsimp : u.zp + u.wp + u.zp * u.wp = u.y * u.x ↔ u.wp + u.zp + u.wp * u.zp = u.x * u.y
⊢ u.flip.IsSpecial ↔ u.IsSpecial

Tactic:
dsimp [IsSpecial, flip]

Premises used: PNat.XgcdType.flip, PNat.XgcdType.IsSpecial
-- Module: Mathlib.Data.PNat.Xgcd
Goal:
u : XgcdType
rw : u.zp + u.wp + u.zp * u.wp = u.y * u.x ↔ u.wp + u.zp + u.wp * u.zp = u.y * u.x
rw₁ : u.zp + u.wp + u.wp * u.zp = u.y * u.x ↔ u.wp + u.zp + u.wp * u.zp = u.y * u.x
rw₂ rw₃ : u.wp + u.zp + u.wp * u.zp = u.y * u.x ↔ u.wp + u.zp + u.wp * u.zp = u.y * u.x
⊢ u.zp + u.wp + u.zp * u.wp = u.y * u.x ↔ u.wp + u.zp + u.wp * u.zp = u.x * u.y

Tactic:
rw [mul_comm u.x, mul_comm u.zp, add_comm u.zp]

Premises used: PNat.XgcdType.zp, PNat.XgcdType.x, add_comm, mul_comm
-- Module: Mathlib.Data.PNat.Xgcd
Goal:
u : XgcdType
dsimp :
  ((↑u.z : ℕ) * (↑u.b : ℕ) + u.y * (↑u.a : ℕ), u.x * (↑u.b : ℕ) + (↑u.w : ℕ) * (↑u.a : ℕ)) =
    (u.y * (↑u.a : ℕ) + (↑u.z : ℕ) * (↑u.b : ℕ), (↑u.w : ℕ) * (↑u.a : ℕ) + u.x * (↑u.b : ℕ))
⊢ u.flip.v = u.v.swap

Tactic:
dsimp [v]

Premises used: PNat.XgcdType.v
-- Module: Mathlib.Data.PNat.Xgcd
Goal:
u : XgcdType
fst :
  ((↑u.z : ℕ) * (↑u.b : ℕ) + u.y * (↑u.a : ℕ), u.x * (↑u.b : ℕ) + (↑u.w : ℕ) * (↑u.a : ℕ)).1 =
    (u.y * (↑u.a : ℕ) + (↑u.z : ℕ) * (↑u.b : ℕ), (↑u.w : ℕ) * (↑u.a : ℕ) + u.x * (↑u.b : ℕ)).1
snd :
  ((↑u.z : ℕ) * (↑u.b : ℕ) + u.y * (↑u.a : ℕ), u.x * (↑u.b : ℕ) + (↑u.w : ℕ) * (↑u.a : ℕ)).2 =
    (u.y * (↑u.a : ℕ) + (↑u.z : ℕ) * (↑u.b : ℕ), (↑u.w : ℕ) * (↑u.a : ℕ) + u.x * (↑u.b : ℕ)).2
⊢ ((↑u.z : ℕ) * (↑u.b : ℕ) + u.y * (↑u.a : ℕ), u.x * (↑u.b : ℕ) + (↑u.w : ℕ) * (↑u.a : ℕ)) =
    (u.y * (↑u.a : ℕ) + (↑u.z : ℕ) * (↑u.b : ℕ), (↑u.w : ℕ) * (↑u.a : ℕ) + u.x * (↑u.b : ℕ))

Tactic:
ext
-- Module: Mathlib.Data.PNat.Xgcd
Goal:
u : XgcdType
⊢ (↑u.z : ℕ) * (↑u.b : ℕ) + u.y * (↑u.a : ℕ) = u.y * (↑u.a : ℕ) + (↑u.z : ℕ) * (↑u.b : ℕ)

Tactic:
ring
-- Module: Mathlib.Data.PNat.Xgcd
Goal:
u : XgcdType
⊢ u.x * (↑u.b : ℕ) + (↑u.w : ℕ) * (↑u.a : ℕ) = (↑u.w : ℕ) * (↑u.a : ℕ) + u.x * (↑u.b : ℕ)

Tactic:
ring
-- Module: Mathlib.Data.PNat.Xgcd
Goal:
u : XgcdType
⊢ u.r + (u.bp + 1) * u.q = u.ap + 1

Tactic:
Nat.mod_add_div (u.ap + 1) (u.bp + 1)

Premises used: PNat.XgcdType.r, Nat.mod_add_div, HAdd.hAdd, PNat.XgcdType.bp, OfNat.ofNat, PNat.XgcdType.ap, PNat.XgcdType.q
-- Module: Mathlib.Data.PNat.Xgcd
Goal:
u : XgcdType
hr : u.r = 0
pos : ∀ (hq : u.q = 0), u.q = u.qp + 1
neg : ∀ (hq : ¬u.q = 0), u.q = u.qp + 1
⊢ u.q = u.qp + 1

Tactic:
by_cases hq : u.q = 0

Premises used: PNat.XgcdType.q
-- Module: Mathlib.Data.PNat.Xgcd
Goal:
u : XgcdType
hr : u.r = 0
hq : u.q = 0
h : u.r + (u.bp + 1) * u.q = u.ap + 1 := ⋯
⊢ 0 = u.ap + 1

Tactic:
rw [hr, hq, mul_zero, add_zero] at h

Premises used: MulZeroClass.mul_zero, add_zero
-- Module: Mathlib.Data.PNat.Xgcd
Goal:
u : XgcdType
hr : u.r = 0
hq : u.q = 0
h : 0 = u.ap + 1
⊢ u.q = u.qp + 1

Tactic:
cases h
-- Module: Mathlib.Data.PNat.Xgcd
Goal:
u : XgcdType
hr : u.r = 0
hq : ¬u.q = 0
⊢ u.q = u.qp + 1

Tactic:
(Nat.succ_pred_eq_of_pos (Nat.pos_of_ne_zero hq)).symm

Premises used: Nat.succ_pred_eq_of_pos, PNat.XgcdType.qp, Nat.pos_of_ne_zero, Eq.symm, Nat.pred, PNat.XgcdType.q
-- Module: Mathlib.Data.PNat.Xgcd
Goal:
u : XgcdType
hr : u.r = 0
hq : ¬u.q = 0
⊢ u.q = u.qp + 1

Tactic:
exact (Nat.succ_pred_eq_of_pos (Nat.pos_of_ne_zero hq)).symm

Premises used: Nat.succ_pred_eq_of_pos, Nat.pos_of_ne_zero, Eq.symm
-- Module: Mathlib.Data.PNat.Xgcd
Goal:
a b : ℕ+
⊢ (start a b).IsSpecial

Tactic:
dsimp [start, IsSpecial]

Premises used: PNat.XgcdType.start, PNat.XgcdType.IsSpecial
-- Module: Mathlib.Data.PNat.Xgcd
Goal:
a b : ℕ+
⊢ 0 < (↑a : ℕ)

Tactic:
have := a.pos
-- Module: Mathlib.Data.PNat.Xgcd
Goal:
a b : ℕ+
this : 0 < (↑a : ℕ)
⊢ 0 < (↑b : ℕ)

Tactic:
have := b.pos
-- Module: Mathlib.Data.PNat.Xgcd
Goal:
a b : ℕ+
this_1 : 0 < (↑a : ℕ)
this : 0 < (↑b : ℕ)
⊢ (1 * ((↑a : ℕ) - 1 + 1) + 0 * ((↑b : ℕ) - 1 + 1), 0 * ((↑a : ℕ) - 1 + 1) + 1 * ((↑b : ℕ) - 1 + 1)) =
    ((↑a : ℕ), (↑b : ℕ))

Tactic:
lia
-- Module: Mathlib.Data.PNat.Xgcd
Goal:
u : XgcdType
⊢ u.finish.ap = u.finish.bp

Tactic:
rfl
-- Module: Mathlib.Data.PNat.Xgcd
Goal:
u : XgcdType
hs : u.IsSpecial
dsimp : u.wp + (u.y * u.qp + u.zp) + u.wp * (u.y * u.qp + u.zp) = ((u.wp + 1) * u.qp + u.x) * u.y
⊢ u.finish.IsSpecial

Tactic:
dsimp [IsSpecial, finish] at hs ⊢

Premises used: PNat.XgcdType.finish, PNat.XgcdType.IsSpecial
-- Module: Mathlib.Data.PNat.Xgcd
Goal:
u : XgcdType
hs : u.wp + u.zp + u.wp * u.zp = u.x * u.y
rw : u.wp + (u.y * u.qp + u.zp) + u.wp * (u.y * u.qp + u.zp) = u.wp + u.zp + u.wp * u.zp + (u.wp + 1) * u.qp * u.y
⊢ u.wp + (u.y * u.qp + u.zp) + u.wp * (u.y * u.qp + u.zp) = ((u.wp + 1) * u.qp + u.x) * u.y

Tactic:
rw [add_mul _ _ u.y, add_comm _ (u.x * u.y), ← hs]

Premises used: add_mul, HMul.hMul, PNat.XgcdType.y, PNat.XgcdType.x, add_comm
-- Module: Mathlib.Data.PNat.Xgcd
Goal:
u : XgcdType
hs : u.wp + u.zp + u.wp * u.zp = u.x * u.y
⊢ u.wp + (u.y * u.qp + u.zp) + u.wp * (u.y * u.qp + u.zp) = u.wp + u.zp + u.wp * u.zp + (u.wp + 1) * u.qp * u.y

Tactic:
ring
-- Module: Mathlib.Data.PNat.Xgcd
Goal:
u : XgcdType
hr : u.r = 0
ha : u.r + (↑u.b : ℕ) * u.q = (↑u.a : ℕ) := ⋯
⊢ (↑u.b : ℕ) * u.q = (↑u.a : ℕ)

Tactic:
rw [hr, zero_add] at ha

Premises used: zero_add
-- Module: Mathlib.Data.PNat.Xgcd
Goal:
u : XgcdType
hr : u.r = 0
ha : (↑u.b : ℕ) * u.q = (↑u.a : ℕ)
fst : u.finish.v.1 = u.v.1
snd : u.finish.v.2 = u.v.2
⊢ u.finish.v = u.v

Tactic:
ext
-- Module: Mathlib.Data.PNat.Xgcd
Goal:
u : XgcdType
hr : u.r = 0
ha : (↑u.b : ℕ) * u.q = (↑u.a : ℕ)
fst : (u.wp + 1) * (↑u.b : ℕ) + ((u.wp + 1) * u.qp + u.x) * (↑u.b : ℕ) = (↑u.w : ℕ) * (↑u.a : ℕ) + u.x * (↑u.b : ℕ)
⊢ u.finish.v.1 = u.v.1

Tactic:
change (u.wp + 1) * u.b + ((u.wp + 1) * u.qp + u.x) * u.b = u.w * u.a + u.x * u.b

Premises used: HMul.hMul, PNat.XgcdType.x, PNat.XgcdType.w, PNat.XgcdType.wp, PNat.XgcdType.qp, HAdd.hAdd, PNat.XgcdType.a, OfNat.ofNat, PNat.XgcdType.b
-- Module: Mathlib.Data.PNat.Xgcd
Goal:
u : XgcdType
hr : u.r = 0
ha : (↑u.b : ℕ) * u.q = (↑u.a : ℕ)
⊢ u.wp + 1 = (↑u.w : ℕ)

Tactic:
have : u.wp + 1 = u.w := rfl
-- Module: Mathlib.Data.PNat.Xgcd
Goal:
u : XgcdType
hr : u.r = 0
ha : (↑u.b : ℕ) * u.q = (↑u.a : ℕ)
this : u.wp + 1 = (↑u.w : ℕ)
fst :
  (↑u.w : ℕ) * (↑u.b : ℕ) + ((↑u.w : ℕ) * u.qp + u.x) * (↑u.b : ℕ) =
    (↑u.w : ℕ) * ((↑u.b : ℕ) * (u.qp + 1)) + u.x * (↑u.b : ℕ)
⊢ (u.wp + 1) * (↑u.b : ℕ) + ((u.wp + 1) * u.qp + u.x) * (↑u.b : ℕ) = (↑u.w : ℕ) * (↑u.a : ℕ) + u.x * (↑u.b : ℕ)

Tactic:
rw [this, ← ha, u.qp_eq hr]

Premises used: PNat.XgcdType.qp_eq
-- Module: Mathlib.Data.PNat.Xgcd
Goal:
u : XgcdType
hr : u.r = 0
ha : (↑u.b : ℕ) * u.q = (↑u.a : ℕ)
this : u.wp + 1 = (↑u.w : ℕ)
⊢ (↑u.w : ℕ) * (↑u.b : ℕ) + ((↑u.w : ℕ) * u.qp + u.x) * (↑u.b : ℕ) =
    (↑u.w : ℕ) * ((↑u.b : ℕ) * (u.qp + 1)) + u.x * (↑u.b : ℕ)

Tactic:
ring
-- Module: Mathlib.Data.PNat.Xgcd
Goal:
u : XgcdType
hr : u.r = 0
ha : (↑u.b : ℕ) * u.q = (↑u.a : ℕ)
snd : u.y * (↑u.b : ℕ) + (u.y * u.qp + (↑u.z : ℕ)) * (↑u.b : ℕ) = u.y * (↑u.a : ℕ) + (↑u.z : ℕ) * (↑u.b : ℕ)
⊢ u.finish.v.2 = u.v.2

Tactic:
change u.y * u.b + (u.y * u.qp + u.z) * u.b = u.y * u.a + u.z * u.b

Premises used: PNat.val, HMul.hMul, PNat.XgcdType.y, PNat.XgcdType.qp, HAdd.hAdd, PNat.XgcdType.a, PNat.XgcdType.z, PNat.XgcdType.b
-- Module: Mathlib.Data.PNat.Xgcd
Goal:
u : XgcdType
hr : u.r = 0
ha : (↑u.b : ℕ) * u.q = (↑u.a : ℕ)
snd :
  u.y * (↑u.b : ℕ) + (u.y * u.qp + (↑u.z : ℕ)) * (↑u.b : ℕ) = u.y * ((↑u.b : ℕ) * (u.qp + 1)) + (↑u.z : ℕ) * (↑u.b : ℕ)
⊢ u.y * (↑u.b : ℕ) + (u.y * u.qp + (↑u.z : ℕ)) * (↑u.b : ℕ) = u.y * (↑u.a : ℕ) + (↑u.z : ℕ) * (↑u.b : ℕ)

Tactic:
rw [← ha, u.qp_eq hr]

Premises used: PNat.XgcdType.qp_eq
-- Module: Mathlib.Data.PNat.Xgcd
Goal:
u : XgcdType
hr : u.r = 0
ha : (↑u.b : ℕ) * u.q = (↑u.a : ℕ)
⊢ u.y * (↑u.b : ℕ) + (u.y * u.qp + (↑u.z : ℕ)) * (↑u.b : ℕ) = u.y * ((↑u.b : ℕ) * (u.qp + 1)) + (↑u.z : ℕ) * (↑u.b : ℕ)

Tactic:
ring
-- Module: Mathlib.Data.PNat.Xgcd
Goal:
u : XgcdType
hr : u.r ≠ 0
⊢ u.r - 1 + 1 = u.r

Tactic:
have h₀ : u.r - 1 + 1 = u.r := Nat.succ_pred_eq_of_pos (Nat.pos_of_ne_zero hr)
-- Module: Mathlib.Data.PNat.Xgcd
Goal:
u : XgcdType
hr : u.r ≠ 0
h₀ : u.r - 1 + 1 = u.r
⊢ u.r < u.bp + 1

Tactic:
have h₁ : u.r < u.bp + 1 := Nat.mod_lt (u.ap + 1) u.bp.succ_pos
-- Module: Mathlib.Data.PNat.Xgcd
Goal:
u : XgcdType
hr : u.r ≠ 0
h₀ : u.r - 1 + 1 = u.r
h₁ : u.r < u.bp + 1
⊢ u.r - 1 + 1 < u.bp + 1

Tactic:
rw [← h₀] at h₁
-- Module: Mathlib.Data.PNat.Xgcd
Goal:
u : XgcdType
hr : u.r ≠ 0
h₀ : u.r - 1 + 1 = u.r
h₁ : u.r - 1 + 1 < u.bp + 1
⊢ u.r - 1 < u.bp

Tactic:
lt_of_succ_lt_succ h₁

Premises used: Nat.lt_of_succ_lt_succ
-- Module: Mathlib.Data.PNat.Xgcd
Goal:
u : XgcdType
hr : u.r ≠ 0
h₀ : u.r - 1 + 1 = u.r
h₁ : u.r - 1 + 1 < u.bp + 1
⊢ u.r - 1 < u.bp

Tactic:
exact lt_of_succ_lt_succ h₁

Premises used: Nat.lt_of_succ_lt_succ
-- Module: Mathlib.Data.PNat.Xgcd
Goal:
u : XgcdType
hs : u.IsSpecial
dsimp : u.y * u.q + u.zp + u.wp + (u.y * u.q + u.zp) * u.wp = u.y * ((u.wp + 1) * u.q + u.x)
⊢ u.step.IsSpecial

Tactic:
dsimp [IsSpecial, step] at hs ⊢

Premises used: PNat.XgcdType.step, PNat.XgcdType.IsSpecial
-- Module: Mathlib.Data.PNat.Xgcd
Goal:
u : XgcdType
hs : u.wp + u.zp + u.wp * u.zp = u.x * u.y
rw : u.y * u.q + u.zp + u.wp + (u.y * u.q + u.zp) * u.wp = u.y * ((u.wp + 1) * u.q) + (u.wp + u.zp + u.wp * u.zp)
⊢ u.y * u.q + u.zp + u.wp + (u.y * u.q + u.zp) * u.wp = u.y * ((u.wp + 1) * u.q + u.x)

Tactic:
rw [mul_add, mul_comm u.y u.x, ← hs]

Premises used: PNat.XgcdType.y, PNat.XgcdType.x, mul_comm, mul_add
-- Module: Mathlib.Data.PNat.Xgcd
Goal:
u : XgcdType
hs : u.wp + u.zp + u.wp * u.zp = u.x * u.y
⊢ u.y * u.q + u.zp + u.wp + (u.y * u.q + u.zp) * u.wp = u.y * ((u.wp + 1) * u.q) + (u.wp + u.zp + u.wp * u.zp)

Tactic:
ring
-- Module: Mathlib.Data.PNat.Xgcd
Goal:
u : XgcdType
hr_1 : u.r ≠ 0
ha : u.r + (↑u.b : ℕ) * u.q = (↑u.a : ℕ) := ⋯
hr : u.r - 1 + 1 = u.r := ⋯
fst : u.step.v.1 = u.v.swap.1
snd : u.step.v.2 = u.v.swap.2
⊢ u.step.v = u.v.swap

Tactic:
ext
-- Module: Mathlib.Data.PNat.Xgcd
Goal:
u : XgcdType
hr_1 : u.r ≠ 0
ha : u.r + (↑u.b : ℕ) * u.q = (↑u.a : ℕ) := ⋯
hr : u.r - 1 + 1 = u.r := ⋯
fst : (u.y * u.q + (↑u.z : ℕ)) * (↑u.b : ℕ) + u.y * (u.r - 1 + 1) = u.y * (↑u.a : ℕ) + (↑u.z : ℕ) * (↑u.b : ℕ)
⊢ u.step.v.1 = u.v.swap.1

Tactic:
change ((u.y * u.q + u.z) * u.b + u.y * (u.r - 1 + 1) : ℕ) = u.y * u.a + u.z * u.b

Premises used: PNat.val, HMul.hMul, PNat.XgcdType.y, PNat.XgcdType.r, HSub.hSub, HAdd.hAdd, PNat.XgcdType.a, PNat.XgcdType.z, OfNat.ofNat, PNat.XgcdType.b, PNat.XgcdType.q
-- Module: Mathlib.Data.PNat.Xgcd
Goal:
u : XgcdType
hr_1 : u.r ≠ 0
ha : u.r + (↑u.b : ℕ) * u.q = (↑u.a : ℕ) := ⋯
hr : u.r - 1 + 1 = u.r := ⋯
fst : (u.y * u.q + (↑u.z : ℕ)) * (↑u.b : ℕ) + u.y * u.r = u.y * (u.r + (↑u.b : ℕ) * u.q) + (↑u.z : ℕ) * (↑u.b : ℕ)
⊢ (u.y * u.q + (↑u.z : ℕ)) * (↑u.b : ℕ) + u.y * (u.r - 1 + 1) = u.y * (↑u.a : ℕ) + (↑u.z : ℕ) * (↑u.b : ℕ)

Tactic:
rw [← ha, hr]
-- Module: Mathlib.Data.PNat.Xgcd
Goal:
u : XgcdType
hr_1 : u.r ≠ 0
ha : u.r + (↑u.b : ℕ) * u.q = (↑u.a : ℕ) := ⋯
hr : u.r - 1 + 1 = u.r := ⋯
⊢ (u.y * u.q + (↑u.z : ℕ)) * (↑u.b : ℕ) + u.y * u.r = u.y * (u.r + (↑u.b : ℕ) * u.q) + (↑u.z : ℕ) * (↑u.b : ℕ)

Tactic:
ring
-- Module: Mathlib.Data.PNat.Xgcd
Goal:
u : XgcdType
hr_1 : u.r ≠ 0
ha : u.r + (↑u.b : ℕ) * u.q = (↑u.a : ℕ) := ⋯
hr : u.r - 1 + 1 = u.r := ⋯
snd : ((↑u.w : ℕ) * u.q + u.x) * (↑u.b : ℕ) + (↑u.w : ℕ) * (u.r - 1 + 1) = (↑u.w : ℕ) * (↑u.a : ℕ) + u.x * (↑u.b : ℕ)
⊢ u.step.v.2 = u.v.swap.2

Tactic:
change ((u.w * u.q + u.x) * u.b + u.w * (u.r - 1 + 1) : ℕ) = u.w * u.a + u.x * u.b

Premises used: PNat.val, HMul.hMul, PNat.XgcdType.r, HSub.hSub, PNat.XgcdType.x, PNat.XgcdType.w, HAdd.hAdd, PNat.XgcdType.a, OfNat.ofNat, PNat.XgcdType.b, PNat.XgcdType.q
-- Module: Mathlib.Data.PNat.Xgcd
Goal:
u : XgcdType
hr_1 : u.r ≠ 0
ha : u.r + (↑u.b : ℕ) * u.q = (↑u.a : ℕ) := ⋯
hr : u.r - 1 + 1 = u.r := ⋯
snd :
  ((↑u.w : ℕ) * u.q + u.x) * (↑u.b : ℕ) + (↑u.w : ℕ) * u.r = (↑u.w : ℕ) * (u.r + (↑u.b : ℕ) * u.q) + u.x * (↑u.b : ℕ)
⊢ ((↑u.w : ℕ) * u.q + u.x) * (↑u.b : ℕ) + (↑u.w : ℕ) * (u.r - 1 + 1) = (↑u.w : ℕ) * (↑u.a : ℕ) + u.x * (↑u.b : ℕ)

Tactic:
rw [← ha, hr]
-- Module: Mathlib.Data.PNat.Xgcd
Goal:
u : XgcdType
hr_1 : u.r ≠ 0
ha : u.r + (↑u.b : ℕ) * u.q = (↑u.a : ℕ) := ⋯
hr : u.r - 1 + 1 = u.r := ⋯
⊢ ((↑u.w : ℕ) * u.q + u.x) * (↑u.b : ℕ) + (↑u.w : ℕ) * u.r = (↑u.w : ℕ) * (u.r + (↑u.b : ℕ) * u.q) + u.x * (↑u.b : ℕ)

Tactic:
ring
-- Module: Mathlib.Data.PNat.Xgcd
Goal:
u : XgcdType
_h : ¬u.r = 0
⊢ sizeOf u.step < sizeOf u

Tactic:
apply u.step_wf _h

Premises used: PNat.XgcdType.step_wf
-- Module: Mathlib.Data.PNat.Xgcd
Goal:
u : XgcdType
_h : ¬u.r = 0
⊢ sizeOf u.step < sizeOf u

Tactic:
decreasing_by apply u.step_wf _h

Premises used: PNat.XgcdType.step_wf
-- Module: Mathlib.Data.PNat.Xgcd
Goal:
u : XgcdType
h : u.r = 0
rw : (if x : u.r = 0 then u.finish else u.step.reduce.flip) = u.finish
⊢ u.reduce = u.finish

Tactic:
rw [reduce]

Premises used: PNat.XgcdType.reduce
-- Module: Mathlib.Data.PNat.Xgcd
Goal:
u : XgcdType
h : u.r = 0
⊢ (if x : u.r = 0 then u.finish else u.step.reduce.flip) = u.finish

Tactic:
if_pos h

Premises used: if_pos, dite
-- Module: Mathlib.Data.PNat.Xgcd
Goal:
u : XgcdType
h : u.r = 0
⊢ (if x : u.r = 0 then u.finish else u.step.reduce.flip) = u.finish

Tactic:
exact if_pos h

Premises used: if_pos
-- Module: Mathlib.Data.PNat.Xgcd
Goal:
u : XgcdType
h : u.r ≠ 0
rw : (if x : u.r = 0 then u.finish else u.step.reduce.flip) = u.step.reduce.flip
⊢ u.reduce = u.step.reduce.flip

Tactic:
rw [reduce]

Premises used: PNat.XgcdType.reduce
-- Module: Mathlib.Data.PNat.Xgcd
Goal:
u : XgcdType
h : u.r ≠ 0
⊢ (if x : u.r = 0 then u.finish else u.step.reduce.flip) = u.step.reduce.flip

Tactic:
if_neg h

Premises used: dite, if_neg
-- Module: Mathlib.Data.PNat.Xgcd
Goal:
u : XgcdType
h : u.r ≠ 0
⊢ (if x : u.r = 0 then u.finish else u.step.reduce.flip) = u.step.reduce.flip

Tactic:
exact if_neg h

Premises used: if_neg
-- Module: Mathlib.Data.PNat.Xgcd
Goal:
x : XgcdType
u : XgcdType := x
h : u.r = 0
rw : u.finish.IsReduced
⊢ x.reduce.IsReduced

Tactic:
rw [reduce_a h]

Premises used: PNat.XgcdType.reduce_a
-- Module: Mathlib.Data.PNat.Xgcd
Goal:
x : XgcdType
u : XgcdType := x
h : u.r = 0
⊢ u.finish.IsReduced

Tactic:
u.finish_isReduced

Premises used: PNat.XgcdType.finish_isReduced
-- Module: Mathlib.Data.PNat.Xgcd
Goal:
x : XgcdType
u : XgcdType := x
h : u.r = 0
⊢ u.finish.IsReduced

Tactic:
exact u.finish_isReduced

Premises used: PNat.XgcdType.finish_isReduced
-- Module: Mathlib.Data.PNat.Xgcd
Goal:
x : XgcdType
u : XgcdType := x
h : ¬u.r = 0
⊢ sizeOf u.step < sizeOf u

Tactic:
have : SizeOf.sizeOf u.step < SizeOf.sizeOf u := u.step_wf h
-- Module: Mathlib.Data.PNat.Xgcd
Goal:
x : XgcdType
u : XgcdType := x
h : ¬u.r = 0
this : sizeOf u.step < sizeOf u
rw : u.step.reduce.IsReduced
⊢ x.reduce.IsReduced

Tactic:
rw [reduce_b h, flip_isReduced]

Premises used: PNat.XgcdType.flip_isReduced, PNat.XgcdType.reduce_b