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

State before:
R✝ : Type ?u.20619
inst✝²⁰ : Semiring R✝
X✝ : Type ?u.20625
inst✝¹⁹ : TopologicalSpace X✝
inst✝¹⁸ : AddCommMonoid X✝
inst✝¹⁷ : Module R✝ X✝
Y✝ : Type ?u.20659
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_3
inst✝⁹ : TopologicalSpace Y
inst✝⁸ : AddCommMonoid Y
inst✝⁷ : Module R Y
Z : Type ?u.20763
inst✝⁶ : TopologicalSpace Z
inst✝⁵ : AddCommMonoid Z
inst✝⁴ : Module R Z
ι : Type ?u.20795
inst✝³ : Fintype ι
E : ι → Type ?u.20803
inst✝² : (i : ι) → TopologicalSpace (E i)
inst✝¹ : (i : ι) → AddCommMonoid (E i)
inst✝ : (i : ι) → Module R (E i)
⊢ ∀ (x : X), 0 = 0 x
Tactic:
simp
State after:
no goals