`macro` と `macro_rules` の使用例: MILの min max 問題を解くタクティクを自作する

[Seasawher]

import Mathlib.Data.Real.Basic
import Mathlib.Tactic

section
variable (a b c d : ℝ)

open Lean Parser Elab Tactic

syntax "super_split" : tactic
macro_rules | `(tactic| super_split) => `(tactic| repeat split <;> super_split)

macro "minimax" : tactic => 
  `(tactic| with_reducible
    repeat rw [min_def _ _]
    repeat rw [max_def _ _]
    super_split
    all_goals linarith)

example : min a b = min b a := by
  minimax

example : max a b = max b a := by
  minimax

example : min (min a b) c = min a (min b c) := by
  minimax

example : max (max a b) c = max a (max b c) := by
  minimax

[Seasawher]

Mathlibに依存しない例にした方がいいね