-- Mathlib/Analysis/NormedSpace/PiTensorProduct/InjectiveSeminorm.lean
theorem mapL_add_smul_aux {ι : Type uι}
    {E : ι → Type uE} [(i : ι) → SeminormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)]
    {E' : ι → Type u_1} [(i : ι) → SeminormedAddCommGroup (E' i)] [(i : ι) → NormedSpace 𝕜 (E' i)]
    (f : (i : ι) → E i →L[𝕜] E' i)
    [DecidableEq ι] (i : ι) (u : E i →L[𝕜] E' i) :
    (fun j ↦ (update f i u j).toLinearMap) =
      update (fun j ↦ (f j).toLinearMap) i u.toLinearMap

Proof state:
𝕜 : Type u𝕜
inst✝⁵ : NontriviallyNormedField 𝕜
ι : Type uι
E : ι → Type uE
inst✝⁴ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝³ : (i : ι) → NormedSpace 𝕜 (E i)
E' : ι → Type u_1
inst✝² : (i : ι) → SeminormedAddCommGroup (E' i)
inst✝¹ : (i : ι) → NormedSpace 𝕜 (E' i)
f : (i : ι) → E i →L[𝕜] E' i
inst✝ : DecidableEq ι
i : ι
u : E i →L[𝕜] E' i
⊢ (fun j => ↑(update f i u j)) = update (fun j => ↑(f j)) i ↑u

Tactic:
symm

Result:
𝕜 : Type u𝕜
inst✝⁵ : NontriviallyNormedField 𝕜
ι : Type uι
E : ι → Type uE
inst✝⁴ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝³ : (i : ι) → NormedSpace 𝕜 (E i)
E' : ι → Type u_1
inst✝² : (i : ι) → SeminormedAddCommGroup (E' i)
inst✝¹ : (i : ι) → NormedSpace 𝕜 (E' i)
f : (i : ι) → E i →L[𝕜] E' i
inst✝ : DecidableEq ι
i : ι
u : E i →L[𝕜] E' i
⊢ update (fun j => ↑(f j)) i ↑u = fun j => ↑(update f i u j)

Proof state:
case right
𝕜 : Type u𝕜
inst✝⁵ : NontriviallyNormedField 𝕜
ι : Type uι
E : ι → Type uE
inst✝⁴ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝³ : (i : ι) → NormedSpace 𝕜 (E i)
E' : ι → Type u_1
inst✝² : (i : ι) → SeminormedAddCommGroup (E' i)
inst✝¹ : (i : ι) → NormedSpace 𝕜 (E' i)
f : (i : ι) → E i →L[𝕜] E' i
inst✝ : DecidableEq ι
i : ι
u : E i →L[𝕜] E' i
⊢ ∀ (x : ι), x ≠ i → ↑(f x) = ↑(update f i u x)

Tactic:
exact fun _ h ↦ by simp only [ne_eq, h, not_false_eq_true, update_of_ne]

Result:
no goals

Proof state:
𝕜 : Type u𝕜
inst✝⁵ : NontriviallyNormedField 𝕜
ι : Type uι
E : ι → Type uE
inst✝⁴ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝³ : (i : ι) → NormedSpace 𝕜 (E i)
E' : ι → Type u_1
inst✝² : (i : ι) → SeminormedAddCommGroup (E' i)
inst✝¹ : (i : ι) → NormedSpace 𝕜 (E' i)
f : (i : ι) → E i →L[𝕜] E' i
inst✝ : DecidableEq ι
i : ι
u : E i →L[𝕜] E' i
⊢ update (fun j => ↑(f j)) i ↑u = fun j => ↑(update f i u j)

Tactic:
rw [update_eq_iff]

Result:
𝕜 : Type u𝕜
inst✝⁵ : NontriviallyNormedField 𝕜
ι : Type uι
E : ι → Type uE
inst✝⁴ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝³ : (i : ι) → NormedSpace 𝕜 (E i)
E' : ι → Type u_1
inst✝² : (i : ι) → SeminormedAddCommGroup (E' i)
inst✝¹ : (i : ι) → NormedSpace 𝕜 (E' i)
f : (i : ι) → E i →L[𝕜] E' i
inst✝ : DecidableEq ι
i : ι
u : E i →L[𝕜] E' i
⊢ ↑u = ↑(update f i u i) ∧ ∀ (x : ι), x ≠ i → ↑(f x) = ↑(update f i u x)

Proof state:
𝕜 : Type u𝕜
inst✝⁵ : NontriviallyNormedField 𝕜
ι : Type uι
E : ι → Type uE
inst✝⁴ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝³ : (i : ι) → NormedSpace 𝕜 (E i)
E' : ι → Type u_1
inst✝² : (i : ι) → SeminormedAddCommGroup (E' i)
inst✝¹ : (i : ι) → NormedSpace 𝕜 (E' i)
f : (i : ι) → E i →L[𝕜] E' i
inst✝ : DecidableEq ι
i : ι
u : E i →L[𝕜] E' i
x✝ : ι
h : x✝ ≠ i
⊢ ↑(f x✝) = ↑(update f i u x✝)

Tactic:
simp only [ne_eq, h, not_false_eq_true, update_of_ne]

Result:
no goals

Proof state:
case left
𝕜 : Type u𝕜
inst✝⁵ : NontriviallyNormedField 𝕜
ι : Type uι
E : ι → Type uE
inst✝⁴ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝³ : (i : ι) → NormedSpace 𝕜 (E i)
E' : ι → Type u_1
inst✝² : (i : ι) → SeminormedAddCommGroup (E' i)
inst✝¹ : (i : ι) → NormedSpace 𝕜 (E' i)
f : (i : ι) → E i →L[𝕜] E' i
inst✝ : DecidableEq ι
i : ι
u : E i →L[𝕜] E' i
⊢ ↑u = ↑(update f i u i)

Tactic:
simp only [update_self]

Result:
no goals

Proof state:
𝕜 : Type u𝕜
inst✝⁵ : NontriviallyNormedField 𝕜
ι : Type uι
E : ι → Type uE
inst✝⁴ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝³ : (i : ι) → NormedSpace 𝕜 (E i)
E' : ι → Type u_1
inst✝² : (i : ι) → SeminormedAddCommGroup (E' i)
inst✝¹ : (i : ι) → NormedSpace 𝕜 (E' i)
f : (i : ι) → E i →L[𝕜] E' i
inst✝ : DecidableEq ι
i : ι
u : E i →L[𝕜] E' i
⊢ ↑u = ↑(update f i u i) ∧ ∀ (x : ι), x ≠ i → ↑(f x) = ↑(update f i u x)

Tactic:
constructor

Result:
case left
𝕜 : Type u𝕜
inst✝⁵ : NontriviallyNormedField 𝕜
ι : Type uι
E : ι → Type uE
inst✝⁴ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝³ : (i : ι) → NormedSpace 𝕜 (E i)
E' : ι → Type u_1
inst✝² : (i : ι) → SeminormedAddCommGroup (E' i)
inst✝¹ : (i : ι) → NormedSpace 𝕜 (E' i)
f : (i : ι) → E i →L[𝕜] E' i
inst✝ : DecidableEq ι
i : ι
u : E i →L[𝕜] E' i
⊢ ↑u = ↑(update f i u i)

case right
𝕜 : Type u𝕜
inst✝⁵ : NontriviallyNormedField 𝕜
ι : Type uι
E : ι → Type uE
inst✝⁴ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝³ : (i : ι) → NormedSpace 𝕜 (E i)
E' : ι → Type u_1
inst✝² : (i : ι) → SeminormedAddCommGroup (E' i)
inst✝¹ : (i : ι) → NormedSpace 𝕜 (E' i)
f : (i : ι) → E i →L[𝕜] E' i
inst✝ : DecidableEq ι
i : ι
u : E i →L[𝕜] E' i
⊢ ∀ (x : ι), x ≠ i → ↑(f x) = ↑(update f i u x)