Theorem: AnalyticAt.deriv2 (Ray/Analytic/Analytic.lean)

State before:
𝕜 : Type
inst✝¹³ : NontriviallyNormedField 𝕜
E : Type
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedSpace 𝕜 E
inst✝¹⁰ : CompleteSpace E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace 𝕜 F
inst✝⁷ : CompleteSpace F
G : Type
inst✝⁶ : NormedAddCommGroup G
inst✝⁵ : NormedSpace 𝕜 G
inst✝⁴ : CompleteSpace G
H : Type
inst✝³ : NormedAddCommGroup H
inst✝² : NormedSpace 𝕜 H
inst✝¹ : CompleteSpace H
inst✝ : CompleteSpace 𝕜
f : E → 𝕜 → 𝕜
c : E × 𝕜
fa : AnalyticAt 𝕜 (uncurry f) c
⊢ AnalyticAt 𝕜 (fun x => _root_.deriv (f x.1) x.2) c
Tactic:
set p : (E × 𝕜 →L[𝕜] 𝕜) →L[𝕜] 𝕜 := ContinuousLinearMap.apply 𝕜 𝕜 (0, 1)
State after:
𝕜 : Type
inst✝¹³ : NontriviallyNormedField 𝕜
E : Type
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedSpace 𝕜 E
inst✝¹⁰ : CompleteSpace E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace 𝕜 F
inst✝⁷ : CompleteSpace F
G : Type
inst✝⁶ : NormedAddCommGroup G
inst✝⁵ : NormedSpace 𝕜 G
inst✝⁴ : CompleteSpace G
H : Type
inst✝³ : NormedAddCommGroup H
inst✝² : NormedSpace 𝕜 H
inst✝¹ : CompleteSpace H
inst✝ : CompleteSpace 𝕜
f : E → 𝕜 → 𝕜
c : E × 𝕜
fa : AnalyticAt 𝕜 (uncurry f) c
p : (E × 𝕜 →L[𝕜] 𝕜) →L[𝕜] 𝕜 := (ContinuousLinearMap.apply 𝕜 𝕜) (0, 1)
⊢ AnalyticAt 𝕜 (fun x => _root_.deriv (f x.1) x.2) c

State before:
𝕜 : Type
inst✝¹³ : NontriviallyNormedField 𝕜
E : Type
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedSpace 𝕜 E
inst✝¹⁰ : CompleteSpace E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace 𝕜 F
inst✝⁷ : CompleteSpace F
G : Type
inst✝⁶ : NormedAddCommGroup G
inst✝⁵ : NormedSpace 𝕜 G
inst✝⁴ : CompleteSpace G
H : Type
inst✝³ : NormedAddCommGroup H
inst✝² : NormedSpace 𝕜 H
inst✝¹ : CompleteSpace H
inst✝ : CompleteSpace 𝕜
f : E → 𝕜 → 𝕜
c : E × 𝕜
fa : AnalyticAt 𝕜 (uncurry f) c
p : (E × 𝕜 →L[𝕜] 𝕜) →L[𝕜] 𝕜 := (ContinuousLinearMap.apply 𝕜 𝕜) (0, 1)
e : ∀ᶠ (x : E × 𝕜) in 𝓝 c, _root_.deriv (f x.1) x.2 = p (_root_.fderiv 𝕜 (uncurry f) x)
⊢ AnalyticAt 𝕜 (fun x => _root_.deriv (f x.1) x.2) c
Tactic:
rw [analyticAt_congr e]
State after:
𝕜 : Type
inst✝¹³ : NontriviallyNormedField 𝕜
E : Type
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedSpace 𝕜 E
inst✝¹⁰ : CompleteSpace E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace 𝕜 F
inst✝⁷ : CompleteSpace F
G : Type
inst✝⁶ : NormedAddCommGroup G
inst✝⁵ : NormedSpace 𝕜 G
inst✝⁴ : CompleteSpace G
H : Type
inst✝³ : NormedAddCommGroup H
inst✝² : NormedSpace 𝕜 H
inst✝¹ : CompleteSpace H
inst✝ : CompleteSpace 𝕜
f : E → 𝕜 → 𝕜
c : E × 𝕜
fa : AnalyticAt 𝕜 (uncurry f) c
p : (E × 𝕜 →L[𝕜] 𝕜) →L[𝕜] 𝕜 := (ContinuousLinearMap.apply 𝕜 𝕜) (0, 1)
e : ∀ᶠ (x : E × 𝕜) in 𝓝 c, _root_.deriv (f x.1) x.2 = p (_root_.fderiv 𝕜 (uncurry f) x)
⊢ AnalyticAt 𝕜 (fun x => p (_root_.fderiv 𝕜 (uncurry f) x)) c

State before:
𝕜 : Type
inst✝¹³ : NontriviallyNormedField 𝕜
E : Type
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedSpace 𝕜 E
inst✝¹⁰ : CompleteSpace E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace 𝕜 F
inst✝⁷ : CompleteSpace F
G : Type
inst✝⁶ : NormedAddCommGroup G
inst✝⁵ : NormedSpace 𝕜 G
inst✝⁴ : CompleteSpace G
H : Type
inst✝³ : NormedAddCommGroup H
inst✝² : NormedSpace 𝕜 H
inst✝¹ : CompleteSpace H
inst✝ : CompleteSpace 𝕜
f : E → 𝕜 → 𝕜
c : E × 𝕜
fa : AnalyticAt 𝕜 (uncurry f) c
p : (E × 𝕜 →L[𝕜] 𝕜) →L[𝕜] 𝕜 := (ContinuousLinearMap.apply 𝕜 𝕜) (0, 1)
e : ∀ᶠ (x : E × 𝕜) in 𝓝 c, _root_.deriv (f x.1) x.2 = p (_root_.fderiv 𝕜 (uncurry f) x)
⊢ AnalyticAt 𝕜 (fun x => p (_root_.fderiv 𝕜 (uncurry f) x)) c
Tactic:
exact (p.analyticAt _).comp fa.fderiv
State after:
no goals

State before:
𝕜 : Type
inst✝¹³ : NontriviallyNormedField 𝕜
E : Type
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedSpace 𝕜 E
inst✝¹⁰ : CompleteSpace E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace 𝕜 F
inst✝⁷ : CompleteSpace F
G : Type
inst✝⁶ : NormedAddCommGroup G
inst✝⁵ : NormedSpace 𝕜 G
inst✝⁴ : CompleteSpace G
H : Type
inst✝³ : NormedAddCommGroup H
inst✝² : NormedSpace 𝕜 H
inst✝¹ : CompleteSpace H
inst✝ : CompleteSpace 𝕜
f : E → 𝕜 → 𝕜
c : E × 𝕜
fa : AnalyticAt 𝕜 (uncurry f) c
p : (E × 𝕜 →L[𝕜] 𝕜) →L[𝕜] 𝕜 := (ContinuousLinearMap.apply 𝕜 𝕜) (0, 1)
⊢ ∀ᶠ (x : E × 𝕜) in 𝓝 c, _root_.deriv (f x.1) x.2 = p (_root_.fderiv 𝕜 (uncurry f) x)
Tactic:
refine fa.eventually_analyticAt.mp (eventually_of_forall ?_)
State after:
𝕜 : Type
inst✝¹³ : NontriviallyNormedField 𝕜
E : Type
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedSpace 𝕜 E
inst✝¹⁰ : CompleteSpace E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace 𝕜 F
inst✝⁷ : CompleteSpace F
G : Type
inst✝⁶ : NormedAddCommGroup G
inst✝⁵ : NormedSpace 𝕜 G
inst✝⁴ : CompleteSpace G
H : Type
inst✝³ : NormedAddCommGroup H
inst✝² : NormedSpace 𝕜 H
inst✝¹ : CompleteSpace H
inst✝ : CompleteSpace 𝕜
f : E → 𝕜 → 𝕜
c : E × 𝕜
fa : AnalyticAt 𝕜 (uncurry f) c
p : (E × 𝕜 →L[𝕜] 𝕜) →L[𝕜] 𝕜 := (ContinuousLinearMap.apply 𝕜 𝕜) (0, 1)
⊢ ∀ (x : E × 𝕜), AnalyticAt 𝕜 (uncurry f) x → _root_.deriv (f x.1) x.2 = p (_root_.fderiv 𝕜 (uncurry f) x)

State before:
𝕜 : Type
inst✝¹³ : NontriviallyNormedField 𝕜
E : Type
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedSpace 𝕜 E
inst✝¹⁰ : CompleteSpace E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace 𝕜 F
inst✝⁷ : CompleteSpace F
G : Type
inst✝⁶ : NormedAddCommGroup G
inst✝⁵ : NormedSpace 𝕜 G
inst✝⁴ : CompleteSpace G
H : Type
inst✝³ : NormedAddCommGroup H
inst✝² : NormedSpace 𝕜 H
inst✝¹ : CompleteSpace H
inst✝ : CompleteSpace 𝕜
f : E → 𝕜 → 𝕜
c : E × 𝕜
fa : AnalyticAt 𝕜 (uncurry f) c
p : (E × 𝕜 →L[𝕜] 𝕜) →L[𝕜] 𝕜 := (ContinuousLinearMap.apply 𝕜 𝕜) (0, 1)
⊢ ∀ (x : E × 𝕜), AnalyticAt 𝕜 (uncurry f) x → _root_.deriv (f x.1) x.2 = p (_root_.fderiv 𝕜 (uncurry f) x)
Tactic:
intro ⟨x, y⟩ fa
State after:
𝕜 : Type
inst✝¹³ : NontriviallyNormedField 𝕜
E : Type
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedSpace 𝕜 E
inst✝¹⁰ : CompleteSpace E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace 𝕜 F
inst✝⁷ : CompleteSpace F
G : Type
inst✝⁶ : NormedAddCommGroup G
inst✝⁵ : NormedSpace 𝕜 G
inst✝⁴ : CompleteSpace G
H : Type
inst✝³ : NormedAddCommGroup H
inst✝² : NormedSpace 𝕜 H
inst✝¹ : CompleteSpace H
inst✝ : CompleteSpace 𝕜
f : E → 𝕜 → 𝕜
c : E × 𝕜
fa✝ : AnalyticAt 𝕜 (uncurry f) c
p : (E × 𝕜 →L[𝕜] 𝕜) →L[𝕜] 𝕜 := (ContinuousLinearMap.apply 𝕜 𝕜) (0, 1)
x : E
y : 𝕜
fa : AnalyticAt 𝕜 (uncurry f) (x, y)
⊢ _root_.deriv (f (x, y).1) (x, y).2 = p (_root_.fderiv 𝕜 (uncurry f) (x, y))

State before:
𝕜 : Type
inst✝¹³ : NontriviallyNormedField 𝕜
E : Type
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedSpace 𝕜 E
inst✝¹⁰ : CompleteSpace E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace 𝕜 F
inst✝⁷ : CompleteSpace F
G : Type
inst✝⁶ : NormedAddCommGroup G
inst✝⁵ : NormedSpace 𝕜 G
inst✝⁴ : CompleteSpace G
H : Type
inst✝³ : NormedAddCommGroup H
inst✝² : NormedSpace 𝕜 H
inst✝¹ : CompleteSpace H
inst✝ : CompleteSpace 𝕜
f : E → 𝕜 → 𝕜
c : E × 𝕜
fa✝ : AnalyticAt 𝕜 (uncurry f) c
p : (E × 𝕜 →L[𝕜] 𝕜) →L[𝕜] 𝕜 := (ContinuousLinearMap.apply 𝕜 𝕜) (0, 1)
x : E
y : 𝕜
fa : AnalyticAt 𝕜 (uncurry f) (x, y)
⊢ _root_.deriv (f (x, y).1) (x, y).2 = p (_root_.fderiv 𝕜 (uncurry f) (x, y))
Tactic:
simp only [← fderiv_deriv]
State after:
𝕜 : Type
inst✝¹³ : NontriviallyNormedField 𝕜
E : Type
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedSpace 𝕜 E
inst✝¹⁰ : CompleteSpace E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace 𝕜 F
inst✝⁷ : CompleteSpace F
G : Type
inst✝⁶ : NormedAddCommGroup G
inst✝⁵ : NormedSpace 𝕜 G
inst✝⁴ : CompleteSpace G
H : Type
inst✝³ : NormedAddCommGroup H
inst✝² : NormedSpace 𝕜 H
inst✝¹ : CompleteSpace H
inst✝ : CompleteSpace 𝕜
f : E → 𝕜 → 𝕜
c : E × 𝕜
fa✝ : AnalyticAt 𝕜 (uncurry f) c
p : (E × 𝕜 →L[𝕜] 𝕜) →L[𝕜] 𝕜 := (ContinuousLinearMap.apply 𝕜 𝕜) (0, 1)
x : E
y : 𝕜
fa : AnalyticAt 𝕜 (uncurry f) (x, y)
⊢ (_root_.fderiv 𝕜 (f x) y) 1 = p (_root_.fderiv 𝕜 (uncurry f) (x, y))

State before:
𝕜 : Type
inst✝¹³ : NontriviallyNormedField 𝕜
E : Type
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedSpace 𝕜 E
inst✝¹⁰ : CompleteSpace E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace 𝕜 F
inst✝⁷ : CompleteSpace F
G : Type
inst✝⁶ : NormedAddCommGroup G
inst✝⁵ : NormedSpace 𝕜 G
inst✝⁴ : CompleteSpace G
H : Type
inst✝³ : NormedAddCommGroup H
inst✝² : NormedSpace 𝕜 H
inst✝¹ : CompleteSpace H
inst✝ : CompleteSpace 𝕜
f : E → 𝕜 → 𝕜
c : E × 𝕜
fa✝ : AnalyticAt 𝕜 (uncurry f) c
p : (E × 𝕜 →L[𝕜] 𝕜) →L[𝕜] 𝕜 := (ContinuousLinearMap.apply 𝕜 𝕜) (0, 1)
x : E
y : 𝕜
fa : AnalyticAt 𝕜 (uncurry f) (x, y)
⊢ (_root_.fderiv 𝕜 (f x) y) 1 = p (_root_.fderiv 𝕜 (uncurry f) (x, y))
Tactic:
have e : f x = uncurry f ∘ fun y ↦ (x, y) := rfl
State after:
𝕜 : Type
inst✝¹³ : NontriviallyNormedField 𝕜
E : Type
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedSpace 𝕜 E
inst✝¹⁰ : CompleteSpace E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace 𝕜 F
inst✝⁷ : CompleteSpace F
G : Type
inst✝⁶ : NormedAddCommGroup G
inst✝⁵ : NormedSpace 𝕜 G
inst✝⁴ : CompleteSpace G
H : Type
inst✝³ : NormedAddCommGroup H
inst✝² : NormedSpace 𝕜 H
inst✝¹ : CompleteSpace H
inst✝ : CompleteSpace 𝕜
f : E → 𝕜 → 𝕜
c : E × 𝕜
fa✝ : AnalyticAt 𝕜 (uncurry f) c
p : (E × 𝕜 →L[𝕜] 𝕜) →L[𝕜] 𝕜 := (ContinuousLinearMap.apply 𝕜 𝕜) (0, 1)
x : E
y : 𝕜
fa : AnalyticAt 𝕜 (uncurry f) (x, y)
e : f x = uncurry f ∘ fun y => (x, y)
⊢ (_root_.fderiv 𝕜 (f x) y) 1 = p (_root_.fderiv 𝕜 (uncurry f) (x, y))

State before:
𝕜 : Type
inst✝¹³ : NontriviallyNormedField 𝕜
E : Type
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedSpace 𝕜 E
inst✝¹⁰ : CompleteSpace E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace 𝕜 F
inst✝⁷ : CompleteSpace F
G : Type
inst✝⁶ : NormedAddCommGroup G
inst✝⁵ : NormedSpace 𝕜 G
inst✝⁴ : CompleteSpace G
H : Type
inst✝³ : NormedAddCommGroup H
inst✝² : NormedSpace 𝕜 H
inst✝¹ : CompleteSpace H
inst✝ : CompleteSpace 𝕜
f : E → 𝕜 → 𝕜
c : E × 𝕜
fa✝ : AnalyticAt 𝕜 (uncurry f) c
p : (E × 𝕜 →L[𝕜] 𝕜) →L[𝕜] 𝕜 := (ContinuousLinearMap.apply 𝕜 𝕜) (0, 1)
x : E
y : 𝕜
fa : AnalyticAt 𝕜 (uncurry f) (x, y)
e : f x = uncurry f ∘ fun y => (x, y)
⊢ (_root_.fderiv 𝕜 (f x) y) 1 = p (_root_.fderiv 𝕜 (uncurry f) (x, y))
Tactic:
rw [e]
State after:
𝕜 : Type
inst✝¹³ : NontriviallyNormedField 𝕜
E : Type
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedSpace 𝕜 E
inst✝¹⁰ : CompleteSpace E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace 𝕜 F
inst✝⁷ : CompleteSpace F
G : Type
inst✝⁶ : NormedAddCommGroup G
inst✝⁵ : NormedSpace 𝕜 G
inst✝⁴ : CompleteSpace G
H : Type
inst✝³ : NormedAddCommGroup H
inst✝² : NormedSpace 𝕜 H
inst✝¹ : CompleteSpace H
inst✝ : CompleteSpace 𝕜
f : E → 𝕜 → 𝕜
c : E × 𝕜
fa✝ : AnalyticAt 𝕜 (uncurry f) c
p : (E × 𝕜 →L[𝕜] 𝕜) →L[𝕜] 𝕜 := (ContinuousLinearMap.apply 𝕜 𝕜) (0, 1)
x : E
y : 𝕜
fa : AnalyticAt 𝕜 (uncurry f) (x, y)
e : f x = uncurry f ∘ fun y => (x, y)
⊢ (_root_.fderiv 𝕜 (uncurry f ∘ fun y => (x, y)) y) 1 = p (_root_.fderiv 𝕜 (uncurry f) (x, y))

State before:
𝕜 : Type
inst✝¹³ : NontriviallyNormedField 𝕜
E : Type
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedSpace 𝕜 E
inst✝¹⁰ : CompleteSpace E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace 𝕜 F
inst✝⁷ : CompleteSpace F
G : Type
inst✝⁶ : NormedAddCommGroup G
inst✝⁵ : NormedSpace 𝕜 G
inst✝⁴ : CompleteSpace G
H : Type
inst✝³ : NormedAddCommGroup H
inst✝² : NormedSpace 𝕜 H
inst✝¹ : CompleteSpace H
inst✝ : CompleteSpace 𝕜
f : E → 𝕜 → 𝕜
c : E × 𝕜
fa✝ : AnalyticAt 𝕜 (uncurry f) c
p : (E × 𝕜 →L[𝕜] 𝕜) →L[𝕜] 𝕜 := (ContinuousLinearMap.apply 𝕜 𝕜) (0, 1)
x : E
y : 𝕜
fa : AnalyticAt 𝕜 (uncurry f) (x, y)
e : f x = uncurry f ∘ fun y => (x, y)
⊢ (_root_.fderiv 𝕜 (uncurry f ∘ fun y => (x, y)) y) 1 = p (_root_.fderiv 𝕜 (uncurry f) (x, y))
Tactic:
rw [fderiv.comp]
State after:
𝕜 : Type
inst✝¹³ : NontriviallyNormedField 𝕜
E : Type
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedSpace 𝕜 E
inst✝¹⁰ : CompleteSpace E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace 𝕜 F
inst✝⁷ : CompleteSpace F
G : Type
inst✝⁶ : NormedAddCommGroup G
inst✝⁵ : NormedSpace 𝕜 G
inst✝⁴ : CompleteSpace G
H : Type
inst✝³ : NormedAddCommGroup H
inst✝² : NormedSpace 𝕜 H
inst✝¹ : CompleteSpace H
inst✝ : CompleteSpace 𝕜
f : E → 𝕜 → 𝕜
c : E × 𝕜
fa✝ : AnalyticAt 𝕜 (uncurry f) c
p : (E × 𝕜 →L[𝕜] 𝕜) →L[𝕜] 𝕜 := (ContinuousLinearMap.apply 𝕜 𝕜) (0, 1)
x : E
y : 𝕜
fa : AnalyticAt 𝕜 (uncurry f) (x, y)
e : f x = uncurry f ∘ fun y => (x, y)
⊢ ((_root_.fderiv 𝕜 (uncurry f) (x, y)).comp (_root_.fderiv 𝕜 (fun y => (x, y)) y)) 1 =
    p (_root_.fderiv 𝕜 (uncurry f) (x, y))

case hg
𝕜 : Type
inst✝¹³ : NontriviallyNormedField 𝕜
E : Type
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedSpace 𝕜 E
inst✝¹⁰ : CompleteSpace E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace 𝕜 F
inst✝⁷ : CompleteSpace F
G : Type
inst✝⁶ : NormedAddCommGroup G
inst✝⁵ : NormedSpace 𝕜 G
inst✝⁴ : CompleteSpace G
H : Type
inst✝³ : NormedAddCommGroup H
inst✝² : NormedSpace 𝕜 H
inst✝¹ : CompleteSpace H
inst✝ : CompleteSpace 𝕜
f : E → 𝕜 → 𝕜
c : E × 𝕜
fa✝ : AnalyticAt 𝕜 (uncurry f) c
p : (E × 𝕜 →L[𝕜] 𝕜) →L[𝕜] 𝕜 := (ContinuousLinearMap.apply 𝕜 𝕜) (0, 1)
x : E
y : 𝕜
fa : AnalyticAt 𝕜 (uncurry f) (x, y)
e : f x = uncurry f ∘ fun y => (x, y)
⊢ DifferentiableAt 𝕜 (uncurry f) (x, y)

case hf
𝕜 : Type
inst✝¹³ : NontriviallyNormedField 𝕜
E : Type
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedSpace 𝕜 E
inst✝¹⁰ : CompleteSpace E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace 𝕜 F
inst✝⁷ : CompleteSpace F
G : Type
inst✝⁶ : NormedAddCommGroup G
inst✝⁵ : NormedSpace 𝕜 G
inst✝⁴ : CompleteSpace G
H : Type
inst✝³ : NormedAddCommGroup H
inst✝² : NormedSpace 𝕜 H
inst✝¹ : CompleteSpace H
inst✝ : CompleteSpace 𝕜
f : E → 𝕜 → 𝕜
c : E × 𝕜
fa✝ : AnalyticAt 𝕜 (uncurry f) c
p : (E × 𝕜 →L[𝕜] 𝕜) →L[𝕜] 𝕜 := (ContinuousLinearMap.apply 𝕜 𝕜) (0, 1)
x : E
y : 𝕜
fa : AnalyticAt 𝕜 (uncurry f) (x, y)
e : f x = uncurry f ∘ fun y => (x, y)
⊢ DifferentiableAt 𝕜 (fun y => (x, y)) y

State before:
𝕜 : Type
inst✝¹³ : NontriviallyNormedField 𝕜
E : Type
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedSpace 𝕜 E
inst✝¹⁰ : CompleteSpace E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace 𝕜 F
inst✝⁷ : CompleteSpace F
G : Type
inst✝⁶ : NormedAddCommGroup G
inst✝⁵ : NormedSpace 𝕜 G
inst✝⁴ : CompleteSpace G
H : Type
inst✝³ : NormedAddCommGroup H
inst✝² : NormedSpace 𝕜 H
inst✝¹ : CompleteSpace H
inst✝ : CompleteSpace 𝕜
f : E → 𝕜 → 𝕜
c : E × 𝕜
fa✝ : AnalyticAt 𝕜 (uncurry f) c
p : (E × 𝕜 →L[𝕜] 𝕜) →L[𝕜] 𝕜 := (ContinuousLinearMap.apply 𝕜 𝕜) (0, 1)
x : E
y : 𝕜
fa : AnalyticAt 𝕜 (uncurry f) (x, y)
e : f x = uncurry f ∘ fun y => (x, y)
⊢ ((_root_.fderiv 𝕜 (uncurry f) (x, y)).comp (_root_.fderiv 𝕜 (fun y => (x, y)) y)) 1 =
    p (_root_.fderiv 𝕜 (uncurry f) (x, y))

case hg
𝕜 : Type
inst✝¹³ : NontriviallyNormedField 𝕜
E : Type
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedSpace 𝕜 E
inst✝¹⁰ : CompleteSpace E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace 𝕜 F
inst✝⁷ : CompleteSpace F
G : Type
inst✝⁶ : NormedAddCommGroup G
inst✝⁵ : NormedSpace 𝕜 G
inst✝⁴ : CompleteSpace G
H : Type
inst✝³ : NormedAddCommGroup H
inst✝² : NormedSpace 𝕜 H
inst✝¹ : CompleteSpace H
inst✝ : CompleteSpace 𝕜
f : E → 𝕜 → 𝕜
c : E × 𝕜
fa✝ : AnalyticAt 𝕜 (uncurry f) c
p : (E × 𝕜 →L[𝕜] 𝕜) →L[𝕜] 𝕜 := (ContinuousLinearMap.apply 𝕜 𝕜) (0, 1)
x : E
y : 𝕜
fa : AnalyticAt 𝕜 (uncurry f) (x, y)
e : f x = uncurry f ∘ fun y => (x, y)
⊢ DifferentiableAt 𝕜 (uncurry f) (x, y)

case hf
𝕜 : Type
inst✝¹³ : NontriviallyNormedField 𝕜
E : Type
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedSpace 𝕜 E
inst✝¹⁰ : CompleteSpace E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace 𝕜 F
inst✝⁷ : CompleteSpace F
G : Type
inst✝⁶ : NormedAddCommGroup G
inst✝⁵ : NormedSpace 𝕜 G
inst✝⁴ : CompleteSpace G
H : Type
inst✝³ : NormedAddCommGroup H
inst✝² : NormedSpace 𝕜 H
inst✝¹ : CompleteSpace H
inst✝ : CompleteSpace 𝕜
f : E → 𝕜 → 𝕜
c : E × 𝕜
fa✝ : AnalyticAt 𝕜 (uncurry f) c
p : (E × 𝕜 →L[𝕜] 𝕜) →L[𝕜] 𝕜 := (ContinuousLinearMap.apply 𝕜 𝕜) (0, 1)
x : E
y : 𝕜
fa : AnalyticAt 𝕜 (uncurry f) (x, y)
e : f x = uncurry f ∘ fun y => (x, y)
⊢ DifferentiableAt 𝕜 (fun y => (x, y)) y
Tactic:
have pd : _root_.fderiv 𝕜 (fun y : 𝕜 ↦ (x, y)) y = ContinuousLinearMap.inr 𝕜 E 𝕜 := by
  apply HasFDerivAt.fderiv; apply hasFDerivAt_prod_mk_right
State after:
𝕜 : Type
inst✝¹³ : NontriviallyNormedField 𝕜
E : Type
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedSpace 𝕜 E
inst✝¹⁰ : CompleteSpace E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace 𝕜 F
inst✝⁷ : CompleteSpace F
G : Type
inst✝⁶ : NormedAddCommGroup G
inst✝⁵ : NormedSpace 𝕜 G
inst✝⁴ : CompleteSpace G
H : Type
inst✝³ : NormedAddCommGroup H
inst✝² : NormedSpace 𝕜 H
inst✝¹ : CompleteSpace H
inst✝ : CompleteSpace 𝕜
f : E → 𝕜 → 𝕜
c : E × 𝕜
fa✝ : AnalyticAt 𝕜 (uncurry f) c
p : (E × 𝕜 →L[𝕜] 𝕜) →L[𝕜] 𝕜 := (ContinuousLinearMap.apply 𝕜 𝕜) (0, 1)
x : E
y : 𝕜
fa : AnalyticAt 𝕜 (uncurry f) (x, y)
e : f x = uncurry f ∘ fun y => (x, y)
pd : _root_.fderiv 𝕜 (fun y => (x, y)) y = ContinuousLinearMap.inr 𝕜 E 𝕜
⊢ ((_root_.fderiv 𝕜 (uncurry f) (x, y)).comp (_root_.fderiv 𝕜 (fun y => (x, y)) y)) 1 =
    p (_root_.fderiv 𝕜 (uncurry f) (x, y))

case hg
𝕜 : Type
inst✝¹³ : NontriviallyNormedField 𝕜
E : Type
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedSpace 𝕜 E
inst✝¹⁰ : CompleteSpace E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace 𝕜 F
inst✝⁷ : CompleteSpace F
G : Type
inst✝⁶ : NormedAddCommGroup G
inst✝⁵ : NormedSpace 𝕜 G
inst✝⁴ : CompleteSpace G
H : Type
inst✝³ : NormedAddCommGroup H
inst✝² : NormedSpace 𝕜 H
inst✝¹ : CompleteSpace H
inst✝ : CompleteSpace 𝕜
f : E → 𝕜 → 𝕜
c : E × 𝕜
fa✝ : AnalyticAt 𝕜 (uncurry f) c
p : (E × 𝕜 →L[𝕜] 𝕜) →L[𝕜] 𝕜 := (ContinuousLinearMap.apply 𝕜 𝕜) (0, 1)
x : E
y : 𝕜
fa : AnalyticAt 𝕜 (uncurry f) (x, y)
e : f x = uncurry f ∘ fun y => (x, y)
⊢ DifferentiableAt 𝕜 (uncurry f) (x, y)

case hf
𝕜 : Type
inst✝¹³ : NontriviallyNormedField 𝕜
E : Type
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedSpace 𝕜 E
inst✝¹⁰ : CompleteSpace E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace 𝕜 F
inst✝⁷ : CompleteSpace F
G : Type
inst✝⁶ : NormedAddCommGroup G
inst✝⁵ : NormedSpace 𝕜 G
inst✝⁴ : CompleteSpace G
H : Type
inst✝³ : NormedAddCommGroup H
inst✝² : NormedSpace 𝕜 H
inst✝¹ : CompleteSpace H
inst✝ : CompleteSpace 𝕜
f : E → 𝕜 → 𝕜
c : E × 𝕜
fa✝ : AnalyticAt 𝕜 (uncurry f) c
p : (E × 𝕜 →L[𝕜] 𝕜) →L[𝕜] 𝕜 := (ContinuousLinearMap.apply 𝕜 𝕜) (0, 1)
x : E
y : 𝕜
fa : AnalyticAt 𝕜 (uncurry f) (x, y)
e : f x = uncurry f ∘ fun y => (x, y)
⊢ DifferentiableAt 𝕜 (fun y => (x, y)) y

State before:
𝕜 : Type
inst✝¹³ : NontriviallyNormedField 𝕜
E : Type
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedSpace 𝕜 E
inst✝¹⁰ : CompleteSpace E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace 𝕜 F
inst✝⁷ : CompleteSpace F
G : Type
inst✝⁶ : NormedAddCommGroup G
inst✝⁵ : NormedSpace 𝕜 G
inst✝⁴ : CompleteSpace G
H : Type
inst✝³ : NormedAddCommGroup H
inst✝² : NormedSpace 𝕜 H
inst✝¹ : CompleteSpace H
inst✝ : CompleteSpace 𝕜
f : E → 𝕜 → 𝕜
c : E × 𝕜
fa✝ : AnalyticAt 𝕜 (uncurry f) c
p : (E × 𝕜 →L[𝕜] 𝕜) →L[𝕜] 𝕜 := (ContinuousLinearMap.apply 𝕜 𝕜) (0, 1)
x : E
y : 𝕜
fa : AnalyticAt 𝕜 (uncurry f) (x, y)
e : f x = uncurry f ∘ fun y => (x, y)
pd : _root_.fderiv 𝕜 (fun y => (x, y)) y = ContinuousLinearMap.inr 𝕜 E 𝕜
⊢ ((_root_.fderiv 𝕜 (uncurry f) (x, y)).comp (_root_.fderiv 𝕜 (fun y => (x, y)) y)) 1 =
    p (_root_.fderiv 𝕜 (uncurry f) (x, y))

case hg
𝕜 : Type
inst✝¹³ : NontriviallyNormedField 𝕜
E : Type
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedSpace 𝕜 E
inst✝¹⁰ : CompleteSpace E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace 𝕜 F
inst✝⁷ : CompleteSpace F
G : Type
inst✝⁶ : NormedAddCommGroup G
inst✝⁵ : NormedSpace 𝕜 G
inst✝⁴ : CompleteSpace G
H : Type
inst✝³ : NormedAddCommGroup H
inst✝² : NormedSpace 𝕜 H
inst✝¹ : CompleteSpace H
inst✝ : CompleteSpace 𝕜
f : E → 𝕜 → 𝕜
c : E × 𝕜
fa✝ : AnalyticAt 𝕜 (uncurry f) c
p : (E × 𝕜 →L[𝕜] 𝕜) →L[𝕜] 𝕜 := (ContinuousLinearMap.apply 𝕜 𝕜) (0, 1)
x : E
y : 𝕜
fa : AnalyticAt 𝕜 (uncurry f) (x, y)
e : f x = uncurry f ∘ fun y => (x, y)
⊢ DifferentiableAt 𝕜 (uncurry f) (x, y)

case hf
𝕜 : Type
inst✝¹³ : NontriviallyNormedField 𝕜
E : Type
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedSpace 𝕜 E
inst✝¹⁰ : CompleteSpace E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace 𝕜 F
inst✝⁷ : CompleteSpace F
G : Type
inst✝⁶ : NormedAddCommGroup G
inst✝⁵ : NormedSpace 𝕜 G
inst✝⁴ : CompleteSpace G
H : Type
inst✝³ : NormedAddCommGroup H
inst✝² : NormedSpace 𝕜 H
inst✝¹ : CompleteSpace H
inst✝ : CompleteSpace 𝕜
f : E → 𝕜 → 𝕜
c : E × 𝕜
fa✝ : AnalyticAt 𝕜 (uncurry f) c
p : (E × 𝕜 →L[𝕜] 𝕜) →L[𝕜] 𝕜 := (ContinuousLinearMap.apply 𝕜 𝕜) (0, 1)
x : E
y : 𝕜
fa : AnalyticAt 𝕜 (uncurry f) (x, y)
e : f x = uncurry f ∘ fun y => (x, y)
⊢ DifferentiableAt 𝕜 (fun y => (x, y)) y
Tactic:
rw [pd, ContinuousLinearMap.comp_apply, ContinuousLinearMap.inr_apply,
  ContinuousLinearMap.apply_apply]
State after:
case hg
𝕜 : Type
inst✝¹³ : NontriviallyNormedField 𝕜
E : Type
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedSpace 𝕜 E
inst✝¹⁰ : CompleteSpace E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace 𝕜 F
inst✝⁷ : CompleteSpace F
G : Type
inst✝⁶ : NormedAddCommGroup G
inst✝⁵ : NormedSpace 𝕜 G
inst✝⁴ : CompleteSpace G
H : Type
inst✝³ : NormedAddCommGroup H
inst✝² : NormedSpace 𝕜 H
inst✝¹ : CompleteSpace H
inst✝ : CompleteSpace 𝕜
f : E → 𝕜 → 𝕜
c : E × 𝕜
fa✝ : AnalyticAt 𝕜 (uncurry f) c
p : (E × 𝕜 →L[𝕜] 𝕜) →L[𝕜] 𝕜 := (ContinuousLinearMap.apply 𝕜 𝕜) (0, 1)
x : E
y : 𝕜
fa : AnalyticAt 𝕜 (uncurry f) (x, y)
e : f x = uncurry f ∘ fun y => (x, y)
⊢ DifferentiableAt 𝕜 (uncurry f) (x, y)

case hf
𝕜 : Type
inst✝¹³ : NontriviallyNormedField 𝕜
E : Type
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedSpace 𝕜 E
inst✝¹⁰ : CompleteSpace E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace 𝕜 F
inst✝⁷ : CompleteSpace F
G : Type
inst✝⁶ : NormedAddCommGroup G
inst✝⁵ : NormedSpace 𝕜 G
inst✝⁴ : CompleteSpace G
H : Type
inst✝³ : NormedAddCommGroup H
inst✝² : NormedSpace 𝕜 H
inst✝¹ : CompleteSpace H
inst✝ : CompleteSpace 𝕜
f : E → 𝕜 → 𝕜
c : E × 𝕜
fa✝ : AnalyticAt 𝕜 (uncurry f) c
p : (E × 𝕜 →L[𝕜] 𝕜) →L[𝕜] 𝕜 := (ContinuousLinearMap.apply 𝕜 𝕜) (0, 1)
x : E
y : 𝕜
fa : AnalyticAt 𝕜 (uncurry f) (x, y)
e : f x = uncurry f ∘ fun y => (x, y)
⊢ DifferentiableAt 𝕜 (fun y => (x, y)) y

State before:
𝕜 : Type
inst✝¹³ : NontriviallyNormedField 𝕜
E : Type
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedSpace 𝕜 E
inst✝¹⁰ : CompleteSpace E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace 𝕜 F
inst✝⁷ : CompleteSpace F
G : Type
inst✝⁶ : NormedAddCommGroup G
inst✝⁵ : NormedSpace 𝕜 G
inst✝⁴ : CompleteSpace G
H : Type
inst✝³ : NormedAddCommGroup H
inst✝² : NormedSpace 𝕜 H
inst✝¹ : CompleteSpace H
inst✝ : CompleteSpace 𝕜
f : E → 𝕜 → 𝕜
c : E × 𝕜
fa✝ : AnalyticAt 𝕜 (uncurry f) c
p : (E × 𝕜 →L[𝕜] 𝕜) →L[𝕜] 𝕜 := (ContinuousLinearMap.apply 𝕜 𝕜) (0, 1)
x : E
y : 𝕜
fa : AnalyticAt 𝕜 (uncurry f) (x, y)
e : f x = uncurry f ∘ fun y => (x, y)
⊢ _root_.fderiv 𝕜 (fun y => (x, y)) y = ContinuousLinearMap.inr 𝕜 E 𝕜
Tactic:
apply HasFDerivAt.fderiv
State after:
case h
𝕜 : Type
inst✝¹³ : NontriviallyNormedField 𝕜
E : Type
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedSpace 𝕜 E
inst✝¹⁰ : CompleteSpace E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace 𝕜 F
inst✝⁷ : CompleteSpace F
G : Type
inst✝⁶ : NormedAddCommGroup G
inst✝⁵ : NormedSpace 𝕜 G
inst✝⁴ : CompleteSpace G
H : Type
inst✝³ : NormedAddCommGroup H
inst✝² : NormedSpace 𝕜 H
inst✝¹ : CompleteSpace H
inst✝ : CompleteSpace 𝕜
f : E → 𝕜 → 𝕜
c : E × 𝕜
fa✝ : AnalyticAt 𝕜 (uncurry f) c
p : (E × 𝕜 →L[𝕜] 𝕜) →L[𝕜] 𝕜 := (ContinuousLinearMap.apply 𝕜 𝕜) (0, 1)
x : E
y : 𝕜
fa : AnalyticAt 𝕜 (uncurry f) (x, y)
e : f x = uncurry f ∘ fun y => (x, y)
⊢ HasFDerivAt (fun y => (x, y)) (ContinuousLinearMap.inr 𝕜 E 𝕜) y

State before:
case h
𝕜 : Type
inst✝¹³ : NontriviallyNormedField 𝕜
E : Type
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedSpace 𝕜 E
inst✝¹⁰ : CompleteSpace E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace 𝕜 F
inst✝⁷ : CompleteSpace F
G : Type
inst✝⁶ : NormedAddCommGroup G
inst✝⁵ : NormedSpace 𝕜 G
inst✝⁴ : CompleteSpace G
H : Type
inst✝³ : NormedAddCommGroup H
inst✝² : NormedSpace 𝕜 H
inst✝¹ : CompleteSpace H
inst✝ : CompleteSpace 𝕜
f : E → 𝕜 → 𝕜
c : E × 𝕜
fa✝ : AnalyticAt 𝕜 (uncurry f) c
p : (E × 𝕜 →L[𝕜] 𝕜) →L[𝕜] 𝕜 := (ContinuousLinearMap.apply 𝕜 𝕜) (0, 1)
x : E
y : 𝕜
fa : AnalyticAt 𝕜 (uncurry f) (x, y)
e : f x = uncurry f ∘ fun y => (x, y)
⊢ HasFDerivAt (fun y => (x, y)) (ContinuousLinearMap.inr 𝕜 E 𝕜) y
Tactic:
apply hasFDerivAt_prod_mk_right
State after:
no goals

State before:
case hg
𝕜 : Type
inst✝¹³ : NontriviallyNormedField 𝕜
E : Type
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedSpace 𝕜 E
inst✝¹⁰ : CompleteSpace E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace 𝕜 F
inst✝⁷ : CompleteSpace F
G : Type
inst✝⁶ : NormedAddCommGroup G
inst✝⁵ : NormedSpace 𝕜 G
inst✝⁴ : CompleteSpace G
H : Type
inst✝³ : NormedAddCommGroup H
inst✝² : NormedSpace 𝕜 H
inst✝¹ : CompleteSpace H
inst✝ : CompleteSpace 𝕜
f : E → 𝕜 → 𝕜
c : E × 𝕜
fa✝ : AnalyticAt 𝕜 (uncurry f) c
p : (E × 𝕜 →L[𝕜] 𝕜) →L[𝕜] 𝕜 := (ContinuousLinearMap.apply 𝕜 𝕜) (0, 1)
x : E
y : 𝕜
fa : AnalyticAt 𝕜 (uncurry f) (x, y)
e : f x = uncurry f ∘ fun y => (x, y)
⊢ DifferentiableAt 𝕜 (uncurry f) (x, y)
Tactic:
exact fa.differentiableAt
State after:
no goals

State before:
case hf
𝕜 : Type
inst✝¹³ : NontriviallyNormedField 𝕜
E : Type
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedSpace 𝕜 E
inst✝¹⁰ : CompleteSpace E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace 𝕜 F
inst✝⁷ : CompleteSpace F
G : Type
inst✝⁶ : NormedAddCommGroup G
inst✝⁵ : NormedSpace 𝕜 G
inst✝⁴ : CompleteSpace G
H : Type
inst✝³ : NormedAddCommGroup H
inst✝² : NormedSpace 𝕜 H
inst✝¹ : CompleteSpace H
inst✝ : CompleteSpace 𝕜
f : E → 𝕜 → 𝕜
c : E × 𝕜
fa✝ : AnalyticAt 𝕜 (uncurry f) c
p : (E × 𝕜 →L[𝕜] 𝕜) →L[𝕜] 𝕜 := (ContinuousLinearMap.apply 𝕜 𝕜) (0, 1)
x : E
y : 𝕜
fa : AnalyticAt 𝕜 (uncurry f) (x, y)
e : f x = uncurry f ∘ fun y => (x, y)
⊢ DifferentiableAt 𝕜 (fun y => (x, y)) y
Tactic:
exact (differentiableAt_const _).prod differentiableAt_id
State after:
no goals