Theorem: Nat.pow_eq_zero (Extra/Nat/Lemmas.lean)

State before:
case zero
m : Nat
⊢ m ^ 0 = 0 ↔ m = 0 ∧ 0 ≠ 0
Tactic:
simp
State after:
no goals

State before:
case succ
m n : Nat
ih : m ^ n = 0 ↔ m = 0 ∧ n ≠ 0
⊢ m ^ (n + 1) = 0 ↔ m = 0 ∧ n + 1 ≠ 0
Tactic:
rw [Nat.pow_succ]
State after:
case succ
m n : Nat
ih : m ^ n = 0 ↔ m = 0 ∧ n ≠ 0
⊢ m ^ n * m = 0 ↔ m = 0 ∧ n + 1 ≠ 0

State before:
case succ
m n : Nat
ih : m ^ n = 0 ↔ m = 0 ∧ n ≠ 0
⊢ m ^ n * m = 0 ↔ m = 0 ∧ n + 1 ≠ 0
Tactic:
rw [Nat.mul_eq_zero]
State after:
case succ
m n : Nat
ih : m ^ n = 0 ↔ m = 0 ∧ n ≠ 0
⊢ m ^ n = 0 ∨ m = 0 ↔ m = 0 ∧ n + 1 ≠ 0

State before:
case succ
m n : Nat
ih : m ^ n = 0 ↔ m = 0 ∧ n ≠ 0
⊢ m ^ n = 0 ∨ m = 0 ↔ m = 0 ∧ n + 1 ≠ 0
Tactic:
constructor
State after:
case succ.mp
m n : Nat
ih : m ^ n = 0 ↔ m = 0 ∧ n ≠ 0
⊢ m ^ n = 0 ∨ m = 0 → m = 0 ∧ n + 1 ≠ 0

case succ.mpr
m n : Nat
ih : m ^ n = 0 ↔ m = 0 ∧ n ≠ 0
⊢ m = 0 ∧ n + 1 ≠ 0 → m ^ n = 0 ∨ m = 0

State before:
m n : Nat
ih : m ^ n = 0 ↔ m = 0 ∧ n ≠ 0
x✝ : m ^ n = 0 ∨ m = 0
h : m ^ n = 0
⊢ m = 0 ∧ n + 1 ≠ 0
Tactic:
constructor
State after:
case left
m n : Nat
ih : m ^ n = 0 ↔ m = 0 ∧ n ≠ 0
x✝ : m ^ n = 0 ∨ m = 0
h : m ^ n = 0
⊢ m = 0

case right
m n : Nat
ih : m ^ n = 0 ↔ m = 0 ∧ n ≠ 0
x✝ : m ^ n = 0 ∨ m = 0
h : m ^ n = 0
⊢ n + 1 ≠ 0

State before:
case left
m n : Nat
ih : m ^ n = 0 ↔ m = 0 ∧ n ≠ 0
x✝ : m ^ n = 0 ∨ m = 0
h : m ^ n = 0
⊢ m = 0
Tactic:
rw [ih] at h
State after:
case left
m n : Nat
ih : m ^ n = 0 ↔ m = 0 ∧ n ≠ 0
x✝ : m ^ n = 0 ∨ m = 0
h : m = 0 ∧ n ≠ 0
⊢ m = 0

State before:
case left
m n : Nat
ih : m ^ n = 0 ↔ m = 0 ∧ n ≠ 0
x✝ : m ^ n = 0 ∨ m = 0
h : m = 0 ∧ n ≠ 0
⊢ m = 0
Tactic:
exact h.1
State after:
no goals

State before:
case right
m n : Nat
ih : m ^ n = 0 ↔ m = 0 ∧ n ≠ 0
x✝ : m ^ n = 0 ∨ m = 0
h : m ^ n = 0
⊢ n + 1 ≠ 0
Tactic:
exact Nat.succ_ne_zero _
State after:
no goals

State before:
m n : Nat
ih : m ^ n = 0 ↔ m = 0 ∧ n ≠ 0
x✝ : m ^ n = 0 ∨ m = 0
h : m = 0
⊢ m = 0 ∧ n + 1 ≠ 0
Tactic:
constructor
State after:
case left
m n : Nat
ih : m ^ n = 0 ↔ m = 0 ∧ n ≠ 0
x✝ : m ^ n = 0 ∨ m = 0
h : m = 0
⊢ m = 0

case right
m n : Nat
ih : m ^ n = 0 ↔ m = 0 ∧ n ≠ 0
x✝ : m ^ n = 0 ∨ m = 0
h : m = 0
⊢ n + 1 ≠ 0

State before:
case left
m n : Nat
ih : m ^ n = 0 ↔ m = 0 ∧ n ≠ 0
x✝ : m ^ n = 0 ∨ m = 0
h : m = 0
⊢ m = 0
Tactic:
exact h
State after:
no goals

State before:
case right
m n : Nat
ih : m ^ n = 0 ↔ m = 0 ∧ n ≠ 0
x✝ : m ^ n = 0 ∨ m = 0
h : m = 0
⊢ n + 1 ≠ 0
Tactic:
exact Nat.succ_ne_zero _
State after:
no goals

State before:
case succ.mpr
m n : Nat
ih : m ^ n = 0 ↔ m = 0 ∧ n ≠ 0
⊢ m = 0 ∧ n + 1 ≠ 0 → m ^ n = 0 ∨ m = 0
Tactic:
intro ⟨h, _⟩
State after:
case succ.mpr
m n : Nat
ih : m ^ n = 0 ↔ m = 0 ∧ n ≠ 0
h : m = 0
right✝ : n + 1 ≠ 0
⊢ m ^ n = 0 ∨ m = 0

State before:
case succ.mpr
m n : Nat
ih : m ^ n = 0 ↔ m = 0 ∧ n ≠ 0
h : m = 0
right✝ : n + 1 ≠ 0
⊢ m ^ n = 0 ∨ m = 0
Tactic:
exact .inr h
State after:
no goals