chore(*): tweak priorities for linear algebra (#3840)

We make sure that the canonical path from `NonAssocSemiring` to `Ring` passes through `Semiring`,
as this is a path which is followed all the time in linear algebra where the defining semilinear map
`σ : R →+* S` depends on the `NonAssocSemiring` structure of `R` and `S` while the module
definition depends on the `Semiring` structure.

Tt is not currently possible to adjust priorities by hand (see lean4#2115). Instead, the last
declared instance is used, so we make sure that `Semiring` is declared after `NonAssocRing`, so
that `Semiring -> NonAssocSemiring` is tried before `NonAssocRing -> NonAssocSemiring`.

Mathlib/Algebra/Algebra/Unitization.lean

@@ -466,7 +466,6 @@ instance nonAssocSemiring [Semiring R] [NonUnitalNonAssocSemiring A] [Module R A
           simp only [add_smul, smul_add, add_mul]
           abel }
 
-set_option synthInstance.etaExperiment true in
 instance monoid [CommMonoid R] [NonUnitalSemiring A] [DistribMulAction R A] [IsScalarTower R A A]
     [SMulCommClass R A A] : Monoid (Unitization R A) :=
   { Unitization.mulOneClass with
@@ -651,8 +650,6 @@ theorem algHom_ext' {φ ψ : Unitization R A →ₐ[R] C}
       φ.toNonUnitalAlgHom.comp (inrNonUnitalAlgHom R A) =
         ψ.toNonUnitalAlgHom.comp (inrNonUnitalAlgHom R A)) :
     φ = ψ :=
-    -- porting note: this is due to lean4#2074 and it succeeds with
-    -- `set_option synthInstance.etaExperiment true`
   algHom_ext (NonUnitalAlgHom.congr_fun h) (by simp [AlgHom.commutes])
 #align unitization.alg_hom_ext' Unitization.algHom_ext'
 

Mathlib/Algebra/Order/Floor.lean

@@ -1533,14 +1533,17 @@ theorem ceil_congr (h : ∀ n : ℤ, a ≤ n ↔ b ≤ n) : ⌈a⌉ = ⌈b⌉ :=
   (ceil_le.2 <| (h _).2 <| le_ceil _).antisymm <| ceil_le.2 <| (h _).1 <| le_ceil _
 #align int.ceil_congr Int.ceil_congr
 
+set_option synthInstance.etaExperiment true in
 theorem map_floor (f : F) (hf : StrictMono f) (a : α) : ⌊f a⌋ = ⌊a⌋ :=
   floor_congr fun n => by rw [← map_intCast f, hf.le_iff_le]
 #align int.map_floor Int.map_floor
 
+set_option synthInstance.etaExperiment true in
 theorem map_ceil (f : F) (hf : StrictMono f) (a : α) : ⌈f a⌉ = ⌈a⌉ :=
   ceil_congr fun n => by rw [← map_intCast f, hf.le_iff_le]
 #align int.map_ceil Int.map_ceil
 
+set_option synthInstance.etaExperiment true in
 theorem map_fract (f : F) (hf : StrictMono f) (a : α) : fract (f a) = f (fract a) := by
   simp_rw [fract, map_sub, map_intCast, map_floor _ hf]
 #align int.map_fract Int.map_fract

Mathlib/Algebra/Ring/Defs.lean

@@ -100,9 +100,18 @@ theorem distrib_three_right [Mul R] [Add R] [RightDistribClass R] (a b c d : R)
 #align distrib_three_right distrib_three_right
 
 /-!
-### Semirings
--/
+### Classes of semirings and rings
+
+We make sure that the canonical path from `NonAssocSemiring` to `Ring` passes through `Semiring`,
+as this is a path which is followed all the time in linear algebra where the defining semilinear map
+`σ : R →+* S` depends on the `NonAssocSemiring` structure of `R` and `S` while the module
+definition depends on the `Semiring` structure.
 
+It is not currently possible to adjust priorities by hand (see lean4#2115). Instead, the last
+declared instance is used, so we make sure that `Semiring` is declared after `NonAssocRing`, so
+that `Semiring -> NonAssocSemiring` is tried before `NonAssocRing -> NonAssocSemiring`.
+TODO: clean this once lean4#2115 is fixed
+-/
 
 /-- A not-necessarily-unital, not-necessarily-associative semiring. -/
 class NonUnitalNonAssocSemiring (α : Type u) extends AddCommMonoid α, Distrib α, MulZeroClass α
@@ -117,9 +126,31 @@ class NonAssocSemiring (α : Type u) extends NonUnitalNonAssocSemiring α, MulZe
     AddCommMonoidWithOne α
 #align non_assoc_semiring NonAssocSemiring
 
+/-- A not-necessarily-unital, not-necessarily-associative ring. -/
+class NonUnitalNonAssocRing (α : Type u) extends AddCommGroup α, NonUnitalNonAssocSemiring α
+#align non_unital_non_assoc_ring NonUnitalNonAssocRing
+
+-- We defer the instance `NonUnitalNonAssocRing.toHasDistribNeg` to `Algebra.Ring.Basic`
+-- as it relies on the lemma `eq_neg_of_add_eq_zero_left`.
+/-- An associative but not-necessarily unital ring. -/
+class NonUnitalRing (α : Type _) extends NonUnitalNonAssocRing α, NonUnitalSemiring α
+#align non_unital_ring NonUnitalRing
+
+/-- A unital but not-necessarily-associative ring. -/
+class NonAssocRing (α : Type _) extends NonUnitalNonAssocRing α, NonAssocSemiring α,
+    AddCommGroupWithOne α
+#align non_assoc_ring NonAssocRing
+
 class Semiring (α : Type u) extends NonUnitalSemiring α, NonAssocSemiring α, MonoidWithZero α
 #align semiring Semiring
 
+class Ring (R : Type u) extends Semiring R, AddCommGroup R, AddGroupWithOne R
+#align ring Ring
+
+/-!
+### Semirings
+-/
+
 section DistribMulOneClass
 
 variable [Add α] [MulOneClass α]
@@ -320,25 +351,6 @@ end HasDistribNeg
 ### Rings
 -/
 
-
-/-- A not-necessarily-unital, not-necessarily-associative ring. -/
-class NonUnitalNonAssocRing (α : Type u) extends AddCommGroup α, NonUnitalNonAssocSemiring α
-#align non_unital_non_assoc_ring NonUnitalNonAssocRing
-
--- We defer the instance `NonUnitalNonAssocRing.toHasDistribNeg` to `Algebra.Ring.Basic`
--- as it relies on the lemma `eq_neg_of_add_eq_zero_left`.
-/-- An associative but not-necessarily unital ring. -/
-class NonUnitalRing (α : Type _) extends NonUnitalNonAssocRing α, NonUnitalSemiring α
-#align non_unital_ring NonUnitalRing
-
-/-- A unital but not-necessarily-associative ring. -/
-class NonAssocRing (α : Type _) extends NonUnitalNonAssocRing α, NonAssocSemiring α,
-    AddCommGroupWithOne α
-#align non_assoc_ring NonAssocRing
-
-class Ring (R : Type u) extends Semiring R, AddCommGroup R, AddGroupWithOne R
-#align ring Ring
-
 section NonUnitalNonAssocRing
 
 variable [NonUnitalNonAssocRing α]

Mathlib/Algebra/Star/Basic.lean

@@ -356,6 +356,7 @@ section
 -- Porting note: This takes too long
 set_option maxHeartbeats 0
 
+set_option synthInstance.etaExperiment true in
 @[simp, norm_cast]
 theorem star_intCast [Ring R] [StarRing R] (z : ℤ) : star (z : R) = z :=
   (congr_arg unop <| map_intCast (starRingEquiv : R ≃+* Rᵐᵒᵖ) z).trans (unop_intCast _)

Mathlib/Algebra/Star/SelfAdjoint.lean

@@ -364,6 +364,7 @@ section CommRing
 
 variable [CommRing R] [StarRing R]
 
+set_option synthInstance.etaExperiment true in
 instance : CommRing (selfAdjoint R) :=
   Function.Injective.commRing _ Subtype.coe_injective (selfAdjoint R).coe_zero val_one
     (selfAdjoint R).coe_add val_mul (selfAdjoint R).coe_neg (selfAdjoint R).coe_sub
@@ -403,6 +404,7 @@ theorem val_zpow (x : selfAdjoint R) (z : ℤ) : ↑(x ^ z) = (x : R) ^ z :=
   rfl
 #align self_adjoint.coe_zpow selfAdjoint.val_zpow
 
+set_option synthInstance.etaExperiment true in
 instance : RatCast (selfAdjoint R) where
   ratCast n := ⟨n, isSelfAdjoint_ratCast n⟩
 
@@ -411,6 +413,7 @@ theorem val_ratCast (x : ℚ) : ↑(x : selfAdjoint R) = (x : R) :=
   rfl
 #align self_adjoint.coe_rat_cast selfAdjoint.val_ratCast
 
+set_option synthInstance.etaExperiment true in
 instance instQSMul : SMul ℚ (selfAdjoint R) where
   smul a x :=
     ⟨a • (x : R), by rw [Rat.smul_def]; exact IsSelfAdjoint.mul (isSelfAdjoint_ratCast a) x.prop⟩
@@ -421,6 +424,7 @@ theorem val_rat_smul (x : selfAdjoint R) (a : ℚ) : ↑(a • x) = a • (x : R
   rfl
 #align self_adjoint.coe_rat_smul selfAdjoint.val_rat_smul
 
+set_option synthInstance.etaExperiment true in
 instance : Field (selfAdjoint R) :=
   Function.Injective.field _ Subtype.coe_injective (selfAdjoint R).coe_zero val_one
     (selfAdjoint R).coe_add val_mul (selfAdjoint R).coe_neg (selfAdjoint R).coe_sub

Mathlib/Analysis/Normed/Field/Basic.lean

@@ -1007,6 +1007,7 @@ def NormedField.induced [Field R] [NormedField S] [NonUnitalRingHomClass F R S]
     mul_comm := mul_comm }
 #align normed_field.induced NormedField.induced
 
+set_option synthInstance.etaExperiment true in
 /-- A ring homomorphism from a `Ring R` to a `SeminormedRing S` which induces the norm structure
 `SeminormedRing.induced` makes `R` satisfy `‖(1 : R)‖ = 1` whenever `‖(1 : S)‖ = 1`. -/
 theorem NormOneClass.induced {F : Type _} (R S : Type _) [Ring R] [SeminormedRing S]
@@ -1023,10 +1024,12 @@ namespace SubringClass
 
 variable {S R : Type _} [SetLike S R]
 
+set_option synthInstance.etaExperiment true in
 instance toSeminormedRing [SeminormedRing R] [SubringClass S R] (s : S) : SeminormedRing s :=
   SeminormedRing.induced s R (SubringClass.subtype s)
 #align subring_class.to_semi_normed_ring SubringClass.toSeminormedRing
 
+set_option synthInstance.etaExperiment true in
 instance toNormedRing [NormedRing R] [SubringClass S R] (s : S) : NormedRing s :=
   NormedRing.induced s R (SubringClass.subtype s) Subtype.val_injective
 #align subring_class.to_normed_ring SubringClass.toNormedRing

Mathlib/Analysis/NormedSpace/Star/Basic.lean

@@ -202,6 +202,8 @@ end ProdPi
 
 section Unital
 
+set_option synthInstance.etaExperiment true
+
 variable [NormedRing E] [StarRing E] [CstarRing E]
 
 @[simp, nolint simpNF] -- Porting note: simp cannot prove this
@@ -265,6 +267,7 @@ end Unital
 
 end CstarRing
 
+set_option synthInstance.etaExperiment true in
 theorem IsSelfAdjoint.nnnorm_pow_two_pow [NormedRing E] [StarRing E] [CstarRing E] {x : E}
     (hx : IsSelfAdjoint x) (n : ℕ) : ‖x ^ 2 ^ n‖₊ = ‖x‖₊ ^ 2 ^ n := by
   induction' n with k hk
@@ -274,6 +277,7 @@ theorem IsSelfAdjoint.nnnorm_pow_two_pow [NormedRing E] [StarRing E] [CstarRing
     rw [← star_pow, CstarRing.nnnorm_star_mul_self, ← sq, hk, pow_mul']
 #align is_self_adjoint.nnnorm_pow_two_pow IsSelfAdjoint.nnnorm_pow_two_pow
 
+set_option synthInstance.etaExperiment true in
 theorem selfAdjoint.nnnorm_pow_two_pow [NormedRing E] [StarRing E] [CstarRing E] (x : selfAdjoint E)
     (n : ℕ) : ‖x ^ 2 ^ n‖₊ = ‖x‖₊ ^ 2 ^ n :=
   x.prop.nnnorm_pow_two_pow _

Mathlib/Analysis/Seminorm.lean

@@ -306,14 +306,6 @@ noncomputable instance smul_nnreal_real : SMul ℝ≥0 ℝ := inferInstance
 
 variable [SMul R ℝ] [SMul R ℝ≥0] [IsScalarTower R ℝ≥0 ℝ]
 
--- Porting note:
--- This is failing, because we are not finding the right instances!
--- example (f : E →ₛₗ[σ₁₂] E₂) : E → E₂ := f
--- However `etaExperiment` saves the day:
--- set_option synthInstance.etaExperiment true in
--- example (f : E →ₛₗ[σ₁₂] E₂) : E → E₂ := f
-
-set_option synthInstance.etaExperiment true in
 /-- Composition of a seminorm with a linear map is a seminorm. -/
 def comp (p : Seminorm 𝕜₂ E₂) (f : E →ₛₗ[σ₁₂] E₂) : Seminorm 𝕜 E :=
   { p.toAddGroupSeminorm.comp f.toAddMonoidHom with
@@ -323,24 +315,20 @@ def comp (p : Seminorm 𝕜₂ E₂) (f : E →ₛₗ[σ₁₂] E₂) : Seminorm
     smul' := fun _ _ => by simp only [map_smulₛₗ]; rw [map_smul_eq_mul, RingHomIsometric.is_iso] }
 #align seminorm.comp Seminorm.comp
 
-set_option synthInstance.etaExperiment true in
 theorem coe_comp (p : Seminorm 𝕜₂ E₂) (f : E →ₛₗ[σ₁₂] E₂) : ⇑(p.comp f) = p ∘ f :=
   rfl
 #align seminorm.coe_comp Seminorm.coe_comp
 
-set_option synthInstance.etaExperiment true in
 @[simp]
 theorem comp_apply (p : Seminorm 𝕜₂ E₂) (f : E →ₛₗ[σ₁₂] E₂) (x : E) : (p.comp f) x = p (f x) :=
   rfl
 #align seminorm.comp_apply Seminorm.comp_apply
 
-set_option synthInstance.etaExperiment true in
 @[simp]
 theorem comp_id (p : Seminorm 𝕜 E) : p.comp LinearMap.id = p :=
   ext fun _ => rfl
 #align seminorm.comp_id Seminorm.comp_id
 
-set_option synthInstance.etaExperiment true in
 @[simp]
 theorem comp_zero (p : Seminorm 𝕜₂ E₂) : p.comp (0 : E →ₛₗ[σ₁₂] E₂) = 0 :=
   ext fun _ => map_zero p
@@ -351,7 +339,6 @@ theorem zero_comp (f : E →ₛₗ[σ₁₂] E₂) : (0 : Seminorm 𝕜₂ E₂)
   ext fun _ => rfl
 #align seminorm.zero_comp Seminorm.zero_comp
 
-set_option synthInstance.etaExperiment true in
 theorem comp_comp [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] (p : Seminorm 𝕜₃ E₃) (g : E₂ →ₛₗ[σ₂₃] E₃)
     (f : E →ₛₗ[σ₁₂] E₂) : p.comp (g.comp f) = (p.comp g).comp f :=
   ext fun _ => rfl
@@ -362,7 +349,6 @@ theorem add_comp (p q : Seminorm 𝕜₂ E₂) (f : E →ₛₗ[σ₁₂] E₂)
   ext fun _ => rfl
 #align seminorm.add_comp Seminorm.add_comp
 
-set_option synthInstance.etaExperiment true in
 theorem comp_add_le (p : Seminorm 𝕜₂ E₂) (f g : E →ₛₗ[σ₁₂] E₂) :
     p.comp (f + g) ≤ p.comp f + p.comp g := fun _ => map_add_le_add p _ _
 #align seminorm.comp_add_le Seminorm.comp_add_le
@@ -456,21 +442,13 @@ variable {σ₁₂ : 𝕜 →+* 𝕜₂} [RingHomIsometric σ₁₂]
 
 variable [AddCommGroup E] [AddCommGroup E₂] [Module 𝕜 E] [Module 𝕜₂ E₂]
 
--- Porting note: unhappily, turning on `synthInstance.etaExperiment` isn't enough here:
--- we need to elaborate a fragment of the type using `eta_experiment%`,
--- but then can't use it for the proof!
--- Porting note:
--- finding the instance `SMul ℝ≥0 (Seminorm 𝕜 E)` is slow,
--- and needs an increase to `synthInstance.maxHeartbeats`.
-set_option synthInstance.maxHeartbeats 30000 in
 theorem comp_smul (p : Seminorm 𝕜₂ E₂) (f : E →ₛₗ[σ₁₂] E₂) (c : 𝕜₂) :
-    p.comp (eta_experiment% c • f) = ‖c‖₊ • p.comp f :=
+    p.comp (c • f) = ‖c‖₊ • p.comp f :=
   ext fun _ => by
     rw [comp_apply, smul_apply, LinearMap.smul_apply, map_smul_eq_mul, NNReal.smul_def, coe_nnnorm,
       smul_eq_mul, comp_apply]
 #align seminorm.comp_smul Seminorm.comp_smul
 
-set_option synthInstance.etaExperiment true in
 theorem comp_smul_apply (p : Seminorm 𝕜₂ E₂) (f : E →ₛₗ[σ₁₂] E₂) (c : 𝕜₂) (x : E) :
     p.comp (c • f) x = ‖c‖ * p (f x) :=
   map_smul_eq_mul p _ _
@@ -817,14 +795,12 @@ variable [SeminormedRing 𝕜₂] [AddCommGroup E₂] [Module 𝕜₂ E₂]
 
 variable {σ₁₂ : 𝕜 →+* 𝕜₂} [RingHomIsometric σ₁₂]
 
-set_option synthInstance.etaExperiment true in
 theorem ball_comp (p : Seminorm 𝕜₂ E₂) (f : E →ₛₗ[σ₁₂] E₂) (x : E) (r : ℝ) :
     (p.comp f).ball x r = f ⁻¹' p.ball (f x) r := by
   ext
   simp_rw [ball, mem_preimage, comp_apply, Set.mem_setOf_eq, map_sub]
 #align seminorm.ball_comp Seminorm.ball_comp
 
-set_option synthInstance.etaExperiment true in
 theorem closedBall_comp (p : Seminorm 𝕜₂ E₂) (f : E →ₛₗ[σ₁₂] E₂) (x : E) (r : ℝ) :
     (p.comp f).closedBall x r = f ⁻¹' p.closedBall (f x) r := by
   ext

Mathlib/Data/MvPolynomial/CommRing.lean

@@ -140,11 +140,13 @@ theorem eval₂_neg : (-p).eval₂ f g = -p.eval₂ f g :=
   (eval₂Hom f g).map_neg _
 #align mv_polynomial.eval₂_neg MvPolynomial.eval₂_neg
 
+set_option synthInstance.etaExperiment true in
 theorem hom_C (f : MvPolynomial σ ℤ →+* S) (n : ℤ) : f (C n) = (n : S) :=
   eq_intCast (f.comp C) n
 set_option linter.uppercaseLean3 false in
 #align mv_polynomial.hom_C MvPolynomial.hom_C
 
+set_option synthInstance.etaExperiment true in
 /-- A ring homomorphism f : Z[X_1, X_2, ...] → R
 is determined by the evaluations f(X_1), f(X_2), ... -/
 @[simp]

Mathlib/Data/Polynomial/Eval.lean

@@ -980,6 +980,7 @@ theorem eval_nat_cast_map (f : R →+* S) (p : R[X]) (n : ℕ) :
     simp only [map_natCast f, eval_monomial, map_monomial, f.map_pow, f.map_mul]
 #align polynomial.eval_nat_cast_map Polynomial.eval_nat_cast_map
 
+set_option synthInstance.etaExperiment true in
 @[simp]
 theorem eval_int_cast_map {R S : Type _} [Ring R] [Ring S] (f : R →+* S) (p : R[X]) (i : ℤ) :
     (p.map f).eval (i : S) = f (p.eval i) := by

Mathlib/Data/Polynomial/Splits.lean

@@ -112,7 +112,9 @@ theorem splits_of_natDegree_eq_one {f : K[X]} (hf : natDegree f = 1) : Splits i
   splits_of_natDegree_le_one i (le_of_eq hf)
 #align polynomial.splits_of_nat_degree_eq_one Polynomial.splits_of_natDegree_eq_one
 
-attribute [-instance] Ring.toNonAssocRing in -- Porting note: gets around lean4#2074
+set_option synthInstance.etaExperiment true in
+set_option synthInstance.maxHeartbeats 100000 in
+set_option maxHeartbeats 300000 in
 theorem splits_mul {f g : K[X]} (hf : Splits i f) (hg : Splits i g) : Splits i (f * g) :=
   if h : (f * g).map i = 0 then Or.inl h
   else

Mathlib/Data/Rat/Cast.lean

@@ -434,6 +434,7 @@ end Rat
 
 open Rat
 
+set_option synthInstance.etaExperiment true in
 @[simp]
 theorem map_ratCast [DivisionRing α] [DivisionRing β] [RingHomClass F α β] (f : F) (q : ℚ) :
     f q = q := by rw [cast_def, map_div₀, map_intCast, map_natCast, cast_def]

Mathlib/Data/ZMod/Algebra.lean

@@ -27,6 +27,7 @@ section
 
 variable {n : ℕ} (m : ℕ) [CharP R m]
 
+set_option synthInstance.etaExperiment true in
 /-- The `ZMod n`-algebra structure on rings whose characteristic `m` divides `n` -/
 def algebra' (h : m ∣ n) : Algebra (ZMod n) R :=
   { ZMod.castHom h R with

Mathlib/Data/ZMod/Basic.lean

@@ -355,6 +355,7 @@ theorem cast_nat_cast (h : m ∣ n) (k : ℕ) : ((k : ZMod n) : R) = k :=
   map_natCast (castHom h R) k
 #align zmod.cast_nat_cast ZMod.cast_nat_cast
 
+set_option synthInstance.etaExperiment true in
 @[simp, norm_cast]
 theorem cast_int_cast (h : m ∣ n) (k : ℤ) : ((k : ZMod n) : R) = k :=
   map_intCast (castHom h R) k
@@ -406,6 +407,7 @@ theorem cast_int_cast' (k : ℤ) : ((k : ZMod n) : R) = k :=
 
 variable (R)
 
+set_option synthInstance.etaExperiment true in
 theorem castHom_injective : Function.Injective (ZMod.castHom (dvd_refl n) R) := by
   rw [injective_iff_map_eq_zero]
   intro x
@@ -425,6 +427,7 @@ theorem castHom_bijective [Fintype R] (h : Fintype.card R = n) :
   apply ZMod.castHom_injective
 #align zmod.cast_hom_bijective ZMod.castHom_bijective
 
+set_option synthInstance.etaExperiment true in
 /-- The unique ring isomorphism between `ZMod n` and a ring `R`
 of characteristic `n` and cardinality `n`. -/
 noncomputable def ringEquiv [Fintype R] (h : Fintype.card R = n) : ZMod n ≃+* R :=
@@ -1159,6 +1162,7 @@ instance subsingleton_ringEquiv [Semiring R] : Subsingleton (ZMod n ≃+* R) :=
     apply RingHom.ext_zmod _ _⟩
 #align zmod.subsingleton_ring_equiv ZMod.subsingleton_ringEquiv
 
+set_option synthInstance.etaExperiment true in
 @[simp]
 theorem ringHom_map_cast [Ring R] (f : R →+* ZMod n) (k : ZMod n) : f k = k := by
   cases n
@@ -1176,7 +1180,6 @@ theorem ringHom_surjective [Ring R] (f : R →+* ZMod n) : Function.Surjective f
   (ringHom_rightInverse f).surjective
 #align zmod.ring_hom_surjective ZMod.ringHom_surjective
 
-set_option synthInstance.etaExperiment true in
 theorem ringHom_eq_of_ker_eq [CommRing R] (f g : R →+* ZMod n)
     (h : RingHom.ker f = RingHom.ker g) : f = g := by
   have := f.liftOfRightInverse_comp _ (ZMod.ringHom_rightInverse f) ⟨g, le_of_eq h⟩