-- Mathlib/Analysis/Convex/Radon.lean
theorem helly_theorem_set' {F : Finset (Set E)}
    (h_convex : ∀ X ∈ F, Convex 𝕜 X)
    (h_inter : ∀ G : Finset (Set E), G ⊆ F → #G ≤ finrank 𝕜 E + 1 → (⋂₀ G : Set E).Nonempty) :
    (⋂₀ (F : Set (Set E))).Nonempty

Proof state:
𝕜 : Type u_2
E : Type u_3
inst✝³ : LinearOrderedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
F : Finset (Set E)
h_convex : ∀ X ∈ F, Convex 𝕜 X
h_inter : ∀ G ⊆ F, #G ≤ finrank 𝕜 E + 1 → (⋂₀ ↑G).Nonempty
⊢ ⋂₀ ↑F = ⋂ X ∈ F, X

Tactic:
ext

Result:
case h
𝕜 : Type u_2
E : Type u_3
inst✝³ : LinearOrderedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
F : Finset (Set E)
h_convex : ∀ X ∈ F, Convex 𝕜 X
h_inter : ∀ G ⊆ F, #G ≤ finrank 𝕜 E + 1 → (⋂₀ ↑G).Nonempty
x✝ : E
⊢ x✝ ∈ ⋂₀ ↑F ↔ x✝ ∈ ⋂ X ∈ F, X

Proof state:
𝕜 : Type u_2
E : Type u_3
inst✝³ : LinearOrderedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
F : Finset (Set E)
h_convex : ∀ X ∈ F, Convex 𝕜 X
h_inter : ∀ G ⊆ F, #G ≤ finrank 𝕜 E + 1 → (⋂₀ ↑G).Nonempty
G : Finset (Set E)
hG_ss : G ⊆ F
hG_card : #G ≤ finrank 𝕜 E + 1
⊢ ⋂ X ∈ G, X = ⋂₀ ↑G

Tactic:
ext

Result:
case h
𝕜 : Type u_2
E : Type u_3
inst✝³ : LinearOrderedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
F : Finset (Set E)
h_convex : ∀ X ∈ F, Convex 𝕜 X
h_inter : ∀ G ⊆ F, #G ≤ finrank 𝕜 E + 1 → (⋂₀ ↑G).Nonempty
G : Finset (Set E)
hG_ss : G ⊆ F
hG_card : #G ≤ finrank 𝕜 E + 1
x✝ : E
⊢ x✝ ∈ ⋂ X ∈ G, X ↔ x✝ ∈ ⋂₀ ↑G

Proof state:
case h
𝕜 : Type u_2
E : Type u_3
inst✝³ : LinearOrderedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
F : Finset (Set E)
h_convex : ∀ X ∈ F, Convex 𝕜 X
h_inter : ∀ G ⊆ F, #G ≤ finrank 𝕜 E + 1 → (⋂₀ ↑G).Nonempty
x✝ : E
⊢ x✝ ∈ ⋂₀ ↑F ↔ x✝ ∈ ⋂ X ∈ F, X

Tactic:
simp

Result:
no goals

Proof state:
𝕜 : Type u_2
E : Type u_3
inst✝³ : LinearOrderedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
F : Finset (Set E)
h_convex : ∀ X ∈ F, Convex 𝕜 X
h_inter : ∀ G ⊆ F, #G ≤ finrank 𝕜 E + 1 → (⋂₀ ↑G).Nonempty
G : Finset (Set E)
hG_ss : G ⊆ F
hG_card : #G ≤ finrank 𝕜 E + 1
⊢ (⋂ i ∈ G, i).Nonempty

Tactic:
rw [show ⋂ X ∈ G, X = ⋂₀ G by ext; simp]

Result:
𝕜 : Type u_2
E : Type u_3
inst✝³ : LinearOrderedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
F : Finset (Set E)
h_convex : ∀ X ∈ F, Convex 𝕜 X
h_inter : ∀ G ⊆ F, #G ≤ finrank 𝕜 E + 1 → (⋂₀ ↑G).Nonempty
G : Finset (Set E)
hG_ss : G ⊆ F
hG_card : #G ≤ finrank 𝕜 E + 1
⊢ (⋂₀ ↑G).Nonempty

Proof state:
𝕜 : Type u_2
E : Type u_3
inst✝³ : LinearOrderedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
F : Finset (Set E)
h_convex : ∀ X ∈ F, Convex 𝕜 X
h_inter : ∀ G ⊆ F, #G ≤ finrank 𝕜 E + 1 → (⋂₀ ↑G).Nonempty
G : Finset (Set E)
hG_ss : G ⊆ F
hG_card : #G ≤ finrank 𝕜 E + 1
⊢ (⋂₀ ↑G).Nonempty

Tactic:
exact h_inter G hG_ss hG_card

Result:
no goals

Proof state:
𝕜 : Type u_2
E : Type u_3
inst✝³ : LinearOrderedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
F : Finset (Set E)
h_convex : ∀ X ∈ F, Convex 𝕜 X
h_inter : ∀ G ⊆ F, #G ≤ finrank 𝕜 E + 1 → (⋂₀ ↑G).Nonempty
⊢ (⋂ X ∈ F, X).Nonempty

Tactic:
apply helly_theorem' h_convex

Result:
𝕜 : Type u_2
E : Type u_3
inst✝³ : LinearOrderedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
F : Finset (Set E)
h_convex : ∀ X ∈ F, Convex 𝕜 X
h_inter : ∀ G ⊆ F, #G ≤ finrank 𝕜 E + 1 → (⋂₀ ↑G).Nonempty
⊢ ∀ I ⊆ F, #I ≤ finrank 𝕜 E + 1 → (⋂ i ∈ I, i).Nonempty

Proof state:
case h
𝕜 : Type u_2
E : Type u_3
inst✝³ : LinearOrderedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
F : Finset (Set E)
h_convex : ∀ X ∈ F, Convex 𝕜 X
h_inter : ∀ G ⊆ F, #G ≤ finrank 𝕜 E + 1 → (⋂₀ ↑G).Nonempty
G : Finset (Set E)
hG_ss : G ⊆ F
hG_card : #G ≤ finrank 𝕜 E + 1
x✝ : E
⊢ x✝ ∈ ⋂ X ∈ G, X ↔ x✝ ∈ ⋂₀ ↑G

Tactic:
simp

Result:
no goals

Proof state:
𝕜 : Type u_2
E : Type u_3
inst✝³ : LinearOrderedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
F : Finset (Set E)
h_convex : ∀ X ∈ F, Convex 𝕜 X
h_inter : ∀ G ⊆ F, #G ≤ finrank 𝕜 E + 1 → (⋂₀ ↑G).Nonempty
⊢ ∀ I ⊆ F, #I ≤ finrank 𝕜 E + 1 → (⋂ i ∈ I, i).Nonempty

Tactic:
intro G hG_ss hG_card

Result:
𝕜 : Type u_2
E : Type u_3
inst✝³ : LinearOrderedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
F : Finset (Set E)
h_convex : ∀ X ∈ F, Convex 𝕜 X
h_inter : ∀ G ⊆ F, #G ≤ finrank 𝕜 E + 1 → (⋂₀ ↑G).Nonempty
G : Finset (Set E)
hG_ss : G ⊆ F
hG_card : #G ≤ finrank 𝕜 E + 1
⊢ (⋂ i ∈ G, i).Nonempty

Proof state:
𝕜 : Type u_2
E : Type u_3
inst✝³ : LinearOrderedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
F : Finset (Set E)
h_convex : ∀ X ∈ F, Convex 𝕜 X
h_inter : ∀ G ⊆ F, #G ≤ finrank 𝕜 E + 1 → (⋂₀ ↑G).Nonempty
⊢ (⋂₀ ↑F).Nonempty

Tactic:
classical 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

Result:
no goals

Proof state:
𝕜 : Type u_2
E : Type u_3
inst✝³ : LinearOrderedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
F : Finset (Set E)
h_convex : ∀ X ∈ F, Convex 𝕜 X
h_inter : ∀ G ⊆ F, #G ≤ finrank 𝕜 E + 1 → (⋂₀ ↑G).Nonempty
⊢ (⋂₀ ↑F).Nonempty

Tactic:
rw [show ⋂₀ F = ⋂ X ∈ F, (X : Set E) by ext; simp]

Result:
𝕜 : Type u_2
E : Type u_3
inst✝³ : LinearOrderedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
F : Finset (Set E)
h_convex : ∀ X ∈ F, Convex 𝕜 X
h_inter : ∀ G ⊆ F, #G ≤ finrank 𝕜 E + 1 → (⋂₀ ↑G).Nonempty
⊢ (⋂ X ∈ F, X).Nonempty