simp only [Finset.mem_univ, ne_eq, Finite.disjoint_toFinset, forall_true_left]
case inr.refine_1
α : Type u_1
β : Type u_2
s✝ t : Set α
n : ℕ
ι : Type u_3
inst✝ : Fintype ι
s : ι → Set α
hs : univ.PairwiseDisjoint s
h : ∀ (x : ι), (s x).Finite
⊢ ∀ x ∈ Finset.univ, ∀ y ∈ Finset.univ, x ≠ y → Disjoint ((fun i => ⋯.toFinset) x) ((fun i => ⋯.toFinset) y)
case inr.refine_1
α : Type u_1
β : Type u_2
s✝ t : Set α
n : ℕ
ι : Type u_3
inst✝ : Fintype ι
s : ι → Set α
hs : univ.PairwiseDisjoint s
h : ∀ (x : ι), (s x).Finite
⊢ ∀ (x y : ι), ¬x = y → Disjoint (s x) (s y)