awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
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 (pos n) = bif g false true then pos n else 0
fn0 : ∀ (n : PosNum), f (pos n) 0 = bif g true false then pos n else 0
fnn : ∀ (m n : PosNum), f (pos m) (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 pos n else 0)
pb1 : ∀ (a : Bool) (m : PosNum), p (PosNum.bit a m) 1 = bit (g a true) (bif g true false then 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 pos n else 0) : ℕ)
this' : ∀ (b : Bool) (n : PosNum), (↑(pos (PosNum.bit b n)) : ℕ) = Nat.bit b (↑n : ℕ)
m : PosNum
IH : ∀ (n : PosNum), (↑(p m n) : ℕ) = Nat.bitwise g (↑(pos m) : ℕ) (↑(pos n) : ℕ)
⊢ (↑(p (PosNum.bit true m) 1) : ℕ) = Nat.bitwise g (↑(pos (PosNum.bit true m)) : ℕ) (Nat.bit true 0)
have pos : (↑(p (PosNum.bit true m) 1) : ℕ) = Nat.bitwise g (Nat.bit true (↑m : ℕ)) (Nat.bit true 0)
Tactic: repeat rw [this']
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
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 (pos n) = bif g false true then pos n else 0
fn0 : ∀ (n : PosNum), f (pos n) 0 = bif g true false then pos n else 0
fnn : ∀ (m n : PosNum), f (pos m) (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 pos n else 0)
pb1 : ∀ (a : Bool) (m : PosNum), p (PosNum.bit a m) 1 = bit (g a true) (bif g true false then 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 pos n else 0) : ℕ)
this' : ∀ (b : Bool) (n : PosNum), (↑(pos (PosNum.bit b n)) : ℕ) = Nat.bit b (↑n : ℕ)
m : PosNum
IH : ∀ (n : PosNum), (↑(p m n) : ℕ) = Nat.bitwise g (↑(pos m) : ℕ) (↑(pos n) : ℕ)
⊢ (↑(p (PosNum.bit true m) 1) : ℕ) = Nat.bitwise g (Nat.bit true (↑m : ℕ)) (Nat.bit true 0)
have pos : (↑(p (PosNum.bit true m) 1) : ℕ) = Nat.bit (g true true) (Nat.bitwise g (↑m : ℕ) 0)
Tactic: rw [Nat.bitwise_bit gff]
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
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 (pos n) = bif g false true then pos n else 0
fn0 : ∀ (n : PosNum), f (pos n) 0 = bif g true false then pos n else 0
fnn : ∀ (m n : PosNum), f (pos m) (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 pos n else 0)
pb1 : ∀ (a : Bool) (m : PosNum), p (PosNum.bit a m) 1 = bit (g a true) (bif g true false then 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 pos n else 0) : ℕ)
this' : ∀ (b : Bool) (n : PosNum), (↑(pos (PosNum.bit b n)) : ℕ) = Nat.bit b (↑n : ℕ)
m : PosNum
IH : ∀ (n : PosNum), (↑(p m n) : ℕ) = Nat.bitwise g (↑(pos m) : ℕ) (↑(pos n) : ℕ)
n : PosNum
⊢ (↑(p (PosNum.bit true m) (PosNum.bit true n)) : ℕ) =
    Nat.bitwise g (↑(pos (PosNum.bit true m)) : ℕ) (↑(pos (PosNum.bit true n)) : ℕ)
have pos : (↑(p (PosNum.bit true m) (PosNum.bit true n)) : ℕ) =
  Nat.bitwise g (Nat.bit true (↑m : ℕ)) (↑(pos (PosNum.bit true n)) : ℕ)
Tactic: rw [this']
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
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 (pos n) = bif g false true then pos n else 0
fn0 : ∀ (n : PosNum), f (pos n) 0 = bif g true false then pos n else 0
fnn : ∀ (m n : PosNum), f (pos m) (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 pos n else 0)
pb1 : ∀ (a : Bool) (m : PosNum), p (PosNum.bit a m) 1 = bit (g a true) (bif g true false then 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 pos n else 0) : ℕ)
this' : ∀ (b : Bool) (n : PosNum), (↑(pos (PosNum.bit b n)) : ℕ) = Nat.bit b (↑n : ℕ)
m : PosNum
IH : ∀ (n : PosNum), (↑(p m n) : ℕ) = Nat.bitwise g (↑(pos m) : ℕ) (↑(pos n) : ℕ)
n : PosNum
⊢ (↑(p (PosNum.bit true m) (PosNum.bit true n)) : ℕ) =
    Nat.bitwise g (Nat.bit true (↑m : ℕ)) (↑(pos (PosNum.bit true n)) : ℕ)
have pos : (↑(p (PosNum.bit true m) (PosNum.bit true n)) : ℕ) = Nat.bitwise g (Nat.bit true (↑m : ℕ)) (Nat.bit true (↑n : ℕ))
Tactic: rw [this']
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
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 (pos n) = bif g false true then pos n else 0
fn0 : ∀ (n : PosNum), f (pos n) 0 = bif g true false then pos n else 0
fnn : ∀ (m n : PosNum), f (pos m) (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 pos n else 0)
pb1 : ∀ (a : Bool) (m : PosNum), p (PosNum.bit a m) 1 = bit (g a true) (bif g true false then 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 pos n else 0) : ℕ)
this' : ∀ (b : Bool) (n : PosNum), (↑(pos (PosNum.bit b n)) : ℕ) = Nat.bit b (↑n : ℕ)
m : PosNum
IH : ∀ (n : PosNum), (↑(p m n) : ℕ) = Nat.bitwise g (↑(pos m) : ℕ) (↑(pos n) : ℕ)
n : PosNum
⊢ (↑(p (PosNum.bit true m) (PosNum.bit true n)) : ℕ) =
    Nat.bitwise g (↑(pos (PosNum.bit true m)) : ℕ) (↑(pos (PosNum.bit true n)) : ℕ)
have pos : (↑(p (PosNum.bit true m) (PosNum.bit true n)) : ℕ) = Nat.bitwise g (Nat.bit true (↑m : ℕ)) (Nat.bit true (↑n : ℕ))
Tactic: repeat rw [this']
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
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 (pos n) = bif g false true then pos n else 0
fn0 : ∀ (n : PosNum), f (pos n) 0 = bif g true false then pos n else 0
fnn : ∀ (m n : PosNum), f (pos m) (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 pos n else 0)
pb1 : ∀ (a : Bool) (m : PosNum), p (PosNum.bit a m) 1 = bit (g a true) (bif g true false then 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 pos n else 0) : ℕ)
this' : ∀ (b : Bool) (n : PosNum), (↑(pos (PosNum.bit b n)) : ℕ) = Nat.bit b (↑n : ℕ)
m : PosNum
IH : ∀ (n : PosNum), (↑(p m n) : ℕ) = Nat.bitwise g (↑(pos m) : ℕ) (↑(pos n) : ℕ)
n : PosNum
⊢ (↑(p (PosNum.bit true m) (PosNum.bit true n)) : ℕ) = Nat.bitwise g (Nat.bit true (↑m : ℕ)) (Nat.bit true (↑n : ℕ))
have pos : (↑(p (PosNum.bit true m) (PosNum.bit true n)) : ℕ) = Nat.bit (g true true) (Nat.bitwise g (↑m : ℕ) (↑n : ℕ))
Tactic: rw [Nat.bitwise_bit gff]
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
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 (pos n) = bif g false true then pos n else 0
fn0 : ∀ (n : PosNum), f (pos n) 0 = bif g true false then pos n else 0
fnn : ∀ (m n : PosNum), f (pos m) (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 pos n else 0)
pb1 : ∀ (a : Bool) (m : PosNum), p (PosNum.bit a m) 1 = bit (g a true) (bif g true false then 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 pos n else 0) : ℕ)
this' : ∀ (b : Bool) (n : PosNum), (↑(pos (PosNum.bit b n)) : ℕ) = Nat.bit b (↑n : ℕ)
m : PosNum
IH : ∀ (n : PosNum), (↑(p m n) : ℕ) = Nat.bitwise g (↑(pos m) : ℕ) (↑(pos n) : ℕ)
n : PosNum
⊢ (↑(p (PosNum.bit true m) (PosNum.bit false n)) : ℕ) =
    Nat.bitwise g (↑(pos (PosNum.bit true m)) : ℕ) (↑(pos (PosNum.bit false n)) : ℕ)
have pos : (↑(p (PosNum.bit true m) (PosNum.bit false n)) : ℕ) =
  Nat.bitwise g (Nat.bit true (↑m : ℕ)) (↑(pos (PosNum.bit false n)) : ℕ)
Tactic: rw [this']
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
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 (pos n) = bif g false true then pos n else 0
fn0 : ∀ (n : PosNum), f (pos n) 0 = bif g true false then pos n else 0
fnn : ∀ (m n : PosNum), f (pos m) (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 pos n else 0)
pb1 : ∀ (a : Bool) (m : PosNum), p (PosNum.bit a m) 1 = bit (g a true) (bif g true false then 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 pos n else 0) : ℕ)
this' : ∀ (b : Bool) (n : PosNum), (↑(pos (PosNum.bit b n)) : ℕ) = Nat.bit b (↑n : ℕ)
m : PosNum
IH : ∀ (n : PosNum), (↑(p m n) : ℕ) = Nat.bitwise g (↑(pos m) : ℕ) (↑(pos n) : ℕ)
n : PosNum
⊢ (↑(p (PosNum.bit true m) (PosNum.bit false n)) : ℕ) =
    Nat.bitwise g (Nat.bit true (↑m : ℕ)) (↑(pos (PosNum.bit false n)) : ℕ)
have pos : (↑(p (PosNum.bit true m) (PosNum.bit false n)) : ℕ) = Nat.bitwise g (Nat.bit true (↑m : ℕ)) (Nat.bit false (↑n : ℕ))
Tactic: rw [this']
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
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 (pos n) = bif g false true then pos n else 0
fn0 : ∀ (n : PosNum), f (pos n) 0 = bif g true false then pos n else 0
fnn : ∀ (m n : PosNum), f (pos m) (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 pos n else 0)
pb1 : ∀ (a : Bool) (m : PosNum), p (PosNum.bit a m) 1 = bit (g a true) (bif g true false then 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 pos n else 0) : ℕ)
this' : ∀ (b : Bool) (n : PosNum), (↑(pos (PosNum.bit b n)) : ℕ) = Nat.bit b (↑n : ℕ)
m : PosNum
IH : ∀ (n : PosNum), (↑(p m n) : ℕ) = Nat.bitwise g (↑(pos m) : ℕ) (↑(pos n) : ℕ)
n : PosNum
⊢ (↑(p (PosNum.bit true m) (PosNum.bit false n)) : ℕ) =
    Nat.bitwise g (↑(pos (PosNum.bit true m)) : ℕ) (↑(pos (PosNum.bit false n)) : ℕ)
have pos : (↑(p (PosNum.bit true m) (PosNum.bit false n)) : ℕ) = Nat.bitwise g (Nat.bit true (↑m : ℕ)) (Nat.bit false (↑n : ℕ))
Tactic: repeat rw [this']
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
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 (pos n) = bif g false true then pos n else 0
fn0 : ∀ (n : PosNum), f (pos n) 0 = bif g true false then pos n else 0
fnn : ∀ (m n : PosNum), f (pos m) (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 pos n else 0)
pb1 : ∀ (a : Bool) (m : PosNum), p (PosNum.bit a m) 1 = bit (g a true) (bif g true false then 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 pos n else 0) : ℕ)
this' : ∀ (b : Bool) (n : PosNum), (↑(pos (PosNum.bit b n)) : ℕ) = Nat.bit b (↑n : ℕ)
m : PosNum
IH : ∀ (n : PosNum), (↑(p m n) : ℕ) = Nat.bitwise g (↑(pos m) : ℕ) (↑(pos n) : ℕ)
n : PosNum
⊢ (↑(p (PosNum.bit true m) (PosNum.bit false n)) : ℕ) = Nat.bitwise g (Nat.bit true (↑m : ℕ)) (Nat.bit false (↑n : ℕ))
have pos : (↑(p (PosNum.bit true m) (PosNum.bit false n)) : ℕ) = Nat.bit (g true false) (Nat.bitwise g (↑m : ℕ) (↑n : ℕ))
Tactic: rw [Nat.bitwise_bit gff]
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
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 (pos n) = bif g false true then pos n else 0
fn0 : ∀ (n : PosNum), f (pos n) 0 = bif g true false then pos n else 0
fnn : ∀ (m n : PosNum), f (pos m) (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 pos n else 0)
pb1 : ∀ (a : Bool) (m : PosNum), p (PosNum.bit a m) 1 = bit (g a true) (bif g true false then 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 pos n else 0) : ℕ)
this' : ∀ (b : Bool) (n : PosNum), (↑(pos (PosNum.bit b n)) : ℕ) = Nat.bit b (↑n : ℕ)
m : PosNum
IH : ∀ (n : PosNum), (↑(p m n) : ℕ) = Nat.bitwise g (↑(pos m) : ℕ) (↑(pos n) : ℕ)
⊢ (↑(p (PosNum.bit false m) 1) : ℕ) = Nat.bitwise g (↑(pos (PosNum.bit false m)) : ℕ) (Nat.bit true 0)
have pos : (↑(p (PosNum.bit false m) 1) : ℕ) = Nat.bitwise g (Nat.bit false (↑m : ℕ)) (Nat.bit true 0)
Tactic: rw [this']
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
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 (pos n) = bif g false true then pos n else 0
fn0 : ∀ (n : PosNum), f (pos n) 0 = bif g true false then pos n else 0
fnn : ∀ (m n : PosNum), f (pos m) (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 pos n else 0)
pb1 : ∀ (a : Bool) (m : PosNum), p (PosNum.bit a m) 1 = bit (g a true) (bif g true false then 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 pos n else 0) : ℕ)
this' : ∀ (b : Bool) (n : PosNum), (↑(pos (PosNum.bit b n)) : ℕ) = Nat.bit b (↑n : ℕ)
m : PosNum
IH : ∀ (n : PosNum), (↑(p m n) : ℕ) = Nat.bitwise g (↑(pos m) : ℕ) (↑(pos n) : ℕ)
⊢ (↑(p (PosNum.bit false m) 1) : ℕ) = Nat.bitwise g (↑(pos (PosNum.bit false m)) : ℕ) (Nat.bit true 0)
have pos : (↑(p (PosNum.bit false m) 1) : ℕ) = Nat.bitwise g (Nat.bit false (↑m : ℕ)) (Nat.bit true 0)
Tactic: repeat rw [this']
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
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 (pos n) = bif g false true then pos n else 0
fn0 : ∀ (n : PosNum), f (pos n) 0 = bif g true false then pos n else 0
fnn : ∀ (m n : PosNum), f (pos m) (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 pos n else 0)
pb1 : ∀ (a : Bool) (m : PosNum), p (PosNum.bit a m) 1 = bit (g a true) (bif g true false then 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 pos n else 0) : ℕ)
this' : ∀ (b : Bool) (n : PosNum), (↑(pos (PosNum.bit b n)) : ℕ) = Nat.bit b (↑n : ℕ)
m : PosNum
IH : ∀ (n : PosNum), (↑(p m n) : ℕ) = Nat.bitwise g (↑(pos m) : ℕ) (↑(pos n) : ℕ)
⊢ (↑(p (PosNum.bit false m) 1) : ℕ) = Nat.bitwise g (Nat.bit false (↑m : ℕ)) (Nat.bit true 0)
have pos : (↑(p (PosNum.bit false m) 1) : ℕ) = Nat.bit (g false true) (Nat.bitwise g (↑m : ℕ) 0)
Tactic: rw [Nat.bitwise_bit gff]
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
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 (pos n) = bif g false true then pos n else 0
fn0 : ∀ (n : PosNum), f (pos n) 0 = bif g true false then pos n else 0
fnn : ∀ (m n : PosNum), f (pos m) (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 pos n else 0)
pb1 : ∀ (a : Bool) (m : PosNum), p (PosNum.bit a m) 1 = bit (g a true) (bif g true false then 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 pos n else 0) : ℕ)
this' : ∀ (b : Bool) (n : PosNum), (↑(pos (PosNum.bit b n)) : ℕ) = Nat.bit b (↑n : ℕ)
m : PosNum
IH : ∀ (n : PosNum), (↑(p m n) : ℕ) = Nat.bitwise g (↑(pos m) : ℕ) (↑(pos n) : ℕ)
n : PosNum
⊢ (↑(p (PosNum.bit false m) (PosNum.bit true n)) : ℕ) =
    Nat.bitwise g (↑(pos (PosNum.bit false m)) : ℕ) (↑(pos (PosNum.bit true n)) : ℕ)
have pos : (↑(p (PosNum.bit false m) (PosNum.bit true n)) : ℕ) =
  Nat.bitwise g (Nat.bit false (↑m : ℕ)) (↑(pos (PosNum.bit true n)) : ℕ)
Tactic: rw [this']
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
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 (pos n) = bif g false true then pos n else 0
fn0 : ∀ (n : PosNum), f (pos n) 0 = bif g true false then pos n else 0
fnn : ∀ (m n : PosNum), f (pos m) (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 pos n else 0)
pb1 : ∀ (a : Bool) (m : PosNum), p (PosNum.bit a m) 1 = bit (g a true) (bif g true false then 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 pos n else 0) : ℕ)
this' : ∀ (b : Bool) (n : PosNum), (↑(pos (PosNum.bit b n)) : ℕ) = Nat.bit b (↑n : ℕ)
m : PosNum
IH : ∀ (n : PosNum), (↑(p m n) : ℕ) = Nat.bitwise g (↑(pos m) : ℕ) (↑(pos n) : ℕ)
n : PosNum
⊢ (↑(p (PosNum.bit false m) (PosNum.bit true n)) : ℕ) =
    Nat.bitwise g (Nat.bit false (↑m : ℕ)) (↑(pos (PosNum.bit true n)) : ℕ)
have pos : (↑(p (PosNum.bit false m) (PosNum.bit true n)) : ℕ) = Nat.bitwise g (Nat.bit false (↑m : ℕ)) (Nat.bit true (↑n : ℕ))
Tactic: rw [this']
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
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 (pos n) = bif g false true then pos n else 0
fn0 : ∀ (n : PosNum), f (pos n) 0 = bif g true false then pos n else 0
fnn : ∀ (m n : PosNum), f (pos m) (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 pos n else 0)
pb1 : ∀ (a : Bool) (m : PosNum), p (PosNum.bit a m) 1 = bit (g a true) (bif g true false then 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 pos n else 0) : ℕ)
this' : ∀ (b : Bool) (n : PosNum), (↑(pos (PosNum.bit b n)) : ℕ) = Nat.bit b (↑n : ℕ)
m : PosNum
IH : ∀ (n : PosNum), (↑(p m n) : ℕ) = Nat.bitwise g (↑(pos m) : ℕ) (↑(pos n) : ℕ)
n : PosNum
⊢ (↑(p (PosNum.bit false m) (PosNum.bit true n)) : ℕ) =
    Nat.bitwise g (↑(pos (PosNum.bit false m)) : ℕ) (↑(pos (PosNum.bit true n)) : ℕ)
have pos : (↑(p (PosNum.bit false m) (PosNum.bit true n)) : ℕ) = Nat.bitwise g (Nat.bit false (↑m : ℕ)) (Nat.bit true (↑n : ℕ))
Tactic: repeat rw [this']
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
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 (pos n) = bif g false true then pos n else 0
fn0 : ∀ (n : PosNum), f (pos n) 0 = bif g true false then pos n else 0
fnn : ∀ (m n : PosNum), f (pos m) (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 pos n else 0)
pb1 : ∀ (a : Bool) (m : PosNum), p (PosNum.bit a m) 1 = bit (g a true) (bif g true false then 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 pos n else 0) : ℕ)
this' : ∀ (b : Bool) (n : PosNum), (↑(pos (PosNum.bit b n)) : ℕ) = Nat.bit b (↑n : ℕ)
m : PosNum
IH : ∀ (n : PosNum), (↑(p m n) : ℕ) = Nat.bitwise g (↑(pos m) : ℕ) (↑(pos n) : ℕ)
n : PosNum
⊢ (↑(p (PosNum.bit false m) (PosNum.bit true n)) : ℕ) = Nat.bitwise g (Nat.bit false (↑m : ℕ)) (Nat.bit true (↑n : ℕ))
have pos : (↑(p (PosNum.bit false m) (PosNum.bit true n)) : ℕ) = Nat.bit (g false true) (Nat.bitwise g (↑m : ℕ) (↑n : ℕ))
Tactic: rw [Nat.bitwise_bit gff]
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
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 (pos n) = bif g false true then pos n else 0
fn0 : ∀ (n : PosNum), f (pos n) 0 = bif g true false then pos n else 0
fnn : ∀ (m n : PosNum), f (pos m) (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 pos n else 0)
pb1 : ∀ (a : Bool) (m : PosNum), p (PosNum.bit a m) 1 = bit (g a true) (bif g true false then 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 pos n else 0) : ℕ)
this' : ∀ (b : Bool) (n : PosNum), (↑(pos (PosNum.bit b n)) : ℕ) = Nat.bit b (↑n : ℕ)
m : PosNum
IH : ∀ (n : PosNum), (↑(p m n) : ℕ) = Nat.bitwise g (↑(pos m) : ℕ) (↑(pos n) : ℕ)
n : PosNum
⊢ (↑(p (PosNum.bit false m) (PosNum.bit false n)) : ℕ) =
    Nat.bitwise g (↑(pos (PosNum.bit false m)) : ℕ) (↑(pos (PosNum.bit false n)) : ℕ)
have pos : (↑(p (PosNum.bit false m) (PosNum.bit false n)) : ℕ) =
  Nat.bitwise g (Nat.bit false (↑m : ℕ)) (↑(pos (PosNum.bit false n)) : ℕ)
Tactic: rw [this']