awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.KruskalKatona (hypothesis)
Goal:
n r : ℕ
𝒜 : Finset (Finset (Fin n))
h : Set.Sized r (↑𝒜 : Set (Finset (Fin n)))
usable : Finset (Finset (Fin n) × Finset (Fin n)) :=
  {t : Finset (Fin n) × Finset (Fin n) | UsefulCompression t.1 t.2 ∧ ¬IsCompressed t.1 t.2 𝒜}
husable : usable.Nonempty
U V : Finset (Fin n)
hUV :
  Membership.mem (γ := Finset (Finset (Fin n) × Finset (Fin n))) univ (U, V) ∧
    UsefulCompression (U, V).1 (U, V).2 ∧ ¬IsCompressed (U, V).1 (U, V).2 𝒜
t : ∀ x' ∈ usable, #(U, V).1 ≤ #x'.1
h₂ : ∀ (U₁ V₁ : Finset (Fin n)), UsefulCompression U₁ V₁ → #U₁ < #U → IsCompressed U₁ V₁ 𝒜
p1 : #(∂ (𝓒 U V 𝒜)) ≤ #(∂ 𝒜)
hUV' : #(U, V).1 = #(U, V).2
⊢ ∃ (ℬ : Finset (Finset (Fin n))),
    #(∂ ℬ) ≤ #(∂ 𝒜) ∧
      #𝒜 = #ℬ ∧
        Set.Sized r (↑ℬ : Set (Finset (Fin n))) ∧ ∀ (U V : Finset (Fin n)), UsefulCompression U V → IsCompressed U V ℬ
have hu : (U, V).1.Nonempty
Tactic: obtain ⟨-, hUV', hu, hv, hmax⟩ := hUV.2.1
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.KruskalKatona (hypothesis)
Goal:
n r : ℕ
𝒜 : Finset (Finset (Fin n))
h : Set.Sized r (↑𝒜 : Set (Finset (Fin n)))
usable : Finset (Finset (Fin n) × Finset (Fin n)) :=
  {t : Finset (Fin n) × Finset (Fin n) | UsefulCompression t.1 t.2 ∧ ¬IsCompressed t.1 t.2 𝒜}
husable : usable.Nonempty
U V : Finset (Fin n)
hUV :
  Membership.mem (γ := Finset (Finset (Fin n) × Finset (Fin n))) univ (U, V) ∧
    UsefulCompression (U, V).1 (U, V).2 ∧ ¬IsCompressed (U, V).1 (U, V).2 𝒜
t : ∀ x' ∈ usable, #(U, V).1 ≤ #x'.1
h₂ : ∀ (U₁ V₁ : Finset (Fin n)), UsefulCompression U₁ V₁ → #U₁ < #U → IsCompressed U₁ V₁ 𝒜
p1 : #(∂ (𝓒 U V 𝒜)) ≤ #(∂ 𝒜)
hUV' : #(U, V).1 = #(U, V).2
hu : (U, V).1.Nonempty
⊢ ∃ (ℬ : Finset (Finset (Fin n))),
    #(∂ ℬ) ≤ #(∂ 𝒜) ∧
      #𝒜 = #ℬ ∧
        Set.Sized r (↑ℬ : Set (Finset (Fin n))) ∧ ∀ (U V : Finset (Fin n)), UsefulCompression U V → IsCompressed U V ℬ
have hv : (U, V).2.Nonempty
Tactic: obtain ⟨-, hUV', hu, hv, hmax⟩ := hUV.2.1
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.KruskalKatona (hypothesis)
Goal:
n r : ℕ
𝒜 : Finset (Finset (Fin n))
h : Set.Sized r (↑𝒜 : Set (Finset (Fin n)))
usable : Finset (Finset (Fin n) × Finset (Fin n)) :=
  {t : Finset (Fin n) × Finset (Fin n) | UsefulCompression t.1 t.2 ∧ ¬IsCompressed t.1 t.2 𝒜}
husable : usable.Nonempty
U V : Finset (Fin n)
hUV :
  Membership.mem (γ := Finset (Finset (Fin n) × Finset (Fin n))) univ (U, V) ∧
    UsefulCompression (U, V).1 (U, V).2 ∧ ¬IsCompressed (U, V).1 (U, V).2 𝒜
t : ∀ x' ∈ usable, #(U, V).1 ≤ #x'.1
h₂ : ∀ (U₁ V₁ : Finset (Fin n)), UsefulCompression U₁ V₁ → #U₁ < #U → IsCompressed U₁ V₁ 𝒜
p1 : #(∂ (𝓒 U V 𝒜)) ≤ #(∂ 𝒜)
hUV' : #(U, V).1 = #(U, V).2
hu : (U, V).1.Nonempty
hv : (U, V).2.Nonempty
⊢ ∃ (ℬ : Finset (Finset (Fin n))),
    #(∂ ℬ) ≤ #(∂ 𝒜) ∧
      #𝒜 = #ℬ ∧
        Set.Sized r (↑ℬ : Set (Finset (Fin n))) ∧ ∀ (U V : Finset (Fin n)), UsefulCompression U V → IsCompressed U V ℬ
have hmax : (U, V).1.max' hu < (U, V).2.max' hv
Tactic: obtain ⟨-, hUV', hu, hv, hmax⟩ := hUV.2.1
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.KruskalKatona (hypothesis)
Goal:
n r : ℕ
𝒜 : Finset (Finset (Fin n))
h : Set.Sized r (↑𝒜 : Set (Finset (Fin n)))
usable : Finset (Finset (Fin n) × Finset (Fin n)) :=
  {t : Finset (Fin n) × Finset (Fin n) | UsefulCompression t.1 t.2 ∧ ¬IsCompressed t.1 t.2 𝒜}
husable : usable.Nonempty
U V : Finset (Fin n)
hUV :
  Membership.mem (γ := Finset (Finset (Fin n) × Finset (Fin n))) univ (U, V) ∧
    UsefulCompression (U, V).1 (U, V).2 ∧ ¬IsCompressed (U, V).1 (U, V).2 𝒜
t : ∀ x' ∈ usable, #(U, V).1 ≤ #x'.1
h₂ : ∀ (U₁ V₁ : Finset (Fin n)), UsefulCompression U₁ V₁ → #U₁ < #U → IsCompressed U₁ V₁ 𝒜
p1 : #(∂ (𝓒 U V 𝒜)) ≤ #(∂ 𝒜)
hUV' : #(U, V).1 = #(U, V).2
hu : (U, V).1.Nonempty
hv : (U, V).2.Nonempty
hmax : (U, V).1.max' hu < (U, V).2.max' hv
⊢ ∃ (ℬ : Finset (Finset (Fin n))),
    #(∂ ℬ) ≤ #(∂ 𝒜) ∧
      #𝒜 = #ℬ ∧
        Set.Sized r (↑ℬ : Set (Finset (Fin n))) ∧ ∀ (U V : Finset (Fin n)), UsefulCompression U V → IsCompressed U V ℬ
have this : familyMeasure (𝓒 (U, V).1 (U, V).2 𝒜) < familyMeasure 𝒜
Tactic: have := familyMeasure_compression_lt_familyMeasure hmax hUV.2.2
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.KruskalKatona (goal)
Goal:
n r : ℕ
𝒜 : Finset (Finset (Fin n))
h : Set.Sized r (↑𝒜 : Set (Finset (Fin n)))
usable : Finset (Finset (Fin n) × Finset (Fin n)) :=
  {t : Finset (Fin n) × Finset (Fin n) | UsefulCompression t.1 t.2 ∧ ¬IsCompressed t.1 t.2 𝒜}
husable : usable.Nonempty
U V : Finset (Fin n)
hUV :
  Membership.mem (γ := Finset (Finset (Fin n) × Finset (Fin n))) univ (U, V) ∧
    UsefulCompression (U, V).1 (U, V).2 ∧ ¬IsCompressed (U, V).1 (U, V).2 𝒜
t : ∀ x' ∈ usable, #(U, V).1 ≤ #x'.1
h₂ : ∀ (U₁ V₁ : Finset (Fin n)), UsefulCompression U₁ V₁ → #U₁ < #U → IsCompressed U₁ V₁ 𝒜
p1 : #(∂ (𝓒 U V 𝒜)) ≤ #(∂ 𝒜)
hUV' : #(U, V).1 = #(U, V).2
hu : (U, V).1.Nonempty
hv : (U, V).2.Nonempty
hmax : (U, V).1.max' hu < (U, V).2.max' hv
this : familyMeasure (𝓒 (U, V).1 (U, V).2 𝒜) < familyMeasure 𝒜
⊢ ∃ (ℬ : Finset (Finset (Fin n))),
    #(∂ ℬ) ≤ #(∂ 𝒜) ∧
      #𝒜 = #ℬ ∧
        Set.Sized r (↑ℬ : Set (Finset (Fin n))) ∧ ∀ (U V : Finset (Fin n)), UsefulCompression U V → IsCompressed U V ℬ
have inr : ∀ (t : Finset (Finset (Fin n))) (q1 : #(∂ t) ≤ #(∂ (𝓒 U V 𝒜))) (q2 : #(𝓒 U V 𝒜) = #t)
  (q3 : Set.Sized r (↑t : Set (Finset (Fin n))))
  (q4 : ∀ (U V : Finset (Fin n)), UsefulCompression U V → IsCompressed U V t),
  ∃ (ℬ : Finset (Finset (Fin n))),
    #(∂ ℬ) ≤ #(∂ 𝒜) ∧
      #𝒜 = #ℬ ∧
        Set.Sized r (↑ℬ : Set (Finset (Fin n))) ∧ ∀ (U V : Finset (Fin n)), UsefulCompression U V → IsCompressed U V ℬ
Tactic: obtain ⟨t, q1, q2, q3, q4⟩ := UV.kruskal_katona_helper (𝓒 U V 𝒜) (h.uvCompression hUV')
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.KruskalKatona (goal)
Goal:
n r : ℕ
𝒜 : Finset (Finset (Fin n))
h : Set.Sized r (↑𝒜 : Set (Finset (Fin n)))
Are Are₁ :
  ∃ (ℬ : Finset (Finset (Fin n))),
    #(∂ ℬ) ≤ #(∂ 𝒜) ∧
      #𝒜 = #ℬ ∧
        Set.Sized r (↑ℬ : Set (Finset (Fin n))) ∧ ∀ (U V : Finset (Fin n)), UsefulCompression U V → IsCompressed U V ℬ
⊢ ∃ (ℬ : Finset (Finset (Fin n))),
    #(∂ ℬ) ≤ #(∂ 𝒜) ∧
      #𝒜 = #ℬ ∧
        Set.Sized r (↑ℬ : Set (Finset (Fin n))) ∧ ∀ (U V : Finset (Fin n)), UsefulCompression U V → IsCompressed U V ℬ
have inl : let usable : Finset (Finset (Fin n) × Finset (Fin n)) :=
  {t : Finset (Fin n) × Finset (Fin n) | UsefulCompression t.1 t.2 ∧ ¬IsCompressed t.1 t.2 𝒜};
∀ (husable : usable = ∅),
  ∃ (ℬ : Finset (Finset (Fin n))),
    #(∂ ℬ) ≤ #(∂ 𝒜) ∧
      #𝒜 = #ℬ ∧
        Set.Sized r (↑ℬ : Set (Finset (Fin n))) ∧ ∀ (U V : Finset (Fin n)), UsefulCompression U V → IsCompressed U V ℬ
Tactic: classical
  -- Are there any compressions we can make now?
  set usable : Finset (Finset (Fin n) × Finset (Fin n)) :=
    {t | UsefulCompression t.1 t.2 ∧ ¬ IsCompressed t.1 t.2 𝒜}
  obtain husable | husable := usable.eq_empty_or_nonempty
  -- No. Then where we are is the required set family.
  · refine ⟨𝒜, le_rfl, rfl, h, fun U V hUV ↦ ?_⟩
    rw [eq_empty_iff_forall_notMem] at husable
    by_contra h
    exact husable ⟨U, V⟩ <| mem_filter.2 ⟨mem_univ _, hUV, h⟩
  -- Yes. Then apply the smallest compression, then keep going
  obtain ⟨⟨U, V⟩, hUV, t⟩ := exists_min_image usable (fun t ↦ #t.1) husable
  rw [mem_filter] at hUV
  have h₂ : ∀ U₁ V₁, UsefulCompression U₁ V₁ → #U₁ < #U → IsCompressed U₁ V₁ 𝒜 := by
    rintro U₁ V₁ huseful hUcard
    by_contra h
    exact hUcard.not_ge <| t ⟨U₁, V₁⟩ <| mem_filter.2 ⟨mem_univ _, huseful, h⟩
  have p1 : #(∂ (𝓒 U V 𝒜)) ≤ #(∂ 𝒜) := compression_improved _ hUV.2.1 h₂
  obtain ⟨-, hUV', hu, hv, hmax⟩ := hUV.2.1
  have := familyMeasure_compression_lt_familyMeasure hmax hUV.2.2
  obtain ⟨t, q1, q2, q3, q4⟩ := UV.kruskal_katona_helper (𝓒 U V 𝒜) (h.uvCompression hUV')
  exact ⟨t, q1.trans p1, (card_compression _ _ _).symm.trans q2, q3, q4⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.KruskalKatona (goal)
Goal:
n r : ℕ
𝒜 : Finset (Finset (Fin n))
h : Set.Sized r (↑𝒜 : Set (Finset (Fin n)))
Are Are₁ :
  ∃ (ℬ : Finset (Finset (Fin n))),
    #(∂ ℬ) ≤ #(∂ 𝒜) ∧
      #𝒜 = #ℬ ∧
        Set.Sized r (↑ℬ : Set (Finset (Fin n))) ∧ ∀ (U V : Finset (Fin n)), UsefulCompression U V → IsCompressed U V ℬ
inl :
  let usable : Finset (Finset (Fin n) × Finset (Fin n)) :=
    {t : Finset (Fin n) × Finset (Fin n) | UsefulCompression t.1 t.2 ∧ ¬IsCompressed t.1 t.2 𝒜};
  ∀ (husable : usable = ∅),
    ∃ (ℬ : Finset (Finset (Fin n))),
      #(∂ ℬ) ≤ #(∂ 𝒜) ∧
        #𝒜 = #ℬ ∧
          Set.Sized r (↑ℬ : Set (Finset (Fin n))) ∧ ∀ (U V : Finset (Fin n)), UsefulCompression U V → IsCompressed U V ℬ
⊢ ∃ (ℬ : Finset (Finset (Fin n))),
    #(∂ ℬ) ≤ #(∂ 𝒜) ∧
      #𝒜 = #ℬ ∧
        Set.Sized r (↑ℬ : Set (Finset (Fin n))) ∧ ∀ (U V : Finset (Fin n)), UsefulCompression U V → IsCompressed U V ℬ
have inr : let usable : Finset (Finset (Fin n) × Finset (Fin n)) :=
  {t : Finset (Fin n) × Finset (Fin n) | UsefulCompression t.1 t.2 ∧ ¬IsCompressed t.1 t.2 𝒜};
∀ (husable : usable.Nonempty),
  ∃ (ℬ : Finset (Finset (Fin n))),
    #(∂ ℬ) ≤ #(∂ 𝒜) ∧
      #𝒜 = #ℬ ∧
        Set.Sized r (↑ℬ : Set (Finset (Fin n))) ∧ ∀ (U V : Finset (Fin n)), UsefulCompression U V → IsCompressed U V ℬ
Tactic: classical
  -- Are there any compressions we can make now?
  set usable : Finset (Finset (Fin n) × Finset (Fin n)) :=
    {t | UsefulCompression t.1 t.2 ∧ ¬ IsCompressed t.1 t.2 𝒜}
  obtain husable | husable := usable.eq_empty_or_nonempty
  -- No. Then where we are is the required set family.
  · refine ⟨𝒜, le_rfl, rfl, h, fun U V hUV ↦ ?_⟩
    rw [eq_empty_iff_forall_notMem] at husable
    by_contra h
    exact husable ⟨U, V⟩ <| mem_filter.2 ⟨mem_univ _, hUV, h⟩
  -- Yes. Then apply the smallest compression, then keep going
  obtain ⟨⟨U, V⟩, hUV, t⟩ := exists_min_image usable (fun t ↦ #t.1) husable
  rw [mem_filter] at hUV
  have h₂ : ∀ U₁ V₁, UsefulCompression U₁ V₁ → #U₁ < #U → IsCompressed U₁ V₁ 𝒜 := by
    rintro U₁ V₁ huseful hUcard
    by_contra h
    exact hUcard.not_ge <| t ⟨U₁, V₁⟩ <| mem_filter.2 ⟨mem_univ _, huseful, h⟩
  have p1 : #(∂ (𝓒 U V 𝒜)) ≤ #(∂ 𝒜) := compression_improved _ hUV.2.1 h₂
  obtain ⟨-, hUV', hu, hv, hmax⟩ := hUV.2.1
  have := familyMeasure_compression_lt_familyMeasure hmax hUV.2.2
  obtain ⟨t, q1, q2, q3, q4⟩ := UV.kruskal_katona_helper (𝓒 U V 𝒜) (h.uvCompression hUV')
  exact ⟨t, q1.trans p1, (card_compression _ _ _).symm.trans q2, q3, q4⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.KruskalKatona (goal)
Goal:
n r : ℕ
𝒜 : Finset (Finset (Fin n))
h : Set.Sized r (↑𝒜 : Set (Finset (Fin n)))
Are Are₁ :
  ∃ (ℬ : Finset (Finset (Fin n))),
    #(∂ ℬ) ≤ #(∂ 𝒜) ∧
      #𝒜 = #ℬ ∧
        Set.Sized r (↑ℬ : Set (Finset (Fin n))) ∧ ∀ (U V : Finset (Fin n)), UsefulCompression U V → IsCompressed U V ℬ
inl :
  let usable : Finset (Finset (Fin n) × Finset (Fin n)) :=
    {t : Finset (Fin n) × Finset (Fin n) | UsefulCompression t.1 t.2 ∧ ¬IsCompressed t.1 t.2 𝒜};
  ∀ (husable : usable = ∅),
    ∃ (ℬ : Finset (Finset (Fin n))),
      #(∂ ℬ) ≤ #(∂ 𝒜) ∧
        #𝒜 = #ℬ ∧
          Set.Sized r (↑ℬ : Set (Finset (Fin n))) ∧ ∀ (U V : Finset (Fin n)), UsefulCompression U V → IsCompressed U V ℬ
inr inr₁ :
  let usable : Finset (Finset (Fin n) × Finset (Fin n)) :=
    {t : Finset (Fin n) × Finset (Fin n) | UsefulCompression t.1 t.2 ∧ ¬IsCompressed t.1 t.2 𝒜};
  ∀ (husable : usable.Nonempty),
    ∃ (ℬ : Finset (Finset (Fin n))),
      #(∂ ℬ) ≤ #(∂ 𝒜) ∧
        #𝒜 = #ℬ ∧
          Set.Sized r (↑ℬ : Set (Finset (Fin n))) ∧ ∀ (U V : Finset (Fin n)), UsefulCompression U V → IsCompressed U V ℬ
⊢ ∃ (ℬ : Finset (Finset (Fin n))),
    #(∂ ℬ) ≤ #(∂ 𝒜) ∧
      #𝒜 = #ℬ ∧
        Set.Sized r (↑ℬ : Set (Finset (Fin n))) ∧ ∀ (U V : Finset (Fin n)), UsefulCompression U V → IsCompressed U V ℬ
have inr₂ : let usable : Finset (Finset (Fin n) × Finset (Fin n)) :=
  {t : Finset (Fin n) × Finset (Fin n) | UsefulCompression t.1 t.2 ∧ ¬IsCompressed t.1 t.2 𝒜};
∀ (husable : usable.Nonempty) (U V : Finset (Fin n)) (hUV : (U, V) ∈ usable) (t : ∀ x' ∈ usable, #(U, V).1 ≤ #x'.1),
  ∃ (ℬ : Finset (Finset (Fin n))),
    #(∂ ℬ) ≤ #(∂ 𝒜) ∧
      #𝒜 = #ℬ ∧
        Set.Sized r (↑ℬ : Set (Finset (Fin n))) ∧ ∀ (U V : Finset (Fin n)), UsefulCompression U V → IsCompressed U V ℬ
Tactic: classical
  -- Are there any compressions we can make now?
  set usable : Finset (Finset (Fin n) × Finset (Fin n)) :=
    {t | UsefulCompression t.1 t.2 ∧ ¬ IsCompressed t.1 t.2 𝒜}
  obtain husable | husable := usable.eq_empty_or_nonempty
  -- No. Then where we are is the required set family.
  · refine ⟨𝒜, le_rfl, rfl, h, fun U V hUV ↦ ?_⟩
    rw [eq_empty_iff_forall_notMem] at husable
    by_contra h
    exact husable ⟨U, V⟩ <| mem_filter.2 ⟨mem_univ _, hUV, h⟩
  -- Yes. Then apply the smallest compression, then keep going
  obtain ⟨⟨U, V⟩, hUV, t⟩ := exists_min_image usable (fun t ↦ #t.1) husable
  rw [mem_filter] at hUV
  have h₂ : ∀ U₁ V₁, UsefulCompression U₁ V₁ → #U₁ < #U → IsCompressed U₁ V₁ 𝒜 := by
    rintro U₁ V₁ huseful hUcard
    by_contra h
    exact hUcard.not_ge <| t ⟨U₁, V₁⟩ <| mem_filter.2 ⟨mem_univ _, huseful, h⟩
  have p1 : #(∂ (𝓒 U V 𝒜)) ≤ #(∂ 𝒜) := compression_improved _ hUV.2.1 h₂
  obtain ⟨-, hUV', hu, hv, hmax⟩ := hUV.2.1
  have := familyMeasure_compression_lt_familyMeasure hmax hUV.2.2
  obtain ⟨t, q1, q2, q3, q4⟩ := UV.kruskal_katona_helper (𝓒 U V 𝒜) (h.uvCompression hUV')
  exact ⟨t, q1.trans p1, (card_compression _ _ _).symm.trans q2, q3, q4⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.KruskalKatona (goal)
Goal:
n r : ℕ
𝒜 𝒞 : Finset (Finset (Fin n))
h𝒜r : Set.Sized r (↑𝒜 : Set (Finset (Fin n)))
h𝒞𝒜 : #𝒞 ≤ #𝒜
h𝒞 : IsInitSeg 𝒞 r
⊢ #(∂ 𝒞) ≤ #(∂ 𝒜)
have obtain : ∀ (𝒜' : Finset (Finset (Fin n))) (h𝒜 : 𝒜' ⊆ 𝒜) (h𝒜𝒞 : #𝒜' = #𝒞), #(∂ 𝒞) ≤ #(∂ 𝒜)
Tactic: obtain ⟨𝒜', h𝒜, h𝒜𝒞⟩ := exists_subset_card_eq h𝒞𝒜
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.KruskalKatona (goal)
Goal:
n r : ℕ
𝒜 𝒞 : Finset (Finset (Fin n))
h𝒜r : Set.Sized r (↑𝒜 : Set (Finset (Fin n)))
h𝒞𝒜 : #𝒞 ≤ #𝒜
h𝒞 : IsInitSeg 𝒞 r
𝒜' : Finset (Finset (Fin n))
h𝒜 : 𝒜' ⊆ 𝒜
h𝒜𝒞 : #𝒜' = #𝒞
⊢ #(∂ 𝒞) ≤ #(∂ 𝒜)
have obtain : ∀ (ℬ : Finset (Finset (Fin n))) (hℬ𝒜 : #(∂ ℬ) ≤ #(∂ 𝒜')) (h𝒜ℬ : #𝒜' = #ℬ)
  (hℬr : Set.Sized r (↑ℬ : Set (Finset (Fin n))))
  (hℬ : ∀ (U V : Finset (Fin n)), UV.UsefulCompression U V → IsCompressed U V ℬ), #(∂ 𝒞) ≤ #(∂ 𝒜)
Tactic: obtain ⟨ℬ, hℬ𝒜, h𝒜ℬ, hℬr, hℬ⟩ := UV.kruskal_katona_helper 𝒜' (h𝒜r.mono (by gcongr))
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.KruskalKatona (goal)
Goal:
n r : ℕ
𝒜 𝒞 : Finset (Finset (Fin n))
h𝒜r : Set.Sized r (↑𝒜 : Set (Finset (Fin n)))
h𝒞𝒜 : #𝒞 ≤ #𝒜
h𝒞 : IsInitSeg 𝒞 r
𝒜' : Finset (Finset (Fin n))
h𝒜 : 𝒜' ⊆ 𝒜
h𝒜𝒞 : #𝒜' = #𝒞
ℬ : Finset (Finset (Fin n))
hℬ𝒜 : #(∂ ℬ) ≤ #(∂ 𝒜')
h𝒜ℬ : #𝒜' = #ℬ
hℬr : Set.Sized r (↑ℬ : Set (Finset (Fin n)))
hℬ : ∀ (U V : Finset (Fin n)), UV.UsefulCompression U V → IsCompressed U V ℬ
this : ℬ = 𝒞
⊢ #(∂ 𝒞) ≤ #(∂ 𝒜)
have subst : ∀ (h𝒞𝒜 : #ℬ ≤ #𝒜) (h𝒞 : IsInitSeg ℬ r) (h𝒜𝒞 : #𝒜' = #ℬ), #(∂ ℬ) ≤ #(∂ 𝒜)
Tactic: subst 𝒞
Cleared hypotheses: 𝒞, h𝒞𝒜, h𝒞, h𝒜𝒞, this
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.KruskalKatona (goal)
Goal:
n r : ℕ
𝒜 𝒞 : Finset (Finset (Fin n))
h𝒜r : Set.Sized r (↑𝒜 : Set (Finset (Fin n)))
h𝒞𝒜 : #𝒞 ≤ #𝒜
h𝒞 : IsInitSeg 𝒞 r
𝒜' : Finset (Finset (Fin n))
h𝒜 : 𝒜' ⊆ 𝒜
h𝒜𝒞 : #𝒜' = #𝒞
ℬ : Finset (Finset (Fin n))
hℬ𝒜 : #(∂ ℬ) ≤ #(∂ 𝒜')
h𝒜ℬ : #𝒜' = #ℬ
hℬr : Set.Sized r (↑ℬ : Set (Finset (Fin n)))
hℬ : ∀ (U V : Finset (Fin n)), UV.UsefulCompression U V → IsCompressed U V ℬ
⊢ #(∂ 𝒞) ≤ #(∂ 𝒜)
have suffices : ℬ = 𝒞
Tactic: suffices ℬ = 𝒞 by subst 𝒞; exact hℬ𝒜.trans (by gcongr)
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.KruskalKatona (hypothesis)
Goal:
n r : ℕ
𝒜 𝒞 : Finset (Finset (Fin n))
h𝒜r : Set.Sized r (↑𝒜 : Set (Finset (Fin n)))
h𝒞𝒜 : #𝒞 ≤ #𝒜
h𝒞 : IsInitSeg 𝒞 r
𝒜' : Finset (Finset (Fin n))
h𝒜 : 𝒜' ⊆ 𝒜
h𝒜𝒞 : #𝒜' = #𝒞
ℬ : Finset (Finset (Fin n))
hℬ𝒜 : #(∂ ℬ) ≤ #(∂ 𝒜')
h𝒜ℬ : #𝒜' = #ℬ
hℬr : Set.Sized r (↑ℬ : Set (Finset (Fin n)))
hℬ : ∀ (U V : Finset (Fin n)), UV.UsefulCompression U V → IsCompressed U V ℬ
⊢ ℬ = 𝒞
have hcard : #ℬ = #𝒞
Tactic: have hcard : #ℬ = #𝒞 := h𝒜ℬ.symm.trans h𝒜𝒞
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.KruskalKatona (goal)
Goal:
n r : ℕ
𝒜 𝒞 : Finset (Finset (Fin n))
h𝒜r : Set.Sized r (↑𝒜 : Set (Finset (Fin n)))
h𝒞𝒜 : #𝒞 ≤ #𝒜
h𝒞 : IsInitSeg 𝒞 r
𝒜' : Finset (Finset (Fin n))
h𝒜 : 𝒜' ⊆ 𝒜
h𝒜𝒞 : #𝒜' = #𝒞
ℬ : Finset (Finset (Fin n))
hℬ𝒜 : #(∂ ℬ) ≤ #(∂ 𝒜')
h𝒜ℬ : #𝒜' = #ℬ
hℬr : Set.Sized r (↑ℬ : Set (Finset (Fin n)))
hℬ : ∀ (U V : Finset (Fin n)), UV.UsefulCompression U V → IsCompressed U V ℬ
hcard : #ℬ = #𝒞
⊢ ℬ = 𝒞
have inl : ∀ (h𝒞ℬ : 𝒞 ⊆ ℬ), ℬ = 𝒞
Tactic: obtain h𝒞ℬ | hℬ𝒞 := h𝒞.total (UV.isInitSeg_of_compressed hℬr hℬ)
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.KruskalKatona (goal)
Goal:
n r : ℕ
𝒜 𝒞 : Finset (Finset (Fin n))
h𝒜r : Set.Sized r (↑𝒜 : Set (Finset (Fin n)))
h𝒞𝒜 : #𝒞 ≤ #𝒜
h𝒞 : IsInitSeg 𝒞 r
𝒜' : Finset (Finset (Fin n))
h𝒜 : 𝒜' ⊆ 𝒜
h𝒜𝒞 : #𝒜' = #𝒞
ℬ : Finset (Finset (Fin n))
hℬ𝒜 : #(∂ ℬ) ≤ #(∂ 𝒜')
h𝒜ℬ : #𝒜' = #ℬ
hℬr : Set.Sized r (↑ℬ : Set (Finset (Fin n)))
hℬ : ∀ (U V : Finset (Fin n)), UV.UsefulCompression U V → IsCompressed U V ℬ
hcard : #ℬ = #𝒞
inl : ∀ (h𝒞ℬ : 𝒞 ⊆ ℬ), ℬ = 𝒞
⊢ ℬ = 𝒞
have inr : ∀ (hℬ𝒞 : ℬ ⊆ 𝒞), ℬ = 𝒞
Tactic: obtain h𝒞ℬ | hℬ𝒞 := h𝒞.total (UV.isInitSeg_of_compressed hℬr hℬ)
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.KruskalKatona (goal)
Goal:
n n_1 : ℕ
ih :
  ∀ {r : ℕ} {𝒜 𝒞 : Finset (Finset (Fin n))} (h₁ : Set.Sized r (↑𝒜 : Set (Finset (Fin n)))) (h₂ : #𝒞 ≤ #𝒜)
    (h₃ : IsInitSeg 𝒞 r), #(∂^[n_1] 𝒞) ≤ #(∂^[n_1] 𝒜)
r : ℕ
𝒜 𝒞 : Finset (Finset (Fin n))
h₁ : Set.Sized r (↑𝒜 : Set (Finset (Fin n)))
h₂ : #𝒞 ≤ #𝒜
h₃ : IsInitSeg 𝒞 r
⊢ #(∂^[n_1 + 1] 𝒞) ≤ #(∂^[n_1 + 1] 𝒜)
have succ : IsInitSeg (∂ 𝒞) (r - 1)
Tactic: refine ih h₁.shadow (kruskal_katona h₁ h₂ h₃) ?_
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.KruskalKatona (goal)
Goal:
n r k : ℕ
𝒜 𝒞 : Finset (Finset (Fin n))
h₁ : Set.Sized r (↑𝒜 : Set (Finset (Fin n)))
h₂ : #𝒞 ≤ #𝒜
h₃ : IsInitSeg 𝒞 r
⊢ #(∂^[k] 𝒞) ≤ #(∂^[k] 𝒜)
have zero : ∀ {r : ℕ} {𝒜 𝒞 : Finset (Finset (Fin n))} (h₁ : Set.Sized r (↑𝒜 : Set (Finset (Fin n)))) (h₂ : #𝒞 ≤ #𝒜)
  (h₃ : IsInitSeg 𝒞 r), #(∂^[0] 𝒞) ≤ #(∂^[0] 𝒜)
Tactic: induction k generalizing r 𝒜 𝒞 with
  | zero => simpa
  | succ _ ih =>
    refine ih h₁.shadow (kruskal_katona h₁ h₂ h₃) ?_
    convert! h₃.shadow
Cleared hypotheses: r, k, 𝒜, 𝒞, h₁, h₂, h₃
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.KruskalKatona (goal)
Goal:
n r k : ℕ
𝒜 𝒞 : Finset (Finset (Fin n))
h₁ : Set.Sized r (↑𝒜 : Set (Finset (Fin n)))
h₂ : #𝒞 ≤ #𝒜
h₃ : IsInitSeg 𝒞 r
zero :
  ∀ {r : ℕ} {𝒜 𝒞 : Finset (Finset (Fin n))} (h₁ : Set.Sized r (↑𝒜 : Set (Finset (Fin n)))) (h₂ : #𝒞 ≤ #𝒜)
    (h₃ : IsInitSeg 𝒞 r), #(∂^[0] 𝒞) ≤ #(∂^[0] 𝒜)
⊢ #(∂^[k] 𝒞) ≤ #(∂^[k] 𝒜)
have succ : ∀ (n_1 : ℕ)
  (ih :
    ∀ {r : ℕ} {𝒜 𝒞 : Finset (Finset (Fin n))} (h₁ : Set.Sized r (↑𝒜 : Set (Finset (Fin n)))) (h₂ : #𝒞 ≤ #𝒜)
      (h₃ : IsInitSeg 𝒞 r), #(∂^[n_1] 𝒞) ≤ #(∂^[n_1] 𝒜))
  {r : ℕ} {𝒜 𝒞 : Finset (Finset (Fin n))} (h₁ : Set.Sized r (↑𝒜 : Set (Finset (Fin n)))) (h₂ : #𝒞 ≤ #𝒜)
  (h₃ : IsInitSeg 𝒞 r), #(∂^[n_1 + 1] 𝒞) ≤ #(∂^[n_1 + 1] 𝒜)
Tactic: induction k generalizing r 𝒜 𝒞 with
  | zero => simpa
  | succ _ ih =>
    refine ih h₁.shadow (kruskal_katona h₁ h₂ h₃) ?_
    convert! h₃.shadow
Cleared hypotheses: r, k, 𝒜, 𝒞, h₁, h₂, h₃
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.KruskalKatona (goal)
Goal:
n r k i : ℕ
𝒜 : Finset (Finset (Fin n))
hir : i ≤ r
hrk : r ≤ k
hkn : k ≤ n
h₁ : Set.Sized r (↑𝒜 : Set (Finset (Fin n)))
h₂ : k.choose r ≤ #𝒜
m : ℕ
⊢ m ∈ range k → m < n
have rw : m < k → m < n
Tactic: rw [mem_range]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.KruskalKatona (hypothesis)
Goal:
n r k i : ℕ
𝒜 : Finset (Finset (Fin n))
hir : i ≤ r
hrk : r ≤ k
hkn : k ≤ n
h₁ : Set.Sized r (↑𝒜 : Set (Finset (Fin n)))
h₂ : k.choose r ≤ #𝒜
range'k : Finset (Fin n) := (range k).attachFin ⋯
𝒞 : Finset (Finset (Fin n)) := powersetCard r range'k
⊢ k.choose (r - i) ≤ #(∂^[i] 𝒜)
have this : Set.Sized r (↑𝒞 : Set (Finset (Fin n)))
Tactic: have : (𝒞 : Set (Finset (Fin n))).Sized r := Set.sized_powersetCard _ _
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.KruskalKatona (goal)
Goal:
n r k i : ℕ
𝒜 : Finset (Finset (Fin n))
hir : i ≤ r
hrk : r ≤ k
hkn : k ≤ n
h₁ : Set.Sized r (↑𝒜 : Set (Finset (Fin n)))
h₂ : k.choose r ≤ #𝒜
range'k : Finset (Fin n) := (range k).attachFin ⋯
𝒞 : Finset (Finset (Fin n)) := powersetCard r range'k
this : Set.Sized r (↑𝒞 : Set (Finset (Fin n)))
⊢ k.choose (r - i) = #(powersetCard (r - i) range'k)
have rw : k.choose (r - i) = (#range'k).choose (r - i)
Tactic: rw [card_powersetCard, card_attachFin, card_range]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.KruskalKatona (goal)
Goal:
n r k i : ℕ
𝒜 : Finset (Finset (Fin n))
hir : i ≤ r
hrk : r ≤ k
hkn : k ≤ n
h₁ : Set.Sized r (↑𝒜 : Set (Finset (Fin n)))
h₂ : k.choose r ≤ #𝒜
range'k : Finset (Fin n) := (range k).attachFin ⋯
𝒞 : Finset (Finset (Fin n)) := powersetCard r range'k
this : Set.Sized r (↑𝒞 : Set (Finset (Fin n)))
rw : k.choose (r - i) = (#range'k).choose (r - i)
⊢ k.choose (r - i) = #(powersetCard (r - i) range'k)
have rw₁ : k.choose (r - i) = (#(range k)).choose (r - i)
Tactic: rw [card_powersetCard, card_attachFin, card_range]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.KruskalKatona (goal)
Goal:
n r k i : ℕ
𝒜 : Finset (Finset (Fin n))
hir : i ≤ r
hrk : r ≤ k
hkn : k ≤ n
h₁ : Set.Sized r (↑𝒜 : Set (Finset (Fin n)))
h₂ : k.choose r ≤ #𝒜
range'k : Finset (Fin n) := (range k).attachFin ⋯
𝒞 : Finset (Finset (Fin n)) := powersetCard r range'k
this : Set.Sized r (↑𝒞 : Set (Finset (Fin n)))
rw : k.choose (r - i) = (#range'k).choose (r - i)
rw₁ : k.choose (r - i) = (#(range k)).choose (r - i)
⊢ k.choose (r - i) = #(powersetCard (r - i) range'k)
have rw₂ : k.choose (r - i) = k.choose (r - i)
Tactic: rw [card_powersetCard, card_attachFin, card_range]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.KruskalKatona (goal)
Goal:
n r k i : ℕ
𝒜 : Finset (Finset (Fin n))
hir : i ≤ r
hrk : r ≤ k
hkn : k ≤ n
h₁ : Set.Sized r (↑𝒜 : Set (Finset (Fin n)))
h₂ : k.choose r ≤ #𝒜
range'k : Finset (Fin n) := (range k).attachFin ⋯
𝒞 : Finset (Finset (Fin n)) := powersetCard r range'k
this : Set.Sized r (↑𝒞 : Set (Finset (Fin n)))
⊢ #(powersetCard (r - i) range'k) = #(∂^[i] 𝒞)
have h : powersetCard (r - i) range'k = ∂^[i] 𝒞
Tactic: congr!
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.KruskalKatona (goal)
Goal:
n r k i : ℕ
𝒜 : Finset (Finset (Fin n))
hir : i ≤ r
hrk : r ≤ k
hkn : k ≤ n
h₁ : Set.Sized r (↑𝒜 : Set (Finset (Fin n)))
h₂ : k.choose r ≤ #𝒜
range'k : Finset (Fin n) := (range k).attachFin ⋯
𝒞 : Finset (Finset (Fin n)) := powersetCard r range'k
this : Set.Sized r (↑𝒞 : Set (Finset (Fin n)))
⊢ powersetCard (r - i) range'k = ∂^[i] 𝒞
have h : ∀ (B : Finset (Fin n)), B ∈ powersetCard (r - i) range'k ↔ B ∈ ∂^[i] 𝒞
Tactic: ext B
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.KruskalKatona (goal)
Goal:
n r k i : ℕ
𝒜 : Finset (Finset (Fin n))
hir : i ≤ r
hrk : r ≤ k
hkn : k ≤ n
h₁ : Set.Sized r (↑𝒜 : Set (Finset (Fin n)))
h₂ : k.choose r ≤ #𝒜
range'k : Finset (Fin n) := (range k).attachFin ⋯
𝒞 : Finset (Finset (Fin n)) := powersetCard r range'k
this : Set.Sized r (↑𝒞 : Set (Finset (Fin n)))
B : Finset (Fin n)
⊢ B ∈ powersetCard (r - i) range'k ↔ B ∈ ∂^[i] 𝒞
have h : B ⊆ range'k ∧ #B = r - i ↔ ∃ s ∈ 𝒞, B ⊆ s ∧ #(s \ B) = i
Tactic: rw [mem_powersetCard, mem_shadow_iterate_iff_exists_sdiff]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.KruskalKatona (goal)
Goal:
n r k i : ℕ
𝒜 : Finset (Finset (Fin n))
hir : i ≤ r
hrk : r ≤ k
hkn : k ≤ n
h₁ : Set.Sized r (↑𝒜 : Set (Finset (Fin n)))
h₂ : k.choose r ≤ #𝒜
range'k : Finset (Fin n) := (range k).attachFin ⋯
𝒞 : Finset (Finset (Fin n)) := powersetCard r range'k
this : Set.Sized r (↑𝒞 : Set (Finset (Fin n)))
B : Finset (Fin n)
⊢ B ⊆ range'k ∧ #B = r - i ↔ ∃ s ∈ 𝒞, B ⊆ s ∧ #(s \ B) = i
have h : B ⊆ range'k ∧ #B = r - i → ∃ s ∈ 𝒞, B ⊆ s ∧ #(s \ B) = i
Tactic: constructor