-- Mathlib/Analysis/Convex/Combination.lean
theorem Finset.centerMass_ite_eq (hi : i ∈ t) :
    t.centerMass (fun j => if i = j then (1 : R) else 0) z = z i

Proof state:
R : Type u_1
E : Type u_3
ι : Type u_5
inst✝² : LinearOrderedField R
inst✝¹ : AddCommGroup E
inst✝ : Module R E
i : ι
t : Finset ι
z : ι → E
hi : i ∈ t
⊢ t.centerMass (fun j => if i = j then 1 else 0) z = z i

Tactic:
rw [Finset.centerMass_eq_of_sum_1]

Result:
R : Type u_1
E : Type u_3
ι : Type u_5
inst✝² : LinearOrderedField R
inst✝¹ : AddCommGroup E
inst✝ : Module R E
i : ι
t : Finset ι
z : ι → E
hi : i ∈ t
⊢ ∑ i_1 ∈ t, (if i = i_1 then 1 else 0) • z i_1 = z i

case hw
R : Type u_1
E : Type u_3
ι : Type u_5
inst✝² : LinearOrderedField R
inst✝¹ : AddCommGroup E
inst✝ : Module R E
i : ι
t : Finset ι
z : ι → E
hi : i ∈ t
⊢ (∑ i_1 ∈ t, if i = i_1 then 1 else 0) = 1

Proof state:
R : Type u_1
E : Type u_3
ι : Type u_5
inst✝² : LinearOrderedField R
inst✝¹ : AddCommGroup E
inst✝ : Module R E
i : ι
t : Finset ι
z : ι → E
hi : i ∈ t
⊢ ∑ i_1 ∈ t, (if i = i_1 then 1 else 0) • z i_1 = z i

Tactic:
trans ∑ j ∈ t, if i = j then z i else 0

Result:
R : Type u_1
E : Type u_3
ι : Type u_5
inst✝² : LinearOrderedField R
inst✝¹ : AddCommGroup E
inst✝ : Module R E
i : ι
t : Finset ι
z : ι → E
hi : i ∈ t
⊢ ∑ i_1 ∈ t, (if i = i_1 then 1 else 0) • z i_1 = ∑ j ∈ t, if i = j then z i else 0

R : Type u_1
E : Type u_3
ι : Type u_5
inst✝² : LinearOrderedField R
inst✝¹ : AddCommGroup E
inst✝ : Module R E
i : ι
t : Finset ι
z : ι → E
hi : i ∈ t
⊢ (∑ j ∈ t, if i = j then z i else 0) = z i

Proof state:
case hw
R : Type u_1
E : Type u_3
ι : Type u_5
inst✝² : LinearOrderedField R
inst✝¹ : AddCommGroup E
inst✝ : Module R E
i : ι
t : Finset ι
z : ι → E
hi : i ∈ t
⊢ (∑ i_1 ∈ t, if i = i_1 then 1 else 0) = 1

Tactic:
rw [sum_ite_eq, if_pos hi]

Result:
no goals

Proof state:
R : Type u_1
E : Type u_3
ι : Type u_5
inst✝² : LinearOrderedField R
inst✝¹ : AddCommGroup E
inst✝ : Module R E
i : ι
t : Finset ι
z : ι → E
hi : i ∈ t
⊢ (∑ j ∈ t, if i = j then z i else 0) = z i

Tactic:
rw [sum_ite_eq, if_pos hi]

Result:
no goals

Proof state:
case pos
R : Type u_1
E : Type u_3
ι : Type u_5
inst✝² : LinearOrderedField R
inst✝¹ : AddCommGroup E
inst✝ : Module R E
i✝ : ι
t : Finset ι
z : ι → E
hi : i✝ ∈ t
i : ι
h : i✝ = i
⊢ 1 • z i = z i✝

case neg
R : Type u_1
E : Type u_3
ι : Type u_5
inst✝² : LinearOrderedField R
inst✝¹ : AddCommGroup E
inst✝ : Module R E
i✝ : ι
t : Finset ι
z : ι → E
hi : i✝ ∈ t
i : ι
h : ¬i✝ = i
⊢ 0 • z i = 0

Tactic:
exacts [h ▸ one_smul _ _, zero_smul _ _]

Result:
no goals

Proof state:
R : Type u_1
E : Type u_3
ι : Type u_5
inst✝² : LinearOrderedField R
inst✝¹ : AddCommGroup E
inst✝ : Module R E
i : ι
t : Finset ι
z : ι → E
hi : i ∈ t
⊢ ∑ i_1 ∈ t, (if i = i_1 then 1 else 0) • z i_1 = ∑ j ∈ t, if i = j then z i else 0

Tactic:
congr with i

Result:
case e_f.h
R : Type u_1
E : Type u_3
ι : Type u_5
inst✝² : LinearOrderedField R
inst✝¹ : AddCommGroup E
inst✝ : Module R E
i✝ : ι
t : Finset ι
z : ι → E
hi : i✝ ∈ t
i : ι
⊢ (if i✝ = i then 1 else 0) • z i = if i✝ = i then z i✝ else 0

Proof state:
case e_f.h
R : Type u_1
E : Type u_3
ι : Type u_5
inst✝² : LinearOrderedField R
inst✝¹ : AddCommGroup E
inst✝ : Module R E
i✝ : ι
t : Finset ι
z : ι → E
hi : i✝ ∈ t
i : ι
⊢ (if i✝ = i then 1 else 0) • z i = if i✝ = i then z i✝ else 0

Tactic:
split_ifs with h

Result:
case pos
R : Type u_1
E : Type u_3
ι : Type u_5
inst✝² : LinearOrderedField R
inst✝¹ : AddCommGroup E
inst✝ : Module R E
i✝ : ι
t : Finset ι
z : ι → E
hi : i✝ ∈ t
i : ι
h : i✝ = i
⊢ 1 • z i = z i✝

case neg
R : Type u_1
E : Type u_3
ι : Type u_5
inst✝² : LinearOrderedField R
inst✝¹ : AddCommGroup E
inst✝ : Module R E
i✝ : ι
t : Finset ι
z : ι → E
hi : i✝ ∈ t
i : ι
h : ¬i✝ = i
⊢ 0 • z i = 0