The simp_rw tactic

This file defines the simp_rw tactic: it functions as a mix of simp and rw. Like rw, it applies each rewrite rule in the given order, but like simp it repeatedly applies these rules and also under binders like ∀ x, ..., ∃ x, ... and fun x ↦ ....

def Mathlib.Tactic.withSimpRWRulesSeq (token rwRulesSeqStx : Lean.Syntax) (x : Bool → Lean.Syntax → Lean.Elab.Tactic.TacticM Unit) : Lean.Elab.Tactic.TacticM Unit

A version of withRWRulesSeq (in core) that doesn't attempt to find equation lemmas, and simply passes the rw rules on to x.

def Mathlib.Tactic.tacticSimp_rw___ : Lean.ParserDescr

simp_rw functions as a mix of simp and rw. Like rw, it applies each rewrite rule in the given order, but like simp it repeatedly applies these rules and also under binders like ∀ x, ..., ∃ x, ... and fun x ↦.... Usage:

• simp_rw [lemma_1, ..., lemma_n] will rewrite the goal by applying the lemmas in that order. A lemma preceded by ← is applied in the reverse direction.
• simp_rw [lemma_1, ..., lemma_n] at h₁ ... hₙ will rewrite the given hypotheses.
• simp_rw [...] at * rewrites in the whole context: all hypotheses and the goal.

Lemmas passed to simp_rw must be expressions that are valid arguments to simp. For example, neither simp nor rw can solve the following, but simp_rw can:

example {a : ℕ}
    (h1 : ∀ a b : ℕ, a - 1 ≤ b ↔ a ≤ b + 1)
    (h2 : ∀ a b : ℕ, a ≤ b ↔ ∀ c, c < a → c < b) :
    (∀ b, a - 1 ≤ b) = ∀ b c : ℕ, c < a → c < b + 1 := by
  simp_rw [h1, h2]