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

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

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

State before:
case a
n i : Nat
⊢ getBit (n ||| 0) i = getBit n i
Tactic:
conv =>
  change (bitwise or n 0).getBit i = n.getBit i
  rw [bitwise_getBit, zero_getBit, Bool.or_false]
State after:
no goals