awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
gff : (false != false) = false
f00 : HXor.hXor (α := Num) 0 0 = 0
f0n : ∀ (n : PosNum), 0 ^^^ pos n = bif false != true then pos n else 0
fn0 : ∀ (n : PosNum), pos n ^^^ 0 = bif true != false then pos n else 0
fnn : ∀ (m n : PosNum), pos m ^^^ pos n = m.lxor n
⊢ ∀ (m n : Num), (↑(m ^^^ n) : ℕ) = HXor.hXor (α := ℕ) (↑m : ℕ) (↑n : ℕ)
have p11 : PosNum.lxor 1 1 = bif true != true then 1 else 0
Tactic: apply castNum_eq_bitwise PosNum.lxor
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
gff : (false != false) = false
f00 : HXor.hXor (α := Num) 0 0 = 0
f0n : ∀ (n : PosNum), 0 ^^^ pos n = bif false != true then pos n else 0
fn0 : ∀ (n : PosNum), pos n ^^^ 0 = bif true != false then pos n else 0
fnn : ∀ (m n : PosNum), pos m ^^^ pos n = m.lxor n
p11 : PosNum.lxor 1 1 = bif true != true then 1 else 0
⊢ ∀ (m n : Num), (↑(m ^^^ n) : ℕ) = HXor.hXor (α := ℕ) (↑m : ℕ) (↑n : ℕ)
have p1b : ∀ (b : Bool) (n : PosNum), PosNum.lxor 1 (PosNum.bit b n) = bit (true != b) (bif false != true then pos n else 0)
Tactic: apply castNum_eq_bitwise PosNum.lxor
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
gff : (false != false) = false
f00 : HXor.hXor (α := Num) 0 0 = 0
f0n : ∀ (n : PosNum), 0 ^^^ pos n = bif false != true then pos n else 0
fn0 : ∀ (n : PosNum), pos n ^^^ 0 = bif true != false then pos n else 0
fnn : ∀ (m n : PosNum), pos m ^^^ pos n = m.lxor n
p11 : PosNum.lxor 1 1 = bif true != true then 1 else 0
p1b : ∀ (b : Bool) (n : PosNum), PosNum.lxor 1 (PosNum.bit b n) = bit (true != b) (bif false != true then pos n else 0)
⊢ ∀ (m n : Num), (↑(m ^^^ n) : ℕ) = HXor.hXor (α := ℕ) (↑m : ℕ) (↑n : ℕ)
have pb1 : ∀ (a : Bool) (m : PosNum), (PosNum.bit a m).lxor 1 = bit (a != true) (bif true != false then pos m else 0)
Tactic: apply castNum_eq_bitwise PosNum.lxor
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
gff : (false != false) = false
f00 : HXor.hXor (α := Num) 0 0 = 0
f0n : ∀ (n : PosNum), 0 ^^^ pos n = bif false != true then pos n else 0
fn0 : ∀ (n : PosNum), pos n ^^^ 0 = bif true != false then pos n else 0
fnn : ∀ (m n : PosNum), pos m ^^^ pos n = m.lxor n
p11 : PosNum.lxor 1 1 = bif true != true then 1 else 0
p1b : ∀ (b : Bool) (n : PosNum), PosNum.lxor 1 (PosNum.bit b n) = bit (true != b) (bif false != true then pos n else 0)
pb1 : ∀ (a : Bool) (m : PosNum), (PosNum.bit a m).lxor 1 = bit (a != true) (bif true != false then pos m else 0)
⊢ ∀ (m n : Num), (↑(m ^^^ n) : ℕ) = HXor.hXor (α := ℕ) (↑m : ℕ) (↑n : ℕ)
have pbb : ∀ (a b : Bool) (m n : PosNum), (PosNum.bit a m).lxor (PosNum.bit b n) = bit (a != b) (m.lxor n)
Tactic: apply castNum_eq_bitwise PosNum.lxor
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
b : Bool
n : PosNum
⊢ PosNum.lxor 1 (PosNum.bit b n) = bit (true != b) (bif false != true then pos n else 0)
have p1b : PosNum.lxor 1 (PosNum.bit false n) = bit (true != false) (bif false != true then pos n else 0)
Tactic: cases_type* Bool
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
b : Bool
n : PosNum
p1b : PosNum.lxor 1 (PosNum.bit false n) = bit (true != false) (bif false != true then pos n else 0)
⊢ PosNum.lxor 1 (PosNum.bit b n) = bit (true != b) (bif false != true then pos n else 0)
have p1b₁ : PosNum.lxor 1 (PosNum.bit true n) = bit (true != true) (bif false != true then pos n else 0)
Tactic: cases_type* Bool
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
b : Bool
n : PosNum
⊢ PosNum.lxor 1 (PosNum.bit b n) = bit (true != b) (bif false != true then pos n else 0)
have p1b : PosNum.lxor 1 (PosNum.bit false n) = bit (true != false) (bif false != true then pos n else 0)
Tactic: try cases_type* Bool
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
b : Bool
n : PosNum
p1b : PosNum.lxor 1 (PosNum.bit false n) = bit (true != false) (bif false != true then pos n else 0)
⊢ PosNum.lxor 1 (PosNum.bit b n) = bit (true != b) (bif false != true then pos n else 0)
have p1b₁ : PosNum.lxor 1 (PosNum.bit true n) = bit (true != true) (bif false != true then pos n else 0)
Tactic: try cases_type* Bool
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
a : Bool
m : PosNum
⊢ (PosNum.bit a m).lxor 1 = bit (a != true) (bif true != false then pos m else 0)
have pb1 : (PosNum.bit false m).lxor 1 = bit (false != true) (bif true != false then pos m else 0)
Tactic: cases_type* Bool
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
a : Bool
m : PosNum
pb1 : (PosNum.bit false m).lxor 1 = bit (false != true) (bif true != false then pos m else 0)
⊢ (PosNum.bit a m).lxor 1 = bit (a != true) (bif true != false then pos m else 0)
have pb1₁ : (PosNum.bit true m).lxor 1 = bit (true != true) (bif true != false then pos m else 0)
Tactic: cases_type* Bool
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
a : Bool
m : PosNum
⊢ (PosNum.bit a m).lxor 1 = bit (a != true) (bif true != false then pos m else 0)
have pb1 : (PosNum.bit false m).lxor 1 = bit (false != true) (bif true != false then pos m else 0)
Tactic: try cases_type* Bool
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
a : Bool
m : PosNum
pb1 : (PosNum.bit false m).lxor 1 = bit (false != true) (bif true != false then pos m else 0)
⊢ (PosNum.bit a m).lxor 1 = bit (a != true) (bif true != false then pos m else 0)
have pb1₁ : (PosNum.bit true m).lxor 1 = bit (true != true) (bif true != false then pos m else 0)
Tactic: try cases_type* Bool
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
a b : Bool
m n : PosNum
⊢ (PosNum.bit a m).lxor (PosNum.bit b n) = bit (a != b) (m.lxor n)
have pbb : (PosNum.bit false m).lxor (PosNum.bit false n) = bit (false != false) (m.lxor n)
Tactic: cases_type* Bool
Cleared hypotheses: a, b
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
a b : Bool
m n : PosNum
pbb : (PosNum.bit false m).lxor (PosNum.bit false n) = bit (false != false) (m.lxor n)
⊢ (PosNum.bit a m).lxor (PosNum.bit b n) = bit (a != b) (m.lxor n)
have pbb₁ : (PosNum.bit false m).lxor (PosNum.bit true n) = bit (false != true) (m.lxor n)
Tactic: cases_type* Bool
Cleared hypotheses: a, b
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
a b : Bool
m n : PosNum
pbb : (PosNum.bit false m).lxor (PosNum.bit false n) = bit (false != false) (m.lxor n)
pbb₁ : (PosNum.bit false m).lxor (PosNum.bit true n) = bit (false != true) (m.lxor n)
⊢ (PosNum.bit a m).lxor (PosNum.bit b n) = bit (a != b) (m.lxor n)
have pbb₂ : (PosNum.bit true m).lxor (PosNum.bit false n) = bit (true != false) (m.lxor n)
Tactic: cases_type* Bool
Cleared hypotheses: a, b
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
a b : Bool
m n : PosNum
pbb : (PosNum.bit false m).lxor (PosNum.bit false n) = bit (false != false) (m.lxor n)
pbb₁ : (PosNum.bit false m).lxor (PosNum.bit true n) = bit (false != true) (m.lxor n)
pbb₂ : (PosNum.bit true m).lxor (PosNum.bit false n) = bit (true != false) (m.lxor n)
⊢ (PosNum.bit a m).lxor (PosNum.bit b n) = bit (a != b) (m.lxor n)
have pbb₃ : (PosNum.bit true m).lxor (PosNum.bit true n) = bit (true != true) (m.lxor n)
Tactic: cases_type* Bool
Cleared hypotheses: a, b
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
a b : Bool
m n : PosNum
⊢ (PosNum.bit a m).lxor (PosNum.bit b n) = bit (a != b) (m.lxor n)
have pbb : (PosNum.bit false m).lxor (PosNum.bit false n) = bit (false != false) (m.lxor n)
Tactic: try cases_type* Bool
Cleared hypotheses: a, b
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
a b : Bool
m n : PosNum
pbb : (PosNum.bit false m).lxor (PosNum.bit false n) = bit (false != false) (m.lxor n)
⊢ (PosNum.bit a m).lxor (PosNum.bit b n) = bit (a != b) (m.lxor n)
have pbb₁ : (PosNum.bit false m).lxor (PosNum.bit true n) = bit (false != true) (m.lxor n)
Tactic: try cases_type* Bool
Cleared hypotheses: a, b
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
a b : Bool
m n : PosNum
pbb : (PosNum.bit false m).lxor (PosNum.bit false n) = bit (false != false) (m.lxor n)
pbb₁ : (PosNum.bit false m).lxor (PosNum.bit true n) = bit (false != true) (m.lxor n)
⊢ (PosNum.bit a m).lxor (PosNum.bit b n) = bit (a != b) (m.lxor n)
have pbb₂ : (PosNum.bit true m).lxor (PosNum.bit false n) = bit (true != false) (m.lxor n)
Tactic: try cases_type* Bool
Cleared hypotheses: a, b
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
a b : Bool
m n : PosNum
pbb : (PosNum.bit false m).lxor (PosNum.bit false n) = bit (false != false) (m.lxor n)
pbb₁ : (PosNum.bit false m).lxor (PosNum.bit true n) = bit (false != true) (m.lxor n)
pbb₂ : (PosNum.bit true m).lxor (PosNum.bit false n) = bit (true != false) (m.lxor n)
⊢ (PosNum.bit a m).lxor (PosNum.bit b n) = bit (a != b) (m.lxor n)
have pbb₃ : (PosNum.bit true m).lxor (PosNum.bit true n) = bit (true != true) (m.lxor n)
Tactic: try cases_type* Bool
Cleared hypotheses: a, b
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
m : Num
n : ℕ
⊢ (↑(m <<< n) : ℕ) = (↑m : ℕ) <<< n
have zero : (↑(zero <<< n) : ℕ) = (↑zero : ℕ) <<< n
Tactic: cases m
Cleared hypotheses: m
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
m : Num
n : ℕ
zero : (↑(Num.zero <<< n) : ℕ) = (↑Num.zero : ℕ) <<< n
⊢ (↑(m <<< n) : ℕ) = (↑m : ℕ) <<< n
have pos : ∀ (a : PosNum), (↑(pos a <<< n) : ℕ) = (↑(pos a) : ℕ) <<< n
Tactic: cases m
Cleared hypotheses: m
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
n : ℕ
⊢ (↑0 : ℕ) = (↑zero : ℕ) <<< n
have zero : (↑zero : ℕ) <<< n = (↑0 : ℕ)
Tactic: symm
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
n : ℕ
a : PosNum
⊢ (↑(a <<< n) : ℕ) = (↑a : ℕ) <<< n
have pos : (↑(a <<< 0) : ℕ) = HShiftLeft.hShiftLeft (α := ℕ) (↑a : ℕ) 0
Tactic: induction n with
  | zero => rfl
  | succ n IH =>
    simp [PosNum.shiftl_succ_eq_bit0_shiftl, Nat.shiftLeft_succ, IH, mul_comm,
      -shiftl_eq_shiftLeft, -PosNum.shiftl_eq_shiftLeft, mul_two]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
n : ℕ
a : PosNum
pos : (↑(a <<< 0) : ℕ) = HShiftLeft.hShiftLeft (α := ℕ) (↑a : ℕ) 0
⊢ (↑(a <<< n) : ℕ) = (↑a : ℕ) <<< n
have pos₁ : ∀ (n : ℕ) (IH : (↑(a <<< n) : ℕ) = (↑a : ℕ) <<< n), (↑(a <<< (n + 1)) : ℕ) = (↑a : ℕ) <<< (n + 1)
Tactic: induction n with
  | zero => rfl
  | succ n IH =>
    simp [PosNum.shiftl_succ_eq_bit0_shiftl, Nat.shiftLeft_succ, IH, mul_comm,
      -shiftl_eq_shiftLeft, -PosNum.shiftl_eq_shiftLeft, mul_two]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
m : Num
n : ℕ
⊢ (↑(m >>> n) : ℕ) = HShiftRight.hShiftRight (α := ℕ) (↑m : ℕ) n
have zero : (↑(zero >>> n) : ℕ) = HShiftRight.hShiftRight (α := ℕ) (↑zero : ℕ) n
Tactic: obtain - | m := m
Cleared hypotheses: m
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
m : Num
n : ℕ
zero : (↑(Num.zero >>> n) : ℕ) = HShiftRight.hShiftRight (α := ℕ) (↑Num.zero : ℕ) n
⊢ (↑(m >>> n) : ℕ) = HShiftRight.hShiftRight (α := ℕ) (↑m : ℕ) n
have pos : ∀ (m : PosNum), (↑(pos m >>> n) : ℕ) = HShiftRight.hShiftRight (α := ℕ) (↑(pos m) : ℕ) n
Tactic: obtain - | m := m
Cleared hypotheses: m
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
n : ℕ
⊢ (↑0 : ℕ) = HShiftRight.hShiftRight (α := ℕ) (↑zero : ℕ) n
have zero : HShiftRight.hShiftRight (α := ℕ) (↑zero : ℕ) n = (↑0 : ℕ)
Tactic: symm
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
m : PosNum
⊢ (↑(HShiftRight.hShiftRight (β := ℕ) m 0) : ℕ) = HShiftRight.hShiftRight (α := ℕ) (β := ℕ) (↑(pos m) : ℕ) 0
have pos : (↑(HShiftRight.hShiftRight (β := ℕ) one 0) : ℕ) = HShiftRight.hShiftRight (α := ℕ) (β := ℕ) (↑(pos one) : ℕ) 0
Tactic: cases m
Cleared hypotheses: m
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
m : PosNum
pos : (↑(HShiftRight.hShiftRight (β := ℕ) one 0) : ℕ) = HShiftRight.hShiftRight (α := ℕ) (β := ℕ) (↑(Num.pos one) : ℕ) 0
⊢ (↑(HShiftRight.hShiftRight (β := ℕ) m 0) : ℕ) = HShiftRight.hShiftRight (α := ℕ) (β := ℕ) (↑(Num.pos m) : ℕ) 0
have pos₁ : ∀ (a : PosNum),
  (↑(HShiftRight.hShiftRight (β := ℕ) a.bit1 0) : ℕ) =
    HShiftRight.hShiftRight (α := ℕ) (β := ℕ) (↑(Num.pos a.bit1) : ℕ) 0
Tactic: cases m
Cleared hypotheses: m
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
m : PosNum
pos : (↑(HShiftRight.hShiftRight (β := ℕ) one 0) : ℕ) = HShiftRight.hShiftRight (α := ℕ) (β := ℕ) (↑(Num.pos one) : ℕ) 0
pos₁ :
  ∀ (a : PosNum),
    (↑(HShiftRight.hShiftRight (β := ℕ) a.bit1 0) : ℕ) =
      HShiftRight.hShiftRight (α := ℕ) (β := ℕ) (↑(Num.pos a.bit1) : ℕ) 0
⊢ (↑(HShiftRight.hShiftRight (β := ℕ) m 0) : ℕ) = HShiftRight.hShiftRight (α := ℕ) (β := ℕ) (↑(Num.pos m) : ℕ) 0
have pos₂ : ∀ (a : PosNum),
  (↑(HShiftRight.hShiftRight (β := ℕ) a.bit0 0) : ℕ) =
    HShiftRight.hShiftRight (α := ℕ) (β := ℕ) (↑(Num.pos a.bit0) : ℕ) 0
Tactic: cases m
Cleared hypotheses: m
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
n : ℕ
m : PosNum
⊢ (↑(m >>> n) : ℕ) = HShiftRight.hShiftRight (α := ℕ) (↑(pos m) : ℕ) n
have pos : ∀ (n : ℕ) (IH : ∀ (m : PosNum), (↑(m >>> n) : ℕ) = HShiftRight.hShiftRight (α := ℕ) (↑(pos m) : ℕ) n) (m : PosNum),
  (↑(m >>> (n + 1)) : ℕ) = HShiftRight.hShiftRight (α := ℕ) (↑(pos m) : ℕ) (n + 1)
Tactic: induction n generalizing m with
  | zero => cases m <;> rfl
  | succ n IH => ?_
Cleared hypotheses: n, m
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (hypothesis)
Goal:
n : ℕ
IH : ∀ (m : PosNum), (↑(m >>> n) : ℕ) = HShiftRight.hShiftRight (α := ℕ) (↑(pos m) : ℕ) n
m : PosNum
⊢ (↑(m >>> (n + 1)) : ℕ) = HShiftRight.hShiftRight (α := ℕ) (↑(pos m) : ℕ) (n + 1)
have hdiv2 : ∀ (m : ℕ), (m + m).div2 = m
Tactic: have hdiv2 : ∀ m, Nat.div2 (m + m) = m := by intro; rw [Nat.div2_val]; lia
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
n : ℕ
IH : ∀ (m : PosNum), (↑(m >>> n) : ℕ) = HShiftRight.hShiftRight (α := ℕ) (↑(pos m) : ℕ) n
m : PosNum
hdiv2 : ∀ (m : ℕ), (m + m).div2 = m
⊢ (↑(m >>> (n + 1)) : ℕ) = HShiftRight.hShiftRight (α := ℕ) (↑(pos m) : ℕ) (n + 1)
have pos : (↑(one >>> (n + 1)) : ℕ) = HShiftRight.hShiftRight (α := ℕ) (↑(pos one) : ℕ) (n + 1)
Tactic: obtain - | m | m := m
Cleared hypotheses: m
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
n : ℕ
IH : ∀ (m : PosNum), (↑(m >>> n) : ℕ) = HShiftRight.hShiftRight (α := ℕ) (↑(Num.pos m) : ℕ) n
m : PosNum
hdiv2 : ∀ (m : ℕ), (m + m).div2 = m
pos : (↑(one >>> (n + 1)) : ℕ) = HShiftRight.hShiftRight (α := ℕ) (↑(Num.pos one) : ℕ) (n + 1)
⊢ (↑(m >>> (n + 1)) : ℕ) = HShiftRight.hShiftRight (α := ℕ) (↑(Num.pos m) : ℕ) (n + 1)
have pos₁ : ∀ (m : PosNum), (↑(m.bit1 >>> (n + 1)) : ℕ) = HShiftRight.hShiftRight (α := ℕ) (↑(Num.pos m.bit1) : ℕ) (n + 1)
Tactic: obtain - | m | m := m
Cleared hypotheses: m
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
n : ℕ
IH : ∀ (m : PosNum), (↑(m >>> n) : ℕ) = HShiftRight.hShiftRight (α := ℕ) (↑(Num.pos m) : ℕ) n
m : PosNum
hdiv2 : ∀ (m : ℕ), (m + m).div2 = m
pos : (↑(one >>> (n + 1)) : ℕ) = HShiftRight.hShiftRight (α := ℕ) (↑(Num.pos one) : ℕ) (n + 1)
pos₁ : ∀ (m : PosNum), (↑(m.bit1 >>> (n + 1)) : ℕ) = HShiftRight.hShiftRight (α := ℕ) (↑(Num.pos m.bit1) : ℕ) (n + 1)
⊢ (↑(m >>> (n + 1)) : ℕ) = HShiftRight.hShiftRight (α := ℕ) (↑(Num.pos m) : ℕ) (n + 1)
have pos₂ : ∀ (m : PosNum), (↑(m.bit0 >>> (n + 1)) : ℕ) = HShiftRight.hShiftRight (α := ℕ) (↑(Num.pos m.bit0) : ℕ) (n + 1)
Tactic: obtain - | m | m := m
Cleared hypotheses: m
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
n : ℕ
IH : ∀ (m : PosNum), (↑(m >>> n) : ℕ) = HShiftRight.hShiftRight (α := ℕ) (↑(pos m) : ℕ) n
hdiv2 : ∀ (m : ℕ), (m + m).div2 = m
m : PosNum
⊢ (↑(m.bit1 >>> (n + 1)) : ℕ) = HShiftRight.hShiftRight (α := ℕ) (↑(pos m.bit1) : ℕ) (n + 1)
have pos : (↑(m.shiftr n) : ℕ) = HShiftRight.hShiftRight (α := ℕ) (↑(pos m.bit1) : ℕ) (n + 1)
Tactic: dsimp only [PosNum.shiftr, ← PosNum.shiftr_eq_shiftRight]
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
n : ℕ
IH : ∀ (m : PosNum), (↑(m >>> n) : ℕ) = HShiftRight.hShiftRight (α := ℕ) (↑(pos m) : ℕ) n
hdiv2 : ∀ (m : ℕ), (m + m).div2 = m
m : PosNum
⊢ (↑(m.bit0 >>> (n + 1)) : ℕ) = HShiftRight.hShiftRight (α := ℕ) (↑(pos m.bit0) : ℕ) (n + 1)
have pos : (↑(m.shiftr n) : ℕ) = HShiftRight.hShiftRight (α := ℕ) (↑(pos m.bit0) : ℕ) (n + 1)
Tactic: dsimp only [PosNum.shiftr, ← PosNum.shiftr_eq_shiftRight]
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
n : ℕ
IH : ∀ (m : PosNum), (↑(m >>> n) : ℕ) = HShiftRight.hShiftRight (α := ℕ) (↑(pos m) : ℕ) n
hdiv2 : ∀ (m : ℕ), (m + m).div2 = m
⊢ (↑0 : ℕ) = HShiftRight.hShiftRight (α := ℕ) (↑(pos one) : ℕ) (n + 1)
have pos : (↑0 : ℕ) = (↑(pos one) : ℕ) / HPow.hPow (α := ℕ) 2 (n + 1)
Tactic: rw [Nat.shiftRight_eq_div_pow]
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
n : ℕ
IH : ∀ (m : PosNum), (↑(m >>> n) : ℕ) = HShiftRight.hShiftRight (α := ℕ) (↑(pos m) : ℕ) n
hdiv2 : ∀ (m : ℕ), (m + m).div2 = m
⊢ (↑0 : ℕ) = (↑(pos one) : ℕ) / HPow.hPow (α := ℕ) 2 (n + 1)
have pos : (↑(pos one) : ℕ) / HPow.hPow (α := ℕ) 2 (n + 1) = (↑0 : ℕ)
Tactic: symm
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
n : ℕ
IH : ∀ (m : PosNum), (↑(m >>> n) : ℕ) = HShiftRight.hShiftRight (α := ℕ) (↑(pos m) : ℕ) n
hdiv2 : ∀ (m : ℕ), (m + m).div2 = m
⊢ (↑(pos one) : ℕ) / HPow.hPow (α := ℕ) 2 (n + 1) = (↑0 : ℕ)
have pos : (↑(pos one) : ℕ) < HPow.hPow (α := ℕ) 2 (n + 1)
Tactic: apply Nat.div_eq_of_lt
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
n : ℕ
IH : ∀ (m : PosNum), (↑(m >>> n) : ℕ) = HShiftRight.hShiftRight (α := ℕ) (↑(pos m) : ℕ) n
hdiv2 : ∀ (m : ℕ), (m + m).div2 = m
m : PosNum
⊢ (↑(m.shiftr n) : ℕ) = HShiftRight.hShiftRight (α := ℕ) (↑(pos m.bit1) : ℕ) (n + 1)
have trans : (↑(m.shiftr n) : ℕ) = HShiftRight.hShiftRight (α := ℕ) (↑(pos m) : ℕ) n
Tactic: trans
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
n : ℕ
IH : ∀ (m : PosNum), (↑(m >>> n) : ℕ) = HShiftRight.hShiftRight (α := ℕ) (↑(pos m) : ℕ) n
hdiv2 : ∀ (m : ℕ), (m + m).div2 = m
m : PosNum
trans : (↑(m.shiftr n) : ℕ) = HShiftRight.hShiftRight (α := ℕ) (↑(pos m) : ℕ) n
⊢ (↑(m.shiftr n) : ℕ) = HShiftRight.hShiftRight (α := ℕ) (↑(pos m.bit1) : ℕ) (n + 1)
have trans₁ : HShiftRight.hShiftRight (α := ℕ) (↑(pos m) : ℕ) n = HShiftRight.hShiftRight (α := ℕ) (↑(pos m.bit1) : ℕ) (n + 1)
Tactic: trans
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
n : ℕ
IH : ∀ (m : PosNum), (↑(m >>> n) : ℕ) = HShiftRight.hShiftRight (α := ℕ) (↑(pos m) : ℕ) n
hdiv2 : ∀ (m : ℕ), (m + m).div2 = m
m : PosNum
⊢ Nat.shiftRight (↑m : ℕ) n = (HAdd.hAdd (α := ℕ) (↑m : ℕ) (↑m : ℕ) + 1).shiftRight (n + 1)
have rw : Nat.shiftRight (↑m : ℕ) n = HShiftRight.hShiftRight (β := ℕ) (HAdd.hAdd (α := ℕ) (↑m : ℕ) (↑m : ℕ) + 1) 1 >>> n
Tactic: rw [add_comm n 1, @Nat.shiftRight_eq _ (1 + n), Nat.shiftRight_add]
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
n : ℕ
IH : ∀ (m : PosNum), (↑(m >>> n) : ℕ) = HShiftRight.hShiftRight (α := ℕ) (↑(pos m) : ℕ) n
hdiv2 : ∀ (m : ℕ), (m + m).div2 = m
m : PosNum
⊢ Nat.shiftRight (↑m : ℕ) n = HShiftRight.hShiftRight (β := ℕ) (HAdd.hAdd (α := ℕ) (↑m : ℕ) (↑m : ℕ) + 1) 1 >>> n
have apply : (↑m : ℕ) = HShiftRight.hShiftRight (β := ℕ) (HAdd.hAdd (α := ℕ) (↑m : ℕ) (↑m : ℕ) + 1) 1
Tactic: apply congr_arg fun x => Nat.shiftRight x n
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
n : ℕ
IH : ∀ (m : PosNum), (↑(m >>> n) : ℕ) = HShiftRight.hShiftRight (α := ℕ) (↑(pos m) : ℕ) n
hdiv2 : ∀ (m : ℕ), (m + m).div2 = m
m : PosNum
⊢ (↑(m.shiftr n) : ℕ) = HShiftRight.hShiftRight (α := ℕ) (↑(pos m.bit0) : ℕ) (n + 1)
have trans : (↑(m.shiftr n) : ℕ) = HShiftRight.hShiftRight (α := ℕ) (↑(pos m) : ℕ) n
Tactic: trans
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
n : ℕ
IH : ∀ (m : PosNum), (↑(m >>> n) : ℕ) = HShiftRight.hShiftRight (α := ℕ) (↑(pos m) : ℕ) n
hdiv2 : ∀ (m : ℕ), (m + m).div2 = m
m : PosNum
trans : (↑(m.shiftr n) : ℕ) = HShiftRight.hShiftRight (α := ℕ) (↑(pos m) : ℕ) n
⊢ (↑(m.shiftr n) : ℕ) = HShiftRight.hShiftRight (α := ℕ) (↑(pos m.bit0) : ℕ) (n + 1)
have trans₁ : HShiftRight.hShiftRight (α := ℕ) (↑(pos m) : ℕ) n = HShiftRight.hShiftRight (α := ℕ) (↑(pos m.bit0) : ℕ) (n + 1)
Tactic: trans
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
n : ℕ
IH : ∀ (m : PosNum), (↑(m >>> n) : ℕ) = HShiftRight.hShiftRight (α := ℕ) (↑(pos m) : ℕ) n
hdiv2 : ∀ (m : ℕ), (m + m).div2 = m
m : PosNum
⊢ Nat.shiftRight (↑m : ℕ) n = (HAdd.hAdd (α := ℕ) (↑m : ℕ) (↑m : ℕ)).shiftRight (n + 1)
have rw : Nat.shiftRight (↑m : ℕ) n = HShiftRight.hShiftRight (β := ℕ) (HAdd.hAdd (α := ℕ) (↑m : ℕ) (↑m : ℕ)) 1 >>> n
Tactic: rw [add_comm n 1, @Nat.shiftRight_eq _ (1 + n), Nat.shiftRight_add]
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
n : ℕ
IH : ∀ (m : PosNum), (↑(m >>> n) : ℕ) = HShiftRight.hShiftRight (α := ℕ) (↑(pos m) : ℕ) n
hdiv2 : ∀ (m : ℕ), (m + m).div2 = m
m : PosNum
⊢ Nat.shiftRight (↑m : ℕ) n = HShiftRight.hShiftRight (β := ℕ) (HAdd.hAdd (α := ℕ) (↑m : ℕ) (↑m : ℕ)) 1 >>> n
have apply : (↑m : ℕ) = HShiftRight.hShiftRight (β := ℕ) (HAdd.hAdd (α := ℕ) (↑m : ℕ) (↑m : ℕ)) 1
Tactic: apply congr_arg fun x => Nat.shiftRight x n
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
n : ℕ
⊢ false = Nat.testBit (↑zero : ℕ) n
have zero : false = Nat.testBit 0 n
Tactic: rw [show (Num.zero : Nat) = 0 from rfl, Nat.zero_testBit]
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
n : ℕ
zero : false = Nat.testBit 0 n
⊢ false = Nat.testBit (↑Num.zero : ℕ) n
have zero₁ : false = false
Tactic: rw [show (Num.zero : Nat) = 0 from rfl, Nat.zero_testBit]
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
n : ℕ
m : PosNum
⊢ m.testBit n = Nat.testBit (↑m : ℕ) n
have pos : ∀ (m : PosNum), m.testBit 0 = Nat.testBit (↑m : ℕ) 0
Tactic: induction n generalizing m
Cleared hypotheses: n, m
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
n : ℕ
m : PosNum
pos : ∀ (m : PosNum), m.testBit 0 = Nat.testBit (↑m : ℕ) 0
⊢ m.testBit n = Nat.testBit (↑m : ℕ) n
have pos₁ : ∀ (n : ℕ),
  (∀ (m : PosNum), m.testBit n = Nat.testBit (↑m : ℕ) n) →
    ∀ (m : PosNum), m.testBit (n + 1) = Nat.testBit (↑m : ℕ) (n + 1)
Tactic: induction n generalizing m
Cleared hypotheses: n, m
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
m : PosNum
⊢ m.testBit 0 = Nat.testBit (↑m : ℕ) 0
have pos : one.testBit 0 = Nat.testBit (↑one : ℕ) 0
Tactic: obtain - | m | m := m
Cleared hypotheses: m
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
m : PosNum
pos : one.testBit 0 = Nat.testBit (↑one : ℕ) 0
⊢ m.testBit 0 = Nat.testBit (↑m : ℕ) 0
have pos₁ : ∀ (m : PosNum), m.bit1.testBit 0 = Nat.testBit (↑m.bit1 : ℕ) 0
Tactic: obtain - | m | m := m
Cleared hypotheses: m
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
m : PosNum
pos : one.testBit 0 = Nat.testBit (↑one : ℕ) 0
pos₁ : ∀ (m : PosNum), m.bit1.testBit 0 = Nat.testBit (↑m.bit1 : ℕ) 0
⊢ m.testBit 0 = Nat.testBit (↑m : ℕ) 0
have pos₂ : ∀ (m : PosNum), m.bit0.testBit 0 = Nat.testBit (↑m.bit0 : ℕ) 0
Tactic: obtain - | m | m := m
Cleared hypotheses: m
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
n : ℕ
h : ∀ (m : PosNum), m.testBit n = Nat.testBit (↑m : ℕ) n
m : PosNum
⊢ m.testBit (n + 1) = Nat.testBit (↑m : ℕ) (n + 1)
have pos : one.testBit (n + 1) = Nat.testBit (↑one : ℕ) (n + 1)
Tactic: obtain - | m | m := m
Cleared hypotheses: m
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
n : ℕ
h : ∀ (m : PosNum), m.testBit n = Nat.testBit (↑m : ℕ) n
m : PosNum
pos : one.testBit (n + 1) = Nat.testBit (↑one : ℕ) (n + 1)
⊢ m.testBit (n + 1) = Nat.testBit (↑m : ℕ) (n + 1)
have pos₁ : ∀ (m : PosNum), m.bit1.testBit (n + 1) = Nat.testBit (↑m.bit1 : ℕ) (n + 1)
Tactic: obtain - | m | m := m
Cleared hypotheses: m
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
n : ℕ
h : ∀ (m : PosNum), m.testBit n = Nat.testBit (↑m : ℕ) n
m : PosNum
pos : one.testBit (n + 1) = Nat.testBit (↑one : ℕ) (n + 1)
pos₁ : ∀ (m : PosNum), m.bit1.testBit (n + 1) = Nat.testBit (↑m.bit1 : ℕ) (n + 1)
⊢ m.testBit (n + 1) = Nat.testBit (↑m : ℕ) (n + 1)
have pos₂ : ∀ (m : PosNum), m.bit0.testBit (n + 1) = Nat.testBit (↑m.bit0 : ℕ) (n + 1)
Tactic: obtain - | m | m := m
Cleared hypotheses: m