Theorem: Function.update_eq_add_sum_filter_single (ForML/ContinuousLinearMapCo.lean)

State before:
ι : Type u_1
R : Type u_2
inst✝¹⁰ : Fintype ι
inst✝⁹ : DecidableEq ι
inst✝⁸ : NontriviallyNormedField R
M₁ : Type u_3
M₂ : Type u_4
inst✝⁷ : NormedAddCommGroup M₁
inst✝⁶ : NormedSpace R M₁
inst✝⁵ : NormedAddCommGroup M₂
inst✝⁴ : NormedSpace R M₂
M : ι → Type u_5
inst✝³ : (i : ι) → NormedAddCommGroup (M i)
inst✝² : (i : ι) → NormedSpace R (M i)
F : Type u_6
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace R F
i : ι
x : (i : ι) → M i
xi : M i
⊢ update x i xi = Pi.single i xi + ∑ k in Finset.filter (fun k => k ≠ i) Finset.univ, Pi.single k (x k)
Tactic:
ext j
State after:
case h
ι : Type u_1
R : Type u_2
inst✝¹⁰ : Fintype ι
inst✝⁹ : DecidableEq ι
inst✝⁸ : NontriviallyNormedField R
M₁ : Type u_3
M₂ : Type u_4
inst✝⁷ : NormedAddCommGroup M₁
inst✝⁶ : NormedSpace R M₁
inst✝⁵ : NormedAddCommGroup M₂
inst✝⁴ : NormedSpace R M₂
M : ι → Type u_5
inst✝³ : (i : ι) → NormedAddCommGroup (M i)
inst✝² : (i : ι) → NormedSpace R (M i)
F : Type u_6
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace R F
i : ι
x : (i : ι) → M i
xi : M i
j : ι
⊢ update x i xi j = (Pi.single i xi + ∑ k in Finset.filter (fun k => k ≠ i) Finset.univ, Pi.single k (x k)) j

State before:
case h
ι : Type u_1
R : Type u_2
inst✝¹⁰ : Fintype ι
inst✝⁹ : DecidableEq ι
inst✝⁸ : NontriviallyNormedField R
M₁ : Type u_3
M₂ : Type u_4
inst✝⁷ : NormedAddCommGroup M₁
inst✝⁶ : NormedSpace R M₁
inst✝⁵ : NormedAddCommGroup M₂
inst✝⁴ : NormedSpace R M₂
M : ι → Type u_5
inst✝³ : (i : ι) → NormedAddCommGroup (M i)
inst✝² : (i : ι) → NormedSpace R (M i)
F : Type u_6
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace R F
i : ι
x : (i : ι) → M i
xi : M i
j : ι
⊢ update x i xi j = (Pi.single i xi + ∑ k in Finset.filter (fun k => k ≠ i) Finset.univ, Pi.single k (x k)) j
Tactic:
simp
State after:
case h
ι : Type u_1
R : Type u_2
inst✝¹⁰ : Fintype ι
inst✝⁹ : DecidableEq ι
inst✝⁸ : NontriviallyNormedField R
M₁ : Type u_3
M₂ : Type u_4
inst✝⁷ : NormedAddCommGroup M₁
inst✝⁶ : NormedSpace R M₁
inst✝⁵ : NormedAddCommGroup M₂
inst✝⁴ : NormedSpace R M₂
M : ι → Type u_5
inst✝³ : (i : ι) → NormedAddCommGroup (M i)
inst✝² : (i : ι) → NormedSpace R (M i)
F : Type u_6
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace R F
i : ι
x : (i : ι) → M i
xi : M i
j : ι
⊢ update x i xi j = Pi.single i xi j + if j = i then 0 else x j

State before:
case h
ι : Type u_1
R : Type u_2
inst✝¹⁰ : Fintype ι
inst✝⁹ : DecidableEq ι
inst✝⁸ : NontriviallyNormedField R
M₁ : Type u_3
M₂ : Type u_4
inst✝⁷ : NormedAddCommGroup M₁
inst✝⁶ : NormedSpace R M₁
inst✝⁵ : NormedAddCommGroup M₂
inst✝⁴ : NormedSpace R M₂
M : ι → Type u_5
inst✝³ : (i : ι) → NormedAddCommGroup (M i)
inst✝² : (i : ι) → NormedSpace R (M i)
F : Type u_6
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace R F
i : ι
x : (i : ι) → M i
xi : M i
j : ι
⊢ update x i xi j = Pi.single i xi j + if j = i then 0 else x j
Tactic:
by_cases h : j = i <;> simp [h]
State after:
case pos
ι : Type u_1
R : Type u_2
inst✝¹⁰ : Fintype ι
inst✝⁹ : DecidableEq ι
inst✝⁸ : NontriviallyNormedField R
M₁ : Type u_3
M₂ : Type u_4
inst✝⁷ : NormedAddCommGroup M₁
inst✝⁶ : NormedSpace R M₁
inst✝⁵ : NormedAddCommGroup M₂
inst✝⁴ : NormedSpace R M₂
M : ι → Type u_5
inst✝³ : (i : ι) → NormedAddCommGroup (M i)
inst✝² : (i : ι) → NormedSpace R (M i)
F : Type u_6
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace R F
i : ι
x : (i : ι) → M i
xi : M i
j : ι
h : j = i
⊢ update x i xi j = Pi.single i xi j

State before:
case pos
ι : Type u_1
R : Type u_2
inst✝¹⁰ : Fintype ι
inst✝⁹ : DecidableEq ι
inst✝⁸ : NontriviallyNormedField R
M₁ : Type u_3
M₂ : Type u_4
inst✝⁷ : NormedAddCommGroup M₁
inst✝⁶ : NormedSpace R M₁
inst✝⁵ : NormedAddCommGroup M₂
inst✝⁴ : NormedSpace R M₂
M : ι → Type u_5
inst✝³ : (i : ι) → NormedAddCommGroup (M i)
inst✝² : (i : ι) → NormedSpace R (M i)
F : Type u_6
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace R F
i : ι
x : (i : ι) → M i
xi : M i
j : ι
h : j = i
⊢ update x i xi j = Pi.single i xi j
Tactic:
rw [Pi.single]
State after:
case pos
ι : Type u_1
R : Type u_2
inst✝¹⁰ : Fintype ι
inst✝⁹ : DecidableEq ι
inst✝⁸ : NontriviallyNormedField R
M₁ : Type u_3
M₂ : Type u_4
inst✝⁷ : NormedAddCommGroup M₁
inst✝⁶ : NormedSpace R M₁
inst✝⁵ : NormedAddCommGroup M₂
inst✝⁴ : NormedSpace R M₂
M : ι → Type u_5
inst✝³ : (i : ι) → NormedAddCommGroup (M i)
inst✝² : (i : ι) → NormedSpace R (M i)
F : Type u_6
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace R F
i : ι
x : (i : ι) → M i
xi : M i
j : ι
h : j = i
⊢ update x i xi j = update 0 i xi j

State before:
case pos
ι : Type u_1
R : Type u_2
inst✝¹⁰ : Fintype ι
inst✝⁹ : DecidableEq ι
inst✝⁸ : NontriviallyNormedField R
M₁ : Type u_3
M₂ : Type u_4
inst✝⁷ : NormedAddCommGroup M₁
inst✝⁶ : NormedSpace R M₁
inst✝⁵ : NormedAddCommGroup M₂
inst✝⁴ : NormedSpace R M₂
M : ι → Type u_5
inst✝³ : (i : ι) → NormedAddCommGroup (M i)
inst✝² : (i : ι) → NormedSpace R (M i)
F : Type u_6
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace R F
i : ι
x : (i : ι) → M i
xi : M i
j : ι
h : j = i
⊢ update x i xi j = update 0 i xi j
Tactic:
simp [update, h]
State after:
no goals