awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.PNat.Xgcd
Goal:
x : XgcdType
u : XgcdType := x
h : ¬u.r = 0
this : sizeOf u.step < sizeOf u
⊢ u.step.reduce.IsReduced

Tactic:
apply reduce_isReduced
-- Module: Mathlib.Data.PNat.Xgcd
Goal:
u : XgcdType
⊢ u.reduce.IsReduced'

Tactic:
(isReduced_iff _).mp u.reduce_isReduced

Premises used: PNat.XgcdType.reduce_isReduced, Iff.mp, PNat.XgcdType.isReduced_iff
-- Module: Mathlib.Data.PNat.Xgcd
Goal:
x : XgcdType
u : XgcdType := x
h : u.r = 0
hs : x.IsSpecial
rw : u.finish.IsSpecial
⊢ x.reduce.IsSpecial

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
hs : x.IsSpecial
⊢ u.finish.IsSpecial

Tactic:
u.finish_isSpecial hs

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

Tactic:
exact u.finish_isSpecial hs

Premises used: PNat.XgcdType.finish_isSpecial
-- Module: Mathlib.Data.PNat.Xgcd
Goal:
x : XgcdType
u : XgcdType := x
h : ¬u.r = 0
hs : x.IsSpecial
⊢ 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
hs : x.IsSpecial
this : sizeOf u.step < sizeOf u
rw : u.step.reduce.flip.IsSpecial
⊢ x.reduce.IsSpecial

Tactic:
rw [reduce_b h]

Premises used: PNat.XgcdType.reduce_b
-- Module: Mathlib.Data.PNat.Xgcd
Goal:
x : XgcdType
u : XgcdType := x
h : ¬u.r = 0
hs : x.IsSpecial
this : sizeOf u.step < sizeOf u
⊢ u.step.reduce.flip.IsSpecial

Tactic:
(flip_isSpecial _).mpr (reduce_isSpecial _ (u.step_isSpecial hs))

Premises used: Iff.mpr, PNat.XgcdType.step_isSpecial, PNat.XgcdType.flip_isSpecial
-- Module: Mathlib.Data.PNat.Xgcd
Goal:
x : XgcdType
u : XgcdType := x
h : ¬u.r = 0
hs : x.IsSpecial
this : sizeOf u.step < sizeOf u
⊢ u.step.reduce.flip.IsSpecial

Tactic:
exact (flip_isSpecial _).mpr (reduce_isSpecial _ (u.step_isSpecial hs))

Premises used: Iff.mpr, PNat.XgcdType.step_isSpecial, PNat.XgcdType.flip_isSpecial
-- Module: Mathlib.Data.PNat.Xgcd
Goal:
u : XgcdType
hs : u.IsSpecial
⊢ u.reduce.IsSpecial'

Tactic:
(isSpecial_iff _).mp (u.reduce_isSpecial hs)

Premises used: PNat.XgcdType.reduce_isSpecial, PNat.XgcdType.isSpecial_iff, Iff.mp
-- Module: Mathlib.Data.PNat.Xgcd
Goal:
x : XgcdType
u : XgcdType := x
h : u.r = 0
rw : u.finish.v = x.v
rw₁ rw₂ : u.v = x.v
⊢ x.reduce.v = x.v

Tactic:
rw [reduce_a h, finish_v u h]

Premises used: PNat.XgcdType.finish_v, PNat.XgcdType.reduce_a
-- 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.flip.v = x.v
rw₁ : u.step.reduce.v.swap = x.v
rw₂ : u.step.v.swap = x.v
rw₃ : u.v.swap.swap = x.v
rw₄ rw₅ : u.v = x.v
⊢ x.reduce.v = x.v

Tactic:
rw [reduce_b h, flip_v, reduce_v (step u), step_v u h, Prod.swap_swap]

Premises used: PNat.XgcdType.step, Prod.swap_swap, PNat.XgcdType.reduce_b, PNat.XgcdType.flip_v, PNat.XgcdType.step_v
-- Module: Mathlib.Data.PNat.Xgcd
Goal:
a b : ℕ+
rw rw₁ : (a.xgcd b).wp + 1 + (a.xgcd b).x = (a.xgcd b).wp + 1 + (a.xgcd b).x
⊢ (a.xgcd b).wp + (a.xgcd b).x + 1 = (a.xgcd b).wp + 1 + (a.xgcd b).x

Tactic:
rw [add_right_comm]

Premises used: add_right_comm
-- Module: Mathlib.Data.PNat.Xgcd
Goal:
a b : ℕ+
rw rw₁ : (a.xgcd b).y + ((a.xgcd b).zp + 1) = (a.xgcd b).y + ((a.xgcd b).zp + 1)
⊢ (a.xgcd b).y + (a.xgcd b).zp + 1 = (a.xgcd b).y + ((a.xgcd b).zp + 1)

Tactic:
rw [add_assoc]

Premises used: add_assoc
-- Module: Mathlib.Data.PNat.Xgcd
Goal:
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
⊢ d = ur.b

Tactic:
have hb : d = ur.b := u.reduce_isReduced'
-- Module: Mathlib.Data.PNat.Xgcd
Goal:
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
hb : d = ur.b
⊢ (↑a' : ℕ) = (↑w : ℕ) + x

Tactic:
have ha' : (a' : ℕ) = w + x := gcdA'_coe a b
-- Module: Mathlib.Data.PNat.Xgcd
Goal:
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
hb : d = ur.b
ha' : (↑a' : ℕ) = (↑w : ℕ) + x
⊢ (↑b' : ℕ) = y + (↑z : ℕ)

Tactic:
have hb' : (b' : ℕ) = y + z := gcdB'_coe a b
-- Module: Mathlib.Data.PNat.Xgcd
Goal:
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
hb : d = ur.b
ha' : (↑a' : ℕ) = (↑w : ℕ) + x
hb' : (↑b' : ℕ) = y + (↑z : ℕ)
⊢ w * z = (x * y).succPNat

Tactic:
have hdet : w * z = succPNat (x * y) := u.reduce_isSpecial' rfl
-- Module: Mathlib.Data.PNat.Xgcd
Goal:
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
hb : d = ur.b
ha' : (↑a' : ℕ) = (↑w : ℕ) + x
hb' : (↑b' : ℕ) = y + (↑z : ℕ)
hdet left : w * z = (x * y).succPNat
right :
  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 : ℕ)
⊢ w * z = (x * y).succPNat ∧
    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:
constructor
-- Module: Mathlib.Data.PNat.Xgcd
Goal:
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
hb : d = ur.b
ha' : (↑a' : ℕ) = (↑w : ℕ) + x
hb' : (↑b' : ℕ) = y + (↑z : ℕ)
hdet : w * z = (x * y).succPNat
⊢ w * z = (x * y).succPNat

Tactic:
hdet
-- Module: Mathlib.Data.PNat.Xgcd
Goal:
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
hb : d = ur.b
ha' : (↑a' : ℕ) = (↑w : ℕ) + x
hb' : (↑b' : ℕ) = y + (↑z : ℕ)
hdet : w * z = (x * y).succPNat
⊢ w * z = (x * y).succPNat

Tactic:
exact hdet
-- Module: Mathlib.Data.PNat.Xgcd
Goal:
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
hb : d = ur.b
ha' : (↑a' : ℕ) = (↑w : ℕ) + x
hb' : (↑b' : ℕ) = y + (↑z : ℕ)
hdet : w * z = (x * y).succPNat
rw : (↑(w * z) : ℕ) = x * y + 1
rw₁ : (↑(x * y).succPNat : ℕ) = x * y + 1
rw₂ rw₃ : (x * y).succ = x * y + 1
⊢ (↑w : ℕ) * (↑z : ℕ) = x * y + 1

Tactic:
rw [← mul_coe, hdet, succPNat_coe]

Premises used: Nat.succPNat_coe, PNat.mul_coe
-- Module: Mathlib.Data.PNat.Xgcd
Goal:
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
hb : d = ur.b
ha' : (↑a' : ℕ) = (↑w : ℕ) + x
hb' : (↑b' : ℕ) = y + (↑z : ℕ)
hdet : w * z = (x * y).succPNat
⊢ (↑w : ℕ) * (↑z : ℕ) = x * y + 1

Tactic:
have hdet' : (w * z : ℕ) = x * y + 1 := by rw [← mul_coe, hdet, succPNat_coe]
-- Module: Mathlib.Data.PNat.Xgcd
Goal:
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
hb : d = ur.b
ha' : (↑a' : ℕ) = (↑w : ℕ) + x
hb' : (↑b' : ℕ) = y + (↑z : ℕ)
hdet : w * z = (x * y).succPNat
hdet' : (↑w : ℕ) * (↑z : ℕ) = x * y + 1
hv : ((↑w : ℕ) * (↑d : ℕ) + x * (↑ur.b : ℕ), y * (↑d : ℕ) + (↑z : ℕ) * (↑ur.b : ℕ)) = ((↑a : ℕ), (↑b : ℕ)) := ⋯
⊢ ((↑a' : ℕ) * (↑d : ℕ), (↑b' : ℕ) * (↑d : ℕ)) = ((↑a : ℕ), (↑b : ℕ))

Tactic:
rw [← hb, ← add_mul, ← add_mul, ← ha', ← hb'] at hv

Premises used: add_mul
-- Module: Mathlib.Data.PNat.Xgcd
Goal:
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
hb : d = ur.b
ha' : (↑a' : ℕ) = (↑w : ℕ) + x
hb' : (↑b' : ℕ) = y + (↑z : ℕ)
hdet : w * z = (x * y).succPNat
hdet' : (↑w : ℕ) * (↑z : ℕ) = x * y + 1
hv : ((↑a' : ℕ) * (↑d : ℕ), (↑b' : ℕ) * (↑d : ℕ)) = ((↑a : ℕ), (↑b : ℕ))
⊢ (↑a : ℕ) = (↑a' : ℕ) * (↑d : ℕ)

Tactic:
have ha'' : (a : ℕ) = a' * d := (congr_arg Prod.fst hv).symm
-- Module: Mathlib.Data.PNat.Xgcd
Goal:
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
hb : d = ur.b
ha' : (↑a' : ℕ) = (↑w : ℕ) + x
hb' : (↑b' : ℕ) = y + (↑z : ℕ)
hdet : w * z = (x * y).succPNat
hdet' : (↑w : ℕ) * (↑z : ℕ) = x * y + 1
hv : ((↑a' : ℕ) * (↑d : ℕ), (↑b' : ℕ) * (↑d : ℕ)) = ((↑a : ℕ), (↑b : ℕ))
ha'' : (↑a : ℕ) = (↑a' : ℕ) * (↑d : ℕ)
⊢ (↑b : ℕ) = (↑b' : ℕ) * (↑d : ℕ)

Tactic:
have hb'' : (b : ℕ) = b' * d := (congr_arg Prod.snd hv).symm
-- Module: Mathlib.Data.PNat.Xgcd
Goal:
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
hb : d = ur.b
ha' : (↑a' : ℕ) = (↑w : ℕ) + x
hb' : (↑b' : ℕ) = y + (↑z : ℕ)
hdet : w * z = (x * y).succPNat
hdet' : (↑w : ℕ) * (↑z : ℕ) = x * y + 1
hv : ((↑a' : ℕ) * (↑d : ℕ), (↑b' : ℕ) * (↑d : ℕ)) = ((↑a : ℕ), (↑b : ℕ))
ha'' : (↑a : ℕ) = (↑a' : ℕ) * (↑d : ℕ)
hb'' : (↑b : ℕ) = (↑b' : ℕ) * (↑d : ℕ)
right : a = a' * d
right₁ :
  b = b' * d ∧
    z * a' = (x * (↑b' : ℕ)).succPNat ∧
      w * b' = (y * (↑a' : ℕ)).succPNat ∧
        (↑z : ℕ) * (↑a : ℕ) = x * (↑b : ℕ) + (↑d : ℕ) ∧ (↑w : ℕ) * (↑b : ℕ) = y * (↑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 : ℕ)

Tactic:
constructor
-- Module: Mathlib.Data.PNat.Xgcd
Goal:
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
hb : d = ur.b
ha' : (↑a' : ℕ) = (↑w : ℕ) + x
hb' : (↑b' : ℕ) = y + (↑z : ℕ)
hdet : w * z = (x * y).succPNat
hdet' : (↑w : ℕ) * (↑z : ℕ) = x * y + 1
hv : ((↑a' : ℕ) * (↑d : ℕ), (↑b' : ℕ) * (↑d : ℕ)) = ((↑a : ℕ), (↑b : ℕ))
ha'' : (↑a : ℕ) = (↑a' : ℕ) * (↑d : ℕ)
hb'' : (↑b : ℕ) = (↑b' : ℕ) * (↑d : ℕ)
⊢ a = a' * d

Tactic:
eq ha''

Premises used: PNat.eq
-- Module: Mathlib.Data.PNat.Xgcd
Goal:
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
hb : d = ur.b
ha' : (↑a' : ℕ) = (↑w : ℕ) + x
hb' : (↑b' : ℕ) = y + (↑z : ℕ)
hdet : w * z = (x * y).succPNat
hdet' : (↑w : ℕ) * (↑z : ℕ) = x * y + 1
hv : ((↑a' : ℕ) * (↑d : ℕ), (↑b' : ℕ) * (↑d : ℕ)) = ((↑a : ℕ), (↑b : ℕ))
ha'' : (↑a : ℕ) = (↑a' : ℕ) * (↑d : ℕ)
hb'' : (↑b : ℕ) = (↑b' : ℕ) * (↑d : ℕ)
⊢ a = a' * d

Tactic:
exact eq ha''

Premises used: PNat.eq
-- Module: Mathlib.Data.PNat.Xgcd
Goal:
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
hb : d = ur.b
ha' : (↑a' : ℕ) = (↑w : ℕ) + x
hb' : (↑b' : ℕ) = y + (↑z : ℕ)
hdet : w * z = (x * y).succPNat
hdet' : (↑w : ℕ) * (↑z : ℕ) = x * y + 1
hv : ((↑a' : ℕ) * (↑d : ℕ), (↑b' : ℕ) * (↑d : ℕ)) = ((↑a : ℕ), (↑b : ℕ))
ha'' : (↑a : ℕ) = (↑a' : ℕ) * (↑d : ℕ)
hb'' : (↑b : ℕ) = (↑b' : ℕ) * (↑d : ℕ)
right : b = b' * d
right₁ :
  z * a' = (x * (↑b' : ℕ)).succPNat ∧
    w * b' = (y * (↑a' : ℕ)).succPNat ∧
      (↑z : ℕ) * (↑a : ℕ) = x * (↑b : ℕ) + (↑d : ℕ) ∧ (↑w : ℕ) * (↑b : ℕ) = y * (↑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:
constructor
-- Module: Mathlib.Data.PNat.Xgcd
Goal:
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
hb : d = ur.b
ha' : (↑a' : ℕ) = (↑w : ℕ) + x
hb' : (↑b' : ℕ) = y + (↑z : ℕ)
hdet : w * z = (x * y).succPNat
hdet' : (↑w : ℕ) * (↑z : ℕ) = x * y + 1
hv : ((↑a' : ℕ) * (↑d : ℕ), (↑b' : ℕ) * (↑d : ℕ)) = ((↑a : ℕ), (↑b : ℕ))
ha'' : (↑a : ℕ) = (↑a' : ℕ) * (↑d : ℕ)
hb'' : (↑b : ℕ) = (↑b' : ℕ) * (↑d : ℕ)
⊢ b = b' * d

Tactic:
eq hb''

Premises used: PNat.eq
-- Module: Mathlib.Data.PNat.Xgcd
Goal:
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
hb : d = ur.b
ha' : (↑a' : ℕ) = (↑w : ℕ) + x
hb' : (↑b' : ℕ) = y + (↑z : ℕ)
hdet : w * z = (x * y).succPNat
hdet' : (↑w : ℕ) * (↑z : ℕ) = x * y + 1
hv : ((↑a' : ℕ) * (↑d : ℕ), (↑b' : ℕ) * (↑d : ℕ)) = ((↑a : ℕ), (↑b : ℕ))
ha'' : (↑a : ℕ) = (↑a' : ℕ) * (↑d : ℕ)
hb'' : (↑b : ℕ) = (↑b' : ℕ) * (↑d : ℕ)
⊢ b = b' * d

Tactic:
exact eq hb''

Premises used: PNat.eq
-- Module: Mathlib.Data.PNat.Xgcd
Goal:
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
hb : d = ur.b
ha' : (↑a' : ℕ) = (↑w : ℕ) + x
hb' : (↑b' : ℕ) = y + (↑z : ℕ)
hdet : w * z = (x * y).succPNat
hdet' : (↑w : ℕ) * (↑z : ℕ) = x * y + 1
hv : ((↑a' : ℕ) * (↑d : ℕ), (↑b' : ℕ) * (↑d : ℕ)) = ((↑a : ℕ), (↑b : ℕ))
ha'' : (↑a : ℕ) = (↑a' : ℕ) * (↑d : ℕ)
hb'' : (↑b : ℕ) = (↑b' : ℕ) * (↑d : ℕ)
rw : x * y + 1 + (↑z : ℕ) * x = x * y + x * (↑z : ℕ) + 1
⊢ (↑z : ℕ) * (↑a' : ℕ) = x * (↑b' : ℕ) + 1

Tactic:
rw [ha', hb', mul_add, mul_add, mul_comm (z : ℕ), hdet']

Premises used: PNat.val, mul_comm, mul_add
-- Module: Mathlib.Data.PNat.Xgcd
Goal:
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
hb : d = ur.b
ha' : (↑a' : ℕ) = (↑w : ℕ) + x
hb' : (↑b' : ℕ) = y + (↑z : ℕ)
hdet : w * z = (x * y).succPNat
hdet' : (↑w : ℕ) * (↑z : ℕ) = x * y + 1
hv : ((↑a' : ℕ) * (↑d : ℕ), (↑b' : ℕ) * (↑d : ℕ)) = ((↑a : ℕ), (↑b : ℕ))
ha'' : (↑a : ℕ) = (↑a' : ℕ) * (↑d : ℕ)
hb'' : (↑b : ℕ) = (↑b' : ℕ) * (↑d : ℕ)
⊢ x * y + 1 + (↑z : ℕ) * x = x * y + x * (↑z : ℕ) + 1

Tactic:
ring
-- Module: Mathlib.Data.PNat.Xgcd
Goal:
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
hb : d = ur.b
ha' : (↑a' : ℕ) = (↑w : ℕ) + x
hb' : (↑b' : ℕ) = y + (↑z : ℕ)
hdet : w * z = (x * y).succPNat
hdet' : (↑w : ℕ) * (↑z : ℕ) = x * y + 1
hv : ((↑a' : ℕ) * (↑d : ℕ), (↑b' : ℕ) * (↑d : ℕ)) = ((↑a : ℕ), (↑b : ℕ))
ha'' : (↑a : ℕ) = (↑a' : ℕ) * (↑d : ℕ)
hb'' : (↑b : ℕ) = (↑b' : ℕ) * (↑d : ℕ)
⊢ (↑z : ℕ) * (↑a' : ℕ) = x * (↑b' : ℕ) + 1

Tactic:
have hza' : (z * a' : ℕ) = x * b' + 1 := by
    rw [ha', hb', mul_add, mul_add, mul_comm (z : ℕ), hdet']
    ring
-- Module: Mathlib.Data.PNat.Xgcd
Goal:
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
hb : d = ur.b
ha' : (↑a' : ℕ) = (↑w : ℕ) + x
hb' : (↑b' : ℕ) = y + (↑z : ℕ)
hdet : w * z = (x * y).succPNat
hdet' : (↑w : ℕ) * (↑z : ℕ) = x * y + 1
hv : ((↑a' : ℕ) * (↑d : ℕ), (↑b' : ℕ) * (↑d : ℕ)) = ((↑a : ℕ), (↑b : ℕ))
ha'' : (↑a : ℕ) = (↑a' : ℕ) * (↑d : ℕ)
hb'' : (↑b : ℕ) = (↑b' : ℕ) * (↑d : ℕ)
hza' : (↑z : ℕ) * (↑a' : ℕ) = x * (↑b' : ℕ) + 1
rw : (↑w : ℕ) * y + (x * y + 1) = y * (↑w : ℕ) + y * x + 1
⊢ (↑w : ℕ) * (↑b' : ℕ) = y * (↑a' : ℕ) + 1

Tactic:
rw [ha', hb', mul_add, mul_add, hdet']

Premises used: mul_add
-- Module: Mathlib.Data.PNat.Xgcd
Goal:
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
hb : d = ur.b
ha' : (↑a' : ℕ) = (↑w : ℕ) + x
hb' : (↑b' : ℕ) = y + (↑z : ℕ)
hdet : w * z = (x * y).succPNat
hdet' : (↑w : ℕ) * (↑z : ℕ) = x * y + 1
hv : ((↑a' : ℕ) * (↑d : ℕ), (↑b' : ℕ) * (↑d : ℕ)) = ((↑a : ℕ), (↑b : ℕ))
ha'' : (↑a : ℕ) = (↑a' : ℕ) * (↑d : ℕ)
hb'' : (↑b : ℕ) = (↑b' : ℕ) * (↑d : ℕ)
hza' : (↑z : ℕ) * (↑a' : ℕ) = x * (↑b' : ℕ) + 1
⊢ (↑w : ℕ) * y + (x * y + 1) = y * (↑w : ℕ) + y * x + 1

Tactic:
ring
-- Module: Mathlib.Data.PNat.Xgcd
Goal:
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
hb : d = ur.b
ha' : (↑a' : ℕ) = (↑w : ℕ) + x
hb' : (↑b' : ℕ) = y + (↑z : ℕ)
hdet : w * z = (x * y).succPNat
hdet' : (↑w : ℕ) * (↑z : ℕ) = x * y + 1
hv : ((↑a' : ℕ) * (↑d : ℕ), (↑b' : ℕ) * (↑d : ℕ)) = ((↑a : ℕ), (↑b : ℕ))
ha'' : (↑a : ℕ) = (↑a' : ℕ) * (↑d : ℕ)
hb'' : (↑b : ℕ) = (↑b' : ℕ) * (↑d : ℕ)
hza' : (↑z : ℕ) * (↑a' : ℕ) = x * (↑b' : ℕ) + 1
⊢ (↑w : ℕ) * (↑b' : ℕ) = y * (↑a' : ℕ) + 1

Tactic:
have hwb' : (w * b' : ℕ) = y * a' + 1 := by
    rw [ha', hb', mul_add, mul_add, hdet']
    ring
-- Module: Mathlib.Data.PNat.Xgcd
Goal:
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
hb : d = ur.b
ha' : (↑a' : ℕ) = (↑w : ℕ) + x
hb' : (↑b' : ℕ) = y + (↑z : ℕ)
hdet : w * z = (x * y).succPNat
hdet' : (↑w : ℕ) * (↑z : ℕ) = x * y + 1
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
right : z * a' = (x * (↑b' : ℕ)).succPNat
right₁ :
  w * b' = (y * (↑a' : ℕ)).succPNat ∧
    (↑z : ℕ) * (↑a : ℕ) = x * (↑b : ℕ) + (↑d : ℕ) ∧ (↑w : ℕ) * (↑b : ℕ) = y * (↑a : ℕ) + (↑d : ℕ)
⊢ z * a' = (x * (↑b' : ℕ)).succPNat ∧
    w * b' = (y * (↑a' : ℕ)).succPNat ∧
      (↑z : ℕ) * (↑a : ℕ) = x * (↑b : ℕ) + (↑d : ℕ) ∧ (↑w : ℕ) * (↑b : ℕ) = y * (↑a : ℕ) + (↑d : ℕ)

Tactic:
constructor
-- Module: Mathlib.Data.PNat.Xgcd
Goal:
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
hb : d = ur.b
ha' : (↑a' : ℕ) = (↑w : ℕ) + x
hb' : (↑b' : ℕ) = y + (↑z : ℕ)
hdet : w * z = (x * y).succPNat
hdet' : (↑w : ℕ) * (↑z : ℕ) = x * y + 1
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
right : (↑(z * a') : ℕ) = (↑(x * (↑b' : ℕ)).succPNat : ℕ)
⊢ z * a' = (x * (↑b' : ℕ)).succPNat

Tactic:
apply eq

Premises used: PNat.eq
-- Module: Mathlib.Data.PNat.Xgcd
Goal:
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
hb : d = ur.b
ha' : (↑a' : ℕ) = (↑w : ℕ) + x
hb' : (↑b' : ℕ) = y + (↑z : ℕ)
hdet : w * z = (x * y).succPNat
hdet' : (↑w : ℕ) * (↑z : ℕ) = x * y + 1
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
right : (↑(z * a') : ℕ) = (x * (↑b' : ℕ)).succ
right₁ : (↑(z * a') : ℕ) = x * (↑b' : ℕ) + 1
right₂ : (↑z : ℕ) * (↑a' : ℕ) = x * (↑b' : ℕ) + 1
right₃ right₄ : x * (↑b' : ℕ) + 1 = x * (↑b' : ℕ) + 1
⊢ (↑(z * a') : ℕ) = (↑(x * (↑b' : ℕ)).succPNat : ℕ)

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

Premises used: Nat.succ_eq_add_one, Nat.succPNat_coe, PNat.mul_coe
-- Module: Mathlib.Data.PNat.Xgcd
Goal:
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
hb : d = ur.b
ha' : (↑a' : ℕ) = (↑w : ℕ) + x
hb' : (↑b' : ℕ) = y + (↑z : ℕ)
hdet : w * z = (x * y).succPNat
hdet' : (↑w : ℕ) * (↑z : ℕ) = x * y + 1
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
right : w * b' = (y * (↑a' : ℕ)).succPNat
right₁ : (↑z : ℕ) * (↑a : ℕ) = x * (↑b : ℕ) + (↑d : ℕ) ∧ (↑w : ℕ) * (↑b : ℕ) = y * (↑a : ℕ) + (↑d : ℕ)
⊢ w * b' = (y * (↑a' : ℕ)).succPNat ∧
    (↑z : ℕ) * (↑a : ℕ) = x * (↑b : ℕ) + (↑d : ℕ) ∧ (↑w : ℕ) * (↑b : ℕ) = y * (↑a : ℕ) + (↑d : ℕ)

Tactic:
constructor
-- Module: Mathlib.Data.PNat.Xgcd
Goal:
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
hb : d = ur.b
ha' : (↑a' : ℕ) = (↑w : ℕ) + x
hb' : (↑b' : ℕ) = y + (↑z : ℕ)
hdet : w * z = (x * y).succPNat
hdet' : (↑w : ℕ) * (↑z : ℕ) = x * y + 1
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
right : (↑(w * b') : ℕ) = (↑(y * (↑a' : ℕ)).succPNat : ℕ)
⊢ w * b' = (y * (↑a' : ℕ)).succPNat

Tactic:
apply eq

Premises used: PNat.eq
-- Module: Mathlib.Data.PNat.Xgcd
Goal:
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
hb : d = ur.b
ha' : (↑a' : ℕ) = (↑w : ℕ) + x
hb' : (↑b' : ℕ) = y + (↑z : ℕ)
hdet : w * z = (x * y).succPNat
hdet' : (↑w : ℕ) * (↑z : ℕ) = x * y + 1
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
right : (↑(w * b') : ℕ) = (y * (↑a' : ℕ)).succ
right₁ : (↑(w * b') : ℕ) = y * (↑a' : ℕ) + 1
right₂ : (↑w : ℕ) * (↑b' : ℕ) = y * (↑a' : ℕ) + 1
right₃ right₄ : y * (↑a' : ℕ) + 1 = y * (↑a' : ℕ) + 1
⊢ (↑(w * b') : ℕ) = (↑(y * (↑a' : ℕ)).succPNat : ℕ)

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

Premises used: Nat.succ_eq_add_one, Nat.succPNat_coe, PNat.mul_coe