awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Convex.Radon
Goal:
𝕜 : Type u_2
E : Type u_3
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
inst_5 : FiniteDimensional 𝕜 E
F : Finset (Set E)
h_convex : ∀ X ∈ F, Convex 𝕜 X
h_inter : ∀ G ⊆ F, #G ≤ finrank 𝕜 E + 1 → (⋂₀ (↑G : Set (Set E))).Nonempty
x : E
⊢ x ∈ ⋂₀ (↑F : Set (Set E)) ↔ Membership.mem (γ := Set E) (⋂ X ∈ F, X) x

Tactic:
simp
-- Module: Mathlib.Analysis.Convex.Radon
Goal:
𝕜 : Type u_2
E : Type u_3
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
inst_5 : FiniteDimensional 𝕜 E
F : Finset (Set E)
h_convex : ∀ X ∈ F, Convex 𝕜 X
h_inter : ∀ G ⊆ F, #G ≤ finrank 𝕜 E + 1 → (⋂₀ (↑G : Set (Set E))).Nonempty
rw : Set.Nonempty.{u_3} (α := E) (⋂ X ∈ F, X)
⊢ (⋂₀ (↑F : Set (Set E))).Nonempty

Tactic:
rw [show ⋂₀ F = ⋂ X ∈ F, (X : Set E) by ext; simp]
-- Module: Mathlib.Analysis.Convex.Radon
Goal:
𝕜 : Type u_2
E : Type u_3
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
inst_5 : FiniteDimensional 𝕜 E
F : Finset (Set E)
h_convex : ∀ X ∈ F, Convex 𝕜 X
h_inter : ∀ G ⊆ F, #G ≤ finrank 𝕜 E + 1 → (⋂₀ (↑G : Set (Set E))).Nonempty
apply : ∀ I ⊆ F, #I ≤ finrank 𝕜 E + 1 → Set.Nonempty.{u_3} (α := E) (⋂ i ∈ I, i)
⊢ Set.Nonempty.{u_3} (α := E) (⋂ X ∈ F, X)

Tactic:
apply helly_theorem' h_convex

Premises used: Convex.helly_theorem'
-- Module: Mathlib.Analysis.Convex.Radon
Goal:
𝕜 : Type u_2
E : Type u_3
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
inst_5 : FiniteDimensional 𝕜 E
F : Finset (Set E)
h_convex : ∀ X ∈ F, Convex 𝕜 X
h_inter : ∀ G ⊆ F, #G ≤ finrank 𝕜 E + 1 → (⋂₀ (↑G : Set (Set E))).Nonempty
G : Finset (Set E)
hG_ss : G ⊆ F
hG_card : #G ≤ finrank 𝕜 E + 1
h : ∀ (x : E), Membership.mem (γ := Set E) (⋂ X ∈ G, X) x ↔ x ∈ ⋂₀ (↑G : Set (Set E))
⊢ ⋂ X ∈ G, X = ⋂₀ (↑G : Set (Set E))

Tactic:
ext
-- Module: Mathlib.Analysis.Convex.Radon
Goal:
𝕜 : Type u_2
E : Type u_3
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
inst_5 : FiniteDimensional 𝕜 E
F : Finset (Set E)
h_convex : ∀ X ∈ F, Convex 𝕜 X
h_inter : ∀ G ⊆ F, #G ≤ finrank 𝕜 E + 1 → (⋂₀ (↑G : Set (Set E))).Nonempty
G : Finset (Set E)
hG_ss : G ⊆ F
hG_card : #G ≤ finrank 𝕜 E + 1
x : E
⊢ Membership.mem (γ := Set E) (⋂ X ∈ G, X) x ↔ x ∈ ⋂₀ (↑G : Set (Set E))

Tactic:
simp
-- Module: Mathlib.Analysis.Convex.Radon
Goal:
𝕜 : Type u_2
E : Type u_3
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
inst_5 : FiniteDimensional 𝕜 E
F : Finset (Set E)
h_convex : ∀ X ∈ F, Convex 𝕜 X
h_inter : ∀ G ⊆ F, #G ≤ finrank 𝕜 E + 1 → (⋂₀ (↑G : Set (Set E))).Nonempty
G : Finset (Set E)
hG_ss : G ⊆ F
hG_card : #G ≤ finrank 𝕜 E + 1
rw : (⋂₀ (↑G : Set (Set E))).Nonempty
⊢ Set.Nonempty.{u_3} (α := E) (⋂ i ∈ G, i)

Tactic:
rw [show ⋂ X ∈ G, X = ⋂₀ G by ext; simp]
-- Module: Mathlib.Analysis.Convex.Radon
Goal:
𝕜 : Type u_2
E : Type u_3
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
inst_5 : FiniteDimensional 𝕜 E
F : Finset (Set E)
h_convex : ∀ X ∈ F, Convex 𝕜 X
h_inter : ∀ G ⊆ F, #G ≤ finrank 𝕜 E + 1 → (⋂₀ (↑G : Set (Set E))).Nonempty
G : Finset (Set E)
hG_ss : G ⊆ F
hG_card : #G ≤ finrank 𝕜 E + 1
⊢ (⋂₀ (↑G : Set (Set E))).Nonempty

Tactic:
h_inter G hG_ss hG_card
-- Module: Mathlib.Analysis.Convex.Radon
Goal:
𝕜 : Type u_2
E : Type u_3
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
inst_5 : FiniteDimensional 𝕜 E
F : Finset (Set E)
h_convex : ∀ X ∈ F, Convex 𝕜 X
h_inter : ∀ G ⊆ F, #G ≤ finrank 𝕜 E + 1 → (⋂₀ (↑G : Set (Set E))).Nonempty
G : Finset (Set E)
hG_ss : G ⊆ F
hG_card : #G ≤ finrank 𝕜 E + 1
⊢ (⋂₀ (↑G : Set (Set E))).Nonempty

Tactic:
exact h_inter G hG_ss hG_card
-- Module: Mathlib.Analysis.Convex.Radon
Goal:
𝕜 : Type u_2
E : Type u_3
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
inst_5 : FiniteDimensional 𝕜 E
F : Finset (Set E)
h_convex : ∀ X ∈ F, Convex 𝕜 X
h_inter : ∀ G ⊆ F, #G ≤ finrank 𝕜 E + 1 → (⋂₀ (↑G : Set (Set E))).Nonempty
classical classical₁ classical₂ : Set.Nonempty.{u_3} (α := E) (⋂ X ∈ F, X)
classical₃ classical₄ :
  ∀ (G : Finset (Set E)) (hG_ss : G ⊆ F) (hG_card : #G ≤ finrank 𝕜 E + 1), Set.Nonempty.{u_3} (α := E) (⋂ i ∈ G, i)
classical₅ : ∀ (G : Finset (Set E)) (hG_ss : G ⊆ F) (hG_card : #G ≤ finrank 𝕜 E + 1), (⋂₀ (↑G : Set (Set E))).Nonempty
⊢ (⋂₀ (↑F : Set (Set E))).Nonempty

Tactic:
classical -- for DecidableEq, required for the family version
  rw [show ⋂₀ F = ⋂ X ∈ F, (X : Set E) by ext; simp]
  apply helly_theorem' h_convex
  intro G hG_ss hG_card
  rw [show ⋂ X ∈ G, X = ⋂₀ G by ext; simp]
  exact h_inter G hG_ss hG_card

Premises used: Convex.helly_theorem'
-- Module: Mathlib.Analysis.Convex.Radon
Goal:
𝕜 : Type u_2
E : Type u_3
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
inst_5 : FiniteDimensional 𝕜 E
F : Finset (Set E)
h_card : finrank 𝕜 E + 1 ≤ #F
h_convex : ∀ X ∈ F, Convex 𝕜 X
h_inter : ∀ G ⊆ F, #G = finrank 𝕜 E + 1 → (⋂₀ (↑G : Set (Set E))).Nonempty
apply : ∀ G ⊆ F, #G ≤ finrank 𝕜 E + 1 → (⋂₀ (↑G : Set (Set E))).Nonempty
⊢ (⋂₀ (↑F : Set (Set E))).Nonempty

Tactic:
apply helly_theorem_set' h_convex

Premises used: Convex.helly_theorem_set'
-- Module: Mathlib.Analysis.Convex.Radon
Goal:
𝕜 : Type u_2
E : Type u_3
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
inst_5 : FiniteDimensional 𝕜 E
F : Finset (Set E)
h_card : finrank 𝕜 E + 1 ≤ #F
h_convex : ∀ X ∈ F, Convex 𝕜 X
h_inter : ∀ G ⊆ F, #G = finrank 𝕜 E + 1 → (⋂₀ (↑G : Set (Set E))).Nonempty
I : Finset (Set E)
hI_ss : I ⊆ F
hI_card : #I ≤ finrank 𝕜 E + 1
obtain :
  ∀ (J : Finset (Set E)), I ⊆ J → ∀ (hJ_ss : J ⊆ F) (hJ_card : #J = finrank 𝕜 E + 1), (⋂₀ (↑I : Set (Set E))).Nonempty
⊢ (⋂₀ (↑I : Set (Set E))).Nonempty

Tactic:
obtain ⟨J, _, hJ_ss, hJ_card⟩ := exists_subsuperset_card_eq hI_ss hI_card h_card

Premises used: Finset.exists_subsuperset_card_eq
-- Module: Mathlib.Analysis.Convex.Radon
Goal:
𝕜 : Type u_2
E : Type u_3
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
inst_5 : FiniteDimensional 𝕜 E
F : Finset (Set E)
h_card : finrank 𝕜 E + 1 ≤ #F
h_convex : ∀ X ∈ F, Convex 𝕜 X
h_inter : ∀ G ⊆ F, #G = finrank 𝕜 E + 1 → (⋂₀ (↑G : Set (Set E))).Nonempty
I : Finset (Set E)
hI_ss : I ⊆ F
hI_card : #I ≤ finrank 𝕜 E + 1
J : Finset (Set E)
left : I ⊆ J
hJ_ss : J ⊆ F
hJ_card : #J = finrank 𝕜 E + 1
⊢ (↑I : Set (Set E)) ⊆ (↑J : Set (Set E))

Tactic:
simpa [hI_ss]
-- Module: Mathlib.Analysis.Convex.Radon
Goal:
𝕜 : Type u_2
E : Type u_3
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
inst_5 : FiniteDimensional 𝕜 E
F : Finset (Set E)
h_card : finrank 𝕜 E + 1 ≤ #F
h_convex : ∀ X ∈ F, Convex 𝕜 X
h_inter : ∀ G ⊆ F, #G = finrank 𝕜 E + 1 → (⋂₀ (↑G : Set (Set E))).Nonempty
I : Finset (Set E)
hI_ss : I ⊆ F
hI_card : #I ≤ finrank 𝕜 E + 1
J : Finset (Set E)
left : I ⊆ J
hJ_ss : J ⊆ F
hJ_card : #J = finrank 𝕜 E + 1
⊢ ⋂₀ (↑J : Set (Set E)) ⊆ ⋂₀ (↑I : Set (Set E))

Tactic:
have : ⋂₀ (J : Set (Set E)) ⊆ ⋂₀ I := sInter_mono (by simpa [hI_ss])
-- Module: Mathlib.Analysis.Convex.Radon
Goal:
𝕜 : Type u_2
E : Type u_3
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
inst_5 : FiniteDimensional 𝕜 E
F : Finset (Set E)
h_card : finrank 𝕜 E + 1 ≤ #F
h_convex : ∀ X ∈ F, Convex 𝕜 X
h_inter : ∀ G ⊆ F, #G = finrank 𝕜 E + 1 → (⋂₀ (↑G : Set (Set E))).Nonempty
I : Finset (Set E)
hI_ss : I ⊆ F
hI_card : #I ≤ finrank 𝕜 E + 1
J : Finset (Set E)
left : I ⊆ J
hJ_ss : J ⊆ F
hJ_card : #J = finrank 𝕜 E + 1
this : ⋂₀ (↑J : Set (Set E)) ⊆ ⋂₀ (↑I : Set (Set E))
apply : (⋂₀ (↑J : Set (Set E))).Nonempty
⊢ (⋂₀ (↑I : Set (Set E))).Nonempty

Tactic:
apply Set.Nonempty.mono this

Premises used: Set.Nonempty.mono
-- Module: Mathlib.Analysis.Convex.Radon
Goal:
𝕜 : Type u_2
E : Type u_3
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
inst_5 : FiniteDimensional 𝕜 E
F : Finset (Set E)
h_card : finrank 𝕜 E + 1 ≤ #F
h_convex : ∀ X ∈ F, Convex 𝕜 X
h_inter : ∀ G ⊆ F, #G = finrank 𝕜 E + 1 → (⋂₀ (↑G : Set (Set E))).Nonempty
I : Finset (Set E)
hI_ss : I ⊆ F
hI_card : #I ≤ finrank 𝕜 E + 1
J : Finset (Set E)
left : I ⊆ J
hJ_ss : J ⊆ F
hJ_card : #J = finrank 𝕜 E + 1
this : ⋂₀ (↑J : Set (Set E)) ⊆ ⋂₀ (↑I : Set (Set E))
⊢ #J = finrank 𝕜 E + 1

Tactic:
lia
-- Module: Mathlib.Analysis.Convex.Radon
Goal:
𝕜 : Type u_2
E : Type u_3
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
inst_5 : FiniteDimensional 𝕜 E
F : Finset (Set E)
h_card : finrank 𝕜 E + 1 ≤ #F
h_convex : ∀ X ∈ F, Convex 𝕜 X
h_inter : ∀ G ⊆ F, #G = finrank 𝕜 E + 1 → (⋂₀ (↑G : Set (Set E))).Nonempty
I : Finset (Set E)
hI_ss : I ⊆ F
hI_card : #I ≤ finrank 𝕜 E + 1
J : Finset (Set E)
left : I ⊆ J
hJ_ss : J ⊆ F
hJ_card : #J = finrank 𝕜 E + 1
this : ⋂₀ (↑J : Set (Set E)) ⊆ ⋂₀ (↑I : Set (Set E))
⊢ (⋂₀ (↑J : Set (Set E))).Nonempty

Tactic:
exact h_inter J hJ_ss (by lia)
-- Module: Mathlib.Analysis.Convex.Radon
Goal:
ι : Type u_1
𝕜 : Type u_2
E : Type u_3
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
inst_5 : FiniteDimensional 𝕜 E
inst_6 : TopologicalSpace E
inst_7 : T2Space E
F : ι → Set E
h_convex : ∀ (i : ι), Convex 𝕜 (F i)
h_compact : ∀ (i : ι), IsCompact (F i)
h_inter : ∀ (I : Finset ι), #I ≤ finrank 𝕜 E + 1 → Set.Nonempty.{u_3} (α := E) (⋂ i ∈ I, F i)
inl : IsEmpty ι → Set.Nonempty.{u_3} (α := E) (⋂ (i : ι), F i)
inr : ∀ (h_nonempty : Nonempty ι), Set.Nonempty.{u_3} (α := E) (⋂ (i : ι), F i)
⊢ Set.Nonempty.{u_3} (α := E) (⋂ (i : ι), F i)

Tactic:
rcases isEmpty_or_nonempty ι with _ | h_nonempty

Premises used: isEmpty_or_nonempty
-- Module: Mathlib.Analysis.Convex.Radon
Goal:
ι : Type u_1
𝕜 : Type u_2
E : Type u_3
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
inst_5 : FiniteDimensional 𝕜 E
inst_6 : TopologicalSpace E
inst_7 : T2Space E
F : ι → Set E
h_convex : ∀ (i : ι), Convex 𝕜 (F i)
h_compact : ∀ (i : ι), IsCompact (F i)
h_inter : ∀ (I : Finset ι), #I ≤ finrank 𝕜 E + 1 → Set.Nonempty.{u_3} (α := E) (⋂ i ∈ I, F i)
h : IsEmpty ι
⊢ Set.Nonempty.{u_3} (α := E) (⋂ (i : ι), F i)

Tactic:
simp only [iInter_of_empty, Set.univ_nonempty]

Premises used: Set.univ_nonempty, Set.iInter_of_empty
-- Module: Mathlib.Analysis.Convex.Radon
Goal:
ι : Type u_1
𝕜 : Type u_2
E : Type u_3
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
inst_5 : FiniteDimensional 𝕜 E
inst_6 : TopologicalSpace E
inst_7 : T2Space E
F : ι → Set E
h_convex : ∀ (i : ι), Convex 𝕜 (F i)
h_compact : ∀ (i : ι), IsCompact (F i)
h_inter : ∀ (I : Finset ι), #I ≤ finrank 𝕜 E + 1 → Set.Nonempty.{u_3} (α := E) (⋂ i ∈ I, F i)
h_nonempty : Nonempty ι
I : Finset ι
⊢ ∀ i ∈ I, Convex 𝕜 (F i)

Tactic:
simp [h_convex]
-- Module: Mathlib.Analysis.Convex.Radon
Goal:
ι : Type u_1
𝕜 : Type u_2
E : Type u_3
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
inst_5 : FiniteDimensional 𝕜 E
inst_6 : TopologicalSpace E
inst_7 : T2Space E
F : ι → Set E
h_convex : ∀ (i : ι), Convex 𝕜 (F i)
h_compact : ∀ (i : ι), IsCompact (F i)
h_inter : ∀ (I : Finset ι), #I ≤ finrank 𝕜 E + 1 → Set.Nonempty.{u_3} (α := E) (⋂ i ∈ I, F i)
h_nonempty : Nonempty ι
I : Finset ι
apply : ∀ I_1 ⊆ I, #I_1 ≤ finrank 𝕜 E + 1 → Set.Nonempty.{u_3} (α := E) (⋂ i ∈ I_1, F i)
⊢ Set.Nonempty.{u_3} (α := E) (⋂ i ∈ I, F i)

Tactic:
apply helly_theorem' (s := I) (𝕜 := 𝕜) (by simp [h_convex])

Premises used: Convex.helly_theorem'
-- Module: Mathlib.Analysis.Convex.Radon
Goal:
ι : Type u_1
𝕜 : Type u_2
E : Type u_3
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
inst_5 : FiniteDimensional 𝕜 E
inst_6 : TopologicalSpace E
inst_7 : T2Space E
F : ι → Set E
h_convex : ∀ (i : ι), Convex 𝕜 (F i)
h_compact : ∀ (i : ι), IsCompact (F i)
h_inter : ∀ (I : Finset ι), #I ≤ finrank 𝕜 E + 1 → Set.Nonempty.{u_3} (α := E) (⋂ i ∈ I, F i)
h_nonempty : Nonempty ι
I : Finset ι
⊢ ∀ I_1 ⊆ I, #I_1 ≤ finrank 𝕜 E + 1 → Set.Nonempty.{u_3} (α := E) (⋂ i ∈ I_1, F i)

Tactic:
fun J _ hJ_card ↦ h_inter J hJ_card
-- Module: Mathlib.Analysis.Convex.Radon
Goal:
ι : Type u_1
𝕜 : Type u_2
E : Type u_3
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
inst_5 : FiniteDimensional 𝕜 E
inst_6 : TopologicalSpace E
inst_7 : T2Space E
F : ι → Set E
h_convex : ∀ (i : ι), Convex 𝕜 (F i)
h_compact : ∀ (i : ι), IsCompact (F i)
h_inter : ∀ (I : Finset ι), #I ≤ finrank 𝕜 E + 1 → Set.Nonempty.{u_3} (α := E) (⋂ i ∈ I, F i)
h_nonempty : Nonempty ι
I : Finset ι
⊢ ∀ I_1 ⊆ I, #I_1 ≤ finrank 𝕜 E + 1 → Set.Nonempty.{u_3} (α := E) (⋂ i ∈ I_1, F i)

Tactic:
exact fun J _ hJ_card ↦ h_inter J hJ_card
-- Module: Mathlib.Analysis.Convex.Radon
Goal:
ι : Type u_1
𝕜 : Type u_2
E : Type u_3
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
inst_5 : FiniteDimensional 𝕜 E
inst_6 : TopologicalSpace E
inst_7 : T2Space E
F : ι → Set E
h_convex : ∀ (i : ι), Convex 𝕜 (F i)
h_compact : ∀ (i : ι), IsCompact (F i)
h_inter : ∀ (I : Finset ι), #I ≤ finrank 𝕜 E + 1 → Set.Nonempty.{u_3} (α := E) (⋂ i ∈ I, F i)
h_nonempty : Nonempty ι
⊢ ∀ (I : Finset ι), Set.Nonempty.{u_3} (α := E) (⋂ i ∈ I, F i)

Tactic:
have h_fin (I : Finset ι) : (⋂ i ∈ I, F i).Nonempty := by
    apply helly_theorem' (s := I) (𝕜 := 𝕜) (by simp [h_convex])
    exact fun J _ hJ_card ↦ h_inter J hJ_card
-- Module: Mathlib.Analysis.Convex.Radon
Goal:
ι : Type u_1
𝕜 : Type u_2
E : Type u_3
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
inst_5 : FiniteDimensional 𝕜 E
inst_6 : TopologicalSpace E
inst_7 : T2Space E
F : ι → Set E
h_convex : ∀ (i : ι), Convex 𝕜 (F i)
h_compact : ∀ (i : ι), IsCompact (F i)
h_inter : ∀ (I : Finset ι), #I ≤ finrank 𝕜 E + 1 → Set.Nonempty.{u_3} (α := E) (⋂ i ∈ I, F i)
h_nonempty : Nonempty ι
h_fin : ∀ (I : Finset ι), Set.Nonempty.{u_3} (α := E) (⋂ i ∈ I, F i)
inr : ∀ (i0 : ι), Set.Nonempty.{u_3} (α := E) (⋂ (i : ι), F i)
⊢ Set.Nonempty.{u_3} (α := E) (⋂ (i : ι), F i)

Tactic:
have i0 : ι := Nonempty.some h_nonempty
-- Module: Mathlib.Analysis.Convex.Radon
Goal:
ι : Type u_1
𝕜 : Type u_2
E : Type u_3
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
inst_5 : FiniteDimensional 𝕜 E
inst_6 : TopologicalSpace E
inst_7 : T2Space E
F : ι → Set E
h_convex : ∀ (i : ι), Convex 𝕜 (F i)
h_compact : ∀ (i : ι), IsCompact (F i)
h_inter : ∀ (I : Finset ι), #I ≤ finrank 𝕜 E + 1 → Set.Nonempty.{u_3} (α := E) (⋂ i ∈ I, F i)
h_nonempty : Nonempty ι
h_fin : ∀ (I : Finset ι), Set.Nonempty.{u_3} (α := E) (⋂ i ∈ I, F i)
i0 : ι
⊢ ⋂ (i : ι), F i = F i0 ∩ ⋂ (i : ι), F i

Tactic:
simp [iInter_subset]

Premises used: Set.iInter_subset
-- Module: Mathlib.Analysis.Convex.Radon
Goal:
ι : Type u_1
𝕜 : Type u_2
E : Type u_3
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
inst_5 : FiniteDimensional 𝕜 E
inst_6 : TopologicalSpace E
inst_7 : T2Space E
F : ι → Set E
h_convex : ∀ (i : ι), Convex 𝕜 (F i)
h_compact : ∀ (i : ι), IsCompact (F i)
h_inter : ∀ (I : Finset ι), #I ≤ finrank 𝕜 E + 1 → Set.Nonempty.{u_3} (α := E) (⋂ i ∈ I, F i)
h_nonempty : Nonempty ι
h_fin : ∀ (I : Finset ι), Set.Nonempty.{u_3} (α := E) (⋂ i ∈ I, F i)
i0 : ι
inr : (F i0 ∩ ⋂ (i : ι), F i).Nonempty
⊢ Set.Nonempty.{u_3} (α := E) (⋂ (i : ι), F i)

Tactic:
rw [show ⋂ i, F i = (F i0) ∩ ⋂ i, F i by simp [iInter_subset]]
-- Module: Mathlib.Analysis.Convex.Radon
Goal:
ι : Type u_1
𝕜 : Type u_2
E : Type u_3
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
inst_5 : FiniteDimensional 𝕜 E
inst_6 : TopologicalSpace E
inst_7 : T2Space E
F : ι → Set E
h_convex : ∀ (i : ι), Convex 𝕜 (F i)
h_compact : ∀ (i : ι), IsCompact (F i)
h_inter : ∀ (I : Finset ι), #I ≤ finrank 𝕜 E + 1 → Set.Nonempty.{u_3} (α := E) (⋂ i ∈ I, F i)
h_nonempty : Nonempty ι
h_fin : ∀ (I : Finset ι), Set.Nonempty.{u_3} (α := E) (⋂ i ∈ I, F i)
i0 : ι
inr : IsCompact (F i0)
inr₁ : ∀ (i : ι), IsClosed (F i)
inr₂ : ∀ (u : Finset ι), (F i0 ∩ ⋂ i ∈ u, F i).Nonempty
⊢ (F i0 ∩ ⋂ (i : ι), F i).Nonempty

Tactic:
apply IsCompact.inter_iInter_nonempty

Premises used: IsCompact.inter_iInter_nonempty
-- Module: Mathlib.Analysis.Convex.Radon
Goal:
ι : Type u_1
𝕜 : Type u_2
E : Type u_3
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
inst_5 : FiniteDimensional 𝕜 E
inst_6 : TopologicalSpace E
inst_7 : T2Space E
F : ι → Set E
h_convex : ∀ (i : ι), Convex 𝕜 (F i)
h_compact : ∀ (i : ι), IsCompact (F i)
h_inter : ∀ (I : Finset ι), #I ≤ finrank 𝕜 E + 1 → Set.Nonempty.{u_3} (α := E) (⋂ i ∈ I, F i)
h_nonempty : Nonempty ι
h_fin : ∀ (I : Finset ι), Set.Nonempty.{u_3} (α := E) (⋂ i ∈ I, F i)
i0 : ι
⊢ IsCompact (F i0)

Tactic:
h_compact i0
-- Module: Mathlib.Analysis.Convex.Radon
Goal:
ι : Type u_1
𝕜 : Type u_2
E : Type u_3
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
inst_5 : FiniteDimensional 𝕜 E
inst_6 : TopologicalSpace E
inst_7 : T2Space E
F : ι → Set E
h_convex : ∀ (i : ι), Convex 𝕜 (F i)
h_compact : ∀ (i : ι), IsCompact (F i)
h_inter : ∀ (I : Finset ι), #I ≤ finrank 𝕜 E + 1 → Set.Nonempty.{u_3} (α := E) (⋂ i ∈ I, F i)
h_nonempty : Nonempty ι
h_fin : ∀ (I : Finset ι), Set.Nonempty.{u_3} (α := E) (⋂ i ∈ I, F i)
i0 : ι
⊢ IsCompact (F i0)

Tactic:
exact h_compact i0
-- Module: Mathlib.Analysis.Convex.Radon
Goal:
ι : Type u_1
𝕜 : Type u_2
E : Type u_3
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
inst_5 : FiniteDimensional 𝕜 E
inst_6 : TopologicalSpace E
inst_7 : T2Space E
F : ι → Set E
h_convex : ∀ (i : ι), Convex 𝕜 (F i)
h_compact : ∀ (i : ι), IsCompact (F i)
h_inter : ∀ (I : Finset ι), #I ≤ finrank 𝕜 E + 1 → Set.Nonempty.{u_3} (α := E) (⋂ i ∈ I, F i)
h_nonempty : Nonempty ι
h_fin : ∀ (I : Finset ι), Set.Nonempty.{u_3} (α := E) (⋂ i ∈ I, F i)
i0 i : ι
⊢ IsClosed (F i)

Tactic:
(h_compact i).isClosed

Premises used: IsCompact.isClosed
-- Module: Mathlib.Analysis.Convex.Radon
Goal:
ι : Type u_1
𝕜 : Type u_2
E : Type u_3
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
inst_5 : FiniteDimensional 𝕜 E
inst_6 : TopologicalSpace E
inst_7 : T2Space E
F : ι → Set E
h_convex : ∀ (i : ι), Convex 𝕜 (F i)
h_compact : ∀ (i : ι), IsCompact (F i)
h_inter : ∀ (I : Finset ι), #I ≤ finrank 𝕜 E + 1 → Set.Nonempty.{u_3} (α := E) (⋂ i ∈ I, F i)
h_nonempty : Nonempty ι
h_fin : ∀ (I : Finset ι), Set.Nonempty.{u_3} (α := E) (⋂ i ∈ I, F i)
i0 i : ι
⊢ IsClosed (F i)

Tactic:
exact (h_compact i).isClosed

Premises used: IsCompact.isClosed
-- Module: Mathlib.Analysis.Convex.Radon
Goal:
ι : Type u_1
𝕜 : Type u_2
E : Type u_3
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
inst_5 : FiniteDimensional 𝕜 E
inst_6 : TopologicalSpace E
inst_7 : T2Space E
F : ι → Set E
h_convex : ∀ (i : ι), Convex 𝕜 (F i)
h_compact : ∀ (i : ι), IsCompact (F i)
h_inter : ∀ (I : Finset ι), #I ≤ finrank 𝕜 E + 1 → Set.Nonempty.{u_3} (α := E) (⋂ i ∈ I, F i)
h_nonempty : Nonempty ι
h_fin : ∀ (I : Finset ι), Set.Nonempty.{u_3} (α := E) (⋂ i ∈ I, F i)
i0 : ι
I : Finset ι
⊢ (F i0 ∩ ⋂ i ∈ I, F i).Nonempty

Tactic:
simpa using h_fin ({i0} ∪ I)

Premises used: Union.union, Singleton.singleton
-- Module: Mathlib.Analysis.Convex.Radon
Goal:
ι : Type u_1
𝕜 : Type u_2
E : Type u_3
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
inst_5 : FiniteDimensional 𝕜 E
inst_6 : TopologicalSpace E
inst_7 : T2Space E
F : ι → Set E
h_convex : ∀ (i : ι), Convex 𝕜 (F i)
h_compact : ∀ (i : ι), IsCompact (F i)
h_inter : ∀ (I : Finset ι), #I ≤ finrank 𝕜 E + 1 → Set.Nonempty.{u_3} (α := E) (⋂ i ∈ I, F i)
inl : IsEmpty ι → Set.Nonempty.{u_3} (α := E) (⋂ (i : ι), F i)
inr inr₁ : ∀ (h_nonempty : Nonempty ι), Set.Nonempty.{u_3} (α := E) (⋂ (i : ι), F i)
inr₂ :
  ∀ (h_nonempty : Nonempty ι) (h_fin : ∀ (I : Finset ι), Set.Nonempty.{u_3} (α := E) (⋂ i ∈ I, F i)),
    Set.Nonempty.{u_3} (α := E) (⋂ (i : ι), F i)
inr₃ :
  ∀ (h_nonempty : Nonempty ι) (h_fin : ∀ (I : Finset ι), Set.Nonempty.{u_3} (α := E) (⋂ i ∈ I, F i)) (i0 : ι),
    Set.Nonempty.{u_3} (α := E) (⋂ (i : ι), F i)
inr₄ :
  ∀ (h_nonempty : Nonempty ι) (h_fin : ∀ (I : Finset ι), Set.Nonempty.{u_3} (α := E) (⋂ i ∈ I, F i)) (i0 : ι),
    (F i0 ∩ ⋂ (i : ι), F i).Nonempty
inr₅ :
  ∀ (h_nonempty : Nonempty ι) (h_fin : ∀ (I : Finset ι), Set.Nonempty.{u_3} (α := E) (⋂ i ∈ I, F i)) (i0 : ι),
    IsCompact (F i0)
inr₆ :
  ∀ (h_nonempty : Nonempty ι) (h_fin : ∀ (I : Finset ι), Set.Nonempty.{u_3} (α := E) (⋂ i ∈ I, F i)) (i0 i : ι),
    IsClosed (F i)
inr₇ :
  ∀ (h_nonempty : Nonempty ι) (h_fin : ∀ (I : Finset ι), Set.Nonempty.{u_3} (α := E) (⋂ i ∈ I, F i)) (i0 : ι)
    (u : Finset ι), (F i0 ∩ ⋂ i ∈ u, F i).Nonempty
inr₈ :
  ∀ (h_nonempty : Nonempty ι) (h_fin : ∀ (I : Finset ι), Set.Nonempty.{u_3} (α := E) (⋂ i ∈ I, F i)) (i0 i : ι),
    IsClosed (F i)
inr₉ inr₁₀ :
  ∀ (h_nonempty : Nonempty ι) (h_fin : ∀ (I : Finset ι), Set.Nonempty.{u_3} (α := E) (⋂ i ∈ I, F i)) (i0 : ι)
    (u : Finset ι), (F i0 ∩ ⋂ i ∈ u, F i).Nonempty
⊢ Set.Nonempty.{u_3} (α := E) (⋂ (i : ι), F i)

Tactic:
classical
  /- If `ι` is empty the statement is trivial. -/
  rcases isEmpty_or_nonempty ι with _ | h_nonempty
  · simp only [iInter_of_empty, Set.univ_nonempty]
  /- By the finite version of theorem, every finite subfamily has an intersection. -/
  have h_fin (I : Finset ι) : (⋂ i ∈ I, F i).Nonempty := by
    apply helly_theorem' (s := I) (𝕜 := 𝕜) (by simp [h_convex])
    exact fun J _ hJ_card ↦ h_inter J hJ_card
  /- The following is a clumsy proof that family of compact sets with the finite intersection
  property has a nonempty intersection. -/
  have i0 : ι := Nonempty.some h_nonempty
  rw [show ⋂ i, F i = (F i0) ∩ ⋂ i, F i by simp [iInter_subset]]
  apply IsCompact.inter_iInter_nonempty
  · exact h_compact i0
  · intro i
    exact (h_compact i).isClosed
  · intro I
    simpa using h_fin ({i0} ∪ I)

Premises used: IsCompact.inter_iInter_nonempty, Set.univ_nonempty, isEmpty_or_nonempty, Set.iInter_of_empty
-- Module: Mathlib.Analysis.Convex.Radon
Goal:
ι : Type u_1
𝕜 : Type u_2
E : Type u_3
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
inst_5 : FiniteDimensional 𝕜 E
inst_6 : TopologicalSpace E
inst_7 : T2Space E
F : ι → Set E
h_card : HAdd.hAdd (α := ℕ∞) (↑(finrank 𝕜 E) : ℕ∞) 1 ≤ ENat.card ι
h_convex : ∀ (i : ι), Convex 𝕜 (F i)
h_compact : ∀ (i : ι), IsCompact (F i)
h_inter : ∀ (I : Finset ι), #I = finrank 𝕜 E + 1 → Set.Nonempty.{u_3} (α := E) (⋂ i ∈ I, F i)
apply : ∀ (I : Finset ι), #I ≤ finrank 𝕜 E + 1 → Set.Nonempty.{u_3} (α := E) (⋂ i ∈ I, F i)
⊢ Set.Nonempty.{u_3} (α := E) (⋂ (i : ι), F i)

Tactic:
apply helly_theorem_compact' h_convex h_compact

Premises used: Convex.helly_theorem_compact'