awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
pbb : ∀ (m n : PosNum), pos ((PosNum.bit false m).lor (PosNum.bit false n)) = bit (false || false) (pos (m.lor n))
⊢ ∀ (b : Bool) (m n : PosNum), pos ((PosNum.bit false m).lor (PosNum.bit b n)) = bit (false || b) (pos (m.lor n))
have pbb₁ : ∀ (m n : PosNum), pos ((PosNum.bit false m).lor (PosNum.bit true n)) = bit (false || true) (pos (m.lor n))
Tactic: try rintro (_ | _)
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
⊢ ∀ (b : Bool) (m n : PosNum), pos ((PosNum.bit true m).lor (PosNum.bit b n)) = bit (true || b) (pos (m.lor n))
have pbb : ∀ (m n : PosNum), pos ((PosNum.bit true m).lor (PosNum.bit false n)) = bit (true || false) (pos (m.lor n))
Tactic: try rintro (_ | _)
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
pbb : ∀ (m n : PosNum), pos ((PosNum.bit true m).lor (PosNum.bit false n)) = bit (true || false) (pos (m.lor n))
⊢ ∀ (b : Bool) (m n : PosNum), pos ((PosNum.bit true m).lor (PosNum.bit b n)) = bit (true || b) (pos (m.lor n))
have pbb₁ : ∀ (m n : PosNum), pos ((PosNum.bit true m).lor (PosNum.bit true n)) = bit (true || true) (pos (m.lor n))
Tactic: try rintro (_ | _)
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
⊢ ∀ (m n : Num), (↑(m &&& n) : ℕ) = HAnd.hAnd (α := ℕ) (↑m : ℕ) (↑n : ℕ)
have gff : (false && false) = false
Tactic: apply castNum_eq_bitwise PosNum.land
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
gff : (false && false) = false
⊢ ∀ (m n : Num), (↑(m &&& n) : ℕ) = HAnd.hAnd (α := ℕ) (↑m : ℕ) (↑n : ℕ)
have f00 : HAnd.hAnd (α := Num) 0 0 = 0
Tactic: apply castNum_eq_bitwise PosNum.land
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
gff : (false && false) = false
f00 : HAnd.hAnd (α := Num) 0 0 = 0
⊢ ∀ (m n : Num), (↑(m &&& n) : ℕ) = HAnd.hAnd (α := ℕ) (↑m : ℕ) (↑n : ℕ)
have f0n : ∀ (n : PosNum), 0 &&& pos n = bif false && true then pos n else 0
Tactic: apply castNum_eq_bitwise PosNum.land
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
gff : (false && false) = false
f00 : HAnd.hAnd (α := Num) 0 0 = 0
f0n : ∀ (n : PosNum), 0 &&& pos n = bif false && true then pos n else 0
⊢ ∀ (m n : Num), (↑(m &&& n) : ℕ) = HAnd.hAnd (α := ℕ) (↑m : ℕ) (↑n : ℕ)
have fn0 : ∀ (n : PosNum), pos n &&& 0 = bif true && false then pos n else 0
Tactic: apply castNum_eq_bitwise PosNum.land
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
gff : (false && false) = false
f00 : HAnd.hAnd (α := 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
⊢ ∀ (m n : Num), (↑(m &&& n) : ℕ) = HAnd.hAnd (α := ℕ) (↑m : ℕ) (↑n : ℕ)
have fnn : ∀ (m n : PosNum), pos m &&& pos n = m.land n
Tactic: apply castNum_eq_bitwise PosNum.land
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
gff : (false && false) = false
f00 : HAnd.hAnd (α := 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.land n
⊢ ∀ (m n : Num), (↑(m &&& n) : ℕ) = HAnd.hAnd (α := ℕ) (↑m : ℕ) (↑n : ℕ)
have p11 : PosNum.land 1 1 = bif true && true then 1 else 0
Tactic: apply castNum_eq_bitwise PosNum.land
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
gff : (false && false) = false
f00 : HAnd.hAnd (α := 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.land n
p11 : PosNum.land 1 1 = bif true && true then 1 else 0
⊢ ∀ (m n : Num), (↑(m &&& n) : ℕ) = HAnd.hAnd (α := ℕ) (↑m : ℕ) (↑n : ℕ)
have p1b : ∀ (b : Bool) (n : PosNum), PosNum.land 1 (PosNum.bit b n) = bit (true && b) (bif false && true then pos n else 0)
Tactic: apply castNum_eq_bitwise PosNum.land
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
gff : (false && false) = false
f00 : HAnd.hAnd (α := 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.land n
p11 : PosNum.land 1 1 = bif true && true then 1 else 0
p1b : ∀ (b : Bool) (n : PosNum), PosNum.land 1 (PosNum.bit b n) = bit (true && b) (bif false && true then pos n else 0)
⊢ ∀ (m n : Num), (↑(m &&& n) : ℕ) = HAnd.hAnd (α := ℕ) (↑m : ℕ) (↑n : ℕ)
have pb1 : ∀ (a : Bool) (m : PosNum), (PosNum.bit a m).land 1 = bit (a && true) (bif true && false then pos m else 0)
Tactic: apply castNum_eq_bitwise PosNum.land
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
gff : (false && false) = false
f00 : HAnd.hAnd (α := 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.land n
p11 : PosNum.land 1 1 = bif true && true then 1 else 0
p1b : ∀ (b : Bool) (n : PosNum), PosNum.land 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).land 1 = bit (a && true) (bif true && false then pos m else 0)
⊢ ∀ (m n : Num), (↑(m &&& n) : ℕ) = HAnd.hAnd (α := ℕ) (↑m : ℕ) (↑n : ℕ)
have pbb : ∀ (a b : Bool) (m n : PosNum), (PosNum.bit a m).land (PosNum.bit b n) = bit (a && b) (m.land n)
Tactic: apply castNum_eq_bitwise PosNum.land
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
b : Bool
n : PosNum
⊢ PosNum.land 1 (PosNum.bit b n) = bit (true && b) (bif false && true then pos n else 0)
have p1b : PosNum.land 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.land 1 (PosNum.bit false n) = bit (true && false) (bif false && true then pos n else 0)
⊢ PosNum.land 1 (PosNum.bit b n) = bit (true && b) (bif false && true then pos n else 0)
have p1b₁ : PosNum.land 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.land 1 (PosNum.bit b n) = bit (true && b) (bif false && true then pos n else 0)
have p1b : PosNum.land 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.land 1 (PosNum.bit false n) = bit (true && false) (bif false && true then pos n else 0)
⊢ PosNum.land 1 (PosNum.bit b n) = bit (true && b) (bif false && true then pos n else 0)
have p1b₁ : PosNum.land 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).land 1 = bit (a && true) (bif true && false then pos m else 0)
have pb1 : (PosNum.bit false m).land 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).land 1 = bit (false && true) (bif true && false then pos m else 0)
⊢ (PosNum.bit a m).land 1 = bit (a && true) (bif true && false then pos m else 0)
have pb1₁ : (PosNum.bit true m).land 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).land 1 = bit (a && true) (bif true && false then pos m else 0)
have pb1 : (PosNum.bit false m).land 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).land 1 = bit (false && true) (bif true && false then pos m else 0)
⊢ (PosNum.bit a m).land 1 = bit (a && true) (bif true && false then pos m else 0)
have pb1₁ : (PosNum.bit true m).land 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).land (PosNum.bit b n) = bit (a && b) (m.land n)
have pbb : (PosNum.bit false m).land (PosNum.bit false n) = bit (false && false) (m.land 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).land (PosNum.bit false n) = bit (false && false) (m.land n)
⊢ (PosNum.bit a m).land (PosNum.bit b n) = bit (a && b) (m.land n)
have pbb₁ : (PosNum.bit false m).land (PosNum.bit true n) = bit (false && true) (m.land 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).land (PosNum.bit false n) = bit (false && false) (m.land n)
pbb₁ : (PosNum.bit false m).land (PosNum.bit true n) = bit (false && true) (m.land n)
⊢ (PosNum.bit a m).land (PosNum.bit b n) = bit (a && b) (m.land n)
have pbb₂ : (PosNum.bit true m).land (PosNum.bit false n) = bit (true && false) (m.land 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).land (PosNum.bit false n) = bit (false && false) (m.land n)
pbb₁ : (PosNum.bit false m).land (PosNum.bit true n) = bit (false && true) (m.land n)
pbb₂ : (PosNum.bit true m).land (PosNum.bit false n) = bit (true && false) (m.land n)
⊢ (PosNum.bit a m).land (PosNum.bit b n) = bit (a && b) (m.land n)
have pbb₃ : (PosNum.bit true m).land (PosNum.bit true n) = bit (true && true) (m.land 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).land (PosNum.bit b n) = bit (a && b) (m.land n)
have pbb : (PosNum.bit false m).land (PosNum.bit false n) = bit (false && false) (m.land 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).land (PosNum.bit false n) = bit (false && false) (m.land n)
⊢ (PosNum.bit a m).land (PosNum.bit b n) = bit (a && b) (m.land n)
have pbb₁ : (PosNum.bit false m).land (PosNum.bit true n) = bit (false && true) (m.land 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).land (PosNum.bit false n) = bit (false && false) (m.land n)
pbb₁ : (PosNum.bit false m).land (PosNum.bit true n) = bit (false && true) (m.land n)
⊢ (PosNum.bit a m).land (PosNum.bit b n) = bit (a && b) (m.land n)
have pbb₂ : (PosNum.bit true m).land (PosNum.bit false n) = bit (true && false) (m.land 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).land (PosNum.bit false n) = bit (false && false) (m.land n)
pbb₁ : (PosNum.bit false m).land (PosNum.bit true n) = bit (false && true) (m.land n)
pbb₂ : (PosNum.bit true m).land (PosNum.bit false n) = bit (true && false) (m.land n)
⊢ (PosNum.bit a m).land (PosNum.bit b n) = bit (a && b) (m.land n)
have pbb₃ : (PosNum.bit true m).land (PosNum.bit true n) = bit (true && true) (m.land n)
Tactic: try cases_type* Bool
Cleared hypotheses: a, b
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
⊢ ∀ (m n : Num), (↑(m.ldiff n) : ℕ) = Nat.ldiff (↑m : ℕ) (↑n : ℕ)
have gff : (false && !false) = false
Tactic: apply castNum_eq_bitwise PosNum.ldiff
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
gff : (false && !false) = false
⊢ ∀ (m n : Num), (↑(m.ldiff n) : ℕ) = Nat.ldiff (↑m : ℕ) (↑n : ℕ)
have f00 : ldiff 0 0 = 0
Tactic: apply castNum_eq_bitwise PosNum.ldiff
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
gff : (false && !false) = false
f00 : ldiff 0 0 = 0
⊢ ∀ (m n : Num), (↑(m.ldiff n) : ℕ) = Nat.ldiff (↑m : ℕ) (↑n : ℕ)
have f0n : ∀ (n : PosNum), ldiff 0 (pos n) = bif false && !true then pos n else 0
Tactic: apply castNum_eq_bitwise PosNum.ldiff
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
gff : (false && !false) = false
f00 : ldiff 0 0 = 0
f0n : ∀ (n : PosNum), ldiff 0 (pos n) = bif false && !true then pos n else 0
⊢ ∀ (m n : Num), (↑(m.ldiff n) : ℕ) = Nat.ldiff (↑m : ℕ) (↑n : ℕ)
have fn0 : ∀ (n : PosNum), (pos n).ldiff 0 = bif true && !false then pos n else 0
Tactic: apply castNum_eq_bitwise PosNum.ldiff
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
gff : (false && !false) = false
f00 : ldiff 0 0 = 0
f0n : ∀ (n : PosNum), ldiff 0 (pos n) = bif false && !true then pos n else 0
fn0 : ∀ (n : PosNum), (pos n).ldiff 0 = bif true && !false then pos n else 0
⊢ ∀ (m n : Num), (↑(m.ldiff n) : ℕ) = Nat.ldiff (↑m : ℕ) (↑n : ℕ)
have fnn : ∀ (m n : PosNum), (pos m).ldiff (pos n) = m.ldiff n
Tactic: apply castNum_eq_bitwise PosNum.ldiff
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
gff : (false && !false) = false
f00 : ldiff 0 0 = 0
f0n : ∀ (n : PosNum), ldiff 0 (pos n) = bif false && !true then pos n else 0
fn0 : ∀ (n : PosNum), (pos n).ldiff 0 = bif true && !false then pos n else 0
fnn : ∀ (m n : PosNum), (pos m).ldiff (pos n) = m.ldiff n
⊢ ∀ (m n : Num), (↑(m.ldiff n) : ℕ) = Nat.ldiff (↑m : ℕ) (↑n : ℕ)
have p11 : PosNum.ldiff 1 1 = bif true && !true then 1 else 0
Tactic: apply castNum_eq_bitwise PosNum.ldiff
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
gff : (false && !false) = false
f00 : ldiff 0 0 = 0
f0n : ∀ (n : PosNum), ldiff 0 (pos n) = bif false && !true then pos n else 0
fn0 : ∀ (n : PosNum), (pos n).ldiff 0 = bif true && !false then pos n else 0
fnn : ∀ (m n : PosNum), (pos m).ldiff (pos n) = m.ldiff n
p11 : PosNum.ldiff 1 1 = bif true && !true then 1 else 0
⊢ ∀ (m n : Num), (↑(m.ldiff n) : ℕ) = Nat.ldiff (↑m : ℕ) (↑n : ℕ)
have p1b : ∀ (b : Bool) (n : PosNum), PosNum.ldiff 1 (PosNum.bit b n) = bit (true && !b) (bif false && !true then pos n else 0)
Tactic: apply castNum_eq_bitwise PosNum.ldiff
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
gff : (false && !false) = false
f00 : ldiff 0 0 = 0
f0n : ∀ (n : PosNum), ldiff 0 (pos n) = bif false && !true then pos n else 0
fn0 : ∀ (n : PosNum), (pos n).ldiff 0 = bif true && !false then pos n else 0
fnn : ∀ (m n : PosNum), (pos m).ldiff (pos n) = m.ldiff n
p11 : PosNum.ldiff 1 1 = bif true && !true then 1 else 0
p1b :
  ∀ (b : Bool) (n : PosNum), PosNum.ldiff 1 (PosNum.bit b n) = bit (true && !b) (bif false && !true then pos n else 0)
⊢ ∀ (m n : Num), (↑(m.ldiff n) : ℕ) = Nat.ldiff (↑m : ℕ) (↑n : ℕ)
have pb1 : ∀ (a : Bool) (m : PosNum), (PosNum.bit a m).ldiff 1 = bit (a && !true) (bif true && !false then pos m else 0)
Tactic: apply castNum_eq_bitwise PosNum.ldiff
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
gff : (false && !false) = false
f00 : ldiff 0 0 = 0
f0n : ∀ (n : PosNum), ldiff 0 (pos n) = bif false && !true then pos n else 0
fn0 : ∀ (n : PosNum), (pos n).ldiff 0 = bif true && !false then pos n else 0
fnn : ∀ (m n : PosNum), (pos m).ldiff (pos n) = m.ldiff n
p11 : PosNum.ldiff 1 1 = bif true && !true then 1 else 0
p1b :
  ∀ (b : Bool) (n : PosNum), PosNum.ldiff 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).ldiff 1 = bit (a && !true) (bif true && !false then pos m else 0)
⊢ ∀ (m n : Num), (↑(m.ldiff n) : ℕ) = Nat.ldiff (↑m : ℕ) (↑n : ℕ)
have pbb : ∀ (a b : Bool) (m n : PosNum), (PosNum.bit a m).ldiff (PosNum.bit b n) = bit (a && !b) (m.ldiff n)
Tactic: apply castNum_eq_bitwise PosNum.ldiff
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
b : Bool
n : PosNum
⊢ PosNum.ldiff 1 (PosNum.bit b n) = bit (true && !b) (bif false && !true then pos n else 0)
have p1b : PosNum.ldiff 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.ldiff 1 (PosNum.bit false n) = bit (true && !false) (bif false && !true then pos n else 0)
⊢ PosNum.ldiff 1 (PosNum.bit b n) = bit (true && !b) (bif false && !true then pos n else 0)
have p1b₁ : PosNum.ldiff 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.ldiff 1 (PosNum.bit b n) = bit (true && !b) (bif false && !true then pos n else 0)
have p1b : PosNum.ldiff 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.ldiff 1 (PosNum.bit false n) = bit (true && !false) (bif false && !true then pos n else 0)
⊢ PosNum.ldiff 1 (PosNum.bit b n) = bit (true && !b) (bif false && !true then pos n else 0)
have p1b₁ : PosNum.ldiff 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).ldiff 1 = bit (a && !true) (bif true && !false then pos m else 0)
have pb1 : (PosNum.bit false m).ldiff 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).ldiff 1 = bit (false && !true) (bif true && !false then pos m else 0)
⊢ (PosNum.bit a m).ldiff 1 = bit (a && !true) (bif true && !false then pos m else 0)
have pb1₁ : (PosNum.bit true m).ldiff 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).ldiff 1 = bit (a && !true) (bif true && !false then pos m else 0)
have pb1 : (PosNum.bit false m).ldiff 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).ldiff 1 = bit (false && !true) (bif true && !false then pos m else 0)
⊢ (PosNum.bit a m).ldiff 1 = bit (a && !true) (bif true && !false then pos m else 0)
have pb1₁ : (PosNum.bit true m).ldiff 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).ldiff (PosNum.bit b n) = bit (a && !b) (m.ldiff n)
have pbb : (PosNum.bit false m).ldiff (PosNum.bit false n) = bit (false && !false) (m.ldiff 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).ldiff (PosNum.bit false n) = bit (false && !false) (m.ldiff n)
⊢ (PosNum.bit a m).ldiff (PosNum.bit b n) = bit (a && !b) (m.ldiff n)
have pbb₁ : (PosNum.bit false m).ldiff (PosNum.bit true n) = bit (false && !true) (m.ldiff 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).ldiff (PosNum.bit false n) = bit (false && !false) (m.ldiff n)
pbb₁ : (PosNum.bit false m).ldiff (PosNum.bit true n) = bit (false && !true) (m.ldiff n)
⊢ (PosNum.bit a m).ldiff (PosNum.bit b n) = bit (a && !b) (m.ldiff n)
have pbb₂ : (PosNum.bit true m).ldiff (PosNum.bit false n) = bit (true && !false) (m.ldiff 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).ldiff (PosNum.bit false n) = bit (false && !false) (m.ldiff n)
pbb₁ : (PosNum.bit false m).ldiff (PosNum.bit true n) = bit (false && !true) (m.ldiff n)
pbb₂ : (PosNum.bit true m).ldiff (PosNum.bit false n) = bit (true && !false) (m.ldiff n)
⊢ (PosNum.bit a m).ldiff (PosNum.bit b n) = bit (a && !b) (m.ldiff n)
have pbb₃ : (PosNum.bit true m).ldiff (PosNum.bit true n) = bit (true && !true) (m.ldiff 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).ldiff (PosNum.bit b n) = bit (a && !b) (m.ldiff n)
have pbb : (PosNum.bit false m).ldiff (PosNum.bit false n) = bit (false && !false) (m.ldiff 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).ldiff (PosNum.bit false n) = bit (false && !false) (m.ldiff n)
⊢ (PosNum.bit a m).ldiff (PosNum.bit b n) = bit (a && !b) (m.ldiff n)
have pbb₁ : (PosNum.bit false m).ldiff (PosNum.bit true n) = bit (false && !true) (m.ldiff 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).ldiff (PosNum.bit false n) = bit (false && !false) (m.ldiff n)
pbb₁ : (PosNum.bit false m).ldiff (PosNum.bit true n) = bit (false && !true) (m.ldiff n)
⊢ (PosNum.bit a m).ldiff (PosNum.bit b n) = bit (a && !b) (m.ldiff n)
have pbb₂ : (PosNum.bit true m).ldiff (PosNum.bit false n) = bit (true && !false) (m.ldiff 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).ldiff (PosNum.bit false n) = bit (false && !false) (m.ldiff n)
pbb₁ : (PosNum.bit false m).ldiff (PosNum.bit true n) = bit (false && !true) (m.ldiff n)
pbb₂ : (PosNum.bit true m).ldiff (PosNum.bit false n) = bit (true && !false) (m.ldiff n)
⊢ (PosNum.bit a m).ldiff (PosNum.bit b n) = bit (a && !b) (m.ldiff n)
have pbb₃ : (PosNum.bit true m).ldiff (PosNum.bit true n) = bit (true && !true) (m.ldiff n)
Tactic: try cases_type* Bool
Cleared hypotheses: a, b
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
⊢ ∀ (m n : Num), (↑(m ^^^ n) : ℕ) = HXor.hXor (α := ℕ) (↑m : ℕ) (↑n : ℕ)
have gff : (false != false) = false
Tactic: apply castNum_eq_bitwise PosNum.lxor
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
gff : (false != false) = false
⊢ ∀ (m n : Num), (↑(m ^^^ n) : ℕ) = HXor.hXor (α := ℕ) (↑m : ℕ) (↑n : ℕ)
have f00 : HXor.hXor (α := Num) 0 0 = 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
⊢ ∀ (m n : Num), (↑(m ^^^ n) : ℕ) = HXor.hXor (α := ℕ) (↑m : ℕ) (↑n : ℕ)
have f0n : ∀ (n : PosNum), 0 ^^^ pos n = 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
⊢ ∀ (m n : Num), (↑(m ^^^ n) : ℕ) = HXor.hXor (α := ℕ) (↑m : ℕ) (↑n : ℕ)
have fn0 : ∀ (n : PosNum), pos n ^^^ 0 = bif true != false 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
⊢ ∀ (m n : Num), (↑(m ^^^ n) : ℕ) = HXor.hXor (α := ℕ) (↑m : ℕ) (↑n : ℕ)
have fnn : ∀ (m n : PosNum), pos m ^^^ pos n = m.lxor n
Tactic: apply castNum_eq_bitwise PosNum.lxor