-- 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)ˣ
h :
  Eq.{u_3 + 1} (α := (FractionalIdeal.{u_1, u_3} (R := R) R⁰ K')ˣ)
    ((Units.mapEquiv (RingEquiv.toMulEquiv (canonicalEquiv R⁰ (FractionRing R) K')) :
          (a : (FractionalIdeal R⁰ (FractionRing R))ˣ) → (FractionalIdeal R⁰ K')ˣ)
        (((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) :
      (FractionalIdeal.{u_1, u_3} (R := R) R⁰ K')ˣ)
    (((Units.mapEquiv (↑(canonicalEquiv R⁰ K K') : FractionalIdeal R⁰ K ≃* FractionalIdeal R⁰ K') :
            MulEquiv.{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 :
      (FractionalIdeal.{u_1, u_3} (R := R) R⁰ K')ˣ)
⊢ Eq (α :=
    HasQuotient.Quotient (FractionalIdeal.{u_1, u_3} (R := R) R⁰ K')ˣ (B :=
      Subgroup (FractionalIdeal.{u_1, u_3} (R := R) R⁰ K')ˣ) (MonoidHom.range (toPrincipalIdeal R K')))
    ((QuotientGroup.mk' (MonoidHom.range (toPrincipalIdeal R K')) :
          (a : (FractionalIdeal R⁰ K')ˣ) → (FractionalIdeal R⁰ K')ˣ ⧸ (toPrincipalIdeal R K').range)
        ((Units.mapEquiv (RingEquiv.toMulEquiv (canonicalEquiv R⁰ (FractionRing R) K')) :
            (a : (FractionalIdeal R⁰ (FractionRing R))ˣ) → (FractionalIdeal R⁰ K')ˣ)
          (((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.{u_1, u_3} (R := R) R⁰ K')ˣ (B :=
        Subgroup (FractionalIdeal.{u_1, u_3} (R := R) R⁰ K')ˣ) (MonoidHom.range (toPrincipalIdeal R K')))
    ((QuotientGroup.mk' (MonoidHom.range (toPrincipalIdeal R K')) :
          (a : (FractionalIdeal R⁰ K')ˣ) → (FractionalIdeal R⁰ K')ˣ ⧸ (toPrincipalIdeal R K').range)
        (((Units.mapEquiv (↑(canonicalEquiv R⁰ K K') : FractionalIdeal R⁰ K ≃* FractionalIdeal R⁰ K') :
              MulEquiv.{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.{u_1, u_3} (R := R) R⁰ K')ˣ (B :=
        Subgroup (FractionalIdeal.{u_1, u_3} (R := R) R⁰ K')ˣ) (MonoidHom.range (toPrincipalIdeal R K')))

Tactic:
congr