no goals
α : Type u_1
c : Set (Set α)
hc : IsPartition c
s : Set α
x✝ : s ∈ classes (mkClasses c (_ : ∀ (a : α), ∃! b x, a ∈ b))
y : α
hs : s = {x | Rel (mkClasses c (_ : ∀ (a : α), ∃! b x, a ∈ b)) x y}
b : Set α
hm : b ∈ c
hb : y ∈ b
_hy : ∀ (y_1 : Set α), y_1 ∈ c → y ∈ y_1 → y_1 = b
⊢ s ∈ c
rwa [show s = b from hs.symm ▸ Set.ext fun x =>
  ⟨fun hx => symm' (mkClasses c hc.2) hx b hm hb, fun hx b' hc' hx' =>
      eq_of_mem_eqv_class hc.2 hm hx hc' hx' ▸ hb⟩]