case succ
m n✝ : ℤ
n : ℕ
ih : Even (m ^ n) ↔ Even m ∧ n ≠ 0
⊢ Even m → ¬n = 0 → Even m
m n✝ : ℤ
n : ℕ
⊢ Even (m ^ n) ↔ Even m ∧ n ≠ 0
induction' n with n ih <;> simp [*, even_mul, pow_succ]
no goals
case succ
m n✝ : ℤ
n : ℕ
ih : Even (m ^ n) ↔ Even m ∧ n ≠ 0
⊢ Even m → ¬n = 0 → Even m
tauto