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) : ℕ)
n : PosNum
⊢ (↑(p (PosNum.bit false m) (PosNum.bit true n)) : ℕ) = Nat.bit (g false true) (↑(p m n) : ℕ)
have pos : Eq (α := ℕ) (↑(p (PosNum.bit false m) (PosNum.bit true n)) : ℕ) (↑(bit (g false true) (p m n)) : ℕ)
Tactic: rw [← bit_to_nat, pbb]
-- 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 : Eq (α := ℕ) (↑(p (PosNum.bit false m) (PosNum.bit true 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) : ℕ)
have pos₁ : Eq (α := ℕ) (↑(bit (g false true) (p m n)) : ℕ) (↑(bit (g false true) (p m n)) : ℕ)
Tactic: rw [← bit_to_nat, pbb]
-- 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.bit (g false false) (Nat.bitwise g (↑m : ℕ) (↑n : ℕ))
have pos : (↑(p (PosNum.bit false m) (PosNum.bit false n)) : ℕ) = Nat.bit (g false false) (↑(p m n) : ℕ)
Tactic: rw [← show ∀ n : PosNum, ↑(p m n) = Nat.bitwise g ↑m ↑n from IH]
-- 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.bit (g false false) (↑(p m n) : ℕ)
have pos : Eq (α := ℕ) (↑(p (PosNum.bit false m) (PosNum.bit false n)) : ℕ) (↑(bit (g false false) (p m n)) : ℕ)
Tactic: rw [← bit_to_nat, pbb]
-- 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 : Eq (α := ℕ) (↑(p (PosNum.bit false m) (PosNum.bit false 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) : ℕ)
have pos₁ : Eq (α := ℕ) (↑(bit (g false false) (p m n)) : ℕ) (↑(bit (g false false) (p m n)) : ℕ)
Tactic: rw [← bit_to_nat, pbb]
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
⊢ ∀ (m n : Num), (↑(m ||| n) : ℕ) = HOr.hOr (α := ℕ) (↑m : ℕ) (↑n : ℕ)
have gff : (false || false) = false
Tactic: apply castNum_eq_bitwise fun x y => pos (PosNum.lor x y)
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
gff : (false || false) = false
⊢ ∀ (m n : Num), (↑(m ||| n) : ℕ) = HOr.hOr (α := ℕ) (↑m : ℕ) (↑n : ℕ)
have f00 : HOr.hOr (α := Num) 0 0 = 0
Tactic: apply castNum_eq_bitwise fun x y => pos (PosNum.lor x y)
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
gff : (false || false) = false
f00 : HOr.hOr (α := Num) 0 0 = 0
⊢ ∀ (m n : Num), (↑(m ||| n) : ℕ) = HOr.hOr (α := ℕ) (↑m : ℕ) (↑n : ℕ)
have f0n : ∀ (n : PosNum), 0 ||| pos n = bif false || true then pos n else 0
Tactic: apply castNum_eq_bitwise fun x y => pos (PosNum.lor x y)
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
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
⊢ ∀ (m n : Num), (↑(m ||| n) : ℕ) = HOr.hOr (α := ℕ) (↑m : ℕ) (↑n : ℕ)
have fn0 : ∀ (n : PosNum), pos n ||| 0 = bif true || false then pos n else 0
Tactic: apply castNum_eq_bitwise fun x y => pos (PosNum.lor x y)
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
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
⊢ ∀ (m n : Num), (↑(m ||| n) : ℕ) = HOr.hOr (α := ℕ) (↑m : ℕ) (↑n : ℕ)
have fnn : ∀ (m n : PosNum), pos m ||| pos n = pos (m.lor n)
Tactic: apply castNum_eq_bitwise fun x y => pos (PosNum.lor x y)
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
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)
⊢ ∀ (m n : Num), (↑(m ||| n) : ℕ) = HOr.hOr (α := ℕ) (↑m : ℕ) (↑n : ℕ)
have p11 : pos (lor 1 1) = bif true || true then 1 else 0
Tactic: apply castNum_eq_bitwise fun x y => pos (PosNum.lor x y)
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
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
⊢ ∀ (m n : Num), (↑(m ||| n) : ℕ) = HOr.hOr (α := ℕ) (↑m : ℕ) (↑n : ℕ)
have p1b : ∀ (b : Bool) (n : PosNum), pos (lor 1 (PosNum.bit b n)) = bit (true || b) (bif false || true then pos n else 0)
Tactic: apply castNum_eq_bitwise fun x y => pos (PosNum.lor x y)
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
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)
⊢ ∀ (m n : Num), (↑(m ||| n) : ℕ) = HOr.hOr (α := ℕ) (↑m : ℕ) (↑n : ℕ)
have pb1 : ∀ (a : Bool) (m : PosNum), pos ((PosNum.bit a m).lor 1) = bit (a || true) (bif true || false then pos m else 0)
Tactic: apply castNum_eq_bitwise fun x y => pos (PosNum.lor x y)
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
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)
⊢ ∀ (m n : Num), (↑(m ||| n) : ℕ) = HOr.hOr (α := ℕ) (↑m : ℕ) (↑n : ℕ)
have pbb : ∀ (a b : Bool) (m n : PosNum), pos ((PosNum.bit a m).lor (PosNum.bit b n)) = bit (a || b) (pos (m.lor n))
Tactic: apply castNum_eq_bitwise fun x y => pos (PosNum.lor x y)
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
⊢ ∀ (n : PosNum), 0 ||| pos n = bif false || true then pos n else 0
have f0n : 0 ||| pos one = bif false || true then pos one else 0
Tactic: try rintro (_ | _)
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
f0n : 0 ||| pos one = bif false || true then pos one else 0
⊢ ∀ (n : PosNum), 0 ||| pos n = bif false || true then pos n else 0
have f0n₁ : ∀ (a : PosNum), 0 ||| pos a.bit1 = bif false || true then pos a.bit1 else 0
Tactic: try rintro (_ | _)
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
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
⊢ ∀ (n : PosNum), 0 ||| pos n = bif false || true then pos n else 0
have f0n₂ : ∀ (a : PosNum), 0 ||| pos a.bit0 = bif false || true then pos a.bit0 else 0
Tactic: try rintro (_ | _)
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
⊢ ∀ (n : PosNum), pos n ||| 0 = bif true || false then pos n else 0
have fn0 : pos one ||| 0 = bif true || false then pos one else 0
Tactic: try rintro (_ | _)
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
fn0 : pos one ||| 0 = bif true || false then pos one else 0
⊢ ∀ (n : PosNum), pos n ||| 0 = bif true || false then pos n else 0
have fn0₁ : ∀ (a : PosNum), pos a.bit1 ||| 0 = bif true || false then pos a.bit1 else 0
Tactic: try rintro (_ | _)
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
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
⊢ ∀ (n : PosNum), pos n ||| 0 = bif true || false then pos n else 0
have fn0₂ : ∀ (a : PosNum), pos a.bit0 ||| 0 = bif true || false then pos a.bit0 else 0
Tactic: try rintro (_ | _)
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
⊢ ∀ (m n : PosNum), pos m ||| pos n = pos (m.lor n)
have fnn : ∀ (n : PosNum), pos one ||| pos n = pos (one.lor n)
Tactic: try rintro (_ | _)
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
fnn : ∀ (n : PosNum), pos one ||| pos n = pos (one.lor n)
⊢ ∀ (m n : PosNum), pos m ||| pos n = pos (m.lor n)
have fnn₁ : ∀ (a n : PosNum), pos a.bit1 ||| pos n = pos (a.bit1.lor n)
Tactic: try rintro (_ | _)
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
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)
⊢ ∀ (m n : PosNum), pos m ||| pos n = pos (m.lor n)
have fnn₂ : ∀ (a n : PosNum), pos a.bit0 ||| pos n = pos (a.bit0.lor n)
Tactic: try rintro (_ | _)
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
⊢ ∀ (b : Bool) (n : PosNum), pos (lor 1 (PosNum.bit b n)) = bit (true || b) (bif false || true then pos n else 0)
have p1b : ∀ (n : PosNum), pos (lor 1 (PosNum.bit false n)) = bit (true || false) (bif false || true then pos n else 0)
Tactic: try rintro (_ | _)
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
p1b : ∀ (n : PosNum), pos (lor 1 (PosNum.bit false n)) = bit (true || false) (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)
have p1b₁ : ∀ (n : PosNum), pos (lor 1 (PosNum.bit true n)) = bit (true || true) (bif false || true then pos n else 0)
Tactic: try rintro (_ | _)
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
⊢ ∀ (a : Bool) (m : PosNum), pos ((PosNum.bit a m).lor 1) = bit (a || true) (bif true || false then pos m else 0)
have pb1 : ∀ (m : PosNum), pos ((PosNum.bit false m).lor 1) = bit (false || true) (bif true || false then pos m else 0)
Tactic: try rintro (_ | _)
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
pb1 : ∀ (m : PosNum), pos ((PosNum.bit false m).lor 1) = bit (false || 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)
have pb1₁ : ∀ (m : PosNum), pos ((PosNum.bit true m).lor 1) = bit (true || true) (bif true || false then pos m else 0)
Tactic: try rintro (_ | _)
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
⊢ ∀ (a b : Bool) (m n : PosNum), pos ((PosNum.bit a m).lor (PosNum.bit b n)) = bit (a || b) (pos (m.lor n))
have pbb : ∀ (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 (_ | _)
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
pbb : ∀ (b : Bool) (m n : PosNum), pos ((PosNum.bit false m).lor (PosNum.bit b n)) = bit (false || 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))
have pbb₁ : ∀ (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 (_ | _)
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
⊢ ∀ (n : PosNum), pos one ||| pos n = pos (one.lor n)
have fnn : pos one ||| pos one = pos (one.lor one)
Tactic: try rintro (_ | _)
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
fnn : pos one ||| pos one = pos (one.lor one)
⊢ ∀ (n : PosNum), pos one ||| pos n = pos (one.lor n)
have fnn₁ : ∀ (a : PosNum), pos one ||| pos a.bit1 = pos (one.lor a.bit1)
Tactic: try rintro (_ | _)
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
fnn : pos one ||| pos one = pos (one.lor one)
fnn₁ : ∀ (a : PosNum), pos one ||| pos a.bit1 = pos (one.lor a.bit1)
⊢ ∀ (n : PosNum), pos one ||| pos n = pos (one.lor n)
have fnn₂ : ∀ (a : PosNum), pos one ||| pos a.bit0 = pos (one.lor a.bit0)
Tactic: try rintro (_ | _)
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
a : PosNum
⊢ ∀ (n : PosNum), pos a.bit1 ||| pos n = pos (a.bit1.lor n)
have fnn : pos a.bit1 ||| pos one = pos (a.bit1.lor one)
Tactic: try rintro (_ | _)
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
a : PosNum
fnn : pos a.bit1 ||| pos one = pos (a.bit1.lor one)
⊢ ∀ (n : PosNum), pos a.bit1 ||| pos n = pos (a.bit1.lor n)
have fnn₁ : ∀ (a_1 : PosNum), pos a.bit1 ||| pos a_1.bit1 = pos (a.bit1.lor a_1.bit1)
Tactic: try rintro (_ | _)
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
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)
⊢ ∀ (n : PosNum), pos a.bit1 ||| pos n = pos (a.bit1.lor n)
have fnn₂ : ∀ (a_1 : PosNum), pos a.bit1 ||| pos a_1.bit0 = pos (a.bit1.lor a_1.bit0)
Tactic: try rintro (_ | _)
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
a : PosNum
⊢ ∀ (n : PosNum), pos a.bit0 ||| pos n = pos (a.bit0.lor n)
have fnn : pos a.bit0 ||| pos one = pos (a.bit0.lor one)
Tactic: try rintro (_ | _)
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
a : PosNum
fnn : pos a.bit0 ||| pos one = pos (a.bit0.lor one)
⊢ ∀ (n : PosNum), pos a.bit0 ||| pos n = pos (a.bit0.lor n)
have fnn₁ : ∀ (a_1 : PosNum), pos a.bit0 ||| pos a_1.bit1 = pos (a.bit0.lor a_1.bit1)
Tactic: try rintro (_ | _)
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
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)
⊢ ∀ (n : PosNum), pos a.bit0 ||| pos n = pos (a.bit0.lor n)
have fnn₂ : ∀ (a_1 : PosNum), pos a.bit0 ||| pos a_1.bit0 = pos (a.bit0.lor a_1.bit0)
Tactic: try rintro (_ | _)
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
⊢ ∀ (n : PosNum), pos (lor 1 (PosNum.bit false n)) = bit (true || false) (bif false || true then pos n else 0)
have p1b : pos (lor 1 (PosNum.bit false one)) = bit (true || false) (bif false || true then pos one else 0)
Tactic: try rintro (_ | _)
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
p1b : pos (lor 1 (PosNum.bit false one)) = bit (true || false) (bif false || true then pos one else 0)
⊢ ∀ (n : PosNum), pos (lor 1 (PosNum.bit false n)) = bit (true || false) (bif false || true then pos n else 0)
have p1b₁ : ∀ (a : PosNum), pos (lor 1 (PosNum.bit false a.bit1)) = bit (true || false) (bif false || true then pos a.bit1 else 0)
Tactic: try rintro (_ | _)
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
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)
⊢ ∀ (n : PosNum), pos (lor 1 (PosNum.bit false n)) = bit (true || false) (bif false || true then pos n else 0)
have p1b₂ : ∀ (a : PosNum), pos (lor 1 (PosNum.bit false a.bit0)) = bit (true || false) (bif false || true then pos a.bit0 else 0)
Tactic: try rintro (_ | _)
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
⊢ ∀ (n : PosNum), pos (lor 1 (PosNum.bit true n)) = bit (true || true) (bif false || true then pos n else 0)
have p1b : pos (lor 1 (PosNum.bit true one)) = bit (true || true) (bif false || true then pos one else 0)
Tactic: try rintro (_ | _)
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
p1b : pos (lor 1 (PosNum.bit true one)) = bit (true || true) (bif false || true then pos one else 0)
⊢ ∀ (n : PosNum), pos (lor 1 (PosNum.bit true n)) = bit (true || true) (bif false || true then pos n else 0)
have p1b₁ : ∀ (a : PosNum), pos (lor 1 (PosNum.bit true a.bit1)) = bit (true || true) (bif false || true then pos a.bit1 else 0)
Tactic: try rintro (_ | _)
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
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)
⊢ ∀ (n : PosNum), pos (lor 1 (PosNum.bit true n)) = bit (true || true) (bif false || true then pos n else 0)
have p1b₂ : ∀ (a : PosNum), pos (lor 1 (PosNum.bit true a.bit0)) = bit (true || true) (bif false || true then pos a.bit0 else 0)
Tactic: try rintro (_ | _)
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
⊢ ∀ (m : PosNum), pos ((PosNum.bit false m).lor 1) = bit (false || true) (bif true || false then pos m else 0)
have pb1 : pos ((PosNum.bit false one).lor 1) = bit (false || true) (bif true || false then pos one else 0)
Tactic: try rintro (_ | _)
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
pb1 : pos ((PosNum.bit false one).lor 1) = bit (false || true) (bif true || false then pos one else 0)
⊢ ∀ (m : PosNum), pos ((PosNum.bit false m).lor 1) = bit (false || true) (bif true || false then pos m else 0)
have pb1₁ : ∀ (a : PosNum), pos ((PosNum.bit false a.bit1).lor 1) = bit (false || true) (bif true || false then pos a.bit1 else 0)
Tactic: try rintro (_ | _)
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
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)
⊢ ∀ (m : PosNum), pos ((PosNum.bit false m).lor 1) = bit (false || true) (bif true || false then pos m else 0)
have pb1₂ : ∀ (a : PosNum), pos ((PosNum.bit false a.bit0).lor 1) = bit (false || true) (bif true || false then pos a.bit0 else 0)
Tactic: try rintro (_ | _)
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
⊢ ∀ (m : PosNum), pos ((PosNum.bit true m).lor 1) = bit (true || true) (bif true || false then pos m else 0)
have pb1 : pos ((PosNum.bit true one).lor 1) = bit (true || true) (bif true || false then pos one else 0)
Tactic: try rintro (_ | _)
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
pb1 : pos ((PosNum.bit true one).lor 1) = bit (true || true) (bif true || false then pos one else 0)
⊢ ∀ (m : PosNum), pos ((PosNum.bit true m).lor 1) = bit (true || true) (bif true || false then pos m else 0)
have pb1₁ : ∀ (a : PosNum), pos ((PosNum.bit true a.bit1).lor 1) = bit (true || true) (bif true || false then pos a.bit1 else 0)
Tactic: try rintro (_ | _)
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
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)
⊢ ∀ (m : PosNum), pos ((PosNum.bit true m).lor 1) = bit (true || true) (bif true || false then pos m else 0)
have pb1₂ : ∀ (a : PosNum), pos ((PosNum.bit true a.bit0).lor 1) = bit (true || true) (bif true || false then pos a.bit0 else 0)
Tactic: try rintro (_ | _)
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
⊢ ∀ (b : Bool) (m n : PosNum), pos ((PosNum.bit false m).lor (PosNum.bit b n)) = bit (false || b) (pos (m.lor n))
have pbb : ∀ (m n : PosNum), pos ((PosNum.bit false m).lor (PosNum.bit false n)) = bit (false || false) (pos (m.lor n))
Tactic: try rintro (_ | _)