Theorem: DividedPowers.OfInvertibleFactorial.dpow_eq_of_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 = Ring.inverse ↑m ! * x ^ m
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) = Ring.inverse ↑m ! * x ^ m

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) = Ring.inverse ↑m ! * x ^ m
Tactic:
rw [if_pos hx]
State after:
no goals