Theorem: DividedPowers.OfSquareZero.dpow_of_two_le (DividedPowers/RatAlgebra.lean)

State before:
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI2 : I ^ 2 = 0
n : ℕ
hn : 2 ≤ n
a : A
⊢ (dividedPowers hI2).dpow n a = 0
Tactic:
simp only [dividedPowers, OfInvertibleFactorial.dpow_def, ite_eq_right_iff]
State after:
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI2 : I ^ 2 = 0
n : ℕ
hn : 2 ≤ n
a : A
⊢ a ∈ I → Ring.inverse ↑n ! * a ^ n = 0

State before:
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI2 : I ^ 2 = 0
n : ℕ
hn : 2 ≤ n
a : A
⊢ a ∈ I → Ring.inverse ↑n ! * a ^ n = 0
Tactic:
intro ha
State after:
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI2 : I ^ 2 = 0
n : ℕ
hn : 2 ≤ n
a : A
ha : a ∈ I
⊢ Ring.inverse ↑n ! * a ^ n = 0

State before:
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI2 : I ^ 2 = 0
n : ℕ
hn : 2 ≤ n
a : A
ha : a ∈ I
⊢ Ring.inverse ↑n ! * a ^ n = 0
Tactic:
suffices h : a ^ n = 0 by
  rw [h, mul_zero]
State after:
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI2 : I ^ 2 = 0
n : ℕ
hn : 2 ≤ n
a : A
ha : a ∈ I
⊢ a ^ n = 0

State before:
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI2 : I ^ 2 = 0
n : ℕ
hn : 2 ≤ n
a : A
ha : a ∈ I
⊢ a ^ n = 0
Tactic:
exact Ideal.mem_pow_eq_zero 2 n hI2 hn ha
State after:
no goals

State before:
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI2 : I ^ 2 = 0
n : ℕ
hn : 2 ≤ n
a : A
ha : a ∈ I
h : a ^ n = 0
⊢ Ring.inverse ↑n ! * a ^ n = 0
Tactic:
rw [h, mul_zero]
State after:
no goals