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
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: 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)
-- 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)
inr inr₁ : ∀ (h_nonempty : Nonempty ι), Set.Nonempty.{u_3} (α := E) (⋂ (i : ι), F i)
⊢ Set.Nonempty.{u_3} (α := E) (⋂ (i : ι), F i)
have inr₂ : ∀ (h_nonempty : Nonempty ι) (h_fin : ∀ (I : Finset ι), Set.Nonempty.{u_3} (α := E) (⋂ i ∈ I, F i)),
  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)
-- 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)
inr inr₁ : ∀ (h_nonempty : Nonempty ι), Set.Nonempty.{u_3} (α := E) (⋂ (i : ι), F i)
inr₂ :
  ∀ (h_nonempty : Nonempty ι) (h_fin : ∀ (I : Finset ι), Set.Nonempty.{u_3} (α := E) (⋂ i ∈ I, F i)),
    Set.Nonempty.{u_3} (α := E) (⋂ (i : ι), F i)
⊢ Set.Nonempty.{u_3} (α := E) (⋂ (i : ι), F i)
have inr₃ : ∀ (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)
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)
-- 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)
inr inr₁ : ∀ (h_nonempty : Nonempty ι), Set.Nonempty.{u_3} (α := E) (⋂ (i : ι), F i)
inr₂ :
  ∀ (h_nonempty : Nonempty ι) (h_fin : ∀ (I : Finset ι), Set.Nonempty.{u_3} (α := E) (⋂ i ∈ I, F i)),
    Set.Nonempty.{u_3} (α := E) (⋂ (i : ι), F i)
inr₃ :
  ∀ (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)
⊢ Set.Nonempty.{u_3} (α := E) (⋂ (i : ι), F i)
have inr₄ : ∀ (h_nonempty : Nonempty ι) (h_fin : ∀ (I : Finset ι), Set.Nonempty.{u_3} (α := E) (⋂ i ∈ I, F i)) (i0 : ι),
  (F i0 ∩ ⋂ (i : ι), F i).Nonempty
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)
-- 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)
inr inr₁ : ∀ (h_nonempty : Nonempty ι), Set.Nonempty.{u_3} (α := E) (⋂ (i : ι), F i)
inr₂ :
  ∀ (h_nonempty : Nonempty ι) (h_fin : ∀ (I : Finset ι), Set.Nonempty.{u_3} (α := E) (⋂ i ∈ I, F i)),
    Set.Nonempty.{u_3} (α := E) (⋂ (i : ι), F i)
inr₃ :
  ∀ (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)
inr₄ :
  ∀ (h_nonempty : Nonempty ι) (h_fin : ∀ (I : Finset ι), Set.Nonempty.{u_3} (α := E) (⋂ i ∈ I, F i)) (i0 : ι),
    (F i0 ∩ ⋂ (i : ι), F i).Nonempty
⊢ Set.Nonempty.{u_3} (α := E) (⋂ (i : ι), F i)
have inr₅ : ∀ (h_nonempty : Nonempty ι) (h_fin : ∀ (I : Finset ι), Set.Nonempty.{u_3} (α := E) (⋂ i ∈ I, F i)) (i0 : ι),
  IsCompact (F i0)
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)
-- 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)
inr inr₁ : ∀ (h_nonempty : Nonempty ι), Set.Nonempty.{u_3} (α := E) (⋂ (i : ι), F i)
inr₂ :
  ∀ (h_nonempty : Nonempty ι) (h_fin : ∀ (I : Finset ι), Set.Nonempty.{u_3} (α := E) (⋂ i ∈ I, F i)),
    Set.Nonempty.{u_3} (α := E) (⋂ (i : ι), F i)
inr₃ :
  ∀ (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)
inr₄ :
  ∀ (h_nonempty : Nonempty ι) (h_fin : ∀ (I : Finset ι), Set.Nonempty.{u_3} (α := E) (⋂ i ∈ I, F i)) (i0 : ι),
    (F i0 ∩ ⋂ (i : ι), F i).Nonempty
inr₅ :
  ∀ (h_nonempty : Nonempty ι) (h_fin : ∀ (I : Finset ι), Set.Nonempty.{u_3} (α := E) (⋂ i ∈ I, F i)) (i0 : ι),
    IsCompact (F i0)
⊢ Set.Nonempty.{u_3} (α := E) (⋂ (i : ι), F i)
have inr₆ : ∀ (h_nonempty : Nonempty ι) (h_fin : ∀ (I : Finset ι), Set.Nonempty.{u_3} (α := E) (⋂ i ∈ I, F i)) (i0 i : ι),
  IsClosed (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)
-- 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)
inr inr₁ : ∀ (h_nonempty : Nonempty ι), Set.Nonempty.{u_3} (α := E) (⋂ (i : ι), F i)
inr₂ :
  ∀ (h_nonempty : Nonempty ι) (h_fin : ∀ (I : Finset ι), Set.Nonempty.{u_3} (α := E) (⋂ i ∈ I, F i)),
    Set.Nonempty.{u_3} (α := E) (⋂ (i : ι), F i)
inr₃ :
  ∀ (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)
inr₄ :
  ∀ (h_nonempty : Nonempty ι) (h_fin : ∀ (I : Finset ι), Set.Nonempty.{u_3} (α := E) (⋂ i ∈ I, F i)) (i0 : ι),
    (F i0 ∩ ⋂ (i : ι), F i).Nonempty
inr₅ :
  ∀ (h_nonempty : Nonempty ι) (h_fin : ∀ (I : Finset ι), Set.Nonempty.{u_3} (α := E) (⋂ i ∈ I, F i)) (i0 : ι),
    IsCompact (F i0)
inr₆ :
  ∀ (h_nonempty : Nonempty ι) (h_fin : ∀ (I : Finset ι), Set.Nonempty.{u_3} (α := E) (⋂ i ∈ I, F i)) (i0 i : ι),
    IsClosed (F i)
⊢ Set.Nonempty.{u_3} (α := E) (⋂ (i : ι), F i)
have inr₇ : ∀ (h_nonempty : Nonempty ι) (h_fin : ∀ (I : Finset ι), Set.Nonempty.{u_3} (α := E) (⋂ i ∈ I, F i)) (i0 : ι)
  (u : Finset ι), (F i0 ∩ ⋂ i ∈ u, F i).Nonempty
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)
-- 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_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)
⊢ Set.Nonempty.{u_3} (α := E) (⋂ (i : ι), F i)
have apply : ∀ (I : Finset ι), #I ≤ finrank 𝕜 E + 1 → Set.Nonempty.{u_3} (α := E) (⋂ i ∈ I, F i)
Tactic: apply helly_theorem_compact' h_convex h_compact
-- 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_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
have pos : ∀ (h : Infinite ι), ∃ (J : Finset ι), I ⊆ J ∧ #J = finrank 𝕜 E + 1
Tactic: by_cases h : Infinite ι
-- 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_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
⊢ ∃ (J : Finset ι), I ⊆ J ∧ #J = finrank 𝕜 E + 1
have neg : ∀ (h : ¬Infinite ι), ∃ (J : Finset ι), I ⊆ J ∧ #J = finrank 𝕜 E + 1
Tactic: by_cases h : Infinite ι
-- 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_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
have this : Finite ι
Tactic: have : Finite ι := Finite.of_not_infinite h
-- 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_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 ι
⊢ ∃ (J : Finset ι), I ⊆ J ∧ #J = finrank 𝕜 E + 1
have neg : ∀ (this : Fintype ι), ∃ (J : Finset ι), I ⊆ J ∧ #J = finrank 𝕜 E + 1
Tactic: have : Fintype ι := Fintype.ofFinite ι
-- 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_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 ι
⊢ ∃ (J : Finset ι), I ⊆ J ∧ #J = finrank 𝕜 E + 1
have neg : finrank 𝕜 E + 1 ≤ Fintype.card ι
Tactic: apply exists_superset_card_eq hI_card
-- 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_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 ι
⊢ finrank 𝕜 E + 1 ≤ Fintype.card ι
have h_card₁ : HAdd.hAdd (α := ℕ∞) (↑(finrank 𝕜 E) : ℕ∞) 1 ≤ (↑(Fintype.card ι) : ℕ∞)
Tactic: simp only [ENat.card_eq_coe_fintype_card] at h_card
Cleared hypotheses: 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
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 ι) : ℕ∞)
⊢ finrank 𝕜 E + 1 ≤ Fintype.card ι
have neg : ∀ (h_card : HAdd.hAdd (α := ℕ∞) (↑(finrank 𝕜 E) : ℕ∞) (↑1 : ℕ∞) ≤ (↑(Fintype.card ι) : ℕ∞)),
  finrank 𝕜 E + 1 ≤ Fintype.card ι
Tactic: rwa [← Nat.cast_one, ← Nat.cast_add, Nat.cast_le] at h_card
Cleared hypotheses: 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
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 ι
⊢ finrank 𝕜 E + 1 ≤ Fintype.card ι
have neg₁ : ∀ (h_card : LE.le (α := ℕ∞) (↑(finrank 𝕜 E + 1) : ℕ∞) (↑(Fintype.card ι) : ℕ∞)), finrank 𝕜 E + 1 ≤ Fintype.card ι
Tactic: rwa [← Nat.cast_one, ← Nat.cast_add, Nat.cast_le] at h_card
Cleared hypotheses: 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
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 ι
⊢ finrank 𝕜 E + 1 ≤ Fintype.card ι
have neg₂ : ∀ (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
Cleared hypotheses: h_card
-- 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_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
⊢ Set.Nonempty.{u_3} (α := E) (⋂ i ∈ I, F i)
have hJ : ∃ (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
-- 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_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
⊢ Set.Nonempty.{u_3} (α := E) (⋂ i ∈ I, F i)
have obtain : ∀ (J : Finset ι) (hJ_ss : I ⊆ J) (hJ_card : #J = finrank 𝕜 E + 1), Set.Nonempty.{u_3} (α := E) (⋂ i ∈ I, F i)
Tactic: obtain ⟨J, hJ_ss, hJ_card⟩ := hJ
Cleared hypotheses: hJ