# Documentation

Mathlib.Tactic.SimpIntro

# simp_intro tactic #

partial def Mathlib.Tactic.simpIntroCore (g : Lean.MVarId) (ctx : Lean.Meta.Simp.Context) (discharge? : ) (more : Bool) (ids : List (Lean.TSyntax Lean.binderIdent)) :

Main loop of the simp_intro tactic.

• g: the original goal
• ctx: the simp context, which is extended with local variables as we enter the binders
• discharge?: the discharger
• more: if true, we will keep introducing binders as long as we can
• ids: the list of binder identifiers

The simp_intro tactic is a combination of simp and intro: it will simplify the types of variables as it introduces them and uses the new variables to simplify later arguments and the goal.

• simp_intro x y z introduces variables named x y z
• simp_intro x y z .. introduces variables named x y z and then keeps introducing _ binders
• simp_intro (config := cfg) (discharger := tac) x y .. only [h₁, h₂]: simp_intro takes the same options as simp (see simp)
example : x + 0 = y → x = z := by
simp_intro h
-- h: x = y ⊢ y = z
sorry
`
Equations
• One or more equations did not get rendered due to their size.