case zero
n✝ n : ℕ
⊢ testBit n zero = List.getI (bits n) zero

case succ
n✝ i : ℕ
ih : ∀ (n : ℕ), testBit n i = List.getI (bits n) i
n : ℕ
⊢ testBit n (succ i) = List.getI (bits n) (succ i)
n i : ℕ
⊢ testBit n i = List.getI (bits n) i
induction' i with i ih generalizing n
case succ
n✝ i : ℕ
ih : ∀ (n : ℕ), testBit n i = List.getI (bits n) i
n : ℕ
⊢ testBit (bit (bodd n) (div2 n)) (succ i) = List.getI (bits n) (succ i)
case succ
n✝ i : ℕ
ih : ∀ (n : ℕ), testBit n i = List.getI (bits n) i
n : ℕ
⊢ testBit n (succ i) = List.getI (bits n) (succ i)
conv_lhs => rw [← bit_decomp n]
case succ
n✝ i : ℕ
ih : ∀ (n : ℕ), testBit n i = List.getI (bits n) i
n : ℕ
⊢ List.getI (List.tail (bits n)) i = List.getI (bits n) (succ i)
case succ
n✝ i : ℕ
ih : ∀ (n : ℕ), testBit n i = List.getI (bits n) i
n : ℕ
⊢ testBit (bit (bodd n) (div2 n)) (succ i) = List.getI (bits n) (succ i)
rw [testBit_succ, ih n.div2, div2_bits_eq_tail]
no goals
case succ
n✝ i : ℕ
ih : ∀ (n : ℕ), testBit n i = List.getI (bits n) i
n : ℕ
⊢ List.getI (List.tail (bits n)) i = List.getI (bits n) (succ i)
cases n.bits <;> simp
no goals
case zero
n✝ n : ℕ
⊢ testBit n zero = List.getI (bits n) zero
simp [testBit, shiftr, bodd_eq_bits_head, List.getI_zero_eq_headI]