Theorem: SciLean.IsContinuousLinearMap.pi_rule (SciLean/Core/FunctionPropositions/IsContinuousLinearMap.lean)

State before:
R✝ : Type ?u.44507
inst✝²⁰ : Semiring R✝
X✝ : Type ?u.44513
inst✝¹⁹ : TopologicalSpace X✝
inst✝¹⁸ : AddCommMonoid X✝
inst✝¹⁷ : Module R✝ X✝
Y✝ : Type ?u.44547
inst✝¹⁶ : TopologicalSpace Y✝
inst✝¹⁵ : AddCommMonoid Y✝
inst✝¹⁴ : Module R✝ Y✝
R : Type u_1
inst✝¹³ : Semiring R
X : Type u_2
inst✝¹² : TopologicalSpace X
inst✝¹¹ : AddCommMonoid X
inst✝¹⁰ : Module R X
Y : Type ?u.44619
inst✝⁹ : TopologicalSpace Y
inst✝⁸ : AddCommMonoid Y
inst✝⁷ : Module R Y
Z : Type ?u.44651
inst✝⁶ : TopologicalSpace Z
inst✝⁵ : AddCommMonoid Z
inst✝⁴ : Module R Z
ι : Type u_4
inst✝³ : Fintype ι
E : ι → Type u_3
inst✝² : (i : ι) → TopologicalSpace (E i)
inst✝¹ : (i : ι) → AddCommMonoid (E i)
inst✝ : (i : ι) → Module R (E i)
f : X → (i : ι) → E i
hf : ∀ (i : ι), IsContinuousLinearMap R fun x => f x i
⊢ ∀ (x : X), (fun i => f x i) = (ContinuousLinearMap.pi fun i => fun x =>L[R] f x i) x
Tactic:
simp
State after:
no goals