no goals
m n✝ n : ℤ
⊢ Xor' (Even n) (Odd n)
cases even_or_odd n with
| inl h => exact Or.inl ⟨h, even_iff_not_odd.mp h⟩
| inr h => exact Or.inr ⟨h, odd_iff_not_even.mp h⟩
no goals
case inl
m n✝ n : ℤ
h : Even n
⊢ Xor' (Even n) (Odd n)
exact Or.inl ⟨h, even_iff_not_odd.mp h⟩
no goals
case inr
m n✝ n : ℤ
h : Odd n
⊢ Xor' (Even n) (Odd n)
exact Or.inr ⟨h, odd_iff_not_even.mp h⟩