awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Convex.Radon
Goal:
ι : Type u_1
𝕜 : Type u_2
E : Type u_3
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
f : ι → E
s : Finset ι
w : ι → 𝕜
h_wsum : s.sum w = 0
h_vsum : Eq.{u_3 + 1} (α := E) (∑ e ∈ s, w e • f e) 0
nonzero_w_index : ι
h1 : nonzero_w_index ∈ s
h2 : w nonzero_w_index ≠ 0
I : Finset ι := {i ∈ s | 0 ≤ w i}
J : Finset ι := {i ∈ s | w i < 0}
p : E := I.centerMass w f
hJI : HAdd.hAdd (α := 𝕜) (∑ j ∈ J, w j) (∑ i ∈ I, w i) = 0
hI : LT.lt.{u_2} (α := 𝕜) 0 (∑ i ∈ I, w i)
hp : J.centerMass w f = p
⊢ Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) (f '' (↑I : Set ι)) : Set E) p

Tactic:
centerMass_mem_convexHull _ (fun _i hi ↦ (mem_filter.mp hi).2) hI
      (fun _i hi ↦ mem_image_of_mem _ hi)

Premises used: Set.Mem, Finset.centerMass_mem_convexHull, And.right, Set.mem_image_of_mem, Iff.mp, Finset.mem_filter
-- Module: Mathlib.Analysis.Convex.Radon
Goal:
ι : Type u_1
𝕜 : Type u_2
E : Type u_3
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
f : ι → E
s : Finset ι
w : ι → 𝕜
h_wsum : s.sum w = 0
h_vsum : Eq.{u_3 + 1} (α := E) (∑ e ∈ s, w e • f e) 0
nonzero_w_index : ι
h1 : nonzero_w_index ∈ s
h2 : w nonzero_w_index ≠ 0
I : Finset ι := {i ∈ s | 0 ≤ w i}
J : Finset ι := {i ∈ s | w i < 0}
p : E := I.centerMass w f
hJI : HAdd.hAdd (α := 𝕜) (∑ j ∈ J, w j) (∑ i ∈ I, w i) = 0
hI : LT.lt.{u_2} (α := 𝕜) 0 (∑ i ∈ I, w i)
hp : J.centerMass w f = p
⊢ Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) (f '' (↑I : Set ι)) : Set E) p

Tactic:
exact centerMass_mem_convexHull _ (fun _i hi ↦ (mem_filter.mp hi).2) hI
      (fun _i hi ↦ mem_image_of_mem _ hi)

Premises used: Finset.centerMass_mem_convexHull, And.right, Set.mem_image_of_mem, Iff.mp, Finset.mem_filter
-- Module: Mathlib.Analysis.Convex.Radon
Goal:
ι : Type u_1
𝕜 : Type u_2
E : Type u_3
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
f : ι → E
s : Finset ι
w : ι → 𝕜
h_wsum : s.sum w = 0
h_vsum : Eq.{u_3 + 1} (α := E) (∑ e ∈ s, w e • f e) 0
nonzero_w_index : ι
h1 : nonzero_w_index ∈ s
h2 : w nonzero_w_index ≠ 0
I : Finset ι := {i ∈ s | 0 ≤ w i}
J : Finset ι := {i ∈ s | w i < 0}
p : E := I.centerMass w f
hJI : HAdd.hAdd (α := 𝕜) (∑ j ∈ J, w j) (∑ i ∈ I, w i) = 0
hI : LT.lt.{u_2} (α := 𝕜) 0 (∑ i ∈ I, w i)
hp : J.centerMass w f = p
refine_2 :
  Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) (f '' (↑I : Set ι)ᶜ) : Set E) (J.centerMass w f)
⊢ Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) (f '' (↑I : Set ι)ᶜ) : Set E) p

Tactic:
rw [← hp]
-- Module: Mathlib.Analysis.Convex.Radon
Goal:
ι : Type u_1
𝕜 : Type u_2
E : Type u_3
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
f : ι → E
s : Finset ι
w : ι → 𝕜
h_wsum : s.sum w = 0
h_vsum : Eq.{u_3 + 1} (α := E) (∑ e ∈ s, w e • f e) 0
nonzero_w_index : ι
h1 : nonzero_w_index ∈ s
h2 : w nonzero_w_index ≠ 0
I : Finset ι := {i ∈ s | 0 ≤ w i}
J : Finset ι := {i ∈ s | w i < 0}
p : E := I.centerMass w f
hJI : HAdd.hAdd (α := 𝕜) (∑ j ∈ J, w j) (∑ i ∈ I, w i) = 0
hI : LT.lt.{u_2} (α := 𝕜) 0 (∑ i ∈ I, w i)
hp : J.centerMass w f = p
⊢ Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) (f '' (↑I : Set ι)ᶜ) : Set E) (J.centerMass w f)

Tactic:
centerMass_mem_convexHull_of_nonpos _ (fun _ hi ↦ (mem_filter.mp hi).2.le) ?_
    (fun _i hi ↦ mem_image_of_mem _ fun hi' ↦ ?_)

Premises used: LT.lt.le, And.right, Set.mem_image_of_mem, Iff.mp, Finset.mem_filter, Finset.centerMass_mem_convexHull_of_nonpos
-- Module: Mathlib.Analysis.Convex.Radon
Goal:
ι : Type u_1
𝕜 : Type u_2
E : Type u_3
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
f : ι → E
s : Finset ι
w : ι → 𝕜
h_wsum : s.sum w = 0
h_vsum : Eq.{u_3 + 1} (α := E) (∑ e ∈ s, w e • f e) 0
nonzero_w_index : ι
h1 : nonzero_w_index ∈ s
h2 : w nonzero_w_index ≠ 0
I : Finset ι := {i ∈ s | 0 ≤ w i}
J : Finset ι := {i ∈ s | w i < 0}
p : E := I.centerMass w f
hJI : HAdd.hAdd (α := 𝕜) (∑ j ∈ J, w j) (∑ i ∈ I, w i) = 0
hI : LT.lt.{u_2} (α := 𝕜) 0 (∑ i ∈ I, w i)
hp : J.centerMass w f = p
refine_2 : LT.lt.{u_2} (α := 𝕜) (∑ i ∈ J, w i) 0
refine_2₁ : ∀ (_i : ι) (hi : _i ∈ J) (hi' : _i ∈ (↑I : Set ι)), False
⊢ Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) (f '' (↑I : Set ι)ᶜ) : Set E) (J.centerMass w f)

Tactic:
refine centerMass_mem_convexHull_of_nonpos _ (fun _ hi ↦ (mem_filter.mp hi).2.le) ?_
    (fun _i hi ↦ mem_image_of_mem _ fun hi' ↦ ?_)
-- Module: Mathlib.Analysis.Convex.Radon
Goal:
ι : Type u_1
𝕜 : Type u_2
E : Type u_3
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
f : ι → E
s : Finset ι
w : ι → 𝕜
h_wsum : s.sum w = 0
h_vsum : Eq.{u_3 + 1} (α := E) (∑ e ∈ s, w e • f e) 0
nonzero_w_index : ι
h1 : nonzero_w_index ∈ s
h2 : w nonzero_w_index ≠ 0
I : Finset ι := {i ∈ s | 0 ≤ w i}
J : Finset ι := {i ∈ s | w i < 0}
p : E := I.centerMass w f
hJI : HAdd.hAdd (α := 𝕜) (∑ j ∈ J, w j) (∑ i ∈ I, w i) = 0
hI : LT.lt.{u_2} (α := 𝕜) 0 (∑ i ∈ I, w i)
hp : J.centerMass w f = p
linarith :
  LE.le.{u_2} (α := 𝕜) 0 (∑ i ∈ J, w i) →
    HSub.hSub (α := 𝕜) 0 (∑ i ∈ J, w i) + HSub.hSub (α := 𝕜) 0 (∑ i ∈ I, w i) +
        (HAdd.hAdd (α := 𝕜) (∑ j ∈ J, w j) (∑ i ∈ I, w i) - 0) =
      0
⊢ LT.lt.{u_2} (α := 𝕜) (∑ i ∈ J, w i) 0

Tactic:
linarith only [hI, hJI]
-- Module: Mathlib.Analysis.Convex.Radon
Goal:
ι : Type u_1
𝕜 : Type u_2
E : Type u_3
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
f : ι → E
s : Finset ι
w : ι → 𝕜
h_wsum : s.sum w = 0
h_vsum : Eq.{u_3 + 1} (α := E) (∑ e ∈ s, w e • f e) 0
nonzero_w_index : ι
h1 : nonzero_w_index ∈ s
h2 : w nonzero_w_index ≠ 0
I : Finset ι := {i ∈ s | 0 ≤ w i}
J : Finset ι := {i ∈ s | w i < 0}
p : E := I.centerMass w f
hJI : HAdd.hAdd (α := 𝕜) (∑ j ∈ J, w j) (∑ i ∈ I, w i) = 0
hI : LT.lt.{u_2} (α := 𝕜) 0 (∑ i ∈ I, w i)
hp : J.centerMass w f = p
_i : ι
hi : _i ∈ J
hi' : _i ∈ (↑I : Set ι)
⊢ False

Tactic:
(mem_filter.mp hi').2.not_gt (mem_filter.mp hi).2

Premises used: And.right, LE.le.not_gt, Iff.mp, Finset.mem_filter
-- Module: Mathlib.Analysis.Convex.Radon
Goal:
ι : Type u_1
𝕜 : Type u_2
E : Type u_3
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
f : ι → E
s : Finset ι
w : ι → 𝕜
h_wsum : s.sum w = 0
h_vsum : Eq.{u_3 + 1} (α := E) (∑ e ∈ s, w e • f e) 0
nonzero_w_index : ι
h1 : nonzero_w_index ∈ s
h2 : w nonzero_w_index ≠ 0
I : Finset ι := {i ∈ s | 0 ≤ w i}
J : Finset ι := {i ∈ s | w i < 0}
p : E := I.centerMass w f
hJI : HAdd.hAdd (α := 𝕜) (∑ j ∈ J, w j) (∑ i ∈ I, w i) = 0
hI : LT.lt.{u_2} (α := 𝕜) 0 (∑ i ∈ I, w i)
hp : J.centerMass w f = p
_i : ι
hi : _i ∈ J
hi' : _i ∈ (↑I : Set ι)
⊢ False

Tactic:
exact (mem_filter.mp hi').2.not_gt (mem_filter.mp hi).2

Premises used: And.right, LE.le.not_gt, Iff.mp, Finset.mem_filter
-- Module: Mathlib.Analysis.Convex.Radon
Goal:
ι : Type u_1
𝕜 : Type u_2
E : Type u_3
inst : Field 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
F : ι → Set E
s : Finset ι
h_card_small : #s ≤ finrank 𝕜 E + 1
h_inter : ∀ I ⊆ s, #I ≤ finrank 𝕜 E + 1 → Set.Nonempty.{u_3} (α := E) (⋂ i ∈ I, F i)
⊢ s ⊆ s

Tactic:
simp
-- Module: Mathlib.Analysis.Convex.Radon
Goal:
ι : Type u_1
𝕜 : Type u_2
E : Type u_3
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
inst_5 : FiniteDimensional 𝕜 E
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 : ∀ (h_card : finrank 𝕜 E + 1 ≤ #s), Set.Nonempty.{u_3} (α := E) (⋂ i ∈ s, F i)
⊢ Set.Nonempty.{u_3} (α := E) (⋂ i ∈ s, F i)

Tactic:
obtain h_card | h_card := lt_or_ge #s (finrank 𝕜 E + 1)

Premises used: HAdd.hAdd, Finset.card, lt_or_ge, OfNat.ofNat, Module.finrank
-- Module: Mathlib.Analysis.Convex.Radon
Goal:
ι : Type u_1
𝕜 : Type u_2
E : Type u_3
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
inst_5 : FiniteDimensional 𝕜 E
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)
h_card : #s < finrank 𝕜 E + 1
⊢ Set.Nonempty.{u_3} (α := E) (⋂ i ∈ s, F i)

Tactic:
helly_theorem_corner (le_of_lt h_card) h_inter

Premises used: le_of_lt, _private.0.Convex.helly_theorem_corner
-- Module: Mathlib.Analysis.Convex.Radon
Goal:
ι : Type u_1
𝕜 : Type u_2
E : Type u_3
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
inst_5 : FiniteDimensional 𝕜 E
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)
h_card : #s < finrank 𝕜 E + 1
⊢ Set.Nonempty.{u_3} (α := E) (⋂ i ∈ s, F i)

Tactic:
exact helly_theorem_corner (le_of_lt h_card) h_inter

Premises used: le_of_lt, _private.0.Convex.helly_theorem_corner
-- Module: Mathlib.Analysis.Convex.Radon
Goal:
ι : Type u_1
𝕜 : Type u_2
E : Type u_3
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
inst_5 : FiniteDimensional 𝕜 E
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)
h_card : finrank 𝕜 E + 1 ≤ #s
inr : ∀ (n : ℕ) (hn : #s = n), Set.Nonempty.{u_3} (α := E) (⋂ i ∈ s, F i)
⊢ Set.Nonempty.{u_3} (α := E) (⋂ i ∈ s, F i)

Tactic:
generalize hn : #s = n
-- Module: Mathlib.Analysis.Convex.Radon
Goal:
ι : Type u_1
𝕜 : Type u_2
E : Type u_3
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
inst_5 : FiniteDimensional 𝕜 E
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)
h_card : finrank 𝕜 E + 1 ≤ #s
n : ℕ
hn : #s = n
⊢ finrank 𝕜 E + 1 ≤ n

Tactic:
rw [hn] at h_card
-- Module: Mathlib.Analysis.Convex.Radon
Goal:
ι : Type u_1
𝕜 : Type u_2
E : Type u_3
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
inst_5 : FiniteDimensional 𝕜 E
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)
h_card : finrank 𝕜 E + 1 ≤ #s
n : ℕ
hn : #s = n
h_card₁ : finrank 𝕜 E + 1 ≤ n
⊢ #s = n

Tactic:
rw [hn] at h_card
-- Module: Mathlib.Analysis.Convex.Radon
Goal:
𝕜 : Type u_2
E : Type u_3
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
inst_5 : FiniteDimensional 𝕜 E
n : ℕ
ι : 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:
helly_theorem_corner (le_of_eq hn) h_inter

Premises used: _private.0.Convex.helly_theorem_corner, le_of_eq
-- Module: Mathlib.Analysis.Convex.Radon
Goal:
𝕜 : Type u_2
E : Type u_3
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
inst_5 : FiniteDimensional 𝕜 E
n : ℕ
ι : 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:
exact helly_theorem_corner (le_of_eq hn) h_inter

Premises used: _private.0.Convex.helly_theorem_corner, le_of_eq
-- Module: Mathlib.Analysis.Convex.Radon
Goal:
𝕜 : Type u_2
E : Type u_3
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
inst_5 : FiniteDimensional 𝕜 E
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
i : ↥s
h_convex₁ : ∀ i_1 ∈ s.erase (↑i : ι), Convex 𝕜 (F i_1)
h_inter₁ : ∀ I ⊆ s.erase (↑i : ι), #I ≤ finrank 𝕜 E + 1 → Set.Nonempty.{u_3} (α := E) (⋂ i ∈ I, F i)
hn₁ : #(s.erase (↑i : ι)) = k
⊢ Set.Nonempty.{u_3} (α := E) (⋂ j ∈ s.erase (↑i : ι), F j)

Tactic:
apply hk (s := s.erase i)
-- Module: Mathlib.Analysis.Convex.Radon
Goal:
𝕜 : Type u_2
E : Type u_3
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
inst_5 : FiniteDimensional 𝕜 E
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
i : ↥s
⊢ ∀ i_1 ∈ s.erase (↑i : ι), Convex 𝕜 (F i_1)

Tactic:
fun i hi ↦ h_convex i (mem_of_mem_erase hi)

Premises used: Finset.mem_of_mem_erase
-- Module: Mathlib.Analysis.Convex.Radon
Goal:
𝕜 : Type u_2
E : Type u_3
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
inst_5 : FiniteDimensional 𝕜 E
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
i : ↥s
⊢ ∀ i_1 ∈ s.erase (↑i : ι), Convex 𝕜 (F i_1)

Tactic:
exact fun i hi ↦ h_convex i (mem_of_mem_erase hi)

Premises used: Finset.mem_of_mem_erase
-- Module: Mathlib.Analysis.Convex.Radon
Goal:
𝕜 : Type u_2
E : Type u_3
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
inst_5 : FiniteDimensional 𝕜 E
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
i : ↥s
J : Finset ι
hJ_ss : J ⊆ s.erase (↑i : ι)
hJ_card : #J ≤ finrank 𝕜 E + 1
⊢ Set.Nonempty.{u_3} (α := E) (⋂ i ∈ J, F i)

Tactic:
h_inter J (subset_trans hJ_ss (erase_subset i.val s)) hJ_card

Premises used: subset_trans, Subtype.val, Finset.erase_subset
-- Module: Mathlib.Analysis.Convex.Radon
Goal:
𝕜 : Type u_2
E : Type u_3
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
inst_5 : FiniteDimensional 𝕜 E
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
i : ↥s
J : Finset ι
hJ_ss : J ⊆ s.erase (↑i : ι)
hJ_card : #J ≤ finrank 𝕜 E + 1
⊢ Set.Nonempty.{u_3} (α := E) (⋂ i ∈ J, F i)

Tactic:
exact h_inter J (subset_trans hJ_ss (erase_subset i.val s)) hJ_card

Premises used: subset_trans, Subtype.val, Finset.erase_subset
-- Module: Mathlib.Analysis.Convex.Radon
Goal:
𝕜 : Type u_2
E : Type u_3
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
inst_5 : FiniteDimensional 𝕜 E
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
i : ↥s
hn₁ : #s - 1 = k
⊢ #(s.erase (↑i : ι)) = k

Tactic:
simp only [coe_mem, card_erase_of_mem]

Premises used: Finset.coe_mem, Finset.card_erase_of_mem
-- Module: Mathlib.Analysis.Convex.Radon
Goal:
𝕜 : Type u_2
E : Type u_3
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
inst_5 : FiniteDimensional 𝕜 E
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
i : ↥s
⊢ #s - 1 = k

Tactic:
lia
-- Module: Mathlib.Analysis.Convex.Radon
Goal:
𝕜 : Type u_2
E : Type u_3
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
inst_5 : FiniteDimensional 𝕜 E
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) ⋯
rw : finrank.{u_2, u_3} 𝕜 ↥(vectorSpan 𝕜 (Set.range a)) ≤ k - 1
rw₁ : Fintype.card.{u_1} ↥s = k - 1 + 2
⊢ ¬AffineIndependent 𝕜 a

Tactic:
rw [← finrank_vectorSpan_le_iff_not_affineIndependent 𝕜 a (n := (k - 1))]

Premises used: finrank_vectorSpan_le_iff_not_affineIndependent
-- Module: Mathlib.Analysis.Convex.Radon
Goal:
𝕜 : Type u_2
E : Type u_3
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
inst_5 : FiniteDimensional 𝕜 E
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) ⋯
⊢ finrank.{u_2, u_3} 𝕜 ↥(vectorSpan 𝕜 (Set.range a)) ≤ k - 1

Tactic:
(Submodule.finrank_le (vectorSpan 𝕜 (range a))).trans (Nat.le_pred_of_lt h_card)

Premises used: vectorSpan, Nat.le_pred_of_lt, Submodule.finrank_le, Set.range, LE.le.trans
-- Module: Mathlib.Analysis.Convex.Radon
Goal:
𝕜 : Type u_2
E : Type u_3
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
inst_5 : FiniteDimensional 𝕜 E
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) ⋯
⊢ finrank.{u_2, u_3} 𝕜 ↥(vectorSpan 𝕜 (Set.range a)) ≤ k - 1

Tactic:
exact (Submodule.finrank_le (vectorSpan 𝕜 (range a))).trans (Nat.le_pred_of_lt h_card)

Premises used: vectorSpan, Nat.le_pred_of_lt, Submodule.finrank_le, Set.range, LE.le.trans
-- Module: Mathlib.Analysis.Convex.Radon
Goal:
𝕜 : Type u_2
E : Type u_3
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
inst_5 : FiniteDimensional 𝕜 E
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) ⋯
simp : #s = k - 1 + 2
⊢ Fintype.card.{u_1} ↥s = k - 1 + 2

Tactic:
simp only [card_coe]

Premises used: Fintype.card_coe
-- Module: Mathlib.Analysis.Convex.Radon
Goal:
𝕜 : Type u_2
E : Type u_3
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
inst_5 : FiniteDimensional 𝕜 E
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) ⋯
⊢ #s = k - 1 + 2

Tactic:
lia
-- Module: Mathlib.Analysis.Convex.Radon
Goal:
𝕜 : Type u_2
E : Type u_3
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
inst_5 : FiniteDimensional 𝕜 E
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) ⋯
⊢ ¬AffineIndependent 𝕜 a

Tactic:
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