𝕜 : Type u_2
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type u_4
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type u_1
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
G' : Type ?u.60346
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
iso : E ≃L[𝕜] F
f : G → E
s : Set G
x : G
H : DifferentiableWithinAt 𝕜 (↑iso ∘ f) s x
⊢ DifferentiableWithinAt 𝕜 f s x
𝕜 : Type u_2
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type u_4
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type u_1
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
G' : Type ?u.60346
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
iso : E ≃L[𝕜] F
f : G → E
s : Set G
x : G
⊢ DifferentiableWithinAt 𝕜 (↑iso ∘ f) s x ↔ DifferentiableWithinAt 𝕜 f s x
refine'
  ⟨fun H => _, fun H => iso.differentiable.differentiableAt.comp_differentiableWithinAt x H⟩
𝕜 : Type u_2
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type u_4
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type u_1
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
G' : Type ?u.60346
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
iso : E ≃L[𝕜] F
f : G → E
s : Set G
x : G
H : DifferentiableWithinAt 𝕜 (↑iso ∘ f) s x
this : DifferentiableWithinAt 𝕜 (↑(ContinuousLinearEquiv.symm iso) ∘ ↑iso ∘ f) s x
⊢ DifferentiableWithinAt 𝕜 f s x
𝕜 : Type u_2
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type u_4
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type u_1
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
G' : Type ?u.60346
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
iso : E ≃L[𝕜] F
f : G → E
s : Set G
x : G
H : DifferentiableWithinAt 𝕜 (↑iso ∘ f) s x
⊢ DifferentiableWithinAt 𝕜 f s x
have : DifferentiableWithinAt 𝕜 (iso.symm ∘ iso ∘ f) s x :=
  iso.symm.differentiable.differentiableAt.comp_differentiableWithinAt x H
no goals
𝕜 : Type u_2
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type u_4
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type u_1
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
G' : Type ?u.60346
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
iso : E ≃L[𝕜] F
f : G → E
s : Set G
x : G
H : DifferentiableWithinAt 𝕜 (↑iso ∘ f) s x
this : DifferentiableWithinAt 𝕜 (↑(ContinuousLinearEquiv.symm iso) ∘ ↑iso ∘ f) s x
⊢ DifferentiableWithinAt 𝕜 f s x
rwa [← Function.comp.assoc iso.symm iso f, iso.symm_comp_self] at this