no goals
R : Type u_1
K : Type u_3
L : Type ?u.985383
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
K' : Type u_2
inst✝² : Field K'
inst✝¹ : Algebra R K'
inst✝ : IsFractionRing R K'
I : { x // x ∈ (Ideal R)⁰ }
⊢ ↑(canonicalEquiv R⁰ K K') ↑(↑(mk0 K) I) = ↑(↑(mk0 K') I)
simp only [FractionalIdeal.coe_mk0, FractionalIdeal.canonicalEquiv_coeIdeal]