chore: remove set_option autoImplicit false (#1608)

These were mostly added in the process of porting and weren't removed at the end. There was one that may have been needed, let's see what CI says.
leanprover-community · Jan 17, 2023 · 4535a7d · 4535a7d
1 parent f768b2c
commit 4535a7d
Show file tree

Hide file tree

Showing 5 changed files with 0 additions and 12 deletions.
diff --git a/Mathlib/Control/Functor.lean b/Mathlib/Control/Functor.lean
@@ -212,8 +212,6 @@ protected theorem id_map : ∀ x : Comp F G α, Comp.map id x = x
   -- porting note: `rfl` wasn't needed in mathlib3
 #align functor.comp.id_map Functor.Comp.id_map
 
--- porting note: because `LawfulFunctor G` wasn't needed in the proof we need `autoImplicit`s off
-set_option autoImplicit false in
 protected theorem comp_map (g' : α → β) (h : β → γ) :
     ∀ x : Comp F G α, Comp.map (h ∘ g') x = Comp.map h (Comp.map g' x)
   | Comp.mk x => by simp [Comp.map, Comp.mk, Functor.map_comp_map, functor_norm]

diff --git a/Mathlib/Data/Fin/Basic.lean b/Mathlib/Data/Fin/Basic.lean
@@ -81,8 +81,6 @@ This file expands on the development in the core library.
 
 -/
 
--- set_option autoImplicit false
-
 universe u v
 
 open Fin Nat Function
@@ -1125,8 +1123,6 @@ theorem castAdd_lt {m : ℕ} (n : ℕ) (i : Fin m) : (castAdd n i : ℕ) < m :=
   simp
 #align fin.cast_add_lt Fin.castAdd_lt
 
-set_option autoImplicit false
-
 @[simp]
 theorem castAdd_mk (m : ℕ) (i : ℕ) (h : i < n) : castAdd m ⟨i, h⟩ = ⟨i, Nat.lt_add_right i n m h⟩ :=
   rfl

diff --git a/Mathlib/Data/Set/Functor.lean b/Mathlib/Data/Set/Functor.lean
@@ -18,8 +18,6 @@ import Mathlib.Control.Basic
 This file defines the functor structure of `Set`.
 -/
 
-set_option autoImplicit false
-
 universe u
 
 open Function

diff --git a/Mathlib/Data/Set/UnionLift.lean b/Mathlib/Data/Set/UnionLift.lean
@@ -41,8 +41,6 @@ constants, unary functions, or binary functions are preserved. These lemmas are:
 directed union, directed supremum, glue, gluing
 -/
 
-set_option autoImplicit false
-
 variable {α ι β : Type _}
 
 namespace Set

diff --git a/Mathlib/Data/Setoid/Basic.lean b/Mathlib/Data/Setoid/Basic.lean
@@ -37,8 +37,6 @@ reason about them using the existing `Setoid` and its infrastructure.
 setoid, equivalence, iseqv, relation, equivalence relation
 -/
 
-set_option autoImplicit false
-
 variable {α : Type _} {β : Type _}
 
 /-- A version of `Setoid.r` that takes the equivalence relation as an explicit argument. -/