internlm/Lean-Github huggingface dataset:
Theorem: SciLean.IsContinuousLinearMap.Prod.fst.arg_self.IsContinuousLinearMap_rule
Proof state before:
R✝¹ : Type ?u.73036
inst✝³⁴ : Semiring R✝¹
X✝¹ : Type ?u.73042
inst✝³³ : TopologicalSpace X✝¹
inst✝³² : AddCommMonoid X✝¹
inst✝³¹ : Module R✝¹ X✝¹
Y✝¹ : Type ?u.73076
inst✝³⁰ : TopologicalSpace Y✝¹
inst✝²⁹ : AddCommMonoid Y✝¹
inst✝²⁸ : Module R✝¹ Y✝¹
R✝ : Type ?u.73108
inst✝²⁷ : Semiring R✝
X✝ : Type ?u.73114
inst✝²⁶ : TopologicalSpace X✝
inst✝²⁵ : AddCommMonoid X✝
inst✝²⁴ : Module R✝ X✝
Y✝ : Type ?u.73148
inst✝²³ : TopologicalSpace Y✝
inst✝²² : AddCommMonoid Y✝
inst✝²¹ : Module R✝ Y✝
Z✝ : Type ?u.73180
inst✝²⁰ : TopologicalSpace Z✝
inst✝¹⁹ : AddCommMonoid Z✝
inst✝¹⁸ : Module R✝ Z✝
ι✝ : Type ?u.73212
inst✝¹⁷ : Fintype ι✝
E✝ : ι✝ → Type ?u.73220
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_1
inst✝⁹ : TopologicalSpace Y
inst✝⁸ : AddCommMonoid Y
inst✝⁷ : Module R Y
Z : Type u_2
inst✝⁶ : TopologicalSpace Z
inst✝⁵ : AddCommMonoid Z
inst✝⁴ : Module R Z
ι : Type ?u.73377
inst✝³ : Fintype ι
E : ι → Type ?u.73385
inst✝² : (i : ι) → TopologicalSpace (E i)
inst✝¹ : (i : ι) → AddCommMonoid (E i)
inst✝ : (i : ι) → Module R (E i)
f : X → Y × Z
hf : IsContinuousLinearMap R f
⊢ ∀ (x : X), (f x).1 = (ContinuousLinearMap.comp (ContinuousLinearMap.fst R Y Z) (mk' R f hf)) x
Tactic:
simp
Proof state after:
no goals
Theorem: SciLean.IsContinuousLinearMap.Prod.snd.arg_self.IsContinuousLinearMap_rule
Proof state before:
R✝¹ : Type ?u.80134
inst✝³⁴ : Semiring R✝¹
X✝¹ : Type ?u.80140
inst✝³³ : TopologicalSpace X✝¹
inst✝³² : AddCommMonoid X✝¹
inst✝³¹ : Module R✝¹ X✝¹
Y✝¹ : Type ?u.80174
inst✝³⁰ : TopologicalSpace Y✝¹
inst✝²⁹ : AddCommMonoid Y✝¹
inst✝²⁸ : Module R✝¹ Y✝¹
R✝ : Type ?u.80206
inst✝²⁷ : Semiring R✝
X✝ : Type ?u.80212
inst✝²⁶ : TopologicalSpace X✝
inst✝²⁵ : AddCommMonoid X✝
inst✝²⁴ : Module R✝ X✝
Y✝ : Type ?u.80246
inst✝²³ : TopologicalSpace Y✝
inst✝²² : AddCommMonoid Y✝
inst✝²¹ : Module R✝ Y✝
Z✝ : Type ?u.80278
inst✝²⁰ : TopologicalSpace Z✝
inst✝¹⁹ : AddCommMonoid Z✝
inst✝¹⁸ : Module R✝ Z✝
ι✝ : Type ?u.80310
inst✝¹⁷ : Fintype ι✝
E✝ : ι✝ → Type ?u.80318
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_1
inst✝⁹ : TopologicalSpace Y
inst✝⁸ : AddCommMonoid Y
inst✝⁷ : Module R Y
Z : Type u_2
inst✝⁶ : TopologicalSpace Z
inst✝⁵ : AddCommMonoid Z
inst✝⁴ : Module R Z
ι : Type ?u.80475
inst✝³ : Fintype ι
E : ι → Type ?u.80483
inst✝² : (i : ι) → TopologicalSpace (E i)
inst✝¹ : (i : ι) → AddCommMonoid (E i)
inst✝ : (i : ι) → Module R (E i)
f : X → Y × Z
hf : IsContinuousLinearMap R f
⊢ ∀ (x : X), (f x).2 = (ContinuousLinearMap.comp (ContinuousLinearMap.snd R Y Z) (mk' R f hf)) x
Tactic:
simp
Proof state after:
no goals
Theorem: SciLean.IsContinuousLinearMap.Neg.neg.arg_a0.IsContinuousLinearMap_rule
Proof 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]
Proof state after:
no goals
Theorem: SciLean.IsContinuousLinearMap.HAdd.hAdd.arg_a0a1.IsContinuousLinearMap_rule
Proof state before:
R✝¹ : Type ?u.100515
inst✝³⁵ : Semiring R✝¹
X✝¹ : Type ?u.100521
inst✝³⁴ : TopologicalSpace X✝¹
inst✝³³ : AddCommMonoid X✝¹
inst✝³² : Module R✝¹ X✝¹
Y✝¹ : Type ?u.100555
inst✝³¹ : TopologicalSpace Y✝¹
inst✝³⁰ : AddCommMonoid Y✝¹
inst✝²⁹ : Module R✝¹ Y✝¹
R✝ : Type ?u.100587
inst✝²⁸ : Semiring R✝
X✝ : Type ?u.100593
inst✝²⁷ : TopologicalSpace X✝
inst✝²⁶ : AddCommMonoid X✝
inst✝²⁵ : Module R✝ X✝
Y✝ : Type ?u.100627
inst✝²⁴ : TopologicalSpace Y✝
inst✝²³ : AddCommMonoid Y✝
inst✝²² : Module R✝ Y✝
Z✝ : Type ?u.100659
inst✝²¹ : TopologicalSpace Z✝
inst✝²⁰ : AddCommMonoid Z✝
inst✝¹⁹ : Module R✝ Z✝
ι✝ : Type ?u.100691
inst✝¹⁸ : Fintype ι✝
E✝ : ι✝ → Type ?u.100699
inst✝¹⁷ : (i : ι✝) → TopologicalSpace (E✝ i)
inst✝¹⁶ : (i : ι✝) → AddCommMonoid (E✝ i)
inst✝¹⁵ : (i : ι✝) → Module R✝ (E✝ i)
R : Type u_2
inst✝¹⁴ : Semiring R
X : Type u_3
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.100823
inst✝⁷ : TopologicalSpace Z
inst✝⁶ : AddCommMonoid Z
inst✝⁵ : Module R Z
ι : Type ?u.100856
inst✝⁴ : Fintype ι
E : ι → Type ?u.100864
inst✝³ : (i : ι) → TopologicalSpace (E i)
inst✝² : (i : ι) → AddCommMonoid (E i)
inst✝¹ : (i : ι) → Module R (E i)
inst✝ : ContinuousAdd Y
f g : X → Y
hf : IsContinuousLinearMap R f
hg : IsContinuousLinearMap R g
⊢ ∀ (x : X), f x + g x = (Add.add (mk' R f hf) (mk' R g hg)) x
Tactic:
simp[ContinuousLinearMap.add]
Proof state after:
no goals
Theorem: SciLean.IsContinuousLinearMap.HSub.hSub.arg_a0a1.IsContinuousLinearMap_rule
Proof state before:
R✝² : Type ?u.111801
inst✝⁴² : Semiring R✝²
X✝² : Type ?u.111807
inst✝⁴¹ : TopologicalSpace X✝²
inst✝⁴⁰ : AddCommMonoid X✝²
inst✝³⁹ : Module R✝² X✝²
Y✝² : Type ?u.111841
inst✝³⁸ : TopologicalSpace Y✝²
inst✝³⁷ : AddCommMonoid Y✝²
inst✝³⁶ : Module R✝² Y✝²
R✝¹ : Type ?u.111873
inst✝³⁵ : Semiring R✝¹
X✝¹ : Type ?u.111879
inst✝³⁴ : TopologicalSpace X✝¹
inst✝³³ : AddCommMonoid X✝¹
inst✝³² : Module R✝¹ X✝¹
Y✝¹ : Type ?u.111913
inst✝³¹ : TopologicalSpace Y✝¹
inst✝³⁰ : AddCommMonoid Y✝¹
inst✝²⁹ : Module R✝¹ Y✝¹
Z✝ : Type ?u.111945
inst✝²⁸ : TopologicalSpace Z✝
inst✝²⁷ : AddCommMonoid Z✝
inst✝²⁶ : Module R✝¹ Z✝
ι✝ : Type ?u.111977
inst✝²⁵ : Fintype ι✝
E✝ : ι✝ → Type ?u.111985
inst✝²⁴ : (i : ι✝) → TopologicalSpace (E✝ i)
inst✝²³ : (i : ι✝) → AddCommMonoid (E✝ i)
inst✝²² : (i : ι✝) → Module R✝¹ (E✝ i)
R✝ : Type ?u.112035
inst✝²¹ : Semiring R✝
X✝ : Type ?u.112041
inst✝²⁰ : TopologicalSpace X✝
inst✝¹⁹ : AddCommMonoid X✝
inst✝¹⁸ : Module R✝ X✝
Y✝ : Type ?u.112076
inst✝¹⁷ : TopologicalSpace Y✝
inst✝¹⁶ : AddCommMonoid Y✝
inst✝¹⁵ : Module R✝ Y✝
Z : Type ?u.112109
inst✝¹⁴ : TopologicalSpace Z
inst✝¹³ : AddCommMonoid Z
inst✝¹² : Module R✝ Z
ι : Type ?u.112142
inst✝¹¹ : Fintype ι
E : ι → Type ?u.112150
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 g : X → Y
hf : IsContinuousLinearMap R f
hg : IsContinuousLinearMap R g
⊢ ∀ (x : X), f x - g x = (Sub.sub (mk' R f hf) (mk' R g hg)) x
Tactic:
simp[ContinuousLinearMap.sub]
Proof state after:
no goals
Theorem: SciLean.IsContinuousLinearMap.HMul.hMul.arg_a0.IsContinuousLinearMap_rule
Proof state before:
R✝² : Type ?u.155348
inst✝⁴² : Semiring R✝²
X✝² : Type ?u.155354
inst✝⁴¹ : TopologicalSpace X✝²
inst✝⁴⁰ : AddCommMonoid X✝²
inst✝³⁹ : Module R✝² X✝²
Y✝² : Type ?u.155388
inst✝³⁸ : TopologicalSpace Y✝²
inst✝³⁷ : AddCommMonoid Y✝²
inst✝³⁶ : Module R✝² Y✝²
R✝¹ : Type ?u.155420
inst✝³⁵ : Semiring R✝¹
X✝¹ : Type ?u.155426
inst✝³⁴ : TopologicalSpace X✝¹
inst✝³³ : AddCommMonoid X✝¹
inst✝³² : Module R✝¹ X✝¹
Y✝¹ : Type ?u.155460
inst✝³¹ : TopologicalSpace Y✝¹
inst✝³⁰ : AddCommMonoid Y✝¹
inst✝²⁹ : Module R✝¹ Y✝¹
Z✝ : Type ?u.155492
inst✝²⁸ : TopologicalSpace Z✝
inst✝²⁷ : AddCommMonoid Z✝
inst✝²⁶ : Module R✝¹ Z✝
ι✝ : Type ?u.155524
inst✝²⁵ : Fintype ι✝
E✝ : ι✝ → Type ?u.155532
inst✝²⁴ : (i : ι✝) → TopologicalSpace (E✝ i)
inst✝²³ : (i : ι✝) → AddCommMonoid (E✝ i)
inst✝²² : (i : ι✝) → Module R✝¹ (E✝ i)
R✝ : Type ?u.155582
inst✝²¹ : Semiring R✝
X✝ : Type ?u.155588
inst✝²⁰ : TopologicalSpace X✝
inst✝¹⁹ : AddCommMonoid X✝
inst✝¹⁸ : Module R✝ X✝
Y✝ : Type ?u.155623
inst✝¹⁷ : TopologicalSpace Y✝
inst✝¹⁶ : AddCommMonoid Y✝
inst✝¹⁵ : Module R✝ Y✝
Z : Type ?u.155656
inst✝¹⁴ : TopologicalSpace Z
inst✝¹³ : AddCommMonoid Z
inst✝¹² : Module R✝ Z
ι : Type ?u.155689
inst✝¹¹ : Fintype ι
E : ι → Type ?u.155697
inst✝¹⁰ : (i : ι) → TopologicalSpace (E i)
inst✝⁹ : (i : ι) → AddCommMonoid (E i)
inst✝⁸ : (i : ι) → Module R✝ (E i)
R : Type u_1
inst✝⁷ : CommSemiring R
X : Type u_2
inst✝⁶ : TopologicalSpace X
inst✝⁵ : AddCommMonoid X
inst✝⁴ : Module R X
Y : Type u_3
inst✝³ : TopologicalSpace Y
inst✝² : Semiring Y
inst✝¹ : Algebra R Y
inst✝ : TopologicalSemiring Y
f : X → Y
hf : IsContinuousLinearMap R f
y' : Y
⊢ ∀ (x : X), f x * y' = (ContinuousLinearMap.comp (ContinuousLinearMap.mul_right y') (mk' R f hf)) x
Tactic:
simp[ContinuousLinearMap.mul_right]
Proof state after:
no goals
Theorem: SciLean.IsContinuousLinearMap.HMul.hMul.arg_a1.IsContinuousLinearMap_rule
Proof state before:
R✝² : Type ?u.167279
inst✝⁴² : Semiring R✝²
X✝² : Type ?u.167285
inst✝⁴¹ : TopologicalSpace X✝²
inst✝⁴⁰ : AddCommMonoid X✝²
inst✝³⁹ : Module R✝² X✝²
Y✝² : Type ?u.167319
inst✝³⁸ : TopologicalSpace Y✝²
inst✝³⁷ : AddCommMonoid Y✝²
inst✝³⁶ : Module R✝² Y✝²
R✝¹ : Type ?u.167351
inst✝³⁵ : Semiring R✝¹
X✝¹ : Type ?u.167357
inst✝³⁴ : TopologicalSpace X✝¹
inst✝³³ : AddCommMonoid X✝¹
inst✝³² : Module R✝¹ X✝¹
Y✝¹ : Type ?u.167391
inst✝³¹ : TopologicalSpace Y✝¹
inst✝³⁰ : AddCommMonoid Y✝¹
inst✝²⁹ : Module R✝¹ Y✝¹
Z✝ : Type ?u.167423
inst✝²⁸ : TopologicalSpace Z✝
inst✝²⁷ : AddCommMonoid Z✝
inst✝²⁶ : Module R✝¹ Z✝
ι✝ : Type ?u.167455
inst✝²⁵ : Fintype ι✝
E✝ : ι✝ → Type ?u.167463
inst✝²⁴ : (i : ι✝) → TopologicalSpace (E✝ i)
inst✝²³ : (i : ι✝) → AddCommMonoid (E✝ i)
inst✝²² : (i : ι✝) → Module R✝¹ (E✝ i)
R✝ : Type ?u.167513
inst✝²¹ : Semiring R✝
X✝ : Type ?u.167519
inst✝²⁰ : TopologicalSpace X✝
inst✝¹⁹ : AddCommMonoid X✝
inst✝¹⁸ : Module R✝ X✝
Y✝ : Type ?u.167554
inst✝¹⁷ : TopologicalSpace Y✝
inst✝¹⁶ : AddCommMonoid Y✝
inst✝¹⁵ : Module R✝ Y✝
Z : Type ?u.167587
inst✝¹⁴ : TopologicalSpace Z
inst✝¹³ : AddCommMonoid Z
inst✝¹² : Module R✝ Z
ι : Type ?u.167620
inst✝¹¹ : Fintype ι
E : ι → Type ?u.167628
inst✝¹⁰ : (i : ι) → TopologicalSpace (E i)
inst✝⁹ : (i : ι) → AddCommMonoid (E i)
inst✝⁸ : (i : ι) → Module R✝ (E i)
R : Type u_1
inst✝⁷ : CommSemiring R
X : Type u_2
inst✝⁶ : TopologicalSpace X
inst✝⁵ : AddCommMonoid X
inst✝⁴ : Module R X
Y : Type u_3
inst✝³ : TopologicalSpace Y
inst✝² : Semiring Y
inst✝¹ : Algebra R Y
inst✝ : TopologicalSemiring Y
f : X → Y
hf : IsContinuousLinearMap R f
y' : Y
⊢ ∀ (x : X), y' * f x = (ContinuousLinearMap.comp (ContinuousLinearMap.mul_left y') (mk' R f hf)) x
Tactic:
simp[ContinuousLinearMap.mul_left]
Proof state after:
no goals
Theorem: SciLean.IsContinuousLinearMap.HSMul.hSMul.arg_a0.IsContinuousLinearMap_rule
Proof state before:
R✝¹ : Type ?u.194642
inst✝³⁶ : Semiring R✝¹
X✝¹ : Type ?u.194648
inst✝³⁵ : TopologicalSpace X✝¹
inst✝³⁴ : AddCommMonoid X✝¹
inst✝³³ : Module R✝¹ X✝¹
Y✝¹ : Type ?u.194682
inst✝³² : TopologicalSpace Y✝¹
inst✝³¹ : AddCommMonoid Y✝¹
inst✝³⁰ : Module R✝¹ Y✝¹
R✝ : Type ?u.194714
inst✝²⁹ : Semiring R✝
X✝ : Type ?u.194720
inst✝²⁸ : TopologicalSpace X✝
inst✝²⁷ : AddCommMonoid X✝
inst✝²⁶ : Module R✝ X✝
Y✝ : Type ?u.194754
inst✝²⁵ : TopologicalSpace Y✝
inst✝²⁴ : AddCommMonoid Y✝
inst✝²³ : Module R✝ Y✝
Z✝ : Type ?u.194786
inst✝²² : TopologicalSpace Z✝
inst✝²¹ : AddCommMonoid Z✝
inst✝²⁰ : Module R✝ Z✝
ι✝ : Type ?u.194818
inst✝¹⁹ : Fintype ι✝
E✝ : ι✝ → Type ?u.194826
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_3
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.194950
inst✝⁸ : TopologicalSpace Z
inst✝⁷ : AddCommMonoid Z
inst✝⁶ : Module R Z
ι : Type ?u.194983
inst✝⁵ : Fintype ι
E : ι → Type ?u.194991
inst✝⁴ : (i : ι) → TopologicalSpace (E i)
inst✝³ : (i : ι) → AddCommMonoid (E i)
inst✝² : (i : ι) → Module R (E i)
inst✝¹ : TopologicalSpace R
inst✝ : ContinuousSMul R Y
f : X → R
hf : IsContinuousLinearMap R f
y : Y
⊢ ∀ (x : X), f x • y = (ContinuousLinearMap.smulRight (mk' R f hf) y) x
Tactic:
simp
Proof state after:
no goals
Theorem: SciLean.IsContinuousLinearMap.HSMul.hSMul.arg_a1.IsContinuousLinearMap_rule
Proof state before:
R✝² : Type ?u.207940
inst✝⁴² : Semiring R✝²
X✝² : Type ?u.207946
inst✝⁴¹ : TopologicalSpace X✝²
inst✝⁴⁰ : AddCommMonoid X✝²
inst✝³⁹ : Module R✝² X✝²
Y✝² : Type ?u.207980
inst✝³⁸ : TopologicalSpace Y✝²
inst✝³⁷ : AddCommMonoid Y✝²
inst✝³⁶ : Module R✝² Y✝²
R✝¹ : Type ?u.208012
inst✝³⁵ : Semiring R✝¹
X✝¹ : Type ?u.208018
inst✝³⁴ : TopologicalSpace X✝¹
inst✝³³ : AddCommMonoid X✝¹
inst✝³² : Module R✝¹ X✝¹
Y✝¹ : Type ?u.208052
inst✝³¹ : TopologicalSpace Y✝¹
inst✝³⁰ : AddCommMonoid Y✝¹
inst✝²⁹ : Module R✝¹ Y✝¹
Z✝ : Type ?u.208084
inst✝²⁸ : TopologicalSpace Z✝
inst✝²⁷ : AddCommMonoid Z✝
inst✝²⁶ : Module R✝¹ Z✝
ι✝ : Type ?u.208116
inst✝²⁵ : Fintype ι✝
E✝ : ι✝ → Type ?u.208124
inst✝²⁴ : (i : ι✝) → TopologicalSpace (E✝ i)
inst✝²³ : (i : ι✝) → AddCommMonoid (E✝ i)
inst✝²² : (i : ι✝) → Module R✝¹ (E✝ i)
R✝ : Type ?u.208174
inst✝²¹ : Semiring R✝
X✝ : Type ?u.208180
inst✝²⁰ : TopologicalSpace X✝
inst✝¹⁹ : AddCommMonoid X✝
inst✝¹⁸ : Module R✝ X✝
Y✝ : Type ?u.208215
inst✝¹⁷ : TopologicalSpace Y✝
inst✝¹⁶ : AddCommMonoid Y✝
inst✝¹⁵ : Module R✝ Y✝
Z : Type ?u.208248
inst✝¹⁴ : TopologicalSpace Z
inst✝¹³ : AddCommMonoid Z
inst✝¹² : Module R✝ Z
ι : Type ?u.208281
inst✝¹¹ : Fintype ι
E : ι → Type ?u.208289
inst✝¹⁰ : (i : ι) → TopologicalSpace (E i)
inst✝⁹ : (i : ι) → AddCommMonoid (E i)
inst✝⁸ : (i : ι) → Module R✝ (E i)
R : Type u_1
inst✝⁷ : CommSemiring 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
inst✝ : ContinuousConstSMul R Y
c : R
f : X → Y
hf : IsContinuousLinearMap R f
⊢ ∀ (x : X), c • f x = (ContinuousLinearMap.smulLeft (mk' R f hf) c) x
Tactic:
simp
Proof state after:
no goals
Theorem: SciLean.IsContinuousLinearMap.HDiv.hDiv.arg_a0.IsContinuousLinearMap_rule
Proof 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
Proof state after:
no goals
Theorem: SciLean.IsContinuousLinearMap.ite.arg_te.IsContinuousLinearMap_rule
Proof state before:
R✝¹ : Type ?u.246592
inst✝³⁴ : Semiring R✝¹
X✝¹ : Type ?u.246598
inst✝³³ : TopologicalSpace X✝¹
inst✝³² : AddCommMonoid X✝¹
inst✝³¹ : Module R✝¹ X✝¹
Y✝¹ : Type ?u.246632
inst✝³⁰ : TopologicalSpace Y✝¹
inst✝²⁹ : AddCommMonoid Y✝¹
inst✝²⁸ : Module R✝¹ Y✝¹
R✝ : Type ?u.246664
inst✝²⁷ : Semiring R✝
X✝ : Type ?u.246670
inst✝²⁶ : TopologicalSpace X✝
inst✝²⁵ : AddCommMonoid X✝
inst✝²⁴ : Module R✝ X✝
Y✝ : Type ?u.246704
inst✝²³ : TopologicalSpace Y✝
inst✝²² : AddCommMonoid Y✝
inst✝²¹ : Module R✝ Y✝
Z✝ : Type ?u.246736
inst✝²⁰ : TopologicalSpace Z✝
inst✝¹⁹ : AddCommMonoid Z✝
inst✝¹⁸ : Module R✝ Z✝
ι✝ : Type ?u.246768
inst✝¹⁷ : Fintype ι✝
E✝ : ι✝ → Type ?u.246776
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.246900
inst✝⁶ : TopologicalSpace Z
inst✝⁵ : AddCommMonoid Z
inst✝⁴ : Module R Z
ι : Type ?u.246933
inst✝³ : Fintype ι
E : ι → Type ?u.246941
inst✝² : (i : ι) → TopologicalSpace (E i)
inst✝¹ : (i : ι) → AddCommMonoid (E i)
inst✝ : (i : ι) → Module R (E i)
c : Prop
t e : X → Y
ht : IsContinuousLinearMap R t
he : IsContinuousLinearMap R e
h : c
⊢ IsContinuousLinearMap R fun x => if c then t x else e x
Tactic:
case isTrue h  => simp[h]; fun_prop
Proof state after:
no goals
Theorem: SciLean.IsContinuousLinearMap.ite.arg_te.IsContinuousLinearMap_rule
Proof state before:
R✝¹ : Type ?u.246592
inst✝³⁴ : Semiring R✝¹
X✝¹ : Type ?u.246598
inst✝³³ : TopologicalSpace X✝¹
inst✝³² : AddCommMonoid X✝¹
inst✝³¹ : Module R✝¹ X✝¹
Y✝¹ : Type ?u.246632
inst✝³⁰ : TopologicalSpace Y✝¹
inst✝²⁹ : AddCommMonoid Y✝¹
inst✝²⁸ : Module R✝¹ Y✝¹
R✝ : Type ?u.246664
inst✝²⁷ : Semiring R✝
X✝ : Type ?u.246670
inst✝²⁶ : TopologicalSpace X✝
inst✝²⁵ : AddCommMonoid X✝
inst✝²⁴ : Module R✝ X✝
Y✝ : Type ?u.246704
inst✝²³ : TopologicalSpace Y✝
inst✝²² : AddCommMonoid Y✝
inst✝²¹ : Module R✝ Y✝
Z✝ : Type ?u.246736
inst✝²⁰ : TopologicalSpace Z✝
inst✝¹⁹ : AddCommMonoid Z✝
inst✝¹⁸ : Module R✝ Z✝
ι✝ : Type ?u.246768
inst✝¹⁷ : Fintype ι✝
E✝ : ι✝ → Type ?u.246776
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.246900
inst✝⁶ : TopologicalSpace Z
inst✝⁵ : AddCommMonoid Z
inst✝⁴ : Module R Z
ι : Type ?u.246933
inst✝³ : Fintype ι
E : ι → Type ?u.246941
inst✝² : (i : ι) → TopologicalSpace (E i)
inst✝¹ : (i : ι) → AddCommMonoid (E i)
inst✝ : (i : ι) → Module R (E i)
c : Prop
t e : X → Y
ht : IsContinuousLinearMap R t
he : IsContinuousLinearMap R e
h : ¬c
⊢ IsContinuousLinearMap R fun x => if c then t x else e x
Tactic:
case isFalse h => simp[h]; fun_prop
Proof state after:
no goals
Theorem: SciLean.IsContinuousLinearMap.ite.arg_te.IsContinuousLinearMap_rule
Proof state before:
R✝¹ : Type ?u.246592
inst✝³⁴ : Semiring R✝¹
X✝¹ : Type ?u.246598
inst✝³³ : TopologicalSpace X✝¹
inst✝³² : AddCommMonoid X✝¹
inst✝³¹ : Module R✝¹ X✝¹
Y✝¹ : Type ?u.246632
inst✝³⁰ : TopologicalSpace Y✝¹
inst✝²⁹ : AddCommMonoid Y✝¹
inst✝²⁸ : Module R✝¹ Y✝¹
R✝ : Type ?u.246664
inst✝²⁷ : Semiring R✝
X✝ : Type ?u.246670
inst✝²⁶ : TopologicalSpace X✝
inst✝²⁵ : AddCommMonoid X✝
inst✝²⁴ : Module R✝ X✝
Y✝ : Type ?u.246704
inst✝²³ : TopologicalSpace Y✝
inst✝²² : AddCommMonoid Y✝
inst✝²¹ : Module R✝ Y✝
Z✝ : Type ?u.246736
inst✝²⁰ : TopologicalSpace Z✝
inst✝¹⁹ : AddCommMonoid Z✝
inst✝¹⁸ : Module R✝ Z✝
ι✝ : Type ?u.246768
inst✝¹⁷ : Fintype ι✝
E✝ : ι✝ → Type ?u.246776
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.246900
inst✝⁶ : TopologicalSpace Z
inst✝⁵ : AddCommMonoid Z
inst✝⁴ : Module R Z
ι : Type ?u.246933
inst✝³ : Fintype ι
E : ι → Type ?u.246941
inst✝² : (i : ι) → TopologicalSpace (E i)
inst✝¹ : (i : ι) → AddCommMonoid (E i)
inst✝ : (i : ι) → Module R (E i)
c : Prop
t e : X → Y
ht : IsContinuousLinearMap R t
he : IsContinuousLinearMap R e
h : c
⊢ IsContinuousLinearMap R fun x => if c then t x else e x
Tactic:
simp[h]
Proof state after:
R✝¹ : Type ?u.246592
inst✝³⁴ : Semiring R✝¹
X✝¹ : Type ?u.246598
inst✝³³ : TopologicalSpace X✝¹
inst✝³² : AddCommMonoid X✝¹
inst✝³¹ : Module R✝¹ X✝¹
Y✝¹ : Type ?u.246632
inst✝³⁰ : TopologicalSpace Y✝¹
inst✝²⁹ : AddCommMonoid Y✝¹
inst✝²⁸ : Module R✝¹ Y✝¹
R✝ : Type ?u.246664
inst✝²⁷ : Semiring R✝
X✝ : Type ?u.246670
inst✝²⁶ : TopologicalSpace X✝
inst✝²⁵ : AddCommMonoid X✝
inst✝²⁴ : Module R✝ X✝
Y✝ : Type ?u.246704
inst✝²³ : TopologicalSpace Y✝
inst✝²² : AddCommMonoid Y✝
inst✝²¹ : Module R✝ Y✝
Z✝ : Type ?u.246736
inst✝²⁰ : TopologicalSpace Z✝
inst✝¹⁹ : AddCommMonoid Z✝
inst✝¹⁸ : Module R✝ Z✝
ι✝ : Type ?u.246768
inst✝¹⁷ : Fintype ι✝
E✝ : ι✝ → Type ?u.246776
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.246900
inst✝⁶ : TopologicalSpace Z
inst✝⁵ : AddCommMonoid Z
inst✝⁴ : Module R Z
ι : Type ?u.246933
inst✝³ : Fintype ι
E : ι → Type ?u.246941
inst✝² : (i : ι) → TopologicalSpace (E i)
inst✝¹ : (i : ι) → AddCommMonoid (E i)
inst✝ : (i : ι) → Module R (E i)
c : Prop
t e : X → Y
ht : IsContinuousLinearMap R t
he : IsContinuousLinearMap R e
h : c
⊢ IsContinuousLinearMap R fun x => t x