chore(*): remove instance binders in exists, for mathport (#9083)

Per @digama0's request at https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Instance.20binders.20in.20exists.

Instance binders under an "Exists" aren't allowed in Lean4, so we're backport removing them. I've just turned relevant `[X]` binders into `(_ : X)` binders, and it seems to all still work. (i.e. the instance binders weren't actually doing anything).

It turns out two of the problem binders were in `infi` or `supr`, not `Exists`, but I treated them the same way.



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

src/analysis/convex/caratheodory.lean

@@ -157,7 +157,7 @@ end
 
 /-- A more explicit version of `convex_hull_eq_union`. -/
 theorem eq_pos_convex_span_of_mem_convex_hull {x : E} (hx : x ∈ convex_hull s) :
-  ∃ (ι : Sort (u+1)) [fintype ι], by exactI ∃ (z : ι → E) (w : ι → ℝ)
+  ∃ (ι : Sort (u+1)) (_ : fintype ι), by exactI ∃ (z : ι → E) (w : ι → ℝ)
     (hss : set.range z ⊆ s) (hai : affine_independent ℝ z)
     (hw : ∀ i, 0 < w i), ∑ i, w i = 1 ∧ ∑ i, w i • z i = x :=
 begin

src/category_theory/abelian/pseudoelements.lean

@@ -93,7 +93,7 @@ a.hom ≫ f
 /-- Two arrows `f : X ⟶ P` and `g : Y ⟶ P` are called pseudo-equal if there is some object
     `R` and epimorphisms `p : R ⟶ X` and `q : R ⟶ Y` such that `p ≫ f = q ≫ g`. -/
 def pseudo_equal (P : C) (f g : over P) : Prop :=
-∃ (R : C) (p : R ⟶ f.1) (q : R ⟶ g.1) [epi p] [epi q], p ≫ f.hom = q ≫ g.hom
+∃ (R : C) (p : R ⟶ f.1) (q : R ⟶ g.1) (_ : epi p) (_ : epi q), p ≫ f.hom = q ≫ g.hom
 
 lemma pseudo_equal_refl {P : C} : reflexive (pseudo_equal P) :=
 λ f, ⟨f.1, 𝟙 f.1, 𝟙 f.1, by apply_instance, by apply_instance, by simp⟩

src/category_theory/essentially_small.lean

@@ -29,7 +29,7 @@ namespace category_theory
 /-- A category is `essentially_small.{w}` if there exists
 an equivalence to some `S : Type w` with `[small_category S]`. -/
 class essentially_small (C : Type u) [category.{v} C] : Prop :=
-(equiv_small_category : ∃ (S : Type w) [small_category S], by exactI nonempty (C ≌ S))
+(equiv_small_category : ∃ (S : Type w) (_ : small_category S), by exactI nonempty (C ≌ S))
 
 /-- Constructor for `essentially_small C` from an explicit small category witness. -/
 lemma essentially_small.mk' {C : Type u} [category.{v} C] {S : Type w} [small_category S]

src/combinatorics/hales_jewett.lean

@@ -174,7 +174,7 @@ by simp_rw [line.apply, line.diagonal, option.get_or_else_none]
 for the proof. See `exists_mono_in_high_dimension` for a fully universe-polymorphic version. -/
 private theorem exists_mono_in_high_dimension' :
   ∀ (α : Type u) [fintype α] (κ : Type (max v u)) [fintype κ],
-  ∃ (ι : Type) [fintype ι], ∀ C : (ι → α) → κ, ∃ l : line α ι, l.is_mono C :=
+  ∃ (ι : Type) (_ : fintype ι), ∀ C : (ι → α) → κ, ∃ l : line α ι, l.is_mono C :=
 -- The proof proceeds by induction on `α`.
 fintype.induction_empty_option
 -- We have to show that the theorem is invariant under `α ≃ α'` for the induction to work.
@@ -196,7 +196,7 @@ begin -- Now we have to show that the theorem holds for `option α` if it holds
     rintros (_ | ⟨a⟩), refl, exact (h ⟨a⟩).elim, },
 -- The key idea is to show that for every `r`, in high dimension we can either find
 -- `r` color focused lines or a monochromatic line.
-  suffices key : ∀ r : ℕ, ∃ (ι : Type) [fintype ι], ∀ C : (ι → (option α)) → κ,
+  suffices key : ∀ r : ℕ, ∃ (ι : Type) (_ : fintype ι), ∀ C : (ι → (option α)) → κ,
     (∃ s : color_focused C, s.lines.card = r) ∨ (∃ l, is_mono C l),
 -- Given the key claim, we simply take `r = |κ| + 1`. We cannot have this many distinct colors so
 -- we must be in the second case, where there is a monochromatic line.

src/group_theory/subgroup.lean

@@ -1228,7 +1228,7 @@ theorem normal_closure_mono {s t : set G} (h : s ⊆ t) : normal_closure s ≤ n
 normal_closure_le_normal (set.subset.trans h subset_normal_closure)
 
 theorem normal_closure_eq_infi : normal_closure s =
-  ⨅ (N : subgroup G) [normal N] (hs : s ⊆ N), N :=
+  ⨅ (N : subgroup G) (_ : normal N) (hs : s ⊆ N), N :=
 le_antisymm
   (le_infi (λ N, le_infi (λ hN, by exactI le_infi (normal_closure_le_normal))))
   (infi_le_of_le (normal_closure s) (infi_le_of_le (by apply_instance)
@@ -1270,7 +1270,7 @@ lemma normal_core_mono {H K : subgroup G} (h : H ≤ K) : H.normal_core ≤ K.no
 normal_le_normal_core.mpr (H.normal_core_le.trans h)
 
 lemma normal_core_eq_supr (H : subgroup G) :
-  H.normal_core = ⨆ (N : subgroup G) [normal N] (hs : N ≤ H), N :=
+  H.normal_core = ⨆ (N : subgroup G) (_ : normal N) (hs : N ≤ H), N :=
 le_antisymm (le_supr_of_le H.normal_core
   (le_supr_of_le H.normal_core_normal (le_supr_of_le H.normal_core_le le_rfl)))
   (supr_le (λ N, supr_le (λ hN, supr_le (by exactI normal_le_normal_core.mpr))))

src/order/extension.lean

@@ -21,7 +21,7 @@ open_locale classical
 Any partial order can be extended to a linear order.
 -/
 theorem extend_partial_order {α : Type u} (r : α → α → Prop) [is_partial_order α r] :
-  ∃ (s : α → α → Prop) [is_linear_order α s], r ≤ s :=
+  ∃ (s : α → α → Prop) (_ : is_linear_order α s), r ≤ s :=
 begin
   let S := {s | is_partial_order α s},
   have hS : ∀ c, c ⊆ S → zorn.chain (≤) c → ∀ y ∈ c, (∃ ub ∈ S, ∀ z ∈ c, z ≤ ub),

src/ring_theory/finiteness.lean

@@ -176,7 +176,7 @@ end
 
 /-- An algebra is finitely generated if and only if it is a quotient
 of a polynomial ring whose variables are indexed by a fintype. -/
-lemma iff_quotient_mv_polynomial' : (finite_type R A) ↔ ∃ (ι : Type u_2) [fintype ι]
+lemma iff_quotient_mv_polynomial' : (finite_type R A) ↔ ∃ (ι : Type u_2) (_ : fintype ι)
   (f : (mv_polynomial ι R) →ₐ[R] A), (surjective f) :=
 begin
   split,
@@ -306,7 +306,7 @@ end
 
 /-- An algebra is finitely presented if and only if it is a quotient of a polynomial ring whose
 variables are indexed by a fintype by a finitely generated ideal. -/
-lemma iff_quotient_mv_polynomial' : finite_presentation R A ↔ ∃ (ι : Type u_2) [fintype ι]
+lemma iff_quotient_mv_polynomial' : finite_presentation R A ↔ ∃ (ι : Type u_2) (_ : fintype ι)
   (f : (_root_.mv_polynomial ι R) →ₐ[R] A), (surjective f) ∧ f.to_ring_hom.ker.fg :=
 begin
   split,

src/ring_theory/polynomial/dickson.lean

@@ -182,7 +182,7 @@ begin
   -- Since `X ^ p` also satisfies this property in characteristic `p`,
   -- we can use a variant on `polynomial.funext` to conclude that these polynomials are equal.
   -- For this argument, we need an arbitrary infinite field of characteristic `p`.
-  obtain ⟨K, _, _, H⟩ : ∃ (K : Type) [field K], by exactI ∃ [char_p K p], infinite K,
+  obtain ⟨K, _, _, H⟩ : ∃ (K : Type) (_ : field K), by exactI ∃ (_ : char_p K p), infinite K,
   { let K := fraction_ring (polynomial (zmod p)),
     let f : zmod p →+* K := (algebra_map _ (fraction_ring _)).comp C,
     haveI : char_p K p, { rw ← f.char_p_iff_char_p, apply_instance },

src/topology/metric_space/basic.lean

@@ -560,7 +560,7 @@ theorem totally_bounded_iff {s : set α} :
 /-- A pseudometric space space is totally bounded if one can reconstruct up to any ε>0 any element
 of the space from finitely many data. -/
 lemma totally_bounded_of_finite_discretization {s : set α}
-  (H : ∀ε > (0 : ℝ), ∃ (β : Type u) [fintype β] (F : s → β),
+  (H : ∀ε > (0 : ℝ), ∃ (β : Type u) (_ : fintype β) (F : s → β),
     ∀x y, F x = F y → dist (x:α) y < ε) :
   totally_bounded s :=
 begin
@@ -2110,7 +2110,7 @@ open topological_space
 /-- A metric space space is second countable if one can reconstruct up to any `ε>0` any element of
 the space from countably many data. -/
 lemma second_countable_of_countable_discretization {α : Type u} [metric_space α]
-  (H : ∀ε > (0 : ℝ), ∃ (β : Type*) [encodable β] (F : α → β), ∀x y, F x = F y → dist x y ≤ ε) :
+  (H : ∀ε > (0 : ℝ), ∃ (β : Type*) (_ : encodable β) (F : α → β), ∀x y, F x = F y → dist x y ≤ ε) :
   second_countable_topology α :=
 begin
   cases (univ : set α).eq_empty_or_nonempty with hs hs,