case mp
n✝ n : ℕ
b : Bool
⊢ bit b n = 0 → n = 0 ∧ b = false

case mpr
n✝ n : ℕ
b : Bool
⊢ n = 0 ∧ b = false → bit b n = 0
n✝ n : ℕ
b : Bool
⊢ bit b n = 0 ↔ n = 0 ∧ b = false
constructor
no goals
case mp
n✝ n : ℕ
b : Bool
⊢ bit b n = 0 → n = 0 ∧ b = false
cases b <;> simp [Nat.bit, Nat.bit0_eq_zero, Nat.bit1_ne_zero]
case mpr.intro
n : ℕ
⊢ bit false 0 = 0
case mpr
n✝ n : ℕ
b : Bool
⊢ n = 0 ∧ b = false → bit b n = 0
rintro ⟨rfl, rfl⟩
no goals
case mpr.intro
n : ℕ
⊢ bit false 0 = 0
rfl