case pos
𝕜 : Type u_2
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type u_1
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type u_4
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
G' : Type ?u.233580
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 : F → G
s : Set F
x : E
hxs : UniqueDiffWithinAt 𝕜 (↑iso ⁻¹' s) x
h : DifferentiableWithinAt 𝕜 f s (↑iso x)
⊢ fderivWithin 𝕜 (f ∘ ↑iso) (↑iso ⁻¹' s) x = comp (fderivWithin 𝕜 f s (↑iso x)) ↑iso

case neg
𝕜 : Type u_2
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type u_1
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type u_4
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
G' : Type ?u.233580
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 : F → G
s : Set F
x : E
hxs : UniqueDiffWithinAt 𝕜 (↑iso ⁻¹' s) x
h : ¬DifferentiableWithinAt 𝕜 f s (↑iso x)
⊢ fderivWithin 𝕜 (f ∘ ↑iso) (↑iso ⁻¹' s) x = comp (fderivWithin 𝕜 f s (↑iso x)) ↑iso
𝕜 : Type u_2
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type u_1
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type u_4
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
G' : Type ?u.233580
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 : F → G
s : Set F
x : E
hxs : UniqueDiffWithinAt 𝕜 (↑iso ⁻¹' s) x
⊢ fderivWithin 𝕜 (f ∘ ↑iso) (↑iso ⁻¹' s) x = comp (fderivWithin 𝕜 f s (↑iso x)) ↑iso
by_cases h : DifferentiableWithinAt 𝕜 f s (iso x)
no goals
case pos
𝕜 : Type u_2
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type u_1
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type u_4
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
G' : Type ?u.233580
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 : F → G
s : Set F
x : E
hxs : UniqueDiffWithinAt 𝕜 (↑iso ⁻¹' s) x
h : DifferentiableWithinAt 𝕜 f s (↑iso x)
⊢ fderivWithin 𝕜 (f ∘ ↑iso) (↑iso ⁻¹' s) x = comp (fderivWithin 𝕜 f s (↑iso x)) ↑iso
exact (iso.comp_right_hasFDerivWithinAt_iff.2 h.hasFDerivWithinAt).fderivWithin hxs
case neg
𝕜 : Type u_2
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type u_1
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type u_4
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
G' : Type ?u.233580
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 : F → G
s : Set F
x : E
hxs : UniqueDiffWithinAt 𝕜 (↑iso ⁻¹' s) x
h : ¬DifferentiableWithinAt 𝕜 f s (↑iso x)
this : ¬DifferentiableWithinAt 𝕜 (f ∘ ↑iso) (↑iso ⁻¹' s) x
⊢ fderivWithin 𝕜 (f ∘ ↑iso) (↑iso ⁻¹' s) x = comp (fderivWithin 𝕜 f s (↑iso x)) ↑iso
case neg
𝕜 : Type u_2
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type u_1
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type u_4
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
G' : Type ?u.233580
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 : F → G
s : Set F
x : E
hxs : UniqueDiffWithinAt 𝕜 (↑iso ⁻¹' s) x
h : ¬DifferentiableWithinAt 𝕜 f s (↑iso x)
⊢ fderivWithin 𝕜 (f ∘ ↑iso) (↑iso ⁻¹' s) x = comp (fderivWithin 𝕜 f s (↑iso x)) ↑iso
have : ¬DifferentiableWithinAt 𝕜 (f ∘ iso) (iso ⁻¹' s) x := by
  intro h'
  exact h (iso.comp_right_differentiableWithinAt_iff.1 h')
no goals
case neg
𝕜 : Type u_2
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type u_1
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type u_4
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
G' : Type ?u.233580
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 : F → G
s : Set F
x : E
hxs : UniqueDiffWithinAt 𝕜 (↑iso ⁻¹' s) x
h : ¬DifferentiableWithinAt 𝕜 f s (↑iso x)
this : ¬DifferentiableWithinAt 𝕜 (f ∘ ↑iso) (↑iso ⁻¹' s) x
⊢ fderivWithin 𝕜 (f ∘ ↑iso) (↑iso ⁻¹' s) x = comp (fderivWithin 𝕜 f s (↑iso x)) ↑iso
rw [fderivWithin_zero_of_not_differentiableWithinAt h,
  fderivWithin_zero_of_not_differentiableWithinAt this, ContinuousLinearMap.zero_comp]
𝕜 : Type u_2
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type u_1
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type u_4
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
G' : Type ?u.233580
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 : F → G
s : Set F
x : E
hxs : UniqueDiffWithinAt 𝕜 (↑iso ⁻¹' s) x
h : ¬DifferentiableWithinAt 𝕜 f s (↑iso x)
h' : DifferentiableWithinAt 𝕜 (f ∘ ↑iso) (↑iso ⁻¹' s) x
⊢ False
𝕜 : Type u_2
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type u_1
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type u_4
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
G' : Type ?u.233580
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 : F → G
s : Set F
x : E
hxs : UniqueDiffWithinAt 𝕜 (↑iso ⁻¹' s) x
h : ¬DifferentiableWithinAt 𝕜 f s (↑iso x)
⊢ ¬DifferentiableWithinAt 𝕜 (f ∘ ↑iso) (↑iso ⁻¹' s) x
intro h'
no goals
𝕜 : Type u_2
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type u_1
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type u_4
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
G' : Type ?u.233580
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 : F → G
s : Set F
x : E
hxs : UniqueDiffWithinAt 𝕜 (↑iso ⁻¹' s) x
h : ¬DifferentiableWithinAt 𝕜 f s (↑iso x)
h' : DifferentiableWithinAt 𝕜 (f ∘ ↑iso) (↑iso ⁻¹' s) x
⊢ False
exact h (iso.comp_right_differentiableWithinAt_iff.1 h')