Theorem: DividedPowers.SubDPIdeal.le_generatedDpow (DividedPowers/SubDPIdeal.lean)

State before:
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
S : Set A
hS : S ⊆ ↑I
x : A
hx : x ∈ S
⊢ x = hI.dpow 1 x
Tactic:
rw [hI.dpow_one (hS hx)]
State after:
no goals