The erw? tactic

erw? [r, ...] calls erw [r, ...] (at hypothesis h if written erw [r, ...] at h), and then attempts to identify any subexpression which would block the use of rw instead. It does so by identifying subexpressions which are defeq, but not at reducible transparency.

opaque Mathlib.Tactic.Erw?.tactic.erw?.verbose : Lean.Option Bool

If set to true, erw? will log more information as it attempts to identify subexpressions which would block the use of rw instead.

def Mathlib.Tactic.Erw?.erw? : Lean.ParserDescr

erw? [r, ...] calls erw [r, ...] (at hypothesis h if written erw [r, ...] at h), and then attempts to identify any subexpression which would block the use of rw instead. It does so by identifying subexpressions which are defeq, but not at reducible transparency.

def Mathlib.Tactic.Erw?.logDiffs (tk : Lean.Syntax) (e₁ e₂ : Lean.Expr) : StateT (Array (Unit → Lean.MessageData)) Lean.MetaM Bool

Check if two expressions are different at reducible transparency. Attempt to log an info message for the first subexpressions which are different (but agree at default transparency).

Also returns an array of messages for the verbose report.

def Mathlib.Tactic.Erw?.extractRewriteEq (e : Lean.Expr) : Lean.MetaM (Lean.Expr × Lean.Expr)

Checks that the input Expr represents a proof produced by (e)rw and returns the types of the LHS of the equality being written (one from the target, the other from the lemma used). These will be defeq, but not necessarily reducibly so.

def Mathlib.Tactic.Erw?.extractRewriteHypEq (e : Lean.Expr) : Lean.MetaM Lean.Expr

Checks that the input Expr represents a proof produced by (e)rw at and returns the type of the LHS of the equality (from the lemma used). This will be defeq to the hypothesis being written, but not necessarily reducibly so.