awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.PNat.Xgcd (goal)
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.a : ℕ) + (↑u.z : ℕ) * (↑u.b : ℕ)
have snd : u.y * (↑u.b : ℕ) + (u.y * u.qp + (↑u.z : ℕ)) * (↑u.b : ℕ) = u.y * ((↑u.b : ℕ) * (u.qp + 1)) + (↑u.z : ℕ) * (↑u.b : ℕ)
Tactic: rw [← ha, u.qp_eq hr]
-- Lean 4 proof step from Mathlib.Data.PNat.Xgcd (hypothesis)
Goal:
u : XgcdType
hr : u.r ≠ 0
⊢ u.r - 1 < u.bp
have h₀ : 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)
-- Lean 4 proof step from Mathlib.Data.PNat.Xgcd (hypothesis)
Goal:
u : XgcdType
hr : u.r ≠ 0
h₀ : u.r - 1 + 1 = u.r
⊢ u.r - 1 < u.bp
have h₁ : u.r < u.bp + 1
Tactic: have h₁ : u.r < u.bp + 1 := Nat.mod_lt (u.ap + 1) u.bp.succ_pos
-- Lean 4 proof step from Mathlib.Data.PNat.Xgcd (hypothesis)
Goal:
u : XgcdType
hr : u.r ≠ 0
h₀ : u.r - 1 + 1 = u.r
h₁ : u.r < u.bp + 1
⊢ u.r - 1 < u.bp
have h₂ : u.r - 1 + 1 < u.bp + 1
Tactic: rw [← h₀] at h₁
Cleared hypotheses: h₁
-- Lean 4 proof step from Mathlib.Data.PNat.Xgcd (goal)
Goal:
u : XgcdType
hs : u.IsSpecial
⊢ u.step.IsSpecial
have 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)
Tactic: dsimp [IsSpecial, step] at hs ⊢
-- Lean 4 proof step from Mathlib.Data.PNat.Xgcd (goal)
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.x)
have 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)
Tactic: rw [mul_add, mul_comm u.y u.x, ← hs]
-- Lean 4 proof step from Mathlib.Data.PNat.Xgcd (goal)
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.step.v = u.v.swap
have fst : u.step.v.1 = u.v.swap.1
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.PNat.Xgcd (goal)
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
⊢ u.step.v = u.v.swap
have snd : u.step.v.2 = u.v.swap.2
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.PNat.Xgcd (goal)
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.step.v.1 = u.v.swap.1
have fst : (u.y * u.q + (↑u.z : ℕ)) * (↑u.b : ℕ) + u.y * (u.r - 1 + 1) = u.y * (↑u.a : ℕ) + (↑u.z : ℕ) * (↑u.b : ℕ)
Tactic: change ((u.y * u.q + u.z) * u.b + u.y * (u.r - 1 + 1) : ℕ) = u.y * u.a + u.z * u.b
-- Lean 4 proof step from Mathlib.Data.PNat.Xgcd (goal)
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 - 1 + 1) = u.y * (↑u.a : ℕ) + (↑u.z : ℕ) * (↑u.b : ℕ)
have 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 : ℕ)
Tactic: rw [← ha, hr]
-- Lean 4 proof step from Mathlib.Data.PNat.Xgcd (goal)
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.step.v.2 = u.v.swap.2
have snd : ((↑u.w : ℕ) * u.q + u.x) * (↑u.b : ℕ) + (↑u.w : ℕ) * (u.r - 1 + 1) = (↑u.w : ℕ) * (↑u.a : ℕ) + u.x * (↑u.b : ℕ)
Tactic: change ((u.w * u.q + u.x) * u.b + u.w * (u.r - 1 + 1) : ℕ) = u.w * u.a + u.x * u.b
-- Lean 4 proof step from Mathlib.Data.PNat.Xgcd (goal)
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 - 1 + 1) = (↑u.w : ℕ) * (↑u.a : ℕ) + u.x * (↑u.b : ℕ)
have 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 : ℕ)
Tactic: rw [← ha, hr]
-- Lean 4 proof step from Mathlib.Data.PNat.Xgcd (goal)
Goal:
u : XgcdType
h : u.r = 0
⊢ u.reduce = u.finish
have rw : (if x : u.r = 0 then u.finish else u.step.reduce.flip) = u.finish
Tactic: rw [reduce]
-- Lean 4 proof step from Mathlib.Data.PNat.Xgcd (goal)
Goal:
u : XgcdType
h : u.r ≠ 0
⊢ u.reduce = u.step.reduce.flip
have rw : (if x : u.r = 0 then u.finish else u.step.reduce.flip) = u.step.reduce.flip
Tactic: rw [reduce]
-- Lean 4 proof step from Mathlib.Data.PNat.Xgcd (goal)
Goal:
x : XgcdType
u : XgcdType := x
h : u.r = 0
⊢ x.reduce.IsReduced
have rw : u.finish.IsReduced
Tactic: rw [reduce_a h]
-- Lean 4 proof step from Mathlib.Data.PNat.Xgcd (hypothesis)
Goal:
x : XgcdType
u : XgcdType := x
h : ¬u.r = 0
⊢ x.reduce.IsReduced
have this : sizeOf u.step < sizeOf u
Tactic: have : SizeOf.sizeOf u.step < SizeOf.sizeOf u := u.step_wf h
-- Lean 4 proof step from Mathlib.Data.PNat.Xgcd (goal)
Goal:
x : XgcdType
u : XgcdType := x
h : ¬u.r = 0
this : sizeOf u.step < sizeOf u
⊢ x.reduce.IsReduced
have rw : u.step.reduce.IsReduced
Tactic: rw [reduce_b h, flip_isReduced]
-- Lean 4 proof step from Mathlib.Data.PNat.Xgcd (goal)
Goal:
x : XgcdType
u : XgcdType := x
h : u.r = 0
hs : x.IsSpecial
⊢ x.reduce.IsSpecial
have rw : u.finish.IsSpecial
Tactic: rw [reduce_a h]
-- Lean 4 proof step from Mathlib.Data.PNat.Xgcd (hypothesis)
Goal:
x : XgcdType
u : XgcdType := x
h : ¬u.r = 0
hs : x.IsSpecial
⊢ x.reduce.IsSpecial
have this : sizeOf u.step < sizeOf u
Tactic: have : SizeOf.sizeOf u.step < SizeOf.sizeOf u := u.step_wf h
-- Lean 4 proof step from Mathlib.Data.PNat.Xgcd (goal)
Goal:
x : XgcdType
u : XgcdType := x
h : ¬u.r = 0
hs : x.IsSpecial
this : sizeOf u.step < sizeOf u
⊢ x.reduce.IsSpecial
have rw : u.step.reduce.flip.IsSpecial
Tactic: rw [reduce_b h]
-- Lean 4 proof step from Mathlib.Data.PNat.Xgcd (goal)
Goal:
x : XgcdType
u : XgcdType := x
h : u.r = 0
⊢ x.reduce.v = x.v
have rw : u.finish.v = x.v
Tactic: rw [reduce_a h, finish_v u h]
-- Lean 4 proof step from Mathlib.Data.PNat.Xgcd (goal)
Goal:
x : XgcdType
u : XgcdType := x
h : u.r = 0
rw : u.finish.v = x.v
⊢ x.reduce.v = x.v
have rw₁ : u.v = x.v
Tactic: rw [reduce_a h, finish_v u h]
-- Lean 4 proof step from Mathlib.Data.PNat.Xgcd (hypothesis)
Goal:
x : XgcdType
u : XgcdType := x
h : ¬u.r = 0
⊢ x.reduce.v = x.v
have this : sizeOf u.step < sizeOf u
Tactic: have : SizeOf.sizeOf u.step < SizeOf.sizeOf u := u.step_wf h
-- Lean 4 proof step from Mathlib.Data.PNat.Xgcd (goal)
Goal:
x : XgcdType
u : XgcdType := x
h : ¬u.r = 0
this : sizeOf u.step < sizeOf u
⊢ x.reduce.v = x.v
have rw : u.step.reduce.flip.v = x.v
Tactic: rw [reduce_b h, flip_v, reduce_v (step u), step_v u h, Prod.swap_swap]
-- Lean 4 proof step from Mathlib.Data.PNat.Xgcd (goal)
Goal:
x : XgcdType
u : XgcdType := x
h : ¬u.r = 0
this : sizeOf u.step < sizeOf u
rw : u.step.reduce.flip.v = x.v
⊢ x.reduce.v = x.v
have rw₁ : u.step.reduce.v.swap = x.v
Tactic: rw [reduce_b h, flip_v, reduce_v (step u), step_v u h, Prod.swap_swap]
-- Lean 4 proof step from Mathlib.Data.PNat.Xgcd (goal)
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
⊢ x.reduce.v = x.v
have rw₂ : u.step.v.swap = x.v
Tactic: rw [reduce_b h, flip_v, reduce_v (step u), step_v u h, Prod.swap_swap]
-- Lean 4 proof step from Mathlib.Data.PNat.Xgcd (goal)
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
⊢ x.reduce.v = x.v
have rw₃ : u.v.swap.swap = x.v
Tactic: rw [reduce_b h, flip_v, reduce_v (step u), step_v u h, Prod.swap_swap]
-- Lean 4 proof step from Mathlib.Data.PNat.Xgcd (goal)
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
⊢ x.reduce.v = x.v
have rw₄ : u.v = x.v
Tactic: rw [reduce_b h, flip_v, reduce_v (step u), step_v u h, Prod.swap_swap]
-- Lean 4 proof step from Mathlib.Data.PNat.Xgcd (goal)
Goal:
a b : ℕ+
⊢ (a.xgcd b).wp + (a.xgcd b).x + 1 = (a.xgcd b).wp + 1 + (a.xgcd b).x
have rw : (a.xgcd b).wp + 1 + (a.xgcd b).x = (a.xgcd b).wp + 1 + (a.xgcd b).x
Tactic: rw [add_right_comm]
-- Lean 4 proof step from Mathlib.Data.PNat.Xgcd (goal)
Goal:
a b : ℕ+
⊢ (a.xgcd b).y + (a.xgcd b).zp + 1 = (a.xgcd b).y + ((a.xgcd b).zp + 1)
have rw : (a.xgcd b).y + ((a.xgcd b).zp + 1) = (a.xgcd b).y + ((a.xgcd b).zp + 1)
Tactic: rw [add_assoc]
-- Lean 4 proof step from Mathlib.Data.PNat.Xgcd (hypothesis)
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
⊢ 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 : ℕ)
have hb : d = ur.b
Tactic: have hb : d = ur.b := u.reduce_isReduced'
-- Lean 4 proof step from Mathlib.Data.PNat.Xgcd (hypothesis)
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
⊢ 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 : ℕ)
have ha' : (↑a' : ℕ) = (↑w : ℕ) + x
Tactic: have ha' : (a' : ℕ) = w + x := gcdA'_coe a b
-- Lean 4 proof step from Mathlib.Data.PNat.Xgcd (hypothesis)
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
⊢ 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 : ℕ)
have hb' : (↑b' : ℕ) = y + (↑z : ℕ)
Tactic: have hb' : (b' : ℕ) = y + z := gcdB'_coe a b
-- Lean 4 proof step from Mathlib.Data.PNat.Xgcd (hypothesis)
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 ∧
    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 : ℕ)
have hdet : w * z = (x * y).succPNat
Tactic: have hdet : w * z = succPNat (x * y) := u.reduce_isSpecial' rfl
-- Lean 4 proof step from Mathlib.Data.PNat.Xgcd (goal)
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
⊢ 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 : ℕ)
have 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 : ℕ)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.PNat.Xgcd (goal)
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
have rw : (↑(w * z) : ℕ) = x * y + 1
Tactic: rw [← mul_coe, hdet, succPNat_coe]
-- Lean 4 proof step from Mathlib.Data.PNat.Xgcd (goal)
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
⊢ (↑w : ℕ) * (↑z : ℕ) = x * y + 1
have rw₁ : (↑(x * y).succPNat : ℕ) = x * y + 1
Tactic: rw [← mul_coe, hdet, succPNat_coe]
-- Lean 4 proof step from Mathlib.Data.PNat.Xgcd (goal)
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
⊢ (↑w : ℕ) * (↑z : ℕ) = x * y + 1
have rw₂ : (x * y).succ = x * y + 1
Tactic: rw [← mul_coe, hdet, succPNat_coe]
-- Lean 4 proof step from Mathlib.Data.PNat.Xgcd (hypothesis)
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
⊢ 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 : ℕ)
have hdet' : (↑w : ℕ) * (↑z : ℕ) = x * y + 1
Tactic: have hdet' : (w * z : ℕ) = x * y + 1 := by rw [← mul_coe, hdet, succPNat_coe]
-- Lean 4 proof step from Mathlib.Data.PNat.Xgcd (hypothesis)
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 = 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 : ℕ)
have hv₁ : ((↑a' : ℕ) * (↑d : ℕ), (↑b' : ℕ) * (↑d : ℕ)) = ((↑a : ℕ), (↑b : ℕ))
Tactic: rw [← hb, ← add_mul, ← add_mul, ← ha', ← hb'] at hv
Cleared hypotheses: hv
-- Lean 4 proof step from Mathlib.Data.PNat.Xgcd (hypothesis)
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 ∧
    b = b' * d ∧
      z * a' = (x * (↑b' : ℕ)).succPNat ∧
        w * b' = (y * (↑a' : ℕ)).succPNat ∧
          (↑z : ℕ) * (↑a : ℕ) = x * (↑b : ℕ) + (↑d : ℕ) ∧ (↑w : ℕ) * (↑b : ℕ) = y * (↑a : ℕ) + (↑d : ℕ)
have ha'' : (↑a : ℕ) = (↑a' : ℕ) * (↑d : ℕ)
Tactic: have ha'' : (a : ℕ) = a' * d := (congr_arg Prod.fst hv).symm
-- Lean 4 proof step from Mathlib.Data.PNat.Xgcd (hypothesis)
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 : ℕ)
⊢ 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 : ℕ)
have hb'' : (↑b : ℕ) = (↑b' : ℕ) * (↑d : ℕ)
Tactic: have hb'' : (b : ℕ) = b' * d := (congr_arg Prod.snd hv).symm
-- Lean 4 proof step from Mathlib.Data.PNat.Xgcd (goal)
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 ∧
    b = b' * d ∧
      z * a' = (x * (↑b' : ℕ)).succPNat ∧
        w * b' = (y * (↑a' : ℕ)).succPNat ∧
          (↑z : ℕ) * (↑a : ℕ) = x * (↑b : ℕ) + (↑d : ℕ) ∧ (↑w : ℕ) * (↑b : ℕ) = y * (↑a : ℕ) + (↑d : ℕ)
have right : a = a' * d
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.PNat.Xgcd (goal)
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
⊢ 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 : ℕ)
have right₁ : 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
-- Lean 4 proof step from Mathlib.Data.PNat.Xgcd (goal)
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 ∧
    z * a' = (x * (↑b' : ℕ)).succPNat ∧
      w * b' = (y * (↑a' : ℕ)).succPNat ∧
        (↑z : ℕ) * (↑a : ℕ) = x * (↑b : ℕ) + (↑d : ℕ) ∧ (↑w : ℕ) * (↑b : ℕ) = y * (↑a : ℕ) + (↑d : ℕ)
have right : b = b' * d
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.PNat.Xgcd (goal)
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
⊢ b = b' * d ∧
    z * a' = (x * (↑b' : ℕ)).succPNat ∧
      w * b' = (y * (↑a' : ℕ)).succPNat ∧
        (↑z : ℕ) * (↑a : ℕ) = x * (↑b : ℕ) + (↑d : ℕ) ∧ (↑w : ℕ) * (↑b : ℕ) = y * (↑a : ℕ) + (↑d : ℕ)
have right₁ : z * a' = (x * (↑b' : ℕ)).succPNat ∧
  w * b' = (y * (↑a' : ℕ)).succPNat ∧
    (↑z : ℕ) * (↑a : ℕ) = x * (↑b : ℕ) + (↑d : ℕ) ∧ (↑w : ℕ) * (↑b : ℕ) = y * (↑a : ℕ) + (↑d : ℕ)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.PNat.Xgcd (goal)
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
have rw : x * y + 1 + (↑z : ℕ) * x = x * y + x * (↑z : ℕ) + 1
Tactic: rw [ha', hb', mul_add, mul_add, mul_comm (z : ℕ), hdet']
-- Lean 4 proof step from Mathlib.Data.PNat.Xgcd (hypothesis)
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' : ℕ)).succPNat ∧
    w * b' = (y * (↑a' : ℕ)).succPNat ∧
      (↑z : ℕ) * (↑a : ℕ) = x * (↑b : ℕ) + (↑d : ℕ) ∧ (↑w : ℕ) * (↑b : ℕ) = y * (↑a : ℕ) + (↑d : ℕ)
have hza' : (↑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
-- Lean 4 proof step from Mathlib.Data.PNat.Xgcd (goal)
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
have rw : (↑w : ℕ) * y + (x * y + 1) = y * (↑w : ℕ) + y * x + 1
Tactic: rw [ha', hb', mul_add, mul_add, hdet']
-- Lean 4 proof step from Mathlib.Data.PNat.Xgcd (hypothesis)
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
⊢ z * a' = (x * (↑b' : ℕ)).succPNat ∧
    w * b' = (y * (↑a' : ℕ)).succPNat ∧
      (↑z : ℕ) * (↑a : ℕ) = x * (↑b : ℕ) + (↑d : ℕ) ∧ (↑w : ℕ) * (↑b : ℕ) = y * (↑a : ℕ) + (↑d : ℕ)
have hwb' : (↑w : ℕ) * (↑b' : ℕ) = y * (↑a' : ℕ) + 1
Tactic: have hwb' : (w * b' : ℕ) = y * a' + 1 := by
    rw [ha', hb', mul_add, mul_add, hdet']
    ring