Theorem: Ideal.mem_pow_eq_zero (DividedPowers/ForMathlib/AlgebraLemmas.lean)

State before:
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
n m : ℕ
hnI : I ^ n = 0
hmn : n ≤ m
x : A
hx : x ∈ I
⊢ x ^ m = 0
Tactic:
have hxn : x ^ n = 0 := by
  rw [Ideal.zero_eq_bot] at hnI
  rw [← Ideal.mem_bot, ← hnI]
  exact Ideal.pow_mem_pow hx n
State after:
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
n m : ℕ
hnI : I ^ n = 0
hmn : n ≤ m
x : A
hx : x ∈ I
hxn : x ^ n = 0
⊢ x ^ m = 0

State before:
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
n m : ℕ
hnI : I ^ n = 0
hmn : n ≤ m
x : A
hx : x ∈ I
hxn : x ^ n = 0
⊢ x ^ m = 0
Tactic:
obtain ⟨c, hc⟩ := Nat.exists_eq_add_of_le hmn
State after:
case intro
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
n m : ℕ
hnI : I ^ n = 0
hmn : n ≤ m
x : A
hx : x ∈ I
hxn : x ^ n = 0
c : ℕ
hc : m = n + c
⊢ x ^ m = 0

State before:
case intro
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
n m : ℕ
hnI : I ^ n = 0
hmn : n ≤ m
x : A
hx : x ∈ I
hxn : x ^ n = 0
c : ℕ
hc : m = n + c
⊢ x ^ m = 0
Tactic:
rw [hc, pow_add, hxn, MulZeroClass.zero_mul]
State after:
no goals

State before:
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
n m : ℕ
hnI : I ^ n = 0
hmn : n ≤ m
x : A
hx : x ∈ I
⊢ x ^ n = 0
Tactic:
rw [Ideal.zero_eq_bot] at hnI
State after:
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
n m : ℕ
hnI : I ^ n = ⊥
hmn : n ≤ m
x : A
hx : x ∈ I
⊢ x ^ n = 0

State before:
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
n m : ℕ
hnI : I ^ n = ⊥
hmn : n ≤ m
x : A
hx : x ∈ I
⊢ x ^ n = 0
Tactic:
rw [← Ideal.mem_bot, ← hnI]
State after:
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
n m : ℕ
hnI : I ^ n = ⊥
hmn : n ≤ m
x : A
hx : x ∈ I
⊢ x ^ n ∈ I ^ n

State before:
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
n m : ℕ
hnI : I ^ n = ⊥
hmn : n ≤ m
x : A
hx : x ∈ I
⊢ x ^ n ∈ I ^ n
Tactic:
exact Ideal.pow_mem_pow hx n
State after:
no goals