R : Type u_1
K : Type u_2
L : Type ?u.1295805
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)⁰ }
⊢ ↑(QuotientGroup.mk' (MonoidHom.range (toPrincipalIdeal R K)))
      (↑(Units.mapEquiv ↑(canonicalEquiv R⁰ (FractionRing R) K)) (↑(FractionalIdeal.mk0 (FractionRing R)) I)) =
    ↑(QuotientGroup.mk' (MonoidHom.range (toPrincipalIdeal R K))) (↑(FractionalIdeal.mk0 K) I)
R : Type u_1
K : Type u_2
L : Type ?u.1295805
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)⁰ }
⊢ ↑(equiv K) (↑mk0 I) = ↑(QuotientGroup.mk' (MonoidHom.range (toPrincipalIdeal R K))) (↑(FractionalIdeal.mk0 K) I)
rw [ClassGroup.mk0, MonoidHom.comp_apply, ClassGroup.equiv_mk]
case h.e_6.h
R : Type u_1
K : Type u_2
L : Type ?u.1295805
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)⁰ }
⊢ ↑(Units.mapEquiv ↑(canonicalEquiv R⁰ (FractionRing R) K)) (↑(FractionalIdeal.mk0 (FractionRing R)) I) =
    ↑(FractionalIdeal.mk0 K) I
R : Type u_1
K : Type u_2
L : Type ?u.1295805
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)⁰ }
⊢ ↑(QuotientGroup.mk' (MonoidHom.range (toPrincipalIdeal R K)))
      (↑(Units.mapEquiv ↑(canonicalEquiv R⁰ (FractionRing R) K)) (↑(FractionalIdeal.mk0 (FractionRing R)) I)) =
    ↑(QuotientGroup.mk' (MonoidHom.range (toPrincipalIdeal R K))) (↑(FractionalIdeal.mk0 K) I)
congr 1
no goals
case h.e_6.h
R : Type u_1
K : Type u_2
L : Type ?u.1295805
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)⁰ }
⊢ ↑(Units.mapEquiv ↑(canonicalEquiv R⁰ (FractionRing R) K)) (↑(FractionalIdeal.mk0 (FractionRing R)) I) =
    ↑(FractionalIdeal.mk0 K) I
simp [← Units.eq_iff]