awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 α) * (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))))
have inr : HPow.hPow (α := ℕ) 2 (Fintype.card α) + #(s.biUnion f') ≤
  2 * (HPow.hPow (α := ℕ) 2 (Fintype.card α) - HPow.hPow (α := ℕ) 2 (Fintype.card α - #(cons i s hi)))
Tactic: gcongr
-- 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 α) + #(s.biUnion f') ≤
    2 * (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 α) - HPow.hPow (α := ℕ) 2 (Fintype.card α - #s)) ≤
  2 * (HPow.hPow (α := ℕ) 2 (Fintype.card α) - HPow.hPow (α := ℕ) 2 (Fintype.card α - #(cons i s hi)))
Tactic: refine (add_le_add_right
    (ih _ (fun i hi ↦ (hf₁ _ <| subset_cons _ hi).2.2)
    ((card_le_card <| subset_cons _).trans hs)) _).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 α))
⊢ HPow.hPow (α := ℕ) 2 (Fintype.card α) +
      (HPow.hPow (α := ℕ) 2 (Fintype.card α) - HPow.hPow (α := ℕ) 2 (Fintype.card α - #s)) ≤
    2 * (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 α) - HPow.hPow (α := ℕ) 2 (Fintype.card α - #s)) ≤
  2 * HPow.hPow (α := ℕ) 2 (Fintype.card α) - 2 * HPow.hPow (α := ℕ) 2 (Fintype.card α - #(cons i s hi))
Tactic: rw [mul_tsub, two_mul, ← pow_succ',
    ← add_tsub_assoc_of_le (pow_right_mono₀ (one_le_two : (1 : ℕ) ≤ 2) tsub_le_self),
    tsub_add_eq_add_tsub hs, card_cons, add_tsub_add_eq_tsub_right]
-- 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 :
  HPow.hPow (α := ℕ) 2 (Fintype.card α) +
      (HPow.hPow (α := ℕ) 2 (Fintype.card α) - HPow.hPow (α := ℕ) 2 (Fintype.card α - #s)) ≤
    2 * HPow.hPow (α := ℕ) 2 (Fintype.card α) - 2 * HPow.hPow (α := ℕ) 2 (Fintype.card α - #(cons i s hi))
⊢ HPow.hPow (α := ℕ) 2 (Fintype.card α) +
      (HPow.hPow (α := ℕ) 2 (Fintype.card α) - HPow.hPow (α := ℕ) 2 (Fintype.card α - #s)) ≤
    2 * (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 α) - HPow.hPow (α := ℕ) 2 (Fintype.card α - #s)) ≤
  HPow.hPow (α := ℕ) 2 (Fintype.card α) + HPow.hPow (α := ℕ) 2 (Fintype.card α) -
    2 * HPow.hPow (α := ℕ) 2 (Fintype.card α - #(cons i s hi))
Tactic: rw [mul_tsub, two_mul, ← pow_succ',
    ← add_tsub_assoc_of_le (pow_right_mono₀ (one_le_two : (1 : ℕ) ≤ 2) tsub_le_self),
    tsub_add_eq_add_tsub hs, card_cons, add_tsub_add_eq_tsub_right]
-- 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 :
  HPow.hPow (α := ℕ) 2 (Fintype.card α) +
      (HPow.hPow (α := ℕ) 2 (Fintype.card α) - HPow.hPow (α := ℕ) 2 (Fintype.card α - #s)) ≤
    2 * HPow.hPow (α := ℕ) 2 (Fintype.card α) - 2 * HPow.hPow (α := ℕ) 2 (Fintype.card α - #(cons i s hi))
inr₁ :
  HPow.hPow (α := ℕ) 2 (Fintype.card α) +
      (HPow.hPow (α := ℕ) 2 (Fintype.card α) - HPow.hPow (α := ℕ) 2 (Fintype.card α - #s)) ≤
    HPow.hPow (α := ℕ) 2 (Fintype.card α) + HPow.hPow (α := ℕ) 2 (Fintype.card α) -
      2 * HPow.hPow (α := ℕ) 2 (Fintype.card α - #(cons i s hi))
⊢ HPow.hPow (α := ℕ) 2 (Fintype.card α) +
      (HPow.hPow (α := ℕ) 2 (Fintype.card α) - HPow.hPow (α := ℕ) 2 (Fintype.card α - #s)) ≤
    2 * (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 α) - HPow.hPow (α := ℕ) 2 (Fintype.card α - #s)) ≤
  HPow.hPow (α := ℕ) 2 (Fintype.card α) + HPow.hPow (α := ℕ) 2 (Fintype.card α) -
    HPow.hPow (α := ℕ) 2 (Fintype.card α - #(cons i s hi) + 1)
Tactic: rw [mul_tsub, two_mul, ← pow_succ',
    ← add_tsub_assoc_of_le (pow_right_mono₀ (one_le_two : (1 : ℕ) ≤ 2) tsub_le_self),
    tsub_add_eq_add_tsub hs, card_cons, add_tsub_add_eq_tsub_right]
-- 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 :
  HPow.hPow (α := ℕ) 2 (Fintype.card α) +
      (HPow.hPow (α := ℕ) 2 (Fintype.card α) - HPow.hPow (α := ℕ) 2 (Fintype.card α - #s)) ≤
    2 * HPow.hPow (α := ℕ) 2 (Fintype.card α) - 2 * HPow.hPow (α := ℕ) 2 (Fintype.card α - #(cons i s hi))
inr₁ :
  HPow.hPow (α := ℕ) 2 (Fintype.card α) +
      (HPow.hPow (α := ℕ) 2 (Fintype.card α) - HPow.hPow (α := ℕ) 2 (Fintype.card α - #s)) ≤
    HPow.hPow (α := ℕ) 2 (Fintype.card α) + HPow.hPow (α := ℕ) 2 (Fintype.card α) -
      2 * HPow.hPow (α := ℕ) 2 (Fintype.card α - #(cons i s hi))
inr₂ :
  HPow.hPow (α := ℕ) 2 (Fintype.card α) +
      (HPow.hPow (α := ℕ) 2 (Fintype.card α) - HPow.hPow (α := ℕ) 2 (Fintype.card α - #s)) ≤
    HPow.hPow (α := ℕ) 2 (Fintype.card α) + HPow.hPow (α := ℕ) 2 (Fintype.card α) -
      HPow.hPow (α := ℕ) 2 (Fintype.card α - #(cons i s hi) + 1)
⊢ HPow.hPow (α := ℕ) 2 (Fintype.card α) +
      (HPow.hPow (α := ℕ) 2 (Fintype.card α) - HPow.hPow (α := ℕ) 2 (Fintype.card α - #s)) ≤
    2 * (HPow.hPow (α := ℕ) 2 (Fintype.card α) - HPow.hPow (α := ℕ) 2 (Fintype.card α - #(cons i s hi)))
have inr₃ : HPow.hPow (α := ℕ) 2 (Fintype.card α) + (fun (x : ℕ) ↦ HPow.hPow (α := ℕ) 2 x) (Fintype.card α) -
    (fun (x : ℕ) ↦ HPow.hPow (α := ℕ) 2 x) (Fintype.card α - #s) ≤
  HPow.hPow (α := ℕ) 2 (Fintype.card α) + HPow.hPow (α := ℕ) 2 (Fintype.card α) -
    HPow.hPow (α := ℕ) 2 (Fintype.card α - #(cons i s hi) + 1)
Tactic: rw [mul_tsub, two_mul, ← pow_succ',
    ← add_tsub_assoc_of_le (pow_right_mono₀ (one_le_two : (1 : ℕ) ≤ 2) tsub_le_self),
    tsub_add_eq_add_tsub hs, card_cons, add_tsub_add_eq_tsub_right]
-- 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 :
  HPow.hPow (α := ℕ) 2 (Fintype.card α) +
      (HPow.hPow (α := ℕ) 2 (Fintype.card α) - HPow.hPow (α := ℕ) 2 (Fintype.card α - #s)) ≤
    2 * HPow.hPow (α := ℕ) 2 (Fintype.card α) - 2 * HPow.hPow (α := ℕ) 2 (Fintype.card α - #(cons i s hi))
inr₁ :
  HPow.hPow (α := ℕ) 2 (Fintype.card α) +
      (HPow.hPow (α := ℕ) 2 (Fintype.card α) - HPow.hPow (α := ℕ) 2 (Fintype.card α - #s)) ≤
    HPow.hPow (α := ℕ) 2 (Fintype.card α) + HPow.hPow (α := ℕ) 2 (Fintype.card α) -
      2 * HPow.hPow (α := ℕ) 2 (Fintype.card α - #(cons i s hi))
inr₂ :
  HPow.hPow (α := ℕ) 2 (Fintype.card α) +
      (HPow.hPow (α := ℕ) 2 (Fintype.card α) - HPow.hPow (α := ℕ) 2 (Fintype.card α - #s)) ≤
    HPow.hPow (α := ℕ) 2 (Fintype.card α) + HPow.hPow (α := ℕ) 2 (Fintype.card α) -
      HPow.hPow (α := ℕ) 2 (Fintype.card α - #(cons i s hi) + 1)
inr₃ :
  HPow.hPow (α := ℕ) 2 (Fintype.card α) + (fun (x : ℕ) ↦ HPow.hPow (α := ℕ) 2 x) (Fintype.card α) -
      (fun (x : ℕ) ↦ HPow.hPow (α := ℕ) 2 x) (Fintype.card α - #s) ≤
    HPow.hPow (α := ℕ) 2 (Fintype.card α) + HPow.hPow (α := ℕ) 2 (Fintype.card α) -
      HPow.hPow (α := ℕ) 2 (Fintype.card α - #(cons i s hi) + 1)
⊢ HPow.hPow (α := ℕ) 2 (Fintype.card α) +
      (HPow.hPow (α := ℕ) 2 (Fintype.card α) - HPow.hPow (α := ℕ) 2 (Fintype.card α - #s)) ≤
    2 * (HPow.hPow (α := ℕ) 2 (Fintype.card α) - HPow.hPow (α := ℕ) 2 (Fintype.card α - #(cons i s hi)))
have inr₄ : HPow.hPow (α := ℕ) 2 (Fintype.card α) + (fun (x : ℕ) ↦ HPow.hPow (α := ℕ) 2 x) (Fintype.card α) -
    (fun (x : ℕ) ↦ HPow.hPow (α := ℕ) 2 x) (Fintype.card α - #s) ≤
  HPow.hPow (α := ℕ) 2 (Fintype.card α) + HPow.hPow (α := ℕ) 2 (Fintype.card α) -
    HPow.hPow (α := ℕ) 2 (Fintype.card α + 1 - #(cons i s hi))
Tactic: rw [mul_tsub, two_mul, ← pow_succ',
    ← add_tsub_assoc_of_le (pow_right_mono₀ (one_le_two : (1 : ℕ) ≤ 2) tsub_le_self),
    tsub_add_eq_add_tsub hs, card_cons, add_tsub_add_eq_tsub_right]
-- 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 α
s : Finset ι
f : ι → Finset (Finset α)
hf : ∀ i ∈ s, (↑(f i) : Set (Finset α)).Intersecting
this : DecidableEq ι
hs : #s ≤ Fintype.card α
⊢ #(s.biUnion f) ≤ HPow.hPow (α := ℕ) 2 (Fintype.card α) - HPow.hPow (α := ℕ) 2 (Fintype.card α - #s)
have inr : ∀ (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: induction s using Finset.cons_induction generalizing f with
  | empty => simp
  | cons i s hi ih =>
  set f' : ι → Finset (Finset α) :=
    fun j ↦ if hj : j ∈ cons i s hi then (hf j hj).exists_card_eq.choose else ∅
  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
  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
  refine (card_le_card <| biUnion_mono fun j hj ↦ (hf₁ _ hj).1).trans ?_
  nth_rw 1 [cons_eq_insert i]
  rw [biUnion_insert]
  refine (card_mono <| @le_sup_sdiff _ _ _ <| f' i).trans ((card_union_le _ _).trans ?_)
  rw [union_sdiff_left, sdiff_eq_inter_compl]
  refine le_of_mul_le_mul_left ?_ (pow_pos (zero_lt_two' ℕ) <| Fintype.card α + 1)
  rw [pow_succ, mul_add, mul_assoc, mul_comm _ 2, mul_assoc]
  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 ?_
  · rw [coe_biUnion]
    exact isUpperSet_iUnion₂ fun i hi ↦ hf₂ _ <| subset_cons _ hi
  · rw [coe_compl]
    exact (hf₂ _ <| mem_cons_self _ _).compl
  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]
  gcongr
  refine (add_le_add_right
    (ih _ (fun i hi ↦ (hf₁ _ <| subset_cons _ hi).2.2)
    ((card_le_card <| subset_cons _).trans hs)) _).trans ?_
  rw [mul_tsub, two_mul, ← pow_succ',
    ← add_tsub_assoc_of_le (pow_right_mono₀ (one_le_two : (1 : ℕ) ≤ 2) tsub_le_self),
    tsub_add_eq_add_tsub hs, card_cons, add_tsub_add_eq_tsub_right]
Cleared hypotheses: s, f, hf, hs
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.KruskalKatona (goal)
Goal:
α : Type u_1
inst : LinearOrder α
s : Finset α
inst_1 : Fintype α
hs : s.Nonempty
⊢ ∂ (initSeg s) = initSeg (s.erase (s.min' hs))
have h : ∀ (t : Finset α), t ∈ ∂ (initSeg s) ↔ t ∈ initSeg (s.erase (s.min' hs))
Tactic: ext t
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.KruskalKatona (goal)
Goal:
α : Type u_1
inst : LinearOrder α
s : Finset α
inst_1 : Fintype α
hs : s.Nonempty
t : Finset α
⊢ t ∈ ∂ (initSeg s) ↔ t ∈ initSeg (s.erase (s.min' hs))
have h : (∃ a ∉ t,
    #s = #(insert a t) ∧
      LE.le (α := Colex (Finset α)) ((toColex : (a : Finset α) → Colex (Finset α)) (insert a t) : Colex (Finset α))
        ((toColex : (a : Finset α) → Colex (Finset α)) s : Colex (Finset α))) ↔
  #(s.erase (s.min' hs)) = #t ∧
    LE.le (α := Colex (Finset α)) ((toColex : (a : Finset α) → Colex (Finset α)) t : Colex (Finset α))
      ((toColex : (a : Finset α) → Colex (Finset α)) (s.erase (s.min' hs)) : Colex (Finset α))
Tactic: simp only [mem_shadow_iff_insert_mem, mem_initSeg]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.KruskalKatona (goal)
Goal:
α : Type u_1
inst : LinearOrder α
s : Finset α
inst_1 : Fintype α
hs : s.Nonempty
t : Finset α
⊢ (∃ a ∉ t,
      #s = #(insert a t) ∧
        LE.le (α := Colex (Finset α)) ((toColex : (a : Finset α) → Colex (Finset α)) (insert a t) : Colex (Finset α))
          ((toColex : (a : Finset α) → Colex (Finset α)) s : Colex (Finset α))) ↔
    #(s.erase (s.min' hs)) = #t ∧
      LE.le (α := Colex (Finset α)) ((toColex : (a : Finset α) → Colex (Finset α)) t : Colex (Finset α))
        ((toColex : (a : Finset α) → Colex (Finset α)) (s.erase (s.min' hs)) : Colex (Finset α))
have h : (∃ a ∉ t,
    #s = #(insert a t) ∧
      LE.le (α := Colex (Finset α)) ((toColex : (a : Finset α) → Colex (Finset α)) (insert a t) : Colex (Finset α))
        ((toColex : (a : Finset α) → Colex (Finset α)) s : Colex (Finset α))) →
  #(s.erase (s.min' hs)) = #t ∧
    LE.le (α := Colex (Finset α)) ((toColex : (a : Finset α) → Colex (Finset α)) t : Colex (Finset α))
      ((toColex : (a : Finset α) → Colex (Finset α)) (s.erase (s.min' hs)) : Colex (Finset α))
Tactic: constructor
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.KruskalKatona (goal)
Goal:
α : Type u_1
inst : LinearOrder α
s : Finset α
inst_1 : Fintype α
hs : s.Nonempty
t : Finset α
h :
  (∃ a ∉ t,
      #s = #(insert a t) ∧
        LE.le (α := Colex (Finset α)) ((toColex : (a : Finset α) → Colex (Finset α)) (insert a t) : Colex (Finset α))
          ((toColex : (a : Finset α) → Colex (Finset α)) s : Colex (Finset α))) →
    #(s.erase (s.min' hs)) = #t ∧
      LE.le (α := Colex (Finset α)) ((toColex : (a : Finset α) → Colex (Finset α)) t : Colex (Finset α))
        ((toColex : (a : Finset α) → Colex (Finset α)) (s.erase (s.min' hs)) : Colex (Finset α))
⊢ (∃ a ∉ t,
      #s = #(insert a t) ∧
        LE.le (α := Colex (Finset α)) ((toColex : (a : Finset α) → Colex (Finset α)) (insert a t) : Colex (Finset α))
          ((toColex : (a : Finset α) → Colex (Finset α)) s : Colex (Finset α))) ↔
    #(s.erase (s.min' hs)) = #t ∧
      LE.le (α := Colex (Finset α)) ((toColex : (a : Finset α) → Colex (Finset α)) t : Colex (Finset α))
        ((toColex : (a : Finset α) → Colex (Finset α)) (s.erase (s.min' hs)) : Colex (Finset α))
have h₁ : #(s.erase (s.min' hs)) = #t ∧
    LE.le (α := Colex (Finset α)) ((toColex : (a : Finset α) → Colex (Finset α)) t : Colex (Finset α))
      ((toColex : (a : Finset α) → Colex (Finset α)) (s.erase (s.min' hs)) : Colex (Finset α)) →
  ∃ a ∉ t,
    #s = #(insert a t) ∧
      LE.le (α := Colex (Finset α)) ((toColex : (a : Finset α) → Colex (Finset α)) (insert a t) : Colex (Finset α))
        ((toColex : (a : Finset α) → Colex (Finset α)) s : Colex (Finset α))
Tactic: constructor
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.KruskalKatona (goal)
Goal:
α : Type u_1
inst : LinearOrder α
s : Finset α
inst_1 : Fintype α
hs : s.Nonempty
t : Finset α
a : α
ha : a ∉ t
hst : #s = #(insert a t)
hts :
  LE.le (α := Colex (Finset α)) ((toColex : (a : Finset α) → Colex (Finset α)) (insert a t) : Colex (Finset α))
    ((toColex : (a : Finset α) → Colex (Finset α)) s : Colex (Finset α))
⊢ #(s.erase (s.min' hs)) = #t ∧
    LE.le (α := Colex (Finset α)) ((toColex : (a : Finset α) → Colex (Finset α)) t : Colex (Finset α))
      ((toColex : (a : Finset α) → Colex (Finset α)) (s.erase (s.min' hs)) : Colex (Finset α))
have h : #(s.erase (s.min' hs)) = #t
Tactic: constructor
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.KruskalKatona (goal)
Goal:
α : Type u_1
inst : LinearOrder α
s : Finset α
inst_1 : Fintype α
hs : s.Nonempty
t : Finset α
a : α
ha : a ∉ t
hst : #s = #(insert a t)
hts :
  LE.le (α := Colex (Finset α)) ((toColex : (a : Finset α) → Colex (Finset α)) (insert a t) : Colex (Finset α))
    ((toColex : (a : Finset α) → Colex (Finset α)) s : Colex (Finset α))
h : #(s.erase (s.min' hs)) = #t
⊢ #(s.erase (s.min' hs)) = #t ∧
    LE.le (α := Colex (Finset α)) ((toColex : (a : Finset α) → Colex (Finset α)) t : Colex (Finset α))
      ((toColex : (a : Finset α) → Colex (Finset α)) (s.erase (s.min' hs)) : Colex (Finset α))
have h₁ : LE.le (α := Colex (Finset α)) ((toColex : (a : Finset α) → Colex (Finset α)) t : Colex (Finset α))
  ((toColex : (a : Finset α) → Colex (Finset α)) (s.erase (s.min' hs)) : Colex (Finset α))
Tactic: constructor
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.KruskalKatona (goal)
Goal:
α : Type u_1
inst : LinearOrder α
s : Finset α
inst_1 : Fintype α
hs : s.Nonempty
t : Finset α
a : α
ha : a ∉ t
hst : #s = #(insert a t)
hts :
  LE.le (α := Colex (Finset α)) ((toColex : (a : Finset α) → Colex (Finset α)) (insert a t) : Colex (Finset α))
    ((toColex : (a : Finset α) → Colex (Finset α)) s : Colex (Finset α))
⊢ #(s.erase (s.min' hs)) = #t
have h : #s - 1 = #t
Tactic: rw [card_erase_of_mem (min'_mem _ _), hst, card_insert_of_notMem ha, add_tsub_cancel_right]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.KruskalKatona (goal)
Goal:
α : Type u_1
inst : LinearOrder α
s : Finset α
inst_1 : Fintype α
hs : s.Nonempty
t : Finset α
a : α
ha : a ∉ t
hst : #s = #(insert a t)
hts :
  LE.le (α := Colex (Finset α)) ((toColex : (a : Finset α) → Colex (Finset α)) (insert a t) : Colex (Finset α))
    ((toColex : (a : Finset α) → Colex (Finset α)) s : Colex (Finset α))
h : #s - 1 = #t
⊢ #(s.erase (s.min' hs)) = #t
have h₁ : #(insert a t) - 1 = #t
Tactic: rw [card_erase_of_mem (min'_mem _ _), hst, card_insert_of_notMem ha, add_tsub_cancel_right]