Module: Mathlib.Analysis.Normed.Module.Multilinear.Basic

Goal state before:
pp: case e'_2
𝕜 : Type u
ι : Type v
ι' : Type v'
E : ι → Type wE
E₁ : ι → Type wE₁
E' : ι' → Type wE'
G : Type wG
G' : Type wG'
inst✝¹¹ : Fintype ι'
inst✝¹⁰ : NontriviallyNormedField 𝕜
inst✝⁹ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝⁸ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝⁷ : (i : ι) → SeminormedAddCommGroup (E₁ i)
inst✝⁶ : (i : ι) → NormedSpace 𝕜 (E₁ i)
inst✝⁵ : SeminormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : SeminormedAddCommGroup G'
inst✝² : NormedSpace 𝕜 G'
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
f : (i : ι) → E i →L[𝕜] E₁ i
i : ι
f₁ f₂ : E i →L[𝕜] E₁ i
g : ContinuousMultilinearMap 𝕜 E₁ G
x : (i : ι) → E i
x✝ : ι
⊢ (update f i (f₁ + f₂) x✝) (x x✝) = update (fun j ↦ (f j) (x j)) i (f₁ (x i) + f₂ (x i)) x✝

pp: case e'_3.e'_5
𝕜 : Type u
ι : Type v
ι' : Type v'
E : ι → Type wE
E₁ : ι → Type wE₁
E' : ι' → Type wE'
G : Type wG
G' : Type wG'
inst✝¹¹ : Fintype ι'
inst✝¹⁰ : NontriviallyNormedField 𝕜
inst✝⁹ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝⁸ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝⁷ : (i : ι) → SeminormedAddCommGroup (E₁ i)
inst✝⁶ : (i : ι) → NormedSpace 𝕜 (E₁ i)
inst✝⁵ : SeminormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : SeminormedAddCommGroup G'
inst✝² : NormedSpace 𝕜 G'
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
f : (i : ι) → E i →L[𝕜] E₁ i
i : ι
f₁ f₂ : E i →L[𝕜] E₁ i
g : ContinuousMultilinearMap 𝕜 E₁ G
x : (i : ι) → E i
x✝ : ι
⊢ (update f i f₁ x✝) (x x✝) = update (fun j ↦ (f j) (x j)) i (f₁ (x i)) x✝

pp: case e'_3.e'_6
𝕜 : Type u
ι : Type v
ι' : Type v'
E : ι → Type wE
E₁ : ι → Type wE₁
E' : ι' → Type wE'
G : Type wG
G' : Type wG'
inst✝¹¹ : Fintype ι'
inst✝¹⁰ : NontriviallyNormedField 𝕜
inst✝⁹ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝⁸ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝⁷ : (i : ι) → SeminormedAddCommGroup (E₁ i)
inst✝⁶ : (i : ι) → NormedSpace 𝕜 (E₁ i)
inst✝⁵ : SeminormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : SeminormedAddCommGroup G'
inst✝² : NormedSpace 𝕜 G'
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
f : (i : ι) → E i →L[𝕜] E₁ i
i : ι
f₁ f₂ : E i →L[𝕜] E₁ i
g : ContinuousMultilinearMap 𝕜 E₁ G
x : (i : ι) → E i
x✝ : ι
⊢ (update f i f₂ x✝) (x x✝) = update (fun j ↦ (f j) (x j)) i (f₂ (x i)) x✝

Tactic:
<;>

Goal state after:
case e'_2
𝕜 : Type u
ι : Type v
ι' : Type v'
E : ι → Type wE
E₁ : ι → Type wE₁
E' : ι' → Type wE'
G : Type wG
G' : Type wG'
inst✝¹¹ : Fintype ι'
inst✝¹⁰ : NontriviallyNormedField 𝕜
inst✝⁹ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝⁸ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝⁷ : (i : ι) → SeminormedAddCommGroup (E₁ i)
inst✝⁶ : (i : ι) → NormedSpace 𝕜 (E₁ i)
inst✝⁵ : SeminormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : SeminormedAddCommGroup G'
inst✝² : NormedSpace 𝕜 G'
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
f : (i : ι) → E i →L[𝕜] E₁ i
i : ι
f₁ f₂ : E i →L[𝕜] E₁ i
g : ContinuousMultilinearMap 𝕜 E₁ G
x : (i : ι) → E i
x✝ : ι
⊢ (update f i (f₁ + f₂) x✝) (x x✝) = update (fun j ↦ (f j) (x j)) i (f₁ (x i) + f₂ (x i)) x✝

case e'_3.e'_5
𝕜 : Type u
ι : Type v
ι' : Type v'
E : ι → Type wE
E₁ : ι → Type wE₁
E' : ι' → Type wE'
G : Type wG
G' : Type wG'
inst✝¹¹ : Fintype ι'
inst✝¹⁰ : NontriviallyNormedField 𝕜
inst✝⁹ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝⁸ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝⁷ : (i : ι) → SeminormedAddCommGroup (E₁ i)
inst✝⁶ : (i : ι) → NormedSpace 𝕜 (E₁ i)
inst✝⁵ : SeminormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : SeminormedAddCommGroup G'
inst✝² : NormedSpace 𝕜 G'
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
f : (i : ι) → E i →L[𝕜] E₁ i
i : ι
f₁ f₂ : E i →L[𝕜] E₁ i
g : ContinuousMultilinearMap 𝕜 E₁ G
x : (i : ι) → E i
x✝ : ι
⊢ (update f i f₁ x✝) (x x✝) = update (fun j ↦ (f j) (x j)) i (f₁ (x i)) x✝

case e'_3.e'_6
𝕜 : Type u
ι : Type v
ι' : Type v'
E : ι → Type wE
E₁ : ι → Type wE₁
E' : ι' → Type wE'
G : Type wG
G' : Type wG'
inst✝¹¹ : Fintype ι'
inst✝¹⁰ : NontriviallyNormedField 𝕜
inst✝⁹ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝⁸ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝⁷ : (i : ι) → SeminormedAddCommGroup (E₁ i)
inst✝⁶ : (i : ι) → NormedSpace 𝕜 (E₁ i)
inst✝⁵ : SeminormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : SeminormedAddCommGroup G'
inst✝² : NormedSpace 𝕜 G'
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
f : (i : ι) → E i →L[𝕜] E₁ i
i : ι
f₁ f₂ : E i →L[𝕜] E₁ i
g : ContinuousMultilinearMap 𝕜 E₁ G
x : (i : ι) → E i
x✝ : ι
⊢ (update f i f₂ x✝) (x x✝) = update (fun j ↦ (f j) (x j)) i (f₂ (x i)) x✝