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.

Equations

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

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.

Equations

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

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

Function elaborating GRewrite.Config.

Equations

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

def Mathlib.Tactic.grewriteSeq : Lean.ParserDescr

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

For example,

variable {a b c d n : ℤ}

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₂ : b ∣ a ^ 2 * c) : a ∣ b ^ 2 * c := by
  grewrite [h₁] at *
  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.

Equations

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

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,

variable {a b c d n : ℤ}

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₂ : b ∣ a ^ 2 * c) : a ∣ b ^ 2 * c := by
  grewrite [h₁] at *
  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.

Equations

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

def Mathlib.Tactic.grwSeq : Lean.ParserDescr

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

For example,

variable {a b c d n : ℤ}

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₂ : b ∣ a ^ 2 * c) : a ∣ b ^ 2 * c := by
  grw [h₁] at *
  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.

Equations

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

def Mathlib.Tactic.tacticApply_rewrite___ : Lean.ParserDescr

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

Equations

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

def Mathlib.Tactic.applyRwSeq : Lean.ParserDescr

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

Equations

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

def Mathlib.Tactic.tacticNth_grewrite_____ : Lean.ParserDescr

nth_grewrite is just like nth_rewrite, but for grewrite.

Equations

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

def Mathlib.Tactic.tacticNth_grw_____ : Lean.ParserDescr

nth_grw is just like nth_rw, but for grw.

Equations

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