Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: ⊢ ∀ (m n : Num), ↑(m ||| n) = ↑m ||| ↑n

Tactic:
apply castNum_eq_bitwise fun x y => pos (PosNum.lor x y) <;>
    (try rintro (_ | _)) <;> (try rintro (_ | _))

Goal state after:
case gff
⊢ (false || false) = false

case f00
⊢ 0 ||| 0 = 0

case f0n.one
⊢ 0 ||| pos one = bif false || true then pos one else 0

case f0n.bit1
a✝ : PosNum
⊢ 0 ||| pos a✝.bit1 = bif false || true then pos a✝.bit1 else 0

case f0n.bit0
a✝ : PosNum
⊢ 0 ||| pos a✝.bit0 = bif false || true then pos a✝.bit0 else 0

case fn0.one
⊢ pos one ||| 0 = bif true || false then pos one else 0

case fn0.bit1
a✝ : PosNum
⊢ pos a✝.bit1 ||| 0 = bif true || false then pos a✝.bit1 else 0

case fn0.bit0
a✝ : PosNum
⊢ pos a✝.bit0 ||| 0 = bif true || false then pos a✝.bit0 else 0

case fnn.one.one
⊢ pos one ||| pos one = pos (one.lor one)

case fnn.one.bit1
a✝ : PosNum
⊢ pos one ||| pos a✝.bit1 = pos (one.lor a✝.bit1)

case fnn.one.bit0
a✝ : PosNum
⊢ pos one ||| pos a✝.bit0 = pos (one.lor a✝.bit0)

case fnn.bit1.one
a✝ : PosNum
⊢ pos a✝.bit1 ||| pos one = pos (a✝.bit1.lor one)

case fnn.bit1.bit1
a✝¹ a✝ : PosNum
⊢ pos a✝¹.bit1 ||| pos a✝.bit1 = pos (a✝¹.bit1.lor a✝.bit1)

case fnn.bit1.bit0
a✝¹ a✝ : PosNum
⊢ pos a✝¹.bit1 ||| pos a✝.bit0 = pos (a✝¹.bit1.lor a✝.bit0)

case fnn.bit0.one
a✝ : PosNum
⊢ pos a✝.bit0 ||| pos one = pos (a✝.bit0.lor one)

case fnn.bit0.bit1
a✝¹ a✝ : PosNum
⊢ pos a✝¹.bit0 ||| pos a✝.bit1 = pos (a✝¹.bit0.lor a✝.bit1)

case fnn.bit0.bit0
a✝¹ a✝ : PosNum
⊢ pos a✝¹.bit0 ||| pos a✝.bit0 = pos (a✝¹.bit0.lor a✝.bit0)

case p11
⊢ pos (lor 1 1) = bif true || true then 1 else 0

case p1b.false.one
⊢ pos (lor 1 (PosNum.bit false one)) = bit (true || false) (bif false || true then pos one else 0)

case p1b.false.bit1
a✝ : PosNum
⊢ pos (lor 1 (PosNum.bit false a✝.bit1)) = bit (true || false) (bif false || true then pos a✝.bit1 else 0)

case p1b.false.bit0
a✝ : PosNum
⊢ pos (lor 1 (PosNum.bit false a✝.bit0)) = bit (true || false) (bif false || true then pos a✝.bit0 else 0)

case p1b.true.one
⊢ pos (lor 1 (PosNum.bit true one)) = bit (true || true) (bif false || true then pos one else 0)

case p1b.true.bit1
a✝ : PosNum
⊢ pos (lor 1 (PosNum.bit true a✝.bit1)) = bit (true || true) (bif false || true then pos a✝.bit1 else 0)

case p1b.true.bit0
a✝ : PosNum
⊢ pos (lor 1 (PosNum.bit true a✝.bit0)) = bit (true || true) (bif false || true then pos a✝.bit0 else 0)

case pb1.false.one
⊢ pos ((PosNum.bit false one).lor 1) = bit (false || true) (bif true || false then pos one else 0)

case pb1.false.bit1
a✝ : PosNum
⊢ pos ((PosNum.bit false a✝.bit1).lor 1) = bit (false || true) (bif true || false then pos a✝.bit1 else 0)

case pb1.false.bit0
a✝ : PosNum
⊢ pos ((PosNum.bit false a✝.bit0).lor 1) = bit (false || true) (bif true || false then pos a✝.bit0 else 0)

case pb1.true.one
⊢ pos ((PosNum.bit true one).lor 1) = bit (true || true) (bif true || false then pos one else 0)

case pb1.true.bit1
a✝ : PosNum
⊢ pos ((PosNum.bit true a✝.bit1).lor 1) = bit (true || true) (bif true || false then pos a✝.bit1 else 0)

case pb1.true.bit0
a✝ : PosNum
⊢ pos ((PosNum.bit true a✝.bit0).lor 1) = bit (true || true) (bif true || false then pos a✝.bit0 else 0)

case pbb.false.false
⊢ ∀ (m n : PosNum), pos ((PosNum.bit false m).lor (PosNum.bit false n)) = bit (false || false) (pos (m.lor n))

case pbb.false.true
⊢ ∀ (m n : PosNum), pos ((PosNum.bit false m).lor (PosNum.bit true n)) = bit (false || true) (pos (m.lor n))

case pbb.true.false
⊢ ∀ (m n : PosNum), pos ((PosNum.bit true m).lor (PosNum.bit false n)) = bit (true || false) (pos (m.lor n))

case pbb.true.true
⊢ ∀ (m n : PosNum), pos ((PosNum.bit true m).lor (PosNum.bit true n)) = bit (true || true) (pos (m.lor n))