α : Type u_1
c : Set (Set α)
hc : IsPartition c
x : α
t : Set α
ht : (∃ x_1, x ∈ t) ∧ ∀ (y : Set α), (∃ x_1, x ∈ y) → y = t
⊢ t ∈ c ∧ x ∈ t
α : Type u_1
c : Set (Set α)
hc : IsPartition c
x : α
t : Set α
ht : (fun b => ∃! x_1, x ∈ b) t ∧ ∀ (y : Set α), (fun b => ∃! x_1, x ∈ b) y → y = t
⊢ t ∈ c ∧ x ∈ t
simp only [exists_unique_iff_exists] at ht
no goals
α : Type u_1
c : Set (Set α)
hc : IsPartition c
x : α
t : Set α
ht : (∃ x_1, x ∈ t) ∧ ∀ (y : Set α), (∃ x_1, x ∈ y) → y = t
⊢ t ∈ c ∧ x ∈ t
tauto