-- Module: Mathlib.RingTheory.ClassGroup
Goal:
R : Type u_1
K : Type u_2
inst : CommRing R
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : IsFractionRing R K
inst_4 : IsDomain R
K' : Type u_3
inst_5 : Field K'
inst_6 : Algebra R K'
inst_7 : IsFractionRing R K'
I : (FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)ˣ
rw :
  Eq (α := ClassGroup R)
    ((QuotientGroup.mk' (MonoidHom.range (toPrincipalIdeal R (FractionRing R))) :
          (a : (FractionalIdeal R⁰ (FractionRing R))ˣ) →
            (FractionalIdeal R⁰ (FractionRing R))ˣ ⧸ (toPrincipalIdeal R (FractionRing R)).range)
        (((Units.map
                (↑(canonicalEquiv R⁰ K' (FractionRing R)) :
                  FractionalIdeal R⁰ K' →* FractionalIdeal R⁰ (FractionRing R)) :
              MonoidHom.{u_3, u_1} (FractionalIdeal.{u_1, u_3} (R := R) R⁰ K')ˣ
                (FractionalIdeal (R := R) R⁰ (FractionRing R))ˣ) :
            (a : (FractionalIdeal R⁰ K')ˣ) → (FractionalIdeal R⁰ (FractionRing R))ˣ)
          (((Units.map (↑(canonicalEquiv R⁰ K K') : FractionalIdeal R⁰ K →* FractionalIdeal R⁰ K') :
                MonoidHom.{u_2, u_3} (FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)ˣ
                  (FractionalIdeal.{u_1, u_3} (R := R) R⁰ K')ˣ) :
              (a : (FractionalIdeal R⁰ K)ˣ) → (FractionalIdeal R⁰ K')ˣ)
            I)) :
      HasQuotient.Quotient (FractionalIdeal (R := R) R⁰ (FractionRing R))ˣ (B :=
        Subgroup (FractionalIdeal (R := R) R⁰ (FractionRing R))ˣ)
        (MonoidHom.range (toPrincipalIdeal R (FractionRing R))))
    ((mk K : (a : (FractionalIdeal R⁰ K)ˣ) → ClassGroup R) I : ClassGroup R)
rw₁ :
  Eq (α := ClassGroup R)
    ((QuotientGroup.mk' (MonoidHom.range (toPrincipalIdeal R (FractionRing R))) :
          (a : (FractionalIdeal R⁰ (FractionRing R))ˣ) →
            (FractionalIdeal R⁰ (FractionRing R))ˣ ⧸ (toPrincipalIdeal R (FractionRing R)).range)
        (((Units.map
                (↑(canonicalEquiv R⁰ K' (FractionRing R)) :
                  FractionalIdeal R⁰ K' →* FractionalIdeal R⁰ (FractionRing R)) :
              MonoidHom.{u_3, u_1} (FractionalIdeal.{u_1, u_3} (R := R) R⁰ K')ˣ
                (FractionalIdeal (R := R) R⁰ (FractionRing R))ˣ) :
            (a : (FractionalIdeal R⁰ K')ˣ) → (FractionalIdeal R⁰ (FractionRing R))ˣ)
          (((Units.map (↑(canonicalEquiv R⁰ K K') : FractionalIdeal R⁰ K →* FractionalIdeal R⁰ K') :
                MonoidHom.{u_2, u_3} (FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)ˣ
                  (FractionalIdeal.{u_1, u_3} (R := R) R⁰ K')ˣ) :
              (a : (FractionalIdeal R⁰ K)ˣ) → (FractionalIdeal R⁰ K')ˣ)
            I)) :
      HasQuotient.Quotient (FractionalIdeal (R := R) R⁰ (FractionRing R))ˣ (B :=
        Subgroup (FractionalIdeal (R := R) R⁰ (FractionRing R))ˣ)
        (MonoidHom.range (toPrincipalIdeal R (FractionRing R))))
    ((QuotientGroup.mk' (MonoidHom.range (toPrincipalIdeal R (FractionRing R))) :
          (a : (FractionalIdeal R⁰ (FractionRing R))ˣ) →
            (FractionalIdeal R⁰ (FractionRing R))ˣ ⧸ (toPrincipalIdeal R (FractionRing R)).range)
        (((Units.map
                (↑(canonicalEquiv R⁰ K (FractionRing R)) :
                  FractionalIdeal R⁰ K →* FractionalIdeal R⁰ (FractionRing R)) :
              MonoidHom.{u_2, u_1} (FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)ˣ
                (FractionalIdeal (R := R) R⁰ (FractionRing R))ˣ) :
            (a : (FractionalIdeal R⁰ K)ˣ) → (FractionalIdeal R⁰ (FractionRing R))ˣ)
          I) :
      HasQuotient.Quotient (FractionalIdeal (R := R) R⁰ (FractionRing R))ˣ (B :=
        Subgroup (FractionalIdeal (R := R) R⁰ (FractionRing R))ˣ)
        (MonoidHom.range (toPrincipalIdeal R (FractionRing R))))
rw₂ :
  Eq (α := ClassGroup R)
    ((QuotientGroup.mk' (MonoidHom.range (toPrincipalIdeal R (FractionRing R))) :
          (a : (FractionalIdeal R⁰ (FractionRing R))ˣ) →
            (FractionalIdeal R⁰ (FractionRing R))ˣ ⧸ (toPrincipalIdeal R (FractionRing R)).range)
        (((MonoidHom.comp (N := (FractionalIdeal.{u_1, u_3} (R := R) R⁰ K')ˣ)
                (Units.map
                  (↑(canonicalEquiv R⁰ K' (FractionRing R)) :
                    FractionalIdeal R⁰ K' →* FractionalIdeal R⁰ (FractionRing R)))
                (Units.map (↑(canonicalEquiv R⁰ K K') : FractionalIdeal R⁰ K →* FractionalIdeal R⁰ K')) :
              MonoidHom.{u_2, u_1} (FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)ˣ
                (FractionalIdeal (R := R) R⁰ (FractionRing R))ˣ) :
            (a : (FractionalIdeal R⁰ K)ˣ) → (FractionalIdeal R⁰ (FractionRing R))ˣ)
          I) :
      HasQuotient.Quotient (FractionalIdeal (R := R) R⁰ (FractionRing R))ˣ (B :=
        Subgroup (FractionalIdeal (R := R) R⁰ (FractionRing R))ˣ)
        (MonoidHom.range (toPrincipalIdeal R (FractionRing R))))
    ((QuotientGroup.mk' (MonoidHom.range (toPrincipalIdeal R (FractionRing R))) :
          (a : (FractionalIdeal R⁰ (FractionRing R))ˣ) →
            (FractionalIdeal R⁰ (FractionRing R))ˣ ⧸ (toPrincipalIdeal R (FractionRing R)).range)
        (((Units.map
                (↑(canonicalEquiv R⁰ K (FractionRing R)) :
                  FractionalIdeal R⁰ K →* FractionalIdeal R⁰ (FractionRing R)) :
              MonoidHom.{u_2, u_1} (FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)ˣ
                (FractionalIdeal (R := R) R⁰ (FractionRing R))ˣ) :
            (a : (FractionalIdeal R⁰ K)ˣ) → (FractionalIdeal R⁰ (FractionRing R))ˣ)
          I) :
      HasQuotient.Quotient (FractionalIdeal (R := R) R⁰ (FractionRing R))ˣ (B :=
        Subgroup (FractionalIdeal (R := R) R⁰ (FractionRing R))ˣ)
        (MonoidHom.range (toPrincipalIdeal R (FractionRing R))))
rw₃ :
  Eq (α := ClassGroup R)
    ((QuotientGroup.mk' (MonoidHom.range (toPrincipalIdeal R (FractionRing R))) :
          (a : (FractionalIdeal R⁰ (FractionRing R))ˣ) →
            (FractionalIdeal R⁰ (FractionRing R))ˣ ⧸ (toPrincipalIdeal R (FractionRing R)).range)
        (((Units.map
                (MonoidHom.comp
                  (↑(canonicalEquiv R⁰ K' (FractionRing R)) :
                    FractionalIdeal R⁰ K' →* FractionalIdeal R⁰ (FractionRing R))
                  (↑(canonicalEquiv R⁰ K K') : FractionalIdeal R⁰ K →* FractionalIdeal R⁰ K')) :
              MonoidHom.{u_2, u_1} (FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)ˣ
                (FractionalIdeal (R := R) R⁰ (FractionRing R))ˣ) :
            (a : (FractionalIdeal R⁰ K)ˣ) → (FractionalIdeal R⁰ (FractionRing R))ˣ)
          I) :
      HasQuotient.Quotient (FractionalIdeal (R := R) R⁰ (FractionRing R))ˣ (B :=
        Subgroup (FractionalIdeal (R := R) R⁰ (FractionRing R))ˣ)
        (MonoidHom.range (toPrincipalIdeal R (FractionRing R))))
    ((QuotientGroup.mk' (MonoidHom.range (toPrincipalIdeal R (FractionRing R))) :
          (a : (FractionalIdeal R⁰ (FractionRing R))ˣ) →
            (FractionalIdeal R⁰ (FractionRing R))ˣ ⧸ (toPrincipalIdeal R (FractionRing R)).range)
        (((Units.map
                (↑(canonicalEquiv R⁰ K (FractionRing R)) :
                  FractionalIdeal R⁰ K →* FractionalIdeal R⁰ (FractionRing R)) :
              MonoidHom.{u_2, u_1} (FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)ˣ
                (FractionalIdeal (R := R) R⁰ (FractionRing R))ˣ) :
            (a : (FractionalIdeal R⁰ K)ˣ) → (FractionalIdeal R⁰ (FractionRing R))ˣ)
          I) :
      HasQuotient.Quotient (FractionalIdeal (R := R) R⁰ (FractionRing R))ˣ (B :=
        Subgroup (FractionalIdeal (R := R) R⁰ (FractionRing R))ˣ)
        (MonoidHom.range (toPrincipalIdeal R (FractionRing R))))
rw₄ :
  Eq (α := ClassGroup R)
    ((QuotientGroup.mk' (MonoidHom.range (toPrincipalIdeal R (FractionRing R))) :
          (a : (FractionalIdeal R⁰ (FractionRing R))ˣ) →
            (FractionalIdeal R⁰ (FractionRing R))ˣ ⧸ (toPrincipalIdeal R (FractionRing R)).range)
        (((Units.map
                (↑(RingEquiv.trans (S := FractionalIdeal.{u_1, u_3} (R := R) R⁰ K') (canonicalEquiv R⁰ K K')
                      (canonicalEquiv R⁰ K' (FractionRing R))) :
                  FractionalIdeal R⁰ K →* FractionalIdeal R⁰ (FractionRing R)) :
              MonoidHom.{u_2, u_1} (FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)ˣ
                (FractionalIdeal (R := R) R⁰ (FractionRing R))ˣ) :
            (a : (FractionalIdeal R⁰ K)ˣ) → (FractionalIdeal R⁰ (FractionRing R))ˣ)
          I) :
      HasQuotient.Quotient (FractionalIdeal (R := R) R⁰ (FractionRing R))ˣ (B :=
        Subgroup (FractionalIdeal (R := R) R⁰ (FractionRing R))ˣ)
        (MonoidHom.range (toPrincipalIdeal R (FractionRing R))))
    ((QuotientGroup.mk' (MonoidHom.range (toPrincipalIdeal R (FractionRing R))) :
          (a : (FractionalIdeal R⁰ (FractionRing R))ˣ) →
            (FractionalIdeal R⁰ (FractionRing R))ˣ ⧸ (toPrincipalIdeal R (FractionRing R)).range)
        (((Units.map
                (↑(canonicalEquiv R⁰ K (FractionRing R)) :
                  FractionalIdeal R⁰ K →* FractionalIdeal R⁰ (FractionRing R)) :
              MonoidHom.{u_2, u_1} (FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)ˣ
                (FractionalIdeal (R := R) R⁰ (FractionRing R))ˣ) :
            (a : (FractionalIdeal R⁰ K)ˣ) → (FractionalIdeal R⁰ (FractionRing R))ˣ)
          I) :
      HasQuotient.Quotient (FractionalIdeal (R := R) R⁰ (FractionRing R))ˣ (B :=
        Subgroup (FractionalIdeal (R := R) R⁰ (FractionRing R))ˣ)
        (MonoidHom.range (toPrincipalIdeal R (FractionRing R))))
rw₅ rw₆ :
  Eq (α := ClassGroup R)
    ((QuotientGroup.mk' (MonoidHom.range (toPrincipalIdeal R (FractionRing R))) :
          (a : (FractionalIdeal R⁰ (FractionRing R))ˣ) →
            (FractionalIdeal R⁰ (FractionRing R))ˣ ⧸ (toPrincipalIdeal R (FractionRing R)).range)
        (((Units.map
                (↑(canonicalEquiv R⁰ K (FractionRing R)) :
                  FractionalIdeal R⁰ K →* FractionalIdeal R⁰ (FractionRing R)) :
              MonoidHom.{u_2, u_1} (FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)ˣ
                (FractionalIdeal (R := R) R⁰ (FractionRing R))ˣ) :
            (a : (FractionalIdeal R⁰ K)ˣ) → (FractionalIdeal R⁰ (FractionRing R))ˣ)
          I) :
      HasQuotient.Quotient (FractionalIdeal (R := R) R⁰ (FractionRing R))ˣ (B :=
        Subgroup (FractionalIdeal (R := R) R⁰ (FractionRing R))ˣ)
        (MonoidHom.range (toPrincipalIdeal R (FractionRing R))))
    ((QuotientGroup.mk' (MonoidHom.range (toPrincipalIdeal R (FractionRing R))) :
          (a : (FractionalIdeal R⁰ (FractionRing R))ˣ) →
            (FractionalIdeal R⁰ (FractionRing R))ˣ ⧸ (toPrincipalIdeal R (FractionRing R)).range)
        (((Units.map
                (↑(canonicalEquiv R⁰ K (FractionRing R)) :
                  FractionalIdeal R⁰ K →* FractionalIdeal R⁰ (FractionRing R)) :
              MonoidHom.{u_2, u_1} (FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)ˣ
                (FractionalIdeal (R := R) R⁰ (FractionRing R))ˣ) :
            (a : (FractionalIdeal R⁰ K)ˣ) → (FractionalIdeal R⁰ (FractionRing R))ˣ)
          I) :
      HasQuotient.Quotient (FractionalIdeal (R := R) R⁰ (FractionRing R))ˣ (B :=
        Subgroup (FractionalIdeal (R := R) R⁰ (FractionRing R))ˣ)
        (MonoidHom.range (toPrincipalIdeal R (FractionRing R))))
⊢ Eq.{u_1 + 1} (α := ClassGroup R)
    ((mk K' : (a : (FractionalIdeal R⁰ K')ˣ) → ClassGroup R)
        (((Units.map (↑(canonicalEquiv R⁰ K K') : FractionalIdeal R⁰ K →* FractionalIdeal R⁰ K') :
              MonoidHom.{u_2, u_3} (FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)ˣ
                (FractionalIdeal.{u_1, u_3} (R := R) R⁰ K')ˣ) :
            (a : (FractionalIdeal R⁰ K)ˣ) → (FractionalIdeal R⁰ K')ˣ)
          I) :
      ClassGroup R)
    ((mk K : (a : (FractionalIdeal R⁰ K)ˣ) → ClassGroup R) I : ClassGroup R)

Tactic:
rw [ClassGroup.mk_def, ClassGroup.mk_def, ← MonoidHom.comp_apply (Units.map _),
      ← Units.map_comp, ← RingEquiv.coe_monoidHom_trans,
      FractionalIdeal.canonicalEquiv_trans_canonicalEquiv]

Premises used: FractionalIdeal.canonicalEquiv_trans_canonicalEquiv, Units.map_comp, RingEquiv.coe_monoidHom_trans, ClassGroup.mk_def, Units.map, MonoidHom.comp_apply