Theorem: DividedPowers.OfInvertibleFactorial.dpow_eq_of_not_mem (DividedPowers/RatAlgebra.lean)

State before:
A : Type u_1
inst✝ : CommSemiring A
I✝ I : Ideal A
m : ℕ
x : A
hx : x ∉ I
⊢ dpow I m x = 0
Tactic:
simp only [dpow]
State after:
A : Type u_1
inst✝ : CommSemiring A
I✝ I : Ideal A
m : ℕ
x : A
hx : x ∉ I
⊢ (if x ∈ I then Ring.inverse ↑m ! * x ^ m else 0) = 0

State before:
A : Type u_1
inst✝ : CommSemiring A
I✝ I : Ideal A
m : ℕ
x : A
hx : x ∉ I
⊢ (if x ∈ I then Ring.inverse ↑m ! * x ^ m else 0) = 0
Tactic:
rw [if_neg hx]
State after:
no goals