awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
n k : ℕ
h_card : finrank 𝕜 E + 1 ≤ k
hk :
  ∀ {ι : Type u_1} {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)) (hn : #s = k),
    Set.Nonempty.{u_3} (α := E) (⋂ i ∈ s, F i)
ι : Type u_1
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)
hn : #s = k + 1
a : (i : ↥s) → E := fun (i : ↥s) ↦ Set.Nonempty.some (s := ⋂ j ∈ s.erase (↑i : ι), F j) ⋯
h_ind : ¬AffineIndependent 𝕜 a
I : Set ↥s
p : E
hp_I : Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) (a '' I) : Set E) p
hp_Ic : Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) (a '' Iᶜ) : Set E) p
⊢ Set.Nonempty.{u_3} (α := E) (⋂ i ∈ s, F i)
have h : Membership.mem (γ := Set E) (⋂ i ∈ s, F i) p
Tactic: use p
-- 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
n k : ℕ
h_card : finrank 𝕜 E + 1 ≤ k
hk :
  ∀ {ι : Type u_1} {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)) (hn : #s = k),
    Set.Nonempty.{u_3} (α := E) (⋂ i ∈ s, F i)
ι : Type u_1
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)
hn : #s = k + 1
a : (i : ↥s) → E := fun (i : ↥s) ↦ Set.Nonempty.some (s := ⋂ j ∈ s.erase (↑i : ι), F j) ⋯
h_ind : ¬AffineIndependent 𝕜 a
I : Set ↥s
p : E
hp_I : Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) (a '' I) : Set E) p
hp_Ic : Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) (a '' Iᶜ) : Set E) p
⊢ Membership.mem (γ := Set E) (⋂ i ∈ s, F i) p
have h : ∀ x ∈ (↑s : Set ι), p ∈ F x
Tactic: apply mem_biInter
-- 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
n k : ℕ
h_card : finrank 𝕜 E + 1 ≤ k
hk :
  ∀ {ι : Type u_1} {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)) (hn : #s = k),
    Set.Nonempty.{u_3} (α := E) (⋂ i ∈ s, F i)
ι : Type u_1
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)
hn : #s = k + 1
a : (i : ↥s) → E := fun (i : ↥s) ↦ Set.Nonempty.some (s := ⋂ j ∈ s.erase (↑i : ι), F j) ⋯
h_ind : ¬AffineIndependent 𝕜 a
I : Set ↥s
p : E
hp_I : Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) (a '' I) : Set E) p
hp_Ic : Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) (a '' Iᶜ) : Set E) p
i : ι
hi : i ∈ (↑s : Set ι)
⊢ p ∈ F i
have h : ∀ (i : ↥s), p ∈ F (↑i : ι)
Tactic: lift i to s using hi
Cleared hypotheses: i, hi
-- 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
n k : ℕ
h_card : finrank 𝕜 E + 1 ≤ k
hk :
  ∀ {ι : Type u_1} {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)) (hn : #s = k),
    Set.Nonempty.{u_3} (α := E) (⋂ i ∈ s, F i)
ι : Type u_1
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)
hn : #s = k + 1
a : (i : ↥s) → E := fun (i : ↥s) ↦ Set.Nonempty.some (s := ⋂ j ∈ s.erase (↑i : ι), F j) ⋯
h_ind : ¬AffineIndependent 𝕜 a
I : Set ↥s
p : E
hp_I : Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) (a '' I) : Set E) p
hp_Ic : Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) (a '' Iᶜ) : Set E) p
i : ↥s
this : ∀ (J : Set ↥s), i ∈ J → (convexHull 𝕜 : (a : Set E) → Set E) (a '' Jᶜ) ⊆ F (↑i : ι)
⊢ p ∈ F (↑i : ι)
have pos : ∀ (h : i ∈ I), p ∈ F (↑i : ι)
Tactic: by_cases h : i ∈ I
-- 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
n k : ℕ
h_card : finrank 𝕜 E + 1 ≤ k
hk :
  ∀ {ι : Type u_1} {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)) (hn : #s = k),
    Set.Nonempty.{u_3} (α := E) (⋂ i ∈ s, F i)
ι : Type u_1
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)
hn : #s = k + 1
a : (i : ↥s) → E := fun (i : ↥s) ↦ Set.Nonempty.some (s := ⋂ j ∈ s.erase (↑i : ι), F j) ⋯
h_ind : ¬AffineIndependent 𝕜 a
I : Set ↥s
p : E
hp_I : Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) (a '' I) : Set E) p
hp_Ic : Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) (a '' Iᶜ) : Set E) p
i : ↥s
this : ∀ (J : Set ↥s), i ∈ J → (convexHull 𝕜 : (a : Set E) → Set E) (a '' Jᶜ) ⊆ F (↑i : ι)
pos : ∀ (h : i ∈ I), p ∈ F (↑i : ι)
⊢ p ∈ F (↑i : ι)
have neg : ∀ (h : i ∉ I), p ∈ F (↑i : ι)
Tactic: by_cases h : i ∈ I
-- 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
n k : ℕ
h_card : finrank 𝕜 E + 1 ≤ k
hk :
  ∀ {ι : Type u_1} {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)) (hn : #s = k),
    Set.Nonempty.{u_3} (α := E) (⋂ i ∈ s, F i)
ι : Type u_1
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)
hn : #s = k + 1
a : (i : ↥s) → E := fun (i : ↥s) ↦ Set.Nonempty.some (s := ⋂ j ∈ s.erase (↑i : ι), F j) ⋯
h_ind : ¬AffineIndependent 𝕜 a
I : Set ↥s
p : E
hp_I : Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) (a '' I) : Set E) p
hp_Ic : Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) (a '' Iᶜ) : Set E) p
i : ↥s
this : ∀ (J : Set ↥s), i ∈ J → (convexHull 𝕜 : (a : Set E) → Set E) (a '' Jᶜ) ⊆ F (↑i : ι)
h : i ∉ I
⊢ p ∈ F (↑i : ι)
have neg : Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) (a '' Iᶜᶜ) : Set E) p
Tactic: apply this Iᶜ h
-- 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
n k : ℕ
h_card : finrank 𝕜 E + 1 ≤ k
hk :
  ∀ {ι : Type u_1} {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)) (hn : #s = k),
    Set.Nonempty.{u_3} (α := E) (⋂ i ∈ s, F i)
ι : Type u_1
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)
hn : #s = k + 1
a : (i : ↥s) → E := fun (i : ↥s) ↦ Set.Nonempty.some (s := ⋂ j ∈ s.erase (↑i : ι), F j) ⋯
h_ind : ¬AffineIndependent 𝕜 a
I : Set ↥s
p : E
hp_I : Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) (a '' I) : Set E) p
hp_Ic : Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) (a '' Iᶜ) : Set E) p
i : ↥s
⊢ p ∈ F (↑i : ι)
have h : ∀ (J : Set ↥s), i ∈ J → (convexHull 𝕜 : (a : Set E) → Set E) (a '' Jᶜ) ⊆ F (↑i : ι)
Tactic: 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]
-- 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
n k : ℕ
h_card : finrank 𝕜 E + 1 ≤ k
hk :
  ∀ {ι : Type u_1} {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)) (hn : #s = k),
    Set.Nonempty.{u_3} (α := E) (⋂ i ∈ s, F i)
ι : Type u_1
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)
hn : #s = k + 1
a : (i : ↥s) → E := fun (i : ↥s) ↦ Set.Nonempty.some (s := ⋂ j ∈ s.erase (↑i : ι), F j) ⋯
h_ind : ¬AffineIndependent 𝕜 a
I : Set ↥s
p : E
hp_I : Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) (a '' I) : Set E) p
hp_Ic : Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) (a '' Iᶜ) : Set E) p
i : ↥s
J : Set ↥s
hi : i ∈ J
⊢ (convexHull 𝕜 : (a : Set E) → Set E) (a '' Jᶜ) ⊆ F (↑i : ι)
have h : a '' Jᶜ ⊆ F (↑i : ι)
Tactic: rw [convexHull_subset_iff (h_convex i.1 i.2)]
-- 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
n k : ℕ
h_card : finrank 𝕜 E + 1 ≤ k
hk :
  ∀ {ι : Type u_1} {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)) (hn : #s = k),
    Set.Nonempty.{u_3} (α := E) (⋂ i ∈ s, F i)
ι : Type u_1
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)
hn : #s = k + 1
a : (i : ↥s) → E := fun (i : ↥s) ↦ Set.Nonempty.some (s := ⋂ j ∈ s.erase (↑i : ι), F j) ⋯
h_ind : ¬AffineIndependent 𝕜 a
I : Set ↥s
p : E
hp_I : Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) (a '' I) : Set E) p
hp_Ic : Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) (a '' Iᶜ) : Set E) p
i : ↥s
J : Set ↥s
hi : i ∈ J
v : E
j : ↥s
hj : j ∈ Jᶜ
hj_v : a j = v
⊢ v ∈ F (↑i : ι)
have h : a j ∈ F (↑i : ι)
Tactic: rw [← hj_v]
-- 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
n k : ℕ
h_card : finrank 𝕜 E + 1 ≤ k
hk :
  ∀ {ι : Type u_1} {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)) (hn : #s = k),
    Set.Nonempty.{u_3} (α := E) (⋂ i ∈ s, F i)
ι : Type u_1
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)
hn : #s = k + 1
a : (i : ↥s) → E := fun (i : ↥s) ↦ Set.Nonempty.some (s := ⋂ j ∈ s.erase (↑i : ι), F j) ⋯
h_ind : ¬AffineIndependent 𝕜 a
I : Set ↥s
p : E
hp_I : Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) (a '' I) : Set E) p
hp_Ic : Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) (a '' Iᶜ) : Set E) p
i : ↥s
J : Set ↥s
hi : i ∈ J
v : E
j : ↥s
hj : j ∈ Jᶜ
hj_v : a j = v
⊢ a j ∈ F (↑i : ι)
have h : ⋂ k ∈ s.erase (↑j : ι), F k ⊆ F (↑i : ι)
Tactic: apply mem_of_subset_of_mem (s₁ := ⋂ k ∈ (s.erase j), F k)
-- 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
n k : ℕ
h_card : finrank 𝕜 E + 1 ≤ k
hk :
  ∀ {ι : Type u_1} {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)) (hn : #s = k),
    Set.Nonempty.{u_3} (α := E) (⋂ i ∈ s, F i)
ι : Type u_1
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)
hn : #s = k + 1
a : (i : ↥s) → E := fun (i : ↥s) ↦ Set.Nonempty.some (s := ⋂ j ∈ s.erase (↑i : ι), F j) ⋯
h_ind : ¬AffineIndependent 𝕜 a
I : Set ↥s
p : E
hp_I : Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) (a '' I) : Set E) p
hp_Ic : Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) (a '' Iᶜ) : Set E) p
i : ↥s
J : Set ↥s
hi : i ∈ J
v : E
j : ↥s
hj : j ∈ Jᶜ
hj_v : a j = v
h : ⋂ k ∈ s.erase (↑j : ι), F k ⊆ F (↑i : ι)
⊢ a j ∈ F (↑i : ι)
have h₁ : Membership.mem (γ := Set E) (⋂ k ∈ s.erase (↑j : ι), F k) (a j)
Tactic: apply mem_of_subset_of_mem (s₁ := ⋂ k ∈ (s.erase j), F k)
-- 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
n k : ℕ
h_card : finrank 𝕜 E + 1 ≤ k
hk :
  ∀ {ι : Type u_1} {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)) (hn : #s = k),
    Set.Nonempty.{u_3} (α := E) (⋂ i ∈ s, F i)
ι : Type u_1
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)
hn : #s = k + 1
a : (i : ↥s) → E := fun (i : ↥s) ↦ Set.Nonempty.some (s := ⋂ j ∈ s.erase (↑i : ι), F j) ⋯
h_ind : ¬AffineIndependent 𝕜 a
I : Set ↥s
p : E
hp_I : Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) (a '' I) : Set E) p
hp_Ic : Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) (a '' Iᶜ) : Set E) p
i : ↥s
J : Set ↥s
hi : i ∈ J
v : E
j : ↥s
hj : j ∈ Jᶜ
hj_v : a j = v
⊢ ⋂ k ∈ s.erase (↑j : ι), F k ⊆ F (↑i : ι)
have h : (↑i : ι) ∈ s.erase (↑j : ι)
Tactic: apply 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
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)
n : ℕ
h_card : finrank 𝕜 E + 1 ≤ n
hn : #s = n
⊢ Set.Nonempty.{u_3} (α := E) (⋂ i ∈ s, F i)
have inr : ∀ {ι : Type u_1} {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)) (hn : #s = finrank 𝕜 E + 1),
  Set.Nonempty.{u_3} (α := E) (⋂ i ∈ s, F i)
Tactic: 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
Cleared hypotheses: ι, F, s, h_convex, h_inter, h_card, hn
-- 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)
⊢ Set.Nonempty.{u_3} (α := E) (⋂ i ∈ s, F i)
have inl : ∀ (h_card : #s < finrank 𝕜 E + 1), 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)
⊢ Set.Nonempty.{u_3} (α := E) (⋂ i ∈ s, F i)
have inr : ∀ (h_card : finrank 𝕜 E + 1 ≤ #s), 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