case pos hm =>
  cases hm
  unfold bitwise
  simp [flip]
  by_cases n = 0
  case pos hn =>
    cases hn; rw [if_pos (Eq.refl 0)]
    by_cases f true false <;> simp
  case neg hn => rw [if_neg hn]
f : Bool → Bool → Bool
m n : Nat
hm : m = 0
⊢ bitwise (flip f) m n = bitwise f n m
no goals