awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.Compactness
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)
he'' : ∀ (B : Finset (Finset α)), Set.Nonempty (α := (a : α) → β a) (⋂ i ∈ B, e i)
⊢ ∃ (χ : (a : α) → β a), ∀ (s : Finset α), ∃ (t : Finset α), s ⊆ t ∧ ∀ x ∈ s, χ x = g t x

Tactic:
simpa using CompactSpace.iInter_nonempty he' he''

Premises used: CompactSpace.iInter_nonempty
-- Module: Mathlib.Combinatorics.Compactness
Goal:
α : Type u_1
β : α → Type u_2
inst : ∀ (a : α), Finite.{u_2 + 1} (β a)
g : (s : Finset α) → (a : ↥s) → β (↑a : α)
a : α
⊢ Membership.mem (γ := Finset α) {a} a

Tactic:
simp
-- Module: Mathlib.Combinatorics.Compactness
Goal:
α : Type u_1
β : α → Type u_2
inst : ∀ (a : α), Finite.{u_2 + 1} (β a)
g : (s : Finset α) → (a : ↥s) → β (↑a : α)
⊢ ∀ (a : α), Nonempty.{u_2 + 1} (β a)

Tactic:
have (a : α) : Nonempty (β a) := ⟨g {a} ⟨a, by simp⟩⟩
-- Module: Mathlib.Combinatorics.Compactness
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)
s : Finset α
x : ↥s
⊢ g s x = g' s (↑x : α)

Tactic:
simp [g']
-- Module: Mathlib.Combinatorics.Compactness
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)
⊢ ∀ (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']
-- Module: Mathlib.Combinatorics.Compactness
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)
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:
simpa [hg] using Finset.rado_selection g'

Premises used: Finset.rado_selection
-- Module: Mathlib.Combinatorics.Compactness
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) : α))
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) : α))
⊢ ∃ (χ : (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'
-- Module: Mathlib.Combinatorics.Compactness
Goal:
α : Type u_1
β : α → Type u_2
inst : ∀ (a : α), Finite.{u_2 + 1} (β a)
g : (s : Set α) → s.Finite → (a : α) → β a
obtain :
  ∀ (χ : (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
⊢ ∃ (χ : (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)

Premises used: Finset.rado_selection, SetLike.coe, Finset.finite_toSet
-- Module: Mathlib.Combinatorics.Compactness
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

Tactic:
⟨χ, fun s hs ↦ ?_⟩

Premises used: Exists.intro
-- Module: Mathlib.Combinatorics.Compactness
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
refine : ∀ (s : Set α) (hs : s.Finite), ∃ (t : Set α) (ht : t.Finite), s ⊆ t ∧ ∀ x ∈ s, χ x = g t ht x
⊢ ∃ (χ : (a : α) → β a), ∀ (s : Set α), s.Finite → ∃ (t : Set α) (ht : t.Finite), s ⊆ t ∧ ∀ x ∈ s, χ x = g t ht x

Tactic:
refine ⟨χ, fun s hs ↦ ?_⟩
-- Module: Mathlib.Combinatorics.Compactness
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
obtain :
  ∀ (t : Finset α) (ht : hs.toFinset (s := s) ⊆ t) (ht' : ∀ x ∈ hs.toFinset (s := s), χ x = g (↑t : Set α) ⋯ x),
    ∃ (t : Set α) (ht : t.Finite), s ⊆ t ∧ ∀ x ∈ s, χ x = g t ht x
⊢ ∃ (t : Set α) (ht : t.Finite), s ⊆ t ∧ ∀ x ∈ s, χ x = g t ht x

Tactic:
obtain ⟨t, ht, ht'⟩ := hχ hs.toFinset

Premises used: Set.Finite.toFinset
-- Module: Mathlib.Combinatorics.Compactness
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 : Finset α
ht : hs.toFinset (s := s) ⊆ t
ht' : ∀ x ∈ hs.toFinset (s := s), χ x = g (↑t : Set α) ⋯ x
⊢ ∃ (ht : (↑t : Set α).Finite), s ⊆ (↑t : Set α) ∧ ∀ x ∈ s, χ x = g (↑t : Set α) ht x

Tactic:
simp_all
-- Module: Mathlib.Combinatorics.Compactness
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 : Finset α
ht : hs.toFinset (s := s) ⊆ t
ht' : ∀ x ∈ hs.toFinset (s := s), χ x = g (↑t : Set α) ⋯ x
⊢ ∃ (t : Set α) (ht : t.Finite), s ⊆ t ∧ ∀ x ∈ s, χ x = g t ht x

Tactic:
exact ⟨t, by simp_all⟩
-- Module: Mathlib.Combinatorics.Compactness
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 : α)
obtain :
  ∀ (χ : (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) : α))
⊢ ∃ (χ : (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)

Premises used: SetLike.coe, Finset.finite_toSet, Finset.rado_selection_subtype
-- Module: Mathlib.Combinatorics.Compactness
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) : α))

Tactic:
⟨χ, fun s hs ↦ ?_⟩

Premises used: Exists.intro
-- Module: Mathlib.Combinatorics.Compactness
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) : α))
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) : α))
⊢ ∃ (χ : (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:
refine ⟨χ, fun s hs ↦ ?_⟩
-- Module: Mathlib.Combinatorics.Compactness
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
obtain :
  ∀ (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) : α))
⊢ ∃ (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

Premises used: Set.Finite.toFinset
-- Module: Mathlib.Combinatorics.Compactness
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) : α))
⊢ s ⊆ (↑t : Set α)

Tactic:
simp only [Set.Finite.toFinset_subset] at ht

Premises used: Set.Finite.toFinset_subset
-- Module: Mathlib.Combinatorics.Compactness
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_1 : 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_1 x) :
        β (↑(inclusion (s := (↑(hs.toFinset (s := s)) : Set α)) (t := (↑t : Set α)) ht_1 x) : α))
ht : s ⊆ (↑t : Set α)
⊢ ∃ (ht : (↑t : Set α).Finite) (hst : s ⊆ (↑t : Set α)),
    ∀ (x : (↑s : Type u_1)),
      Eq (α := β (↑x : α)) (χ (↑x : α) : β (↑x : α))
        (g (↑t : Set α) ht (inclusion (s := s) (t := (↑t : Set α)) hst x) :
          β (↑(inclusion (s := s) (t := (↑t : Set α)) hst x) : α))

Tactic:
simp_all
-- Module: Mathlib.Combinatorics.Compactness
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_1 : 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_1 x) :
        β (↑(inclusion (s := (↑(hs.toFinset (s := s)) : Set α)) (t := (↑t : Set α)) ht_1 x) : α))
ht : s ⊆ (↑t : Set α)
⊢ ∃ (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:
exact ⟨t, by simp_all⟩
-- Module: Mathlib.Combinatorics.Configuration
Goal:
P : Type u_1
L : Type u_2
inst : Membership P L
inst_1 : HasPoints P L
l₁ l₂ : L
hl : l₁ ≠ l₂
⊢ ∃! p : P, p ∈ l₁ ∧ p ∈ l₂

Tactic:
⟨mkPoint hl, mkPoint_ax hl, fun _ hp =>
    (eq_or_eq hp.1 (mkPoint_ax hl).1 hp.2 (mkPoint_ax hl).2).resolve_right hl⟩

Premises used: Configuration.Nondegenerate.eq_or_eq, Configuration.HasPoints.mkPoint_ax, And.right, And.left, ExistsUnique, And.intro, Configuration.HasPoints.mkPoint, Exists.intro, Or.resolve_right
-- Module: Mathlib.Combinatorics.Configuration
Goal:
P : Type u_1
L : Type u_2
inst : Membership P L
inst_1 : HasLines P L
p₁ p₂ : P
hp : p₁ ≠ p₂
⊢ ∃! l : L, p₁ ∈ l ∧ p₂ ∈ l

Tactic:
HasPoints.existsUnique_point (Dual L) (Dual P) p₁ p₂ hp

Premises used: Configuration.Dual, Configuration.HasPoints.existsUnique_point
-- Module: Mathlib.Combinatorics.Configuration
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)
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
⊢ ∃ (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

Premises used: Finset.all_card_le_biUnion_card_iff_exists_injective, Iff.mp
-- Module: Mathlib.Combinatorics.Configuration
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
hf1 : Function.Injective f
hf2 : ∀ (x : L), f x ∈ t x
⊢ ∃ (f : L → P), Function.Injective f ∧ ∀ (l : L), f l ∉ l

Tactic:
⟨f, hf1, fun l => Set.mem_toFinset.mp (hf2 l)⟩

Premises used: And.intro, Exists.intro, Iff.mp, Set.mem_toFinset
-- Module: Mathlib.Combinatorics.Configuration
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
hf1 : Function.Injective f
hf2 : ∀ (x : L), f x ∈ t x
⊢ ∃ (f : L → P), Function.Injective f ∧ ∀ (l : L), f l ∉ l

Tactic:
exact ⟨f, hf1, fun l => Set.mem_toFinset.mp (hf2 l)⟩
-- Module: Mathlib.Combinatorics.Configuration
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}
suffices : ∀ (s : Finset L), #s ≤ #(s.biUnion t)
⊢ ∃ (f : L → P), Function.Injective f ∧ ∀ (l : L), f l ∉ l

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)⟩
-- Module: Mathlib.Combinatorics.Configuration
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)
neg : ∀ (hs₀ : ¬#s = 0), #s ≤ #(s.biUnion t)
⊢ #s ≤ #(s.biUnion t)

Tactic:
by_cases hs₀ : #s = 0
-- Module: Mathlib.Combinatorics.Configuration
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 : 0 ≤ #(s.biUnion t)
⊢ #s ≤ #(s.biUnion t)

Tactic:
simp_rw [hs₀, zero_le]

Premises used: zero_le
-- Module: Mathlib.Combinatorics.Configuration
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)
neg : ∀ (hs₁ : ¬#s = 1), #s ≤ #(s.biUnion t)
⊢ #s ≤ #(s.biUnion t)

Tactic:
by_cases hs₁ : #s = 1
-- Module: Mathlib.Combinatorics.Configuration
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
pos :
  ∀ (l : L) (hs₀ : ¬card (α := L) {l} = 0) (hs₁ : card (α := L) {l} = 1), card (α := L) {l} ≤ #(Finset.biUnion {l} t)
⊢ #s ≤ #(s.biUnion t)

Tactic:
obtain ⟨l, rfl⟩ := Finset.card_eq_one.mp hs₁

Premises used: Finset.card_eq_one, Iff.mp, rfl
-- Module: Mathlib.Combinatorics.Configuration
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
pos : ∀ (p : P) (hl : p ∉ l), card (α := L) {l} ≤ #(Finset.biUnion {l} t)
⊢ card (α := L) {l} ≤ #(Finset.biUnion {l} t)

Tactic:
obtain ⟨p, hl⟩ := exists_point (P := P) l

Premises used: Configuration.Nondegenerate.exists_point
-- Module: Mathlib.Combinatorics.Configuration
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
pos : #(t l) ≠ 0
⊢ card (α := L) {l} ≤ #(Finset.biUnion {l} t)

Tactic:
rw [Finset.card_singleton, Finset.singleton_biUnion, Nat.one_le_iff_ne_zero]

Premises used: Finset.singleton_biUnion, Nat.one_le_iff_ne_zero, Finset.card_singleton
-- Module: Mathlib.Combinatorics.Configuration
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
⊢ #(t l) ≠ 0

Tactic:
Finset.card_ne_zero_of_mem (Set.mem_toFinset.mpr hl)

Premises used: Iff.mpr, Finset.card_ne_zero_of_mem, Set.mem_toFinset
-- Module: Mathlib.Combinatorics.Configuration
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
⊢ #(t l) ≠ 0

Tactic:
exact Finset.card_ne_zero_of_mem (Set.mem_toFinset.mpr hl)

Premises used: Iff.mpr, Finset.card_ne_zero_of_mem, Set.mem_toFinset
-- Module: Mathlib.Combinatorics.Configuration
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ᶜ
⊢ Fintype.card P ≤ #(s.biUnion t) + (Fintype.card L - #s)

Tactic:
rw [Finset.card_compl, Finset.card_compl, tsub_le_iff_left] at this

Premises used: Finset.card_compl, tsub_le_iff_left