Theorem: SciLean.IsContinuousLinearMap.by_morphism
Proof state before:
case linear
R✝ : Type ?u.14342
inst✝²⁰ : Semiring R✝
X✝ : Type ?u.14348
inst✝¹⁹ : TopologicalSpace X✝
inst✝¹⁸ : AddCommMonoid X✝
inst✝¹⁷ : Module R✝ X✝
Y✝ : Type ?u.14382
inst✝¹⁶ : TopologicalSpace Y✝
inst✝¹⁵ : AddCommMonoid Y✝
inst✝¹⁴ : Module R✝ Y✝
R : Type u_3
inst✝¹³ : Semiring R
X : Type u_2
inst✝¹² : TopologicalSpace X
inst✝¹¹ : AddCommMonoid X
inst✝¹⁰ : Module R X
Y : Type u_1
inst✝⁹ : TopologicalSpace Y
inst✝⁸ : AddCommMonoid Y
inst✝⁷ : Module R Y
Z : Type ?u.14486
inst✝⁶ : TopologicalSpace Z
inst✝⁵ : AddCommMonoid Z
inst✝⁴ : Module R Z
ι : Type ?u.14518
inst✝³ : Fintype ι
E : ι → Type ?u.14526
inst✝² : (i : ι) → TopologicalSpace (E i)
inst✝¹ : (i : ι) → AddCommMonoid (E i)
inst✝ : (i : ι) → Module R (E i)
f : X → Y
g : X →L[R] Y
h : ∀ (x : X), f x = g x
h' : f = ⇑g
⊢ IsLinearMap R ⇑g

case cont
R✝ : Type ?u.14342
inst✝²⁰ : Semiring R✝
X✝ : Type ?u.14348
inst✝¹⁹ : TopologicalSpace X✝
inst✝¹⁸ : AddCommMonoid X✝
inst✝¹⁷ : Module R✝ X✝
Y✝ : Type ?u.14382
inst✝¹⁶ : TopologicalSpace Y✝
inst✝¹⁵ : AddCommMonoid Y✝
inst✝¹⁴ : Module R✝ Y✝
R : Type u_3
inst✝¹³ : Semiring R
X : Type u_2
inst✝¹² : TopologicalSpace X
inst✝¹¹ : AddCommMonoid X
inst✝¹⁰ : Module R X
Y : Type u_1
inst✝⁹ : TopologicalSpace Y
inst✝⁸ : AddCommMonoid Y
inst✝⁷ : Module R Y
Z : Type ?u.14486
inst✝⁶ : TopologicalSpace Z
inst✝⁵ : AddCommMonoid Z
inst✝⁴ : Module R Z
ι : Type ?u.14518
inst✝³ : Fintype ι
E : ι → Type ?u.14526
inst✝² : (i : ι) → TopologicalSpace (E i)
inst✝¹ : (i : ι) → AddCommMonoid (E i)
inst✝ : (i : ι) → Module R (E i)
f : X → Y
g : X →L[R] Y
h : ∀ (x : X), f x = g x
h' : f = ⇑g
⊢ autoParam (Continuous ⇑g) _auto✝
Tactic:
constructor
Proof state after:
case linear.map_add
R✝ : Type ?u.14342
inst✝²⁰ : Semiring R✝
X✝ : Type ?u.14348
inst✝¹⁹ : TopologicalSpace X✝
inst✝¹⁸ : AddCommMonoid X✝
inst✝¹⁷ : Module R✝ X✝
Y✝ : Type ?u.14382
inst✝¹⁶ : TopologicalSpace Y✝
inst✝¹⁵ : AddCommMonoid Y✝
inst✝¹⁴ : Module R✝ Y✝
R : Type u_3
inst✝¹³ : Semiring R
X : Type u_2
inst✝¹² : TopologicalSpace X
inst✝¹¹ : AddCommMonoid X
inst✝¹⁰ : Module R X
Y : Type u_1
inst✝⁹ : TopologicalSpace Y
inst✝⁸ : AddCommMonoid Y
inst✝⁷ : Module R Y
Z : Type ?u.14486
inst✝⁶ : TopologicalSpace Z
inst✝⁵ : AddCommMonoid Z
inst✝⁴ : Module R Z
ι : Type ?u.14518
inst✝³ : Fintype ι
E : ι → Type ?u.14526
inst✝² : (i : ι) → TopologicalSpace (E i)
inst✝¹ : (i : ι) → AddCommMonoid (E i)
inst✝ : (i : ι) → Module R (E i)
f : X → Y
g : X →L[R] Y
h : ∀ (x : X), f x = g x
h' : f = ⇑g
⊢ ∀ (x y : X), g (x + y) = g x + g y

case linear.map_smul
R✝ : Type ?u.14342
inst✝²⁰ : Semiring R✝
X✝ : Type ?u.14348
inst✝¹⁹ : TopologicalSpace X✝
inst✝¹⁸ : AddCommMonoid X✝
inst✝¹⁷ : Module R✝ X✝
Y✝ : Type ?u.14382
inst✝¹⁶ : TopologicalSpace Y✝
inst✝¹⁵ : AddCommMonoid Y✝
inst✝¹⁴ : Module R✝ Y✝
R : Type u_3
inst✝¹³ : Semiring R
X : Type u_2
inst✝¹² : TopologicalSpace X
inst✝¹¹ : AddCommMonoid X
inst✝¹⁰ : Module R X
Y : Type u_1
inst✝⁹ : TopologicalSpace Y
inst✝⁸ : AddCommMonoid Y
inst✝⁷ : Module R Y
Z : Type ?u.14486
inst✝⁶ : TopologicalSpace Z
inst✝⁵ : AddCommMonoid Z
inst✝⁴ : Module R Z
ι : Type ?u.14518
inst✝³ : Fintype ι
E : ι → Type ?u.14526
inst✝² : (i : ι) → TopologicalSpace (E i)
inst✝¹ : (i : ι) → AddCommMonoid (E i)
inst✝ : (i : ι) → Module R (E i)
f : X → Y
g : X →L[R] Y
h : ∀ (x : X), f x = g x
h' : f = ⇑g
⊢ ∀ (c : R) (x : X), g (c • x) = c • g x

case cont
R✝ : Type ?u.14342
inst✝²⁰ : Semiring R✝
X✝ : Type ?u.14348
inst✝¹⁹ : TopologicalSpace X✝
inst✝¹⁸ : AddCommMonoid X✝
inst✝¹⁷ : Module R✝ X✝
Y✝ : Type ?u.14382
inst✝¹⁶ : TopologicalSpace Y✝
inst✝¹⁵ : AddCommMonoid Y✝
inst✝¹⁴ : Module R✝ Y✝
R : Type u_3
inst✝¹³ : Semiring R
X : Type u_2
inst✝¹² : TopologicalSpace X
inst✝¹¹ : AddCommMonoid X
inst✝¹⁰ : Module R X
Y : Type u_1
inst✝⁹ : TopologicalSpace Y
inst✝⁸ : AddCommMonoid Y
inst✝⁷ : Module R Y
Z : Type ?u.14486
inst✝⁶ : TopologicalSpace Z
inst✝⁵ : AddCommMonoid Z
inst✝⁴ : Module R Z
ι : Type ?u.14518
inst✝³ : Fintype ι
E : ι → Type ?u.14526
inst✝² : (i : ι) → TopologicalSpace (E i)
inst✝¹ : (i : ι) → AddCommMonoid (E i)
inst✝ : (i : ι) → Module R (E i)
f : X → Y
g : X →L[R] Y
h : ∀ (x : X), f x = g x
h' : f = ⇑g
⊢ autoParam (Continuous ⇑g) _auto✝