-- 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.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.val.erase ↑j)

Tactic:
suffices h : i.val ∈ s.erase j by assumption

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 ∈ s.erase ↑j

Proof state:
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 ∈ s.erase ↑j

Tactic:
simp only [mem_erase]

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 ≠ ↑j ∧ ↑i ∈ s

Proof state:
case h.h.intro.intro.h.xs.right
𝕜 : 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 ∈ s

Tactic:
assumption

Result:
no goals

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

Tactic:
apply Nonempty.some_mem

Result:
no goals