awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Kleitman (hypothesis)
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 ∅
⊢ #((cons i s hi).biUnion f) ≤
    HPow.hPow (α := ℕ) 2 (Fintype.card α) - HPow.hPow (α := ℕ) 2 (Fintype.card α - #(cons i s hi))
have hf₁ : ∀ 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
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Kleitman (goal)
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 α))
have refine : ∀ (j : ι) (hj : j ∈ cons i s hi), 2 * #(f' j) = Fintype.card.{u_2} (Finset α)
Tactic: refine fun j hj ↦ (hf₁ _ hj).2.2.isUpperSet' ((hf₁ _ hj).2.2.is_max_iff_card_eq.2 ?_)
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Kleitman (goal)
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) = Fintype.card.{u_2} (Finset α)
have rw : 2 * #(f' j) = HPow.hPow (α := ℕ) 2 (Fintype.card α)
Tactic: rw [Fintype.card_finset]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Kleitman (hypothesis)
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
⊢ #((cons i s hi).biUnion f) ≤
    HPow.hPow (α := ℕ) 2 (Fintype.card α) - HPow.hPow (α := ℕ) 2 (Fintype.card α - #(cons i s hi))
have hf₂ : ∀ 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
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Kleitman (goal)
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))
have inr : #((cons i s hi).biUnion f') ≤
  HPow.hPow (α := ℕ) 2 (Fintype.card α) - HPow.hPow (α := ℕ) 2 (Fintype.card α - #(cons i s hi))
Tactic: refine (card_le_card <| biUnion_mono fun j hj ↦ (hf₁ _ hj).1).trans ?_
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Kleitman (goal)
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))
have inr : #((insert i s).biUnion f') ≤
  HPow.hPow (α := ℕ) 2 (Fintype.card α) - HPow.hPow (α := ℕ) 2 (Fintype.card α - #(cons i s hi))
Tactic: nth_rw 1 [cons_eq_insert i]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Kleitman (goal)
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 α))
⊢ #((insert i s).biUnion f') ≤
    HPow.hPow (α := ℕ) 2 (Fintype.card α) - HPow.hPow (α := ℕ) 2 (Fintype.card α - #(cons i s hi))
have inr : #(f' i ∪ s.biUnion f') ≤ HPow.hPow (α := ℕ) 2 (Fintype.card α) - HPow.hPow (α := ℕ) 2 (Fintype.card α - #(cons i s hi))
Tactic: rw [biUnion_insert]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Kleitman (goal)
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 α))
⊢ #(f' i ∪ s.biUnion f') ≤
    HPow.hPow (α := ℕ) 2 (Fintype.card α) - HPow.hPow (α := ℕ) 2 (Fintype.card α - #(cons i s hi))
have inr : #(f' i) + #((f' i ∪ s.biUnion f') \ f' i) ≤
  HPow.hPow (α := ℕ) 2 (Fintype.card α) - HPow.hPow (α := ℕ) 2 (Fintype.card α - #(cons i s hi))
Tactic: refine (card_mono <| @le_sup_sdiff _ _ _ <| f' i).trans ((card_union_le _ _).trans ?_)
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Kleitman (goal)
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 α))
⊢ #(f' i) + #((f' i ∪ s.biUnion f') \ f' i) ≤
    HPow.hPow (α := ℕ) 2 (Fintype.card α) - HPow.hPow (α := ℕ) 2 (Fintype.card α - #(cons i s hi))
have inr : #(f' i) + #(s.biUnion f' ∩ (f' i)ᶜ) ≤
  HPow.hPow (α := ℕ) 2 (Fintype.card α) - HPow.hPow (α := ℕ) 2 (Fintype.card α - #(cons i s hi))
Tactic: rw [union_sdiff_left, sdiff_eq_inter_compl]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Kleitman (goal)
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 α))
⊢ #(f' i) + #(s.biUnion f' ∩ (f' i)ᶜ) ≤
    HPow.hPow (α := ℕ) 2 (Fintype.card α) - HPow.hPow (α := ℕ) 2 (Fintype.card α - #(cons i s hi))
have inr : HPow.hPow (α := ℕ) 2 (Fintype.card α + 1) * (#(f' i) + #(s.biUnion f' ∩ (f' i)ᶜ)) ≤
  HPow.hPow (α := ℕ) 2 (Fintype.card α + 1) *
    (HPow.hPow (α := ℕ) 2 (Fintype.card α) - HPow.hPow (α := ℕ) 2 (Fintype.card α - #(cons i s hi)))
Tactic: refine le_of_mul_le_mul_left ?_ (pow_pos (zero_lt_two' ℕ) <| Fintype.card α + 1)
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Kleitman (goal)
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 α))
⊢ HPow.hPow (α := ℕ) 2 (Fintype.card α + 1) * (#(f' i) + #(s.biUnion f' ∩ (f' i)ᶜ)) ≤
    HPow.hPow (α := ℕ) 2 (Fintype.card α + 1) *
      (HPow.hPow (α := ℕ) 2 (Fintype.card α) - HPow.hPow (α := ℕ) 2 (Fintype.card α - #(cons i s hi)))
have inr : HPow.hPow (α := ℕ) 2 (Fintype.card α) * (2 * #(f' i)) +
    2 * (HPow.hPow (α := ℕ) 2 (Fintype.card α) * #(s.biUnion f' ∩ (f' i)ᶜ)) ≤
  2 * HPow.hPow (α := ℕ) 2 (Fintype.card α) *
    (HPow.hPow (α := ℕ) 2 (Fintype.card α) - HPow.hPow (α := ℕ) 2 (Fintype.card α - #(cons i s hi)))
Tactic: rw [pow_succ, mul_add, mul_assoc, mul_comm _ 2, mul_assoc]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Kleitman (goal)
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 α))
⊢ HPow.hPow (α := ℕ) 2 (Fintype.card α) * (2 * #(f' i)) +
      2 * (HPow.hPow (α := ℕ) 2 (Fintype.card α) * #(s.biUnion f' ∩ (f' i)ᶜ)) ≤
    2 * HPow.hPow (α := ℕ) 2 (Fintype.card α) *
      (HPow.hPow (α := ℕ) 2 (Fintype.card α) - HPow.hPow (α := ℕ) 2 (Fintype.card α - #(cons i s hi)))
have inr : IsUpperSet (↑(s.biUnion f') : Set (Finset α))
Tactic: refine (add_le_add
      ((mul_le_mul_iff_right₀ <| pow_pos (zero_lt_two' ℕ) _).2
      (hf₁ _ <| mem_cons_self _ _).2.2.card_le) <|
      (mul_le_mul_iff_right₀ <| zero_lt_two' ℕ).2 <| IsUpperSet.card_inter_le_finset ?_ ?_).trans ?_
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Kleitman (goal)
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 α))
inr : IsUpperSet (↑(s.biUnion f') : Set (Finset α))
⊢ HPow.hPow (α := ℕ) 2 (Fintype.card α) * (2 * #(f' i)) +
      2 * (HPow.hPow (α := ℕ) 2 (Fintype.card α) * #(s.biUnion f' ∩ (f' i)ᶜ)) ≤
    2 * HPow.hPow (α := ℕ) 2 (Fintype.card α) *
      (HPow.hPow (α := ℕ) 2 (Fintype.card α) - HPow.hPow (α := ℕ) 2 (Fintype.card α - #(cons i s hi)))
have inr₁ : IsLowerSet (↑(f' i)ᶜ : Set (Finset α))
Tactic: refine (add_le_add
      ((mul_le_mul_iff_right₀ <| pow_pos (zero_lt_two' ℕ) _).2
      (hf₁ _ <| mem_cons_self _ _).2.2.card_le) <|
      (mul_le_mul_iff_right₀ <| zero_lt_two' ℕ).2 <| IsUpperSet.card_inter_le_finset ?_ ?_).trans ?_
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Kleitman (goal)
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 α))
inr : IsUpperSet (↑(s.biUnion f') : Set (Finset α))
inr₁ : IsLowerSet (↑(f' i)ᶜ : Set (Finset α))
⊢ HPow.hPow (α := ℕ) 2 (Fintype.card α) * (2 * #(f' i)) +
      2 * (HPow.hPow (α := ℕ) 2 (Fintype.card α) * #(s.biUnion f' ∩ (f' i)ᶜ)) ≤
    2 * HPow.hPow (α := ℕ) 2 (Fintype.card α) *
      (HPow.hPow (α := ℕ) 2 (Fintype.card α) - HPow.hPow (α := ℕ) 2 (Fintype.card α - #(cons i s hi)))
have inr₂ : HPow.hPow (α := ℕ) 2 (Fintype.card α) * Fintype.card.{u_2} (Finset α) + 2 * (#(s.biUnion f') * #(f' i)ᶜ) ≤
  2 * HPow.hPow (α := ℕ) 2 (Fintype.card α) *
    (HPow.hPow (α := ℕ) 2 (Fintype.card α) - HPow.hPow (α := ℕ) 2 (Fintype.card α - #(cons i s hi)))
Tactic: refine (add_le_add
      ((mul_le_mul_iff_right₀ <| pow_pos (zero_lt_two' ℕ) _).2
      (hf₁ _ <| mem_cons_self _ _).2.2.card_le) <|
      (mul_le_mul_iff_right₀ <| zero_lt_two' ℕ).2 <| IsUpperSet.card_inter_le_finset ?_ ?_).trans ?_
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Kleitman (goal)
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 α))
⊢ IsUpperSet (↑(s.biUnion f') : Set (Finset α))
have inr : IsUpperSet.{u_2} (α := Finset α) (⋃ x ∈ (↑s : Set ι), (↑(f' x) : Set (Finset α)))
Tactic: rw [coe_biUnion]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Kleitman (goal)
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 α))
⊢ IsLowerSet (↑(f' i)ᶜ : Set (Finset α))
have inr : IsLowerSet (↑(f' i) : Set (Finset α))ᶜ
Tactic: rw [coe_compl]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Kleitman (goal)
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 α))
⊢ HPow.hPow (α := ℕ) 2 (Fintype.card α) * Fintype.card.{u_2} (Finset α) + 2 * (#(s.biUnion f') * #(f' i)ᶜ) ≤
    2 * HPow.hPow (α := ℕ) 2 (Fintype.card α) *
      (HPow.hPow (α := ℕ) 2 (Fintype.card α) - HPow.hPow (α := ℕ) 2 (Fintype.card α - #(cons i s hi)))
have inr : HPow.hPow (α := ℕ) 2 (Fintype.card α) * (HPow.hPow (α := ℕ) 2 (Fintype.card α) + #(s.biUnion f')) ≤
  HPow.hPow (α := ℕ) 2 (Fintype.card α) *
    (2 * (HPow.hPow (α := ℕ) 2 (Fintype.card α) - HPow.hPow (α := ℕ) 2 (Fintype.card α - #(cons i s hi))))
Tactic: rw [mul_tsub, card_compl, Fintype.card_finset, mul_left_comm, mul_tsub,
    (hf₁ _ <| mem_cons_self _ _).2.1, two_mul, add_tsub_cancel_left, ← mul_tsub, ← mul_two,
    mul_assoc, ← add_mul, mul_comm]