diff --git a/src/Init/MetaTypes.lean b/src/Init/MetaTypes.lean
index c5832eb4ed04..9c9465a283ef 100644
--- a/src/Init/MetaTypes.lean
+++ b/src/Init/MetaTypes.lean
@@ -169,6 +169,11 @@ structure Config where
   That is, given a local context containing entry `x : t := e`, the free variable `x` reduces to `e`.
   -/
   zetaDelta         : Bool := false
+  /--
+  When `index` (default : `true`) is `false`, `simp` will only use the root symbol
+  to find candidate `simp` theorems. It approximates Lean 3 `simp` behavior.
+  -/
+  index             : Bool := true
   deriving Inhabited, BEq
 
 -- Configuration object for `simp_all`
diff --git a/src/Lean/Meta/DiscrTree.lean b/src/Lean/Meta/DiscrTree.lean
index fe782eb15607..4b6b882141fa 100644
--- a/src/Lean/Meta/DiscrTree.lean
+++ b/src/Lean/Meta/DiscrTree.lean
@@ -634,6 +634,55 @@ where
     else
       return result
 
+/--
+Return the root symbol for `e`, and the number of arguments after `reduceDT`.
+-/
+def getMatchKeyRootFor (e : Expr) (config : WhnfCoreConfig) : MetaM (Key × Nat) := do
+  let e ← reduceDT e (root := true) config
+  let numArgs := e.getAppNumArgs
+  let key := match e.getAppFn with
+    | .lit v         => .lit v
+    | .fvar fvarId   => .fvar fvarId numArgs
+    | .mvar _        => .other
+    | .proj s i _ .. => .proj s i numArgs
+    | .forallE ..    => .arrow
+    | .const c _     =>
+      -- This method is used by the simplifier only, we do **not** support
+      -- (← getConfig).isDefEqStuckEx
+      .const c numArgs
+    | _ => .other
+  return (key, numArgs)
+
+/--
+Get all results under key `k`.
+-/
+private partial def getAllValuesForKey (d : DiscrTree α) (k : Key) (result : Array α) : Array α :=
+  match d.root.find? k with
+  | none      => result
+  | some trie => go trie result
+where
+  go (trie : Trie α) (result : Array α) : Array α := Id.run do
+    match trie with
+    | .node vs cs =>
+      let mut result := result ++ vs
+      for (_, trie) in cs do
+        result := go trie result
+      return result
+
+/--
+A liberal version of `getMatch` which only takes the root symbol of `e` into account.
+We use this method to simulate Lean 3's indexing.
+
+The natural number in the result is the number of arguments in `e` after `reduceDT`.
+-/
+def getMatchLiberal (d : DiscrTree α) (e : Expr) (config : WhnfCoreConfig) : MetaM (Array α × Nat) := do
+  withReducible do
+    let result := getStarResult d
+    let (k, numArgs) ← getMatchKeyRootFor e config
+    match k with
+    | .star  => return (result, numArgs)
+    | _      => return (getAllValuesForKey d k result, numArgs)
+
 partial def getUnify (d : DiscrTree α) (e : Expr) (config : WhnfCoreConfig) : MetaM (Array α) :=
   withReducible do
     let (k, args) ← getUnifyKeyArgs e (root := true) config
diff --git a/src/Lean/Meta/Tactic/Simp/Diagnostics.lean b/src/Lean/Meta/Tactic/Simp/Diagnostics.lean
index df2ff3261d8a..3a07e5c172d6 100644
--- a/src/Lean/Meta/Tactic/Simp/Diagnostics.lean
+++ b/src/Lean/Meta/Tactic/Simp/Diagnostics.lean
@@ -9,6 +9,16 @@ import Lean.Meta.Tactic.Simp.Types
 
 namespace Lean.Meta.Simp
 
+private def originToKey (thmId : Origin) : MetaM MessageData := do
+  match thmId with
+  | .decl declName _ _ =>
+    if (← getEnv).contains declName then
+      pure m!"{MessageData.ofConst (← mkConstWithLevelParams declName)}"
+    else
+      pure m!"{declName} (builtin simproc)"
+  | .fvar fvarId => pure m!"{mkFVar fvarId}"
+  | _ => pure thmId.key
+
 def mkSimpDiagSummary (counters : PHashMap Origin Nat) (usedCounters? : Option (PHashMap Origin Nat) := none) : MetaM DiagSummary := do
   let threshold := diagnostics.threshold.get (← getOptions)
   let entries := collectAboveThreshold counters threshold (fun _ => true) (lt := (· < ·))
@@ -17,14 +27,7 @@ def mkSimpDiagSummary (counters : PHashMap Origin Nat) (usedCounters? : Option (
   else
     let mut data := #[]
     for (thmId, counter) in entries do
-      let key ← match thmId with
-        | .decl declName _ _ =>
-          if (← getEnv).contains declName then
-            pure m!"{MessageData.ofConst (← mkConstWithLevelParams declName)}"
-          else
-            pure m!"{declName} (builtin simproc)"
-        | .fvar fvarId => pure m!"{mkFVar fvarId}"
-        | _ => pure thmId.key
+      let key ← originToKey thmId
       let usedMsg ← if let some usedCounters := usedCounters? then
         if let some c := usedCounters.find? thmId then pure s!", succeeded: {c}" else pure s!" {crossEmoji}" -- not used
       else
@@ -32,16 +35,28 @@ def mkSimpDiagSummary (counters : PHashMap Origin Nat) (usedCounters? : Option (
       data := data.push m!"{if data.isEmpty then "  " else "\n"}{key} ↦ {counter}{usedMsg}"
     return { data, max := entries[0]!.2 }
 
+private def mkTheoremsWithBadKeySummary (thms : PArray SimpTheorem) : MetaM DiagSummary := do
+  if thms.isEmpty then
+    return {}
+  else
+    let mut data := #[]
+    for thm in thms do
+      data := data.push m!"{if data.isEmpty then "  " else "\n"}{← originToKey thm.origin}, key: {thm.keys.map (·.format)}"
+      pure ()
+    return { data }
+
 def reportDiag (diag : Simp.Diagnostics) : MetaM Unit := do
   if (← isDiagnosticsEnabled) then
     let used ← mkSimpDiagSummary diag.usedThmCounter
     let tried ← mkSimpDiagSummary diag.triedThmCounter diag.usedThmCounter
     let congr ← mkDiagSummary diag.congrThmCounter
-    unless used.isEmpty && tried.isEmpty && congr.isEmpty do
+    let thmsWithBadKeys ← mkTheoremsWithBadKeySummary diag.thmsWithBadKeys
+    unless used.isEmpty && tried.isEmpty && congr.isEmpty && thmsWithBadKeys.isEmpty do
       let m := MessageData.nil
       let m := appendSection m `simp "used theorems" used
       let m := appendSection m `simp "tried theorems" tried
       let m := appendSection m `simp "tried congruence theorems" congr
+      let m := appendSection m `simp "theorems with bad keys" thmsWithBadKeys (resultSummary := false)
       let m := m ++ "use `set_option diagnostics.threshold <num>` to control threshold for reporting counters"
       logInfo m
 
diff --git a/src/Lean/Meta/Tactic/Simp/Rewrite.lean b/src/Lean/Meta/Tactic/Simp/Rewrite.lean
index bb8d9045e156..9c4827f782da 100644
--- a/src/Lean/Meta/Tactic/Simp/Rewrite.lean
+++ b/src/Lean/Meta/Tactic/Simp/Rewrite.lean
@@ -189,19 +189,62 @@ def tryTheorem? (e : Expr) (thm : SimpTheorem) : SimpM (Option Result) := do
 Remark: the parameter tag is used for creating trace messages. It is irrelevant otherwise.
 -/
 def rewrite? (e : Expr) (s : SimpTheoremTree) (erased : PHashSet Origin) (tag : String) (rflOnly : Bool) : SimpM (Option Result) := do
-  let candidates ← s.getMatchWithExtra e (getDtConfig (← getConfig))
-  if candidates.isEmpty then
-    trace[Debug.Meta.Tactic.simp] "no theorems found for {tag}-rewriting {e}"
-    return none
+  if (← getConfig).index then
+    rewriteUsingIndex?
   else
-    let candidates := candidates.insertionSort fun e₁ e₂ => e₁.1.priority > e₂.1.priority
-    for (thm, numExtraArgs) in candidates do
-      unless inErasedSet thm || (rflOnly && !thm.rfl) do
-        if let some result ← tryTheoremWithExtraArgs? e thm numExtraArgs then
-          trace[Debug.Meta.Tactic.simp] "rewrite result {e} => {result.expr}"
-          return some result
-    return none
+    rewriteNoIndex?
 where
+  /-- For `(← getConfig).index := true`, use discrimination tree structure when collecting `simp` theorem candidates. -/
+  rewriteUsingIndex? : SimpM (Option Result) := do
+    let candidates ← s.getMatchWithExtra e (getDtConfig (← getConfig))
+    if candidates.isEmpty then
+      trace[Debug.Meta.Tactic.simp] "no theorems found for {tag}-rewriting {e}"
+      return none
+    else
+      let candidates := candidates.insertionSort fun e₁ e₂ => e₁.1.priority > e₂.1.priority
+      for (thm, numExtraArgs) in candidates do
+        unless inErasedSet thm || (rflOnly && !thm.rfl) do
+          if let some result ← tryTheoremWithExtraArgs? e thm numExtraArgs then
+            trace[Debug.Meta.Tactic.simp] "rewrite result {e} => {result.expr}"
+            return some result
+      return none
+
+  /--
+  For `(← getConfig).index := false`, Lean 3 style `simp` theorem retrieval.
+  Only the root symbol is taken into account. Most of the structure of the discrimination tree is ignored.
+  -/
+  rewriteNoIndex? : SimpM (Option Result) := do
+    let (candidates, numArgs) ← s.getMatchLiberal e (getDtConfig (← getConfig))
+    if candidates.isEmpty then
+      trace[Debug.Meta.Tactic.simp] "no theorems found for {tag}-rewriting {e}"
+      return none
+    else
+      let candidates := candidates.insertionSort fun e₁ e₂ => e₁.priority > e₂.priority
+      for thm in candidates do
+        unless inErasedSet thm || (rflOnly && !thm.rfl) do
+          let result? ← withNewMCtxDepth do
+            let val  ← thm.getValue
+            let type ← inferType val
+            let (xs, bis, type) ← forallMetaTelescopeReducing type
+            let type ← whnf (← instantiateMVars type)
+            let lhs := type.appFn!.appArg!
+            let lhsNumArgs := lhs.getAppNumArgs
+            tryTheoremCore lhs xs bis val type e thm (numArgs - lhsNumArgs)
+          if let some result := result? then
+            trace[Debug.Meta.Tactic.simp] "rewrite result {e} => {result.expr}"
+            diagnoseWhenNoIndex thm
+            return some result
+    return none
+
+  diagnoseWhenNoIndex (thm : SimpTheorem) : SimpM Unit := do
+    if (← isDiagnosticsEnabled) then
+      let candidates ← s.getMatchWithExtra e (getDtConfig (← getConfig))
+      for (candidate, _) in candidates do
+        if unsafe ptrEq thm candidate then
+          return ()
+      -- `thm` would not have been applied if `index := true`
+      recordTheoremWithBadKeys thm
+
   inErasedSet (thm : SimpTheorem) : Bool :=
     erased.contains thm.origin
 
diff --git a/src/Lean/Meta/Tactic/Simp/Types.lean b/src/Lean/Meta/Tactic/Simp/Types.lean
index 962a936271ff..b39a70b29323 100644
--- a/src/Lean/Meta/Tactic/Simp/Types.lean
+++ b/src/Lean/Meta/Tactic/Simp/Types.lean
@@ -111,6 +111,13 @@ structure Diagnostics where
   triedThmCounter : PHashMap Origin Nat := {}
   /-- Number of times each congr theorem has been tried. -/
   congrThmCounter : PHashMap Name Nat := {}
+  /--
+  When using `Simp.Config.index := false`, and `set_option diagnostics true`,
+  for every theorem used by `simp`, we check whether the theorem would be
+  also applied if `index := true`, and we store it here if it would not have
+  been tried.
+  -/
+  thmsWithBadKeys : PArray SimpTheorem := {}
   deriving Inhabited
 
 structure State where
@@ -325,14 +332,14 @@ Save current cache, reset it, execute `x`, and then restore original cache.
   withReader (fun r => { MethodsRef.toMethods r with discharge?, wellBehavedDischarge }.toMethodsRef) x
 
 def recordTriedSimpTheorem (thmId : Origin) : SimpM Unit := do
-  modifyDiag fun { usedThmCounter, triedThmCounter, congrThmCounter } =>
-    let cNew := if let some c := triedThmCounter.find? thmId then c + 1 else 1
-    { usedThmCounter, triedThmCounter := triedThmCounter.insert thmId cNew, congrThmCounter }
+  modifyDiag fun s =>
+    let cNew := if let some c := s.triedThmCounter.find? thmId then c + 1 else 1
+    { s with triedThmCounter := s.triedThmCounter.insert thmId cNew }
 
 def recordSimpTheorem (thmId : Origin) : SimpM Unit := do
-  modifyDiag fun { usedThmCounter, triedThmCounter, congrThmCounter } =>
-    let cNew := if let some c := usedThmCounter.find? thmId then c + 1 else 1
-    { usedThmCounter := usedThmCounter.insert thmId cNew, triedThmCounter, congrThmCounter }
+  modifyDiag fun s =>
+    let cNew := if let some c := s.usedThmCounter.find? thmId then c + 1 else 1
+    { s with usedThmCounter := s.usedThmCounter.insert thmId cNew }
   /-
   If `thmId` is an equational theorem (e.g., `foo.eq_1`), we should record `foo` instead.
   See issue #3547.
@@ -353,9 +360,17 @@ def recordSimpTheorem (thmId : Origin) : SimpM Unit := do
     { s with usedTheorems := s.usedTheorems.insert thmId n }
 
 def recordCongrTheorem (declName : Name) : SimpM Unit := do
-  modifyDiag fun { usedThmCounter, triedThmCounter, congrThmCounter } =>
-    let cNew := if let some c := congrThmCounter.find? declName then c + 1 else 1
-    { congrThmCounter := congrThmCounter.insert declName cNew, triedThmCounter, usedThmCounter }
+  modifyDiag fun s =>
+    let cNew := if let some c := s.congrThmCounter.find? declName then c + 1 else 1
+    { s with congrThmCounter := s.congrThmCounter.insert declName cNew }
+
+def recordTheoremWithBadKeys (thm : SimpTheorem) : SimpM Unit := do
+  modifyDiag fun s =>
+    -- check whether it is already there
+    if unsafe s.thmsWithBadKeys.any fun thm' => ptrEq thm thm' then
+      s
+    else
+      { s with thmsWithBadKeys := s.thmsWithBadKeys.push thm }
 
 def Result.getProof (r : Result) : MetaM Expr := do
   match r.proof? with
diff --git a/tests/lean/run/4171.lean b/tests/lean/run/4171.lean
new file mode 100644
index 000000000000..e387e573e37b
--- /dev/null
+++ b/tests/lean/run/4171.lean
@@ -0,0 +1,782 @@
+/-!
+This is a minimization of a problem in Mathlib where a simp lemma `foo` would not fire,
+but variants:
+* `simp [(foo)]`
+* `simp [foo.{v₁ + 1}]`
+* `simp [foo']`, where a `no_index` is added in the statement
+all work.
+-/
+
+section Mathlib.Data.Opposite
+
+universe v u
+
+variable (α : Sort u)
+
+structure Opposite :=
+  op ::
+  unop : α
+
+notation:max α "ᵒᵖ" => Opposite α
+
+end Mathlib.Data.Opposite
+
+section Mathlib.Combinatorics.Quiver.Basic
+
+open Opposite
+
+universe v v₁ v₂ u u₁ u₂
+
+class Quiver (V : Type u) where
+  Hom : V → V → Sort v
+
+infixr:10 " ⟶ " => Quiver.Hom
+
+structure Prefunctor (V : Type u₁) [Quiver.{v₁} V] (W : Type u₂) [Quiver.{v₂} W] where
+  obj : V → W
+  map : ∀ {X Y : V}, (X ⟶ Y) → (obj X ⟶ obj Y)
+namespace Quiver
+
+instance opposite {V} [Quiver V] : Quiver Vᵒᵖ :=
+  ⟨fun a b => (unop b ⟶ unop a)ᵒᵖ⟩
+
+def Hom.op {V} [Quiver V] {X Y : V} (f : X ⟶ Y) : op Y ⟶ op X := ⟨f⟩
+
+def Hom.unop {V} [Quiver V] {X Y : Vᵒᵖ} (f : X ⟶ Y) : unop Y ⟶ unop X := Opposite.unop f
+
+end Quiver
+
+
+end Mathlib.Combinatorics.Quiver.Basic
+
+section Mathlib.CategoryTheory.Category.Basic
+
+universe v u
+
+namespace CategoryTheory
+
+class CategoryStruct (obj : Type u) extends Quiver.{v + 1} obj : Type max u (v + 1) where
+  id : ∀ X : obj, Hom X X
+  comp : ∀ {X Y Z : obj}, (X ⟶ Y) → (Y ⟶ Z) → (X ⟶ Z)
+
+scoped notation "𝟙" => CategoryStruct.id
+
+scoped infixr:80 " ≫ " => CategoryStruct.comp
+
+class Category (obj : Type u) extends CategoryStruct.{v} obj : Type max u (v + 1) where
+  id_comp : ∀ {X Y : obj} (f : X ⟶ Y), 𝟙 X ≫ f = f
+  comp_id : ∀ {X Y : obj} (f : X ⟶ Y), f ≫ 𝟙 Y = f
+
+attribute [simp] Category.id_comp Category.comp_id
+
+end CategoryTheory
+
+end Mathlib.CategoryTheory.Category.Basic
+
+section Mathlib.CategoryTheory.Functor.Basic
+
+namespace CategoryTheory
+
+universe v v₁ v₂ v₃ u u₁ u₂ u₃
+
+structure Functor (C : Type u₁) [Category.{v₁} C] (D : Type u₂) [Category.{v₂} D]
+    extends Prefunctor C D : Type max v₁ v₂ u₁ u₂ where
+
+infixr:26 " ⥤ " => Functor
+
+namespace Functor
+
+section
+
+variable (C : Type u₁) [Category.{v₁} C]
+
+protected def id : C ⥤ C where
+  obj X := X
+  map f := f
+
+notation "𝟭" => Functor.id
+
+variable {C}
+
+@[simp]
+theorem id_obj (X : C) : (𝟭 C).obj X = X := rfl
+
+end
+
+variable {C : Type u₁} [Category.{v₁} C] {D : Type u₂} [Category.{v₂} D]
+  {E : Type u₃} [Category.{v₃} E]
+
+@[simp]
+def comp (F : C ⥤ D) (G : D ⥤ E) : C ⥤ E where
+  obj X := G.obj (F.obj X)
+  map f := G.map (F.map f)
+
+infixr:80 " ⋙ " => Functor.comp
+
+end Functor
+
+end CategoryTheory
+
+
+end Mathlib.CategoryTheory.Functor.Basic
+
+section Mathlib.CategoryTheory.NatTrans
+
+namespace CategoryTheory
+
+universe v₁ v₂ v₃ v₄ u₁ u₂ u₃ u₄
+
+variable {C : Type u₁} [Category.{v₁} C] {D : Type u₂} [Category.{v₂} D]
+
+structure NatTrans (F G : C ⥤ D) : Type max u₁ v₂ where
+  app : ∀ X : C, F.obj X ⟶ G.obj X
+
+end CategoryTheory
+
+end Mathlib.CategoryTheory.NatTrans
+
+section Mathlib.CategoryTheory.Iso
+
+universe v u
+
+namespace CategoryTheory
+
+open Category
+
+structure Iso {C : Type u} [Category.{v} C] (X Y : C) where
+  hom : X ⟶ Y
+  inv : Y ⟶ X
+
+infixr:10 " ≅ " => Iso
+
+variable {C : Type u} [Category.{v} C] {X Y Z : C}
+
+namespace Iso
+
+@[simp]
+def symm (I : X ≅ Y) : Y ≅ X where
+  hom := I.inv
+  inv := I.hom
+
+@[simp]
+def refl (X : C) : X ≅ X where
+  hom := 𝟙 X
+  inv := 𝟙 X
+
+@[simp]
+def trans (α : X ≅ Y) (β : Y ≅ Z) : X ≅ Z where
+  hom := α.hom ≫ β.hom
+  inv := β.inv ≫ α.inv
+
+infixr:80 " ≪≫ " => Iso.trans
+
+end Iso
+
+namespace Functor
+
+universe u₂ v₂
+
+variable {D : Type u₂} [Category.{v₂} D]
+
+@[simp]
+def mapIso (F : C ⥤ D) {X Y : C} (i : X ≅ Y) : F.obj X ≅ F.obj Y where
+  hom := F.map i.hom
+  inv := F.map i.inv
+
+end Functor
+
+end CategoryTheory
+
+
+end Mathlib.CategoryTheory.Iso
+
+section Mathlib.CategoryTheory.Functor.Category
+
+namespace CategoryTheory
+
+universe v₁ v₂ v₃ u₁ u₂ u₃
+
+variable (C : Type u₁) [Category.{v₁} C] (D : Type u₂) [Category.{v₂} D]
+
+instance Functor.category : Category.{max u₁ v₂} (C ⥤ D) where
+  Hom F G := NatTrans F G
+  id F := sorry
+  comp α β := sorry
+  id_comp := sorry
+  comp_id := sorry
+
+end CategoryTheory
+
+end Mathlib.CategoryTheory.Functor.Category
+
+section Mathlib.CategoryTheory.NatIso
+
+
+open CategoryTheory
+
+universe v₁ v₂ v₃ v₄ u₁ u₂ u₃ u₄
+
+namespace CategoryTheory
+
+variable {C : Type u₁} [Category.{v₁} C] {D : Type u₂} [Category.{v₂} D]
+
+namespace Iso
+
+@[simp]
+def app {F G : C ⥤ D} (α : F ≅ G) (X : C) : F.obj X ≅ G.obj X where
+  hom := α.hom.app X
+  inv := α.inv.app X
+
+end Iso
+
+namespace NatIso
+
+variable {F G : C ⥤ D} {X : C}
+
+@[simp]
+def ofComponents (app : ∀ X : C, F.obj X ≅ G.obj X) :
+    F ≅ G where
+  hom :=
+  { app := fun X => (app X).hom }
+  inv :=
+    { app := fun X => (app X).inv }
+
+end NatIso
+
+
+end CategoryTheory
+
+
+end Mathlib.CategoryTheory.NatIso
+
+section Mathlib.CategoryTheory.Equivalence
+
+namespace CategoryTheory
+
+open CategoryTheory.Functor NatIso Category
+
+universe v₁ v₂ v₃ u₁ u₂ u₃
+
+structure Equivalence (C : Type u₁) (D : Type u₂) [Category.{v₁} C] [Category.{v₂} D] where mk' ::
+  functor : C ⥤ D
+  inverse : D ⥤ C
+  unitIso : 𝟭 C ≅ functor ⋙ inverse
+  counitIso : inverse ⋙ functor ≅ 𝟭 D
+
+infixr:10 " ≌ " => Equivalence
+
+variable {C : Type u₁} [Category.{v₁} C] {D : Type u₂} [Category.{v₂} D]
+
+@[simp]
+def Equivalence.symm (e : C ≌ D) : D ≌ C :=
+  ⟨e.inverse, e.functor, e.counitIso.symm, e.unitIso.symm⟩
+
+end CategoryTheory
+
+
+end Mathlib.CategoryTheory.Equivalence
+
+section Mathlib.CategoryTheory.Opposites
+
+universe v₁ v₂ u₁ u₂
+
+open Opposite
+
+variable {C : Type u₁}
+
+@[simp]
+theorem Quiver.Hom.unop_op [Quiver.{v₁} C] {X Y : C} (f : X ⟶ Y) : f.op.unop = f :=
+  rfl
+
+namespace CategoryTheory
+
+variable [Category.{v₁} C]
+
+instance Category.opposite : Category.{v₁} Cᵒᵖ where
+  comp f g := (g.unop ≫ f.unop).op
+  id X := (𝟙 (unop X)).op
+  id_comp := sorry
+  comp_id := sorry
+
+protected def Iso.op {X Y : C} (α : X ≅ Y) : op Y ≅ op X where
+  hom := α.hom.op
+  inv := α.inv.op
+
+end CategoryTheory
+
+
+end Mathlib.CategoryTheory.Opposites
+
+section Mathlib.CategoryTheory.Monoidal.Category
+
+universe v u
+
+namespace CategoryTheory
+
+class MonoidalCategoryStruct (C : Type u) [𝒞 : Category.{v} C] where
+  tensorObj : C → C → C
+  whiskerLeft (X : C) {Y₁ Y₂ : C} (f : Y₁ ⟶ Y₂) : tensorObj X Y₁ ⟶ tensorObj X Y₂
+  whiskerRight {X₁ X₂ : C} (f : X₁ ⟶ X₂) (Y : C) : tensorObj X₁ Y ⟶ tensorObj X₂ Y
+  tensorHom {X₁ Y₁ X₂ Y₂ : C} (f : X₁ ⟶ Y₁) (g: X₂ ⟶ Y₂) : (tensorObj X₁ X₂ ⟶ tensorObj Y₁ Y₂) :=
+    whiskerRight f X₂ ≫ whiskerLeft Y₁ g
+  tensorUnit : C
+  rightUnitor : ∀ X : C, tensorObj X tensorUnit ≅ X
+
+namespace MonoidalCategory
+
+scoped infixr:70 " ⊗ " => MonoidalCategoryStruct.tensorObj
+scoped infixr:81 " ◁ " => MonoidalCategoryStruct.whiskerLeft
+scoped infixl:81 " ▷ " => MonoidalCategoryStruct.whiskerRight
+scoped infixr:70 " ⊗ " => MonoidalCategoryStruct.tensorHom
+scoped notation "𝟙_ " C:max => (MonoidalCategoryStruct.tensorUnit : C)
+scoped notation "ρ_" => MonoidalCategoryStruct.rightUnitor
+
+end MonoidalCategory
+
+open MonoidalCategory
+
+class MonoidalCategory (C : Type u) [𝒞 : Category.{v} C] extends MonoidalCategoryStruct C where
+  id_whiskerRight : ∀ (X Y : C), 𝟙 X ▷ Y = 𝟙 (X ⊗ Y)
+
+attribute [simp] MonoidalCategory.id_whiskerRight
+
+namespace MonoidalCategory
+
+variable {C : Type u} [𝒞 : Category.{v} C] [MonoidalCategory C]
+
+@[simp]
+theorem id_tensorHom (X : C) {Y₁ Y₂ : C} (f : Y₁ ⟶ Y₂) :
+    𝟙 X ⊗ f = X ◁ f := sorry
+
+@[simp]
+theorem tensorHom_id {X₁ X₂ : C} (f : X₁ ⟶ X₂) (Y : C) :
+    f ⊗ 𝟙 Y = f ▷ Y := sorry
+
+end MonoidalCategory
+
+@[simp]
+def tensorIso {C : Type u} {X Y X' Y' : C} [Category.{v} C] [MonoidalCategory.{v} C] (f : X ≅ Y)
+    (g : X' ≅ Y') : X ⊗ X' ≅ Y ⊗ Y' where
+  hom := f.hom ⊗ g.hom
+  inv := f.inv ⊗ g.inv
+
+infixr:70 " ⊗ " => tensorIso
+
+end CategoryTheory
+
+end Mathlib.CategoryTheory.Monoidal.Category
+
+section Mathlib.CategoryTheory.Monoidal.Opposite
+
+universe v₁ v₂ u₁ u₂
+
+namespace CategoryTheory
+
+variable {C : Type u₁} [Category.{v₁} C] [MonoidalCategory.{v₁} C]
+
+open Opposite MonoidalCategory
+
+instance monoidalCategoryOp : MonoidalCategory Cᵒᵖ where
+  tensorObj X Y := op (unop X ⊗ unop Y)
+  whiskerLeft X _ _ f := (X.unop ◁ f.unop).op
+  whiskerRight f X := (f.unop ▷ X.unop).op
+  tensorHom f g := (f.unop ⊗ g.unop).op
+  tensorUnit := op (𝟙_ C)
+  id_whiskerRight := sorry
+  rightUnitor X := (ρ_ (unop X)).symm.op
+
+
+@[simp] theorem op_whiskerLeft (X : C) {Y Z : C} (f : Y ⟶ Z) :
+    (X ◁ f).op = op X ◁ f.op := rfl
+@[simp] theorem unop_whiskerLeft (X : Cᵒᵖ) {Y Z : Cᵒᵖ} (f : Y ⟶ Z) :
+    (X ◁ f).unop =  unop X ◁ f.unop := rfl
+
+@[simp] theorem op_hom_rightUnitor (X : C) : (ρ_ X).hom.op = (ρ_ (op X)).inv := rfl
+@[simp] theorem unop_hom_rightUnitor (X : Cᵒᵖ) : (ρ_ X).hom.unop = (ρ_ (unop X)).inv := rfl
+
+@[simp] theorem op_inv_rightUnitor (X : C) : (ρ_ X).inv.op = (ρ_ (op X)).hom := rfl
+@[simp] theorem unop_inv_rightUnitor (X : Cᵒᵖ) : (ρ_ X).inv.unop = (ρ_ (unop X)).hom := rfl
+
+end CategoryTheory
+
+
+end Mathlib.CategoryTheory.Monoidal.Opposite
+
+section Mathlib.CategoryTheory.Monoidal.Transport
+
+universe v₁ v₂ u₁ u₂
+
+noncomputable section
+
+open CategoryTheory Category MonoidalCategory
+
+namespace CategoryTheory.Monoidal
+
+variable {C : Type u₁} [Category.{v₁} C] [MonoidalCategory.{v₁} C]
+variable {D : Type u₂} [Category.{v₂} D]
+
+abbrev induced [MonoidalCategoryStruct D] (F : D ⥤ C) :
+    MonoidalCategory.{v₂} D where
+  id_whiskerRight X Y := sorry
+
+def transportStruct (e : C ≌ D) : MonoidalCategoryStruct.{v₂} D where
+  tensorObj X Y := e.functor.obj (e.inverse.obj X ⊗ e.inverse.obj Y)
+  whiskerLeft X _ _ f := e.functor.map (e.inverse.obj X ◁ e.inverse.map f)
+  whiskerRight f X := sorry
+  tensorHom f g := sorry
+  tensorUnit := e.functor.obj (𝟙_ C)
+  rightUnitor X :=
+    e.functor.mapIso ((Iso.refl _ ⊗ (e.unitIso.app _).symm) ≪≫ ρ_ (e.inverse.obj X)) ≪≫
+      e.counitIso.app _
+
+@[simp] theorem transportStruct_whiskerLeft (e : C ≌ D) (X x x_1 : D) (f : x ⟶ x_1) :
+  (transportStruct e).whiskerLeft X f = e.functor.map (e.inverse.obj X ◁ e.inverse.map f) := rfl
+
+@[simp] theorem transportStruct_rightUnitor (e : C ≌ D) (X : D) :
+  (transportStruct e).rightUnitor X =
+    e.functor.mapIso ((Iso.refl _ ⊗ (e.unitIso.app _).symm) ≪≫ ρ_ (e.inverse.obj X)) ≪≫
+      e.counitIso.app _ := rfl
+
+def transport (e : C ≌ D) : MonoidalCategory.{v₂} D :=
+  letI : MonoidalCategoryStruct.{v₂} D := transportStruct e
+  induced e.inverse
+
+end CategoryTheory.Monoidal
+
+end
+
+end Mathlib.CategoryTheory.Monoidal.Transport
+
+section Mathlib.CategoryTheory.Monoidal.Braided.Basic
+
+open CategoryTheory MonoidalCategory
+
+universe v v₁ v₂ v₃ u u₁ u₂ u₃
+
+namespace CategoryTheory
+
+variable (C : Type u₁) [Category.{v₁} C] [MonoidalCategory C]
+
+def tensor_μ (X Y : C × C) : (X.1 ⊗ X.2) ⊗ Y.1 ⊗ Y.2 ⟶ (X.1 ⊗ Y.1) ⊗ X.2 ⊗ Y.2 :=
+  sorry
+
+end CategoryTheory
+
+end Mathlib.CategoryTheory.Monoidal.Braided.Basic
+
+section Mathlib.CategoryTheory.Monoidal.Mon_
+
+universe v₁ v₂ u₁ u₂ u
+
+open CategoryTheory MonoidalCategory
+
+variable (C : Type u₁) [Category.{v₁} C] [MonoidalCategory.{v₁} C]
+
+structure Mon_ where
+  X : C
+  one : 𝟙_ C ⟶ X
+  mul : X ⊗ X ⟶ X
+  mul_one : (X ◁ one) ≫ mul = (ρ_ X).hom
+
+attribute [simp] Mon_.mul_one
+namespace Mon_
+
+@[simp]
+def trivial : Mon_ C where
+  X := 𝟙_ C
+  one := 𝟙 _
+  mul := sorry
+  mul_one := sorry
+
+variable {C}
+variable {M : Mon_ C}
+
+structure Hom (M N : Mon_ C) where
+  hom : M.X ⟶ N.X
+
+@[simp]
+def id (M : Mon_ C) : Hom M M where
+  hom := 𝟙 M.X
+
+@[simp]
+def comp {M N O : Mon_ C} (f : Hom M N) (g : Hom N O) : Hom M O where
+  hom := f.hom ≫ g.hom
+
+instance : Category (Mon_ C) where
+  Hom M N := Hom M N
+  id := id
+  comp f g := comp f g
+  id_comp := sorry
+  comp_id := sorry
+
+@[ext]
+theorem ext {X Y : Mon_ C} {f g : X ⟶ Y} (w : f.hom = g.hom) : f = g := sorry
+
+@[simp]
+theorem id_hom' (M : Mon_ C) : (𝟙 M : Hom M M).hom = 𝟙 M.X := sorry
+
+@[simp]
+theorem comp_hom' {M N K : Mon_ C} (f : M ⟶ N) (g : N ⟶ K) :
+    (f ≫ g : Hom M K).hom = f.hom ≫ g.hom := sorry
+
+variable (C) in
+@[simp]
+def forget : Mon_ C ⥤ C where
+  obj A := A.X
+  map f := f.hom
+
+@[simp]
+def isoOfIso {M N : Mon_ C} (f : M.X ≅ N.X) : M ≅ N where
+  hom := { hom := f.hom }
+  inv := { hom := f.inv }
+
+
+
+@[simp]
+instance monMonoidalStruct : MonoidalCategoryStruct (Mon_ C) :=
+  let tensorObj (M N : Mon_ C) : Mon_ C :=
+    { X := M.X ⊗ N.X
+      one := sorry
+      mul := tensor_μ C (M.X, N.X) (M.X, N.X) ≫ (M.mul ⊗ N.mul)
+      mul_one := sorry }
+  let tensorHom {X₁ Y₁ X₂ Y₂ : Mon_ C} (f : X₁ ⟶ Y₁) (g : X₂ ⟶ Y₂) :
+      tensorObj _ _ ⟶ tensorObj _ _ :=
+    { hom := f.hom ⊗ g.hom }
+  { tensorObj := tensorObj
+    tensorHom := tensorHom
+    whiskerRight := fun f Y => tensorHom f (𝟙 Y)
+    whiskerLeft := fun X _ _ g => tensorHom (𝟙 X) g
+    tensorUnit := trivial C
+    rightUnitor := fun M ↦ isoOfIso (ρ_ M.X) }
+
+@[simp]
+theorem whiskerLeft_hom {X Y : Mon_ C} (f : X ⟶ Y) (Z : Mon_ C) :
+    (f ▷ Z).hom = f.hom ▷ Z.X := by
+  rw [← tensorHom_id]; rfl
+
+@[simp]
+theorem whiskerRight_hom (X : Mon_ C) {Y Z : Mon_ C} (f : Y ⟶ Z) :
+    (X ◁ f).hom = X.X ◁ f.hom := by
+  rw [← id_tensorHom]; rfl
+
+@[simp]
+theorem rightUnitor_inv_hom (X : Mon_ C) : (ρ_ X).inv.hom = (ρ_ X.X).inv := rfl
+
+instance monMonoidal : MonoidalCategory (Mon_ C) where
+  id_whiskerRight := sorry
+
+end Mon_
+
+end Mathlib.CategoryTheory.Monoidal.Mon_
+
+section Mathlib.CategoryTheory.Monoidal.Comon_
+
+universe v₁ v₂ u₁ u₂ u
+
+open CategoryTheory MonoidalCategory
+
+variable (C : Type u₁) [Category.{v₁} C] [MonoidalCategory.{v₁} C]
+
+structure Comon_ where
+  X : C
+  counit : X ⟶ 𝟙_ C
+  comul : X ⟶ X ⊗ X
+
+namespace Comon_
+
+variable {C}
+variable {M : Comon_ C}
+
+structure Hom (M N : Comon_ C) where
+  hom : M.X ⟶ N.X
+
+@[simp]
+def id (M : Comon_ C) : Hom M M where
+  hom := 𝟙 M.X
+
+@[simp]
+def comp {M N O : Comon_ C} (f : Hom M N) (g : Hom N O) : Hom M O where
+  hom := f.hom ≫ g.hom
+
+instance : Category (Comon_ C) where
+  Hom M N := Hom M N
+  id := id
+  comp f g := comp f g
+  comp_id := sorry
+  id_comp := sorry
+
+@[ext] theorem ext {X Y : Comon_ C} {f g : X ⟶ Y} (w : f.hom = g.hom) : f = g := sorry
+
+@[simp] theorem id_hom' (M : Comon_ C) : (𝟙 M : Hom M M).hom = 𝟙 M.X := rfl
+
+@[simp]
+theorem comp_hom' {M N K : Comon_ C} (f : M ⟶ N) (g : N ⟶ K) : (f ≫ g).hom = f.hom ≫ g.hom :=
+  rfl
+
+open Opposite
+
+variable (C)
+
+def Comon_to_Mon_op_op_obj' (A : Comon_ C) : Mon_ (Cᵒᵖ) where
+  X := op A.X
+  one := A.counit.op
+  mul := A.comul.op
+  mul_one := sorry
+
+@[simp] theorem Comon_to_Mon_op_op_obj'_X (A : Comon_ C) : (Comon_to_Mon_op_op_obj' C A).X = op A.X := rfl
+
+@[simp] def Comon_to_Mon_op_op : Comon_ C ⥤ (Mon_ (Cᵒᵖ))ᵒᵖ where
+  obj A := op (Comon_to_Mon_op_op_obj' C A)
+  map := fun f => op <| { hom := f.hom.op }
+
+def Mon_op_op_to_Comon_obj' (A : (Mon_ (Cᵒᵖ))) : Comon_ C where
+  X := unop A.X
+  counit := A.one.unop
+  comul := A.mul.unop
+
+@[simp] theorem Mon_op_op_to_Comon_obj'_X (A : (Mon_ (Cᵒᵖ))) : (Mon_op_op_to_Comon_obj' C A).X = unop A.X := rfl
+
+@[simp]
+def Mon_op_op_to_Comon : (Mon_ (Cᵒᵖ))ᵒᵖ ⥤ Comon_ C where
+  obj A := Mon_op_op_to_Comon_obj' C (unop A)
+  map := fun f =>
+    { hom := f.unop.hom.unop }
+
+@[simp]
+def Comon_equiv_Mon_op_op : Comon_ C ≌ (Mon_ (Cᵒᵖ))ᵒᵖ :=
+  { functor := Comon_to_Mon_op_op C
+    inverse := Mon_op_op_to_Comon C
+    unitIso := NatIso.ofComponents (fun _ => Iso.refl _)
+    counitIso := NatIso.ofComponents (fun _ => Iso.refl _) }
+
+instance : MonoidalCategory (Comon_ C) :=
+  Monoidal.transport (Comon_equiv_Mon_op_op C).symm
+
+end Comon_
+
+namespace CategoryTheory.Functor
+
+variable {C} {D : Type u₂} [Category.{v₂} D] [MonoidalCategory.{v₂} D]
+
+def mapComon (F : C ⥤ D) : Comon_ C ⥤ Comon_ D where
+  obj A :=
+    { X := F.obj A.X
+      counit := sorry
+      comul := sorry }
+  map f := sorry
+
+end CategoryTheory.Functor
+
+
+end Mathlib.CategoryTheory.Monoidal.Comon_
+
+section Mathlib.CategoryTheory.Monoidal.Bimon_
+
+noncomputable section
+
+universe v₁ v₂ u₁ u₂ u
+
+open CategoryTheory MonoidalCategory
+
+variable (C : Type u₁) [Category.{v₁} C] [MonoidalCategory.{v₁} C]
+
+def toComon_ : Comon_ (Mon_ C) ⥤ Comon_ C := (Mon_.forget C).mapComon
+
+@[simp] theorem toComon_obj_X (M : Comon_ (Mon_ C)) : ((toComon_ C).obj M).X = M.X.X := rfl
+
+theorem foo {V} [Quiver V] {X Y x} :
+    @Quiver.Hom.unop V _ X Y (Opposite.op (unop := x)) = x := rfl
+
+example (M : Comon_ (Mon_ C)) : Mon_ (Comon_ C) where
+  X := (toComon_ C).obj M
+  one := { hom := M.X.one }
+  mul := { hom := M.X.mul }
+  mul_one := by
+    ext
+    simp [(foo)] -- parentheses around `foo` works
+
+example (M : Comon_ (Mon_ C)) : Mon_ (Comon_ C) where
+  X := (toComon_ C).obj M
+  one := { hom := M.X.one }
+  mul := { hom := M.X.mul }
+  mul_one := by
+    ext
+    simp [foo.{v₁ + 1}] -- specifying the universe level explicitly works!
+
+theorem foo' {V} [Quiver V] {X Y x} :
+    @Quiver.Hom.unop V _ X Y no_index (Opposite.op (unop := x)) = x := rfl
+
+example (M : Comon_ (Mon_ C)) : Mon_ (Comon_ C) where
+  X := (toComon_ C).obj M
+  one := { hom := M.X.one }
+  mul := { hom := M.X.mul }
+  mul_one := by
+    ext
+    simp [foo'] -- or adding a `no_index` in the statement
+
+
+/--
+info: [simp] theorems with bad keys
+    foo, key: [Quiver.Hom.unop,
+   *,
+   *,
+   *,
+   *,
+   Opposite.op,
+   Quiver.Hom,
+   *,
+   *,
+   Opposite.0,
+   *,
+   Opposite.0,
+   *,
+   *]use `set_option diagnostics.threshold <num>` to control threshold for reporting counters
+-/
+#guard_msgs in
+example (M : Comon_ (Mon_ C)) : Mon_ (Comon_ C) where
+  X := (toComon_ C).obj M
+  one := { hom := M.X.one }
+  mul := { hom := M.X.mul, }
+  mul_one := by
+    ext
+    -- increase the threshold to ensure the guard_msgs docstring is not too big.
+    set_option diagnostics.threshold 100000 in
+    set_option diagnostics true in
+    -- `index := false` ignores most of the discrimination tree structure.
+    simp (config := { index := false }) [foo]
+
+attribute [simp] foo
+
+/--
+info: [simp] theorems with bad keys
+    foo, key: [Quiver.Hom.unop,
+   *,
+   *,
+   *,
+   *,
+   Opposite.op,
+   Quiver.Hom,
+   *,
+   *,
+   Opposite.0,
+   *,
+   Opposite.0,
+   *,
+   *]use `set_option diagnostics.threshold <num>` to control threshold for reporting counters
+-/
+#guard_msgs in
+example (M : Comon_ (Mon_ C)) : Mon_ (Comon_ C) where
+  X := (toComon_ C).obj M
+  one := { hom := M.X.one }
+  mul := { hom := M.X.mul, }
+  mul_one := by
+    ext
+    -- increase the threshold to ensure the guard_msgs docstring is not too big.
+    set_option diagnostics.threshold 100000 in
+    set_option diagnostics true in
+    -- `index := false` ignores most of the discrimination tree structure.
+    simp (config := { index := false })
+
+end
+
+end Mathlib.CategoryTheory.Monoidal.Bimon_