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)

def Lean.Expr.relSidesIfSymm? (e : Lean.Expr) : Lean.MetaM (Option (Lean.Name × Lean.Expr × Lean.Expr))

If e is the form @R .. x y, where R is a symmetric relation, return some (R, x, y). As a special case, if e is @HEq α a β b, return some (`HEq, a, b).

Equations

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