awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Convex.Radon (goal)
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
F : ι → Set E
s : Finset ι
h_convex : ∀ i ∈ s, Convex 𝕜 (F i)
h_inter : ∀ I ⊆ s, #I ≤ finrank 𝕜 E + 1 → Set.Nonempty.{u_3} (α := E) (⋂ i ∈ I, F i)
inl : ∀ (h_card : #s < finrank 𝕜 E + 1), Set.Nonempty.{u_3} (α := E) (⋂ i ∈ s, F i)
inr inr₁ : ∀ (h_card : finrank 𝕜 E + 1 ≤ #s), Set.Nonempty.{u_3} (α := E) (⋂ i ∈ s, F i)
⊢ Set.Nonempty.{u_3} (α := E) (⋂ i ∈ s, F i)
have inr₂ : ∀ (h_card : finrank 𝕜 E + 1 ≤ #s) (n : ℕ) (hn : #s = n), Set.Nonempty.{u_3} (α := E) (⋂ i ∈ s, F i)
Tactic: classical
  obtain h_card | h_card := lt_or_ge #s (finrank 𝕜 E + 1)
  · exact helly_theorem_corner (le_of_lt h_card) h_inter
  generalize hn : #s = n
  rw [hn] at h_card
  induction n, h_card using Nat.le_induction generalizing ι with
  | base => exact helly_theorem_corner (le_of_eq hn) h_inter
  /- Construct a family of vectors indexed by `ι` such that the vector corresponding to `i : ι`
  is an arbitrary element of the intersection of all `F j` except `F i`. -/
  | succ k h_card hk =>
  let a (i : s) : E := Set.Nonempty.some (s := ⋂ j ∈ s.erase i, F j) <| by
    apply hk (s := s.erase i)
    · exact fun i hi ↦ h_convex i (mem_of_mem_erase hi)
    · intro J hJ_ss hJ_card
      exact h_inter J (subset_trans hJ_ss (erase_subset i.val s)) hJ_card
    · simp only [coe_mem, card_erase_of_mem]; lia
  /- This family of vectors is not affine independent because the number of them exceeds the
  dimension of the space. -/
  have h_ind : ¬AffineIndependent 𝕜 a := by
    rw [← finrank_vectorSpan_le_iff_not_affineIndependent 𝕜 a (n := (k - 1))]
    · exact (Submodule.finrank_le (vectorSpan 𝕜 (range a))).trans (Nat.le_pred_of_lt h_card)
    · simp only [card_coe]; lia
  /- Use `radon_partition` to conclude there is a subset `I` of `s` and a point `p : E` which
  lies in the convex hull of either `a '' I` or `a '' Iᶜ`. We claim that `p ∈ ⋂ i ∈ s, F i`. -/
  obtain ⟨I, p, hp_I, hp_Ic⟩ := radon_partition h_ind
  use p
  apply mem_biInter
  intro i hi
  lift i to s using hi
  /- It suffices to show that for any subcollection `J` of `s` containing `i`, the convex
  hull of `a '' (s \ J)` is contained in `F i`. -/
  suffices ∀ J : Set s, (i ∈ J) → (convexHull 𝕜) (a '' Jᶜ) ⊆ F i by
    by_cases h : i ∈ I
    · exact this I h hp_Ic
    · apply this Iᶜ h; rwa [compl_compl]
  /- Given any subcollection `J` of `ι` containing `i`, because `F i` is convex, we need only
  show that `a j ∈ F i` for each `j ∈ s \ J`. -/
  intro J hi
  rw [convexHull_subset_iff (h_convex i.1 i.2)]
  rintro v ⟨j, hj, hj_v⟩
  rw [← hj_v]
  /- Since `j ∈ Jᶜ` and `i ∈ J`, we conclude that `i ≠ j`, and hence by the definition of `a`:
  `a j ∈ ⋂ F '' (Set.univ \ {j}) ⊆ F i`. -/
  apply mem_of_subset_of_mem (s₁ := ⋂ k ∈ (s.erase j), F k)
  · apply iInter₂_subset
    simp [mem_erase, ne_of_mem_of_not_mem hi hj]
  · apply Nonempty.some_mem
-- Lean 4 proof step from Mathlib.Analysis.Convex.Radon (goal)
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
F : ι → Set E
s : Finset ι
h_convex : ∀ i ∈ s, Convex 𝕜 (F i)
h_inter : ∀ I ⊆ s, #I ≤ finrank 𝕜 E + 1 → Set.Nonempty.{u_3} (α := E) (⋂ i ∈ I, F i)
inl : ∀ (h_card : #s < finrank 𝕜 E + 1), Set.Nonempty.{u_3} (α := E) (⋂ i ∈ s, F i)
inr inr₁ : ∀ (h_card : finrank 𝕜 E + 1 ≤ #s), Set.Nonempty.{u_3} (α := E) (⋂ i ∈ s, F i)
inr₂ : ∀ (h_card : finrank 𝕜 E + 1 ≤ #s) (n : ℕ) (hn : #s = n), Set.Nonempty.{u_3} (α := E) (⋂ i ∈ s, F i)
⊢ Set.Nonempty.{u_3} (α := E) (⋂ i ∈ s, F i)
have inr₃ : ∀ (n : ℕ) (h_card : finrank 𝕜 E + 1 ≤ n) (hn : #s = n), Set.Nonempty.{u_3} (α := E) (⋂ i ∈ s, F i)
Tactic: classical
  obtain h_card | h_card := lt_or_ge #s (finrank 𝕜 E + 1)
  · exact helly_theorem_corner (le_of_lt h_card) h_inter
  generalize hn : #s = n
  rw [hn] at h_card
  induction n, h_card using Nat.le_induction generalizing ι with
  | base => exact helly_theorem_corner (le_of_eq hn) h_inter
  /- Construct a family of vectors indexed by `ι` such that the vector corresponding to `i : ι`
  is an arbitrary element of the intersection of all `F j` except `F i`. -/
  | succ k h_card hk =>
  let a (i : s) : E := Set.Nonempty.some (s := ⋂ j ∈ s.erase i, F j) <| by
    apply hk (s := s.erase i)
    · exact fun i hi ↦ h_convex i (mem_of_mem_erase hi)
    · intro J hJ_ss hJ_card
      exact h_inter J (subset_trans hJ_ss (erase_subset i.val s)) hJ_card
    · simp only [coe_mem, card_erase_of_mem]; lia
  /- This family of vectors is not affine independent because the number of them exceeds the
  dimension of the space. -/
  have h_ind : ¬AffineIndependent 𝕜 a := by
    rw [← finrank_vectorSpan_le_iff_not_affineIndependent 𝕜 a (n := (k - 1))]
    · exact (Submodule.finrank_le (vectorSpan 𝕜 (range a))).trans (Nat.le_pred_of_lt h_card)
    · simp only [card_coe]; lia
  /- Use `radon_partition` to conclude there is a subset `I` of `s` and a point `p : E` which
  lies in the convex hull of either `a '' I` or `a '' Iᶜ`. We claim that `p ∈ ⋂ i ∈ s, F i`. -/
  obtain ⟨I, p, hp_I, hp_Ic⟩ := radon_partition h_ind
  use p
  apply mem_biInter
  intro i hi
  lift i to s using hi
  /- It suffices to show that for any subcollection `J` of `s` containing `i`, the convex
  hull of `a '' (s \ J)` is contained in `F i`. -/
  suffices ∀ J : Set s, (i ∈ J) → (convexHull 𝕜) (a '' Jᶜ) ⊆ F i by
    by_cases h : i ∈ I
    · exact this I h hp_Ic
    · apply this Iᶜ h; rwa [compl_compl]
  /- Given any subcollection `J` of `ι` containing `i`, because `F i` is convex, we need only
  show that `a j ∈ F i` for each `j ∈ s \ J`. -/
  intro J hi
  rw [convexHull_subset_iff (h_convex i.1 i.2)]
  rintro v ⟨j, hj, hj_v⟩
  rw [← hj_v]
  /- Since `j ∈ Jᶜ` and `i ∈ J`, we conclude that `i ≠ j`, and hence by the definition of `a`:
  `a j ∈ ⋂ F '' (Set.univ \ {j}) ⊆ F i`. -/
  apply mem_of_subset_of_mem (s₁ := ⋂ k ∈ (s.erase j), F k)
  · apply iInter₂_subset
    simp [mem_erase, ne_of_mem_of_not_mem hi hj]
  · apply Nonempty.some_mem
-- Lean 4 proof step from Mathlib.Analysis.Convex.Radon (goal)
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
F : ι → Set E
s : Finset ι
h_card : finrank 𝕜 E + 1 ≤ #s
h_convex : ∀ i ∈ s, Convex 𝕜 (F i)
h_inter : ∀ I ⊆ s, #I = finrank 𝕜 E + 1 → Set.Nonempty.{u_3} (α := E) (⋂ i ∈ I, F i)
⊢ Set.Nonempty.{u_3} (α := E) (⋂ i ∈ s, F i)
have apply : ∀ I ⊆ s, #I ≤ finrank 𝕜 E + 1 → Set.Nonempty.{u_3} (α := E) (⋂ i ∈ I, F i)
Tactic: apply helly_theorem' h_convex
-- Lean 4 proof step from Mathlib.Analysis.Convex.Radon (goal)
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
F : ι → Set E
s : Finset ι
h_card : finrank 𝕜 E + 1 ≤ #s
h_convex : ∀ i ∈ s, Convex 𝕜 (F i)
h_inter : ∀ I ⊆ s, #I = finrank 𝕜 E + 1 → Set.Nonempty.{u_3} (α := E) (⋂ i ∈ I, F i)
I : Finset ι
hI_ss : I ⊆ s
hI_card : #I ≤ finrank 𝕜 E + 1
⊢ Set.Nonempty.{u_3} (α := E) (⋂ i ∈ I, F i)
have obtain : ∀ (J : Finset ι) (hI_ss_J : I ⊆ J) (hJ_ss : J ⊆ s) (hJ_card : #J = finrank 𝕜 E + 1),
  Set.Nonempty.{u_3} (α := E) (⋂ i ∈ I, F i)
Tactic: obtain ⟨J, hI_ss_J, hJ_ss, hJ_card⟩ := exists_subsuperset_card_eq hI_ss hI_card h_card
-- Lean 4 proof step from Mathlib.Analysis.Convex.Radon (goal)
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
F : ι → Set E
s : Finset ι
h_card : finrank 𝕜 E + 1 ≤ #s
h_convex : ∀ i ∈ s, Convex 𝕜 (F i)
h_inter : ∀ I ⊆ s, #I = finrank 𝕜 E + 1 → Set.Nonempty.{u_3} (α := E) (⋂ i ∈ I, F i)
I : Finset ι
hI_ss : I ⊆ s
hI_card : #I ≤ finrank 𝕜 E + 1
J : Finset ι
hI_ss_J : I ⊆ J
hJ_ss : J ⊆ s
hJ_card : #J = finrank 𝕜 E + 1
⊢ Set.Nonempty.{u_3} (α := E) (⋂ i ∈ I, F i)
have apply : Set.Nonempty.{u_3} (α := E) (⋂ x ∈ (↑J : Set ι), F x)
Tactic: apply Set.Nonempty.mono <| biInter_mono hI_ss_J (fun _ _ ↦ Set.Subset.rfl)
-- Lean 4 proof step from Mathlib.Analysis.Convex.Radon (goal)
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
F : Finset (Set E)
h_convex : ∀ X ∈ F, Convex 𝕜 X
h_inter : ∀ G ⊆ F, #G ≤ finrank 𝕜 E + 1 → (⋂₀ (↑G : Set (Set E))).Nonempty
⊢ ⋂₀ (↑F : Set (Set E)) = ⋂ X ∈ F, X
have h : ∀ (x : E), x ∈ ⋂₀ (↑F : Set (Set E)) ↔ Membership.mem (γ := Set E) (⋂ X ∈ F, X) x
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.Convex.Radon (goal)
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
F : Finset (Set E)
h_convex : ∀ X ∈ F, Convex 𝕜 X
h_inter : ∀ G ⊆ F, #G ≤ finrank 𝕜 E + 1 → (⋂₀ (↑G : Set (Set E))).Nonempty
⊢ (⋂₀ (↑F : Set (Set E))).Nonempty
have rw : Set.Nonempty.{u_3} (α := E) (⋂ X ∈ F, X)
Tactic: rw [show ⋂₀ F = ⋂ X ∈ F, (X : Set E) by ext; simp]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Radon (goal)
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
F : Finset (Set E)
h_convex : ∀ X ∈ F, Convex 𝕜 X
h_inter : ∀ G ⊆ F, #G ≤ finrank 𝕜 E + 1 → (⋂₀ (↑G : Set (Set E))).Nonempty
⊢ Set.Nonempty.{u_3} (α := E) (⋂ X ∈ F, X)
have apply : ∀ I ⊆ F, #I ≤ finrank 𝕜 E + 1 → Set.Nonempty.{u_3} (α := E) (⋂ i ∈ I, i)
Tactic: apply helly_theorem' h_convex
-- Lean 4 proof step from Mathlib.Analysis.Convex.Radon (goal)
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
F : Finset (Set E)
h_convex : ∀ X ∈ F, Convex 𝕜 X
h_inter : ∀ G ⊆ F, #G ≤ finrank 𝕜 E + 1 → (⋂₀ (↑G : Set (Set E))).Nonempty
G : Finset (Set E)
hG_ss : G ⊆ F
hG_card : #G ≤ finrank 𝕜 E + 1
⊢ ⋂ X ∈ G, X = ⋂₀ (↑G : Set (Set E))
have h : ∀ (x : E), Membership.mem (γ := Set E) (⋂ X ∈ G, X) x ↔ x ∈ ⋂₀ (↑G : Set (Set E))
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.Convex.Radon (goal)
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
F : Finset (Set E)
h_convex : ∀ X ∈ F, Convex 𝕜 X
h_inter : ∀ G ⊆ F, #G ≤ finrank 𝕜 E + 1 → (⋂₀ (↑G : Set (Set E))).Nonempty
G : Finset (Set E)
hG_ss : G ⊆ F
hG_card : #G ≤ finrank 𝕜 E + 1
⊢ Set.Nonempty.{u_3} (α := E) (⋂ i ∈ G, i)
have rw : (⋂₀ (↑G : Set (Set E))).Nonempty
Tactic: rw [show ⋂ X ∈ G, X = ⋂₀ G by ext; simp]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Radon (goal)
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
F : Finset (Set E)
h_convex : ∀ X ∈ F, Convex 𝕜 X
h_inter : ∀ G ⊆ F, #G ≤ finrank 𝕜 E + 1 → (⋂₀ (↑G : Set (Set E))).Nonempty
⊢ (⋂₀ (↑F : Set (Set E))).Nonempty
have classical : Set.Nonempty.{u_3} (α := E) (⋂ X ∈ F, X)
Tactic: classical -- for DecidableEq, required for the family version
  rw [show ⋂₀ F = ⋂ X ∈ F, (X : Set E) by ext; simp]
  apply helly_theorem' h_convex
  intro G hG_ss hG_card
  rw [show ⋂ X ∈ G, X = ⋂₀ G by ext; simp]
  exact h_inter G hG_ss hG_card
-- Lean 4 proof step from Mathlib.Analysis.Convex.Radon (goal)
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
F : Finset (Set E)
h_convex : ∀ X ∈ F, Convex 𝕜 X
h_inter : ∀ G ⊆ F, #G ≤ finrank 𝕜 E + 1 → (⋂₀ (↑G : Set (Set E))).Nonempty
classical classical₁ classical₂ : Set.Nonempty.{u_3} (α := E) (⋂ X ∈ F, X)
⊢ (⋂₀ (↑F : Set (Set E))).Nonempty
have classical₃ : ∀ I ⊆ F, #I ≤ finrank 𝕜 E + 1 → Set.Nonempty.{u_3} (α := E) (⋂ i ∈ I, i)
Tactic: classical -- for DecidableEq, required for the family version
  rw [show ⋂₀ F = ⋂ X ∈ F, (X : Set E) by ext; simp]
  apply helly_theorem' h_convex
  intro G hG_ss hG_card
  rw [show ⋂ X ∈ G, X = ⋂₀ G by ext; simp]
  exact h_inter G hG_ss hG_card
-- Lean 4 proof step from Mathlib.Analysis.Convex.Radon (goal)
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
F : Finset (Set E)
h_card : finrank 𝕜 E + 1 ≤ #F
h_convex : ∀ X ∈ F, Convex 𝕜 X
h_inter : ∀ G ⊆ F, #G = finrank 𝕜 E + 1 → (⋂₀ (↑G : Set (Set E))).Nonempty
⊢ (⋂₀ (↑F : Set (Set E))).Nonempty
have apply : ∀ G ⊆ F, #G ≤ finrank 𝕜 E + 1 → (⋂₀ (↑G : Set (Set E))).Nonempty
Tactic: apply helly_theorem_set' h_convex
-- Lean 4 proof step from Mathlib.Analysis.Convex.Radon (goal)
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
F : Finset (Set E)
h_card : finrank 𝕜 E + 1 ≤ #F
h_convex : ∀ X ∈ F, Convex 𝕜 X
h_inter : ∀ G ⊆ F, #G = finrank 𝕜 E + 1 → (⋂₀ (↑G : Set (Set E))).Nonempty
I : Finset (Set E)
hI_ss : I ⊆ F
hI_card : #I ≤ finrank 𝕜 E + 1
⊢ (⋂₀ (↑I : Set (Set E))).Nonempty
have obtain : ∀ (J : Finset (Set E)), I ⊆ J → ∀ (hJ_ss : J ⊆ F) (hJ_card : #J = finrank 𝕜 E + 1), (⋂₀ (↑I : Set (Set E))).Nonempty
Tactic: obtain ⟨J, _, hJ_ss, hJ_card⟩ := exists_subsuperset_card_eq hI_ss hI_card h_card
-- Lean 4 proof step from Mathlib.Analysis.Convex.Radon (hypothesis)
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
F : Finset (Set E)
h_card : finrank 𝕜 E + 1 ≤ #F
h_convex : ∀ X ∈ F, Convex 𝕜 X
h_inter : ∀ G ⊆ F, #G = finrank 𝕜 E + 1 → (⋂₀ (↑G : Set (Set E))).Nonempty
I : Finset (Set E)
hI_ss : I ⊆ F
hI_card : #I ≤ finrank 𝕜 E + 1
J : Finset (Set E)
left : I ⊆ J
hJ_ss : J ⊆ F
hJ_card : #J = finrank 𝕜 E + 1
⊢ (⋂₀ (↑I : Set (Set E))).Nonempty
have this : ⋂₀ (↑J : Set (Set E)) ⊆ ⋂₀ (↑I : Set (Set E))
Tactic: have : ⋂₀ (J : Set (Set E)) ⊆ ⋂₀ I := sInter_mono (by simpa [hI_ss])
-- Lean 4 proof step from Mathlib.Analysis.Convex.Radon (goal)
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
F : Finset (Set E)
h_card : finrank 𝕜 E + 1 ≤ #F
h_convex : ∀ X ∈ F, Convex 𝕜 X
h_inter : ∀ G ⊆ F, #G = finrank 𝕜 E + 1 → (⋂₀ (↑G : Set (Set E))).Nonempty
I : Finset (Set E)
hI_ss : I ⊆ F
hI_card : #I ≤ finrank 𝕜 E + 1
J : Finset (Set E)
left : I ⊆ J
hJ_ss : J ⊆ F
hJ_card : #J = finrank 𝕜 E + 1
this : ⋂₀ (↑J : Set (Set E)) ⊆ ⋂₀ (↑I : Set (Set E))
⊢ (⋂₀ (↑I : Set (Set E))).Nonempty
have apply : (⋂₀ (↑J : Set (Set E))).Nonempty
Tactic: apply Set.Nonempty.mono this
-- Lean 4 proof step from Mathlib.Analysis.Convex.Radon (goal)
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)
⊢ Set.Nonempty.{u_3} (α := E) (⋂ (i : ι), F i)
have inl : IsEmpty ι → Set.Nonempty.{u_3} (α := E) (⋂ (i : ι), F i)
Tactic: rcases isEmpty_or_nonempty ι with _ | h_nonempty
-- Lean 4 proof step from Mathlib.Analysis.Convex.Radon (goal)
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)
inl : IsEmpty ι → Set.Nonempty.{u_3} (α := E) (⋂ (i : ι), F i)
⊢ Set.Nonempty.{u_3} (α := E) (⋂ (i : ι), F i)
have inr : ∀ (h_nonempty : Nonempty ι), Set.Nonempty.{u_3} (α := E) (⋂ (i : ι), F i)
Tactic: rcases isEmpty_or_nonempty ι with _ | h_nonempty
-- Lean 4 proof step from Mathlib.Analysis.Convex.Radon (goal)
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)
h_nonempty : Nonempty ι
I : Finset ι
⊢ Set.Nonempty.{u_3} (α := E) (⋂ i ∈ I, F i)
have apply : ∀ I_1 ⊆ I, #I_1 ≤ finrank 𝕜 E + 1 → Set.Nonempty.{u_3} (α := E) (⋂ i ∈ I_1, F i)
Tactic: apply helly_theorem' (s := I) (𝕜 := 𝕜) (by simp [h_convex])
-- Lean 4 proof step from Mathlib.Analysis.Convex.Radon (hypothesis)
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)
h_nonempty : Nonempty ι
⊢ Set.Nonempty.{u_3} (α := E) (⋂ (i : ι), F i)
have h_fin : ∀ (I : Finset ι), Set.Nonempty.{u_3} (α := E) (⋂ i ∈ I, F i)
Tactic: have h_fin (I : Finset ι) : (⋂ i ∈ I, F i).Nonempty := by
    apply helly_theorem' (s := I) (𝕜 := 𝕜) (by simp [h_convex])
    exact fun J _ hJ_card ↦ h_inter J hJ_card
-- Lean 4 proof step from Mathlib.Analysis.Convex.Radon (goal)
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)
h_nonempty : Nonempty ι
h_fin : ∀ (I : Finset ι), Set.Nonempty.{u_3} (α := E) (⋂ i ∈ I, F i)
⊢ Set.Nonempty.{u_3} (α := E) (⋂ (i : ι), F i)
have inr : ∀ (i0 : ι), Set.Nonempty.{u_3} (α := E) (⋂ (i : ι), F i)
Tactic: have i0 : ι := Nonempty.some h_nonempty
-- Lean 4 proof step from Mathlib.Analysis.Convex.Radon (goal)
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)
h_nonempty : Nonempty ι
h_fin : ∀ (I : Finset ι), Set.Nonempty.{u_3} (α := E) (⋂ i ∈ I, F i)
i0 : ι
⊢ Set.Nonempty.{u_3} (α := E) (⋂ (i : ι), F i)
have inr : (F i0 ∩ ⋂ (i : ι), F i).Nonempty
Tactic: rw [show ⋂ i, F i = (F i0) ∩ ⋂ i, F i by simp [iInter_subset]]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Radon (goal)
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)
h_nonempty : Nonempty ι
h_fin : ∀ (I : Finset ι), Set.Nonempty.{u_3} (α := E) (⋂ i ∈ I, F i)
i0 : ι
⊢ (F i0 ∩ ⋂ (i : ι), F i).Nonempty
have inr : IsCompact (F i0)
Tactic: apply IsCompact.inter_iInter_nonempty
-- Lean 4 proof step from Mathlib.Analysis.Convex.Radon (goal)
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)
h_nonempty : Nonempty ι
h_fin : ∀ (I : Finset ι), Set.Nonempty.{u_3} (α := E) (⋂ i ∈ I, F i)
i0 : ι
inr : IsCompact (F i0)
⊢ (F i0 ∩ ⋂ (i : ι), F i).Nonempty
have inr₁ : ∀ (i : ι), IsClosed (F i)
Tactic: apply IsCompact.inter_iInter_nonempty
-- Lean 4 proof step from Mathlib.Analysis.Convex.Radon (goal)
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)
h_nonempty : Nonempty ι
h_fin : ∀ (I : Finset ι), Set.Nonempty.{u_3} (α := E) (⋂ i ∈ I, F i)
i0 : ι
inr : IsCompact (F i0)
inr₁ : ∀ (i : ι), IsClosed (F i)
⊢ (F i0 ∩ ⋂ (i : ι), F i).Nonempty
have inr₂ : ∀ (u : Finset ι), (F i0 ∩ ⋂ i ∈ u, F i).Nonempty
Tactic: apply IsCompact.inter_iInter_nonempty
-- Lean 4 proof step from Mathlib.Analysis.Convex.Radon (goal)
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)
⊢ Set.Nonempty.{u_3} (α := E) (⋂ (i : ι), F i)
have inl : IsEmpty ι → Set.Nonempty.{u_3} (α := E) (⋂ (i : ι), F i)
Tactic: classical
  /- If `ι` is empty the statement is trivial. -/
  rcases isEmpty_or_nonempty ι with _ | h_nonempty
  · simp only [iInter_of_empty, Set.univ_nonempty]
  /- By the finite version of theorem, every finite subfamily has an intersection. -/
  have h_fin (I : Finset ι) : (⋂ i ∈ I, F i).Nonempty := by
    apply helly_theorem' (s := I) (𝕜 := 𝕜) (by simp [h_convex])
    exact fun J _ hJ_card ↦ h_inter J hJ_card
  /- The following is a clumsy proof that family of compact sets with the finite intersection
  property has a nonempty intersection. -/
  have i0 : ι := Nonempty.some h_nonempty
  rw [show ⋂ i, F i = (F i0) ∩ ⋂ i, F i by simp [iInter_subset]]
  apply IsCompact.inter_iInter_nonempty
  · exact h_compact i0
  · intro i
    exact (h_compact i).isClosed
  · intro I
    simpa using h_fin ({i0} ∪ I)