Extensible, typeclass-driven `calc` in Lean 4

Calc.lean

class Trans (r : α → β → Prop) (s : β → γ → Prop) (t : outParam (α → γ → Prop)) where
  trans : r a b → s b c → t a c

export Trans (trans)

instance (r : α → γ → Prop) : Trans Eq r r where
  trans heq h' := heq ▸ h'

instance (r : α → β → Prop) : Trans r Eq r where
  trans h' heq := heq ▸ h'

notation "..." => _
-- enforce indentation of calc steps so we know when to stop parsing them
syntax calcStep := colGe term " := " term
syntax "calc " withPosition(calcStep+) : term

macro_rules
  | `(calc $p:term := $h) => `(($h : $p))
  | `(calc $p:term := $h $rest:calcStep*) => `(trans ($h : $p) (calc $rest:calcStep*))

variable (t1 t2 t3 t4 : Nat)
variable (pf12 : t1 = t2) (pf23 : t2 = t3) (pf34 : t3 = t4)

theorem foo : t1 = t4 :=
 calc
   t1 = t2 := pf12
   ... = t3 := pf23
   ... = t4 := pf34

variable (t5 : Nat)
variable (pf23' : t2 < t3) (pf45' : t4 < t5)

instance [HasLess α] : Trans (α := α) Less Less Less where
  trans := sorry

theorem foo' : t1 < t5 :=
 calc
   t1 = t2 := pf12
   ... < t3 := pf23'
   ... = t4 := pf34
   ... < t5 := pf45'