internlm/Lean-Github huggingface dataset:
Theorem: dite.arg_te.revDerivM_rule
Proof state before:
case h
ι : Sort ?u.96370
K : Type
inst✝⁹ : RCLike K
m m' : Type → Type
inst✝⁸ : Monad m
inst✝⁷ : Monad m'
inst✝⁶ : RevDerivMonad K m m'
inst✝⁵ : LawfulMonad m
inst✝⁴ : LawfulMonad m'
X : Type
inst✝³ : SemiInnerProductSpace K X
Y : Type
inst✝² : SemiInnerProductSpace K Y
Z : Type
inst✝¹ : SemiInnerProductSpace K Z
E : ι → Type
inst✝ : (i : ι) → SemiInnerProductSpace K (E i)
c : Prop
t : c → X → m Y
e : ¬c → X → m Y
h : ¬c
y : X
⊢ revDerivM K (fun x => if h : c then t h x else e h x) y = if h : c then revDerivM K (t h) y else revDerivM K (e h) y
Tactic:
simp[h]
Proof state after:
no goals
Theorem: SciLean.isomorphicType_equiv_id
Proof state before:
α✝ : Type ?u.9726
α' : Type ?u.9729
β : Type ?u.9732
β' : Type ?u.9735
γ : Type ?u.9738
γ' : Type ?u.9741
inst✝² : IsomorphicType `RealToFloat α✝ α'
inst✝¹ : IsomorphicType `RealToFloat β β'
inst✝ : IsomorphicType `RealToFloat γ γ'
α : Type u_1
a : α
⊢ (IsomorphicType.equiv `RealToFloat) a = a
Tactic:
rfl
Proof state after:
no goals
Theorem: SciLean.ContinuousLinearMap.mk'_eval
Proof state before:
R : Type u_1
inst✝⁶ : Semiring R
X : Type u_2
inst✝⁵ : TopologicalSpace X
inst✝⁴ : AddCommMonoid X
inst✝³ : Module R X
Y : Type u_3
inst✝² : TopologicalSpace Y
inst✝¹ : AddCommMonoid Y
inst✝ : Module R Y
x : X
f : X → Y
hf : IsContinuousLinearMap R f
⊢ (mk' R f hf) x = f x
Tactic:
rfl
Proof state after:
no goals
Theorem: SciLean.ContinuousLinearMap.eta_reduce
Proof state before:
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
f : X →L[R] Y
⊢ mk' R ⇑f ⋯ = f
Tactic:
ext
Proof state after:
case h
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
f : X →L[R] Y
x✝ : X
⊢ (mk' R ⇑f ⋯) x✝ = f x✝
Theorem: SciLean.ContinuousLinearMap.eta_reduce
Proof state before:
case h
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
f : X →L[R] Y
x✝ : X
⊢ (mk' R ⇑f ⋯) x✝ = f x✝
Tactic:
simp
Proof state after:
no goals
Theorem: SciLean.IsContinuousLinearMap.by_morphism
Proof state before:
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
⊢ IsContinuousLinearMap R f
Tactic:
have h' : f = g := by funext x; apply h
Proof state after:
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
⊢ IsContinuousLinearMap R f
Theorem: SciLean.IsContinuousLinearMap.by_morphism
Proof state before:
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
⊢ IsContinuousLinearMap R f
Tactic:
rw[h']
Proof state after:
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
⊢ IsContinuousLinearMap R ⇑g
Theorem: SciLean.IsContinuousLinearMap.by_morphism
Proof state before:
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
⊢ IsContinuousLinearMap R ⇑g
Tactic:
constructor
Proof state after:
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✝
Theorem: SciLean.IsContinuousLinearMap.by_morphism
Proof state before:
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✝
Tactic:
apply g.1.2
Proof state after:
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✝
Theorem: SciLean.IsContinuousLinearMap.by_morphism
Proof state before:
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:
apply g.2
Proof state after:
no goals
Theorem: SciLean.IsContinuousLinearMap.by_morphism
Proof state before:
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
⊢ f = ⇑g
Tactic:
funext x
Proof state after:
case h
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
x : X
⊢ f x = g x
Theorem: SciLean.IsContinuousLinearMap.by_morphism
Proof state before:
case h
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
x : X
⊢ f x = g x
Tactic:
apply h
Proof state after:
no goals
Theorem: SciLean.IsContinuousLinearMap.id_rule
Proof 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
Proof state after:
no goals
Theorem: SciLean.IsContinuousLinearMap.const_rule
Proof state before:
R✝ : Type ?u.20619
inst✝²⁰ : Semiring R✝
X✝ : Type ?u.20625
inst✝¹⁹ : TopologicalSpace X✝
inst✝¹⁸ : AddCommMonoid X✝
inst✝¹⁷ : Module R✝ X✝
Y✝ : Type ?u.20659
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_3
inst✝⁹ : TopologicalSpace Y
inst✝⁸ : AddCommMonoid Y
inst✝⁷ : Module R Y
Z : Type ?u.20763
inst✝⁶ : TopologicalSpace Z
inst✝⁵ : AddCommMonoid Z
inst✝⁴ : Module R Z
ι : Type ?u.20795
inst✝³ : Fintype ι
E : ι → Type ?u.20803
inst✝² : (i : ι) → TopologicalSpace (E i)
inst✝¹ : (i : ι) → AddCommMonoid (E i)
inst✝ : (i : ι) → Module R (E i)
⊢ ∀ (x : X), 0 = 0 x
Tactic:
simp
Proof state after:
no goals
Theorem: SciLean.IsContinuousLinearMap.comp_rule
Proof state before:
R✝ : Type ?u.25843
inst✝²⁰ : Semiring R✝
X✝ : Type ?u.25849
inst✝¹⁹ : TopologicalSpace X✝
inst✝¹⁸ : AddCommMonoid X✝
inst✝¹⁷ : Module R✝ X✝
Y✝ : Type ?u.25883
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_3
inst✝⁹ : TopologicalSpace Y
inst✝⁸ : AddCommMonoid Y
inst✝⁷ : Module R Y
Z : Type u_4
inst✝⁶ : TopologicalSpace Z
inst✝⁵ : AddCommMonoid Z
inst✝⁴ : Module R Z
ι : Type ?u.26019
inst✝³ : Fintype ι
E : ι → Type ?u.26027
inst✝² : (i : ι) → TopologicalSpace (E i)
inst✝¹ : (i : ι) → AddCommMonoid (E i)
inst✝ : (i : ι) → Module R (E i)
g : X → Y
hg : IsContinuousLinearMap R g
f : Y → Z
hf : IsContinuousLinearMap R f
⊢ ∀ (x : X), f (g x) = (ContinuousLinearMap.comp (mk' R f hf) (mk' R g hg)) x
Tactic:
simp[ContinuousLinearMap.comp]
Proof state after:
no goals
Theorem: SciLean.IsContinuousLinearMap.apply_rule
Proof state before:
R✝ : Type ?u.33859
inst✝²⁰ : Semiring R✝
X✝ : Type ?u.33865
inst✝¹⁹ : TopologicalSpace X✝
inst✝¹⁸ : AddCommMonoid X✝
inst✝¹⁷ : Module R✝ X✝
Y✝ : Type ?u.33899
inst✝¹⁶ : TopologicalSpace Y✝
inst✝¹⁵ : AddCommMonoid Y✝
inst✝¹⁴ : Module R✝ Y✝
R : Type u_1
inst✝¹³ : Semiring R
X : Type ?u.33937
inst✝¹² : TopologicalSpace X
inst✝¹¹ : AddCommMonoid X
inst✝¹⁰ : Module R X
Y : Type ?u.33971
inst✝⁹ : TopologicalSpace Y
inst✝⁸ : AddCommMonoid Y
inst✝⁷ : Module R Y
Z : Type ?u.34003
inst✝⁶ : TopologicalSpace Z
inst✝⁵ : AddCommMonoid Z
inst✝⁴ : Module R Z
ι : Type u_2
inst✝³ : Fintype ι
E : ι → Type u_3
inst✝² : (i : ι) → TopologicalSpace (E i)
inst✝¹ : (i : ι) → AddCommMonoid (E i)
inst✝ : (i : ι) → Module R (E i)
i : ι
⊢ ∀ (x : (i : ι) → E i), x i = (ContinuousLinearMap.proj i) x
Tactic:
simp
Proof state after:
no goals
Theorem: SciLean.IsContinuousLinearMap.pi_rule
Proof state before:
R✝ : Type ?u.44507
inst✝²⁰ : Semiring R✝
X✝ : Type ?u.44513
inst✝¹⁹ : TopologicalSpace X✝
inst✝¹⁸ : AddCommMonoid X✝
inst✝¹⁷ : Module R✝ X✝
Y✝ : Type ?u.44547
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.44619
inst✝⁹ : TopologicalSpace Y
inst✝⁸ : AddCommMonoid Y
inst✝⁷ : Module R Y
Z : Type ?u.44651
inst✝⁶ : TopologicalSpace Z
inst✝⁵ : AddCommMonoid Z
inst✝⁴ : Module R Z
ι : Type u_4
inst✝³ : Fintype ι
E : ι → Type u_3
inst✝² : (i : ι) → TopologicalSpace (E i)
inst✝¹ : (i : ι) → AddCommMonoid (E i)
inst✝ : (i : ι) → Module R (E i)
f : X → (i : ι) → E i
hf : ∀ (i : ι), IsContinuousLinearMap R fun x => f x i
⊢ ∀ (x : X), (fun i => f x i) = (ContinuousLinearMap.pi fun i => fun x =>L[R] f x i) x
Tactic:
simp
Proof state after:
no goals
Theorem: SciLean.IsContinuousLinearMap.FunLike.coe.arg_a.IsContinuousLinearMap_rule
Proof state before:
R✝¹ : Type ?u.52736
inst✝³⁴ : Semiring R✝¹
X✝¹ : Type ?u.52742
inst✝³³ : TopologicalSpace X✝¹
inst✝³² : AddCommMonoid X✝¹
inst✝³¹ : Module R✝¹ X✝¹
Y✝¹ : Type ?u.52776
inst✝³⁰ : TopologicalSpace Y✝¹
inst✝²⁹ : AddCommMonoid Y✝¹
inst✝²⁸ : Module R✝¹ Y✝¹
R✝ : Type ?u.52808
inst✝²⁷ : Semiring R✝
X✝ : Type ?u.52814
inst✝²⁶ : TopologicalSpace X✝
inst✝²⁵ : AddCommMonoid X✝
inst✝²⁴ : Module R✝ X✝
Y✝ : Type ?u.52848
inst✝²³ : TopologicalSpace Y✝
inst✝²² : AddCommMonoid Y✝
inst✝²¹ : Module R✝ Y✝
Z✝ : Type ?u.52880
inst✝²⁰ : TopologicalSpace Z✝
inst✝¹⁹ : AddCommMonoid Z✝
inst✝¹⁸ : Module R✝ Z✝
ι✝ : Type ?u.52912
inst✝¹⁷ : Fintype ι✝
E✝ : ι✝ → Type ?u.52920
inst✝¹⁶ : (i : ι✝) → TopologicalSpace (E✝ i)
inst✝¹⁵ : (i : ι✝) → AddCommMonoid (E✝ i)
inst✝¹⁴ : (i : ι✝) → Module R✝ (E✝ i)
R : Type u_3
inst✝¹³ : Semiring R
X : Type ?u.52976
inst✝¹² : TopologicalSpace X
inst✝¹¹ : AddCommMonoid X
inst✝¹⁰ : Module R X
Y : Type u_2
inst✝⁹ : TopologicalSpace Y
inst✝⁸ : AddCommMonoid Y
inst✝⁷ : Module R Y
Z : Type u_1
inst✝⁶ : TopologicalSpace Z
inst✝⁵ : AddCommMonoid Z
inst✝⁴ : Module R Z
ι : Type ?u.53077
inst✝³ : Fintype ι
E : ι → Type ?u.53085
inst✝² : (i : ι) → TopologicalSpace (E i)
inst✝¹ : (i : ι) → AddCommMonoid (E i)
inst✝ : (i : ι) → Module R (E i)
f : Y →L[R] Z
⊢ ∀ (x : Y), f x = f x
Tactic:
simp
Proof state after:
no goals
Theorem: SciLean.IsContinuousLinearMap.FunLike.coe.arg_a.IsContinuousLinearMap_rule'
Proof state before:
R✝¹ : Type ?u.57348
inst✝³⁴ : Semiring R✝¹
X✝¹ : Type ?u.57354
inst✝³³ : TopologicalSpace X✝¹
inst✝³² : AddCommMonoid X✝¹
inst✝³¹ : Module R✝¹ X✝¹
Y✝¹ : Type ?u.57388
inst✝³⁰ : TopologicalSpace Y✝¹
inst✝²⁹ : AddCommMonoid Y✝¹
inst✝²⁸ : Module R✝¹ Y✝¹
R✝ : Type ?u.57420
inst✝²⁷ : Semiring R✝
X✝ : Type ?u.57426
inst✝²⁶ : TopologicalSpace X✝
inst✝²⁵ : AddCommMonoid X✝
inst✝²⁴ : Module R✝ X✝
Y✝ : Type ?u.57460
inst✝²³ : TopologicalSpace Y✝
inst✝²² : AddCommMonoid Y✝
inst✝²¹ : Module R✝ Y✝
Z✝ : Type ?u.57492
inst✝²⁰ : TopologicalSpace Z✝
inst✝¹⁹ : AddCommMonoid Z✝
inst✝¹⁸ : Module R✝ Z✝
ι✝ : Type ?u.57524
inst✝¹⁷ : Fintype ι✝
E✝ : ι✝ → Type ?u.57532
inst✝¹⁶ : (i : ι✝) → TopologicalSpace (E✝ i)
inst✝¹⁵ : (i : ι✝) → AddCommMonoid (E✝ i)
inst✝¹⁴ : (i : ι✝) → Module R✝ (E✝ i)
R : Type u_3
inst✝¹³ : Semiring R
X : Type u_4
inst✝¹² : TopologicalSpace X
inst✝¹¹ : AddCommMonoid X
inst✝¹⁰ : Module R X
Y : Type u_2
inst✝⁹ : TopologicalSpace Y
inst✝⁸ : AddCommMonoid Y
inst✝⁷ : Module R Y
Z : Type u_1
inst✝⁶ : TopologicalSpace Z
inst✝⁵ : AddCommMonoid Z
inst✝⁴ : Module R Z
ι : Type ?u.57689
inst✝³ : Fintype ι
E : ι → Type ?u.57697
inst✝² : (i : ι) → TopologicalSpace (E i)
inst✝¹ : (i : ι) → AddCommMonoid (E i)
inst✝ : (i : ι) → Module R (E i)
f : Y →L[R] Z
g : X → Y
hg : IsContinuousLinearMap R g
⊢ ∀ (x : X), f (g x) = (ContinuousLinearMap.comp f (mk' R g hg)) x
Tactic:
simp
Proof state after:
no goals
Theorem: SciLean.IsContinuousLinearMap.Prod.mk.arg_fstsnd.IsContinuousLinearMap_rule
Proof state before:
R✝¹ : Type ?u.65707
inst✝³⁴ : Semiring R✝¹
X✝¹ : Type ?u.65713
inst✝³³ : TopologicalSpace X✝¹
inst✝³² : AddCommMonoid X✝¹
inst✝³¹ : Module R✝¹ X✝¹
Y✝¹ : Type ?u.65747
inst✝³⁰ : TopologicalSpace Y✝¹
inst✝²⁹ : AddCommMonoid Y✝¹
inst✝²⁸ : Module R✝¹ Y✝¹
R✝ : Type ?u.65779
inst✝²⁷ : Semiring R✝
X✝ : Type ?u.65785
inst✝²⁶ : TopologicalSpace X✝
inst✝²⁵ : AddCommMonoid X✝
inst✝²⁴ : Module R✝ X✝
Y✝ : Type ?u.65819
inst✝²³ : TopologicalSpace Y✝
inst✝²² : AddCommMonoid Y✝
inst✝²¹ : Module R✝ Y✝
Z✝ : Type ?u.65851
inst✝²⁰ : TopologicalSpace Z✝
inst✝¹⁹ : AddCommMonoid Z✝
inst✝¹⁸ : Module R✝ Z✝
ι✝ : Type ?u.65883
inst✝¹⁷ : Fintype ι✝
E✝ : ι✝ → Type ?u.65891
inst✝¹⁶ : (i : ι✝) → TopologicalSpace (E✝ i)
inst✝¹⁵ : (i : ι✝) → AddCommMonoid (E✝ i)
inst✝¹⁴ : (i : ι✝) → Module R✝ (E✝ i)
R : Type u_1
inst✝¹³ : Semiring R
X : Type u_2
inst✝¹² : TopologicalSpace X
inst✝¹¹ : AddCommMonoid X
inst✝¹⁰ : Module R X
Y : Type u_3
inst✝⁹ : TopologicalSpace Y
inst✝⁸ : AddCommMonoid Y
inst✝⁷ : Module R Y
Z : Type u_4
inst✝⁶ : TopologicalSpace Z
inst✝⁵ : AddCommMonoid Z
inst✝⁴ : Module R Z
ι : Type ?u.66048
inst✝³ : Fintype ι
E : ι → Type ?u.66056
inst✝² : (i : ι) → TopologicalSpace (E i)
inst✝¹ : (i : ι) → AddCommMonoid (E i)
inst✝ : (i : ι) → Module R (E i)
g : X → Y
hg : IsContinuousLinearMap R g
f : X → Z
hf : IsContinuousLinearMap R f
⊢ ∀ (x : X), (g x, f x) = (ContinuousLinearMap.prod (mk' R g hg) (mk' R f hf)) x
Tactic:
simp
Proof state after:
no goals