From dbbfd1a2fec68eed5c53d434daf39f9442de4bad Mon Sep 17 00:00:00 2001
From: Kevin Buzzard <k.buzzard@imperial.ac.uk>
Date: Sun, 24 May 2026 14:34:52 +0100
Subject: [PATCH] perf: add some fast_instance%

---
 Mathlib/Algebra/Group/Pi/Basic.lean       | 7 ++++---
 Mathlib/Algebra/Group/TypeTags/Basic.lean | 3 ++-
 2 files changed, 6 insertions(+), 4 deletions(-)

diff --git a/Mathlib/Algebra/Group/Pi/Basic.lean b/Mathlib/Algebra/Group/Pi/Basic.lean
index ba7f7d9d87f6f1..385970fed5071d 100644
--- a/Mathlib/Algebra/Group/Pi/Basic.lean
+++ b/Mathlib/Algebra/Group/Pi/Basic.lean
@@ -10,6 +10,7 @@ public import Mathlib.Algebra.Notation.Pi.Basic
 public import Mathlib.Data.Sum.Basic
 public import Mathlib.Logic.Unique
 public import Mathlib.Tactic.Spread
+import Mathlib.Tactic.FastInstance
 
 /-!
 # Instances and theorems on pi types
@@ -61,15 +62,15 @@ instance invOneClass [∀ i, InvOneClass (f i)] : InvOneClass (∀ i, f i) where
   inv_one := by ext; exact inv_one
 
 @[to_additive]
-instance monoid [∀ i, Monoid (f i)] : Monoid (∀ i, f i) where
+instance monoid [∀ i, Monoid (f i)] : Monoid (∀ i, f i) := fast_instance% {
   __ := semigroup
   __ := mulOneClass
   npow := fun n x i => x i ^ n
   npow_zero := by intros; ext; exact Monoid.npow_zero _
-  npow_succ := by intros; ext; exact Monoid.npow_succ _ _
+  npow_succ := by intros; ext; exact Monoid.npow_succ _ _ }
 
 @[to_additive]
-instance commMonoid [∀ i, CommMonoid (f i)] : CommMonoid (∀ i, f i) :=
+instance commMonoid [∀ i, CommMonoid (f i)] : CommMonoid (∀ i, f i) := fast_instance%
   { monoid, commSemigroup with }
 
 @[to_additive Pi.subNegMonoid]
diff --git a/Mathlib/Algebra/Group/TypeTags/Basic.lean b/Mathlib/Algebra/Group/TypeTags/Basic.lean
index 07c87018aaf344..a1b759021d8e40 100644
--- a/Mathlib/Algebra/Group/TypeTags/Basic.lean
+++ b/Mathlib/Algebra/Group/TypeTags/Basic.lean
@@ -10,6 +10,7 @@ public import Mathlib.Algebra.Notation.Pi.Basic
 public import Mathlib.Data.FunLike.Basic
 public import Mathlib.Logic.Function.Iterate
 public import Mathlib.Logic.Equiv.Defs
+import Mathlib.Tactic.FastInstance
 
 /-!
 # Type tags that turn additive structures into multiplicative, and vice versa
@@ -267,7 +268,7 @@ instance Additive.addMonoid [h : Monoid α] : AddMonoid (Additive α) :=
     nsmul_zero := @Monoid.npow_zero α h
     nsmul_succ := @Monoid.npow_succ α h }
 
-instance Multiplicative.monoid [h : AddMonoid α] : Monoid (Multiplicative α) :=
+instance Multiplicative.monoid [h : AddMonoid α] : Monoid (Multiplicative α) := fast_instance%
   { Multiplicative.mulOneClass, Multiplicative.semigroup with
     npow := @AddMonoid.nsmul α h
     npow_zero := @AddMonoid.nsmul_zero α h