mathlib documentation

core / init.meta.injection_tactic

meta def tactic.injection (h : expr) (base : name := name.mk_string "h" name.anonymous) (offset : option := 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.

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.