Theorem: Nat.lor_land (Algdata/Data/Nat/Bits.lean)

State before:
l m n : Nat
⊢ (l ||| m) &&& n = l &&& n ||| m &&& n
Tactic:
apply bitext
State after:
case a
l m n : Nat
⊢ ∀ (i : Nat), getBit ((l ||| m) &&& n) i = getBit (l &&& n ||| m &&& n) i

State before:
case a
l m n : Nat
⊢ ∀ (i : Nat), getBit ((l ||| m) &&& n) i = getBit (l &&& n ||| m &&& n) i
Tactic:
intro i
State after:
case a
l m n i : Nat
⊢ getBit ((l ||| m) &&& n) i = getBit (l &&& n ||| m &&& n) i

State before:
case a
l m n i : Nat
⊢ getBit ((l ||| m) &&& n) i = getBit (l &&& n ||| m &&& n) i
Tactic:
simp [Nat.lor_getBit, Nat.land_getBit]
State after:
case a
l m n i : Nat
⊢ ((getBit l i || getBit m i) && getBit n i) = (getBit l i && getBit n i || getBit m i && getBit n i)

State before:
case a
l m n i : Nat
⊢ ((getBit l i || getBit m i) && getBit n i) = (getBit l i && getBit n i || getBit m i && getBit n i)
Tactic:
cases l.getBit i <;> cases m.getBit i <;> cases n.getBit i <;> decide
State after:
no goals