1. FormalConjectures
  2. Wikipedia
  3. UnionClosed
/- Copyright 2025 The Formal Conjectures Authors. Licensed under the Apache License, Version 2.0 (the "License"); you may not use this file except in compliance with the License. You may obtain a copy of the License at https://www.apache.org/licenses/LICENSE-2.0 Unless required by applicable law or agreed to in writing, software distributed under the License is distributed on an "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. See the License for the specific language governing permissions and limitations under the License. -/ import FormalConjecturesUtil

Union-closed sets conjecture

Reference: Wikipedia

In this file, we:

    state the conjecture

    state three solved variants of the conjecture, without proof

    prove two solved variants of the conjecture

    prove the conjecture is sharp

open Finset variable {n : Type*} [DecidableEq n] {A : Finset (Finset n)} namespace UnionClosed abbrev IsUnionClosed (A : Finset (Finset n)) : Prop := ∀ᵉ (X ∈ A) (Y ∈ A), X ∪ Y ∈ A @[category API, AMS 5] lemma isUnionClosed_univ (n : Type*) [DecidableEq n] [Fintype n] : IsUnionClosed (univ (α := Finset n)) := n:Type u_2inst✝¹:DecidableEq ninst✝:Fintype n⊢ IsUnionClosed univ All goals completed! 🐙 @[category API, AMS 5] lemma isUnionClosed_powerset (S : Finset n) : IsUnionClosed S.powerset := n:Type u_1inst✝:DecidableEq nS:Finset n⊢ IsUnionClosed S.powerset intro X n:Type u_1inst✝:DecidableEq nS:Finset nX:Finset nhX:X ∈ S.powerset⊢ ∀ Y ∈ S.powerset, X ∪ Y ∈ S.powerset n:Type u_1inst✝:DecidableEq nS:Finset nX:Finset nhX:X ∈ S.powersetY:Finset n⊢ Y ∈ S.powerset → X ∪ Y ∈ S.powerset n:Type u_1inst✝:DecidableEq nS:Finset nX:Finset nhX:X ∈ S.powersetY:Finset nhY:Y ∈ S.powerset⊢ X ∪ Y ∈ S.powerset n:Type u_1inst✝:DecidableEq nS:Finset nX:Finset nhX:X ⊆ SY:Finset nhY:Y ⊆ S⊢ X ∪ Y ⊆ S All goals completed! 🐙

For every finite union-closed family of sets, other than the family containing only the empty set, there exists an element that belongs to at least half of the sets in the family.

@[category research open, AMS 5] theorem declaration uses 'sorry'union_closed [Nonempty n] (h_ne_singleton_empty : A ≠ {∅}) (h_union_closed : IsUnionClosed A) : ∃ i : n, (1 / 2 : ℚ) * #A ≤ #{x ∈ A | i ∈ x} := n:Type u_1inst✝¹:DecidableEq nA:Finset (Finset n)inst✝:Nonempty nh_ne_singleton_empty:A ≠ {∅}h_union_closed:IsUnionClosed A⊢ ∃ i, 1 / 2 * ↑(#A) ≤ ↑(#({x ∈ A | i ∈ x})) All goals completed! 🐙

Yu [Yu23] showed that the union-closed sets conjecture holds with a constant of approximately 0.38234 instead of 1/2. [Yu23] Yu, Lei (2023). "Dimension-free bounds for the union-closed sets conjecture". Entropy. 25 (5): 767.

@[category research solved, AMS 5] theorem declaration uses 'sorry'union_closed.variants.yu [Nonempty n] (h_ne_singleton_empty : A ≠ {∅}) (h_union_closed : IsUnionClosed A) : ∃ i : n, (0.38234 : ℚ) * #A ≤ #{x ∈ A | i ∈ x} := n:Type u_1inst✝¹:DecidableEq nA:Finset (Finset n)inst✝:Nonempty nh_ne_singleton_empty:A ≠ {∅}h_union_closed:IsUnionClosed A⊢ ∃ i, 0.38234 * ↑(#A) ≤ ↑(#({x ∈ A | i ∈ x})) All goals completed! 🐙

Vuckovic and Zivkovic [Vu17] showed that the union-closed sets conjecture holds for set families whose universal set has cardinality at most 12. [Vu17] Vuckovic, Bojan; Zivkovic, Miodrag (2017). "The 12-Element Case of Frankl's Conjecture" (PDF). IPSI BGD Transactions on Internet Research. 13 (1): 65.

@[category research solved, AMS 5] theorem declaration uses 'sorry'union_closed.variants.univ_card [Fintype n] [Nonempty n] (h_ne_singleton_empty : A ≠ {∅}) (h_union_closed : IsUnionClosed A) (h_card : Fintype.card n ≤ 12) : ∃ i : n, (1 / 2 : ℚ) * #A ≤ #{x ∈ A | i ∈ x} := n:Type u_1inst✝²:DecidableEq nA:Finset (Finset n)inst✝¹:Fintype ninst✝:Nonempty nh_ne_singleton_empty:A ≠ {∅}h_union_closed:IsUnionClosed Ah_card:Fintype.card n ≤ 12⊢ ∃ i, 1 / 2 * ↑(#A) ≤ ↑(#({x ∈ A | i ∈ x})) All goals completed! 🐙

Roberts and Simpson [Ro10] showed that the union-closed sets conjecture holds for set families of size at most 46. Their method, however, combined with the result of [Vu17], further shows that it holds for #A ≤ 50 as well. [Ro10] Roberts, Ian; Simpson, Jamie (2010). "A note on the union-closed sets conjecture" (PDF). Australas. J. Combin. 47: 265–267. [Vu17] Vuckovic, Bojan; Zivkovic, Miodrag (2017). "The 12-Element Case of Frankl's Conjecture" (PDF). IPSI BGD Transactions on Internet Research. 13 (1): 65.

@[category research solved, AMS 5] theorem declaration uses 'sorry'union_closed.variants.family_card [Nonempty n] (h_ne_singleton_empty : A ≠ {∅}) (h_union_closed : IsUnionClosed A) (hA : #A ≤ 50) : ∃ i : n, (1 / 2 : ℚ) * #A ≤ #{x ∈ A | i ∈ x} := n:Type u_1inst✝¹:DecidableEq nA:Finset (Finset n)inst✝:Nonempty nh_ne_singleton_empty:A ≠ {∅}h_union_closed:IsUnionClosed AhA:#A ≤ 50⊢ ∃ i, 1 / 2 * ↑(#A) ≤ ↑(#({x ∈ A | i ∈ x})) All goals completed! 🐙

We can show the union-closed sets conjecture is true for the case where the universal set has cardinality 2, by brute force.

@[category research solved, AMS 5] theorem union_closed.variants.univ_card_two (A : Finset (Finset (Fin 2))) (h_ne_singleton_empty : A ≠ {∅}) (h_union_closed : IsUnionClosed A) : ∃ i, (1 / 2 : ℚ) * #A ≤ #{x ∈ A | i ∈ x} := A:Finset (Finset (Fin 2))h_ne_singleton_empty:A ≠ {∅}h_union_closed:IsUnionClosed A⊢ ∃ i, 1 / 2 * ↑(#A) ≤ ↑(#({x ∈ A | i ∈ x})) All goals completed! 🐙

We can show the union-closed sets conjecture is true for the case where the set family contains some singleton.

@[category research solved, AMS 5] theorem union_closed.variants.singleton_mem (h_union_closed : IsUnionClosed A) (i : n) (hi : {i} ∈ A) : ∃ i, (1 / 2 : ℚ) * #A ≤ #{x ∈ A | i ∈ x} := n:Type u_1inst✝:DecidableEq nA:Finset (Finset n)h_union_closed:IsUnionClosed Ai:nhi:{i} ∈ A⊢ ∃ i, 1 / 2 * ↑(#A) ≤ ↑(#({x ∈ A | i ∈ x})) n:Type u_1inst✝:DecidableEq nA:Finset (Finset n)h_union_closed:IsUnionClosed Ai:nhi:{i} ∈ A⊢ 1 / 2 * ↑(#A) ≤ ↑(#({x ∈ A | i ∈ x})) n:Type u_1inst✝:DecidableEq nA:Finset (Finset n)h_union_closed:IsUnionClosed Ai:nhi:{i} ∈ AB:Finset (Finset n) := {x ∈ A | i ∉ x}⊢ 1 / 2 * ↑(#A) ≤ ↑(#({x ∈ A | i ∈ x})) n:Type u_1inst✝:DecidableEq nA:Finset (Finset n)h_union_closed:IsUnionClosed Ai:nhi:{i} ∈ AB:Finset (Finset n) := {x ∈ A | i ∉ x}C:Finset (Finset n) := {x ∈ A | i ∈ x}⊢ 1 / 2 * ↑(#A) ≤ ↑(#C) have h₁ : (B : Set <| Finset n).InjOn (insert i) := n:Type u_1inst✝:DecidableEq nA:Finset (Finset n)h_union_closed:IsUnionClosed Ai:nhi:{i} ∈ A⊢ ∃ i, 1 / 2 * ↑(#A) ≤ ↑(#({x ∈ A | i ∈ x})) n:Type u_1inst✝:DecidableEq nA:Finset (Finset n)h_union_closed:IsUnionClosed Ai:nhi:{i} ∈ AB:Finset (Finset n) := {x ∈ A | i ∉ x}C:Finset (Finset n) := {x ∈ A | i ∈ x}⊢ ∀ ⦃x₁ : Finset n⦄, x₁ ∈ A → i ∉ x₁ → ∀ ⦃x₂ : Finset n⦄, x₂ ∈ A → i ∉ x₂ → insert i x₁ = insert i x₂ → x₁ = x₂ n:Type u_1inst✝:DecidableEq nA:Finset (Finset n)h_union_closed:IsUnionClosed Ai:nhi:{i} ∈ AB:Finset (Finset n) := {x ∈ A | i ∉ x}C:Finset (Finset n) := {x ∈ A | i ∈ x}x:Finset nhx:i ∉ xy:Finset nhy:i ∉ yhxy:insert i x = insert i y⊢ x = y n:Type u_1inst✝:DecidableEq nA:Finset (Finset n)h_union_closed:IsUnionClosed Ai:nhi:{i} ∈ AB:Finset (Finset n) := {x ∈ A | i ∉ x}C:Finset (Finset n) := {x ∈ A | i ∈ x}x:Finset nhx:i ∉ xy:Finset nhy:i ∉ yhxy:insert i x = insert i ythis:(insert i x).erase i = (insert i y).erase i := id (congrArg (fun x => x.erase i) hxy)⊢ x = y rwa [erase_insert hx, erase_insert hyn:Type u_1inst✝:DecidableEq nA:Finset (Finset n)h_union_closed:IsUnionClosed Ai:nhi:{i} ∈ AB:Finset (Finset n) := {x ∈ A | i ∉ x}C:Finset (Finset n) := {x ∈ A | i ∈ x}x:Finset nhx:i ∉ xy:Finset nhy:i ∉ yhxy:insert i x = insert i ythis:x = y⊢ x = y at this have h₂ : (B : Set <| Finset n).MapsTo (insert i) C := n:Type u_1inst✝:DecidableEq nA:Finset (Finset n)h_union_closed:IsUnionClosed Ai:nhi:{i} ∈ A⊢ ∃ i, 1 / 2 * ↑(#A) ≤ ↑(#({x ∈ A | i ∈ x})) n:Type u_1inst✝:DecidableEq nA:Finset (Finset n)h_union_closed:IsUnionClosed Ai:nhi:{i} ∈ AB:Finset (Finset n) := {x ∈ A | i ∉ x}C:Finset (Finset n) := {x ∈ A | i ∈ x}h₁:Set.InjOn (insert i) ↑B := Eq.mpr (id (forall_congr fun ⦃x₁⦄ => Eq.trans (implies_congr (congrArg (fun x => x₁ ∈ x) (coe_filter (fun x => i ∉ x) A)) (forall_congr fun ⦃x₂⦄ => Eq.trans (implies_congr (congrArg (fun x => x₂ ∈ x) (coe_filter (fun x => i ∉ x) A)) (Eq.refl (insert i x₁ = insert i x₂ → x₁ = x₂))) singleton_mem._simp_1)) singleton_mem._simp_1)) fun ⦃x⦄ a hx ⦃y⦄ a_1 hy hxy => have this := id (congrArg (fun x => x.erase i) hxy); Eq.mp (congrArg (fun _a => x = _a) (erase_insert hy)) (Eq.mp (congrArg (fun _a => _a = (insert i y).erase i) (erase_insert hx)) this)⊢ ∀ ⦃x : Finset n⦄, x ∈ A → i ∉ x → insert i x ∈ A intro x n:Type u_1inst✝:DecidableEq nA:Finset (Finset n)h_union_closed:IsUnionClosed Ai:nhi:{i} ∈ AB:Finset (Finset n) := {x ∈ A | i ∉ x}C:Finset (Finset n) := {x ∈ A | i ∈ x}h₁:Set.InjOn (insert i) ↑B := Eq.mpr (id (forall_congr fun ⦃x₁⦄ => Eq.trans (implies_congr (congrArg (fun x => x₁ ∈ x) (coe_filter (fun x => i ∉ x) A)) (forall_congr fun ⦃x₂⦄ => Eq.trans (implies_congr (congrArg (fun x => x₂ ∈ x) (coe_filter (fun x => i ∉ x) A)) (Eq.refl (insert i x₁ = insert i x₂ → x₁ = x₂))) singleton_mem._simp_1)) singleton_mem._simp_1)) fun ⦃x⦄ a hx ⦃y⦄ a_1 hy hxy => have this := id (congrArg (fun x => x.erase i) hxy); Eq.mp (congrArg (fun _a => x = _a) (erase_insert hy)) (Eq.mp (congrArg (fun _a => _a = (insert i y).erase i) (erase_insert hx)) this)x:Finset nhx:x ∈ A⊢ i ∉ x → insert i x ∈ A n:Type u_1inst✝:DecidableEq nA:Finset (Finset n)h_union_closed:IsUnionClosed Ai:nhi:{i} ∈ AB:Finset (Finset n) := {x ∈ A | i ∉ x}C:Finset (Finset n) := {x ∈ A | i ∈ x}h₁:Set.InjOn (insert i) ↑B := Eq.mpr (id (forall_congr fun ⦃x₁⦄ => Eq.trans (implies_congr (congrArg (fun x => x₁ ∈ x) (coe_filter (fun x => i ∉ x) A)) (forall_congr fun ⦃x₂⦄ => Eq.trans (implies_congr (congrArg (fun x => x₂ ∈ x) (coe_filter (fun x => i ∉ x) A)) (Eq.refl (insert i x₁ = insert i x₂ → x₁ = x₂))) singleton_mem._simp_1)) singleton_mem._simp_1)) fun ⦃x⦄ a hx ⦃y⦄ a_1 hy hxy => have this := id (congrArg (fun x => x.erase i) hxy); Eq.mp (congrArg (fun _a => x = _a) (erase_insert hy)) (Eq.mp (congrArg (fun _a => _a = (insert i y).erase i) (erase_insert hx)) this)x:Finset nhx:x ∈ Ahix:i ∉ x⊢ insert i x ∈ A n:Type u_1inst✝:DecidableEq nA:Finset (Finset n)h_union_closed:IsUnionClosed Ai:nhi:{i} ∈ AB:Finset (Finset n) := {x ∈ A | i ∉ x}C:Finset (Finset n) := {x ∈ A | i ∈ x}h₁:Set.InjOn (insert i) ↑B := Eq.mpr (id (forall_congr fun ⦃x₁⦄ => Eq.trans (implies_congr (congrArg (fun x => x₁ ∈ x) (coe_filter (fun x => i ∉ x) A)) (forall_congr fun ⦃x₂⦄ => Eq.trans (implies_congr (congrArg (fun x => x₂ ∈ x) (coe_filter (fun x => i ∉ x) A)) (Eq.refl (insert i x₁ = insert i x₂ → x₁ = x₂))) singleton_mem._simp_1)) singleton_mem._simp_1)) fun ⦃x⦄ a hx ⦃y⦄ a_1 hy hxy => have this := id (congrArg (fun x => x.erase i) hxy); Eq.mp (congrArg (fun _a => x = _a) (erase_insert hy)) (Eq.mp (congrArg (fun _a => _a = (insert i y).erase i) (erase_insert hx)) this)x:Finset nhx:x ∈ Ahix:i ∉ x⊢ {i} ∪ x ∈ A All goals completed! 🐙 n:Type u_1inst✝:DecidableEq nA:Finset (Finset n)h_union_closed:IsUnionClosed Ai:nhi:{i} ∈ AB:Finset (Finset n) := {x ∈ A | i ∉ x}C:Finset (Finset n) := {x ∈ A | i ∈ x}h₁:Set.InjOn (insert i) ↑B := Eq.mpr (id (forall_congr fun ⦃x₁⦄ => Eq.trans (implies_congr (congrArg (fun x => x₁ ∈ x) (coe_filter (fun x => i ∉ x) A)) (forall_congr fun ⦃x₂⦄ => Eq.trans (implies_congr (congrArg (fun x => x₂ ∈ x) (coe_filter (fun x => i ∉ x) A)) (Eq.refl (insert i x₁ = insert i x₂ → x₁ = x₂))) singleton_mem._simp_1)) singleton_mem._simp_1)) fun ⦃x⦄ a hx ⦃y⦄ a_1 hy hxy => have this := id (congrArg (fun x => x.erase i) hxy); Eq.mp (congrArg (fun _a => x = _a) (erase_insert hy)) (Eq.mp (congrArg (fun _a => _a = (insert i y).erase i) (erase_insert hx)) this)h₂:Set.MapsTo (insert i) ↑B ↑C := Eq.mpr (id (forall_congr fun ⦃x⦄ => Eq.trans (implies_congr (congrArg (fun x_1 => x ∈ x_1) (coe_filter (fun x => i ∉ x) A)) (Eq.trans (congrArg (fun x_1 => insert i x ∈ x_1) (coe_filter (fun x => i ∈ x) A)) (Eq.trans (congrArg (And (insert i x ∈ A)) (Eq.trans singleton_mem._simp_2 (Eq.trans (congrArg (fun x_1 => x_1 ∨ i ∈ x) (eq_self i)) (true_or (i ∈ x))))) (and_true (insert i x ∈ A))))) singleton_mem._simp_1)) fun ⦃x⦄ hx hix => Eq.mpr (id (congrArg (fun _a => _a ∈ A) (insert_eq i x))) (h_union_closed {i} hi x hx)h₃:#B ≤ #C := card_le_card_of_injOn (insert i) h₂ h₁⊢ 1 / 2 * ↑(#A) ≤ ↑(#C) have h₄ : #C + #B = #A := n:Type u_1inst✝:DecidableEq nA:Finset (Finset n)h_union_closed:IsUnionClosed Ai:nhi:{i} ∈ A⊢ ∃ i, 1 / 2 * ↑(#A) ≤ ↑(#({x ∈ A | i ∈ x})) All goals completed! 🐙 have : #A ≤ 2 * #C := n:Type u_1inst✝:DecidableEq nA:Finset (Finset n)h_union_closed:IsUnionClosed Ai:nhi:{i} ∈ A⊢ ∃ i, 1 / 2 * ↑(#A) ≤ ↑(#({x ∈ A | i ∈ x})) All goals completed! 🐙 n:Type u_1inst✝:DecidableEq nA:Finset (Finset n)h_union_closed:IsUnionClosed Ai:nhi:{i} ∈ AB:Finset (Finset n) := {x ∈ A | i ∉ x}C:Finset (Finset n) := {x ∈ A | i ∈ x}h₁:Set.InjOn (insert i) ↑B := Eq.mpr (id (forall_congr fun ⦃x₁⦄ => Eq.trans (implies_congr (congrArg (fun x => x₁ ∈ x) (coe_filter (fun x => i ∉ x) A)) (forall_congr fun ⦃x₂⦄ => Eq.trans (implies_congr (congrArg (fun x => x₂ ∈ x) (coe_filter (fun x => i ∉ x) A)) (Eq.refl (insert i x₁ = insert i x₂ → x₁ = x₂))) singleton_mem._simp_1)) singleton_mem._simp_1)) fun ⦃x⦄ a hx ⦃y⦄ a_1 hy hxy => have this := id (congrArg (fun x => x.erase i) hxy); Eq.mp (congrArg (fun _a => x = _a) (erase_insert hy)) (Eq.mp (congrArg (fun _a => _a = (insert i y).erase i) (erase_insert hx)) this)h₂:Set.MapsTo (insert i) ↑B ↑C := Eq.mpr (id (forall_congr fun ⦃x⦄ => Eq.trans (implies_congr (congrArg (fun x_1 => x ∈ x_1) (coe_filter (fun x => i ∉ x) A)) (Eq.trans (congrArg (fun x_1 => insert i x ∈ x_1) (coe_filter (fun x => i ∈ x) A)) (Eq.trans (congrArg (And (insert i x ∈ A)) (Eq.trans singleton_mem._simp_2 (Eq.trans (congrArg (fun x_1 => x_1 ∨ i ∈ x) (eq_self i)) (true_or (i ∈ x))))) (and_true (insert i x ∈ A))))) singleton_mem._simp_1)) fun ⦃x⦄ hx hix => Eq.mpr (id (congrArg (fun _a => _a ∈ A) (insert_eq i x))) (h_union_closed {i} hi x hx)h₃:#B ≤ #C := card_le_card_of_injOn (insert i) h₂ h₁h₄:#C + #B = #A := Eq.mpr (id (congrArg (fun _a => _a = #A) (card_filter_add_card_filter_not fun x => i ∈ x))) (Eq.refl #A)this:#A ≤ 2 * #C := Decidable.byContradiction fun a => singleton_mem._proof_2 i h₃ h₄ a⊢ ↑(#A) ≤ 2 * ↑(#C) All goals completed! 🐙

The union-closed sets conjecture is sharp in the sense that if we replace the constant 1/2 with any larger constant, then the conjecture fails.

@[category research solved, AMS 5] theorem union_closed.variants.sharpness [Fintype n] (c : ℝ) (hc : 1 / 2 < c) : ¬ (∀ A : Finset (Finset n), A ≠ {∅} → IsUnionClosed A → ∃ i : n, c * #A ≤ #{x ∈ A | i ∈ x}) := n:Type u_1inst✝¹:DecidableEq ninst✝:Fintype nc:ℝhc:1 / 2 < c⊢ ¬∀ (A : Finset (Finset n)), A ≠ {∅} → IsUnionClosed A → ∃ i, c * ↑(#A) ≤ ↑(#({x ∈ A | i ∈ x})) n:Type u_1inst✝¹:DecidableEq ninst✝:Fintype nc:ℝhc:1 / 2 < ch:∀ (A : Finset (Finset n)), A ≠ {∅} → IsUnionClosed A → ∃ i, c * ↑(#A) ≤ ↑(#({x ∈ A | i ∈ x}))⊢ False -- We can safely assume `n` is nonempty. n:Type u_1inst✝¹:DecidableEq ninst✝:Fintype nc:ℝhc:1 / 2 < ch:∀ (A : Finset (Finset n)), A ≠ {∅} → IsUnionClosed A → ∃ i, c * ↑(#A) ≤ ↑(#({x ∈ A | i ∈ x}))hn:IsEmpty n⊢ Falsen:Type u_1inst✝¹:DecidableEq ninst✝:Fintype nc:ℝhc:1 / 2 < ch:∀ (A : Finset (Finset n)), A ≠ {∅} → IsUnionClosed A → ∃ i, c * ↑(#A) ≤ ↑(#({x ∈ A | i ∈ x}))hn:Nonempty n⊢ False n:Type u_1inst✝¹:DecidableEq ninst✝:Fintype nc:ℝhc:1 / 2 < ch:∀ (A : Finset (Finset n)), A ≠ {∅} → IsUnionClosed A → ∃ i, c * ↑(#A) ≤ ↑(#({x ∈ A | i ∈ x}))hn:IsEmpty n⊢ False n:Type u_1inst✝¹:DecidableEq ninst✝:Fintype nc:ℝhc:1 / 2 < chn:IsEmpty nh:∅ ≠ {∅} → IsUnionClosed ∅ → ∃ i, c * ↑(#∅) ≤ ↑(#({x ∈ ∅ | i ∈ x}))⊢ False n:Type u_1inst✝¹:DecidableEq ninst✝:Fintype nc:ℝhc:1 / 2 < chn:IsEmpty nh:∅ = {∅}⊢ False have : ∅ ∈ (∅ : Finset (Finset n)) := n:Type u_1inst✝¹:DecidableEq ninst✝:Fintype nc:ℝhc:1 / 2 < c⊢ ¬∀ (A : Finset (Finset n)), A ≠ {∅} → IsUnionClosed A → ∃ i, c * ↑(#A) ≤ ↑(#({x ∈ A | i ∈ x})) All goals completed! 🐙 All goals completed! 🐙 -- Use A as the set of all subsets of `n`, which is not singleton empty and is union-closed. n:Type u_1inst✝¹:DecidableEq ninst✝:Fintype nc:ℝhc:1 / 2 < ch:∀ (A : Finset (Finset n)), A ≠ {∅} → IsUnionClosed A → ∃ i, c * ↑(#A) ≤ ↑(#({x ∈ A | i ∈ x}))hn:Nonempty nA:Finset (Finset n) := univ⊢ False have h_ne_singleton_empty : A ≠ {∅} := n:Type u_1inst✝¹:DecidableEq ninst✝:Fintype nc:ℝhc:1 / 2 < c⊢ ¬∀ (A : Finset (Finset n)), A ≠ {∅} → IsUnionClosed A → ∃ i, c * ↑(#A) ≤ ↑(#({x ∈ A | i ∈ x})) have : #A = 2 ^ Fintype.card n := n:Type u_1inst✝¹:DecidableEq ninst✝:Fintype nc:ℝhc:1 / 2 < c⊢ ¬∀ (A : Finset (Finset n)), A ≠ {∅} → IsUnionClosed A → ∃ i, c * ↑(#A) ≤ ↑(#({x ∈ A | i ∈ x})) All goals completed! 🐙 have : 1 < #A := n:Type u_1inst✝¹:DecidableEq ninst✝:Fintype nc:ℝhc:1 / 2 < c⊢ ¬∀ (A : Finset (Finset n)), A ≠ {∅} → IsUnionClosed A → ∃ i, c * ↑(#A) ≤ ↑(#({x ∈ A | i ∈ x})) All goals completed! 🐙 n:Type u_1inst✝¹:DecidableEq ninst✝:Fintype nc:ℝhc:1 / 2 < ch✝:∀ (A : Finset (Finset n)), A ≠ {∅} → IsUnionClosed A → ∃ i, c * ↑(#A) ≤ ↑(#({x ∈ A | i ∈ x}))hn:Nonempty nA:Finset (Finset n) := univthis✝:#A = 2 ^ Fintype.card n := of_eq_true (Eq.trans (congrArg (fun x => x = 2 ^ Fintype.card n) Fintype.card_finset) (eq_self (2 ^ Fintype.card n)))this:1 < #A := of_eq_true (Eq.trans (Eq.trans (congrArg (LT.lt 1) this✝) (Nat.one_lt_pow_iff._simp_1 (of_eq_true (Eq.trans (congrArg Not Fintype.card_ne_zero._simp_1) not_false_eq_true)))) Nat.one_lt_ofNat._simp_1)h:A = {∅}⊢ False All goals completed! 🐙 n:Type u_1inst✝¹:DecidableEq ninst✝:Fintype nc:ℝhc:1 / 2 < ch:∀ (A : Finset (Finset n)), A ≠ {∅} → IsUnionClosed A → ∃ i, c * ↑(#A) ≤ ↑(#({x ∈ A | i ∈ x}))hn:Nonempty nA:Finset (Finset n) := univh_ne_singleton_empty:A ≠ {∅} := have this := of_eq_true (Eq.trans (congrArg (fun x => x = 2 ^ Fintype.card n) Fintype.card_finset) (eq_self (2 ^ Fintype.card n))); have this := of_eq_true (Eq.trans (Eq.trans (congrArg (LT.lt 1) this) (Nat.one_lt_pow_iff._simp_1 (of_eq_true (Eq.trans (congrArg Not Fintype.card_ne_zero._simp_1) not_false_eq_true)))) Nat.one_lt_ofNat._simp_1); fun h => False.elim (Eq.mp (Eq.trans (congrArg (LT.lt 1) (Eq.trans (congrArg card h) (card_singleton ∅))) (lt_self_iff_false._simp_1 1)) this)i:nhi:c * ↑(#univ) ≤ ↑(#{x | i ∈ x})⊢ False have hn : 1 ≤ Fintype.card n := n:Type u_1inst✝¹:DecidableEq ninst✝:Fintype nc:ℝhc:1 / 2 < c⊢ ¬∀ (A : Finset (Finset n)), A ≠ {∅} → IsUnionClosed A → ∃ i, c * ↑(#A) ≤ ↑(#({x ∈ A | i ∈ x})) n:Type u_1inst✝¹:DecidableEq ninst✝:Fintype nc:ℝhc:1 / 2 < ch:∀ (A : Finset (Finset n)), A ≠ {∅} → IsUnionClosed A → ∃ i, c * ↑(#A) ≤ ↑(#({x ∈ A | i ∈ x}))hn:Nonempty nA:Finset (Finset n) := univh_ne_singleton_empty:A ≠ {∅} := have this := of_eq_true (Eq.trans (congrArg (fun x => x = 2 ^ Fintype.card n) Fintype.card_finset) (eq_self (2 ^ Fintype.card n))); have this := of_eq_true (Eq.trans (Eq.trans (congrArg (LT.lt 1) this) (Nat.one_lt_pow_iff._simp_1 (of_eq_true (Eq.trans (congrArg Not Fintype.card_ne_zero._simp_1) not_false_eq_true)))) Nat.one_lt_ofNat._simp_1); fun h => False.elim (Eq.mp (Eq.trans (congrArg (LT.lt 1) (Eq.trans (congrArg card h) (card_singleton ∅))) (lt_self_iff_false._simp_1 1)) this)i:nhi:c * ↑(#univ) ≤ ↑(#{x | i ∈ x})⊢ 0 < Fintype.card n All goals completed! 🐙 -- Now the number of sets containing `i` is `2 ^ (Fintype.card n - 1)` have : #{x : Finset n | i ∈ x} = 2 ^ (Fintype.card n - 1) := n:Type u_1inst✝¹:DecidableEq ninst✝:Fintype nc:ℝhc:1 / 2 < c⊢ ¬∀ (A : Finset (Finset n)), A ≠ {∅} → IsUnionClosed A → ∃ i, c * ↑(#A) ≤ ↑(#({x ∈ A | i ∈ x})) have : ({x : Finset n | i ∈ x} : Finset _) = (univ.erase i).powerset.image (insert i) := n:Type u_1inst✝¹:DecidableEq ninst✝:Fintype nc:ℝhc:1 / 2 < c⊢ ¬∀ (A : Finset (Finset n)), A ≠ {∅} → IsUnionClosed A → ∃ i, c * ↑(#A) ≤ ↑(#({x ∈ A | i ∈ x})) n:Type u_1inst✝¹:DecidableEq ninst✝:Fintype nc:ℝhc:1 / 2 < ch:∀ (A : Finset (Finset n)), A ≠ {∅} → IsUnionClosed A → ∃ i, c * ↑(#A) ≤ ↑(#({x ∈ A | i ∈ x}))hn✝:Nonempty nA:Finset (Finset n) := univh_ne_singleton_empty:A ≠ {∅} := have this := of_eq_true (Eq.trans (congrArg (fun x => x = 2 ^ Fintype.card n) Fintype.card_finset) (eq_self (2 ^ Fintype.card n))); have this := of_eq_true (Eq.trans (Eq.trans (congrArg (LT.lt 1) this) (Nat.one_lt_pow_iff._simp_1 (of_eq_true (Eq.trans (congrArg Not Fintype.card_ne_zero._simp_1) not_false_eq_true)))) Nat.one_lt_ofNat._simp_1); fun h => False.elim (Eq.mp (Eq.trans (congrArg (LT.lt 1) (Eq.trans (congrArg card h) (card_singleton ∅))) (lt_self_iff_false._simp_1 1)) this)i:nhi:c * ↑(#univ) ≤ ↑(#{x | i ∈ x})hn:1 ≤ Fintype.card n := Eq.mpr (id (congrArg (fun _a => _a) (propext Nat.add_one_le_iff))) Fintype.card_posx:Finset n⊢ x ∈ {x | i ∈ x} ↔ x ∈ image (insert i) (univ.erase i).powerset n:Type u_1inst✝¹:DecidableEq ninst✝:Fintype nc:ℝhc:1 / 2 < ch:∀ (A : Finset (Finset n)), A ≠ {∅} → IsUnionClosed A → ∃ i, c * ↑(#A) ≤ ↑(#({x ∈ A | i ∈ x}))hn✝:Nonempty nA:Finset (Finset n) := univh_ne_singleton_empty:A ≠ {∅} := have this := of_eq_true (Eq.trans (congrArg (fun x => x = 2 ^ Fintype.card n) Fintype.card_finset) (eq_self (2 ^ Fintype.card n))); have this := of_eq_true (Eq.trans (Eq.trans (congrArg (LT.lt 1) this) (Nat.one_lt_pow_iff._simp_1 (of_eq_true (Eq.trans (congrArg Not Fintype.card_ne_zero._simp_1) not_false_eq_true)))) Nat.one_lt_ofNat._simp_1); fun h => False.elim (Eq.mp (Eq.trans (congrArg (LT.lt 1) (Eq.trans (congrArg card h) (card_singleton ∅))) (lt_self_iff_false._simp_1 1)) this)i:nhi:c * ↑(#univ) ≤ ↑(#{x | i ∈ x})hn:1 ≤ Fintype.card n := Eq.mpr (id (congrArg (fun _a => _a) (propext Nat.add_one_le_iff))) Fintype.card_posx:Finset n⊢ i ∈ x ↔ ∃ a, i ∉ a ∧ insert i a = x n:Type u_1inst✝¹:DecidableEq ninst✝:Fintype nc:ℝhc:1 / 2 < ch:∀ (A : Finset (Finset n)), A ≠ {∅} → IsUnionClosed A → ∃ i, c * ↑(#A) ≤ ↑(#({x ∈ A | i ∈ x}))hn✝:Nonempty nA:Finset (Finset n) := univh_ne_singleton_empty:A ≠ {∅} := have this := of_eq_true (Eq.trans (congrArg (fun x => x = 2 ^ Fintype.card n) Fintype.card_finset) (eq_self (2 ^ Fintype.card n))); have this := of_eq_true (Eq.trans (Eq.trans (congrArg (LT.lt 1) this) (Nat.one_lt_pow_iff._simp_1 (of_eq_true (Eq.trans (congrArg Not Fintype.card_ne_zero._simp_1) not_false_eq_true)))) Nat.one_lt_ofNat._simp_1); fun h => False.elim (Eq.mp (Eq.trans (congrArg (LT.lt 1) (Eq.trans (congrArg card h) (card_singleton ∅))) (lt_self_iff_false._simp_1 1)) this)i:nhi:c * ↑(#univ) ≤ ↑(#{x | i ∈ x})hn:1 ≤ Fintype.card n := Eq.mpr (id (congrArg (fun _a => _a) (propext Nat.add_one_le_iff))) Fintype.card_posx:Finset n⊢ i ∈ x → ∃ a, i ∉ a ∧ insert i a = xn:Type u_1inst✝¹:DecidableEq ninst✝:Fintype nc:ℝhc:1 / 2 < ch:∀ (A : Finset (Finset n)), A ≠ {∅} → IsUnionClosed A → ∃ i, c * ↑(#A) ≤ ↑(#({x ∈ A | i ∈ x}))hn✝:Nonempty nA:Finset (Finset n) := univh_ne_singleton_empty:A ≠ {∅} := have this := of_eq_true (Eq.trans (congrArg (fun x => x = 2 ^ Fintype.card n) Fintype.card_finset) (eq_self (2 ^ Fintype.card n))); have this := of_eq_true (Eq.trans (Eq.trans (congrArg (LT.lt 1) this) (Nat.one_lt_pow_iff._simp_1 (of_eq_true (Eq.trans (congrArg Not Fintype.card_ne_zero._simp_1) not_false_eq_true)))) Nat.one_lt_ofNat._simp_1); fun h => False.elim (Eq.mp (Eq.trans (congrArg (LT.lt 1) (Eq.trans (congrArg card h) (card_singleton ∅))) (lt_self_iff_false._simp_1 1)) this)i:nhi:c * ↑(#univ) ≤ ↑(#{x | i ∈ x})hn:1 ≤ Fintype.card n := Eq.mpr (id (congrArg (fun _a => _a) (propext Nat.add_one_le_iff))) Fintype.card_posx:Finset n⊢ (∃ a, i ∉ a ∧ insert i a = x) → i ∈ x n:Type u_1inst✝¹:DecidableEq ninst✝:Fintype nc:ℝhc:1 / 2 < ch:∀ (A : Finset (Finset n)), A ≠ {∅} → IsUnionClosed A → ∃ i, c * ↑(#A) ≤ ↑(#({x ∈ A | i ∈ x}))hn✝:Nonempty nA:Finset (Finset n) := univh_ne_singleton_empty:A ≠ {∅} := have this := of_eq_true (Eq.trans (congrArg (fun x => x = 2 ^ Fintype.card n) Fintype.card_finset) (eq_self (2 ^ Fintype.card n))); have this := of_eq_true (Eq.trans (Eq.trans (congrArg (LT.lt 1) this) (Nat.one_lt_pow_iff._simp_1 (of_eq_true (Eq.trans (congrArg Not Fintype.card_ne_zero._simp_1) not_false_eq_true)))) Nat.one_lt_ofNat._simp_1); fun h => False.elim (Eq.mp (Eq.trans (congrArg (LT.lt 1) (Eq.trans (congrArg card h) (card_singleton ∅))) (lt_self_iff_false._simp_1 1)) this)i:nhi:c * ↑(#univ) ≤ ↑(#{x | i ∈ x})hn:1 ≤ Fintype.card n := Eq.mpr (id (congrArg (fun _a => _a) (propext Nat.add_one_le_iff))) Fintype.card_posx:Finset n⊢ i ∈ x → ∃ a, i ∉ a ∧ insert i a = x n:Type u_1inst✝¹:DecidableEq ninst✝:Fintype nc:ℝhc:1 / 2 < ch✝:∀ (A : Finset (Finset n)), A ≠ {∅} → IsUnionClosed A → ∃ i, c * ↑(#A) ≤ ↑(#({x ∈ A | i ∈ x}))hn✝:Nonempty nA:Finset (Finset n) := univh_ne_singleton_empty:A ≠ {∅} := have this := of_eq_true (Eq.trans (congrArg (fun x => x = 2 ^ Fintype.card n) Fintype.card_finset) (eq_self (2 ^ Fintype.card n))); have this := of_eq_true (Eq.trans (Eq.trans (congrArg (LT.lt 1) this) (Nat.one_lt_pow_iff._simp_1 (of_eq_true (Eq.trans (congrArg Not Fintype.card_ne_zero._simp_1) not_false_eq_true)))) Nat.one_lt_ofNat._simp_1); fun h => False.elim (Eq.mp (Eq.trans (congrArg (LT.lt 1) (Eq.trans (congrArg card h) (card_singleton ∅))) (lt_self_iff_false._simp_1 1)) this)i:nhi:c * ↑(#univ) ≤ ↑(#{x | i ∈ x})hn:1 ≤ Fintype.card n := Eq.mpr (id (congrArg (fun _a => _a) (propext Nat.add_one_le_iff))) Fintype.card_posx:Finset nh:i ∈ x⊢ ∃ a, i ∉ a ∧ insert i a = x n:Type u_1inst✝¹:DecidableEq ninst✝:Fintype nc:ℝhc:1 / 2 < ch✝:∀ (A : Finset (Finset n)), A ≠ {∅} → IsUnionClosed A → ∃ i, c * ↑(#A) ≤ ↑(#({x ∈ A | i ∈ x}))hn✝:Nonempty nA:Finset (Finset n) := univh_ne_singleton_empty:A ≠ {∅} := have this := of_eq_true (Eq.trans (congrArg (fun x => x = 2 ^ Fintype.card n) Fintype.card_finset) (eq_self (2 ^ Fintype.card n))); have this := of_eq_true (Eq.trans (Eq.trans (congrArg (LT.lt 1) this) (Nat.one_lt_pow_iff._simp_1 (of_eq_true (Eq.trans (congrArg Not Fintype.card_ne_zero._simp_1) not_false_eq_true)))) Nat.one_lt_ofNat._simp_1); fun h => False.elim (Eq.mp (Eq.trans (congrArg (LT.lt 1) (Eq.trans (congrArg card h) (card_singleton ∅))) (lt_self_iff_false._simp_1 1)) this)i:nhi:c * ↑(#univ) ≤ ↑(#{x | i ∈ x})hn:1 ≤ Fintype.card n := Eq.mpr (id (congrArg (fun _a => _a) (propext Nat.add_one_le_iff))) Fintype.card_posx:Finset nh:i ∈ x⊢ i ∉ x.erase i ∧ insert i (x.erase i) = x All goals completed! 🐙 n:Type u_1inst✝¹:DecidableEq ninst✝:Fintype nc:ℝhc:1 / 2 < ch:∀ (A : Finset (Finset n)), A ≠ {∅} → IsUnionClosed A → ∃ i, c * ↑(#A) ≤ ↑(#({x ∈ A | i ∈ x}))hn✝:Nonempty nA:Finset (Finset n) := univh_ne_singleton_empty:A ≠ {∅} := have this := of_eq_true (Eq.trans (congrArg (fun x => x = 2 ^ Fintype.card n) Fintype.card_finset) (eq_self (2 ^ Fintype.card n))); have this := of_eq_true (Eq.trans (Eq.trans (congrArg (LT.lt 1) this) (Nat.one_lt_pow_iff._simp_1 (of_eq_true (Eq.trans (congrArg Not Fintype.card_ne_zero._simp_1) not_false_eq_true)))) Nat.one_lt_ofNat._simp_1); fun h => False.elim (Eq.mp (Eq.trans (congrArg (LT.lt 1) (Eq.trans (congrArg card h) (card_singleton ∅))) (lt_self_iff_false._simp_1 1)) this)i:nhi:c * ↑(#univ) ≤ ↑(#{x | i ∈ x})hn:1 ≤ Fintype.card n := Eq.mpr (id (congrArg (fun _a => _a) (propext Nat.add_one_le_iff))) Fintype.card_posx:Finset n⊢ (∃ a, i ∉ a ∧ insert i a = x) → i ∈ x n:Type u_1inst✝¹:DecidableEq ninst✝:Fintype nc:ℝhc:1 / 2 < ch:∀ (A : Finset (Finset n)), A ≠ {∅} → IsUnionClosed A → ∃ i, c * ↑(#A) ≤ ↑(#({x ∈ A | i ∈ x}))hn✝:Nonempty nA:Finset (Finset n) := univh_ne_singleton_empty:A ≠ {∅} := have this := of_eq_true (Eq.trans (congrArg (fun x => x = 2 ^ Fintype.card n) Fintype.card_finset) (eq_self (2 ^ Fintype.card n))); have this := of_eq_true (Eq.trans (Eq.trans (congrArg (LT.lt 1) this) (Nat.one_lt_pow_iff._simp_1 (of_eq_true (Eq.trans (congrArg Not Fintype.card_ne_zero._simp_1) not_false_eq_true)))) Nat.one_lt_ofNat._simp_1); fun h => False.elim (Eq.mp (Eq.trans (congrArg (LT.lt 1) (Eq.trans (congrArg card h) (card_singleton ∅))) (lt_self_iff_false._simp_1 1)) this)i:nhi:c * ↑(#univ) ≤ ↑(#{x | i ∈ x})hn:1 ≤ Fintype.card n := Eq.mpr (id (congrArg (fun _a => _a) (propext Nat.add_one_le_iff))) Fintype.card_posw✝:Finset nleft✝:i ∉ w✝⊢ i ∈ insert i w✝ All goals completed! 🐙 n:Type u_1inst✝¹:DecidableEq ninst✝:Fintype nc:ℝhc:1 / 2 < ch:∀ (A : Finset (Finset n)), A ≠ {∅} → IsUnionClosed A → ∃ i, c * ↑(#A) ≤ ↑(#({x ∈ A | i ∈ x}))hn✝:Nonempty nA:Finset (Finset n) := univh_ne_singleton_empty:A ≠ {∅} := have this := of_eq_true (Eq.trans (congrArg (fun x => x = 2 ^ Fintype.card n) Fintype.card_finset) (eq_self (2 ^ Fintype.card n))); have this := of_eq_true (Eq.trans (Eq.trans (congrArg (LT.lt 1) this) (Nat.one_lt_pow_iff._simp_1 (of_eq_true (Eq.trans (congrArg Not Fintype.card_ne_zero._simp_1) not_false_eq_true)))) Nat.one_lt_ofNat._simp_1); fun h => False.elim (Eq.mp (Eq.trans (congrArg (LT.lt 1) (Eq.trans (congrArg card h) (card_singleton ∅))) (lt_self_iff_false._simp_1 1)) this)i:nhi:c * ↑(#univ) ≤ ↑(#{x | i ∈ x})hn:1 ≤ Fintype.card n := Eq.mpr (id (congrArg (fun _a => _a) (propext Nat.add_one_le_iff))) Fintype.card_posthis:{x | i ∈ x} = image (insert i) (univ.erase i).powerset := ext fun x => Eq.mpr (id (congr (congrArg Iff (Eq.trans sharpness._simp_8 (Eq.trans (congrArg (fun x_1 => x_1 ∧ i ∈ x) (sharpness._simp_9 x)) (true_and (i ∈ x))))) (Eq.trans sharpness._simp_10 (congrArg Exists (funext fun a => congrArg (fun x_1 => x_1 ∧ insert i a = x) (Eq.trans sharpness._simp_11 (Eq.trans sharpness._simp_12 (Eq.trans (congrArg (fun x => x ∧ i ∉ a) (sharpness._simp_13 a)) (true_and (i ∉ a)))))))))) { mp := fun h => Exists.intro (x.erase i) (of_eq_true (Eq.trans (congr (congrArg And (Eq.trans (congrArg Not (Eq.trans mem_erase._simp_1 (Eq.trans (congr (congrArg And (Eq.trans (congrArg Not (eq_self i)) not_true_eq_false)) (eq_true h)) (and_true False)))) not_false_eq_true)) (Eq.trans (congrArg (fun x_1 => x_1 = x) (insert_erase h)) (eq_self x))) (and_self True))), mpr := fun a => Exists.casesOn a fun w h => And.casesOn h fun left right => right ▸ of_eq_true (Eq.trans mem_insert._simp_1 (Eq.trans (congrArg (fun x => x ∨ i ∈ w) (eq_self i)) (true_or (i ∈ w)))) }⊢ 2 ^ #(univ.erase i) = 2 ^ (Fintype.card n - 1)n:Type u_1inst✝¹:DecidableEq ninst✝:Fintype nc:ℝhc:1 / 2 < ch:∀ (A : Finset (Finset n)), A ≠ {∅} → IsUnionClosed A → ∃ i, c * ↑(#A) ≤ ↑(#({x ∈ A | i ∈ x}))hn✝:Nonempty nA:Finset (Finset n) := univh_ne_singleton_empty:A ≠ {∅} := have this := of_eq_true (Eq.trans (congrArg (fun x => x = 2 ^ Fintype.card n) Fintype.card_finset) (eq_self (2 ^ Fintype.card n))); have this := of_eq_true (Eq.trans (Eq.trans (congrArg (LT.lt 1) this) (Nat.one_lt_pow_iff._simp_1 (of_eq_true (Eq.trans (congrArg Not Fintype.card_ne_zero._simp_1) not_false_eq_true)))) Nat.one_lt_ofNat._simp_1); fun h => False.elim (Eq.mp (Eq.trans (congrArg (LT.lt 1) (Eq.trans (congrArg card h) (card_singleton ∅))) (lt_self_iff_false._simp_1 1)) this)i:nhi:c * ↑(#univ) ≤ ↑(#{x | i ∈ x})hn:1 ≤ Fintype.card n := Eq.mpr (id (congrArg (fun _a => _a) (propext Nat.add_one_le_iff))) Fintype.card_posthis:{x | i ∈ x} = image (insert i) (univ.erase i).powerset := ext fun x => Eq.mpr (id (congr (congrArg Iff (Eq.trans sharpness._simp_8 (Eq.trans (congrArg (fun x_1 => x_1 ∧ i ∈ x) (sharpness._simp_9 x)) (true_and (i ∈ x))))) (Eq.trans sharpness._simp_10 (congrArg Exists (funext fun a => congrArg (fun x_1 => x_1 ∧ insert i a = x) (Eq.trans sharpness._simp_11 (Eq.trans sharpness._simp_12 (Eq.trans (congrArg (fun x => x ∧ i ∉ a) (sharpness._simp_13 a)) (true_and (i ∉ a)))))))))) { mp := fun h => Exists.intro (x.erase i) (of_eq_true (Eq.trans (congr (congrArg And (Eq.trans (congrArg Not (Eq.trans mem_erase._simp_1 (Eq.trans (congr (congrArg And (Eq.trans (congrArg Not (eq_self i)) not_true_eq_false)) (eq_true h)) (and_true False)))) not_false_eq_true)) (Eq.trans (congrArg (fun x_1 => x_1 = x) (insert_erase h)) (eq_self x))) (and_self True))), mpr := fun a => Exists.casesOn a fun w h => And.casesOn h fun left right => right ▸ of_eq_true (Eq.trans mem_insert._simp_1 (Eq.trans (congrArg (fun x => x ∨ i ∈ w) (eq_self i)) (true_or (i ∈ w)))) }⊢ Set.InjOn (insert i) ↑(univ.erase i).powerset n:Type u_1inst✝¹:DecidableEq ninst✝:Fintype nc:ℝhc:1 / 2 < ch:∀ (A : Finset (Finset n)), A ≠ {∅} → IsUnionClosed A → ∃ i, c * ↑(#A) ≤ ↑(#({x ∈ A | i ∈ x}))hn✝:Nonempty nA:Finset (Finset n) := univh_ne_singleton_empty:A ≠ {∅} := have this := of_eq_true (Eq.trans (congrArg (fun x => x = 2 ^ Fintype.card n) Fintype.card_finset) (eq_self (2 ^ Fintype.card n))); have this := of_eq_true (Eq.trans (Eq.trans (congrArg (LT.lt 1) this) (Nat.one_lt_pow_iff._simp_1 (of_eq_true (Eq.trans (congrArg Not Fintype.card_ne_zero._simp_1) not_false_eq_true)))) Nat.one_lt_ofNat._simp_1); fun h => False.elim (Eq.mp (Eq.trans (congrArg (LT.lt 1) (Eq.trans (congrArg card h) (card_singleton ∅))) (lt_self_iff_false._simp_1 1)) this)i:nhi:c * ↑(#univ) ≤ ↑(#{x | i ∈ x})hn:1 ≤ Fintype.card n := Eq.mpr (id (congrArg (fun _a => _a) (propext Nat.add_one_le_iff))) Fintype.card_posthis:{x | i ∈ x} = image (insert i) (univ.erase i).powerset := ext fun x => Eq.mpr (id (congr (congrArg Iff (Eq.trans sharpness._simp_8 (Eq.trans (congrArg (fun x_1 => x_1 ∧ i ∈ x) (sharpness._simp_9 x)) (true_and (i ∈ x))))) (Eq.trans sharpness._simp_10 (congrArg Exists (funext fun a => congrArg (fun x_1 => x_1 ∧ insert i a = x) (Eq.trans sharpness._simp_11 (Eq.trans sharpness._simp_12 (Eq.trans (congrArg (fun x => x ∧ i ∉ a) (sharpness._simp_13 a)) (true_and (i ∉ a)))))))))) { mp := fun h => Exists.intro (x.erase i) (of_eq_true (Eq.trans (congr (congrArg And (Eq.trans (congrArg Not (Eq.trans mem_erase._simp_1 (Eq.trans (congr (congrArg And (Eq.trans (congrArg Not (eq_self i)) not_true_eq_false)) (eq_true h)) (and_true False)))) not_false_eq_true)) (Eq.trans (congrArg (fun x_1 => x_1 = x) (insert_erase h)) (eq_self x))) (and_self True))), mpr := fun a => Exists.casesOn a fun w h => And.casesOn h fun left right => right ▸ of_eq_true (Eq.trans mem_insert._simp_1 (Eq.trans (congrArg (fun x => x ∨ i ∈ w) (eq_self i)) (true_or (i ∈ w)))) }⊢ 2 ^ #(univ.erase i) = 2 ^ (Fintype.card n - 1) All goals completed! 🐙 intro a n:Type u_1inst✝¹:DecidableEq ninst✝:Fintype nc:ℝhc:1 / 2 < ch:∀ (A : Finset (Finset n)), A ≠ {∅} → IsUnionClosed A → ∃ i, c * ↑(#A) ≤ ↑(#({x ∈ A | i ∈ x}))hn✝:Nonempty nA:Finset (Finset n) := univh_ne_singleton_empty:A ≠ {∅} := have this := of_eq_true (Eq.trans (congrArg (fun x => x = 2 ^ Fintype.card n) Fintype.card_finset) (eq_self (2 ^ Fintype.card n))); have this := of_eq_true (Eq.trans (Eq.trans (congrArg (LT.lt 1) this) (Nat.one_lt_pow_iff._simp_1 (of_eq_true (Eq.trans (congrArg Not Fintype.card_ne_zero._simp_1) not_false_eq_true)))) Nat.one_lt_ofNat._simp_1); fun h => False.elim (Eq.mp (Eq.trans (congrArg (LT.lt 1) (Eq.trans (congrArg card h) (card_singleton ∅))) (lt_self_iff_false._simp_1 1)) this)i:nhi:c * ↑(#univ) ≤ ↑(#{x | i ∈ x})hn:1 ≤ Fintype.card n := Eq.mpr (id (congrArg (fun _a => _a) (propext Nat.add_one_le_iff))) Fintype.card_posthis:{x | i ∈ x} = image (insert i) (univ.erase i).powerset := ext fun x => Eq.mpr (id (congr (congrArg Iff (Eq.trans sharpness._simp_8 (Eq.trans (congrArg (fun x_1 => x_1 ∧ i ∈ x) (sharpness._simp_9 x)) (true_and (i ∈ x))))) (Eq.trans sharpness._simp_10 (congrArg Exists (funext fun a => congrArg (fun x_1 => x_1 ∧ insert i a = x) (Eq.trans sharpness._simp_11 (Eq.trans sharpness._simp_12 (Eq.trans (congrArg (fun x => x ∧ i ∉ a) (sharpness._simp_13 a)) (true_and (i ∉ a)))))))))) { mp := fun h => Exists.intro (x.erase i) (of_eq_true (Eq.trans (congr (congrArg And (Eq.trans (congrArg Not (Eq.trans mem_erase._simp_1 (Eq.trans (congr (congrArg And (Eq.trans (congrArg Not (eq_self i)) not_true_eq_false)) (eq_true h)) (and_true False)))) not_false_eq_true)) (Eq.trans (congrArg (fun x_1 => x_1 = x) (insert_erase h)) (eq_self x))) (and_self True))), mpr := fun a => Exists.casesOn a fun w h => And.casesOn h fun left right => right ▸ of_eq_true (Eq.trans mem_insert._simp_1 (Eq.trans (congrArg (fun x => x ∨ i ∈ w) (eq_self i)) (true_or (i ∈ w)))) }a:Finset nha:a ∈ ↑(univ.erase i).powerset⊢ ∀ ⦃x₂ : Finset n⦄, x₂ ∈ ↑(univ.erase i).powerset → insert i a = insert i x₂ → a = x₂ n:Type u_1inst✝¹:DecidableEq ninst✝:Fintype nc:ℝhc:1 / 2 < ch:∀ (A : Finset (Finset n)), A ≠ {∅} → IsUnionClosed A → ∃ i, c * ↑(#A) ≤ ↑(#({x ∈ A | i ∈ x}))hn✝:Nonempty nA:Finset (Finset n) := univh_ne_singleton_empty:A ≠ {∅} := have this := of_eq_true (Eq.trans (congrArg (fun x => x = 2 ^ Fintype.card n) Fintype.card_finset) (eq_self (2 ^ Fintype.card n))); have this := of_eq_true (Eq.trans (Eq.trans (congrArg (LT.lt 1) this) (Nat.one_lt_pow_iff._simp_1 (of_eq_true (Eq.trans (congrArg Not Fintype.card_ne_zero._simp_1) not_false_eq_true)))) Nat.one_lt_ofNat._simp_1); fun h => False.elim (Eq.mp (Eq.trans (congrArg (LT.lt 1) (Eq.trans (congrArg card h) (card_singleton ∅))) (lt_self_iff_false._simp_1 1)) this)i:nhi:c * ↑(#univ) ≤ ↑(#{x | i ∈ x})hn:1 ≤ Fintype.card n := Eq.mpr (id (congrArg (fun _a => _a) (propext Nat.add_one_le_iff))) Fintype.card_posthis:{x | i ∈ x} = image (insert i) (univ.erase i).powerset := ext fun x => Eq.mpr (id (congr (congrArg Iff (Eq.trans sharpness._simp_8 (Eq.trans (congrArg (fun x_1 => x_1 ∧ i ∈ x) (sharpness._simp_9 x)) (true_and (i ∈ x))))) (Eq.trans sharpness._simp_10 (congrArg Exists (funext fun a => congrArg (fun x_1 => x_1 ∧ insert i a = x) (Eq.trans sharpness._simp_11 (Eq.trans sharpness._simp_12 (Eq.trans (congrArg (fun x => x ∧ i ∉ a) (sharpness._simp_13 a)) (true_and (i ∉ a)))))))))) { mp := fun h => Exists.intro (x.erase i) (of_eq_true (Eq.trans (congr (congrArg And (Eq.trans (congrArg Not (Eq.trans mem_erase._simp_1 (Eq.trans (congr (congrArg And (Eq.trans (congrArg Not (eq_self i)) not_true_eq_false)) (eq_true h)) (and_true False)))) not_false_eq_true)) (Eq.trans (congrArg (fun x_1 => x_1 = x) (insert_erase h)) (eq_self x))) (and_self True))), mpr := fun a => Exists.casesOn a fun w h => And.casesOn h fun left right => right ▸ of_eq_true (Eq.trans mem_insert._simp_1 (Eq.trans (congrArg (fun x => x ∨ i ∈ w) (eq_self i)) (true_or (i ∈ w)))) }a:Finset nha:a ∈ ↑(univ.erase i).powersetb:Finset n⊢ b ∈ ↑(univ.erase i).powerset → insert i a = insert i b → a = b n:Type u_1inst✝¹:DecidableEq ninst✝:Fintype nc:ℝhc:1 / 2 < ch:∀ (A : Finset (Finset n)), A ≠ {∅} → IsUnionClosed A → ∃ i, c * ↑(#A) ≤ ↑(#({x ∈ A | i ∈ x}))hn✝:Nonempty nA:Finset (Finset n) := univh_ne_singleton_empty:A ≠ {∅} := have this := of_eq_true (Eq.trans (congrArg (fun x => x = 2 ^ Fintype.card n) Fintype.card_finset) (eq_self (2 ^ Fintype.card n))); have this := of_eq_true (Eq.trans (Eq.trans (congrArg (LT.lt 1) this) (Nat.one_lt_pow_iff._simp_1 (of_eq_true (Eq.trans (congrArg Not Fintype.card_ne_zero._simp_1) not_false_eq_true)))) Nat.one_lt_ofNat._simp_1); fun h => False.elim (Eq.mp (Eq.trans (congrArg (LT.lt 1) (Eq.trans (congrArg card h) (card_singleton ∅))) (lt_self_iff_false._simp_1 1)) this)i:nhi:c * ↑(#univ) ≤ ↑(#{x | i ∈ x})hn:1 ≤ Fintype.card n := Eq.mpr (id (congrArg (fun _a => _a) (propext Nat.add_one_le_iff))) Fintype.card_posthis:{x | i ∈ x} = image (insert i) (univ.erase i).powerset := ext fun x => Eq.mpr (id (congr (congrArg Iff (Eq.trans sharpness._simp_8 (Eq.trans (congrArg (fun x_1 => x_1 ∧ i ∈ x) (sharpness._simp_9 x)) (true_and (i ∈ x))))) (Eq.trans sharpness._simp_10 (congrArg Exists (funext fun a => congrArg (fun x_1 => x_1 ∧ insert i a = x) (Eq.trans sharpness._simp_11 (Eq.trans sharpness._simp_12 (Eq.trans (congrArg (fun x => x ∧ i ∉ a) (sharpness._simp_13 a)) (true_and (i ∉ a)))))))))) { mp := fun h => Exists.intro (x.erase i) (of_eq_true (Eq.trans (congr (congrArg And (Eq.trans (congrArg Not (Eq.trans mem_erase._simp_1 (Eq.trans (congr (congrArg And (Eq.trans (congrArg Not (eq_self i)) not_true_eq_false)) (eq_true h)) (and_true False)))) not_false_eq_true)) (Eq.trans (congrArg (fun x_1 => x_1 = x) (insert_erase h)) (eq_self x))) (and_self True))), mpr := fun a => Exists.casesOn a fun w h => And.casesOn h fun left right => right ▸ of_eq_true (Eq.trans mem_insert._simp_1 (Eq.trans (congrArg (fun x => x ∨ i ∈ w) (eq_self i)) (true_or (i ∈ w)))) }a:Finset nha:a ∈ ↑(univ.erase i).powersetb:Finset nhb:b ∈ ↑(univ.erase i).powerset⊢ insert i a = insert i b → a = b n:Type u_1inst✝¹:DecidableEq ninst✝:Fintype nc:ℝhc:1 / 2 < ch✝:∀ (A : Finset (Finset n)), A ≠ {∅} → IsUnionClosed A → ∃ i, c * ↑(#A) ≤ ↑(#({x ∈ A | i ∈ x}))hn✝:Nonempty nA:Finset (Finset n) := univh_ne_singleton_empty:A ≠ {∅} := have this := of_eq_true (Eq.trans (congrArg (fun x => x = 2 ^ Fintype.card n) Fintype.card_finset) (eq_self (2 ^ Fintype.card n))); have this := of_eq_true (Eq.trans (Eq.trans (congrArg (LT.lt 1) this) (Nat.one_lt_pow_iff._simp_1 (of_eq_true (Eq.trans (congrArg Not Fintype.card_ne_zero._simp_1) not_false_eq_true)))) Nat.one_lt_ofNat._simp_1); fun h => False.elim (Eq.mp (Eq.trans (congrArg (LT.lt 1) (Eq.trans (congrArg card h) (card_singleton ∅))) (lt_self_iff_false._simp_1 1)) this)i:nhi:c * ↑(#univ) ≤ ↑(#{x | i ∈ x})hn:1 ≤ Fintype.card n := Eq.mpr (id (congrArg (fun _a => _a) (propext Nat.add_one_le_iff))) Fintype.card_posthis:{x | i ∈ x} = image (insert i) (univ.erase i).powerset := ext fun x => Eq.mpr (id (congr (congrArg Iff (Eq.trans sharpness._simp_8 (Eq.trans (congrArg (fun x_1 => x_1 ∧ i ∈ x) (sharpness._simp_9 x)) (true_and (i ∈ x))))) (Eq.trans sharpness._simp_10 (congrArg Exists (funext fun a => congrArg (fun x_1 => x_1 ∧ insert i a = x) (Eq.trans sharpness._simp_11 (Eq.trans sharpness._simp_12 (Eq.trans (congrArg (fun x => x ∧ i ∉ a) (sharpness._simp_13 a)) (true_and (i ∉ a)))))))))) { mp := fun h => Exists.intro (x.erase i) (of_eq_true (Eq.trans (congr (congrArg And (Eq.trans (congrArg Not (Eq.trans mem_erase._simp_1 (Eq.trans (congr (congrArg And (Eq.trans (congrArg Not (eq_self i)) not_true_eq_false)) (eq_true h)) (and_true False)))) not_false_eq_true)) (Eq.trans (congrArg (fun x_1 => x_1 = x) (insert_erase h)) (eq_self x))) (and_self True))), mpr := fun a => Exists.casesOn a fun w h => And.casesOn h fun left right => right ▸ of_eq_true (Eq.trans mem_insert._simp_1 (Eq.trans (congrArg (fun x => x ∨ i ∈ w) (eq_self i)) (true_or (i ∈ w)))) }a:Finset nha:a ∈ ↑(univ.erase i).powersetb:Finset nhb:b ∈ ↑(univ.erase i).powerseth:insert i a = insert i b⊢ a = b n:Type u_1inst✝¹:DecidableEq ninst✝:Fintype nc:ℝhc:1 / 2 < ch✝:∀ (A : Finset (Finset n)), A ≠ {∅} → IsUnionClosed A → ∃ i, c * ↑(#A) ≤ ↑(#({x ∈ A | i ∈ x}))hn✝:Nonempty nA:Finset (Finset n) := univh_ne_singleton_empty:A ≠ {∅} := have this := of_eq_true (Eq.trans (congrArg (fun x => x = 2 ^ Fintype.card n) Fintype.card_finset) (eq_self (2 ^ Fintype.card n))); have this := of_eq_true (Eq.trans (Eq.trans (congrArg (LT.lt 1) this) (Nat.one_lt_pow_iff._simp_1 (of_eq_true (Eq.trans (congrArg Not Fintype.card_ne_zero._simp_1) not_false_eq_true)))) Nat.one_lt_ofNat._simp_1); fun h => False.elim (Eq.mp (Eq.trans (congrArg (LT.lt 1) (Eq.trans (congrArg card h) (card_singleton ∅))) (lt_self_iff_false._simp_1 1)) this)i:nhi:c * ↑(#univ) ≤ ↑(#{x | i ∈ x})hn:1 ≤ Fintype.card n := Eq.mpr (id (congrArg (fun _a => _a) (propext Nat.add_one_le_iff))) Fintype.card_posthis:{x | i ∈ x} = image (insert i) (univ.erase i).powerset := ext fun x => Eq.mpr (id (congr (congrArg Iff (Eq.trans sharpness._simp_8 (Eq.trans (congrArg (fun x_1 => x_1 ∧ i ∈ x) (sharpness._simp_9 x)) (true_and (i ∈ x))))) (Eq.trans sharpness._simp_10 (congrArg Exists (funext fun a => congrArg (fun x_1 => x_1 ∧ insert i a = x) (Eq.trans sharpness._simp_11 (Eq.trans sharpness._simp_12 (Eq.trans (congrArg (fun x => x ∧ i ∉ a) (sharpness._simp_13 a)) (true_and (i ∉ a)))))))))) { mp := fun h => Exists.intro (x.erase i) (of_eq_true (Eq.trans (congr (congrArg And (Eq.trans (congrArg Not (Eq.trans mem_erase._simp_1 (Eq.trans (congr (congrArg And (Eq.trans (congrArg Not (eq_self i)) not_true_eq_false)) (eq_true h)) (and_true False)))) not_false_eq_true)) (Eq.trans (congrArg (fun x_1 => x_1 = x) (insert_erase h)) (eq_self x))) (and_self True))), mpr := fun a => Exists.casesOn a fun w h => And.casesOn h fun left right => right ▸ of_eq_true (Eq.trans mem_insert._simp_1 (Eq.trans (congrArg (fun x => x ∨ i ∈ w) (eq_self i)) (true_or (i ∈ w)))) }a:Finset nb:Finset nh:insert i a = insert i bha:i ∉ ahb:i ∉ b⊢ a = b n:Type u_1inst✝¹:DecidableEq ninst✝:Fintype nc:ℝhc:1 / 2 < ch✝:∀ (A : Finset (Finset n)), A ≠ {∅} → IsUnionClosed A → ∃ i, c * ↑(#A) ≤ ↑(#({x ∈ A | i ∈ x}))hn✝:Nonempty nA:Finset (Finset n) := univh_ne_singleton_empty:A ≠ {∅} := have this := of_eq_true (Eq.trans (congrArg (fun x => x = 2 ^ Fintype.card n) Fintype.card_finset) (eq_self (2 ^ Fintype.card n))); have this := of_eq_true (Eq.trans (Eq.trans (congrArg (LT.lt 1) this) (Nat.one_lt_pow_iff._simp_1 (of_eq_true (Eq.trans (congrArg Not Fintype.card_ne_zero._simp_1) not_false_eq_true)))) Nat.one_lt_ofNat._simp_1); fun h => False.elim (Eq.mp (Eq.trans (congrArg (LT.lt 1) (Eq.trans (congrArg card h) (card_singleton ∅))) (lt_self_iff_false._simp_1 1)) this)i:nhi:c * ↑(#univ) ≤ ↑(#{x | i ∈ x})hn:1 ≤ Fintype.card n := Eq.mpr (id (congrArg (fun _a => _a) (propext Nat.add_one_le_iff))) Fintype.card_posthis✝:{x | i ∈ x} = image (insert i) (univ.erase i).powerset := ext fun x => Eq.mpr (id (congr (congrArg Iff (Eq.trans sharpness._simp_8 (Eq.trans (congrArg (fun x_1 => x_1 ∧ i ∈ x) (sharpness._simp_9 x)) (true_and (i ∈ x))))) (Eq.trans sharpness._simp_10 (congrArg Exists (funext fun a => congrArg (fun x_1 => x_1 ∧ insert i a = x) (Eq.trans sharpness._simp_11 (Eq.trans sharpness._simp_12 (Eq.trans (congrArg (fun x => x ∧ i ∉ a) (sharpness._simp_13 a)) (true_and (i ∉ a)))))))))) { mp := fun h => Exists.intro (x.erase i) (of_eq_true (Eq.trans (congr (congrArg And (Eq.trans (congrArg Not (Eq.trans mem_erase._simp_1 (Eq.trans (congr (congrArg And (Eq.trans (congrArg Not (eq_self i)) not_true_eq_false)) (eq_true h)) (and_true False)))) not_false_eq_true)) (Eq.trans (congrArg (fun x_1 => x_1 = x) (insert_erase h)) (eq_self x))) (and_self True))), mpr := fun a => Exists.casesOn a fun w h => And.casesOn h fun left right => right ▸ of_eq_true (Eq.trans mem_insert._simp_1 (Eq.trans (congrArg (fun x => x ∨ i ∈ w) (eq_self i)) (true_or (i ∈ w)))) }a:Finset nb:Finset nh:insert i a = insert i bha:i ∉ ahb:i ∉ bthis:(insert i a).erase i = (insert i b).erase i := id (congrArg (fun x => x.erase i) h)⊢ a = b rwa [erase_insert ha, erase_insert hbn:Type u_1inst✝¹:DecidableEq ninst✝:Fintype nc:ℝhc:1 / 2 < ch✝:∀ (A : Finset (Finset n)), A ≠ {∅} → IsUnionClosed A → ∃ i, c * ↑(#A) ≤ ↑(#({x ∈ A | i ∈ x}))hn✝:Nonempty nA:Finset (Finset n) := univh_ne_singleton_empty:A ≠ {∅} := have this := of_eq_true (Eq.trans (congrArg (fun x => x = 2 ^ Fintype.card n) Fintype.card_finset) (eq_self (2 ^ Fintype.card n))); have this := of_eq_true (Eq.trans (Eq.trans (congrArg (LT.lt 1) this) (Nat.one_lt_pow_iff._simp_1 (of_eq_true (Eq.trans (congrArg Not Fintype.card_ne_zero._simp_1) not_false_eq_true)))) Nat.one_lt_ofNat._simp_1); fun h => False.elim (Eq.mp (Eq.trans (congrArg (LT.lt 1) (Eq.trans (congrArg card h) (card_singleton ∅))) (lt_self_iff_false._simp_1 1)) this)i:nhi:c * ↑(#univ) ≤ ↑(#{x | i ∈ x})hn:1 ≤ Fintype.card n := Eq.mpr (id (congrArg (fun _a => _a) (propext Nat.add_one_le_iff))) Fintype.card_posthis✝:{x | i ∈ x} = image (insert i) (univ.erase i).powerset := ext fun x => Eq.mpr (id (congr (congrArg Iff (Eq.trans sharpness._simp_8 (Eq.trans (congrArg (fun x_1 => x_1 ∧ i ∈ x) (sharpness._simp_9 x)) (true_and (i ∈ x))))) (Eq.trans sharpness._simp_10 (congrArg Exists (funext fun a => congrArg (fun x_1 => x_1 ∧ insert i a = x) (Eq.trans sharpness._simp_11 (Eq.trans sharpness._simp_12 (Eq.trans (congrArg (fun x => x ∧ i ∉ a) (sharpness._simp_13 a)) (true_and (i ∉ a)))))))))) { mp := fun h => Exists.intro (x.erase i) (of_eq_true (Eq.trans (congr (congrArg And (Eq.trans (congrArg Not (Eq.trans mem_erase._simp_1 (Eq.trans (congr (congrArg And (Eq.trans (congrArg Not (eq_self i)) not_true_eq_false)) (eq_true h)) (and_true False)))) not_false_eq_true)) (Eq.trans (congrArg (fun x_1 => x_1 = x) (insert_erase h)) (eq_self x))) (and_self True))), mpr := fun a => Exists.casesOn a fun w h => And.casesOn h fun left right => right ▸ of_eq_true (Eq.trans mem_insert._simp_1 (Eq.trans (congrArg (fun x => x ∨ i ∈ w) (eq_self i)) (true_or (i ∈ w)))) }a:Finset nb:Finset nh:insert i a = insert i bha:i ∉ ahb:i ∉ bthis:a = b⊢ a = b at this n:Type u_1inst✝¹:DecidableEq ninst✝:Fintype nc:ℝhc:1 / 2 < ch:∀ (A : Finset (Finset n)), A ≠ {∅} → IsUnionClosed A → ∃ i, c * ↑(#A) ≤ ↑(#({x ∈ A | i ∈ x}))hn✝:Nonempty nA:Finset (Finset n) := univh_ne_singleton_empty:A ≠ {∅} := have this := of_eq_true (Eq.trans (congrArg (fun x => x = 2 ^ Fintype.card n) Fintype.card_finset) (eq_self (2 ^ Fintype.card n))); have this := of_eq_true (Eq.trans (Eq.trans (congrArg (LT.lt 1) this) (Nat.one_lt_pow_iff._simp_1 (of_eq_true (Eq.trans (congrArg Not Fintype.card_ne_zero._simp_1) not_false_eq_true)))) Nat.one_lt_ofNat._simp_1); fun h => False.elim (Eq.mp (Eq.trans (congrArg (LT.lt 1) (Eq.trans (congrArg card h) (card_singleton ∅))) (lt_self_iff_false._simp_1 1)) this)i:nhn:1 ≤ Fintype.card n := Eq.mpr (id (congrArg (fun _a => _a) (propext Nat.add_one_le_iff))) Fintype.card_posthis:#{x | i ∈ x} = 2 ^ (Fintype.card n - 1) := have this := ext fun x => Eq.mpr (id (congr (congrArg Iff (Eq.trans sharpness._simp_8 (Eq.trans (congrArg (fun x_1 => x_1 ∧ i ∈ x) (sharpness._simp_9 x)) (true_and (i ∈ x))))) (Eq.trans sharpness._simp_10 (congrArg Exists (funext fun a => congrArg (fun x_1 => x_1 ∧ insert i a = x) (Eq.trans sharpness._simp_11 (Eq.trans sharpness._simp_12 (Eq.trans (congrArg (fun x => x ∧ i ∉ a) (sharpness._simp_13 a)) (true_and (i ∉ a)))))))))) { mp := fun h => Exists.intro (x.erase i) (of_eq_true (Eq.trans (congr (congrArg And (Eq.trans (congrArg Not (Eq.trans mem_erase._simp_1 (Eq.trans (congr (congrArg And (Eq.trans (congrArg Not (eq_self i)) not_true_eq_false)) (eq_true h)) (and_true False)))) not_false_eq_true)) (Eq.trans (congrArg (fun x_1 => x_1 = x) (insert_erase h)) (eq_self x))) (and_self True))), mpr := fun a => Exists.casesOn a fun w h => And.casesOn h fun left right => right ▸ of_eq_true (Eq.trans mem_insert._simp_1 (Eq.trans (congrArg (fun x => x ∨ i ∈ w) (eq_self i)) (true_or (i ∈ w)))) }; Eq.mpr (id (congrArg (fun _a => #_a = 2 ^ (Fintype.card n - 1)) this)) (Eq.mpr (id (congrArg (fun _a => _a = 2 ^ (Fintype.card n - 1)) (card_image_of_injOn fun ⦃a⦄ ha ⦃b⦄ hb h => have this := id (congrArg (fun x => x.erase i) h); Eq.mp (congrArg (fun _a => a = _a) (erase_insert (Eq.mp (Eq.trans (Eq.trans (congrArg (fun x => b ∈ x) (Eq.trans (coe_powerset (univ.erase i)) (congrArg (fun x => SetLike.coe ⁻¹' 𝒫 x) (Eq.trans (coe_erase i univ) (congrArg (fun x => x \ {i}) coe_univ))))) sharpness._simp_14) (Eq.trans (sharpness._simp_15 (↑b) (Set.univ \ {i})) (Eq.trans sharpness._simp_16 (Eq.trans (congr (congrArg And (sharpness._simp_17 ↑b)) (Eq.trans sharpness._simp_18 (congrArg Not sharpness._simp_19))) (true_and (i ∉ b)))))) hb))) (Eq.mp (congrArg (fun _a => _a = (insert i b).erase i) (erase_insert (Eq.mp (Eq.trans (Eq.trans (congrArg (fun x => a ∈ x) (Eq.trans (coe_powerset (univ.erase i)) (congrArg (fun x => SetLike.coe ⁻¹' 𝒫 x) (Eq.trans (coe_erase i univ) (congrArg (fun x => x \ {i}) coe_univ))))) sharpness._simp_14) (Eq.trans (sharpness._simp_15 (↑a) (Set.univ \ {i})) (Eq.trans sharpness._simp_16 (Eq.trans (congr (congrArg And (sharpness._simp_17 ↑a)) (Eq.trans sharpness._simp_18 (congrArg Not sharpness._simp_19))) (true_and (i ∉ a)))))) ha))) this)))) (Eq.mpr (id (congrArg (fun _a => _a = 2 ^ (Fintype.card n - 1)) (card_powerset (univ.erase i)))) (of_eq_true (Eq.trans (congrArg (fun x => 2 ^ x = 2 ^ (Fintype.card n - 1)) (card_erase_of_mem (of_eq_true (mem_univ._simp_1 i)))) (eq_self (2 ^ (Fintype.card n - 1)))))))hi:c * 2 ^ Fintype.card n ≤ 2 ^ (Fintype.card n - 1)⊢ False n:Type u_1inst✝¹:DecidableEq ninst✝:Fintype nc:ℝhc:1 / 2 < ch:∀ (A : Finset (Finset n)), A ≠ {∅} → IsUnionClosed A → ∃ i, c * ↑(#A) ≤ ↑(#({x ∈ A | i ∈ x}))hn✝:Nonempty nA:Finset (Finset n) := univh_ne_singleton_empty:A ≠ {∅} := have this := of_eq_true (Eq.trans (congrArg (fun x => x = 2 ^ Fintype.card n) Fintype.card_finset) (eq_self (2 ^ Fintype.card n))); have this := of_eq_true (Eq.trans (Eq.trans (congrArg (LT.lt 1) this) (Nat.one_lt_pow_iff._simp_1 (of_eq_true (Eq.trans (congrArg Not Fintype.card_ne_zero._simp_1) not_false_eq_true)))) Nat.one_lt_ofNat._simp_1); fun h => False.elim (Eq.mp (Eq.trans (congrArg (LT.lt 1) (Eq.trans (congrArg card h) (card_singleton ∅))) (lt_self_iff_false._simp_1 1)) this)i:nhn:1 ≤ Fintype.card n := Eq.mpr (id (congrArg (fun _a => _a) (propext Nat.add_one_le_iff))) Fintype.card_posthis:#{x | i ∈ x} = 2 ^ (Fintype.card n - 1) := have this := ext fun x => Eq.mpr (id (congr (congrArg Iff (Eq.trans sharpness._simp_8 (Eq.trans (congrArg (fun x_1 => x_1 ∧ i ∈ x) (sharpness._simp_9 x)) (true_and (i ∈ x))))) (Eq.trans sharpness._simp_10 (congrArg Exists (funext fun a => congrArg (fun x_1 => x_1 ∧ insert i a = x) (Eq.trans sharpness._simp_11 (Eq.trans sharpness._simp_12 (Eq.trans (congrArg (fun x => x ∧ i ∉ a) (sharpness._simp_13 a)) (true_and (i ∉ a)))))))))) { mp := fun h => Exists.intro (x.erase i) (of_eq_true (Eq.trans (congr (congrArg And (Eq.trans (congrArg Not (Eq.trans mem_erase._simp_1 (Eq.trans (congr (congrArg And (Eq.trans (congrArg Not (eq_self i)) not_true_eq_false)) (eq_true h)) (and_true False)))) not_false_eq_true)) (Eq.trans (congrArg (fun x_1 => x_1 = x) (insert_erase h)) (eq_self x))) (and_self True))), mpr := fun a => Exists.casesOn a fun w h => And.casesOn h fun left right => right ▸ of_eq_true (Eq.trans mem_insert._simp_1 (Eq.trans (congrArg (fun x => x ∨ i ∈ w) (eq_self i)) (true_or (i ∈ w)))) }; Eq.mpr (id (congrArg (fun _a => #_a = 2 ^ (Fintype.card n - 1)) this)) (Eq.mpr (id (congrArg (fun _a => _a = 2 ^ (Fintype.card n - 1)) (card_image_of_injOn fun ⦃a⦄ ha ⦃b⦄ hb h => have this := id (congrArg (fun x => x.erase i) h); Eq.mp (congrArg (fun _a => a = _a) (erase_insert (Eq.mp (Eq.trans (Eq.trans (congrArg (fun x => b ∈ x) (Eq.trans (coe_powerset (univ.erase i)) (congrArg (fun x => SetLike.coe ⁻¹' 𝒫 x) (Eq.trans (coe_erase i univ) (congrArg (fun x => x \ {i}) coe_univ))))) sharpness._simp_14) (Eq.trans (sharpness._simp_15 (↑b) (Set.univ \ {i})) (Eq.trans sharpness._simp_16 (Eq.trans (congr (congrArg And (sharpness._simp_17 ↑b)) (Eq.trans sharpness._simp_18 (congrArg Not sharpness._simp_19))) (true_and (i ∉ b)))))) hb))) (Eq.mp (congrArg (fun _a => _a = (insert i b).erase i) (erase_insert (Eq.mp (Eq.trans (Eq.trans (congrArg (fun x => a ∈ x) (Eq.trans (coe_powerset (univ.erase i)) (congrArg (fun x => SetLike.coe ⁻¹' 𝒫 x) (Eq.trans (coe_erase i univ) (congrArg (fun x => x \ {i}) coe_univ))))) sharpness._simp_14) (Eq.trans (sharpness._simp_15 (↑a) (Set.univ \ {i})) (Eq.trans sharpness._simp_16 (Eq.trans (congr (congrArg And (sharpness._simp_17 ↑a)) (Eq.trans sharpness._simp_18 (congrArg Not sharpness._simp_19))) (true_and (i ∉ a)))))) ha))) this)))) (Eq.mpr (id (congrArg (fun _a => _a = 2 ^ (Fintype.card n - 1)) (card_powerset (univ.erase i)))) (of_eq_true (Eq.trans (congrArg (fun x => 2 ^ x = 2 ^ (Fintype.card n - 1)) (card_erase_of_mem (of_eq_true (mem_univ._simp_1 i)))) (eq_self (2 ^ (Fintype.card n - 1)))))))hi:c * 2 ^ Fintype.card n ≤ 2 ^ Fintype.card n * (2 ^ 1)⁻¹⊢ False -- which is a contradiction. have : (1 / 2 : ℚ) * 2 ^ (Fintype.card n) < c * 2 ^ (Fintype.card n) := n:Type u_1inst✝¹:DecidableEq ninst✝:Fintype nc:ℝhc:1 / 2 < c⊢ ¬∀ (A : Finset (Finset n)), A ≠ {∅} → IsUnionClosed A → ∃ i, c * ↑(#A) ≤ ↑(#({x ∈ A | i ∈ x})) n:Type u_1inst✝¹:DecidableEq ninst✝:Fintype nc:ℝhc:1 / 2 < ch:∀ (A : Finset (Finset n)), A ≠ {∅} → IsUnionClosed A → ∃ i, c * ↑(#A) ≤ ↑(#({x ∈ A | i ∈ x}))hn✝:Nonempty nA:Finset (Finset n) := univh_ne_singleton_empty:A ≠ {∅} := have this := of_eq_true (Eq.trans (congrArg (fun x => x = 2 ^ Fintype.card n) Fintype.card_finset) (eq_self (2 ^ Fintype.card n))); have this := of_eq_true (Eq.trans (Eq.trans (congrArg (LT.lt 1) this) (Nat.one_lt_pow_iff._simp_1 (of_eq_true (Eq.trans (congrArg Not Fintype.card_ne_zero._simp_1) not_false_eq_true)))) Nat.one_lt_ofNat._simp_1); fun h => False.elim (Eq.mp (Eq.trans (congrArg (LT.lt 1) (Eq.trans (congrArg card h) (card_singleton ∅))) (lt_self_iff_false._simp_1 1)) this)i:nhn:1 ≤ Fintype.card n := Eq.mpr (id (congrArg (fun _a => _a) (propext Nat.add_one_le_iff))) Fintype.card_posthis:#{x | i ∈ x} = 2 ^ (Fintype.card n - 1) := have this := ext fun x => Eq.mpr (id (congr (congrArg Iff (Eq.trans sharpness._simp_8 (Eq.trans (congrArg (fun x_1 => x_1 ∧ i ∈ x) (sharpness._simp_9 x)) (true_and (i ∈ x))))) (Eq.trans sharpness._simp_10 (congrArg Exists (funext fun a => congrArg (fun x_1 => x_1 ∧ insert i a = x) (Eq.trans sharpness._simp_11 (Eq.trans sharpness._simp_12 (Eq.trans (congrArg (fun x => x ∧ i ∉ a) (sharpness._simp_13 a)) (true_and (i ∉ a)))))))))) { mp := fun h => Exists.intro (x.erase i) (of_eq_true (Eq.trans (congr (congrArg And (Eq.trans (congrArg Not (Eq.trans mem_erase._simp_1 (Eq.trans (congr (congrArg And (Eq.trans (congrArg Not (eq_self i)) not_true_eq_false)) (eq_true h)) (and_true False)))) not_false_eq_true)) (Eq.trans (congrArg (fun x_1 => x_1 = x) (insert_erase h)) (eq_self x))) (and_self True))), mpr := fun a => Exists.casesOn a fun w h => And.casesOn h fun left right => right ▸ of_eq_true (Eq.trans mem_insert._simp_1 (Eq.trans (congrArg (fun x => x ∨ i ∈ w) (eq_self i)) (true_or (i ∈ w)))) }; Eq.mpr (id (congrArg (fun _a => #_a = 2 ^ (Fintype.card n - 1)) this)) (Eq.mpr (id (congrArg (fun _a => _a = 2 ^ (Fintype.card n - 1)) (card_image_of_injOn fun ⦃a⦄ ha ⦃b⦄ hb h => have this := id (congrArg (fun x => x.erase i) h); Eq.mp (congrArg (fun _a => a = _a) (erase_insert (Eq.mp (Eq.trans (Eq.trans (congrArg (fun x => b ∈ x) (Eq.trans (coe_powerset (univ.erase i)) (congrArg (fun x => SetLike.coe ⁻¹' 𝒫 x) (Eq.trans (coe_erase i univ) (congrArg (fun x => x \ {i}) coe_univ))))) sharpness._simp_14) (Eq.trans (sharpness._simp_15 (↑b) (Set.univ \ {i})) (Eq.trans sharpness._simp_16 (Eq.trans (congr (congrArg And (sharpness._simp_17 ↑b)) (Eq.trans sharpness._simp_18 (congrArg Not sharpness._simp_19))) (true_and (i ∉ b)))))) hb))) (Eq.mp (congrArg (fun _a => _a = (insert i b).erase i) (erase_insert (Eq.mp (Eq.trans (Eq.trans (congrArg (fun x => a ∈ x) (Eq.trans (coe_powerset (univ.erase i)) (congrArg (fun x => SetLike.coe ⁻¹' 𝒫 x) (Eq.trans (coe_erase i univ) (congrArg (fun x => x \ {i}) coe_univ))))) sharpness._simp_14) (Eq.trans (sharpness._simp_15 (↑a) (Set.univ \ {i})) (Eq.trans sharpness._simp_16 (Eq.trans (congr (congrArg And (sharpness._simp_17 ↑a)) (Eq.trans sharpness._simp_18 (congrArg Not sharpness._simp_19))) (true_and (i ∉ a)))))) ha))) this)))) (Eq.mpr (id (congrArg (fun _a => _a = 2 ^ (Fintype.card n - 1)) (card_powerset (univ.erase i)))) (of_eq_true (Eq.trans (congrArg (fun x => 2 ^ x = 2 ^ (Fintype.card n - 1)) (card_erase_of_mem (of_eq_true (mem_univ._simp_1 i)))) (eq_self (2 ^ (Fintype.card n - 1)))))))hi:c * 2 ^ Fintype.card n ≤ 2 ^ Fintype.card n * (2 ^ 1)⁻¹⊢ ↑(1 / 2) < c All goals completed! 🐙 have : (0 : ℝ) < 0 := n:Type u_1inst✝¹:DecidableEq ninst✝:Fintype nc:ℝhc:1 / 2 < c⊢ ¬∀ (A : Finset (Finset n)), A ≠ {∅} → IsUnionClosed A → ∃ i, c * ↑(#A) ≤ ↑(#({x ∈ A | i ∈ x})) All goals completed! 🐙 All goals completed! 🐙

If the UC conjecture is tight for some family A then $|A| = 2^k$ for some $k$.

Reference: Conjecture 3 in https://www.nieuwarchief.nl/serie5/pdf/naw5-2023-24-4-225.pdf.

@[category research open, AMS 5] theorem declaration uses 'sorry'union_closed.variants.cardinality_even_of_union_closed_tight [Nonempty n] (hA : A ≠ {∅} ∧ A ≠ ∅) (hA : IsUnionClosed A) (UCC_tight : ∀ i, #{x ∈ A | i ∈ x} = (1 / 2 : ℝ) * #A) : ∃ k, #A = 2 ^ k := n:Type u_1inst✝¹:DecidableEq nA:Finset (Finset n)inst✝:Nonempty nhA✝:A ≠ {∅} ∧ A ≠ ∅hA:IsUnionClosed AUCC_tight:∀ (i : n), ↑(#({x ∈ A | i ∈ x})) = 1 / 2 * ↑(#A)⊢ ∃ k, #A = 2 ^ k All goals completed! 🐙 end UnionClosed