-- 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
inst_5 : IsDedekindDomain R
I : ↥(Ideal R)⁰
rw :
  Eq.{u_1 + 1} (α := ClassGroup R)
    ((mk K : (a : (FractionalIdeal R⁰ K)ˣ) → ClassGroup R)
        ((FractionalIdeal.mk0 K : (a : ↥(Ideal R)⁰) → (FractionalIdeal R⁰ K)ˣ) I) :
      ClassGroup R)
    ((MonoidHom.comp (N := (FractionalIdeal (R := R) R⁰ (FractionRing R))ˣ) (mk (FractionRing R))
            (FractionalIdeal.mk0 (FractionRing R)) :
          (a : ↥(Ideal R)⁰) → ClassGroup R)
        I :
      ClassGroup R)
rw₁ :
  Eq (α := ClassGroup R)
    ((mk K : (a : (FractionalIdeal R⁰ K)ˣ) → ClassGroup R)
        ((FractionalIdeal.mk0 K : (a : ↥(Ideal R)⁰) → (FractionalIdeal R⁰ K)ˣ) I) :
      ClassGroup R)
    ((mk (FractionRing R) : (a : (FractionalIdeal R⁰ (FractionRing R))ˣ) → ClassGroup R)
        (((FractionalIdeal.mk0 (FractionRing R) : ↥(Ideal R)⁰ →* (FractionalIdeal (R := R) R⁰ (FractionRing R))ˣ) :
            (a : ↥(Ideal R)⁰) → (FractionalIdeal R⁰ (FractionRing R))ˣ)
          I) :
      ClassGroup R)
rw₂ :
  Eq.{u_1 + 1} (α := ClassGroup R)
    ((mk (FractionRing R) : (a : (FractionalIdeal R⁰ (FractionRing R))ˣ) → ClassGroup R)
        (((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))ˣ)
          ((FractionalIdeal.mk0 K : (a : ↥(Ideal R)⁰) → (FractionalIdeal R⁰ K)ˣ) I)) :
      ClassGroup R)
    ((mk (FractionRing R) : (a : (FractionalIdeal R⁰ (FractionRing R))ˣ) → ClassGroup R)
        (((FractionalIdeal.mk0 (FractionRing R) : ↥(Ideal R)⁰ →* (FractionalIdeal (R := R) R⁰ (FractionRing R))ˣ) :
            (a : ↥(Ideal R)⁰) → (FractionalIdeal R⁰ (FractionRing R))ˣ)
          I) :
      ClassGroup R)
rw₃ rw₄ :
  Eq (α := ClassGroup R)
    ((mk (FractionRing R) : (a : (FractionalIdeal R⁰ (FractionRing R))ˣ) → ClassGroup R)
        ((FractionalIdeal.mk0 (FractionRing R) : (a : ↥(Ideal R)⁰) → (FractionalIdeal R⁰ (FractionRing R))ˣ) I) :
      ClassGroup R)
    ((mk (FractionRing R) : (a : (FractionalIdeal R⁰ (FractionRing R))ˣ) → ClassGroup R)
        (((FractionalIdeal.mk0 (FractionRing R) : ↥(Ideal R)⁰ →* (FractionalIdeal (R := R) R⁰ (FractionRing R))ˣ) :
            (a : ↥(Ideal R)⁰) → (FractionalIdeal R⁰ (FractionRing R))ˣ)
          I) :
      ClassGroup R)
⊢ Eq.{u_1 + 1} (α := ClassGroup R)
    ((mk K : (a : (FractionalIdeal R⁰ K)ˣ) → ClassGroup R)
        ((FractionalIdeal.mk0 K : (a : ↥(Ideal R)⁰) → (FractionalIdeal R⁰ K)ˣ) I) :
      ClassGroup R)
    ((mk0 : (a : ↥(Ideal R)⁰) → ClassGroup R) I : ClassGroup R)

Tactic:
rw [ClassGroup.mk0, MonoidHom.comp_apply, ← ClassGroup.mk_canonicalEquiv K (FractionRing R),
    FractionalIdeal.map_canonicalEquiv_mk0]

Premises used: FractionRing, ClassGroup.mk0, FractionalIdeal.map_canonicalEquiv_mk0, ClassGroup.mk_canonicalEquiv, MonoidHom.comp_apply