Theorem: SciLean.IsContinuousLinearMap.HDiv.hDiv.arg_a0.IsContinuousLinearMap_rule (SciLean/Core/FunctionPropositions/IsContinuousLinearMap.lean)

State before:
R✝² : Type ?u.235565
inst✝⁴⁰ : Semiring R✝²
X✝² : Type ?u.235571
inst✝³⁹ : TopologicalSpace X✝²
inst✝³⁸ : AddCommMonoid X✝²
inst✝³⁷ : Module R✝² X✝²
Y✝¹ : Type ?u.235605
inst✝³⁶ : TopologicalSpace Y✝¹
inst✝³⁵ : AddCommMonoid Y✝¹
inst✝³⁴ : Module R✝² Y✝¹
R✝¹ : Type ?u.235637
inst✝³³ : Semiring R✝¹
X✝¹ : Type ?u.235643
inst✝³² : TopologicalSpace X✝¹
inst✝³¹ : AddCommMonoid X✝¹
inst✝³⁰ : Module R✝¹ X✝¹
Y✝ : Type ?u.235677
inst✝²⁹ : TopologicalSpace Y✝
inst✝²⁸ : AddCommMonoid Y✝
inst✝²⁷ : Module R✝¹ Y✝
Z✝ : Type ?u.235709
inst✝²⁶ : TopologicalSpace Z✝
inst✝²⁵ : AddCommMonoid Z✝
inst✝²⁴ : Module R✝¹ Z✝
ι✝ : Type ?u.235741
inst✝²³ : Fintype ι✝
E✝ : ι✝ → Type ?u.235749
inst✝²² : (i : ι✝) → TopologicalSpace (E✝ i)
inst✝²¹ : (i : ι✝) → AddCommMonoid (E✝ i)
inst✝²⁰ : (i : ι✝) → Module R✝¹ (E✝ i)
R✝ : Type ?u.235799
inst✝¹⁹ : Semiring R✝
X✝ : Type ?u.235805
inst✝¹⁸ : TopologicalSpace X✝
inst✝¹⁷ : AddCommMonoid X✝
inst✝¹⁶ : Module R✝ X✝
Y : Type ?u.235840
inst✝¹⁵ : TopologicalSpace Y
inst✝¹⁴ : AddCommMonoid Y
inst✝¹³ : Module R✝ Y
Z : Type ?u.235873
inst✝¹² : TopologicalSpace Z
inst✝¹¹ : AddCommMonoid Z
inst✝¹⁰ : Module R✝ Z
ι : Type ?u.235906
inst✝⁹ : Fintype ι
E : ι → Type ?u.235914
inst✝⁸ : (i : ι) → TopologicalSpace (E i)
inst✝⁷ : (i : ι) → AddCommMonoid (E i)
inst✝⁶ : (i : ι) → Module R✝ (E i)
R : Type u_1
inst✝⁵ : NontriviallyNormedField R
K : Type u_2
inst✝⁴ : NontriviallyNormedField K
inst✝³ : NormedAlgebra R K
X : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : AddCommMonoid X
inst✝ : Module R X
f : X → K
hf : IsContinuousLinearMap R f
y : K
⊢ ∀ (x : X), f x / y = (ContinuousLinearMap.divRight (mk' R f hf) y) x
Tactic:
simp
State after:
no goals