Theorem: SciLean.IsContinuousLinearMap.Neg.neg.arg_a0.IsContinuousLinearMap_rule (SciLean/Core/FunctionPropositions/IsContinuousLinearMap.lean)

State before:
R✝² : Type ?u.87232
inst✝⁴² : Semiring R✝²
X✝² : Type ?u.87238
inst✝⁴¹ : TopologicalSpace X✝²
inst✝⁴⁰ : AddCommMonoid X✝²
inst✝³⁹ : Module R✝² X✝²
Y✝² : Type ?u.87272
inst✝³⁸ : TopologicalSpace Y✝²
inst✝³⁷ : AddCommMonoid Y✝²
inst✝³⁶ : Module R✝² Y✝²
R✝¹ : Type ?u.87304
inst✝³⁵ : Semiring R✝¹
X✝¹ : Type ?u.87310
inst✝³⁴ : TopologicalSpace X✝¹
inst✝³³ : AddCommMonoid X✝¹
inst✝³² : Module R✝¹ X✝¹
Y✝¹ : Type ?u.87344
inst✝³¹ : TopologicalSpace Y✝¹
inst✝³⁰ : AddCommMonoid Y✝¹
inst✝²⁹ : Module R✝¹ Y✝¹
Z✝ : Type ?u.87376
inst✝²⁸ : TopologicalSpace Z✝
inst✝²⁷ : AddCommMonoid Z✝
inst✝²⁶ : Module R✝¹ Z✝
ι✝ : Type ?u.87408
inst✝²⁵ : Fintype ι✝
E✝ : ι✝ → Type ?u.87416
inst✝²⁴ : (i : ι✝) → TopologicalSpace (E✝ i)
inst✝²³ : (i : ι✝) → AddCommMonoid (E✝ i)
inst✝²² : (i : ι✝) → Module R✝¹ (E✝ i)
R✝ : Type ?u.87466
inst✝²¹ : Semiring R✝
X✝ : Type ?u.87472
inst✝²⁰ : TopologicalSpace X✝
inst✝¹⁹ : AddCommMonoid X✝
inst✝¹⁸ : Module R✝ X✝
Y✝ : Type ?u.87507
inst✝¹⁷ : TopologicalSpace Y✝
inst✝¹⁶ : AddCommMonoid Y✝
inst✝¹⁵ : Module R✝ Y✝
Z : Type ?u.87540
inst✝¹⁴ : TopologicalSpace Z
inst✝¹³ : AddCommMonoid Z
inst✝¹² : Module R✝ Z
ι : Type ?u.87573
inst✝¹¹ : Fintype ι
E : ι → Type ?u.87581
inst✝¹⁰ : (i : ι) → TopologicalSpace (E i)
inst✝⁹ : (i : ι) → AddCommMonoid (E i)
inst✝⁸ : (i : ι) → Module R✝ (E i)
R : Type u_1
inst✝⁷ : Ring R
X : Type u_2
inst✝⁶ : TopologicalSpace X
inst✝⁵ : AddCommGroup X
inst✝⁴ : Module R X
Y : Type u_3
inst✝³ : TopologicalSpace Y
inst✝² : AddCommGroup Y
inst✝¹ : Module R Y
inst✝ : TopologicalAddGroup Y
f : X → Y
hf : IsContinuousLinearMap R f
⊢ ∀ (x : X), -f x = (-mk' R f hf) x
Tactic:
simp[ContinuousLinearMap.neg]
State after:
no goals