Theorem: combiFrontier_eq (LeanCamCombi/SimplicialComplex/Simplex.lean)

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 : E
⊢ combiFrontier 𝕜 s =
    {x | ∃ w, ∃ (_ : ∀ y ∈ s, 0 ≤ w y) (_ : ∑ y ∈ s, w y = 1) (_ : ∃ y ∈ s, w y = 0), s.centerMass w id = x}
Tactic:
ext x
State after:
case h
𝕜 : 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 ∈ combiFrontier 𝕜 s ↔
    x ∈ {x | ∃ w, ∃ (_ : ∀ y ∈ s, 0 ≤ w y) (_ : ∑ y ∈ s, w y = 1) (_ : ∃ y ∈ s, w y = 0), s.centerMass w id = x}

State before:
case h
𝕜 : 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 ∈ combiFrontier 𝕜 s ↔
    x ∈ {x | ∃ w, ∃ (_ : ∀ y ∈ s, 0 ≤ w y) (_ : ∑ y ∈ s, w y = 1) (_ : ∃ y ∈ s, w y = 0), s.centerMass w id = x}
Tactic:
simp_rw [combiFrontier, Set.mem_iUnion, Set.mem_setOf_eq]
State after:
case h
𝕜 : 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
⊢ (∃ i, ∃ (_ : i ⊂ s), x ∈ (convexHull 𝕜) ↑i) ↔
    ∃ w, ∃ (_ : ∀ y ∈ s, 0 ≤ w y) (_ : ∑ y ∈ s, w y = 1) (_ : ∃ y ∈ s, w y = 0), s.centerMass w id = x

State before:
case h
𝕜 : 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
⊢ (∃ i, ∃ (_ : i ⊂ s), x ∈ (convexHull 𝕜) ↑i) ↔
    ∃ w, ∃ (_ : ∀ y ∈ s, 0 ≤ w y) (_ : ∑ y ∈ s, w y = 1) (_ : ∃ y ∈ s, w y = 0), s.centerMass w id = x
Tactic:
constructor
State after:
case h.mp
𝕜 : 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
⊢ (∃ i, ∃ (_ : i ⊂ s), x ∈ (convexHull 𝕜) ↑i) →
    ∃ w, ∃ (_ : ∀ y ∈ s, 0 ≤ w y) (_ : ∑ y ∈ s, w y = 1) (_ : ∃ y ∈ s, w y = 0), s.centerMass w id = x

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

State before:
case h.mp
𝕜 : 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
⊢ (∃ i, ∃ (_ : i ⊂ s), x ∈ (convexHull 𝕜) ↑i) →
    ∃ w, ∃ (_ : ∀ y ∈ s, 0 ≤ w y) (_ : ∑ y ∈ s, w y = 1) (_ : ∃ y ∈ s, w y = 0), s.centerMass w id = x
Tactic:
simp only [and_imp, exists_prop, exists_imp]
State after:
case h.mp
𝕜 : 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 ⊂ s,
    x ∈ (convexHull 𝕜) ↑x_1 → ∃ w, (∀ y ∈ s, 0 ≤ w y) ∧ ∑ y ∈ s, w y = 1 ∧ (∃ y ∈ s, w y = 0) ∧ s.centerMass w id = x

State before:
case h.mp
𝕜 : 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 ⊂ s,
    x ∈ (convexHull 𝕜) ↑x_1 → ∃ w, (∀ y ∈ s, 0 ≤ w y) ∧ ∑ y ∈ s, w y = 1 ∧ (∃ y ∈ s, w y = 0) ∧ s.centerMass w id = x
Tactic:
intro t ts hx
State after:
case h.mp
𝕜 : 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
hx : x ∈ (convexHull 𝕜) ↑t
⊢ ∃ w, (∀ y ∈ s, 0 ≤ w y) ∧ ∑ y ∈ s, w y = 1 ∧ (∃ y ∈ s, w y = 0) ∧ s.centerMass w id = x

State before:
case h.mp
𝕜 : 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
hx : x ∈ (convexHull 𝕜) ↑t
⊢ ∃ w, (∀ y ∈ s, 0 ≤ w y) ∧ ∑ y ∈ s, w y = 1 ∧ (∃ y ∈ s, w y = 0) ∧ s.centerMass w id = x
Tactic:
rw [Finset.convexHull_eq, Set.mem_setOf_eq] at hx
State after:
case h.mp
𝕜 : 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
hx : ∃ w, (∀ y ∈ t, 0 ≤ w y) ∧ ∑ y ∈ t, w y = 1 ∧ t.centerMass w id = x
⊢ ∃ w, (∀ y ∈ s, 0 ≤ w y) ∧ ∑ y ∈ s, w y = 1 ∧ (∃ y ∈ s, w y = 0) ∧ s.centerMass w id = x

State before:
case h.mp
𝕜 : 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
hx : ∃ w, (∀ y ∈ t, 0 ≤ w y) ∧ ∑ y ∈ t, w y = 1 ∧ t.centerMass w id = x
⊢ ∃ w, (∀ y ∈ s, 0 ≤ w y) ∧ ∑ y ∈ s, w y = 1 ∧ (∃ y ∈ s, w y = 0) ∧ s.centerMass w id = x
Tactic:
rcases hx with ⟨w, hw₀, hw₁, hx⟩
State after:
case h.mp.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
⊢ ∃ w, (∀ y ∈ s, 0 ≤ w y) ∧ ∑ y ∈ s, w y = 1 ∧ (∃ y ∈ s, w y = 0) ∧ s.centerMass w id = x

State before:
case h.mp.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
⊢ ∃ w, (∀ y ∈ s, 0 ≤ w y) ∧ ∑ y ∈ s, w y = 1 ∧ (∃ y ∈ s, w y = 0) ∧ s.centerMass w id = x
Tactic:
rcases Finset.exists_of_ssubset ts with ⟨y, hys, hyt⟩
State after:
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, (∀ y ∈ s, 0 ≤ w y) ∧ ∑ y ∈ s, w y = 1 ∧ (∃ y ∈ s, w y = 0) ∧ s.centerMass w id = x

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, (∀ y ∈ s, 0 ≤ w y) ∧ ∑ y ∈ s, w y = 1 ∧ (∃ y ∈ s, w y = 0) ∧ s.centerMass w id = x
Tactic:
let w' z := if z ∈ t then w z else 0
State after:
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
⊢ ∃ w, (∀ y ∈ s, 0 ≤ w y) ∧ ∑ y ∈ s, w y = 1 ∧ (∃ y ∈ s, w y = 0) ∧ s.centerMass w id = x

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
⊢ ∃ w, (∀ y ∈ s, 0 ≤ w y) ∧ ∑ y ∈ s, w y = 1 ∧ (∃ y ∈ s, w y = 0) ∧ s.centerMass w id = x
Tactic:
have hw'₁ : s.sum w' = 1 := by
  rwa [← Finset.sum_subset ts.1, Finset.sum_extend_by_zero]
  simp only [ite_eq_right_iff]
  tauto
State after:
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

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›, _⟩, _⟩
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

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]
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

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
State after:
no goals

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]
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

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]
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

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
State after:
no goals

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

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

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

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 ‹_›
State after:
no goals

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
State after:
no goals

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›
State after:
no goals

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]
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

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]
State after:
no goals

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

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]
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

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

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

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 _ _ _ • _ = _
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

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]
State after:
no goals

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]
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

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₃
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

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₁, _⟩
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)

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]
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

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), _, _⟩
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

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₂]
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

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₂
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

State before:
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:
rwa [Finset.centerMass_subset _ (s.erase_subset _)]
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
⊢ ∀ i ∈ s, i ∉ s.erase y → w i = 0

State before:
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
⊢ ∀ i ∈ s, i ∉ s.erase y → w i = 0
Tactic:
intro i hi₁ hi₂
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
i : E
hi₁ : i ∈ s
hi₂ : i ∉ s.erase y
⊢ w i = 0

State before:
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
i : E
hi₁ : i ∈ s
hi₂ : i ∉ s.erase y
⊢ w i = 0
Tactic:
simp only [hi₁, and_true_iff, Classical.not_not, Finset.mem_erase] at hi₂
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
i : E
hi₁ : i ∈ s
hi₂ : i = y
⊢ w i = 0

State before:
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
i : E
hi₁ : i ∈ s
hi₂ : i = y
⊢ w i = 0
Tactic:
subst hi₂
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
hy₃ : s.centerMass w id = x
i : E
hi₁ hy₁ : i ∈ s
hy₂ : w i = 0
⊢ w i = 0

State before:
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
hy₃ : s.centerMass w id = x
i : E
hi₁ hy₁ : i ∈ s
hy₂ : w i = 0
⊢ w i = 0
Tactic:
apply hy₂
State after:
no goals