structure Lean.Elab.Tactic.Do.ProofMode.FocusResult : Type

The result of focusing the context of a goal goal : MGoal on a particular hypothesis. The focused hypothesis is returned as focusHyp : Expr, along with the residual restHyps : Expr and a proof : Expr for the property goal.hyps ⊣⊢ₛ restHyps ∧ focusHyp.

• focusHyp : Expr
• restHyps : Expr
• proof : Expr

instance Lean.Elab.Tactic.Do.ProofMode.instInhabitedFocusResult : Inhabited FocusResult

Equations

• Lean.Elab.Tactic.Do.ProofMode.instInhabitedFocusResult = { default := { focusHyp := default, restHyps := default, proof := default } }

partial def Lean.Elab.Tactic.Do.ProofMode.focusHyp (u : Level) (σs e : Expr) (name : Name) : Option FocusResult

def Lean.Elab.Tactic.Do.ProofMode.MGoal.focusHyp (goal : MGoal) (name : Name) : Option FocusResult

Equations

• goal.focusHyp name = Lean.Elab.Tactic.Do.ProofMode.focusHyp goal.u goal.σs goal.hyps name

def Lean.Elab.Tactic.Do.ProofMode.FocusResult.refl (u : Level) (σs restHyps focusHyp : Expr) : FocusResult

Equations

• One or more equations did not get rendered due to their size.

def Lean.Elab.Tactic.Do.ProofMode.FocusResult.restGoal (res : FocusResult) (goal : MGoal) : MGoal

Equations

• res.restGoal goal = { u := goal.u, σs := goal.σs, hyps := res.restHyps, target := goal.target }

def Lean.Elab.Tactic.Do.ProofMode.FocusResult.recombineGoal (res : FocusResult) (goal : MGoal) : MGoal

Equations

• res.recombineGoal goal = { u := goal.u, σs := goal.σs, hyps := Lean.Elab.Tactic.Do.ProofMode.SPred.mkAnd! goal.u goal.σs res.restHyps res.focusHyp, target := goal.target }

def Lean.Elab.Tactic.Do.ProofMode.FocusResult.rewriteHyps (res : FocusResult) (goal : MGoal) : Expr → Expr

Turn a proof for (res.recombineGoal goal).toExpr into one for goal.toExpr.

Equations

• One or more equations did not get rendered due to their size.

def Lean.Elab.Tactic.Do.ProofMode.MGoal.focusHypWithInfo (goal : MGoal) (name : Ident) : MetaM FocusResult

Equations

• One or more equations did not get rendered due to their size.