awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Num.Lemmas
Goal:
pb1 : pos ((PosNum.bit true one).lor 1) = bit (true || true) (bif true || false then pos one else 0)
pb1₁ :
  ∀ (a : PosNum), pos ((PosNum.bit true a.bit1).lor 1) = bit (true || true) (bif true || false then pos a.bit1 else 0)
pb1₂ :
  ∀ (a : PosNum), pos ((PosNum.bit true a.bit0).lor 1) = bit (true || true) (bif true || false then pos a.bit0 else 0)
⊢ ∀ (m : PosNum), pos ((PosNum.bit true m).lor 1) = bit (true || true) (bif true || false then pos m else 0)

Tactic:
try rintro (_ | _)
-- Module: Mathlib.Data.Num.Lemmas
Goal:
pbb : ∀ (m n : PosNum), pos ((PosNum.bit false m).lor (PosNum.bit false n)) = bit (false || false) (pos (m.lor n))
pbb₁ : ∀ (m n : PosNum), pos ((PosNum.bit false m).lor (PosNum.bit true n)) = bit (false || true) (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))

Tactic:
try rintro (_ | _)
-- Module: Mathlib.Data.Num.Lemmas
Goal:
pbb : ∀ (m n : PosNum), pos ((PosNum.bit true m).lor (PosNum.bit false n)) = bit (true || false) (pos (m.lor n))
pbb₁ : ∀ (m n : PosNum), pos ((PosNum.bit true m).lor (PosNum.bit true n)) = bit (true || true) (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))

Tactic:
try rintro (_ | _)
-- Module: Mathlib.Data.Num.Lemmas
Goal:
⊢ (false || false) = false

Tactic:
rfl
-- Module: Mathlib.Data.Num.Lemmas
Goal:
⊢ HOr.hOr (α := Num) 0 0 = 0

Tactic:
rfl
-- Module: Mathlib.Data.Num.Lemmas
Goal:
⊢ 0 ||| pos one = bif false || true then pos one else 0

Tactic:
rfl
-- Module: Mathlib.Data.Num.Lemmas
Goal:
a : PosNum
⊢ 0 ||| pos a.bit1 = bif false || true then pos a.bit1 else 0

Tactic:
rfl
-- Module: Mathlib.Data.Num.Lemmas
Goal:
a : PosNum
⊢ 0 ||| pos a.bit0 = bif false || true then pos a.bit0 else 0

Tactic:
rfl
-- Module: Mathlib.Data.Num.Lemmas
Goal:
⊢ pos one ||| 0 = bif true || false then pos one else 0

Tactic:
rfl
-- Module: Mathlib.Data.Num.Lemmas
Goal:
a : PosNum
⊢ pos a.bit1 ||| 0 = bif true || false then pos a.bit1 else 0

Tactic:
rfl
-- Module: Mathlib.Data.Num.Lemmas
Goal:
a : PosNum
⊢ pos a.bit0 ||| 0 = bif true || false then pos a.bit0 else 0

Tactic:
rfl
-- Module: Mathlib.Data.Num.Lemmas
Goal:
⊢ pos one ||| pos one = pos (one.lor one)

Tactic:
rfl
-- Module: Mathlib.Data.Num.Lemmas
Goal:
a : PosNum
⊢ pos one ||| pos a.bit1 = pos (one.lor a.bit1)

Tactic:
rfl
-- Module: Mathlib.Data.Num.Lemmas
Goal:
a : PosNum
⊢ pos one ||| pos a.bit0 = pos (one.lor a.bit0)

Tactic:
rfl
-- Module: Mathlib.Data.Num.Lemmas
Goal:
a : PosNum
⊢ pos a.bit1 ||| pos one = pos (a.bit1.lor one)

Tactic:
rfl
-- Module: Mathlib.Data.Num.Lemmas
Goal:
a a_1 : PosNum
⊢ pos a.bit1 ||| pos a_1.bit1 = pos (a.bit1.lor a_1.bit1)

Tactic:
rfl
-- Module: Mathlib.Data.Num.Lemmas
Goal:
a a_1 : PosNum
⊢ pos a.bit1 ||| pos a_1.bit0 = pos (a.bit1.lor a_1.bit0)

Tactic:
rfl
-- Module: Mathlib.Data.Num.Lemmas
Goal:
a : PosNum
⊢ pos a.bit0 ||| pos one = pos (a.bit0.lor one)

Tactic:
rfl
-- Module: Mathlib.Data.Num.Lemmas
Goal:
a a_1 : PosNum
⊢ pos a.bit0 ||| pos a_1.bit1 = pos (a.bit0.lor a_1.bit1)

Tactic:
rfl
-- Module: Mathlib.Data.Num.Lemmas
Goal:
a a_1 : PosNum
⊢ pos a.bit0 ||| pos a_1.bit0 = pos (a.bit0.lor a_1.bit0)

Tactic:
rfl
-- Module: Mathlib.Data.Num.Lemmas
Goal:
⊢ pos (lor 1 1) = bif true || true then 1 else 0

Tactic:
rfl
-- Module: Mathlib.Data.Num.Lemmas
Goal:
⊢ pos (lor 1 (PosNum.bit false one)) = bit (true || false) (bif false || true then pos one else 0)

Tactic:
rfl
-- Module: Mathlib.Data.Num.Lemmas
Goal:
a : PosNum
⊢ pos (lor 1 (PosNum.bit false a.bit1)) = bit (true || false) (bif false || true then pos a.bit1 else 0)

Tactic:
rfl
-- Module: Mathlib.Data.Num.Lemmas
Goal:
a : PosNum
⊢ pos (lor 1 (PosNum.bit false a.bit0)) = bit (true || false) (bif false || true then pos a.bit0 else 0)

Tactic:
rfl
-- Module: Mathlib.Data.Num.Lemmas
Goal:
⊢ pos (lor 1 (PosNum.bit true one)) = bit (true || true) (bif false || true then pos one else 0)

Tactic:
rfl
-- Module: Mathlib.Data.Num.Lemmas
Goal:
a : PosNum
⊢ pos (lor 1 (PosNum.bit true a.bit1)) = bit (true || true) (bif false || true then pos a.bit1 else 0)

Tactic:
rfl
-- Module: Mathlib.Data.Num.Lemmas
Goal:
a : PosNum
⊢ pos (lor 1 (PosNum.bit true a.bit0)) = bit (true || true) (bif false || true then pos a.bit0 else 0)

Tactic:
rfl
-- Module: Mathlib.Data.Num.Lemmas
Goal:
⊢ pos ((PosNum.bit false one).lor 1) = bit (false || true) (bif true || false then pos one else 0)

Tactic:
rfl
-- Module: Mathlib.Data.Num.Lemmas
Goal:
a : PosNum
⊢ pos ((PosNum.bit false a.bit1).lor 1) = bit (false || true) (bif true || false then pos a.bit1 else 0)

Tactic:
rfl
-- Module: Mathlib.Data.Num.Lemmas
Goal:
a : PosNum
⊢ pos ((PosNum.bit false a.bit0).lor 1) = bit (false || true) (bif true || false then pos a.bit0 else 0)

Tactic:
rfl
-- Module: Mathlib.Data.Num.Lemmas
Goal:
⊢ pos ((PosNum.bit true one).lor 1) = bit (true || true) (bif true || false then pos one else 0)

Tactic:
rfl
-- Module: Mathlib.Data.Num.Lemmas
Goal:
a : PosNum
⊢ pos ((PosNum.bit true a.bit1).lor 1) = bit (true || true) (bif true || false then pos a.bit1 else 0)

Tactic:
rfl
-- Module: Mathlib.Data.Num.Lemmas
Goal:
a : PosNum
⊢ pos ((PosNum.bit true a.bit0).lor 1) = bit (true || true) (bif true || false then pos a.bit0 else 0)

Tactic:
rfl
-- Module: Mathlib.Data.Num.Lemmas
Goal:
m n : PosNum
⊢ pos ((PosNum.bit false m).lor (PosNum.bit false n)) = bit (false || false) (pos (m.lor n))

Tactic:
rfl
-- Module: Mathlib.Data.Num.Lemmas
Goal:
m n : PosNum
⊢ pos ((PosNum.bit false m).lor (PosNum.bit true n)) = bit (false || true) (pos (m.lor n))

Tactic:
rfl
-- Module: Mathlib.Data.Num.Lemmas
Goal:
m n : PosNum
⊢ pos ((PosNum.bit true m).lor (PosNum.bit false n)) = bit (true || false) (pos (m.lor n))

Tactic:
rfl
-- Module: Mathlib.Data.Num.Lemmas
Goal:
m n : PosNum
⊢ pos ((PosNum.bit true m).lor (PosNum.bit true n)) = bit (true || true) (pos (m.lor n))

Tactic:
rfl
-- Module: Mathlib.Data.Num.Lemmas
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)
pbb : ∀ (a b : Bool) (m n : PosNum), (PosNum.bit a m).land (PosNum.bit b n) = bit (a && b) (m.land n)
⊢ ∀ (m n : Num), (↑(m &&& n) : ℕ) = HAnd.hAnd (α := ℕ) (↑m : ℕ) (↑n : ℕ)

Tactic:
apply castNum_eq_bitwise PosNum.land

Premises used: Num.castNum_eq_bitwise, PosNum.land
-- Module: Mathlib.Data.Num.Lemmas
Goal:
b : Bool
n : PosNum
p1b : PosNum.land 1 (PosNum.bit false n) = bit (true && false) (bif false && true then pos n else 0)
p1b₁ : PosNum.land 1 (PosNum.bit true n) = bit (true && true) (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)

Tactic:
cases_type* Bool

Premises used: Bool
-- Module: Mathlib.Data.Num.Lemmas
Goal:
b : Bool
n : PosNum
p1b : PosNum.land 1 (PosNum.bit false n) = bit (true && false) (bif false && true then pos n else 0)
p1b₁ : PosNum.land 1 (PosNum.bit true n) = bit (true && true) (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)

Tactic:
try cases_type* Bool

Premises used: Bool
-- Module: Mathlib.Data.Num.Lemmas
Goal:
a : Bool
m : PosNum
pb1 : (PosNum.bit false m).land 1 = bit (false && true) (bif true && false then pos m else 0)
pb1₁ : (PosNum.bit true m).land 1 = bit (true && 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)

Tactic:
cases_type* Bool

Premises used: Bool
-- Module: Mathlib.Data.Num.Lemmas
Goal:
a : Bool
m : PosNum
pb1 : (PosNum.bit false m).land 1 = bit (false && true) (bif true && false then pos m else 0)
pb1₁ : (PosNum.bit true m).land 1 = bit (true && 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)

Tactic:
try cases_type* Bool

Premises used: Bool
-- Module: Mathlib.Data.Num.Lemmas
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)
pbb₃ : (PosNum.bit true m).land (PosNum.bit true n) = bit (true && true) (m.land n)
⊢ (PosNum.bit a m).land (PosNum.bit b n) = bit (a && b) (m.land n)

Tactic:
cases_type* Bool

Premises used: Bool
-- Module: Mathlib.Data.Num.Lemmas
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)
pbb₃ : (PosNum.bit true m).land (PosNum.bit true n) = bit (true && true) (m.land n)
⊢ (PosNum.bit a m).land (PosNum.bit b n) = bit (a && b) (m.land n)

Tactic:
try cases_type* Bool

Premises used: Bool
-- Module: Mathlib.Data.Num.Lemmas
Goal:
⊢ (false && false) = false

Tactic:
rfl
-- Module: Mathlib.Data.Num.Lemmas
Goal:
⊢ HAnd.hAnd (α := Num) 0 0 = 0

Tactic:
rfl
-- Module: Mathlib.Data.Num.Lemmas
Goal:
n : PosNum
⊢ 0 &&& pos n = bif false && true then pos n else 0

Tactic:
rfl
-- Module: Mathlib.Data.Num.Lemmas
Goal:
n : PosNum
⊢ pos n &&& 0 = bif true && false then pos n else 0

Tactic:
rfl
-- Module: Mathlib.Data.Num.Lemmas
Goal:
m n : PosNum
⊢ pos m &&& pos n = m.land n

Tactic:
rfl
-- Module: Mathlib.Data.Num.Lemmas
Goal:
⊢ PosNum.land 1 1 = bif true && true then 1 else 0

Tactic:
rfl
-- Module: Mathlib.Data.Num.Lemmas
Goal:
n : PosNum
⊢ PosNum.land 1 (PosNum.bit false n) = bit (true && false) (bif false && true then pos n else 0)

Tactic:
rfl
-- Module: Mathlib.Data.Num.Lemmas
Goal:
n : PosNum
⊢ PosNum.land 1 (PosNum.bit true n) = bit (true && true) (bif false && true then pos n else 0)

Tactic:
rfl
-- Module: Mathlib.Data.Num.Lemmas
Goal:
m : PosNum
⊢ (PosNum.bit false m).land 1 = bit (false && true) (bif true && false then pos m else 0)

Tactic:
rfl
-- Module: Mathlib.Data.Num.Lemmas
Goal:
m : PosNum
⊢ (PosNum.bit true m).land 1 = bit (true && true) (bif true && false then pos m else 0)

Tactic:
rfl
-- Module: Mathlib.Data.Num.Lemmas
Goal:
m n : PosNum
⊢ (PosNum.bit false m).land (PosNum.bit false n) = bit (false && false) (m.land n)

Tactic:
rfl
-- Module: Mathlib.Data.Num.Lemmas
Goal:
m n : PosNum
⊢ (PosNum.bit false m).land (PosNum.bit true n) = bit (false && true) (m.land n)

Tactic:
rfl
-- Module: Mathlib.Data.Num.Lemmas
Goal:
m n : PosNum
⊢ (PosNum.bit true m).land (PosNum.bit false n) = bit (true && false) (m.land n)

Tactic:
rfl
-- Module: Mathlib.Data.Num.Lemmas
Goal:
m n : PosNum
⊢ (PosNum.bit true m).land (PosNum.bit true n) = bit (true && true) (m.land n)

Tactic:
rfl
-- Module: Mathlib.Data.Num.Lemmas
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)
pbb : ∀ (a b : Bool) (m n : PosNum), (PosNum.bit a m).ldiff (PosNum.bit b n) = bit (a && !b) (m.ldiff n)
⊢ ∀ (m n : Num), (↑(m.ldiff n) : ℕ) = Nat.ldiff (↑m : ℕ) (↑n : ℕ)

Tactic:
apply castNum_eq_bitwise PosNum.ldiff

Premises used: Num.castNum_eq_bitwise, PosNum.ldiff
-- Module: Mathlib.Data.Num.Lemmas
Goal:
b : Bool
n : PosNum
p1b : PosNum.ldiff 1 (PosNum.bit false n) = bit (true && !false) (bif false && !true then pos n else 0)
p1b₁ : PosNum.ldiff 1 (PosNum.bit true n) = bit (true && !true) (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)

Tactic:
cases_type* Bool

Premises used: Bool
-- Module: Mathlib.Data.Num.Lemmas
Goal:
b : Bool
n : PosNum
p1b : PosNum.ldiff 1 (PosNum.bit false n) = bit (true && !false) (bif false && !true then pos n else 0)
p1b₁ : PosNum.ldiff 1 (PosNum.bit true n) = bit (true && !true) (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)

Tactic:
try cases_type* Bool

Premises used: Bool
-- Module: Mathlib.Data.Num.Lemmas
Goal:
a : Bool
m : PosNum
pb1 : (PosNum.bit false m).ldiff 1 = bit (false && !true) (bif true && !false then pos m else 0)
pb1₁ : (PosNum.bit true m).ldiff 1 = bit (true && !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)

Tactic:
cases_type* Bool

Premises used: Bool
-- Module: Mathlib.Data.Num.Lemmas
Goal:
a : Bool
m : PosNum
pb1 : (PosNum.bit false m).ldiff 1 = bit (false && !true) (bif true && !false then pos m else 0)
pb1₁ : (PosNum.bit true m).ldiff 1 = bit (true && !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)

Tactic:
try cases_type* Bool

Premises used: Bool
-- Module: Mathlib.Data.Num.Lemmas
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)
pbb₃ : (PosNum.bit true m).ldiff (PosNum.bit true n) = bit (true && !true) (m.ldiff n)
⊢ (PosNum.bit a m).ldiff (PosNum.bit b n) = bit (a && !b) (m.ldiff n)

Tactic:
cases_type* Bool

Premises used: Bool
-- Module: Mathlib.Data.Num.Lemmas
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)
pbb₃ : (PosNum.bit true m).ldiff (PosNum.bit true n) = bit (true && !true) (m.ldiff n)
⊢ (PosNum.bit a m).ldiff (PosNum.bit b n) = bit (a && !b) (m.ldiff n)

Tactic:
try cases_type* Bool

Premises used: Bool
-- Module: Mathlib.Data.Num.Lemmas
Goal:
⊢ (false && !false) = false

Tactic:
rfl
-- Module: Mathlib.Data.Num.Lemmas
Goal:
⊢ ldiff 0 0 = 0

Tactic:
rfl
-- Module: Mathlib.Data.Num.Lemmas
Goal:
n : PosNum
⊢ ldiff 0 (pos n) = bif false && !true then pos n else 0

Tactic:
rfl
-- Module: Mathlib.Data.Num.Lemmas
Goal:
n : PosNum
⊢ (pos n).ldiff 0 = bif true && !false then pos n else 0

Tactic:
rfl
-- Module: Mathlib.Data.Num.Lemmas
Goal:
m n : PosNum
⊢ (pos m).ldiff (pos n) = m.ldiff n

Tactic:
rfl
-- Module: Mathlib.Data.Num.Lemmas
Goal:
⊢ PosNum.ldiff 1 1 = bif true && !true then 1 else 0

Tactic:
rfl
-- Module: Mathlib.Data.Num.Lemmas
Goal:
n : PosNum
⊢ PosNum.ldiff 1 (PosNum.bit false n) = bit (true && !false) (bif false && !true then pos n else 0)

Tactic:
rfl
-- Module: Mathlib.Data.Num.Lemmas
Goal:
n : PosNum
⊢ PosNum.ldiff 1 (PosNum.bit true n) = bit (true && !true) (bif false && !true then pos n else 0)

Tactic:
rfl
-- Module: Mathlib.Data.Num.Lemmas
Goal:
m : PosNum
⊢ (PosNum.bit false m).ldiff 1 = bit (false && !true) (bif true && !false then pos m else 0)

Tactic:
rfl
-- Module: Mathlib.Data.Num.Lemmas
Goal:
m : PosNum
⊢ (PosNum.bit true m).ldiff 1 = bit (true && !true) (bif true && !false then pos m else 0)

Tactic:
rfl
-- Module: Mathlib.Data.Num.Lemmas
Goal:
m n : PosNum
⊢ (PosNum.bit false m).ldiff (PosNum.bit false n) = bit (false && !false) (m.ldiff n)

Tactic:
rfl
-- Module: Mathlib.Data.Num.Lemmas
Goal:
m n : PosNum
⊢ (PosNum.bit false m).ldiff (PosNum.bit true n) = bit (false && !true) (m.ldiff n)

Tactic:
rfl
-- Module: Mathlib.Data.Num.Lemmas
Goal:
m n : PosNum
⊢ (PosNum.bit true m).ldiff (PosNum.bit false n) = bit (true && !false) (m.ldiff n)

Tactic:
rfl
-- Module: Mathlib.Data.Num.Lemmas
Goal:
m n : PosNum
⊢ (PosNum.bit true m).ldiff (PosNum.bit true n) = bit (true && !true) (m.ldiff n)

Tactic:
rfl
-- Module: Mathlib.Data.Num.Lemmas
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)
pbb : ∀ (a b : Bool) (m n : PosNum), (PosNum.bit a m).lxor (PosNum.bit b n) = bit (a != b) (m.lxor n)
⊢ ∀ (m n : Num), (↑(m ^^^ n) : ℕ) = HXor.hXor (α := ℕ) (↑m : ℕ) (↑n : ℕ)

Tactic:
apply castNum_eq_bitwise PosNum.lxor

Premises used: Num.castNum_eq_bitwise, PosNum.lxor
-- Module: Mathlib.Data.Num.Lemmas
Goal:
b : Bool
n : PosNum
p1b : PosNum.lxor 1 (PosNum.bit false n) = bit (true != false) (bif false != true then pos n else 0)
p1b₁ : PosNum.lxor 1 (PosNum.bit true n) = bit (true != true) (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)

Tactic:
cases_type* Bool

Premises used: Bool
-- Module: Mathlib.Data.Num.Lemmas
Goal:
b : Bool
n : PosNum
p1b : PosNum.lxor 1 (PosNum.bit false n) = bit (true != false) (bif false != true then pos n else 0)
p1b₁ : PosNum.lxor 1 (PosNum.bit true n) = bit (true != true) (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)

Tactic:
try cases_type* Bool

Premises used: Bool
-- Module: Mathlib.Data.Num.Lemmas
Goal:
a : Bool
m : PosNum
pb1 : (PosNum.bit false m).lxor 1 = bit (false != true) (bif true != false then pos m else 0)
pb1₁ : (PosNum.bit true m).lxor 1 = bit (true != 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)

Tactic:
cases_type* Bool

Premises used: Bool
-- Module: Mathlib.Data.Num.Lemmas
Goal:
a : Bool
m : PosNum
pb1 : (PosNum.bit false m).lxor 1 = bit (false != true) (bif true != false then pos m else 0)
pb1₁ : (PosNum.bit true m).lxor 1 = bit (true != 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)

Tactic:
try cases_type* Bool

Premises used: Bool
-- Module: Mathlib.Data.Num.Lemmas
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)
pbb₃ : (PosNum.bit true m).lxor (PosNum.bit true n) = bit (true != true) (m.lxor n)
⊢ (PosNum.bit a m).lxor (PosNum.bit b n) = bit (a != b) (m.lxor n)

Tactic:
cases_type* Bool

Premises used: Bool
-- Module: Mathlib.Data.Num.Lemmas
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)
pbb₃ : (PosNum.bit true m).lxor (PosNum.bit true n) = bit (true != true) (m.lxor n)
⊢ (PosNum.bit a m).lxor (PosNum.bit b n) = bit (a != b) (m.lxor n)

Tactic:
try cases_type* Bool

Premises used: Bool
-- Module: Mathlib.Data.Num.Lemmas
Goal:
⊢ (false != false) = false

Tactic:
rfl
-- Module: Mathlib.Data.Num.Lemmas
Goal:
⊢ HXor.hXor (α := Num) 0 0 = 0

Tactic:
rfl
-- Module: Mathlib.Data.Num.Lemmas
Goal:
n : PosNum
⊢ 0 ^^^ pos n = bif false != true then pos n else 0

Tactic:
rfl
-- Module: Mathlib.Data.Num.Lemmas
Goal:
n : PosNum
⊢ pos n ^^^ 0 = bif true != false then pos n else 0

Tactic:
rfl
-- Module: Mathlib.Data.Num.Lemmas
Goal:
m n : PosNum
⊢ pos m ^^^ pos n = m.lxor n

Tactic:
rfl
-- Module: Mathlib.Data.Num.Lemmas
Goal:
⊢ PosNum.lxor 1 1 = bif true != true then 1 else 0

Tactic:
rfl
-- Module: Mathlib.Data.Num.Lemmas
Goal:
n : PosNum
⊢ PosNum.lxor 1 (PosNum.bit false n) = bit (true != false) (bif false != true then pos n else 0)

Tactic:
rfl
-- Module: Mathlib.Data.Num.Lemmas
Goal:
n : PosNum
⊢ PosNum.lxor 1 (PosNum.bit true n) = bit (true != true) (bif false != true then pos n else 0)

Tactic:
rfl
-- Module: Mathlib.Data.Num.Lemmas
Goal:
m : PosNum
⊢ (PosNum.bit false m).lxor 1 = bit (false != true) (bif true != false then pos m else 0)

Tactic:
rfl
-- Module: Mathlib.Data.Num.Lemmas
Goal:
m : PosNum
⊢ (PosNum.bit true m).lxor 1 = bit (true != true) (bif true != false then pos m else 0)

Tactic:
rfl
-- Module: Mathlib.Data.Num.Lemmas
Goal:
m n : PosNum
⊢ (PosNum.bit false m).lxor (PosNum.bit false n) = bit (false != false) (m.lxor n)

Tactic:
rfl
-- Module: Mathlib.Data.Num.Lemmas
Goal:
m n : PosNum
⊢ (PosNum.bit false m).lxor (PosNum.bit true n) = bit (false != true) (m.lxor n)

Tactic:
rfl
-- Module: Mathlib.Data.Num.Lemmas
Goal:
m n : PosNum
⊢ (PosNum.bit true m).lxor (PosNum.bit false n) = bit (true != false) (m.lxor n)

Tactic:
rfl
-- Module: Mathlib.Data.Num.Lemmas
Goal:
m n : PosNum
⊢ (PosNum.bit true m).lxor (PosNum.bit true n) = bit (true != true) (m.lxor n)

Tactic:
rfl
-- Module: Mathlib.Data.Num.Lemmas
Goal:
m : Num
n : ℕ
zero : (↑(Num.zero <<< n) : ℕ) = (↑Num.zero : ℕ) <<< n
pos : ∀ (a : PosNum), (↑(Num.pos a <<< n) : ℕ) = (↑(Num.pos a) : ℕ) <<< n
⊢ (↑(m <<< n) : ℕ) = (↑m : ℕ) <<< n

Tactic:
cases m
-- Module: Mathlib.Data.Num.Lemmas
Goal:
n : ℕ
zero : (↑Num.zero : ℕ) <<< n = (↑0 : ℕ)
⊢ (↑0 : ℕ) = (↑Num.zero : ℕ) <<< n

Tactic:
symm
-- Module: Mathlib.Data.Num.Lemmas
Goal:
n : ℕ
⊢ (↑zero : ℕ) <<< n = (↑0 : ℕ)

Tactic:
apply Nat.zero_shiftLeft

Premises used: Nat.zero_shiftLeft
-- Module: Mathlib.Data.Num.Lemmas
Goal:
a : PosNum
⊢ (↑(a <<< 0) : ℕ) = HShiftLeft.hShiftLeft (α := ℕ) (↑a : ℕ) 0

Tactic:
rfl
-- Module: Mathlib.Data.Num.Lemmas
Goal:
a : PosNum
n : ℕ
IH : (↑(a <<< n) : ℕ) = (↑a : ℕ) <<< n
⊢ (↑(a <<< (n + 1)) : ℕ) = (↑a : ℕ) <<< (n + 1)

Tactic:
simp [PosNum.shiftl_succ_eq_bit0_shiftl, Nat.shiftLeft_succ, IH, mul_comm,
      -shiftl_eq_shiftLeft, -PosNum.shiftl_eq_shiftLeft, mul_two]

Premises used: PosNum.shiftl_eq_shiftLeft, Nat.shiftLeft_succ, Num.shiftl_eq_shiftLeft, PosNum.shiftl_succ_eq_bit0_shiftl, mul_comm, mul_two
-- Module: Mathlib.Data.Num.Lemmas
Goal:
n : ℕ
a : PosNum
pos : (↑(a <<< 0) : ℕ) = HShiftLeft.hShiftLeft (α := ℕ) (↑a : ℕ) 0
pos₁ : ∀ (n : ℕ) (IH : (↑(a <<< n) : ℕ) = (↑a : ℕ) <<< n), (↑(a <<< (n + 1)) : ℕ) = (↑a : ℕ) <<< (n + 1)
⊢ (↑(a <<< n) : ℕ) = (↑a : ℕ) <<< n

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]

Premises used: PosNum.shiftl_eq_shiftLeft, Nat.shiftLeft_succ, Num.succ, Num.shiftl_eq_shiftLeft, PosNum.shiftl_succ_eq_bit0_shiftl, mul_comm, mul_two, Num.zero
-- Module: Mathlib.Data.Num.Lemmas
Goal:
m : Num
n : ℕ
zero : (↑(Num.zero >>> n) : ℕ) = HShiftRight.hShiftRight (α := ℕ) (↑Num.zero : ℕ) n
pos : ∀ (m : PosNum), (↑(Num.pos m >>> n) : ℕ) = HShiftRight.hShiftRight (α := ℕ) (↑(Num.pos m) : ℕ) n
⊢ (↑(m >>> n) : ℕ) = HShiftRight.hShiftRight (α := ℕ) (↑m : ℕ) n

Tactic:
obtain - | m := m
-- Module: Mathlib.Data.Num.Lemmas
Goal:
n : ℕ
zero : HShiftRight.hShiftRight (α := ℕ) (↑Num.zero : ℕ) n = (↑0 : ℕ)
⊢ (↑0 : ℕ) = HShiftRight.hShiftRight (α := ℕ) (↑Num.zero : ℕ) n

Tactic:
symm
-- Module: Mathlib.Data.Num.Lemmas
Goal:
n : ℕ
⊢ HShiftRight.hShiftRight (α := ℕ) (↑zero : ℕ) n = (↑0 : ℕ)

Tactic:
apply Nat.zero_shiftRight

Premises used: Nat.zero_shiftRight