-- Mathlib/Order/Partition/Finpartition.lean
theorem card_filter_atomise_le_two_pow (ht : t ∈ F) :
    #{u ∈ (atomise s F).parts | u ⊆ t ∧ u.Nonempty} ≤ 2 ^ (#F - 1)

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
F : Finset (Finset α)
ht : t ∈ F
i : α
P : Finset (Finset α)
PQ : P ⊆ F
hi : i ∈ filter (fun i => ∀ u ∈ F, u ∈ P ↔ i ∈ u) s
hy₂ : filter (fun i => ∀ u ∈ F, u ∈ P ↔ i ∈ u) s ⊆ t
j : α
_hj : j ∈ filter (fun i => ∀ u ∈ F, u ∈ P ↔ i ∈ u) s
⊢ filter (fun i => ∀ x ∈ F, x ∈ insert t (P.erase t) ↔ i ∈ x) s = filter (fun i => ∀ u ∈ F, u ∈ P ↔ i ∈ u) s

Tactic:
simp only [insert_erase (((mem_filter.1 hi).2 _ ht).2 <| hy₂ hi)]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
F : Finset (Finset α)
ht : t ∈ F
⊢ ∀ ⦃x : Finset α⦄,
    x ∈ filter (fun u => u ⊆ t ∧ u.Nonempty) (atomise s F).parts →
      x ∈ image (fun P => filter (fun i => ∀ x ∈ F, x ∈ insert t P ↔ i ∈ x) s) (F.erase t).powerset

Tactic:
simp_rw [mem_image, mem_powerset, mem_filter, and_imp, Finset.Nonempty, exists_imp, mem_atomise,
  and_imp, Finset.Nonempty, exists_imp, and_imp]

Result:
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
F : Finset (Finset α)
ht : t ∈ F
⊢ ∀ ⦃x : Finset α⦄,
    ∀ x_1 ∈ x,
      ∀ x_2 ⊆ F,
        filter (fun i => ∀ u ∈ F, u ∈ x_2 ↔ i ∈ u) s = x →
          x ⊆ t → ∀ x_3 ∈ x, ∃ a ⊆ F.erase t, filter (fun i => ∀ x ∈ F, x ∈ insert t a ↔ i ∈ x) s = x

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
F : Finset (Finset α)
ht : t ∈ F
i : α
P : Finset (Finset α)
PQ : P ⊆ F
hi : i ∈ filter (fun i => ∀ u ∈ F, u ∈ P ↔ i ∈ u) s
hy₂ : filter (fun i => ∀ u ∈ F, u ∈ P ↔ i ∈ u) s ⊆ t
j : α
_hj : j ∈ filter (fun i => ∀ u ∈ F, u ∈ P ↔ i ∈ u) s
⊢ ∃ a ⊆ F.erase t, filter (fun i => ∀ x ∈ F, x ∈ insert t a ↔ i ∈ x) s = filter (fun i => ∀ u ∈ F, u ∈ P ↔ i ∈ u) s

Tactic:
refine ⟨P.erase t, erase_subset_erase _ PQ, ?_⟩

Result:
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
F : Finset (Finset α)
ht : t ∈ F
i : α
P : Finset (Finset α)
PQ : P ⊆ F
hi : i ∈ filter (fun i => ∀ u ∈ F, u ∈ P ↔ i ∈ u) s
hy₂ : filter (fun i => ∀ u ∈ F, u ∈ P ↔ i ∈ u) s ⊆ t
j : α
_hj : j ∈ filter (fun i => ∀ u ∈ F, u ∈ P ↔ i ∈ u) s
⊢ filter (fun i => ∀ x ∈ F, x ∈ insert t (P.erase t) ↔ i ∈ x) s = filter (fun i => ∀ u ∈ F, u ∈ P ↔ i ∈ u) s

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
F : Finset (Finset α)
ht : t ∈ F
h :
  filter (fun u => u ⊆ t ∧ u.Nonempty) (atomise s F).parts ⊆
    image (fun P => filter (fun i => ∀ x ∈ F, x ∈ insert t P ↔ i ∈ x) s) (F.erase t).powerset
⊢ #(filter (fun u => u ⊆ t ∧ u.Nonempty) (atomise s F).parts) ≤ 2 ^ (#F - 1)

Tactic:
refine (card_le_card h).trans (card_image_le.trans ?_)

Result:
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
F : Finset (Finset α)
ht : t ∈ F
h :
  filter (fun u => u ⊆ t ∧ u.Nonempty) (atomise s F).parts ⊆
    image (fun P => filter (fun i => ∀ x ∈ F, x ∈ insert t P ↔ i ∈ x) s) (F.erase t).powerset
⊢ #(F.erase t).powerset ≤ 2 ^ (#F - 1)

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
F : Finset (Finset α)
ht : t ∈ F
⊢ #(filter (fun u => u ⊆ t ∧ u.Nonempty) (atomise s F).parts) ≤ 2 ^ (#F - 1)

Tactic:
suffices h :
  {u ∈ (atomise s F).parts | u ⊆ t ∧ u.Nonempty} ⊆
    (F.erase t).powerset.image fun P ↦ {i ∈ s | ∀ x ∈ F, x ∈ insert t P ↔ i ∈ x} by
  refine (card_le_card h).trans (card_image_le.trans ?_)
  rw [card_powerset, card_erase_of_mem ht]

Result:
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
F : Finset (Finset α)
ht : t ∈ F
⊢ filter (fun u => u ⊆ t ∧ u.Nonempty) (atomise s F).parts ⊆
    image (fun P => filter (fun i => ∀ x ∈ F, x ∈ insert t P ↔ i ∈ x) s) (F.erase t).powerset

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
F : Finset (Finset α)
ht : t ∈ F
⊢ filter (fun u => u ⊆ t ∧ u.Nonempty) (atomise s F).parts ⊆
    image (fun P => filter (fun i => ∀ x ∈ F, x ∈ insert t P ↔ i ∈ x) s) (F.erase t).powerset

Tactic:
rw [subset_iff]

Result:
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
F : Finset (Finset α)
ht : t ∈ F
⊢ ∀ ⦃x : Finset α⦄,
    x ∈ filter (fun u => u ⊆ t ∧ u.Nonempty) (atomise s F).parts →
      x ∈ image (fun P => filter (fun i => ∀ x ∈ F, x ∈ insert t P ↔ i ∈ x) s) (F.erase t).powerset

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
F : Finset (Finset α)
ht : t ∈ F
⊢ ∀ ⦃x : Finset α⦄,
    ∀ x_1 ∈ x,
      ∀ x_2 ⊆ F,
        filter (fun i => ∀ u ∈ F, u ∈ x_2 ↔ i ∈ u) s = x →
          x ⊆ t → ∀ x_3 ∈ x, ∃ a ⊆ F.erase t, filter (fun i => ∀ x ∈ F, x ∈ insert t a ↔ i ∈ x) s = x

Tactic:
rintro P' i hi P PQ rfl hy₂ j _hj

Result:
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
F : Finset (Finset α)
ht : t ∈ F
i : α
P : Finset (Finset α)
PQ : P ⊆ F
hi : i ∈ filter (fun i => ∀ u ∈ F, u ∈ P ↔ i ∈ u) s
hy₂ : filter (fun i => ∀ u ∈ F, u ∈ P ↔ i ∈ u) s ⊆ t
j : α
_hj : j ∈ filter (fun i => ∀ u ∈ F, u ∈ P ↔ i ∈ u) s
⊢ ∃ a ⊆ F.erase t, filter (fun i => ∀ x ∈ F, x ∈ insert t a ↔ i ∈ x) s = filter (fun i => ∀ u ∈ F, u ∈ P ↔ i ∈ u) s

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
F : Finset (Finset α)
ht : t ∈ F
h :
  filter (fun u => u ⊆ t ∧ u.Nonempty) (atomise s F).parts ⊆
    image (fun P => filter (fun i => ∀ x ∈ F, x ∈ insert t P ↔ i ∈ x) s) (F.erase t).powerset
⊢ #(F.erase t).powerset ≤ 2 ^ (#F - 1)

Tactic:
rw [card_powerset, card_erase_of_mem ht]

Result:
no goals