chore: add placeholders for mkInjectiveTheorems

We can activate them yet since the method is failing when there are
heterogeous equalities in the injectivity theorem type.

src/Lean/Elab/Inductive.lean

@@ -9,6 +9,7 @@ import Lean.Util.CollectLevelParams
 import Lean.Util.Constructions
 import Lean.Meta.CollectFVars
 import Lean.Meta.SizeOf
+import Lean.Meta.Injective
 import Lean.Meta.IndPredBelow
 import Lean.Elab.Command
 import Lean.Elab.DefView
@@ -519,6 +520,8 @@ def elabInductiveViews (views : Array InductiveView) : CommandElabM Unit := do
     mkInductiveDecl vars views
     mkSizeOfInstances view0.declName
     Lean.Meta.IndPredBelow.mkBelow view0.declName
+    -- for view in views do
+    --  mkInjectiveTheorems view.declName
   applyDerivingHandlers views
 
 end Lean.Elab.Command

src/Lean/Elab/Structure.lean

@@ -6,6 +6,7 @@ Authors: Leonardo de Moura
 import Lean.Parser.Command
 import Lean.Meta.Closure
 import Lean.Meta.SizeOf
+import Lean.Meta.Injective
 import Lean.Elab.Command
 import Lean.Elab.DeclModifiers
 import Lean.Elab.DeclUtil
@@ -581,6 +582,7 @@ def elabStructure (modifiers : Modifiers) (stx : Syntax) : CommandElabM Unit :=
             }
             unless isClass do
               mkSizeOfInstances declName
+              -- mkInjectiveTheorems declName
             return declName
   derivingClassViews.forM fun view => view.applyHandlers #[declName]