symm_saturate tactic

For every hypothesis h : a ~ b where a @[symm] lemma is available, add a hypothesis h_symm : b ~ a.

def Lean.MVarId.symmSaturate (g : Lean.MVarId) : Lean.MetaM Lean.MVarId

For every hypothesis h : a ~ b where a @[symm] lemma is available, add a hypothesis h_symm : b ~ a.

Equations

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

def Mathlib.Tactic.tacticSymm_saturate : Lean.ParserDescr

For every hypothesis h : a ~ b where a @[symm] lemma is available, add a hypothesis h_symm : b ~ a.

Equations

• Mathlib.Tactic.tacticSymm_saturate = Lean.ParserDescr.node `Mathlib.Tactic.tacticSymm_saturate 1024 (Lean.ParserDescr.nonReservedSymbol "symm_saturate" false)