no goals
R : Type ?u.977234
A : Type u_1
K : Type ?u.977240
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Field K
inst✝¹ : IsDomain A
inst✝ : IsDedekindDomain A
I : Ideal R
J : Ideal A
X : ↑{p | p ∣ J}
⊢ ↑(idealFactorsFunOfQuotHom (_ : Function.Surjective ↑(RingHom.id (A ⧸ J)))) X = ↑OrderHom.id X
simp only [idealFactorsFunOfQuotHom, map_id, OrderHom.coe_fun_mk, OrderHom.id_coe, id.def,
  comap_map_of_surjective (Ideal.Quotient.mk J) Quotient.mk_surjective, ←
  RingHom.ker_eq_comap_bot (Ideal.Quotient.mk J), mk_ker,
  sup_eq_left.mpr (dvd_iff_le.mp X.prop), Subtype.coe_eta]