case zero
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type ?u.135699
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type ?u.135794
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
G' : Type ?u.135889
inst✝¹ : NormedAddCommGroup G'
inst✝ : NormedSpace 𝕜 G'
f✝ f₀ f₁ g : E → F
f'✝ f₀' f₁' g' e : E →L[𝕜] F
x : E
s t : Set E
L L₁ L₂ : Filter E
f : E → E
f' : E →L[𝕜] E
hf : HasFDerivAtFilter f f' x L
hL : Tendsto f L L
hx : f x = x
⊢ HasFDerivAtFilter (f^[Nat.zero]) (f' ^ Nat.zero) x L

case succ
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type ?u.135699
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type ?u.135794
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
G' : Type ?u.135889
inst✝¹ : NormedAddCommGroup G'
inst✝ : NormedSpace 𝕜 G'
f✝ f₀ f₁ g : E → F
f'✝ f₀' f₁' g' e : E →L[𝕜] F
x : E
s t : Set E
L L₁ L₂ : Filter E
f : E → E
f' : E →L[𝕜] E
hf : HasFDerivAtFilter f f' x L
hL : Tendsto f L L
hx : f x = x
n : ℕ
ihn : HasFDerivAtFilter (f^[n]) (f' ^ n) x L
⊢ HasFDerivAtFilter (f^[Nat.succ n]) (f' ^ Nat.succ n) x L
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type ?u.135699
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type ?u.135794
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
G' : Type ?u.135889
inst✝¹ : NormedAddCommGroup G'
inst✝ : NormedSpace 𝕜 G'
f✝ f₀ f₁ g : E → F
f'✝ f₀' f₁' g' e : E →L[𝕜] F
x : E
s t : Set E
L L₁ L₂ : Filter E
f : E → E
f' : E →L[𝕜] E
hf : HasFDerivAtFilter f f' x L
hL : Tendsto f L L
hx : f x = x
n : ℕ
⊢ HasFDerivAtFilter (f^[n]) (f' ^ n) x L
induction' n with n ihn
no goals
case zero
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type ?u.135699
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type ?u.135794
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
G' : Type ?u.135889
inst✝¹ : NormedAddCommGroup G'
inst✝ : NormedSpace 𝕜 G'
f✝ f₀ f₁ g : E → F
f'✝ f₀' f₁' g' e : E →L[𝕜] F
x : E
s t : Set E
L L₁ L₂ : Filter E
f : E → E
f' : E →L[𝕜] E
hf : HasFDerivAtFilter f f' x L
hL : Tendsto f L L
hx : f x = x
⊢ HasFDerivAtFilter (f^[Nat.zero]) (f' ^ Nat.zero) x L
exact hasFDerivAtFilter_id x L
case succ
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type ?u.135699
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type ?u.135794
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
G' : Type ?u.135889
inst✝¹ : NormedAddCommGroup G'
inst✝ : NormedSpace 𝕜 G'
f✝ f₀ f₁ g : E → F
f'✝ f₀' f₁' g' e : E →L[𝕜] F
x : E
s t : Set E
L L₁ L₂ : Filter E
f : E → E
f' : E →L[𝕜] E
hf : HasFDerivAtFilter f f' x L
hL : Tendsto f L L
hx : f x = x
n : ℕ
ihn : HasFDerivAtFilter (f^[n]) (f' ^ n) x L
⊢ HasFDerivAtFilter (f^[n] ∘ f) (f' ^ n * f') x L
case succ
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type ?u.135699
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type ?u.135794
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
G' : Type ?u.135889
inst✝¹ : NormedAddCommGroup G'
inst✝ : NormedSpace 𝕜 G'
f✝ f₀ f₁ g : E → F
f'✝ f₀' f₁' g' e : E →L[𝕜] F
x : E
s t : Set E
L L₁ L₂ : Filter E
f : E → E
f' : E →L[𝕜] E
hf : HasFDerivAtFilter f f' x L
hL : Tendsto f L L
hx : f x = x
n : ℕ
ihn : HasFDerivAtFilter (f^[n]) (f' ^ n) x L
⊢ HasFDerivAtFilter (f^[Nat.succ n]) (f' ^ Nat.succ n) x L
rw [Function.iterate_succ, pow_succ']
case succ
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type ?u.135699
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type ?u.135794
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
G' : Type ?u.135889
inst✝¹ : NormedAddCommGroup G'
inst✝ : NormedSpace 𝕜 G'
f✝ f₀ f₁ g : E → F
f'✝ f₀' f₁' g' e : E →L[𝕜] F
x : E
s t : Set E
L L₁ L₂ : Filter E
f : E → E
f' : E →L[𝕜] E
hf : HasFDerivAtFilter f f' x L
hL : Tendsto f L L
hx : f x = x
n : ℕ
ihn : HasFDerivAtFilter (f^[n]) (f' ^ n) (f x) L
⊢ HasFDerivAtFilter (f^[n] ∘ f) (f' ^ n * f') x L
case succ
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type ?u.135699
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type ?u.135794
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
G' : Type ?u.135889
inst✝¹ : NormedAddCommGroup G'
inst✝ : NormedSpace 𝕜 G'
f✝ f₀ f₁ g : E → F
f'✝ f₀' f₁' g' e : E →L[𝕜] F
x : E
s t : Set E
L L₁ L₂ : Filter E
f : E → E
f' : E →L[𝕜] E
hf : HasFDerivAtFilter f f' x L
hL : Tendsto f L L
hx : f x = x
n : ℕ
ihn : HasFDerivAtFilter (f^[n]) (f' ^ n) x L
⊢ HasFDerivAtFilter (f^[n] ∘ f) (f' ^ n * f') x L
rw [← hx] at ihn
no goals
case succ
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type ?u.135699
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type ?u.135794
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
G' : Type ?u.135889
inst✝¹ : NormedAddCommGroup G'
inst✝ : NormedSpace 𝕜 G'
f✝ f₀ f₁ g : E → F
f'✝ f₀' f₁' g' e : E →L[𝕜] F
x : E
s t : Set E
L L₁ L₂ : Filter E
f : E → E
f' : E →L[𝕜] E
hf : HasFDerivAtFilter f f' x L
hL : Tendsto f L L
hx : f x = x
n : ℕ
ihn : HasFDerivAtFilter (f^[n]) (f' ^ n) (f x) L
⊢ HasFDerivAtFilter (f^[n] ∘ f) (f' ^ n * f') x L
exact ihn.comp x hf hL