Elided props in binders

Stream: mathlib4

[Yaël Dillies]

Houston, we've got a problem:

import Mathlib.Data.Finset.Lattice

#check Finset.supᵢ_bunionᵢ
/-
Finset.supᵢ_bunionᵢ.{u_3, u_2, u_1} {α : Type u_2} {β : Type u_3} {γ : Type u_1} [inst✝ : CompleteLattice β]
  [inst✝¹ : DecidableEq α] (s : Finset γ) (t : γ → Finset α) (f : α → β) : (⨆ y, ⨆ h, f y) = ⨆ x, ⨆ h, ⨆ y, ⨆ h, f y
-/

[Yaël Dillies]

The statement ((⨆ y ∈ s.bunionᵢ t, f y) = ⨆ (x ∈ s) (y ∈ t x), f y) is completely mangled in printing (goal state, #check, docs4#Finset.supᵢ_bunionᵢ) because the Props the suprema are running over get elided.

[Kyle Miller]

Here's a delaborator to at least show the domain when the variable is a proof:

import Mathlib.Data.Finset.Lattice

open Lean Lean.PrettyPrinter.Delaborator in
@[delab app.supᵢ]
def supᵢ_delab : Delab := do
  let #[_, _, ι, f] := (← SubExpr.getExpr).getAppArgs | failure
  unless (← Meta.isProp ι) && f.isLambda do failure
  SubExpr.withAppArg do
    let dom ← SubExpr.withBindingDomain delab
    withBindingBodyUnusedName $ fun x => do
      let body ← delab
      `(⨆ ($(.mk x):ident : $dom), $body)

#check Finset.supᵢ_bunionᵢ
/-
Finset.supᵢ_bunionᵢ.{u_3, u_2, u_1} {α : Type u_2} {β : Type u_3} {γ : Type u_1} [inst✝ : CompleteLattice β]
  [inst✝¹ : DecidableEq α] (s : Finset γ) (t : γ → Finset α) (f : α → β) :
  (⨆ y, ⨆ (h : y ∈ Finset.bunionᵢ s t), f y) = ⨆ x, ⨆ (h : x ∈ s), ⨆ y, ⨆ (h : y ∈ t x), f y
-/

[Yaël Dillies]

Nice! Do you think we can recover Lean 3's binder collecting behavior?