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

State before:
n : Nat
⊢ n <<< 1 ||| 1 = 2 * n + 1
Tactic:
rw [shiftLeft_one]
State after:
n : Nat
⊢ 2 * n ||| 1 = 2 * n + 1

State before:
n : Nat
⊢ 2 * n ||| 1 = 2 * n + 1
Tactic:
apply or_one_eq_add_one
State after:
case a
n : Nat
⊢ 2 * n % 2 = 0

State before:
case a
n : Nat
⊢ 2 * n % 2 = 0
Tactic:
exact Nat.mul_mod_right 2 n
State after:
no goals