feat: pp.analyze isSubstLike support Eq.rec

src/Lean/PrettyPrinter/Delaborator/TopDownAnalyze.lean

@@ -216,7 +216,7 @@ def isFunLike (e : Expr) : MetaM Bool := do
   withTransparency TransparencyMode.all do forallTelescopeReducing (← inferType e) fun xs b => xs.size > 0
 
 def isSubstLike (e : Expr) : Bool :=
-  e.isAppOfArity `Eq.ndrec 6
+  e.isAppOfArity `Eq.ndrec 6 || e.isAppOfArity `Eq.rec 6
 
 def nameNotRoundtrippable (n : Name) : Bool :=
   n.hasMacroScopes || isPrivateName n || containsNum n

tests/lean/ppProofs.lean

@@ -1,3 +1,5 @@
+set_option pp.analyze.trustSubst true
+set_option pp.proofs false
 example (h : α = β) : h ▸ (a : α) = (b : β) := _
 example (h : α = β) : id h ▸ (a : α) = (b : β) := _
 example (h : α = β) : id h ▸ (a : α) = (b : β) := by simp