awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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) ⋯
h_ind : ¬AffineIndependent 𝕜 a
inr :
  ∀ (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)
⊢ Set.Nonempty.{u_3} (α := E) (⋂ i ∈ s, F i)

Tactic:
obtain ⟨I, p, hp_I, hp_Ic⟩ := radon_partition h_ind

Premises used: Convex.radon_partition
-- 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) ⋯
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
h : Membership.mem (γ := Set E) (⋂ i ∈ s, F i) p
⊢ Set.Nonempty.{u_3} (α := E) (⋂ i ∈ s, F i)

Tactic:
use p
-- 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) ⋯
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
h : ∀ x ∈ (↑s : Set ι), p ∈ F x
⊢ Membership.mem (γ := Set E) (⋂ i ∈ s, F i) p

Tactic:
apply mem_biInter

Premises used: Set.mem_biInter
-- 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) ⋯
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 ι)
⊢ i ∈ s

Tactic:
hi
-- 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) ⋯
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 ι)
h : ∀ (i : ↥s), p ∈ F (↑i : ι)
⊢ p ∈ F i

Tactic:
lift i to s using hi
-- 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) ⋯
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 : ι)
neg : ∀ (h : i ∉ I), p ∈ F (↑i : ι)
⊢ p ∈ F (↑i : ι)

Tactic:
by_cases h : i ∈ 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
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 : ι)

Tactic:
this I h hp_Ic
-- 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) ⋯
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 : ι)

Tactic:
exact this I h hp_Ic
-- 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) ⋯
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
neg : Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) (a '' Iᶜᶜ) : Set E) p
⊢ p ∈ F (↑i : ι)

Tactic:
apply this Iᶜ h

Premises used: Compl.compl
-- 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) ⋯
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
neg neg₁ neg₂ neg₃ : Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) (a '' I) : Set E) p
⊢ Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) (a '' Iᶜᶜ) : Set E) p

Tactic:
rwa [compl_compl]

Premises used: compl_compl
-- 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) ⋯
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
h : ∀ (J : Set ↥s), i ∈ J → (convexHull 𝕜 : (a : Set E) → Set E) (a '' Jᶜ) ⊆ F (↑i : ι)
⊢ p ∈ 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]
-- 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) ⋯
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
h : a '' Jᶜ ⊆ F (↑i : ι)
⊢ (convexHull 𝕜 : (a : Set E) → Set E) (a '' Jᶜ) ⊆ F (↑i : ι)

Tactic:
rw [convexHull_subset_iff (h_convex i.1 i.2)]

Premises used: Convex.convexHull_subset_iff, Subtype.val, Subtype.property
-- 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) ⋯
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 : a j ∈ F (↑i : ι)
⊢ v ∈ F (↑i : ι)

Tactic:
rw [← hj_v]
-- 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) ⋯
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 : ι)
h₁ : Membership.mem (γ := Set E) (⋂ k ∈ s.erase (↑j : ι), F k) (a j)
⊢ a j ∈ F (↑i : ι)

Tactic:
apply mem_of_subset_of_mem (s₁ := ⋂ k ∈ (s.erase j), F k)

Premises used: Set.mem_of_subset_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
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 : (↑i : ι) ∈ s.erase (↑j : ι)
⊢ ⋂ k ∈ s.erase (↑j : ι), F k ⊆ F (↑i : ι)

Tactic:
apply iInter₂_subset

Premises used: Set.iInter₂_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
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
⊢ (↑i : ι) ∈ s.erase (↑j : ι)

Tactic:
simp [mem_erase, ne_of_mem_of_not_mem hi hj]

Premises used: ne_of_mem_of_not_mem, Finset.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
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
⊢ Membership.mem (γ := Set E) (⋂ k ∈ s.erase (↑j : ι), F k) (a j)

Tactic:
apply Nonempty.some_mem

Premises used: Set.Nonempty.some_mem
-- 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_card : finrank 𝕜 E + 1 ≤ #s
h_convex : ∀ i ∈ s, Convex 𝕜 (F i)
h_inter : ∀ I ⊆ s, #I = finrank 𝕜 E + 1 → Set.Nonempty.{u_3} (α := E) (⋂ i ∈ I, F i)
apply : ∀ I ⊆ s, #I ≤ finrank 𝕜 E + 1 → Set.Nonempty.{u_3} (α := E) (⋂ i ∈ I, F i)
⊢ Set.Nonempty.{u_3} (α := E) (⋂ i ∈ s, F i)

Tactic:
apply helly_theorem' h_convex

Premises used: Convex.helly_theorem'
-- 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_card : finrank 𝕜 E + 1 ≤ #s
h_convex : ∀ i ∈ s, Convex 𝕜 (F i)
h_inter : ∀ I ⊆ s, #I = finrank 𝕜 E + 1 → Set.Nonempty.{u_3} (α := E) (⋂ i ∈ I, F i)
I : Finset ι
hI_ss : I ⊆ s
hI_card : #I ≤ finrank 𝕜 E + 1
obtain :
  ∀ (J : Finset ι) (hI_ss_J : I ⊆ J) (hJ_ss : J ⊆ s) (hJ_card : #J = finrank 𝕜 E + 1),
    Set.Nonempty.{u_3} (α := E) (⋂ i ∈ I, F i)
⊢ Set.Nonempty.{u_3} (α := E) (⋂ i ∈ I, F i)

Tactic:
obtain ⟨J, hI_ss_J, hJ_ss, hJ_card⟩ := exists_subsuperset_card_eq hI_ss hI_card h_card

Premises used: Finset.exists_subsuperset_card_eq
-- 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_card : finrank 𝕜 E + 1 ≤ #s
h_convex : ∀ i ∈ s, Convex 𝕜 (F i)
h_inter : ∀ I ⊆ s, #I = finrank 𝕜 E + 1 → Set.Nonempty.{u_3} (α := E) (⋂ i ∈ I, F i)
I : Finset ι
hI_ss : I ⊆ s
hI_card : #I ≤ finrank 𝕜 E + 1
J : Finset ι
hI_ss_J : I ⊆ J
hJ_ss : J ⊆ s
hJ_card : #J = finrank 𝕜 E + 1
apply : Set.Nonempty.{u_3} (α := E) (⋂ x ∈ (↑J : Set ι), F x)
⊢ Set.Nonempty.{u_3} (α := E) (⋂ i ∈ I, F i)

Tactic:
apply Set.Nonempty.mono <| biInter_mono hI_ss_J (fun _ _ ↦ Set.Subset.rfl)

Premises used: Set.biInter_mono, Set.Nonempty.mono, Set.Subset.rfl
-- 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_card : finrank 𝕜 E + 1 ≤ #s
h_convex : ∀ i ∈ s, Convex 𝕜 (F i)
h_inter : ∀ I ⊆ s, #I = finrank 𝕜 E + 1 → Set.Nonempty.{u_3} (α := E) (⋂ i ∈ I, F i)
I : Finset ι
hI_ss : I ⊆ s
hI_card : #I ≤ finrank 𝕜 E + 1
J : Finset ι
hI_ss_J : I ⊆ J
hJ_ss : J ⊆ s
hJ_card : #J = finrank 𝕜 E + 1
⊢ Set.Nonempty.{u_3} (α := E) (⋂ x ∈ (↑J : Set ι), F x)

Tactic:
h_inter J hJ_ss hJ_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_card : finrank 𝕜 E + 1 ≤ #s
h_convex : ∀ i ∈ s, Convex 𝕜 (F i)
h_inter : ∀ I ⊆ s, #I = finrank 𝕜 E + 1 → Set.Nonempty.{u_3} (α := E) (⋂ i ∈ I, F i)
I : Finset ι
hI_ss : I ⊆ s
hI_card : #I ≤ finrank 𝕜 E + 1
J : Finset ι
hI_ss_J : I ⊆ J
hJ_ss : J ⊆ s
hJ_card : #J = finrank 𝕜 E + 1
⊢ Set.Nonempty.{u_3} (α := E) (⋂ x ∈ (↑J : Set ι), F x)

Tactic:
exact h_inter J hJ_ss hJ_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
F : Finset (Set E)
h_convex : ∀ X ∈ F, Convex 𝕜 X
h_inter : ∀ G ⊆ F, #G ≤ finrank 𝕜 E + 1 → (⋂₀ (↑G : Set (Set E))).Nonempty
h : ∀ (x : E), x ∈ ⋂₀ (↑F : Set (Set E)) ↔ Membership.mem (γ := Set E) (⋂ X ∈ F, X) x
⊢ ⋂₀ (↑F : Set (Set E)) = ⋂ X ∈ F, X

Tactic:
ext