-- Mathlib/Analysis/Convex/Radon.lean
theorem helly_theorem' {F : ι → Set E} {s : Finset ι}
    (h_convex : ∀ i ∈ s, Convex 𝕜 (F i))
    (h_inter : ∀ I ⊆ s, #I ≤ finrank 𝕜 E + 1 → (⋂ i ∈ I, F i).Nonempty) :
    (⋂ i ∈ s, F i).Nonempty

Proof state:
𝕜 : Type u_2
E : Type u_3
inst✝³ : LinearOrderedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
n k : ℕ
h_card : finrank 𝕜 E + 1 ≤ k
hk :
  ∀ {ι : Type u_1} {F : ι → Set E} {s : Finset ι},
    (∀ i ∈ s, Convex 𝕜 (F i)) →
      (∀ I ⊆ s, #I ≤ finrank 𝕜 E + 1 → (⋂ i ∈ I, F i).Nonempty) → #s = k → (⋂ i ∈ s, F i).Nonempty
ι : Type u_1
F : ι → Set E
s : Finset ι
h_convex : ∀ i ∈ s, Convex 𝕜 (F i)
h_inter : ∀ I ⊆ s, #I ≤ finrank 𝕜 E + 1 → (⋂ i ∈ I, F i).Nonempty
hn : #s = k + 1
a : { x // x ∈ s } → E := fun i => ⋯.some
h_ind : ¬AffineIndependent 𝕜 a
I : Set { x // x ∈ s }
p : E
hp_I : p ∈ (convexHull 𝕜) (a '' I)
hp_Ic : p ∈ (convexHull 𝕜) (a '' Iᶜ)
i✝ : ι
hi✝ : i✝ ∈ Membership.mem s.val
i : { x // x ∈ s } := ⟨i✝, hi✝⟩
J : Set { x // x ∈ s }
hi : i ∈ J
v : E
j : { x // x ∈ s }
hj : j ∈ Jᶜ
hj_v : a j = v
h : ↑i ∈ s.erase ↑j
⊢ ↑i ∈ Membership.mem (s.val.erase ↑j)

Tactic:
assumption

Result:
no goals

Proof state:
𝕜 : Type u_2
E : Type u_3
inst✝³ : LinearOrderedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
n k : ℕ
h_card : finrank 𝕜 E + 1 ≤ k
hk :
  ∀ {ι : Type u_1} {F : ι → Set E} {s : Finset ι},
    (∀ i ∈ s, Convex 𝕜 (F i)) →
      (∀ I ⊆ s, #I ≤ finrank 𝕜 E + 1 → (⋂ i ∈ I, F i).Nonempty) → #s = k → (⋂ i ∈ s, F i).Nonempty
ι : Type u_1
F : ι → Set E
s : Finset ι
h_convex : ∀ i ∈ s, Convex 𝕜 (F i)
h_inter : ∀ I ⊆ s, #I ≤ finrank 𝕜 E + 1 → (⋂ i ∈ I, F i).Nonempty
hn : #s = k + 1
a : { x // x ∈ s } → E := fun i => ⋯.some
h_ind : ¬AffineIndependent 𝕜 a
I : Set { x // x ∈ s }
p : E
hp_I : p ∈ (convexHull 𝕜) (a '' I)
hp_Ic : p ∈ (convexHull 𝕜) (a '' Iᶜ)
i✝ : ι
hi : i✝ ∈ Membership.mem s.val
i : { x // x ∈ s } := ⟨i✝, hi⟩
this : ∀ (J : Set { x // x ∈ s }), i ∈ J → (convexHull 𝕜) (a '' Jᶜ) ⊆ F ↑i
⊢ p ∈ F i✝

Tactic:
by_cases h : i ∈ I

Result:
case pos
𝕜 : Type u_2
E : Type u_3
inst✝³ : LinearOrderedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
n k : ℕ
h_card : finrank 𝕜 E + 1 ≤ k
hk :
  ∀ {ι : Type u_1} {F : ι → Set E} {s : Finset ι},
    (∀ i ∈ s, Convex 𝕜 (F i)) →
      (∀ I ⊆ s, #I ≤ finrank 𝕜 E + 1 → (⋂ i ∈ I, F i).Nonempty) → #s = k → (⋂ i ∈ s, F i).Nonempty
ι : Type u_1
F : ι → Set E
s : Finset ι
h_convex : ∀ i ∈ s, Convex 𝕜 (F i)
h_inter : ∀ I ⊆ s, #I ≤ finrank 𝕜 E + 1 → (⋂ i ∈ I, F i).Nonempty
hn : #s = k + 1
a : { x // x ∈ s } → E := fun i => ⋯.some
h_ind : ¬AffineIndependent 𝕜 a
I : Set { x // x ∈ s }
p : E
hp_I : p ∈ (convexHull 𝕜) (a '' I)
hp_Ic : p ∈ (convexHull 𝕜) (a '' Iᶜ)
i✝ : ι
hi : i✝ ∈ Membership.mem s.val
i : { x // x ∈ s } := ⟨i✝, hi⟩
this : ∀ (J : Set { x // x ∈ s }), i ∈ J → (convexHull 𝕜) (a '' Jᶜ) ⊆ F ↑i
h : i ∈ I
⊢ p ∈ F i✝

case neg
𝕜 : Type u_2
E : Type u_3
inst✝³ : LinearOrderedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
n k : ℕ
h_card : finrank 𝕜 E + 1 ≤ k
hk :
  ∀ {ι : Type u_1} {F : ι → Set E} {s : Finset ι},
    (∀ i ∈ s, Convex 𝕜 (F i)) →
      (∀ I ⊆ s, #I ≤ finrank 𝕜 E + 1 → (⋂ i ∈ I, F i).Nonempty) → #s = k → (⋂ i ∈ s, F i).Nonempty
ι : Type u_1
F : ι → Set E
s : Finset ι
h_convex : ∀ i ∈ s, Convex 𝕜 (F i)
h_inter : ∀ I ⊆ s, #I ≤ finrank 𝕜 E + 1 → (⋂ i ∈ I, F i).Nonempty
hn : #s = k + 1
a : { x // x ∈ s } → E := fun i => ⋯.some
h_ind : ¬AffineIndependent 𝕜 a
I : Set { x // x ∈ s }
p : E
hp_I : p ∈ (convexHull 𝕜) (a '' I)
hp_Ic : p ∈ (convexHull 𝕜) (a '' Iᶜ)
i✝ : ι
hi : i✝ ∈ Membership.mem s.val
i : { x // x ∈ s } := ⟨i✝, hi⟩
this : ∀ (J : Set { x // x ∈ s }), i ∈ J → (convexHull 𝕜) (a '' Jᶜ) ⊆ F ↑i
h : i ∉ I
⊢ p ∈ F i✝

Proof state:
case h.h.intro.intro
𝕜 : Type u_2
E : Type u_3
inst✝³ : LinearOrderedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
n k : ℕ
h_card : finrank 𝕜 E + 1 ≤ k
hk :
  ∀ {ι : Type u_1} {F : ι → Set E} {s : Finset ι},
    (∀ i ∈ s, Convex 𝕜 (F i)) →
      (∀ I ⊆ s, #I ≤ finrank 𝕜 E + 1 → (⋂ i ∈ I, F i).Nonempty) → #s = k → (⋂ i ∈ s, F i).Nonempty
ι : Type u_1
F : ι → Set E
s : Finset ι
h_convex : ∀ i ∈ s, Convex 𝕜 (F i)
h_inter : ∀ I ⊆ s, #I ≤ finrank 𝕜 E + 1 → (⋂ i ∈ I, F i).Nonempty
hn : #s = k + 1
a : { x // x ∈ s } → E := fun i => ⋯.some
h_ind : ¬AffineIndependent 𝕜 a
I : Set { x // x ∈ s }
p : E
hp_I : p ∈ (convexHull 𝕜) (a '' I)
hp_Ic : p ∈ (convexHull 𝕜) (a '' Iᶜ)
i✝ : ι
hi✝ : i✝ ∈ Membership.mem s.val
i : { x // x ∈ s } := ⟨i✝, hi✝⟩
J : Set { x // x ∈ s }
hi : i ∈ J
v : E
j : { x // x ∈ s }
hj : j ∈ Jᶜ
hj_v : a j = v
⊢ a j ∈ F ↑i

Tactic:
apply mem_of_subset_of_mem (s₁ := ⋂ k ∈ (s.erase j), F k)

Result:
case h.h.intro.intro.h
𝕜 : Type u_2
E : Type u_3
inst✝³ : LinearOrderedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
n k : ℕ
h_card : finrank 𝕜 E + 1 ≤ k
hk :
  ∀ {ι : Type u_1} {F : ι → Set E} {s : Finset ι},
    (∀ i ∈ s, Convex 𝕜 (F i)) →
      (∀ I ⊆ s, #I ≤ finrank 𝕜 E + 1 → (⋂ i ∈ I, F i).Nonempty) → #s = k → (⋂ i ∈ s, F i).Nonempty
ι : Type u_1
F : ι → Set E
s : Finset ι
h_convex : ∀ i ∈ s, Convex 𝕜 (F i)
h_inter : ∀ I ⊆ s, #I ≤ finrank 𝕜 E + 1 → (⋂ i ∈ I, F i).Nonempty
hn : #s = k + 1
a : { x // x ∈ s } → E := fun i => ⋯.some
h_ind : ¬AffineIndependent 𝕜 a
I : Set { x // x ∈ s }
p : E
hp_I : p ∈ (convexHull 𝕜) (a '' I)
hp_Ic : p ∈ (convexHull 𝕜) (a '' Iᶜ)
i✝ : ι
hi✝ : i✝ ∈ Membership.mem s.val
i : { x // x ∈ s } := ⟨i✝, hi✝⟩
J : Set { x // x ∈ s }
hi : i ∈ J
v : E
j : { x // x ∈ s }
hj : j ∈ Jᶜ
hj_v : a j = v
⊢ ⋂ k ∈ s.erase ↑j, F k ⊆ F ↑i

case h.h.intro.intro.a
𝕜 : Type u_2
E : Type u_3
inst✝³ : LinearOrderedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
n k : ℕ
h_card : finrank 𝕜 E + 1 ≤ k
hk :
  ∀ {ι : Type u_1} {F : ι → Set E} {s : Finset ι},
    (∀ i ∈ s, Convex 𝕜 (F i)) →
      (∀ I ⊆ s, #I ≤ finrank 𝕜 E + 1 → (⋂ i ∈ I, F i).Nonempty) → #s = k → (⋂ i ∈ s, F i).Nonempty
ι : Type u_1
F : ι → Set E
s : Finset ι
h_convex : ∀ i ∈ s, Convex 𝕜 (F i)
h_inter : ∀ I ⊆ s, #I ≤ finrank 𝕜 E + 1 → (⋂ i ∈ I, F i).Nonempty
hn : #s = k + 1
a : { x // x ∈ s } → E := fun i => ⋯.some
h_ind : ¬AffineIndependent 𝕜 a
I : Set { x // x ∈ s }
p : E
hp_I : p ∈ (convexHull 𝕜) (a '' I)
hp_Ic : p ∈ (convexHull 𝕜) (a '' Iᶜ)
i✝ : ι
hi✝ : i✝ ∈ Membership.mem s.val
i : { x // x ∈ s } := ⟨i✝, hi✝⟩
J : Set { x // x ∈ s }
hi : i ∈ J
v : E
j : { x // x ∈ s }
hj : j ∈ Jᶜ
hj_v : a j = v
⊢ a j ∈ ⋂ k ∈ s.erase ↑j, F k