chore: use etaExperiment rather than hacking with instances (#3668)

This is to fix timeouts in #3552.

See discussion at https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/!4.233552.20.28LinearAlgebra.2EMatrix.2EToLin.29.



Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

Mathlib/Algebra/Algebra/Subalgebra/Basic.lean

@@ -1455,6 +1455,7 @@ theorem mem_of_finset_sum_eq_one_of_pow_smul_mem {S : Type _} [CommRing S] [Alge
   exact ⟨⟨_, hn i⟩, rfl⟩
 #align subalgebra.mem_of_finset_sum_eq_one_of_pow_smul_mem Subalgebra.mem_of_finset_sum_eq_one_of_pow_smul_mem
 
+set_option synthInstance.etaExperiment true in
 theorem mem_of_span_eq_top_of_smul_pow_mem {S : Type _} [CommRing S] [Algebra R S]
     (S' : Subalgebra R S) (s : Set S) (l : s →₀ S) (hs : Finsupp.total s S S (↑) l = 1)
     (hs' : s ⊆ S') (hl : ∀ i, l i ∈ S') (x : S) (H : ∀ r : s, ∃ n : ℕ, (r : S) ^ n • x ∈ S') :

Mathlib/Algebra/CharP/Two.lean

@@ -63,6 +63,7 @@ section Ring
 
 variable [Ring R] [CharP R 2]
 
+set_option synthInstance.etaExperiment true in
 @[simp]
 theorem neg_eq (x : R) : -x = x := by
   rw [neg_eq_iff_add_eq_zero, ← two_smul R x, two_eq_zero, zero_smul]

Mathlib/Algebra/Module/Projective.lean

@@ -154,6 +154,7 @@ section Ring
 
 variable {R : Type _} [Ring R] {P : Type _} [AddCommGroup P] [Module R P]
 
+set_option synthInstance.etaExperiment true in
 /-- Free modules are projective. -/
 theorem Projective.of_basis {ι : Type _} (b : Basis ι R P) : Projective R P := by
   -- need P →ₗ (P →₀ R) for definition of projective.

Mathlib/Algebra/Order/Algebra.lean

@@ -41,8 +41,7 @@ variable {R A : Type _} {a b : A} {r : R}
 
 variable [OrderedCommRing R] [OrderedRing A] [Algebra R A]
 
--- Porting note: added the following line, fails to be inferred otherwise. Probably lean4#2074
-instance : Module R A := Algebra.toModule
+set_option synthInstance.etaExperiment true
 
 variable [OrderedSMul R A]
 

Mathlib/Analysis/NormedSpace/Basic.lean

@@ -82,10 +82,7 @@ instance (priority := 100) NormedSpace.boundedSMul [NormedSpace α β] : Bounded
   dist_pair_smul' x₁ x₂ y := by simpa [dist_eq_norm, sub_smul] using norm_smul_le (x₁ - x₂) y
 #align normed_space.has_bounded_smul NormedSpace.boundedSMul
 
--- Shortcut instance, as otherwise this will be found by `NormedSpace.toModule` and be
--- noncomputable.
-instance : Module ℝ ℝ := by infer_instance
-
+set_option synthInstance.etaExperiment true in
 instance NormedField.toNormedSpace : NormedSpace α α where norm_smul_le a b := norm_mul_le a b
 #align normed_field.to_normed_space NormedField.toNormedSpace
 

Mathlib/Analysis/Seminorm.lean

@@ -457,7 +457,7 @@ 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 fragement of the type using `eta_experiment%`,
+-- 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,

Mathlib/Data/Polynomial/Module.lean

@@ -120,6 +120,7 @@ instance (M : Type u) [AddCommGroup M] [Module R M] [Module S M] [IsScalarTower
     IsScalarTower S R (PolynomialModule R M) :=
   Finsupp.isScalarTower _ _
 
+set_option synthInstance.etaExperiment true in
 instance isScalarTower' (M : Type u) [AddCommGroup M] [Module R M] [Module S M]
     [IsScalarTower S R M] : IsScalarTower S R[X] (PolynomialModule R M) := by
   haveI : IsScalarTower R R[X] (PolynomialModule R M) := modulePolynomialOfEndo.isScalarTower _
@@ -196,7 +197,11 @@ theorem smul_apply (f : R[X]) (g : PolynomialModule R M) (n : ℕ) :
     exacts [rfl, (zero_smul R _).symm]
 #align polynomial_module.smul_apply PolynomialModule.smul_apply
 
-
+-- Porting note: typeclass inference goes haywire in the next declaration,
+-- possibly due to either lean4#2074 or upstream workarounds for it.
+-- One way to prune the bad branches is:
+attribute [-instance] IsDomain.toCancelCommMonoidWithZero in
+set_option synthInstance.etaExperiment true in
 /-- `PolynomialModule R R` is isomorphic to `R[X]` as an `R[X]` module. -/
 noncomputable def equivPolynomialSelf : PolynomialModule R R ≃ₗ[R[X]] R[X] :=
   { (Polynomial.toFinsuppIso R).symm with

Mathlib/Data/Polynomial/RingDivision.lean

@@ -87,6 +87,7 @@ theorem add_modByMonic (p₁ p₂ : R[X]) : (p₁ + p₂) %ₘ q = p₁ %ₘ q +
   · simp_rw [modByMonic_eq_of_not_monic _ hq]
 #align polynomial.add_mod_by_monic Polynomial.add_modByMonic
 
+set_option synthInstance.etaExperiment true in
 theorem smul_modByMonic (c : R) (p : R[X]) : c • p %ₘ q = c • (p %ₘ q) := by
   by_cases hq : q.Monic
   · cases' subsingleton_or_nontrivial R with hR hR

Mathlib/LinearAlgebra/Basis.lean

@@ -832,6 +832,7 @@ theorem singleton_repr (ι R : Type _) [Unique ι] [Semiring R] (x i) :
     (Basis.singleton ι R).repr x i = x := by simp [Basis.singleton, Unique.eq_default i]
 #align basis.singleton_repr Basis.singleton_repr
 
+set_option synthInstance.etaExperiment true in
 theorem basis_singleton_iff {R M : Type _} [Ring R] [Nontrivial R] [AddCommGroup M] [Module R M]
     [NoZeroSMulDivisors R M] (ι : Type _) [Unique ι] :
     Nonempty (Basis ι R M) ↔ ∃ (x : _)(_ : x ≠ 0), ∀ y : M, ∃ r : R, r • x = y := by
@@ -1116,6 +1117,7 @@ section Mk
 
 variable (hli : LinearIndependent R v) (hsp : ⊤ ≤ span R (range v))
 
+set_option synthInstance.etaExperiment true in
 /-- A linear independent family of vectors spanning the whole module is a basis. -/
 protected noncomputable def mk : Basis ι R M :=
   .ofRepr
@@ -1128,6 +1130,7 @@ protected noncomputable def mk : Basis ι R M :=
       right_inv := fun _ => hli.repr_eq rfl }
 #align basis.mk Basis.mk
 
+set_option synthInstance.etaExperiment true in
 @[simp]
 theorem mk_repr : (Basis.mk hli hsp).repr x = hli.repr ⟨x, hsp Submodule.mem_top⟩ :=
   rfl
@@ -1144,12 +1147,14 @@ theorem coe_mk : ⇑(Basis.mk hli hsp) = v :=
 
 variable {hli hsp}
 
+set_option synthInstance.etaExperiment true in
 /-- Given a basis, the `i`th element of the dual basis evaluates to 1 on the `i`th element of the
 basis. -/
 theorem mk_coord_apply_eq (i : ι) : (Basis.mk hli hsp).coord i (v i) = 1 :=
   show hli.repr ⟨v i, Submodule.subset_span (mem_range_self i)⟩ i = 1 by simp [hli.repr_eq_single i]
 #align basis.mk_coord_apply_eq Basis.mk_coord_apply_eq
 
+set_option synthInstance.etaExperiment true in
 /-- Given a basis, the `i`th element of the dual basis evaluates to 0 on the `j`th element of the
 basis if `j ≠ i`. -/
 theorem mk_coord_apply_ne {i j : ι} (h : j ≠ i) : (Basis.mk hli hsp).coord i (v j) = 0 :=
@@ -1232,6 +1237,7 @@ theorem groupSmul_apply {G : Type _} [Group G] [DistribMulAction G R] [DistribMu
     (groupSmul_span_eq_top v.span_eq).ge i
 #align basis.group_smul_apply Basis.groupSmul_apply
 
+set_option synthInstance.etaExperiment true in
 theorem units_smul_span_eq_top {v : ι → M} (hv : Submodule.span R (Set.range v) = ⊤) {w : ι → Rˣ} :
     Submodule.span R (Set.range (w • v)) = ⊤ :=
   groupSmul_span_eq_top hv
@@ -1249,6 +1255,7 @@ theorem unitsSmul_apply {v : Basis ι R M} {w : ι → Rˣ} (i : ι) : unitsSmul
     (units_smul_span_eq_top v.span_eq).ge i
 #align basis.units_smul_apply Basis.unitsSmul_apply
 
+set_option synthInstance.etaExperiment true in
 @[simp]
 theorem coord_unitsSmul (e : Basis ι R₂ M) (w : ι → R₂ˣ) (i : ι) :
     (unitsSmul e w).coord i = (w i)⁻¹ • e.coord i := by
@@ -1263,8 +1270,7 @@ theorem coord_unitsSmul (e : Basis ι R₂ M) (w : ι → R₂ˣ) (i : ι) :
     split_ifs with h <;> simp [h]
 #align basis.coord_units_smul Basis.coord_unitsSmul
 
--- Porting note: TODO: workaround for lean4#2074
-attribute [-instance] Ring.toNonAssocRing in
+set_option synthInstance.etaExperiment true in
 @[simp]
 theorem repr_unitsSmul (e : Basis ι R₂ M) (w : ι → R₂ˣ) (v : M) (i : ι) :
     (e.unitsSmul w).repr v i = (w i)⁻¹ • e.repr v i :=
@@ -1618,6 +1624,7 @@ theorem LinearMap.exists_extend {p : Submodule K V} (f : p →ₗ[K] V') :
 
 open Submodule LinearMap
 
+set_option synthInstance.etaExperiment true in
 /-- If `p < ⊤` is a subspace of a vector space `V`, then there exists a nonzero linear map
 `f : V →ₗ[K] K` such that `p ≤ ker f`. -/
 theorem Submodule.exists_le_ker_of_lt_top (p : Submodule K V) (hp : p < ⊤) :

Mathlib/LinearAlgebra/Dfinsupp.lean

@@ -542,6 +542,7 @@ theorem independent_iff_dfinsupp_sumAddHom_injective (p : ι → AddSubgroup N)
   ⟨Independent.dfinsupp_sumAddHom_injective, independent_of_dfinsupp_sumAddHom_injective' p⟩
 #align complete_lattice.independent_iff_dfinsupp_sum_add_hom_injective CompleteLattice.independent_iff_dfinsupp_sumAddHom_injective
 
+set_option synthInstance.etaExperiment true in
 /-- If a family of submodules is `Independent`, then a choice of nonzero vector from each submodule
 forms a linearly independent family.
 

Mathlib/LinearAlgebra/Dimension.lean

@@ -328,6 +328,7 @@ theorem LinearIndependent.set_finite_of_isNoetherian [IsNoetherian R M] {s : Set
   @Set.toFinite _ _ hi.finite_of_isNoetherian
 #align linear_independent.set_finite_of_is_noetherian LinearIndependent.set_finite_of_isNoetherian
 
+set_option synthInstance.etaExperiment true in
 -- One might hope that a finite spanning set implies that any linearly independent set is finite.
 -- While this is true over a division ring
 -- (simply because any linearly independent set can be extended to a basis),
@@ -549,6 +550,7 @@ variable {R : Type u} [Ring R] [InvariantBasisNumber R]
 
 variable {M : Type v} [AddCommGroup M] [Module R M]
 
+set_option synthInstance.etaExperiment true in
 /-- The dimension theorem: if `v` and `v'` are two bases, their index types
 have the same cardinalities. -/
 theorem mk_eq_mk_of_basis (v : Basis ι R M) (v' : Basis ι' R M) :
@@ -595,6 +597,7 @@ variable {R : Type u} [Ring R] [RankCondition R]
 
 variable {M : Type v} [AddCommGroup M] [Module R M]
 
+set_option synthInstance.etaExperiment true in
 /-- An auxiliary lemma for `Basis.le_span`.
 
 If `R` satisfies the rank condition,
@@ -627,6 +630,7 @@ theorem basis_le_span' {ι : Type _} (b : Basis ι R M) {w : Set M} [Fintype w]
   exact Basis.le_span'' b s
 #align basis_le_span' basis_le_span'
 
+set_option synthInstance.etaExperiment true in
 -- Note that if `R` satisfies the strong rank condition,
 -- this also follows from `linearIndependent_le_span` below.
 /-- If `R` satisfies the rank condition,
@@ -669,6 +673,7 @@ variable {M : Type v} [AddCommGroup M] [Module R M]
 
 open Submodule
 
+set_option synthInstance.etaExperiment true in
 -- An auxiliary lemma for `linearIndependent_le_span'`,
 -- with the additional assumption that the linearly independent family is finite.
 theorem linearIndependent_le_span_aux' {ι : Type _} [Fintype ι] (v : ι → M)
@@ -769,6 +774,7 @@ theorem linearIndependent_le_basis {ι : Type _} (b : Basis ι R M) {κ : Type _
     exact linearIndependent_le_infinite_basis b v i
 #align linear_independent_le_basis linearIndependent_le_basis
 
+set_option synthInstance.etaExperiment true in
 /-- Let `R` satisfy the strong rank condition. If `m` elements of a free rank `n` `R`-module are
 linearly independent, then `m ≤ n`. -/
 theorem Basis.card_le_card_of_linearIndependent_aux {R : Type _} [Ring R] [StrongRankCondition R]
@@ -918,6 +924,7 @@ theorem Ideal.rank_eq {R S : Type _} [CommRing R] [StrongRankCondition R] [Ring
 
 variable (R)
 
+set_option synthInstance.etaExperiment true in
 @[simp]
 theorem rank_self : Module.rank R R = 1 := by
   rw [← Cardinal.lift_inj, ← (Basis.singleton PUnit R).mk_eq_rank, Cardinal.mk_punit]
@@ -1051,6 +1058,7 @@ theorem rank_fun' : Module.rank K (η → K) = Fintype.card η := by
   rw [rank_fun_eq_lift_mul, rank_self, Cardinal.lift_one, mul_one, Cardinal.natCast_inj]
 #align rank_fun' rank_fun'
 
+set_option synthInstance.etaExperiment true in
 theorem rank_fin_fun (n : ℕ) : Module.rank K (Fin n → K) = n := by simp [rank_fun']
 #align rank_fin_fun rank_fin_fun
 

Mathlib/LinearAlgebra/FiniteDimensional.lean

@@ -597,6 +597,7 @@ end
 
 end
 
+set_option synthInstance.etaExperiment true in
 /-- In a vector space with dimension 1, each set {v} is a basis for `v ≠ 0`. -/
 @[simps repr_apply]
 noncomputable def basisSingleton (ι : Type _) [Unique ι] (h : finrank K V = 1) (v : V)
@@ -622,6 +623,7 @@ noncomputable def basisSingleton (ι : Type _) [Unique ι] (h : finrank K V = 1)
         exact mul_div_cancel _ h }
 #align finite_dimensional.basis_singleton FiniteDimensional.basisSingleton
 
+set_option synthInstance.etaExperiment true in
 @[simp]
 theorem basisSingleton_apply (ι : Type _) [Unique ι] (h : finrank K V = 1) (v : V) (hv : v ≠ 0)
     (i : ι) : basisSingleton ι h v hv i = v := by
@@ -1129,6 +1131,7 @@ noncomputable def divisionRingOfFiniteDimensional (F K : Type _) [Field F] [Ring
     inv_zero := dif_pos rfl }
 #align division_ring_of_finite_dimensional divisionRingOfFiniteDimensional
 
+set_option synthInstance.etaExperiment true in
 /-- An integral domain that is module-finite as an algebra over a field is a field. -/
 noncomputable def fieldOfFiniteDimensional (F K : Type _) [Field F] [CommRing K] [IsDomain K]
     [Algebra F K] [FiniteDimensional F K] : Field K :=
@@ -1586,6 +1589,7 @@ open Module
 
 open Cardinal
 
+set_option synthInstance.etaExperiment true in
 theorem cardinal_mk_eq_cardinal_mk_field_pow_rank (K V : Type u) [DivisionRing K] [AddCommGroup V]
     [Module K V] [FiniteDimensional K V] : (#V) = (#K) ^ Module.rank K V := by
   let s := Basis.ofVectorSpaceIndex K V

Mathlib/LinearAlgebra/Finrank.lean

@@ -137,19 +137,22 @@ theorem finrank_eq_card_finset_basis {ι : Type w} {b : Finset ι} (h : Basis.{w
 
 variable (K)
 
+set_option synthInstance.etaExperiment true in
 /-- A ring satisfying `StrongRankCondition` (such as a `DivisionRing`) is one-dimensional as a
 module over itself. -/
 @[simp]
 theorem finrank_self : finrank K K = 1 :=
   finrank_eq_of_rank_eq (by simp)
 #align finite_dimensional.finrank_self FiniteDimensional.finrank_self
 
+set_option synthInstance.etaExperiment true in
 /-- The vector space of functions on a `Fintype ι` has finrank equal to the cardinality of `ι`. -/
 @[simp]
 theorem finrank_fintype_fun_eq_card {ι : Type v} [Fintype ι] : finrank K (ι → K) = Fintype.card ι :=
   finrank_eq_of_rank_eq rank_fun'
 #align finite_dimensional.finrank_fintype_fun_eq_card FiniteDimensional.finrank_fintype_fun_eq_card
 
+set_option synthInstance.etaExperiment true in
 /-- The vector space of functions on `Fin n` has finrank equal to `n`. -/
 -- @[simp] -- Porting note: simp already proves this
 theorem finrank_fin_fun {n : ℕ} : finrank K (Fin n → K) = n := by simp

Mathlib/LinearAlgebra/FreeAlgebra.lean

@@ -25,6 +25,7 @@ universe u v
 
 namespace FreeAlgebra
 
+set_option synthInstance.etaExperiment true in
 /-- The `FreeMonoid X` basis on the `FreeAlgebra R X`,
 mapping `[x₁, x₂, ..., xₙ]` to the "monomial" `1 • x₁ * x₂ * ⋯ * xₙ` -/
 -- @[simps]

Mathlib/LinearAlgebra/FreeModule/Finite/Basic.lean

@@ -61,6 +61,7 @@ theorem _root_.Module.Finite.of_basis {R M ι : Type _} [CommRing R] [AddCommGro
     simp only [Set.image_univ, Finset.coe_univ, Finset.coe_image, Basis.span_eq]
 #align module.finite.of_basis Module.Finite.of_basis
 
+set_option synthInstance.etaExperiment true in
 instance _root_.Module.Finite.matrix {ι₁ ι₂ : Type _} [_root_.Finite ι₁] [_root_.Finite ι₂] :
     Module.Finite R (Matrix ι₁ ι₂ R) := by
   cases nonempty_fintype ι₁

Mathlib/LinearAlgebra/FreeModule/Finite/Rank.lean

@@ -93,12 +93,14 @@ theorem finrank_eq_card_chooseBasisIndex :
   simp [finrank, rank_eq_card_chooseBasisIndex]
 #align finite_dimensional.finrank_eq_card_choose_basis_index FiniteDimensional.finrank_eq_card_chooseBasisIndex
 
+set_option synthInstance.etaExperiment true in
 /-- The finrank of `(ι →₀ R)` is `Fintype.card ι`. -/
 @[simp]
 theorem finrank_finsupp {ι : Type v} [Fintype ι] : finrank R (ι →₀ R) = card ι := by
   rw [finrank, rank_finsupp_self, ← mk_toNat_eq_card, toNat_lift]
 #align finite_dimensional.finrank_finsupp FiniteDimensional.finrank_finsupp
 
+set_option synthInstance.etaExperiment true in
 /-- The finrank of `(ι → R)` is `Fintype.card ι`. -/
 theorem finrank_pi {ι : Type v} [Fintype ι] : finrank R (ι → R) = card ι := by
   set_option synthInstance.etaExperiment true in -- Porting note: gets around lean4#2074

Mathlib/LinearAlgebra/FreeModule/PID.lean

@@ -78,6 +78,7 @@ theorem eq_bot_of_generator_maximal_map_eq_zero (b : Basis ι R M) {N : Submodul
       ⟨x, hx, rfl⟩
 #align eq_bot_of_generator_maximal_map_eq_zero eq_bot_of_generator_maximal_map_eq_zero
 
+set_option synthInstance.etaExperiment true in
 theorem eq_bot_of_generator_maximal_submoduleImage_eq_zero {N O : Submodule R M} (b : Basis ι R O)
     (hNO : N ≤ O) {ϕ : O →ₗ[R] R} (hϕ : ∀ ψ : O →ₗ[R] R, ¬ϕ.submoduleImage N < ψ.submoduleImage N)
     [(ϕ.submoduleImage N).IsPrincipal] (hgen : generator (ϕ.submoduleImage N) = 0) : N = ⊥ := by
@@ -100,6 +101,7 @@ variable {M : Type _} [AddCommGroup M] [Module R M] {b : ι → M}
 
 open Submodule.IsPrincipal Set Submodule
 
+set_option synthInstance.etaExperiment true in
 theorem dvd_generator_iff {I : Ideal R} [I.IsPrincipal] {x : R} (hx : x ∈ I) :
     x ∣ generator I ↔ I = Ideal.span {x} := by
   conv_rhs => rw [← span_singleton_generator I]
@@ -525,6 +527,7 @@ section Ideal
 
 variable {S : Type _} [CommRing S] [IsDomain S] [Algebra R S]
 
+set_option synthInstance.etaExperiment true in
 /-- If `S` a finite-dimensional ring extension of a PID `R` which is free as an `R`-module,
 then any nonzero `S`-ideal `I` is free as an `R`-submodule of `S`, and we can
 find a basis for `S` and `I` such that the inclusion map is a square diagonal
@@ -547,6 +550,7 @@ noncomputable def Ideal.smithNormalForm [Fintype ι] (b : Basis ι R S) (I : Ide
 
 variable [Finite ι]
 
+set_option synthInstance.etaExperiment true in
 /-- If `S` a finite-dimensional ring extension of a PID `R` which is free as an `R`-module,
 then any nonzero `S`-ideal `I` is free as an `R`-submodule of `S`, and we can
 find a basis for `S` and `I` such that the inclusion map is a square diagonal
@@ -573,6 +577,7 @@ theorem Ideal.exists_smith_normal_form (b : Basis ι R S) (I : Ideal S) (hI : I
             Submodule.restrictScalarsEquiv_apply, Basis.coe_reindex, (·∘·)]⟩
 #align ideal.exists_smith_normal_form Ideal.exists_smith_normal_form
 
+set_option synthInstance.etaExperiment true in
 /-- If `S` a finite-dimensional ring extension of a PID `R` which is free as an `R`-module,
 then any nonzero `S`-ideal `I` is free as an `R`-submodule of `S`, and we can
 find a basis for `S` and `I` such that the inclusion map is a square diagonal
@@ -585,6 +590,7 @@ noncomputable def Ideal.ringBasis (b : Basis ι R S) (I : Ideal S) (hI : I ≠ 
   (Ideal.exists_smith_normal_form b I hI).choose
 #align ideal.ring_basis Ideal.ringBasis
 
+set_option synthInstance.etaExperiment true in
 /-- If `S` a finite-dimensional ring extension of a PID `R` which is free as an `R`-module,
 then any nonzero `S`-ideal `I` is free as an `R`-submodule of `S`, and we can
 find a basis for `S` and `I` such that the inclusion map is a square diagonal
@@ -597,6 +603,7 @@ noncomputable def Ideal.selfBasis (b : Basis ι R S) (I : Ideal S) (hI : I ≠ 
   (Ideal.exists_smith_normal_form b I hI).choose_spec.choose_spec.choose
 #align ideal.self_basis Ideal.selfBasis
 
+set_option synthInstance.etaExperiment true in
 /-- If `S` a finite-dimensional ring extension of a PID `R` which is free as an `R`-module,
 then any nonzero `S`-ideal `I` is free as an `R`-submodule of `S`, and we can
 find a basis for `S` and `I` such that the inclusion map is a square diagonal
@@ -609,6 +616,7 @@ noncomputable def Ideal.smithCoeffs (b : Basis ι R S) (I : Ideal S) (hI : I ≠
   (Ideal.exists_smith_normal_form b I hI).choose_spec.choose
 #align ideal.smith_coeffs Ideal.smithCoeffs
 
+set_option synthInstance.etaExperiment true in
 /-- If `S` a finite-dimensional ring extension of a PID `R` which is free as an `R`-module,
 then any nonzero `S`-ideal `I` is free as an `R`-submodule of `S`, and we can
 find a basis for `S` and `I` such that the inclusion map is a square diagonal
@@ -620,6 +628,7 @@ theorem Ideal.selfBasis_def (b : Basis ι R S) (I : Ideal S) (hI : I ≠ ⊥) :
   (Ideal.exists_smith_normal_form b I hI).choose_spec.choose_spec.choose_spec
 #align ideal.self_basis_def Ideal.selfBasis_def
 
+set_option synthInstance.etaExperiment true in
 @[simp]
 theorem Ideal.smithCoeffs_ne_zero (b : Basis ι R S) (I : Ideal S) (hI : I ≠ ⊥) (i) :
     Ideal.smithCoeffs b I hI i ≠ 0 := by