Recursive destructuring

Stream: Is there code for X?

[Robert Maxton]

Working in Mathlib.CategoryTheory, I often find myself opening proofs with lines like

refine
  ⟨fun F =>
    ⟨⟨⟨⟨?prod,
      fun {pt := X, ..} => ⟨?pi, ?nat⟩,
      ?commutes⟩,
    ⟨
      fun {pt := P', ..} => ?univ,
      fun {pt := P', ..} X => ?spec,
      fun {pt := P', ..} hom' spec' => ?unique⟩⟩⟩⟩⟩

Aside from being somewhat hard to read, it's also very mechanical and seems like it ought to be easily automated -- like rcongr, except instead of alternating between congr and ext we alternate between fconstructor and ext, maybe taking a using n modifier in case we want to stop halfway down. But rcases won't do it because many of these types aren't inductive, being instead some mix of quantifiers (Nonempty instances and forall/arrow types), and I didn't see any other tactics that seemed appropriate.

... There's an issue here with knowing where to stop, but it at least seems only tricky and not entirely insoluble (and if nothing else we could take the rcases approach and only expand as far as the user provides metavariables). I thought I'd at least check to see if I was missing anything before taking a crack at a rconstructor tactic myself.