. intro h; apply And.intro h
  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)
  cases this
  intro _ hj; cases hj
case mp
i : Nat
⊢ getBit 1 i = true → getBit 1 i = true ∧ ∀ (j : Nat), j < i → getBit 1 j = false

case mpr
i : Nat
⊢ (getBit 1 i = true ∧ ∀ (j : Nat), j < i → getBit 1 j = false) → getBit 1 i = true
case mpr
i : Nat
⊢ (getBit 1 i = true ∧ ∀ (j : Nat), j < i → getBit 1 j = false) → getBit 1 i = true