chore: test fast_instance% everywhere

Mathlib/Algebra/AddConstMap/Basic.lean

@@ -378,7 +378,7 @@ theorem coe_vadd {K : Type*} [VAdd K H] [VAddAssocClass K H H] (c : K) (f : G 
 
 instance {K : Type*} [AddMonoid K] [AddAction K H] [VAddAssocClass K H H] :
     AddAction K (G →+c[a, b] H) :=
-  DFunLike.coe_injective.addAction _ coe_vadd
+  fast_instance% DFunLike.coe_injective.addAction _ coe_vadd
 
 /-!
 ### Monoid structure on endomorphisms `G →+c[a, a] G`
@@ -391,7 +391,8 @@ instance : Pow (G →+c[a, a] G) ℕ where
   pow f n := ⟨f^[n], Commute.iterate_left (AddConstMapClass.semiconj f) _⟩
 
 instance : Monoid (G →+c[a, a] G) :=
-  DFunLike.coe_injective.monoid (M₂ := Function.End G) _ rfl (fun _ _ ↦ rfl) fun _ _ ↦ rfl
+  fast_instance% DFunLike.coe_injective.monoid (M₂ := Function.End G) _ rfl (fun _ _ ↦ rfl)
+    fun _ _ ↦ rfl
 
 theorem mul_def (f g : G →+c[a, a] G) : f * g = f.comp g := rfl
 @[simp, push_cast] theorem coe_mul (f g : G →+c[a, a] G) : ⇑(f * g) = f ∘ g := rfl

Mathlib/Algebra/Algebra/RestrictScalars.lean

@@ -138,7 +138,7 @@ The preferred way of setting this up is
 `[Module Rᵐᵒᵖ M] [Module Sᵐᵒᵖ M] [IsScalarTower Rᵐᵒᵖ Sᵐᵒᵖ M]`.
 -/
 instance RestrictScalars.opModule [Module Sᵐᵒᵖ M] : Module Rᵐᵒᵖ (RestrictScalars R S M) :=
-  letI : Module Sᵐᵒᵖ (RestrictScalars R S M) := ‹Module Sᵐᵒᵖ M›
+  fast_instance% letI : Module Sᵐᵒᵖ (RestrictScalars R S M) := ‹Module Sᵐᵒᵖ M›
   Module.compHom M (RingHom.op <| algebraMap R S)
 
 instance RestrictScalars.isCentralScalar [Module S M] [Module Sᵐᵒᵖ M] [IsCentralScalar S M] :

Mathlib/Algebra/Category/CoalgCat/Monoidal.lean

@@ -61,6 +61,6 @@ noncomputable def MonoidalCategory.inducingFunctorData :
   rightUnitor_eq X := ModuleCat.hom_ext <| TensorProduct.ext <| by ext; rfl
 
 noncomputable instance instMonoidalCategory : MonoidalCategory (CoalgCat R) :=
-  Monoidal.induced (forget₂ _ (ModuleCat R)) (MonoidalCategory.inducingFunctorData R)
+  fast_instance% Monoidal.induced (forget₂ _ (ModuleCat R)) (MonoidalCategory.inducingFunctorData R)
 
 end CoalgCat

Mathlib/Algebra/Category/Grp/Preadditive.lean

@@ -57,7 +57,7 @@ instance : SMul ℤ (M ⟶ N) where
 @[simp] lemma hom_zsmul (n : ℤ) (f : M ⟶ N) : (n • f).hom = n • f.hom := rfl
 
 instance (P Q : AddCommGrpCat) : AddCommGroup (P ⟶ Q) :=
-  Function.Injective.addCommGroup (Hom.hom) ConcreteCategory.hom_injective
+  fast_instance% Function.Injective.addCommGroup (Hom.hom) ConcreteCategory.hom_injective
     rfl (fun _ _ => rfl) (fun _ => rfl) (fun _ _ => rfl) (fun _ _ => rfl) (fun _ _ => rfl)
 
 instance : Preadditive AddCommGrpCat where

Mathlib/Algebra/Category/ModuleCat/Basic.lean

@@ -355,7 +355,7 @@ instance : SMul ℤ (M ⟶ N) where
 @[simp] lemma hom_zsmul (n : ℤ) (f : M ⟶ N) : (n • f).hom = n • f.hom := rfl
 
 instance : AddCommGroup (M ⟶ N) :=
-  Function.Injective.addCommGroup (Hom.hom) hom_injective
+  fast_instance% Function.Injective.addCommGroup (Hom.hom) hom_injective
     rfl (fun _ _ => rfl) (fun _ => rfl) (fun _ _ => rfl) (fun _ _ => rfl) (fun _ _ => rfl)
 
 @[simp] lemma hom_sum {ι : Type*} (f : ι → (M ⟶ N)) (s : Finset ι) :
@@ -416,7 +416,7 @@ section Module
 variable {M N : ModuleCat.{v} R} {S : Type*} [Semiring S] [Module S N] [SMulCommClass R S N]
 
 instance Hom.instModule : Module S (M ⟶ N) :=
-  Function.Injective.module S
+  fast_instance% Function.Injective.module S
     { toFun := Hom.hom, map_zero' := hom_zero, map_add' := hom_add }
     hom_injective
     (fun _ _ => rfl)

Mathlib/Algebra/Category/ModuleCat/Monoidal/Basic.lean

@@ -308,7 +308,7 @@ instance MonoidalCategory.instMonoidalCategoryStruct :
   rightUnitor M := (TensorProduct.rid R M).toModuleIso
 
 instance monoidalCategory : MonoidalCategory (ModuleCat.{u} R) :=
-  Monoidal.induced equivalenceSemimoduleCat.functor
+  fast_instance% Monoidal.induced equivalenceSemimoduleCat.functor
   { μIso _ _ := .refl _
     εIso := .refl _
     associator_eq _ _ _ := by ext1; exact TensorProduct.ext (TensorProduct.ext rfl)

Mathlib/Algebra/Category/ModuleCat/Monoidal/Symmetric.lean

@@ -111,8 +111,23 @@ namespace ModuleCat.MonoidalCategory
 
 variable {R : Type u} [CommRing R]
 
+/-- The monoidal structure on the equivalence between `ModuleCat` and `SemimoduleCat`. -/
+local instance instMonoidalSemimoduleCatFunctorEquivalenceSemimoduleCat :
+    equivalenceSemimoduleCat (R := R).functor.Monoidal :=
+  CategoryTheory.Monoidal.fromInducedMonoidal equivalenceSemimoduleCat.functor
+  { μIso _ _ := .refl _
+    εIso := .refl _
+    associator_eq _ _ _ := by ext1; exact TensorProduct.ext (TensorProduct.ext rfl)
+    leftUnitor_eq _ := by ext1; exact TensorProduct.ext rfl
+    rightUnitor_eq _ := by ext1; exact TensorProduct.ext rfl }
+
 instance : BraidedCategory (ModuleCat.{u} R) :=
   .ofFaithful equivalenceSemimoduleCat.functor (fun M N ↦ (TensorProduct.comm R M N).toModuleIso)
+    (fun M N ↦ by
+      ext : 1
+      apply TensorProduct.ext'
+      intro m n
+      rfl)
 
 instance : equivalenceSemimoduleCat (R := R).functor.Braided where
 
@@ -129,14 +144,18 @@ theorem braiding_inv_apply {M N : ModuleCat.{u} R} (m : M) (n : N) :
     ((β_ M N).inv : N ⊗ M ⟶ M ⊗ N) (n ⊗ₜ m) = m ⊗ₜ n :=
   rfl
 
+set_option backward.isDefEq.respectTransparency false in
 theorem tensorμ_eq_tensorTensorTensorComm {A B C D : ModuleCat R} :
     tensorμ A B C D = ofHom (TensorProduct.tensorTensorTensorComm R A B C D).toLinearMap :=
-  ModuleCat.hom_ext <| TensorProduct.ext <| TensorProduct.ext <| LinearMap.ext₂ fun _ _ =>
-    TensorProduct.ext <| LinearMap.ext₂ fun _ _ => rfl
+  ModuleCat.hom_ext <| TensorProduct.ext <| TensorProduct.ext <| LinearMap.ext₂ fun a b =>
+    TensorProduct.ext <| LinearMap.ext₂ fun c d => by
+      rfl
 
 @[simp]
 theorem tensorμ_apply
     {A B C D : ModuleCat R} (x : A) (y : B) (z : C) (w : D) :
-    tensorμ A B C D ((x ⊗ₜ y) ⊗ₜ (z ⊗ₜ w)) = (x ⊗ₜ z) ⊗ₜ (y ⊗ₜ w) := rfl
+    tensorμ A B C D ((x ⊗ₜ y) ⊗ₜ (z ⊗ₜ w)) = (x ⊗ₜ z) ⊗ₜ (y ⊗ₜ w) := by
+  rw [tensorμ_eq_tensorTensorTensorComm]
+  rfl
 
 end ModuleCat.MonoidalCategory

Mathlib/Algebra/Category/ModuleCat/Semi.lean

@@ -305,7 +305,8 @@ instance : SMul ℕ (M ⟶ N) where
 alias hom_zsmul := hom_nsmul
 
 instance : AddCommMonoid (M ⟶ N) :=
-  Function.Injective.addCommMonoid Hom.hom hom_injective rfl (fun _ _ => rfl) (fun _ _ => rfl)
+  fast_instance% Function.Injective.addCommMonoid Hom.hom hom_injective rfl (fun _ _ => rfl)
+    (fun _ _ => rfl)
 
 @[simp] lemma hom_sum {ι : Type*} (f : ι → (M ⟶ N)) (s : Finset ι) :
     (∑ i ∈ s, f i).hom = ∑ i ∈ s, (f i).hom :=
@@ -356,7 +357,7 @@ section Module
 variable {M N : SemimoduleCat.{v} R} {S : Type*} [Semiring S] [Module S N] [SMulCommClass R S N]
 
 instance Hom.instModule : Module S (M ⟶ N) :=
-  Function.Injective.module S
+  fast_instance% Function.Injective.module S
     { toFun := Hom.hom, map_zero' := hom_zero, map_add' := hom_add }
     hom_injective
     (fun _ _ => rfl)

Mathlib/Algebra/DirectSum/Ring.lean

@@ -383,8 +383,8 @@ theorem of_zero_mul (a b : A 0) : of _ 0 (a * b) = of _ 0 a * of _ 0 b :=
   of_zero_smul A a b
 
 instance (priority := 900) GradeZero.nonUnitalNonAssocSemiring : NonUnitalNonAssocSemiring (A 0) :=
-  Function.Injective.nonUnitalNonAssocSemiring (of A 0) DFinsupp.single_injective (of A 0).map_zero
-    (of A 0).map_add (of_zero_mul A) (map_nsmul _)
+  fast_instance% Function.Injective.nonUnitalNonAssocSemiring (of A 0) DFinsupp.single_injective
+    (of A 0).map_zero (of A 0).map_add (of_zero_mul A) (map_nsmul _)
 
 instance GradeZero.smulWithZero (i : ι) : SMulWithZero (A 0) (A i) := by
   letI := SMulWithZero.compHom (⨁ i, A i) (of A 0).toZeroHom
@@ -419,8 +419,8 @@ theorem of_zero_ofNat (n : ℕ) [n.AtLeastTwo] : of A 0 ofNat(n) = ofNat(n) :=
 
 /-- The `Semiring` structure derived from `GSemiring A`. -/
 instance (priority := 900) GradeZero.semiring : Semiring (A 0) :=
-  Function.Injective.semiring (of A 0) DFinsupp.single_injective (of A 0).map_zero (of_zero_one A)
-    (of A 0).map_add (of_zero_mul A) (fun _ _ ↦ (of A 0).map_nsmul _ _)
+  fast_instance% Function.Injective.semiring (of A 0) DFinsupp.single_injective (of A 0).map_zero
+    (of_zero_one A) (of A 0).map_add (of_zero_mul A) (fun _ _ ↦ (of A 0).map_nsmul _ _)
     (fun _ _ => of_zero_pow _ _ _) (of_natCast A)
 
 /-- `of A 0` is a `RingHom`, using the `DirectSum.GradeZero.semiring` structure. -/
@@ -433,7 +433,7 @@ def ofZeroRingHom : A 0 →+* ⨁ i, A i :=
 in an overall `Module (A 0) (⨁ i, A i)` structure via `DirectSum.module`.
 -/
 instance GradeZero.module {i} : Module (A 0) (A i) :=
-  letI := Module.compHom (⨁ i, A i) (ofZeroRingHom A)
+  fast_instance% letI := Module.compHom (⨁ i, A i) (ofZeroRingHom A)
   DFinsupp.single_injective.module (A 0) (of A i) fun a => of_zero_smul A a
 
 end Semiring
@@ -444,8 +444,8 @@ variable [∀ i, AddCommMonoid (A i)] [AddCommMonoid ι] [GCommSemiring A]
 
 /-- The `CommSemiring` structure derived from `GCommSemiring A`. -/
 instance (priority := 900) GradeZero.commSemiring : CommSemiring (A 0) :=
-  Function.Injective.commSemiring (of A 0) DFinsupp.single_injective (of A 0).map_zero
-    (of_zero_one A) (of A 0).map_add (of_zero_mul A) (fun _ _ ↦ map_nsmul _ _ _)
+  fast_instance% Function.Injective.commSemiring (of A 0) DFinsupp.single_injective
+    (of A 0).map_zero (of_zero_one A) (of A 0).map_add (of_zero_mul A) (fun _ _ ↦ map_nsmul _ _ _)
     (fun _ _ => of_zero_pow _ _ _) (of_natCast A)
 
 end CommSemiring
@@ -456,8 +456,9 @@ variable [∀ i, AddCommGroup (A i)] [AddZeroClass ι] [GNonUnitalNonAssocSemiri
 
 /-- The `NonUnitalNonAssocRing` derived from `GNonUnitalNonAssocSemiring A`. -/
 instance (priority := 900) GradeZero.nonUnitalNonAssocRing : NonUnitalNonAssocRing (A 0) :=
-  Function.Injective.nonUnitalNonAssocRing (of A 0) DFinsupp.single_injective (of A 0).map_zero
-    (of A 0).map_add (of_zero_mul A) (of A 0).map_neg (of A 0).map_sub (fun _ _ ↦ map_nsmul _ _ _)
+  fast_instance% Function.Injective.nonUnitalNonAssocRing (of A 0) DFinsupp.single_injective
+    (of A 0).map_zero (of A 0).map_add (of_zero_mul A) (of A 0).map_neg (of A 0).map_sub
+    (fun _ _ ↦ map_nsmul _ _ _)
     (fun _ _ ↦ map_zsmul _ _ _)
 
 end Ring
@@ -475,9 +476,10 @@ theorem of_intCast (n : ℤ) : of A 0 n = n := by
 
 /-- The `Ring` derived from `GSemiring A`. -/
 instance (priority := 900) GradeZero.ring : Ring (A 0) :=
-  Function.Injective.ring (of A 0) DFinsupp.single_injective (of A 0).map_zero (of_zero_one A)
-    (of A 0).map_add (of_zero_mul A) (of A 0).map_neg (of A 0).map_sub (fun _ _ ↦ map_nsmul _ _ _)
-    (fun _ _ ↦ map_zsmul _ _ _) (fun _ _ => of_zero_pow _ _ _) (of_natCast A) (of_intCast A)
+  fast_instance% Function.Injective.ring (of A 0) DFinsupp.single_injective (of A 0).map_zero
+    (of_zero_one A) (of A 0).map_add (of_zero_mul A) (of A 0).map_neg (of A 0).map_sub
+    (fun _ _ ↦ map_nsmul _ _ _) (fun _ _ ↦ map_zsmul _ _ _) (fun _ _ => of_zero_pow _ _ _)
+    (of_natCast A) (of_intCast A)
 
 end Ring
 
@@ -487,9 +489,10 @@ variable [∀ i, AddCommGroup (A i)] [AddCommMonoid ι] [GCommRing A]
 
 /-- The `CommRing` derived from `GCommSemiring A`. -/
 instance (priority := 900) GradeZero.commRing : CommRing (A 0) :=
-  Function.Injective.commRing (of A 0) DFinsupp.single_injective (of A 0).map_zero (of_zero_one A)
-    (of A 0).map_add (of_zero_mul A) (of A 0).map_neg (of A 0).map_sub (fun _ _ ↦ map_nsmul _ _ _)
-    (fun _ _ ↦ map_zsmul _ _ _) (fun _ _ => of_zero_pow _ _ _) (of_natCast A) (of_intCast A)
+  fast_instance% Function.Injective.commRing (of A 0) DFinsupp.single_injective (of A 0).map_zero
+    (of_zero_one A) (of A 0).map_add (of_zero_mul A) (of A 0).map_neg (of A 0).map_sub
+    (fun _ _ ↦ map_nsmul _ _ _) (fun _ _ ↦ map_zsmul _ _ _) (fun _ _ => of_zero_pow _ _ _)
+    (of_natCast A) (of_intCast A)
 
 end CommRing
 

Mathlib/Algebra/GradedMonoid.lean

@@ -327,7 +327,7 @@ theorem mk_zero_pow (a : A 0) (n : ℕ) : mk _ (a ^ n) = mk _ a ^ n :=
 
 /-- The `Monoid` structure derived from `GMonoid A`. -/
 instance (priority := 900) GradeZero.monoid : Monoid (A 0) :=
-  Function.Injective.monoid (mk 0) sigma_mk_injective rfl mk_zero_smul mk_zero_pow
+  fast_instance% Function.Injective.monoid (mk 0) sigma_mk_injective rfl mk_zero_smul mk_zero_pow
 
 end Monoid
 
@@ -337,7 +337,8 @@ variable [AddCommMonoid ι] [GCommMonoid A]
 
 /-- The `CommMonoid` structure derived from `GCommMonoid A`. -/
 instance (priority := 900) GradeZero.commMonoid : CommMonoid (A 0) :=
-  Function.Injective.commMonoid (mk 0) sigma_mk_injective rfl mk_zero_smul mk_zero_pow
+  fast_instance% Function.Injective.commMonoid (mk 0) sigma_mk_injective rfl mk_zero_smul
+    mk_zero_pow
 
 end Monoid
 
@@ -354,7 +355,7 @@ def mkZeroMonoidHom : A 0 →* GradedMonoid A where
 
 /-- Each grade `A i` derives an `A 0`-action structure from `GMonoid A`. -/
 instance GradeZero.mulAction {i} : MulAction (A 0) (A i) :=
-  letI := MulAction.compHom (GradedMonoid A) (mkZeroMonoidHom A)
+  fast_instance% letI := MulAction.compHom (GradedMonoid A) (mkZeroMonoidHom A)
   Function.Injective.mulAction (mk i) sigma_mk_injective mk_zero_smul
 
 end MulAction

Mathlib/Algebra/Group/TypeTags/Finite.lean

@@ -32,10 +32,10 @@ instance [h : Infinite α] : Infinite (Additive α) := h
 instance [h : Infinite α] : Infinite (Multiplicative α) := h
 
 instance Additive.fintype : ∀ [Fintype α], Fintype (Additive α) :=
-  Fintype.ofEquiv α Additive.ofMul
+  fast_instance% Fintype.ofEquiv α Additive.ofMul
 
 instance Multiplicative.fintype : ∀ [Fintype α], Fintype (Multiplicative α) :=
-  Fintype.ofEquiv α Multiplicative.ofAdd
+  fast_instance% Fintype.ofEquiv α Multiplicative.ofAdd
 
 @[simp] lemma Fintype.card_multiplicative (α : Type*) [Fintype α] :
     card (Multiplicative α) = card α := Finset.card_map _

Mathlib/Algebra/Group/ULift.lean

@@ -7,6 +7,7 @@ module
 
 public import Mathlib.Algebra.Group.Equiv.Defs
 public import Mathlib.Algebra.Group.InjSurj
+public import Mathlib.Tactic.FastInstance
 
 /-!
 # `ULift` instances for groups and monoids
@@ -80,58 +81,58 @@ instance semigroup [Semigroup α] : Semigroup (ULift α) :=
 
 @[to_additive]
 instance commSemigroup [CommSemigroup α] : CommSemigroup (ULift α) :=
-  (Equiv.ulift.injective.commSemigroup _) fun _ _ => rfl
+  fast_instance% (Equiv.ulift.injective.commSemigroup _) fun _ _ => rfl
 
 @[to_additive]
 instance mulOneClass [MulOneClass α] : MulOneClass (ULift α) :=
-  Equiv.ulift.injective.mulOneClass _ rfl (by intros; rfl)
+  fast_instance% Equiv.ulift.injective.mulOneClass _ rfl (by intros; rfl)
 
 @[to_additive]
 instance monoid [Monoid α] : Monoid (ULift α) :=
-  Equiv.ulift.injective.monoid _ rfl (fun _ _ => rfl) fun _ _ => rfl
+  fast_instance% Equiv.ulift.injective.monoid _ rfl (fun _ _ => rfl) fun _ _ => rfl
 
 @[to_additive]
 instance commMonoid [CommMonoid α] : CommMonoid (ULift α) :=
-  Equiv.ulift.injective.commMonoid _ rfl (fun _ _ => rfl) fun _ _ => rfl
+  fast_instance% Equiv.ulift.injective.commMonoid _ rfl (fun _ _ => rfl) fun _ _ => rfl
 
 @[to_additive]
 instance divInvMonoid [DivInvMonoid α] : DivInvMonoid (ULift α) :=
-  Equiv.ulift.injective.divInvMonoid _ rfl (fun _ _ => rfl) (fun _ => rfl) (fun _ _ => rfl)
-    (fun _ _ => rfl) fun _ _ => rfl
+  fast_instance% Equiv.ulift.injective.divInvMonoid _ rfl (fun _ _ => rfl) (fun _ => rfl)
+    (fun _ _ => rfl) (fun _ _ => rfl) fun _ _ => rfl
 
 @[to_additive]
 instance group [Group α] : Group (ULift α) :=
-  Equiv.ulift.injective.group _ rfl (fun _ _ => rfl) (fun _ => rfl) (fun _ _ => rfl)
+  fast_instance% Equiv.ulift.injective.group _ rfl (fun _ _ => rfl) (fun _ => rfl) (fun _ _ => rfl)
     (fun _ _ => rfl) fun _ _ => rfl
 
 @[to_additive]
 instance commGroup [CommGroup α] : CommGroup (ULift α) :=
-  Equiv.ulift.injective.commGroup _ rfl (fun _ _ => rfl) (fun _ => rfl) (fun _ _ => rfl)
-    (fun _ _ => rfl) fun _ _ => rfl
+  fast_instance% Equiv.ulift.injective.commGroup _ rfl (fun _ _ => rfl) (fun _ => rfl)
+    (fun _ _ => rfl) (fun _ _ => rfl) fun _ _ => rfl
 
 @[to_additive]
 instance leftCancelSemigroup [LeftCancelSemigroup α] : LeftCancelSemigroup (ULift α) :=
-  Equiv.ulift.injective.leftCancelSemigroup _ fun _ _ => rfl
+  fast_instance% Equiv.ulift.injective.leftCancelSemigroup _ fun _ _ => rfl
 
 @[to_additive]
 instance rightCancelSemigroup [RightCancelSemigroup α] : RightCancelSemigroup (ULift α) :=
-  Equiv.ulift.injective.rightCancelSemigroup _ fun _ _ => rfl
+  fast_instance% Equiv.ulift.injective.rightCancelSemigroup _ fun _ _ => rfl
 
 @[to_additive]
 instance leftCancelMonoid [LeftCancelMonoid α] : LeftCancelMonoid (ULift α) :=
-  Equiv.ulift.injective.leftCancelMonoid _ rfl (fun _ _ => rfl) fun _ _ => rfl
+  fast_instance% Equiv.ulift.injective.leftCancelMonoid _ rfl (fun _ _ => rfl) fun _ _ => rfl
 
 @[to_additive]
 instance rightCancelMonoid [RightCancelMonoid α] : RightCancelMonoid (ULift α) :=
-  Equiv.ulift.injective.rightCancelMonoid _ rfl (fun _ _ => rfl) fun _ _ => rfl
+  fast_instance% Equiv.ulift.injective.rightCancelMonoid _ rfl (fun _ _ => rfl) fun _ _ => rfl
 
 @[to_additive]
 instance cancelMonoid [CancelMonoid α] : CancelMonoid (ULift α) :=
-  Equiv.ulift.injective.cancelMonoid _ rfl (fun _ _ => rfl) fun _ _ => rfl
+  fast_instance% Equiv.ulift.injective.cancelMonoid _ rfl (fun _ _ => rfl) fun _ _ => rfl
 
 @[to_additive]
 instance cancelCommMonoid [CancelCommMonoid α] : CancelCommMonoid (ULift α) :=
-  Equiv.ulift.injective.cancelCommMonoid _ rfl (fun _ _ => rfl) fun _ _ => rfl
+  fast_instance% Equiv.ulift.injective.cancelCommMonoid _ rfl (fun _ _ => rfl) fun _ _ => rfl
 
 instance nontrivial [Nontrivial α] : Nontrivial (ULift α) :=
   Equiv.ulift.symm.injective.nontrivial

Mathlib/Algebra/GroupWithZero/ULift.lean

@@ -7,6 +7,7 @@ module
 
 public import Mathlib.Algebra.Group.ULift
 public import Mathlib.Algebra.GroupWithZero.InjSurj
+public import Mathlib.Tactic.FastInstance
 
 /-!
 # `ULift` instances for groups and monoids with zero
@@ -27,20 +28,20 @@ variable {α : Type u}
 namespace ULift
 
 instance mulZeroOneClass [MulZeroOneClass α] : MulZeroOneClass (ULift α) :=
-  Equiv.ulift.injective.mulZeroOneClass _ rfl rfl (by intros; rfl)
+  fast_instance% Equiv.ulift.injective.mulZeroOneClass _ rfl rfl (by intros; rfl)
 
 instance monoidWithZero [MonoidWithZero α] : MonoidWithZero (ULift α) :=
-  Equiv.ulift.injective.monoidWithZero _ rfl rfl (fun _ _ => rfl) fun _ _ => rfl
+  fast_instance% Equiv.ulift.injective.monoidWithZero _ rfl rfl (fun _ _ => rfl) fun _ _ => rfl
 
 instance commMonoidWithZero [CommMonoidWithZero α] : CommMonoidWithZero (ULift α) :=
-  Equiv.ulift.injective.commMonoidWithZero _ rfl rfl (fun _ _ => rfl) fun _ _ => rfl
+  fast_instance% Equiv.ulift.injective.commMonoidWithZero _ rfl rfl (fun _ _ => rfl) fun _ _ => rfl
 
 instance groupWithZero [GroupWithZero α] : GroupWithZero (ULift α) :=
-  Equiv.ulift.injective.groupWithZero _ rfl rfl (fun _ _ => rfl) (fun _ => rfl) (fun _ _ => rfl)
-    (fun _ _ => rfl) fun _ _ => rfl
+  fast_instance% Equiv.ulift.injective.groupWithZero _ rfl rfl (fun _ _ => rfl) (fun _ => rfl)
+    (fun _ _ => rfl) (fun _ _ => rfl) fun _ _ => rfl
 
 instance commGroupWithZero [CommGroupWithZero α] : CommGroupWithZero (ULift α) :=
-  Equiv.ulift.injective.commGroupWithZero _ rfl rfl (fun _ _ => rfl) (fun _ => rfl) (fun _ _ => rfl)
-    (fun _ _ => rfl) fun _ _ => rfl
+  fast_instance% Equiv.ulift.injective.commGroupWithZero _ rfl rfl (fun _ _ => rfl) (fun _ => rfl)
+    (fun _ _ => rfl) (fun _ _ => rfl) fun _ _ => rfl
 
 end ULift

Mathlib/Algebra/Homology/Additive.lean

@@ -80,7 +80,7 @@ theorem zsmul_f_apply (n : ℤ) (f : C ⟶ D) (i : ι) : (n • f).f i = n • f
   rfl
 
 instance : AddCommGroup (C ⟶ D) :=
-  Function.Injective.addCommGroup Hom.f HomologicalComplex.hom_f_injective
+  fast_instance% Function.Injective.addCommGroup Hom.f HomologicalComplex.hom_f_injective
     (by cat_disch) (by cat_disch) (by cat_disch) (by cat_disch) (by cat_disch) (by cat_disch)
 
 instance : Preadditive (HomologicalComplex V c) where

Mathlib/Algebra/Homology/DerivedCategory/Ext/Linear.lean

@@ -37,7 +37,7 @@ variable {R : Type t} [Ring R] {C : Type u} [Category.{v} C] [Abelian C] [Linear
 variable {X Y : C} {n : ℕ}
 
 noncomputable instance : Module R (Ext X Y n) :=
-  letI := HasDerivedCategory.standard C
+  fast_instance% letI := HasDerivedCategory.standard C
   Equiv.module R homEquiv
 
 lemma smul_eq_comp_mk₀ (x : Ext X Y n) (r : R) :