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

State before:
n : Nat
⊢ getBit (Nat.lsb n) 0 = getBit n 0
Tactic:
cases Nat.mod_two_eq_zero_or_one n
State after:
case inl
n : Nat
h✝ : n % 2 = 0
⊢ getBit (Nat.lsb n) 0 = getBit n 0

case inr
n : Nat
h✝ : n % 2 = 1
⊢ getBit (Nat.lsb n) 0 = getBit n 0

State before:
n : Nat
heven : n % 2 = 0
⊢ getBit (Nat.lsb n) 0 = getBit n 0
Tactic:
case inl heven =>
  rw [
    Nat.lsb_of_even heven,
    Nat.shiftLeft_getBit,
    decide_eq_false (p:=0≥1) (by decide),
    Bool.false_and,
  ]
  conv => rhs; dsimp [getBit]; rw [heven]; reduce
State after:
no goals

State before:
n : Nat
hodd : n % 2 = 1
⊢ getBit (Nat.lsb n) 0 = getBit n 0
Tactic:
case inr hodd =>
  rw [Nat.lsb_of_odd hodd]; dsimp [getBit]; rw [hodd]; decide
State after:
no goals

State before:
n : Nat
heven : n % 2 = 0
⊢ getBit (Nat.lsb n) 0 = getBit n 0
Tactic:
rw [
  Nat.lsb_of_even heven,
  Nat.shiftLeft_getBit,
  decide_eq_false (p:=0≥1) (by decide),
  Bool.false_and,
]
State after:
n : Nat
heven : n % 2 = 0
⊢ false = getBit n 0

State before:
n : Nat
heven : n % 2 = 0
⊢ false = getBit n 0
Tactic:
conv => rhs; dsimp [getBit]; rw [heven]; reduce
State after:
no goals

State before:
n : Nat
heven : n % 2 = 0
⊢ ¬0 ≥ 1
Tactic:
decide
State after:
no goals

State before:
n : Nat
hodd : n % 2 = 1
⊢ getBit (Nat.lsb n) 0 = getBit n 0
Tactic:
rw [Nat.lsb_of_odd hodd]
State after:
n : Nat
hodd : n % 2 = 1
⊢ getBit 1 0 = getBit n 0

State before:
n : Nat
hodd : n % 2 = 1
⊢ getBit 1 0 = getBit n 0
Tactic:
dsimp [getBit]
State after:
n : Nat
hodd : n % 2 = 1
⊢ decide (1 % 2 = 1) = decide (n % 2 = 1)

State before:
n : Nat
hodd : n % 2 = 1
⊢ decide (1 % 2 = 1) = decide (n % 2 = 1)
Tactic:
rw [hodd]
State after:
n : Nat
hodd : n % 2 = 1
⊢ decide (1 % 2 = 1) = decide (1 = 1)

State before:
n : Nat
hodd : n % 2 = 1
⊢ decide (1 % 2 = 1) = decide (1 = 1)
Tactic:
decide
State after:
no goals