chore: reenable eta, bump to nightly 2023-05-16 (#3414)

Now that leanprover/lean4#2210 has been merged, this PR:
* removes all the `set_option synthInstance.etaExperiment true` commands (and some `etaExperiment%` term elaborators)
* removes many but not quite all `set_option maxHeartbeats` commands
* makes various other changes required to cope with leanprover/lean4#2210.



Co-authored-by: Scott Morrison <scott.morrison@anu.edu.au>
Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Co-authored-by: Matthew Ballard <matt@mrb.email>

Author: 4 people

Mathlib/Algebra/Algebra/Subalgebra/Basic.lean

@@ -181,8 +181,6 @@ protected theorem prod_mem {R : Type u} {A : Type v} [CommSemiring R] [CommSemir
   prod_mem h
 #align subalgebra.prod_mem Subalgebra.prod_mem
 
--- instance : Module R A := Algebra.toModule -- Porting note: doesn't help
-set_option synthInstance.etaExperiment true in
 instance {R A : Type _} [CommRing R] [Ring A] [Algebra R A] : SubringClass (Subalgebra R A) A :=
   { Subalgebra.SubsemiringClass with
     neg_mem := fun {S x} hx => neg_one_smul R x ▸ S.smul_mem hx _ }
@@ -1417,9 +1415,6 @@ theorem centralizer_univ : centralizer R Set.univ = center R A :=
 
 end Centralizer
 
--- Porting note: in the following proof, we manually add the instances `_i₁` and `_i₂`
--- Removing those lines and enabling `etaExperiment` on the next line gives a *broken* proof
--- set_option synthInstance.etaExperiment true in
 /-- Suppose we are given `∑ i, lᵢ * sᵢ = 1` in `S`, and `S'` a subalgebra of `S` that contains
 `lᵢ` and `sᵢ`. To check that an `x : S` falls in `S'`, we only need to show that
 `sᵢ ^ n • x ∈ S'` for some `n` for each `sᵢ`. -/
@@ -1428,7 +1423,7 @@ theorem mem_of_finset_sum_eq_one_of_pow_smul_mem {S : Type _} [CommRing S] [Alge
     (e : (∑ i in ι', l i * s i) = 1) (hs : ∀ i, s i ∈ S') (hl : ∀ i, l i ∈ S') (x : S)
     (H : ∀ i, ∃ n : ℕ, (s i ^ n : S) • x ∈ S') : x ∈ S' := by
   -- Porting note: needed to add this instance
-  let _i₁ : Algebra { x // x ∈ S' } { x // x ∈ S' } := Algebra.id _
+  let _i : Algebra { x // x ∈ S' } { x // x ∈ S' } := Algebra.id _
   suffices x ∈ Subalgebra.toSubmodule (Algebra.ofId S' S).range by
     obtain ⟨x, rfl⟩ := this
     exact x.2
@@ -1450,13 +1445,10 @@ theorem mem_of_finset_sum_eq_one_of_pow_smul_mem {S : Type _} [CommRing S] [Alge
   rintro ⟨_, _, ⟨i, hi, rfl⟩, rfl⟩
   change s' i ^ N • x ∈ _
   rw [← tsub_add_cancel_of_le (show n i ≤ N from Finset.le_sup hi), pow_add, mul_smul]
-  -- Porting note: needed to add this instance
-  let _i₂ : SubmonoidClass (Subalgebra R S) S := Subalgebra.SubsemiringClass.toSubmonoidClass
   refine' Submodule.smul_mem _ (⟨_, pow_mem (hs i) _⟩ : S') _
   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/BigOperators/Basic.lean

@@ -1247,7 +1247,7 @@ theorem prod_range_add (f : ℕ → β) (n m : ℕ) :
     (∏ x in range (n + m), f x) = (∏ x in range n, f x) * ∏ x in range m, f (n + x) := by
   induction' m with m hm
   · simp
-  · erw [Nat.add_succ, prod_range_succ, prod_range_succ, hm, mul_assoc]; rfl
+  · erw [Nat.add_succ, prod_range_succ, prod_range_succ, hm, mul_assoc]
 #align finset.prod_range_add Finset.prod_range_add
 #align finset.sum_range_add Finset.sum_range_add
 

Mathlib/Algebra/Category/ModuleCat/Tannaka.lean

@@ -23,7 +23,6 @@ universe u
 
 open CategoryTheory
 
-set_option synthInstance.etaExperiment true in
 /-- An ingredient of Tannaka duality for rings:
 A ring `R` is equivalent to
 the endomorphisms of the additive forgetful functor `Module R ⥤ AddCommGroup`.

Mathlib/Algebra/CharP/Quotient.lean

@@ -47,7 +47,6 @@ theorem quotient' {R : Type _} [CommRing R] (p : ℕ) [CharP R p] (I : Ideal R)
 
 end CharP
 
-set_option synthInstance.etaExperiment true in
 theorem Ideal.Quotient.index_eq_zero {R : Type _} [CommRing R] (I : Ideal R) :
     (↑I.toAddSubgroup.index : R ⧸ I) = 0 := by
   rw [AddSubgroup.index, Nat.card_eq]

Mathlib/Algebra/CharP/Two.lean

@@ -63,7 +63,6 @@ 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/CubicDiscriminant.lean

@@ -531,8 +531,6 @@ theorem eq_prod_three_roots (ha : P.a ≠ 0) (h3 : (map φ P).roots = {x, y, z})
   rw [prod_cons, prod_cons, prod_singleton, mul_assoc, mul_assoc]
 #align cubic.eq_prod_three_roots Cubic.eq_prod_three_roots
 
--- Porting note: Increased heartbeat limit for `C_mul_prod_X_sub_C_eq`
-set_option maxHeartbeats 500000 in
 theorem eq_sum_three_roots (ha : P.a ≠ 0) (h3 : (map φ P).roots = {x, y, z}) :
     map φ P =
       ⟨φ P.a, φ P.a * -(x + y + z), φ P.a * (x * y + x * z + y * z), φ P.a * -(x * y * z)⟩ := by

Mathlib/Algebra/DirectSum/Basic.lean

@@ -389,8 +389,6 @@ def IsInternal {M S : Type _} [DecidableEq ι] [AddCommMonoid M] [SetLike S M]
   Function.Bijective (DirectSum.coeAddMonoidHom A)
 #align direct_sum.is_internal DirectSum.IsInternal
 
--- Porting note: This times out; lean4#2003 may fix this?
-set_option maxHeartbeats 0
 theorem IsInternal.addSubmonoid_iSup_eq_top {M : Type _} [DecidableEq ι] [AddCommMonoid M]
     (A : ι → AddSubmonoid M) (h : IsInternal A) : iSup A = ⊤ := by
   rw [AddSubmonoid.iSup_eq_mrange_dfinsupp_sumAddHom, AddMonoidHom.mrange_top_iff_surjective]

Mathlib/Algebra/Group/Ext.lean

@@ -136,7 +136,7 @@ theorem DivInvMonoid.ext {M : Type _} ⦃m₁ m₂ : DivInvMonoid M⦄ (h_mul :
   have : m₁.div = m₂.div := by
     ext (a b)
     exact @map_div' _ _
-      (@MonoidHom _ _ (_) _) (_) _
+      (@MonoidHom _ _ (_) _) (id _) _
       (@MonoidHom.monoidHomClass _ _ (_) _) f (congr_fun h_inv) a b
   rcases m₁ with @⟨_, ⟨_⟩, ⟨_⟩⟩
   rcases m₂ with @⟨_, ⟨_⟩, ⟨_⟩⟩

Mathlib/Algebra/Hom/Centroid.lean

@@ -498,7 +498,6 @@ theorem toEnd_int_cast (z : ℤ) : (z : CentroidHom α).toEnd = ↑z :=
   rfl
 #align centroid_hom.to_End_int_cast CentroidHom.toEnd_int_cast
 
-set_option maxHeartbeats 1000000 in
 instance : Ring (CentroidHom α) :=
   toEnd_injective.ring _ toEnd_zero toEnd_one toEnd_add toEnd_mul toEnd_neg toEnd_sub
     toEnd_nsmul toEnd_zsmul toEnd_pow toEnd_nat_cast toEnd_int_cast

Mathlib/Algebra/Hom/Equiv/Basic.lean

@@ -192,6 +192,10 @@ instance [Mul M] [Mul N] : MulEquivClass (M ≃* N) M N where
     apply Equiv.coe_fn_injective h₁
   map_mul := map_mul'
 
+@[to_additive] -- shortcut instance that doesn't generate any subgoals
+instance [Mul M] [Mul N] : CoeFun (M ≃* N) fun _ => M → N where
+  coe f := f
+
 variable [Mul M] [Mul N] [Mul P] [Mul Q]
 
 @[to_additive (attr := simp)]