chore: use more inferInstanceAs (#37315)

Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>

Author: sgouezel

Mathlib/Analysis/SpecialFunctions/Trigonometric/Angle.lean

@@ -41,10 +41,9 @@ protected def coe (r : ℝ) : Angle := QuotientAddGroup.mk r
 instance : Coe ℝ Angle := ⟨Angle.coe⟩
 
 instance : CircularOrder Real.Angle :=
-  QuotientAddGroup.circularOrder (hp' := ⟨by simp [pi_pos]⟩)
+  fast_instance% QuotientAddGroup.circularOrder (hp' := ⟨by simp [pi_pos]⟩)
 
-
-@[continuity]
+@[continuity, fun_prop]
 theorem continuous_coe : Continuous ((↑) : ℝ → Angle) :=
   continuous_quotient_mk'
 

Mathlib/Combinatorics/SimpleGraph/Connectivity/Finite.lean

@@ -57,7 +57,7 @@ instance : DecidableRel G.Reachable := fun u v =>
   decidable_of_iff' _ (reachable_iff_exists_finsetWalkLength_nonempty G u v)
 
 instance : Fintype G.ConnectedComponent :=
-  @Quotient.fintype _ _ G.reachableSetoid (inferInstance : DecidableRel G.Reachable)
+  fast_instance% @Quotient.fintype _ _ G.reachableSetoid (inferInstance : DecidableRel G.Reachable)
 
 instance : Decidable G.Preconnected :=
   inferInstanceAs <| Decidable (∀ u v, G.Reachable u v)

Mathlib/Combinatorics/SimpleGraph/EdgeLabeling.lean

@@ -38,7 +38,7 @@ def EdgeLabeling (G : SimpleGraph V) (K : Type*) :=
   G.edgeSet → K
 
 instance [DecidableEq V] [Fintype G.edgeSet] [Fintype K] : Fintype (EdgeLabeling G K) :=
-  Pi.instFintype
+  inferInstanceAs <| Fintype (G.edgeSet → K)
 
 instance [Finite G.edgeSet] [Finite K] : Finite (EdgeLabeling G K) :=
   Pi.finite
@@ -47,7 +47,7 @@ instance [Nonempty K] : Nonempty (EdgeLabeling G K) :=
   Pi.instNonempty
 
 instance [Inhabited K] : Inhabited (EdgeLabeling G K) :=
-  Pi.instInhabited
+  inferInstanceAs <| Inhabited (G.edgeSet → K)
 
 instance [Subsingleton K] : Subsingleton (EdgeLabeling G K) :=
   Pi.instSubsingleton
@@ -56,7 +56,7 @@ instance [Nonempty G.edgeSet] [Nontrivial K] : Nontrivial (EdgeLabeling G K) :=
   Function.nontrivial
 
 instance [Unique K] : Unique (EdgeLabeling G K) :=
-  Pi.unique
+  inferInstanceAs <| Unique (G.edgeSet → K)
 
 /--
 An edge labeling of the complete graph on `V` with labels in type `K`.

Mathlib/Combinatorics/SimpleGraph/Walks/Counting.lean

@@ -125,7 +125,7 @@ instance fintypeSetWalkLength (u v : V) (n : ℕ) : Fintype {p : G.Walk u v | p.
     rw [← Finset.mem_coe, coe_finsetWalkLength_eq]
 
 instance fintypeSubtypeWalkLength (u v : V) (n : ℕ) : Fintype {p : G.Walk u v // p.length = n} :=
-  fintypeSetWalkLength G u v n
+  inferInstanceAs <| Fintype {p : G.Walk u v | p.length = n}
 
 theorem set_walk_length_toFinset_eq (n : ℕ) (u v : V) :
     {p : G.Walk u v | p.length = n}.toFinset = G.finsetWalkLength n u v := by
@@ -143,7 +143,7 @@ instance fintypeSetWalkLengthLT (u v : V) (n : ℕ) : Fintype {p : G.Walk u v |
     rw [← Finset.mem_coe, coe_finsetWalkLengthLT_eq]
 
 instance fintypeSubtypeWalkLengthLT (u v : V) (n : ℕ) : Fintype {p : G.Walk u v // p.length < n} :=
-  fintypeSetWalkLengthLT G u v n
+  inferInstanceAs <| Fintype {p : G.Walk u v | p.length < n}
 
 instance fintypeSetPathLength (u v : V) (n : ℕ) :
     Fintype {p : G.Walk u v | p.IsPath ∧ p.length = n} :=
@@ -152,7 +152,7 @@ instance fintypeSetPathLength (u v : V) (n : ℕ) :
 
 instance fintypeSubtypePathLength (u v : V) (n : ℕ) :
     Fintype {p : G.Walk u v // p.IsPath ∧ p.length = n} :=
-  fintypeSetPathLength G u v n
+  inferInstanceAs <| Fintype {p : G.Walk u v | p.IsPath ∧ p.length = n}
 
 instance fintypeSetPathLengthLT (u v : V) (n : ℕ) :
     Fintype {p : G.Walk u v | p.IsPath ∧ p.length < n} :=
@@ -161,7 +161,7 @@ instance fintypeSetPathLengthLT (u v : V) (n : ℕ) :
 
 instance fintypeSubtypePathLengthLT (u v : V) (n : ℕ) :
     Fintype {p : G.Walk u v // p.IsPath ∧ p.length < n} :=
-  fintypeSetPathLengthLT G u v n
+  inferInstanceAs <| Fintype {p : G.Walk u v | p.IsPath ∧ p.length < n}
 
 end LocallyFinite
 

Mathlib/Computability/Language.lean

@@ -64,14 +64,13 @@ variable {α β γ : Type*}
 /-- A language is a set of strings over an alphabet. -/
 def Language (α) :=
   Set (List α)
+deriving CompleteAtomicBooleanAlgebra
 
 namespace Language
 
 instance : Membership (List α) (Language α) := ⟨Set.Mem⟩
 instance : Singleton (List α) (Language α) := ⟨Set.singleton⟩
 instance : Insert (List α) (Language α) := ⟨Set.insert⟩
-instance instCompleteAtomicBooleanAlgebra : CompleteAtomicBooleanAlgebra (Language α) :=
-  Set.instCompleteAtomicBooleanAlgebra
 
 variable {l m : Language α} {a b x : List α}
 
@@ -409,8 +408,8 @@ lemma reverse_kstar (l : Language α) : l∗.reverse = l.reverse∗ := by
 lemma mem_inf {x : List α} {l m : Language α} : x ∈ l ⊓ m ↔ x ∈ l ∧ x ∈ m := by
   apply Set.mem_inter_iff
 
-lemma compl_compl (l : Language α) : lᶜᶜ = l := by
-  simp [compl]
+lemma compl_compl (l : Language α) : lᶜᶜ = l :=
+  _root_.compl_compl l
 
 end Language
 

Mathlib/Data/Fintype/Vector.lean

@@ -19,10 +19,10 @@ open List (Vector)
 variable {α : Type*}
 
 instance Vector.fintype [Fintype α] {n : ℕ} : Fintype (List.Vector α n) :=
-  Fintype.ofEquiv _ (Equiv.vectorEquivFin _ _).symm
+  fast_instance% Fintype.ofEquiv _ (Equiv.vectorEquivFin _ _).symm
 
 instance [DecidableEq α] [Fintype α] {n : ℕ} : Fintype (Sym.Sym' α n) :=
-  Quotient.fintype _
+  inferInstanceAs <| Fintype (Quotient _)
 
 instance [DecidableEq α] [Fintype α] {n : ℕ} : Fintype (Sym α n) :=
-  Fintype.ofEquiv _ Sym.symEquivSym'.symm
+  fast_instance% Fintype.ofEquiv _ Sym.symEquivSym'.symm

Mathlib/Data/Fintype/WithTopBot.lean

@@ -18,7 +18,7 @@ variable {α : Type*}
 
 @[to_dual]
 instance [Fintype α] : Fintype (WithTop α) :=
-  instFintypeOption
+  inferInstanceAs <| Fintype (Option α)
 
 @[to_dual]
 instance [Finite α] : Finite (WithTop α) :=

Mathlib/Data/Holor.lean

@@ -101,23 +101,30 @@ instance [Add α] : Add (Holor α ds) :=
 instance [Neg α] : Neg (Holor α ds) :=
   ⟨fun a t => -a t⟩
 
-instance [AddSemigroup α] : AddSemigroup (Holor α ds) := Pi.addSemigroup
+instance [AddSemigroup α] : AddSemigroup (Holor α ds) :=
+  inferInstanceAs <| AddSemigroup (HolorIndex ds → α)
 
-instance [AddCommSemigroup α] : AddCommSemigroup (Holor α ds) := Pi.addCommSemigroup
+instance [AddCommSemigroup α] : AddCommSemigroup (Holor α ds) :=
+  inferInstanceAs <| AddCommSemigroup (HolorIndex ds → α)
 
-instance [AddMonoid α] : AddMonoid (Holor α ds) := Pi.addMonoid
+instance [AddMonoid α] : AddMonoid (Holor α ds) :=
+  inferInstanceAs <| AddMonoid (HolorIndex ds → α)
 
-instance [AddCommMonoid α] : AddCommMonoid (Holor α ds) := Pi.addCommMonoid
+instance [AddCommMonoid α] : AddCommMonoid (Holor α ds) :=
+  inferInstanceAs <| AddCommMonoid (HolorIndex ds → α)
 
-instance [AddGroup α] : AddGroup (Holor α ds) := Pi.addGroup
+instance [AddGroup α] : AddGroup (Holor α ds) :=
+  inferInstanceAs <| AddGroup (HolorIndex ds → α)
 
-instance [AddCommGroup α] : AddCommGroup (Holor α ds) := Pi.addCommGroup
+instance [AddCommGroup α] : AddCommGroup (Holor α ds) :=
+  inferInstanceAs <| AddCommGroup (HolorIndex ds → α)
 
 -- scalar product
 instance [Mul α] : SMul α (Holor α ds) :=
   ⟨fun a x => fun t => a * x t⟩
 
-instance [Semiring α] : Module α (Holor α ds) := Pi.module _ _ _
+instance [Semiring α] : Module α (Holor α ds) :=
+  inferInstanceAs <| Module α (HolorIndex ds → α)
 
 /-- The tensor product of two holors. -/
 def mul [Mul α] (x : Holor α ds₁) (y : Holor α ds₂) : Holor α (ds₁ ++ ds₂) := fun t =>

Mathlib/Data/PNat/Interval.lean

@@ -24,7 +24,8 @@ namespace PNat
 
 variable (a b : ℕ+)
 
-instance instLocallyFiniteOrder : LocallyFiniteOrder ℕ+ := Subtype.instLocallyFiniteOrder _
+instance instLocallyFiniteOrder : LocallyFiniteOrder ℕ+ :=
+  inferInstanceAs <| LocallyFiniteOrder (Subtype _)
 
 theorem Icc_eq_finset_subtype : Icc a b = (Icc (a : ℕ) b).subtype fun n : ℕ => 0 < n :=
   rfl

Mathlib/Data/Prod/Lex.lean

@@ -10,6 +10,7 @@ public import Mathlib.Order.BoundedOrder.Basic
 public import Mathlib.Order.Lattice
 public import Mathlib.Order.Lex
 public import Mathlib.Tactic.Tauto
+public import Mathlib.Tactic.FastInstance
 
 /-!
 # Lexicographic order
@@ -146,7 +147,7 @@ instance instPartialOrder (α β : Type*) [PartialOrder α] [PartialOrder β] :
     PartialOrder (α ×ₗ β) where
   le_antisymm _ _ := antisymm_of (Prod.Lex _ _)
 
-instance instOrdLexProd [Ord α] [Ord β] : Ord (α ×ₗ β) := lexOrd
+instance instOrdLexProd [Ord α] [Ord β] : Ord (α ×ₗ β) := fast_instance% lexOrd
 
 theorem compare_def [Ord α] [Ord β] : @compare (α ×ₗ β) _ =
     compareLex (compareOn fun x => (ofLex x).1) (compareOn fun x => (ofLex x).2) := rfl