Theorem: pow_self_ne_zero (LeanCourse/Common.lean)

State before:
n : ℕ
⊢ n ^ n ≠ 0
Tactic:
by_cases hn : n = 0
State after:
case pos
n : ℕ
hn : n = 0
⊢ n ^ n ≠ 0

case neg
n : ℕ
hn : ¬n = 0
⊢ n ^ n ≠ 0

State before:
case pos
n : ℕ
hn : n = 0
⊢ n ^ n ≠ 0
Tactic:
simp [hn]
State after:
no goals

State before:
case neg
n : ℕ
hn : ¬n = 0
⊢ n ^ n ≠ 0
Tactic:
positivity
State after:
no goals