From d33499d2c3cba07b20595061f530957996457533 Mon Sep 17 00:00:00 2001
From: mariainesdff <mariaines.dff@gmail.com>
Date: Thu, 19 Feb 2026 12:54:25 +0100
Subject: [PATCH 01/14] feat(RingTheory/ClassGroup): prove mulEquiv

---
 Mathlib/RingTheory/ClassGroup.lean            |  39 +++++
 .../FractionalIdeal/Operations.lean           | 144 ++++++++++++++++++
 .../RingTheory/Localization/FractionRing.lean |  30 ++++
 3 files changed, 213 insertions(+)

diff --git a/Mathlib/RingTheory/ClassGroup.lean b/Mathlib/RingTheory/ClassGroup.lean
index 334dee1ecc6d62..ebedf262b0d0cf 100644
--- a/Mathlib/RingTheory/ClassGroup.lean
+++ b/Mathlib/RingTheory/ClassGroup.lean
@@ -418,3 +418,42 @@ theorem card_classGroup_eq_one_iff [IsDedekindDomain R] [Fintype (ClassGroup R)]
   by_cases hI : I = ⊥
   · rw [hI]; exact bot_isPrincipal
   · exact (ClassGroup.mk0_eq_one_iff (mem_nonZeroDivisors_iff_ne_zero.mpr hI)).mp (eq_one _)
+
+section MulEquiv
+
+theorem FractionalIdeal.map_ringEquivOfRingEquiv_toPrincipalIdeal {S L : Type*} [CommRing S]
+    [IsDomain S] [Field L] [Algebra S L] [IsFractionRing S L] (f : R ≃+* S) :
+  Subgroup.map ((Units.mapEquiv (ringEquivOfRingEquiv K L f))).toMonoidHom
+    (toPrincipalIdeal R K).range = (toPrincipalIdeal S L).range := by
+  ext I
+  simp only [MulEquiv.toMonoidHom_eq_coe, Subgroup.mem_map, MonoidHom.mem_range,
+    toPrincipalIdeal_eq_iff, MonoidHom.coe_coe]
+  refine ⟨fun ⟨u, ⟨v, huv⟩, hu⟩ ↦ ?_, fun ⟨u, hu⟩ ↦ ?_⟩
+  · use Units.map (IsFractionRing.ringEquivOfRingEquiv f (K := K)
+      (L := L)).toRingHom v
+    rw [← hu]
+    simp only [RingEquiv.toRingHom_eq_coe, Units.coe_map, MonoidHom.coe_coe, RingHom.coe_coe,
+      Units.coe_mapEquiv, ← huv, RingEquiv.coe_toMulEquiv]
+    rw [FractionalIdeal.ringEquivOfRingEquiv_spanSingleton]
+  · use Units.mapEquiv (FractionalIdeal.ringEquivOfRingEquiv _ _ f).symm.toMulEquiv I
+    refine ⟨?_, by simp [← Units.val_inj]⟩
+    · use Units.map (IsFractionRing.ringEquivOfRingEquiv f (K := K)
+        (L := L)).symm.toRingHom u
+      simp only [IsFractionRing.ringEquivOfRingEquiv_symm, RingEquiv.toRingHom_eq_coe,
+        Units.coe_map, MonoidHom.coe_coe, RingHom.coe_coe, RingEquiv.toMulEquiv_eq_coe,
+        RingEquiv.coe_toMulEquiv_symm, Units.coe_mapEquiv]
+      rw [← FractionalIdeal.ringEquivOfRingEquiv_spanSingleton,
+        ← FractionalIdeal.ringEquivOfRingEquiv_symm_eq, hu]
+      rfl
+
+/-- A ring isomorphism `P ≃+* P'` induces an isomorphism on their class groups. -/
+noncomputable def RingEquiv.classGroupEquiv {P P' : Type*} [CommRing P] [IsDomain P] [CommRing P']
+    [IsDomain P'] (g : P ≃+* P') : ClassGroup P ≃* ClassGroup P' :=
+  (ClassGroup.equiv (R := P) (FractionRing P)).trans
+    ((QuotientGroup.congr (toPrincipalIdeal P (FractionRing P)).range
+        (toPrincipalIdeal P' (FractionRing P')).range
+        (Units.mapEquiv (FractionalIdeal.ringEquivOfRingEquiv (FractionRing P) (FractionRing P') g))
+        (FractionalIdeal.map_ringEquivOfRingEquiv_toPrincipalIdeal g)).trans
+      (ClassGroup.equiv (R := P') (FractionRing P')))
+
+end MulEquiv
diff --git a/Mathlib/RingTheory/FractionalIdeal/Operations.lean b/Mathlib/RingTheory/FractionalIdeal/Operations.lean
index 9343db5827de8f..0532e065d9b2b9 100644
--- a/Mathlib/RingTheory/FractionalIdeal/Operations.lean
+++ b/Mathlib/RingTheory/FractionalIdeal/Operations.lean
@@ -916,4 +916,148 @@ theorem mem_adjoinIntegral_self (hx : IsIntegral R x) : x ∈ adjoinIntegral S x
 
 end Adjoin
 
+section RingEquiv
+
+variable {R S : Type*} (K L : Type*) [CommRing R] [IsDomain R] [CommRing S] [IsDomain S]
+  [CommRing K] [CommRing L] [Algebra R K] [Algebra S L] [IsFractionRing R K] [IsFractionRing S L]
+  (f : R ≃+* S)
+
+theorem _root_.IsFractional.map' [RingHomSurjective f.toRingHom]
+    {I : Submodule R K} (hI : IsFractional (nonZeroDivisors R) I) :
+    IsFractional (nonZeroDivisors S)
+      (Submodule.map (IsFractionRing.semilinearEquivOfRingEquiv K L f).toLinearMap I) := by
+  simp only [IsFractional, mem_nonZeroDivisors_iff_ne_zero, ne_eq,
+    RingEquiv.toRingHom_eq_coe, Submodule.mem_map, forall_exists_index, and_imp,
+    forall_apply_eq_imp_iff₂] at hI ⊢
+  obtain ⟨r, hr0, hr⟩ := hI
+  use f r
+  refine ⟨by simp [hr0], ?_⟩
+  intro x hx
+  specialize hr x hx
+  simp only [IsLocalization.IsInteger, RingHom.mem_rangeS] at hr ⊢
+  obtain ⟨r', hr'⟩ := hr
+  use f r'
+  simp only [IsFractionRing.semilinearEquivOfRingEquiv, RingEquiv.toRingHom_eq_coe,
+    RingEquiv.toEquiv_eq_coe, Equiv.toFun_as_coe, EquivLike.coe_coe, Equiv.invFun_as_coe,
+    LinearMap.coe_mk, AddHom.coe_mk]
+  rw [Algebra.smul_def, ← IsFractionRing.ringEquivOfRingEquiv_algebraMap f (K := K) (L := L) r,
+    ← map_mul, ← Algebra.smul_def, ← hr', IsFractionRing.ringEquivOfRingEquiv_algebraMap]
+
+/-- The map `FractionalIdeal (nonZeroDivisors R) K →+* FractionalIdeal (nonZeroDivisors S) L`
+  induced by a ring isomorphism `f : R ≃+* S`. -/
+noncomputable def ringHomOfRingEquiv (f : R ≃+* S) :
+    FractionalIdeal (nonZeroDivisors R) K →+* FractionalIdeal (nonZeroDivisors S) L where
+  toFun I := ⟨Submodule.map (IsFractionRing.semilinearEquivOfRingEquiv _ _ f).toLinearMap I.val,
+      IsFractional.map' K L f I.prop⟩
+  map_one' := by
+    rw [Subtype.ext_iff]
+    ext x
+    simp only [RingEquiv.toRingHom_eq_coe, val_eq_coe, coe_one, Submodule.mem_map_equiv,
+      Submodule.mem_one]
+    refine ⟨fun ⟨r, hr⟩ ↦ ⟨f r, ?_⟩, fun ⟨s, hs⟩ ↦ ⟨f.symm s, ?_⟩⟩
+    · simp only [← (LinearEquiv.injective (IsFractionRing.semilinearEquivOfRingEquiv K L f)).eq_iff,
+        RingEquiv.toRingHom_eq_coe, LinearEquiv.apply_symm_apply] at hr
+      simp [← hr, IsFractionRing.semilinearEquivOfRingEquiv]
+    · rw [← hs, IsFractionRing.semilinearEquivOfRingEquiv_symm_apply]; simp
+  map_zero' := by
+    simp only [RingEquiv.toRingHom_eq_coe, val_eq_coe, coe_zero, Submodule.map_bot]
+    exact coeToSubmodule_eq_bot.mp rfl
+  map_add' I J := by
+    rw [Subtype.ext_iff]
+    simp
+  map_mul' I J := by
+    rw [Subtype.ext_iff]
+    simp only [RingEquiv.toRingHom_eq_coe, val_eq_coe, coe_mul, coe_mk]
+    set g := (IsFractionRing.semilinearEquivOfRingEquiv K L f) with hg
+    calc Submodule.map g.toLinearMap (↑I * ↑J)
+      _ = ⨆ i : I.val, (J.val.map (LinearMap.mul R K i)).map g.toLinearMap := by
+        rw [Submodule.mul_eq_map₂]; apply Submodule.map_iSup
+      _ = Submodule.map g.toLinearMap ↑I * Submodule.map g.toLinearMap ↑J := by
+        rw [Submodule.mul_eq_map₂]
+        apply congr_arg sSup
+        ext S
+        constructor <;> rintro ⟨y, hy⟩
+        · refine ⟨⟨g y, Submodule.mem_map.mpr ⟨y.1, y.2, rfl⟩⟩, Eq.trans ?_ hy⟩
+          ext x
+          simp only [RingEquiv.toRingHom_eq_coe, val_eq_coe, Submodule.mem_map, mem_coe,
+            LinearMap.mul_apply_apply]
+          refine ⟨fun  ⟨w, ⟨z, hzJ, hzy⟩, hw⟩ ↦ ⟨g.symm x, ⟨z, hzJ, ?_⟩, by simp⟩,
+            fun ⟨w, ⟨⟨z, hzJ, hzw⟩, hw⟩⟩ ↦ ⟨g z, ⟨z, hzJ, rfl⟩, ?_⟩⟩
+          · simp [← (LinearEquiv.injective g).eq_iff, ← hw, ← hzy,
+                hg, IsFractionRing.semilinearEquivOfRingEquiv]
+          · simp [← hw, ← hzw, hg, IsFractionRing.semilinearEquivOfRingEquiv]
+        · obtain ⟨y', hy', fy_eq⟩ := Submodule.mem_map.mp y.2
+          refine ⟨⟨y', hy'⟩, Eq.trans ?_ hy⟩
+          ext x
+          simp only [RingEquiv.toRingHom_eq_coe, val_eq_coe, Submodule.mem_map, mem_coe,
+            LinearMap.mul_apply_apply, ← fy_eq, LinearEquiv.coe_coe]
+          refine ⟨fun ⟨w, ⟨z, hzJ, hzy⟩, hw⟩ ↦ ⟨g z, ⟨z, hzJ, rfl⟩, ?_⟩,
+            fun ⟨y, ⟨⟨z, hzJ, hzy⟩, hy⟩⟩ ↦ ⟨g.symm x, ⟨z, hzJ, ?_⟩, by simp⟩⟩
+          · simp [hg, IsFractionRing.semilinearEquivOfRingEquiv, ← hw, ← hzy]
+          · simp [← (LinearEquiv.injective g).eq_iff, hg,
+              IsFractionRing.semilinearEquivOfRingEquiv, ← hzy, ← hy]
+
+/-- The equiv `FractionalIdeal (nonZeroDivisors R) K ≃+* FractionalIdeal (nonZeroDivisors S) L`
+  induced by a ring isomorphism `f : R ≃+* S`. -/
+noncomputable def ringEquivOfRingEquiv :
+    FractionalIdeal (nonZeroDivisors R) K ≃+* FractionalIdeal (nonZeroDivisors S) L :=
+  { FractionalIdeal.ringHomOfRingEquiv K L f with
+    invFun := FractionalIdeal.ringHomOfRingEquiv L K f.symm
+    left_inv I := by
+      have : RingHomCompTriple (f : R →+* S) (f.symm : S →+* R) (RingHom.id R) := ⟨by simp⟩
+      rw [Subtype.ext_iff]
+      simp only [ringHomOfRingEquiv, RingEquiv.toRingHom_eq_coe, RingEquiv.symm_symm, val_eq_coe,
+        RingHom.toMonoidHom_eq_coe, RingHom.coe_monoidHom_mk, OneHom.toFun_eq_coe, OneHom.coe_mk,
+        RingHom.coe_mk, MonoidHom.coe_mk, coe_mk, ← Submodule.map_comp (σ₁₃ := RingHom.id R)]
+      convert Submodule.map_id _
+      ext x
+      simp only [LinearEquiv.comp_coe, LinearEquiv.coe_coe, LinearEquiv.trans_apply,
+        LinearMap.id_coe, id_eq]
+      exact (LinearEquiv.eq_symm_apply
+        (IsFractionRing.semilinearEquivOfRingEquiv _ _ f.symm)).mp rfl
+    right_inv I := by
+      have : RingHomCompTriple (f.symm : S →+* R) (f : R →+* S) (RingHom.id S) := ⟨by simp⟩
+      rw [Subtype.ext_iff]
+      simp only [ringHomOfRingEquiv, RingEquiv.toRingHom_eq_coe, RingEquiv.symm_symm, val_eq_coe,
+        RingHom.toMonoidHom_eq_coe, RingHom.coe_monoidHom_mk, OneHom.toFun_eq_coe, OneHom.coe_mk,
+        RingHom.coe_mk, MonoidHom.coe_mk, coe_mk, ← Submodule.map_comp (σ₁₃ := RingHom.id S)]
+      convert Submodule.map_id _
+      ext x
+      simp only [LinearEquiv.comp_coe, LinearEquiv.coe_coe, LinearEquiv.trans_apply,
+        LinearMap.id_coe, id_eq]
+      exact (LinearEquiv.eq_symm_apply
+        (IsFractionRing.semilinearEquivOfRingEquiv _ _ f)).mp rfl }
+
+lemma ringEquivOfRingEquiv_spanSingleton (x : K) :
+    FractionalIdeal.ringEquivOfRingEquiv K L f (spanSingleton (nonZeroDivisors R) x) =
+      spanSingleton (nonZeroDivisors S) (IsFractionRing.ringEquivOfRingEquiv (L := L) f x) := by
+  simp only [ringEquivOfRingEquiv, ringHomOfRingEquiv, RingEquiv.toRingHom_eq_coe, val_eq_coe,
+    RingHom.toMonoidHom_eq_coe, RingHom.coe_monoidHom_mk, OneHom.toFun_eq_coe, OneHom.coe_mk,
+    RingEquiv.symm_symm, RingHom.coe_mk, MonoidHom.coe_mk, RingEquiv.coe_mk, Equiv.coe_fn_mk,
+    coe_spanSingleton]
+  rw [Subtype.ext_iff]
+  simp only [val_eq_coe, coe_spanSingleton]
+  ext I
+  simp only [Submodule.mem_map_equiv, Submodule.mem_span_singleton]
+  refine ⟨fun ⟨r, hr⟩ ↦ ?_, fun ⟨s, hs⟩ ↦ ?_⟩
+  · use f r
+    rw [← (IsFractionRing.semilinearEquivOfRingEquiv K L f).injective.eq_iff] at hr
+    simp only [RingEquiv.toRingHom_eq_coe, LinearEquiv.apply_symm_apply] at hr
+    simp only [IsFractionRing.ringEquivOfRingEquiv, IsLocalization.ringEquivOfRingEquiv_apply, ← hr]
+    exact Eq.symm (map_smulₛₗ _ r x)
+  · use f.symm s
+    simp only [Algebra.smul_def, ← hs]
+    rw [IsFractionRing.semilinearEquivOfRingEquiv_symm_apply]
+    simp only [ map_mul, RingEquiv.symm_apply_apply]
+    simp [IsFractionRing.ringEquivOfRingEquiv_symm,
+      IsFractionRing.ringEquivOfRingEquiv_algebraMap]
+
+lemma ringEquivOfRingEquiv_symm_eq :
+    (FractionalIdeal.ringEquivOfRingEquiv K L f).symm =
+      FractionalIdeal.ringEquivOfRingEquiv L K f.symm := by
+  exact (RingEquiv.coe_nonUnitalRingHom_inj_iff (ringEquivOfRingEquiv K L f).symm
+          (ringEquivOfRingEquiv L K f.symm)).mpr rfl
+
+end RingEquiv
+
 end FractionalIdeal
diff --git a/Mathlib/RingTheory/Localization/FractionRing.lean b/Mathlib/RingTheory/Localization/FractionRing.lean
index 61e07e891c398b..4b4b60cffe3294 100644
--- a/Mathlib/RingTheory/Localization/FractionRing.lean
+++ b/Mathlib/RingTheory/Localization/FractionRing.lean
@@ -424,6 +424,36 @@ lemma ringEquivOfRingEquiv_symm :
 
 end ringEquivOfRingEquiv
 
+section semilinearEquivOfRingEquiv
+
+instance _root_.RingHomInvPair.ofRingEquiv {R S : Type*} [CommSemiring R] [CommSemiring S]
+    (f : R ≃+* S) : RingHomInvPair f.toRingHom f.symm.toRingHom where
+  comp_eq := by simp
+  comp_eq₂ := by simp_all
+
+variable {A B : Type*} (K L : Type*) [CommRing A] [CommRing B] [CommRing K] [CommRing L]
+    [Algebra A K] [IsFractionRing A K] [Algebra B L] [IsFractionRing B L] (f : A ≃+* B)
+
+/-- Given rings `A, B` and localization maps to their fraction rings
+`f : A →+* K, g : B →+* L`, an isomorphism `h : A ≃+* B` induces a semilinear equivalence
+fraction rings `K ≃ₛₗ[f.toRingHom] L`. -/
+noncomputable def semilinearEquivOfRingEquiv : K ≃ₛₗ[f.toRingHom] L :=
+{ ringEquivOfRingEquiv f with
+  map_smul' r x := by simp [Algebra.smul_def] }
+
+lemma semilinearEquivOfRingEquiv_apply (x : K) :
+    (semilinearEquivOfRingEquiv K L f) x = (ringEquivOfRingEquiv f) x := rfl
+
+@[simp]
+lemma semilinearEquivOfRingEquiv_algebraMap (a : A) :
+    semilinearEquivOfRingEquiv K L f (algebraMap A K a) = algebraMap B L (f a) := by
+  simp [semilinearEquivOfRingEquiv, ringEquivOfRingEquiv]
+
+lemma semilinearEquivOfRingEquiv_symm_apply (x : L) :
+    (semilinearEquivOfRingEquiv K L f).symm x = (ringEquivOfRingEquiv f).symm x := rfl
+
+end semilinearEquivOfRingEquiv
+
 section algEquivOfAlgEquiv
 
 variable {R A K B L : Type*} [CommSemiring R] [CommRing A] [CommRing B] [CommRing K] [CommRing L]

From 6a6138c9fe40c1dbb1c08182acd15c7a885ee9d1 Mon Sep 17 00:00:00 2001
From: mariainesdff <mariaines.dff@gmail.com>
Date: Mon, 23 Feb 2026 15:30:47 +0100
Subject: [PATCH 02/14] some suggested changes

---
 Mathlib/Algebra/Ring/CompTypeclasses.lean     |  5 +-
 Mathlib/RingTheory/ClassGroup.lean            |  5 +-
 .../FractionalIdeal/Operations.lean           | 53 ++++++++++---------
 .../RingTheory/Localization/FractionRing.lean |  8 +--
 4 files changed, 35 insertions(+), 36 deletions(-)

diff --git a/Mathlib/Algebra/Ring/CompTypeclasses.lean b/Mathlib/Algebra/Ring/CompTypeclasses.lean
index 9347bdd1eb8cb1..858c6dbce8b1de 100644
--- a/Mathlib/Algebra/Ring/CompTypeclasses.lean
+++ b/Mathlib/Algebra/Ring/CompTypeclasses.lean
@@ -113,10 +113,9 @@ instance triples₂ {σ₂₁ : R₂ →+* R₁} [RingHomInvPair σ₁₂ σ₂
 
 /-- Construct a `RingHomInvPair` from both directions of a ring equiv.
 
-This is not an instance, as for equivalences that are involutions, a better instance
-would be `RingHomInvPair e e`. Indeed, this declaration is not currently used in mathlib.
+Note that for equivalences that are involutions, a better instance would be `RingHomInvPair e e`.
 -/
-theorem of_ringEquiv (e : R₁ ≃+* R₂) : RingHomInvPair (↑e : R₁ →+* R₂) ↑e.symm :=
+instance of_ringEquiv (e : R₁ ≃+* R₂) : RingHomInvPair (↑e : R₁ →+* R₂) ↑e.symm :=
   ⟨e.symm_toRingHom_comp_toRingHom, e.symm.symm_toRingHom_comp_toRingHom⟩
 
 /--
diff --git a/Mathlib/RingTheory/ClassGroup.lean b/Mathlib/RingTheory/ClassGroup.lean
index ebedf262b0d0cf..a254a04ccd2e2c 100644
--- a/Mathlib/RingTheory/ClassGroup.lean
+++ b/Mathlib/RingTheory/ClassGroup.lean
@@ -447,13 +447,14 @@ theorem FractionalIdeal.map_ringEquivOfRingEquiv_toPrincipalIdeal {S L : Type*}
       rfl
 
 /-- A ring isomorphism `P ≃+* P'` induces an isomorphism on their class groups. -/
-noncomputable def RingEquiv.classGroupEquiv {P P' : Type*} [CommRing P] [IsDomain P] [CommRing P']
+@[simps!]
+noncomputable def ClassGroup.mulEquiv {P P' : Type*} [CommRing P] [IsDomain P] [CommRing P']
     [IsDomain P'] (g : P ≃+* P') : ClassGroup P ≃* ClassGroup P' :=
   (ClassGroup.equiv (R := P) (FractionRing P)).trans
     ((QuotientGroup.congr (toPrincipalIdeal P (FractionRing P)).range
         (toPrincipalIdeal P' (FractionRing P')).range
         (Units.mapEquiv (FractionalIdeal.ringEquivOfRingEquiv (FractionRing P) (FractionRing P') g))
         (FractionalIdeal.map_ringEquivOfRingEquiv_toPrincipalIdeal g)).trans
-      (ClassGroup.equiv (R := P') (FractionRing P')))
+      (ClassGroup.equiv (FractionRing P')).symm)
 
 end MulEquiv
diff --git a/Mathlib/RingTheory/FractionalIdeal/Operations.lean b/Mathlib/RingTheory/FractionalIdeal/Operations.lean
index 0532e065d9b2b9..0472e2f3bb3ede 100644
--- a/Mathlib/RingTheory/FractionalIdeal/Operations.lean
+++ b/Mathlib/RingTheory/FractionalIdeal/Operations.lean
@@ -922,13 +922,12 @@ variable {R S : Type*} (K L : Type*) [CommRing R] [IsDomain R] [CommRing S] [IsD
   [CommRing K] [CommRing L] [Algebra R K] [Algebra S L] [IsFractionRing R K] [IsFractionRing S L]
   (f : R ≃+* S)
 
-theorem _root_.IsFractional.map' [RingHomSurjective f.toRingHom]
+theorem _root_.IsFractional.map' [RingHomSurjective (f : R →+* S)]
     {I : Submodule R K} (hI : IsFractional (nonZeroDivisors R) I) :
     IsFractional (nonZeroDivisors S)
       (Submodule.map (IsFractionRing.semilinearEquivOfRingEquiv K L f).toLinearMap I) := by
-  simp only [IsFractional, mem_nonZeroDivisors_iff_ne_zero, ne_eq,
-    RingEquiv.toRingHom_eq_coe, Submodule.mem_map, forall_exists_index, and_imp,
-    forall_apply_eq_imp_iff₂] at hI ⊢
+  simp only [IsFractional, mem_nonZeroDivisors_iff_ne_zero, ne_eq, Submodule.mem_map,
+    forall_exists_index, and_imp, forall_apply_eq_imp_iff₂] at hI ⊢
   obtain ⟨r, hr0, hr⟩ := hI
   use f r
   refine ⟨by simp [hr0], ?_⟩
@@ -937,14 +936,14 @@ theorem _root_.IsFractional.map' [RingHomSurjective f.toRingHom]
   simp only [IsLocalization.IsInteger, RingHom.mem_rangeS] at hr ⊢
   obtain ⟨r', hr'⟩ := hr
   use f r'
-  simp only [IsFractionRing.semilinearEquivOfRingEquiv, RingEquiv.toRingHom_eq_coe,
-    RingEquiv.toEquiv_eq_coe, Equiv.toFun_as_coe, EquivLike.coe_coe, Equiv.invFun_as_coe,
-    LinearMap.coe_mk, AddHom.coe_mk]
+  simp only [IsFractionRing.semilinearEquivOfRingEquiv, RingEquiv.toEquiv_eq_coe,
+    Equiv.toFun_as_coe, EquivLike.coe_coe, Equiv.invFun_as_coe, LinearMap.coe_mk, AddHom.coe_mk]
   rw [Algebra.smul_def, ← IsFractionRing.ringEquivOfRingEquiv_algebraMap f (K := K) (L := L) r,
     ← map_mul, ← Algebra.smul_def, ← hr', IsFractionRing.ringEquivOfRingEquiv_algebraMap]
 
 /-- The map `FractionalIdeal (nonZeroDivisors R) K →+* FractionalIdeal (nonZeroDivisors S) L`
   induced by a ring isomorphism `f : R ≃+* S`. -/
+--@[simps]
 noncomputable def ringHomOfRingEquiv (f : R ≃+* S) :
     FractionalIdeal (nonZeroDivisors R) K →+* FractionalIdeal (nonZeroDivisors S) L where
   toFun I := ⟨Submodule.map (IsFractionRing.semilinearEquivOfRingEquiv _ _ f).toLinearMap I.val,
@@ -952,22 +951,21 @@ noncomputable def ringHomOfRingEquiv (f : R ≃+* S) :
   map_one' := by
     rw [Subtype.ext_iff]
     ext x
-    simp only [RingEquiv.toRingHom_eq_coe, val_eq_coe, coe_one, Submodule.mem_map_equiv,
-      Submodule.mem_one]
+    simp only [val_eq_coe, coe_one, Submodule.mem_map_equiv, Submodule.mem_one]
     refine ⟨fun ⟨r, hr⟩ ↦ ⟨f r, ?_⟩, fun ⟨s, hs⟩ ↦ ⟨f.symm s, ?_⟩⟩
     · simp only [← (LinearEquiv.injective (IsFractionRing.semilinearEquivOfRingEquiv K L f)).eq_iff,
-        RingEquiv.toRingHom_eq_coe, LinearEquiv.apply_symm_apply] at hr
+        LinearEquiv.apply_symm_apply] at hr
       simp [← hr, IsFractionRing.semilinearEquivOfRingEquiv]
     · rw [← hs, IsFractionRing.semilinearEquivOfRingEquiv_symm_apply]; simp
   map_zero' := by
-    simp only [RingEquiv.toRingHom_eq_coe, val_eq_coe, coe_zero, Submodule.map_bot]
+    simp only [val_eq_coe, coe_zero, Submodule.map_bot]
     exact coeToSubmodule_eq_bot.mp rfl
   map_add' I J := by
     rw [Subtype.ext_iff]
     simp
   map_mul' I J := by
     rw [Subtype.ext_iff]
-    simp only [RingEquiv.toRingHom_eq_coe, val_eq_coe, coe_mul, coe_mk]
+    simp only [val_eq_coe, coe_mul, coe_mk]
     set g := (IsFractionRing.semilinearEquivOfRingEquiv K L f) with hg
     calc Submodule.map g.toLinearMap (↑I * ↑J)
       _ = ⨆ i : I.val, (J.val.map (LinearMap.mul R K i)).map g.toLinearMap := by
@@ -979,8 +977,7 @@ noncomputable def ringHomOfRingEquiv (f : R ≃+* S) :
         constructor <;> rintro ⟨y, hy⟩
         · refine ⟨⟨g y, Submodule.mem_map.mpr ⟨y.1, y.2, rfl⟩⟩, Eq.trans ?_ hy⟩
           ext x
-          simp only [RingEquiv.toRingHom_eq_coe, val_eq_coe, Submodule.mem_map, mem_coe,
-            LinearMap.mul_apply_apply]
+          simp only [val_eq_coe, Submodule.mem_map, mem_coe, LinearMap.mul_apply_apply]
           refine ⟨fun  ⟨w, ⟨z, hzJ, hzy⟩, hw⟩ ↦ ⟨g.symm x, ⟨z, hzJ, ?_⟩, by simp⟩,
             fun ⟨w, ⟨⟨z, hzJ, hzw⟩, hw⟩⟩ ↦ ⟨g z, ⟨z, hzJ, rfl⟩, ?_⟩⟩
           · simp [← (LinearEquiv.injective g).eq_iff, ← hw, ← hzy,
@@ -989,7 +986,7 @@ noncomputable def ringHomOfRingEquiv (f : R ≃+* S) :
         · obtain ⟨y', hy', fy_eq⟩ := Submodule.mem_map.mp y.2
           refine ⟨⟨y', hy'⟩, Eq.trans ?_ hy⟩
           ext x
-          simp only [RingEquiv.toRingHom_eq_coe, val_eq_coe, Submodule.mem_map, mem_coe,
+          simp only [val_eq_coe, Submodule.mem_map, mem_coe,
             LinearMap.mul_apply_apply, ← fy_eq, LinearEquiv.coe_coe]
           refine ⟨fun ⟨w, ⟨z, hzJ, hzy⟩, hw⟩ ↦ ⟨g z, ⟨z, hzJ, rfl⟩, ?_⟩,
             fun ⟨y, ⟨⟨z, hzJ, hzy⟩, hy⟩⟩ ↦ ⟨g.symm x, ⟨z, hzJ, ?_⟩, by simp⟩⟩
@@ -997,8 +994,15 @@ noncomputable def ringHomOfRingEquiv (f : R ≃+* S) :
           · simp [← (LinearEquiv.injective g).eq_iff, hg,
               IsFractionRing.semilinearEquivOfRingEquiv, ← hzy, ← hy]
 
+@[simp]
+lemma ringHomOfRingEquiv_apply (f : R ≃+* S) (I : FractionalIdeal (nonZeroDivisors R) K) :
+    ringHomOfRingEquiv K L f I =
+      ⟨Submodule.map (IsFractionRing.semilinearEquivOfRingEquiv _ _ f).toLinearMap I.val,
+        IsFractional.map' K L f I.prop⟩ := rfl
+
 /-- The equiv `FractionalIdeal (nonZeroDivisors R) K ≃+* FractionalIdeal (nonZeroDivisors S) L`
   induced by a ring isomorphism `f : R ≃+* S`. -/
+@[simps]
 noncomputable def ringEquivOfRingEquiv :
     FractionalIdeal (nonZeroDivisors R) K ≃+* FractionalIdeal (nonZeroDivisors S) L :=
   { FractionalIdeal.ringHomOfRingEquiv K L f with
@@ -1006,8 +1010,8 @@ noncomputable def ringEquivOfRingEquiv :
     left_inv I := by
       have : RingHomCompTriple (f : R →+* S) (f.symm : S →+* R) (RingHom.id R) := ⟨by simp⟩
       rw [Subtype.ext_iff]
-      simp only [ringHomOfRingEquiv, RingEquiv.toRingHom_eq_coe, RingEquiv.symm_symm, val_eq_coe,
-        RingHom.toMonoidHom_eq_coe, RingHom.coe_monoidHom_mk, OneHom.toFun_eq_coe, OneHom.coe_mk,
+      simp only [ringHomOfRingEquiv, RingEquiv.symm_symm, val_eq_coe, RingHom.toMonoidHom_eq_coe,
+        RingHom.coe_monoidHom_mk, OneHom.toFun_eq_coe, OneHom.coe_mk,
         RingHom.coe_mk, MonoidHom.coe_mk, coe_mk, ← Submodule.map_comp (σ₁₃ := RingHom.id R)]
       convert Submodule.map_id _
       ext x
@@ -1018,9 +1022,9 @@ noncomputable def ringEquivOfRingEquiv :
     right_inv I := by
       have : RingHomCompTriple (f.symm : S →+* R) (f : R →+* S) (RingHom.id S) := ⟨by simp⟩
       rw [Subtype.ext_iff]
-      simp only [ringHomOfRingEquiv, RingEquiv.toRingHom_eq_coe, RingEquiv.symm_symm, val_eq_coe,
-        RingHom.toMonoidHom_eq_coe, RingHom.coe_monoidHom_mk, OneHom.toFun_eq_coe, OneHom.coe_mk,
-        RingHom.coe_mk, MonoidHom.coe_mk, coe_mk, ← Submodule.map_comp (σ₁₃ := RingHom.id S)]
+      simp only [ringHomOfRingEquiv, RingEquiv.symm_symm, val_eq_coe, RingHom.toMonoidHom_eq_coe,
+        RingHom.coe_monoidHom_mk, OneHom.toFun_eq_coe, OneHom.coe_mk, RingHom.coe_mk,
+        MonoidHom.coe_mk, coe_mk, ← Submodule.map_comp (σ₁₃ := RingHom.id S)]
       convert Submodule.map_id _
       ext x
       simp only [LinearEquiv.comp_coe, LinearEquiv.coe_coe, LinearEquiv.trans_apply,
@@ -1031,10 +1035,9 @@ noncomputable def ringEquivOfRingEquiv :
 lemma ringEquivOfRingEquiv_spanSingleton (x : K) :
     FractionalIdeal.ringEquivOfRingEquiv K L f (spanSingleton (nonZeroDivisors R) x) =
       spanSingleton (nonZeroDivisors S) (IsFractionRing.ringEquivOfRingEquiv (L := L) f x) := by
-  simp only [ringEquivOfRingEquiv, ringHomOfRingEquiv, RingEquiv.toRingHom_eq_coe, val_eq_coe,
-    RingHom.toMonoidHom_eq_coe, RingHom.coe_monoidHom_mk, OneHom.toFun_eq_coe, OneHom.coe_mk,
-    RingEquiv.symm_symm, RingHom.coe_mk, MonoidHom.coe_mk, RingEquiv.coe_mk, Equiv.coe_fn_mk,
-    coe_spanSingleton]
+  simp only [ringEquivOfRingEquiv, ringHomOfRingEquiv, val_eq_coe, RingHom.toMonoidHom_eq_coe,
+    RingHom.coe_monoidHom_mk, OneHom.toFun_eq_coe, OneHom.coe_mk, RingEquiv.symm_symm,
+    RingHom.coe_mk, MonoidHom.coe_mk, RingEquiv.coe_mk, Equiv.coe_fn_mk, coe_spanSingleton]
   rw [Subtype.ext_iff]
   simp only [val_eq_coe, coe_spanSingleton]
   ext I
@@ -1042,7 +1045,7 @@ lemma ringEquivOfRingEquiv_spanSingleton (x : K) :
   refine ⟨fun ⟨r, hr⟩ ↦ ?_, fun ⟨s, hs⟩ ↦ ?_⟩
   · use f r
     rw [← (IsFractionRing.semilinearEquivOfRingEquiv K L f).injective.eq_iff] at hr
-    simp only [RingEquiv.toRingHom_eq_coe, LinearEquiv.apply_symm_apply] at hr
+    simp only [LinearEquiv.apply_symm_apply] at hr
     simp only [IsFractionRing.ringEquivOfRingEquiv, IsLocalization.ringEquivOfRingEquiv_apply, ← hr]
     exact Eq.symm (map_smulₛₗ _ r x)
   · use f.symm s
diff --git a/Mathlib/RingTheory/Localization/FractionRing.lean b/Mathlib/RingTheory/Localization/FractionRing.lean
index 4b4b60cffe3294..fee58a71242889 100644
--- a/Mathlib/RingTheory/Localization/FractionRing.lean
+++ b/Mathlib/RingTheory/Localization/FractionRing.lean
@@ -9,6 +9,7 @@ public import Mathlib.Algebra.Field.Equiv
 public import Mathlib.Algebra.Field.Subfield.Basic
 public import Mathlib.Algebra.Order.GroupWithZero.Submonoid
 public import Mathlib.Algebra.Order.Ring.Int
+public import Mathlib.Algebra.Ring.CompTypeclasses
 public import Mathlib.RingTheory.Localization.Basic
 public import Mathlib.RingTheory.SimpleRing.Basic
 
@@ -426,18 +427,13 @@ end ringEquivOfRingEquiv
 
 section semilinearEquivOfRingEquiv
 
-instance _root_.RingHomInvPair.ofRingEquiv {R S : Type*} [CommSemiring R] [CommSemiring S]
-    (f : R ≃+* S) : RingHomInvPair f.toRingHom f.symm.toRingHom where
-  comp_eq := by simp
-  comp_eq₂ := by simp_all
-
 variable {A B : Type*} (K L : Type*) [CommRing A] [CommRing B] [CommRing K] [CommRing L]
     [Algebra A K] [IsFractionRing A K] [Algebra B L] [IsFractionRing B L] (f : A ≃+* B)
 
 /-- Given rings `A, B` and localization maps to their fraction rings
 `f : A →+* K, g : B →+* L`, an isomorphism `h : A ≃+* B` induces a semilinear equivalence
 fraction rings `K ≃ₛₗ[f.toRingHom] L`. -/
-noncomputable def semilinearEquivOfRingEquiv : K ≃ₛₗ[f.toRingHom] L :=
+noncomputable def semilinearEquivOfRingEquiv : K ≃ₛₗ[(f : A →+* B)] L :=
 { ringEquivOfRingEquiv f with
   map_smul' r x := by simp [Algebra.smul_def] }
 

From 3b717ee081ae72b9220ef1d41dedafd037b9c95f Mon Sep 17 00:00:00 2001
From: mariainesdff <mariaines.dff@gmail.com>
Date: Mon, 23 Feb 2026 16:38:20 +0100
Subject: [PATCH 03/14] suggested change

---
 .../FractionalIdeal/Operations.lean           | 64 ++++++++++++-------
 .../RingTheory/Localization/FractionRing.lean | 24 ++++++-
 2 files changed, 64 insertions(+), 24 deletions(-)

diff --git a/Mathlib/RingTheory/FractionalIdeal/Operations.lean b/Mathlib/RingTheory/FractionalIdeal/Operations.lean
index 0472e2f3bb3ede..1702631cf52b8a 100644
--- a/Mathlib/RingTheory/FractionalIdeal/Operations.lean
+++ b/Mathlib/RingTheory/FractionalIdeal/Operations.lean
@@ -1000,6 +1000,42 @@ lemma ringHomOfRingEquiv_apply (f : R ≃+* S) (I : FractionalIdeal (nonZeroDivi
       ⟨Submodule.map (IsFractionRing.semilinearEquivOfRingEquiv _ _ f).toLinearMap I.val,
         IsFractional.map' K L f I.prop⟩ := rfl
 
+@[simp]
+lemma ringHomOfRingEquiv_comp {T : Type*} [CommRing T] [IsDomain T] (M : Type*) [CommRing M]
+    [Algebra T M] [IsFractionRing T M]
+    (f : R ≃+* S) (g : S ≃+* T) :
+    ringHomOfRingEquiv K M (f.trans g) =
+      (ringHomOfRingEquiv L M g).comp (ringHomOfRingEquiv K L f) := by
+  have : RingHomCompTriple f (g : S →+* T) (f.trans g : R →+* T) := ⟨rfl⟩
+  apply RingHom.ext
+  intro I
+  rw [Subtype.ext_iff]
+  simp only [ringHomOfRingEquiv, RingEquiv.coe_ringHom_trans, val_eq_coe, RingHom.coe_mk,
+    MonoidHom.coe_mk, OneHom.coe_mk, coe_mk, RingHom.coe_comp, Function.comp_apply]
+  rw [← Submodule.map_comp, IsFractionRing.semilinearEquivOfRingEquiv_comp K L f M]
+  rfl
+
+@[simp]
+lemma ringHomOfRingEquiv_comp_apply {T : Type*} [CommRing T] [IsDomain T] (M : Type*) [CommRing M]
+    [Algebra T M] [IsFractionRing T M]
+    (f : R ≃+* S) (g : S ≃+* T) (I : FractionalIdeal R⁰ K) :
+    ringHomOfRingEquiv K M (f.trans g) I =
+      (ringHomOfRingEquiv L M g) ((ringHomOfRingEquiv K L f) I) := by
+  have : RingHomCompTriple f (g : S →+* T) (f.trans g : R →+* T) := ⟨rfl⟩
+  rw [ringHomOfRingEquiv_comp K L M]
+  simp
+
+lemma ringHomOfRingEquiv_refl :
+    ringHomOfRingEquiv K K (RingEquiv.refl R) = RingHom.id (FractionalIdeal R⁰ K) := by
+  apply RingHom.ext
+  intro I
+  rw [Subtype.ext_iff]
+  simp only [ringHomOfRingEquiv_apply, RingEquiv.coe_ringHom_refl, RingEquiv.symm_refl, val_eq_coe,
+    coe_mk, RingHom.id_apply]
+  convert Submodule.map_id _
+  ext x
+  simp [IsFractionRing.semilinearEquivOfRingEquiv]
+
 /-- The equiv `FractionalIdeal (nonZeroDivisors R) K ≃+* FractionalIdeal (nonZeroDivisors S) L`
   induced by a ring isomorphism `f : R ≃+* S`. -/
 @[simps]
@@ -1009,28 +1045,13 @@ noncomputable def ringEquivOfRingEquiv :
     invFun := FractionalIdeal.ringHomOfRingEquiv L K f.symm
     left_inv I := by
       have : RingHomCompTriple (f : R →+* S) (f.symm : S →+* R) (RingHom.id R) := ⟨by simp⟩
-      rw [Subtype.ext_iff]
-      simp only [ringHomOfRingEquiv, RingEquiv.symm_symm, val_eq_coe, RingHom.toMonoidHom_eq_coe,
-        RingHom.coe_monoidHom_mk, OneHom.toFun_eq_coe, OneHom.coe_mk,
-        RingHom.coe_mk, MonoidHom.coe_mk, coe_mk, ← Submodule.map_comp (σ₁₃ := RingHom.id R)]
-      convert Submodule.map_id _
-      ext x
-      simp only [LinearEquiv.comp_coe, LinearEquiv.coe_coe, LinearEquiv.trans_apply,
-        LinearMap.id_coe, id_eq]
-      exact (LinearEquiv.eq_symm_apply
-        (IsFractionRing.semilinearEquivOfRingEquiv _ _ f.symm)).mp rfl
+      erw [← RingHom.comp_apply]
+      simp [← ringHomOfRingEquiv_comp, ringHomOfRingEquiv_refl]
     right_inv I := by
       have : RingHomCompTriple (f.symm : S →+* R) (f : R →+* S) (RingHom.id S) := ⟨by simp⟩
-      rw [Subtype.ext_iff]
-      simp only [ringHomOfRingEquiv, RingEquiv.symm_symm, val_eq_coe, RingHom.toMonoidHom_eq_coe,
-        RingHom.coe_monoidHom_mk, OneHom.toFun_eq_coe, OneHom.coe_mk, RingHom.coe_mk,
-        MonoidHom.coe_mk, coe_mk, ← Submodule.map_comp (σ₁₃ := RingHom.id S)]
-      convert Submodule.map_id _
-      ext x
-      simp only [LinearEquiv.comp_coe, LinearEquiv.coe_coe, LinearEquiv.trans_apply,
-        LinearMap.id_coe, id_eq]
-      exact (LinearEquiv.eq_symm_apply
-        (IsFractionRing.semilinearEquivOfRingEquiv _ _ f)).mp rfl }
+      have h := ringHomOfRingEquiv_comp_apply L K L f.symm f I
+      simp only [RingEquiv.symm_trans_self, ringHomOfRingEquiv_refl, RingHom.id_apply] at h
+      exact h.symm }
 
 lemma ringEquivOfRingEquiv_spanSingleton (x : K) :
     FractionalIdeal.ringEquivOfRingEquiv K L f (spanSingleton (nonZeroDivisors R) x) =
@@ -1052,8 +1073,7 @@ lemma ringEquivOfRingEquiv_spanSingleton (x : K) :
     simp only [Algebra.smul_def, ← hs]
     rw [IsFractionRing.semilinearEquivOfRingEquiv_symm_apply]
     simp only [ map_mul, RingEquiv.symm_apply_apply]
-    simp [IsFractionRing.ringEquivOfRingEquiv_symm,
-      IsFractionRing.ringEquivOfRingEquiv_algebraMap]
+    simp [IsFractionRing.ringEquivOfRingEquiv_symm]
 
 lemma ringEquivOfRingEquiv_symm_eq :
     (FractionalIdeal.ringEquivOfRingEquiv K L f).symm =
diff --git a/Mathlib/RingTheory/Localization/FractionRing.lean b/Mathlib/RingTheory/Localization/FractionRing.lean
index fee58a71242889..a1aeb1b45bef9e 100644
--- a/Mathlib/RingTheory/Localization/FractionRing.lean
+++ b/Mathlib/RingTheory/Localization/FractionRing.lean
@@ -411,18 +411,26 @@ variable {A K B L : Type*} [CommRing A] [CommRing B] [CommRing K] [CommRing L]
 /-- Given rings `A, B` and localization maps to their fraction rings
 `f : A →+* K, g : B →+* L`, an isomorphism `h : A ≃+* B` induces an isomorphism of
 fraction rings `K ≃+* L`. -/
+@[simps!]
 noncomputable def ringEquivOfRingEquiv : K ≃+* L :=
   IsLocalization.ringEquivOfRingEquiv K L h (MulEquivClass.map_nonZeroDivisors h)
 
-@[simp]
 lemma ringEquivOfRingEquiv_algebraMap
     (a : A) : ringEquivOfRingEquiv h (algebraMap A K a) = algebraMap B L (h a) := by
-  simp [ringEquivOfRingEquiv]
+  simp
 
 @[simp]
 lemma ringEquivOfRingEquiv_symm :
     (ringEquivOfRingEquiv h : K ≃+* L).symm = ringEquivOfRingEquiv h.symm := rfl
 
+variable (K L) in
+theorem ringEquivOfRingEquiv_comp {C : Type*} (M : Type*) [CommRing C]
+  [CommRing M] [Algebra C M] [IsFractionRing C M] (f : A ≃+* B) (g : B ≃+* C) :
+  (ringEquivOfRingEquiv (f.trans g)) =
+    (ringEquivOfRingEquiv (K := K) f).trans (ringEquivOfRingEquiv (K := L) (L := M) g) := by
+  ext a
+  simp [IsLocalization.map_map]
+
 end ringEquivOfRingEquiv
 
 section semilinearEquivOfRingEquiv
@@ -448,6 +456,18 @@ lemma semilinearEquivOfRingEquiv_algebraMap (a : A) :
 lemma semilinearEquivOfRingEquiv_symm_apply (x : L) :
     (semilinearEquivOfRingEquiv K L f).symm x = (ringEquivOfRingEquiv f).symm x := rfl
 
+lemma semilinearEquivOfRingEquiv_comp {C : Type*} (M : Type*) [CommRing C] [CommRing M]
+    [Algebra C M] [IsFractionRing C M] (g : B ≃+* C) :
+    let : RingHomCompTriple f (g : B →+* C) (f.trans g : A →+* C) := ⟨rfl⟩
+    let : RingHomCompTriple g.symm (f.symm : B →+* A) ((f.trans g).symm : C →+* A) := ⟨rfl⟩
+    (semilinearEquivOfRingEquiv K M (f.trans g)) =
+      LinearEquiv.trans (σ₁₃ := (f.trans g)) (σ₃₁ := (f.trans g).symm)
+      (semilinearEquivOfRingEquiv K L f)
+      (semilinearEquivOfRingEquiv L M g) := by
+  ext a
+  simp [semilinearEquivOfRingEquiv_apply, semilinearEquivOfRingEquiv_apply K M,
+    ringEquivOfRingEquiv_comp K L M]
+
 end semilinearEquivOfRingEquiv
 
 section algEquivOfAlgEquiv

From cbb0ffe1df8bbd3f59a6c014cc66b05681282c47 Mon Sep 17 00:00:00 2001
From: mariainesdff <mariaines.dff@gmail.com>
Date: Mon, 23 Feb 2026 16:47:47 +0100
Subject: [PATCH 04/14] fix build

---
 Mathlib/RingTheory/IntegralClosure/IsIntegral/Basic.lean | 3 +--
 Mathlib/RingTheory/LocalProperties/Basic.lean            | 2 +-
 2 files changed, 2 insertions(+), 3 deletions(-)

diff --git a/Mathlib/RingTheory/IntegralClosure/IsIntegral/Basic.lean b/Mathlib/RingTheory/IntegralClosure/IsIntegral/Basic.lean
index 4a1f77290daef8..ab077954e84a6b 100644
--- a/Mathlib/RingTheory/IntegralClosure/IsIntegral/Basic.lean
+++ b/Mathlib/RingTheory/IntegralClosure/IsIntegral/Basic.lean
@@ -175,8 +175,7 @@ theorem RingEquiv.isIntegral_iff {R S T : Type*} [CommRing R] [Ring S] [CommRing
       ⟨fun r t s ↦ by simp only [Algebra.smul_def, map_mul, ← h, mul_assoc]; rfl⟩
     exact IsIntegral.tower_top ha
   · have h' : (algebraMap T S) = (algebraMap R S).comp φ.symm.toRingHom := by
-      simp only [← h, RingHom.comp_assoc, RingEquiv.toRingHom_eq_coe, RingEquiv.comp_symm,
-        RingHomCompTriple.comp_eq]
+      simp only [← h, RingHom.comp_assoc, RingEquiv.toRingHom_eq_coe, RingHomCompTriple.comp_eq]
     letI : Algebra T R := φ.symm.toRingHom.toAlgebra
     letI : IsScalarTower T R S :=
       ⟨fun r t s ↦ by simp only [Algebra.smul_def, map_mul, h', mul_assoc]; rfl⟩
diff --git a/Mathlib/RingTheory/LocalProperties/Basic.lean b/Mathlib/RingTheory/LocalProperties/Basic.lean
index 1a6cdc0095f8fb..92f02635a50a60 100644
--- a/Mathlib/RingTheory/LocalProperties/Basic.lean
+++ b/Mathlib/RingTheory/LocalProperties/Basic.lean
@@ -332,7 +332,7 @@ lemma RingHom.LocalizationAwayPreserves.respectsIso
     have : (IsLocalization.Away.map R T f 1).comp e.symm.toRingHom = f :=
       IsLocalization.map_comp ..
     conv_lhs => rw [← this, RingHom.comp_assoc]
-    simp only [RingEquiv.toRingHom_eq_coe, RingEquiv.symm_comp, RingHomCompTriple.comp_eq]
+    simp only [RingEquiv.toRingHom_eq_coe, RingHomCompTriple.comp_eq]
 
 lemma RingHom.StableUnderCompositionWithLocalizationAway.respectsIso
     (hP : StableUnderCompositionWithLocalizationAway P) :

From 162070256eab37154ea2d612e7a75e85265ef9a7 Mon Sep 17 00:00:00 2001
From: mariainesdff <mariaines.dff@gmail.com>
Date: Wed, 25 Feb 2026 10:13:24 +0100
Subject: [PATCH 05/14] lint

---
 Mathlib/RingTheory/FractionalIdeal/Operations.lean | 2 --
 1 file changed, 2 deletions(-)

diff --git a/Mathlib/RingTheory/FractionalIdeal/Operations.lean b/Mathlib/RingTheory/FractionalIdeal/Operations.lean
index 1702631cf52b8a..2521ff8bff6d57 100644
--- a/Mathlib/RingTheory/FractionalIdeal/Operations.lean
+++ b/Mathlib/RingTheory/FractionalIdeal/Operations.lean
@@ -1000,7 +1000,6 @@ lemma ringHomOfRingEquiv_apply (f : R ≃+* S) (I : FractionalIdeal (nonZeroDivi
       ⟨Submodule.map (IsFractionRing.semilinearEquivOfRingEquiv _ _ f).toLinearMap I.val,
         IsFractional.map' K L f I.prop⟩ := rfl
 
-@[simp]
 lemma ringHomOfRingEquiv_comp {T : Type*} [CommRing T] [IsDomain T] (M : Type*) [CommRing M]
     [Algebra T M] [IsFractionRing T M]
     (f : R ≃+* S) (g : S ≃+* T) :
@@ -1015,7 +1014,6 @@ lemma ringHomOfRingEquiv_comp {T : Type*} [CommRing T] [IsDomain T] (M : Type*)
   rw [← Submodule.map_comp, IsFractionRing.semilinearEquivOfRingEquiv_comp K L f M]
   rfl
 
-@[simp]
 lemma ringHomOfRingEquiv_comp_apply {T : Type*} [CommRing T] [IsDomain T] (M : Type*) [CommRing M]
     [Algebra T M] [IsFractionRing T M]
     (f : R ≃+* S) (g : S ≃+* T) (I : FractionalIdeal R⁰ K) :

From 303359370682de516a40fe4e2767ccd823d15b5c Mon Sep 17 00:00:00 2001
From: mariainesdff <mariaines.dff@gmail.com>
Date: Wed, 4 Mar 2026 11:21:01 +0100
Subject: [PATCH 06/14] suggested changes

---
 .../FractionalIdeal/Operations.lean           | 171 +++++++-----------
 1 file changed, 68 insertions(+), 103 deletions(-)

diff --git a/Mathlib/RingTheory/FractionalIdeal/Operations.lean b/Mathlib/RingTheory/FractionalIdeal/Operations.lean
index 2521ff8bff6d57..d323788e6236a2 100644
--- a/Mathlib/RingTheory/FractionalIdeal/Operations.lean
+++ b/Mathlib/RingTheory/FractionalIdeal/Operations.lean
@@ -922,10 +922,15 @@ variable {R S : Type*} (K L : Type*) [CommRing R] [IsDomain R] [CommRing S] [IsD
   [CommRing K] [CommRing L] [Algebra R K] [Algebra S L] [IsFractionRing R K] [IsFractionRing S L]
   (f : R ≃+* S)
 
+/-- If `f : R →+* S` is a surjective ring homomorphism and `I : Submodule R K` is fractional
+with respect to `R⁰`, then `I.map (IsFractionRing.semilinearEquivOfRingEquiv K L f).toLinearMap`
+is fractional with respect to `S⁰`.
+
+Do not confuse with `IsFractional.map`. -/
 theorem _root_.IsFractional.map' [RingHomSurjective (f : R →+* S)]
-    {I : Submodule R K} (hI : IsFractional (nonZeroDivisors R) I) :
-    IsFractional (nonZeroDivisors S)
-      (Submodule.map (IsFractionRing.semilinearEquivOfRingEquiv K L f).toLinearMap I) := by
+    {I : Submodule R K} (hI : IsFractional R⁰ I) :
+    IsFractional S⁰
+      (I.map (IsFractionRing.semilinearEquivOfRingEquiv K L f).toLinearMap) := by
   simp only [IsFractional, mem_nonZeroDivisors_iff_ne_zero, ne_eq, Submodule.mem_map,
     forall_exists_index, and_imp, forall_apply_eq_imp_iff₂] at hI ⊢
   obtain ⟨r, hr0, hr⟩ := hI
@@ -941,122 +946,80 @@ theorem _root_.IsFractional.map' [RingHomSurjective (f : R →+* S)]
   rw [Algebra.smul_def, ← IsFractionRing.ringEquivOfRingEquiv_algebraMap f (K := K) (L := L) r,
     ← map_mul, ← Algebra.smul_def, ← hr', IsFractionRing.ringEquivOfRingEquiv_algebraMap]
 
-/-- The map `FractionalIdeal (nonZeroDivisors R) K →+* FractionalIdeal (nonZeroDivisors S) L`
+/-- The equiv `FractionalIdeal R⁰ K ≃+* FractionalIdeal S⁰ L`
   induced by a ring isomorphism `f : R ≃+* S`. -/
---@[simps]
-noncomputable def ringHomOfRingEquiv (f : R ≃+* S) :
-    FractionalIdeal (nonZeroDivisors R) K →+* FractionalIdeal (nonZeroDivisors S) L where
-  toFun I := ⟨Submodule.map (IsFractionRing.semilinearEquivOfRingEquiv _ _ f).toLinearMap I.val,
+@[simps -isSimp]
+noncomputable def ringEquivOfRingEquiv :
+    FractionalIdeal R⁰ K ≃+* FractionalIdeal S⁰ L :=
+  { toFun I := ⟨Submodule.map (IsFractionRing.semilinearEquivOfRingEquiv _ _ f).toLinearMap I.val,
       IsFractional.map' K L f I.prop⟩
-  map_one' := by
-    rw [Subtype.ext_iff]
-    ext x
-    simp only [val_eq_coe, coe_one, Submodule.mem_map_equiv, Submodule.mem_one]
-    refine ⟨fun ⟨r, hr⟩ ↦ ⟨f r, ?_⟩, fun ⟨s, hs⟩ ↦ ⟨f.symm s, ?_⟩⟩
-    · simp only [← (LinearEquiv.injective (IsFractionRing.semilinearEquivOfRingEquiv K L f)).eq_iff,
-        LinearEquiv.apply_symm_apply] at hr
-      simp [← hr, IsFractionRing.semilinearEquivOfRingEquiv]
-    · rw [← hs, IsFractionRing.semilinearEquivOfRingEquiv_symm_apply]; simp
-  map_zero' := by
-    simp only [val_eq_coe, coe_zero, Submodule.map_bot]
-    exact coeToSubmodule_eq_bot.mp rfl
-  map_add' I J := by
-    rw [Subtype.ext_iff]
-    simp
-  map_mul' I J := by
-    rw [Subtype.ext_iff]
-    simp only [val_eq_coe, coe_mul, coe_mk]
-    set g := (IsFractionRing.semilinearEquivOfRingEquiv K L f) with hg
-    calc Submodule.map g.toLinearMap (↑I * ↑J)
-      _ = ⨆ i : I.val, (J.val.map (LinearMap.mul R K i)).map g.toLinearMap := by
-        rw [Submodule.mul_eq_map₂]; apply Submodule.map_iSup
-      _ = Submodule.map g.toLinearMap ↑I * Submodule.map g.toLinearMap ↑J := by
-        rw [Submodule.mul_eq_map₂]
-        apply congr_arg sSup
-        ext S
-        constructor <;> rintro ⟨y, hy⟩
-        · refine ⟨⟨g y, Submodule.mem_map.mpr ⟨y.1, y.2, rfl⟩⟩, Eq.trans ?_ hy⟩
-          ext x
-          simp only [val_eq_coe, Submodule.mem_map, mem_coe, LinearMap.mul_apply_apply]
-          refine ⟨fun  ⟨w, ⟨z, hzJ, hzy⟩, hw⟩ ↦ ⟨g.symm x, ⟨z, hzJ, ?_⟩, by simp⟩,
-            fun ⟨w, ⟨⟨z, hzJ, hzw⟩, hw⟩⟩ ↦ ⟨g z, ⟨z, hzJ, rfl⟩, ?_⟩⟩
-          · simp [← (LinearEquiv.injective g).eq_iff, ← hw, ← hzy,
-                hg, IsFractionRing.semilinearEquivOfRingEquiv]
-          · simp [← hw, ← hzw, hg, IsFractionRing.semilinearEquivOfRingEquiv]
-        · obtain ⟨y', hy', fy_eq⟩ := Submodule.mem_map.mp y.2
-          refine ⟨⟨y', hy'⟩, Eq.trans ?_ hy⟩
-          ext x
-          simp only [val_eq_coe, Submodule.mem_map, mem_coe,
-            LinearMap.mul_apply_apply, ← fy_eq, LinearEquiv.coe_coe]
-          refine ⟨fun ⟨w, ⟨z, hzJ, hzy⟩, hw⟩ ↦ ⟨g z, ⟨z, hzJ, rfl⟩, ?_⟩,
-            fun ⟨y, ⟨⟨z, hzJ, hzy⟩, hy⟩⟩ ↦ ⟨g.symm x, ⟨z, hzJ, ?_⟩, by simp⟩⟩
-          · simp [hg, IsFractionRing.semilinearEquivOfRingEquiv, ← hw, ← hzy]
-          · simp [← (LinearEquiv.injective g).eq_iff, hg,
-              IsFractionRing.semilinearEquivOfRingEquiv, ← hzy, ← hy]
+    invFun J := ⟨J.val.map (IsFractionRing.semilinearEquivOfRingEquiv _ _ f.symm).toLinearMap,
+      IsFractional.map' L K f.symm J.prop⟩
+    map_add' I J := by
+      rw [Subtype.ext_iff]
+      simp
+    map_mul' I J := by
+      simp only [FractionalIdeal.coe_ext_iff, val_eq_coe, coe_mul, coe_mk]
+      apply le_antisymm <;> simp only [map_le_iff_le_comap, Submodule.mul_le, mem_coe, mem_comap,
+          IsFractionRing.semilinearEquivOfRingEquiv_apply, map_mul, mem_map_equiv,
+          IsFractionRing.semilinearEquivOfRingEquiv_symm_apply, LinearEquiv.coe_coe]
+      · exact fun m hm n hn ↦ Submodule.mul_mem_mul (mem_map_of_mem hm) (mem_map_of_mem hn)
+      · exact fun m hm n hn ↦ Submodule.mul_mem_mul hm hn
+    left_inv I := by
+      simp only [RingEquiv.symm_symm, val_eq_coe, ← Submodule.map_comp, LinearEquiv.comp_coe,
+        coe_ext_iff, coe_mk]
+      convert Submodule.map_id _
+      ext; simp [IsFractionRing.semilinearEquivOfRingEquiv_apply, IsLocalization.map_map]
+    right_inv I := by
+      simp only [RingEquiv.symm_symm, val_eq_coe, ← Submodule.map_comp, LinearEquiv.comp_coe,
+        coe_ext_iff, coe_mk]
+      convert Submodule.map_id _
+      ext; simp [IsFractionRing.semilinearEquivOfRingEquiv_apply, IsLocalization.map_map]}
 
-@[simp]
-lemma ringHomOfRingEquiv_apply (f : R ≃+* S) (I : FractionalIdeal (nonZeroDivisors R) K) :
-    ringHomOfRingEquiv K L f I =
+lemma ringEquivOfRingEquiv_apply (f : R ≃+* S) (I : FractionalIdeal (nonZeroDivisors R) K) :
+    ringEquivOfRingEquiv K L f I =
       ⟨Submodule.map (IsFractionRing.semilinearEquivOfRingEquiv _ _ f).toLinearMap I.val,
         IsFractional.map' K L f I.prop⟩ := rfl
 
-lemma ringHomOfRingEquiv_comp {T : Type*} [CommRing T] [IsDomain T] (M : Type*) [CommRing M]
+lemma ringEquivOfRingEquiv_apply_val (f : R ≃+* S) (I : FractionalIdeal R⁰ K) :
+    (ringEquivOfRingEquiv K L f I).val =
+      I.val.map (IsFractionRing.semilinearEquivOfRingEquiv _ _ f).toLinearMap  := rfl
+
+lemma ringEquivOfRingEquiv_trans {T : Type*} [CommRing T] [IsDomain T] (M : Type*) [CommRing M]
     [Algebra T M] [IsFractionRing T M]
     (f : R ≃+* S) (g : S ≃+* T) :
-    ringHomOfRingEquiv K M (f.trans g) =
-      (ringHomOfRingEquiv L M g).comp (ringHomOfRingEquiv K L f) := by
+    ringEquivOfRingEquiv K M (f.trans g) =
+      (ringEquivOfRingEquiv K L f).trans (ringEquivOfRingEquiv L M g) := by
   have : RingHomCompTriple f (g : S →+* T) (f.trans g : R →+* T) := ⟨rfl⟩
-  apply RingHom.ext
-  intro I
+  ext1 I
   rw [Subtype.ext_iff]
-  simp only [ringHomOfRingEquiv, RingEquiv.coe_ringHom_trans, val_eq_coe, RingHom.coe_mk,
-    MonoidHom.coe_mk, OneHom.coe_mk, coe_mk, RingHom.coe_comp, Function.comp_apply]
+  simp only [ringEquivOfRingEquiv, RingEquiv.coe_ringHom_trans, val_eq_coe, RingEquiv.symm_symm,
+    RingEquiv.coe_mk, Equiv.coe_fn_mk, coe_mk, RingEquiv.coe_trans, Function.comp_apply]
   rw [← Submodule.map_comp, IsFractionRing.semilinearEquivOfRingEquiv_comp K L f M]
   rfl
 
-lemma ringHomOfRingEquiv_comp_apply {T : Type*} [CommRing T] [IsDomain T] (M : Type*) [CommRing M]
-    [Algebra T M] [IsFractionRing T M]
+lemma ringEquivOfRingEquiv_trans_apply {T : Type*} [CommRing T] [IsDomain T] (M : Type*)
+    [CommRing M] [Algebra T M] [IsFractionRing T M]
     (f : R ≃+* S) (g : S ≃+* T) (I : FractionalIdeal R⁰ K) :
-    ringHomOfRingEquiv K M (f.trans g) I =
-      (ringHomOfRingEquiv L M g) ((ringHomOfRingEquiv K L f) I) := by
-  have : RingHomCompTriple f (g : S →+* T) (f.trans g : R →+* T) := ⟨rfl⟩
-  rw [ringHomOfRingEquiv_comp K L M]
-  simp
+    ringEquivOfRingEquiv K M (f.trans g) I =
+      ringEquivOfRingEquiv L M g (ringEquivOfRingEquiv K L f I) := by
+  simp [ringEquivOfRingEquiv_trans K L M]
 
-lemma ringHomOfRingEquiv_refl :
-    ringHomOfRingEquiv K K (RingEquiv.refl R) = RingHom.id (FractionalIdeal R⁰ K) := by
-  apply RingHom.ext
-  intro I
+lemma ringEquivOfRingEquiv_refl :
+    ringEquivOfRingEquiv K K (RingEquiv.refl R) = RingHom.id (FractionalIdeal R⁰ K) := by
+  ext1 I
   rw [Subtype.ext_iff]
-  simp only [ringHomOfRingEquiv_apply, RingEquiv.coe_ringHom_refl, RingEquiv.symm_refl, val_eq_coe,
-    coe_mk, RingHom.id_apply]
+  simp only [RingHom.coe_coe, ringEquivOfRingEquiv_apply, RingEquiv.coe_ringHom_refl,
+    RingEquiv.symm_refl, val_eq_coe, coe_mk, RingHom.id_apply]
   convert Submodule.map_id _
   ext x
   simp [IsFractionRing.semilinearEquivOfRingEquiv]
 
-/-- The equiv `FractionalIdeal (nonZeroDivisors R) K ≃+* FractionalIdeal (nonZeroDivisors S) L`
-  induced by a ring isomorphism `f : R ≃+* S`. -/
-@[simps]
-noncomputable def ringEquivOfRingEquiv :
-    FractionalIdeal (nonZeroDivisors R) K ≃+* FractionalIdeal (nonZeroDivisors S) L :=
-  { FractionalIdeal.ringHomOfRingEquiv K L f with
-    invFun := FractionalIdeal.ringHomOfRingEquiv L K f.symm
-    left_inv I := by
-      have : RingHomCompTriple (f : R →+* S) (f.symm : S →+* R) (RingHom.id R) := ⟨by simp⟩
-      erw [← RingHom.comp_apply]
-      simp [← ringHomOfRingEquiv_comp, ringHomOfRingEquiv_refl]
-    right_inv I := by
-      have : RingHomCompTriple (f.symm : S →+* R) (f : R →+* S) (RingHom.id S) := ⟨by simp⟩
-      have h := ringHomOfRingEquiv_comp_apply L K L f.symm f I
-      simp only [RingEquiv.symm_trans_self, ringHomOfRingEquiv_refl, RingHom.id_apply] at h
-      exact h.symm }
-
 lemma ringEquivOfRingEquiv_spanSingleton (x : K) :
-    FractionalIdeal.ringEquivOfRingEquiv K L f (spanSingleton (nonZeroDivisors R) x) =
-      spanSingleton (nonZeroDivisors S) (IsFractionRing.ringEquivOfRingEquiv (L := L) f x) := by
-  simp only [ringEquivOfRingEquiv, ringHomOfRingEquiv, val_eq_coe, RingHom.toMonoidHom_eq_coe,
-    RingHom.coe_monoidHom_mk, OneHom.toFun_eq_coe, OneHom.coe_mk, RingEquiv.symm_symm,
-    RingHom.coe_mk, MonoidHom.coe_mk, RingEquiv.coe_mk, Equiv.coe_fn_mk, coe_spanSingleton]
+    FractionalIdeal.ringEquivOfRingEquiv K L f (spanSingleton R⁰ x) =
+      spanSingleton S⁰ (IsFractionRing.ringEquivOfRingEquiv (L := L) f x) := by
+  simp only [ringEquivOfRingEquiv, val_eq_coe, RingEquiv.symm_symm, RingEquiv.coe_mk,
+    Equiv.coe_fn_mk, coe_spanSingleton, IsFractionRing.ringEquivOfRingEquiv_apply]
   rw [Subtype.ext_iff]
   simp only [val_eq_coe, coe_spanSingleton]
   ext I
@@ -1065,13 +1028,15 @@ lemma ringEquivOfRingEquiv_spanSingleton (x : K) :
   · use f r
     rw [← (IsFractionRing.semilinearEquivOfRingEquiv K L f).injective.eq_iff] at hr
     simp only [LinearEquiv.apply_symm_apply] at hr
-    simp only [IsFractionRing.ringEquivOfRingEquiv, IsLocalization.ringEquivOfRingEquiv_apply, ← hr]
+    simp only [← hr]
     exact Eq.symm (map_smulₛₗ _ r x)
   · use f.symm s
-    simp only [Algebra.smul_def, ← hs]
-    rw [IsFractionRing.semilinearEquivOfRingEquiv_symm_apply]
-    simp only [ map_mul, RingEquiv.symm_apply_apply]
-    simp [IsFractionRing.ringEquivOfRingEquiv_symm]
+    simp only [Algebra.smul_def, ← hs, IsFractionRing.semilinearEquivOfRingEquiv_symm_apply,
+      map_mul]
+    simp only [IsFractionRing.ringEquivOfRingEquiv_symm, IsFractionRing.ringEquivOfRingEquiv_apply,
+      map_eq, RingHom.coe_coe]
+    rw [← RingHom.comp_apply, IsLocalization.map_comp_map]
+    simp only [RingHomCompTriple.comp_eq, IsLocalization.map_id]
 
 lemma ringEquivOfRingEquiv_symm_eq :
     (FractionalIdeal.ringEquivOfRingEquiv K L f).symm =

From 656ca84d5255a758a65aad4c59b046296025dc97 Mon Sep 17 00:00:00 2001
From: mariainesdff <mariaines.dff@gmail.com>
Date: Wed, 4 Mar 2026 11:38:04 +0100
Subject: [PATCH 07/14] remove instance

---
 Mathlib/Algebra/Ring/CompTypeclasses.lean                | 4 +---
 Mathlib/RingTheory/FractionalIdeal/Operations.lean       | 3 +++
 Mathlib/RingTheory/IntegralClosure/IsIntegral/Basic.lean | 3 +++
 Mathlib/RingTheory/Localization/FractionRing.lean        | 3 +++
 4 files changed, 10 insertions(+), 3 deletions(-)

diff --git a/Mathlib/Algebra/Ring/CompTypeclasses.lean b/Mathlib/Algebra/Ring/CompTypeclasses.lean
index 391e5746c40e3f..930b2f215fc7fe 100644
--- a/Mathlib/Algebra/Ring/CompTypeclasses.lean
+++ b/Mathlib/Algebra/Ring/CompTypeclasses.lean
@@ -120,10 +120,8 @@ def toRingEquiv : R₁ ≃+* R₂ := .ofRingHom σ σ' comp_eq₂ comp_eq
 
 This is not an instance, as for equivalences that are involutions, a better instance
 would be `RingHomInvPair e e`.
-
-Note that for equivalences that are involutions, a better instance would be `RingHomInvPair e e`.
 -/
-instance of_ringEquiv (e : R₁ ≃+* R₂) : RingHomInvPair (↑e : R₁ →+* R₂) ↑e.symm :=
+lemma of_ringEquiv (e : R₁ ≃+* R₂) : RingHomInvPair (↑e : R₁ →+* R₂) ↑e.symm :=
   ⟨e.symm_toRingHom_comp_toRingHom, e.symm.symm_toRingHom_comp_toRingHom⟩
 
 /-- Construct a `RingHomInvPair` from both directions of a ring equiv.
diff --git a/Mathlib/RingTheory/FractionalIdeal/Operations.lean b/Mathlib/RingTheory/FractionalIdeal/Operations.lean
index d323788e6236a2..35e5054150e40f 100644
--- a/Mathlib/RingTheory/FractionalIdeal/Operations.lean
+++ b/Mathlib/RingTheory/FractionalIdeal/Operations.lean
@@ -922,6 +922,9 @@ variable {R S : Type*} (K L : Type*) [CommRing R] [IsDomain R] [CommRing S] [IsD
   [CommRing K] [CommRing L] [Algebra R K] [Algebra S L] [IsFractionRing R K] [IsFractionRing S L]
   (f : R ≃+* S)
 
+local instance (f : R ≃+* S) : RingHomInvPair (f : R →+* S) f.symm :=
+  RingHomInvPair.of_ringEquiv f
+
 /-- If `f : R →+* S` is a surjective ring homomorphism and `I : Submodule R K` is fractional
 with respect to `R⁰`, then `I.map (IsFractionRing.semilinearEquivOfRingEquiv K L f).toLinearMap`
 is fractional with respect to `S⁰`.
diff --git a/Mathlib/RingTheory/IntegralClosure/IsIntegral/Basic.lean b/Mathlib/RingTheory/IntegralClosure/IsIntegral/Basic.lean
index ab077954e84a6b..c64a554d2f1377 100644
--- a/Mathlib/RingTheory/IntegralClosure/IsIntegral/Basic.lean
+++ b/Mathlib/RingTheory/IntegralClosure/IsIntegral/Basic.lean
@@ -162,6 +162,9 @@ theorem IsIntegral.tower_top [Algebra A B] [IsScalarTower R A B] {x : B}
   let ⟨p, hp, hpx⟩ := hx
   ⟨p.map <| algebraMap R A, hp.map _, by rw [← aeval_def, aeval_map_algebraMap, aeval_def, hpx]⟩
 
+local instance (f : R ≃+* S) : RingHomInvPair (f : R →+* S) f.symm :=
+  RingHomInvPair.of_ringEquiv f
+
 /- If `R` and `T` are isomorphic commutative rings and `S` is an `R`-algebra and a `T`-algebra in
 a compatible way, then an element `a ∈ S` is integral over `R` if and only if it is integral
 over `T`. -/
diff --git a/Mathlib/RingTheory/Localization/FractionRing.lean b/Mathlib/RingTheory/Localization/FractionRing.lean
index a1aeb1b45bef9e..82ffaa90782abf 100644
--- a/Mathlib/RingTheory/Localization/FractionRing.lean
+++ b/Mathlib/RingTheory/Localization/FractionRing.lean
@@ -438,6 +438,9 @@ section semilinearEquivOfRingEquiv
 variable {A B : Type*} (K L : Type*) [CommRing A] [CommRing B] [CommRing K] [CommRing L]
     [Algebra A K] [IsFractionRing A K] [Algebra B L] [IsFractionRing B L] (f : A ≃+* B)
 
+local instance : RingHomInvPair (f : A →+* B) f.symm :=
+  RingHomInvPair.of_ringEquiv f
+
 /-- Given rings `A, B` and localization maps to their fraction rings
 `f : A →+* K, g : B →+* L`, an isomorphism `h : A ≃+* B` induces a semilinear equivalence
 fraction rings `K ≃ₛₗ[f.toRingHom] L`. -/

From 689b7e15dbc37df5f40ef173131a5a599d5fc76f Mon Sep 17 00:00:00 2001
From: mariainesdff <mariaines.dff@gmail.com>
Date: Wed, 4 Mar 2026 13:07:27 +0100
Subject: [PATCH 08/14] fix

---
 Mathlib/RingTheory/IntegralClosure/IsIntegral/Basic.lean | 4 +---
 Mathlib/RingTheory/LocalProperties/Basic.lean            | 1 +
 2 files changed, 2 insertions(+), 3 deletions(-)

diff --git a/Mathlib/RingTheory/IntegralClosure/IsIntegral/Basic.lean b/Mathlib/RingTheory/IntegralClosure/IsIntegral/Basic.lean
index c64a554d2f1377..d8061608309f5c 100644
--- a/Mathlib/RingTheory/IntegralClosure/IsIntegral/Basic.lean
+++ b/Mathlib/RingTheory/IntegralClosure/IsIntegral/Basic.lean
@@ -162,9 +162,6 @@ theorem IsIntegral.tower_top [Algebra A B] [IsScalarTower R A B] {x : B}
   let ⟨p, hp, hpx⟩ := hx
   ⟨p.map <| algebraMap R A, hp.map _, by rw [← aeval_def, aeval_map_algebraMap, aeval_def, hpx]⟩
 
-local instance (f : R ≃+* S) : RingHomInvPair (f : R →+* S) f.symm :=
-  RingHomInvPair.of_ringEquiv f
-
 /- If `R` and `T` are isomorphic commutative rings and `S` is an `R`-algebra and a `T`-algebra in
 a compatible way, then an element `a ∈ S` is integral over `R` if and only if it is integral
 over `T`. -/
@@ -178,6 +175,7 @@ theorem RingEquiv.isIntegral_iff {R S T : Type*} [CommRing R] [Ring S] [CommRing
       ⟨fun r t s ↦ by simp only [Algebra.smul_def, map_mul, ← h, mul_assoc]; rfl⟩
     exact IsIntegral.tower_top ha
   · have h' : (algebraMap T S) = (algebraMap R S).comp φ.symm.toRingHom := by
+      have : RingHomInvPair (φ : R →+* T) φ.symm := RingHomInvPair.of_ringEquiv _
       simp only [← h, RingHom.comp_assoc, RingEquiv.toRingHom_eq_coe, RingHomCompTriple.comp_eq]
     letI : Algebra T R := φ.symm.toRingHom.toAlgebra
     letI : IsScalarTower T R S :=
diff --git a/Mathlib/RingTheory/LocalProperties/Basic.lean b/Mathlib/RingTheory/LocalProperties/Basic.lean
index 92f02635a50a60..24c2552addbbbf 100644
--- a/Mathlib/RingTheory/LocalProperties/Basic.lean
+++ b/Mathlib/RingTheory/LocalProperties/Basic.lean
@@ -329,6 +329,7 @@ lemma RingHom.LocalizationAwayPreserves.respectsIso
     have : IsLocalization.Away (f 1) T :=
       IsLocalization.away_of_isUnit_of_bijective _ (by simp) (Equiv.refl _).bijective
     convert hP f 1 R T hf
+    have : RingHomInvPair (e : R →+* S) e.symm := RingHomInvPair.of_ringEquiv _
     have : (IsLocalization.Away.map R T f 1).comp e.symm.toRingHom = f :=
       IsLocalization.map_comp ..
     conv_lhs => rw [← this, RingHom.comp_assoc]

From 8fdb5918d5cbc73d54efbf9d3ce096bb7dc41ced Mon Sep 17 00:00:00 2001
From: mariainesdff <mariaines.dff@gmail.com>
Date: Thu, 5 Mar 2026 12:38:48 +0100
Subject: [PATCH 09/14] fix

---
 Mathlib/RingTheory/Localization/FractionRing.lean | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/Mathlib/RingTheory/Localization/FractionRing.lean b/Mathlib/RingTheory/Localization/FractionRing.lean
index 16e1c9f999e2d5..9050833ca791b4 100644
--- a/Mathlib/RingTheory/Localization/FractionRing.lean
+++ b/Mathlib/RingTheory/Localization/FractionRing.lean
@@ -476,8 +476,8 @@ lemma semilinearEquivOfRingEquiv_comp {C : Type*} (M : Type*) [CommRing C] [Comm
       (semilinearEquivOfRingEquiv K L f)
       (semilinearEquivOfRingEquiv L M g) := by
   ext a
-  simp [semilinearEquivOfRingEquiv_apply, semilinearEquivOfRingEquiv_apply K M,
-    ringEquivOfRingEquiv_comp K L M]
+  simp [-RingEquiv.coe_ringHom_trans, semilinearEquivOfRingEquiv_apply,
+    semilinearEquivOfRingEquiv_apply K M, ringEquivOfRingEquiv_comp K L M]
 
 end semilinearEquivOfRingEquiv
 

From dc8a439359f046cd5350690fd88c3bac67976e03 Mon Sep 17 00:00:00 2001
From: mariainesdff <mariaines.dff@gmail.com>
Date: Fri, 6 Mar 2026 16:04:23 +0100
Subject: [PATCH 10/14] fix

---
 Mathlib/RingTheory/FractionalIdeal/Operations.lean | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/Mathlib/RingTheory/FractionalIdeal/Operations.lean b/Mathlib/RingTheory/FractionalIdeal/Operations.lean
index 35e5054150e40f..286ec7eefb2b75 100644
--- a/Mathlib/RingTheory/FractionalIdeal/Operations.lean
+++ b/Mathlib/RingTheory/FractionalIdeal/Operations.lean
@@ -949,6 +949,7 @@ theorem _root_.IsFractional.map' [RingHomSurjective (f : R →+* S)]
   rw [Algebra.smul_def, ← IsFractionRing.ringEquivOfRingEquiv_algebraMap f (K := K) (L := L) r,
     ← map_mul, ← Algebra.smul_def, ← hr', IsFractionRing.ringEquivOfRingEquiv_algebraMap]
 
+set_option backward.isDefEq.respectTransparency false in
 /-- The equiv `FractionalIdeal R⁰ K ≃+* FractionalIdeal S⁰ L`
   induced by a ring isomorphism `f : R ≃+* S`. -/
 @[simps -isSimp]
@@ -988,6 +989,7 @@ lemma ringEquivOfRingEquiv_apply_val (f : R ≃+* S) (I : FractionalIdeal R⁰ K
     (ringEquivOfRingEquiv K L f I).val =
       I.val.map (IsFractionRing.semilinearEquivOfRingEquiv _ _ f).toLinearMap  := rfl
 
+set_option backward.isDefEq.respectTransparency false in
 lemma ringEquivOfRingEquiv_trans {T : Type*} [CommRing T] [IsDomain T] (M : Type*) [CommRing M]
     [Algebra T M] [IsFractionRing T M]
     (f : R ≃+* S) (g : S ≃+* T) :
@@ -1008,6 +1010,7 @@ lemma ringEquivOfRingEquiv_trans_apply {T : Type*} [CommRing T] [IsDomain T] (M
       ringEquivOfRingEquiv L M g (ringEquivOfRingEquiv K L f I) := by
   simp [ringEquivOfRingEquiv_trans K L M]
 
+set_option backward.isDefEq.respectTransparency false in
 lemma ringEquivOfRingEquiv_refl :
     ringEquivOfRingEquiv K K (RingEquiv.refl R) = RingHom.id (FractionalIdeal R⁰ K) := by
   ext1 I
@@ -1018,6 +1021,7 @@ lemma ringEquivOfRingEquiv_refl :
   ext x
   simp [IsFractionRing.semilinearEquivOfRingEquiv]
 
+set_option backward.isDefEq.respectTransparency false in
 lemma ringEquivOfRingEquiv_spanSingleton (x : K) :
     FractionalIdeal.ringEquivOfRingEquiv K L f (spanSingleton R⁰ x) =
       spanSingleton S⁰ (IsFractionRing.ringEquivOfRingEquiv (L := L) f x) := by

From 13afa3af4f228d5ade1e14f4ef3ea5b293611871 Mon Sep 17 00:00:00 2001
From: mariainesdff <mariaines.dff@gmail.com>
Date: Wed, 8 Apr 2026 18:09:13 +0200
Subject: [PATCH 11/14] suggested change

---
 Mathlib/RingTheory/FractionalIdeal/Operations.lean | 10 ++++------
 1 file changed, 4 insertions(+), 6 deletions(-)

diff --git a/Mathlib/RingTheory/FractionalIdeal/Operations.lean b/Mathlib/RingTheory/FractionalIdeal/Operations.lean
index 286ec7eefb2b75..e068c50197578a 100644
--- a/Mathlib/RingTheory/FractionalIdeal/Operations.lean
+++ b/Mathlib/RingTheory/FractionalIdeal/Operations.lean
@@ -925,15 +925,13 @@ variable {R S : Type*} (K L : Type*) [CommRing R] [IsDomain R] [CommRing S] [IsD
 local instance (f : R ≃+* S) : RingHomInvPair (f : R →+* S) f.symm :=
   RingHomInvPair.of_ringEquiv f
 
-/-- If `f : R →+* S` is a surjective ring homomorphism and `I : Submodule R K` is fractional
-with respect to `R⁰`, then `I.map (IsFractionRing.semilinearEquivOfRingEquiv K L f).toLinearMap`
+/-- If `f : R →+* S` is a ring isomorphism and `I : Submodule R K` is fractional with respect to
+`R⁰`, then `I.map (IsFractionRing.semilinearEquivOfRingEquiv K L f).toLinearMap`
 is fractional with respect to `S⁰`.
 
 Do not confuse with `IsFractional.map`. -/
-theorem _root_.IsFractional.map' [RingHomSurjective (f : R →+* S)]
-    {I : Submodule R K} (hI : IsFractional R⁰ I) :
-    IsFractional S⁰
-      (I.map (IsFractionRing.semilinearEquivOfRingEquiv K L f).toLinearMap) := by
+theorem _root_.IsFractional.map' {I : Submodule R K} (hI : IsFractional R⁰ I) :
+    IsFractional S⁰ (I.map (IsFractionRing.semilinearEquivOfRingEquiv K L f).toLinearMap) := by
   simp only [IsFractional, mem_nonZeroDivisors_iff_ne_zero, ne_eq, Submodule.mem_map,
     forall_exists_index, and_imp, forall_apply_eq_imp_iff₂] at hI ⊢
   obtain ⟨r, hr0, hr⟩ := hI

From 2d0b331a33d5256d8c8992471c0093166b441235 Mon Sep 17 00:00:00 2001
From: mariainesdff <mariaines.dff@gmail.com>
Date: Tue, 28 Apr 2026 11:22:46 +0200
Subject: [PATCH 12/14] test change

---
 Mathlib/RingTheory/FractionalIdeal/Operations.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Mathlib/RingTheory/FractionalIdeal/Operations.lean b/Mathlib/RingTheory/FractionalIdeal/Operations.lean
index 2ffaf71330a12b..4aa59648d5d556 100644
--- a/Mathlib/RingTheory/FractionalIdeal/Operations.lean
+++ b/Mathlib/RingTheory/FractionalIdeal/Operations.lean
@@ -916,7 +916,7 @@ variable {R S : Type*} (K L : Type*) [CommRing R] [IsDomain R] [CommRing S] [IsD
 local instance (f : R ≃+* S) : RingHomInvPair (f : R →+* S) f.symm :=
   RingHomInvPair.of_ringEquiv f
 
-/-- If `f : R →+* S` is a ring isomorphism and `I : Submodule R K` is fractional with respect to
+/-- If `f : R ≃+* S` is a ring isomorphism and `I : Submodule R K` is fractional with respect to
 `R⁰`, then `I.map (IsFractionRing.semilinearEquivOfRingEquiv K L f).toLinearMap`
 is fractional with respect to `S⁰`.
 

From 7d620cc4fcfc80355ccfcdccae0187afac5c8993 Mon Sep 17 00:00:00 2001
From: mariainesdff <mariaines.dff@gmail.com>
Date: Tue, 28 Apr 2026 11:50:34 +0200
Subject: [PATCH 13/14] suggested changes

---
 .../FractionalIdeal/Operations.lean           | 97 ++++++++-----------
 1 file changed, 41 insertions(+), 56 deletions(-)

diff --git a/Mathlib/RingTheory/FractionalIdeal/Operations.lean b/Mathlib/RingTheory/FractionalIdeal/Operations.lean
index 4aa59648d5d556..74119c26b13972 100644
--- a/Mathlib/RingTheory/FractionalIdeal/Operations.lean
+++ b/Mathlib/RingTheory/FractionalIdeal/Operations.lean
@@ -909,6 +909,8 @@ end Adjoin
 
 section RingEquiv
 
+open IsFractionRing
+
 variable {R S : Type*} (K L : Type*) [CommRing R] [IsDomain R] [CommRing S] [IsDomain S]
   [CommRing K] [CommRing L] [Algebra R K] [Algebra S L] [IsFractionRing R K] [IsFractionRing S L]
   (f : R ≃+* S)
@@ -921,8 +923,8 @@ local instance (f : R ≃+* S) : RingHomInvPair (f : R →+* S) f.symm :=
 is fractional with respect to `S⁰`.
 
 Do not confuse with `IsFractional.map`. -/
-theorem _root_.IsFractional.map' {I : Submodule R K} (hI : IsFractional R⁰ I) :
-    IsFractional S⁰ (I.map (IsFractionRing.semilinearEquivOfRingEquiv K L f).toLinearMap) := by
+theorem _root_.IsFractional.mapEquiv {I : Submodule R K} (hI : IsFractional R⁰ I) :
+    IsFractional S⁰ (I.map (semilinearEquivOfRingEquiv K L f).toLinearMap) := by
   simp only [IsFractional, mem_nonZeroDivisors_iff_ne_zero, ne_eq, Submodule.mem_map,
     forall_exists_index, and_imp, forall_apply_eq_imp_iff₂] at hI ⊢
   obtain ⟨r, hr0, hr⟩ := hI
@@ -933,64 +935,57 @@ theorem _root_.IsFractional.map' {I : Submodule R K} (hI : IsFractional R⁰ I)
   simp only [IsLocalization.IsInteger, RingHom.mem_rangeS] at hr ⊢
   obtain ⟨r', hr'⟩ := hr
   use f r'
-  simp only [IsFractionRing.semilinearEquivOfRingEquiv, RingEquiv.toEquiv_eq_coe,
-    Equiv.toFun_as_coe, EquivLike.coe_coe, Equiv.invFun_as_coe, LinearMap.coe_mk, AddHom.coe_mk]
-  rw [Algebra.smul_def, ← IsFractionRing.ringEquivOfRingEquiv_algebraMap f (K := K) (L := L) r,
-    ← map_mul, ← Algebra.smul_def, ← hr', IsFractionRing.ringEquivOfRingEquiv_algebraMap]
+  simp only [semilinearEquivOfRingEquiv, RingEquiv.toEquiv_eq_coe, Equiv.toFun_as_coe,
+    EquivLike.coe_coe, Equiv.invFun_as_coe, LinearMap.coe_mk, AddHom.coe_mk]
+  rw [Algebra.smul_def, ← ringEquivOfRingEquiv_algebraMap f (K := K) (L := L) r,
+    ← map_mul, ← Algebra.smul_def, ← hr', ringEquivOfRingEquiv_algebraMap]
 
-set_option backward.isDefEq.respectTransparency false in
 /-- The equiv `FractionalIdeal R⁰ K ≃+* FractionalIdeal S⁰ L`
   induced by a ring isomorphism `f : R ≃+* S`. -/
 @[simps -isSimp]
 noncomputable def ringEquivOfRingEquiv :
     FractionalIdeal R⁰ K ≃+* FractionalIdeal S⁰ L :=
-  { toFun I := ⟨Submodule.map (IsFractionRing.semilinearEquivOfRingEquiv _ _ f).toLinearMap I.val,
-      IsFractional.map' K L f I.prop⟩
-    invFun J := ⟨J.val.map (IsFractionRing.semilinearEquivOfRingEquiv _ _ f.symm).toLinearMap,
-      IsFractional.map' L K f.symm J.prop⟩
-    map_add' I J := by
-      rw [Subtype.ext_iff]
-      simp
+  { toFun I := ⟨Submodule.map (semilinearEquivOfRingEquiv _ _ f).toLinearMap I.val,
+      IsFractional.mapEquiv K L f I.prop⟩
+    invFun J := ⟨J.val.map (semilinearEquivOfRingEquiv _ _ f.symm).toLinearMap,
+      IsFractional.mapEquiv L K f.symm J.prop⟩
+    map_add' I J := by ext x; simp [← mem_coe]
     map_mul' I J := by
       simp only [FractionalIdeal.coe_ext_iff, val_eq_coe, coe_mul, coe_mk]
       apply le_antisymm <;> simp only [map_le_iff_le_comap, Submodule.mul_le, mem_coe, mem_comap,
-          IsFractionRing.semilinearEquivOfRingEquiv_apply, map_mul, mem_map_equiv,
-          IsFractionRing.semilinearEquivOfRingEquiv_symm_apply, LinearEquiv.coe_coe]
+          semilinearEquivOfRingEquiv_apply, map_mul, mem_map_equiv,
+          semilinearEquivOfRingEquiv_symm_apply, LinearEquiv.coe_coe]
       · exact fun m hm n hn ↦ Submodule.mul_mem_mul (mem_map_of_mem hm) (mem_map_of_mem hn)
       · exact fun m hm n hn ↦ Submodule.mul_mem_mul hm hn
     left_inv I := by
       simp only [RingEquiv.symm_symm, val_eq_coe, ← Submodule.map_comp, LinearEquiv.comp_coe,
         coe_ext_iff, coe_mk]
       convert Submodule.map_id _
-      ext; simp [IsFractionRing.semilinearEquivOfRingEquiv_apply, IsLocalization.map_map]
+      ext; simp [semilinearEquivOfRingEquiv, IsLocalization.map_map]
     right_inv I := by
       simp only [RingEquiv.symm_symm, val_eq_coe, ← Submodule.map_comp, LinearEquiv.comp_coe,
         coe_ext_iff, coe_mk]
       convert Submodule.map_id _
-      ext; simp [IsFractionRing.semilinearEquivOfRingEquiv_apply, IsLocalization.map_map]}
+      ext; simp [semilinearEquivOfRingEquiv, IsLocalization.map_map]}
 
 lemma ringEquivOfRingEquiv_apply (f : R ≃+* S) (I : FractionalIdeal (nonZeroDivisors R) K) :
     ringEquivOfRingEquiv K L f I =
-      ⟨Submodule.map (IsFractionRing.semilinearEquivOfRingEquiv _ _ f).toLinearMap I.val,
-        IsFractional.map' K L f I.prop⟩ := rfl
+      ⟨Submodule.map (semilinearEquivOfRingEquiv _ _ f).toLinearMap I.val,
+        IsFractional.mapEquiv K L f I.prop⟩ := rfl
 
 lemma ringEquivOfRingEquiv_apply_val (f : R ≃+* S) (I : FractionalIdeal R⁰ K) :
     (ringEquivOfRingEquiv K L f I).val =
-      I.val.map (IsFractionRing.semilinearEquivOfRingEquiv _ _ f).toLinearMap  := rfl
+      I.val.map (semilinearEquivOfRingEquiv _ _ f).toLinearMap  := rfl
 
-set_option backward.isDefEq.respectTransparency false in
 lemma ringEquivOfRingEquiv_trans {T : Type*} [CommRing T] [IsDomain T] (M : Type*) [CommRing M]
-    [Algebra T M] [IsFractionRing T M]
-    (f : R ≃+* S) (g : S ≃+* T) :
+    [Algebra T M] [IsFractionRing T M] (f : R ≃+* S) (g : S ≃+* T) :
     ringEquivOfRingEquiv K M (f.trans g) =
       (ringEquivOfRingEquiv K L f).trans (ringEquivOfRingEquiv L M g) := by
   have : RingHomCompTriple f (g : S →+* T) (f.trans g : R →+* T) := ⟨rfl⟩
   ext1 I
-  rw [Subtype.ext_iff]
-  simp only [ringEquivOfRingEquiv, RingEquiv.coe_ringHom_trans, val_eq_coe, RingEquiv.symm_symm,
-    RingEquiv.coe_mk, Equiv.coe_fn_mk, coe_mk, RingEquiv.coe_trans, Function.comp_apply]
-  rw [← Submodule.map_comp, IsFractionRing.semilinearEquivOfRingEquiv_comp K L f M]
-  rfl
+  simp only [ringEquivOfRingEquiv, RingEquiv.coe_ringHom_trans, Function.comp_apply,
+    semilinearEquivOfRingEquiv_comp K L f M, LinearEquiv.coe_trans,
+    Submodule.map_comp, RingEquiv.coe_mk, Equiv.coe_fn_mk, RingEquiv.coe_trans]
 
 lemma ringEquivOfRingEquiv_trans_apply {T : Type*} [CommRing T] [IsDomain T] (M : Type*)
     [CommRing M] [Algebra T M] [IsFractionRing T M]
@@ -999,40 +994,30 @@ lemma ringEquivOfRingEquiv_trans_apply {T : Type*} [CommRing T] [IsDomain T] (M
       ringEquivOfRingEquiv L M g (ringEquivOfRingEquiv K L f I) := by
   simp [ringEquivOfRingEquiv_trans K L M]
 
-set_option backward.isDefEq.respectTransparency false in
 lemma ringEquivOfRingEquiv_refl :
-    ringEquivOfRingEquiv K K (RingEquiv.refl R) = RingHom.id (FractionalIdeal R⁰ K) := by
-  ext1 I
-  rw [Subtype.ext_iff]
-  simp only [RingHom.coe_coe, ringEquivOfRingEquiv_apply, RingEquiv.coe_ringHom_refl,
-    RingEquiv.symm_refl, val_eq_coe, coe_mk, RingHom.id_apply]
-  convert Submodule.map_id _
-  ext x
-  simp [IsFractionRing.semilinearEquivOfRingEquiv]
+    ringEquivOfRingEquiv K K (RingEquiv.refl R) = RingEquiv.refl (FractionalIdeal R⁰ K) := by
+  ext I x
+  simp only [ringEquivOfRingEquiv_apply, RingEquiv.coe_ringHom_refl, RingEquiv.symm_refl,
+    val_eq_coe, RingEquiv.refl_apply, ← mem_coe]
+  simp [semilinearEquivOfRingEquiv]
 
-set_option backward.isDefEq.respectTransparency false in
 lemma ringEquivOfRingEquiv_spanSingleton (x : K) :
     FractionalIdeal.ringEquivOfRingEquiv K L f (spanSingleton R⁰ x) =
       spanSingleton S⁰ (IsFractionRing.ringEquivOfRingEquiv (L := L) f x) := by
   simp only [ringEquivOfRingEquiv, val_eq_coe, RingEquiv.symm_symm, RingEquiv.coe_mk,
     Equiv.coe_fn_mk, coe_spanSingleton, IsFractionRing.ringEquivOfRingEquiv_apply]
-  rw [Subtype.ext_iff]
-  simp only [val_eq_coe, coe_spanSingleton]
-  ext I
-  simp only [Submodule.mem_map_equiv, Submodule.mem_span_singleton]
-  refine ⟨fun ⟨r, hr⟩ ↦ ?_, fun ⟨s, hs⟩ ↦ ?_⟩
-  · use f r
-    rw [← (IsFractionRing.semilinearEquivOfRingEquiv K L f).injective.eq_iff] at hr
-    simp only [LinearEquiv.apply_symm_apply] at hr
-    simp only [← hr]
-    exact Eq.symm (map_smulₛₗ _ r x)
-  · use f.symm s
-    simp only [Algebra.smul_def, ← hs, IsFractionRing.semilinearEquivOfRingEquiv_symm_apply,
-      map_mul]
-    simp only [IsFractionRing.ringEquivOfRingEquiv_symm, IsFractionRing.ringEquivOfRingEquiv_apply,
-      map_eq, RingHom.coe_coe]
-    rw [← RingHom.comp_apply, IsLocalization.map_comp_map]
-    simp only [RingHomCompTriple.comp_eq, IsLocalization.map_id]
+  rw [SetLike.ext_iff]
+  intro y
+  simp only [← FractionalIdeal.mem_coe, coe_mk, mem_map_equiv, coe_spanSingleton,
+    Submodule.mem_span_singleton, (semilinearEquivOfRingEquiv K L f).eq_symm_apply]
+  constructor
+  · rintro ⟨r, rfl⟩
+    use f r
+    exact .symm (map_smulₛₗ _ r x)
+  · rintro ⟨s, rfl⟩
+    use f.symm s
+    simp only [Algebra.smul_def, semilinearEquivOfRingEquiv_apply, map_mul, map_eq, RingHom.coe_coe,
+      IsFractionRing.ringEquivOfRingEquiv_apply, RingEquiv.apply_symm_apply]
 
 lemma ringEquivOfRingEquiv_symm_eq :
     (FractionalIdeal.ringEquivOfRingEquiv K L f).symm =

From 0854ea2a87aca39c3e2e628c782b74e97b200eab Mon Sep 17 00:00:00 2001
From: mariainesdff <mariaines.dff@gmail.com>
Date: Wed, 29 Apr 2026 15:51:16 +0200
Subject: [PATCH 14/14] suggested change

---
 Mathlib/RingTheory/ClassGroup.lean | 16 ++++++++--------
 1 file changed, 8 insertions(+), 8 deletions(-)

diff --git a/Mathlib/RingTheory/ClassGroup.lean b/Mathlib/RingTheory/ClassGroup.lean
index d1c791f67373e2..6bba7a37bb83da 100644
--- a/Mathlib/RingTheory/ClassGroup.lean
+++ b/Mathlib/RingTheory/ClassGroup.lean
@@ -442,15 +442,15 @@ theorem FractionalIdeal.map_ringEquivOfRingEquiv_toPrincipalIdeal {S L : Type*}
         ← FractionalIdeal.ringEquivOfRingEquiv_symm_eq, hu]
       rfl
 
-/-- A ring isomorphism `P ≃+* P'` induces an isomorphism on their class groups. -/
+/-- A ring isomorphism `R ≃+* R'` induces an isomorphism on their class groups. -/
 @[simps!]
-noncomputable def ClassGroup.mulEquiv {P P' : Type*} [CommRing P] [IsDomain P] [CommRing P']
-    [IsDomain P'] (g : P ≃+* P') : ClassGroup P ≃* ClassGroup P' :=
-  (ClassGroup.equiv (R := P) (FractionRing P)).trans
-    ((QuotientGroup.congr (toPrincipalIdeal P (FractionRing P)).range
-        (toPrincipalIdeal P' (FractionRing P')).range
-        (Units.mapEquiv (FractionalIdeal.ringEquivOfRingEquiv (FractionRing P) (FractionRing P') g))
+noncomputable def ClassGroup.mulEquiv {R' : Type*} [CommRing R'] [IsDomain R'] (g : R ≃+* R') :
+    ClassGroup R ≃* ClassGroup R' :=
+  (ClassGroup.equiv (R := R) (FractionRing R)).trans
+    ((QuotientGroup.congr (toPrincipalIdeal R (FractionRing R)).range
+        (toPrincipalIdeal R' (FractionRing R')).range
+        (Units.mapEquiv (FractionalIdeal.ringEquivOfRingEquiv (FractionRing R) (FractionRing R') g))
         (FractionalIdeal.map_ringEquivOfRingEquiv_toPrincipalIdeal g)).trans
-      (ClassGroup.equiv (FractionRing P')).symm)
+      (ClassGroup.equiv (FractionRing R')).symm)
 
 end MulEquiv