internlm/Lean-Github huggingface dataset:
Theorem: HasDerivAt.of_deriv
Proof state before:
𝕜 : Type u_1
𝕜' : Type u_2
F : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NontriviallyNormedField 𝕜'
inst✝⁴ : NormedAlgebra 𝕜 𝕜'
inst✝³ : NontriviallyNormedField F
inst✝² : NormedAlgebra 𝕜 F
inst✝¹ : NormedAlgebra 𝕜' F
inst✝ : IsScalarTower 𝕜 𝕜' F
x : 𝕜
f f' : 𝕜 → F
h : DifferentiableAt 𝕜 f x
h' : _root_.deriv f x = f' x
⊢ HasDerivAt f (_root_.deriv f x) x
Tactic:
exact h.hasDerivAt
Proof state after:
no goals
Theorem: HasDerivAt.comp_of_deriv
Proof state before:
𝕜 : Type u_1
𝕜' : Type u_2
F : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NontriviallyNormedField 𝕜'
inst✝⁴ : NormedAlgebra 𝕜 𝕜'
inst✝³ : NontriviallyNormedField F
inst✝² : NormedAlgebra 𝕜 F
inst✝¹ : NormedAlgebra 𝕜' F
inst✝ : IsScalarTower 𝕜 𝕜' F
x : 𝕜
f : 𝕜' → F
g : 𝕜 → 𝕜'
fg' : 𝕜 → F
hf : DifferentiableAt 𝕜 f (g x)
hg : DifferentiableAt 𝕜 g x
hf' : _root_.deriv (fun x => f (g x)) x = fg' x
⊢ HasDerivAt (fun x => f (g x)) (fg' x) x
Tactic:
rw [← hf']
Proof state after:
𝕜 : Type u_1
𝕜' : Type u_2
F : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NontriviallyNormedField 𝕜'
inst✝⁴ : NormedAlgebra 𝕜 𝕜'
inst✝³ : NontriviallyNormedField F
inst✝² : NormedAlgebra 𝕜 F
inst✝¹ : NormedAlgebra 𝕜' F
inst✝ : IsScalarTower 𝕜 𝕜' F
x : 𝕜
f : 𝕜' → F
g : 𝕜 → 𝕜'
fg' : 𝕜 → F
hf : DifferentiableAt 𝕜 f (g x)
hg : DifferentiableAt 𝕜 g x
hf' : _root_.deriv (fun x => f (g x)) x = fg' x
⊢ HasDerivAt (fun x => f (g x)) (_root_.deriv (fun x => f (g x)) x) x
Theorem: HasDerivAt.comp_of_deriv
Proof state before:
𝕜 : Type u_1
𝕜' : Type u_2
F : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NontriviallyNormedField 𝕜'
inst✝⁴ : NormedAlgebra 𝕜 𝕜'
inst✝³ : NontriviallyNormedField F
inst✝² : NormedAlgebra 𝕜 F
inst✝¹ : NormedAlgebra 𝕜' F
inst✝ : IsScalarTower 𝕜 𝕜' F
x : 𝕜
f : 𝕜' → F
g : 𝕜 → 𝕜'
fg' : 𝕜 → F
hf : DifferentiableAt 𝕜 f (g x)
hg : DifferentiableAt 𝕜 g x
hf' : _root_.deriv (fun x => f (g x)) x = fg' x
⊢ HasDerivAt (fun x => f (g x)) (_root_.deriv (fun x => f (g x)) x) x
Tactic:
refine DifferentiableAt.hasDerivAt ?_
Proof state after:
𝕜 : Type u_1
𝕜' : Type u_2
F : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NontriviallyNormedField 𝕜'
inst✝⁴ : NormedAlgebra 𝕜 𝕜'
inst✝³ : NontriviallyNormedField F
inst✝² : NormedAlgebra 𝕜 F
inst✝¹ : NormedAlgebra 𝕜' F
inst✝ : IsScalarTower 𝕜 𝕜' F
x : 𝕜
f : 𝕜' → F
g : 𝕜 → 𝕜'
fg' : 𝕜 → F
hf : DifferentiableAt 𝕜 f (g x)
hg : DifferentiableAt 𝕜 g x
hf' : _root_.deriv (fun x => f (g x)) x = fg' x
⊢ DifferentiableAt 𝕜 (fun x => f (g x)) x
Theorem: HasDerivAt.comp_of_deriv
Proof state before:
𝕜 : Type u_1
𝕜' : Type u_2
F : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NontriviallyNormedField 𝕜'
inst✝⁴ : NormedAlgebra 𝕜 𝕜'
inst✝³ : NontriviallyNormedField F
inst✝² : NormedAlgebra 𝕜 F
inst✝¹ : NormedAlgebra 𝕜' F
inst✝ : IsScalarTower 𝕜 𝕜' F
x : 𝕜
f : 𝕜' → F
g : 𝕜 → 𝕜'
fg' : 𝕜 → F
hf : DifferentiableAt 𝕜 f (g x)
hg : DifferentiableAt 𝕜 g x
hf' : _root_.deriv (fun x => f (g x)) x = fg' x
⊢ DifferentiableAt 𝕜 (fun x => f (g x)) x
Tactic:
exact DifferentiableAt.comp x hf hg
Proof state after:
no goals
Theorem: HasDerivAt.comp_of_deriv'
Proof state before:
𝕜 : Type u_1
𝕜' : Type u_2
F : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NontriviallyNormedField 𝕜'
inst✝⁴ : NormedAlgebra 𝕜 𝕜'
inst✝³ : NontriviallyNormedField F
inst✝² : NormedAlgebra 𝕜 F
inst✝¹ : NormedAlgebra 𝕜' F
inst✝ : IsScalarTower 𝕜 𝕜' F
x : 𝕜
f : 𝕜' → F
g : 𝕜 → 𝕜'
fg' : 𝕜 → F
hf : DifferentiableAt 𝕜' f (g x)
hg : DifferentiableAt 𝕜 g x
hf' : _root_.deriv g x • _root_.deriv f (g x) = fg' x
⊢ HasDerivAt (fun x => f (g x)) (fg' x) x
Tactic:
rw [← hf']
Proof state after:
𝕜 : Type u_1
𝕜' : Type u_2
F : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NontriviallyNormedField 𝕜'
inst✝⁴ : NormedAlgebra 𝕜 𝕜'
inst✝³ : NontriviallyNormedField F
inst✝² : NormedAlgebra 𝕜 F
inst✝¹ : NormedAlgebra 𝕜' F
inst✝ : IsScalarTower 𝕜 𝕜' F
x : 𝕜
f : 𝕜' → F
g : 𝕜 → 𝕜'
fg' : 𝕜 → F
hf : DifferentiableAt 𝕜' f (g x)
hg : DifferentiableAt 𝕜 g x
hf' : _root_.deriv g x • _root_.deriv f (g x) = fg' x
⊢ HasDerivAt (fun x => f (g x)) (_root_.deriv g x • _root_.deriv f (g x)) x
Theorem: HasDerivAt.comp_of_deriv'
Proof state before:
𝕜 : Type u_1
𝕜' : Type u_2
F : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NontriviallyNormedField 𝕜'
inst✝⁴ : NormedAlgebra 𝕜 𝕜'
inst✝³ : NontriviallyNormedField F
inst✝² : NormedAlgebra 𝕜 F
inst✝¹ : NormedAlgebra 𝕜' F
inst✝ : IsScalarTower 𝕜 𝕜' F
x : 𝕜
f : 𝕜' → F
g : 𝕜 → 𝕜'
fg' : 𝕜 → F
hf : DifferentiableAt 𝕜' f (g x)
hg : DifferentiableAt 𝕜 g x
hf' : _root_.deriv g x • _root_.deriv f (g x) = fg' x
⊢ HasDerivAt (fun x => f (g x)) (_root_.deriv g x • _root_.deriv f (g x)) x
Tactic:
exact comp_of_tower x hf.hasDerivAt hg.hasDerivAt
Proof state after:
no goals
Theorem: HasDerivAt.bilin
Proof state before:
𝕜 : Type u_1
S : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝¹⁸ : NontriviallyNormedField 𝕜
inst✝¹⁷ : NormedAddCommGroup E
inst✝¹⁶ : NormedSpace ℝ E
inst✝¹⁵ : NormedSpace 𝕜 E
inst✝¹⁴ : NormedAddCommGroup F
inst✝¹³ : NormedSpace ℝ F
inst✝¹² : NormedSpace 𝕜 F
inst✝¹¹ : NormedAddCommGroup G
inst✝¹⁰ : NormedSpace ℝ G
inst✝⁹ : NormedSpace 𝕜 G
inst✝⁸ : CompleteSpace G
inst✝⁷ : NontriviallyNormedField S
inst✝⁶ : NormedSpace S G
inst✝⁵ : NormedSpace ℝ S
inst✝⁴ : SMulCommClass ℝ S G
inst✝³ : IsScalarTower ℝ S G
inst✝² : NormedSpace 𝕜 S
inst✝¹ : SMulCommClass 𝕜 S G
inst✝ : IsScalarTower 𝕜 S G
u : 𝕜 → E
u' : E
v : 𝕜 → F
v' : F
B : E →L[𝕜] F →L[𝕜] G
x : 𝕜
hu : HasDerivAt u u' x
hv : HasDerivAt v v' x
⊢ HasDerivAt (fun x => (B (u x)) (v x)) ((B u') (v x) + (B (u x)) v') x
Tactic:
rw [hasDerivAt_iff_hasFDerivAt] at hu hv ⊢
Proof state after:
𝕜 : Type u_1
S : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝¹⁸ : NontriviallyNormedField 𝕜
inst✝¹⁷ : NormedAddCommGroup E
inst✝¹⁶ : NormedSpace ℝ E
inst✝¹⁵ : NormedSpace 𝕜 E
inst✝¹⁴ : NormedAddCommGroup F
inst✝¹³ : NormedSpace ℝ F
inst✝¹² : NormedSpace 𝕜 F
inst✝¹¹ : NormedAddCommGroup G
inst✝¹⁰ : NormedSpace ℝ G
inst✝⁹ : NormedSpace 𝕜 G
inst✝⁸ : CompleteSpace G
inst✝⁷ : NontriviallyNormedField S
inst✝⁶ : NormedSpace S G
inst✝⁵ : NormedSpace ℝ S
inst✝⁴ : SMulCommClass ℝ S G
inst✝³ : IsScalarTower ℝ S G
inst✝² : NormedSpace 𝕜 S
inst✝¹ : SMulCommClass 𝕜 S G
inst✝ : IsScalarTower 𝕜 S G
u : 𝕜 → E
u' : E
v : 𝕜 → F
v' : F
B : E →L[𝕜] F →L[𝕜] G
x : 𝕜
hu : HasFDerivAt u (ContinuousLinearMap.smulRight 1 u') x
hv : HasFDerivAt v (ContinuousLinearMap.smulRight 1 v') x
⊢ HasFDerivAt (fun x => (B (u x)) (v x)) (ContinuousLinearMap.smulRight 1 ((B u') (v x) + (B (u x)) v')) x
Theorem: HasDerivAt.bilin
Proof state before:
𝕜 : Type u_1
S : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝¹⁸ : NontriviallyNormedField 𝕜
inst✝¹⁷ : NormedAddCommGroup E
inst✝¹⁶ : NormedSpace ℝ E
inst✝¹⁵ : NormedSpace 𝕜 E
inst✝¹⁴ : NormedAddCommGroup F
inst✝¹³ : NormedSpace ℝ F
inst✝¹² : NormedSpace 𝕜 F
inst✝¹¹ : NormedAddCommGroup G
inst✝¹⁰ : NormedSpace ℝ G
inst✝⁹ : NormedSpace 𝕜 G
inst✝⁸ : CompleteSpace G
inst✝⁷ : NontriviallyNormedField S
inst✝⁶ : NormedSpace S G
inst✝⁵ : NormedSpace ℝ S
inst✝⁴ : SMulCommClass ℝ S G
inst✝³ : IsScalarTower ℝ S G
inst✝² : NormedSpace 𝕜 S
inst✝¹ : SMulCommClass 𝕜 S G
inst✝ : IsScalarTower 𝕜 S G
u : 𝕜 → E
u' : E
v : 𝕜 → F
v' : F
B : E →L[𝕜] F →L[𝕜] G
x : 𝕜
hu : HasFDerivAt u (ContinuousLinearMap.smulRight 1 u') x
hv : HasFDerivAt v (ContinuousLinearMap.smulRight 1 v') x
⊢ HasFDerivAt (fun x => (B (u x)) (v x)) (ContinuousLinearMap.smulRight 1 ((B u') (v x) + (B (u x)) v')) x
Tactic:
refine (ContinuousLinearMap.hasFDerivAt_of_bilinear B hu hv).congr_fderiv ?_
Proof state after:
𝕜 : Type u_1
S : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝¹⁸ : NontriviallyNormedField 𝕜
inst✝¹⁷ : NormedAddCommGroup E
inst✝¹⁶ : NormedSpace ℝ E
inst✝¹⁵ : NormedSpace 𝕜 E
inst✝¹⁴ : NormedAddCommGroup F
inst✝¹³ : NormedSpace ℝ F
inst✝¹² : NormedSpace 𝕜 F
inst✝¹¹ : NormedAddCommGroup G
inst✝¹⁰ : NormedSpace ℝ G
inst✝⁹ : NormedSpace 𝕜 G
inst✝⁸ : CompleteSpace G
inst✝⁷ : NontriviallyNormedField S
inst✝⁶ : NormedSpace S G
inst✝⁵ : NormedSpace ℝ S
inst✝⁴ : SMulCommClass ℝ S G
inst✝³ : IsScalarTower ℝ S G
inst✝² : NormedSpace 𝕜 S
inst✝¹ : SMulCommClass 𝕜 S G
inst✝ : IsScalarTower 𝕜 S G
u : 𝕜 → E
u' : E
v : 𝕜 → F
v' : F
B : E →L[𝕜] F →L[𝕜] G
x : 𝕜
hu : HasFDerivAt u (ContinuousLinearMap.smulRight 1 u') x
hv : HasFDerivAt v (ContinuousLinearMap.smulRight 1 v') x
⊢ ((ContinuousLinearMap.precompR 𝕜 B) (u x)) (ContinuousLinearMap.smulRight 1 v') +
      ((ContinuousLinearMap.precompL 𝕜 B) (ContinuousLinearMap.smulRight 1 u')) (v x) =
    ContinuousLinearMap.smulRight 1 ((B u') (v x) + (B (u x)) v')
Theorem: HasDerivAt.bilin
Proof state before:
𝕜 : Type u_1
S : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝¹⁸ : NontriviallyNormedField 𝕜
inst✝¹⁷ : NormedAddCommGroup E
inst✝¹⁶ : NormedSpace ℝ E
inst✝¹⁵ : NormedSpace 𝕜 E
inst✝¹⁴ : NormedAddCommGroup F
inst✝¹³ : NormedSpace ℝ F
inst✝¹² : NormedSpace 𝕜 F
inst✝¹¹ : NormedAddCommGroup G
inst✝¹⁰ : NormedSpace ℝ G
inst✝⁹ : NormedSpace 𝕜 G
inst✝⁸ : CompleteSpace G
inst✝⁷ : NontriviallyNormedField S
inst✝⁶ : NormedSpace S G
inst✝⁵ : NormedSpace ℝ S
inst✝⁴ : SMulCommClass ℝ S G
inst✝³ : IsScalarTower ℝ S G
inst✝² : NormedSpace 𝕜 S
inst✝¹ : SMulCommClass 𝕜 S G
inst✝ : IsScalarTower 𝕜 S G
u : 𝕜 → E
u' : E
v : 𝕜 → F
v' : F
B : E →L[𝕜] F →L[𝕜] G
x : 𝕜
hu : HasFDerivAt u (ContinuousLinearMap.smulRight 1 u') x
hv : HasFDerivAt v (ContinuousLinearMap.smulRight 1 v') x
⊢ ((ContinuousLinearMap.precompR 𝕜 B) (u x)) (ContinuousLinearMap.smulRight 1 v') +
      ((ContinuousLinearMap.precompL 𝕜 B) (ContinuousLinearMap.smulRight 1 u')) (v x) =
    ContinuousLinearMap.smulRight 1 ((B u') (v x) + (B (u x)) v')
Tactic:
refine ContinuousLinearMap.ext ?_
Proof state after:
𝕜 : Type u_1
S : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝¹⁸ : NontriviallyNormedField 𝕜
inst✝¹⁷ : NormedAddCommGroup E
inst✝¹⁶ : NormedSpace ℝ E
inst✝¹⁵ : NormedSpace 𝕜 E
inst✝¹⁴ : NormedAddCommGroup F
inst✝¹³ : NormedSpace ℝ F
inst✝¹² : NormedSpace 𝕜 F
inst✝¹¹ : NormedAddCommGroup G
inst✝¹⁰ : NormedSpace ℝ G
inst✝⁹ : NormedSpace 𝕜 G
inst✝⁸ : CompleteSpace G
inst✝⁷ : NontriviallyNormedField S
inst✝⁶ : NormedSpace S G
inst✝⁵ : NormedSpace ℝ S
inst✝⁴ : SMulCommClass ℝ S G
inst✝³ : IsScalarTower ℝ S G
inst✝² : NormedSpace 𝕜 S
inst✝¹ : SMulCommClass 𝕜 S G
inst✝ : IsScalarTower 𝕜 S G
u : 𝕜 → E
u' : E
v : 𝕜 → F
v' : F
B : E →L[𝕜] F →L[𝕜] G
x : 𝕜
hu : HasFDerivAt u (ContinuousLinearMap.smulRight 1 u') x
hv : HasFDerivAt v (ContinuousLinearMap.smulRight 1 v') x
⊢ ∀ (x_1 : 𝕜),
    (((ContinuousLinearMap.precompR 𝕜 B) (u x)) (ContinuousLinearMap.smulRight 1 v') +
          ((ContinuousLinearMap.precompL 𝕜 B) (ContinuousLinearMap.smulRight 1 u')) (v x))
        x_1 =
      (ContinuousLinearMap.smulRight 1 ((B u') (v x) + (B (u x)) v')) x_1
Theorem: HasDerivAt.bilin
Proof state before:
𝕜 : Type u_1
S : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝¹⁸ : NontriviallyNormedField 𝕜
inst✝¹⁷ : NormedAddCommGroup E
inst✝¹⁶ : NormedSpace ℝ E
inst✝¹⁵ : NormedSpace 𝕜 E
inst✝¹⁴ : NormedAddCommGroup F
inst✝¹³ : NormedSpace ℝ F
inst✝¹² : NormedSpace 𝕜 F
inst✝¹¹ : NormedAddCommGroup G
inst✝¹⁰ : NormedSpace ℝ G
inst✝⁹ : NormedSpace 𝕜 G
inst✝⁸ : CompleteSpace G
inst✝⁷ : NontriviallyNormedField S
inst✝⁶ : NormedSpace S G
inst✝⁵ : NormedSpace ℝ S
inst✝⁴ : SMulCommClass ℝ S G
inst✝³ : IsScalarTower ℝ S G
inst✝² : NormedSpace 𝕜 S
inst✝¹ : SMulCommClass 𝕜 S G
inst✝ : IsScalarTower 𝕜 S G
u : 𝕜 → E
u' : E
v : 𝕜 → F
v' : F
B : E →L[𝕜] F →L[𝕜] G
x : 𝕜
hu : HasFDerivAt u (ContinuousLinearMap.smulRight 1 u') x
hv : HasFDerivAt v (ContinuousLinearMap.smulRight 1 v') x
⊢ ∀ (x_1 : 𝕜),
    (((ContinuousLinearMap.precompR 𝕜 B) (u x)) (ContinuousLinearMap.smulRight 1 v') +
          ((ContinuousLinearMap.precompL 𝕜 B) (ContinuousLinearMap.smulRight 1 u')) (v x))
        x_1 =
      (ContinuousLinearMap.smulRight 1 ((B u') (v x) + (B (u x)) v')) x_1
Tactic:
intro dx
Proof state after:
𝕜 : Type u_1
S : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝¹⁸ : NontriviallyNormedField 𝕜
inst✝¹⁷ : NormedAddCommGroup E
inst✝¹⁶ : NormedSpace ℝ E
inst✝¹⁵ : NormedSpace 𝕜 E
inst✝¹⁴ : NormedAddCommGroup F
inst✝¹³ : NormedSpace ℝ F
inst✝¹² : NormedSpace 𝕜 F
inst✝¹¹ : NormedAddCommGroup G
inst✝¹⁰ : NormedSpace ℝ G
inst✝⁹ : NormedSpace 𝕜 G
inst✝⁸ : CompleteSpace G
inst✝⁷ : NontriviallyNormedField S
inst✝⁶ : NormedSpace S G
inst✝⁵ : NormedSpace ℝ S
inst✝⁴ : SMulCommClass ℝ S G
inst✝³ : IsScalarTower ℝ S G
inst✝² : NormedSpace 𝕜 S
inst✝¹ : SMulCommClass 𝕜 S G
inst✝ : IsScalarTower 𝕜 S G
u : 𝕜 → E
u' : E
v : 𝕜 → F
v' : F
B : E →L[𝕜] F →L[𝕜] G
x : 𝕜
hu : HasFDerivAt u (ContinuousLinearMap.smulRight 1 u') x
hv : HasFDerivAt v (ContinuousLinearMap.smulRight 1 v') x
dx : 𝕜
⊢ (((ContinuousLinearMap.precompR 𝕜 B) (u x)) (ContinuousLinearMap.smulRight 1 v') +
        ((ContinuousLinearMap.precompL 𝕜 B) (ContinuousLinearMap.smulRight 1 u')) (v x))
      dx =
    (ContinuousLinearMap.smulRight 1 ((B u') (v x) + (B (u x)) v')) dx
Theorem: HasDerivAt.bilin
Proof state before:
𝕜 : Type u_1
S : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝¹⁸ : NontriviallyNormedField 𝕜
inst✝¹⁷ : NormedAddCommGroup E
inst✝¹⁶ : NormedSpace ℝ E
inst✝¹⁵ : NormedSpace 𝕜 E
inst✝¹⁴ : NormedAddCommGroup F
inst✝¹³ : NormedSpace ℝ F
inst✝¹² : NormedSpace 𝕜 F
inst✝¹¹ : NormedAddCommGroup G
inst✝¹⁰ : NormedSpace ℝ G
inst✝⁹ : NormedSpace 𝕜 G
inst✝⁸ : CompleteSpace G
inst✝⁷ : NontriviallyNormedField S
inst✝⁶ : NormedSpace S G
inst✝⁵ : NormedSpace ℝ S
inst✝⁴ : SMulCommClass ℝ S G
inst✝³ : IsScalarTower ℝ S G
inst✝² : NormedSpace 𝕜 S
inst✝¹ : SMulCommClass 𝕜 S G
inst✝ : IsScalarTower 𝕜 S G
u : 𝕜 → E
u' : E
v : 𝕜 → F
v' : F
B : E →L[𝕜] F →L[𝕜] G
x : 𝕜
hu : HasFDerivAt u (ContinuousLinearMap.smulRight 1 u') x
hv : HasFDerivAt v (ContinuousLinearMap.smulRight 1 v') x
dx : 𝕜
⊢ (((ContinuousLinearMap.precompR 𝕜 B) (u x)) (ContinuousLinearMap.smulRight 1 v') +
        ((ContinuousLinearMap.precompL 𝕜 B) (ContinuousLinearMap.smulRight 1 u')) (v x))
      dx =
    (ContinuousLinearMap.smulRight 1 ((B u') (v x) + (B (u x)) v')) dx
Tactic:
simp [ContinuousLinearMap.precompL]
Proof state after:
𝕜 : Type u_1
S : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝¹⁸ : NontriviallyNormedField 𝕜
inst✝¹⁷ : NormedAddCommGroup E
inst✝¹⁶ : NormedSpace ℝ E
inst✝¹⁵ : NormedSpace 𝕜 E
inst✝¹⁴ : NormedAddCommGroup F
inst✝¹³ : NormedSpace ℝ F
inst✝¹² : NormedSpace 𝕜 F
inst✝¹¹ : NormedAddCommGroup G
inst✝¹⁰ : NormedSpace ℝ G
inst✝⁹ : NormedSpace 𝕜 G
inst✝⁸ : CompleteSpace G
inst✝⁷ : NontriviallyNormedField S
inst✝⁶ : NormedSpace S G
inst✝⁵ : NormedSpace ℝ S
inst✝⁴ : SMulCommClass ℝ S G
inst✝³ : IsScalarTower ℝ S G
inst✝² : NormedSpace 𝕜 S
inst✝¹ : SMulCommClass 𝕜 S G
inst✝ : IsScalarTower 𝕜 S G
u : 𝕜 → E
u' : E
v : 𝕜 → F
v' : F
B : E →L[𝕜] F →L[𝕜] G
x : 𝕜
hu : HasFDerivAt u (ContinuousLinearMap.smulRight 1 u') x
hv : HasFDerivAt v (ContinuousLinearMap.smulRight 1 v') x
dx : 𝕜
⊢ dx • (B (u x)) v' + dx • (B u') (v x) = dx • (B u') (v x) + dx • (B (u x)) v'
Theorem: HasDerivAt.bilin
Proof state before:
𝕜 : Type u_1
S : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝¹⁸ : NontriviallyNormedField 𝕜
inst✝¹⁷ : NormedAddCommGroup E
inst✝¹⁶ : NormedSpace ℝ E
inst✝¹⁵ : NormedSpace 𝕜 E
inst✝¹⁴ : NormedAddCommGroup F
inst✝¹³ : NormedSpace ℝ F
inst✝¹² : NormedSpace 𝕜 F
inst✝¹¹ : NormedAddCommGroup G
inst✝¹⁰ : NormedSpace ℝ G
inst✝⁹ : NormedSpace 𝕜 G
inst✝⁸ : CompleteSpace G
inst✝⁷ : NontriviallyNormedField S
inst✝⁶ : NormedSpace S G
inst✝⁵ : NormedSpace ℝ S
inst✝⁴ : SMulCommClass ℝ S G
inst✝³ : IsScalarTower ℝ S G
inst✝² : NormedSpace 𝕜 S
inst✝¹ : SMulCommClass 𝕜 S G
inst✝ : IsScalarTower 𝕜 S G
u : 𝕜 → E
u' : E
v : 𝕜 → F
v' : F
B : E →L[𝕜] F →L[𝕜] G
x : 𝕜
hu : HasFDerivAt u (ContinuousLinearMap.smulRight 1 u') x
hv : HasFDerivAt v (ContinuousLinearMap.smulRight 1 v') x
dx : 𝕜
⊢ dx • (B (u x)) v' + dx • (B u') (v x) = dx • (B u') (v x) + dx • (B (u x)) v'
Tactic:
rw [add_comm]
Proof state after:
no goals
Theorem: intervalIntegral.integral_deriv_bilin_eq_sub
Proof state before:
𝕜 : Type u_1
S : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝¹⁸ : NontriviallyNormedField 𝕜
inst✝¹⁷ : NormedAddCommGroup E
inst✝¹⁶ : NormedSpace ℝ E
inst✝¹⁵ : NormedSpace 𝕜 E
inst✝¹⁴ : NormedAddCommGroup F
inst✝¹³ : NormedSpace ℝ F
inst✝¹² : NormedSpace 𝕜 F
inst✝¹¹ : NormedAddCommGroup G
inst✝¹⁰ : NormedSpace ℝ G
inst✝⁹ : NormedSpace 𝕜 G
inst✝⁸ : CompleteSpace G
inst✝⁷ : NontriviallyNormedField S
inst✝⁶ : NormedSpace S G
inst✝⁵ : NormedSpace ℝ S
inst✝⁴ : SMulCommClass ℝ S G
inst✝³ : IsScalarTower ℝ S G
inst✝² : NormedSpace 𝕜 S
inst✝¹ : SMulCommClass 𝕜 S G
inst✝ : IsScalarTower 𝕜 S G
a b : ℝ
u u' : ℝ → E
v v' : ℝ → F
B : E →L[ℝ] F →L[ℝ] G
hu : ∀ x ∈ Set.uIcc a b, HasDerivAt u (u' x) x
hv : ∀ x ∈ Set.uIcc a b, HasDerivAt v (v' x) x
hu' : ContinuousOn u' (Set.uIcc a b)
hv' : ContinuousOn v' (Set.uIcc a b)
⊢ ∫ (x : ℝ) in a..b, (B (u' x)) (v x) + (B (u x)) (v' x) = (B (u b)) (v b) - (B (u a)) (v a)
Tactic:
refine integral_eq_sub_of_hasDerivAt (fun x hx => HasDerivAt.bilin B (hu x hx) (hv x hx)) ?_
Proof state after:
𝕜 : Type u_1
S : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝¹⁸ : NontriviallyNormedField 𝕜
inst✝¹⁷ : NormedAddCommGroup E
inst✝¹⁶ : NormedSpace ℝ E
inst✝¹⁵ : NormedSpace 𝕜 E
inst✝¹⁴ : NormedAddCommGroup F
inst✝¹³ : NormedSpace ℝ F
inst✝¹² : NormedSpace 𝕜 F
inst✝¹¹ : NormedAddCommGroup G
inst✝¹⁰ : NormedSpace ℝ G
inst✝⁹ : NormedSpace 𝕜 G
inst✝⁸ : CompleteSpace G
inst✝⁷ : NontriviallyNormedField S
inst✝⁶ : NormedSpace S G
inst✝⁵ : NormedSpace ℝ S
inst✝⁴ : SMulCommClass ℝ S G
inst✝³ : IsScalarTower ℝ S G
inst✝² : NormedSpace 𝕜 S
inst✝¹ : SMulCommClass 𝕜 S G
inst✝ : IsScalarTower 𝕜 S G
a b : ℝ
u u' : ℝ → E
v v' : ℝ → F
B : E →L[ℝ] F →L[ℝ] G
hu : ∀ x ∈ Set.uIcc a b, HasDerivAt u (u' x) x
hv : ∀ x ∈ Set.uIcc a b, HasDerivAt v (v' x) x
hu' : ContinuousOn u' (Set.uIcc a b)
hv' : ContinuousOn v' (Set.uIcc a b)
⊢ IntervalIntegrable (fun x => (B (u' x)) (v x) + (B (u x)) (v' x)) volume a b
Theorem: intervalIntegral.integral_deriv_bilin_eq_sub
Proof state before:
𝕜 : Type u_1
S : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝¹⁸ : NontriviallyNormedField 𝕜
inst✝¹⁷ : NormedAddCommGroup E
inst✝¹⁶ : NormedSpace ℝ E
inst✝¹⁵ : NormedSpace 𝕜 E
inst✝¹⁴ : NormedAddCommGroup F
inst✝¹³ : NormedSpace ℝ F
inst✝¹² : NormedSpace 𝕜 F
inst✝¹¹ : NormedAddCommGroup G
inst✝¹⁰ : NormedSpace ℝ G
inst✝⁹ : NormedSpace 𝕜 G
inst✝⁸ : CompleteSpace G
inst✝⁷ : NontriviallyNormedField S
inst✝⁶ : NormedSpace S G
inst✝⁵ : NormedSpace ℝ S
inst✝⁴ : SMulCommClass ℝ S G
inst✝³ : IsScalarTower ℝ S G
inst✝² : NormedSpace 𝕜 S
inst✝¹ : SMulCommClass 𝕜 S G
inst✝ : IsScalarTower 𝕜 S G
a b : ℝ
u u' : ℝ → E
v v' : ℝ → F
B : E →L[ℝ] F →L[ℝ] G
hu : ∀ x ∈ Set.uIcc a b, HasDerivAt u (u' x) x
hv : ∀ x ∈ Set.uIcc a b, HasDerivAt v (v' x) x
hu' : ContinuousOn u' (Set.uIcc a b)
hv' : ContinuousOn v' (Set.uIcc a b)
⊢ IntervalIntegrable (fun x => (B (u' x)) (v x) + (B (u x)) (v' x)) volume a b
Tactic:
refine (ContinuousOn.add ?_ ?_).intervalIntegrable
Proof state after:
case refine_1
𝕜 : Type u_1
S : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝¹⁸ : NontriviallyNormedField 𝕜
inst✝¹⁷ : NormedAddCommGroup E
inst✝¹⁶ : NormedSpace ℝ E
inst✝¹⁵ : NormedSpace 𝕜 E
inst✝¹⁴ : NormedAddCommGroup F
inst✝¹³ : NormedSpace ℝ F
inst✝¹² : NormedSpace 𝕜 F
inst✝¹¹ : NormedAddCommGroup G
inst✝¹⁰ : NormedSpace ℝ G
inst✝⁹ : NormedSpace 𝕜 G
inst✝⁸ : CompleteSpace G
inst✝⁷ : NontriviallyNormedField S
inst✝⁶ : NormedSpace S G
inst✝⁵ : NormedSpace ℝ S
inst✝⁴ : SMulCommClass ℝ S G
inst✝³ : IsScalarTower ℝ S G
inst✝² : NormedSpace 𝕜 S
inst✝¹ : SMulCommClass 𝕜 S G
inst✝ : IsScalarTower 𝕜 S G
a b : ℝ
u u' : ℝ → E
v v' : ℝ → F
B : E →L[ℝ] F →L[ℝ] G
hu : ∀ x ∈ Set.uIcc a b, HasDerivAt u (u' x) x
hv : ∀ x ∈ Set.uIcc a b, HasDerivAt v (v' x) x
hu' : ContinuousOn u' (Set.uIcc a b)
hv' : ContinuousOn v' (Set.uIcc a b)
⊢ ContinuousOn (fun x => (B (u' x)) (v x)) (Set.uIcc a b)

case refine_2
𝕜 : Type u_1
S : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝¹⁸ : NontriviallyNormedField 𝕜
inst✝¹⁷ : NormedAddCommGroup E
inst✝¹⁶ : NormedSpace ℝ E
inst✝¹⁵ : NormedSpace 𝕜 E
inst✝¹⁴ : NormedAddCommGroup F
inst✝¹³ : NormedSpace ℝ F
inst✝¹² : NormedSpace 𝕜 F
inst✝¹¹ : NormedAddCommGroup G
inst✝¹⁰ : NormedSpace ℝ G
inst✝⁹ : NormedSpace 𝕜 G
inst✝⁸ : CompleteSpace G
inst✝⁷ : NontriviallyNormedField S
inst✝⁶ : NormedSpace S G
inst✝⁵ : NormedSpace ℝ S
inst✝⁴ : SMulCommClass ℝ S G
inst✝³ : IsScalarTower ℝ S G
inst✝² : NormedSpace 𝕜 S
inst✝¹ : SMulCommClass 𝕜 S G
inst✝ : IsScalarTower 𝕜 S G
a b : ℝ
u u' : ℝ → E
v v' : ℝ → F
B : E →L[ℝ] F →L[ℝ] G
hu : ∀ x ∈ Set.uIcc a b, HasDerivAt u (u' x) x
hv : ∀ x ∈ Set.uIcc a b, HasDerivAt v (v' x) x
hu' : ContinuousOn u' (Set.uIcc a b)
hv' : ContinuousOn v' (Set.uIcc a b)
⊢ ContinuousOn (fun x => (B (u x)) (v' x)) (Set.uIcc a b)
Theorem: intervalIntegral.integral_deriv_bilin_eq_sub
Proof state before:
case refine_1
𝕜 : Type u_1
S : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝¹⁸ : NontriviallyNormedField 𝕜
inst✝¹⁷ : NormedAddCommGroup E
inst✝¹⁶ : NormedSpace ℝ E
inst✝¹⁵ : NormedSpace 𝕜 E
inst✝¹⁴ : NormedAddCommGroup F
inst✝¹³ : NormedSpace ℝ F
inst✝¹² : NormedSpace 𝕜 F
inst✝¹¹ : NormedAddCommGroup G
inst✝¹⁰ : NormedSpace ℝ G
inst✝⁹ : NormedSpace 𝕜 G
inst✝⁸ : CompleteSpace G
inst✝⁷ : NontriviallyNormedField S
inst✝⁶ : NormedSpace S G
inst✝⁵ : NormedSpace ℝ S
inst✝⁴ : SMulCommClass ℝ S G
inst✝³ : IsScalarTower ℝ S G
inst✝² : NormedSpace 𝕜 S
inst✝¹ : SMulCommClass 𝕜 S G
inst✝ : IsScalarTower 𝕜 S G
a b : ℝ
u u' : ℝ → E
v v' : ℝ → F
B : E →L[ℝ] F →L[ℝ] G
hu : ∀ x ∈ Set.uIcc a b, HasDerivAt u (u' x) x
hv : ∀ x ∈ Set.uIcc a b, HasDerivAt v (v' x) x
hu' : ContinuousOn u' (Set.uIcc a b)
hv' : ContinuousOn v' (Set.uIcc a b)
⊢ ContinuousOn (fun x => (B (u' x)) (v x)) (Set.uIcc a b)

case refine_2
𝕜 : Type u_1
S : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝¹⁸ : NontriviallyNormedField 𝕜
inst✝¹⁷ : NormedAddCommGroup E
inst✝¹⁶ : NormedSpace ℝ E
inst✝¹⁵ : NormedSpace 𝕜 E
inst✝¹⁴ : NormedAddCommGroup F
inst✝¹³ : NormedSpace ℝ F
inst✝¹² : NormedSpace 𝕜 F
inst✝¹¹ : NormedAddCommGroup G
inst✝¹⁰ : NormedSpace ℝ G
inst✝⁹ : NormedSpace 𝕜 G
inst✝⁸ : CompleteSpace G
inst✝⁷ : NontriviallyNormedField S
inst✝⁶ : NormedSpace S G
inst✝⁵ : NormedSpace ℝ S
inst✝⁴ : SMulCommClass ℝ S G
inst✝³ : IsScalarTower ℝ S G
inst✝² : NormedSpace 𝕜 S
inst✝¹ : SMulCommClass 𝕜 S G
inst✝ : IsScalarTower 𝕜 S G
a b : ℝ
u u' : ℝ → E
v v' : ℝ → F
B : E →L[ℝ] F →L[ℝ] G
hu : ∀ x ∈ Set.uIcc a b, HasDerivAt u (u' x) x
hv : ∀ x ∈ Set.uIcc a b, HasDerivAt v (v' x) x
hu' : ContinuousOn u' (Set.uIcc a b)
hv' : ContinuousOn v' (Set.uIcc a b)
⊢ ContinuousOn (fun x => (B (u x)) (v' x)) (Set.uIcc a b)
Tactic:
. exact ContinuousOn.bilin hu' (HasDerivAt.continuousOn hv)
Proof state after:
case refine_2
𝕜 : Type u_1
S : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝¹⁸ : NontriviallyNormedField 𝕜
inst✝¹⁷ : NormedAddCommGroup E
inst✝¹⁶ : NormedSpace ℝ E
inst✝¹⁵ : NormedSpace 𝕜 E
inst✝¹⁴ : NormedAddCommGroup F
inst✝¹³ : NormedSpace ℝ F
inst✝¹² : NormedSpace 𝕜 F
inst✝¹¹ : NormedAddCommGroup G
inst✝¹⁰ : NormedSpace ℝ G
inst✝⁹ : NormedSpace 𝕜 G
inst✝⁸ : CompleteSpace G
inst✝⁷ : NontriviallyNormedField S
inst✝⁶ : NormedSpace S G
inst✝⁵ : NormedSpace ℝ S
inst✝⁴ : SMulCommClass ℝ S G
inst✝³ : IsScalarTower ℝ S G
inst✝² : NormedSpace 𝕜 S
inst✝¹ : SMulCommClass 𝕜 S G
inst✝ : IsScalarTower 𝕜 S G
a b : ℝ
u u' : ℝ → E
v v' : ℝ → F
B : E →L[ℝ] F →L[ℝ] G
hu : ∀ x ∈ Set.uIcc a b, HasDerivAt u (u' x) x
hv : ∀ x ∈ Set.uIcc a b, HasDerivAt v (v' x) x
hu' : ContinuousOn u' (Set.uIcc a b)
hv' : ContinuousOn v' (Set.uIcc a b)
⊢ ContinuousOn (fun x => (B (u x)) (v' x)) (Set.uIcc a b)