awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
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 : ℕ)
have right : z * a' = (x * (↑b' : ℕ)).succPNat
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 : ℕ)
hza' : (↑z : ℕ) * (↑a' : ℕ) = x * (↑b' : ℕ) + 1
hwb' : (↑w : ℕ) * (↑b' : ℕ) = y * (↑a' : ℕ) + 1
right : z * a' = (x * (↑b' : ℕ)).succPNat
⊢ z * a' = (x * (↑b' : ℕ)).succPNat ∧
    w * b' = (y * (↑a' : ℕ)).succPNat ∧
      (↑z : ℕ) * (↑a : ℕ) = x * (↑b : ℕ) + (↑d : ℕ) ∧ (↑w : ℕ) * (↑b : ℕ) = y * (↑a : ℕ) + (↑d : ℕ)
have right₁ : 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 : ℕ)
hza' : (↑z : ℕ) * (↑a' : ℕ) = x * (↑b' : ℕ) + 1
hwb' : (↑w : ℕ) * (↑b' : ℕ) = y * (↑a' : ℕ) + 1
⊢ z * a' = (x * (↑b' : ℕ)).succPNat
have right : (↑(z * a') : ℕ) = (↑(x * (↑b' : ℕ)).succPNat : ℕ)
Tactic: apply eq
-- 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
hwb' : (↑w : ℕ) * (↑b' : ℕ) = y * (↑a' : ℕ) + 1
⊢ (↑(z * a') : ℕ) = (↑(x * (↑b' : ℕ)).succPNat : ℕ)
have right : (↑(z * a') : ℕ) = (x * (↑b' : ℕ)).succ
Tactic: rw [succPNat_coe, Nat.succ_eq_add_one, mul_coe, hza']
-- 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
hwb' : (↑w : ℕ) * (↑b' : ℕ) = y * (↑a' : ℕ) + 1
right : (↑(z * a') : ℕ) = (x * (↑b' : ℕ)).succ
right₁ : (↑(z * a') : ℕ) = x * (↑b' : ℕ) + 1
right₂ : (↑z : ℕ) * (↑a' : ℕ) = x * (↑b' : ℕ) + 1
⊢ (↑(z * a') : ℕ) = (↑(x * (↑b' : ℕ)).succPNat : ℕ)
have right₃ : x * (↑b' : ℕ) + 1 = x * (↑b' : ℕ) + 1
Tactic: rw [succPNat_coe, Nat.succ_eq_add_one, mul_coe, hza']
-- 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
hwb' : (↑w : ℕ) * (↑b' : ℕ) = y * (↑a' : ℕ) + 1
⊢ w * b' = (y * (↑a' : ℕ)).succPNat ∧
    (↑z : ℕ) * (↑a : ℕ) = x * (↑b : ℕ) + (↑d : ℕ) ∧ (↑w : ℕ) * (↑b : ℕ) = y * (↑a : ℕ) + (↑d : ℕ)
have right : w * b' = (y * (↑a' : ℕ)).succPNat
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 : ℕ)
hza' : (↑z : ℕ) * (↑a' : ℕ) = x * (↑b' : ℕ) + 1
hwb' : (↑w : ℕ) * (↑b' : ℕ) = y * (↑a' : ℕ) + 1
right : w * b' = (y * (↑a' : ℕ)).succPNat
⊢ w * b' = (y * (↑a' : ℕ)).succPNat ∧
    (↑z : ℕ) * (↑a : ℕ) = x * (↑b : ℕ) + (↑d : ℕ) ∧ (↑w : ℕ) * (↑b : ℕ) = y * (↑a : ℕ) + (↑d : ℕ)
have right₁ : (↑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 : ℕ)
hza' : (↑z : ℕ) * (↑a' : ℕ) = x * (↑b' : ℕ) + 1
hwb' : (↑w : ℕ) * (↑b' : ℕ) = y * (↑a' : ℕ) + 1
⊢ w * b' = (y * (↑a' : ℕ)).succPNat
have right : (↑(w * b') : ℕ) = (↑(y * (↑a' : ℕ)).succPNat : ℕ)
Tactic: apply eq
-- 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
hwb' : (↑w : ℕ) * (↑b' : ℕ) = y * (↑a' : ℕ) + 1
⊢ (↑(w * b') : ℕ) = (↑(y * (↑a' : ℕ)).succPNat : ℕ)
have right : (↑(w * b') : ℕ) = (y * (↑a' : ℕ)).succ
Tactic: rw [succPNat_coe, Nat.succ_eq_add_one, mul_coe, hwb']
-- 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
hwb' : (↑w : ℕ) * (↑b' : ℕ) = y * (↑a' : ℕ) + 1
right : (↑(w * b') : ℕ) = (y * (↑a' : ℕ)).succ
right₁ : (↑(w * b') : ℕ) = y * (↑a' : ℕ) + 1
right₂ : (↑w : ℕ) * (↑b' : ℕ) = y * (↑a' : ℕ) + 1
⊢ (↑(w * b') : ℕ) = (↑(y * (↑a' : ℕ)).succPNat : ℕ)
have right₃ : y * (↑a' : ℕ) + 1 = y * (↑a' : ℕ) + 1
Tactic: rw [succPNat_coe, Nat.succ_eq_add_one, mul_coe, hwb']
-- Lean 4 proof step from Mathlib.Data.PNat.Xgcd (hypothesis)
Goal:
a b : ℕ+
⊢ a.gcdD b = a.gcd b
have left : a.gcdW b * a.gcdZ b = (a.gcdX b * a.gcdY b).succPNat
Tactic: rcases gcd_props a b with ⟨_, h₁, h₂, _, _, h₅, _⟩
-- Lean 4 proof step from Mathlib.Data.PNat.Xgcd (hypothesis)
Goal:
a b : ℕ+
left : a.gcdW b * a.gcdZ b = (a.gcdX b * a.gcdY b).succPNat
⊢ a.gcdD b = a.gcd b
have h₁ : a = a.gcdA' b * a.gcdD b
Tactic: rcases gcd_props a b with ⟨_, h₁, h₂, _, _, h₅, _⟩
-- Lean 4 proof step from Mathlib.Data.PNat.Xgcd (hypothesis)
Goal:
a b : ℕ+
left : a.gcdW b * a.gcdZ b = (a.gcdX b * a.gcdY b).succPNat
h₁ : a = a.gcdA' b * a.gcdD b
⊢ a.gcdD b = a.gcd b
have h₂ : b = a.gcdB' b * a.gcdD b
Tactic: rcases gcd_props a b with ⟨_, h₁, h₂, _, _, h₅, _⟩
-- Lean 4 proof step from Mathlib.Data.PNat.Xgcd (hypothesis)
Goal:
a b : ℕ+
left : a.gcdW b * a.gcdZ b = (a.gcdX b * a.gcdY b).succPNat
h₁ : a = a.gcdA' b * a.gcdD b
h₂ : b = a.gcdB' b * a.gcdD b
⊢ a.gcdD b = a.gcd b
have left₁ : a.gcdZ b * a.gcdA' b = (a.gcdX b * (↑(a.gcdB' b) : ℕ)).succPNat
Tactic: rcases gcd_props a b with ⟨_, h₁, h₂, _, _, h₅, _⟩
-- Lean 4 proof step from Mathlib.Data.PNat.Xgcd (hypothesis)
Goal:
a b : ℕ+
left : a.gcdW b * a.gcdZ b = (a.gcdX b * a.gcdY b).succPNat
h₁ : a = a.gcdA' b * a.gcdD b
h₂ : b = a.gcdB' b * a.gcdD b
left₁ : a.gcdZ b * a.gcdA' b = (a.gcdX b * (↑(a.gcdB' b) : ℕ)).succPNat
⊢ a.gcdD b = a.gcd b
have left₂ : a.gcdW b * a.gcdB' b = (a.gcdY b * (↑(a.gcdA' b) : ℕ)).succPNat
Tactic: rcases gcd_props a b with ⟨_, h₁, h₂, _, _, h₅, _⟩
-- Lean 4 proof step from Mathlib.Data.PNat.Xgcd (hypothesis)
Goal:
a b : ℕ+
left : a.gcdW b * a.gcdZ b = (a.gcdX b * a.gcdY b).succPNat
h₁ : a = a.gcdA' b * a.gcdD b
h₂ : b = a.gcdB' b * a.gcdD b
left₁ : a.gcdZ b * a.gcdA' b = (a.gcdX b * (↑(a.gcdB' b) : ℕ)).succPNat
left₂ : a.gcdW b * a.gcdB' b = (a.gcdY b * (↑(a.gcdA' b) : ℕ)).succPNat
⊢ a.gcdD b = a.gcd b
have h₅ : (↑(a.gcdZ b) : ℕ) * (↑a : ℕ) = a.gcdX b * (↑b : ℕ) + (↑(a.gcdD b) : ℕ)
Tactic: rcases gcd_props a b with ⟨_, h₁, h₂, _, _, h₅, _⟩
-- Lean 4 proof step from Mathlib.Data.PNat.Xgcd (hypothesis)
Goal:
a b : ℕ+
left : a.gcdW b * a.gcdZ b = (a.gcdX b * a.gcdY b).succPNat
h₁ : a = a.gcdA' b * a.gcdD b
h₂ : b = a.gcdB' b * a.gcdD b
left₁ : a.gcdZ b * a.gcdA' b = (a.gcdX b * (↑(a.gcdB' b) : ℕ)).succPNat
left₂ : a.gcdW b * a.gcdB' b = (a.gcdY b * (↑(a.gcdA' b) : ℕ)).succPNat
h₅ : (↑(a.gcdZ b) : ℕ) * (↑a : ℕ) = a.gcdX b * (↑b : ℕ) + (↑(a.gcdD b) : ℕ)
⊢ a.gcdD b = a.gcd b
have right : (↑(a.gcdW b) : ℕ) * (↑b : ℕ) = a.gcdY b * (↑a : ℕ) + (↑(a.gcdD b) : ℕ)
Tactic: rcases gcd_props a b with ⟨_, h₁, h₂, _, _, h₅, _⟩
-- Lean 4 proof step from Mathlib.Data.PNat.Xgcd (goal)
Goal:
a b : ℕ+
left : a.gcdW b * a.gcdZ b = (a.gcdX b * a.gcdY b).succPNat
h₁ : a = a.gcdA' b * a.gcdD b
h₂ : b = a.gcdB' b * a.gcdD b
left_1 : a.gcdZ b * a.gcdA' b = (a.gcdX b * (↑(a.gcdB' b) : ℕ)).succPNat
left_2 : a.gcdW b * a.gcdB' b = (a.gcdY b * (↑(a.gcdA' b) : ℕ)).succPNat
h₅ : (↑(a.gcdZ b) : ℕ) * (↑a : ℕ) = a.gcdX b * (↑b : ℕ) + (↑(a.gcdD b) : ℕ)
right : (↑(a.gcdW b) : ℕ) * (↑b : ℕ) = a.gcdY b * (↑a : ℕ) + (↑(a.gcdD b) : ℕ)
⊢ a.gcdD b = a.gcd b
have a₁ : a.gcdD b ∣ a.gcd b
Tactic: apply dvd_antisymm
-- Lean 4 proof step from Mathlib.Data.PNat.Xgcd (goal)
Goal:
a b : ℕ+
left : a.gcdW b * a.gcdZ b = (a.gcdX b * a.gcdY b).succPNat
h₁ : a = a.gcdA' b * a.gcdD b
h₂ : b = a.gcdB' b * a.gcdD b
left_1 : a.gcdZ b * a.gcdA' b = (a.gcdX b * (↑(a.gcdB' b) : ℕ)).succPNat
left_2 : a.gcdW b * a.gcdB' b = (a.gcdY b * (↑(a.gcdA' b) : ℕ)).succPNat
h₅ : (↑(a.gcdZ b) : ℕ) * (↑a : ℕ) = a.gcdX b * (↑b : ℕ) + (↑(a.gcdD b) : ℕ)
right : (↑(a.gcdW b) : ℕ) * (↑b : ℕ) = a.gcdY b * (↑a : ℕ) + (↑(a.gcdD b) : ℕ)
a₁ : a.gcdD b ∣ a.gcd b
⊢ a.gcdD b = a.gcd b
have a₂ : a.gcd b ∣ a.gcdD b
Tactic: apply dvd_antisymm
-- Lean 4 proof step from Mathlib.Data.PNat.Xgcd (goal)
Goal:
a b : ℕ+
left : a.gcdW b * a.gcdZ b = (a.gcdX b * a.gcdY b).succPNat
h₁ : a = a.gcdA' b * a.gcdD b
h₂ : b = a.gcdB' b * a.gcdD b
left_1 : a.gcdZ b * a.gcdA' b = (a.gcdX b * (↑(a.gcdB' b) : ℕ)).succPNat
left_2 : a.gcdW b * a.gcdB' b = (a.gcdY b * (↑(a.gcdA' b) : ℕ)).succPNat
h₅ : (↑(a.gcdZ b) : ℕ) * (↑a : ℕ) = a.gcdX b * (↑b : ℕ) + (↑(a.gcdD b) : ℕ)
right : (↑(a.gcdW b) : ℕ) * (↑b : ℕ) = a.gcdY b * (↑a : ℕ) + (↑(a.gcdD b) : ℕ)
⊢ a.gcdD b ∣ a.gcd b
have a₁ : a.gcdD b ∣ a
Tactic: apply dvd_gcd
-- Lean 4 proof step from Mathlib.Data.PNat.Xgcd (goal)
Goal:
a b : ℕ+
left : a.gcdW b * a.gcdZ b = (a.gcdX b * a.gcdY b).succPNat
h₁ : a = a.gcdA' b * a.gcdD b
h₂ : b = a.gcdB' b * a.gcdD b
left_1 : a.gcdZ b * a.gcdA' b = (a.gcdX b * (↑(a.gcdB' b) : ℕ)).succPNat
left_2 : a.gcdW b * a.gcdB' b = (a.gcdY b * (↑(a.gcdA' b) : ℕ)).succPNat
h₅ : (↑(a.gcdZ b) : ℕ) * (↑a : ℕ) = a.gcdX b * (↑b : ℕ) + (↑(a.gcdD b) : ℕ)
right : (↑(a.gcdW b) : ℕ) * (↑b : ℕ) = a.gcdY b * (↑a : ℕ) + (↑(a.gcdD b) : ℕ)
a₁ : a.gcdD b ∣ a
⊢ a.gcdD b ∣ a.gcd b
have a₂ : a.gcdD b ∣ b
Tactic: apply dvd_gcd
-- Lean 4 proof step from Mathlib.Data.PNat.Xgcd (hypothesis)
Goal:
a b : ℕ+
left : a.gcdW b * a.gcdZ b = (a.gcdX b * a.gcdY b).succPNat
h₁ : a = a.gcdA' b * a.gcdD b
h₂ : b = a.gcdB' b * a.gcdD b
left_1 : a.gcdZ b * a.gcdA' b = (a.gcdX b * (↑(a.gcdB' b) : ℕ)).succPNat
left_2 : a.gcdW b * a.gcdB' b = (a.gcdY b * (↑(a.gcdA' b) : ℕ)).succPNat
h₅ : (↑(a.gcdZ b) : ℕ) * (↑a : ℕ) = a.gcdX b * (↑b : ℕ) + (↑(a.gcdD b) : ℕ)
right : (↑(a.gcdW b) : ℕ) * (↑b : ℕ) = a.gcdY b * (↑a : ℕ) + (↑(a.gcdD b) : ℕ)
h₇ : (↑(a.gcd b) : ℕ) ∣ (↑(a.gcdZ b) : ℕ) * (↑a : ℕ)
h₈ : (↑(a.gcd b) : ℕ) ∣ a.gcdX b * (↑b : ℕ)
⊢ a.gcd b ∣ a.gcdD b
have h₉ : (↑(a.gcd b) : ℕ) ∣ a.gcdX b * (↑b : ℕ) + (↑(a.gcdD b) : ℕ)
Tactic: rw [h₅] at h₇
Cleared hypotheses: h₇, h₈
-- Lean 4 proof step from Mathlib.Data.PNat.Xgcd (goal)
Goal:
a b : ℕ+
left : a.gcdW b * a.gcdZ b = (a.gcdX b * a.gcdY b).succPNat
h₁ : a = a.gcdA' b * a.gcdD b
h₂ : b = a.gcdB' b * a.gcdD b
left_1 : a.gcdZ b * a.gcdA' b = (a.gcdX b * (↑(a.gcdB' b) : ℕ)).succPNat
left_2 : a.gcdW b * a.gcdB' b = (a.gcdY b * (↑(a.gcdA' b) : ℕ)).succPNat
h₅ : (↑(a.gcdZ b) : ℕ) * (↑a : ℕ) = a.gcdX b * (↑b : ℕ) + (↑(a.gcdD b) : ℕ)
right : (↑(a.gcdW b) : ℕ) * (↑b : ℕ) = a.gcdY b * (↑a : ℕ) + (↑(a.gcdD b) : ℕ)
h₇ : (↑(a.gcd b) : ℕ) ∣ a.gcdX b * (↑b : ℕ) + (↑(a.gcdD b) : ℕ)
h₈ : (↑(a.gcd b) : ℕ) ∣ a.gcdX b * (↑b : ℕ)
⊢ a.gcd b ∣ a.gcdD b
have a₁ : (↑(a.gcd b) : ℕ) ∣ (↑(a.gcdD b) : ℕ)
Tactic: rw [dvd_iff]
-- Lean 4 proof step from Mathlib.Data.PSigma.Order (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : Preorder ι
inst_1 : (i : ι) → Preorder (α i)
a₁ : ι
b₁ : α a₁
a₂ : ι
b₂ : α a₂
a₃ : ι
b₃ : α a₃
h : a₁ < a₂
h_1 : a₂ < a₃
⊢ mk (β := fun (i : ι) ↦ α i) a₁ b₁ ≤ mk (β := fun (i : ι) ↦ α i) a₃ b₃
have left : a₁ < a₃
Tactic: left
-- Lean 4 proof step from Mathlib.Data.PSigma.Order (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : Preorder ι
inst_1 : (i : ι) → Preorder (α i)
a₁ : ι
b₁ b₂ : α a₁
h : b₁ ≤ b₂
b₂_1 : α a₁
h_1 : b₂ ≤ b₂_1
⊢ mk (β := fun (i : ι) ↦ α i) a₁ b₁ ≤ mk (β := fun (i : ι) ↦ α i) a₁ b₂_1
have right : b₁ ≤ b₂_1
Tactic: right
-- Lean 4 proof step from Mathlib.Data.PSigma.Order (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : Preorder ι
inst_1 : (i : ι) → Preorder (α i)
⊢ ∀ (a b : Σₗ' (i : ι), α i), a < b ↔ a ≤ b ∧ ¬b ≤ a
have refine_1 : ∀ (a b : Σₗ' (i : ι), α i) (hab : a < b), ¬b ≤ a
Tactic: refine fun a b => ⟨fun hab => ⟨hab.mono_right fun i a b => le_of_lt, ?_⟩, ?_⟩
-- Lean 4 proof step from Mathlib.Data.PSigma.Order (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : Preorder ι
inst_1 : (i : ι) → Preorder (α i)
refine_1 : ∀ (a b : Σₗ' (i : ι), α i) (hab : a < b), ¬b ≤ a
⊢ ∀ (a b : Σₗ' (i : ι), α i), a < b ↔ a ≤ b ∧ ¬b ≤ a
have refine_2 : ∀ (a b : Σₗ' (i : ι), α i), a ≤ b ∧ ¬b ≤ a → a < b
Tactic: refine fun a b => ⟨fun hab => ⟨hab.mono_right fun i a b => le_of_lt, ?_⟩, ?_⟩
-- Lean 4 proof step from Mathlib.Data.PSigma.Order (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : Preorder ι
inst_1 : (i : ι) → Preorder (α i)
a₁ : ι
i : α a₁
a₂ : ι
a : α a₂
hji : a₁ < a₂
hab : mk (β := fun (i : ι) ↦ α i) a₂ a < mk (β := fun (i : ι) ↦ α i) a₁ i
⊢ False
have refine_1 : ∀ (hij : a₂ < a₁), False
Tactic: obtain ⟨_, _, hij⟩ | ⟨_, hab⟩ := hab
Cleared hypotheses: hab
-- Lean 4 proof step from Mathlib.Data.PSigma.Order (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : Preorder ι
inst_1 : (i : ι) → Preorder (α i)
a₁ : ι
i : α a₁
a₂ : ι
a : α a₂
hji : a₁ < a₂
hab : mk (β := fun (i : ι) ↦ α i) a₂ a < mk (β := fun (i : ι) ↦ α i) a₁ i
refine_1 : ∀ (hij : a₂ < a₁), False
⊢ False
have refine_1₁ : ∀ (a : α a₁) (hji : a₁ < a₁) (hab : a < i), False
Tactic: obtain ⟨_, _, hij⟩ | ⟨_, hab⟩ := hab
Cleared hypotheses: a₂, a, hji, hab
-- Lean 4 proof step from Mathlib.Data.PSigma.Order (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : Preorder ι
inst_1 : (i : ι) → Preorder (α i)
i : ι
b₁ b₂ : α i
hba : b₁ ≤ b₂
hab : mk (β := fun (i : ι) ↦ α i) i b₂ < mk (β := fun (i : ι) ↦ α i) i b₁
⊢ False
have refine_1 : ∀ (hij : i < i), False
Tactic: obtain ⟨_, _, hij⟩ | ⟨_, hab⟩ := hab
Cleared hypotheses: hab
-- Lean 4 proof step from Mathlib.Data.PSigma.Order (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : Preorder ι
inst_1 : (i : ι) → Preorder (α i)
i : ι
b₁ b₂ : α i
hba : b₁ ≤ b₂
hab : mk (β := fun (i : ι) ↦ α i) i b₂ < mk (β := fun (i : ι) ↦ α i) i b₁
refine_1 : ∀ (hij : i < i), False
⊢ False
have refine_1₁ : ∀ (hab : b₂ < b₁), False
Tactic: obtain ⟨_, _, hij⟩ | ⟨_, hab⟩ := hab
Cleared hypotheses: hab
-- Lean 4 proof step from Mathlib.Data.PSigma.Order (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : PartialOrder ι
inst_1 : (i : ι) → PartialOrder (α i)
a₁ : ι
b₁ b₂ : α a₁
hlt₁ : b₁ ≤ b₂
hlt₂ : b₂ ≤ b₁
⊢ mk (β := fun (i : ι) ↦ α i) a₁ b₁ = mk (β := fun (i : ι) ↦ α i) a₁ b₂
have right : mk (β := fun (i : ι) ↦ α i) a₁ b₂ = mk (β := fun (i : ι) ↦ α i) a₁ b₂
Tactic: rw [hlt₁.antisymm hlt₂]
-- Lean 4 proof step from Mathlib.Data.PSigma.Order (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : LinearOrder ι
inst_1 : (i : ι) → LinearOrder (α i)
i : ι
a : α i
j : ι
b : α j
⊢ mk (β := fun (i : ι) ↦ α i) i a ≤ mk (β := fun (i : ι) ↦ α i) j b ∨
    mk (β := fun (i : ι) ↦ α i) j b ≤ mk (β := fun (i : ι) ↦ α i) i a
have inl : ∀ (hij : i < j),
  mk (β := fun (i : ι) ↦ α i) i a ≤ mk (β := fun (i : ι) ↦ α i) j b ∨
    mk (β := fun (i : ι) ↦ α i) j b ≤ mk (β := fun (i : ι) ↦ α i) i a
Tactic: obtain hij | rfl | hji := lt_trichotomy i j
-- Lean 4 proof step from Mathlib.Data.PSigma.Order (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : LinearOrder ι
inst_1 : (i : ι) → LinearOrder (α i)
i : ι
a : α i
j : ι
b : α j
inl :
  ∀ (hij : i < j),
    mk (β := fun (i : ι) ↦ α i) i a ≤ mk (β := fun (i : ι) ↦ α i) j b ∨
      mk (β := fun (i : ι) ↦ α i) j b ≤ mk (β := fun (i : ι) ↦ α i) i a
⊢ mk (β := fun (i : ι) ↦ α i) i a ≤ mk (β := fun (i : ι) ↦ α i) j b ∨
    mk (β := fun (i : ι) ↦ α i) j b ≤ mk (β := fun (i : ι) ↦ α i) i a
have inr : ∀ (b : α i),
  mk (β := fun (i : ι) ↦ α i) i a ≤ mk (β := fun (i : ι) ↦ α i) i b ∨
    mk (β := fun (i : ι) ↦ α i) i b ≤ mk (β := fun (i : ι) ↦ α i) i a
Tactic: obtain hij | rfl | hji := lt_trichotomy i j
Cleared hypotheses: j, b
-- Lean 4 proof step from Mathlib.Data.PSigma.Order (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : LinearOrder ι
inst_1 : (i : ι) → LinearOrder (α i)
i : ι
a : α i
j : ι
b : α j
inl :
  ∀ (hij : i < j),
    mk (β := fun (i : ι) ↦ α i) i a ≤ mk (β := fun (i : ι) ↦ α i) j b ∨
      mk (β := fun (i : ι) ↦ α i) j b ≤ mk (β := fun (i : ι) ↦ α i) i a
inr :
  ∀ (b : α i),
    mk (β := fun (i : ι) ↦ α i) i a ≤ mk (β := fun (i : ι) ↦ α i) i b ∨
      mk (β := fun (i : ι) ↦ α i) i b ≤ mk (β := fun (i : ι) ↦ α i) i a
⊢ mk (β := fun (i : ι) ↦ α i) i a ≤ mk (β := fun (i : ι) ↦ α i) j b ∨
    mk (β := fun (i : ι) ↦ α i) j b ≤ mk (β := fun (i : ι) ↦ α i) i a
have inr₁ : ∀ (hji : j < i),
  mk (β := fun (i : ι) ↦ α i) i a ≤ mk (β := fun (i : ι) ↦ α i) j b ∨
    mk (β := fun (i : ι) ↦ α i) j b ≤ mk (β := fun (i : ι) ↦ α i) i a
Tactic: obtain hij | rfl | hji := lt_trichotomy i j
-- Lean 4 proof step from Mathlib.Data.PSigma.Order (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : LinearOrder ι
inst_1 : (i : ι) → LinearOrder (α i)
i : ι
a b : α i
⊢ mk (β := fun (i : ι) ↦ α i) i a ≤ mk (β := fun (i : ι) ↦ α i) i b ∨
    mk (β := fun (i : ι) ↦ α i) i b ≤ mk (β := fun (i : ι) ↦ α i) i a
have inr : ∀ (hab : a ≤ b),
  mk (β := fun (i : ι) ↦ α i) i a ≤ mk (β := fun (i : ι) ↦ α i) i b ∨
    mk (β := fun (i : ι) ↦ α i) i b ≤ mk (β := fun (i : ι) ↦ α i) i a
Tactic: obtain hab | hba := le_total a b
-- Lean 4 proof step from Mathlib.Data.PSigma.Order (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : LinearOrder ι
inst_1 : (i : ι) → LinearOrder (α i)
i : ι
a b : α i
inr :
  ∀ (hab : a ≤ b),
    mk (β := fun (i : ι) ↦ α i) i a ≤ mk (β := fun (i : ι) ↦ α i) i b ∨
      mk (β := fun (i : ι) ↦ α i) i b ≤ mk (β := fun (i : ι) ↦ α i) i a
⊢ mk (β := fun (i : ι) ↦ α i) i a ≤ mk (β := fun (i : ι) ↦ α i) i b ∨
    mk (β := fun (i : ι) ↦ α i) i b ≤ mk (β := fun (i : ι) ↦ α i) i a
have inr₁ : ∀ (hba : b ≤ a),
  mk (β := fun (i : ι) ↦ α i) i a ≤ mk (β := fun (i : ι) ↦ α i) i b ∨
    mk (β := fun (i : ι) ↦ α i) i b ≤ mk (β := fun (i : ι) ↦ α i) i a
Tactic: obtain hab | hba := le_total a b
-- Lean 4 proof step from Mathlib.Data.PSigma.Order (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : PartialOrder ι
inst_1 : OrderBot ι
inst_2 : (i : ι) → Preorder (α i)
inst_3 : OrderBot (α ⊥)
x : Σₗ' (i : ι), α i
a : ι
b : α a
⊢ mk (β := fun (i : ι) ↦ α i) ⊥ ⊥ ≤ mk (β := fun (i : ι) ↦ α i) a b
have inl : ∀ (b : α ⊥), mk (β := fun (i : ι) ↦ α i) ⊥ ⊥ ≤ mk (β := fun (i : ι) ↦ α i) ⊥ b
Tactic: obtain rfl | ha := eq_bot_or_bot_lt a
Cleared hypotheses: a, b
-- Lean 4 proof step from Mathlib.Data.PSigma.Order (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : PartialOrder ι
inst_1 : OrderBot ι
inst_2 : (i : ι) → Preorder (α i)
inst_3 : OrderBot (α ⊥)
x : Σₗ' (i : ι), α i
a : ι
b : α a
inl : ∀ (b : α ⊥), mk (β := fun (i : ι) ↦ α i) ⊥ ⊥ ≤ mk (β := fun (i : ι) ↦ α i) ⊥ b
⊢ mk (β := fun (i : ι) ↦ α i) ⊥ ⊥ ≤ mk (β := fun (i : ι) ↦ α i) a b
have inr : ∀ (ha : ⊥ < a), mk (β := fun (i : ι) ↦ α i) ⊥ ⊥ ≤ mk (β := fun (i : ι) ↦ α i) a b
Tactic: obtain rfl | ha := eq_bot_or_bot_lt a
-- Lean 4 proof step from Mathlib.Data.PSigma.Order (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : PartialOrder ι
inst_1 : OrderTop ι
inst_2 : (i : ι) → Preorder (α i)
inst_3 : OrderTop (α ⊤)
x : Σₗ' (i : ι), α i
a : ι
b : α a
⊢ mk (β := fun (i : ι) ↦ α i) a b ≤ mk (β := fun (i : ι) ↦ α i) ⊤ ⊤
have inl : ∀ (b : α ⊤), mk (β := fun (i : ι) ↦ α i) ⊤ b ≤ mk (β := fun (i : ι) ↦ α i) ⊤ ⊤
Tactic: obtain rfl | ha := eq_top_or_lt_top a
Cleared hypotheses: a, b
-- Lean 4 proof step from Mathlib.Data.PSigma.Order (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : PartialOrder ι
inst_1 : OrderTop ι
inst_2 : (i : ι) → Preorder (α i)
inst_3 : OrderTop (α ⊤)
x : Σₗ' (i : ι), α i
a : ι
b : α a
inl : ∀ (b : α ⊤), mk (β := fun (i : ι) ↦ α i) ⊤ b ≤ mk (β := fun (i : ι) ↦ α i) ⊤ ⊤
⊢ mk (β := fun (i : ι) ↦ α i) a b ≤ mk (β := fun (i : ι) ↦ α i) ⊤ ⊤
have inr : ∀ (ha : a < ⊤), mk (β := fun (i : ι) ↦ α i) a b ≤ mk (β := fun (i : ι) ↦ α i) ⊤ ⊤
Tactic: obtain rfl | ha := eq_top_or_lt_top a