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_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) (⋂ i ∈ I, F i)
have apply : Set.Nonempty.{u_3} (α := E) (⋂ x ∈ (↑J : Set ι), F x)
Tactic: apply Set.Nonempty.mono <| biInter_mono hJ_ss (by intro _ _; 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
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
⊢ ⋂₀ F = ⋂ (X : (↑F : Type u_3)), (↑X : Set E)
have h : ∀ (x : E), x ∈ ⋂₀ F ↔ Membership.mem (γ := Set E) (⋂ (X : (↑F : Type u_3)), (↑X : Set E)) 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
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
⊢ (⋂₀ F).Nonempty
have rw : Set.Nonempty.{u_3} (α := E) (⋂ (X : (↑F : Type u_3)), (↑X : Set E))
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
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
⊢ Set.Nonempty.{u_3} (α := E) (⋂ (X : (↑F : Type u_3)), (↑X : Set E))
have 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)
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)) ?_
-- 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
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
⊢ Set.Nonempty.{u_3} (α := E) (⋂ i ∈ G, (fun (x : (↑F : Type u_3)) ↦ (↑x : Set E)) i)
have rw : (⋂₀ (↑G' : Set (Set E))).Nonempty
Tactic: rw [show ⋂ i ∈ G, ↑i = ⋂₀ (G' : Set (Set E)) by simp [G']]
-- 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
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))).Nonempty
have a : (↑G' : Set (Set E)) ⊆ F
Tactic: apply h_inter G'
-- 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
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
⊢ (⋂₀ (↑G' : Set (Set E))).Nonempty
have a₁ : #G' ≤ finrank 𝕜 E + 1
Tactic: apply h_inter G'
-- 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
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
⊢ (⋂₀ F).Nonempty
have classical : Set.Nonempty.{u_3} (α := E) (⋂ (X : (↑F : Type u_3)), (↑X : Set E))
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
-- 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
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))
⊢ (⋂₀ F).Nonempty
have classical₃ : ∀ (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)
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
-- 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
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)
⊢ (⋂₀ F).Nonempty
have 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
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
-- 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
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
⊢ (⋂₀ F).Nonempty
have 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
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
-- 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
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
⊢ (⋂₀ F).Nonempty
have 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
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
-- 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
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
⊢ (⋂₀ F).Nonempty
have apply : ∀ (G : Finset (Set E)), (↑G : Set (Set E)) ⊆ F → #G ≤ finrank 𝕜 E + 1 → (⋂₀ (↑G : Set (Set E))).Nonempty
Tactic: apply helly_theorem_set_compact' h_convex h_compact
-- 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
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))).Nonempty
have obtain : ∀ (J : Set (Set E)),
  (↑I : Set (Set E)) ⊆ J →
    ∀ (hJ_ss : J ⊆ F) (hJ_card : J.encard = HAdd.hAdd (α := ℕ∞) (↑(finrank 𝕜 E) : ℕ∞) 1),
      (⋂₀ (↑I : Set (Set E))).Nonempty
Tactic: obtain ⟨J, _, hJ_ss, hJ_card⟩ := exists_superset_subset_encard_eq hI_ss (hkt := h_card)
    (by simpa only [encard_coe_eq_coe_finsetCard, ← ENat.coe_one, ← ENat.coe_add, Nat.cast_le])
-- 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
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
J : Set (Set E)
left : (↑I : Set (Set E)) ⊆ J
hJ_ss : J ⊆ F
hJ_card : J.encard = HAdd.hAdd (α := ℕ∞) (↑(finrank 𝕜 E) : ℕ∞) 1
⊢ (⋂₀ (↑I : Set (Set E))).Nonempty
have apply : (⋂₀ J).Nonempty
Tactic: apply Set.Nonempty.mono <| 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
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
J : Set (Set E)
left : (↑I : Set (Set E)) ⊆ J
hJ_ss : J ⊆ F
hJ_card : J.encard = HAdd.hAdd (α := ℕ∞) (↑(finrank 𝕜 E) : ℕ∞) 1
⊢ (⋂₀ J).Nonempty
have have : ∀ (hJ_fin : Fintype (↑J : Type u_3)), (⋂₀ J).Nonempty
Tactic: have hJ_fin : Fintype J := Finite.fintype <| finite_of_encard_eq_coe hJ_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
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
J : Set (Set E)
left : (↑I : Set (Set E)) ⊆ J
hJ_ss : J ⊆ F
hJ_card : J.encard = HAdd.hAdd (α := ℕ∞) (↑(finrank 𝕜 E) : ℕ∞) 1
hJ_fin : Fintype (↑J : Type u_3)
J' : Finset (Set E) := J.toFinset
⊢ (⋂₀ J).Nonempty
have rw : (⋂₀ (↑J.toFinset : Set (Set E))).Nonempty
Tactic: rw [← coe_toFinset J]
-- 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
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
J : Set (Set E)
left : (↑I : Set (Set E)) ⊆ J
hJ_ss : J ⊆ F
hJ_card : J.encard = HAdd.hAdd (α := ℕ∞) (↑(finrank 𝕜 E) : ℕ∞) 1
hJ_fin : Fintype (↑J : Type u_3)
J' : Finset (Set E) := J.toFinset
⊢ (⋂₀ (↑J.toFinset : Set (Set E))).Nonempty
have a : (↑J' : Set (Set E)) ⊆ F
Tactic: apply h_inter J'
-- 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
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
J : Set (Set E)
left : (↑I : Set (Set E)) ⊆ J
hJ_ss : J ⊆ F
hJ_card : J.encard = HAdd.hAdd (α := ℕ∞) (↑(finrank 𝕜 E) : ℕ∞) 1
hJ_fin : Fintype (↑J : Type u_3)
J' : Finset (Set E) := J.toFinset
a : (↑J' : Set (Set E)) ⊆ F
⊢ (⋂₀ (↑J.toFinset : Set (Set E))).Nonempty
have a₁ : #J' = finrank 𝕜 E + 1
Tactic: apply h_inter J'
-- 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
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
J : Set (Set E)
left : (↑I : Set (Set E)) ⊆ J
hJ_ss : J ⊆ F
hJ_card : J.encard = HAdd.hAdd (α := ℕ∞) (↑(finrank 𝕜 E) : ℕ∞) 1
hJ_fin : Fintype (↑J : Type u_3)
J' : Finset (Set E) := J.toFinset
⊢ #J' = finrank 𝕜 E + 1
have a : ∀ (hJ_card : (↑(#J.toFinset) : ℕ∞) = HAdd.hAdd (α := ℕ∞) (↑(finrank 𝕜 E) : ℕ∞) 1),
  let J' := J.toFinset;
  #J' = finrank 𝕜 E + 1
Tactic: rwa [encard_eq_coe_toFinset_card J, ← ENat.coe_one, ← ENat.coe_add, Nat.cast_inj] at hJ_card
Cleared hypotheses: hJ_card, J'
-- 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
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
J : Set (Set E)
left : (↑I : Set (Set E)) ⊆ J
hJ_ss : J ⊆ F
hJ_card : J.encard = HAdd.hAdd (α := ℕ∞) (↑(finrank 𝕜 E) : ℕ∞) 1
hJ_fin : Fintype (↑J : Type u_3)
J' : Finset (Set E) := J.toFinset
a :
  ∀ (hJ_card : (↑(#J.toFinset) : ℕ∞) = HAdd.hAdd (α := ℕ∞) (↑(finrank 𝕜 E) : ℕ∞) 1),
    let J' := J.toFinset;
    #J' = finrank 𝕜 E + 1
⊢ #J' = finrank 𝕜 E + 1
have a₁ : ∀ (hJ_card : (↑(#J.toFinset) : ℕ∞) = HAdd.hAdd (α := ℕ∞) (↑(finrank 𝕜 E) : ℕ∞) (↑1 : ℕ∞)),
  let J' := J.toFinset;
  #J' = finrank 𝕜 E + 1
Tactic: rwa [encard_eq_coe_toFinset_card J, ← ENat.coe_one, ← ENat.coe_add, Nat.cast_inj] at hJ_card
Cleared hypotheses: hJ_card, J'
-- 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
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
J : Set (Set E)
left : (↑I : Set (Set E)) ⊆ J
hJ_ss : J ⊆ F
hJ_card : J.encard = HAdd.hAdd (α := ℕ∞) (↑(finrank 𝕜 E) : ℕ∞) 1
hJ_fin : Fintype (↑J : Type u_3)
J' : Finset (Set E) := J.toFinset
a :
  ∀ (hJ_card : (↑(#J.toFinset) : ℕ∞) = HAdd.hAdd (α := ℕ∞) (↑(finrank 𝕜 E) : ℕ∞) 1),
    let J' := J.toFinset;
    #J' = finrank 𝕜 E + 1
a₁ :
  ∀ (hJ_card : (↑(#J.toFinset) : ℕ∞) = HAdd.hAdd (α := ℕ∞) (↑(finrank 𝕜 E) : ℕ∞) (↑1 : ℕ∞)),
    let J' := J.toFinset;
    #J' = finrank 𝕜 E + 1
⊢ #J' = finrank 𝕜 E + 1
have a₂ : ∀ (hJ_card : Eq (α := ℕ∞) (↑(#J.toFinset) : ℕ∞) (↑(finrank 𝕜 E + 1) : ℕ∞)),
  let J' := J.toFinset;
  #J' = finrank 𝕜 E + 1
Tactic: rwa [encard_eq_coe_toFinset_card J, ← ENat.coe_one, ← ENat.coe_add, Nat.cast_inj] at hJ_card
Cleared hypotheses: hJ_card, J'
-- 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
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
J : Set (Set E)
left : (↑I : Set (Set E)) ⊆ J
hJ_ss : J ⊆ F
hJ_card : J.encard = HAdd.hAdd (α := ℕ∞) (↑(finrank 𝕜 E) : ℕ∞) 1
hJ_fin : Fintype (↑J : Type u_3)
J' : Finset (Set E) := J.toFinset
a :
  ∀ (hJ_card : (↑(#J.toFinset) : ℕ∞) = HAdd.hAdd (α := ℕ∞) (↑(finrank 𝕜 E) : ℕ∞) 1),
    let J' := J.toFinset;
    #J' = finrank 𝕜 E + 1
a₁ :
  ∀ (hJ_card : (↑(#J.toFinset) : ℕ∞) = HAdd.hAdd (α := ℕ∞) (↑(finrank 𝕜 E) : ℕ∞) (↑1 : ℕ∞)),
    let J' := J.toFinset;
    #J' = finrank 𝕜 E + 1
a₂ :
  ∀ (hJ_card : Eq (α := ℕ∞) (↑(#J.toFinset) : ℕ∞) (↑(finrank 𝕜 E + 1) : ℕ∞)),
    let J' := J.toFinset;
    #J' = finrank 𝕜 E + 1
⊢ #J' = finrank 𝕜 E + 1
have a₃ : ∀ (hJ_card : #J.toFinset = finrank 𝕜 E + 1),
  let J' := J.toFinset;
  #J' = finrank 𝕜 E + 1
Tactic: rwa [encard_eq_coe_toFinset_card J, ← ENat.coe_one, ← ENat.coe_add, Nat.cast_inj] at hJ_card
Cleared hypotheses: hJ_card, J'