chore(Order): remove almost all autoImplicit (#14304)

grunweg · grunweg · commit aa30cf905a80 · 2024-07-01T17:37:33.000Z
In two files, only reduce the scope of it;
the other occurrences seem harder to remove.
diff --git a/Mathlib/Order/Atoms.lean b/Mathlib/Order/Atoms.lean
@@ -49,10 +49,7 @@ which are lattices with only two elements, and related ideas.
 
 -/
 
-set_option autoImplicit true
-
-
-variable {α β : Type*}
+variable {ι : Sort*} {α β : Type*}
 
 section Atoms
 
@@ -114,7 +111,7 @@ alias ⟨CovBy.is_atom, IsAtom.bot_covBy⟩ := bot_covBy_iff
 
 end PartialOrder
 
-theorem atom_le_iSup [Order.Frame α] (ha : IsAtom a) {f : ι → α} :
+theorem atom_le_iSup [Order.Frame α] {a : α} (ha : IsAtom a) {f : ι → α} :
     a ≤ iSup f ↔ ∃ i, a ≤ f i := by
   refine ⟨?_, fun ⟨i, hi⟩ => le_trans hi (le_iSup _ _)⟩
   show (a ≤ ⨆ i, f i) → _
@@ -204,7 +201,7 @@ alias ⟨CovBy.isCoatom, IsCoatom.covBy_top⟩ := covBy_top_iff
 
 end PartialOrder
 
-theorem iInf_le_coatom [Order.Coframe α] (ha : IsCoatom a) {f : ι → α} :
+theorem iInf_le_coatom [Order.Coframe α] {a : α} (ha : IsCoatom a) {f : ι → α} :
     iInf f ≤ a ↔ ∃ i, f i ≤ a :=
   atom_le_iSup (α := αᵒᵈ) ha
 
@@ -1003,7 +1000,8 @@ end «Prop»
 
 namespace Pi
 
-variable {π : ι → Type u}
+universe u
+variable {ι : Type*} {π : ι → Type u}
 
 protected theorem eq_bot_iff [∀ i, Bot (π i)] {f : ∀ i, π i} : f = ⊥ ↔ ∀ i, f i = ⊥ :=
   ⟨(· ▸ by simp), fun h => funext fun i => by simp [h]⟩
@@ -1037,8 +1035,8 @@ theorem isAtom_iff {f : ∀ i, π i} [∀ i, PartialOrder (π i)] [∀ i, OrderB
       simpa using this (fun k => by by_cases h : k = j; { subst h; simp }; simp [h]) i
         (by rwa [Function.update_noteq (Ne.symm hj), bot_apply, bot_lt_iff_ne_bot]) j
 
-theorem isAtom_single [DecidableEq ι] [∀ i, PartialOrder (π i)] [∀ i, OrderBot (π i)] {a : π i}
-    (h : IsAtom a) : IsAtom (Function.update (⊥ : ∀ i, π i) i a) :=
+theorem isAtom_single {i : ι} [DecidableEq ι] [∀ i, PartialOrder (π i)] [∀ i, OrderBot (π i)]
+    {a : π i} (h : IsAtom a) : IsAtom (Function.update (⊥ : ∀ i, π i) i a) :=
   isAtom_iff.2 ⟨i, by simpa, fun j hji => Function.update_noteq hji _ _⟩
 
 theorem isAtom_iff_eq_single [DecidableEq ι] [∀ i, PartialOrder (π i)]
diff --git a/Mathlib/Order/Bounds/OrderIso.lean b/Mathlib/Order/Bounds/OrderIso.lean
@@ -12,13 +12,11 @@ import Mathlib.Order.Hom.Set
 # Order isomorphisms and bounds.
 -/
 
-set_option autoImplicit true
-
 open Set
 
 namespace OrderIso
 
-variable [Preorder α] [Preorder β] (f : α ≃o β)
+variable {α β : Type*} [Preorder α] [Preorder β] (f : α ≃o β)
 
 theorem upperBounds_image {s : Set α} : upperBounds (f '' s) = f '' upperBounds s :=
   Subset.antisymm
diff --git a/Mathlib/Order/CompleteBooleanAlgebra.lean b/Mathlib/Order/CompleteBooleanAlgebra.lean
@@ -50,12 +50,9 @@ distributive lattice.
 * [Francis Borceux, *Handbook of Categorical Algebra III*][borceux-vol3]
 -/
 
-set_option autoImplicit true
-
-
 open Function Set
 
-universe u v w
+universe u v w w'
 
 variable {α : Type u} {β : Type v} {ι : Sort w} {κ : ι → Sort w'}
 
diff --git a/Mathlib/Order/Filter/AtTopBot.lean b/Mathlib/Order/Filter/AtTopBot.lean
@@ -28,8 +28,6 @@ In this file we define the filters
 Then we prove many lemmas like “if `f → +∞`, then `f ± c → +∞`”.
 -/
 
-set_option autoImplicit true
-
 variable {ι ι' α β γ : Type*}
 
 open Set
@@ -263,12 +261,12 @@ theorem eventually_forall_le_atBot [Preorder α] {p : α → Prop} :
     (∀ᶠ x in atBot, ∀ y, y ≤ x → p y) ↔ ∀ᶠ x in atBot, p x :=
   eventually_forall_ge_atTop (α := αᵒᵈ)
 
-theorem Tendsto.eventually_forall_ge_atTop {α β : Type*} [Preorder β] {l : Filter α}
+theorem Tendsto.eventually_forall_ge_atTop [Preorder β] {l : Filter α}
     {p : β → Prop} {f : α → β} (hf : Tendsto f l atTop) (h_evtl : ∀ᶠ x in atTop, p x) :
     ∀ᶠ x in l, ∀ y, f x ≤ y → p y := by
   rw [← Filter.eventually_forall_ge_atTop] at h_evtl; exact (h_evtl.comap f).filter_mono hf.le_comap
 
-theorem Tendsto.eventually_forall_le_atBot {α β : Type*} [Preorder β] {l : Filter α}
+theorem Tendsto.eventually_forall_le_atBot [Preorder β] {l : Filter α}
     {p : β → Prop} {f : α → β} (hf : Tendsto f l atBot) (h_evtl : ∀ᶠ x in atBot, p x) :
     ∀ᶠ x in l, ∀ y, y ≤ f x → p y := by
   rw [← Filter.eventually_forall_le_atBot] at h_evtl; exact (h_evtl.comap f).filter_mono hf.le_comap
@@ -651,7 +649,7 @@ theorem frequently_low_scores [LinearOrder β] [NoMinOrder β] {u : ℕ → β}
   @frequently_high_scores βᵒᵈ _ _ _ hu
 #align filter.frequently_low_scores Filter.frequently_low_scores
 
-theorem strictMono_subseq_of_tendsto_atTop {β : Type*} [LinearOrder β] [NoMaxOrder β] {u : ℕ → β}
+theorem strictMono_subseq_of_tendsto_atTop [LinearOrder β] [NoMaxOrder β] {u : ℕ → β}
     (hu : Tendsto u atTop atTop) : ∃ φ : ℕ → ℕ, StrictMono φ ∧ StrictMono (u ∘ φ) :=
   let ⟨φ, h, h'⟩ := extraction_of_frequently_atTop (frequently_high_scores hu)
   ⟨φ, h, fun _ m hnm => h' m _ (h hnm)⟩
@@ -1545,9 +1543,9 @@ theorem prod_atTop_atTop_eq [Preorder α] [Preorder β] :
 #align filter.prod_at_top_at_top_eq Filter.prod_atTop_atTop_eq
 
 -- Porting note: generalized from `SemilatticeSup` to `Preorder`
-theorem prod_atBot_atBot_eq [Preorder β₁] [Preorder β₂] :
-    (atBot : Filter β₁) ×ˢ (atBot : Filter β₂) = (atBot : Filter (β₁ × β₂)) :=
-  @prod_atTop_atTop_eq β₁ᵒᵈ β₂ᵒᵈ _ _
+theorem prod_atBot_atBot_eq [Preorder α] [Preorder β] :
+    (atBot : Filter α) ×ˢ (atBot : Filter β) = (atBot : Filter (α × β)) :=
+  @prod_atTop_atTop_eq αᵒᵈ βᵒᵈ _ _
 #align filter.prod_at_bot_at_bot_eq Filter.prod_atBot_atBot_eq
 
 -- Porting note: generalized from `SemilatticeSup` to `Preorder`
@@ -2023,7 +2021,7 @@ lemma frequently_iff_seq_forall {ι : Type*} {l : Filter ι} {p : ι → Prop}
     hnsl.frequently <| frequently_of_forall hpns⟩
 
 /-- A sequence converges if every subsequence has a convergent subsequence. -/
-theorem tendsto_of_subseq_tendsto {α ι : Type*} {x : ι → α} {f : Filter α} {l : Filter ι}
+theorem tendsto_of_subseq_tendsto {ι : Type*} {x : ι → α} {f : Filter α} {l : Filter ι}
     [l.IsCountablyGenerated]
     (hxy : ∀ ns : ℕ → ι, Tendsto ns atTop l →
       ∃ ms : ℕ → ℕ, Tendsto (fun n => x (ns <| ms n)) atTop f) :
diff --git a/Mathlib/Order/Filter/Bases.lean b/Mathlib/Order/Filter/Bases.lean
@@ -78,14 +78,8 @@ machinery, e.g., `simp only [true_and]` or `simp only [forall_const]` can help w
 `p = fun _ ↦ True`.
 -/
 
-set_option autoImplicit true
-
-
 open Set Filter
 
-open scoped Classical
-open Filter
-
 section sort
 
 variable {α β γ : Type*} {ι ι' : Sort*}
diff --git a/Mathlib/Order/Filter/Basic.lean b/Mathlib/Order/Filter/Basic.lean
@@ -79,9 +79,6 @@ we do *not* require. This gives `Filter X` better formal properties, in particul
 
 assert_not_exists OrderedSemiring
 
-set_option autoImplicit true
-
-
 open Function Set Order
 open scoped Classical
 
@@ -1333,10 +1330,11 @@ theorem Eventually.exists {p : α → Prop} {f : Filter α} [NeBot f] (hp : ∀
   hp.frequently.exists
 #align filter.eventually.exists Filter.Eventually.exists
 
-lemma frequently_iff_neBot {p : α → Prop} : (∃ᶠ x in l, p x) ↔ NeBot (l ⊓ 𝓟 {x | p x}) := by
+lemma frequently_iff_neBot {l : Filter α} {p : α → Prop} :
+    (∃ᶠ x in l, p x) ↔ NeBot (l ⊓ 𝓟 {x | p x}) := by
   rw [neBot_iff, Ne, inf_principal_eq_bot]; rfl
 
-lemma frequently_mem_iff_neBot {s : Set α} : (∃ᶠ x in l, x ∈ s) ↔ NeBot (l ⊓ 𝓟 s) :=
+lemma frequently_mem_iff_neBot {l : Filter α} {s : Set α} : (∃ᶠ x in l, x ∈ s) ↔ NeBot (l ⊓ 𝓟 s) :=
   frequently_iff_neBot
 
 theorem frequently_iff_forall_eventually_exists_and {p : α → Prop} {f : Filter α} :
@@ -1539,7 +1537,8 @@ theorem EventuallyEq.trans {l : Filter α} {f g h : α → β} (H₁ : f =ᶠ[l]
   H₂.rw (fun x y => f x = y) H₁
 #align filter.eventually_eq.trans Filter.EventuallyEq.trans
 
-instance : Trans ((· =ᶠ[l] ·) : (α → β) → (α → β) → Prop) (· =ᶠ[l] ·) (· =ᶠ[l] ·) where
+instance {l : Filter α} :
+    Trans ((· =ᶠ[l] ·) : (α → β) → (α → β) → Prop) (· =ᶠ[l] ·) (· =ᶠ[l] ·) where
   trans := EventuallyEq.trans
 
 theorem EventuallyEq.prod_mk {l} {f f' : α → β} (hf : f =ᶠ[l] f') {g g' : α → γ} (hg : g =ᶠ[l] g') :
@@ -1734,6 +1733,8 @@ instance : Trans ((· ≤ᶠ[l] ·) : (α → β) → (α → β) → Prop) (·
 
 end Preorder
 
+variable {l : Filter α}
+
 theorem EventuallyLE.antisymm [PartialOrder β] {l : Filter α} {f g : α → β} (h₁ : f ≤ᶠ[l] g)
     (h₂ : g ≤ᶠ[l] f) : f =ᶠ[l] g :=
   h₂.mp <| h₁.mono fun _ => le_antisymm
@@ -2139,7 +2140,7 @@ theorem map_pure (f : α → β) (a : α) : map f (pure a) = pure (f a) :=
   rfl
 #align filter.map_pure Filter.map_pure
 
-theorem pure_le_principal (a : α) : pure a ≤ 𝓟 s ↔ a ∈ s := by
+theorem pure_le_principal {s : Set α} (a : α) : pure a ≤ 𝓟 s ↔ a ∈ s := by
   simp
 
 @[simp] theorem join_pure (f : Filter α) : join (pure f) = f := rfl
@@ -2367,11 +2368,13 @@ theorem comap_mono : Monotone (comap m) :=
 #align filter.comap_mono Filter.comap_mono
 
 /-- Temporary lemma that we can tag with `gcongr` -/
-@[gcongr] theorem _root_.GCongr.Filter.map_le_map (h : F ≤ G) : map m F ≤ map m G := map_mono h
+@[gcongr] theorem _root_.GCongr.Filter.map_le_map {F G : Filter α} (h : F ≤ G) :
+    map m F ≤ map m G := map_mono h
 
 /-- Temporary lemma that we can tag with `gcongr` -/
 @[gcongr]
-theorem _root_.GCongr.Filter.comap_le_comap (h : F ≤ G) : comap m F ≤ comap m G := comap_mono h
+theorem _root_.GCongr.Filter.comap_le_comap {F G : Filter β} (h : F ≤ G) :
+    comap m F ≤ comap m G := comap_mono h
 
 @[simp] theorem map_bot : map m ⊥ = ⊥ := (gc_map_comap m).l_bot
 #align filter.map_bot Filter.map_bot
@@ -3317,25 +3320,27 @@ theorem Set.MapsTo.tendsto {α β} {s : Set α} {t : Set β} {f : α → β} (h
   Filter.tendsto_principal_principal.2 h
 #align set.maps_to.tendsto Set.MapsTo.tendsto
 
-theorem Filter.EventuallyEq.comp_tendsto {f' : α → β} (H : f =ᶠ[l] f') {g : γ → α} {lc : Filter γ}
-    (hg : Tendsto g lc l) : f ∘ g =ᶠ[lc] f' ∘ g :=
+theorem Filter.EventuallyEq.comp_tendsto {α β γ : Type*} {l : Filter α} {f : α → β} {f' : α → β}
+    (H : f =ᶠ[l] f') {g : γ → α} {lc : Filter γ} (hg : Tendsto g lc l) :
+    f ∘ g =ᶠ[lc] f' ∘ g :=
   hg.eventually H
 #align filter.eventually_eq.comp_tendsto Filter.EventuallyEq.comp_tendsto
 
+variable {α β : Type*} {F : Filter α} {G : Filter β}
+
 theorem Filter.map_mapsTo_Iic_iff_tendsto {m : α → β} :
     MapsTo (map m) (Iic F) (Iic G) ↔ Tendsto m F G :=
   ⟨fun hm ↦ hm right_mem_Iic, fun hm _ ↦ hm.mono_left⟩
 
 alias ⟨_, Filter.Tendsto.map_mapsTo_Iic⟩ := Filter.map_mapsTo_Iic_iff_tendsto
 
-theorem Filter.map_mapsTo_Iic_iff_mapsTo {m : α → β} :
+theorem Filter.map_mapsTo_Iic_iff_mapsTo {s : Set α} {t : Set β} {m : α → β} :
     MapsTo (map m) (Iic <| 𝓟 s) (Iic <| 𝓟 t) ↔ MapsTo m s t := by
   rw [map_mapsTo_Iic_iff_tendsto, tendsto_principal_principal, MapsTo]
 
 alias ⟨_, Set.MapsTo.filter_map_Iic⟩ := Filter.map_mapsTo_Iic_iff_mapsTo
 
 -- TODO(Anatole): unify with the global case
-
 theorem Filter.map_surjOn_Iic_iff_le_map {m : α → β} :
     SurjOn (map m) (Iic F) (Iic G) ↔ G ≤ map m F := by
   refine ⟨fun hm ↦ ?_, fun hm ↦ ?_⟩
@@ -3345,13 +3350,13 @@ theorem Filter.map_surjOn_Iic_iff_le_map {m : α → β} :
       fun H (hHG : H ≤ G) ↦ by simpa [Filter.push_pull] using hHG.trans hm
     exact this.surjOn fun H _ ↦ mem_Iic.mpr inf_le_left
 
-theorem Filter.map_surjOn_Iic_iff_surjOn {m : α → β} :
+theorem Filter.map_surjOn_Iic_iff_surjOn {s : Set α} {t : Set β} {m : α → β} :
     SurjOn (map m) (Iic <| 𝓟 s) (Iic <| 𝓟 t) ↔ SurjOn m s t := by
   rw [map_surjOn_Iic_iff_le_map, map_principal, principal_mono, SurjOn]
 
 alias ⟨_, Set.SurjOn.filter_map_Iic⟩ := Filter.map_surjOn_Iic_iff_surjOn
 
-theorem Filter.filter_injOn_Iic_iff_injOn {m : α → β} :
+theorem Filter.filter_injOn_Iic_iff_injOn {s : Set α} {m : α → β} :
     InjOn (map m) (Iic <| 𝓟 s) ↔ InjOn m s := by
   refine ⟨fun hm x hx y hy hxy ↦ ?_, fun hm F hF G hG ↦ ?_⟩
   · rwa [← pure_injective.eq_iff, ← map_pure, ← map_pure, hm.eq_iff, pure_injective.eq_iff]
diff --git a/Mathlib/Order/Filter/CountableSeparatingOn.lean b/Mathlib/Order/Filter/CountableSeparatingOn.lean
@@ -70,8 +70,6 @@ We formalize several versions of this theorem in
 filter, countable
 -/
 
-set_option autoImplicit true
-
 open Function Set Filter
 
 /-- We say that a type `α` has a *countable separating family of sets* satisfying a predicate
@@ -140,7 +138,7 @@ theorem HasCountableSeparatingOn.subtype_iff {α : Type*} {p : Set α → Prop}
 
 namespace Filter
 
-variable {l : Filter α} [CountableInterFilter l] {f g : α → β}
+variable {α β : Type*} {l : Filter α} [CountableInterFilter l] {f g : α → β}
 
 /-!
 ### Filters supported on a (sub)singleton
diff --git a/Mathlib/Order/InitialSeg.lean b/Mathlib/Order/InitialSeg.lean
@@ -39,9 +39,6 @@ any `b' < b` also belongs to the range). The type of these embeddings from `r` t
 `InitialSeg r s`, and denoted by `r ≼i s`.
 -/
 
-set_option autoImplicit true
-
-
 variable {α : Type*} {β : Type*} {γ : Type*} {r : α → α → Prop} {s : β → β → Prop}
   {t : γ → γ → Prop}
 
@@ -89,7 +86,7 @@ theorem init (f : r ≼i s) {a : α} {b : β} : s b (f a) → ∃ a', f a' = b :
   f.init' _ _
 #align initial_seg.init InitialSeg.init
 
-theorem map_rel_iff (f : r ≼i s) : s (f a) (f b) ↔ r a b :=
+theorem map_rel_iff {a b : α} (f : r ≼i s) : s (f a) (f b) ↔ r a b :=
   f.map_rel_iff'
 #align initial_seg.map_rel_iff InitialSeg.map_rel_iff
 
diff --git a/Mathlib/Order/Interval/Finset/Defs.lean b/Mathlib/Order/Interval/Finset/Defs.lean
@@ -95,9 +95,6 @@ successor (and actually a predecessor as well), so it is a `SuccOrder`, but it's
 as `Icc (-1) 1` is infinite.
 -/
 
-set_option autoImplicit true
-
-
 open Finset Function
 
 /-- This is a mixin class describing a locally finite order,
@@ -1269,6 +1266,8 @@ end Finite
 /-! We make the instances below low priority
 so when alternative constructions are available they are preferred. -/
 
+variable {y : α}
+
 instance (priority := low) [Preorder α] [DecidableRel ((· : α) ≤ ·)] [LocallyFiniteOrder α] :
     LocallyFiniteOrderTop { x : α // x ≤ y } where
   finsetIoi a := Finset.Ioc a ⟨y, by rfl⟩
diff --git a/Mathlib/Order/LiminfLimsup.lean b/Mathlib/Order/LiminfLimsup.lean
@@ -36,9 +36,6 @@ the definitions of Limsup and Liminf.
 In complete lattices, however, it coincides with the `Inf Sup` definition.
 -/
 
-set_option autoImplicit true
-
-
 open Filter Set Function
 
 variable {α β γ ι ι' : Type*}
@@ -244,7 +241,7 @@ theorem IsBounded.isCobounded_le [Preorder α] [NeBot f] (h : f.IsBounded (· 
   h.isCobounded_flip
 #align filter.is_bounded.is_cobounded_le Filter.IsBounded.isCobounded_le
 
-theorem IsBoundedUnder.isCoboundedUnder_flip {l : Filter γ} [IsTrans α r] [NeBot l]
+theorem IsBoundedUnder.isCoboundedUnder_flip {u : γ → α} {l : Filter γ} [IsTrans α r] [NeBot l]
     (h : l.IsBoundedUnder r u) : l.IsCoboundedUnder (flip r) u :=
   h.isCobounded_flip
 
diff --git a/Mathlib/Order/Minimal.lean b/Mathlib/Order/Minimal.lean
diff --git a/Mathlib/Order/RelIso/Basic.lean b/Mathlib/Order/RelIso/Basic.lean
