The generalized rewriting tactic

This file defines the tactics that use the backend defined in Mathlib.Tactic.GRewrite.Core:

• grewrite
• grw
• apply_rw
• nth_grewrite
• nth_grw

def Mathlib.Tactic.grewriteTarget (stx : Lean.Syntax) (symm : Bool) (config : GRewrite.Config) : Lean.Elab.Tactic.TacticM Unit

Apply the grewrite tactic to the current goal.

def Mathlib.Tactic.grewriteLocalDecl (stx : Lean.Syntax) (symm : Bool) (fvarId : Lean.FVarId) (config : GRewrite.Config) : Lean.Elab.Tactic.TacticM Unit

Apply the grewrite tactic to a local hypothesis.

def Mathlib.Tactic.elabGRewriteConfig : Lean.Syntax → Lean.Elab.Tactic.TacticM GRewrite.Config

Function elaborating GRewrite.Config.

def Mathlib.Tactic.grewriteSeq : Lean.ParserDescr

grewrite [e] works just like rewrite [e], but e can be a relation other than = or ↔.

For example,

example (h₁ : a < b) (h₂ : b ≤ c) : a + d ≤ c + d := by
  grewrite [h₁, h₂]; rfl

example (h : a ≡ b [ZMOD n]) : a ^ 2 ≡ b ^ 2 [ZMOD n] := by
  grewrite [h]; rfl

example : (h₁ : a ∣ b) (h₂ : c ∣ a * d) : a ∣ b * d := by
  grewrite [h₁]
  exact h₂

To be able to use grewrite, the relevant lemmas need to be tagged with @[gcongr]. To rewrite inside a transitive relation, you can also give it an IsTrans instance.

def Mathlib.Tactic.evalGRewriteSeq : Lean.Elab.Tactic.Tactic

grewrite [e] works just like rewrite [e], but e can be a relation other than = or ↔.

For example,

example (h₁ : a < b) (h₂ : b ≤ c) : a + d ≤ c + d := by
  grewrite [h₁, h₂]; rfl

example (h : a ≡ b [ZMOD n]) : a ^ 2 ≡ b ^ 2 [ZMOD n] := by
  grewrite [h]; rfl

example : (h₁ : a ∣ b) (h₂ : c ∣ a * d) : a ∣ b * d := by
  grewrite [h₁]
  exact h₂

To be able to use grewrite, the relevant lemmas need to be tagged with @[gcongr]. To rewrite inside a transitive relation, you can also give it an IsTrans instance.

def Mathlib.Tactic.rwSeq : Lean.ParserDescr

grw [e] works just like rw [e], but e can be a relation other than = or ↔.

For example,

example (h₁ : a < b) (h₂ : b ≤ c) : a + d ≤ c + d := by
  grw [h₁, h₂]

example (h : a ≡ b [ZMOD n]) : a ^ 2 ≡ b ^ 2 [ZMOD n] := by
  grw [h]

example : (h₁ : a ∣ b) (h₂ : c ∣ a * d) : a ∣ b * d := by
  grw [h₁]
  exact h₂

To be able to use grw, the relevant lemmas need to be tagged with @[gcongr]. To rewrite inside a transitive relation, you can also give it an IsTrans instance.

def Mathlib.Tactic.tacticApply_rewrite___ : Lean.ParserDescr

apply_rewrite [rules] is a shorthand for grewrite +implicationHyp [rules].

def Mathlib.Tactic.applyRwSeq : Lean.ParserDescr

apply_rw [rules] is a shorthand for grw +implicationHyp [rules].

def Mathlib.Tactic.tacticNth_grewrite_____ : Lean.ParserDescr

nth_grewrite is just like nth_rewrite, but for grewrite.

def Mathlib.Tactic.tacticNth_grw_____ : Lean.ParserDescr

nth_grw is just like nth_rw, but for grw.