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

State before:
R✝ : Type ?u.33859
inst✝²⁰ : Semiring R✝
X✝ : Type ?u.33865
inst✝¹⁹ : TopologicalSpace X✝
inst✝¹⁸ : AddCommMonoid X✝
inst✝¹⁷ : Module R✝ X✝
Y✝ : Type ?u.33899
inst✝¹⁶ : TopologicalSpace Y✝
inst✝¹⁵ : AddCommMonoid Y✝
inst✝¹⁴ : Module R✝ Y✝
R : Type u_1
inst✝¹³ : Semiring R
X : Type ?u.33937
inst✝¹² : TopologicalSpace X
inst✝¹¹ : AddCommMonoid X
inst✝¹⁰ : Module R X
Y : Type ?u.33971
inst✝⁹ : TopologicalSpace Y
inst✝⁸ : AddCommMonoid Y
inst✝⁷ : Module R Y
Z : Type ?u.34003
inst✝⁶ : TopologicalSpace Z
inst✝⁵ : AddCommMonoid Z
inst✝⁴ : Module R Z
ι : Type u_2
inst✝³ : Fintype ι
E : ι → Type u_3
inst✝² : (i : ι) → TopologicalSpace (E i)
inst✝¹ : (i : ι) → AddCommMonoid (E i)
inst✝ : (i : ι) → Module R (E i)
i : ι
⊢ ∀ (x : (i : ι) → E i), x i = (ContinuousLinearMap.proj i) x
Tactic:
simp
State after:
no goals