Theorem: Ideal.pow_eq_bot (DividedPowers/DPAlgebra/Misc.lean)

State before:
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
I : Ideal R
n : ℕ
hn : n ≠ 0
⊢ I ^ n = ⊥ ↔ I = ⊥
Tactic:
induction' n with n ih
State after:
case zero
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
I : Ideal R
hn : 0 ≠ 0
⊢ I ^ 0 = ⊥ ↔ I = ⊥

case succ
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
I : Ideal R
n : ℕ
ih : n ≠ 0 → (I ^ n = ⊥ ↔ I = ⊥)
hn : n + 1 ≠ 0
⊢ I ^ (n + 1) = ⊥ ↔ I = ⊥

State before:
case zero
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
I : Ideal R
hn : 0 ≠ 0
⊢ I ^ 0 = ⊥ ↔ I = ⊥
Tactic:
exfalso
State after:
case zero
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
I : Ideal R
hn : 0 ≠ 0
⊢ False

State before:
case zero
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
I : Ideal R
hn : 0 ≠ 0
⊢ False
Tactic:
exact hn (Eq.refl _)
State after:
no goals

State before:
case succ
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
I : Ideal R
n : ℕ
ih : n ≠ 0 → (I ^ n = ⊥ ↔ I = ⊥)
hn : n + 1 ≠ 0
⊢ I ^ (n + 1) = ⊥ ↔ I = ⊥
Tactic:
by_cases hn0 : n = 0
State after:
case pos
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
I : Ideal R
n : ℕ
ih : n ≠ 0 → (I ^ n = ⊥ ↔ I = ⊥)
hn : n + 1 ≠ 0
hn0 : n = 0
⊢ I ^ (n + 1) = ⊥ ↔ I = ⊥

case neg
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
I : Ideal R
n : ℕ
ih : n ≠ 0 → (I ^ n = ⊥ ↔ I = ⊥)
hn : n + 1 ≠ 0
hn0 : ¬n = 0
⊢ I ^ (n + 1) = ⊥ ↔ I = ⊥

State before:
case pos
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
I : Ideal R
n : ℕ
ih : n ≠ 0 → (I ^ n = ⊥ ↔ I = ⊥)
hn : n + 1 ≠ 0
hn0 : n = 0
⊢ I ^ (n + 1) = ⊥ ↔ I = ⊥
Tactic:
rw [hn0, pow_one]
State after:
no goals

State before:
case neg
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
I : Ideal R
n : ℕ
ih : n ≠ 0 → (I ^ n = ⊥ ↔ I = ⊥)
hn : n + 1 ≠ 0
hn0 : ¬n = 0
⊢ I ^ (n + 1) = ⊥ ↔ I = ⊥
Tactic:
rw [pow_succ, mul_eq_bot, ih hn0, or_self_iff]
State after:
no goals