no goals
R : Type u
inst✝¹ : CommRing R
S : Type v
inst✝ : CommRing S
f : R →+* S
p : Ideal R
P : Ideal S
hfp : NeZero e
i : ℕ
a : S
a_mem : a ∈ P ^ i
x : S
⊢ quotientToQuotientRangePowQuotSuccAux f p P a_mem (Submodule.Quotient.mk x) =
    Submodule.Quotient.mk
      { val := ↑(Quotient.mk (P ^ e)) (x * a),
        property := (_ : ↑(Quotient.mk (P ^ e)) (x * a) ∈ map (Quotient.mk (P ^ e)) (P ^ i)) }
apply Quotient.map'_mk''