no goals
R : Type u_1
K : Type u_2
L : Type ?u.1219112
inst✝¹¹ : CommRing R
inst✝¹⁰ : Field K
inst✝⁹ : Field L
inst✝⁸ : DecidableEq L
inst✝⁷ : Algebra R K
inst✝⁶ : IsFractionRing R K
inst✝⁵ : Algebra K L
inst✝⁴ : FiniteDimensional K L
inst✝³ : Algebra R L
inst✝² : IsScalarTower R K L
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
I : { x // x ∈ (Ideal R)⁰ }
⊢ ↑mk (↑(FractionalIdeal.mk0 K) I) = ↑mk0 I
rw [ClassGroup.mk0, MonoidHom.comp_apply, ← ClassGroup.mk_canonicalEquiv K (FractionRing R),
  FractionalIdeal.map_canonicalEquiv_mk0]