Theorem: AnalyticAt.deriv2
Proof 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
Proof 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