R : Type u_2
K : Type u_3
L : Type ?u.841605
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
K' : Type u_1
inst✝² : Field K'
inst✝¹ : Algebra R K'
inst✝ : IsFractionRing R K'
I : (FractionalIdeal R⁰ K)ˣ
⊢ ↑(QuotientGroup.mk' (MonoidHom.range (toPrincipalIdeal R (FractionRing R))))
      (↑(Units.map ↑(canonicalEquiv R⁰ K (FractionRing R))) I) =
    ↑mk I
R : Type u_2
K : Type u_3
L : Type ?u.841605
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
K' : Type u_1
inst✝² : Field K'
inst✝¹ : Algebra R K'
inst✝ : IsFractionRing R K'
I : (FractionalIdeal R⁰ K)ˣ
⊢ ↑mk (↑(Units.map ↑(canonicalEquiv R⁰ K K')) I) = ↑mk I
rw [ClassGroup.mk, MonoidHom.comp_apply, ← MonoidHom.comp_apply (Units.map _), ← Units.map_comp, ←
    RingEquiv.coe_monoidHom_trans, FractionalIdeal.canonicalEquiv_trans_canonicalEquiv]
no goals
R : Type u_2
K : Type u_3
L : Type ?u.841605
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
K' : Type u_1
inst✝² : Field K'
inst✝¹ : Algebra R K'
inst✝ : IsFractionRing R K'
I : (FractionalIdeal R⁰ K)ˣ
⊢ ↑(QuotientGroup.mk' (MonoidHom.range (toPrincipalIdeal R (FractionRing R))))
      (↑(Units.map ↑(canonicalEquiv R⁰ K (FractionRing R))) I) =
    ↑mk I
rfl