linter.fugue.existsIntro

exists w₁, w₂ supplies the witnesses for an existential goal and leaves what remains as the goal — no ?_ to count, no closing ⟩ to match, and it descends through ∧. refine ⟨w₁, w₂, ?_, …⟩ on a goal whose head is Exists, with every hole trailing and bare, is that pattern spelled the long way.

use is the sibling to reach for when exists's trailing try trivial would close a goal that should stay open (it discharges at reducible transparency, and use (discharger := skip) turns it off), or when the last conjunct also needs supplying (exists must leave one goal, use need not). Both also split ∧ and any one-constructor structure/inductive — but this linter flags only an Exists-headed goal (see the note in existsIntroCore).

A hole nested in a term (Or.inr ?_, λ i ↦ ?_) has no exists/use spelling, so an element that is not either hole-free or a bare ?_/_ disqualifies the whole refine. The existential check is semantic — the goal the refine faced.