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)
m : PosNum
⊢ Eq (α := ℕ) (↑(bif g true false then pos m else 0) : ℕ) (if g true false = true then (↑(pos m) : ℕ) else 0)
have pos : Eq (α := ℕ) (↑(bif false then pos m else 0) : ℕ) (if false = true then (↑(pos m) : ℕ) else 0)
Tactic: cases g true false
-- 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 (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)
m : PosNum
pos : Eq (α := ℕ) (↑(bif false then Num.pos m else 0) : ℕ) (if false = true then (↑(Num.pos m) : ℕ) else 0)
⊢ Eq (α := ℕ) (↑(bif g true false then Num.pos m else 0) : ℕ) (if g true false = true then (↑(Num.pos m) : ℕ) else 0)
have pos₁ : Eq (α := ℕ) (↑(bif true then Num.pos m else 0) : ℕ) (if true = true then (↑(Num.pos m) : ℕ) else 0)
Tactic: cases g true false
-- 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)
m n : PosNum
⊢ (↑(f (pos m) (pos n)) : ℕ) = Nat.bitwise g (↑(pos m) : ℕ) (↑(pos n) : ℕ)
have pos : (↑(p m n) : ℕ) = Nat.bitwise g (↑(pos m) : ℕ) (↑(pos n) : ℕ)
Tactic: rw [fnn]
-- 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)
m n_1 : PosNum
b : Bool
n : PosNum
⊢ Eq (α := ℕ) (bif b then (↑n : ℕ) else 0) (↑(bif b then pos n else 0) : ℕ)
have false : Eq (α := ℕ) (bif false then (↑n : ℕ) else 0) (↑(bif false then pos n else 0) : ℕ)
Tactic: cases b
Cleared hypotheses: b
-- 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 Bool.false Bool.false = Bool.false
f00 : f 0 0 = 0
f0n : ∀ (n : PosNum), f 0 (pos n) = bif g Bool.false true then pos n else 0
fn0 : ∀ (n : PosNum), f (pos n) 0 = bif g true Bool.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 Bool.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 Bool.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)
m n_1 : PosNum
b : Bool
n : PosNum
false : Eq (α := ℕ) (bif Bool.false then (↑n : ℕ) else 0) (↑(bif Bool.false then pos n else 0) : ℕ)
⊢ Eq (α := ℕ) (bif b then (↑n : ℕ) else 0) (↑(bif b then pos n else 0) : ℕ)
have true : Eq (α := ℕ) (bif true then (↑n : ℕ) else 0) (↑(bif true then pos n else 0) : ℕ)
Tactic: cases b
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (hypothesis)
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)
m n : PosNum
⊢ (↑(p m n) : ℕ) = Nat.bitwise g (↑(pos m) : ℕ) (↑(pos n) : ℕ)
have this : ∀ (b : Bool) (n : PosNum), Eq (α := ℕ) (bif b then (↑n : ℕ) else 0) (↑(bif b then pos n else 0) : ℕ)
Tactic: have this b (n : PosNum) : (cond b (↑n) 0 : ℕ) = ↑(cond b (pos n) 0 : Num) := by
      cases b <;> rfl
-- 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)
m n_1 : PosNum
this : ∀ (b : Bool) (n : PosNum), Eq (α := ℕ) (bif b then (↑n : ℕ) else 0) (↑(bif b then pos n else 0) : ℕ)
b : Bool
n : PosNum
⊢ (↑(pos (PosNum.bit b n)) : ℕ) = Nat.bit b (↑n : ℕ)
have false : (↑(pos (PosNum.bit false n)) : ℕ) = Nat.bit false (↑n : ℕ)
Tactic: cases b
Cleared hypotheses: b
-- 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 Bool.false Bool.false = Bool.false
f00 : f 0 0 = 0
f0n : ∀ (n : PosNum), f 0 (pos n) = bif g Bool.false true then pos n else 0
fn0 : ∀ (n : PosNum), f (pos n) 0 = bif g true Bool.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 Bool.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 Bool.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)
m n_1 : PosNum
this : ∀ (b : Bool) (n : PosNum), Eq (α := ℕ) (bif b then (↑n : ℕ) else 0) (↑(bif b then pos n else 0) : ℕ)
b : Bool
n : PosNum
false : (↑(pos (PosNum.bit Bool.false n)) : ℕ) = Nat.bit Bool.false (↑n : ℕ)
⊢ (↑(pos (PosNum.bit b n)) : ℕ) = Nat.bit b (↑n : ℕ)
have true : (↑(pos (PosNum.bit true n)) : ℕ) = Nat.bit true (↑n : ℕ)
Tactic: cases b
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (hypothesis)
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)
m n : PosNum
this : ∀ (b : Bool) (n : PosNum), Eq (α := ℕ) (bif b then (↑n : ℕ) else 0) (↑(bif b then pos n else 0) : ℕ)
⊢ (↑(p m n) : ℕ) = Nat.bitwise g (↑(pos m) : ℕ) (↑(pos n) : ℕ)
have this' : ∀ (b : Bool) (n : PosNum), (↑(pos (PosNum.bit b n)) : ℕ) = Nat.bit b (↑n : ℕ)
Tactic: have this' b (n : PosNum) : ↑(pos (PosNum.bit b n)) = Nat.bit b ↑n := by
      cases b <;> simp
-- 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)
m n : PosNum
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 : ℕ)
⊢ (↑(p m n) : ℕ) = Nat.bitwise g (↑(pos m) : ℕ) (↑(pos n) : ℕ)
have pos : ∀ (n : PosNum), (↑(p one n) : ℕ) = Nat.bitwise g (↑(pos one) : ℕ) (↑(pos n) : ℕ)
Tactic: induction m generalizing n with | one => ?_ | bit1 m IH => ?_ | bit0 m IH => ?_
Cleared hypotheses: m, n
-- 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 (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)
m n : PosNum
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 : ℕ)
pos : ∀ (n : PosNum), (↑(p one n) : ℕ) = Nat.bitwise g (↑(Num.pos one) : ℕ) (↑(Num.pos n) : ℕ)
⊢ (↑(p m n) : ℕ) = Nat.bitwise g (↑(Num.pos m) : ℕ) (↑(Num.pos n) : ℕ)
have pos₁ : ∀ (m : PosNum) (IH : ∀ (n : PosNum), (↑(p m n) : ℕ) = Nat.bitwise g (↑(Num.pos m) : ℕ) (↑(Num.pos n) : ℕ)) (n : PosNum),
  (↑(p m.bit1 n) : ℕ) = Nat.bitwise g (↑(Num.pos m.bit1) : ℕ) (↑(Num.pos n) : ℕ)
Tactic: induction m generalizing n with | one => ?_ | bit1 m IH => ?_ | bit0 m IH => ?_
Cleared hypotheses: m, n
-- 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 (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)
m n : PosNum
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 : ℕ)
pos : ∀ (n : PosNum), (↑(p one n) : ℕ) = Nat.bitwise g (↑(Num.pos one) : ℕ) (↑(Num.pos n) : ℕ)
pos₁ :
  ∀ (m : PosNum) (IH : ∀ (n : PosNum), (↑(p m n) : ℕ) = Nat.bitwise g (↑(Num.pos m) : ℕ) (↑(Num.pos n) : ℕ))
    (n : PosNum), (↑(p m.bit1 n) : ℕ) = Nat.bitwise g (↑(Num.pos m.bit1) : ℕ) (↑(Num.pos n) : ℕ)
⊢ (↑(p m n) : ℕ) = Nat.bitwise g (↑(Num.pos m) : ℕ) (↑(Num.pos n) : ℕ)
have pos₂ : ∀ (m : PosNum) (IH : ∀ (n : PosNum), (↑(p m n) : ℕ) = Nat.bitwise g (↑(Num.pos m) : ℕ) (↑(Num.pos n) : ℕ)) (n : PosNum),
  (↑(p m.bit0 n) : ℕ) = Nat.bitwise g (↑(Num.pos m.bit0) : ℕ) (↑(Num.pos n) : ℕ)
Tactic: induction m generalizing n with | one => ?_ | bit1 m IH => ?_ | bit0 m IH => ?_
Cleared hypotheses: m, n
-- 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 : ℕ)
n : PosNum
⊢ (↑(p one n) : ℕ) = Nat.bitwise g (↑(pos one) : ℕ) (↑(pos n) : ℕ)
have pos : (↑(p one one) : ℕ) = Nat.bitwise g (↑(pos one) : ℕ) (↑(pos one) : ℕ)
Tactic: obtain - | n | n := n
Cleared hypotheses: n
-- 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 (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 one one) : ℕ) = Nat.bitwise g (↑(Num.pos one) : ℕ) (↑(Num.pos one) : ℕ)
⊢ (↑(p one n) : ℕ) = Nat.bitwise g (↑(Num.pos one) : ℕ) (↑(Num.pos n) : ℕ)
have pos₁ : ∀ (n : PosNum), (↑(p one n.bit1) : ℕ) = Nat.bitwise g (↑(Num.pos one) : ℕ) (↑(Num.pos n.bit1) : ℕ)
Tactic: obtain - | n | n := n
Cleared hypotheses: n
-- 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 (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 one one) : ℕ) = Nat.bitwise g (↑(Num.pos one) : ℕ) (↑(Num.pos one) : ℕ)
pos₁ : ∀ (n : PosNum), (↑(p one n.bit1) : ℕ) = Nat.bitwise g (↑(Num.pos one) : ℕ) (↑(Num.pos n.bit1) : ℕ)
⊢ (↑(p one n) : ℕ) = Nat.bitwise g (↑(Num.pos one) : ℕ) (↑(Num.pos n) : ℕ)
have pos₂ : ∀ (n : PosNum), (↑(p one n.bit0) : ℕ) = Nat.bitwise g (↑(Num.pos one) : ℕ) (↑(Num.pos n.bit0) : ℕ)
Tactic: obtain - | n | n := n
Cleared hypotheses: n
-- 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 m.bit1 n) : ℕ) = Nat.bitwise g (↑(pos m.bit1) : ℕ) (↑(pos n) : ℕ)
have pos : (↑(p m.bit1 one) : ℕ) = Nat.bitwise g (↑(pos m.bit1) : ℕ) (↑(pos one) : ℕ)
Tactic: obtain - | n | n := n
Cleared hypotheses: n
-- 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 (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 m.bit1 one) : ℕ) = Nat.bitwise g (↑(Num.pos m.bit1) : ℕ) (↑(Num.pos one) : ℕ)
⊢ (↑(p m.bit1 n) : ℕ) = Nat.bitwise g (↑(Num.pos m.bit1) : ℕ) (↑(Num.pos n) : ℕ)
have pos₁ : ∀ (n : PosNum), (↑(p m.bit1 n.bit1) : ℕ) = Nat.bitwise g (↑(Num.pos m.bit1) : ℕ) (↑(Num.pos n.bit1) : ℕ)
Tactic: obtain - | n | n := n
Cleared hypotheses: n
-- 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 (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 m.bit1 one) : ℕ) = Nat.bitwise g (↑(Num.pos m.bit1) : ℕ) (↑(Num.pos one) : ℕ)
pos₁ : ∀ (n : PosNum), (↑(p m.bit1 n.bit1) : ℕ) = Nat.bitwise g (↑(Num.pos m.bit1) : ℕ) (↑(Num.pos n.bit1) : ℕ)
⊢ (↑(p m.bit1 n) : ℕ) = Nat.bitwise g (↑(Num.pos m.bit1) : ℕ) (↑(Num.pos n) : ℕ)
have pos₂ : ∀ (n : PosNum), (↑(p m.bit1 n.bit0) : ℕ) = Nat.bitwise g (↑(Num.pos m.bit1) : ℕ) (↑(Num.pos n.bit0) : ℕ)
Tactic: obtain - | n | n := n
Cleared hypotheses: n
-- 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 m.bit0 n) : ℕ) = Nat.bitwise g (↑(pos m.bit0) : ℕ) (↑(pos n) : ℕ)
have pos : (↑(p m.bit0 one) : ℕ) = Nat.bitwise g (↑(pos m.bit0) : ℕ) (↑(pos one) : ℕ)
Tactic: obtain - | n | n := n
Cleared hypotheses: n
-- 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 (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 m.bit0 one) : ℕ) = Nat.bitwise g (↑(Num.pos m.bit0) : ℕ) (↑(Num.pos one) : ℕ)
⊢ (↑(p m.bit0 n) : ℕ) = Nat.bitwise g (↑(Num.pos m.bit0) : ℕ) (↑(Num.pos n) : ℕ)
have pos₁ : ∀ (n : PosNum), (↑(p m.bit0 n.bit1) : ℕ) = Nat.bitwise g (↑(Num.pos m.bit0) : ℕ) (↑(Num.pos n.bit1) : ℕ)
Tactic: obtain - | n | n := n
Cleared hypotheses: n