internlm/Lean-Github huggingface dataset:
Theorem: combiFrontier_eq
Proof state before:
case h.mp.intro.intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t✝ : Finset E
x✝ x : E
t : Finset E
ts : t ⊂ s
w : E → 𝕜
hw₀ : ∀ y ∈ t, 0 ≤ w y
hw₁ : ∑ y ∈ t, w y = 1
hx : t.centerMass w id = x
y : E
hys : y ∈ s
hyt : y ∉ t
w' : E → 𝕜 := fun z => if z ∈ t then w z else 0
hw'₁ : s.sum w' = 1
⊢ ∃ w, (∀ y ∈ s, 0 ≤ w y) ∧ ∑ y ∈ s, w y = 1 ∧ (∃ y ∈ s, w y = 0) ∧ s.centerMass w id = x
Tactic:
refine' ⟨w', _, hw'₁, ⟨_, ‹y ∈ s›, _⟩, _⟩
Proof state after:
case h.mp.intro.intro.intro.intro.intro.refine'_1
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t✝ : Finset E
x✝ x : E
t : Finset E
ts : t ⊂ s
w : E → 𝕜
hw₀ : ∀ y ∈ t, 0 ≤ w y
hw₁ : ∑ y ∈ t, w y = 1
hx : t.centerMass w id = x
y : E
hys : y ∈ s
hyt : y ∉ t
w' : E → 𝕜 := fun z => if z ∈ t then w z else 0
hw'₁ : s.sum w' = 1
⊢ ∀ y ∈ s, 0 ≤ w' y

case h.mp.intro.intro.intro.intro.intro.refine'_2
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t✝ : Finset E
x✝ x : E
t : Finset E
ts : t ⊂ s
w : E → 𝕜
hw₀ : ∀ y ∈ t, 0 ≤ w y
hw₁ : ∑ y ∈ t, w y = 1
hx : t.centerMass w id = x
y : E
hys : y ∈ s
hyt : y ∉ t
w' : E → 𝕜 := fun z => if z ∈ t then w z else 0
hw'₁ : s.sum w' = 1
⊢ w' y = 0

case h.mp.intro.intro.intro.intro.intro.refine'_3
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t✝ : Finset E
x✝ x : E
t : Finset E
ts : t ⊂ s
w : E → 𝕜
hw₀ : ∀ y ∈ t, 0 ≤ w y
hw₁ : ∑ y ∈ t, w y = 1
hx : t.centerMass w id = x
y : E
hys : y ∈ s
hyt : y ∉ t
w' : E → 𝕜 := fun z => if z ∈ t then w z else 0
hw'₁ : s.sum w' = 1
⊢ s.centerMass w' id = x
Theorem: combiFrontier_eq
Proof state before:
case h.mp.intro.intro.intro.intro.intro.refine'_3
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t✝ : Finset E
x✝ x : E
t : Finset E
ts : t ⊂ s
w : E → 𝕜
hw₀ : ∀ y ∈ t, 0 ≤ w y
hw₁ : ∑ y ∈ t, w y = 1
hx : t.centerMass w id = x
y : E
hys : y ∈ s
hyt : y ∉ t
w' : E → 𝕜 := fun z => if z ∈ t then w z else 0
hw'₁ : s.sum w' = 1
⊢ s.centerMass w' id = x
Tactic:
rw [← Finset.centerMass_subset id ts.1]
Proof state after:
case h.mp.intro.intro.intro.intro.intro.refine'_3
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t✝ : Finset E
x✝ x : E
t : Finset E
ts : t ⊂ s
w : E → 𝕜
hw₀ : ∀ y ∈ t, 0 ≤ w y
hw₁ : ∑ y ∈ t, w y = 1
hx : t.centerMass w id = x
y : E
hys : y ∈ s
hyt : y ∉ t
w' : E → 𝕜 := fun z => if z ∈ t then w z else 0
hw'₁ : s.sum w' = 1
⊢ t.centerMass w' id = x

case h.mp.intro.intro.intro.intro.intro.refine'_3
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t✝ : Finset E
x✝ x : E
t : Finset E
ts : t ⊂ s
w : E → 𝕜
hw₀ : ∀ y ∈ t, 0 ≤ w y
hw₁ : ∑ y ∈ t, w y = 1
hx : t.centerMass w id = x
y : E
hys : y ∈ s
hyt : y ∉ t
w' : E → 𝕜 := fun z => if z ∈ t then w z else 0
hw'₁ : s.sum w' = 1
⊢ ∀ i ∈ s, i ∉ t → w' i = 0
Theorem: combiFrontier_eq
Proof state before:
case h.mp.intro.intro.intro.intro.intro.refine'_3
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t✝ : Finset E
x✝ x : E
t : Finset E
ts : t ⊂ s
w : E → 𝕜
hw₀ : ∀ y ∈ t, 0 ≤ w y
hw₁ : ∑ y ∈ t, w y = 1
hx : t.centerMass w id = x
y : E
hys : y ∈ s
hyt : y ∉ t
w' : E → 𝕜 := fun z => if z ∈ t then w z else 0
hw'₁ : s.sum w' = 1
⊢ ∀ i ∈ s, i ∉ t → w' i = 0
Tactic:
exact fun i _ hi => if_neg hi
Proof state after:
no goals
Theorem: combiFrontier_eq
Proof state before:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t✝ : Finset E
x✝ x : E
t : Finset E
ts : t ⊂ s
w : E → 𝕜
hw₀ : ∀ y ∈ t, 0 ≤ w y
hw₁ : ∑ y ∈ t, w y = 1
hx : t.centerMass w id = x
y : E
hys : y ∈ s
hyt : y ∉ t
w' : E → 𝕜 := fun z => if z ∈ t then w z else 0
⊢ s.sum w' = 1
Tactic:
rwa [← Finset.sum_subset ts.1, Finset.sum_extend_by_zero]
Proof state after:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t✝ : Finset E
x✝ x : E
t : Finset E
ts : t ⊂ s
w : E → 𝕜
hw₀ : ∀ y ∈ t, 0 ≤ w y
hw₁ : ∑ y ∈ t, w y = 1
hx : t.centerMass w id = x
y : E
hys : y ∈ s
hyt : y ∉ t
w' : E → 𝕜 := fun z => if z ∈ t then w z else 0
⊢ ∀ x ∈ s, x ∉ t → (if x ∈ t then w x else 0) = 0
Theorem: combiFrontier_eq
Proof state before:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t✝ : Finset E
x✝ x : E
t : Finset E
ts : t ⊂ s
w : E → 𝕜
hw₀ : ∀ y ∈ t, 0 ≤ w y
hw₁ : ∑ y ∈ t, w y = 1
hx : t.centerMass w id = x
y : E
hys : y ∈ s
hyt : y ∉ t
w' : E → 𝕜 := fun z => if z ∈ t then w z else 0
⊢ ∀ x ∈ s, x ∉ t → (if x ∈ t then w x else 0) = 0
Tactic:
simp only [ite_eq_right_iff]
Proof state after:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t✝ : Finset E
x✝ x : E
t : Finset E
ts : t ⊂ s
w : E → 𝕜
hw₀ : ∀ y ∈ t, 0 ≤ w y
hw₁ : ∑ y ∈ t, w y = 1
hx : t.centerMass w id = x
y : E
hys : y ∈ s
hyt : y ∉ t
w' : E → 𝕜 := fun z => if z ∈ t then w z else 0
⊢ ∀ x ∈ s, x ∉ t → x ∈ t → w x = 0
Theorem: combiFrontier_eq
Proof state before:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t✝ : Finset E
x✝ x : E
t : Finset E
ts : t ⊂ s
w : E → 𝕜
hw₀ : ∀ y ∈ t, 0 ≤ w y
hw₁ : ∑ y ∈ t, w y = 1
hx : t.centerMass w id = x
y : E
hys : y ∈ s
hyt : y ∉ t
w' : E → 𝕜 := fun z => if z ∈ t then w z else 0
⊢ ∀ x ∈ s, x ∉ t → x ∈ t → w x = 0
Tactic:
tauto
Proof state after:
no goals
Theorem: combiFrontier_eq
Proof state before:
case h.mp.intro.intro.intro.intro.intro.refine'_1
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t✝ : Finset E
x✝ x : E
t : Finset E
ts : t ⊂ s
w : E → 𝕜
hw₀ : ∀ y ∈ t, 0 ≤ w y
hw₁ : ∑ y ∈ t, w y = 1
hx : t.centerMass w id = x
y : E
hys : y ∈ s
hyt : y ∉ t
w' : E → 𝕜 := fun z => if z ∈ t then w z else 0
hw'₁ : s.sum w' = 1
⊢ ∀ y ∈ s, 0 ≤ w' y
Tactic:
rintro y -
Proof state after:
case h.mp.intro.intro.intro.intro.intro.refine'_1
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t✝ : Finset E
x✝ x : E
t : Finset E
ts : t ⊂ s
w : E → 𝕜
hw₀ : ∀ y ∈ t, 0 ≤ w y
hw₁ : ∑ y ∈ t, w y = 1
hx : t.centerMass w id = x
y✝ : E
hys : y✝ ∈ s
hyt : y✝ ∉ t
w' : E → 𝕜 := fun z => if z ∈ t then w z else 0
hw'₁ : s.sum w' = 1
y : E
⊢ 0 ≤ w' y
Theorem: combiFrontier_eq
Proof state before:
case h.mp.intro.intro.intro.intro.intro.refine'_1
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t✝ : Finset E
x✝ x : E
t : Finset E
ts : t ⊂ s
w : E → 𝕜
hw₀ : ∀ y ∈ t, 0 ≤ w y
hw₁ : ∑ y ∈ t, w y = 1
hx : t.centerMass w id = x
y✝ : E
hys : y✝ ∈ s
hyt : y✝ ∉ t
w' : E → 𝕜 := fun z => if z ∈ t then w z else 0
hw'₁ : s.sum w' = 1
y : E
⊢ 0 ≤ w' y
Tactic:
change 0 ≤ ite (y ∈ t) (w y) 0
Proof state after:
case h.mp.intro.intro.intro.intro.intro.refine'_1
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t✝ : Finset E
x✝ x : E
t : Finset E
ts : t ⊂ s
w : E → 𝕜
hw₀ : ∀ y ∈ t, 0 ≤ w y
hw₁ : ∑ y ∈ t, w y = 1
hx : t.centerMass w id = x
y✝ : E
hys : y✝ ∈ s
hyt : y✝ ∉ t
w' : E → 𝕜 := fun z => if z ∈ t then w z else 0
hw'₁ : s.sum w' = 1
y : E
⊢ 0 ≤ if y ∈ t then w y else 0
Theorem: combiFrontier_eq
Proof state before:
case h.mp.intro.intro.intro.intro.intro.refine'_1
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t✝ : Finset E
x✝ x : E
t : Finset E
ts : t ⊂ s
w : E → 𝕜
hw₀ : ∀ y ∈ t, 0 ≤ w y
hw₁ : ∑ y ∈ t, w y = 1
hx : t.centerMass w id = x
y✝ : E
hys : y✝ ∈ s
hyt : y✝ ∉ t
w' : E → 𝕜 := fun z => if z ∈ t then w z else 0
hw'₁ : s.sum w' = 1
y : E
⊢ 0 ≤ if y ∈ t then w y else 0
Tactic:
split_ifs
Proof state after:
case pos
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t✝ : Finset E
x✝ x : E
t : Finset E
ts : t ⊂ s
w : E → 𝕜
hw₀ : ∀ y ∈ t, 0 ≤ w y
hw₁ : ∑ y ∈ t, w y = 1
hx : t.centerMass w id = x
y✝ : E
hys : y✝ ∈ s
hyt : y✝ ∉ t
w' : E → 𝕜 := fun z => if z ∈ t then w z else 0
hw'₁ : s.sum w' = 1
y : E
h✝ : y ∈ t
⊢ 0 ≤ w y

case neg
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t✝ : Finset E
x✝ x : E
t : Finset E
ts : t ⊂ s
w : E → 𝕜
hw₀ : ∀ y ∈ t, 0 ≤ w y
hw₁ : ∑ y ∈ t, w y = 1
hx : t.centerMass w id = x
y✝ : E
hys : y✝ ∈ s
hyt : y✝ ∉ t
w' : E → 𝕜 := fun z => if z ∈ t then w z else 0
hw'₁ : s.sum w' = 1
y : E
h✝ : y ∉ t
⊢ 0 ≤ 0
Theorem: combiFrontier_eq
Proof state before:
case pos
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t✝ : Finset E
x✝ x : E
t : Finset E
ts : t ⊂ s
w : E → 𝕜
hw₀ : ∀ y ∈ t, 0 ≤ w y
hw₁ : ∑ y ∈ t, w y = 1
hx : t.centerMass w id = x
y✝ : E
hys : y✝ ∈ s
hyt : y✝ ∉ t
w' : E → 𝕜 := fun z => if z ∈ t then w z else 0
hw'₁ : s.sum w' = 1
y : E
h✝ : y ∈ t
⊢ 0 ≤ w y
Tactic:
apply hw₀ y ‹_›
Proof state after:
no goals
Theorem: combiFrontier_eq
Proof state before:
case neg
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t✝ : Finset E
x✝ x : E
t : Finset E
ts : t ⊂ s
w : E → 𝕜
hw₀ : ∀ y ∈ t, 0 ≤ w y
hw₁ : ∑ y ∈ t, w y = 1
hx : t.centerMass w id = x
y✝ : E
hys : y✝ ∈ s
hyt : y✝ ∉ t
w' : E → 𝕜 := fun z => if z ∈ t then w z else 0
hw'₁ : s.sum w' = 1
y : E
h✝ : y ∉ t
⊢ 0 ≤ 0
Tactic:
rfl
Proof state after:
no goals
Theorem: combiFrontier_eq
Proof state before:
case h.mp.intro.intro.intro.intro.intro.refine'_2
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t✝ : Finset E
x✝ x : E
t : Finset E
ts : t ⊂ s
w : E → 𝕜
hw₀ : ∀ y ∈ t, 0 ≤ w y
hw₁ : ∑ y ∈ t, w y = 1
hx : t.centerMass w id = x
y : E
hys : y ∈ s
hyt : y ∉ t
w' : E → 𝕜 := fun z => if z ∈ t then w z else 0
hw'₁ : s.sum w' = 1
⊢ w' y = 0
Tactic:
apply if_neg ‹y ∉ t›
Proof state after:
no goals
Theorem: combiFrontier_eq
Proof state before:
case h.mp.intro.intro.intro.intro.intro.refine'_3
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t✝ : Finset E
x✝ x : E
t : Finset E
ts : t ⊂ s
w : E → 𝕜
hw₀ : ∀ y ∈ t, 0 ≤ w y
hw₁ : ∑ y ∈ t, w y = 1
hx : t.centerMass w id = x
y : E
hys : y ∈ s
hyt : y ∉ t
w' : E → 𝕜 := fun z => if z ∈ t then w z else 0
hw'₁ : s.sum w' = 1
⊢ t.centerMass w' id = x
Tactic:
rw [Finset.centerMass_eq_of_sum_1]
Proof state after:
case h.mp.intro.intro.intro.intro.intro.refine'_3
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t✝ : Finset E
x✝ x : E
t : Finset E
ts : t ⊂ s
w : E → 𝕜
hw₀ : ∀ y ∈ t, 0 ≤ w y
hw₁ : ∑ y ∈ t, w y = 1
hx : t.centerMass w id = x
y : E
hys : y ∈ s
hyt : y ∉ t
w' : E → 𝕜 := fun z => if z ∈ t then w z else 0
hw'₁ : s.sum w' = 1
⊢ ∑ i ∈ t, w' i • id i = x

case h.mp.intro.intro.intro.intro.intro.refine'_3.hw
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t✝ : Finset E
x✝ x : E
t : Finset E
ts : t ⊂ s
w : E → 𝕜
hw₀ : ∀ y ∈ t, 0 ≤ w y
hw₁ : ∑ y ∈ t, w y = 1
hx : t.centerMass w id = x
y : E
hys : y ∈ s
hyt : y ∉ t
w' : E → 𝕜 := fun z => if z ∈ t then w z else 0
hw'₁ : s.sum w' = 1
⊢ ∑ i ∈ t, w' i = 1
Theorem: combiFrontier_eq
Proof state before:
case h.mp.intro.intro.intro.intro.intro.refine'_3.hw
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t✝ : Finset E
x✝ x : E
t : Finset E
ts : t ⊂ s
w : E → 𝕜
hw₀ : ∀ y ∈ t, 0 ≤ w y
hw₁ : ∑ y ∈ t, w y = 1
hx : t.centerMass w id = x
y : E
hys : y ∈ s
hyt : y ∉ t
w' : E → 𝕜 := fun z => if z ∈ t then w z else 0
hw'₁ : s.sum w' = 1
⊢ ∑ i ∈ t, w' i = 1
Tactic:
rwa [Finset.sum_extend_by_zero]
Proof state after:
no goals
Theorem: combiFrontier_eq
Proof state before:
case h.mp.intro.intro.intro.intro.intro.refine'_3
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t✝ : Finset E
x✝ x : E
t : Finset E
ts : t ⊂ s
w : E → 𝕜
hw₀ : ∀ y ∈ t, 0 ≤ w y
hw₁ : ∑ y ∈ t, w y = 1
hx : t.centerMass w id = x
y : E
hys : y ∈ s
hyt : y ∉ t
w' : E → 𝕜 := fun z => if z ∈ t then w z else 0
hw'₁ : s.sum w' = 1
⊢ ∑ i ∈ t, w' i • id i = x
Tactic:
rw [Finset.centerMass_eq_of_sum_1 _ _ hw₁] at hx
Proof state after:
case h.mp.intro.intro.intro.intro.intro.refine'_3
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t✝ : Finset E
x✝ x : E
t : Finset E
ts : t ⊂ s
w : E → 𝕜
hw₀ : ∀ y ∈ t, 0 ≤ w y
hw₁ : ∑ y ∈ t, w y = 1
hx : ∑ i ∈ t, w i • id i = x
y : E
hys : y ∈ s
hyt : y ∉ t
w' : E → 𝕜 := fun z => if z ∈ t then w z else 0
hw'₁ : s.sum w' = 1
⊢ ∑ i ∈ t, w' i • id i = x
Theorem: combiFrontier_eq
Proof state before:
case h.mp.intro.intro.intro.intro.intro.refine'_3
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t✝ : Finset E
x✝ x : E
t : Finset E
ts : t ⊂ s
w : E → 𝕜
hw₀ : ∀ y ∈ t, 0 ≤ w y
hw₁ : ∑ y ∈ t, w y = 1
hx : ∑ i ∈ t, w i • id i = x
y : E
hys : y ∈ s
hyt : y ∉ t
w' : E → 𝕜 := fun z => if z ∈ t then w z else 0
hw'₁ : s.sum w' = 1
⊢ ∑ i ∈ t, w' i • id i = x
Tactic:
rw [← hx]
Proof state after:
case h.mp.intro.intro.intro.intro.intro.refine'_3
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t✝ : Finset E
x✝ x : E
t : Finset E
ts : t ⊂ s
w : E → 𝕜
hw₀ : ∀ y ∈ t, 0 ≤ w y
hw₁ : ∑ y ∈ t, w y = 1
hx : ∑ i ∈ t, w i • id i = x
y : E
hys : y ∈ s
hyt : y ∉ t
w' : E → 𝕜 := fun z => if z ∈ t then w z else 0
hw'₁ : s.sum w' = 1
⊢ ∑ i ∈ t, w' i • id i = ∑ i ∈ t, w i • id i
Theorem: combiFrontier_eq
Proof state before:
case h.mp.intro.intro.intro.intro.intro.refine'_3
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t✝ : Finset E
x✝ x : E
t : Finset E
ts : t ⊂ s
w : E → 𝕜
hw₀ : ∀ y ∈ t, 0 ≤ w y
hw₁ : ∑ y ∈ t, w y = 1
hx : ∑ i ∈ t, w i • id i = x
y : E
hys : y ∈ s
hyt : y ∉ t
w' : E → 𝕜 := fun z => if z ∈ t then w z else 0
hw'₁ : s.sum w' = 1
⊢ ∑ i ∈ t, w' i • id i = ∑ i ∈ t, w i • id i
Tactic:
apply Finset.sum_congr rfl
Proof state after:
case h.mp.intro.intro.intro.intro.intro.refine'_3
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t✝ : Finset E
x✝ x : E
t : Finset E
ts : t ⊂ s
w : E → 𝕜
hw₀ : ∀ y ∈ t, 0 ≤ w y
hw₁ : ∑ y ∈ t, w y = 1
hx : ∑ i ∈ t, w i • id i = x
y : E
hys : y ∈ s
hyt : y ∉ t
w' : E → 𝕜 := fun z => if z ∈ t then w z else 0
hw'₁ : s.sum w' = 1
⊢ ∀ x ∈ t, w' x • id x = w x • id x
Theorem: combiFrontier_eq
Proof state before:
case h.mp.intro.intro.intro.intro.intro.refine'_3
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t✝ : Finset E
x✝ x : E
t : Finset E
ts : t ⊂ s
w : E → 𝕜
hw₀ : ∀ y ∈ t, 0 ≤ w y
hw₁ : ∑ y ∈ t, w y = 1
hx : ∑ i ∈ t, w i • id i = x
y : E
hys : y ∈ s
hyt : y ∉ t
w' : E → 𝕜 := fun z => if z ∈ t then w z else 0
hw'₁ : s.sum w' = 1
⊢ ∀ x ∈ t, w' x • id x = w x • id x
Tactic:
intro x hx
Proof state after:
case h.mp.intro.intro.intro.intro.intro.refine'_3
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t✝ : Finset E
x✝¹ x✝ : E
t : Finset E
ts : t ⊂ s
w : E → 𝕜
hw₀ : ∀ y ∈ t, 0 ≤ w y
hw₁ : ∑ y ∈ t, w y = 1
hx✝ : ∑ i ∈ t, w i • id i = x✝
y : E
hys : y ∈ s
hyt : y ∉ t
w' : E → 𝕜 := fun z => if z ∈ t then w z else 0
hw'₁ : s.sum w' = 1
x : E
hx : x ∈ t
⊢ w' x • id x = w x • id x
Theorem: combiFrontier_eq
Proof state before:
case h.mp.intro.intro.intro.intro.intro.refine'_3
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t✝ : Finset E
x✝¹ x✝ : E
t : Finset E
ts : t ⊂ s
w : E → 𝕜
hw₀ : ∀ y ∈ t, 0 ≤ w y
hw₁ : ∑ y ∈ t, w y = 1
hx✝ : ∑ i ∈ t, w i • id i = x✝
y : E
hys : y ∈ s
hyt : y ∉ t
w' : E → 𝕜 := fun z => if z ∈ t then w z else 0
hw'₁ : s.sum w' = 1
x : E
hx : x ∈ t
⊢ w' x • id x = w x • id x
Tactic:
change ite _ _ _ • _ = _
Proof state after:
case h.mp.intro.intro.intro.intro.intro.refine'_3
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t✝ : Finset E
x✝¹ x✝ : E
t : Finset E
ts : t ⊂ s
w : E → 𝕜
hw₀ : ∀ y ∈ t, 0 ≤ w y
hw₁ : ∑ y ∈ t, w y = 1
hx✝ : ∑ i ∈ t, w i • id i = x✝
y : E
hys : y ∈ s
hyt : y ∉ t
w' : E → 𝕜 := fun z => if z ∈ t then w z else 0
hw'₁ : s.sum w' = 1
x : E
hx : x ∈ t
⊢ (if x ∈ t then w x else 0) • id x = w x • id x
Theorem: combiFrontier_eq
Proof state before:
case h.mp.intro.intro.intro.intro.intro.refine'_3
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t✝ : Finset E
x✝¹ x✝ : E
t : Finset E
ts : t ⊂ s
w : E → 𝕜
hw₀ : ∀ y ∈ t, 0 ≤ w y
hw₁ : ∑ y ∈ t, w y = 1
hx✝ : ∑ i ∈ t, w i • id i = x✝
y : E
hys : y ∈ s
hyt : y ∉ t
w' : E → 𝕜 := fun z => if z ∈ t then w z else 0
hw'₁ : s.sum w' = 1
x : E
hx : x ∈ t
⊢ (if x ∈ t then w x else 0) • id x = w x • id x
Tactic:
rw [if_pos hx]
Proof state after:
no goals
Theorem: combiFrontier_eq
Proof state before:
case h.mpr
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Finset E
x✝ x : E
⊢ (∃ w, ∃ (_ : ∀ y ∈ s, 0 ≤ w y) (_ : ∑ y ∈ s, w y = 1) (_ : ∃ y ∈ s, w y = 0), s.centerMass w id = x) →
    ∃ i, ∃ (_ : i ⊂ s), x ∈ (convexHull 𝕜) ↑i
Tactic:
simp only [and_imp, exists_prop, exists_imp]
Proof state after:
case h.mpr
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Finset E
x✝ x : E
⊢ ∀ (x_1 : E → 𝕜),
    (∀ y ∈ s, 0 ≤ x_1 y) →
      ∑ y ∈ s, x_1 y = 1 → ∀ x_2 ∈ s, x_1 x_2 = 0 → s.centerMass x_1 id = x → ∃ i ⊂ s, x ∈ (convexHull 𝕜) ↑i
Theorem: combiFrontier_eq
Proof state before:
case h.mpr
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Finset E
x✝ x : E
⊢ ∀ (x_1 : E → 𝕜),
    (∀ y ∈ s, 0 ≤ x_1 y) →
      ∑ y ∈ s, x_1 y = 1 → ∀ x_2 ∈ s, x_1 x_2 = 0 → s.centerMass x_1 id = x → ∃ i ⊂ s, x ∈ (convexHull 𝕜) ↑i
Tactic:
intro w hw₁ hw₂ y hy₁ hy₂ hy₃
Proof state after:
case h.mpr
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Finset E
x✝ x : E
w : E → 𝕜
hw₁ : ∀ y ∈ s, 0 ≤ w y
hw₂ : ∑ y ∈ s, w y = 1
y : E
hy₁ : y ∈ s
hy₂ : w y = 0
hy₃ : s.centerMass w id = x
⊢ ∃ i ⊂ s, x ∈ (convexHull 𝕜) ↑i
Theorem: combiFrontier_eq
Proof state before:
case h.mpr
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Finset E
x✝ x : E
w : E → 𝕜
hw₁ : ∀ y ∈ s, 0 ≤ w y
hw₂ : ∑ y ∈ s, w y = 1
y : E
hy₁ : y ∈ s
hy₂ : w y = 0
hy₃ : s.centerMass w id = x
⊢ ∃ i ⊂ s, x ∈ (convexHull 𝕜) ↑i
Tactic:
refine' ⟨s.erase y, Finset.erase_ssubset hy₁, _⟩
Proof state after:
case h.mpr
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Finset E
x✝ x : E
w : E → 𝕜
hw₁ : ∀ y ∈ s, 0 ≤ w y
hw₂ : ∑ y ∈ s, w y = 1
y : E
hy₁ : y ∈ s
hy₂ : w y = 0
hy₃ : s.centerMass w id = x
⊢ x ∈ (convexHull 𝕜) ↑(s.erase y)
Theorem: combiFrontier_eq
Proof state before:
case h.mpr
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Finset E
x✝ x : E
w : E → 𝕜
hw₁ : ∀ y ∈ s, 0 ≤ w y
hw₂ : ∑ y ∈ s, w y = 1
y : E
hy₁ : y ∈ s
hy₂ : w y = 0
hy₃ : s.centerMass w id = x
⊢ x ∈ (convexHull 𝕜) ↑(s.erase y)
Tactic:
rw [Finset.convexHull_eq, Set.mem_setOf_eq]
Proof state after:
case h.mpr
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Finset E
x✝ x : E
w : E → 𝕜
hw₁ : ∀ y ∈ s, 0 ≤ w y
hw₂ : ∑ y ∈ s, w y = 1
y : E
hy₁ : y ∈ s
hy₂ : w y = 0
hy₃ : s.centerMass w id = x
⊢ ∃ w, (∀ y_1 ∈ s.erase y, 0 ≤ w y_1) ∧ ∑ y ∈ s.erase y, w y = 1 ∧ (s.erase y).centerMass w id = x
Theorem: combiFrontier_eq
Proof state before:
case h.mpr
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Finset E
x✝ x : E
w : E → 𝕜
hw₁ : ∀ y ∈ s, 0 ≤ w y
hw₂ : ∑ y ∈ s, w y = 1
y : E
hy₁ : y ∈ s
hy₂ : w y = 0
hy₃ : s.centerMass w id = x
⊢ ∃ w, (∀ y_1 ∈ s.erase y, 0 ≤ w y_1) ∧ ∑ y ∈ s.erase y, w y = 1 ∧ (s.erase y).centerMass w id = x
Tactic:
refine' ⟨w, fun z hz => hw₁ z (s.erase_subset _ hz), _, _⟩
Proof state after:
case h.mpr.refine'_1
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Finset E
x✝ x : E
w : E → 𝕜
hw₁ : ∀ y ∈ s, 0 ≤ w y
hw₂ : ∑ y ∈ s, w y = 1
y : E
hy₁ : y ∈ s
hy₂ : w y = 0
hy₃ : s.centerMass w id = x
⊢ ∑ y ∈ s.erase y, w y = 1

case h.mpr.refine'_2
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Finset E
x✝ x : E
w : E → 𝕜
hw₁ : ∀ y ∈ s, 0 ≤ w y
hw₂ : ∑ y ∈ s, w y = 1
y : E
hy₁ : y ∈ s
hy₂ : w y = 0
hy₃ : s.centerMass w id = x
⊢ (s.erase y).centerMass w id = x
Theorem: combiFrontier_eq
Proof state before:
case h.mpr.refine'_1
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Finset E
x✝ x : E
w : E → 𝕜
hw₁ : ∀ y ∈ s, 0 ≤ w y
hw₂ : ∑ y ∈ s, w y = 1
y : E
hy₁ : y ∈ s
hy₂ : w y = 0
hy₃ : s.centerMass w id = x
⊢ ∑ y ∈ s.erase y, w y = 1

case h.mpr.refine'_2
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Finset E
x✝ x : E
w : E → 𝕜
hw₁ : ∀ y ∈ s, 0 ≤ w y
hw₂ : ∑ y ∈ s, w y = 1
y : E
hy₁ : y ∈ s
hy₂ : w y = 0
hy₃ : s.centerMass w id = x
⊢ (s.erase y).centerMass w id = x
Tactic:
rw [Finset.sum_erase _ hy₂]
Proof state after:
case h.mpr.refine'_1
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Finset E
x✝ x : E
w : E → 𝕜
hw₁ : ∀ y ∈ s, 0 ≤ w y
hw₂ : ∑ y ∈ s, w y = 1
y : E
hy₁ : y ∈ s
hy₂ : w y = 0
hy₃ : s.centerMass w id = x
⊢ ∑ x ∈ s, w x = 1

case h.mpr.refine'_2
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Finset E
x✝ x : E
w : E → 𝕜
hw₁ : ∀ y ∈ s, 0 ≤ w y
hw₂ : ∑ y ∈ s, w y = 1
y : E
hy₁ : y ∈ s
hy₂ : w y = 0
hy₃ : s.centerMass w id = x
⊢ (s.erase y).centerMass w id = x
Theorem: combiFrontier_eq
Proof state before:
case h.mpr.refine'_1
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Finset E
x✝ x : E
w : E → 𝕜
hw₁ : ∀ y ∈ s, 0 ≤ w y
hw₂ : ∑ y ∈ s, w y = 1
y : E
hy₁ : y ∈ s
hy₂ : w y = 0
hy₃ : s.centerMass w id = x
⊢ ∑ x ∈ s, w x = 1

case h.mpr.refine'_2
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Finset E
x✝ x : E
w : E → 𝕜
hw₁ : ∀ y ∈ s, 0 ≤ w y
hw₂ : ∑ y ∈ s, w y = 1
y : E
hy₁ : y ∈ s
hy₂ : w y = 0
hy₃ : s.centerMass w id = x
⊢ (s.erase y).centerMass w id = x
Tactic:
apply hw₂
Proof state after:
case h.mpr.refine'_2
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Finset E
x✝ x : E
w : E → 𝕜
hw₁ : ∀ y ∈ s, 0 ≤ w y
hw₂ : ∑ y ∈ s, w y = 1
y : E
hy₁ : y ∈ s
hy₂ : w y = 0
hy₃ : s.centerMass w id = x
⊢ (s.erase y).centerMass w id = x