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

State before:
n : Nat
⊢ Nat.lsb n = 0 → n = 0
Tactic:
intro h
State after:
n : Nat
h : Nat.lsb n = 0
⊢ n = 0

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

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

State before:
case a
n : Nat
h : Nat.lsb n = 0
i : Nat
⊢ getBit n i = getBit 0 i
Tactic:
rw [Nat.zero_getBit]
State after:
case a
n : Nat
h : Nat.lsb n = 0
i : Nat
⊢ getBit n i = false

State before:
case a
n : Nat
h : Nat.lsb n = 0
i : Nat
⊢ getBit n i = false
Tactic:
induction i using Nat.recComplete
State after:
case a.ind
n : Nat
h : Nat.lsb n = 0
n✝ : Nat
a✝ : ∀ (k : Nat), k < n✝ → getBit n k = false
⊢ getBit n n✝ = false

State before:
n : Nat
h : Nat.lsb n = 0
i : Nat
h_ind : ∀ (k : Nat), k < i → getBit n k = false
⊢ getBit n i = false
Tactic:
case a.ind i h_ind =>
cases hni : n.getBit i
case false => rfl
case true =>
  calc
    true = n.lsb.getBit i := Eq.symm $ n.lsb_getBit_iff.mpr ⟨hni, h_ind⟩
    _    = Nat.getBit 0 i := by rw [h]
    _    = false          := Nat.zero_getBit i
State after:
no goals

State before:
n : Nat
h : Nat.lsb n = 0
i : Nat
h_ind : ∀ (k : Nat), k < i → getBit n k = false
⊢ getBit n i = false
Tactic:
cases hni : n.getBit i
State after:
case false
n : Nat
h : Nat.lsb n = 0
i : Nat
h_ind : ∀ (k : Nat), k < i → getBit n k = false
hni : getBit n i = false
⊢ false = false

case true
n : Nat
h : Nat.lsb n = 0
i : Nat
h_ind : ∀ (k : Nat), k < i → getBit n k = false
hni : getBit n i = true
⊢ true = false

State before:
n : Nat
h : Nat.lsb n = 0
i : Nat
h_ind : ∀ (k : Nat), k < i → getBit n k = false
hni : getBit n i = false
⊢ false = false
Tactic:
case false => rfl
State after:
no goals

State before:
n : Nat
h : Nat.lsb n = 0
i : Nat
h_ind : ∀ (k : Nat), k < i → getBit n k = false
hni : getBit n i = true
⊢ true = false
Tactic:
case true =>
  calc
    true = n.lsb.getBit i := Eq.symm $ n.lsb_getBit_iff.mpr ⟨hni, h_ind⟩
    _    = Nat.getBit 0 i := by rw [h]
    _    = false          := Nat.zero_getBit i
State after:
no goals

State before:
n : Nat
h : Nat.lsb n = 0
i : Nat
h_ind : ∀ (k : Nat), k < i → getBit n k = false
hni : getBit n i = false
⊢ false = false
Tactic:
rfl
State after:
no goals

State before:
n : Nat
h : Nat.lsb n = 0
i : Nat
h_ind : ∀ (k : Nat), k < i → getBit n k = false
hni : getBit n i = true
⊢ true = false
Tactic:
calc
  true = n.lsb.getBit i := Eq.symm $ n.lsb_getBit_iff.mpr ⟨hni, h_ind⟩
  _    = Nat.getBit 0 i := by rw [h]
  _    = false          := Nat.zero_getBit i
State after:
no goals

State before:
n : Nat
h : Nat.lsb n = 0
i : Nat
h_ind : ∀ (k : Nat), k < i → getBit n k = false
hni : getBit n i = true
⊢ getBit (Nat.lsb n) i = getBit 0 i
Tactic:
rw [h]
State after:
no goals