diff --git a/src/Lean/Elab/Deriving/BEq.lean b/src/Lean/Elab/Deriving/BEq.lean
index cb8c62f19e08..77a9f9311e35 100644
--- a/src/Lean/Elab/Deriving/BEq.lean
+++ b/src/Lean/Elab/Deriving/BEq.lean
@@ -206,8 +206,8 @@ def mkMutualBlock (ctx : Context) : TermElabM Syntax := do
      $auxDefs:command*
     end)
 
-def mkBEqInstanceCmds (ctx : Context) (declName : Name) : TermElabM (Array Syntax) := do
-  let cmds := #[← mkMutualBlock ctx] ++ (← mkInstanceCmds ctx `BEq #[declName])
+def mkBEqInstanceCmds (ctx : Context) (declNames : Array Name) : TermElabM (Array Syntax) := do
+  let cmds := #[← mkMutualBlock ctx] ++ (← mkInstanceCmds ctx `BEq declNames)
   trace[Elab.Deriving.beq] "\n{cmds}"
   return cmds
 
@@ -222,22 +222,27 @@ def mkBEqEnumCmd (ctx : Context) (name : Name): TermElabM (Array Syntax) := do
 
 open Command
 
-def mkBEqInstance (declName : Name) : CommandElabM Unit := do
-  withoutExposeFromCtors declName do
+/-- Derives `BEq` for `declNames`, which must belong to the same mutual block. -/
+def mkBEqInstance (declNames : Array Name) : CommandElabM Unit := do
+  let declName := declNames[0]!
+  withoutExposeFromCtorsAll declNames do
     let ctx ← liftTermElabM <| mkContext ``BEq "beq" declName
     let cmds ← liftTermElabM <|
       if (← isEnumType declName) then
         mkBEqEnumCmd ctx declName
       else
-        mkBEqInstanceCmds ctx declName
+        mkBEqInstanceCmds ctx declNames
+    -- `mkInstName` picks names still free, so compute them before adding the instances.
+    let instNames ← liftTermElabM <| declNames.mapM (mkInstName ``BEq)
     cmds.forM elabCommand
     unless ctx.usePartial do
-      elabCommand (← `(attribute [method_specs] $(mkIdent ctx.instName):ident))
+      for instName in instNames do
+        elabCommand (← `(attribute [method_specs] $(mkIdent instName):ident))
 
 def mkBEqInstanceHandler (declNames : Array Name) : CommandElabM Bool := do
   if (← declNames.allM isInductive) then
-    for declName in declNames do
-      mkBEqInstance declName
+    for block in ← liftCoreM <| groupByMutualBlock declNames do
+      mkBEqInstance block
     return true
   else
     return false
diff --git a/src/Lean/Elab/Deriving/Hashable.lean b/src/Lean/Elab/Deriving/Hashable.lean
index 77932d73a9c8..40888be0e1d6 100644
--- a/src/Lean/Elab/Deriving/Hashable.lean
+++ b/src/Lean/Elab/Deriving/Hashable.lean
@@ -80,18 +80,19 @@ def mkHashFuncs (ctx : Context) : TermElabM Syntax := do
     auxDefs := auxDefs.push (← mkAuxFunction ctx i)
   `(mutual $auxDefs:command* end)
 
-private def mkHashableInstanceCmds (declName : Name) : TermElabM (Array Syntax) := do
-  let ctx ← mkContext ``Hashable "hash" declName
-  let cmds := #[← mkHashFuncs ctx] ++ (← mkInstanceCmds ctx `Hashable #[declName])
+/-- Builds one aux-function block for the mutual block of `declNames` and an instance for each. -/
+private def mkHashableInstanceCmds (declNames : Array Name) : TermElabM (Array Syntax) := do
+  let ctx ← mkContext ``Hashable "hash" declNames[0]!
+  let cmds := #[← mkHashFuncs ctx] ++ (← mkInstanceCmds ctx `Hashable declNames)
   trace[Elab.Deriving.hashable] "\n{cmds}"
   return cmds
 
 def mkHashableHandler (declNames : Array Name) : CommandElabM Bool := do
   withoutExporting do  -- This deriving handler handles visibility of generated decls syntactically
   if (← declNames.allM isInductive)  then
-    for declName in declNames do
-      withoutExposeFromCtors declName do
-        let cmds ← liftTermElabM <| mkHashableInstanceCmds declName
+    for block in ← liftCoreM <| groupByMutualBlock declNames do
+      withoutExposeFromCtorsAll block do
+        let cmds ← liftTermElabM <| mkHashableInstanceCmds block
         cmds.forM elabCommand
     return true
   else
diff --git a/src/Lean/Elab/Deriving/Repr.lean b/src/Lean/Elab/Deriving/Repr.lean
index f855cd9e404c..a31fb68acacb 100644
--- a/src/Lean/Elab/Deriving/Repr.lean
+++ b/src/Lean/Elab/Deriving/Repr.lean
@@ -112,9 +112,10 @@ def mkMutualBlock (ctx : Context) : TermElabM Syntax := do
      $auxDefs:command*
     end)
 
-private def mkReprInstanceCmd (declName : Name) : TermElabM (Array Syntax) := do
-  let ctx ← mkContext ``Repr "repr" declName
-  let cmds := #[← mkMutualBlock ctx] ++ (← mkInstanceCmds ctx `Repr #[declName])
+/-- Builds one aux-function block for the mutual block of `declNames` and an instance for each. -/
+private def mkReprInstanceCmds (declNames : Array Name) : TermElabM (Array Syntax) := do
+  let ctx ← mkContext ``Repr "repr" declNames[0]!
+  let cmds := #[← mkMutualBlock ctx] ++ (← mkInstanceCmds ctx `Repr declNames)
   trace[Elab.Deriving.repr] "\n{cmds}"
   return cmds
 
@@ -122,9 +123,9 @@ open Command
 
 def mkReprInstanceHandler (declNames : Array Name) : CommandElabM Bool := do
   if (← declNames.allM isInductive) then
-    for declName in declNames do
-      withoutExposeFromCtors declName do
-        let cmds ← liftTermElabM <| mkReprInstanceCmd declName
+    for block in ← liftCoreM <| groupByMutualBlock declNames do
+      withoutExposeFromCtorsAll block do
+        let cmds ← liftTermElabM <| mkReprInstanceCmds block
         cmds.forM elabCommand
     return true
   else
diff --git a/src/Lean/Elab/Deriving/Util.lean b/src/Lean/Elab/Deriving/Util.lean
index 3d3bf9c59892..a21e31d443d1 100644
--- a/src/Lean/Elab/Deriving/Util.lean
+++ b/src/Lean/Elab/Deriving/Util.lean
@@ -83,7 +83,15 @@ def withoutExposeFromCtors (typeName : Name) (cont : CommandElabM α) : CommandE
         attrs := sc.attrs.filter (!· matches `(Parser.Term.attrInstance| expose)) }) cont
   else cont
 
+/-- Runs `cont` under `withoutExposeFromCtors` for each of `typeNames`. -/
+def withoutExposeFromCtorsAll (typeNames : Array Name) (cont : CommandElabM α) : CommandElabM α :=
+  typeNames.foldr withoutExposeFromCtors cont
+
 structure Context where
+  /--
+  The instance name for the type passed to `mkContext`, which also prefixes `auxFunNames`.
+  `mkInstanceCmds` names each instance after its own type instead.
+  -/
   instName    : Name
   typeInfos   : Array InductiveVal
   auxFunNames : Array Name
@@ -158,10 +166,24 @@ def mkInstanceCmds (ctx : Context) (className : Name) (typeNames : Array Name) (
       let mut val      := mkIdent auxFunName
       if useAnonCtor then
         val ← `(⟨$val⟩)
-      let instCmd ← `(instance $(mkIdent ctx.instName):ident $binders:implicitBinder* : $type := $val)
+      let instName     ← mkInstName className indVal.name
+      let instCmd ← `(instance $(mkIdent instName):ident $binders:implicitBinder* : $type := $val)
       instances := instances.push instCmd
   return instances
 
+/-- Groups inductive type names by mutual block, keeping the given order. -/
+def groupByMutualBlock (declNames : Array Name) : CoreM (Array (Array Name)) := do
+  let mut blocks : Array (Array Name) := #[]
+  let mut idxOfBlock : NameMap Nat := {}
+  for declName in declNames do
+    let head := (← getConstInfoInduct declName).all.head!
+    if let some i := idxOfBlock.find? head then
+      blocks := blocks.modify i (·.push declName)
+    else
+      idxOfBlock := idxOfBlock.insert head blocks.size
+      blocks := blocks.push #[declName]
+  return blocks
+
 def mkDiscr (varName : Name) : TermElabM (TSyntax ``Parser.Term.matchDiscr) :=
  `(Parser.Term.matchDiscr| $(mkIdent varName):term)
 
diff --git a/tests/elab/derivingBEqMutualOnce.lean b/tests/elab/derivingBEqMutualOnce.lean
new file mode 100644
index 000000000000..592492b9baeb
--- /dev/null
+++ b/tests/elab/derivingBEqMutualOnce.lean
@@ -0,0 +1,81 @@
+/-!
+`deriving BEq` on a mutual block generates one block of auxiliary functions for the whole block
+instead of one per type, and still names each instance after its own type.
+-/
+
+/--
+trace: [Elab.Deriving.beq]
+    [mutual
+       set_option match.ignoreUnusedAlts✝ true
+       partial def instBEqA.beq_1 (x✝ : @A✝) (x✝¹ : @A✝) : Bool✝ :=
+         let localinst✝ : BEq✝ (@A✝) := ⟨instBEqA.beq_1⟩;
+         let localinst✝¹ : BEq✝ (@B✝) := ⟨instBEqA.beq_2⟩;
+         match x✝, x✝¹ with
+         | @A.a a✝, @A.a b✝ => a✝ == b✝
+         | @A.leaf, @A.leaf => true✝
+         | _, _ => false✝
+       partial def instBEqA.beq_2 (x✝² : @B✝) (x✝³ : @B✝) : Bool✝ :=
+         let localinst✝² : BEq✝ (@A✝) := ⟨instBEqA.beq_1⟩;
+         let localinst✝³ : BEq✝ (@B✝) := ⟨instBEqA.beq_2⟩;
+         match x✝², x✝³ with
+         | @B.b a✝¹, @B.b b✝¹ => a✝¹ == b✝¹
+         | @B.leaf, @B.leaf => true✝
+         | _, _ => false✝
+     end,
+     instance instBEqA : BEq✝ (@A✝) :=
+       ⟨instBEqA.beq_1⟩,
+     instance instBEqB : BEq✝ (@B✝) :=
+       ⟨instBEqA.beq_2⟩]
+-/
+#guard_msgs (whitespace := lax) in
+set_option trace.Elab.Deriving.beq true in
+mutual
+inductive A where
+  | a (b : B)
+  | leaf
+  deriving BEq
+inductive B where
+  | b (a : A)
+  | leaf
+  deriving BEq
+end
+
+#guard A.a (.b .leaf) == A.a (.b .leaf)
+#guard A.a (.b .leaf) != A.a .leaf
+#guard B.b (.a .leaf) == B.b (.a .leaf)
+#guard B.b (.a .leaf) != B.leaf
+
+example : BEq A := instBEqA
+example : BEq B := instBEqB
+
+/-! Types from different mutual blocks, and an enum, in one `deriving instance` command. -/
+
+mutual
+inductive C where
+  | c (d : D)
+  | leaf
+inductive D where
+  | d (c : C)
+  | leaf
+end
+
+inductive E where
+  | e (n : Nat)
+
+inductive F where
+  | x | y
+
+deriving instance BEq for C, E, F, D
+
+#guard C.c (.d .leaf) == C.c (.d .leaf)
+#guard C.c (.d .leaf) != C.leaf
+#guard D.d (.c .leaf) == D.d (.c .leaf)
+#guard E.e 3 == E.e 3
+#guard E.e 3 != E.e 4
+#guard F.x == F.x
+#guard F.x != F.y
+
+example : BEq C := instBEqC
+example : BEq D := instBEqD
+example : BEq E := instBEqE
+example : BEq F := instBEqF
diff --git a/tests/elab/derivingHashableMutualOnce.lean b/tests/elab/derivingHashableMutualOnce.lean
new file mode 100644
index 000000000000..e2c898295ddc
--- /dev/null
+++ b/tests/elab/derivingHashableMutualOnce.lean
@@ -0,0 +1,69 @@
+/-!
+`deriving Hashable` on a mutual block generates one block of auxiliary functions for the whole
+block instead of one per type, and still names each instance after its own type.
+-/
+
+/--
+trace: [Elab.Deriving.hashable]
+    [mutual
+       partial def instHashableA.hash_1 (x✝ : @A✝) : UInt64✝ :=
+         let localinst✝ : Hashable✝ (@A✝) := ⟨instHashableA.hash_1⟩;
+         let localinst✝¹ : Hashable✝ (@B✝) := ⟨instHashableA.hash_2⟩;
+         match x✝ with
+         | @A.a a✝ => mixHash✝ 0 (instHashableA.hash_2 a✝)
+         | @A.leaf => 1
+       partial def instHashableA.hash_2 (x✝¹ : @B✝) : UInt64✝ :=
+         let localinst✝² : Hashable✝ (@A✝) := ⟨instHashableA.hash_1⟩;
+         let localinst✝³ : Hashable✝ (@B✝) := ⟨instHashableA.hash_2⟩;
+         match x✝¹ with
+         | @B.b a✝¹ => mixHash✝ 0 (instHashableA.hash_1 a✝¹)
+         | @B.leaf => 1
+     end,
+     instance instHashableA : Hashable✝ (@A✝) :=
+       ⟨instHashableA.hash_1⟩,
+     instance instHashableB : Hashable✝ (@B✝) :=
+       ⟨instHashableA.hash_2⟩]
+-/
+#guard_msgs (whitespace := lax) in
+set_option trace.Elab.Deriving.hashable true in
+mutual
+inductive A where
+  | a (b : B)
+  | leaf
+  deriving Hashable
+inductive B where
+  | b (a : A)
+  | leaf
+  deriving Hashable
+end
+
+#guard hash (A.a (.b .leaf)) == hash (A.a (.b .leaf))
+#guard hash (A.a (.b .leaf)) != hash (A.a .leaf)
+#guard hash (B.b (.a .leaf)) != hash B.leaf
+
+example : Hashable A := instHashableA
+example : Hashable B := instHashableB
+
+/-! Types from different mutual blocks in one `deriving instance` command. -/
+
+mutual
+inductive C where
+  | c (d : D)
+  | leaf
+inductive D where
+  | d (c : C)
+  | leaf
+end
+
+inductive E where
+  | e (n : Nat)
+
+deriving instance Hashable for C, E, D
+
+#guard hash (C.c (.d .leaf)) == hash (C.c (.d .leaf))
+#guard hash (D.d (.c .leaf)) != hash D.leaf
+#guard hash (E.e 3) != hash (E.e 4)
+
+example : Hashable C := instHashableC
+example : Hashable D := instHashableD
+example : Hashable E := instHashableE
diff --git a/tests/elab/derivingReprMutualOnce.lean b/tests/elab/derivingReprMutualOnce.lean
new file mode 100644
index 000000000000..af805e9d8216
--- /dev/null
+++ b/tests/elab/derivingReprMutualOnce.lean
@@ -0,0 +1,90 @@
+/-!
+`deriving Repr` on a mutual block generates one block of auxiliary functions for the whole block
+instead of one per type, and still names each instance after its own type.
+-/
+
+/--
+trace: [Elab.Deriving.repr]
+    [mutual
+       @[no_expose✝]
+       partial def instReprA.repr_1 (x✝ : @A✝) (prec✝ : Nat✝) : Format✝ :=
+         let localinst✝ : Repr✝ (@A✝) := ⟨instReprA.repr_1⟩;
+         let localinst✝¹ : Repr✝ (@B✝) := ⟨instReprA.repr_2⟩;
+         match x✝ with
+         | @A.a a✝ =>
+           Repr.addAppParen✝
+             (Format.group✝
+               (Format.nest✝ (if prec✝ ≥ max_prec then 1 else 2) (Format.text✝ "A.a" ++ Format.line✝ ++ reprArg✝ a✝)))
+             prec✝
+         | @A.leaf =>
+           Repr.addAppParen✝ (Format.group✝ (Format.nest✝ (if prec✝ ≥ max_prec then 1 else 2) (Format.text✝ "A.leaf")))
+             prec✝
+       @[no_expose✝]
+       partial def instReprA.repr_2 (x✝¹ : @B✝) (prec✝ : Nat✝) : Format✝ :=
+         let localinst✝² : Repr✝ (@A✝) := ⟨instReprA.repr_1⟩;
+         let localinst✝³ : Repr✝ (@B✝) := ⟨instReprA.repr_2⟩;
+         match x✝¹ with
+         | @B.b a✝¹ =>
+           Repr.addAppParen✝
+             (Format.group✝
+               (Format.nest✝ (if prec✝ ≥ max_prec then 1 else 2) (Format.text✝ "B.b" ++ Format.line✝ ++ reprArg✝ a✝¹)))
+             prec✝
+         | @B.leaf =>
+           Repr.addAppParen✝ (Format.group✝ (Format.nest✝ (if prec✝ ≥ max_prec then 1 else 2) (Format.text✝ "B.leaf")))
+             prec✝
+     end,
+     instance instReprA : Repr✝ (@A✝) :=
+       ⟨instReprA.repr_1⟩,
+     instance instReprB : Repr✝ (@B✝) :=
+       ⟨instReprA.repr_2⟩]
+-/
+#guard_msgs (whitespace := lax) in
+set_option trace.Elab.Deriving.repr true in
+mutual
+inductive A where
+  | a (b : B)
+  | leaf
+  deriving Repr
+inductive B where
+  | b (a : A)
+  | leaf
+  deriving Repr
+end
+
+/-- info: A.a (B.b (A.leaf)) -/
+#guard_msgs in #eval A.a (.b .leaf)
+
+/-- info: B.b (A.a (B.leaf)) -/
+#guard_msgs in #eval B.b (.a .leaf)
+
+example : Repr A := instReprA
+example : Repr B := instReprB
+
+/-! Types from different mutual blocks in one `deriving instance` command. -/
+
+mutual
+inductive C where
+  | c (d : D)
+  | leaf
+inductive D where
+  | d (c : C)
+  | leaf
+end
+
+inductive E where
+  | e (n : Nat)
+
+deriving instance Repr for C, E, D
+
+/-- info: C.c (D.d (C.leaf)) -/
+#guard_msgs in #eval C.c (.d .leaf)
+
+/-- info: D.d (C.c (D.leaf)) -/
+#guard_msgs in #eval D.d (.c .leaf)
+
+/-- info: E.e 3 -/
+#guard_msgs in #eval E.e 3
+
+example : Repr C := instReprC
+example : Repr D := instReprD
+example : Repr E := instReprE
diff --git a/tests/elab_bench/deriving_mutual_block.lean b/tests/elab_bench/deriving_mutual_block.lean
new file mode 100644
index 000000000000..3b15014557d4
--- /dev/null
+++ b/tests/elab_bench/deriving_mutual_block.lean
@@ -0,0 +1,44 @@
+import Lean
+
+/-!
+Derives `Repr`, `BEq` and `Hashable` on a large mutual block: a hub `H` with `n` constructors
+`cᵢ : Tᵢ → H`, where each structure `Tᵢ` points back to `H`. Deriving handlers used to generate the
+whole block's auxiliary functions once per type, which made this quadratic in `n`.
+-/
+
+set_option Elab.async false
+
+open Lean Elab Command Parser.Command
+
+structure Meta where
+  a : Nat
+  deriving Repr, BEq, Hashable
+
+set_option hygiene false in
+/-- Elaborates the mutual block, with `n` hub constructors. -/
+elab "#mutual_block" : command => do
+  let n := if (← IO.getEnv "TEST_BENCH") == some "1" then 40 else 10
+  let ts := (Array.range n).map fun i => mkIdent (.mkSimple s!"T{i}")
+  let mut ctors ← ts.mapIdxM fun i t => `(ctor| | $(mkIdent (.mkSimple s!"c{i}")):ident : $t → H)
+  ctors := ctors.push (← `(ctor| | other (a : Option Meta) (s : String) : H))
+  let hub ← `(inductive H where
+      $ctors:ctor*
+      deriving Repr, BEq, Hashable)
+  let h2 ← `(structure H2 where
+      p : Option Meta := none
+      f1 : H
+      f2 : String
+      deriving Repr, BEq, Hashable)
+  let structs ← ts.mapM fun t => `(structure $t:ident where
+      p : Option Meta := none
+      f1 : H
+      f2 : Array H2
+      deriving Repr, BEq, Hashable)
+  let decls : Array Command := #[hub, h2] ++ structs
+  elabCommand (← `(mutual $decls:command* end))
+
+#mutual_block
+
+example : Repr T0 := inferInstance
+example : BEq H := inferInstance
+example : Hashable H2 := inferInstance