diff --git a/Mathlib/Algebra/Algebra/Bilinear.lean b/Mathlib/Algebra/Algebra/Bilinear.lean
index 4c63b9100f474..2f0197dfe0431 100644
--- a/Mathlib/Algebra/Algebra/Bilinear.lean
+++ b/Mathlib/Algebra/Algebra/Bilinear.lean
@@ -235,12 +235,6 @@ section Ring
 
 variable {R A : Type _} [CommSemiring R] [Ring A] [Algebra R A]
 
-/-- This instance should not be necessary. porting note: drop after lean4#2074 resolved? -/
-local instance : Module R A := Algebra.toModule
-
-/-- This instance should not be necessary. porting note: drop after lean4#2074 resolved? -/
-local instance : Module A A := Semiring.toModule
-
 theorem mulLeft_injective [NoZeroDivisors A] {x : A} (hx : x ≠ 0) :
     Function.Injective (mulLeft R x) := by
   letI : Nontrivial A := ⟨⟨x, 0, hx⟩⟩
diff --git a/Mathlib/Algebra/Algebra/Hom.lean b/Mathlib/Algebra/Algebra/Hom.lean
index a11746553b6fa..97b6419bfddbf 100644
--- a/Mathlib/Algebra/Algebra/Hom.lean
+++ b/Mathlib/Algebra/Algebra/Hom.lean
@@ -495,9 +495,6 @@ end AlgHom
 
 namespace RingHom
 
--- Porting note: TODO Erase this line. Needed because we don't have η for classes. (lean4#2074)
-attribute [-instance] Ring.toNonAssocRing
-
 variable {R S : Type _}
 
 /-- Reinterpret a `RingHom` as an `ℕ`-algebra homomorphism. -/
@@ -509,18 +506,7 @@ def toNatAlgHom [Semiring R] [Semiring S] (f : R →+* S) : R →ₐ[ℕ] S :=
 
 /-- Reinterpret a `RingHom` as a `ℤ`-algebra homomorphism. -/
 def toIntAlgHom [Ring R] [Ring S] [Algebra ℤ R] [Algebra ℤ S] (f : R →+* S) : R →ₐ[ℤ] S :=
-  { f with
-    commutes' := fun n => by
-      -- Porting note: TODO Erase these `have`s.
-      --               Needed because we don't have η for classes. (lean4#2074)
-      have e₁ : algebraMap ℤ R n = n :=
-        @eq_intCast _ R Ring.toNonAssocRing RingHom.instRingHomClassRingHom (algebraMap ℤ R) n
-      have e₂ : algebraMap ℤ S n = n :=
-        @eq_intCast _ S Ring.toNonAssocRing RingHom.instRingHomClassRingHom (algebraMap ℤ S) n
-      have e₃ : f n = n :=
-        @map_intCast _ R S Ring.toNonAssocRing Ring.toNonAssocRing RingHom.instRingHomClassRingHom
-          f n
-      simp [e₁, e₂, e₃] }
+  { f with commutes' := fun n => by simp }
 #align ring_hom.to_int_alg_hom RingHom.toIntAlgHom
 
 /-- Reinterpret a `RingHom` as a `ℚ`-algebra homomorphism. This actually yields an equivalence,
@@ -539,9 +525,6 @@ end RingHom
 
 section
 
--- Porting note: TODO Erase this line. Needed because we don't have η for classes. (lean4#2074)
-attribute [-instance] Ring.toNonAssocRing
-
 variable {R S : Type _}
 
 @[simp]
diff --git a/Mathlib/Algebra/Algebra/Operations.lean b/Mathlib/Algebra/Algebra/Operations.lean
index 0afb757b92124..3ce3ff61caac5 100644
--- a/Mathlib/Algebra/Algebra/Operations.lean
+++ b/Mathlib/Algebra/Algebra/Operations.lean
@@ -322,21 +322,11 @@ section
 
 open Pointwise
 
-/-
-Porting note: the following def ought to be
-```
-protected def hasDistribPointwiseNeg {A} [Ring A] [Algebra R A] : HasDistribNeg (Submodule R A) :=
-  toAddSubmonoid_injective.hasDistribNeg _ neg_toAddSubmonoid mul_toAddSubmonoid
-```
-but this is not possible due to η-for-classes issues. See lean4#2074
--/
 /-- `Submodule.pointwiseNeg` distributes over multiplication.
 
-This is available as an instance in the `pointwise` locale. -/
-protected def hasDistribPointwiseNeg {A} [Ring A] [Algebra R A] :
-    HasDistribNeg (@Submodule R A _ _ Algebra.toModule) :=
-  @Function.Injective.hasDistribNeg _ _ _ _ (id _) _ _ toAddSubmonoid_injective
-    (@neg_toAddSubmonoid R A _ _ Algebra.toModule) mul_toAddSubmonoid
+This is available as an instance in the `Pointwise` locale. -/
+protected def hasDistribPointwiseNeg {A} [Ring A] [Algebra R A] : HasDistribNeg (Submodule R A) :=
+  toAddSubmonoid_injective.hasDistribNeg _ neg_toAddSubmonoid mul_toAddSubmonoid
 #align submodule.has_distrib_pointwise_neg Submodule.hasDistribPointwiseNeg
 
 scoped[Pointwise] attribute [instance] Submodule.hasDistribPointwiseNeg
diff --git a/Mathlib/Algebra/Algebra/Subalgebra/Basic.lean b/Mathlib/Algebra/Algebra/Subalgebra/Basic.lean
index fe85ff1e484f7..0a987e39998aa 100644
--- a/Mathlib/Algebra/Algebra/Subalgebra/Basic.lean
+++ b/Mathlib/Algebra/Algebra/Subalgebra/Basic.lean
@@ -449,8 +449,6 @@ theorem val_apply (x : S) : S.val x = (x : A) := rfl
 theorem toSubsemiring_subtype : S.toSubsemiring.subtype = (S.val : S →+* A) := rfl
 #align subalgebra.to_subsemiring_subtype Subalgebra.toSubsemiring_subtype
 
--- Porting note: workaround for lean#2074
-attribute [-instance] Ring.toNonAssocRing
 @[simp]
 theorem toSubring_subtype {R A : Type _} [CommRing R] [Ring A] [Algebra R A] (S : Subalgebra R A) :
     S.toSubring.subtype = (S.val : S →+* A) := rfl
diff --git a/Mathlib/Algebra/Lie/Basic.lean b/Mathlib/Algebra/Lie/Basic.lean
index e95257b3e69f9..efd717a480c53 100644
--- a/Mathlib/Algebra/Lie/Basic.lean
+++ b/Mathlib/Algebra/Lie/Basic.lean
@@ -224,9 +224,6 @@ theorem lie_jacobi : ⁅x, ⁅y, z⁆⁆ + ⁅y, ⁅z, x⁆⁆ + ⁅z, ⁅x, y
 instance LieRing.intLieAlgebra : LieAlgebra ℤ L where lie_smul n x y := lie_zsmul x y n
 #align lie_ring.int_lie_algebra LieRing.intLieAlgebra
 
--- Porting note: TODO Erase this line. Needed because we don't have η for classes. (lean4#2074)
-attribute [-instance] Ring.toNonAssocRing
-
 instance : LieRingModule L (M →ₗ[R] N) where
   bracket x f :=
     { toFun := fun m => ⁅x, f m⁆ - f ⁅x, m⁆
@@ -265,9 +262,6 @@ instance : LieModule R L (M →ₗ[R] N)
 
 end BasicProperties
 
--- Porting note: TODO Erase this line. Needed because we don't have η for classes. (lean4#2074)
-attribute [-instance] Ring.toNonAssocRing
-
 /-- A morphism of Lie algebras is a linear map respecting the bracket operations. -/
 structure LieHom (R L L': Type _) [CommRing R] [LieRing L] [LieAlgebra R L]
   [LieRing L'] [LieAlgebra R L'] extends L →ₗ[R] L' where
diff --git a/Mathlib/Algebra/Lie/Subalgebra.lean b/Mathlib/Algebra/Lie/Subalgebra.lean
index 43a4fcba413bc..62f1917b3fa00 100644
--- a/Mathlib/Algebra/Lie/Subalgebra.lean
+++ b/Mathlib/Algebra/Lie/Subalgebra.lean
@@ -257,9 +257,6 @@ instance : LieModule R L' M
   smul_lie t x m := by simp only [coe_bracket_of_module, smul_lie, Submodule.coe_smul_of_tower]
   lie_smul t x m := by simp only [coe_bracket_of_module, lie_smul]
 
--- Porting note: Needed because we don't have η for classes. (lean4#2074)
-attribute [-instance] Ring.toNonAssocRing
-
 /-- An `L`-equivariant map of Lie modules `M → N` is `L'`-equivariant for any Lie subalgebra
 `L' ⊆ L`. -/
 def _root_.LieModuleHom.restrictLie (f : M →ₗ⁅R,L⁆ N) (L' : LieSubalgebra R L) : M →ₗ⁅R,L'⁆ N :=
@@ -303,9 +300,6 @@ variable (f : L →ₗ⁅R⁆ L₂)
 
 namespace LieHom
 
--- Porting note: Needed because we don't have η for classes. (lean4#2074)
-attribute [-instance] Ring.toNonAssocRing
-
 /-- The range of a morphism of Lie algebras is a Lie subalgebra. -/
 def range : LieSubalgebra R L₂ :=
   { LinearMap.range (f : L →ₗ[R] L₂) with
@@ -383,9 +377,6 @@ theorem incl_range : K.incl.range = K := by
   exact (K : Submodule R L).range_subtype
 #align lie_subalgebra.incl_range LieSubalgebra.incl_range
 
--- Porting note: Needed because we don't have η for classes. (lean4#2074)
-attribute [-instance] Ring.toNonAssocRing
-
 /-- The image of a Lie subalgebra under a Lie algebra morphism is a Lie subalgebra of the
 codomain. -/
 def map : LieSubalgebra R L₂ :=
@@ -771,9 +762,6 @@ variable {R : Type u} {L₁ : Type v} {L₂ : Type w}
 
 variable [CommRing R] [LieRing L₁] [LieRing L₂] [LieAlgebra R L₁] [LieAlgebra R L₂]
 
--- Porting note: Needed because we don't have η for classes. (lean4#2074)
-attribute [-instance] Ring.toNonAssocRing
-
 /-- An injective Lie algebra morphism is an equivalence onto its range. -/
 noncomputable def ofInjective (f : L₁ →ₗ⁅R⁆ L₂) (h : Function.Injective f) : L₁ ≃ₗ⁅R⁆ f.range :=
   { LinearEquiv.ofInjective (f : L₁ →ₗ[R] L₂) <| by rwa [LieHom.coe_toLinearMap] with
diff --git a/Mathlib/Algebra/Star/Module.lean b/Mathlib/Algebra/Star/Module.lean
index 79e73c8db723f..b2c5233c6787d 100644
--- a/Mathlib/Algebra/Star/Module.lean
+++ b/Mathlib/Algebra/Star/Module.lean
@@ -75,11 +75,6 @@ theorem star_rat_smul {R : Type _} [AddCommGroup R] [StarAddMonoid R] [Module 
 
 end SmulLemmas
 
-section deinstance
--- porting note: this is lean#2074 at play
-attribute [-instance] Ring.toNonUnitalRing
-attribute [-instance] CommRing.toNonUnitalCommRing
-
 /-- If `A` is a module over a commutative `R` with compatible actions,
 then `star` is a semilinear equivalence. -/
 @[simps]
@@ -90,8 +85,6 @@ def starLinearEquiv (R : Type _) {A : Type _} [CommRing R] [StarRing R] [Semirin
     map_smul' := star_smul }
 #align star_linear_equiv starLinearEquiv
 
-end deinstance
-
 variable (R : Type _) (A : Type _) [Semiring R] [StarSemigroup R] [TrivialStar R] [AddCommGroup A]
   [Module R A] [StarAddMonoid A] [StarModule R A]
 
diff --git a/Mathlib/Algebra/Star/SelfAdjoint.lean b/Mathlib/Algebra/Star/SelfAdjoint.lean
index 3eeb9029a6130..4b33b588af913 100644
--- a/Mathlib/Algebra/Star/SelfAdjoint.lean
+++ b/Mathlib/Algebra/Star/SelfAdjoint.lean
@@ -329,9 +329,8 @@ theorem val_one : ↑(1 : selfAdjoint R) = (1 : R) :=
 instance [Nontrivial R] : Nontrivial (selfAdjoint R) :=
   ⟨⟨0, 1, Subtype.ne_of_val_ne zero_ne_one⟩⟩
 
-instance : NatCast (selfAdjoint R) where
-  -- porting note: `(_)` works around lean4#2074
-  natCast n := ⟨n, @isSelfAdjoint_natCast _ _ (_) n⟩
+instance : NatCast (selfAdjoint R) :=
+  ⟨fun n => ⟨n, isSelfAdjoint_natCast _⟩⟩
 
 instance : IntCast (selfAdjoint R) where
   intCast n := ⟨n, isSelfAdjoint_intCast _⟩
@@ -376,27 +375,21 @@ section Field
 
 variable [Field R] [StarRing R]
 
-instance : Inv (selfAdjoint R) where
-  -- porting note: `(_)` works around lean4#2074
-  inv x := ⟨x.val⁻¹, @IsSelfAdjoint.inv _ _ (_) _ x.prop⟩
+instance : Inv (selfAdjoint R) where inv x := ⟨x.val⁻¹, x.prop.inv⟩
 
 @[simp, norm_cast]
 theorem val_inv (x : selfAdjoint R) : ↑x⁻¹ = (x : R)⁻¹ :=
   rfl
 #align self_adjoint.coe_inv selfAdjoint.val_inv
 
-instance : Div (selfAdjoint R) where
-  -- porting note: `(_)` works around lean4#2074
-  div x y := ⟨x / y, @IsSelfAdjoint.div _ _ (_) _ _ x.prop y.prop⟩
+instance : Div (selfAdjoint R) where div x y := ⟨x / y, x.prop.div y.prop⟩
 
 @[simp, norm_cast]
 theorem val_div (x y : selfAdjoint R) : ↑(x / y) = (x / y : R) :=
   rfl
 #align self_adjoint.coe_div selfAdjoint.val_div
 
-instance : Pow (selfAdjoint R) ℤ where
-  -- porting note: `(_)` works around lean4#2074
-  pow x z := ⟨(x : R) ^ z, @IsSelfAdjoint.zpow _ _ (_) _ x.prop z⟩
+instance : Pow (selfAdjoint R) ℤ where pow x z := ⟨(x : R) ^ z, x.prop.zpow z⟩
 
 @[simp, norm_cast]
 theorem val_zpow (x : selfAdjoint R) (z : ℤ) : ↑(x ^ z) = (x : R) ^ z :=
diff --git a/Mathlib/Data/Polynomial/Splits.lean b/Mathlib/Data/Polynomial/Splits.lean
index 6f38e19ce0449..ec759be6a4ae3 100644
--- a/Mathlib/Data/Polynomial/Splits.lean
+++ b/Mathlib/Data/Polynomial/Splits.lean
@@ -91,7 +91,6 @@ theorem splits_of_map_degree_eq_one {f : K[X]} (hf : degree (f.map i) = 1) : Spl
     tauto
 #align polynomial.splits_of_map_degree_eq_one Polynomial.splits_of_map_degree_eq_one
 
-attribute [-instance] Ring.toNonAssocRing in -- Porting note: gets around lean4#2074
 theorem splits_of_degree_le_one {f : K[X]} (hf : degree f ≤ 1) : Splits i f :=
   if hif : degree (f.map i) ≤ 0 then splits_of_map_eq_C i (degree_le_zero_iff.mp hif)
   else by
diff --git a/Mathlib/LinearAlgebra/AffineSpace/AffineEquiv.lean b/Mathlib/LinearAlgebra/AffineSpace/AffineEquiv.lean
index fcdbe8a72fc50..c0c3051b09265 100644
--- a/Mathlib/LinearAlgebra/AffineSpace/AffineEquiv.lean
+++ b/Mathlib/LinearAlgebra/AffineSpace/AffineEquiv.lean
@@ -41,9 +41,6 @@ open Function Set
 
 open Affine
 
--- Porting note: this is needed because of lean4#2074
-attribute [-instance] Ring.toNonAssocRing
-
 /-- An affine equivalence is an equivalence between affine spaces such that both forward
 and inverse maps are affine.
 
diff --git a/Mathlib/LinearAlgebra/AffineSpace/AffineMap.lean b/Mathlib/LinearAlgebra/AffineSpace/AffineMap.lean
index 7786ace4a516d..0ef57066f5460 100644
--- a/Mathlib/LinearAlgebra/AffineSpace/AffineMap.lean
+++ b/Mathlib/LinearAlgebra/AffineSpace/AffineMap.lean
@@ -46,8 +46,6 @@ topology are defined elsewhere; see `Analysis.NormedSpace.AddTorsor` and
 * https://en.wikipedia.org/wiki/Principal_homogeneous_space
 -/
 
--- Porting note: Workaround for lean4#2074
-attribute [-instance] Ring.toNonAssocRing
 
 open Affine
 
@@ -247,10 +245,6 @@ theorem smul_linear (t : R) (f : P1 →ᵃ[k] V2) : (t • f).linear = t • f.l
   rfl
 #align affine_map.smul_linear AffineMap.smul_linear
 
--- Porting note: Workaround for lean4#2074
-instance [DistribMulAction Rᵐᵒᵖ V2] [IsCentralScalar R V2] : SMulCommClass k Rᵐᵒᵖ V2 :=
-SMulCommClass.op_right
-
 instance isCentralScalar [DistribMulAction Rᵐᵒᵖ V2] [IsCentralScalar R V2] :
   IsCentralScalar R (P1 →ᵃ[k] V2) where
     op_smul_eq_smul _r _x := ext fun _ => op_smul_eq_smul _ _
@@ -512,8 +506,6 @@ theorem image_vsub_image {s t : Set P1} (f : P1 →ᵃ[k] P2) :
 
 /-! ### Definition of `AffineMap.lineMap` and lemmas about it -/
 
--- Porting note: Workaround for lean4#2074
-instance : Module k k := Semiring.toModule
 
 /-- The affine map from `k` to `P1` sending `0` to `p₀` and `1` to `p₁`. -/
 def lineMap (p₀ p₁ : P1) : k →ᵃ[k] P1 :=
@@ -703,9 +695,6 @@ section
 variable {ι : Type _} {V : ∀ _ : ι, Type _} {P : ∀ _ : ι, Type _} [∀ i, AddCommGroup (V i)]
   [∀ i, Module k (V i)] [∀ i, AddTorsor (V i) (P i)]
 
--- Workaround for lean4#2074
-instance : AffineSpace (∀ i : ι, (V i)) (∀ i : ι, P i) := Pi.instAddTorsorForAllForAllAddGroup
-
 /-- Evaluation at a point as an affine map. -/
 def proj (i : ι) : (∀ i : ι, P i) →ᵃ[k] P i where
   toFun f := f i
@@ -766,12 +755,6 @@ instance : Module R (P1 →ᵃ[k] V2) :=
 
 variable (R)
 
--- Porting note: Workarounds for lean4#2074
-instance : AddCommMonoid (V1 →ₗ[k] V2) := LinearMap.addCommMonoid
-instance : AddCommMonoid (V2 × (V1 →ₗ[k] V2)) := Prod.instAddCommMonoidSum
-instance : Module R (V1 →ₗ[k] V2) := LinearMap.instModuleLinearMapAddCommMonoid
-instance : Module R (V2 × (V1 →ₗ[k] V2)) := Prod.module
-
 /-- The space of affine maps between two modules is linearly equivalent to the product of the
 domain with the space of linear maps, by taking the value of the affine map at `(0 : V1)` and the
 linear part.
diff --git a/Mathlib/LinearAlgebra/AffineSpace/Slope.lean b/Mathlib/LinearAlgebra/AffineSpace/Slope.lean
index 9cf4ac1549d59..2c8dbd21185ed 100644
--- a/Mathlib/LinearAlgebra/AffineSpace/Slope.lean
+++ b/Mathlib/LinearAlgebra/AffineSpace/Slope.lean
@@ -24,9 +24,6 @@ interval is convex on this interval.
 affine space, slope
 -/
 
--- Porting note: Workaround for lean4#2074
-attribute [-instance] Ring.toNonAssocRing
-
 open AffineMap
 
 variable {k E PE : Type _} [Field k] [AddCommGroup E] [Module k E] [AddTorsor E PE]
diff --git a/Mathlib/LinearAlgebra/Basis.lean b/Mathlib/LinearAlgebra/Basis.lean
index 4f1a6d775d872..cfc0653832c13 100644
--- a/Mathlib/LinearAlgebra/Basis.lean
+++ b/Mathlib/LinearAlgebra/Basis.lean
@@ -74,9 +74,6 @@ open Function Set Submodule
 
 open BigOperators
 
--- Porting note: TODO: workaround for lean4#2074
--- attribute [-instance] Ring.toNonAssocRing
-
 variable {ι : Type _} {ι' : Type _} {R : Type _} {R₂ : Type _} {K : Type _}
 variable {M : Type _} {M' M'' : Type _} {V : Type u} {V' : Type _}
 
@@ -1556,9 +1553,6 @@ instance : IsAtomistic (Submodule K V) where
 
 end AtomsOfSubmoduleLattice
 
--- Porting note: TODO: workaround for lean4#2074
-attribute [-instance] Ring.toNonAssocRing
-
 variable {K V}
 
 theorem LinearMap.exists_leftInverse_of_injective (f : V →ₗ[K] V') (hf_inj : LinearMap.ker f = ⊥) :
diff --git a/Mathlib/LinearAlgebra/Dfinsupp.lean b/Mathlib/LinearAlgebra/Dfinsupp.lean
index ff100bb04cd3b..189f37eac73c4 100644
--- a/Mathlib/LinearAlgebra/Dfinsupp.lean
+++ b/Mathlib/LinearAlgebra/Dfinsupp.lean
@@ -37,9 +37,6 @@ much more developed, but many lemmas in that file should be eligible to copy ove
 function with finite support, module, linear algebra
 -/
 
--- Porting note: TODO Erase this line. Workaround for lean4#2074.
-attribute [-instance] Ring.toNonAssocRing
-
 variable {ι : Type _} {R : Type _} {S : Type _} {M : ι → Type _} {N : Type _}
 
 variable [dec_ι : DecidableEq ι]
diff --git a/Mathlib/LinearAlgebra/LinearPMap.lean b/Mathlib/LinearAlgebra/LinearPMap.lean
index 205bffee310f5..23cca5126efdc 100644
--- a/Mathlib/LinearAlgebra/LinearPMap.lean
+++ b/Mathlib/LinearAlgebra/LinearPMap.lean
@@ -36,9 +36,6 @@ They are also the basis for the theory of unbounded operators.
 
 open Set
 
--- Porting note: TODO Erase this line. Needed because we don't have η for classes. (lean4#2074)
-attribute [-instance] Ring.toNonAssocRing
-
 universe u v w
 
 /-- A `LinearPMap R E F` or `E →ₗ.[R] F` is a linear map from a submodule of `E` to `F`. -/
diff --git a/Mathlib/LinearAlgebra/Prod.lean b/Mathlib/LinearAlgebra/Prod.lean
index 2df60994271f9..28fe46ad96a3e 100644
--- a/Mathlib/LinearAlgebra/Prod.lean
+++ b/Mathlib/LinearAlgebra/Prod.lean
@@ -829,9 +829,6 @@ end
 
 end LinearEquiv
 
--- Porting note: TODO Erase this line. Needed because we don't have η for classes. (lean4#2074)
-attribute [-instance] Ring.toNonAssocRing
-
 namespace LinearMap
 
 open Submodule
diff --git a/Mathlib/LinearAlgebra/Projection.lean b/Mathlib/LinearAlgebra/Projection.lean
index bc3be79a20e93..42a1299c82404 100644
--- a/Mathlib/LinearAlgebra/Projection.lean
+++ b/Mathlib/LinearAlgebra/Projection.lean
@@ -28,8 +28,6 @@ We also provide some lemmas justifying correctness of our definitions.
 projection, complement subspace
 -/
 
--- Porting note: TODO Erase this line. Needed because we don't have η for classes. (lean4#2074)
-attribute [-instance] Ring.toNonAssocRing
 
 noncomputable section Ring
 
diff --git a/Mathlib/LinearAlgebra/Quotient.lean b/Mathlib/LinearAlgebra/Quotient.lean
index 1d582b5658148..d7b9b9add14e6 100644
--- a/Mathlib/LinearAlgebra/Quotient.lean
+++ b/Mathlib/LinearAlgebra/Quotient.lean
@@ -19,10 +19,6 @@ import Mathlib.LinearAlgebra.Span
 
 -/
 
-section deinstance_nonassocring
--- porting note: because we're missing lean4#2074 we need this, see:
--- https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/LinearAlgebra.2ESpan.20!4.232248
-attribute [-instance] Ring.toNonAssocRing
 
 -- For most of this file we work over a noncommutative ring
 section Ring
@@ -695,5 +691,3 @@ def mapQLinear : compatibleMaps p q →ₗ[R] M ⧸ p →ₗ[R] M₂ ⧸ q
 end Submodule
 
 end CommRing
-
-end deinstance_nonassocring
diff --git a/Mathlib/LinearAlgebra/QuotientPi.lean b/Mathlib/LinearAlgebra/QuotientPi.lean
index b688eb5cd5bef..b35b0019db796 100644
--- a/Mathlib/LinearAlgebra/QuotientPi.lean
+++ b/Mathlib/LinearAlgebra/QuotientPi.lean
@@ -38,9 +38,6 @@ variable {N : Type _} [AddCommGroup N] [Module R N]
 
 variable {Ns : ι → Type _} [∀ i, AddCommGroup (Ns i)] [∀ i, Module R (Ns i)]
 
--- Porting note: TODO remove after https://github.com/leanprover/lean4/issues/2074 fixed
-attribute [-instance] Ring.toNonAssocRing
-
 /-- Lift a family of maps to the direct sum of quotients. -/
 def piQuotientLift [Fintype ι] [DecidableEq ι] (p : ∀ i, Submodule R (Ms i)) (q : Submodule R N)
     (f : ∀ i, Ms i →ₗ[R] N) (hf : ∀ i, p i ≤ q.comap (f i)) : (∀ i, Ms i ⧸ p i) →ₗ[R] N ⧸ q :=
diff --git a/Mathlib/LinearAlgebra/Ray.lean b/Mathlib/LinearAlgebra/Ray.lean
index 890911f9628f1..71509153aead3 100644
--- a/Mathlib/LinearAlgebra/Ray.lean
+++ b/Mathlib/LinearAlgebra/Ray.lean
@@ -492,9 +492,6 @@ theorem units_smul_of_neg (u : Rˣ) (hu : u.1 < 0) (v : Module.Ray R M) : u •
   rwa [Units.val_neg, Right.neg_pos_iff]
 #align module.ray.units_smul_of_neg Module.Ray.units_smul_of_neg
 
--- Porting note: TODO Erase this line. Needed because we don't have η for classes. (lean4#2074)
-attribute [-instance] Ring.toNonAssocRing
-
 @[simp]
 protected theorem map_neg (f : M ≃ₗ[R] N) (v : Module.Ray R M) : map f (-v) = -map f v := by
   induction' v using Module.Ray.ind with g hg
diff --git a/Mathlib/RingTheory/Ideal/Basic.lean b/Mathlib/RingTheory/Ideal/Basic.lean
index c6d04aedb52cf..acc13ba1c8db9 100644
--- a/Mathlib/RingTheory/Ideal/Basic.lean
+++ b/Mathlib/RingTheory/Ideal/Basic.lean
@@ -668,11 +668,8 @@ protected theorem sub_mem : a ∈ I → b ∈ I → a - b ∈ I :=
   Submodule.sub_mem I
 #align ideal.sub_mem Ideal.sub_mem
 
-example : Module α α := Semiring.toModule
-
 theorem mem_span_insert' {s : Set α} {x y} : x ∈ span (insert y s) ↔ ∃ a, x + a * y ∈ span s :=
-  @Submodule.mem_span_insert' α α _ _ Semiring.toModule _ _ _
--- porting note: Lean 4 issue #2074: Lean can't infer `Module R R` from `Ring R` on its own.
+  Submodule.mem_span_insert'
 #align ideal.mem_span_insert' Ideal.mem_span_insert'
 
 @[simp]
diff --git a/Mathlib/RingTheory/Ideal/Operations.lean b/Mathlib/RingTheory/Ideal/Operations.lean
index d6e1e5fab0fff..f298eecd146ad 100644
--- a/Mathlib/RingTheory/Ideal/Operations.lean
+++ b/Mathlib/RingTheory/Ideal/Operations.lean
@@ -21,9 +21,6 @@ import Mathlib.RingTheory.NonZeroDivisors
 -/
 
 
--- Porting note: TODO Erase this line, lean#2074
-attribute [-instance] Ring.toNonAssocRing
-
 universe u v w x
 
 open BigOperators Pointwise
diff --git a/Mathlib/RingTheory/Ideal/QuotientOperations.lean b/Mathlib/RingTheory/Ideal/QuotientOperations.lean
index 37a846fccbbe6..2e3ad18b668e8 100644
--- a/Mathlib/RingTheory/Ideal/QuotientOperations.lean
+++ b/Mathlib/RingTheory/Ideal/QuotientOperations.lean
@@ -16,9 +16,6 @@ import Mathlib.RingTheory.Ideal.Quotient
 -/
 
 
--- Porting note: Without this line, timeouts occur (lean4#2074)
-attribute [-instance] Ring.toNonAssocRing
-
 universe u v w
 
 namespace RingHom
diff --git a/Mathlib/RingTheory/Noetherian.lean b/Mathlib/RingTheory/Noetherian.lean
index d2c6d32be1cb1..dd76b379b9cf0 100644
--- a/Mathlib/RingTheory/Noetherian.lean
+++ b/Mathlib/RingTheory/Noetherian.lean
@@ -406,10 +406,6 @@ theorem isNoetherian_of_range_eq_ker [IsNoetherian R M] [IsNoetherian R P] (f :
       (by simp [Submodule.map_comap_eq, inf_comm]) (by simp [Submodule.comap_map_eq, h])
 #align is_noetherian_of_range_eq_ker isNoetherian_of_range_eq_ker
 
-/- Porting note (lean4#2074): this seems to cause a diamond with Ring.toSemiring when going to
-NonAssocSemiring -/
-attribute [-instance] Ring.toNonAssocRing
-
 /-- For any endomorphism of a Noetherian module, there is some nontrivial iterate
 with disjoint kernel and range.
 -/
diff --git a/Mathlib/RingTheory/QuotientNoetherian.lean b/Mathlib/RingTheory/QuotientNoetherian.lean
index 28e77bfe0a03a..264d6c8a2841a 100644
--- a/Mathlib/RingTheory/QuotientNoetherian.lean
+++ b/Mathlib/RingTheory/QuotientNoetherian.lean
@@ -15,13 +15,8 @@ import Mathlib.RingTheory.QuotientNilpotent
 # Noetherian quotient rings and quotient modules
 -/
 
--- Porting note: we keep this instance local to avoid downstream effects.
--- I haven't been able to work out how to omit it or inline it into the the construction below.
--- The fact we need this issue is surely related to lean4#2074.
-local instance {R : Type _} [CommRing R] : Module R R := inferInstance
 
-instance Ideal.Quotient.isNoetherianRing {R : Type _} [CommRing R] [h : IsNoetherianRing R]
+instance Ideal.Quotient.isNoetherianRing {R : Type _} [CommRing R] [IsNoetherianRing R]
     (I : Ideal R) : IsNoetherianRing (R ⧸ I) :=
-  have : IsNoetherian R R := by simp_all only -- Porting note: this instance is needed
   isNoetherianRing_iff.mpr <| isNoetherian_of_tower R <| Submodule.Quotient.isNoetherian _
 #align ideal.quotient.is_noetherian_ring Ideal.Quotient.isNoetherianRing
diff --git a/Mathlib/Topology/Algebra/UniformMulAction.lean b/Mathlib/Topology/Algebra/UniformMulAction.lean
index 3fda2627aa75d..fb1a997c6d709 100644
--- a/Mathlib/Topology/Algebra/UniformMulAction.lean
+++ b/Mathlib/Topology/Algebra/UniformMulAction.lean
@@ -70,28 +70,18 @@ theorem uniformContinuousConstSMul_of_continuousConstSMul [Monoid R] [AddCommGro
       (Continuous.continuousAt (continuous_const_smul r))⟩
 #align has_uniform_continuous_const_smul_of_continuous_const_smul uniformContinuousConstSMul_of_continuousConstSMul
 
-section instances
-
-variable [Ring R]
-
--- Porting note: needs Lean4#2074
-local instance : Module R R := Semiring.toModule
 /-- The action of `Semiring.toModule` is uniformly continuous. -/
 instance Ring.uniformContinuousConstSMul [Ring R] [UniformSpace R] [UniformAddGroup R]
     [ContinuousMul R] : UniformContinuousConstSMul R R :=
   uniformContinuousConstSMul_of_continuousConstSMul _ _
 #align ring.has_uniform_continuous_const_smul Ring.uniformContinuousConstSMul
 
--- Porting note: needs Lean4#2074
-local instance : Module Rᵐᵒᵖ R := Semiring.toOppositeModule
 /-- The action of `Semiring.toOppositeModule` is uniformly continuous. -/
 instance Ring.uniformContinuousConstSMul_op [Ring R] [UniformSpace R] [UniformAddGroup R]
     [ContinuousMul R] : UniformContinuousConstSMul Rᵐᵒᵖ R :=
   uniformContinuousConstSMul_of_continuousConstSMul _ _
 #align ring.has_uniform_continuous_const_op_smul Ring.uniformContinuousConstSMul_op
 
-end instances
-
 section SMul
 
 variable [SMul M X]