Theorem: DividedPowers.Quotient.isSubDPIdeal_aux (DividedPowers/SubDPIdeal.lean)

State before:
A : Type u_1
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hIJ : hI.isSubDPIdeal (J ⊓ I)
⊢ hI.isSubDPIdeal (RingHom.ker (Ideal.Quotient.mk J) ⊓ I)
Tactic:
simpa [Ideal.mk_ker] using hIJ
State after:
no goals