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

State before:
R✝¹ : Type ?u.248959
inst✝³⁹ : Semiring R✝¹
X✝² : Type ?u.248965
inst✝³⁸ : TopologicalSpace X✝²
inst✝³⁷ : AddCommMonoid X✝²
inst✝³⁶ : Module R✝¹ X✝²
Y✝² : Type ?u.248999
inst✝³⁵ : TopologicalSpace Y✝²
inst✝³⁴ : AddCommMonoid Y✝²
inst✝³³ : Module R✝¹ Y✝²
R✝ : Type ?u.249031
inst✝³² : Semiring R✝
X✝¹ : Type ?u.249037
inst✝³¹ : TopologicalSpace X✝¹
inst✝³⁰ : AddCommMonoid X✝¹
inst✝²⁹ : Module R✝ X✝¹
Y✝¹ : Type ?u.249071
inst✝²⁸ : TopologicalSpace Y✝¹
inst✝²⁷ : AddCommMonoid Y✝¹
inst✝²⁶ : Module R✝ Y✝¹
Z✝ : Type ?u.249103
inst✝²⁵ : TopologicalSpace Z✝
inst✝²⁴ : AddCommMonoid Z✝
inst✝²³ : Module R✝ Z✝
ι✝ : Type ?u.249135
inst✝²² : Fintype ι✝
E✝ : ι✝ → Type ?u.249143
inst✝²¹ : (i : ι✝) → TopologicalSpace (E✝ i)
inst✝²⁰ : (i : ι✝) → AddCommMonoid (E✝ i)
inst✝¹⁹ : (i : ι✝) → Module R✝ (E✝ i)
R : Type ?u.249193
inst✝¹⁸ : Semiring R
X✝ : Type ?u.249199
inst✝¹⁷ : TopologicalSpace X✝
inst✝¹⁶ : AddCommMonoid X✝
inst✝¹⁵ : Module R X✝
Y✝ : Type ?u.249234
inst✝¹⁴ : TopologicalSpace Y✝
inst✝¹³ : AddCommMonoid Y✝
inst✝¹² : Module R Y✝
Z : Type ?u.249267
inst✝¹¹ : TopologicalSpace Z
inst✝¹⁰ : AddCommMonoid Z
inst✝⁹ : Module R Z
ι : Type ?u.249300
inst✝⁸ : Fintype ι
E : ι → Type ?u.249308
inst✝⁷ : (i : ι) → TopologicalSpace (E i)
inst✝⁶ : (i : ι) → AddCommMonoid (E i)
inst✝⁵ : (i : ι) → Module R (E i)
K : Type u_1
inst✝⁴ : RCLike K
X : Type u_2
inst✝³ : NormedAddCommGroup X
inst✝² : NormedSpace K X
Y : Type u_3
inst✝¹ : NormedAddCommGroup Y
inst✝ : NormedSpace K Y
f : X → Y
hf : IsContinuousLinearMap K f
⊢ Differentiable K f
Tactic:
have := hf
State after:
R✝¹ : Type ?u.248959
inst✝³⁹ : Semiring R✝¹
X✝² : Type ?u.248965
inst✝³⁸ : TopologicalSpace X✝²
inst✝³⁷ : AddCommMonoid X✝²
inst✝³⁶ : Module R✝¹ X✝²
Y✝² : Type ?u.248999
inst✝³⁵ : TopologicalSpace Y✝²
inst✝³⁴ : AddCommMonoid Y✝²
inst✝³³ : Module R✝¹ Y✝²
R✝ : Type ?u.249031
inst✝³² : Semiring R✝
X✝¹ : Type ?u.249037
inst✝³¹ : TopologicalSpace X✝¹
inst✝³⁰ : AddCommMonoid X✝¹
inst✝²⁹ : Module R✝ X✝¹
Y✝¹ : Type ?u.249071
inst✝²⁸ : TopologicalSpace Y✝¹
inst✝²⁷ : AddCommMonoid Y✝¹
inst✝²⁶ : Module R✝ Y✝¹
Z✝ : Type ?u.249103
inst✝²⁵ : TopologicalSpace Z✝
inst✝²⁴ : AddCommMonoid Z✝
inst✝²³ : Module R✝ Z✝
ι✝ : Type ?u.249135
inst✝²² : Fintype ι✝
E✝ : ι✝ → Type ?u.249143
inst✝²¹ : (i : ι✝) → TopologicalSpace (E✝ i)
inst✝²⁰ : (i : ι✝) → AddCommMonoid (E✝ i)
inst✝¹⁹ : (i : ι✝) → Module R✝ (E✝ i)
R : Type ?u.249193
inst✝¹⁸ : Semiring R
X✝ : Type ?u.249199
inst✝¹⁷ : TopologicalSpace X✝
inst✝¹⁶ : AddCommMonoid X✝
inst✝¹⁵ : Module R X✝
Y✝ : Type ?u.249234
inst✝¹⁴ : TopologicalSpace Y✝
inst✝¹³ : AddCommMonoid Y✝
inst✝¹² : Module R Y✝
Z : Type ?u.249267
inst✝¹¹ : TopologicalSpace Z
inst✝¹⁰ : AddCommMonoid Z
inst✝⁹ : Module R Z
ι : Type ?u.249300
inst✝⁸ : Fintype ι
E : ι → Type ?u.249308
inst✝⁷ : (i : ι) → TopologicalSpace (E i)
inst✝⁶ : (i : ι) → AddCommMonoid (E i)
inst✝⁵ : (i : ι) → Module R (E i)
K : Type u_1
inst✝⁴ : RCLike K
X : Type u_2
inst✝³ : NormedAddCommGroup X
inst✝² : NormedSpace K X
Y : Type u_3
inst✝¹ : NormedAddCommGroup Y
inst✝ : NormedSpace K Y
f : X → Y
hf this : IsContinuousLinearMap K f
⊢ Differentiable K f

State before:
R✝¹ : Type ?u.248959
inst✝³⁹ : Semiring R✝¹
X✝² : Type ?u.248965
inst✝³⁸ : TopologicalSpace X✝²
inst✝³⁷ : AddCommMonoid X✝²
inst✝³⁶ : Module R✝¹ X✝²
Y✝² : Type ?u.248999
inst✝³⁵ : TopologicalSpace Y✝²
inst✝³⁴ : AddCommMonoid Y✝²
inst✝³³ : Module R✝¹ Y✝²
R✝ : Type ?u.249031
inst✝³² : Semiring R✝
X✝¹ : Type ?u.249037
inst✝³¹ : TopologicalSpace X✝¹
inst✝³⁰ : AddCommMonoid X✝¹
inst✝²⁹ : Module R✝ X✝¹
Y✝¹ : Type ?u.249071
inst✝²⁸ : TopologicalSpace Y✝¹
inst✝²⁷ : AddCommMonoid Y✝¹
inst✝²⁶ : Module R✝ Y✝¹
Z✝ : Type ?u.249103
inst✝²⁵ : TopologicalSpace Z✝
inst✝²⁴ : AddCommMonoid Z✝
inst✝²³ : Module R✝ Z✝
ι✝ : Type ?u.249135
inst✝²² : Fintype ι✝
E✝ : ι✝ → Type ?u.249143
inst✝²¹ : (i : ι✝) → TopologicalSpace (E✝ i)
inst✝²⁰ : (i : ι✝) → AddCommMonoid (E✝ i)
inst✝¹⁹ : (i : ι✝) → Module R✝ (E✝ i)
R : Type ?u.249193
inst✝¹⁸ : Semiring R
X✝ : Type ?u.249199
inst✝¹⁷ : TopologicalSpace X✝
inst✝¹⁶ : AddCommMonoid X✝
inst✝¹⁵ : Module R X✝
Y✝ : Type ?u.249234
inst✝¹⁴ : TopologicalSpace Y✝
inst✝¹³ : AddCommMonoid Y✝
inst✝¹² : Module R Y✝
Z : Type ?u.249267
inst✝¹¹ : TopologicalSpace Z
inst✝¹⁰ : AddCommMonoid Z
inst✝⁹ : Module R Z
ι : Type ?u.249300
inst✝⁸ : Fintype ι
E : ι → Type ?u.249308
inst✝⁷ : (i : ι) → TopologicalSpace (E i)
inst✝⁶ : (i : ι) → AddCommMonoid (E i)
inst✝⁵ : (i : ι) → Module R (E i)
K : Type u_1
inst✝⁴ : RCLike K
X : Type u_2
inst✝³ : NormedAddCommGroup X
inst✝² : NormedSpace K X
Y : Type u_3
inst✝¹ : NormedAddCommGroup Y
inst✝ : NormedSpace K Y
f : X → Y
hf this : IsContinuousLinearMap K f
⊢ Differentiable K f
Tactic:
sorry_proof
State after:
no goals