awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Convex.Quasiconvex (goal)
Goal:
𝕜 : Type u_1
β : Type u_3
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
s : Set 𝕜
f : 𝕜 → β
inst_3 : LinearOrder β
hf : QuasilinearOn 𝕜 s f
a : 𝕜
ha : a ∈ s
b : 𝕜
hb : b ∈ s
c : 𝕜
h_1 : c ∈ s
h : c ∈ segment 𝕜 a b
refine_1 : Membership.mem (γ := Set 𝕜) {x : 𝕜 | x ∈ s ∧ min (f a) (f b) ≤ f x} a
refine_2 : Membership.mem (γ := Set 𝕜) {x : 𝕜 | x ∈ s ∧ min (f a) (f b) ≤ f x} b
⊢ f c ∈ uIcc (f a) (f b)
have refine_3 : Membership.mem (γ := Set 𝕜) {x : 𝕜 | x ∈ s ∧ f x ≤ max (f a) (f b)} a
Tactic: refine ⟨((hf.2 _).segment_subset ?_ ?_ h).2, ((hf.1 _).segment_subset ?_ ?_ h).2⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.Quasiconvex (goal)
Goal:
𝕜 : Type u_1
β : Type u_3
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
s : Set 𝕜
f : 𝕜 → β
inst_3 : LinearOrder β
hf : QuasilinearOn 𝕜 s f
a : 𝕜
ha : a ∈ s
b : 𝕜
hb : b ∈ s
c : 𝕜
h_1 : c ∈ s
h : c ∈ segment 𝕜 a b
refine_1 : Membership.mem (γ := Set 𝕜) {x : 𝕜 | x ∈ s ∧ min (f a) (f b) ≤ f x} a
refine_2 : Membership.mem (γ := Set 𝕜) {x : 𝕜 | x ∈ s ∧ min (f a) (f b) ≤ f x} b
refine_3 : Membership.mem (γ := Set 𝕜) {x : 𝕜 | x ∈ s ∧ f x ≤ max (f a) (f b)} a
⊢ f c ∈ uIcc (f a) (f b)
have refine_4 : Membership.mem (γ := Set 𝕜) {x : 𝕜 | x ∈ s ∧ f x ≤ max (f a) (f b)} b
Tactic: refine ⟨((hf.2 _).segment_subset ?_ ?_ h).2, ((hf.1 _).segment_subset ?_ ?_ h).2⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.Radon (hypothesis)
Goal:
ι : Type u_1
𝕜 : Type u_2
E : Type u_3
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
f : ι → E
h : ¬AffineIndependent 𝕜 f
⊢ ∃ (I : Set ι),
    Set.Nonempty.{u_3} (α := E)
      ((convexHull 𝕜 : (a : Set E) → Set E) (f '' I) ∩ (convexHull 𝕜 : (a : Set E) → Set E) (f '' Iᶜ))
have h₁ : ¬∀ (s : Finset ι) (w : ι → 𝕜), s.sum w = 0 → Eq.{u_3 + 1} (α := E) (∑ e ∈ s, w e • f e) 0 → ∀ e ∈ s, w e = 0
Tactic: rw [affineIndependent_iff] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.Convex.Radon (hypothesis)
Goal:
ι : Type u_1
𝕜 : Type u_2
E : Type u_3
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
f : ι → E
h : ¬∀ (s : Finset ι) (w : ι → 𝕜), s.sum w = 0 → Eq.{u_3 + 1} (α := E) (∑ e ∈ s, w e • f e) 0 → ∀ e ∈ s, w e = 0
⊢ ∃ (I : Set ι),
    Set.Nonempty.{u_3} (α := E)
      ((convexHull 𝕜 : (a : Set E) → Set E) (f '' I) ∩ (convexHull 𝕜 : (a : Set E) → Set E) (f '' Iᶜ))
have h₁ : ∃ (s : Finset ι) (w : ι → 𝕜), s.sum w = 0 ∧ Eq.{u_3 + 1} (α := E) (∑ e ∈ s, w e • f e) 0 ∧ ∃ e ∈ s, w e ≠ 0
Tactic: push Not at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.Convex.Radon (goal)
Goal:
ι : Type u_1
𝕜 : Type u_2
E : Type u_3
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
f : ι → E
h : ∃ (s : Finset ι) (w : ι → 𝕜), s.sum w = 0 ∧ Eq.{u_3 + 1} (α := E) (∑ e ∈ s, w e • f e) 0 ∧ ∃ e ∈ s, w e ≠ 0
⊢ ∃ (I : Set ι),
    Set.Nonempty.{u_3} (α := E)
      ((convexHull 𝕜 : (a : Set E) → Set E) (f '' I) ∩ (convexHull 𝕜 : (a : Set E) → Set E) (f '' Iᶜ))
have obtain : ∀ (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 : Set ι),
    Set.Nonempty.{u_3} (α := E)
      ((convexHull 𝕜 : (a : Set E) → Set E) (f '' I) ∩ (convexHull 𝕜 : (a : Set E) → Set E) (f '' Iᶜ))
Tactic: obtain ⟨s, w, h_wsum, h_vsum, nonzero_w_index, h1, h2⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.Convex.Radon (hypothesis)
Goal:
ι : Type u_1
𝕜 : Type u_2
E : Type u_3
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
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
⊢ ∃ (I : Set ι),
    Set.Nonempty.{u_3} (α := E)
      ((convexHull 𝕜 : (a : Set E) → Set E) (f '' I) ∩ (convexHull 𝕜 : (a : Set E) → Set E) (f '' Iᶜ))
have hJI : HAdd.hAdd (α := 𝕜) (∑ j ∈ J, w j) (∑ i ∈ I, w i) = 0
Tactic: have hJI : ∑ j ∈ J, w j + ∑ i ∈ I, w i = 0 := by
    simpa only [h_wsum, not_lt] using sum_filter_add_sum_filter_not s (fun i ↦ w i < 0) w
-- 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
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
⊢ LT.lt.{u_2} (α := 𝕜) 0 (∑ i ∈ I, w i)
have rcases : ∀ (pos_w_index : ι) (h1' : pos_w_index ∈ s) (h2' : 0 < w pos_w_index), LT.lt.{u_2} (α := 𝕜) 0 (∑ i ∈ I, w i)
Tactic: rcases exists_pos_of_sum_zero_of_exists_nonzero _ h_wsum ⟨nonzero_w_index, h1, h2⟩
      with ⟨pos_w_index, h1', h2'⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.Radon (hypothesis)
Goal:
ι : Type u_1
𝕜 : Type u_2
E : Type u_3
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
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
⊢ ∃ (I : Set ι),
    Set.Nonempty.{u_3} (α := E)
      ((convexHull 𝕜 : (a : Set E) → Set E) (f '' I) ∩ (convexHull 𝕜 : (a : Set E) → Set E) (f '' Iᶜ))
have hI : LT.lt.{u_2} (α := 𝕜) 0 (∑ i ∈ I, w i)
Tactic: have hI : 0 < ∑ i ∈ I, w i := by
    rcases exists_pos_of_sum_zero_of_exists_nonzero _ h_wsum ⟨nonzero_w_index, h1, h2⟩
      with ⟨pos_w_index, h1', h2'⟩
    exact sum_pos' (fun _i hi ↦ (mem_filter.1 hi).2)
      ⟨pos_w_index, by simp only [I, mem_filter, h1', h2'.le, and_self, h2']⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.Radon (hypothesis)
Goal:
ι : Type u_1
𝕜 : Type u_2
E : Type u_3
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
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)
⊢ ∃ (I : Set ι),
    Set.Nonempty.{u_3} (α := E)
      ((convexHull 𝕜 : (a : Set E) → Set E) (f '' I) ∩ (convexHull 𝕜 : (a : Set E) → Set E) (f '' Iᶜ))
have hp : J.centerMass w f = p
Tactic: have hp : centerMass J w f = p := centerMass_of_sum_add_sum_eq_zero hJI <| by
    simpa only [← h_vsum, not_lt] using sum_filter_add_sum_filter_not s (fun i ↦ w i < 0) _
-- 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
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 : Set ι),
    Set.Nonempty.{u_3} (α := E)
      ((convexHull 𝕜 : (a : Set E) → Set E) (f '' I) ∩ (convexHull 𝕜 : (a : Set E) → Set E) (f '' Iᶜ))
have refine_1 : Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) (f '' (↑I : Set ι)) : Set E) p
Tactic: refine ⟨I, p, ?_, ?_⟩
-- 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
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_1 : Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) (f '' (↑I : Set ι)) : Set E) p
⊢ ∃ (I : Set ι),
    Set.Nonempty.{u_3} (α := E)
      ((convexHull 𝕜 : (a : Set E) → Set E) (f '' I) ∩ (convexHull 𝕜 : (a : Set E) → Set E) (f '' Iᶜ))
have refine_2 : Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) (f '' (↑I : Set ι)ᶜ) : Set E) p
Tactic: refine ⟨I, p, ?_, ?_⟩
-- 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
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
have refine_2 : Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) (f '' (↑I : Set ι)ᶜ) : Set E) (J.centerMass w f)
Tactic: rw [← hp]
-- 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
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)
have refine_2 : LT.lt.{u_2} (α := 𝕜) (∑ i ∈ J, w i) 0
Tactic: refine centerMass_mem_convexHull_of_nonpos _ (fun _ hi ↦ (mem_filter.mp hi).2.le) ?_
    (fun _i hi ↦ mem_image_of_mem _ fun hi' ↦ ?_)
-- 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
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
⊢ Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) (f '' (↑I : Set ι)ᶜ) : Set E) (J.centerMass w f)
have refine_2₁ : ∀ (_i : ι) (hi : _i ∈ J) (hi' : _i ∈ (↑I : Set ι)), False
Tactic: refine centerMass_mem_convexHull_of_nonpos _ (fun _ hi ↦ (mem_filter.mp hi).2.le) ?_
    (fun _i hi ↦ mem_image_of_mem _ fun hi' ↦ ?_)
-- 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
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
⊢ LT.lt.{u_2} (α := 𝕜) (∑ i ∈ J, w i) 0
have 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
Tactic: linarith only [hI, hJI]
-- 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: obtain h_card | h_card := lt_or_ge #s (finrank 𝕜 E + 1)
-- 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: obtain h_card | h_card := lt_or_ge #s (finrank 𝕜 E + 1)
-- 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)
h_card : finrank 𝕜 E + 1 ≤ #s
⊢ Set.Nonempty.{u_3} (α := E) (⋂ i ∈ s, F i)
have inr : ∀ (n : ℕ) (hn : #s = n), Set.Nonempty.{u_3} (α := E) (⋂ i ∈ s, F i)
Tactic: generalize hn : #s = n
-- Lean 4 proof step from Mathlib.Analysis.Convex.Radon (hypothesis)
Goal:
ι : Type u_1
𝕜 : Type u_2
E : Type u_3
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
inst_5 : FiniteDimensional 𝕜 E
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
⊢ Set.Nonempty.{u_3} (α := E) (⋂ i ∈ s, F i)
have h_card₁ : finrank 𝕜 E + 1 ≤ n
Tactic: rw [hn] at h_card
Cleared hypotheses: h_card, hn
-- 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
i : ↥s
⊢ Set.Nonempty.{u_3} (α := E) (⋂ j ∈ s.erase (↑i : ι), F j)
have h_convex₁ : ∀ i_1 ∈ s.erase (↑i : ι), Convex 𝕜 (F i_1)
Tactic: apply hk (s := s.erase 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
i : ↥s
h_convex₁ : ∀ i_1 ∈ s.erase (↑i : ι), Convex 𝕜 (F i_1)
⊢ Set.Nonempty.{u_3} (α := E) (⋂ j ∈ s.erase (↑i : ι), F j)
have h_inter₁ : ∀ I ⊆ s.erase (↑i : ι), #I ≤ finrank 𝕜 E + 1 → Set.Nonempty.{u_3} (α := E) (⋂ i ∈ I, F i)
Tactic: apply hk (s := s.erase 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
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)
⊢ Set.Nonempty.{u_3} (α := E) (⋂ j ∈ s.erase (↑i : ι), F j)
have hn₁ : #(s.erase (↑i : ι)) = k
Tactic: apply hk (s := s.erase 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
i : ↥s
⊢ #(s.erase (↑i : ι)) = k
have hn₁ : #s - 1 = k
Tactic: simp only [coe_mem, card_erase_of_mem]
-- 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) ⋯
⊢ ¬AffineIndependent 𝕜 a
have rw : finrank.{u_2, u_3} 𝕜 ↥(vectorSpan 𝕜 (Set.range a)) ≤ k - 1
Tactic: rw [← finrank_vectorSpan_le_iff_not_affineIndependent 𝕜 a (n := (k - 1))]
-- 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) ⋯
rw : finrank.{u_2, u_3} 𝕜 ↥(vectorSpan 𝕜 (Set.range a)) ≤ k - 1
⊢ ¬AffineIndependent 𝕜 a
have rw₁ : Fintype.card.{u_1} ↥s = k - 1 + 2
Tactic: rw [← finrank_vectorSpan_le_iff_not_affineIndependent 𝕜 a (n := (k - 1))]
-- 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) ⋯
⊢ Fintype.card.{u_1} ↥s = k - 1 + 2
have simp : #s = k - 1 + 2
Tactic: simp only [card_coe]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Radon (hypothesis)
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) ⋯
⊢ Set.Nonempty.{u_3} (α := E) (⋂ i ∈ s, F i)
have h_ind : ¬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
-- 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
⊢ Set.Nonempty.{u_3} (α := E) (⋂ i ∈ s, F i)
have 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)
Tactic: obtain ⟨I, p, hp_I, hp_Ic⟩ := radon_partition h_ind