awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.SetFamily.Intersecting
Goal:
α : Type u_1
inst : BooleanAlgebra α
inst_1 : Nontrivial α
inst_2 : Fintype α
s_1 : Finset α
this : #s_1 ≤ Fintype.card α / 2
s : Finset α
ih :
  ∀ {t₂ : Finset α},
    #t₂ ≤ Fintype.card α / 2 →
      s ⊂ t₂ →
        ∀ (hs : (↑t₂ : Set α).Intersecting),
          ∃ (t : Finset α), t₂ ⊆ t ∧ 2 * #t = Fintype.card α ∧ (↑t : Set α).Intersecting
_hcard : #s ≤ Fintype.card α / 2
hs : (↑s : Set α).Intersecting
t : Finset α
ht : (↑t : Set α).Intersecting
hst : s ⊆ t ∧ s ≠ t
⊢ ∃ (t : Finset α), s ⊆ t ∧ 2 * #t = Fintype.card α ∧ (↑t : Set α).Intersecting

Tactic:
(ih ?_ (_root_.ssubset_iff_subset_ne.2 hst) ht).imp fun u => And.imp_left hst.1.trans

Premises used: Iff.mpr, HasSubset.Subset.trans, And.imp_left, Exists.imp, And.left, ssubset_iff_subset_ne
-- Module: Mathlib.Combinatorics.SetFamily.Intersecting
Goal:
α : Type u_1
inst : BooleanAlgebra α
inst_1 : Nontrivial α
inst_2 : Fintype α
s_1 : Finset α
this : #s_1 ≤ Fintype.card α / 2
s : Finset α
ih :
  ∀ {t₂ : Finset α},
    #t₂ ≤ Fintype.card α / 2 →
      s ⊂ t₂ →
        ∀ (hs : (↑t₂ : Set α).Intersecting),
          ∃ (t : Finset α), t₂ ⊆ t ∧ 2 * #t = Fintype.card α ∧ (↑t : Set α).Intersecting
_hcard : #s ≤ Fintype.card α / 2
hs : (↑s : Set α).Intersecting
t : Finset α
ht : (↑t : Set α).Intersecting
hst : s ⊆ t ∧ s ≠ t
neg : #t ≤ Fintype.card α / 2
⊢ ∃ (t : Finset α), s ⊆ t ∧ 2 * #t = Fintype.card α ∧ (↑t : Set α).Intersecting

Tactic:
refine (ih ?_ (_root_.ssubset_iff_subset_ne.2 hst) ht).imp fun u => And.imp_left hst.1.trans

Premises used: Iff.mpr, HasSubset.Subset.trans, And.imp_left, Exists.imp, And.left, ssubset_iff_subset_ne
-- Module: Mathlib.Combinatorics.SetFamily.Intersecting
Goal:
α : Type u_1
inst : BooleanAlgebra α
inst_1 : Nontrivial α
inst_2 : Fintype α
s_1 : Finset α
this : #s_1 ≤ Fintype.card α / 2
s : Finset α
ih :
  ∀ {t₂ : Finset α},
    #t₂ ≤ Fintype.card α / 2 →
      s ⊂ t₂ →
        ∀ (hs : (↑t₂ : Set α).Intersecting),
          ∃ (t : Finset α), t₂ ⊆ t ∧ 2 * #t = Fintype.card α ∧ (↑t : Set α).Intersecting
_hcard : #s ≤ Fintype.card α / 2
hs : (↑s : Set α).Intersecting
t : Finset α
ht : (↑t : Set α).Intersecting
hst : s ⊆ t ∧ s ≠ t
neg : 2 * #t ≤ Fintype.card α
⊢ #t ≤ Fintype.card α / 2

Tactic:
rw [Nat.le_div_iff_mul_le Nat.two_pos, Nat.mul_comm]

Premises used: Nat.two_pos, Nat.mul_comm, Nat.le_div_iff_mul_le
-- Module: Mathlib.Combinatorics.SetFamily.Intersecting
Goal:
α : Type u_1
inst : BooleanAlgebra α
inst_1 : Nontrivial α
inst_2 : Fintype α
s_1 : Finset α
this : #s_1 ≤ Fintype.card α / 2
s : Finset α
ih :
  ∀ {t₂ : Finset α},
    #t₂ ≤ Fintype.card α / 2 →
      s ⊂ t₂ →
        ∀ (hs : (↑t₂ : Set α).Intersecting),
          ∃ (t : Finset α), t₂ ⊆ t ∧ 2 * #t = Fintype.card α ∧ (↑t : Set α).Intersecting
_hcard : #s ≤ Fintype.card α / 2
hs : (↑s : Set α).Intersecting
t : Finset α
ht : (↑t : Set α).Intersecting
hst : s ⊆ t ∧ s ≠ t
⊢ 2 * #t ≤ Fintype.card α

Tactic:
ht.card_le

Premises used: Set.Intersecting.card_le
-- Module: Mathlib.Combinatorics.SetFamily.Intersecting
Goal:
α : Type u_1
inst : BooleanAlgebra α
inst_1 : Nontrivial α
inst_2 : Fintype α
s_1 : Finset α
this : #s_1 ≤ Fintype.card α / 2
s : Finset α
ih :
  ∀ {t₂ : Finset α},
    #t₂ ≤ Fintype.card α / 2 →
      s ⊂ t₂ →
        ∀ (hs : (↑t₂ : Set α).Intersecting),
          ∃ (t : Finset α), t₂ ⊆ t ∧ 2 * #t = Fintype.card α ∧ (↑t : Set α).Intersecting
_hcard : #s ≤ Fintype.card α / 2
hs : (↑s : Set α).Intersecting
t : Finset α
ht : (↑t : Set α).Intersecting
hst : s ⊆ t ∧ s ≠ t
⊢ 2 * #t ≤ Fintype.card α

Tactic:
exact ht.card_le

Premises used: Set.Intersecting.card_le
-- Module: Mathlib.Combinatorics.SetFamily.Intersecting
Goal:
L L' : Set ℕ
α : Type u_1
inst : DecidableEq α
𝒜 : Set (Finset α)
h : L ⊆ L'
hL : L.IsIntersectingOf 𝒜
tauto tauto₁ tauto₂ tauto₃ tauto₄ tauto₅ :
  ∀ ⦃x : Finset α⦄, x ∈ 𝒜 → ∀ ⦃y : Finset α⦄, y ∈ 𝒜 → x ≠ y → (fun (s t : Finset α) ↦ #(s ∩ t) ∈ L') x y
tauto₆ tauto₇ tauto₈ tauto₉ tauto₁₀ tauto₁₁ tauto₁₂ tauto₁₃ :
  ∀ ⦃x : Finset α⦄, x ∈ 𝒜 → ∀ ⦃y : Finset α⦄, y ∈ 𝒜 → x ≠ y → #(x ∩ y) ∈ L'
⊢ L'.IsIntersectingOf 𝒜

Tactic:
tauto
-- Module: Mathlib.Combinatorics.SetFamily.Intersecting
Goal:
L : Set ℕ
α : Type u_1
inst : DecidableEq α
𝒜 ℬ : Set (Finset α)
h : ℬ ⊆ 𝒜
h𝒜 : L.IsIntersectingOf 𝒜
⊢ L.IsIntersectingOf ℬ

Tactic:
Pairwise.mono h h𝒜

Premises used: Set.Pairwise.mono, Set.IsIntersectingOf
-- Module: Mathlib.Combinatorics.SetFamily.Intersecting
Goal:
L : Set ℕ
α : Type u_1
inst : DecidableEq α
tauto tauto₁ tauto₂ tauto₃ :
  ∀ ⦃x : Finset α⦄,
    Membership.mem (γ := Set (Finset α)) ∅ x →
      ∀ ⦃y : Finset α⦄, Membership.mem (γ := Set (Finset α)) ∅ y → x ≠ y → (fun (s t : Finset α) ↦ #(s ∩ t) ∈ L) x y
⊢ IsIntersectingOf.{u_1} (α := α) L ∅

Tactic:
tauto
-- Module: Mathlib.Combinatorics.SetFamily.Intersecting
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 : Set (Finset α)
⊢ IsIntersectingOf univ 𝒜

Tactic:
𝒜.pairwise_of_forall _ fun _ _ ↦ trivial

Premises used: trivial, Set.pairwise_of_forall, Set.IsIntersectingOf
-- Module: Mathlib.Combinatorics.SetFamily.Kleitman
Goal:
ι : Type u_1
α : Type u_2
inst : Fintype α
inst_1 : DecidableEq α
inst_2 : Nonempty α
s : Finset ι
f : ι → Finset (Finset α)
hf : ∀ i ∈ s, (↑(f i) : Set (Finset α)).Intersecting
⊢ DecidableEq ι

Tactic:
infer_instance
-- Module: Mathlib.Combinatorics.SetFamily.Kleitman
Goal:
ι : Type u_1
α : Type u_2
inst : Fintype α
inst_1 : DecidableEq α
inst_2 : Nonempty α
s : Finset ι
f : ι → Finset (Finset α)
hf : ∀ i ∈ s, (↑(f i) : Set (Finset α)).Intersecting
⊢ DecidableEq ι

Tactic:
classical
    infer_instance
-- Module: Mathlib.Combinatorics.SetFamily.Kleitman
Goal:
ι : Type u_1
α : Type u_2
inst : Fintype α
inst_1 : DecidableEq α
inst_2 : Nonempty α
s : Finset ι
f : ι → Finset (Finset α)
hf : ∀ i ∈ s, (↑(f i) : Set (Finset α)).Intersecting
have :
  ∀ (this : DecidableEq ι),
    #(s.biUnion f) ≤ HPow.hPow (α := ℕ) 2 (Fintype.card α) - HPow.hPow (α := ℕ) 2 (Fintype.card α - #s)
⊢ #(s.biUnion f) ≤ HPow.hPow (α := ℕ) 2 (Fintype.card α) - HPow.hPow (α := ℕ) 2 (Fintype.card α - #s)

Tactic:
have : DecidableEq ι := by
    classical
    infer_instance
-- Module: Mathlib.Combinatorics.SetFamily.Kleitman
Goal:
ι : Type u_1
α : Type u_2
inst : Fintype α
inst_1 : DecidableEq α
inst_2 : Nonempty α
s : Finset ι
f : ι → Finset (Finset α)
hf : ∀ i ∈ s, (↑(f i) : Set (Finset α)).Intersecting
this : DecidableEq ι
inl :
  ∀ (hs : Fintype.card α ≤ #s),
    #(s.biUnion f) ≤ HPow.hPow (α := ℕ) 2 (Fintype.card α) - HPow.hPow (α := ℕ) 2 (Fintype.card α - #s)
inr :
  ∀ (hs : #s ≤ Fintype.card α),
    #(s.biUnion f) ≤ HPow.hPow (α := ℕ) 2 (Fintype.card α) - HPow.hPow (α := ℕ) 2 (Fintype.card α - #s)
⊢ #(s.biUnion f) ≤ HPow.hPow (α := ℕ) 2 (Fintype.card α) - HPow.hPow (α := ℕ) 2 (Fintype.card α - #s)

Tactic:
obtain hs | hs := le_total (Fintype.card α) #s

Premises used: Fintype.card, le_total, Finset.card
-- Module: Mathlib.Combinatorics.SetFamily.Kleitman
Goal:
ι : Type u_1
α : Type u_2
inst : Fintype α
inst_1 : DecidableEq α
inst_2 : Nonempty α
s : Finset ι
f : ι → Finset (Finset α)
hf : ∀ i ∈ s, (↑(f i) : Set (Finset α)).Intersecting
this : DecidableEq ι
hs : Fintype.card α ≤ #s
inl : #(s.biUnion f) ≤ HPow.hPow (α := ℕ) 2 (Fintype.card α) - 1
⊢ #(s.biUnion f) ≤ HPow.hPow (α := ℕ) 2 (Fintype.card α) - HPow.hPow (α := ℕ) 2 (Fintype.card α - #s)

Tactic:
rw [tsub_eq_zero_of_le hs, pow_zero]

Premises used: tsub_eq_zero_of_le, pow_zero
-- Module: Mathlib.Combinatorics.SetFamily.Kleitman
Goal:
ι : Type u_1
α : Type u_2
inst : Fintype α
inst_1 : DecidableEq α
inst_2 : Nonempty α
s : Finset ι
f : ι → Finset (Finset α)
hf : ∀ i ∈ s, (↑(f i) : Set (Finset α)).Intersecting
this : DecidableEq ι
hs : Fintype.card α ≤ #s
⊢ #(s.biUnion f) ≤ HPow.hPow (α := ℕ) 2 (Fintype.card α) - 1

Tactic:
(card_le_card <| biUnion_subset.2 fun i hi a ha ↦
      mem_compl.2 <| notMem_singleton.2 <| (hf _ hi).ne_bot ha).trans_eq ?_

Premises used: Finset.notMem_singleton, Iff.mpr, Set.Intersecting.ne_bot, LE.le.trans_eq, Finset.card_le_card, Finset.mem_compl, Finset.biUnion_subset
-- Module: Mathlib.Combinatorics.SetFamily.Kleitman
Goal:
ι : Type u_1
α : Type u_2
inst : Fintype α
inst_1 : DecidableEq α
inst_2 : Nonempty α
s : Finset ι
f : ι → Finset (Finset α)
hf : ∀ i ∈ s, (↑(f i) : Set (Finset α)).Intersecting
this : DecidableEq ι
hs : Fintype.card α ≤ #s
inl : card (α := Finset α) {⊥}ᶜ = HPow.hPow (α := ℕ) 2 (Fintype.card α) - 1
⊢ #(s.biUnion f) ≤ HPow.hPow (α := ℕ) 2 (Fintype.card α) - 1

Tactic:
refine (card_le_card <| biUnion_subset.2 fun i hi a ha ↦
      mem_compl.2 <| notMem_singleton.2 <| (hf _ hi).ne_bot ha).trans_eq ?_

Premises used: Finset.notMem_singleton, Iff.mpr, Set.Intersecting.ne_bot, LE.le.trans_eq, Finset.card_le_card, Finset.mem_compl, Finset.biUnion_subset
-- Module: Mathlib.Combinatorics.SetFamily.Kleitman
Goal:
ι : Type u_1
α : Type u_2
inst : Fintype α
inst_1 : DecidableEq α
inst_2 : Nonempty α
s : Finset ι
f : ι → Finset (Finset α)
hf : ∀ i ∈ s, (↑(f i) : Set (Finset α)).Intersecting
this : DecidableEq ι
hs : Fintype.card α ≤ #s
inl : Fintype.card.{u_2} (Finset α) - card (α := Finset α) {⊥} = HPow.hPow (α := ℕ) 2 (Fintype.card α) - 1
inl₁ : HPow.hPow (α := ℕ) 2 (Fintype.card α) - card (α := Finset α) {⊥} = HPow.hPow (α := ℕ) 2 (Fintype.card α) - 1
inl₂ inl₃ : HPow.hPow (α := ℕ) 2 (Fintype.card α) - 1 = HPow.hPow (α := ℕ) 2 (Fintype.card α) - 1
⊢ card (α := Finset α) {⊥}ᶜ = HPow.hPow (α := ℕ) 2 (Fintype.card α) - 1

Tactic:
rw [card_compl, Fintype.card_finset, card_singleton]

Premises used: Finset.card_compl, Fintype.card_finset, Finset.card_singleton
-- Module: Mathlib.Combinatorics.SetFamily.Kleitman
Goal:
ι : Type u_1
α : Type u_2
inst : Fintype α
inst_1 : DecidableEq α
inst_2 : Nonempty α
this : DecidableEq ι
f : ι → Finset (Finset α)
hf : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → (↑(f i) : Set (Finset α)).Intersecting
hs : card.{u_1} (α := ι) ∅ ≤ Fintype.card α
⊢ #(Finset.biUnion ∅ f) ≤
    HPow.hPow (α := ℕ) 2 (Fintype.card α) - HPow.hPow (α := ℕ) 2 (Fintype.card α - card.{u_1} (α := ι) ∅)

Tactic:
simp
-- Module: Mathlib.Combinatorics.SetFamily.Kleitman
Goal:
ι : Type u_1
α : Type u_2
inst : Fintype α
inst_1 : DecidableEq α
inst_2 : Nonempty α
this : DecidableEq ι
i : ι
s : Finset ι
hi : i ∉ s
ih :
  ∀ (f : ι → Finset (Finset α)) (hf : ∀ i ∈ s, (↑(f i) : Set (Finset α)).Intersecting) (hs : #s ≤ Fintype.card α),
    #(s.biUnion f) ≤ HPow.hPow (α := ℕ) 2 (Fintype.card α) - HPow.hPow (α := ℕ) 2 (Fintype.card α - #s)
f : ι → Finset (Finset α)
hf : ∀ i_1 ∈ cons i s hi, (↑(f i_1) : Set (Finset α)).Intersecting
hs : #(cons i s hi) ≤ Fintype.card α
f' : ι → Finset (Finset α) :=
  fun (j : ι) ↦
    if hj : j ∈ cons i s hi then
      Exists.choose (p := fun (t : Finset (Finset α)) ↦
        f j ⊆ t ∧ 2 * #t = Fintype.card.{u_2} (Finset α) ∧ (↑t : Set (Finset α)).Intersecting) ⋯
    else ∅
j : ι
hj : j ∈ cons i s hi
simp_rw :
  f j ⊆
      Exists.choose (p := fun (t : Finset (Finset α)) ↦
        f j ⊆ t ∧ 2 * #t = Fintype.card.{u_2} (Finset α) ∧ (↑t : Set (Finset α)).Intersecting) ⋯ ∧
    2 *
          card.{u_2} (α := Finset α)
            (Exists.choose (p := fun (t : Finset (Finset α)) ↦
              f j ⊆ t ∧ 2 * #t = Fintype.card.{u_2} (Finset α) ∧ (↑t : Set (Finset α)).Intersecting) ⋯) =
        Fintype.card.{u_2} (Finset α) ∧
      (↑(Exists.choose (p := fun (t : Finset (Finset α)) ↦
              f j ⊆ t ∧ 2 * #t = Fintype.card.{u_2} (Finset α) ∧ (↑t : Set (Finset α)).Intersecting) ⋯) :
          Set (Finset α)).Intersecting
⊢ f j ⊆ f' j ∧ 2 * #(f' j) = HPow.hPow (α := ℕ) 2 (Fintype.card α) ∧ (↑(f' j) : Set (Finset α)).Intersecting

Tactic:
simp_rw [f', dif_pos hj, ← Fintype.card_finset]

Premises used: dif_pos, Fintype.card_finset
-- Module: Mathlib.Combinatorics.SetFamily.Kleitman
Goal:
ι : Type u_1
α : Type u_2
inst : Fintype α
inst_1 : DecidableEq α
inst_2 : Nonempty α
this : DecidableEq ι
i : ι
s : Finset ι
hi : i ∉ s
ih :
  ∀ (f : ι → Finset (Finset α)) (hf : ∀ i ∈ s, (↑(f i) : Set (Finset α)).Intersecting) (hs : #s ≤ Fintype.card α),
    #(s.biUnion f) ≤ HPow.hPow (α := ℕ) 2 (Fintype.card α) - HPow.hPow (α := ℕ) 2 (Fintype.card α - #s)
f : ι → Finset (Finset α)
hf : ∀ i_1 ∈ cons i s hi, (↑(f i_1) : Set (Finset α)).Intersecting
hs : #(cons i s hi) ≤ Fintype.card α
f' : ι → Finset (Finset α) :=
  fun (j : ι) ↦
    if hj : j ∈ cons i s hi then
      Exists.choose (p := fun (t : Finset (Finset α)) ↦
        f j ⊆ t ∧ 2 * #t = Fintype.card.{u_2} (Finset α) ∧ (↑t : Set (Finset α)).Intersecting) ⋯
    else ∅
j : ι
hj : j ∈ cons i s hi
⊢ f j ⊆
      Exists.choose (p := fun (t : Finset (Finset α)) ↦
        f j ⊆ t ∧ 2 * #t = Fintype.card.{u_2} (Finset α) ∧ (↑t : Set (Finset α)).Intersecting) ⋯ ∧
    2 *
          card.{u_2} (α := Finset α)
            (Exists.choose (p := fun (t : Finset (Finset α)) ↦
              f j ⊆ t ∧ 2 * #t = Fintype.card.{u_2} (Finset α) ∧ (↑t : Set (Finset α)).Intersecting) ⋯) =
        Fintype.card.{u_2} (Finset α) ∧
      (↑(Exists.choose (p := fun (t : Finset (Finset α)) ↦
              f j ⊆ t ∧ 2 * #t = Fintype.card.{u_2} (Finset α) ∧ (↑t : Set (Finset α)).Intersecting) ⋯) :
          Set (Finset α)).Intersecting

Tactic:
Classical.choose_spec (hf j hj).exists_card_eq

Premises used: Set.Mem, setOf, Classical.choose_spec, Set.Intersecting.exists_card_eq
-- Module: Mathlib.Combinatorics.SetFamily.Kleitman
Goal:
ι : Type u_1
α : Type u_2
inst : Fintype α
inst_1 : DecidableEq α
inst_2 : Nonempty α
this : DecidableEq ι
i : ι
s : Finset ι
hi : i ∉ s
ih :
  ∀ (f : ι → Finset (Finset α)) (hf : ∀ i ∈ s, (↑(f i) : Set (Finset α)).Intersecting) (hs : #s ≤ Fintype.card α),
    #(s.biUnion f) ≤ HPow.hPow (α := ℕ) 2 (Fintype.card α) - HPow.hPow (α := ℕ) 2 (Fintype.card α - #s)
f : ι → Finset (Finset α)
hf : ∀ i_1 ∈ cons i s hi, (↑(f i_1) : Set (Finset α)).Intersecting
hs : #(cons i s hi) ≤ Fintype.card α
f' : ι → Finset (Finset α) :=
  fun (j : ι) ↦
    if hj : j ∈ cons i s hi then
      Exists.choose (p := fun (t : Finset (Finset α)) ↦
        f j ⊆ t ∧ 2 * #t = Fintype.card.{u_2} (Finset α) ∧ (↑t : Set (Finset α)).Intersecting) ⋯
    else ∅
j : ι
hj : j ∈ cons i s hi
⊢ f j ⊆
      Exists.choose (p := fun (t : Finset (Finset α)) ↦
        f j ⊆ t ∧ 2 * #t = Fintype.card.{u_2} (Finset α) ∧ (↑t : Set (Finset α)).Intersecting) ⋯ ∧
    2 *
          card.{u_2} (α := Finset α)
            (Exists.choose (p := fun (t : Finset (Finset α)) ↦
              f j ⊆ t ∧ 2 * #t = Fintype.card.{u_2} (Finset α) ∧ (↑t : Set (Finset α)).Intersecting) ⋯) =
        Fintype.card.{u_2} (Finset α) ∧
      (↑(Exists.choose (p := fun (t : Finset (Finset α)) ↦
              f j ⊆ t ∧ 2 * #t = Fintype.card.{u_2} (Finset α) ∧ (↑t : Set (Finset α)).Intersecting) ⋯) :
          Set (Finset α)).Intersecting

Tactic:
exact Classical.choose_spec (hf j hj).exists_card_eq

Premises used: Classical.choose_spec, Set.Intersecting.exists_card_eq
-- Module: Mathlib.Combinatorics.SetFamily.Kleitman
Goal:
ι : Type u_1
α : Type u_2
inst : Fintype α
inst_1 : DecidableEq α
inst_2 : Nonempty α
this : DecidableEq ι
i : ι
s : Finset ι
hi : i ∉ s
ih :
  ∀ (f : ι → Finset (Finset α)) (hf : ∀ i ∈ s, (↑(f i) : Set (Finset α)).Intersecting) (hs : #s ≤ Fintype.card α),
    #(s.biUnion f) ≤ HPow.hPow (α := ℕ) 2 (Fintype.card α) - HPow.hPow (α := ℕ) 2 (Fintype.card α - #s)
f : ι → Finset (Finset α)
hf : ∀ i_1 ∈ cons i s hi, (↑(f i_1) : Set (Finset α)).Intersecting
hs : #(cons i s hi) ≤ Fintype.card α
f' : ι → Finset (Finset α) :=
  fun (j : ι) ↦
    if hj : j ∈ cons i s hi then
      Exists.choose (p := fun (t : Finset (Finset α)) ↦
        f j ⊆ t ∧ 2 * #t = Fintype.card.{u_2} (Finset α) ∧ (↑t : Set (Finset α)).Intersecting) ⋯
    else ∅
⊢ ∀ j ∈ cons i s hi,
    f j ⊆ f' j ∧ 2 * #(f' j) = HPow.hPow (α := ℕ) 2 (Fintype.card α) ∧ (↑(f' j) : Set (Finset α)).Intersecting

Tactic:
have hf₁ : ∀ j, j ∈ cons i s hi → f j ⊆ f' j ∧ 2 * #(f' j) =
      2 ^ Fintype.card α ∧ (f' j : Set (Finset α)).Intersecting := by
    rintro j hj
    simp_rw [f', dif_pos hj, ← Fintype.card_finset]
    exact Classical.choose_spec (hf j hj).exists_card_eq
-- Module: Mathlib.Combinatorics.SetFamily.Kleitman
Goal:
ι : Type u_1
α : Type u_2
inst : Fintype α
inst_1 : DecidableEq α
inst_2 : Nonempty α
this : DecidableEq ι
i : ι
s : Finset ι
hi : i ∉ s
ih :
  ∀ (f : ι → Finset (Finset α)) (hf : ∀ i ∈ s, (↑(f i) : Set (Finset α)).Intersecting) (hs : #s ≤ Fintype.card α),
    #(s.biUnion f) ≤ HPow.hPow (α := ℕ) 2 (Fintype.card α) - HPow.hPow (α := ℕ) 2 (Fintype.card α - #s)
f : ι → Finset (Finset α)
hf : ∀ i_1 ∈ cons i s hi, (↑(f i_1) : Set (Finset α)).Intersecting
hs : #(cons i s hi) ≤ Fintype.card α
f' : ι → Finset (Finset α) :=
  fun (j : ι) ↦
    if hj : j ∈ cons i s hi then
      Exists.choose (p := fun (t : Finset (Finset α)) ↦
        f j ⊆ t ∧ 2 * #t = Fintype.card.{u_2} (Finset α) ∧ (↑t : Set (Finset α)).Intersecting) ⋯
    else ∅
hf₁ :
  ∀ j ∈ cons i s hi,
    f j ⊆ f' j ∧ 2 * #(f' j) = HPow.hPow (α := ℕ) 2 (Fintype.card α) ∧ (↑(f' j) : Set (Finset α)).Intersecting
⊢ ∀ j ∈ cons i s hi, IsUpperSet (↑(f' j) : Set (Finset α))

Tactic:
fun j hj ↦ (hf₁ _ hj).2.2.isUpperSet' ((hf₁ _ hj).2.2.is_max_iff_card_eq.2 ?_)

Premises used: Iff.mpr, Set.Intersecting.isUpperSet', Set.Intersecting.is_max_iff_card_eq, And.right
-- Module: Mathlib.Combinatorics.SetFamily.Kleitman
Goal:
ι : Type u_1
α : Type u_2
inst : Fintype α
inst_1 : DecidableEq α
inst_2 : Nonempty α
this : DecidableEq ι
i : ι
s : Finset ι
hi : i ∉ s
ih :
  ∀ (f : ι → Finset (Finset α)) (hf : ∀ i ∈ s, (↑(f i) : Set (Finset α)).Intersecting) (hs : #s ≤ Fintype.card α),
    #(s.biUnion f) ≤ HPow.hPow (α := ℕ) 2 (Fintype.card α) - HPow.hPow (α := ℕ) 2 (Fintype.card α - #s)
f : ι → Finset (Finset α)
hf : ∀ i_1 ∈ cons i s hi, (↑(f i_1) : Set (Finset α)).Intersecting
hs : #(cons i s hi) ≤ Fintype.card α
f' : ι → Finset (Finset α) :=
  fun (j : ι) ↦
    if hj : j ∈ cons i s hi then
      Exists.choose (p := fun (t : Finset (Finset α)) ↦
        f j ⊆ t ∧ 2 * #t = Fintype.card.{u_2} (Finset α) ∧ (↑t : Set (Finset α)).Intersecting) ⋯
    else ∅
hf₁ :
  ∀ j ∈ cons i s hi,
    f j ⊆ f' j ∧ 2 * #(f' j) = HPow.hPow (α := ℕ) 2 (Fintype.card α) ∧ (↑(f' j) : Set (Finset α)).Intersecting
refine : ∀ (j : ι) (hj : j ∈ cons i s hi), 2 * #(f' j) = Fintype.card.{u_2} (Finset α)
⊢ ∀ j ∈ cons i s hi, IsUpperSet (↑(f' j) : Set (Finset α))

Tactic:
refine fun j hj ↦ (hf₁ _ hj).2.2.isUpperSet' ((hf₁ _ hj).2.2.is_max_iff_card_eq.2 ?_)

Premises used: Iff.mpr, Set.Intersecting.isUpperSet', Set.Intersecting.is_max_iff_card_eq, And.right
-- Module: Mathlib.Combinatorics.SetFamily.Kleitman
Goal:
ι : Type u_1
α : Type u_2
inst : Fintype α
inst_1 : DecidableEq α
inst_2 : Nonempty α
this : DecidableEq ι
i : ι
s : Finset ι
hi : i ∉ s
ih :
  ∀ (f : ι → Finset (Finset α)) (hf : ∀ i ∈ s, (↑(f i) : Set (Finset α)).Intersecting) (hs : #s ≤ Fintype.card α),
    #(s.biUnion f) ≤ HPow.hPow (α := ℕ) 2 (Fintype.card α) - HPow.hPow (α := ℕ) 2 (Fintype.card α - #s)
f : ι → Finset (Finset α)
hf : ∀ i_1 ∈ cons i s hi, (↑(f i_1) : Set (Finset α)).Intersecting
hs : #(cons i s hi) ≤ Fintype.card α
f' : ι → Finset (Finset α) :=
  fun (j : ι) ↦
    if hj : j ∈ cons i s hi then
      Exists.choose (p := fun (t : Finset (Finset α)) ↦
        f j ⊆ t ∧ 2 * #t = Fintype.card.{u_2} (Finset α) ∧ (↑t : Set (Finset α)).Intersecting) ⋯
    else ∅
hf₁ :
  ∀ j ∈ cons i s hi,
    f j ⊆ f' j ∧ 2 * #(f' j) = HPow.hPow (α := ℕ) 2 (Fintype.card α) ∧ (↑(f' j) : Set (Finset α)).Intersecting
j : ι
hj : j ∈ cons i s hi
rw : 2 * #(f' j) = HPow.hPow (α := ℕ) 2 (Fintype.card α)
⊢ 2 * #(f' j) = Fintype.card.{u_2} (Finset α)

Tactic:
rw [Fintype.card_finset]

Premises used: Fintype.card_finset
-- Module: Mathlib.Combinatorics.SetFamily.Kleitman
Goal:
ι : Type u_1
α : Type u_2
inst : Fintype α
inst_1 : DecidableEq α
inst_2 : Nonempty α
this : DecidableEq ι
i : ι
s : Finset ι
hi : i ∉ s
ih :
  ∀ (f : ι → Finset (Finset α)) (hf : ∀ i ∈ s, (↑(f i) : Set (Finset α)).Intersecting) (hs : #s ≤ Fintype.card α),
    #(s.biUnion f) ≤ HPow.hPow (α := ℕ) 2 (Fintype.card α) - HPow.hPow (α := ℕ) 2 (Fintype.card α - #s)
f : ι → Finset (Finset α)
hf : ∀ i_1 ∈ cons i s hi, (↑(f i_1) : Set (Finset α)).Intersecting
hs : #(cons i s hi) ≤ Fintype.card α
f' : ι → Finset (Finset α) :=
  fun (j : ι) ↦
    if hj : j ∈ cons i s hi then
      Exists.choose (p := fun (t : Finset (Finset α)) ↦
        f j ⊆ t ∧ 2 * #t = Fintype.card.{u_2} (Finset α) ∧ (↑t : Set (Finset α)).Intersecting) ⋯
    else ∅
hf₁ :
  ∀ j ∈ cons i s hi,
    f j ⊆ f' j ∧ 2 * #(f' j) = HPow.hPow (α := ℕ) 2 (Fintype.card α) ∧ (↑(f' j) : Set (Finset α)).Intersecting
j : ι
hj : j ∈ cons i s hi
⊢ 2 * #(f' j) = HPow.hPow (α := ℕ) 2 (Fintype.card α)

Tactic:
(hf₁ _ hj).2.1

Premises used: And.right, And.left
-- Module: Mathlib.Combinatorics.SetFamily.Kleitman
Goal:
ι : Type u_1
α : Type u_2
inst : Fintype α
inst_1 : DecidableEq α
inst_2 : Nonempty α
this : DecidableEq ι
i : ι
s : Finset ι
hi : i ∉ s
ih :
  ∀ (f : ι → Finset (Finset α)) (hf : ∀ i ∈ s, (↑(f i) : Set (Finset α)).Intersecting) (hs : #s ≤ Fintype.card α),
    #(s.biUnion f) ≤ HPow.hPow (α := ℕ) 2 (Fintype.card α) - HPow.hPow (α := ℕ) 2 (Fintype.card α - #s)
f : ι → Finset (Finset α)
hf : ∀ i_1 ∈ cons i s hi, (↑(f i_1) : Set (Finset α)).Intersecting
hs : #(cons i s hi) ≤ Fintype.card α
f' : ι → Finset (Finset α) :=
  fun (j : ι) ↦
    if hj : j ∈ cons i s hi then
      Exists.choose (p := fun (t : Finset (Finset α)) ↦
        f j ⊆ t ∧ 2 * #t = Fintype.card.{u_2} (Finset α) ∧ (↑t : Set (Finset α)).Intersecting) ⋯
    else ∅
hf₁ :
  ∀ j ∈ cons i s hi,
    f j ⊆ f' j ∧ 2 * #(f' j) = HPow.hPow (α := ℕ) 2 (Fintype.card α) ∧ (↑(f' j) : Set (Finset α)).Intersecting
j : ι
hj : j ∈ cons i s hi
⊢ 2 * #(f' j) = HPow.hPow (α := ℕ) 2 (Fintype.card α)

Tactic:
exact (hf₁ _ hj).2.1

Premises used: And.right, And.left
-- Module: Mathlib.Combinatorics.SetFamily.Kleitman
Goal:
ι : Type u_1
α : Type u_2
inst : Fintype α
inst_1 : DecidableEq α
inst_2 : Nonempty α
this : DecidableEq ι
i : ι
s : Finset ι
hi : i ∉ s
ih :
  ∀ (f : ι → Finset (Finset α)) (hf : ∀ i ∈ s, (↑(f i) : Set (Finset α)).Intersecting) (hs : #s ≤ Fintype.card α),
    #(s.biUnion f) ≤ HPow.hPow (α := ℕ) 2 (Fintype.card α) - HPow.hPow (α := ℕ) 2 (Fintype.card α - #s)
f : ι → Finset (Finset α)
hf : ∀ i_1 ∈ cons i s hi, (↑(f i_1) : Set (Finset α)).Intersecting
hs : #(cons i s hi) ≤ Fintype.card α
f' : ι → Finset (Finset α) :=
  fun (j : ι) ↦
    if hj : j ∈ cons i s hi then
      Exists.choose (p := fun (t : Finset (Finset α)) ↦
        f j ⊆ t ∧ 2 * #t = Fintype.card.{u_2} (Finset α) ∧ (↑t : Set (Finset α)).Intersecting) ⋯
    else ∅
hf₁ :
  ∀ j ∈ cons i s hi,
    f j ⊆ f' j ∧ 2 * #(f' j) = HPow.hPow (α := ℕ) 2 (Fintype.card α) ∧ (↑(f' j) : Set (Finset α)).Intersecting
⊢ ∀ j ∈ cons i s hi, IsUpperSet (↑(f' j) : Set (Finset α))

Tactic:
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
-- Module: Mathlib.Combinatorics.SetFamily.Kleitman
Goal:
ι : Type u_1
α : Type u_2
inst : Fintype α
inst_1 : DecidableEq α
inst_2 : Nonempty α
this : DecidableEq ι
i : ι
s : Finset ι
hi : i ∉ s
ih :
  ∀ (f : ι → Finset (Finset α)) (hf : ∀ i ∈ s, (↑(f i) : Set (Finset α)).Intersecting) (hs : #s ≤ Fintype.card α),
    #(s.biUnion f) ≤ HPow.hPow (α := ℕ) 2 (Fintype.card α) - HPow.hPow (α := ℕ) 2 (Fintype.card α - #s)
f : ι → Finset (Finset α)
hf : ∀ i_1 ∈ cons i s hi, (↑(f i_1) : Set (Finset α)).Intersecting
hs : #(cons i s hi) ≤ Fintype.card α
f' : ι → Finset (Finset α) :=
  fun (j : ι) ↦
    if hj : j ∈ cons i s hi then
      Exists.choose (p := fun (t : Finset (Finset α)) ↦
        f j ⊆ t ∧ 2 * #t = Fintype.card.{u_2} (Finset α) ∧ (↑t : Set (Finset α)).Intersecting) ⋯
    else ∅
hf₁ :
  ∀ j ∈ cons i s hi,
    f j ⊆ f' j ∧ 2 * #(f' j) = HPow.hPow (α := ℕ) 2 (Fintype.card α) ∧ (↑(f' j) : Set (Finset α)).Intersecting
hf₂ : ∀ j ∈ cons i s hi, IsUpperSet (↑(f' j) : Set (Finset α))
⊢ #((cons i s hi).biUnion f) ≤
    HPow.hPow (α := ℕ) 2 (Fintype.card α) - HPow.hPow (α := ℕ) 2 (Fintype.card α - #(cons i s hi))

Tactic:
(card_le_card <| biUnion_mono fun j hj ↦ (hf₁ _ hj).1).trans ?_

Premises used: Finset.biUnion_mono, Finset.card_le_card, And.left, LE.le.trans