Lean4
/-- `grw [e]` works just like `rw [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
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.
-/
@[tactic_parser 1000]
public meta def grwSeq : Lean.ParserDescr✝ :=
ParserDescr.node✝ `Mathlib.Tactic.grwSeq 1022
(ParserDescr.binary✝ `andthen
(ParserDescr.binary✝ `andthen
(ParserDescr.binary✝ `andthen (ParserDescr.nonReservedSymbol✝ "grw " false✝) Lean.Parser.Tactic.optConfig)
Lean.Parser.Tactic.rwRuleSeq)
(ParserDescr.unary✝ `optional Lean.Parser.Tactic.location))
