R : Type u_2
K : Type u_3
L : Type ?u.741973
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 K')))
      (↑(Units.mapEquiv (RingEquiv.toMulEquiv (canonicalEquiv R⁰ (FractionRing R) K')))
        (↑(Units.map ↑(canonicalEquiv R⁰ K (FractionRing R))) I)) =
    ↑(QuotientGroup.mk' (MonoidHom.range (toPrincipalIdeal R K'))) (↑(Units.mapEquiv ↑(canonicalEquiv R⁰ K K')) I)
R : Type u_2
K : Type u_3
L : Type ?u.741973
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)ˣ
⊢ ↑(equiv K') (↑mk I) =
    ↑(QuotientGroup.mk' (MonoidHom.range (toPrincipalIdeal R K'))) (↑(Units.mapEquiv ↑(canonicalEquiv R⁰ K K')) I)
rw [ClassGroup.equiv, ClassGroup.mk, MonoidHom.comp_apply, QuotientGroup.congr_mk']
case h.e_6.h
R : Type u_2
K : Type u_3
L : Type ?u.741973
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)ˣ
⊢ ↑(Units.mapEquiv (RingEquiv.toMulEquiv (canonicalEquiv R⁰ (FractionRing R) K')))
      (↑(Units.map ↑(canonicalEquiv R⁰ K (FractionRing R))) I) =
    ↑(Units.mapEquiv ↑(canonicalEquiv R⁰ K K')) I
R : Type u_2
K : Type u_3
L : Type ?u.741973
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 K')))
      (↑(Units.mapEquiv (RingEquiv.toMulEquiv (canonicalEquiv R⁰ (FractionRing R) K')))
        (↑(Units.map ↑(canonicalEquiv R⁰ K (FractionRing R))) I)) =
    ↑(QuotientGroup.mk' (MonoidHom.range (toPrincipalIdeal R K'))) (↑(Units.mapEquiv ↑(canonicalEquiv R⁰ K K')) I)
congr
case h.e_6.h
R : Type u_2
K : Type u_3
L : Type ?u.741973
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)ˣ
⊢ ↑(RingEquiv.toMulEquiv (canonicalEquiv R⁰ (FractionRing R) K')) (↑↑(canonicalEquiv R⁰ K (FractionRing R)) ↑I) =
    ↑↑(canonicalEquiv R⁰ K K') ↑I
case h.e_6.h
R : Type u_2
K : Type u_3
L : Type ?u.741973
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)ˣ
⊢ ↑(Units.mapEquiv (RingEquiv.toMulEquiv (canonicalEquiv R⁰ (FractionRing R) K')))
      (↑(Units.map ↑(canonicalEquiv R⁰ K (FractionRing R))) I) =
    ↑(Units.mapEquiv ↑(canonicalEquiv R⁰ K K')) I
rw [← Units.eq_iff, Units.coe_mapEquiv, Units.coe_mapEquiv, Units.coe_map]
no goals
case h.e_6.h
R : Type u_2
K : Type u_3
L : Type ?u.741973
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)ˣ
⊢ ↑(RingEquiv.toMulEquiv (canonicalEquiv R⁰ (FractionRing R) K')) (↑↑(canonicalEquiv R⁰ K (FractionRing R)) ↑I) =
    ↑↑(canonicalEquiv R⁰ K K') ↑I
exact FractionalIdeal.canonicalEquiv_canonicalEquiv _ _ _ _ _