case a
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
P : Finpartition s
F : Finset (Finset α)
ht : t ∈ F
hts : t ⊆ s
a : α
⊢ a ∈ Finset.biUnion (filter (fun u => u ⊆ t ∧ Finset.Nonempty u) (atomise s F).parts) id ↔ a ∈ t
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
P : Finpartition s
F : Finset (Finset α)
ht : t ∈ F
hts : t ⊆ s
⊢ Finset.biUnion (filter (fun u => u ⊆ t ∧ Finset.Nonempty u) (atomise s F).parts) id = t
ext a
case a
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
P : Finpartition s
F : Finset (Finset α)
ht : t ∈ F
hts : t ⊆ s
a : α
ha : a ∈ t
⊢ ∃ a_1, a_1 ∈ filter (fun u => u ⊆ t ∧ Finset.Nonempty u) (atomise s F).parts ∧ a ∈ id a_1
case a
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
P : Finpartition s
F : Finset (Finset α)
ht : t ∈ F
hts : t ⊆ s
a : α
⊢ a ∈ Finset.biUnion (filter (fun u => u ⊆ t ∧ Finset.Nonempty u) (atomise s F).parts) id ↔ a ∈ t
refine' mem_biUnion.trans ⟨fun ⟨u, hu, ha⟩ ↦ (mem_filter.1 hu).2.1 ha, fun ha ↦ _⟩
case a.intro.intro
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
P : Finpartition s
F : Finset (Finset α)
ht : t ∈ F
hts : t ⊆ s
a : α
ha : a ∈ t
u : Finset α
hu : u ∈ (atomise s F).parts
hau : a ∈ u
⊢ ∃ a_1, a_1 ∈ filter (fun u => u ⊆ t ∧ Finset.Nonempty u) (atomise s F).parts ∧ a ∈ id a_1
case a
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
P : Finpartition s
F : Finset (Finset α)
ht : t ∈ F
hts : t ⊆ s
a : α
ha : a ∈ t
⊢ ∃ a_1, a_1 ∈ filter (fun u => u ⊆ t ∧ Finset.Nonempty u) (atomise s F).parts ∧ a ∈ id a_1
obtain ⟨u, hu, hau⟩ := (atomise s F).exists_mem (hts ha)
case a.intro.intro
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
P : Finpartition s
F : Finset (Finset α)
ht : t ∈ F
hts : t ⊆ s
a : α
ha : a ∈ t
u : Finset α
hu : u ∈ (atomise s F).parts
hau : a ∈ u
b : α
hb : b ∈ u
⊢ b ∈ t
case a.intro.intro
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
P : Finpartition s
F : Finset (Finset α)
ht : t ∈ F
hts : t ⊆ s
a : α
ha : a ∈ t
u : Finset α
hu : u ∈ (atomise s F).parts
hau : a ∈ u
⊢ ∃ a_1, a_1 ∈ filter (fun u => u ⊆ t ∧ Finset.Nonempty u) (atomise s F).parts ∧ a ∈ id a_1
refine' ⟨u, mem_filter.2 ⟨hu, fun b hb ↦ _, _, hau⟩, hau⟩
case a.intro.intro.intro.intro
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
P : Finpartition s
F : Finset (Finset α)
ht : t ∈ F
hts : t ⊆ s
a : α
ha : a ∈ t
b : α
Q : Finset (Finset α)
_hQ : Q ⊆ F
hu : filter (fun i => ∀ (u : Finset α), u ∈ F → (u ∈ Q ↔ i ∈ u)) s ∈ (atomise s F).parts
hau : a ∈ filter (fun i => ∀ (u : Finset α), u ∈ F → (u ∈ Q ↔ i ∈ u)) s
hb : b ∈ filter (fun i => ∀ (u : Finset α), u ∈ F → (u ∈ Q ↔ i ∈ u)) s
⊢ b ∈ t
case a.intro.intro
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
P : Finpartition s
F : Finset (Finset α)
ht : t ∈ F
hts : t ⊆ s
a : α
ha : a ∈ t
u : Finset α
hu : u ∈ (atomise s F).parts
hau : a ∈ u
b : α
hb : b ∈ u
⊢ b ∈ t
obtain ⟨Q, _hQ, rfl⟩ := (mem_atomise.1 hu).2
case a.intro.intro.intro.intro
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
P : Finpartition s
F : Finset (Finset α)
ht : t ∈ F
hts : t ⊆ s
a : α
ha : a ∈ t
b : α
Q : Finset (Finset α)
_hQ : Q ⊆ F
hu : filter (fun i => ∀ (u : Finset α), u ∈ F → (u ∈ Q ↔ i ∈ u)) s ∈ (atomise s F).parts
hau : a ∈ s ∧ ∀ (u : Finset α), u ∈ F → (u ∈ Q ↔ a ∈ u)
hb : b ∈ s ∧ ∀ (u : Finset α), u ∈ F → (u ∈ Q ↔ b ∈ u)
⊢ b ∈ t
case a.intro.intro.intro.intro
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
P : Finpartition s
F : Finset (Finset α)
ht : t ∈ F
hts : t ⊆ s
a : α
ha : a ∈ t
b : α
Q : Finset (Finset α)
_hQ : Q ⊆ F
hu : filter (fun i => ∀ (u : Finset α), u ∈ F → (u ∈ Q ↔ i ∈ u)) s ∈ (atomise s F).parts
hau : a ∈ filter (fun i => ∀ (u : Finset α), u ∈ F → (u ∈ Q ↔ i ∈ u)) s
hb : b ∈ filter (fun i => ∀ (u : Finset α), u ∈ F → (u ∈ Q ↔ i ∈ u)) s
⊢ b ∈ t
rw [mem_filter] at hau hb
no goals
case a.intro.intro.intro.intro
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
P : Finpartition s
F : Finset (Finset α)
ht : t ∈ F
hts : t ⊆ s
a : α
ha : a ∈ t
b : α
Q : Finset (Finset α)
_hQ : Q ⊆ F
hu : filter (fun i => ∀ (u : Finset α), u ∈ F → (u ∈ Q ↔ i ∈ u)) s ∈ (atomise s F).parts
hau : a ∈ s ∧ ∀ (u : Finset α), u ∈ F → (u ∈ Q ↔ a ∈ u)
hb : b ∈ s ∧ ∀ (u : Finset α), u ∈ F → (u ∈ Q ↔ b ∈ u)
⊢ b ∈ t
rwa [← hb.2 _ ht, hau.2 _ ht]