# mathlibdocumentation

core / init.meta.injection_tactic

meta def tactic.injection_with (h : expr) (ns : list name) (base : name := ) (offset : := some 1) :
meta def tactic.injection (h : expr) (base : name := ) (offset : := some 1) :

Simplify the equation h using injectivity of constructors. See injection_with. Returns the hypotheses that were added to the context, or an empty list if the goal was solved by contradiction.

meta def tactic.injections_with (ns : list name) (base : name := ) (offset : := some 1) :

Simplifies equations in the context using injectivity of constructors. For each equation h : C x₁ ... xₙ = D y₁ ... yₘ in the context, where C and D are constructors of the same data type, injections_with does the following:

• If C = D, it adds equations x₁ = y₁, ..., xₙ = yₙ.
• If C ≠ D, it solves the goal by contradiction.

See injection_with for details, including information about base and offset.

injections_with also recurses into the new equations xᵢ = yᵢ. If it has to recurse more than five times, it fails.