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

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

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

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

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

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

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

State before:
case succ.mp
m n : Nat
ih : m ^ n = 1 ↔ m = 1 ∨ n = 0
left✝ : m ^ n = 1
h : m = 1
⊢ m = 1 ∨ n + 1 = 0
Tactic:
exact .inl h
State after:
no goals

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

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

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

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

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