chore: delete 2074 references (#4030)

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⟩⟩

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]

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

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

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

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

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]
 

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 :=

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

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.
 

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.

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]

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 = ⊥) :

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 ι]

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`. -/

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

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
 

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

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 :=

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

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]