awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.Compactness (hypothesis)
Goal:
α : Type u_1
β : α → Type u_2
inst : ∀ (a : α), Finite.{u_2 + 1} (β a)
g : Finset α → (a : α) → β a
instTop : (a : α) → TopologicalSpace (β a) := fun (a : α) ↦ ⊥
instDiscr : ∀ (a : α), DiscreteTopology.{u_2} (β a)
e : (s : Finset α) → Set ((a : α) → β a) :=
  fun (s : Finset α) ↦ {f : (a : α) → β a | ∃ (t : Finset α), s ⊆ t ∧ ∀ x ∈ s, f x = g t x}
this :
  ∀ (s : Finset α),
    s.restrict (π := β) ⁻¹' {f : (i : ↥s) → β (↑i : α) | ∃ (t : Finset α), s ⊆ t ∧ ∀ (x : ↥s), f x = g t (↑x : α)} = e s
he' : ∀ (s : Finset α), IsClosed (e s)
⊢ ∃ (χ : (a : α) → β a), ∀ (s : Finset α), ∃ (t : Finset α), s ⊆ t ∧ ∀ x ∈ s, χ x = g t x
have he'' : ∀ (B : Finset (Finset α)), Set.Nonempty (α := (a : α) → β a) (⋂ i ∈ B, e i)
Tactic: have he'' (B : Finset (Finset α)) : (⋂ i ∈ B, e i).Nonempty := by
    refine ⟨g (B.biUnion id), ?_⟩
    simp only [Set.mem_iInter, Set.mem_setOf_eq, e]
    intro i hi
    exact ⟨_, subset_biUnion_of_mem id hi, by simp⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Compactness (goal)
Goal:
α : Type u_1
β : α → Type u_2
inst : ∀ (a : α), Finite.{u_2 + 1} (β a)
g : Finset α → (a : α) → β a
let let₁ let₂ : ∃ (χ : (a : α) → β a), ∀ (s : Finset α), ∃ (t : Finset α), s ⊆ t ∧ ∀ x ∈ s, χ x = g t x
⊢ ∃ (χ : (a : α) → β a), ∀ (s : Finset α), ∃ (t : Finset α), s ⊆ t ∧ ∀ x ∈ s, χ x = g t x
have let₃ : let instTop : (a : α) → TopologicalSpace (β a) := fun (a : α) ↦ ⊥;
∀ (instDiscr : ∀ (a : α), DiscreteTopology.{u_2} (β a)),
  ∃ (χ : (a : α) → β a), ∀ (s : Finset α), ∃ (t : Finset α), s ⊆ t ∧ ∀ x ∈ s, χ x = g t x
Tactic: classical
  let instTop (a : α) : TopologicalSpace (β a) := ⊥
  have instDiscr (a : α) : DiscreteTopology (β a) := discreteTopology_bot _
  let e (s : Finset α) : Set ((a : α) → β a) := {f | ∃ t, s ⊆ t ∧ ∀ x ∈ s, f x = g t x}
  have (s : Finset α) : s.restrict ⁻¹' {f | ∃ t, s ⊆ t ∧ ∀ x, f x = g t x} = e s := by simp [e]
  have he' (s : Finset α) : IsClosed (e s) := by
    rw [← this]
    exact (isClosed_discrete _).preimage (by fun_prop)
  have he'' (B : Finset (Finset α)) : (⋂ i ∈ B, e i).Nonempty := by
    refine ⟨g (B.biUnion id), ?_⟩
    simp only [Set.mem_iInter, Set.mem_setOf_eq, e]
    intro i hi
    exact ⟨_, subset_biUnion_of_mem id hi, by simp⟩
  simpa using CompactSpace.iInter_nonempty he' he''
-- Lean 4 proof step from Mathlib.Combinatorics.Compactness (goal)
Goal:
α : Type u_1
β : α → Type u_2
inst : ∀ (a : α), Finite.{u_2 + 1} (β a)
g : Finset α → (a : α) → β a
let let₁ let₂ : ∃ (χ : (a : α) → β a), ∀ (s : Finset α), ∃ (t : Finset α), s ⊆ t ∧ ∀ x ∈ s, χ x = g t x
let₃ let₄ :
  let instTop : (a : α) → TopologicalSpace (β a) := fun (a : α) ↦ ⊥;
  ∀ (instDiscr : ∀ (a : α), DiscreteTopology.{u_2} (β a)),
    ∃ (χ : (a : α) → β a), ∀ (s : Finset α), ∃ (t : Finset α), s ⊆ t ∧ ∀ x ∈ s, χ x = g t x
⊢ ∃ (χ : (a : α) → β a), ∀ (s : Finset α), ∃ (t : Finset α), s ⊆ t ∧ ∀ x ∈ s, χ x = g t x
have let₅ : let instTop : (a : α) → TopologicalSpace (β a) := fun (a : α) ↦ ⊥;
∀ (instDiscr : ∀ (a : α), DiscreteTopology.{u_2} (β a)),
  let e : (s : Finset α) → Set ((a : α) → β a) := fun (s : Finset α) ↦
    {f : (a : α) → β a | ∃ (t : Finset α), s ⊆ t ∧ ∀ x ∈ s, f x = g t x};
  ∀
    (this :
      ∀ (s : Finset α),
        s.restrict (π := β) ⁻¹' {f : (i : ↥s) → β (↑i : α) | ∃ (t : Finset α), s ⊆ t ∧ ∀ (x : ↥s), f x = g t (↑x : α)} =
          e s),
    ∃ (χ : (a : α) → β a), ∀ (s : Finset α), ∃ (t : Finset α), s ⊆ t ∧ ∀ x ∈ s, χ x = g t x
Tactic: classical
  let instTop (a : α) : TopologicalSpace (β a) := ⊥
  have instDiscr (a : α) : DiscreteTopology (β a) := discreteTopology_bot _
  let e (s : Finset α) : Set ((a : α) → β a) := {f | ∃ t, s ⊆ t ∧ ∀ x ∈ s, f x = g t x}
  have (s : Finset α) : s.restrict ⁻¹' {f | ∃ t, s ⊆ t ∧ ∀ x, f x = g t x} = e s := by simp [e]
  have he' (s : Finset α) : IsClosed (e s) := by
    rw [← this]
    exact (isClosed_discrete _).preimage (by fun_prop)
  have he'' (B : Finset (Finset α)) : (⋂ i ∈ B, e i).Nonempty := by
    refine ⟨g (B.biUnion id), ?_⟩
    simp only [Set.mem_iInter, Set.mem_setOf_eq, e]
    intro i hi
    exact ⟨_, subset_biUnion_of_mem id hi, by simp⟩
  simpa using CompactSpace.iInter_nonempty he' he''
-- Lean 4 proof step from Mathlib.Combinatorics.Compactness (goal)
Goal:
α : Type u_1
β : α → Type u_2
inst : ∀ (a : α), Finite.{u_2 + 1} (β a)
g : Finset α → (a : α) → β a
let let₁ let₂ : ∃ (χ : (a : α) → β a), ∀ (s : Finset α), ∃ (t : Finset α), s ⊆ t ∧ ∀ x ∈ s, χ x = g t x
let₃ let₄ :
  let instTop : (a : α) → TopologicalSpace (β a) := fun (a : α) ↦ ⊥;
  ∀ (instDiscr : ∀ (a : α), DiscreteTopology.{u_2} (β a)),
    ∃ (χ : (a : α) → β a), ∀ (s : Finset α), ∃ (t : Finset α), s ⊆ t ∧ ∀ x ∈ s, χ x = g t x
let₅ :
  let instTop : (a : α) → TopologicalSpace (β a) := fun (a : α) ↦ ⊥;
  ∀ (instDiscr : ∀ (a : α), DiscreteTopology.{u_2} (β a)),
    let e : (s : Finset α) → Set ((a : α) → β a) := fun (s : Finset α) ↦
      {f : (a : α) → β a | ∃ (t : Finset α), s ⊆ t ∧ ∀ x ∈ s, f x = g t x};
    ∀
      (this :
        ∀ (s : Finset α),
          s.restrict (π := β) ⁻¹'
              {f : (i : ↥s) → β (↑i : α) | ∃ (t : Finset α), s ⊆ t ∧ ∀ (x : ↥s), f x = g t (↑x : α)} =
            e s),
      ∃ (χ : (a : α) → β a), ∀ (s : Finset α), ∃ (t : Finset α), s ⊆ t ∧ ∀ x ∈ s, χ x = g t x
⊢ ∃ (χ : (a : α) → β a), ∀ (s : Finset α), ∃ (t : Finset α), s ⊆ t ∧ ∀ x ∈ s, χ x = g t x
have let₆ : let instTop : (a : α) → TopologicalSpace (β a) := fun (a : α) ↦ ⊥;
∀ (instDiscr : ∀ (a : α), DiscreteTopology.{u_2} (β a)),
  let e : (s : Finset α) → Set ((a : α) → β a) := fun (s : Finset α) ↦
    {f : (a : α) → β a | ∃ (t : Finset α), s ⊆ t ∧ ∀ x ∈ s, f x = g t x};
  ∀
    (this :
      ∀ (s : Finset α),
        s.restrict (π := β) ⁻¹' {f : (i : ↥s) → β (↑i : α) | ∃ (t : Finset α), s ⊆ t ∧ ∀ (x : ↥s), f x = g t (↑x : α)} =
          e s)
    (he' : ∀ (s : Finset α), IsClosed (e s)),
    ∃ (χ : (a : α) → β a), ∀ (s : Finset α), ∃ (t : Finset α), s ⊆ t ∧ ∀ x ∈ s, χ x = g t x
Tactic: classical
  let instTop (a : α) : TopologicalSpace (β a) := ⊥
  have instDiscr (a : α) : DiscreteTopology (β a) := discreteTopology_bot _
  let e (s : Finset α) : Set ((a : α) → β a) := {f | ∃ t, s ⊆ t ∧ ∀ x ∈ s, f x = g t x}
  have (s : Finset α) : s.restrict ⁻¹' {f | ∃ t, s ⊆ t ∧ ∀ x, f x = g t x} = e s := by simp [e]
  have he' (s : Finset α) : IsClosed (e s) := by
    rw [← this]
    exact (isClosed_discrete _).preimage (by fun_prop)
  have he'' (B : Finset (Finset α)) : (⋂ i ∈ B, e i).Nonempty := by
    refine ⟨g (B.biUnion id), ?_⟩
    simp only [Set.mem_iInter, Set.mem_setOf_eq, e]
    intro i hi
    exact ⟨_, subset_biUnion_of_mem id hi, by simp⟩
  simpa using CompactSpace.iInter_nonempty he' he''
-- Lean 4 proof step from Mathlib.Combinatorics.Compactness (hypothesis)
Goal:
α : Type u_1
β : α → Type u_2
inst : ∀ (a : α), Finite.{u_2 + 1} (β a)
g : (s : Finset α) → (a : ↥s) → β (↑a : α)
⊢ ∃ (χ : (a : α) → β a),
    ∀ (s : Finset α),
      ∃ (t : Finset α) (hst : s ⊆ t),
        ∀ (x : ↥s),
          Eq (α := β (↑x : α)) (χ (↑x : α) : β (↑x : α))
            (g t (Set.inclusion (s := (↑s : Set α)) (t := (↑t : Set α)) hst x) :
              β (↑(Set.inclusion (s := (↑s : Set α)) (t := (↑t : Set α)) hst x) : α))
have this : ∀ (a : α), Nonempty.{u_2 + 1} (β a)
Tactic: have (a : α) : Nonempty (β a) := ⟨g {a} ⟨a, by simp⟩⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Compactness (hypothesis)
Goal:
α : Type u_1
β : α → Type u_2
inst : ∀ (a : α), Finite.{u_2 + 1} (β a)
g : (s : Finset α) → (a : ↥s) → β (↑a : α)
this : ∀ (a : α), Nonempty.{u_2 + 1} (β a)
g' : (s : Finset α) → (a : α) → β a :=
  fun (s : Finset α) (a : α) ↦
    if ha : a ∈ s then g s (Subtype.mk (p := fun (x : α) ↦ x ∈ s) a ha) else Classical.arbitrary (β a)
⊢ ∃ (χ : (a : α) → β a),
    ∀ (s : Finset α),
      ∃ (t : Finset α) (hst : s ⊆ t),
        ∀ (x : ↥s),
          Eq (α := β (↑x : α)) (χ (↑x : α) : β (↑x : α))
            (g t (Set.inclusion (s := (↑s : Set α)) (t := (↑t : Set α)) hst x) :
              β (↑(Set.inclusion (s := (↑s : Set α)) (t := (↑t : Set α)) hst x) : α))
have hg : ∀ (s : Finset α) (x : ↥s), g s x = g' s (↑x : α)
Tactic: have hg (s : Finset α) (x : s) : g s x = g' s x := by simp [g']
-- Lean 4 proof step from Mathlib.Combinatorics.Compactness (goal)
Goal:
α : Type u_1
β : α → Type u_2
inst : ∀ (a : α), Finite.{u_2 + 1} (β a)
g : (s : Finset α) → (a : ↥s) → β (↑a : α)
⊢ ∃ (χ : (a : α) → β a),
    ∀ (s : Finset α),
      ∃ (t : Finset α) (hst : s ⊆ t),
        ∀ (x : ↥s),
          Eq (α := β (↑x : α)) (χ (↑x : α) : β (↑x : α))
            (g t (Set.inclusion (s := (↑s : Set α)) (t := (↑t : Set α)) hst x) :
              β (↑(Set.inclusion (s := (↑s : Set α)) (t := (↑t : Set α)) hst x) : α))
have have : ∀ (this : ∀ (a : α), Nonempty.{u_2 + 1} (β a)),
  ∃ (χ : (a : α) → β a),
    ∀ (s : Finset α),
      ∃ (t : Finset α) (hst : s ⊆ t),
        ∀ (x : ↥s),
          Eq (α := β (↑x : α)) (χ (↑x : α) : β (↑x : α))
            (g t (Set.inclusion (s := (↑s : Set α)) (t := (↑t : Set α)) hst x) :
              β (↑(Set.inclusion (s := (↑s : Set α)) (t := (↑t : Set α)) hst x) : α))
Tactic: classical
  have (a : α) : Nonempty (β a) := ⟨g {a} ⟨a, by simp⟩⟩
  let g' (s) (a : α) : β a := if ha : a ∈ s then g s ⟨a, ha⟩ else Classical.arbitrary (β a)
  have hg (s : Finset α) (x : s) : g s x = g' s x := by simp [g']
  simpa [hg] using Finset.rado_selection g'
-- Lean 4 proof step from Mathlib.Combinatorics.Compactness (goal)
Goal:
α : Type u_1
β : α → Type u_2
inst : ∀ (a : α), Finite.{u_2 + 1} (β a)
g : (s : Finset α) → (a : ↥s) → β (↑a : α)
have have₁ have₂ have₃ :
  ∀ (this : ∀ (a : α), Nonempty.{u_2 + 1} (β a)),
    ∃ (χ : (a : α) → β a),
      ∀ (s : Finset α),
        ∃ (t : Finset α) (hst : s ⊆ t),
          ∀ (x : ↥s),
            Eq (α := β (↑x : α)) (χ (↑x : α) : β (↑x : α))
              (g t (Set.inclusion (s := (↑s : Set α)) (t := (↑t : Set α)) hst x) :
                β (↑(Set.inclusion (s := (↑s : Set α)) (t := (↑t : Set α)) hst x) : α))
⊢ ∃ (χ : (a : α) → β a),
    ∀ (s : Finset α),
      ∃ (t : Finset α) (hst : s ⊆ t),
        ∀ (x : ↥s),
          Eq (α := β (↑x : α)) (χ (↑x : α) : β (↑x : α))
            (g t (Set.inclusion (s := (↑s : Set α)) (t := (↑t : Set α)) hst x) :
              β (↑(Set.inclusion (s := (↑s : Set α)) (t := (↑t : Set α)) hst x) : α))
have have₄ : ∀ (this : ∀ (a : α), Nonempty.{u_2 + 1} (β a)),
  let g' : (s : Finset α) → (a : α) → β a := fun (s : Finset α) (a : α) ↦
    if ha : a ∈ s then g s (Subtype.mk (p := fun (x : α) ↦ x ∈ s) a ha) else Classical.arbitrary (β a);
  ∀ (hg : ∀ (s : Finset α) (x : ↥s), g s x = g' s (↑x : α)),
    ∃ (χ : (a : α) → β a),
      ∀ (s : Finset α),
        ∃ (t : Finset α) (hst : s ⊆ t),
          ∀ (x : ↥s),
            Eq (α := β (↑x : α)) (χ (↑x : α) : β (↑x : α))
              (g t (Set.inclusion (s := (↑s : Set α)) (t := (↑t : Set α)) hst x) :
                β (↑(Set.inclusion (s := (↑s : Set α)) (t := (↑t : Set α)) hst x) : α))
Tactic: classical
  have (a : α) : Nonempty (β a) := ⟨g {a} ⟨a, by simp⟩⟩
  let g' (s) (a : α) : β a := if ha : a ∈ s then g s ⟨a, ha⟩ else Classical.arbitrary (β a)
  have hg (s : Finset α) (x : s) : g s x = g' s x := by simp [g']
  simpa [hg] using Finset.rado_selection g'
-- Lean 4 proof step from Mathlib.Combinatorics.Compactness (goal)
Goal:
α : Type u_1
β : α → Type u_2
inst : ∀ (a : α), Finite.{u_2 + 1} (β a)
g : (s : Set α) → s.Finite → (a : α) → β a
⊢ ∃ (χ : (a : α) → β a), ∀ (s : Set α), s.Finite → ∃ (t : Set α) (ht : t.Finite), s ⊆ t ∧ ∀ x ∈ s, χ x = g t ht x
have obtain : ∀ (χ : (a : α) → β a) (hχ : ∀ (s : Finset α), ∃ (t : Finset α), s ⊆ t ∧ ∀ x ∈ s, χ x = g (↑t : Set α) sorry x),
  ∃ (χ : (a : α) → β a), ∀ (s : Set α), s.Finite → ∃ (t : Set α) (ht : t.Finite), s ⊆ t ∧ ∀ x ∈ s, χ x = g t ht x
Tactic: obtain ⟨χ, hχ⟩ := Finset.rado_selection (fun s ↦ g s s.finite_toSet)
-- Lean 4 proof step from Mathlib.Combinatorics.Compactness (goal)
Goal:
α : Type u_1
β : α → Type u_2
inst : ∀ (a : α), Finite.{u_2 + 1} (β a)
g : (s : Set α) → s.Finite → (a : α) → β a
χ : (a : α) → β a
hχ : ∀ (s : Finset α), ∃ (t : Finset α), s ⊆ t ∧ ∀ x ∈ s, χ x = g (↑t : Set α) ⋯ x
⊢ ∃ (χ : (a : α) → β a), ∀ (s : Set α), s.Finite → ∃ (t : Set α) (ht : t.Finite), s ⊆ t ∧ ∀ x ∈ s, χ x = g t ht x
have refine : ∀ (s : Set α) (hs : s.Finite), ∃ (t : Set α) (ht : t.Finite), s ⊆ t ∧ ∀ x ∈ s, χ x = g t ht x
Tactic: refine ⟨χ, fun s hs ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Compactness (goal)
Goal:
α : Type u_1
β : α → Type u_2
inst : ∀ (a : α), Finite.{u_2 + 1} (β a)
g : (s : Set α) → s.Finite → (a : α) → β a
χ : (a : α) → β a
hχ : ∀ (s : Finset α), ∃ (t : Finset α), s ⊆ t ∧ ∀ x ∈ s, χ x = g (↑t : Set α) ⋯ x
s : Set α
hs : s.Finite
⊢ ∃ (t : Set α) (ht : t.Finite), s ⊆ t ∧ ∀ x ∈ s, χ x = g t ht x
have obtain : ∀ (t : Finset α) (ht : hs.toFinset (s := s) ⊆ t) (ht' : ∀ x ∈ hs.toFinset (s := s), χ x = g (↑t : Set α) sorry x),
  ∃ (t : Set α) (ht : t.Finite), s ⊆ t ∧ ∀ x ∈ s, χ x = g t ht x
Tactic: obtain ⟨t, ht, ht'⟩ := hχ hs.toFinset
-- Lean 4 proof step from Mathlib.Combinatorics.Compactness (goal)
Goal:
α : Type u_1
β : α → Type u_2
inst : ∀ (a : α), Finite.{u_2 + 1} (β a)
g : (s : Set α) → s.Finite → (a : (↑s : Type u_1)) → β (↑a : α)
⊢ ∃ (χ : (a : α) → β a),
    ∀ (s : Set α),
      s.Finite →
        ∃ (t : Set α) (ht : t.Finite) (hst : s ⊆ t),
          ∀ (x : (↑s : Type u_1)),
            Eq (α := β (↑x : α)) (χ (↑x : α) : β (↑x : α))
              (g t ht (inclusion (s := s) (t := t) hst x) : β (↑(inclusion (s := s) (t := t) hst x) : α))
have obtain : ∀ (χ : (a : α) → β a)
  (hχ :
    ∀ (s : Finset α),
      ∃ (t : Finset α) (hst : s ⊆ t),
        ∀ (x : ↥s),
          Eq (α := β (↑x : α)) (χ (↑x : α) : β (↑x : α))
            (g (↑t : Set α) sorry (inclusion (s := (↑s : Set α)) (t := (↑t : Set α)) hst x) :
              β (↑(inclusion (s := (↑s : Set α)) (t := (↑t : Set α)) hst x) : α))),
  ∃ (χ : (a : α) → β a),
    ∀ (s : Set α),
      s.Finite →
        ∃ (t : Set α) (ht : t.Finite) (hst : s ⊆ t),
          ∀ (x : (↑s : Type u_1)),
            Eq (α := β (↑x : α)) (χ (↑x : α) : β (↑x : α))
              (g t ht (inclusion (s := s) (t := t) hst x) : β (↑(inclusion (s := s) (t := t) hst x) : α))
Tactic: obtain ⟨χ, hχ⟩ := Finset.rado_selection_subtype (β := β) (fun s ↦ g s s.finite_toSet)
-- Lean 4 proof step from Mathlib.Combinatorics.Compactness (goal)
Goal:
α : Type u_1
β : α → Type u_2
inst : ∀ (a : α), Finite.{u_2 + 1} (β a)
g : (s : Set α) → s.Finite → (a : (↑s : Type u_1)) → β (↑a : α)
χ : (a : α) → β a
hχ :
  ∀ (s : Finset α),
    ∃ (t : Finset α) (hst : s ⊆ t),
      ∀ (x : ↥s),
        Eq (α := β (↑x : α)) (χ (↑x : α) : β (↑x : α))
          (g (↑t : Set α) ⋯ (inclusion (s := (↑s : Set α)) (t := (↑t : Set α)) hst x) :
            β (↑(inclusion (s := (↑s : Set α)) (t := (↑t : Set α)) hst x) : α))
⊢ ∃ (χ : (a : α) → β a),
    ∀ (s : Set α),
      s.Finite →
        ∃ (t : Set α) (ht : t.Finite) (hst : s ⊆ t),
          ∀ (x : (↑s : Type u_1)),
            Eq (α := β (↑x : α)) (χ (↑x : α) : β (↑x : α))
              (g t ht (inclusion (s := s) (t := t) hst x) : β (↑(inclusion (s := s) (t := t) hst x) : α))
have refine : ∀ (s : Set α) (hs : s.Finite),
  ∃ (t : Set α) (ht : t.Finite) (hst : s ⊆ t),
    ∀ (x : (↑s : Type u_1)),
      Eq (α := β (↑x : α)) (χ (↑x : α) : β (↑x : α))
        (g t ht (inclusion (s := s) (t := t) hst x) : β (↑(inclusion (s := s) (t := t) hst x) : α))
Tactic: refine ⟨χ, fun s hs ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Compactness (goal)
Goal:
α : Type u_1
β : α → Type u_2
inst : ∀ (a : α), Finite.{u_2 + 1} (β a)
g : (s : Set α) → s.Finite → (a : (↑s : Type u_1)) → β (↑a : α)
χ : (a : α) → β a
hχ :
  ∀ (s : Finset α),
    ∃ (t : Finset α) (hst : s ⊆ t),
      ∀ (x : ↥s),
        Eq (α := β (↑x : α)) (χ (↑x : α) : β (↑x : α))
          (g (↑t : Set α) ⋯ (inclusion (s := (↑s : Set α)) (t := (↑t : Set α)) hst x) :
            β (↑(inclusion (s := (↑s : Set α)) (t := (↑t : Set α)) hst x) : α))
s : Set α
hs : s.Finite
⊢ ∃ (t : Set α) (ht : t.Finite) (hst : s ⊆ t),
    ∀ (x : (↑s : Type u_1)),
      Eq (α := β (↑x : α)) (χ (↑x : α) : β (↑x : α))
        (g t ht (inclusion (s := s) (t := t) hst x) : β (↑(inclusion (s := s) (t := t) hst x) : α))
have obtain : ∀ (t : Finset α) (ht : hs.toFinset (s := s) ⊆ t)
  (hst :
    ∀ (x : ↥(hs.toFinset (s := s))),
      Eq (α := β (↑x : α)) (χ (↑x : α) : β (↑x : α))
        (g (↑t : Set α) sorry (inclusion (s := (↑(hs.toFinset (s := s)) : Set α)) (t := (↑t : Set α)) ht x) :
          β (↑(inclusion (s := (↑(hs.toFinset (s := s)) : Set α)) (t := (↑t : Set α)) ht x) : α))),
  ∃ (t : Set α) (ht : t.Finite) (hst : s ⊆ t),
    ∀ (x : (↑s : Type u_1)),
      Eq (α := β (↑x : α)) (χ (↑x : α) : β (↑x : α))
        (g t ht (inclusion (s := s) (t := t) hst x) : β (↑(inclusion (s := s) (t := t) hst x) : α))
Tactic: obtain ⟨t, ht, hst⟩ := hχ hs.toFinset
-- Lean 4 proof step from Mathlib.Combinatorics.Compactness (hypothesis)
Goal:
α : Type u_1
β : α → Type u_2
inst : ∀ (a : α), Finite.{u_2 + 1} (β a)
g : (s : Set α) → s.Finite → (a : (↑s : Type u_1)) → β (↑a : α)
χ : (a : α) → β a
hχ :
  ∀ (s : Finset α),
    ∃ (t : Finset α) (hst : s ⊆ t),
      ∀ (x : ↥s),
        Eq (α := β (↑x : α)) (χ (↑x : α) : β (↑x : α))
          (g (↑t : Set α) ⋯ (inclusion (s := (↑s : Set α)) (t := (↑t : Set α)) hst x) :
            β (↑(inclusion (s := (↑s : Set α)) (t := (↑t : Set α)) hst x) : α))
s : Set α
hs : s.Finite
t : Finset α
ht : hs.toFinset (s := s) ⊆ t
hst :
  ∀ (x : ↥(hs.toFinset (s := s))),
    Eq (α := β (↑x : α)) (χ (↑x : α) : β (↑x : α))
      (g (↑t : Set α) ⋯ (inclusion (s := (↑(hs.toFinset (s := s)) : Set α)) (t := (↑t : Set α)) ht x) :
        β (↑(inclusion (s := (↑(hs.toFinset (s := s)) : Set α)) (t := (↑t : Set α)) ht x) : α))
⊢ ∃ (t : Set α) (ht : t.Finite) (hst : s ⊆ t),
    ∀ (x : (↑s : Type u_1)),
      Eq (α := β (↑x : α)) (χ (↑x : α) : β (↑x : α))
        (g t ht (inclusion (s := s) (t := t) hst x) : β (↑(inclusion (s := s) (t := t) hst x) : α))
have ht₁ : s ⊆ (↑t : Set α)
Tactic: simp only [Set.Finite.toFinset_subset] at ht
-- Lean 4 proof step from Mathlib.Combinatorics.Configuration (goal)
Goal:
P : Type u_1
L : Type u_2
inst : Membership P L
inst_1 : Nondegenerate P L
inst_2 : Fintype P
inst_3 : Fintype L
h : Fintype.card L ≤ Fintype.card P
t : L → Finset P := fun (l : L) ↦ Set.toFinset {p : P | p ∉ l}
this : ∀ (s : Finset L), #s ≤ #(s.biUnion t)
⊢ ∃ (f : L → P), Function.Injective f ∧ ∀ (l : L), f l ∉ l
have obtain : ∀ (f : L → P) (hf1 : Function.Injective f) (hf2 : ∀ (x : L), f x ∈ t x),
  ∃ (f : L → P), Function.Injective f ∧ ∀ (l : L), f l ∉ l
Tactic: obtain ⟨f, hf1, hf2⟩ := (Finset.all_card_le_biUnion_card_iff_exists_injective t).mp this
-- Lean 4 proof step from Mathlib.Combinatorics.Configuration (goal)
Goal:
P : Type u_1
L : Type u_2
inst : Membership P L
inst_1 : Nondegenerate P L
inst_2 : Fintype P
inst_3 : Fintype L
h : Fintype.card L ≤ Fintype.card P
t : L → Finset P := fun (l : L) ↦ Set.toFinset {p : P | p ∉ l}
⊢ ∃ (f : L → P), Function.Injective f ∧ ∀ (l : L), f l ∉ l
have suffices : ∀ (s : Finset L), #s ≤ #(s.biUnion t)
Tactic: suffices ∀ s : Finset L, #s ≤ (s.biUnion t).card by
      -- Hall's marriage theorem
      obtain ⟨f, hf1, hf2⟩ := (Finset.all_card_le_biUnion_card_iff_exists_injective t).mp this
      exact ⟨f, hf1, fun l => Set.mem_toFinset.mp (hf2 l)⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Configuration (goal)
Goal:
P : Type u_1
L : Type u_2
inst : Membership P L
inst_1 : Nondegenerate P L
inst_2 : Fintype P
inst_3 : Fintype L
h : Fintype.card L ≤ Fintype.card P
t : L → Finset P := fun (l : L) ↦ Set.toFinset {p : P | p ∉ l}
s : Finset L
⊢ #s ≤ #(s.biUnion t)
have pos : ∀ (hs₀ : #s = 0), #s ≤ #(s.biUnion t)
Tactic: by_cases hs₀ : #s = 0
-- Lean 4 proof step from Mathlib.Combinatorics.Configuration (goal)
Goal:
P : Type u_1
L : Type u_2
inst : Membership P L
inst_1 : Nondegenerate P L
inst_2 : Fintype P
inst_3 : Fintype L
h : Fintype.card L ≤ Fintype.card P
t : L → Finset P := fun (l : L) ↦ Set.toFinset {p : P | p ∉ l}
s : Finset L
pos : ∀ (hs₀ : #s = 0), #s ≤ #(s.biUnion t)
⊢ #s ≤ #(s.biUnion t)
have neg : ∀ (hs₀ : ¬#s = 0), #s ≤ #(s.biUnion t)
Tactic: by_cases hs₀ : #s = 0
-- Lean 4 proof step from Mathlib.Combinatorics.Configuration (goal)
Goal:
P : Type u_1
L : Type u_2
inst : Membership P L
inst_1 : Nondegenerate P L
inst_2 : Fintype P
inst_3 : Fintype L
h : Fintype.card L ≤ Fintype.card P
t : L → Finset P := fun (l : L) ↦ Set.toFinset {p : P | p ∉ l}
s : Finset L
hs₀ : #s = 0
⊢ #s ≤ #(s.biUnion t)
have pos : 0 ≤ #(s.biUnion t)
Tactic: simp_rw [hs₀, zero_le]
-- Lean 4 proof step from Mathlib.Combinatorics.Configuration (goal)
Goal:
P : Type u_1
L : Type u_2
inst : Membership P L
inst_1 : Nondegenerate P L
inst_2 : Fintype P
inst_3 : Fintype L
h : Fintype.card L ≤ Fintype.card P
t : L → Finset P := fun (l : L) ↦ Set.toFinset {p : P | p ∉ l}
s : Finset L
hs₀ : ¬#s = 0
⊢ #s ≤ #(s.biUnion t)
have pos : ∀ (hs₁ : #s = 1), #s ≤ #(s.biUnion t)
Tactic: by_cases hs₁ : #s = 1
-- Lean 4 proof step from Mathlib.Combinatorics.Configuration (goal)
Goal:
P : Type u_1
L : Type u_2
inst : Membership P L
inst_1 : Nondegenerate P L
inst_2 : Fintype P
inst_3 : Fintype L
h : Fintype.card L ≤ Fintype.card P
t : L → Finset P := fun (l : L) ↦ Set.toFinset {p : P | p ∉ l}
s : Finset L
hs₀ : ¬#s = 0
pos : ∀ (hs₁ : #s = 1), #s ≤ #(s.biUnion t)
⊢ #s ≤ #(s.biUnion t)
have neg : ∀ (hs₁ : ¬#s = 1), #s ≤ #(s.biUnion t)
Tactic: by_cases hs₁ : #s = 1
-- Lean 4 proof step from Mathlib.Combinatorics.Configuration (goal)
Goal:
P : Type u_1
L : Type u_2
inst : Membership P L
inst_1 : Nondegenerate P L
inst_2 : Fintype P
inst_3 : Fintype L
h : Fintype.card L ≤ Fintype.card P
t : L → Finset P := fun (l : L) ↦ Set.toFinset {p : P | p ∉ l}
s : Finset L
hs₀ : ¬#s = 0
hs₁ : #s = 1
⊢ #s ≤ #(s.biUnion t)
have pos : ∀ (l : L) (hs₀ : ¬card (α := L) {l} = 0) (hs₁ : card (α := L) {l} = 1), card (α := L) {l} ≤ #(Finset.biUnion {l} t)
Tactic: obtain ⟨l, rfl⟩ := Finset.card_eq_one.mp hs₁
Cleared hypotheses: s, hs₀, hs₁
-- Lean 4 proof step from Mathlib.Combinatorics.Configuration (goal)
Goal:
P : Type u_1
L : Type u_2
inst : Membership P L
inst_1 : Nondegenerate P L
inst_2 : Fintype P
inst_3 : Fintype L
h : Fintype.card L ≤ Fintype.card P
t : L → Finset P := fun (l : L) ↦ Set.toFinset {p : P | p ∉ l}
l : L
hs₀ : ¬card (α := L) {l} = 0
hs₁ : card (α := L) {l} = 1
⊢ card (α := L) {l} ≤ #(Finset.biUnion {l} t)
have pos : ∀ (p : P) (hl : p ∉ l), card (α := L) {l} ≤ #(Finset.biUnion {l} t)
Tactic: obtain ⟨p, hl⟩ := exists_point (P := P) l
-- Lean 4 proof step from Mathlib.Combinatorics.Configuration (goal)
Goal:
P : Type u_1
L : Type u_2
inst : Membership P L
inst_1 : Nondegenerate P L
inst_2 : Fintype P
inst_3 : Fintype L
h : Fintype.card L ≤ Fintype.card P
t : L → Finset P := fun (l : L) ↦ Set.toFinset {p : P | p ∉ l}
l : L
hs₀ : ¬card (α := L) {l} = 0
hs₁ : card (α := L) {l} = 1
p : P
hl : p ∉ l
⊢ card (α := L) {l} ≤ #(Finset.biUnion {l} t)
have pos : #(t l) ≠ 0
Tactic: rw [Finset.card_singleton, Finset.singleton_biUnion, Nat.one_le_iff_ne_zero]
-- Lean 4 proof step from Mathlib.Combinatorics.Configuration (hypothesis)
Goal:
P : Type u_1
L : Type u_2
inst : Membership P L
inst_1 : Nondegenerate P L
inst_2 : Fintype P
inst_3 : Fintype L
h : Fintype.card L ≤ Fintype.card P
t : L → Finset P := fun (l : L) ↦ Set.toFinset {p : P | p ∉ l}
s : Finset L
hs₀ : ¬#s = 0
hs₁ : ¬#s = 1
this : #(s.biUnion t)ᶜ ≤ #sᶜ
⊢ #s ≤ #(s.biUnion t)
have this₁ : Fintype.card P ≤ #(s.biUnion t) + (Fintype.card L - #s)
Tactic: rw [Finset.card_compl, Finset.card_compl, tsub_le_iff_left] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Combinatorics.Configuration (hypothesis)
Goal:
P : Type u_1
L : Type u_2
inst : Membership P L
inst_1 : Nondegenerate P L
inst_2 : Fintype P
inst_3 : Fintype L
h : Fintype.card L ≤ Fintype.card P
t : L → Finset P := fun (l : L) ↦ Set.toFinset {p : P | p ∉ l}
s : Finset L
hs₀ : ¬#s = 0
hs₁ : ¬#s = 1
this : Fintype.card P ≤ #(s.biUnion t) + (Fintype.card L - #s)
⊢ #s ≤ #(s.biUnion t)
have this₁ : Fintype.card L ≤ #(s.biUnion t) + (Fintype.card L - #s)
Tactic: replace := h.trans this
Cleared hypotheses: this