have : i = 0 := by
  conv at h => lhs; change getBit (2^0) i; rw [Nat.getBit_two_pow]
  exact Eq.symm (of_decide_eq_true h)
case mp
i : Nat
h : getBit 1 i = true
⊢ ∀ (j : Nat), j < i → getBit 1 j = false
case mp
i : Nat
h : getBit 1 i = true
this : i = 0
⊢ ∀ (j : Nat), j < i → getBit 1 j = false