-- 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:
case h.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
⊢ a '' Jᶜ ⊆ F ↑i

Tactic:
rintro v ⟨j, hj, hj_v⟩

Result:
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
⊢ v ∈ F ↑i

Proof state:
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✝

Tactic:
exact this I h hp_Ic

Result:
no goals

Proof state:
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

Tactic:
apply biInter_subset_of_mem

Result:
case h.h.intro.intro.h.xs
𝕜 : 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
⊢ ↑i ∈ Membership.mem (s.erase ↑j).val

Proof state:
case h.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
⊢ p ∈ F i

Tactic:
let i : s := ⟨i, hi⟩

Result:
case h.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⟩
⊢ p ∈ F i✝

Proof state:
case inr
ι : Type u_1
𝕜 : Type u_2
E : Type u_3
inst✝³ : LinearOrderedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
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
h_card : finrank 𝕜 E + 1 ≤ #s
⊢ (⋂ i ∈ s, F i).Nonempty

Tactic:
generalize hn : #s = n

Result:
case inr
ι : Type u_1
𝕜 : Type u_2
E : Type u_3
inst✝³ : LinearOrderedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
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
h_card : finrank 𝕜 E + 1 ≤ #s
n : ℕ
hn : #s = n
⊢ (⋂ i ∈ s, F i).Nonempty