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

State before:
n : Nat
⊢ n % 2 = 0 → Nat.lsb n = Nat.lsb (n / 2) <<< 1
Tactic:
intro heven
State after:
n : Nat
heven : n % 2 = 0
⊢ Nat.lsb n = Nat.lsb (n / 2) <<< 1

State before:
n : Nat
heven : n % 2 = 0
⊢ Nat.lsb n = Nat.lsb (n / 2) <<< 1
Tactic:
have hn : n = 0 + 2 * (n/2) := Eq.symm $ heven ▸ Nat.mod_add_div n 2
State after:
n : Nat
heven : n % 2 = 0
hn : n = 0 + 2 * (n / 2)
⊢ Nat.lsb n = Nat.lsb (n / 2) <<< 1

State before:
n : Nat
heven : n % 2 = 0
hn : n = 0 + 2 * (n / 2)
⊢ Nat.lsb n = Nat.lsb (n / 2) <<< 1
Tactic:
rw [Nat.zero_add, ←Nat.shiftLeft_one] at hn
State after:
n : Nat
heven : n % 2 = 0
hn : n = (n / 2) <<< 1
⊢ Nat.lsb n = Nat.lsb (n / 2) <<< 1

State before:
n : Nat
heven : n % 2 = 0
hn : n = (n / 2) <<< 1
⊢ Nat.lsb n = Nat.lsb (n / 2) <<< 1
Tactic:
conv => lhs; rw [hn, ←Nat.lsb_shiftLeft]
State after:
no goals