case pos
n m : ℕ
h : n = m
⊢ (testBit (2 ^ n) m = true) = (n = m)

case neg
n m : ℕ
h : ¬n = m
⊢ (testBit (2 ^ n) m = true) = (n = m)
n m : ℕ
⊢ (testBit (2 ^ n) m = true) = (n = m)
by_cases h : n = m
case pos.refl
n : ℕ
⊢ (testBit (2 ^ n) n = true) = (n = n)
case pos
n m : ℕ
h : n = m
⊢ (testBit (2 ^ n) m = true) = (n = m)
cases h
no goals
case pos.refl
n : ℕ
⊢ (testBit (2 ^ n) n = true) = (n = n)
simp
case neg
n m : ℕ
h : ¬n = m
⊢ (false = true) = (n = m)
case neg
n m : ℕ
h : ¬n = m
⊢ (testBit (2 ^ n) m = true) = (n = m)
rw [testBit_two_pow_of_ne h]
no goals
case neg
n m : ℕ
h : ¬n = m
⊢ (false = true) = (n = m)
simp [h]