-- Mathlib/Analysis/Convex/Radon.lean
theorem helly_theorem_compact [TopologicalSpace E] [T2Space E] {F : ι → Set E}
    (h_card : 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 → (⋂ i ∈ I, F i).Nonempty) :
    (⋂ i, F i).Nonempty

Proof state:
ι : Type u_1
𝕜 : Type u_2
E : Type u_3
inst✝⁵ : LinearOrderedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : FiniteDimensional 𝕜 E
inst✝¹ : TopologicalSpace E
inst✝ : T2Space E
F : ι → Set E
h_card : ↑(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 → (⋂ i ∈ I, F i).Nonempty
I : Finset ι
hI_card : #I ≤ finrank 𝕜 E + 1
⊢ ∃ J, I ⊆ J ∧ #J = finrank 𝕜 E + 1

Tactic:
by_cases h : Infinite ι

Result:
case pos
ι : Type u_1
𝕜 : Type u_2
E : Type u_3
inst✝⁵ : LinearOrderedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : FiniteDimensional 𝕜 E
inst✝¹ : TopologicalSpace E
inst✝ : T2Space E
F : ι → Set E
h_card : ↑(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 → (⋂ i ∈ I, F i).Nonempty
I : Finset ι
hI_card : #I ≤ finrank 𝕜 E + 1
h : Infinite ι
⊢ ∃ J, I ⊆ J ∧ #J = finrank 𝕜 E + 1

case neg
ι : Type u_1
𝕜 : Type u_2
E : Type u_3
inst✝⁵ : LinearOrderedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : FiniteDimensional 𝕜 E
inst✝¹ : TopologicalSpace E
inst✝ : T2Space E
F : ι → Set E
h_card : ↑(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 → (⋂ i ∈ I, F i).Nonempty
I : Finset ι
hI_card : #I ≤ finrank 𝕜 E + 1
h : ¬Infinite ι
⊢ ∃ J, I ⊆ J ∧ #J = finrank 𝕜 E + 1

Proof state:
case intro.intro
ι : Type u_1
𝕜 : Type u_2
E : Type u_3
inst✝⁵ : LinearOrderedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : FiniteDimensional 𝕜 E
inst✝¹ : TopologicalSpace E
inst✝ : T2Space E
F : ι → Set E
h_card : ↑(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 → (⋂ i ∈ I, F i).Nonempty
I : Finset ι
hI_card : #I ≤ finrank 𝕜 E + 1
J : Finset ι
hJ_ss : I ⊆ J
hJ_card : #J = finrank 𝕜 E + 1
⊢ (⋂ i ∈ I, F i).Nonempty

Tactic:
apply Set.Nonempty.mono <| biInter_mono hJ_ss (by intro _ _; rfl)

Result:
case intro.intro
ι : Type u_1
𝕜 : Type u_2
E : Type u_3
inst✝⁵ : LinearOrderedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : FiniteDimensional 𝕜 E
inst✝¹ : TopologicalSpace E
inst✝ : T2Space E
F : ι → Set E
h_card : ↑(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 → (⋂ i ∈ I, F i).Nonempty
I : Finset ι
hI_card : #I ≤ finrank 𝕜 E + 1
J : Finset ι
hJ_ss : I ⊆ J
hJ_card : #J = finrank 𝕜 E + 1
⊢ (⋂ x ∈ Membership.mem J.val, F x).Nonempty

Proof state:
case intro.intro
ι : Type u_1
𝕜 : Type u_2
E : Type u_3
inst✝⁵ : LinearOrderedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : FiniteDimensional 𝕜 E
inst✝¹ : TopologicalSpace E
inst✝ : T2Space E
F : ι → Set E
h_card : ↑(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 → (⋂ i ∈ I, F i).Nonempty
I : Finset ι
hI_card : #I ≤ finrank 𝕜 E + 1
J : Finset ι
hJ_ss : I ⊆ J
hJ_card : #J = finrank 𝕜 E + 1
⊢ (⋂ x ∈ Membership.mem J.val, F x).Nonempty

Tactic:
exact h_inter J hJ_card

Result:
no goals

Proof state:
ι : Type u_1
𝕜 : Type u_2
E : Type u_3
inst✝⁵ : LinearOrderedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : FiniteDimensional 𝕜 E
inst✝¹ : TopologicalSpace E
inst✝ : T2Space E
F : ι → Set E
h_card : ↑(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 → (⋂ i ∈ I, F i).Nonempty
⊢ ∀ (I : Finset ι), #I ≤ finrank 𝕜 E + 1 → (⋂ i ∈ I, F i).Nonempty

Tactic:
intro I hI_card

Result:
ι : Type u_1
𝕜 : Type u_2
E : Type u_3
inst✝⁵ : LinearOrderedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : FiniteDimensional 𝕜 E
inst✝¹ : TopologicalSpace E
inst✝ : T2Space E
F : ι → Set E
h_card : ↑(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 → (⋂ i ∈ I, F i).Nonempty
I : Finset ι
hI_card : #I ≤ finrank 𝕜 E + 1
⊢ (⋂ i ∈ I, F i).Nonempty

Proof state:
case neg
ι : Type u_1
𝕜 : Type u_2
E : Type u_3
inst✝⁵ : LinearOrderedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : FiniteDimensional 𝕜 E
inst✝¹ : TopologicalSpace E
inst✝ : T2Space E
F : ι → Set E
h_card : ↑(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 → (⋂ i ∈ I, F i).Nonempty
I : Finset ι
hI_card : #I ≤ finrank 𝕜 E + 1
h : ¬Infinite ι
this✝ : Finite ι
this : Fintype ι
⊢ finrank 𝕜 E + 1 ≤ Fintype.card ι

Tactic:
simp only [ENat.card_eq_coe_fintype_card] at h_card

Result:
case neg
ι : Type u_1
𝕜 : Type u_2
E : Type u_3
inst✝⁵ : LinearOrderedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : FiniteDimensional 𝕜 E
inst✝¹ : TopologicalSpace E
inst✝ : 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 → (⋂ i ∈ I, F i).Nonempty
I : Finset ι
hI_card : #I ≤ finrank 𝕜 E + 1
h : ¬Infinite ι
this✝ : Finite ι
this : Fintype ι
h_card : ↑(finrank 𝕜 E) + 1 ≤ ↑(Fintype.card ι)
⊢ finrank 𝕜 E + 1 ≤ Fintype.card ι

Proof state:
ι : Type u_1
𝕜 : Type u_2
E : Type u_3
inst✝⁵ : LinearOrderedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : FiniteDimensional 𝕜 E
inst✝¹ : TopologicalSpace E
inst✝ : T2Space E
F : ι → Set E
h_card : ↑(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 → (⋂ i ∈ I, F i).Nonempty
I : Finset ι
hI_card : #I ≤ finrank 𝕜 E + 1
hJ : ∃ J, I ⊆ J ∧ #J = finrank 𝕜 E + 1
⊢ (⋂ i ∈ I, F i).Nonempty

Tactic:
obtain ⟨J, hJ_ss, hJ_card⟩ := hJ

Result:
case intro.intro
ι : Type u_1
𝕜 : Type u_2
E : Type u_3
inst✝⁵ : LinearOrderedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : FiniteDimensional 𝕜 E
inst✝¹ : TopologicalSpace E
inst✝ : T2Space E
F : ι → Set E
h_card : ↑(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 → (⋂ i ∈ I, F i).Nonempty
I : Finset ι
hI_card : #I ≤ finrank 𝕜 E + 1
J : Finset ι
hJ_ss : I ⊆ J
hJ_card : #J = finrank 𝕜 E + 1
⊢ (⋂ i ∈ I, F i).Nonempty

Proof state:
case neg
ι : Type u_1
𝕜 : Type u_2
E : Type u_3
inst✝⁵ : LinearOrderedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : FiniteDimensional 𝕜 E
inst✝¹ : TopologicalSpace E
inst✝ : 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 → (⋂ i ∈ I, F i).Nonempty
I : Finset ι
hI_card : #I ≤ finrank 𝕜 E + 1
h : ¬Infinite ι
this✝ : Finite ι
this : Fintype ι
h_card : ↑(finrank 𝕜 E) + 1 ≤ ↑(Fintype.card ι)
⊢ finrank 𝕜 E + 1 ≤ Fintype.card ι

Tactic:
rwa [← Nat.cast_one, ← Nat.cast_add, Nat.cast_le] at h_card

Result:
no goals