simp_intro tactic

partial def Mathlib.Tactic.simpIntroCore (g : Lean.MVarId) (ctx : Lean.Meta.Simp.Context) (simprocs : Lean.Meta.Simp.SimprocsArray := #[]) (discharge? : Option Lean.Meta.Simp.Discharge) (more : Bool) (ids : List (Lean.TSyntax `Lean.binderIdent)) : Lean.Elab.TermElabM (Option Lean.MVarId)

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

def Mathlib.Tactic.«tacticSimp_intro_____..Only_» : Lean.ParserDescr

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.