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

State before:
R✝ : Type ?u.16475
inst✝²⁰ : Semiring R✝
X✝ : Type ?u.16481
inst✝¹⁹ : TopologicalSpace X✝
inst✝¹⁸ : AddCommMonoid X✝
inst✝¹⁷ : Module R✝ X✝
Y✝ : Type ?u.16515
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.16587
inst✝⁹ : TopologicalSpace Y
inst✝⁸ : AddCommMonoid Y
inst✝⁷ : Module R Y
Z : Type ?u.16619
inst✝⁶ : TopologicalSpace Z
inst✝⁵ : AddCommMonoid Z
inst✝⁴ : Module R Z
ι : Type ?u.16651
inst✝³ : Fintype ι
E : ι → Type ?u.16659
inst✝² : (i : ι) → TopologicalSpace (E i)
inst✝¹ : (i : ι) → AddCommMonoid (E i)
inst✝ : (i : ι) → Module R (E i)
⊢ ∀ (x : X), x = (ContinuousLinearMap.id R X) x
Tactic:
simp
State after:
no goals