R : Type u_3
E : Type u_2
F : Type ?u.57939
ι : Type u_1
ι' : Type ?u.57945
α : Type ?u.57948
inst✝⁷ : LinearOrderedField R
inst✝⁶ : AddCommGroup E
inst✝⁵ : AddCommGroup F
inst✝⁴ : LinearOrderedAddCommGroup α
inst✝³ : Module R E
inst✝² : Module R F
inst✝¹ : Module R α
inst✝ : OrderedSMul R α
s : Set E
i j : ι
c : R
t : Finset ι
w : ι → R
z : ι → E
hi : i ∈ t
⊢ ∑ i_1 in t, (if i = i_1 then 1 else 0) • z i_1 = z i

case hw
R : Type u_3
E : Type u_2
F : Type ?u.57939
ι : Type u_1
ι' : Type ?u.57945
α : Type ?u.57948
inst✝⁷ : LinearOrderedField R
inst✝⁶ : AddCommGroup E
inst✝⁵ : AddCommGroup F
inst✝⁴ : LinearOrderedAddCommGroup α
inst✝³ : Module R E
inst✝² : Module R F
inst✝¹ : Module R α
inst✝ : OrderedSMul R α
s : Set E
i j : ι
c : R
t : Finset ι
w : ι → R
z : ι → E
hi : i ∈ t
⊢ (∑ i_1 in t, if i = i_1 then 1 else 0) = 1
R : Type u_3
E : Type u_2
F : Type ?u.57939
ι : Type u_1
ι' : Type ?u.57945
α : Type ?u.57948
inst✝⁷ : LinearOrderedField R
inst✝⁶ : AddCommGroup E
inst✝⁵ : AddCommGroup F
inst✝⁴ : LinearOrderedAddCommGroup α
inst✝³ : Module R E
inst✝² : Module R F
inst✝¹ : Module R α
inst✝ : OrderedSMul R α
s : Set E
i j : ι
c : R
t : Finset ι
w : ι → R
z : ι → E
hi : i ∈ t
⊢ centerMass t (fun j => if i = j then 1 else 0) z = z i
rw [Finset.centerMass_eq_of_sum_1]
R : Type u_3
E : Type u_2
F : Type ?u.57939
ι : Type u_1
ι' : Type ?u.57945
α : Type ?u.57948
inst✝⁷ : LinearOrderedField R
inst✝⁶ : AddCommGroup E
inst✝⁵ : AddCommGroup F
inst✝⁴ : LinearOrderedAddCommGroup α
inst✝³ : Module R E
inst✝² : Module R F
inst✝¹ : Module R α
inst✝ : OrderedSMul R α
s : Set E
i j : ι
c : R
t : Finset ι
w : ι → R
z : ι → E
hi : i ∈ t
⊢ ∑ i_1 in t, (if i = i_1 then 1 else 0) • z i_1 = ∑ j in t, if i = j then z i else 0

R : Type u_3
E : Type u_2
F : Type ?u.57939
ι : Type u_1
ι' : Type ?u.57945
α : Type ?u.57948
inst✝⁷ : LinearOrderedField R
inst✝⁶ : AddCommGroup E
inst✝⁵ : AddCommGroup F
inst✝⁴ : LinearOrderedAddCommGroup α
inst✝³ : Module R E
inst✝² : Module R F
inst✝¹ : Module R α
inst✝ : OrderedSMul R α
s : Set E
i j : ι
c : R
t : Finset ι
w : ι → R
z : ι → E
hi : i ∈ t
⊢ (∑ j in t, if i = j then z i else 0) = z i

case hw
R : Type u_3
E : Type u_2
F : Type ?u.57939
ι : Type u_1
ι' : Type ?u.57945
α : Type ?u.57948
inst✝⁷ : LinearOrderedField R
inst✝⁶ : AddCommGroup E
inst✝⁵ : AddCommGroup F
inst✝⁴ : LinearOrderedAddCommGroup α
inst✝³ : Module R E
inst✝² : Module R F
inst✝¹ : Module R α
inst✝ : OrderedSMul R α
s : Set E
i j : ι
c : R
t : Finset ι
w : ι → R
z : ι → E
hi : i ∈ t
⊢ (∑ i_1 in t, if i = i_1 then 1 else 0) = 1
R : Type u_3
E : Type u_2
F : Type ?u.57939
ι : Type u_1
ι' : Type ?u.57945
α : Type ?u.57948
inst✝⁷ : LinearOrderedField R
inst✝⁶ : AddCommGroup E
inst✝⁵ : AddCommGroup F
inst✝⁴ : LinearOrderedAddCommGroup α
inst✝³ : Module R E
inst✝² : Module R F
inst✝¹ : Module R α
inst✝ : OrderedSMul R α
s : Set E
i j : ι
c : R
t : Finset ι
w : ι → R
z : ι → E
hi : i ∈ t
⊢ ∑ i_1 in t, (if i = i_1 then 1 else 0) • z i_1 = z i

case hw
R : Type u_3
E : Type u_2
F : Type ?u.57939
ι : Type u_1
ι' : Type ?u.57945
α : Type ?u.57948
inst✝⁷ : LinearOrderedField R
inst✝⁶ : AddCommGroup E
inst✝⁵ : AddCommGroup F
inst✝⁴ : LinearOrderedAddCommGroup α
inst✝³ : Module R E
inst✝² : Module R F
inst✝¹ : Module R α
inst✝ : OrderedSMul R α
s : Set E
i j : ι
c : R
t : Finset ι
w : ι → R
z : ι → E
hi : i ∈ t
⊢ (∑ i_1 in t, if i = i_1 then 1 else 0) = 1
trans ∑ j in t, if i = j then z i else 0
case e_f.h
R : Type u_3
E : Type u_2
F : Type ?u.57939
ι : Type u_1
ι' : Type ?u.57945
α : Type ?u.57948
inst✝⁷ : LinearOrderedField R
inst✝⁶ : AddCommGroup E
inst✝⁵ : AddCommGroup F
inst✝⁴ : LinearOrderedAddCommGroup α
inst✝³ : Module R E
inst✝² : Module R F
inst✝¹ : Module R α
inst✝ : OrderedSMul R α
s : Set E
i✝ j : ι
c : R
t : Finset ι
w : ι → R
z : ι → E
hi : i✝ ∈ t
i : ι
⊢ (if i✝ = i then 1 else 0) • z i = if i✝ = i then z i✝ else 0
R : Type u_3
E : Type u_2
F : Type ?u.57939
ι : Type u_1
ι' : Type ?u.57945
α : Type ?u.57948
inst✝⁷ : LinearOrderedField R
inst✝⁶ : AddCommGroup E
inst✝⁵ : AddCommGroup F
inst✝⁴ : LinearOrderedAddCommGroup α
inst✝³ : Module R E
inst✝² : Module R F
inst✝¹ : Module R α
inst✝ : OrderedSMul R α
s : Set E
i j : ι
c : R
t : Finset ι
w : ι → R
z : ι → E
hi : i ∈ t
⊢ ∑ i_1 in t, (if i = i_1 then 1 else 0) • z i_1 = ∑ j in t, if i = j then z i else 0
congr with i
case e_f.h.inl
R : Type u_3
E : Type u_2
F : Type ?u.57939
ι : Type u_1
ι' : Type ?u.57945
α : Type ?u.57948
inst✝⁷ : LinearOrderedField R
inst✝⁶ : AddCommGroup E
inst✝⁵ : AddCommGroup F
inst✝⁴ : LinearOrderedAddCommGroup α
inst✝³ : Module R E
inst✝² : Module R F
inst✝¹ : Module R α
inst✝ : OrderedSMul R α
s : Set E
i✝ j : ι
c : R
t : Finset ι
w : ι → R
z : ι → E
hi : i✝ ∈ t
i : ι
h : i✝ = i
⊢ 1 • z i = z i✝

case e_f.h.inr
R : Type u_3
E : Type u_2
F : Type ?u.57939
ι : Type u_1
ι' : Type ?u.57945
α : Type ?u.57948
inst✝⁷ : LinearOrderedField R
inst✝⁶ : AddCommGroup E
inst✝⁵ : AddCommGroup F
inst✝⁴ : LinearOrderedAddCommGroup α
inst✝³ : Module R E
inst✝² : Module R F
inst✝¹ : Module R α
inst✝ : OrderedSMul R α
s : Set E
i✝ j : ι
c : R
t : Finset ι
w : ι → R
z : ι → E
hi : i✝ ∈ t
i : ι
h : ¬i✝ = i
⊢ 0 • z i = 0
case e_f.h
R : Type u_3
E : Type u_2
F : Type ?u.57939
ι : Type u_1
ι' : Type ?u.57945
α : Type ?u.57948
inst✝⁷ : LinearOrderedField R
inst✝⁶ : AddCommGroup E
inst✝⁵ : AddCommGroup F
inst✝⁴ : LinearOrderedAddCommGroup α
inst✝³ : Module R E
inst✝² : Module R F
inst✝¹ : Module R α
inst✝ : OrderedSMul R α
s : Set E
i✝ j : ι
c : R
t : Finset ι
w : ι → R
z : ι → E
hi : i✝ ∈ t
i : ι
⊢ (if i✝ = i then 1 else 0) • z i = if i✝ = i then z i✝ else 0
split_ifs with h
no goals
case e_f.h.inl
R : Type u_3
E : Type u_2
F : Type ?u.57939
ι : Type u_1
ι' : Type ?u.57945
α : Type ?u.57948
inst✝⁷ : LinearOrderedField R
inst✝⁶ : AddCommGroup E
inst✝⁵ : AddCommGroup F
inst✝⁴ : LinearOrderedAddCommGroup α
inst✝³ : Module R E
inst✝² : Module R F
inst✝¹ : Module R α
inst✝ : OrderedSMul R α
s : Set E
i✝ j : ι
c : R
t : Finset ι
w : ι → R
z : ι → E
hi : i✝ ∈ t
i : ι
h : i✝ = i
⊢ 1 • z i = z i✝

case e_f.h.inr
R : Type u_3
E : Type u_2
F : Type ?u.57939
ι : Type u_1
ι' : Type ?u.57945
α : Type ?u.57948
inst✝⁷ : LinearOrderedField R
inst✝⁶ : AddCommGroup E
inst✝⁵ : AddCommGroup F
inst✝⁴ : LinearOrderedAddCommGroup α
inst✝³ : Module R E
inst✝² : Module R F
inst✝¹ : Module R α
inst✝ : OrderedSMul R α
s : Set E
i✝ j : ι
c : R
t : Finset ι
w : ι → R
z : ι → E
hi : i✝ ∈ t
i : ι
h : ¬i✝ = i
⊢ 0 • z i = 0
exacts [h ▸ one_smul _ _, zero_smul _ _]
no goals
R : Type u_3
E : Type u_2
F : Type ?u.57939
ι : Type u_1
ι' : Type ?u.57945
α : Type ?u.57948
inst✝⁷ : LinearOrderedField R
inst✝⁶ : AddCommGroup E
inst✝⁵ : AddCommGroup F
inst✝⁴ : LinearOrderedAddCommGroup α
inst✝³ : Module R E
inst✝² : Module R F
inst✝¹ : Module R α
inst✝ : OrderedSMul R α
s : Set E
i j : ι
c : R
t : Finset ι
w : ι → R
z : ι → E
hi : i ∈ t
⊢ (∑ j in t, if i = j then z i else 0) = z i
rw [sum_ite_eq, if_pos hi]
no goals
case hw
R : Type u_3
E : Type u_2
F : Type ?u.57939
ι : Type u_1
ι' : Type ?u.57945
α : Type ?u.57948
inst✝⁷ : LinearOrderedField R
inst✝⁶ : AddCommGroup E
inst✝⁵ : AddCommGroup F
inst✝⁴ : LinearOrderedAddCommGroup α
inst✝³ : Module R E
inst✝² : Module R F
inst✝¹ : Module R α
inst✝ : OrderedSMul R α
s : Set E
i j : ι
c : R
t : Finset ι
w : ι → R
z : ι → E
hi : i ∈ t
⊢ (∑ i_1 in t, if i = i_1 then 1 else 0) = 1
rw [sum_ite_eq, if_pos hi]