n : ℕ
⊢ (match boddDiv2 n with
      | (false, m) => (true, m)
      | (true, m) => (false, succ m)).fst =
    !(boddDiv2 n).fst
n : ℕ
⊢ bodd (succ n) = !bodd n
simp only [bodd, boddDiv2]
n : ℕ
b : Bool
m : ℕ
⊢ (match (b, m) with
      | (false, m) => (true, m)
      | (true, m) => (false, succ m)).fst =
    !(b, m).fst
n : ℕ
⊢ (match boddDiv2 n with
      | (false, m) => (true, m)
      | (true, m) => (false, succ m)).fst =
    !(boddDiv2 n).fst
let ⟨b,m⟩ := boddDiv2 n
no goals
n : ℕ
b : Bool
m : ℕ
⊢ (match (b, m) with
      | (false, m) => (true, m)
      | (true, m) => (false, succ m)).fst =
    !(b, m).fst
cases b <;> rfl