awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Num.Bitwise (goal)
Goal:
b : Bool
false : (Bool.false::zero Bool.false) = zero Bool.false
⊢ (b::zero b) = zero b
have true : (true::zero true) = zero true
Tactic: cases b
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Data.Num.Bitwise (goal)
Goal:
b : Bool
⊢ (b::zero (decide ¬b = true)) = nz (msb b)
have false : (false::zero (decide ¬false = true)) = nz (msb false)
Tactic: cases b
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Data.Num.Bitwise (goal)
Goal:
b : Bool
false : (Bool.false::zero (decide ¬Bool.false = true)) = nz (msb Bool.false)
⊢ (b::zero (decide ¬b = true)) = nz (msb b)
have true : (true::zero (decide ¬true = true)) = nz (msb true)
Tactic: cases b
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Data.Num.Bitwise (goal)
Goal:
C : SNum → Sort u_1
z : (b : Bool) → C (zero b)
s : (b : Bool) → (p : SNum) → C p → C (b::p)
b : Bool
⊢ C (nz (msb b))
have rw : C (b::zero (decide ¬b = true))
Tactic: rw [← bit_one]
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
α : Type u_1
inst : AddMonoidWithOne α
p : PosNum
⊢ Eq.{u_1 + 1} (α := α) (↑(↑p.bit0 : ℕ) : α) (↑p.bit0 : α)
have dsimp : (↑(HAdd.hAdd (α := ℕ) (↑p : ℕ) (↑p : ℕ)) : α) = HAdd.hAdd (α := α) (↑p : α) (↑p : α)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
α : Type u_1
inst : AddMonoidWithOne α
p : PosNum
⊢ (↑(HAdd.hAdd (α := ℕ) (↑p : ℕ) (↑p : ℕ)) : α) = HAdd.hAdd (α := α) (↑p : α) (↑p : α)
have rw : HAdd.hAdd (α := α) (↑(↑p : ℕ) : α) (↑(↑p : ℕ) : α) = HAdd.hAdd (α := α) (↑p : α) (↑p : α)
Tactic: rw [Nat.cast_add, p.cast_to_nat]
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
α : Type u_1
inst : AddMonoidWithOne α
p : PosNum
rw : HAdd.hAdd (α := α) (↑(↑p : ℕ) : α) (↑(↑p : ℕ) : α) = HAdd.hAdd (α := α) (↑p : α) (↑p : α)
⊢ (↑(HAdd.hAdd (α := ℕ) (↑p : ℕ) (↑p : ℕ)) : α) = HAdd.hAdd (α := α) (↑p : α) (↑p : α)
have rw₁ : HAdd.hAdd (α := α) (↑p : α) (↑p : α) = HAdd.hAdd (α := α) (↑p : α) (↑p : α)
Tactic: rw [Nat.cast_add, p.cast_to_nat]
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
α : Type u_1
inst : AddMonoidWithOne α
p : PosNum
⊢ Eq.{u_1 + 1} (α := α) (↑(↑p.bit1 : ℕ) : α) (↑p.bit1 : α)
have dsimp : (↑(HAdd.hAdd (α := ℕ) (↑p : ℕ) (↑p : ℕ) + 1) : α) = HAdd.hAdd (α := α) (↑p : α) (↑p : α) + 1
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
α : Type u_1
inst : AddMonoidWithOne α
p : PosNum
⊢ (↑(HAdd.hAdd (α := ℕ) (↑p : ℕ) (↑p : ℕ) + 1) : α) = HAdd.hAdd (α := α) (↑p : α) (↑p : α) + 1
have rw : HAdd.hAdd (α := α) (↑(HAdd.hAdd (α := ℕ) (↑p : ℕ) (↑p : ℕ)) : α) (↑1 : α) = HAdd.hAdd (α := α) (↑p : α) (↑p : α) + 1
Tactic: rw [Nat.cast_add, Nat.cast_add, Nat.cast_one, p.cast_to_nat]
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
α : Type u_1
inst : AddMonoidWithOne α
p : PosNum
rw :
  HAdd.hAdd (α := α) (↑(HAdd.hAdd (α := ℕ) (↑p : ℕ) (↑p : ℕ)) : α) (↑1 : α) = HAdd.hAdd (α := α) (↑p : α) (↑p : α) + 1
⊢ (↑(HAdd.hAdd (α := ℕ) (↑p : ℕ) (↑p : ℕ) + 1) : α) = HAdd.hAdd (α := α) (↑p : α) (↑p : α) + 1
have rw₁ : HAdd.hAdd (α := α) (↑(↑p : ℕ) : α) (↑(↑p : ℕ) : α) + (↑1 : α) = HAdd.hAdd (α := α) (↑p : α) (↑p : α) + 1
Tactic: rw [Nat.cast_add, Nat.cast_add, Nat.cast_one, p.cast_to_nat]
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
α : Type u_1
inst : AddMonoidWithOne α
p : PosNum
rw :
  HAdd.hAdd (α := α) (↑(HAdd.hAdd (α := ℕ) (↑p : ℕ) (↑p : ℕ)) : α) (↑1 : α) = HAdd.hAdd (α := α) (↑p : α) (↑p : α) + 1
rw₁ : HAdd.hAdd (α := α) (↑(↑p : ℕ) : α) (↑(↑p : ℕ) : α) + (↑1 : α) = HAdd.hAdd (α := α) (↑p : α) (↑p : α) + 1
⊢ (↑(HAdd.hAdd (α := ℕ) (↑p : ℕ) (↑p : ℕ) + 1) : α) = HAdd.hAdd (α := α) (↑p : α) (↑p : α) + 1
have rw₂ : HAdd.hAdd (α := α) (↑(↑p : ℕ) : α) (↑(↑p : ℕ) : α) + 1 = HAdd.hAdd (α := α) (↑p : α) (↑p : α) + 1
Tactic: rw [Nat.cast_add, Nat.cast_add, Nat.cast_one, p.cast_to_nat]
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
α : Type u_1
inst : AddMonoidWithOne α
p : PosNum
rw :
  HAdd.hAdd (α := α) (↑(HAdd.hAdd (α := ℕ) (↑p : ℕ) (↑p : ℕ)) : α) (↑1 : α) = HAdd.hAdd (α := α) (↑p : α) (↑p : α) + 1
rw₁ : HAdd.hAdd (α := α) (↑(↑p : ℕ) : α) (↑(↑p : ℕ) : α) + (↑1 : α) = HAdd.hAdd (α := α) (↑p : α) (↑p : α) + 1
rw₂ : HAdd.hAdd (α := α) (↑(↑p : ℕ) : α) (↑(↑p : ℕ) : α) + 1 = HAdd.hAdd (α := α) (↑p : α) (↑p : α) + 1
⊢ (↑(HAdd.hAdd (α := ℕ) (↑p : ℕ) (↑p : ℕ) + 1) : α) = HAdd.hAdd (α := α) (↑p : α) (↑p : α) + 1
have rw₃ : HAdd.hAdd (α := α) (↑p : α) (↑p : α) + 1 = HAdd.hAdd (α := α) (↑p : α) (↑p : α) + 1
Tactic: rw [Nat.cast_add, Nat.cast_add, Nat.cast_one, p.cast_to_nat]
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
α : Type u_1
inst : AddGroupWithOne α
n : PosNum
⊢ Eq.{u_1 + 1} (α := α) (↑(↑n : ℤ) : α) (↑n : α)
have rw : Eq.{u_1 + 1} (α := α) (↑(↑(↑n : ℕ) : ℤ) : α) (↑n : α)
Tactic: rw [← to_nat_to_int, Int.cast_natCast, cast_to_nat]
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
α : Type u_1
inst : AddGroupWithOne α
n : PosNum
rw : Eq.{u_1 + 1} (α := α) (↑(↑(↑n : ℕ) : ℤ) : α) (↑n : α)
⊢ Eq.{u_1 + 1} (α := α) (↑(↑n : ℤ) : α) (↑n : α)
have rw₁ : Eq.{u_1 + 1} (α := α) (↑(↑n : ℕ) : α) (↑n : α)
Tactic: rw [← to_nat_to_int, Int.cast_natCast, cast_to_nat]
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
α : Type u_1
inst : AddGroupWithOne α
n : PosNum
rw : Eq.{u_1 + 1} (α := α) (↑(↑(↑n : ℕ) : ℤ) : α) (↑n : α)
rw₁ : Eq.{u_1 + 1} (α := α) (↑(↑n : ℕ) : α) (↑n : α)
⊢ Eq.{u_1 + 1} (α := α) (↑(↑n : ℤ) : α) (↑n : α)
have rw₂ : Eq.{u_1 + 1} (α := α) (↑n : α) (↑n : α)
Tactic: rw [← to_nat_to_int, Int.cast_natCast, cast_to_nat]
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
n : PosNum
⊢ 1 + n = n.succ
have one : 1 + one = one.succ
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
n : PosNum
one : 1 + PosNum.one = PosNum.one.succ
⊢ 1 + n = n.succ
have bit1 : ∀ (a : PosNum), 1 + a.bit1 = a.bit1.succ
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
n : PosNum
one : 1 + PosNum.one = PosNum.one.succ
bit1 : ∀ (a : PosNum), 1 + a.bit1 = a.bit1.succ
⊢ 1 + n = n.succ
have bit0 : ∀ (a : PosNum), 1 + a.bit0 = a.bit0.succ
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
n : PosNum
⊢ n + 1 = n.succ
have one : one + 1 = one.succ
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
n : PosNum
one : PosNum.one + 1 = PosNum.one.succ
⊢ n + 1 = n.succ
have bit1 : ∀ (a : PosNum), a.bit1 + 1 = a.bit1.succ
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
n : PosNum
one : PosNum.one + 1 = PosNum.one.succ
bit1 : ∀ (a : PosNum), a.bit1 + 1 = a.bit1.succ
⊢ n + 1 = n.succ
have bit0 : ∀ (a : PosNum), a.bit0 + 1 = a.bit0.succ
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
b : PosNum
⊢ (↑(1 + b) : ℕ) = HAdd.hAdd (α := ℕ) (↑1 : ℕ) (↑b : ℕ)
have rw : (↑b.succ : ℕ) = HAdd.hAdd (α := ℕ) (↑1 : ℕ) (↑b : ℕ)
Tactic: rw [one_add b, succ_to_nat, add_comm, cast_one]
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
b : PosNum
rw : (↑b.succ : ℕ) = HAdd.hAdd (α := ℕ) (↑1 : ℕ) (↑b : ℕ)
⊢ (↑(1 + b) : ℕ) = HAdd.hAdd (α := ℕ) (↑1 : ℕ) (↑b : ℕ)
have rw₁ : HAdd.hAdd (α := ℕ) (↑b : ℕ) 1 = HAdd.hAdd (α := ℕ) (↑1 : ℕ) (↑b : ℕ)
Tactic: rw [one_add b, succ_to_nat, add_comm, cast_one]
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
b : PosNum
rw : (↑b.succ : ℕ) = HAdd.hAdd (α := ℕ) (↑1 : ℕ) (↑b : ℕ)
rw₁ : HAdd.hAdd (α := ℕ) (↑b : ℕ) 1 = HAdd.hAdd (α := ℕ) (↑1 : ℕ) (↑b : ℕ)
⊢ (↑(1 + b) : ℕ) = HAdd.hAdd (α := ℕ) (↑1 : ℕ) (↑b : ℕ)
have rw₂ : HAdd.hAdd (α := ℕ) 1 (↑b : ℕ) = HAdd.hAdd (α := ℕ) (↑1 : ℕ) (↑b : ℕ)
Tactic: rw [one_add b, succ_to_nat, add_comm, cast_one]
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
b : PosNum
rw : (↑b.succ : ℕ) = HAdd.hAdd (α := ℕ) (↑1 : ℕ) (↑b : ℕ)
rw₁ : HAdd.hAdd (α := ℕ) (↑b : ℕ) 1 = HAdd.hAdd (α := ℕ) (↑1 : ℕ) (↑b : ℕ)
rw₂ : HAdd.hAdd (α := ℕ) 1 (↑b : ℕ) = HAdd.hAdd (α := ℕ) (↑1 : ℕ) (↑b : ℕ)
⊢ (↑(1 + b) : ℕ) = HAdd.hAdd (α := ℕ) (↑1 : ℕ) (↑b : ℕ)
have rw₃ : HAdd.hAdd (α := ℕ) 1 (↑b : ℕ) = HAdd.hAdd (α := ℕ) 1 (↑b : ℕ)
Tactic: rw [one_add b, succ_to_nat, add_comm, cast_one]
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
a : PosNum
⊢ (↑(a + 1) : ℕ) = HAdd.hAdd (α := ℕ) (↑a : ℕ) (↑1 : ℕ)
have rw : (↑a.succ : ℕ) = HAdd.hAdd (α := ℕ) (↑a : ℕ) (↑1 : ℕ)
Tactic: rw [add_one a, succ_to_nat, cast_one]
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
a : PosNum
rw : (↑a.succ : ℕ) = HAdd.hAdd (α := ℕ) (↑a : ℕ) (↑1 : ℕ)
⊢ (↑(a + 1) : ℕ) = HAdd.hAdd (α := ℕ) (↑a : ℕ) (↑1 : ℕ)
have rw₁ : HAdd.hAdd (α := ℕ) (↑a : ℕ) 1 = HAdd.hAdd (α := ℕ) (↑a : ℕ) (↑1 : ℕ)
Tactic: rw [add_one a, succ_to_nat, cast_one]
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
a : PosNum
rw : (↑a.succ : ℕ) = HAdd.hAdd (α := ℕ) (↑a : ℕ) (↑1 : ℕ)
rw₁ : HAdd.hAdd (α := ℕ) (↑a : ℕ) 1 = HAdd.hAdd (α := ℕ) (↑a : ℕ) (↑1 : ℕ)
⊢ (↑(a + 1) : ℕ) = HAdd.hAdd (α := ℕ) (↑a : ℕ) (↑1 : ℕ)
have rw₂ : HAdd.hAdd (α := ℕ) (↑a : ℕ) 1 = HAdd.hAdd (α := ℕ) (↑a : ℕ) 1
Tactic: rw [add_one a, succ_to_nat, cast_one]
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
a b : PosNum
⊢ HAdd.hAdd (α := ℕ) (↑(a + b).succ : ℕ) (↑(a + b).succ : ℕ) =
    HAdd.hAdd (α := ℕ) (↑a : ℕ) (↑a : ℕ) + 1 + (HAdd.hAdd (α := ℕ) (↑b : ℕ) (↑b : ℕ) + 1)
have rw : HAdd.hAdd (α := ℕ) (↑a : ℕ) (↑b : ℕ) + 1 + (HAdd.hAdd (α := ℕ) (↑a : ℕ) (↑b : ℕ) + 1) =
  HAdd.hAdd (α := ℕ) (↑a : ℕ) (↑a : ℕ) + 1 + (HAdd.hAdd (α := ℕ) (↑b : ℕ) (↑b : ℕ) + 1)
Tactic: rw [succ_to_nat, add_to_nat a b]
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
p : PosNum
⊢ (p + p).succ.bit0 = p.bit1.bit0
have rw : p.bit0.succ.bit0 = p.bit1.bit0
Tactic: rw [bit0_of_bit0 p, succ]
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
p : PosNum
rw : p.bit0.succ.bit0 = p.bit1.bit0
⊢ (p + p).succ.bit0 = p.bit1.bit0
have rw₁ : p.bit1.bit0 = p.bit1.bit0
Tactic: rw [bit0_of_bit0 p, succ]
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
n : PosNum
⊢ n + n + 1 = n.bit1
have rw : (n + n).succ = n.bit1
Tactic: rw [add_one, bit0_of_bit0, succ]
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
n : PosNum
rw : (n + n).succ = n.bit1
⊢ n + n + 1 = n.bit1
have rw₁ : n.bit0.succ = n.bit1
Tactic: rw [add_one, bit0_of_bit0, succ]
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
n : PosNum
rw : (n + n).succ = n.bit1
rw₁ : n.bit0.succ = n.bit1
⊢ n + n + 1 = n.bit1
have rw₂ : n.bit1 = n.bit1
Tactic: rw [add_one, bit0_of_bit0, succ]
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
m p : PosNum
⊢ HAdd.hAdd (α := ℕ) (↑(m * p) : ℕ) (↑(m * p) : ℕ) = (↑m : ℕ) * HAdd.hAdd (α := ℕ) (↑p : ℕ) (↑p : ℕ)
have rw : HMul.hMul (α := ℕ) (↑m : ℕ) (↑p : ℕ) + HMul.hMul (α := ℕ) (↑m : ℕ) (↑p : ℕ) =
  (↑m : ℕ) * HAdd.hAdd (α := ℕ) (↑p : ℕ) (↑p : ℕ)
Tactic: rw [mul_to_nat m p, left_distrib]
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
m p : PosNum
rw :
  HMul.hMul (α := ℕ) (↑m : ℕ) (↑p : ℕ) + HMul.hMul (α := ℕ) (↑m : ℕ) (↑p : ℕ) =
    (↑m : ℕ) * HAdd.hAdd (α := ℕ) (↑p : ℕ) (↑p : ℕ)
⊢ HAdd.hAdd (α := ℕ) (↑(m * p) : ℕ) (↑(m * p) : ℕ) = (↑m : ℕ) * HAdd.hAdd (α := ℕ) (↑p : ℕ) (↑p : ℕ)
have rw₁ : HMul.hMul (α := ℕ) (↑m : ℕ) (↑p : ℕ) + HMul.hMul (α := ℕ) (↑m : ℕ) (↑p : ℕ) =
  HMul.hMul (α := ℕ) (↑m : ℕ) (↑p : ℕ) + HMul.hMul (α := ℕ) (↑m : ℕ) (↑p : ℕ)
Tactic: rw [mul_to_nat m p, left_distrib]
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
m p : PosNum
⊢ HAdd.hAdd (α := ℕ) (↑(m * p) : ℕ) (↑(m * p) : ℕ) + (↑m : ℕ) =
    (↑m : ℕ) * HAdd.hAdd (α := ℕ) (↑p : ℕ) (↑p : ℕ) + (↑m : ℕ)
have rw : HMul.hMul (α := ℕ) (↑m : ℕ) (↑p : ℕ) + HMul.hMul (α := ℕ) (↑m : ℕ) (↑p : ℕ) + (↑m : ℕ) =
  (↑m : ℕ) * HAdd.hAdd (α := ℕ) (↑p : ℕ) (↑p : ℕ) + (↑m : ℕ)
Tactic: rw [mul_to_nat m p, left_distrib]
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
m p : PosNum
rw :
  HMul.hMul (α := ℕ) (↑m : ℕ) (↑p : ℕ) + HMul.hMul (α := ℕ) (↑m : ℕ) (↑p : ℕ) + (↑m : ℕ) =
    (↑m : ℕ) * HAdd.hAdd (α := ℕ) (↑p : ℕ) (↑p : ℕ) + (↑m : ℕ)
⊢ HAdd.hAdd (α := ℕ) (↑(m * p) : ℕ) (↑(m * p) : ℕ) + (↑m : ℕ) =
    (↑m : ℕ) * HAdd.hAdd (α := ℕ) (↑p : ℕ) (↑p : ℕ) + (↑m : ℕ)
have rw₁ : HMul.hMul (α := ℕ) (↑m : ℕ) (↑p : ℕ) + HMul.hMul (α := ℕ) (↑m : ℕ) (↑p : ℕ) + (↑m : ℕ) =
  HMul.hMul (α := ℕ) (↑m : ℕ) (↑p : ℕ) + HMul.hMul (α := ℕ) (↑m : ℕ) (↑p : ℕ) + (↑m : ℕ)
Tactic: rw [mul_to_nat m p, left_distrib]
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
m n : PosNum
h : LT.lt (α := ℕ) (↑m : ℕ) (↑n : ℕ)
⊢ HAdd.hAdd (α := ℕ) (↑m : ℕ) (↑m : ℕ) + 1 + 1 ≤ HAdd.hAdd (α := ℕ) (↑n : ℕ) (↑n : ℕ)
have rw : HAdd.hAdd (α := ℕ) (↑m : ℕ) 1 + HAdd.hAdd (α := ℕ) (↑m : ℕ) 1 ≤ HAdd.hAdd (α := ℕ) (↑n : ℕ) (↑n : ℕ)
Tactic: rw [Nat.add_right_comm m m 1, add_assoc]
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
m : PosNum
⊢ ∀ (n : PosNum), (m.cmp n).swap = n.cmp m
have one : ∀ (n : PosNum), (one.cmp n).swap = n.cmp one
Tactic: induction m with | one => ?_ | bit1 m IH => ?_ | bit0 m IH => ?_
Cleared hypotheses: m
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
m : PosNum
one : ∀ (n : PosNum), (PosNum.one.cmp n).swap = n.cmp PosNum.one
⊢ ∀ (n : PosNum), (m.cmp n).swap = n.cmp m
have bit1 : ∀ (m : PosNum) (IH : ∀ (n : PosNum), (m.cmp n).swap = n.cmp m) (n : PosNum), (m.bit1.cmp n).swap = n.cmp m.bit1
Tactic: induction m with | one => ?_ | bit1 m IH => ?_ | bit0 m IH => ?_
Cleared hypotheses: m
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
m : PosNum
one : ∀ (n : PosNum), (PosNum.one.cmp n).swap = n.cmp PosNum.one
bit1 : ∀ (m : PosNum) (IH : ∀ (n : PosNum), (m.cmp n).swap = n.cmp m) (n : PosNum), (m.bit1.cmp n).swap = n.cmp m.bit1
⊢ ∀ (n : PosNum), (m.cmp n).swap = n.cmp m
have bit0 : ∀ (m : PosNum) (IH : ∀ (n : PosNum), (m.cmp n).swap = n.cmp m) (n : PosNum), (m.bit0.cmp n).swap = n.cmp m.bit0
Tactic: induction m with | one => ?_ | bit1 m IH => ?_ | bit0 m IH => ?_
Cleared hypotheses: m
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
n : PosNum
⊢ (one.cmp n).swap = n.cmp one
have one : (one.cmp one).swap = one.cmp one
Tactic: obtain - | n | n := n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
n : PosNum
one : (PosNum.one.cmp PosNum.one).swap = PosNum.one.cmp PosNum.one
⊢ (PosNum.one.cmp n).swap = n.cmp PosNum.one
have one₁ : ∀ (n : PosNum), (PosNum.one.cmp n.bit1).swap = n.bit1.cmp PosNum.one
Tactic: obtain - | n | n := n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
n : PosNum
one : (PosNum.one.cmp PosNum.one).swap = PosNum.one.cmp PosNum.one
one₁ : ∀ (n : PosNum), (PosNum.one.cmp n.bit1).swap = n.bit1.cmp PosNum.one
⊢ (PosNum.one.cmp n).swap = n.cmp PosNum.one
have one₂ : ∀ (n : PosNum), (PosNum.one.cmp n.bit0).swap = n.bit0.cmp PosNum.one
Tactic: obtain - | n | n := n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
m : PosNum
IH : ∀ (n : PosNum), (m.cmp n).swap = n.cmp m
n : PosNum
⊢ (m.bit1.cmp n).swap = n.cmp m.bit1
have bit1 : (m.bit1.cmp one).swap = one.cmp m.bit1
Tactic: obtain - | n | n := n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
m : PosNum
IH : ∀ (n : PosNum), (m.cmp n).swap = n.cmp m
n : PosNum
bit1 : (m.bit1.cmp one).swap = one.cmp m.bit1
⊢ (m.bit1.cmp n).swap = n.cmp m.bit1
have bit1₁ : ∀ (n : PosNum), (m.bit1.cmp n.bit1).swap = n.bit1.cmp m.bit1
Tactic: obtain - | n | n := n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
m : PosNum
IH : ∀ (n : PosNum), (m.cmp n).swap = n.cmp m
n : PosNum
bit1 : (m.bit1.cmp one).swap = one.cmp m.bit1
bit1₁ : ∀ (n : PosNum), (m.bit1.cmp n.bit1).swap = n.bit1.cmp m.bit1
⊢ (m.bit1.cmp n).swap = n.cmp m.bit1
have bit1₂ : ∀ (n : PosNum), (m.bit1.cmp n.bit0).swap = n.bit0.cmp m.bit1
Tactic: obtain - | n | n := n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
m : PosNum
IH : ∀ (n : PosNum), (m.cmp n).swap = n.cmp m
n : PosNum
⊢ (m.bit0.cmp n).swap = n.cmp m.bit0
have bit0 : (m.bit0.cmp one).swap = one.cmp m.bit0
Tactic: obtain - | n | n := n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
m : PosNum
IH : ∀ (n : PosNum), (m.cmp n).swap = n.cmp m
n : PosNum
bit0 : (m.bit0.cmp one).swap = one.cmp m.bit0
⊢ (m.bit0.cmp n).swap = n.cmp m.bit0
have bit0₁ : ∀ (n : PosNum), (m.bit0.cmp n.bit1).swap = n.bit1.cmp m.bit0
Tactic: obtain - | n | n := n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
m : PosNum
IH : ∀ (n : PosNum), (m.cmp n).swap = n.cmp m
n : PosNum
bit0 : (m.bit0.cmp one).swap = one.cmp m.bit0
bit0₁ : ∀ (n : PosNum), (m.bit0.cmp n.bit1).swap = n.bit1.cmp m.bit0
⊢ (m.bit0.cmp n).swap = n.cmp m.bit0
have bit0₂ : ∀ (n : PosNum), (m.bit0.cmp n.bit0).swap = n.bit0.cmp m.bit0
Tactic: obtain - | n | n := n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
m : PosNum
IH : ∀ (n : PosNum), (m.cmp n).swap = n.cmp m
n : PosNum
⊢ (m.bit1.cmp n.bit1).swap = n.bit1.cmp m.bit1
have bit1 : (m.cmp n).swap = n.cmp m
Tactic: unfold cmp
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
m : PosNum
IH : ∀ (n : PosNum), (m.cmp n).swap = n.cmp m
n : PosNum
⊢ (m.bit1.cmp n.bit0).swap = n.bit0.cmp m.bit1
have bit1 : Ordering.swap
    (Ordering.casesOn (motive := fun (x : Ordering) ↦ Ordering) (m.cmp n) Ordering.lt Ordering.gt Ordering.gt) =
  Ordering.casesOn (motive := fun (x : Ordering) ↦ Ordering) (n.cmp m) Ordering.lt Ordering.lt Ordering.gt
Tactic: unfold cmp
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
m : PosNum
IH : ∀ (n : PosNum), (m.cmp n).swap = n.cmp m
n : PosNum
⊢ (m.bit0.cmp n.bit1).swap = n.bit1.cmp m.bit0
have bit0 : Ordering.swap
    (Ordering.casesOn (motive := fun (x : Ordering) ↦ Ordering) (m.cmp n) Ordering.lt Ordering.lt Ordering.gt) =
  Ordering.casesOn (motive := fun (x : Ordering) ↦ Ordering) (n.cmp m) Ordering.lt Ordering.gt Ordering.gt
Tactic: unfold cmp
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
m : PosNum
IH : ∀ (n : PosNum), (m.cmp n).swap = n.cmp m
n : PosNum
⊢ (m.bit0.cmp n.bit0).swap = n.bit0.cmp m.bit0
have bit0 : (m.cmp n).swap = n.cmp m
Tactic: unfold cmp
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
m : PosNum
IH : ∀ (n : PosNum), (m.cmp n).swap = n.cmp m
n : PosNum
⊢ (m.cmp n).swap = n.cmp m
have bit1 : (m.cmp n).swap = (m.cmp n).swap
Tactic: rw [← IH]
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
m : PosNum
IH : ∀ (n : PosNum), (m.cmp n).swap = n.cmp m
n : PosNum
⊢ Ordering.swap
      (Ordering.casesOn (motive := fun (x : Ordering) ↦ Ordering) (m.cmp n) Ordering.lt Ordering.gt Ordering.gt) =
    Ordering.casesOn (motive := fun (x : Ordering) ↦ Ordering) (n.cmp m) Ordering.lt Ordering.lt Ordering.gt
have bit1 : Ordering.swap
    (Ordering.casesOn (motive := fun (x : Ordering) ↦ Ordering) (m.cmp n) Ordering.lt Ordering.gt Ordering.gt) =
  Ordering.casesOn (motive := fun (x : Ordering) ↦ Ordering) (m.cmp n).swap Ordering.lt Ordering.lt Ordering.gt
Tactic: rw [← IH]
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
m : PosNum
IH : ∀ (n : PosNum), (m.cmp n).swap = n.cmp m
n : PosNum
⊢ Ordering.swap
      (Ordering.casesOn (motive := fun (x : Ordering) ↦ Ordering) (m.cmp n) Ordering.lt Ordering.lt Ordering.gt) =
    Ordering.casesOn (motive := fun (x : Ordering) ↦ Ordering) (n.cmp m) Ordering.lt Ordering.gt Ordering.gt
have bit0 : Ordering.swap
    (Ordering.casesOn (motive := fun (x : Ordering) ↦ Ordering) (m.cmp n) Ordering.lt Ordering.lt Ordering.gt) =
  Ordering.casesOn (motive := fun (x : Ordering) ↦ Ordering) (m.cmp n).swap Ordering.lt Ordering.gt Ordering.gt
Tactic: rw [← IH]
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
m : PosNum
IH : ∀ (n : PosNum), (m.cmp n).swap = n.cmp m
n : PosNum
⊢ (m.cmp n).swap = n.cmp m
have bit0 : (m.cmp n).swap = (m.cmp n).swap
Tactic: rw [← IH]
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
m : PosNum
IH : ∀ (n : PosNum), (m.cmp n).swap = n.cmp m
n : PosNum
⊢ Ordering.swap
      (Ordering.casesOn (motive := fun (x : Ordering) ↦ Ordering) (m.cmp n) Ordering.lt Ordering.gt Ordering.gt) =
    Ordering.casesOn (motive := fun (x : Ordering) ↦ Ordering) (m.cmp n).swap Ordering.lt Ordering.lt Ordering.gt
have bit1 : Ordering.swap
    (Ordering.casesOn (motive := fun (x : Ordering) ↦ Ordering) Ordering.lt Ordering.lt Ordering.gt Ordering.gt) =
  Ordering.casesOn (motive := fun (x : Ordering) ↦ Ordering) Ordering.lt.swap Ordering.lt Ordering.lt Ordering.gt
Tactic: cases cmp m n
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
m : PosNum
IH : ∀ (n : PosNum), (m.cmp n).swap = n.cmp m
n : PosNum
bit1 :
  Ordering.swap
      (Ordering.casesOn (motive := fun (x : Ordering) ↦ Ordering) Ordering.lt Ordering.lt Ordering.gt Ordering.gt) =
    Ordering.casesOn (motive := fun (x : Ordering) ↦ Ordering) Ordering.lt.swap Ordering.lt Ordering.lt Ordering.gt
⊢ Ordering.swap
      (Ordering.casesOn (motive := fun (x : Ordering) ↦ Ordering) (m.cmp n) Ordering.lt Ordering.gt Ordering.gt) =
    Ordering.casesOn (motive := fun (x : Ordering) ↦ Ordering) (m.cmp n).swap Ordering.lt Ordering.lt Ordering.gt
have bit1₁ : Ordering.swap
    (Ordering.casesOn (motive := fun (x : Ordering) ↦ Ordering) Ordering.eq Ordering.lt Ordering.gt Ordering.gt) =
  Ordering.casesOn (motive := fun (x : Ordering) ↦ Ordering) Ordering.eq.swap Ordering.lt Ordering.lt Ordering.gt
Tactic: cases cmp m n
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
m : PosNum
IH : ∀ (n : PosNum), (m.cmp n).swap = n.cmp m
n : PosNum
bit1 :
  Ordering.swap
      (Ordering.casesOn (motive := fun (x : Ordering) ↦ Ordering) Ordering.lt Ordering.lt Ordering.gt Ordering.gt) =
    Ordering.casesOn (motive := fun (x : Ordering) ↦ Ordering) Ordering.lt.swap Ordering.lt Ordering.lt Ordering.gt
bit1₁ :
  Ordering.swap
      (Ordering.casesOn (motive := fun (x : Ordering) ↦ Ordering) Ordering.eq Ordering.lt Ordering.gt Ordering.gt) =
    Ordering.casesOn (motive := fun (x : Ordering) ↦ Ordering) Ordering.eq.swap Ordering.lt Ordering.lt Ordering.gt
⊢ Ordering.swap
      (Ordering.casesOn (motive := fun (x : Ordering) ↦ Ordering) (m.cmp n) Ordering.lt Ordering.gt Ordering.gt) =
    Ordering.casesOn (motive := fun (x : Ordering) ↦ Ordering) (m.cmp n).swap Ordering.lt Ordering.lt Ordering.gt
have bit1₂ : Ordering.swap
    (Ordering.casesOn (motive := fun (x : Ordering) ↦ Ordering) Ordering.gt Ordering.lt Ordering.gt Ordering.gt) =
  Ordering.casesOn (motive := fun (x : Ordering) ↦ Ordering) Ordering.gt.swap Ordering.lt Ordering.lt Ordering.gt
Tactic: cases cmp m n
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
m : PosNum
IH : ∀ (n : PosNum), (m.cmp n).swap = n.cmp m
n : PosNum
⊢ Ordering.swap
      (Ordering.casesOn (motive := fun (x : Ordering) ↦ Ordering) (m.cmp n) Ordering.lt Ordering.lt Ordering.gt) =
    Ordering.casesOn (motive := fun (x : Ordering) ↦ Ordering) (m.cmp n).swap Ordering.lt Ordering.gt Ordering.gt
have bit0 : Ordering.swap
    (Ordering.casesOn (motive := fun (x : Ordering) ↦ Ordering) Ordering.lt Ordering.lt Ordering.lt Ordering.gt) =
  Ordering.casesOn (motive := fun (x : Ordering) ↦ Ordering) Ordering.lt.swap Ordering.lt Ordering.gt Ordering.gt
Tactic: cases cmp m n
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
m : PosNum
IH : ∀ (n : PosNum), (m.cmp n).swap = n.cmp m
n : PosNum
bit0 :
  Ordering.swap
      (Ordering.casesOn (motive := fun (x : Ordering) ↦ Ordering) Ordering.lt Ordering.lt Ordering.lt Ordering.gt) =
    Ordering.casesOn (motive := fun (x : Ordering) ↦ Ordering) Ordering.lt.swap Ordering.lt Ordering.gt Ordering.gt
⊢ Ordering.swap
      (Ordering.casesOn (motive := fun (x : Ordering) ↦ Ordering) (m.cmp n) Ordering.lt Ordering.lt Ordering.gt) =
    Ordering.casesOn (motive := fun (x : Ordering) ↦ Ordering) (m.cmp n).swap Ordering.lt Ordering.gt Ordering.gt
have bit0₁ : Ordering.swap
    (Ordering.casesOn (motive := fun (x : Ordering) ↦ Ordering) Ordering.eq Ordering.lt Ordering.lt Ordering.gt) =
  Ordering.casesOn (motive := fun (x : Ordering) ↦ Ordering) Ordering.eq.swap Ordering.lt Ordering.gt Ordering.gt
Tactic: cases cmp m n