-- Mathlib/Order/Partition/Finpartition.lean
theorem biUnion_filter_atomise (ht : t ∈ F) (hts : t ⊆ s) :
    {u ∈ (atomise s F).parts | u ⊆ t ∧ u.Nonempty}.biUnion id = t

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
F : Finset (Finset α)
ht : t ∈ F
hts : t ⊆ s
⊢ (filter (fun u => u ⊆ t ∧ u.Nonempty) (atomise s F).parts).biUnion id = t

Tactic:
ext a

Result:
case h
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
F : Finset (Finset α)
ht : t ∈ F
hts : t ⊆ s
a : α
⊢ a ∈ (filter (fun u => u ⊆ t ∧ u.Nonempty) (atomise s F).parts).biUnion id ↔ a ∈ t

Proof state:
case h.intro.intro
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
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

Tactic:
obtain ⟨Q, _hQ, rfl⟩ := (mem_atomise.1 hu).2

Result:
case h.intro.intro.intro.intro
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
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 ∈ F, u ∈ Q ↔ i ∈ u) s ∈ (atomise s F).parts
hau : a ∈ filter (fun i => ∀ u ∈ F, u ∈ Q ↔ i ∈ u) s
hb : b ∈ filter (fun i => ∀ u ∈ F, u ∈ Q ↔ i ∈ u) s
⊢ b ∈ t

Proof state:
case h.intro.intro
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
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 ∈ filter (fun u => u ⊆ t ∧ u.Nonempty) (atomise s F).parts, a ∈ id a_1

Tactic:
refine ⟨u, mem_filter.2 ⟨hu, fun b hb ↦ ?_, _, hau⟩, hau⟩

Result:
case h.intro.intro
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
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

Proof state:
case h
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
F : Finset (Finset α)
ht : t ∈ F
hts : t ⊆ s
a : α
⊢ a ∈ (filter (fun u => u ⊆ t ∧ u.Nonempty) (atomise s F).parts).biUnion id ↔ a ∈ t

Tactic:
refine mem_biUnion.trans ⟨fun ⟨u, hu, ha⟩ ↦ (mem_filter.1 hu).2.1 ha, fun ha ↦ ?_⟩

Result:
case h
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
F : Finset (Finset α)
ht : t ∈ F
hts : t ⊆ s
a : α
ha : a ∈ t
⊢ ∃ a_1 ∈ filter (fun u => u ⊆ t ∧ u.Nonempty) (atomise s F).parts, a ∈ id a_1

Proof state:
case h
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
F : Finset (Finset α)
ht : t ∈ F
hts : t ⊆ s
a : α
ha : a ∈ t
⊢ ∃ a_1 ∈ filter (fun u => u ⊆ t ∧ u.Nonempty) (atomise s F).parts, a ∈ id a_1

Tactic:
obtain ⟨u, hu, hau⟩ := (atomise s F).exists_mem (hts ha)

Result:
case h.intro.intro
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
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 ∈ filter (fun u => u ⊆ t ∧ u.Nonempty) (atomise s F).parts, a ∈ id a_1

Proof state:
case h.intro.intro.intro.intro
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
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 ∈ F, u ∈ Q ↔ i ∈ u) s ∈ (atomise s F).parts
hau : a ∈ filter (fun i => ∀ u ∈ F, u ∈ Q ↔ i ∈ u) s
hb : b ∈ filter (fun i => ∀ u ∈ F, u ∈ Q ↔ i ∈ u) s
⊢ b ∈ t

Tactic:
rw [mem_filter] at hau hb

Result:
case h.intro.intro.intro.intro
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
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 ∈ F, u ∈ Q ↔ i ∈ u) s ∈ (atomise s F).parts
hau : a ∈ s ∧ ∀ u ∈ F, u ∈ Q ↔ a ∈ u
hb : b ∈ s ∧ ∀ u ∈ F, u ∈ Q ↔ b ∈ u
⊢ b ∈ t

Proof state:
case h.intro.intro.intro.intro
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
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 ∈ F, u ∈ Q ↔ i ∈ u) s ∈ (atomise s F).parts
hau : a ∈ s ∧ ∀ u ∈ F, u ∈ Q ↔ a ∈ u
hb : b ∈ s ∧ ∀ u ∈ F, u ∈ Q ↔ b ∈ u
⊢ b ∈ t

Tactic:
rwa [← hb.2 _ ht, hau.2 _ ht]

Result:
no goals