awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
P : ClassGroup R → Prop
h : ∀ (I : (FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)ˣ), P ((mk K : (a : (FractionalIdeal R⁰ K)ˣ) → ClassGroup R) I)
x : ClassGroup R
I : (FractionalIdeal (R := R) R⁰ (FractionRing R))ˣ
this :
  I =
    (Units.mapEquiv (RingEquiv.toMulEquiv (canonicalEquiv R⁰ K (FractionRing R))) :
        (a : (FractionalIdeal R⁰ K)ˣ) → (FractionalIdeal R⁰ (FractionRing R))ˣ)
      ((Units.mapEquiv (RingEquiv.toMulEquiv (canonicalEquiv R⁰ (FractionRing R) K)) :
          (a : (FractionalIdeal R⁰ (FractionRing R))ˣ) → (FractionalIdeal R⁰ K)ˣ)
        I)
rw :
  P
    (↑((Units.mapEquiv (RingEquiv.toMulEquiv (canonicalEquiv R⁰ K (FractionRing R))) :
            (a : (FractionalIdeal R⁰ K)ˣ) → (FractionalIdeal R⁰ (FractionRing R))ˣ)
          ((Units.mapEquiv (RingEquiv.toMulEquiv (canonicalEquiv R⁰ (FractionRing R) K)) :
              (a : (FractionalIdeal R⁰ (FractionRing R))ˣ) → (FractionalIdeal R⁰ K)ˣ)
            I)) :
      (FractionalIdeal R⁰ (FractionRing R))ˣ ⧸ (toPrincipalIdeal R (FractionRing R)).range)
⊢ P (↑I : (FractionalIdeal R⁰ (FractionRing R))ˣ ⧸ (toPrincipalIdeal R (FractionRing R)).range)

Tactic:
rw [congr_arg (QuotientGroup.mk (s := (toPrincipalIdeal R (FractionRing R)).range)) this]

Premises used: QuotientGroup.mk, congr_arg
-- 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
P : ClassGroup R → Prop
h : ∀ (I : (FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)ˣ), P ((mk K : (a : (FractionalIdeal R⁰ K)ˣ) → ClassGroup R) I)
x : ClassGroup R
I : (FractionalIdeal (R := R) R⁰ (FractionRing R))ˣ
this :
  I =
    (Units.mapEquiv (RingEquiv.toMulEquiv (canonicalEquiv R⁰ K (FractionRing R))) :
        (a : (FractionalIdeal R⁰ K)ˣ) → (FractionalIdeal R⁰ (FractionRing R))ˣ)
      ((Units.mapEquiv (RingEquiv.toMulEquiv (canonicalEquiv R⁰ (FractionRing R) K)) :
          (a : (FractionalIdeal R⁰ (FractionRing R))ˣ) → (FractionalIdeal R⁰ K)ˣ)
        I)
⊢ P
    (↑((Units.mapEquiv (RingEquiv.toMulEquiv (canonicalEquiv R⁰ K (FractionRing R))) :
            (a : (FractionalIdeal R⁰ K)ˣ) → (FractionalIdeal R⁰ (FractionRing R))ˣ)
          ((Units.mapEquiv (RingEquiv.toMulEquiv (canonicalEquiv R⁰ (FractionRing R) K)) :
              (a : (FractionalIdeal R⁰ (FractionRing R))ˣ) → (FractionalIdeal R⁰ K)ˣ)
            I)) :
      (FractionalIdeal R⁰ (FractionRing R))ˣ ⧸ (toPrincipalIdeal R (FractionRing R)).range)

Tactic:
h _
-- 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
P : ClassGroup R → Prop
h : ∀ (I : (FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)ˣ), P ((mk K : (a : (FractionalIdeal R⁰ K)ˣ) → ClassGroup R) I)
x : ClassGroup R
I : (FractionalIdeal (R := R) R⁰ (FractionRing R))ˣ
this :
  I =
    (Units.mapEquiv (RingEquiv.toMulEquiv (canonicalEquiv R⁰ K (FractionRing R))) :
        (a : (FractionalIdeal R⁰ K)ˣ) → (FractionalIdeal R⁰ (FractionRing R))ˣ)
      ((Units.mapEquiv (RingEquiv.toMulEquiv (canonicalEquiv R⁰ (FractionRing R) K)) :
          (a : (FractionalIdeal R⁰ (FractionRing R))ˣ) → (FractionalIdeal R⁰ K)ˣ)
        I)
⊢ P
    (↑((Units.mapEquiv (RingEquiv.toMulEquiv (canonicalEquiv R⁰ K (FractionRing R))) :
            (a : (FractionalIdeal R⁰ K)ˣ) → (FractionalIdeal R⁰ (FractionRing R))ˣ)
          ((Units.mapEquiv (RingEquiv.toMulEquiv (canonicalEquiv R⁰ (FractionRing R) K)) :
              (a : (FractionalIdeal R⁰ (FractionRing R))ˣ) → (FractionalIdeal R⁰ K)ˣ)
            I)) :
      (FractionalIdeal R⁰ (FractionRing R))ˣ ⧸ (toPrincipalIdeal R (FractionRing R)).range)

Tactic:
exact h _
-- 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
h :
  ∀ (I : (FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)ˣ),
    Membership.mem (γ := Subgroup (FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)ˣ)
        (Subgroup.map (G := (FractionalIdeal (R := R) R⁰ (FractionRing R))ˣ)
          (MulEquiv.toMonoidHom (Units.mapEquiv (RingEquiv.toMulEquiv (canonicalEquiv R⁰ (FractionRing R) K))) :
            MonoidHom.{u_1, u_2} (FractionalIdeal (R := R) R⁰ (FractionRing R))ˣ
              (FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)ˣ)
          (MonoidHom.range (toPrincipalIdeal R (FractionRing R)) :
            Subgroup (FractionalIdeal (R := R) R⁰ (FractionRing R))ˣ))
        I ↔
      Membership.mem (γ := Subgroup (FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)ˣ)
        (MonoidHom.range (toPrincipalIdeal R K)) I
⊢ Eq (α := Subgroup (FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)ˣ)
    (Subgroup.map (G := (FractionalIdeal (R := R) R⁰ (FractionRing R))ˣ)
      (MulEquiv.toMonoidHom (Units.mapEquiv (RingEquiv.toMulEquiv (canonicalEquiv R⁰ (FractionRing R) K))) :
        MonoidHom.{u_1, u_2} (FractionalIdeal (R := R) R⁰ (FractionRing R))ˣ
          (FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)ˣ)
      (MonoidHom.range (toPrincipalIdeal R (FractionRing R)) :
        Subgroup (FractionalIdeal (R := R) R⁰ (FractionRing R))ˣ))
    (MonoidHom.range (toPrincipalIdeal R K))

Tactic:
ext I
-- 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
I : (FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)ˣ
h :
  (∃ (x : (FractionalIdeal (R := R) R⁰ (FractionRing R))ˣ),
      (∃ (x_1 : FractionRing R), spanSingleton R⁰ x_1 = (↑x : FractionalIdeal R⁰ (FractionRing R))) ∧
        (MulEquiv.toMonoidHom (Units.mapEquiv (RingEquiv.toMulEquiv (canonicalEquiv R⁰ (FractionRing R) K))) :
              (a : (FractionalIdeal R⁰ (FractionRing R))ˣ) → (FractionalIdeal R⁰ K)ˣ)
            x =
          I) ↔
    ∃ (x : K), spanSingleton R⁰ x = (↑I : FractionalIdeal R⁰ K)
⊢ Membership.mem (γ := Subgroup (FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)ˣ)
      (Subgroup.map (G := (FractionalIdeal (R := R) R⁰ (FractionRing R))ˣ)
        (MulEquiv.toMonoidHom (Units.mapEquiv (RingEquiv.toMulEquiv (canonicalEquiv R⁰ (FractionRing R) K))) :
          MonoidHom.{u_1, u_2} (FractionalIdeal (R := R) R⁰ (FractionRing R))ˣ
            (FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)ˣ)
        (MonoidHom.range (toPrincipalIdeal R (FractionRing R)) :
          Subgroup (FractionalIdeal (R := R) R⁰ (FractionRing R))ˣ))
      I ↔
    Membership.mem (γ := Subgroup (FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)ˣ) (MonoidHom.range (toPrincipalIdeal R K))
      I

Tactic:
simp only [Subgroup.mem_map, mem_principal_ideals_iff]

Premises used: mem_principal_ideals_iff, Subgroup.mem_map
-- 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
I : (FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)ˣ
h :
  (∃ (x : (FractionalIdeal (R := R) R⁰ (FractionRing R))ˣ),
      (∃ (x_1 : FractionRing R), spanSingleton R⁰ x_1 = (↑x : FractionalIdeal R⁰ (FractionRing R))) ∧
        (MulEquiv.toMonoidHom (Units.mapEquiv (RingEquiv.toMulEquiv (canonicalEquiv R⁰ (FractionRing R) K))) :
              (a : (FractionalIdeal R⁰ (FractionRing R))ˣ) → (FractionalIdeal R⁰ K)ˣ)
            x =
          I) →
    ∃ (x : K), spanSingleton R⁰ x = (↑I : FractionalIdeal R⁰ K)
h₁ :
  (∃ (x : K), spanSingleton R⁰ x = (↑I : FractionalIdeal R⁰ K)) →
    ∃ (x : (FractionalIdeal (R := R) R⁰ (FractionRing R))ˣ),
      (∃ (x_1 : FractionRing R), spanSingleton R⁰ x_1 = (↑x : FractionalIdeal R⁰ (FractionRing R))) ∧
        (MulEquiv.toMonoidHom (Units.mapEquiv (RingEquiv.toMulEquiv (canonicalEquiv R⁰ (FractionRing R) K))) :
              (a : (FractionalIdeal R⁰ (FractionRing R))ˣ) → (FractionalIdeal R⁰ K)ˣ)
            x =
          I
⊢ (∃ (x : (FractionalIdeal (R := R) R⁰ (FractionRing R))ˣ),
      (∃ (x_1 : FractionRing R), spanSingleton R⁰ x_1 = (↑x : FractionalIdeal R⁰ (FractionRing R))) ∧
        (MulEquiv.toMonoidHom (Units.mapEquiv (RingEquiv.toMulEquiv (canonicalEquiv R⁰ (FractionRing R) K))) :
              (a : (FractionalIdeal R⁰ (FractionRing R))ˣ) → (FractionalIdeal R⁰ K)ˣ)
            x =
          I) ↔
    ∃ (x : K), spanSingleton R⁰ x = (↑I : FractionalIdeal R⁰ K)

Tactic:
constructor
-- 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
I : (FractionalIdeal (R := R) R⁰ (FractionRing R))ˣ
x : FractionRing R
hx : spanSingleton R⁰ x = (↑I : FractionalIdeal R⁰ (FractionRing R))
⊢ ∃ (x : K),
    Eq (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) (spanSingleton R⁰ x)
      (↑((MulEquiv.toMonoidHom (Units.mapEquiv (RingEquiv.toMulEquiv (canonicalEquiv R⁰ (FractionRing R) K))) :
              (a : (FractionalIdeal R⁰ (FractionRing R))ˣ) → (FractionalIdeal R⁰ K)ˣ)
            I) :
        FractionalIdeal R⁰ K)

Tactic:
⟨FractionRing.algEquiv R K x, ?_⟩

Premises used: FractionRing.algEquiv, Exists.intro, DFunLike.coe
-- 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
I : (FractionalIdeal (R := R) R⁰ (FractionRing R))ˣ
x : FractionRing R
hx : spanSingleton R⁰ x = (↑I : FractionalIdeal R⁰ (FractionRing R))
h :
  Eq.{u_2 + 1} (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)
    (spanSingleton R⁰ ((FractionRing.algEquiv R K : (a : FractionRing R) → K) x) :
      FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)
    ((↑((MulEquiv.toMonoidHom (Units.mapEquiv (RingEquiv.toMulEquiv (canonicalEquiv R⁰ (FractionRing R) K))) :
              (a : (FractionalIdeal R⁰ (FractionRing R))ˣ) → (FractionalIdeal R⁰ K)ˣ)
            I) :
        FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) :
      FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)
⊢ ∃ (x : K),
    Eq (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) (spanSingleton R⁰ x)
      (↑((MulEquiv.toMonoidHom (Units.mapEquiv (RingEquiv.toMulEquiv (canonicalEquiv R⁰ (FractionRing R) K))) :
              (a : (FractionalIdeal R⁰ (FractionRing R))ˣ) → (FractionalIdeal R⁰ K)ˣ)
            I) :
        FractionalIdeal R⁰ K)

Tactic:
refine ⟨FractionRing.algEquiv R K x, ?_⟩
-- 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
I : (FractionalIdeal (R := R) R⁰ (FractionRing R))ˣ
x : FractionRing R
hx : spanSingleton R⁰ x = (↑I : FractionalIdeal R⁰ (FractionRing R))
h :
  Eq.{u_2 + 1} (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)
    (spanSingleton R⁰ ((FractionRing.algEquiv R K : (a : FractionRing R) → K) x) :
      FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)
    (spanSingleton R⁰ ((IsLocalization.map (M := R⁰) (T := R⁰) K (RingHom.id R) ⋯ : (a : FractionRing R) → K) x) :
      FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)
⊢ Eq.{u_2 + 1} (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)
    (spanSingleton R⁰ ((FractionRing.algEquiv R K : (a : FractionRing R) → K) x) :
      FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)
    ((↑((MulEquiv.toMonoidHom (Units.mapEquiv (RingEquiv.toMulEquiv (canonicalEquiv R⁰ (FractionRing R) K))) :
              (a : (FractionalIdeal R⁰ (FractionRing R))ˣ) → (FractionalIdeal R⁰ K)ˣ)
            I) :
        FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) :
      FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)

Tactic:
simp only [RingEquiv.toMulEquiv_eq_coe, MulEquiv.coe_toMonoidHom, coe_mapEquiv, ← hx,
        RingEquiv.coe_toMulEquiv, canonicalEquiv_spanSingleton]

Premises used: RingEquiv.coe_toMulEquiv, MulEquiv.coe_toMonoidHom, FractionalIdeal.canonicalEquiv_spanSingleton, RingEquiv.toMulEquiv_eq_coe, Units.coe_mapEquiv
-- 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
I : (FractionalIdeal (R := R) R⁰ (FractionRing R))ˣ
x : FractionRing R
hx : spanSingleton R⁰ x = (↑I : FractionalIdeal R⁰ (FractionRing R))
⊢ Eq.{u_2 + 1} (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)
    (spanSingleton R⁰ ((FractionRing.algEquiv R K : (a : FractionRing R) → K) x) :
      FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)
    (spanSingleton R⁰ ((IsLocalization.map (M := R⁰) (T := R⁰) K (RingHom.id R) ⋯ : (a : FractionRing R) → K) x) :
      FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)

Tactic:
rfl
-- 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
I : (FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)ˣ
x : K
hx : spanSingleton R⁰ x = (↑I : FractionalIdeal R⁰ K)
⊢ ∃ (x : (FractionalIdeal (R := R) R⁰ (FractionRing R))ˣ),
    (∃ (x_1 : FractionRing R), spanSingleton R⁰ x_1 = (↑x : FractionalIdeal R⁰ (FractionRing R))) ∧
      (MulEquiv.toMonoidHom (Units.mapEquiv (RingEquiv.toMulEquiv (canonicalEquiv R⁰ (FractionRing R) K))) :
            (a : (FractionalIdeal R⁰ (FractionRing R))ˣ) → (FractionalIdeal R⁰ K)ˣ)
          x =
        I

Tactic:
⟨Units.mapEquiv (canonicalEquiv R⁰ K (FractionRing R)).toMulEquiv I,
        ⟨(FractionRing.algEquiv R K).symm x, ?_⟩, Units.ext ?_⟩

Premises used: AlgEquiv.symm, RingEquiv.toMulEquiv, FractionRing, nonZeroDivisors, FractionalIdeal.canonicalEquiv, Units.ext, FractionRing.algEquiv, Units.mapEquiv, And.intro, Exists.intro, DFunLike.coe
-- 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
I : (FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)ˣ
x : K
hx : spanSingleton R⁰ x = (↑I : FractionalIdeal R⁰ K)
h :
  Eq.{u_1 + 1} (α := FractionalIdeal (R := R) R⁰ (FractionRing R))
    (spanSingleton R⁰
        (((AlgEquiv.symm (FractionRing.algEquiv R K) : K ≃ₐ[R] FractionRing R) : (a : K) → FractionRing R) x) :
      FractionalIdeal (R := R) R⁰ (FractionRing R))
    ((↑((Units.mapEquiv (RingEquiv.toMulEquiv (canonicalEquiv R⁰ K (FractionRing R))) :
              (a : (FractionalIdeal R⁰ K)ˣ) → (FractionalIdeal R⁰ (FractionRing R))ˣ)
            I) :
        FractionalIdeal (R := R) R⁰ (FractionRing R)) :
      FractionalIdeal (R := R) R⁰ (FractionRing R))
h₁ :
  (↑((MulEquiv.toMonoidHom (Units.mapEquiv (RingEquiv.toMulEquiv (canonicalEquiv R⁰ (FractionRing R) K))) :
            (a : (FractionalIdeal R⁰ (FractionRing R))ˣ) → (FractionalIdeal R⁰ K)ˣ)
          ((Units.mapEquiv (RingEquiv.toMulEquiv (canonicalEquiv R⁰ K (FractionRing R))) :
              (a : (FractionalIdeal R⁰ K)ˣ) → (FractionalIdeal R⁰ (FractionRing R))ˣ)
            I)) :
      FractionalIdeal R⁰ K) =
    (↑I : FractionalIdeal R⁰ K)
⊢ ∃ (x : (FractionalIdeal (R := R) R⁰ (FractionRing R))ˣ),
    (∃ (x_1 : FractionRing R), spanSingleton R⁰ x_1 = (↑x : FractionalIdeal R⁰ (FractionRing R))) ∧
      (MulEquiv.toMonoidHom (Units.mapEquiv (RingEquiv.toMulEquiv (canonicalEquiv R⁰ (FractionRing R) K))) :
            (a : (FractionalIdeal R⁰ (FractionRing R))ˣ) → (FractionalIdeal R⁰ K)ˣ)
          x =
        I

Tactic:
refine ⟨Units.mapEquiv (canonicalEquiv R⁰ K (FractionRing R)).toMulEquiv I,
        ⟨(FractionRing.algEquiv R K).symm x, ?_⟩, Units.ext ?_⟩
-- 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
I : (FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)ˣ
x : K
hx : spanSingleton R⁰ x = (↑I : FractionalIdeal R⁰ K)
h :
  Eq.{u_1 + 1} (α := FractionalIdeal (R := R) R⁰ (FractionRing R))
    (spanSingleton R⁰
        (((AlgEquiv.symm (FractionRing.algEquiv R K) : K ≃ₐ[R] FractionRing R) : (a : K) → FractionRing R) x) :
      FractionalIdeal (R := R) R⁰ (FractionRing R))
    (spanSingleton R⁰
        ((IsLocalization.map (M := R⁰) (T := R⁰) (FractionRing R) (RingHom.id R) ⋯ : (a : K) → FractionRing R) x) :
      FractionalIdeal (R := R) R⁰ (FractionRing R))
⊢ Eq.{u_1 + 1} (α := FractionalIdeal (R := R) R⁰ (FractionRing R))
    (spanSingleton R⁰
        (((AlgEquiv.symm (FractionRing.algEquiv R K) : K ≃ₐ[R] FractionRing R) : (a : K) → FractionRing R) x) :
      FractionalIdeal (R := R) R⁰ (FractionRing R))
    ((↑((Units.mapEquiv (RingEquiv.toMulEquiv (canonicalEquiv R⁰ K (FractionRing R))) :
              (a : (FractionalIdeal R⁰ K)ˣ) → (FractionalIdeal R⁰ (FractionRing R))ˣ)
            I) :
        FractionalIdeal (R := R) R⁰ (FractionRing R)) :
      FractionalIdeal (R := R) R⁰ (FractionRing R))

Tactic:
simp only [RingEquiv.toMulEquiv_eq_coe, coe_mapEquiv, ← hx, RingEquiv.coe_toMulEquiv,
          canonicalEquiv_spanSingleton]

Premises used: RingEquiv.coe_toMulEquiv, FractionalIdeal.canonicalEquiv_spanSingleton, RingEquiv.toMulEquiv_eq_coe, Units.coe_mapEquiv
-- 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
I : (FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)ˣ
x : K
hx : spanSingleton R⁰ x = (↑I : FractionalIdeal R⁰ K)
⊢ Eq.{u_1 + 1} (α := FractionalIdeal (R := R) R⁰ (FractionRing R))
    (spanSingleton R⁰
        (((AlgEquiv.symm (FractionRing.algEquiv R K) : K ≃ₐ[R] FractionRing R) : (a : K) → FractionRing R) x) :
      FractionalIdeal (R := R) R⁰ (FractionRing R))
    (spanSingleton R⁰
        ((IsLocalization.map (M := R⁰) (T := R⁰) (FractionRing R) (RingHom.id R) ⋯ : (a : K) → FractionRing R) x) :
      FractionalIdeal (R := R) R⁰ (FractionRing R))

Tactic:
rfl
-- 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
I : (FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)ˣ
x : K
hx : spanSingleton R⁰ x = (↑I : FractionalIdeal R⁰ K)
⊢ (↑((MulEquiv.toMonoidHom (Units.mapEquiv (RingEquiv.toMulEquiv (canonicalEquiv R⁰ (FractionRing R) K))) :
            (a : (FractionalIdeal R⁰ (FractionRing R))ˣ) → (FractionalIdeal R⁰ K)ˣ)
          ((Units.mapEquiv (RingEquiv.toMulEquiv (canonicalEquiv R⁰ K (FractionRing R))) :
              (a : (FractionalIdeal R⁰ K)ˣ) → (FractionalIdeal R⁰ (FractionRing R))ˣ)
            I)) :
      FractionalIdeal R⁰ K) =
    (↑I : FractionalIdeal R⁰ K)

Tactic:
simp only [RingEquiv.toMulEquiv_eq_coe, MulEquiv.coe_toMonoidHom, coe_mapEquiv,
          RingEquiv.coe_toMulEquiv, canonicalEquiv_canonicalEquiv, canonicalEquiv_self,
          RingEquiv.refl_apply]

Premises used: RingEquiv.coe_toMulEquiv, MulEquiv.coe_toMonoidHom, FractionalIdeal.canonicalEquiv_canonicalEquiv, RingEquiv.toMulEquiv_eq_coe, FractionalIdeal.canonicalEquiv_self, RingEquiv.refl_apply, Units.coe_mapEquiv
-- 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
⊢ Eq (α := Subgroup (FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)ˣ)
    (Subgroup.map (G := (FractionalIdeal (R := R) R⁰ (FractionRing R))ˣ)
      (MulEquiv.toMonoidHom (Units.mapEquiv (RingEquiv.toMulEquiv (canonicalEquiv R⁰ (FractionRing R) K))) :
        MonoidHom.{u_1, u_2} (FractionalIdeal (R := R) R⁰ (FractionRing R))ˣ
          (FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)ˣ)
      (MonoidHom.range (toPrincipalIdeal R (FractionRing R)) :
        Subgroup (FractionalIdeal (R := R) R⁰ (FractionRing R))ˣ))
    (MonoidHom.range (toPrincipalIdeal R K))

Tactic:
haveI : Subgroup.map
    (Units.mapEquiv (canonicalEquiv R⁰ (FractionRing R) K).toMulEquiv).toMonoidHom
    (toPrincipalIdeal R (FractionRing R)).range = (toPrincipalIdeal R K).range := by
    ext I
    simp only [Subgroup.mem_map, mem_principal_ideals_iff]
    constructor
    · rintro ⟨I, ⟨x, hx⟩, rfl⟩
      refine ⟨FractionRing.algEquiv R K x, ?_⟩
      simp only [RingEquiv.toMulEquiv_eq_coe, MulEquiv.coe_toMonoidHom, coe_mapEquiv, ← hx,
        RingEquiv.coe_toMulEquiv, canonicalEquiv_spanSingleton]
      rfl
    · rintro ⟨x, hx⟩
      refine ⟨Units.mapEquiv (canonicalEquiv R⁰ K (FractionRing R)).toMulEquiv I,
        ⟨(FractionRing.algEquiv R K).symm x, ?_⟩, Units.ext ?_⟩
      · simp only [RingEquiv.toMulEquiv_eq_coe, coe_mapEquiv, ← hx, RingEquiv.coe_toMulEquiv,
          canonicalEquiv_spanSingleton]
        rfl
      · simp only [RingEquiv.toMulEquiv_eq_coe, MulEquiv.coe_toMonoidHom, coe_mapEquiv,
          RingEquiv.coe_toMulEquiv, canonicalEquiv_canonicalEquiv, canonicalEquiv_self,
          RingEquiv.refl_apply]
-- 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
this :
  Eq (α := Subgroup (FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)ˣ)
    (Subgroup.map (G := (FractionalIdeal (R := R) R⁰ (FractionRing R))ˣ)
      (MulEquiv.toMonoidHom (Units.mapEquiv (RingEquiv.toMulEquiv (canonicalEquiv R⁰ (FractionRing R) K))) :
        MonoidHom.{u_1, u_2} (FractionalIdeal (R := R) R⁰ (FractionRing R))ˣ
          (FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)ˣ)
      (MonoidHom.range (toPrincipalIdeal R (FractionRing R)) :
        Subgroup (FractionalIdeal (R := R) R⁰ (FractionRing R))ˣ))
    (MonoidHom.range (toPrincipalIdeal R K))
⊢ MulEquiv.{u_1, u_2} (ClassGroup R)
    (HasQuotient.Quotient (FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)ˣ (B :=
      Subgroup (FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)ˣ) (MonoidHom.range (toPrincipalIdeal R K)))

Tactic:
exact QuotientGroup.congr (toPrincipalIdeal R (FractionRing R)).range (toPrincipalIdeal R K).range
    (Units.mapEquiv (FractionalIdeal.canonicalEquiv R⁰ (FractionRing R) K).toMulEquiv) this

Premises used: MonoidHom.range, RingEquiv.toMulEquiv, FractionRing, nonZeroDivisors, FractionalIdeal.canonicalEquiv, Units.mapEquiv, toPrincipalIdeal, QuotientGroup.congr