ι : Type u_1
α : Type u_2
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : Nonempty α
s : Finset ι
f : ι → Finset (Finset α)
hf : ∀ (i : ι), i ∈ s → Set.Intersecting ↑(f i)
this : DecidableEq ι
⊢ card (Finset.biUnion s f) ≤ 2 ^ Fintype.card α - 2 ^ (Fintype.card α - card s)
ι : Type u_1
α : Type u_2
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : Nonempty α
s : Finset ι
f : ι → Finset (Finset α)
hf : ∀ (i : ι), i ∈ s → Set.Intersecting ↑(f i)
⊢ card (Finset.biUnion s f) ≤ 2 ^ Fintype.card α - 2 ^ (Fintype.card α - card s)
have : DecidableEq ι := by
  classical
  infer_instance
case inl
ι : Type u_1
α : Type u_2
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : Nonempty α
s : Finset ι
f : ι → Finset (Finset α)
hf : ∀ (i : ι), i ∈ s → Set.Intersecting ↑(f i)
this : DecidableEq ι
hs : Fintype.card α ≤ card s
⊢ card (Finset.biUnion s f) ≤ 2 ^ Fintype.card α - 2 ^ (Fintype.card α - card s)

case inr
ι : Type u_1
α : Type u_2
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : Nonempty α
s : Finset ι
f : ι → Finset (Finset α)
hf : ∀ (i : ι), i ∈ s → Set.Intersecting ↑(f i)
this : DecidableEq ι
hs : card s ≤ Fintype.card α
⊢ card (Finset.biUnion s f) ≤ 2 ^ Fintype.card α - 2 ^ (Fintype.card α - card s)
ι : Type u_1
α : Type u_2
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : Nonempty α
s : Finset ι
f : ι → Finset (Finset α)
hf : ∀ (i : ι), i ∈ s → Set.Intersecting ↑(f i)
this : DecidableEq ι
⊢ card (Finset.biUnion s f) ≤ 2 ^ Fintype.card α - 2 ^ (Fintype.card α - card s)
obtain hs | hs := le_total (Fintype.card α) s.card
case inr.empty
ι : Type u_1
α : Type u_2
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : Nonempty α
s : Finset ι
f✝ : ι → Finset (Finset α)
hf✝ : ∀ (i : ι), i ∈ s → Set.Intersecting ↑(f✝ i)
this : DecidableEq ι
hs✝ : card s ≤ Fintype.card α
f : ι → Finset (Finset α)
hf : ∀ (i : ι), i ∈ ∅ → Set.Intersecting ↑(f i)
hs : card ∅ ≤ Fintype.card α
⊢ card (Finset.biUnion ∅ f) ≤ 2 ^ Fintype.card α - 2 ^ (Fintype.card α - card ∅)

case inr.cons
ι : Type u_1
α : Type u_2
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : Nonempty α
s✝ : Finset ι
f✝ : ι → Finset (Finset α)
hf✝ : ∀ (i : ι), i ∈ s✝ → Set.Intersecting ↑(f✝ i)
this : DecidableEq ι
hs✝ : card s✝ ≤ Fintype.card α
i : ι
s : Finset ι
hi : ¬i ∈ s
ih :
  ∀ (f : ι → Finset (Finset α)),
    (∀ (i : ι), i ∈ s → Set.Intersecting ↑(f i)) →
      card s ≤ Fintype.card α → card (Finset.biUnion s f) ≤ 2 ^ Fintype.card α - 2 ^ (Fintype.card α - card s)
f : ι → Finset (Finset α)
hf : ∀ (i_1 : ι), i_1 ∈ cons i s hi → Set.Intersecting ↑(f i_1)
hs : card (cons i s hi) ≤ Fintype.card α
⊢ card (Finset.biUnion (cons i s hi) f) ≤ 2 ^ Fintype.card α - 2 ^ (Fintype.card α - card (cons i s hi))
case inr
ι : Type u_1
α : Type u_2
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : Nonempty α
s : Finset ι
f : ι → Finset (Finset α)
hf : ∀ (i : ι), i ∈ s → Set.Intersecting ↑(f i)
this : DecidableEq ι
hs : card s ≤ Fintype.card α
⊢ card (Finset.biUnion s f) ≤ 2 ^ Fintype.card α - 2 ^ (Fintype.card α - card s)
induction' s using Finset.cons_induction with i s hi ih generalizing f
case inr.cons
ι : Type u_1
α : Type u_2
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : Nonempty α
s✝ : Finset ι
f✝ : ι → Finset (Finset α)
hf✝ : ∀ (i : ι), i ∈ s✝ → Set.Intersecting ↑(f✝ i)
this : DecidableEq ι
hs✝ : card s✝ ≤ Fintype.card α
i : ι
s : Finset ι
hi : ¬i ∈ s
ih :
  ∀ (f : ι → Finset (Finset α)),
    (∀ (i : ι), i ∈ s → Set.Intersecting ↑(f i)) →
      card s ≤ Fintype.card α → card (Finset.biUnion s f) ≤ 2 ^ Fintype.card α - 2 ^ (Fintype.card α - card s)
f : ι → Finset (Finset α)
hf : ∀ (i_1 : ι), i_1 ∈ cons i s hi → Set.Intersecting ↑(f i_1)
hs : card (cons i s hi) ≤ Fintype.card α
f' : ι → Finset (Finset α) :=
  fun j =>
    if hj : j ∈ cons i s hi then
      Exists.choose (_ : ∃ t, f j ⊆ t ∧ 2 * card t = Fintype.card (Finset α) ∧ Set.Intersecting ↑t)
    else ∅
⊢ card (Finset.biUnion (cons i s hi) f) ≤ 2 ^ Fintype.card α - 2 ^ (Fintype.card α - card (cons i s hi))
case inr.cons
ι : Type u_1
α : Type u_2
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : Nonempty α
s✝ : Finset ι
f✝ : ι → Finset (Finset α)
hf✝ : ∀ (i : ι), i ∈ s✝ → Set.Intersecting ↑(f✝ i)
this : DecidableEq ι
hs✝ : card s✝ ≤ Fintype.card α
i : ι
s : Finset ι
hi : ¬i ∈ s
ih :
  ∀ (f : ι → Finset (Finset α)),
    (∀ (i : ι), i ∈ s → Set.Intersecting ↑(f i)) →
      card s ≤ Fintype.card α → card (Finset.biUnion s f) ≤ 2 ^ Fintype.card α - 2 ^ (Fintype.card α - card s)
f : ι → Finset (Finset α)
hf : ∀ (i_1 : ι), i_1 ∈ cons i s hi → Set.Intersecting ↑(f i_1)
hs : card (cons i s hi) ≤ Fintype.card α
⊢ card (Finset.biUnion (cons i s hi) f) ≤ 2 ^ Fintype.card α - 2 ^ (Fintype.card α - card (cons i s hi))
set f' : ι → Finset (Finset α) :=
  fun j ↦ if hj : j ∈ cons i s hi then (hf j hj).exists_card_eq.choose else ∅
case inr.cons
ι : Type u_1
α : Type u_2
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : Nonempty α
s✝ : Finset ι
f✝ : ι → Finset (Finset α)
hf✝ : ∀ (i : ι), i ∈ s✝ → Set.Intersecting ↑(f✝ i)
this : DecidableEq ι
hs✝ : card s✝ ≤ Fintype.card α
i : ι
s : Finset ι
hi : ¬i ∈ s
ih :
  ∀ (f : ι → Finset (Finset α)),
    (∀ (i : ι), i ∈ s → Set.Intersecting ↑(f i)) →
      card s ≤ Fintype.card α → card (Finset.biUnion s f) ≤ 2 ^ Fintype.card α - 2 ^ (Fintype.card α - card s)
f : ι → Finset (Finset α)
hf : ∀ (i_1 : ι), i_1 ∈ cons i s hi → Set.Intersecting ↑(f i_1)
hs : card (cons i s hi) ≤ Fintype.card α
f' : ι → Finset (Finset α) :=
  fun j =>
    if hj : j ∈ cons i s hi then
      Exists.choose (_ : ∃ t, f j ⊆ t ∧ 2 * card t = Fintype.card (Finset α) ∧ Set.Intersecting ↑t)
    else ∅
hf₁ : ∀ (j : ι), j ∈ cons i s hi → f j ⊆ f' j ∧ 2 * card (f' j) = 2 ^ Fintype.card α ∧ Set.Intersecting ↑(f' j)
⊢ card (Finset.biUnion (cons i s hi) f) ≤ 2 ^ Fintype.card α - 2 ^ (Fintype.card α - card (cons i s hi))
case inr.cons
ι : Type u_1
α : Type u_2
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : Nonempty α
s✝ : Finset ι
f✝ : ι → Finset (Finset α)
hf✝ : ∀ (i : ι), i ∈ s✝ → Set.Intersecting ↑(f✝ i)
this : DecidableEq ι
hs✝ : card s✝ ≤ Fintype.card α
i : ι
s : Finset ι
hi : ¬i ∈ s
ih :
  ∀ (f : ι → Finset (Finset α)),
    (∀ (i : ι), i ∈ s → Set.Intersecting ↑(f i)) →
      card s ≤ Fintype.card α → card (Finset.biUnion s f) ≤ 2 ^ Fintype.card α - 2 ^ (Fintype.card α - card s)
f : ι → Finset (Finset α)
hf : ∀ (i_1 : ι), i_1 ∈ cons i s hi → Set.Intersecting ↑(f i_1)
hs : card (cons i s hi) ≤ Fintype.card α
f' : ι → Finset (Finset α) :=
  fun j =>
    if hj : j ∈ cons i s hi then
      Exists.choose (_ : ∃ t, f j ⊆ t ∧ 2 * card t = Fintype.card (Finset α) ∧ Set.Intersecting ↑t)
    else ∅
⊢ card (Finset.biUnion (cons i s hi) f) ≤ 2 ^ Fintype.card α - 2 ^ (Fintype.card α - card (cons i s hi))
have hf₁ : ∀ j, j ∈ cons i s hi → f j ⊆ f' j ∧ 2 * (f' j).card =
    2 ^ Fintype.card α ∧ (f' j : Set (Finset α)).Intersecting := by
  rintro j hj
  simp_rw [dif_pos hj, ← Fintype.card_finset]
  exact Classical.choose_spec (hf j hj).exists_card_eq
case inr.cons
ι : Type u_1
α : Type u_2
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : Nonempty α
s✝ : Finset ι
f✝ : ι → Finset (Finset α)
hf✝ : ∀ (i : ι), i ∈ s✝ → Set.Intersecting ↑(f✝ i)
this : DecidableEq ι
hs✝ : card s✝ ≤ Fintype.card α
i : ι
s : Finset ι
hi : ¬i ∈ s
ih :
  ∀ (f : ι → Finset (Finset α)),
    (∀ (i : ι), i ∈ s → Set.Intersecting ↑(f i)) →
      card s ≤ Fintype.card α → card (Finset.biUnion s f) ≤ 2 ^ Fintype.card α - 2 ^ (Fintype.card α - card s)
f : ι → Finset (Finset α)
hf : ∀ (i_1 : ι), i_1 ∈ cons i s hi → Set.Intersecting ↑(f i_1)
hs : card (cons i s hi) ≤ Fintype.card α
f' : ι → Finset (Finset α) :=
  fun j =>
    if hj : j ∈ cons i s hi then
      Exists.choose (_ : ∃ t, f j ⊆ t ∧ 2 * card t = Fintype.card (Finset α) ∧ Set.Intersecting ↑t)
    else ∅
hf₁ : ∀ (j : ι), j ∈ cons i s hi → f j ⊆ f' j ∧ 2 * card (f' j) = 2 ^ Fintype.card α ∧ Set.Intersecting ↑(f' j)
hf₂ : ∀ (j : ι), j ∈ cons i s hi → IsUpperSet ↑(f' j)
⊢ card (Finset.biUnion (cons i s hi) f) ≤ 2 ^ Fintype.card α - 2 ^ (Fintype.card α - card (cons i s hi))
case inr.cons
ι : Type u_1
α : Type u_2
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : Nonempty α
s✝ : Finset ι
f✝ : ι → Finset (Finset α)
hf✝ : ∀ (i : ι), i ∈ s✝ → Set.Intersecting ↑(f✝ i)
this : DecidableEq ι
hs✝ : card s✝ ≤ Fintype.card α
i : ι
s : Finset ι
hi : ¬i ∈ s
ih :
  ∀ (f : ι → Finset (Finset α)),
    (∀ (i : ι), i ∈ s → Set.Intersecting ↑(f i)) →
      card s ≤ Fintype.card α → card (Finset.biUnion s f) ≤ 2 ^ Fintype.card α - 2 ^ (Fintype.card α - card s)
f : ι → Finset (Finset α)
hf : ∀ (i_1 : ι), i_1 ∈ cons i s hi → Set.Intersecting ↑(f i_1)
hs : card (cons i s hi) ≤ Fintype.card α
f' : ι → Finset (Finset α) :=
  fun j =>
    if hj : j ∈ cons i s hi then
      Exists.choose (_ : ∃ t, f j ⊆ t ∧ 2 * card t = Fintype.card (Finset α) ∧ Set.Intersecting ↑t)
    else ∅
hf₁ : ∀ (j : ι), j ∈ cons i s hi → f j ⊆ f' j ∧ 2 * card (f' j) = 2 ^ Fintype.card α ∧ Set.Intersecting ↑(f' j)
⊢ card (Finset.biUnion (cons i s hi) f) ≤ 2 ^ Fintype.card α - 2 ^ (Fintype.card α - card (cons i s hi))
have hf₂ : ∀ j, j ∈ cons i s hi → IsUpperSet (f' j : Set (Finset α)) := by
  refine' fun j hj ↦ (hf₁ _ hj).2.2.isUpperSet' ((hf₁ _ hj).2.2.is_max_iff_card_eq.2 _)
  rw [Fintype.card_finset]
  exact (hf₁ _ hj).2.1
case inr.cons
ι : Type u_1
α : Type u_2
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : Nonempty α
s✝ : Finset ι
f✝ : ι → Finset (Finset α)
hf✝ : ∀ (i : ι), i ∈ s✝ → Set.Intersecting ↑(f✝ i)
this : DecidableEq ι
hs✝ : card s✝ ≤ Fintype.card α
i : ι
s : Finset ι
hi : ¬i ∈ s
ih :
  ∀ (f : ι → Finset (Finset α)),
    (∀ (i : ι), i ∈ s → Set.Intersecting ↑(f i)) →
      card s ≤ Fintype.card α → card (Finset.biUnion s f) ≤ 2 ^ Fintype.card α - 2 ^ (Fintype.card α - card s)
f : ι → Finset (Finset α)
hf : ∀ (i_1 : ι), i_1 ∈ cons i s hi → Set.Intersecting ↑(f i_1)
hs : card (cons i s hi) ≤ Fintype.card α
f' : ι → Finset (Finset α) :=
  fun j =>
    if hj : j ∈ cons i s hi then
      Exists.choose (_ : ∃ t, f j ⊆ t ∧ 2 * card t = Fintype.card (Finset α) ∧ Set.Intersecting ↑t)
    else ∅
hf₁ : ∀ (j : ι), j ∈ cons i s hi → f j ⊆ f' j ∧ 2 * card (f' j) = 2 ^ Fintype.card α ∧ Set.Intersecting ↑(f' j)
hf₂ : ∀ (j : ι), j ∈ cons i s hi → IsUpperSet ↑(f' j)
⊢ card (Finset.biUnion (cons i s hi) fun j => f' j) ≤ 2 ^ Fintype.card α - 2 ^ (Fintype.card α - card (cons i s hi))
case inr.cons
ι : Type u_1
α : Type u_2
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : Nonempty α
s✝ : Finset ι
f✝ : ι → Finset (Finset α)
hf✝ : ∀ (i : ι), i ∈ s✝ → Set.Intersecting ↑(f✝ i)
this : DecidableEq ι
hs✝ : card s✝ ≤ Fintype.card α
i : ι
s : Finset ι
hi : ¬i ∈ s
ih :
  ∀ (f : ι → Finset (Finset α)),
    (∀ (i : ι), i ∈ s → Set.Intersecting ↑(f i)) →
      card s ≤ Fintype.card α → card (Finset.biUnion s f) ≤ 2 ^ Fintype.card α - 2 ^ (Fintype.card α - card s)
f : ι → Finset (Finset α)
hf : ∀ (i_1 : ι), i_1 ∈ cons i s hi → Set.Intersecting ↑(f i_1)
hs : card (cons i s hi) ≤ Fintype.card α
f' : ι → Finset (Finset α) :=
  fun j =>
    if hj : j ∈ cons i s hi then
      Exists.choose (_ : ∃ t, f j ⊆ t ∧ 2 * card t = Fintype.card (Finset α) ∧ Set.Intersecting ↑t)
    else ∅
hf₁ : ∀ (j : ι), j ∈ cons i s hi → f j ⊆ f' j ∧ 2 * card (f' j) = 2 ^ Fintype.card α ∧ Set.Intersecting ↑(f' j)
hf₂ : ∀ (j : ι), j ∈ cons i s hi → IsUpperSet ↑(f' j)
⊢ card (Finset.biUnion (cons i s hi) f) ≤ 2 ^ Fintype.card α - 2 ^ (Fintype.card α - card (cons i s hi))
refine' (card_le_of_subset <| biUnion_mono fun j hj ↦ (hf₁ _ hj).1).trans _
case inr.cons
ι : Type u_1
α : Type u_2
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : Nonempty α
s✝ : Finset ι
f✝ : ι → Finset (Finset α)
hf✝ : ∀ (i : ι), i ∈ s✝ → Set.Intersecting ↑(f✝ i)
this : DecidableEq ι
hs✝ : card s✝ ≤ Fintype.card α
i : ι
s : Finset ι
hi : ¬i ∈ s
ih :
  ∀ (f : ι → Finset (Finset α)),
    (∀ (i : ι), i ∈ s → Set.Intersecting ↑(f i)) →
      card s ≤ Fintype.card α → card (Finset.biUnion s f) ≤ 2 ^ Fintype.card α - 2 ^ (Fintype.card α - card s)
f : ι → Finset (Finset α)
hf : ∀ (i_1 : ι), i_1 ∈ cons i s hi → Set.Intersecting ↑(f i_1)
hs : card (cons i s hi) ≤ Fintype.card α
f' : ι → Finset (Finset α) :=
  fun j =>
    if hj : j ∈ cons i s hi then
      Exists.choose (_ : ∃ t, f j ⊆ t ∧ 2 * card t = Fintype.card (Finset α) ∧ Set.Intersecting ↑t)
    else ∅
hf₁ : ∀ (j : ι), j ∈ cons i s hi → f j ⊆ f' j ∧ 2 * card (f' j) = 2 ^ Fintype.card α ∧ Set.Intersecting ↑(f' j)
hf₂ : ∀ (j : ι), j ∈ cons i s hi → IsUpperSet ↑(f' j)
⊢ card (Finset.biUnion (insert i s) fun j => f' j) ≤ 2 ^ Fintype.card α - 2 ^ (Fintype.card α - card (cons i s hi))
case inr.cons
ι : Type u_1
α : Type u_2
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : Nonempty α
s✝ : Finset ι
f✝ : ι → Finset (Finset α)
hf✝ : ∀ (i : ι), i ∈ s✝ → Set.Intersecting ↑(f✝ i)
this : DecidableEq ι
hs✝ : card s✝ ≤ Fintype.card α
i : ι
s : Finset ι
hi : ¬i ∈ s
ih :
  ∀ (f : ι → Finset (Finset α)),
    (∀ (i : ι), i ∈ s → Set.Intersecting ↑(f i)) →
      card s ≤ Fintype.card α → card (Finset.biUnion s f) ≤ 2 ^ Fintype.card α - 2 ^ (Fintype.card α - card s)
f : ι → Finset (Finset α)
hf : ∀ (i_1 : ι), i_1 ∈ cons i s hi → Set.Intersecting ↑(f i_1)
hs : card (cons i s hi) ≤ Fintype.card α
f' : ι → Finset (Finset α) :=
  fun j =>
    if hj : j ∈ cons i s hi then
      Exists.choose (_ : ∃ t, f j ⊆ t ∧ 2 * card t = Fintype.card (Finset α) ∧ Set.Intersecting ↑t)
    else ∅
hf₁ : ∀ (j : ι), j ∈ cons i s hi → f j ⊆ f' j ∧ 2 * card (f' j) = 2 ^ Fintype.card α ∧ Set.Intersecting ↑(f' j)
hf₂ : ∀ (j : ι), j ∈ cons i s hi → IsUpperSet ↑(f' j)
⊢ card (Finset.biUnion (cons i s hi) fun j => f' j) ≤ 2 ^ Fintype.card α - 2 ^ (Fintype.card α - card (cons i s hi))
nth_rw 1 [cons_eq_insert i]
case inr.cons
ι : Type u_1
α : Type u_2
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : Nonempty α
s✝ : Finset ι
f✝ : ι → Finset (Finset α)
hf✝ : ∀ (i : ι), i ∈ s✝ → Set.Intersecting ↑(f✝ i)
this : DecidableEq ι
hs✝ : card s✝ ≤ Fintype.card α
i : ι
s : Finset ι
hi : ¬i ∈ s
ih :
  ∀ (f : ι → Finset (Finset α)),
    (∀ (i : ι), i ∈ s → Set.Intersecting ↑(f i)) →
      card s ≤ Fintype.card α → card (Finset.biUnion s f) ≤ 2 ^ Fintype.card α - 2 ^ (Fintype.card α - card s)
f : ι → Finset (Finset α)
hf : ∀ (i_1 : ι), i_1 ∈ cons i s hi → Set.Intersecting ↑(f i_1)
hs : card (cons i s hi) ≤ Fintype.card α
f' : ι → Finset (Finset α) :=
  fun j =>
    if hj : j ∈ cons i s hi then
      Exists.choose (_ : ∃ t, f j ⊆ t ∧ 2 * card t = Fintype.card (Finset α) ∧ Set.Intersecting ↑t)
    else ∅
hf₁ : ∀ (j : ι), j ∈ cons i s hi → f j ⊆ f' j ∧ 2 * card (f' j) = 2 ^ Fintype.card α ∧ Set.Intersecting ↑(f' j)
hf₂ : ∀ (j : ι), j ∈ cons i s hi → IsUpperSet ↑(f' j)
⊢ card (f' i ∪ Finset.biUnion s fun j => f' j) ≤ 2 ^ Fintype.card α - 2 ^ (Fintype.card α - card (cons i s hi))
case inr.cons
ι : Type u_1
α : Type u_2
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : Nonempty α
s✝ : Finset ι
f✝ : ι → Finset (Finset α)
hf✝ : ∀ (i : ι), i ∈ s✝ → Set.Intersecting ↑(f✝ i)
this : DecidableEq ι
hs✝ : card s✝ ≤ Fintype.card α
i : ι
s : Finset ι
hi : ¬i ∈ s
ih :
  ∀ (f : ι → Finset (Finset α)),
    (∀ (i : ι), i ∈ s → Set.Intersecting ↑(f i)) →
      card s ≤ Fintype.card α → card (Finset.biUnion s f) ≤ 2 ^ Fintype.card α - 2 ^ (Fintype.card α - card s)
f : ι → Finset (Finset α)
hf : ∀ (i_1 : ι), i_1 ∈ cons i s hi → Set.Intersecting ↑(f i_1)
hs : card (cons i s hi) ≤ Fintype.card α
f' : ι → Finset (Finset α) :=
  fun j =>
    if hj : j ∈ cons i s hi then
      Exists.choose (_ : ∃ t, f j ⊆ t ∧ 2 * card t = Fintype.card (Finset α) ∧ Set.Intersecting ↑t)
    else ∅
hf₁ : ∀ (j : ι), j ∈ cons i s hi → f j ⊆ f' j ∧ 2 * card (f' j) = 2 ^ Fintype.card α ∧ Set.Intersecting ↑(f' j)
hf₂ : ∀ (j : ι), j ∈ cons i s hi → IsUpperSet ↑(f' j)
⊢ card (Finset.biUnion (insert i s) fun j => f' j) ≤ 2 ^ Fintype.card α - 2 ^ (Fintype.card α - card (cons i s hi))
rw [biUnion_insert]
case inr.cons
ι : Type u_1
α : Type u_2
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : Nonempty α
s✝ : Finset ι
f✝ : ι → Finset (Finset α)
hf✝ : ∀ (i : ι), i ∈ s✝ → Set.Intersecting ↑(f✝ i)
this : DecidableEq ι
hs✝ : card s✝ ≤ Fintype.card α
i : ι
s : Finset ι
hi : ¬i ∈ s
ih :
  ∀ (f : ι → Finset (Finset α)),
    (∀ (i : ι), i ∈ s → Set.Intersecting ↑(f i)) →
      card s ≤ Fintype.card α → card (Finset.biUnion s f) ≤ 2 ^ Fintype.card α - 2 ^ (Fintype.card α - card s)
f : ι → Finset (Finset α)
hf : ∀ (i_1 : ι), i_1 ∈ cons i s hi → Set.Intersecting ↑(f i_1)
hs : card (cons i s hi) ≤ Fintype.card α
f' : ι → Finset (Finset α) :=
  fun j =>
    if hj : j ∈ cons i s hi then
      Exists.choose (_ : ∃ t, f j ⊆ t ∧ 2 * card t = Fintype.card (Finset α) ∧ Set.Intersecting ↑t)
    else ∅
hf₁ : ∀ (j : ι), j ∈ cons i s hi → f j ⊆ f' j ∧ 2 * card (f' j) = 2 ^ Fintype.card α ∧ Set.Intersecting ↑(f' j)
hf₂ : ∀ (j : ι), j ∈ cons i s hi → IsUpperSet ↑(f' j)
⊢ card (f' i) + card ((f' i ∪ Finset.biUnion s fun j => f' j) \ f' i) ≤
    2 ^ Fintype.card α - 2 ^ (Fintype.card α - card (cons i s hi))
case inr.cons
ι : Type u_1
α : Type u_2
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : Nonempty α
s✝ : Finset ι
f✝ : ι → Finset (Finset α)
hf✝ : ∀ (i : ι), i ∈ s✝ → Set.Intersecting ↑(f✝ i)
this : DecidableEq ι
hs✝ : card s✝ ≤ Fintype.card α
i : ι
s : Finset ι
hi : ¬i ∈ s
ih :
  ∀ (f : ι → Finset (Finset α)),
    (∀ (i : ι), i ∈ s → Set.Intersecting ↑(f i)) →
      card s ≤ Fintype.card α → card (Finset.biUnion s f) ≤ 2 ^ Fintype.card α - 2 ^ (Fintype.card α - card s)
f : ι → Finset (Finset α)
hf : ∀ (i_1 : ι), i_1 ∈ cons i s hi → Set.Intersecting ↑(f i_1)
hs : card (cons i s hi) ≤ Fintype.card α
f' : ι → Finset (Finset α) :=
  fun j =>
    if hj : j ∈ cons i s hi then
      Exists.choose (_ : ∃ t, f j ⊆ t ∧ 2 * card t = Fintype.card (Finset α) ∧ Set.Intersecting ↑t)
    else ∅
hf₁ : ∀ (j : ι), j ∈ cons i s hi → f j ⊆ f' j ∧ 2 * card (f' j) = 2 ^ Fintype.card α ∧ Set.Intersecting ↑(f' j)
hf₂ : ∀ (j : ι), j ∈ cons i s hi → IsUpperSet ↑(f' j)
⊢ card (f' i ∪ Finset.biUnion s fun j => f' j) ≤ 2 ^ Fintype.card α - 2 ^ (Fintype.card α - card (cons i s hi))
refine' (card_mono <| @le_sup_sdiff _ _ _ <| f' i).trans ((card_union_le _ _).trans _)
case inr.cons
ι : Type u_1
α : Type u_2
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : Nonempty α
s✝ : Finset ι
f✝ : ι → Finset (Finset α)
hf✝ : ∀ (i : ι), i ∈ s✝ → Set.Intersecting ↑(f✝ i)
this : DecidableEq ι
hs✝ : card s✝ ≤ Fintype.card α
i : ι
s : Finset ι
hi : ¬i ∈ s
ih :
  ∀ (f : ι → Finset (Finset α)),
    (∀ (i : ι), i ∈ s → Set.Intersecting ↑(f i)) →
      card s ≤ Fintype.card α → card (Finset.biUnion s f) ≤ 2 ^ Fintype.card α - 2 ^ (Fintype.card α - card s)
f : ι → Finset (Finset α)
hf : ∀ (i_1 : ι), i_1 ∈ cons i s hi → Set.Intersecting ↑(f i_1)
hs : card (cons i s hi) ≤ Fintype.card α
f' : ι → Finset (Finset α) :=
  fun j =>
    if hj : j ∈ cons i s hi then
      Exists.choose (_ : ∃ t, f j ⊆ t ∧ 2 * card t = Fintype.card (Finset α) ∧ Set.Intersecting ↑t)
    else ∅
hf₁ : ∀ (j : ι), j ∈ cons i s hi → f j ⊆ f' j ∧ 2 * card (f' j) = 2 ^ Fintype.card α ∧ Set.Intersecting ↑(f' j)
hf₂ : ∀ (j : ι), j ∈ cons i s hi → IsUpperSet ↑(f' j)
⊢ card (f' i) + card ((Finset.biUnion s fun j => f' j) ∩ f' iᶜ) ≤
    2 ^ Fintype.card α - 2 ^ (Fintype.card α - card (cons i s hi))
case inr.cons
ι : Type u_1
α : Type u_2
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : Nonempty α
s✝ : Finset ι
f✝ : ι → Finset (Finset α)
hf✝ : ∀ (i : ι), i ∈ s✝ → Set.Intersecting ↑(f✝ i)
this : DecidableEq ι
hs✝ : card s✝ ≤ Fintype.card α
i : ι
s : Finset ι
hi : ¬i ∈ s
ih :
  ∀ (f : ι → Finset (Finset α)),
    (∀ (i : ι), i ∈ s → Set.Intersecting ↑(f i)) →
      card s ≤ Fintype.card α → card (Finset.biUnion s f) ≤ 2 ^ Fintype.card α - 2 ^ (Fintype.card α - card s)
f : ι → Finset (Finset α)
hf : ∀ (i_1 : ι), i_1 ∈ cons i s hi → Set.Intersecting ↑(f i_1)
hs : card (cons i s hi) ≤ Fintype.card α
f' : ι → Finset (Finset α) :=
  fun j =>
    if hj : j ∈ cons i s hi then
      Exists.choose (_ : ∃ t, f j ⊆ t ∧ 2 * card t = Fintype.card (Finset α) ∧ Set.Intersecting ↑t)
    else ∅
hf₁ : ∀ (j : ι), j ∈ cons i s hi → f j ⊆ f' j ∧ 2 * card (f' j) = 2 ^ Fintype.card α ∧ Set.Intersecting ↑(f' j)
hf₂ : ∀ (j : ι), j ∈ cons i s hi → IsUpperSet ↑(f' j)
⊢ card (f' i) + card ((f' i ∪ Finset.biUnion s fun j => f' j) \ f' i) ≤
    2 ^ Fintype.card α - 2 ^ (Fintype.card α - card (cons i s hi))
rw [union_sdiff_left, sdiff_eq_inter_compl]
case inr.cons
ι : Type u_1
α : Type u_2
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : Nonempty α
s✝ : Finset ι
f✝ : ι → Finset (Finset α)
hf✝ : ∀ (i : ι), i ∈ s✝ → Set.Intersecting ↑(f✝ i)
this : DecidableEq ι
hs✝ : card s✝ ≤ Fintype.card α
i : ι
s : Finset ι
hi : ¬i ∈ s
ih :
  ∀ (f : ι → Finset (Finset α)),
    (∀ (i : ι), i ∈ s → Set.Intersecting ↑(f i)) →
      card s ≤ Fintype.card α → card (Finset.biUnion s f) ≤ 2 ^ Fintype.card α - 2 ^ (Fintype.card α - card s)
f : ι → Finset (Finset α)
hf : ∀ (i_1 : ι), i_1 ∈ cons i s hi → Set.Intersecting ↑(f i_1)
hs : card (cons i s hi) ≤ Fintype.card α
f' : ι → Finset (Finset α) :=
  fun j =>
    if hj : j ∈ cons i s hi then
      Exists.choose (_ : ∃ t, f j ⊆ t ∧ 2 * card t = Fintype.card (Finset α) ∧ Set.Intersecting ↑t)
    else ∅
hf₁ : ∀ (j : ι), j ∈ cons i s hi → f j ⊆ f' j ∧ 2 * card (f' j) = 2 ^ Fintype.card α ∧ Set.Intersecting ↑(f' j)
hf₂ : ∀ (j : ι), j ∈ cons i s hi → IsUpperSet ↑(f' j)
⊢ 2 ^ (Fintype.card α + 1) * (card (f' i) + card ((Finset.biUnion s fun j => f' j) ∩ f' iᶜ)) ≤
    2 ^ (Fintype.card α + 1) * (2 ^ Fintype.card α - 2 ^ (Fintype.card α - card (cons i s hi)))
case inr.cons
ι : Type u_1
α : Type u_2
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : Nonempty α
s✝ : Finset ι
f✝ : ι → Finset (Finset α)
hf✝ : ∀ (i : ι), i ∈ s✝ → Set.Intersecting ↑(f✝ i)
this : DecidableEq ι
hs✝ : card s✝ ≤ Fintype.card α
i : ι
s : Finset ι
hi : ¬i ∈ s
ih :
  ∀ (f : ι → Finset (Finset α)),
    (∀ (i : ι), i ∈ s → Set.Intersecting ↑(f i)) →
      card s ≤ Fintype.card α → card (Finset.biUnion s f) ≤ 2 ^ Fintype.card α - 2 ^ (Fintype.card α - card s)
f : ι → Finset (Finset α)
hf : ∀ (i_1 : ι), i_1 ∈ cons i s hi → Set.Intersecting ↑(f i_1)
hs : card (cons i s hi) ≤ Fintype.card α
f' : ι → Finset (Finset α) :=
  fun j =>
    if hj : j ∈ cons i s hi then
      Exists.choose (_ : ∃ t, f j ⊆ t ∧ 2 * card t = Fintype.card (Finset α) ∧ Set.Intersecting ↑t)
    else ∅
hf₁ : ∀ (j : ι), j ∈ cons i s hi → f j ⊆ f' j ∧ 2 * card (f' j) = 2 ^ Fintype.card α ∧ Set.Intersecting ↑(f' j)
hf₂ : ∀ (j : ι), j ∈ cons i s hi → IsUpperSet ↑(f' j)
⊢ card (f' i) + card ((Finset.biUnion s fun j => f' j) ∩ f' iᶜ) ≤
    2 ^ Fintype.card α - 2 ^ (Fintype.card α - card (cons i s hi))
refine' le_of_mul_le_mul_left _ (pow_pos (zero_lt_two' ℕ) <| Fintype.card α + 1)
case inr.cons
ι : Type u_1
α : Type u_2
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : Nonempty α
s✝ : Finset ι
f✝ : ι → Finset (Finset α)
hf✝ : ∀ (i : ι), i ∈ s✝ → Set.Intersecting ↑(f✝ i)
this : DecidableEq ι
hs✝ : card s✝ ≤ Fintype.card α
i : ι
s : Finset ι
hi : ¬i ∈ s
ih :
  ∀ (f : ι → Finset (Finset α)),
    (∀ (i : ι), i ∈ s → Set.Intersecting ↑(f i)) →
      card s ≤ Fintype.card α → card (Finset.biUnion s f) ≤ 2 ^ Fintype.card α - 2 ^ (Fintype.card α - card s)
f : ι → Finset (Finset α)
hf : ∀ (i_1 : ι), i_1 ∈ cons i s hi → Set.Intersecting ↑(f i_1)
hs : card (cons i s hi) ≤ Fintype.card α
f' : ι → Finset (Finset α) :=
  fun j =>
    if hj : j ∈ cons i s hi then
      Exists.choose (_ : ∃ t, f j ⊆ t ∧ 2 * card t = Fintype.card (Finset α) ∧ Set.Intersecting ↑t)
    else ∅
hf₁ : ∀ (j : ι), j ∈ cons i s hi → f j ⊆ f' j ∧ 2 * card (f' j) = 2 ^ Fintype.card α ∧ Set.Intersecting ↑(f' j)
hf₂ : ∀ (j : ι), j ∈ cons i s hi → IsUpperSet ↑(f' j)
⊢ 2 ^ Fintype.card α * (2 * card (f' i)) + 2 * (2 ^ Fintype.card α * card ((Finset.biUnion s fun j => f' j) ∩ f' iᶜ)) ≤
    2 * 2 ^ Fintype.card α * (2 ^ Fintype.card α - 2 ^ (Fintype.card α - card (cons i s hi)))
case inr.cons
ι : Type u_1
α : Type u_2
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : Nonempty α
s✝ : Finset ι
f✝ : ι → Finset (Finset α)
hf✝ : ∀ (i : ι), i ∈ s✝ → Set.Intersecting ↑(f✝ i)
this : DecidableEq ι
hs✝ : card s✝ ≤ Fintype.card α
i : ι
s : Finset ι
hi : ¬i ∈ s
ih :
  ∀ (f : ι → Finset (Finset α)),
    (∀ (i : ι), i ∈ s → Set.Intersecting ↑(f i)) →
      card s ≤ Fintype.card α → card (Finset.biUnion s f) ≤ 2 ^ Fintype.card α - 2 ^ (Fintype.card α - card s)
f : ι → Finset (Finset α)
hf : ∀ (i_1 : ι), i_1 ∈ cons i s hi → Set.Intersecting ↑(f i_1)
hs : card (cons i s hi) ≤ Fintype.card α
f' : ι → Finset (Finset α) :=
  fun j =>
    if hj : j ∈ cons i s hi then
      Exists.choose (_ : ∃ t, f j ⊆ t ∧ 2 * card t = Fintype.card (Finset α) ∧ Set.Intersecting ↑t)
    else ∅
hf₁ : ∀ (j : ι), j ∈ cons i s hi → f j ⊆ f' j ∧ 2 * card (f' j) = 2 ^ Fintype.card α ∧ Set.Intersecting ↑(f' j)
hf₂ : ∀ (j : ι), j ∈ cons i s hi → IsUpperSet ↑(f' j)
⊢ 2 ^ (Fintype.card α + 1) * (card (f' i) + card ((Finset.biUnion s fun j => f' j) ∩ f' iᶜ)) ≤
    2 ^ (Fintype.card α + 1) * (2 ^ Fintype.card α - 2 ^ (Fintype.card α - card (cons i s hi)))
rw [pow_succ', mul_add, mul_assoc, mul_comm _ 2, mul_assoc]
case inr.cons.refine'_1
ι : Type u_1
α : Type u_2
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : Nonempty α
s✝ : Finset ι
f✝ : ι → Finset (Finset α)
hf✝ : ∀ (i : ι), i ∈ s✝ → Set.Intersecting ↑(f✝ i)
this : DecidableEq ι
hs✝ : card s✝ ≤ Fintype.card α
i : ι
s : Finset ι
hi : ¬i ∈ s
ih :
  ∀ (f : ι → Finset (Finset α)),
    (∀ (i : ι), i ∈ s → Set.Intersecting ↑(f i)) →
      card s ≤ Fintype.card α → card (Finset.biUnion s f) ≤ 2 ^ Fintype.card α - 2 ^ (Fintype.card α - card s)
f : ι → Finset (Finset α)
hf : ∀ (i_1 : ι), i_1 ∈ cons i s hi → Set.Intersecting ↑(f i_1)
hs : card (cons i s hi) ≤ Fintype.card α
f' : ι → Finset (Finset α) :=
  fun j =>
    if hj : j ∈ cons i s hi then
      Exists.choose (_ : ∃ t, f j ⊆ t ∧ 2 * card t = Fintype.card (Finset α) ∧ Set.Intersecting ↑t)
    else ∅
hf₁ : ∀ (j : ι), j ∈ cons i s hi → f j ⊆ f' j ∧ 2 * card (f' j) = 2 ^ Fintype.card α ∧ Set.Intersecting ↑(f' j)
hf₂ : ∀ (j : ι), j ∈ cons i s hi → IsUpperSet ↑(f' j)
⊢ IsUpperSet ↑(Finset.biUnion s fun j => f' j)

case inr.cons.refine'_2
ι : Type u_1
α : Type u_2
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : Nonempty α
s✝ : Finset ι
f✝ : ι → Finset (Finset α)
hf✝ : ∀ (i : ι), i ∈ s✝ → Set.Intersecting ↑(f✝ i)
this : DecidableEq ι
hs✝ : card s✝ ≤ Fintype.card α
i : ι
s : Finset ι
hi : ¬i ∈ s
ih :
  ∀ (f : ι → Finset (Finset α)),
    (∀ (i : ι), i ∈ s → Set.Intersecting ↑(f i)) →
      card s ≤ Fintype.card α → card (Finset.biUnion s f) ≤ 2 ^ Fintype.card α - 2 ^ (Fintype.card α - card s)
f : ι → Finset (Finset α)
hf : ∀ (i_1 : ι), i_1 ∈ cons i s hi → Set.Intersecting ↑(f i_1)
hs : card (cons i s hi) ≤ Fintype.card α
f' : ι → Finset (Finset α) :=
  fun j =>
    if hj : j ∈ cons i s hi then
      Exists.choose (_ : ∃ t, f j ⊆ t ∧ 2 * card t = Fintype.card (Finset α) ∧ Set.Intersecting ↑t)
    else ∅
hf₁ : ∀ (j : ι), j ∈ cons i s hi → f j ⊆ f' j ∧ 2 * card (f' j) = 2 ^ Fintype.card α ∧ Set.Intersecting ↑(f' j)
hf₂ : ∀ (j : ι), j ∈ cons i s hi → IsUpperSet ↑(f' j)
⊢ IsLowerSet ↑(f' iᶜ)

case inr.cons.refine'_3
ι : Type u_1
α : Type u_2
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : Nonempty α
s✝ : Finset ι
f✝ : ι → Finset (Finset α)
hf✝ : ∀ (i : ι), i ∈ s✝ → Set.Intersecting ↑(f✝ i)
this : DecidableEq ι
hs✝ : card s✝ ≤ Fintype.card α
i : ι
s : Finset ι
hi : ¬i ∈ s
ih :
  ∀ (f : ι → Finset (Finset α)),
    (∀ (i : ι), i ∈ s → Set.Intersecting ↑(f i)) →
      card s ≤ Fintype.card α → card (Finset.biUnion s f) ≤ 2 ^ Fintype.card α - 2 ^ (Fintype.card α - card s)
f : ι → Finset (Finset α)
hf : ∀ (i_1 : ι), i_1 ∈ cons i s hi → Set.Intersecting ↑(f i_1)
hs : card (cons i s hi) ≤ Fintype.card α
f' : ι → Finset (Finset α) :=
  fun j =>
    if hj : j ∈ cons i s hi then
      Exists.choose (_ : ∃ t, f j ⊆ t ∧ 2 * card t = Fintype.card (Finset α) ∧ Set.Intersecting ↑t)
    else ∅
hf₁ : ∀ (j : ι), j ∈ cons i s hi → f j ⊆ f' j ∧ 2 * card (f' j) = 2 ^ Fintype.card α ∧ Set.Intersecting ↑(f' j)
hf₂ : ∀ (j : ι), j ∈ cons i s hi → IsUpperSet ↑(f' j)
⊢ 2 ^ Fintype.card α * Fintype.card (Finset α) + 2 * (card (Finset.biUnion s fun j => f' j) * card (f' iᶜ)) ≤
    2 * 2 ^ Fintype.card α * (2 ^ Fintype.card α - 2 ^ (Fintype.card α - card (cons i s hi)))
case inr.cons
ι : Type u_1
α : Type u_2
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : Nonempty α
s✝ : Finset ι
f✝ : ι → Finset (Finset α)
hf✝ : ∀ (i : ι), i ∈ s✝ → Set.Intersecting ↑(f✝ i)
this : DecidableEq ι
hs✝ : card s✝ ≤ Fintype.card α
i : ι
s : Finset ι
hi : ¬i ∈ s
ih :
  ∀ (f : ι → Finset (Finset α)),
    (∀ (i : ι), i ∈ s → Set.Intersecting ↑(f i)) →
      card s ≤ Fintype.card α → card (Finset.biUnion s f) ≤ 2 ^ Fintype.card α - 2 ^ (Fintype.card α - card s)
f : ι → Finset (Finset α)
hf : ∀ (i_1 : ι), i_1 ∈ cons i s hi → Set.Intersecting ↑(f i_1)
hs : card (cons i s hi) ≤ Fintype.card α
f' : ι → Finset (Finset α) :=
  fun j =>
    if hj : j ∈ cons i s hi then
      Exists.choose (_ : ∃ t, f j ⊆ t ∧ 2 * card t = Fintype.card (Finset α) ∧ Set.Intersecting ↑t)
    else ∅
hf₁ : ∀ (j : ι), j ∈ cons i s hi → f j ⊆ f' j ∧ 2 * card (f' j) = 2 ^ Fintype.card α ∧ Set.Intersecting ↑(f' j)
hf₂ : ∀ (j : ι), j ∈ cons i s hi → IsUpperSet ↑(f' j)
⊢ 2 ^ Fintype.card α * (2 * card (f' i)) + 2 * (2 ^ Fintype.card α * card ((Finset.biUnion s fun j => f' j) ∩ f' iᶜ)) ≤
    2 * 2 ^ Fintype.card α * (2 ^ Fintype.card α - 2 ^ (Fintype.card α - card (cons i s hi)))
refine' (add_le_add
    ((mul_le_mul_left <| pow_pos (zero_lt_two' ℕ) _).2
    (hf₁ _ <| mem_cons_self _ _).2.2.card_le) <|
    (mul_le_mul_left <| zero_lt_two' ℕ).2 <| IsUpperSet.card_inter_le_finset _ _).trans _
case inr.cons.refine'_3
ι : Type u_1
α : Type u_2
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : Nonempty α
s✝ : Finset ι
f✝ : ι → Finset (Finset α)
hf✝ : ∀ (i : ι), i ∈ s✝ → Set.Intersecting ↑(f✝ i)
this : DecidableEq ι
hs✝ : card s✝ ≤ Fintype.card α
i : ι
s : Finset ι
hi : ¬i ∈ s
ih :
  ∀ (f : ι → Finset (Finset α)),
    (∀ (i : ι), i ∈ s → Set.Intersecting ↑(f i)) →
      card s ≤ Fintype.card α → card (Finset.biUnion s f) ≤ 2 ^ Fintype.card α - 2 ^ (Fintype.card α - card s)
f : ι → Finset (Finset α)
hf : ∀ (i_1 : ι), i_1 ∈ cons i s hi → Set.Intersecting ↑(f i_1)
hs : card (cons i s hi) ≤ Fintype.card α
f' : ι → Finset (Finset α) :=
  fun j =>
    if hj : j ∈ cons i s hi then
      Exists.choose (_ : ∃ t, f j ⊆ t ∧ 2 * card t = Fintype.card (Finset α) ∧ Set.Intersecting ↑t)
    else ∅
hf₁ : ∀ (j : ι), j ∈ cons i s hi → f j ⊆ f' j ∧ 2 * card (f' j) = 2 ^ Fintype.card α ∧ Set.Intersecting ↑(f' j)
hf₂ : ∀ (j : ι), j ∈ cons i s hi → IsUpperSet ↑(f' j)
⊢ 2 ^ Fintype.card α * (2 ^ Fintype.card α + card (Finset.biUnion s fun j => f' j)) ≤
    2 ^ Fintype.card α * (2 * (2 ^ Fintype.card α - 2 ^ (Fintype.card α - card (cons i s hi))))
case inr.cons.refine'_3
ι : Type u_1
α : Type u_2
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : Nonempty α
s✝ : Finset ι
f✝ : ι → Finset (Finset α)
hf✝ : ∀ (i : ι), i ∈ s✝ → Set.Intersecting ↑(f✝ i)
this : DecidableEq ι
hs✝ : card s✝ ≤ Fintype.card α
i : ι
s : Finset ι
hi : ¬i ∈ s
ih :
  ∀ (f : ι → Finset (Finset α)),
    (∀ (i : ι), i ∈ s → Set.Intersecting ↑(f i)) →
      card s ≤ Fintype.card α → card (Finset.biUnion s f) ≤ 2 ^ Fintype.card α - 2 ^ (Fintype.card α - card s)
f : ι → Finset (Finset α)
hf : ∀ (i_1 : ι), i_1 ∈ cons i s hi → Set.Intersecting ↑(f i_1)
hs : card (cons i s hi) ≤ Fintype.card α
f' : ι → Finset (Finset α) :=
  fun j =>
    if hj : j ∈ cons i s hi then
      Exists.choose (_ : ∃ t, f j ⊆ t ∧ 2 * card t = Fintype.card (Finset α) ∧ Set.Intersecting ↑t)
    else ∅
hf₁ : ∀ (j : ι), j ∈ cons i s hi → f j ⊆ f' j ∧ 2 * card (f' j) = 2 ^ Fintype.card α ∧ Set.Intersecting ↑(f' j)
hf₂ : ∀ (j : ι), j ∈ cons i s hi → IsUpperSet ↑(f' j)
⊢ 2 ^ Fintype.card α * Fintype.card (Finset α) + 2 * (card (Finset.biUnion s fun j => f' j) * card (f' iᶜ)) ≤
    2 * 2 ^ Fintype.card α * (2 ^ Fintype.card α - 2 ^ (Fintype.card α - card (cons i s hi)))
rw [mul_tsub, card_compl, Fintype.card_finset, mul_left_comm, mul_tsub,
  (hf₁ _ <| mem_cons_self _ _).2.1, two_mul, add_tsub_cancel_left, ← mul_tsub, ← mul_two,
  mul_assoc, ← add_mul, mul_comm]
case inr.cons.refine'_3
ι : Type u_1
α : Type u_2
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : Nonempty α
s✝ : Finset ι
f✝ : ι → Finset (Finset α)
hf✝ : ∀ (i : ι), i ∈ s✝ → Set.Intersecting ↑(f✝ i)
this : DecidableEq ι
hs✝ : card s✝ ≤ Fintype.card α
i : ι
s : Finset ι
hi : ¬i ∈ s
ih :
  ∀ (f : ι → Finset (Finset α)),
    (∀ (i : ι), i ∈ s → Set.Intersecting ↑(f i)) →
      card s ≤ Fintype.card α → card (Finset.biUnion s f) ≤ 2 ^ Fintype.card α - 2 ^ (Fintype.card α - card s)
f : ι → Finset (Finset α)
hf : ∀ (i_1 : ι), i_1 ∈ cons i s hi → Set.Intersecting ↑(f i_1)
hs : card (cons i s hi) ≤ Fintype.card α
f' : ι → Finset (Finset α) :=
  fun j =>
    if hj : j ∈ cons i s hi then
      Exists.choose (_ : ∃ t, f j ⊆ t ∧ 2 * card t = Fintype.card (Finset α) ∧ Set.Intersecting ↑t)
    else ∅
hf₁ : ∀ (j : ι), j ∈ cons i s hi → f j ⊆ f' j ∧ 2 * card (f' j) = 2 ^ Fintype.card α ∧ Set.Intersecting ↑(f' j)
hf₂ : ∀ (j : ι), j ∈ cons i s hi → IsUpperSet ↑(f' j)
⊢ 2 ^ Fintype.card α + card (Finset.biUnion s fun j => f' j) ≤
    2 * (2 ^ Fintype.card α - 2 ^ (Fintype.card α - card (cons i s hi)))
case inr.cons.refine'_3
ι : Type u_1
α : Type u_2
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : Nonempty α
s✝ : Finset ι
f✝ : ι → Finset (Finset α)
hf✝ : ∀ (i : ι), i ∈ s✝ → Set.Intersecting ↑(f✝ i)
this : DecidableEq ι
hs✝ : card s✝ ≤ Fintype.card α
i : ι
s : Finset ι
hi : ¬i ∈ s
ih :
  ∀ (f : ι → Finset (Finset α)),
    (∀ (i : ι), i ∈ s → Set.Intersecting ↑(f i)) →
      card s ≤ Fintype.card α → card (Finset.biUnion s f) ≤ 2 ^ Fintype.card α - 2 ^ (Fintype.card α - card s)
f : ι → Finset (Finset α)
hf : ∀ (i_1 : ι), i_1 ∈ cons i s hi → Set.Intersecting ↑(f i_1)
hs : card (cons i s hi) ≤ Fintype.card α
f' : ι → Finset (Finset α) :=
  fun j =>
    if hj : j ∈ cons i s hi then
      Exists.choose (_ : ∃ t, f j ⊆ t ∧ 2 * card t = Fintype.card (Finset α) ∧ Set.Intersecting ↑t)
    else ∅
hf₁ : ∀ (j : ι), j ∈ cons i s hi → f j ⊆ f' j ∧ 2 * card (f' j) = 2 ^ Fintype.card α ∧ Set.Intersecting ↑(f' j)
hf₂ : ∀ (j : ι), j ∈ cons i s hi → IsUpperSet ↑(f' j)
⊢ 2 ^ Fintype.card α * (2 ^ Fintype.card α + card (Finset.biUnion s fun j => f' j)) ≤
    2 ^ Fintype.card α * (2 * (2 ^ Fintype.card α - 2 ^ (Fintype.card α - card (cons i s hi))))
refine' mul_le_mul_left' _ _
case inr.cons.refine'_3
ι : Type u_1
α : Type u_2
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : Nonempty α
s✝ : Finset ι
f✝ : ι → Finset (Finset α)
hf✝ : ∀ (i : ι), i ∈ s✝ → Set.Intersecting ↑(f✝ i)
this : DecidableEq ι
hs✝ : card s✝ ≤ Fintype.card α
i : ι
s : Finset ι
hi : ¬i ∈ s
ih :
  ∀ (f : ι → Finset (Finset α)),
    (∀ (i : ι), i ∈ s → Set.Intersecting ↑(f i)) →
      card s ≤ Fintype.card α → card (Finset.biUnion s f) ≤ 2 ^ Fintype.card α - 2 ^ (Fintype.card α - card s)
f : ι → Finset (Finset α)
hf : ∀ (i_1 : ι), i_1 ∈ cons i s hi → Set.Intersecting ↑(f i_1)
hs : card (cons i s hi) ≤ Fintype.card α
f' : ι → Finset (Finset α) :=
  fun j =>
    if hj : j ∈ cons i s hi then
      Exists.choose (_ : ∃ t, f j ⊆ t ∧ 2 * card t = Fintype.card (Finset α) ∧ Set.Intersecting ↑t)
    else ∅
hf₁ : ∀ (j : ι), j ∈ cons i s hi → f j ⊆ f' j ∧ 2 * card (f' j) = 2 ^ Fintype.card α ∧ Set.Intersecting ↑(f' j)
hf₂ : ∀ (j : ι), j ∈ cons i s hi → IsUpperSet ↑(f' j)
⊢ 2 ^ Fintype.card α + (2 ^ Fintype.card α - 2 ^ (Fintype.card α - card s)) ≤
    2 * (2 ^ Fintype.card α - 2 ^ (Fintype.card α - card (cons i s hi)))
case inr.cons.refine'_3
ι : Type u_1
α : Type u_2
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : Nonempty α
s✝ : Finset ι
f✝ : ι → Finset (Finset α)
hf✝ : ∀ (i : ι), i ∈ s✝ → Set.Intersecting ↑(f✝ i)
this : DecidableEq ι
hs✝ : card s✝ ≤ Fintype.card α
i : ι
s : Finset ι
hi : ¬i ∈ s
ih :
  ∀ (f : ι → Finset (Finset α)),
    (∀ (i : ι), i ∈ s → Set.Intersecting ↑(f i)) →
      card s ≤ Fintype.card α → card (Finset.biUnion s f) ≤ 2 ^ Fintype.card α - 2 ^ (Fintype.card α - card s)
f : ι → Finset (Finset α)
hf : ∀ (i_1 : ι), i_1 ∈ cons i s hi → Set.Intersecting ↑(f i_1)
hs : card (cons i s hi) ≤ Fintype.card α
f' : ι → Finset (Finset α) :=
  fun j =>
    if hj : j ∈ cons i s hi then
      Exists.choose (_ : ∃ t, f j ⊆ t ∧ 2 * card t = Fintype.card (Finset α) ∧ Set.Intersecting ↑t)
    else ∅
hf₁ : ∀ (j : ι), j ∈ cons i s hi → f j ⊆ f' j ∧ 2 * card (f' j) = 2 ^ Fintype.card α ∧ Set.Intersecting ↑(f' j)
hf₂ : ∀ (j : ι), j ∈ cons i s hi → IsUpperSet ↑(f' j)
⊢ 2 ^ Fintype.card α + card (Finset.biUnion s fun j => f' j) ≤
    2 * (2 ^ Fintype.card α - 2 ^ (Fintype.card α - card (cons i s hi)))
refine' (add_le_add_left
  (ih _ (fun i hi ↦ (hf₁ _ <| subset_cons _ hi).2.2)
  ((card_le_of_subset <| subset_cons _).trans hs)) _).trans _
no goals
case inr.cons.refine'_3
ι : Type u_1
α : Type u_2
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : Nonempty α
s✝ : Finset ι
f✝ : ι → Finset (Finset α)
hf✝ : ∀ (i : ι), i ∈ s✝ → Set.Intersecting ↑(f✝ i)
this : DecidableEq ι
hs✝ : card s✝ ≤ Fintype.card α
i : ι
s : Finset ι
hi : ¬i ∈ s
ih :
  ∀ (f : ι → Finset (Finset α)),
    (∀ (i : ι), i ∈ s → Set.Intersecting ↑(f i)) →
      card s ≤ Fintype.card α → card (Finset.biUnion s f) ≤ 2 ^ Fintype.card α - 2 ^ (Fintype.card α - card s)
f : ι → Finset (Finset α)
hf : ∀ (i_1 : ι), i_1 ∈ cons i s hi → Set.Intersecting ↑(f i_1)
hs : card (cons i s hi) ≤ Fintype.card α
f' : ι → Finset (Finset α) :=
  fun j =>
    if hj : j ∈ cons i s hi then
      Exists.choose (_ : ∃ t, f j ⊆ t ∧ 2 * card t = Fintype.card (Finset α) ∧ Set.Intersecting ↑t)
    else ∅
hf₁ : ∀ (j : ι), j ∈ cons i s hi → f j ⊆ f' j ∧ 2 * card (f' j) = 2 ^ Fintype.card α ∧ Set.Intersecting ↑(f' j)
hf₂ : ∀ (j : ι), j ∈ cons i s hi → IsUpperSet ↑(f' j)
⊢ 2 ^ Fintype.card α + (2 ^ Fintype.card α - 2 ^ (Fintype.card α - card s)) ≤
    2 * (2 ^ Fintype.card α - 2 ^ (Fintype.card α - card (cons i s hi)))
rw [mul_tsub, two_mul, ← pow_succ,
  ← add_tsub_assoc_of_le (pow_le_pow' (one_le_two : (1 : ℕ) ≤ 2) tsub_le_self),
  tsub_add_eq_add_tsub hs, card_cons, add_tsub_add_eq_tsub_right]
no goals
ι : Type u_1
α : Type u_2
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : Nonempty α
s : Finset ι
f : ι → Finset (Finset α)
hf : ∀ (i : ι), i ∈ s → Set.Intersecting ↑(f i)
⊢ DecidableEq ι
classical
infer_instance
no goals
ι : Type u_1
α : Type u_2
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : Nonempty α
s : Finset ι
f : ι → Finset (Finset α)
hf : ∀ (i : ι), i ∈ s → Set.Intersecting ↑(f i)
⊢ DecidableEq ι
infer_instance
case inl
ι : Type u_1
α : Type u_2
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : Nonempty α
s : Finset ι
f : ι → Finset (Finset α)
hf : ∀ (i : ι), i ∈ s → Set.Intersecting ↑(f i)
this : DecidableEq ι
hs : Fintype.card α ≤ card s
⊢ card (Finset.biUnion s f) ≤ 2 ^ Fintype.card α - 1
case inl
ι : Type u_1
α : Type u_2
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : Nonempty α
s : Finset ι
f : ι → Finset (Finset α)
hf : ∀ (i : ι), i ∈ s → Set.Intersecting ↑(f i)
this : DecidableEq ι
hs : Fintype.card α ≤ card s
⊢ card (Finset.biUnion s f) ≤ 2 ^ Fintype.card α - 2 ^ (Fintype.card α - card s)
rw [tsub_eq_zero_of_le hs, pow_zero]
case inl
ι : Type u_1
α : Type u_2
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : Nonempty α
s : Finset ι
f : ι → Finset (Finset α)
hf : ∀ (i : ι), i ∈ s → Set.Intersecting ↑(f i)
this : DecidableEq ι
hs : Fintype.card α ≤ card s
⊢ card ({⊥}ᶜ) = 2 ^ Fintype.card α - 1
case inl
ι : Type u_1
α : Type u_2
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : Nonempty α
s : Finset ι
f : ι → Finset (Finset α)
hf : ∀ (i : ι), i ∈ s → Set.Intersecting ↑(f i)
this : DecidableEq ι
hs : Fintype.card α ≤ card s
⊢ card (Finset.biUnion s f) ≤ 2 ^ Fintype.card α - 1
refine' (card_le_of_subset <| biUnion_subset.2 fun i hi a ha ↦
  mem_compl.2 <| not_mem_singleton.2 <| (hf _ hi).ne_bot ha).trans_eq _
no goals
case inl
ι : Type u_1
α : Type u_2
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : Nonempty α
s : Finset ι
f : ι → Finset (Finset α)
hf : ∀ (i : ι), i ∈ s → Set.Intersecting ↑(f i)
this : DecidableEq ι
hs : Fintype.card α ≤ card s
⊢ card ({⊥}ᶜ) = 2 ^ Fintype.card α - 1
rw [card_compl, Fintype.card_finset, card_singleton]
no goals
case inr.empty
ι : Type u_1
α : Type u_2
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : Nonempty α
s : Finset ι
f✝ : ι → Finset (Finset α)
hf✝ : ∀ (i : ι), i ∈ s → Set.Intersecting ↑(f✝ i)
this : DecidableEq ι
hs✝ : card s ≤ Fintype.card α
f : ι → Finset (Finset α)
hf : ∀ (i : ι), i ∈ ∅ → Set.Intersecting ↑(f i)
hs : card ∅ ≤ Fintype.card α
⊢ card (Finset.biUnion ∅ f) ≤ 2 ^ Fintype.card α - 2 ^ (Fintype.card α - card ∅)
simp
ι : Type u_1
α : Type u_2
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : Nonempty α
s✝ : Finset ι
f✝ : ι → Finset (Finset α)
hf✝ : ∀ (i : ι), i ∈ s✝ → Set.Intersecting ↑(f✝ i)
this : DecidableEq ι
hs✝ : card s✝ ≤ Fintype.card α
i : ι
s : Finset ι
hi : ¬i ∈ s
ih :
  ∀ (f : ι → Finset (Finset α)),
    (∀ (i : ι), i ∈ s → Set.Intersecting ↑(f i)) →
      card s ≤ Fintype.card α → card (Finset.biUnion s f) ≤ 2 ^ Fintype.card α - 2 ^ (Fintype.card α - card s)
f : ι → Finset (Finset α)
hf : ∀ (i_1 : ι), i_1 ∈ cons i s hi → Set.Intersecting ↑(f i_1)
hs : card (cons i s hi) ≤ Fintype.card α
f' : ι → Finset (Finset α) :=
  fun j =>
    if hj : j ∈ cons i s hi then
      Exists.choose (_ : ∃ t, f j ⊆ t ∧ 2 * card t = Fintype.card (Finset α) ∧ Set.Intersecting ↑t)
    else ∅
j : ι
hj : j ∈ cons i s hi
⊢ f j ⊆ f' j ∧ 2 * card (f' j) = 2 ^ Fintype.card α ∧ Set.Intersecting ↑(f' j)
ι : Type u_1
α : Type u_2
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : Nonempty α
s✝ : Finset ι
f✝ : ι → Finset (Finset α)
hf✝ : ∀ (i : ι), i ∈ s✝ → Set.Intersecting ↑(f✝ i)
this : DecidableEq ι
hs✝ : card s✝ ≤ Fintype.card α
i : ι
s : Finset ι
hi : ¬i ∈ s
ih :
  ∀ (f : ι → Finset (Finset α)),
    (∀ (i : ι), i ∈ s → Set.Intersecting ↑(f i)) →
      card s ≤ Fintype.card α → card (Finset.biUnion s f) ≤ 2 ^ Fintype.card α - 2 ^ (Fintype.card α - card s)
f : ι → Finset (Finset α)
hf : ∀ (i_1 : ι), i_1 ∈ cons i s hi → Set.Intersecting ↑(f i_1)
hs : card (cons i s hi) ≤ Fintype.card α
f' : ι → Finset (Finset α) :=
  fun j =>
    if hj : j ∈ cons i s hi then
      Exists.choose (_ : ∃ t, f j ⊆ t ∧ 2 * card t = Fintype.card (Finset α) ∧ Set.Intersecting ↑t)
    else ∅
⊢ ∀ (j : ι), j ∈ cons i s hi → f j ⊆ f' j ∧ 2 * card (f' j) = 2 ^ Fintype.card α ∧ Set.Intersecting ↑(f' j)
rintro j hj
ι : Type u_1
α : Type u_2
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : Nonempty α
s✝ : Finset ι
f✝ : ι → Finset (Finset α)
hf✝ : ∀ (i : ι), i ∈ s✝ → Set.Intersecting ↑(f✝ i)
this : DecidableEq ι
hs✝ : card s✝ ≤ Fintype.card α
i : ι
s : Finset ι
hi : ¬i ∈ s
ih :
  ∀ (f : ι → Finset (Finset α)),
    (∀ (i : ι), i ∈ s → Set.Intersecting ↑(f i)) →
      card s ≤ Fintype.card α → card (Finset.biUnion s f) ≤ 2 ^ Fintype.card α - 2 ^ (Fintype.card α - card s)
f : ι → Finset (Finset α)
hf : ∀ (i_1 : ι), i_1 ∈ cons i s hi → Set.Intersecting ↑(f i_1)
hs : card (cons i s hi) ≤ Fintype.card α
f' : ι → Finset (Finset α) :=
  fun j =>
    if hj : j ∈ cons i s hi then
      Exists.choose (_ : ∃ t, f j ⊆ t ∧ 2 * card t = Fintype.card (Finset α) ∧ Set.Intersecting ↑t)
    else ∅
j : ι
hj : j ∈ cons i s hi
⊢ f j ⊆ Exists.choose (_ : ∃ t, f j ⊆ t ∧ 2 * card t = Fintype.card (Finset α) ∧ Set.Intersecting ↑t) ∧
    2 * card (Exists.choose (_ : ∃ t, f j ⊆ t ∧ 2 * card t = Fintype.card (Finset α) ∧ Set.Intersecting ↑t)) =
        Fintype.card (Finset α) ∧
      Set.Intersecting ↑(Exists.choose (_ : ∃ t, f j ⊆ t ∧ 2 * card t = Fintype.card (Finset α) ∧ Set.Intersecting ↑t))
ι : Type u_1
α : Type u_2
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : Nonempty α
s✝ : Finset ι
f✝ : ι → Finset (Finset α)
hf✝ : ∀ (i : ι), i ∈ s✝ → Set.Intersecting ↑(f✝ i)
this : DecidableEq ι
hs✝ : card s✝ ≤ Fintype.card α
i : ι
s : Finset ι
hi : ¬i ∈ s
ih :
  ∀ (f : ι → Finset (Finset α)),
    (∀ (i : ι), i ∈ s → Set.Intersecting ↑(f i)) →
      card s ≤ Fintype.card α → card (Finset.biUnion s f) ≤ 2 ^ Fintype.card α - 2 ^ (Fintype.card α - card s)
f : ι → Finset (Finset α)
hf : ∀ (i_1 : ι), i_1 ∈ cons i s hi → Set.Intersecting ↑(f i_1)
hs : card (cons i s hi) ≤ Fintype.card α
f' : ι → Finset (Finset α) :=
  fun j =>
    if hj : j ∈ cons i s hi then
      Exists.choose (_ : ∃ t, f j ⊆ t ∧ 2 * card t = Fintype.card (Finset α) ∧ Set.Intersecting ↑t)
    else ∅
j : ι
hj : j ∈ cons i s hi
⊢ f j ⊆ f' j ∧ 2 * card (f' j) = 2 ^ Fintype.card α ∧ Set.Intersecting ↑(f' j)
simp_rw [dif_pos hj, ← Fintype.card_finset]
no goals
ι : Type u_1
α : Type u_2
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : Nonempty α
s✝ : Finset ι
f✝ : ι → Finset (Finset α)
hf✝ : ∀ (i : ι), i ∈ s✝ → Set.Intersecting ↑(f✝ i)
this : DecidableEq ι
hs✝ : card s✝ ≤ Fintype.card α
i : ι
s : Finset ι
hi : ¬i ∈ s
ih :
  ∀ (f : ι → Finset (Finset α)),
    (∀ (i : ι), i ∈ s → Set.Intersecting ↑(f i)) →
      card s ≤ Fintype.card α → card (Finset.biUnion s f) ≤ 2 ^ Fintype.card α - 2 ^ (Fintype.card α - card s)
f : ι → Finset (Finset α)
hf : ∀ (i_1 : ι), i_1 ∈ cons i s hi → Set.Intersecting ↑(f i_1)
hs : card (cons i s hi) ≤ Fintype.card α
f' : ι → Finset (Finset α) :=
  fun j =>
    if hj : j ∈ cons i s hi then
      Exists.choose (_ : ∃ t, f j ⊆ t ∧ 2 * card t = Fintype.card (Finset α) ∧ Set.Intersecting ↑t)
    else ∅
j : ι
hj : j ∈ cons i s hi
⊢ f j ⊆ Exists.choose (_ : ∃ t, f j ⊆ t ∧ 2 * card t = Fintype.card (Finset α) ∧ Set.Intersecting ↑t) ∧
    2 * card (Exists.choose (_ : ∃ t, f j ⊆ t ∧ 2 * card t = Fintype.card (Finset α) ∧ Set.Intersecting ↑t)) =
        Fintype.card (Finset α) ∧
      Set.Intersecting ↑(Exists.choose (_ : ∃ t, f j ⊆ t ∧ 2 * card t = Fintype.card (Finset α) ∧ Set.Intersecting ↑t))
exact Classical.choose_spec (hf j hj).exists_card_eq
ι : Type u_1
α : Type u_2
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : Nonempty α
s✝ : Finset ι
f✝ : ι → Finset (Finset α)
hf✝ : ∀ (i : ι), i ∈ s✝ → Set.Intersecting ↑(f✝ i)
this : DecidableEq ι
hs✝ : card s✝ ≤ Fintype.card α
i : ι
s : Finset ι
hi : ¬i ∈ s
ih :
  ∀ (f : ι → Finset (Finset α)),
    (∀ (i : ι), i ∈ s → Set.Intersecting ↑(f i)) →
      card s ≤ Fintype.card α → card (Finset.biUnion s f) ≤ 2 ^ Fintype.card α - 2 ^ (Fintype.card α - card s)
f : ι → Finset (Finset α)
hf : ∀ (i_1 : ι), i_1 ∈ cons i s hi → Set.Intersecting ↑(f i_1)
hs : card (cons i s hi) ≤ Fintype.card α
f' : ι → Finset (Finset α) :=
  fun j =>
    if hj : j ∈ cons i s hi then
      Exists.choose (_ : ∃ t, f j ⊆ t ∧ 2 * card t = Fintype.card (Finset α) ∧ Set.Intersecting ↑t)
    else ∅
hf₁ : ∀ (j : ι), j ∈ cons i s hi → f j ⊆ f' j ∧ 2 * card (f' j) = 2 ^ Fintype.card α ∧ Set.Intersecting ↑(f' j)
j : ι
hj : j ∈ cons i s hi
⊢ 2 * card (f' j) = Fintype.card (Finset α)
ι : Type u_1
α : Type u_2
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : Nonempty α
s✝ : Finset ι
f✝ : ι → Finset (Finset α)
hf✝ : ∀ (i : ι), i ∈ s✝ → Set.Intersecting ↑(f✝ i)
this : DecidableEq ι
hs✝ : card s✝ ≤ Fintype.card α
i : ι
s : Finset ι
hi : ¬i ∈ s
ih :
  ∀ (f : ι → Finset (Finset α)),
    (∀ (i : ι), i ∈ s → Set.Intersecting ↑(f i)) →
      card s ≤ Fintype.card α → card (Finset.biUnion s f) ≤ 2 ^ Fintype.card α - 2 ^ (Fintype.card α - card s)
f : ι → Finset (Finset α)
hf : ∀ (i_1 : ι), i_1 ∈ cons i s hi → Set.Intersecting ↑(f i_1)
hs : card (cons i s hi) ≤ Fintype.card α
f' : ι → Finset (Finset α) :=
  fun j =>
    if hj : j ∈ cons i s hi then
      Exists.choose (_ : ∃ t, f j ⊆ t ∧ 2 * card t = Fintype.card (Finset α) ∧ Set.Intersecting ↑t)
    else ∅
hf₁ : ∀ (j : ι), j ∈ cons i s hi → f j ⊆ f' j ∧ 2 * card (f' j) = 2 ^ Fintype.card α ∧ Set.Intersecting ↑(f' j)
⊢ ∀ (j : ι), j ∈ cons i s hi → IsUpperSet ↑(f' j)
refine' fun j hj ↦ (hf₁ _ hj).2.2.isUpperSet' ((hf₁ _ hj).2.2.is_max_iff_card_eq.2 _)
ι : Type u_1
α : Type u_2
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : Nonempty α
s✝ : Finset ι
f✝ : ι → Finset (Finset α)
hf✝ : ∀ (i : ι), i ∈ s✝ → Set.Intersecting ↑(f✝ i)
this : DecidableEq ι
hs✝ : card s✝ ≤ Fintype.card α
i : ι
s : Finset ι
hi : ¬i ∈ s
ih :
  ∀ (f : ι → Finset (Finset α)),
    (∀ (i : ι), i ∈ s → Set.Intersecting ↑(f i)) →
      card s ≤ Fintype.card α → card (Finset.biUnion s f) ≤ 2 ^ Fintype.card α - 2 ^ (Fintype.card α - card s)
f : ι → Finset (Finset α)
hf : ∀ (i_1 : ι), i_1 ∈ cons i s hi → Set.Intersecting ↑(f i_1)
hs : card (cons i s hi) ≤ Fintype.card α
f' : ι → Finset (Finset α) :=
  fun j =>
    if hj : j ∈ cons i s hi then
      Exists.choose (_ : ∃ t, f j ⊆ t ∧ 2 * card t = Fintype.card (Finset α) ∧ Set.Intersecting ↑t)
    else ∅
hf₁ : ∀ (j : ι), j ∈ cons i s hi → f j ⊆ f' j ∧ 2 * card (f' j) = 2 ^ Fintype.card α ∧ Set.Intersecting ↑(f' j)
j : ι
hj : j ∈ cons i s hi
⊢ 2 * card (f' j) = 2 ^ Fintype.card α
ι : Type u_1
α : Type u_2
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : Nonempty α
s✝ : Finset ι
f✝ : ι → Finset (Finset α)
hf✝ : ∀ (i : ι), i ∈ s✝ → Set.Intersecting ↑(f✝ i)
this : DecidableEq ι
hs✝ : card s✝ ≤ Fintype.card α
i : ι
s : Finset ι
hi : ¬i ∈ s
ih :
  ∀ (f : ι → Finset (Finset α)),
    (∀ (i : ι), i ∈ s → Set.Intersecting ↑(f i)) →
      card s ≤ Fintype.card α → card (Finset.biUnion s f) ≤ 2 ^ Fintype.card α - 2 ^ (Fintype.card α - card s)
f : ι → Finset (Finset α)
hf : ∀ (i_1 : ι), i_1 ∈ cons i s hi → Set.Intersecting ↑(f i_1)
hs : card (cons i s hi) ≤ Fintype.card α
f' : ι → Finset (Finset α) :=
  fun j =>
    if hj : j ∈ cons i s hi then
      Exists.choose (_ : ∃ t, f j ⊆ t ∧ 2 * card t = Fintype.card (Finset α) ∧ Set.Intersecting ↑t)
    else ∅
hf₁ : ∀ (j : ι), j ∈ cons i s hi → f j ⊆ f' j ∧ 2 * card (f' j) = 2 ^ Fintype.card α ∧ Set.Intersecting ↑(f' j)
j : ι
hj : j ∈ cons i s hi
⊢ 2 * card (f' j) = Fintype.card (Finset α)
rw [Fintype.card_finset]
no goals
ι : Type u_1
α : Type u_2
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : Nonempty α
s✝ : Finset ι
f✝ : ι → Finset (Finset α)
hf✝ : ∀ (i : ι), i ∈ s✝ → Set.Intersecting ↑(f✝ i)
this : DecidableEq ι
hs✝ : card s✝ ≤ Fintype.card α
i : ι
s : Finset ι
hi : ¬i ∈ s
ih :
  ∀ (f : ι → Finset (Finset α)),
    (∀ (i : ι), i ∈ s → Set.Intersecting ↑(f i)) →
      card s ≤ Fintype.card α → card (Finset.biUnion s f) ≤ 2 ^ Fintype.card α - 2 ^ (Fintype.card α - card s)
f : ι → Finset (Finset α)
hf : ∀ (i_1 : ι), i_1 ∈ cons i s hi → Set.Intersecting ↑(f i_1)
hs : card (cons i s hi) ≤ Fintype.card α
f' : ι → Finset (Finset α) :=
  fun j =>
    if hj : j ∈ cons i s hi then
      Exists.choose (_ : ∃ t, f j ⊆ t ∧ 2 * card t = Fintype.card (Finset α) ∧ Set.Intersecting ↑t)
    else ∅
hf₁ : ∀ (j : ι), j ∈ cons i s hi → f j ⊆ f' j ∧ 2 * card (f' j) = 2 ^ Fintype.card α ∧ Set.Intersecting ↑(f' j)
j : ι
hj : j ∈ cons i s hi
⊢ 2 * card (f' j) = 2 ^ Fintype.card α
exact (hf₁ _ hj).2.1
case inr.cons.refine'_1
ι : Type u_1
α : Type u_2
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : Nonempty α
s✝ : Finset ι
f✝ : ι → Finset (Finset α)
hf✝ : ∀ (i : ι), i ∈ s✝ → Set.Intersecting ↑(f✝ i)
this : DecidableEq ι
hs✝ : card s✝ ≤ Fintype.card α
i : ι
s : Finset ι
hi : ¬i ∈ s
ih :
  ∀ (f : ι → Finset (Finset α)),
    (∀ (i : ι), i ∈ s → Set.Intersecting ↑(f i)) →
      card s ≤ Fintype.card α → card (Finset.biUnion s f) ≤ 2 ^ Fintype.card α - 2 ^ (Fintype.card α - card s)
f : ι → Finset (Finset α)
hf : ∀ (i_1 : ι), i_1 ∈ cons i s hi → Set.Intersecting ↑(f i_1)
hs : card (cons i s hi) ≤ Fintype.card α
f' : ι → Finset (Finset α) :=
  fun j =>
    if hj : j ∈ cons i s hi then
      Exists.choose (_ : ∃ t, f j ⊆ t ∧ 2 * card t = Fintype.card (Finset α) ∧ Set.Intersecting ↑t)
    else ∅
hf₁ : ∀ (j : ι), j ∈ cons i s hi → f j ⊆ f' j ∧ 2 * card (f' j) = 2 ^ Fintype.card α ∧ Set.Intersecting ↑(f' j)
hf₂ : ∀ (j : ι), j ∈ cons i s hi → IsUpperSet ↑(f' j)
⊢ IsUpperSet (⋃ (x : ι) (_ : x ∈ ↑s), ↑(f' x))
case inr.cons.refine'_1
ι : Type u_1
α : Type u_2
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : Nonempty α
s✝ : Finset ι
f✝ : ι → Finset (Finset α)
hf✝ : ∀ (i : ι), i ∈ s✝ → Set.Intersecting ↑(f✝ i)
this : DecidableEq ι
hs✝ : card s✝ ≤ Fintype.card α
i : ι
s : Finset ι
hi : ¬i ∈ s
ih :
  ∀ (f : ι → Finset (Finset α)),
    (∀ (i : ι), i ∈ s → Set.Intersecting ↑(f i)) →
      card s ≤ Fintype.card α → card (Finset.biUnion s f) ≤ 2 ^ Fintype.card α - 2 ^ (Fintype.card α - card s)
f : ι → Finset (Finset α)
hf : ∀ (i_1 : ι), i_1 ∈ cons i s hi → Set.Intersecting ↑(f i_1)
hs : card (cons i s hi) ≤ Fintype.card α
f' : ι → Finset (Finset α) :=
  fun j =>
    if hj : j ∈ cons i s hi then
      Exists.choose (_ : ∃ t, f j ⊆ t ∧ 2 * card t = Fintype.card (Finset α) ∧ Set.Intersecting ↑t)
    else ∅
hf₁ : ∀ (j : ι), j ∈ cons i s hi → f j ⊆ f' j ∧ 2 * card (f' j) = 2 ^ Fintype.card α ∧ Set.Intersecting ↑(f' j)
hf₂ : ∀ (j : ι), j ∈ cons i s hi → IsUpperSet ↑(f' j)
⊢ IsUpperSet ↑(Finset.biUnion s fun j => f' j)
rw [coe_biUnion]
no goals
case inr.cons.refine'_1
ι : Type u_1
α : Type u_2
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : Nonempty α
s✝ : Finset ι
f✝ : ι → Finset (Finset α)
hf✝ : ∀ (i : ι), i ∈ s✝ → Set.Intersecting ↑(f✝ i)
this : DecidableEq ι
hs✝ : card s✝ ≤ Fintype.card α
i : ι
s : Finset ι
hi : ¬i ∈ s
ih :
  ∀ (f : ι → Finset (Finset α)),
    (∀ (i : ι), i ∈ s → Set.Intersecting ↑(f i)) →
      card s ≤ Fintype.card α → card (Finset.biUnion s f) ≤ 2 ^ Fintype.card α - 2 ^ (Fintype.card α - card s)
f : ι → Finset (Finset α)
hf : ∀ (i_1 : ι), i_1 ∈ cons i s hi → Set.Intersecting ↑(f i_1)
hs : card (cons i s hi) ≤ Fintype.card α
f' : ι → Finset (Finset α) :=
  fun j =>
    if hj : j ∈ cons i s hi then
      Exists.choose (_ : ∃ t, f j ⊆ t ∧ 2 * card t = Fintype.card (Finset α) ∧ Set.Intersecting ↑t)
    else ∅
hf₁ : ∀ (j : ι), j ∈ cons i s hi → f j ⊆ f' j ∧ 2 * card (f' j) = 2 ^ Fintype.card α ∧ Set.Intersecting ↑(f' j)
hf₂ : ∀ (j : ι), j ∈ cons i s hi → IsUpperSet ↑(f' j)
⊢ IsUpperSet (⋃ (x : ι) (_ : x ∈ ↑s), ↑(f' x))
exact isUpperSet_iUnion₂ fun i hi ↦ hf₂ _ <| subset_cons _ hi
case inr.cons.refine'_2
ι : Type u_1
α : Type u_2
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : Nonempty α
s✝ : Finset ι
f✝ : ι → Finset (Finset α)
hf✝ : ∀ (i : ι), i ∈ s✝ → Set.Intersecting ↑(f✝ i)
this : DecidableEq ι
hs✝ : card s✝ ≤ Fintype.card α
i : ι
s : Finset ι
hi : ¬i ∈ s
ih :
  ∀ (f : ι → Finset (Finset α)),
    (∀ (i : ι), i ∈ s → Set.Intersecting ↑(f i)) →
      card s ≤ Fintype.card α → card (Finset.biUnion s f) ≤ 2 ^ Fintype.card α - 2 ^ (Fintype.card α - card s)
f : ι → Finset (Finset α)
hf : ∀ (i_1 : ι), i_1 ∈ cons i s hi → Set.Intersecting ↑(f i_1)
hs : card (cons i s hi) ≤ Fintype.card α
f' : ι → Finset (Finset α) :=
  fun j =>
    if hj : j ∈ cons i s hi then
      Exists.choose (_ : ∃ t, f j ⊆ t ∧ 2 * card t = Fintype.card (Finset α) ∧ Set.Intersecting ↑t)
    else ∅
hf₁ : ∀ (j : ι), j ∈ cons i s hi → f j ⊆ f' j ∧ 2 * card (f' j) = 2 ^ Fintype.card α ∧ Set.Intersecting ↑(f' j)
hf₂ : ∀ (j : ι), j ∈ cons i s hi → IsUpperSet ↑(f' j)
⊢ IsLowerSet (↑(f' i)ᶜ)
case inr.cons.refine'_2
ι : Type u_1
α : Type u_2
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : Nonempty α
s✝ : Finset ι
f✝ : ι → Finset (Finset α)
hf✝ : ∀ (i : ι), i ∈ s✝ → Set.Intersecting ↑(f✝ i)
this : DecidableEq ι
hs✝ : card s✝ ≤ Fintype.card α
i : ι
s : Finset ι
hi : ¬i ∈ s
ih :
  ∀ (f : ι → Finset (Finset α)),
    (∀ (i : ι), i ∈ s → Set.Intersecting ↑(f i)) →
      card s ≤ Fintype.card α → card (Finset.biUnion s f) ≤ 2 ^ Fintype.card α - 2 ^ (Fintype.card α - card s)
f : ι → Finset (Finset α)
hf : ∀ (i_1 : ι), i_1 ∈ cons i s hi → Set.Intersecting ↑(f i_1)
hs : card (cons i s hi) ≤ Fintype.card α
f' : ι → Finset (Finset α) :=
  fun j =>
    if hj : j ∈ cons i s hi then
      Exists.choose (_ : ∃ t, f j ⊆ t ∧ 2 * card t = Fintype.card (Finset α) ∧ Set.Intersecting ↑t)
    else ∅
hf₁ : ∀ (j : ι), j ∈ cons i s hi → f j ⊆ f' j ∧ 2 * card (f' j) = 2 ^ Fintype.card α ∧ Set.Intersecting ↑(f' j)
hf₂ : ∀ (j : ι), j ∈ cons i s hi → IsUpperSet ↑(f' j)
⊢ IsLowerSet ↑(f' iᶜ)
rw [coe_compl]
no goals
case inr.cons.refine'_2
ι : Type u_1
α : Type u_2
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : Nonempty α
s✝ : Finset ι
f✝ : ι → Finset (Finset α)
hf✝ : ∀ (i : ι), i ∈ s✝ → Set.Intersecting ↑(f✝ i)
this : DecidableEq ι
hs✝ : card s✝ ≤ Fintype.card α
i : ι
s : Finset ι
hi : ¬i ∈ s
ih :
  ∀ (f : ι → Finset (Finset α)),
    (∀ (i : ι), i ∈ s → Set.Intersecting ↑(f i)) →
      card s ≤ Fintype.card α → card (Finset.biUnion s f) ≤ 2 ^ Fintype.card α - 2 ^ (Fintype.card α - card s)
f : ι → Finset (Finset α)
hf : ∀ (i_1 : ι), i_1 ∈ cons i s hi → Set.Intersecting ↑(f i_1)
hs : card (cons i s hi) ≤ Fintype.card α
f' : ι → Finset (Finset α) :=
  fun j =>
    if hj : j ∈ cons i s hi then
      Exists.choose (_ : ∃ t, f j ⊆ t ∧ 2 * card t = Fintype.card (Finset α) ∧ Set.Intersecting ↑t)
    else ∅
hf₁ : ∀ (j : ι), j ∈ cons i s hi → f j ⊆ f' j ∧ 2 * card (f' j) = 2 ^ Fintype.card α ∧ Set.Intersecting ↑(f' j)
hf₂ : ∀ (j : ι), j ∈ cons i s hi → IsUpperSet ↑(f' j)
⊢ IsLowerSet (↑(f' i)ᶜ)
exact (hf₂ _ <| mem_cons_self _ _).compl