awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Num.Lemmas
Goal:
f : Num → Num → Num
g : Bool → Bool → Bool
p : PosNum → PosNum → Num
gff : g false false = false
f00 : f 0 0 = 0
f0n : ∀ (n : PosNum), f 0 (Num.pos n) = bif g false true then Num.pos n else 0
fn0 : ∀ (n : PosNum), f (Num.pos n) 0 = bif g true false then Num.pos n else 0
fnn : ∀ (m n : PosNum), f (Num.pos m) (Num.pos n) = p m n
p11 : p 1 1 = bif g true true then 1 else 0
p1b : ∀ (b : Bool) (n : PosNum), p 1 (PosNum.bit b n) = bit (g true b) (bif g false true then Num.pos n else 0)
pb1 : ∀ (a : Bool) (m : PosNum), p (PosNum.bit a m) 1 = bit (g a true) (bif g true false then Num.pos m else 0)
pbb : ∀ (a b : Bool) (m n : PosNum), p (PosNum.bit a m) (PosNum.bit b n) = bit (g a b) (p m n)
this : ∀ (b : Bool) (n : PosNum), Eq (α := ℕ) (bif b then (↑n : ℕ) else 0) (↑(bif b then Num.pos n else 0) : ℕ)
this' : ∀ (b : Bool) (n : PosNum), (↑(Num.pos (PosNum.bit b n)) : ℕ) = Nat.bit b (↑n : ℕ)
n : PosNum
pos : (↑(p 1 (PosNum.bit true n)) : ℕ) = Nat.bit (g true true) (if g false true = true then (↑n : ℕ) else 0)
pos₁ : (↑(p 1 (PosNum.bit true n)) : ℕ) = Nat.bit (g true true) (bif g false true then (↑n : ℕ) else 0)
pos₂ : (↑(p 1 (PosNum.bit true n)) : ℕ) = Nat.bit (g true true) (↑(bif g false true then Num.pos n else 0) : ℕ)
pos₃ : Eq (α := ℕ) (↑(p 1 (PosNum.bit true n)) : ℕ) (↑(bit (g true true) (bif g false true then Num.pos n else 0)) : ℕ)
pos₄ pos₅ :
  Eq (α := ℕ) (↑(bit (g true true) (bif g false true then Num.pos n else 0)) : ℕ)
    (↑(bit (g true true) (bif g false true then Num.pos n else 0)) : ℕ)
⊢ (↑(p 1 (PosNum.bit true n)) : ℕ) = Nat.bit (g true true) (Nat.bitwise g 0 (↑n : ℕ))

Tactic:
rw [Nat.bitwise_zero_left, ← Bool.cond_eq_ite, this, ← bit_to_nat, p1b]

Premises used: Num.bit_to_nat, Nat.bitwise_zero_left, Bool.cond_eq_ite
-- Module: Mathlib.Data.Num.Lemmas
Goal:
f : Num → Num → Num
g : Bool → Bool → Bool
p : PosNum → PosNum → Num
gff : g false false = false
f00 : f 0 0 = 0
f0n : ∀ (n : PosNum), f 0 (Num.pos n) = bif g false true then Num.pos n else 0
fn0 : ∀ (n : PosNum), f (Num.pos n) 0 = bif g true false then Num.pos n else 0
fnn : ∀ (m n : PosNum), f (Num.pos m) (Num.pos n) = p m n
p11 : p 1 1 = bif g true true then 1 else 0
p1b : ∀ (b : Bool) (n : PosNum), p 1 (PosNum.bit b n) = bit (g true b) (bif g false true then Num.pos n else 0)
pb1 : ∀ (a : Bool) (m : PosNum), p (PosNum.bit a m) 1 = bit (g a true) (bif g true false then Num.pos m else 0)
pbb : ∀ (a b : Bool) (m n : PosNum), p (PosNum.bit a m) (PosNum.bit b n) = bit (g a b) (p m n)
this : ∀ (b : Bool) (n : PosNum), Eq (α := ℕ) (bif b then (↑n : ℕ) else 0) (↑(bif b then Num.pos n else 0) : ℕ)
this' : ∀ (b : Bool) (n : PosNum), (↑(Num.pos (PosNum.bit b n)) : ℕ) = Nat.bit b (↑n : ℕ)
n : PosNum
pos : (↑(p 1 (PosNum.bit false n)) : ℕ) = Nat.bit (g true false) (if g false true = true then (↑n : ℕ) else 0)
pos₁ : (↑(p 1 (PosNum.bit false n)) : ℕ) = Nat.bit (g true false) (bif g false true then (↑n : ℕ) else 0)
pos₂ : (↑(p 1 (PosNum.bit false n)) : ℕ) = Nat.bit (g true false) (↑(bif g false true then Num.pos n else 0) : ℕ)
pos₃ :
  Eq (α := ℕ) (↑(p 1 (PosNum.bit false n)) : ℕ) (↑(bit (g true false) (bif g false true then Num.pos n else 0)) : ℕ)
pos₄ pos₅ :
  Eq (α := ℕ) (↑(bit (g true false) (bif g false true then Num.pos n else 0)) : ℕ)
    (↑(bit (g true false) (bif g false true then Num.pos n else 0)) : ℕ)
⊢ (↑(p 1 (PosNum.bit false n)) : ℕ) = Nat.bit (g true false) (Nat.bitwise g 0 (↑n : ℕ))

Tactic:
rw [Nat.bitwise_zero_left, ← Bool.cond_eq_ite, this, ← bit_to_nat, p1b]

Premises used: Num.bit_to_nat, Nat.bitwise_zero_left, Bool.cond_eq_ite
-- Module: Mathlib.Data.Num.Lemmas
Goal:
f : Num → Num → Num
g : Bool → Bool → Bool
p : PosNum → PosNum → Num
gff : g false false = false
f00 : f 0 0 = 0
f0n : ∀ (n : PosNum), f 0 (Num.pos n) = bif g false true then Num.pos n else 0
fn0 : ∀ (n : PosNum), f (Num.pos n) 0 = bif g true false then Num.pos n else 0
fnn : ∀ (m n : PosNum), f (Num.pos m) (Num.pos n) = p m n
p11 : p 1 1 = bif g true true then 1 else 0
p1b : ∀ (b : Bool) (n : PosNum), p 1 (PosNum.bit b n) = bit (g true b) (bif g false true then Num.pos n else 0)
pb1 : ∀ (a : Bool) (m : PosNum), p (PosNum.bit a m) 1 = bit (g a true) (bif g true false then Num.pos m else 0)
pbb : ∀ (a b : Bool) (m n : PosNum), p (PosNum.bit a m) (PosNum.bit b n) = bit (g a b) (p m n)
this : ∀ (b : Bool) (n : PosNum), Eq (α := ℕ) (bif b then (↑n : ℕ) else 0) (↑(bif b then Num.pos n else 0) : ℕ)
this' : ∀ (b : Bool) (n : PosNum), (↑(Num.pos (PosNum.bit b n)) : ℕ) = Nat.bit b (↑n : ℕ)
m : PosNum
IH : ∀ (n : PosNum), (↑(p m n) : ℕ) = Nat.bitwise g (↑(Num.pos m) : ℕ) (↑(Num.pos n) : ℕ)
pos : (↑(p (PosNum.bit true m) 1) : ℕ) = Nat.bit (g true true) (if g true false = true then (↑m : ℕ) else 0)
pos₁ : (↑(p (PosNum.bit true m) 1) : ℕ) = Nat.bit (g true true) (bif g true false then (↑m : ℕ) else 0)
pos₂ : (↑(p (PosNum.bit true m) 1) : ℕ) = Nat.bit (g true true) (↑(bif g true false then Num.pos m else 0) : ℕ)
pos₃ : Eq (α := ℕ) (↑(p (PosNum.bit true m) 1) : ℕ) (↑(bit (g true true) (bif g true false then Num.pos m else 0)) : ℕ)
pos₄ pos₅ :
  Eq (α := ℕ) (↑(bit (g true true) (bif g true false then Num.pos m else 0)) : ℕ)
    (↑(bit (g true true) (bif g true false then Num.pos m else 0)) : ℕ)
⊢ (↑(p (PosNum.bit true m) 1) : ℕ) = Nat.bit (g true true) (Nat.bitwise g (↑m : ℕ) 0)

Tactic:
rw [Nat.bitwise_zero_right, ← Bool.cond_eq_ite, this, ← bit_to_nat, pb1]

Premises used: Num.bit_to_nat, Nat.bitwise_zero_right, Bool.cond_eq_ite
-- Module: Mathlib.Data.Num.Lemmas
Goal:
f : Num → Num → Num
g : Bool → Bool → Bool
p : PosNum → PosNum → Num
gff : g false false = false
f00 : f 0 0 = 0
f0n : ∀ (n : PosNum), f 0 (Num.pos n) = bif g false true then Num.pos n else 0
fn0 : ∀ (n : PosNum), f (Num.pos n) 0 = bif g true false then Num.pos n else 0
fnn : ∀ (m n : PosNum), f (Num.pos m) (Num.pos n) = p m n
p11 : p 1 1 = bif g true true then 1 else 0
p1b : ∀ (b : Bool) (n : PosNum), p 1 (PosNum.bit b n) = bit (g true b) (bif g false true then Num.pos n else 0)
pb1 : ∀ (a : Bool) (m : PosNum), p (PosNum.bit a m) 1 = bit (g a true) (bif g true false then Num.pos m else 0)
pbb : ∀ (a b : Bool) (m n : PosNum), p (PosNum.bit a m) (PosNum.bit b n) = bit (g a b) (p m n)
this : ∀ (b : Bool) (n : PosNum), Eq (α := ℕ) (bif b then (↑n : ℕ) else 0) (↑(bif b then Num.pos n else 0) : ℕ)
this' : ∀ (b : Bool) (n : PosNum), (↑(Num.pos (PosNum.bit b n)) : ℕ) = Nat.bit b (↑n : ℕ)
m : PosNum
IH : ∀ (n : PosNum), (↑(p m n) : ℕ) = Nat.bitwise g (↑(Num.pos m) : ℕ) (↑(Num.pos n) : ℕ)
pos : (↑(p (PosNum.bit false m) 1) : ℕ) = Nat.bit (g false true) (if g true false = true then (↑m : ℕ) else 0)
pos₁ : (↑(p (PosNum.bit false m) 1) : ℕ) = Nat.bit (g false true) (bif g true false then (↑m : ℕ) else 0)
pos₂ : (↑(p (PosNum.bit false m) 1) : ℕ) = Nat.bit (g false true) (↑(bif g true false then Num.pos m else 0) : ℕ)
pos₃ :
  Eq (α := ℕ) (↑(p (PosNum.bit false m) 1) : ℕ) (↑(bit (g false true) (bif g true false then Num.pos m else 0)) : ℕ)
pos₄ pos₅ :
  Eq (α := ℕ) (↑(bit (g false true) (bif g true false then Num.pos m else 0)) : ℕ)
    (↑(bit (g false true) (bif g true false then Num.pos m else 0)) : ℕ)
⊢ (↑(p (PosNum.bit false m) 1) : ℕ) = Nat.bit (g false true) (Nat.bitwise g (↑m : ℕ) 0)

Tactic:
rw [Nat.bitwise_zero_right, ← Bool.cond_eq_ite, this, ← bit_to_nat, pb1]

Premises used: Num.bit_to_nat, Nat.bitwise_zero_right, Bool.cond_eq_ite
-- Module: Mathlib.Data.Num.Lemmas
Goal:
f : Num → Num → Num
g : Bool → Bool → Bool
p : PosNum → PosNum → Num
gff : g false false = false
f00 : f 0 0 = 0
f0n : ∀ (n : PosNum), f 0 (Num.pos n) = bif g false true then Num.pos n else 0
fn0 : ∀ (n : PosNum), f (Num.pos n) 0 = bif g true false then Num.pos n else 0
fnn : ∀ (m n : PosNum), f (Num.pos m) (Num.pos n) = p m n
p11 : p 1 1 = bif g true true then 1 else 0
p1b : ∀ (b : Bool) (n : PosNum), p 1 (PosNum.bit b n) = bit (g true b) (bif g false true then Num.pos n else 0)
pb1 : ∀ (a : Bool) (m : PosNum), p (PosNum.bit a m) 1 = bit (g a true) (bif g true false then Num.pos m else 0)
pbb : ∀ (a b : Bool) (m n : PosNum), p (PosNum.bit a m) (PosNum.bit b n) = bit (g a b) (p m n)
this : ∀ (b : Bool) (n : PosNum), Eq (α := ℕ) (bif b then (↑n : ℕ) else 0) (↑(bif b then Num.pos n else 0) : ℕ)
this' : ∀ (b : Bool) (n : PosNum), (↑(Num.pos (PosNum.bit b n)) : ℕ) = Nat.bit b (↑n : ℕ)
m : PosNum
IH : ∀ (n : PosNum), (↑(p m n) : ℕ) = Nat.bitwise g (↑(Num.pos m) : ℕ) (↑(Num.pos n) : ℕ)
n : PosNum
pos : (↑(p (PosNum.bit true m) (PosNum.bit true n)) : ℕ) = Nat.bit (g true true) (↑(p m n) : ℕ)
⊢ (↑(p (PosNum.bit true m) (PosNum.bit true n)) : ℕ) = Nat.bit (g true true) (Nat.bitwise g (↑m : ℕ) (↑n : ℕ))

Tactic:
rw [← show ∀ n : PosNum, ↑(p m n) = Nat.bitwise g ↑m ↑n from IH]
-- Module: Mathlib.Data.Num.Lemmas
Goal:
f : Num → Num → Num
g : Bool → Bool → Bool
p : PosNum → PosNum → Num
gff : g false false = false
f00 : f 0 0 = 0
f0n : ∀ (n : PosNum), f 0 (Num.pos n) = bif g false true then Num.pos n else 0
fn0 : ∀ (n : PosNum), f (Num.pos n) 0 = bif g true false then Num.pos n else 0
fnn : ∀ (m n : PosNum), f (Num.pos m) (Num.pos n) = p m n
p11 : p 1 1 = bif g true true then 1 else 0
p1b : ∀ (b : Bool) (n : PosNum), p 1 (PosNum.bit b n) = bit (g true b) (bif g false true then Num.pos n else 0)
pb1 : ∀ (a : Bool) (m : PosNum), p (PosNum.bit a m) 1 = bit (g a true) (bif g true false then Num.pos m else 0)
pbb : ∀ (a b : Bool) (m n : PosNum), p (PosNum.bit a m) (PosNum.bit b n) = bit (g a b) (p m n)
this : ∀ (b : Bool) (n : PosNum), Eq (α := ℕ) (bif b then (↑n : ℕ) else 0) (↑(bif b then Num.pos n else 0) : ℕ)
this' : ∀ (b : Bool) (n : PosNum), (↑(Num.pos (PosNum.bit b n)) : ℕ) = Nat.bit b (↑n : ℕ)
m : PosNum
IH : ∀ (n : PosNum), (↑(p m n) : ℕ) = Nat.bitwise g (↑(Num.pos m) : ℕ) (↑(Num.pos n) : ℕ)
n : PosNum
pos : Eq (α := ℕ) (↑(p (PosNum.bit true m) (PosNum.bit true n)) : ℕ) (↑(bit (g true true) (p m n)) : ℕ)
pos₁ pos₂ : Eq (α := ℕ) (↑(bit (g true true) (p m n)) : ℕ) (↑(bit (g true true) (p m n)) : ℕ)
⊢ (↑(p (PosNum.bit true m) (PosNum.bit true n)) : ℕ) = Nat.bit (g true true) (↑(p m n) : ℕ)

Tactic:
rw [← bit_to_nat, pbb]

Premises used: Num.bit_to_nat
-- Module: Mathlib.Data.Num.Lemmas
Goal:
f : Num → Num → Num
g : Bool → Bool → Bool
p : PosNum → PosNum → Num
gff : g false false = false
f00 : f 0 0 = 0
f0n : ∀ (n : PosNum), f 0 (Num.pos n) = bif g false true then Num.pos n else 0
fn0 : ∀ (n : PosNum), f (Num.pos n) 0 = bif g true false then Num.pos n else 0
fnn : ∀ (m n : PosNum), f (Num.pos m) (Num.pos n) = p m n
p11 : p 1 1 = bif g true true then 1 else 0
p1b : ∀ (b : Bool) (n : PosNum), p 1 (PosNum.bit b n) = bit (g true b) (bif g false true then Num.pos n else 0)
pb1 : ∀ (a : Bool) (m : PosNum), p (PosNum.bit a m) 1 = bit (g a true) (bif g true false then Num.pos m else 0)
pbb : ∀ (a b : Bool) (m n : PosNum), p (PosNum.bit a m) (PosNum.bit b n) = bit (g a b) (p m n)
this : ∀ (b : Bool) (n : PosNum), Eq (α := ℕ) (bif b then (↑n : ℕ) else 0) (↑(bif b then Num.pos n else 0) : ℕ)
this' : ∀ (b : Bool) (n : PosNum), (↑(Num.pos (PosNum.bit b n)) : ℕ) = Nat.bit b (↑n : ℕ)
m : PosNum
IH : ∀ (n : PosNum), (↑(p m n) : ℕ) = Nat.bitwise g (↑(Num.pos m) : ℕ) (↑(Num.pos n) : ℕ)
n : PosNum
pos : (↑(p (PosNum.bit true m) (PosNum.bit false n)) : ℕ) = Nat.bit (g true false) (↑(p m n) : ℕ)
⊢ (↑(p (PosNum.bit true m) (PosNum.bit false n)) : ℕ) = Nat.bit (g true false) (Nat.bitwise g (↑m : ℕ) (↑n : ℕ))

Tactic:
rw [← show ∀ n : PosNum, ↑(p m n) = Nat.bitwise g ↑m ↑n from IH]
-- Module: Mathlib.Data.Num.Lemmas
Goal:
f : Num → Num → Num
g : Bool → Bool → Bool
p : PosNum → PosNum → Num
gff : g false false = false
f00 : f 0 0 = 0
f0n : ∀ (n : PosNum), f 0 (Num.pos n) = bif g false true then Num.pos n else 0
fn0 : ∀ (n : PosNum), f (Num.pos n) 0 = bif g true false then Num.pos n else 0
fnn : ∀ (m n : PosNum), f (Num.pos m) (Num.pos n) = p m n
p11 : p 1 1 = bif g true true then 1 else 0
p1b : ∀ (b : Bool) (n : PosNum), p 1 (PosNum.bit b n) = bit (g true b) (bif g false true then Num.pos n else 0)
pb1 : ∀ (a : Bool) (m : PosNum), p (PosNum.bit a m) 1 = bit (g a true) (bif g true false then Num.pos m else 0)
pbb : ∀ (a b : Bool) (m n : PosNum), p (PosNum.bit a m) (PosNum.bit b n) = bit (g a b) (p m n)
this : ∀ (b : Bool) (n : PosNum), Eq (α := ℕ) (bif b then (↑n : ℕ) else 0) (↑(bif b then Num.pos n else 0) : ℕ)
this' : ∀ (b : Bool) (n : PosNum), (↑(Num.pos (PosNum.bit b n)) : ℕ) = Nat.bit b (↑n : ℕ)
m : PosNum
IH : ∀ (n : PosNum), (↑(p m n) : ℕ) = Nat.bitwise g (↑(Num.pos m) : ℕ) (↑(Num.pos n) : ℕ)
n : PosNum
pos : Eq (α := ℕ) (↑(p (PosNum.bit true m) (PosNum.bit false n)) : ℕ) (↑(bit (g true false) (p m n)) : ℕ)
pos₁ pos₂ : Eq (α := ℕ) (↑(bit (g true false) (p m n)) : ℕ) (↑(bit (g true false) (p m n)) : ℕ)
⊢ (↑(p (PosNum.bit true m) (PosNum.bit false n)) : ℕ) = Nat.bit (g true false) (↑(p m n) : ℕ)

Tactic:
rw [← bit_to_nat, pbb]

Premises used: Num.bit_to_nat
-- Module: Mathlib.Data.Num.Lemmas
Goal:
f : Num → Num → Num
g : Bool → Bool → Bool
p : PosNum → PosNum → Num
gff : g false false = false
f00 : f 0 0 = 0
f0n : ∀ (n : PosNum), f 0 (Num.pos n) = bif g false true then Num.pos n else 0
fn0 : ∀ (n : PosNum), f (Num.pos n) 0 = bif g true false then Num.pos n else 0
fnn : ∀ (m n : PosNum), f (Num.pos m) (Num.pos n) = p m n
p11 : p 1 1 = bif g true true then 1 else 0
p1b : ∀ (b : Bool) (n : PosNum), p 1 (PosNum.bit b n) = bit (g true b) (bif g false true then Num.pos n else 0)
pb1 : ∀ (a : Bool) (m : PosNum), p (PosNum.bit a m) 1 = bit (g a true) (bif g true false then Num.pos m else 0)
pbb : ∀ (a b : Bool) (m n : PosNum), p (PosNum.bit a m) (PosNum.bit b n) = bit (g a b) (p m n)
this : ∀ (b : Bool) (n : PosNum), Eq (α := ℕ) (bif b then (↑n : ℕ) else 0) (↑(bif b then Num.pos n else 0) : ℕ)
this' : ∀ (b : Bool) (n : PosNum), (↑(Num.pos (PosNum.bit b n)) : ℕ) = Nat.bit b (↑n : ℕ)
m : PosNum
IH : ∀ (n : PosNum), (↑(p m n) : ℕ) = Nat.bitwise g (↑(Num.pos m) : ℕ) (↑(Num.pos n) : ℕ)
n : PosNum
pos : (↑(p (PosNum.bit false m) (PosNum.bit true n)) : ℕ) = Nat.bit (g false true) (↑(p m n) : ℕ)
⊢ (↑(p (PosNum.bit false m) (PosNum.bit true n)) : ℕ) = Nat.bit (g false true) (Nat.bitwise g (↑m : ℕ) (↑n : ℕ))

Tactic:
rw [← show ∀ n : PosNum, ↑(p m n) = Nat.bitwise g ↑m ↑n from IH]
-- Module: Mathlib.Data.Num.Lemmas
Goal:
f : Num → Num → Num
g : Bool → Bool → Bool
p : PosNum → PosNum → Num
gff : g false false = false
f00 : f 0 0 = 0
f0n : ∀ (n : PosNum), f 0 (Num.pos n) = bif g false true then Num.pos n else 0
fn0 : ∀ (n : PosNum), f (Num.pos n) 0 = bif g true false then Num.pos n else 0
fnn : ∀ (m n : PosNum), f (Num.pos m) (Num.pos n) = p m n
p11 : p 1 1 = bif g true true then 1 else 0
p1b : ∀ (b : Bool) (n : PosNum), p 1 (PosNum.bit b n) = bit (g true b) (bif g false true then Num.pos n else 0)
pb1 : ∀ (a : Bool) (m : PosNum), p (PosNum.bit a m) 1 = bit (g a true) (bif g true false then Num.pos m else 0)
pbb : ∀ (a b : Bool) (m n : PosNum), p (PosNum.bit a m) (PosNum.bit b n) = bit (g a b) (p m n)
this : ∀ (b : Bool) (n : PosNum), Eq (α := ℕ) (bif b then (↑n : ℕ) else 0) (↑(bif b then Num.pos n else 0) : ℕ)
this' : ∀ (b : Bool) (n : PosNum), (↑(Num.pos (PosNum.bit b n)) : ℕ) = Nat.bit b (↑n : ℕ)
m : PosNum
IH : ∀ (n : PosNum), (↑(p m n) : ℕ) = Nat.bitwise g (↑(Num.pos m) : ℕ) (↑(Num.pos n) : ℕ)
n : PosNum
pos : Eq (α := ℕ) (↑(p (PosNum.bit false m) (PosNum.bit true n)) : ℕ) (↑(bit (g false true) (p m n)) : ℕ)
pos₁ pos₂ : Eq (α := ℕ) (↑(bit (g false true) (p m n)) : ℕ) (↑(bit (g false true) (p m n)) : ℕ)
⊢ (↑(p (PosNum.bit false m) (PosNum.bit true n)) : ℕ) = Nat.bit (g false true) (↑(p m n) : ℕ)

Tactic:
rw [← bit_to_nat, pbb]

Premises used: Num.bit_to_nat
-- Module: Mathlib.Data.Num.Lemmas
Goal:
f : Num → Num → Num
g : Bool → Bool → Bool
p : PosNum → PosNum → Num
gff : g false false = false
f00 : f 0 0 = 0
f0n : ∀ (n : PosNum), f 0 (Num.pos n) = bif g false true then Num.pos n else 0
fn0 : ∀ (n : PosNum), f (Num.pos n) 0 = bif g true false then Num.pos n else 0
fnn : ∀ (m n : PosNum), f (Num.pos m) (Num.pos n) = p m n
p11 : p 1 1 = bif g true true then 1 else 0
p1b : ∀ (b : Bool) (n : PosNum), p 1 (PosNum.bit b n) = bit (g true b) (bif g false true then Num.pos n else 0)
pb1 : ∀ (a : Bool) (m : PosNum), p (PosNum.bit a m) 1 = bit (g a true) (bif g true false then Num.pos m else 0)
pbb : ∀ (a b : Bool) (m n : PosNum), p (PosNum.bit a m) (PosNum.bit b n) = bit (g a b) (p m n)
this : ∀ (b : Bool) (n : PosNum), Eq (α := ℕ) (bif b then (↑n : ℕ) else 0) (↑(bif b then Num.pos n else 0) : ℕ)
this' : ∀ (b : Bool) (n : PosNum), (↑(Num.pos (PosNum.bit b n)) : ℕ) = Nat.bit b (↑n : ℕ)
m : PosNum
IH : ∀ (n : PosNum), (↑(p m n) : ℕ) = Nat.bitwise g (↑(Num.pos m) : ℕ) (↑(Num.pos n) : ℕ)
n : PosNum
pos : (↑(p (PosNum.bit false m) (PosNum.bit false n)) : ℕ) = Nat.bit (g false false) (↑(p m n) : ℕ)
⊢ (↑(p (PosNum.bit false m) (PosNum.bit false n)) : ℕ) = Nat.bit (g false false) (Nat.bitwise g (↑m : ℕ) (↑n : ℕ))

Tactic:
rw [← show ∀ n : PosNum, ↑(p m n) = Nat.bitwise g ↑m ↑n from IH]
-- Module: Mathlib.Data.Num.Lemmas
Goal:
f : Num → Num → Num
g : Bool → Bool → Bool
p : PosNum → PosNum → Num
gff : g false false = false
f00 : f 0 0 = 0
f0n : ∀ (n : PosNum), f 0 (Num.pos n) = bif g false true then Num.pos n else 0
fn0 : ∀ (n : PosNum), f (Num.pos n) 0 = bif g true false then Num.pos n else 0
fnn : ∀ (m n : PosNum), f (Num.pos m) (Num.pos n) = p m n
p11 : p 1 1 = bif g true true then 1 else 0
p1b : ∀ (b : Bool) (n : PosNum), p 1 (PosNum.bit b n) = bit (g true b) (bif g false true then Num.pos n else 0)
pb1 : ∀ (a : Bool) (m : PosNum), p (PosNum.bit a m) 1 = bit (g a true) (bif g true false then Num.pos m else 0)
pbb : ∀ (a b : Bool) (m n : PosNum), p (PosNum.bit a m) (PosNum.bit b n) = bit (g a b) (p m n)
this : ∀ (b : Bool) (n : PosNum), Eq (α := ℕ) (bif b then (↑n : ℕ) else 0) (↑(bif b then Num.pos n else 0) : ℕ)
this' : ∀ (b : Bool) (n : PosNum), (↑(Num.pos (PosNum.bit b n)) : ℕ) = Nat.bit b (↑n : ℕ)
m : PosNum
IH : ∀ (n : PosNum), (↑(p m n) : ℕ) = Nat.bitwise g (↑(Num.pos m) : ℕ) (↑(Num.pos n) : ℕ)
n : PosNum
pos : Eq (α := ℕ) (↑(p (PosNum.bit false m) (PosNum.bit false n)) : ℕ) (↑(bit (g false false) (p m n)) : ℕ)
pos₁ pos₂ : Eq (α := ℕ) (↑(bit (g false false) (p m n)) : ℕ) (↑(bit (g false false) (p m n)) : ℕ)
⊢ (↑(p (PosNum.bit false m) (PosNum.bit false n)) : ℕ) = Nat.bit (g false false) (↑(p m n) : ℕ)

Tactic:
rw [← bit_to_nat, pbb]

Premises used: Num.bit_to_nat
-- Module: Mathlib.Data.Num.Lemmas
Goal:
gff : (false || false) = false
f00 : HOr.hOr (α := 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 = pos (m.lor n)
p11 : pos (lor 1 1) = bif true || true then 1 else 0
p1b : ∀ (b : Bool) (n : PosNum), pos (lor 1 (PosNum.bit b n)) = bit (true || b) (bif false || true then pos n else 0)
pb1 : ∀ (a : Bool) (m : PosNum), pos ((PosNum.bit a m).lor 1) = bit (a || true) (bif true || false then pos m else 0)
pbb : ∀ (a b : Bool) (m n : PosNum), pos ((PosNum.bit a m).lor (PosNum.bit b n)) = bit (a || b) (pos (m.lor n))
⊢ ∀ (m n : Num), (↑(m ||| n) : ℕ) = HOr.hOr (α := ℕ) (↑m : ℕ) (↑n : ℕ)

Tactic:
apply castNum_eq_bitwise fun x y => pos (PosNum.lor x y)

Premises used: Num.castNum_eq_bitwise, PosNum.lor, Num.pos
-- Module: Mathlib.Data.Num.Lemmas
Goal:
f0n : 0 ||| pos one = bif false || true then pos one else 0
f0n₁ : ∀ (a : PosNum), 0 ||| pos a.bit1 = bif false || true then pos a.bit1 else 0
f0n₂ : ∀ (a : PosNum), 0 ||| pos a.bit0 = bif false || true then pos a.bit0 else 0
⊢ ∀ (n : PosNum), 0 ||| pos n = bif false || true then pos n else 0

Tactic:
try rintro (_ | _)
-- Module: Mathlib.Data.Num.Lemmas
Goal:
fn0 : pos one ||| 0 = bif true || false then pos one else 0
fn0₁ : ∀ (a : PosNum), pos a.bit1 ||| 0 = bif true || false then pos a.bit1 else 0
fn0₂ : ∀ (a : PosNum), pos a.bit0 ||| 0 = bif true || false then pos a.bit0 else 0
⊢ ∀ (n : PosNum), pos n ||| 0 = bif true || false then pos n else 0

Tactic:
try rintro (_ | _)
-- Module: Mathlib.Data.Num.Lemmas
Goal:
fnn : ∀ (n : PosNum), pos one ||| pos n = pos (one.lor n)
fnn₁ : ∀ (a n : PosNum), pos a.bit1 ||| pos n = pos (a.bit1.lor n)
fnn₂ : ∀ (a n : PosNum), pos a.bit0 ||| pos n = pos (a.bit0.lor n)
⊢ ∀ (m n : PosNum), pos m ||| pos n = pos (m.lor n)

Tactic:
try rintro (_ | _)
-- Module: Mathlib.Data.Num.Lemmas
Goal:
p1b : ∀ (n : PosNum), pos (lor 1 (PosNum.bit false n)) = bit (true || false) (bif false || true then pos n else 0)
p1b₁ : ∀ (n : PosNum), pos (lor 1 (PosNum.bit true n)) = bit (true || true) (bif false || true then pos n else 0)
⊢ ∀ (b : Bool) (n : PosNum), pos (lor 1 (PosNum.bit b n)) = bit (true || b) (bif false || true then pos n else 0)

Tactic:
try rintro (_ | _)
-- Module: Mathlib.Data.Num.Lemmas
Goal:
pb1 : ∀ (m : PosNum), pos ((PosNum.bit false m).lor 1) = bit (false || true) (bif true || false then pos m else 0)
pb1₁ : ∀ (m : PosNum), pos ((PosNum.bit true m).lor 1) = bit (true || true) (bif true || false then pos m else 0)
⊢ ∀ (a : Bool) (m : PosNum), pos ((PosNum.bit a m).lor 1) = bit (a || true) (bif true || false then pos m else 0)

Tactic:
try rintro (_ | _)
-- Module: Mathlib.Data.Num.Lemmas
Goal:
pbb : ∀ (b : Bool) (m n : PosNum), pos ((PosNum.bit false m).lor (PosNum.bit b n)) = bit (false || b) (pos (m.lor n))
pbb₁ : ∀ (b : Bool) (m n : PosNum), pos ((PosNum.bit true m).lor (PosNum.bit b n)) = bit (true || b) (pos (m.lor n))
⊢ ∀ (a b : Bool) (m n : PosNum), pos ((PosNum.bit a m).lor (PosNum.bit b n)) = bit (a || b) (pos (m.lor n))

Tactic:
try rintro (_ | _)
-- Module: Mathlib.Data.Num.Lemmas
Goal:
fnn : pos one ||| pos one = pos (one.lor one)
fnn₁ : ∀ (a : PosNum), pos one ||| pos a.bit1 = pos (one.lor a.bit1)
fnn₂ : ∀ (a : PosNum), pos one ||| pos a.bit0 = pos (one.lor a.bit0)
⊢ ∀ (n : PosNum), pos one ||| pos n = pos (one.lor n)

Tactic:
try rintro (_ | _)
-- Module: Mathlib.Data.Num.Lemmas
Goal:
a : PosNum
fnn : pos a.bit1 ||| pos one = pos (a.bit1.lor one)
fnn₁ : ∀ (a_1 : PosNum), pos a.bit1 ||| pos a_1.bit1 = pos (a.bit1.lor a_1.bit1)
fnn₂ : ∀ (a_1 : PosNum), pos a.bit1 ||| pos a_1.bit0 = pos (a.bit1.lor a_1.bit0)
⊢ ∀ (n : PosNum), pos a.bit1 ||| pos n = pos (a.bit1.lor n)

Tactic:
try rintro (_ | _)
-- Module: Mathlib.Data.Num.Lemmas
Goal:
a : PosNum
fnn : pos a.bit0 ||| pos one = pos (a.bit0.lor one)
fnn₁ : ∀ (a_1 : PosNum), pos a.bit0 ||| pos a_1.bit1 = pos (a.bit0.lor a_1.bit1)
fnn₂ : ∀ (a_1 : PosNum), pos a.bit0 ||| pos a_1.bit0 = pos (a.bit0.lor a_1.bit0)
⊢ ∀ (n : PosNum), pos a.bit0 ||| pos n = pos (a.bit0.lor n)

Tactic:
try rintro (_ | _)
-- Module: Mathlib.Data.Num.Lemmas
Goal:
p1b : pos (lor 1 (PosNum.bit false one)) = bit (true || false) (bif false || true then pos one else 0)
p1b₁ :
  ∀ (a : PosNum), pos (lor 1 (PosNum.bit false a.bit1)) = bit (true || false) (bif false || true then pos a.bit1 else 0)
p1b₂ :
  ∀ (a : PosNum), pos (lor 1 (PosNum.bit false a.bit0)) = bit (true || false) (bif false || true then pos a.bit0 else 0)
⊢ ∀ (n : PosNum), pos (lor 1 (PosNum.bit false n)) = bit (true || false) (bif false || true then pos n else 0)

Tactic:
try rintro (_ | _)
-- Module: Mathlib.Data.Num.Lemmas
Goal:
p1b : pos (lor 1 (PosNum.bit true one)) = bit (true || true) (bif false || true then pos one else 0)
p1b₁ :
  ∀ (a : PosNum), pos (lor 1 (PosNum.bit true a.bit1)) = bit (true || true) (bif false || true then pos a.bit1 else 0)
p1b₂ :
  ∀ (a : PosNum), pos (lor 1 (PosNum.bit true a.bit0)) = bit (true || true) (bif false || true then pos a.bit0 else 0)
⊢ ∀ (n : PosNum), pos (lor 1 (PosNum.bit true n)) = bit (true || true) (bif false || true then pos n else 0)

Tactic:
try rintro (_ | _)
-- Module: Mathlib.Data.Num.Lemmas
Goal:
pb1 : pos ((PosNum.bit false one).lor 1) = bit (false || true) (bif true || false then pos one else 0)
pb1₁ :
  ∀ (a : PosNum), pos ((PosNum.bit false a.bit1).lor 1) = bit (false || true) (bif true || false then pos a.bit1 else 0)
pb1₂ :
  ∀ (a : PosNum), pos ((PosNum.bit false a.bit0).lor 1) = bit (false || true) (bif true || false then pos a.bit0 else 0)
⊢ ∀ (m : PosNum), pos ((PosNum.bit false m).lor 1) = bit (false || true) (bif true || false then pos m else 0)

Tactic:
try rintro (_ | _)