Theorem: powNeOneIff' (FromTheBook/Ch02/Bertrand/CentralBinom.lean)

State before:
x i : ℕ
⊢ x ^ i ≠ 1 ↔ i ≠ 0 ∧ x ≠ 1
Tactic:
cases i with
| zero => simp
| succ i =>
  simp [not_iff_not]
  simp [pow_succ]  intro hx
  simp [hx]
State after:
no goals

State before:
case zero
x : ℕ
⊢ x ^ Nat.zero ≠ 1 ↔ Nat.zero ≠ 0 ∧ x ≠ 1
Tactic:
simp
State after:
no goals

State before:
case succ
x i : ℕ
⊢ x ^ Nat.succ i ≠ 1 ↔ Nat.succ i ≠ 0 ∧ x ≠ 1
Tactic:
simp [not_iff_not]
State after:
case succ
x i : ℕ
⊢ x ^ Nat.succ i = 1 ↔ x = 1

State before:
case succ
x i : ℕ
⊢ x ^ Nat.succ i = 1 ↔ x = 1
Tactic:
simp [pow_succ]
State after:
case succ
x i : ℕ
⊢ x = 1 → x ^ i = 1

State before:
case succ
x i : ℕ
⊢ x = 1 → x ^ i = 1
Tactic:
intro hx
State after:
case succ
x i : ℕ
hx : x = 1
⊢ x ^ i = 1

State before:
case succ
x i : ℕ
hx : x = 1
⊢ x ^ i = 1
Tactic:
simp [hx]
State after:
no goals