Theorem: ContinuousLinearMap.pi_apply' (ForML/ContinuousLinearMap.lean)

State before:
𝕜 : Type u_1
ι : Type u_2
inst✝¹⁰ : Fintype ι
inst✝⁹ : DecidableEq ι
M : Type u_3
inst✝⁸ : TopologicalSpace M
inst✝⁷ : AddCommGroup M
φ : ι → Type u_4
inst✝⁶ : (i : ι) → TopologicalSpace (φ i)
inst✝⁵ : (i : ι) → AddCommGroup (φ i)
inst✝⁴ : ∀ (i : ι), TopologicalAddGroup (φ i)
inst✝³ : NormedField 𝕜
inst✝² : Module 𝕜 M
inst✝¹ : (i : ι) → Module 𝕜 (φ i)
inst✝ : ∀ (i : ι), ContinuousConstSMul 𝕜 (φ i)
f : (i : ι) → M →L[𝕜] φ i
⊢ pi f = ∑ i : ι, comp (single i) (f i)
Tactic:
ext
State after:
case h.h
𝕜 : Type u_1
ι : Type u_2
inst✝¹⁰ : Fintype ι
inst✝⁹ : DecidableEq ι
M : Type u_3
inst✝⁸ : TopologicalSpace M
inst✝⁷ : AddCommGroup M
φ : ι → Type u_4
inst✝⁶ : (i : ι) → TopologicalSpace (φ i)
inst✝⁵ : (i : ι) → AddCommGroup (φ i)
inst✝⁴ : ∀ (i : ι), TopologicalAddGroup (φ i)
inst✝³ : NormedField 𝕜
inst✝² : Module 𝕜 M
inst✝¹ : (i : ι) → Module 𝕜 (φ i)
inst✝ : ∀ (i : ι), ContinuousConstSMul 𝕜 (φ i)
f : (i : ι) → M →L[𝕜] φ i
x✝¹ : M
x✝ : ι
⊢ (pi f) x✝¹ x✝ = (∑ i : ι, comp (single i) (f i)) x✝¹ x✝

State before:
case h.h
𝕜 : Type u_1
ι : Type u_2
inst✝¹⁰ : Fintype ι
inst✝⁹ : DecidableEq ι
M : Type u_3
inst✝⁸ : TopologicalSpace M
inst✝⁷ : AddCommGroup M
φ : ι → Type u_4
inst✝⁶ : (i : ι) → TopologicalSpace (φ i)
inst✝⁵ : (i : ι) → AddCommGroup (φ i)
inst✝⁴ : ∀ (i : ι), TopologicalAddGroup (φ i)
inst✝³ : NormedField 𝕜
inst✝² : Module 𝕜 M
inst✝¹ : (i : ι) → Module 𝕜 (φ i)
inst✝ : ∀ (i : ι), ContinuousConstSMul 𝕜 (φ i)
f : (i : ι) → M →L[𝕜] φ i
x✝¹ : M
x✝ : ι
⊢ (pi f) x✝¹ x✝ = (∑ i : ι, comp (single i) (f i)) x✝¹ x✝
Tactic:
simp
State after:
no goals