α : Type u_1
inst✝² : BooleanAlgebra α
inst✝¹ : Nontrivial α
inst✝ : Fintype α
s : Finset α
hs : Intersecting ↑s
this : 2 * card s ≤ Fintype.card α
⊢ ∃ t, s ⊆ t ∧ 2 * card t = Fintype.card α ∧ Intersecting ↑t
α : Type u_1
inst✝² : BooleanAlgebra α
inst✝¹ : Nontrivial α
inst✝ : Fintype α
s : Finset α
hs : Intersecting ↑s
⊢ ∃ t, s ⊆ t ∧ 2 * card t = Fintype.card α ∧ Intersecting ↑t
have := hs.card_le
α : Type u_1
inst✝² : BooleanAlgebra α
inst✝¹ : Nontrivial α
inst✝ : Fintype α
s : Finset α
hs : Intersecting ↑s
this : card s ≤ Fintype.card α / 2
⊢ ∃ t, s ⊆ t ∧ 2 * card t = Fintype.card α ∧ Intersecting ↑t
α : Type u_1
inst✝² : BooleanAlgebra α
inst✝¹ : Nontrivial α
inst✝ : Fintype α
s : Finset α
hs : Intersecting ↑s
this : 2 * card s ≤ Fintype.card α
⊢ ∃ t, s ⊆ t ∧ 2 * card t = Fintype.card α ∧ Intersecting ↑t
rw [mul_comm, ← Nat.le_div_iff_mul_le' two_pos] at this
α : Type u_1
inst✝² : BooleanAlgebra α
inst✝¹ : Nontrivial α
inst✝ : Fintype α
s : Finset α
this : card s ≤ Fintype.card α / 2
⊢ Intersecting ↑s → ∃ t, s ⊆ t ∧ 2 * card t = Fintype.card α ∧ Intersecting ↑t
α : Type u_1
inst✝² : BooleanAlgebra α
inst✝¹ : Nontrivial α
inst✝ : Fintype α
s : Finset α
hs : Intersecting ↑s
this : card s ≤ Fintype.card α / 2
⊢ ∃ t, s ⊆ t ∧ 2 * card t = Fintype.card α ∧ Intersecting ↑t
revert hs
α : Type u_1
inst✝² : BooleanAlgebra α
inst✝¹ : Nontrivial α
inst✝ : Fintype α
s : Finset α
this : card s ≤ Fintype.card α / 2
⊢ ∀ (t₁ : Finset α),
    (∀ {t₂ : Finset α},
        card t₂ ≤ Fintype.card α / 2 →
          t₁ ⊂ t₂ → Intersecting ↑t₂ → ∃ t, t₂ ⊆ t ∧ 2 * card t = Fintype.card α ∧ Intersecting ↑t) →
      card t₁ ≤ Fintype.card α / 2 → Intersecting ↑t₁ → ∃ t, t₁ ⊆ t ∧ 2 * card t = Fintype.card α ∧ Intersecting ↑t
α : Type u_1
inst✝² : BooleanAlgebra α
inst✝¹ : Nontrivial α
inst✝ : Fintype α
s : Finset α
this : card s ≤ Fintype.card α / 2
⊢ Intersecting ↑s → ∃ t, s ⊆ t ∧ 2 * card t = Fintype.card α ∧ Intersecting ↑t
refine' s.strongDownwardInductionOn _ this
α : Type u_1
inst✝² : BooleanAlgebra α
inst✝¹ : Nontrivial α
inst✝ : Fintype α
s✝ : Finset α
this : card s✝ ≤ Fintype.card α / 2
s : Finset α
ih :
  ∀ {t₂ : Finset α},
    card t₂ ≤ Fintype.card α / 2 →
      s ⊂ t₂ → Intersecting ↑t₂ → ∃ t, t₂ ⊆ t ∧ 2 * card t = Fintype.card α ∧ Intersecting ↑t
_hcard : card s ≤ Fintype.card α / 2
hs : Intersecting ↑s
⊢ ∃ t, s ⊆ t ∧ 2 * card t = Fintype.card α ∧ Intersecting ↑t
α : Type u_1
inst✝² : BooleanAlgebra α
inst✝¹ : Nontrivial α
inst✝ : Fintype α
s : Finset α
this : card s ≤ Fintype.card α / 2
⊢ ∀ (t₁ : Finset α),
    (∀ {t₂ : Finset α},
        card t₂ ≤ Fintype.card α / 2 →
          t₁ ⊂ t₂ → Intersecting ↑t₂ → ∃ t, t₂ ⊆ t ∧ 2 * card t = Fintype.card α ∧ Intersecting ↑t) →
      card t₁ ≤ Fintype.card α / 2 → Intersecting ↑t₁ → ∃ t, t₁ ⊆ t ∧ 2 * card t = Fintype.card α ∧ Intersecting ↑t
rintro s ih _hcard hs
case pos
α : Type u_1
inst✝² : BooleanAlgebra α
inst✝¹ : Nontrivial α
inst✝ : Fintype α
s✝ : Finset α
this : card s✝ ≤ Fintype.card α / 2
s : Finset α
ih :
  ∀ {t₂ : Finset α},
    card t₂ ≤ Fintype.card α / 2 →
      s ⊂ t₂ → Intersecting ↑t₂ → ∃ t, t₂ ⊆ t ∧ 2 * card t = Fintype.card α ∧ Intersecting ↑t
_hcard : card s ≤ Fintype.card α / 2
hs : Intersecting ↑s
h : ∀ (t : Finset α), Intersecting ↑t → s ⊆ t → s = t
⊢ ∃ t, s ⊆ t ∧ 2 * card t = Fintype.card α ∧ Intersecting ↑t

case neg
α : Type u_1
inst✝² : BooleanAlgebra α
inst✝¹ : Nontrivial α
inst✝ : Fintype α
s✝ : Finset α
this : card s✝ ≤ Fintype.card α / 2
s : Finset α
ih :
  ∀ {t₂ : Finset α},
    card t₂ ≤ Fintype.card α / 2 →
      s ⊂ t₂ → Intersecting ↑t₂ → ∃ t, t₂ ⊆ t ∧ 2 * card t = Fintype.card α ∧ Intersecting ↑t
_hcard : card s ≤ Fintype.card α / 2
hs : Intersecting ↑s
h : ¬∀ (t : Finset α), Intersecting ↑t → s ⊆ t → s = t
⊢ ∃ t, s ⊆ t ∧ 2 * card t = Fintype.card α ∧ Intersecting ↑t
α : Type u_1
inst✝² : BooleanAlgebra α
inst✝¹ : Nontrivial α
inst✝ : Fintype α
s✝ : Finset α
this : card s✝ ≤ Fintype.card α / 2
s : Finset α
ih :
  ∀ {t₂ : Finset α},
    card t₂ ≤ Fintype.card α / 2 →
      s ⊂ t₂ → Intersecting ↑t₂ → ∃ t, t₂ ⊆ t ∧ 2 * card t = Fintype.card α ∧ Intersecting ↑t
_hcard : card s ≤ Fintype.card α / 2
hs : Intersecting ↑s
⊢ ∃ t, s ⊆ t ∧ 2 * card t = Fintype.card α ∧ Intersecting ↑t
by_cases h : ∀ t : Finset α, (t : Set α).Intersecting → s ⊆ t → s = t
case neg
α : Type u_1
inst✝² : BooleanAlgebra α
inst✝¹ : Nontrivial α
inst✝ : Fintype α
s✝ : Finset α
this : card s✝ ≤ Fintype.card α / 2
s : Finset α
ih :
  ∀ {t₂ : Finset α},
    card t₂ ≤ Fintype.card α / 2 →
      s ⊂ t₂ → Intersecting ↑t₂ → ∃ t, t₂ ⊆ t ∧ 2 * card t = Fintype.card α ∧ Intersecting ↑t
_hcard : card s ≤ Fintype.card α / 2
hs : Intersecting ↑s
h : ∃ t, Intersecting ↑t ∧ s ⊆ t ∧ s ≠ t
⊢ ∃ t, s ⊆ t ∧ 2 * card t = Fintype.card α ∧ Intersecting ↑t
case neg
α : Type u_1
inst✝² : BooleanAlgebra α
inst✝¹ : Nontrivial α
inst✝ : Fintype α
s✝ : Finset α
this : card s✝ ≤ Fintype.card α / 2
s : Finset α
ih :
  ∀ {t₂ : Finset α},
    card t₂ ≤ Fintype.card α / 2 →
      s ⊂ t₂ → Intersecting ↑t₂ → ∃ t, t₂ ⊆ t ∧ 2 * card t = Fintype.card α ∧ Intersecting ↑t
_hcard : card s ≤ Fintype.card α / 2
hs : Intersecting ↑s
h : ¬∀ (t : Finset α), Intersecting ↑t → s ⊆ t → s = t
⊢ ∃ t, s ⊆ t ∧ 2 * card t = Fintype.card α ∧ Intersecting ↑t
push_neg  at h
case neg.intro.intro
α : Type u_1
inst✝² : BooleanAlgebra α
inst✝¹ : Nontrivial α
inst✝ : Fintype α
s✝ : Finset α
this : card s✝ ≤ Fintype.card α / 2
s : Finset α
ih :
  ∀ {t₂ : Finset α},
    card t₂ ≤ Fintype.card α / 2 →
      s ⊂ t₂ → Intersecting ↑t₂ → ∃ t, t₂ ⊆ t ∧ 2 * card t = Fintype.card α ∧ Intersecting ↑t
_hcard : card s ≤ Fintype.card α / 2
hs : Intersecting ↑s
t : Finset α
ht : Intersecting ↑t
hst : s ⊆ t ∧ s ≠ t
⊢ ∃ t, s ⊆ t ∧ 2 * card t = Fintype.card α ∧ Intersecting ↑t
case neg
α : Type u_1
inst✝² : BooleanAlgebra α
inst✝¹ : Nontrivial α
inst✝ : Fintype α
s✝ : Finset α
this : card s✝ ≤ Fintype.card α / 2
s : Finset α
ih :
  ∀ {t₂ : Finset α},
    card t₂ ≤ Fintype.card α / 2 →
      s ⊂ t₂ → Intersecting ↑t₂ → ∃ t, t₂ ⊆ t ∧ 2 * card t = Fintype.card α ∧ Intersecting ↑t
_hcard : card s ≤ Fintype.card α / 2
hs : Intersecting ↑s
h : ∃ t, Intersecting ↑t ∧ s ⊆ t ∧ s ≠ t
⊢ ∃ t, s ⊆ t ∧ 2 * card t = Fintype.card α ∧ Intersecting ↑t
obtain ⟨t, ht, hst⟩ := h
case neg.intro.intro
α : Type u_1
inst✝² : BooleanAlgebra α
inst✝¹ : Nontrivial α
inst✝ : Fintype α
s✝ : Finset α
this : card s✝ ≤ Fintype.card α / 2
s : Finset α
ih :
  ∀ {t₂ : Finset α},
    card t₂ ≤ Fintype.card α / 2 →
      s ⊂ t₂ → Intersecting ↑t₂ → ∃ t, t₂ ⊆ t ∧ 2 * card t = Fintype.card α ∧ Intersecting ↑t
_hcard : card s ≤ Fintype.card α / 2
hs : Intersecting ↑s
t : Finset α
ht : Intersecting ↑t
hst : s ⊆ t ∧ s ≠ t
⊢ card t ≤ Fintype.card α / 2
case neg.intro.intro
α : Type u_1
inst✝² : BooleanAlgebra α
inst✝¹ : Nontrivial α
inst✝ : Fintype α
s✝ : Finset α
this : card s✝ ≤ Fintype.card α / 2
s : Finset α
ih :
  ∀ {t₂ : Finset α},
    card t₂ ≤ Fintype.card α / 2 →
      s ⊂ t₂ → Intersecting ↑t₂ → ∃ t, t₂ ⊆ t ∧ 2 * card t = Fintype.card α ∧ Intersecting ↑t
_hcard : card s ≤ Fintype.card α / 2
hs : Intersecting ↑s
t : Finset α
ht : Intersecting ↑t
hst : s ⊆ t ∧ s ≠ t
⊢ ∃ t, s ⊆ t ∧ 2 * card t = Fintype.card α ∧ Intersecting ↑t
refine' (ih _ (_root_.ssubset_iff_subset_ne.2 hst) ht).imp fun u => And.imp_left hst.1.trans
case neg.intro.intro
α : Type u_1
inst✝² : BooleanAlgebra α
inst✝¹ : Nontrivial α
inst✝ : Fintype α
s✝ : Finset α
this : card s✝ ≤ Fintype.card α / 2
s : Finset α
ih :
  ∀ {t₂ : Finset α},
    card t₂ ≤ Fintype.card α / 2 →
      s ⊂ t₂ → Intersecting ↑t₂ → ∃ t, t₂ ⊆ t ∧ 2 * card t = Fintype.card α ∧ Intersecting ↑t
_hcard : card s ≤ Fintype.card α / 2
hs : Intersecting ↑s
t : Finset α
ht : Intersecting ↑t
hst : s ⊆ t ∧ s ≠ t
⊢ 2 * card t ≤ Fintype.card α
case neg.intro.intro
α : Type u_1
inst✝² : BooleanAlgebra α
inst✝¹ : Nontrivial α
inst✝ : Fintype α
s✝ : Finset α
this : card s✝ ≤ Fintype.card α / 2
s : Finset α
ih :
  ∀ {t₂ : Finset α},
    card t₂ ≤ Fintype.card α / 2 →
      s ⊂ t₂ → Intersecting ↑t₂ → ∃ t, t₂ ⊆ t ∧ 2 * card t = Fintype.card α ∧ Intersecting ↑t
_hcard : card s ≤ Fintype.card α / 2
hs : Intersecting ↑s
t : Finset α
ht : Intersecting ↑t
hst : s ⊆ t ∧ s ≠ t
⊢ card t ≤ Fintype.card α / 2
rw [Nat.le_div_iff_mul_le' two_pos, mul_comm]
no goals
case neg.intro.intro
α : Type u_1
inst✝² : BooleanAlgebra α
inst✝¹ : Nontrivial α
inst✝ : Fintype α
s✝ : Finset α
this : card s✝ ≤ Fintype.card α / 2
s : Finset α
ih :
  ∀ {t₂ : Finset α},
    card t₂ ≤ Fintype.card α / 2 →
      s ⊂ t₂ → Intersecting ↑t₂ → ∃ t, t₂ ⊆ t ∧ 2 * card t = Fintype.card α ∧ Intersecting ↑t
_hcard : card s ≤ Fintype.card α / 2
hs : Intersecting ↑s
t : Finset α
ht : Intersecting ↑t
hst : s ⊆ t ∧ s ≠ t
⊢ 2 * card t ≤ Fintype.card α
exact ht.card_le
no goals
case pos
α : Type u_1
inst✝² : BooleanAlgebra α
inst✝¹ : Nontrivial α
inst✝ : Fintype α
s✝ : Finset α
this : card s✝ ≤ Fintype.card α / 2
s : Finset α
ih :
  ∀ {t₂ : Finset α},
    card t₂ ≤ Fintype.card α / 2 →
      s ⊂ t₂ → Intersecting ↑t₂ → ∃ t, t₂ ⊆ t ∧ 2 * card t = Fintype.card α ∧ Intersecting ↑t
_hcard : card s ≤ Fintype.card α / 2
hs : Intersecting ↑s
h : ∀ (t : Finset α), Intersecting ↑t → s ⊆ t → s = t
⊢ ∃ t, s ⊆ t ∧ 2 * card t = Fintype.card α ∧ Intersecting ↑t
exact ⟨s, Subset.rfl, hs.is_max_iff_card_eq.1 h, hs⟩