α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
P : Finpartition s
a : α
ha : a ∈ sup P.parts id
⊢ ∃ t, t ∈ P.parts ∧ a ∈ t
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
P : Finpartition s
a : α
ha : a ∈ s
⊢ ∃ t, t ∈ P.parts ∧ a ∈ t
simp_rw [← P.supParts] at ha
no goals
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
P : Finpartition s
a : α
ha : a ∈ sup P.parts id
⊢ ∃ t, t ∈ P.parts ∧ a ∈ t
exact mem_sup.1 ha