b : Bool
n : ℕ
⊢ testBit (↑(Nat.bit b n)) 0 = b
b : Bool
n : ℕ
⊢ testBit (bit b ↑n) 0 = b
rw [bit_coe_nat]
no goals
b : Bool
n : ℕ
⊢ testBit (↑(Nat.bit b n)) 0 = b
apply Nat.testBit_zero
b : Bool
n : ℕ
⊢ testBit -[Nat.bit (!b) n+1] 0 = b
b : Bool
n : ℕ
⊢ testBit (bit b -[n+1]) 0 = b
rw [bit_negSucc]
b : Bool
n : ℕ
⊢ (!Nat.testBit (Nat.bit (!b) n) 0) = b
b : Bool
n : ℕ
⊢ testBit -[Nat.bit (!b) n+1] 0 = b
dsimp [testBit]
b : Bool
n : ℕ
⊢ (!!b) = b
b : Bool
n : ℕ
⊢ (!Nat.testBit (Nat.bit (!b) n) 0) = b
rw [Nat.testBit_zero]
b : Bool
n : ℕ
⊢ (!!b) = b
b : Bool
n : ℕ
⊢ (!!b) = b
clear testBit_zero
no goals
b : Bool
n : ℕ
⊢ (!!b) = b
cases b <;>
rfl