awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Convex.Radon
Goal:
ι : Type u_1
𝕜 : Type u_2
E : Type u_3
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
inst_5 : FiniteDimensional 𝕜 E
inst_6 : TopologicalSpace E
inst_7 : T2Space E
F : ι → Set E
h_card : HAdd.hAdd (α := ℕ∞) (↑(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 → Set.Nonempty.{u_3} (α := E) (⋂ i ∈ I, F i)
I : Finset ι
hI_card : #I ≤ finrank 𝕜 E + 1
pos : ∀ (h : Infinite ι), ∃ (J : Finset ι), I ⊆ J ∧ #J = finrank 𝕜 E + 1
neg : ∀ (h : ¬Infinite ι), ∃ (J : Finset ι), I ⊆ J ∧ #J = finrank 𝕜 E + 1
⊢ ∃ (J : Finset ι), I ⊆ J ∧ #J = finrank 𝕜 E + 1

Tactic:
by_cases h : Infinite ι

Premises used: Infinite
-- Module: Mathlib.Analysis.Convex.Radon
Goal:
ι : Type u_1
𝕜 : Type u_2
E : Type u_3
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
inst_5 : FiniteDimensional 𝕜 E
inst_6 : TopologicalSpace E
inst_7 : T2Space E
F : ι → Set E
h_card : HAdd.hAdd (α := ℕ∞) (↑(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 → Set.Nonempty.{u_3} (α := E) (⋂ i ∈ I, F i)
I : Finset ι
hI_card : #I ≤ finrank 𝕜 E + 1
h : Infinite ι
⊢ ∃ (J : Finset ι), I ⊆ J ∧ #J = finrank 𝕜 E + 1

Tactic:
Infinite.exists_superset_card_eq _ _ hI_card

Premises used: Infinite.exists_superset_card_eq
-- Module: Mathlib.Analysis.Convex.Radon
Goal:
ι : Type u_1
𝕜 : Type u_2
E : Type u_3
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
inst_5 : FiniteDimensional 𝕜 E
inst_6 : TopologicalSpace E
inst_7 : T2Space E
F : ι → Set E
h_card : HAdd.hAdd (α := ℕ∞) (↑(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 → Set.Nonempty.{u_3} (α := E) (⋂ i ∈ I, F i)
I : Finset ι
hI_card : #I ≤ finrank 𝕜 E + 1
h : Infinite ι
⊢ ∃ (J : Finset ι), I ⊆ J ∧ #J = finrank 𝕜 E + 1

Tactic:
exact Infinite.exists_superset_card_eq _ _ hI_card

Premises used: Infinite.exists_superset_card_eq
-- Module: Mathlib.Analysis.Convex.Radon
Goal:
ι : Type u_1
𝕜 : Type u_2
E : Type u_3
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
inst_5 : FiniteDimensional 𝕜 E
inst_6 : TopologicalSpace E
inst_7 : T2Space E
F : ι → Set E
h_card : HAdd.hAdd (α := ℕ∞) (↑(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 → Set.Nonempty.{u_3} (α := E) (⋂ i ∈ I, F i)
I : Finset ι
hI_card : #I ≤ finrank 𝕜 E + 1
h : ¬Infinite ι
⊢ Finite ι

Tactic:
have : Finite ι := Finite.of_not_infinite h
-- Module: Mathlib.Analysis.Convex.Radon
Goal:
ι : Type u_1
𝕜 : Type u_2
E : Type u_3
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
inst_5 : FiniteDimensional 𝕜 E
inst_6 : TopologicalSpace E
inst_7 : T2Space E
F : ι → Set E
h_card : HAdd.hAdd (α := ℕ∞) (↑(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 → Set.Nonempty.{u_3} (α := E) (⋂ i ∈ I, F i)
I : Finset ι
hI_card : #I ≤ finrank 𝕜 E + 1
h : ¬Infinite ι
this : Finite ι
neg : ∀ (this : Fintype ι), ∃ (J : Finset ι), I ⊆ J ∧ #J = finrank 𝕜 E + 1
⊢ ∃ (J : Finset ι), I ⊆ J ∧ #J = finrank 𝕜 E + 1

Tactic:
have : Fintype ι := Fintype.ofFinite ι
-- Module: Mathlib.Analysis.Convex.Radon
Goal:
ι : Type u_1
𝕜 : Type u_2
E : Type u_3
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
inst_5 : FiniteDimensional 𝕜 E
inst_6 : TopologicalSpace E
inst_7 : T2Space E
F : ι → Set E
h_card : HAdd.hAdd (α := ℕ∞) (↑(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 → Set.Nonempty.{u_3} (α := E) (⋂ i ∈ I, F i)
I : Finset ι
hI_card : #I ≤ finrank 𝕜 E + 1
h : ¬Infinite ι
this_1 : Finite ι
this : Fintype ι
neg : finrank 𝕜 E + 1 ≤ Fintype.card ι
⊢ ∃ (J : Finset ι), I ⊆ J ∧ #J = finrank 𝕜 E + 1

Tactic:
apply exists_superset_card_eq hI_card

Premises used: Finset.exists_superset_card_eq
-- Module: Mathlib.Analysis.Convex.Radon
Goal:
ι : Type u_1
𝕜 : Type u_2
E : Type u_3
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
inst_5 : FiniteDimensional 𝕜 E
inst_6 : TopologicalSpace E
inst_7 : T2Space E
F : ι → Set E
h_card : HAdd.hAdd (α := ℕ∞) (↑(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 → Set.Nonempty.{u_3} (α := E) (⋂ i ∈ I, F i)
I : Finset ι
hI_card : #I ≤ finrank 𝕜 E + 1
h : ¬Infinite ι
this_1 : Finite ι
this : Fintype ι
⊢ HAdd.hAdd (α := ℕ∞) (↑(finrank 𝕜 E) : ℕ∞) 1 ≤ (↑(Fintype.card ι) : ℕ∞)

Tactic:
simp only [ENat.card_eq_coe_fintype_card] at h_card

Premises used: ENat.card_eq_coe_fintype_card
-- Module: Mathlib.Analysis.Convex.Radon
Goal:
ι : Type u_1
𝕜 : Type u_2
E : Type u_3
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
inst_5 : FiniteDimensional 𝕜 E
inst_6 : TopologicalSpace E
inst_7 : 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 → Set.Nonempty.{u_3} (α := E) (⋂ i ∈ I, F i)
I : Finset ι
hI_card : #I ≤ finrank 𝕜 E + 1
h : ¬Infinite ι
this_1 : Finite ι
this : Fintype ι
h_card : HAdd.hAdd (α := ℕ∞) (↑(finrank 𝕜 E) : ℕ∞) 1 ≤ (↑(Fintype.card ι) : ℕ∞)
neg :
  ∀ (h_card : HAdd.hAdd (α := ℕ∞) (↑(finrank 𝕜 E) : ℕ∞) (↑1 : ℕ∞) ≤ (↑(Fintype.card ι) : ℕ∞)),
    finrank 𝕜 E + 1 ≤ Fintype.card ι
neg₁ : ∀ (h_card : LE.le (α := ℕ∞) (↑(finrank 𝕜 E + 1) : ℕ∞) (↑(Fintype.card ι) : ℕ∞)), finrank 𝕜 E + 1 ≤ Fintype.card ι
neg₂ neg₃ neg₄ neg₅ : ∀ (h_card : finrank 𝕜 E + 1 ≤ Fintype.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

Premises used: Nat.cast_add, Nat.cast_le, Nat.cast_one
-- Module: Mathlib.Analysis.Convex.Radon
Goal:
ι : Type u_1
𝕜 : Type u_2
E : Type u_3
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
inst_5 : FiniteDimensional 𝕜 E
inst_6 : TopologicalSpace E
inst_7 : T2Space E
F : ι → Set E
h_card : HAdd.hAdd (α := ℕ∞) (↑(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 → Set.Nonempty.{u_3} (α := E) (⋂ i ∈ I, F i)
I : Finset ι
hI_card : #I ≤ finrank 𝕜 E + 1
⊢ ∃ (J : Finset ι), I ⊆ J ∧ #J = finrank 𝕜 E + 1

Tactic:
have hJ : ∃ J : Finset ι, I ⊆ J ∧ #J = finrank 𝕜 E + 1 := by
    by_cases h : Infinite ι
    · exact Infinite.exists_superset_card_eq _ _ hI_card
    · have : Finite ι := Finite.of_not_infinite h
      have : Fintype ι := Fintype.ofFinite ι
      apply exists_superset_card_eq hI_card
      simp only [ENat.card_eq_coe_fintype_card] at h_card
      rwa [← Nat.cast_one, ← Nat.cast_add, Nat.cast_le] at h_card
-- Module: Mathlib.Analysis.Convex.Radon
Goal:
ι : Type u_1
𝕜 : Type u_2
E : Type u_3
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
inst_5 : FiniteDimensional 𝕜 E
inst_6 : TopologicalSpace E
inst_7 : T2Space E
F : ι → Set E
h_card : HAdd.hAdd (α := ℕ∞) (↑(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 → Set.Nonempty.{u_3} (α := E) (⋂ i ∈ I, F i)
I : Finset ι
hI_card : #I ≤ finrank 𝕜 E + 1
hJ : ∃ (J : Finset ι), I ⊆ J ∧ #J = finrank 𝕜 E + 1
obtain : ∀ (J : Finset ι) (hJ_ss : I ⊆ J) (hJ_card : #J = finrank 𝕜 E + 1), Set.Nonempty.{u_3} (α := E) (⋂ i ∈ I, F i)
⊢ Set.Nonempty.{u_3} (α := E) (⋂ i ∈ I, F i)

Tactic:
obtain ⟨J, hJ_ss, hJ_card⟩ := hJ
-- Module: Mathlib.Analysis.Convex.Radon
Goal:
ι : Type u_1
𝕜 : Type u_2
E : Type u_3
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
inst_5 : FiniteDimensional 𝕜 E
inst_6 : TopologicalSpace E
inst_7 : T2Space E
F : ι → Set E
h_card : HAdd.hAdd (α := ℕ∞) (↑(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 → Set.Nonempty.{u_3} (α := E) (⋂ i ∈ I, F i)
I : Finset ι
hI_card : #I ≤ finrank 𝕜 E + 1
J : Finset ι
hJ_ss : I ⊆ J
hJ_card : #J = finrank 𝕜 E + 1
x : ι
_ : x ∈ (↑I : Set ι) → F x ⊆ F x
⊢ x ∈ (↑I : Set ι) → F x ⊆ F x

Tactic:
_
-- Module: Mathlib.Analysis.Convex.Radon
Goal:
ι : Type u_1
𝕜 : Type u_2
E : Type u_3
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
inst_5 : FiniteDimensional 𝕜 E
inst_6 : TopologicalSpace E
inst_7 : T2Space E
F : ι → Set E
h_card : HAdd.hAdd (α := ℕ∞) (↑(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 → Set.Nonempty.{u_3} (α := E) (⋂ i ∈ I, F i)
I : Finset ι
hI_card : #I ≤ finrank 𝕜 E + 1
J : Finset ι
hJ_ss : I ⊆ J
hJ_card : #J = finrank 𝕜 E + 1
x : ι
h : x ∈ (↑I : Set ι)
⊢ F x ⊆ F x

Tactic:
rfl
-- Module: Mathlib.Analysis.Convex.Radon
Goal:
ι : Type u_1
𝕜 : Type u_2
E : Type u_3
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
inst_5 : FiniteDimensional 𝕜 E
inst_6 : TopologicalSpace E
inst_7 : T2Space E
F : ι → Set E
h_card : HAdd.hAdd (α := ℕ∞) (↑(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 → Set.Nonempty.{u_3} (α := E) (⋂ i ∈ I, F i)
I : Finset ι
hI_card : #I ≤ finrank 𝕜 E + 1
J : Finset ι
hJ_ss : I ⊆ J
hJ_card : #J = finrank 𝕜 E + 1
apply : Set.Nonempty.{u_3} (α := E) (⋂ x ∈ (↑J : Set ι), F x)
⊢ Set.Nonempty.{u_3} (α := E) (⋂ i ∈ I, F i)

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

Premises used: Set.biInter_mono, Set.Nonempty.mono
-- Module: Mathlib.Analysis.Convex.Radon
Goal:
ι : Type u_1
𝕜 : Type u_2
E : Type u_3
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
inst_5 : FiniteDimensional 𝕜 E
inst_6 : TopologicalSpace E
inst_7 : T2Space E
F : ι → Set E
h_card : HAdd.hAdd (α := ℕ∞) (↑(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 → Set.Nonempty.{u_3} (α := E) (⋂ i ∈ I, F i)
I : Finset ι
hI_card : #I ≤ finrank 𝕜 E + 1
J : Finset ι
hJ_ss : I ⊆ J
hJ_card : #J = finrank 𝕜 E + 1
⊢ Set.Nonempty.{u_3} (α := E) (⋂ x ∈ (↑J : Set ι), F x)

Tactic:
h_inter J hJ_card
-- Module: Mathlib.Analysis.Convex.Radon
Goal:
ι : Type u_1
𝕜 : Type u_2
E : Type u_3
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
inst_5 : FiniteDimensional 𝕜 E
inst_6 : TopologicalSpace E
inst_7 : T2Space E
F : ι → Set E
h_card : HAdd.hAdd (α := ℕ∞) (↑(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 → Set.Nonempty.{u_3} (α := E) (⋂ i ∈ I, F i)
I : Finset ι
hI_card : #I ≤ finrank 𝕜 E + 1
J : Finset ι
hJ_ss : I ⊆ J
hJ_card : #J = finrank 𝕜 E + 1
⊢ Set.Nonempty.{u_3} (α := E) (⋂ x ∈ (↑J : Set ι), F x)

Tactic:
exact h_inter J hJ_card
-- Module: Mathlib.Analysis.Convex.Radon
Goal:
𝕜 : Type u_2
E : Type u_3
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
inst_5 : FiniteDimensional 𝕜 E
inst_6 : TopologicalSpace E
inst_7 : T2Space E
F : Set (Set E)
h_convex : ∀ X ∈ F, Convex 𝕜 X
h_compact : ∀ X ∈ F, IsCompact X
h_inter : ∀ (G : Finset (Set E)), (↑G : Set (Set E)) ⊆ F → #G ≤ finrank 𝕜 E + 1 → (⋂₀ (↑G : Set (Set E))).Nonempty
h : ∀ (x : E), x ∈ ⋂₀ F ↔ Membership.mem (γ := Set E) (⋂ (X : (↑F : Type u_3)), (↑X : Set E)) x
⊢ ⋂₀ F = ⋂ (X : (↑F : Type u_3)), (↑X : Set E)

Tactic:
ext
-- Module: Mathlib.Analysis.Convex.Radon
Goal:
𝕜 : Type u_2
E : Type u_3
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
inst_5 : FiniteDimensional 𝕜 E
inst_6 : TopologicalSpace E
inst_7 : T2Space E
F : Set (Set E)
h_convex : ∀ X ∈ F, Convex 𝕜 X
h_compact : ∀ X ∈ F, IsCompact X
h_inter : ∀ (G : Finset (Set E)), (↑G : Set (Set E)) ⊆ F → #G ≤ finrank 𝕜 E + 1 → (⋂₀ (↑G : Set (Set E))).Nonempty
x : E
⊢ x ∈ ⋂₀ F ↔ Membership.mem (γ := Set E) (⋂ (X : (↑F : Type u_3)), (↑X : Set E)) x

Tactic:
simp
-- Module: Mathlib.Analysis.Convex.Radon
Goal:
𝕜 : Type u_2
E : Type u_3
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
inst_5 : FiniteDimensional 𝕜 E
inst_6 : TopologicalSpace E
inst_7 : T2Space E
F : Set (Set E)
h_convex : ∀ X ∈ F, Convex 𝕜 X
h_compact : ∀ X ∈ F, IsCompact X
h_inter : ∀ (G : Finset (Set E)), (↑G : Set (Set E)) ⊆ F → #G ≤ finrank 𝕜 E + 1 → (⋂₀ (↑G : Set (Set E))).Nonempty
rw : Set.Nonempty.{u_3} (α := E) (⋂ (X : (↑F : Type u_3)), (↑X : Set E))
⊢ (⋂₀ F).Nonempty

Tactic:
rw [show ⋂₀ F = ⋂ X : F, (X : Set E) by ext; simp]
-- Module: Mathlib.Analysis.Convex.Radon
Goal:
𝕜 : Type u_2
E : Type u_3
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
inst_5 : FiniteDimensional 𝕜 E
inst_6 : TopologicalSpace E
inst_7 : T2Space E
F : Set (Set E)
h_convex : ∀ X ∈ F, Convex 𝕜 X
h_compact : ∀ X ∈ F, IsCompact X
h_inter : ∀ (G : Finset (Set E)), (↑G : Set (Set E)) ⊆ F → #G ≤ finrank 𝕜 E + 1 → (⋂₀ (↑G : Set (Set E))).Nonempty
X : (↑F : Type u_3)
⊢ (↑X : Set E) ∈ F

Tactic:
simp
-- Module: Mathlib.Analysis.Convex.Radon
Goal:
𝕜 : Type u_2
E : Type u_3
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
inst_5 : FiniteDimensional 𝕜 E
inst_6 : TopologicalSpace E
inst_7 : T2Space E
F : Set (Set E)
h_convex : ∀ X ∈ F, Convex 𝕜 X
h_compact : ∀ X ∈ F, IsCompact X
h_inter : ∀ (G : Finset (Set E)), (↑G : Set (Set E)) ⊆ F → #G ≤ finrank 𝕜 E + 1 → (⋂₀ (↑G : Set (Set E))).Nonempty
refine :
  ∀ (I : Finset (↑F : Type u_3)),
    #I ≤ finrank 𝕜 E + 1 → Set.Nonempty.{u_3} (α := E) (⋂ i ∈ I, (fun (x : (↑F : Type u_3)) ↦ (↑x : Set E)) i)
⊢ Set.Nonempty.{u_3} (α := E) (⋂ (X : (↑F : Type u_3)), (↑X : Set E))

Tactic:
refine helly_theorem_compact' (F := fun x : F ↦ x.val)
    (fun X ↦ h_convex X (by simp)) (fun X ↦ h_compact X (by simp)) ?_

Premises used: Convex.helly_theorem_compact', Subtype.val
-- Module: Mathlib.Analysis.Convex.Radon
Goal:
𝕜 : Type u_2
E : Type u_3
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
inst_5 : FiniteDimensional 𝕜 E
inst_6 : TopologicalSpace E
inst_7 : T2Space E
F : Set (Set E)
h_convex : ∀ X ∈ F, Convex 𝕜 X
h_compact : ∀ X ∈ F, IsCompact X
h_inter : ∀ (G : Finset (Set E)), (↑G : Set (Set E)) ⊆ F → #G ≤ finrank 𝕜 E + 1 → (⋂₀ (↑G : Set (Set E))).Nonempty
G : Finset (↑F : Type u_3)
_ : #G ≤ finrank 𝕜 E + 1 → Set.Nonempty.{u_3} (α := E) (⋂ i ∈ G, (fun (x : (↑F : Type u_3)) ↦ (↑x : Set E)) i)
⊢ #G ≤ finrank 𝕜 E + 1 → Set.Nonempty.{u_3} (α := E) (⋂ i ∈ G, (fun (x : (↑F : Type u_3)) ↦ (↑x : Set E)) i)

Tactic:
_
-- Module: Mathlib.Analysis.Convex.Radon
Goal:
𝕜 : Type u_2
E : Type u_3
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
inst_5 : FiniteDimensional 𝕜 E
inst_6 : TopologicalSpace E
inst_7 : T2Space E
F : Set (Set E)
h_convex : ∀ X ∈ F, Convex 𝕜 X
h_compact : ∀ X ∈ F, IsCompact X
h_inter : ∀ (G : Finset (Set E)), (↑G : Set (Set E)) ⊆ F → #G ≤ finrank 𝕜 E + 1 → (⋂₀ (↑G : Set (Set E))).Nonempty
G : Finset (↑F : Type u_3)
h : #G ≤ finrank 𝕜 E + 1
G' : Finset (Set E) := Finset.image (Subtype.val (p := fun (x : Set E) ↦ x ∈ F)) G
⊢ ⋂ i ∈ G, (↑i : Set E) = ⋂₀ (↑G' : Set (Set E))

Tactic:
simp [G']
-- Module: Mathlib.Analysis.Convex.Radon
Goal:
𝕜 : Type u_2
E : Type u_3
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
inst_5 : FiniteDimensional 𝕜 E
inst_6 : TopologicalSpace E
inst_7 : T2Space E
F : Set (Set E)
h_convex : ∀ X ∈ F, Convex 𝕜 X
h_compact : ∀ X ∈ F, IsCompact X
h_inter : ∀ (G : Finset (Set E)), (↑G : Set (Set E)) ⊆ F → #G ≤ finrank 𝕜 E + 1 → (⋂₀ (↑G : Set (Set E))).Nonempty
G : Finset (↑F : Type u_3)
h : #G ≤ finrank 𝕜 E + 1
G' : Finset (Set E) := Finset.image (Subtype.val (p := fun (x : Set E) ↦ x ∈ F)) G
rw : (⋂₀ (↑G' : Set (Set E))).Nonempty
⊢ Set.Nonempty.{u_3} (α := E) (⋂ i ∈ G, (fun (x : (↑F : Type u_3)) ↦ (↑x : Set E)) i)

Tactic:
rw [show ⋂ i ∈ G, ↑i = ⋂₀ (G' : Set (Set E)) by simp [G']]
-- Module: Mathlib.Analysis.Convex.Radon
Goal:
𝕜 : Type u_2
E : Type u_3
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
inst_5 : FiniteDimensional 𝕜 E
inst_6 : TopologicalSpace E
inst_7 : T2Space E
F : Set (Set E)
h_convex : ∀ X ∈ F, Convex 𝕜 X
h_compact : ∀ X ∈ F, IsCompact X
h_inter : ∀ (G : Finset (Set E)), (↑G : Set (Set E)) ⊆ F → #G ≤ finrank 𝕜 E + 1 → (⋂₀ (↑G : Set (Set E))).Nonempty
G : Finset (↑F : Type u_3)
h : #G ≤ finrank 𝕜 E + 1
G' : Finset (Set E) := Finset.image (Subtype.val (p := fun (x : Set E) ↦ x ∈ F)) G
a : (↑G' : Set (Set E)) ⊆ F
a₁ : #G' ≤ finrank 𝕜 E + 1
⊢ (⋂₀ (↑G' : Set (Set E))).Nonempty

Tactic:
apply h_inter G'
-- Module: Mathlib.Analysis.Convex.Radon
Goal:
𝕜 : Type u_2
E : Type u_3
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
inst_5 : FiniteDimensional 𝕜 E
inst_6 : TopologicalSpace E
inst_7 : T2Space E
F : Set (Set E)
h_convex : ∀ X ∈ F, Convex 𝕜 X
h_compact : ∀ X ∈ F, IsCompact X
h_inter : ∀ (G : Finset (Set E)), (↑G : Set (Set E)) ⊆ F → #G ≤ finrank 𝕜 E + 1 → (⋂₀ (↑G : Set (Set E))).Nonempty
G : Finset (↑F : Type u_3)
h : #G ≤ finrank 𝕜 E + 1
G' : Finset (Set E) := Finset.image (Subtype.val (p := fun (x : Set E) ↦ x ∈ F)) G
⊢ (↑G' : Set (Set E)) ⊆ F

Tactic:
simp [G']
-- Module: Mathlib.Analysis.Convex.Radon
Goal:
𝕜 : Type u_2
E : Type u_3
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
inst_5 : FiniteDimensional 𝕜 E
inst_6 : TopologicalSpace E
inst_7 : T2Space E
F : Set (Set E)
h_convex : ∀ X ∈ F, Convex 𝕜 X
h_compact : ∀ X ∈ F, IsCompact X
h_inter : ∀ (G : Finset (Set E)), (↑G : Set (Set E)) ⊆ F → #G ≤ finrank 𝕜 E + 1 → (⋂₀ (↑G : Set (Set E))).Nonempty
G : Finset (↑F : Type u_3)
h : #G ≤ finrank 𝕜 E + 1
G' : Finset (Set E) := Finset.image (Subtype.val (p := fun (x : Set E) ↦ x ∈ F)) G
a : #G ≤ finrank 𝕜 E + 1
⊢ #G' ≤ finrank 𝕜 E + 1

Tactic:
apply le_trans card_image_le

Premises used: Finset.card_image_le, le_trans
-- Module: Mathlib.Analysis.Convex.Radon
Goal:
𝕜 : Type u_2
E : Type u_3
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
inst_5 : FiniteDimensional 𝕜 E
inst_6 : TopologicalSpace E
inst_7 : T2Space E
F : Set (Set E)
h_convex : ∀ X ∈ F, Convex 𝕜 X
h_compact : ∀ X ∈ F, IsCompact X
h_inter : ∀ (G : Finset (Set E)), (↑G : Set (Set E)) ⊆ F → #G ≤ finrank 𝕜 E + 1 → (⋂₀ (↑G : Set (Set E))).Nonempty
G : Finset (↑F : Type u_3)
h : #G ≤ finrank 𝕜 E + 1
G' : Finset (Set E) := Finset.image (Subtype.val (p := fun (x : Set E) ↦ x ∈ F)) G
⊢ #G ≤ finrank 𝕜 E + 1

Tactic:
assumption
-- Module: Mathlib.Analysis.Convex.Radon
Goal:
𝕜 : Type u_2
E : Type u_3
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
inst_5 : FiniteDimensional 𝕜 E
inst_6 : TopologicalSpace E
inst_7 : T2Space E
F : Set (Set E)
h_convex : ∀ X ∈ F, Convex 𝕜 X
h_compact : ∀ X ∈ F, IsCompact X
h_inter : ∀ (G : Finset (Set E)), (↑G : Set (Set E)) ⊆ F → #G ≤ finrank 𝕜 E + 1 → (⋂₀ (↑G : Set (Set E))).Nonempty
classical classical₁ classical₂ : Set.Nonempty.{u_3} (α := E) (⋂ (X : (↑F : Type u_3)), (↑X : Set E))
classical₃ classical₄ :
  ∀ (G : Finset (↑F : Type u_3)),
    #G ≤ finrank 𝕜 E + 1 → Set.Nonempty.{u_3} (α := E) (⋂ i ∈ G, (fun (x : (↑F : Type u_3)) ↦ (↑x : Set E)) i)
classical₅ :
  ∀ (G : Finset (↑F : Type u_3)),
    #G ≤ finrank 𝕜 E + 1 → Set.Nonempty.{u_3} (α := E) (⋂ i ∈ G, (fun (x : (↑F : Type u_3)) ↦ (↑x : Set E)) i)
classical₆ :
  ∀ (G : Finset (↑F : Type u_3)),
    #G ≤ finrank 𝕜 E + 1 →
      let G' := Finset.image (Subtype.val (p := fun (x : Set E) ↦ x ∈ F)) G;
      (⋂₀ (↑G' : Set (Set E))).Nonempty
a :
  ∀ (G : Finset (↑F : Type u_3)),
    #G ≤ finrank 𝕜 E + 1 →
      let G' := Finset.image (Subtype.val (p := fun (x : Set E) ↦ x ∈ F)) G;
      (↑G' : Set (Set E)) ⊆ F
a₁ a₂ :
  ∀ (G : Finset (↑F : Type u_3)),
    #G ≤ finrank 𝕜 E + 1 →
      let G' := Finset.image (Subtype.val (p := fun (x : Set E) ↦ x ∈ F)) G;
      #G' ≤ finrank 𝕜 E + 1
⊢ (⋂₀ F).Nonempty

Tactic:
classical -- for DecidableEq, required for the family version
  rw [show ⋂₀ F = ⋂ X : F, (X : Set E) by ext; simp]
  refine helly_theorem_compact' (F := fun x : F ↦ x.val)
    (fun X ↦ h_convex X (by simp)) (fun X ↦ h_compact X (by simp)) ?_
  intro G _
  let G' : Finset (Set E) := image Subtype.val G
  rw [show ⋂ i ∈ G, ↑i = ⋂₀ (G' : Set (Set E)) by simp [G']]
  apply h_inter G'
  · simp [G']
  · apply le_trans card_image_le
    assumption

Premises used: Convex.helly_theorem_compact', Finset.card_image_le, Subtype.val, le_trans
-- Module: Mathlib.Analysis.Convex.Radon
Goal:
𝕜 : Type u_2
E : Type u_3
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
inst_5 : FiniteDimensional 𝕜 E
inst_6 : TopologicalSpace E
inst_7 : T2Space E
F : Set (Set E)
h_card : HAdd.hAdd (α := ℕ∞) (↑(finrank 𝕜 E) : ℕ∞) 1 ≤ F.encard
h_convex : ∀ X ∈ F, Convex 𝕜 X
h_compact : ∀ X ∈ F, IsCompact X
h_inter : ∀ (G : Finset (Set E)), (↑G : Set (Set E)) ⊆ F → #G = finrank 𝕜 E + 1 → (⋂₀ (↑G : Set (Set E))).Nonempty
apply : ∀ (G : Finset (Set E)), (↑G : Set (Set E)) ⊆ F → #G ≤ finrank 𝕜 E + 1 → (⋂₀ (↑G : Set (Set E))).Nonempty
⊢ (⋂₀ F).Nonempty

Tactic:
apply helly_theorem_set_compact' h_convex h_compact

Premises used: Convex.helly_theorem_set_compact'
-- Module: Mathlib.Analysis.Convex.Radon
Goal:
𝕜 : Type u_2
E : Type u_3
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
inst_5 : FiniteDimensional 𝕜 E
inst_6 : TopologicalSpace E
inst_7 : T2Space E
F : Set (Set E)
h_card : HAdd.hAdd (α := ℕ∞) (↑(finrank 𝕜 E) : ℕ∞) 1 ≤ F.encard
h_convex : ∀ X ∈ F, Convex 𝕜 X
h_compact : ∀ X ∈ F, IsCompact X
h_inter : ∀ (G : Finset (Set E)), (↑G : Set (Set E)) ⊆ F → #G = finrank 𝕜 E + 1 → (⋂₀ (↑G : Set (Set E))).Nonempty
I : Finset (Set E)
hI_ss : (↑I : Set (Set E)) ⊆ F
hI_card : #I ≤ finrank 𝕜 E + 1
⊢ (↑I : Set (Set E)).encard ≤ HAdd.hAdd (α := ℕ∞) (↑(finrank 𝕜 E) : ℕ∞) 1

Tactic:
simpa only [encard_coe_eq_coe_finsetCard, ← ENat.coe_one, ← ENat.coe_add, Nat.cast_le]

Premises used: ENat.coe_one, Set.encard_coe_eq_coe_finsetCard, Nat.cast_le, ENat.coe_add