Lean4
/-- `grewrite [e]` works just like `rewrite [e]`, but `e` can be a relation other than `=` or `↔`.
For example,
```lean
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.
-/
@[tactic_parser 1000]
public meta def grewriteSeq : Lean.ParserDescr✝ :=
ParserDescr.node✝ `Mathlib.Tactic.grewriteSeq 1022
(ParserDescr.binary✝ `andthen
(ParserDescr.binary✝ `andthen
(ParserDescr.binary✝ `andthen (ParserDescr.nonReservedSymbol✝ "grewrite" false✝) Lean.Parser.Tactic.optConfig)
Lean.Parser.Tactic.rwRuleSeq)
(ParserDescr.unary✝ `optional Lean.Parser.Tactic.location))
