def Lean.Meta.Grind.injection? (mvarId : Lean.MVarId) (fvarId : Lean.FVarId) : Lean.MetaM (Option Lean.MVarId)

The grind tactic includes an auxiliary injection? tactic that is not intended for direct use by users. This tactic is automatically applied when introducing non-dependent propositions. It differs from the user-facing Lean injection tactic in the following ways:

• It does not introduce new propositions. Instead, the grind tactic preprocessor is responsible for introducing them.
• It assumes that fvarId is the latest local declaration in the current goal.
• It does not handle cases where the constructors are different because the simplifier already reduces such equalities to False.
• It does not have support for heterogeneous equality. Recall that the simplifier already reduces them to Eq if the types are definitionally equal.