[GOAL]
e : ℤˣ
⊢ ‖↑e‖₊ = 1
[PROOFSTEP]
obtain rfl | rfl := units_eq_one_or e
[GOAL]
case inl
⊢ ‖↑1‖₊ = 1
[PROOFSTEP]
simp only [Units.coe_neg_one, Units.val_one, nnnorm_neg, nnnorm_one]
[GOAL]
case inr
⊢ ‖↑(-1)‖₊ = 1
[PROOFSTEP]
simp only [Units.coe_neg_one, Units.val_one, nnnorm_neg, nnnorm_one]
[GOAL]
e : ℤˣ
⊢ ‖↑e‖ = 1
[PROOFSTEP]
rw [← coe_nnnorm, nnnorm_coe_units, NNReal.coe_one]
[GOAL]
n : ℤ
⊢ ↑(toNat n) + ↑(toNat (-n)) = ‖n‖₊
[PROOFSTEP]
rw [← Nat.cast_add, toNat_add_toNat_neg_eq_natAbs, NNReal.coe_natAbs]
[GOAL]
n : ℤ
⊢ ↑(toNat n) + ↑(toNat (-n)) = ‖n‖
[PROOFSTEP]
simpa only [NNReal.coe_nat_cast, NNReal.coe_add] using congrArg NNReal.toReal (toNat_add_toNat_neg_eq_nnnorm n)


[GOAL]
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type u_4
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
G' : Type u_5
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
[PROOFSTEP]
refine' ⟨fun H => _, fun H => iso.differentiable.differentiableAt.comp_differentiableWithinAt x H⟩
[GOAL]
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type u_4
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
G' : Type u_5
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
[PROOFSTEP]
have : DifferentiableWithinAt 𝕜 (iso.symm ∘ iso ∘ f) s x :=
  iso.symm.differentiable.differentiableAt.comp_differentiableWithinAt x H
[GOAL]
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type u_4
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
G' : Type u_5
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
[PROOFSTEP]
rwa [← Function.comp.assoc iso.symm iso f, iso.symm_comp_self] at this
[GOAL]
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type u_4
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
G' : Type u_5
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
x : G
⊢ DifferentiableAt 𝕜 (↑iso ∘ f) x ↔ DifferentiableAt 𝕜 f x
[PROOFSTEP]
rw [← differentiableWithinAt_univ, ← differentiableWithinAt_univ, iso.comp_differentiableWithinAt_iff]
[GOAL]
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type u_4
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
G' : Type u_5
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
⊢ DifferentiableOn 𝕜 (↑iso ∘ f) s ↔ DifferentiableOn 𝕜 f s
[PROOFSTEP]
rw [DifferentiableOn, DifferentiableOn]
[GOAL]
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type u_4
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
G' : Type u_5
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), x ∈ s → DifferentiableWithinAt 𝕜 (↑iso ∘ f) s x) ↔ ∀ (x : G), x ∈ s → DifferentiableWithinAt 𝕜 f s x
[PROOFSTEP]
simp only [iso.comp_differentiableWithinAt_iff]
[GOAL]
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type u_4
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
G' : Type u_5
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
⊢ Differentiable 𝕜 (↑iso ∘ f) ↔ Differentiable 𝕜 f
[PROOFSTEP]
rw [← differentiableOn_univ, ← differentiableOn_univ]
[GOAL]
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type u_4
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
G' : Type u_5
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
⊢ DifferentiableOn 𝕜 (↑iso ∘ f) univ ↔ DifferentiableOn 𝕜 f univ
[PROOFSTEP]
exact iso.comp_differentiableOn_iff
[GOAL]
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type u_4
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
G' : Type u_5
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
f' : G →L[𝕜] E
⊢ HasFDerivWithinAt (↑iso ∘ f) (comp (↑iso) f') s x ↔ HasFDerivWithinAt f f' s x
[PROOFSTEP]
refine' ⟨fun H => _, fun H => iso.hasFDerivAt.comp_hasFDerivWithinAt x H⟩
[GOAL]
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type u_4
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
G' : Type u_5
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
f' : G →L[𝕜] E
H : HasFDerivWithinAt (↑iso ∘ f) (comp (↑iso) f') s x
⊢ HasFDerivWithinAt f f' s x
[PROOFSTEP]
have A : f = iso.symm ∘ iso ∘ f := by
  rw [← Function.comp.assoc, iso.symm_comp_self]
  rfl
[GOAL]
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type u_4
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
G' : Type u_5
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
f' : G →L[𝕜] E
H : HasFDerivWithinAt (↑iso ∘ f) (comp (↑iso) f') s x
⊢ f = ↑(ContinuousLinearEquiv.symm iso) ∘ ↑iso ∘ f
[PROOFSTEP]
rw [← Function.comp.assoc, iso.symm_comp_self]
[GOAL]
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type u_4
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
G' : Type u_5
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
f' : G →L[𝕜] E
H : HasFDerivWithinAt (↑iso ∘ f) (comp (↑iso) f') s x
⊢ f = _root_.id ∘ f
[PROOFSTEP]
rfl
[GOAL]
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type u_4
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
G' : Type u_5
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
f' : G →L[𝕜] E
H : HasFDerivWithinAt (↑iso ∘ f) (comp (↑iso) f') s x
A : f = ↑(ContinuousLinearEquiv.symm iso) ∘ ↑iso ∘ f
⊢ HasFDerivWithinAt f f' s x
[PROOFSTEP]
have B : f' = (iso.symm : F →L[𝕜] E).comp ((iso : E →L[𝕜] F).comp f') := by
  rw [← ContinuousLinearMap.comp_assoc, iso.coe_symm_comp_coe, ContinuousLinearMap.id_comp]
[GOAL]
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type u_4
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
G' : Type u_5
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
f' : G →L[𝕜] E
H : HasFDerivWithinAt (↑iso ∘ f) (comp (↑iso) f') s x
A : f = ↑(ContinuousLinearEquiv.symm iso) ∘ ↑iso ∘ f
⊢ f' = comp (↑(ContinuousLinearEquiv.symm iso)) (comp (↑iso) f')
[PROOFSTEP]
rw [← ContinuousLinearMap.comp_assoc, iso.coe_symm_comp_coe, ContinuousLinearMap.id_comp]
[GOAL]
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type u_4
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
G' : Type u_5
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
f' : G →L[𝕜] E
H : HasFDerivWithinAt (↑iso ∘ f) (comp (↑iso) f') s x
A : f = ↑(ContinuousLinearEquiv.symm iso) ∘ ↑iso ∘ f
B : f' = comp (↑(ContinuousLinearEquiv.symm iso)) (comp (↑iso) f')
⊢ HasFDerivWithinAt f f' s x
[PROOFSTEP]
rw [A, B]
[GOAL]
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type u_4
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
G' : Type u_5
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
f' : G →L[𝕜] E
H : HasFDerivWithinAt (↑iso ∘ f) (comp (↑iso) f') s x
A : f = ↑(ContinuousLinearEquiv.symm iso) ∘ ↑iso ∘ f
B : f' = comp (↑(ContinuousLinearEquiv.symm iso)) (comp (↑iso) f')
⊢ HasFDerivWithinAt (↑(ContinuousLinearEquiv.symm iso) ∘ ↑iso ∘ f)
    (comp (↑(ContinuousLinearEquiv.symm iso)) (comp (↑iso) f')) s x
[PROOFSTEP]
exact iso.symm.hasFDerivAt.comp_hasFDerivWithinAt x H
[GOAL]
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type u_4
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
G' : Type u_5
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
x : G
f' : G →L[𝕜] E
⊢ HasStrictFDerivAt (↑iso ∘ f) (comp (↑iso) f') x ↔ HasStrictFDerivAt f f' x
[PROOFSTEP]
refine' ⟨fun H => _, fun H => iso.hasStrictFDerivAt.comp x H⟩
[GOAL]
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type u_4
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
G' : Type u_5
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
x : G
f' : G →L[𝕜] E
H : HasStrictFDerivAt (↑iso ∘ f) (comp (↑iso) f') x
⊢ HasStrictFDerivAt f f' x
[PROOFSTEP]
convert iso.symm.hasStrictFDerivAt.comp x H using 1
[GOAL]
case h.e'_9
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type u_4
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
G' : Type u_5
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
x : G
f' : G →L[𝕜] E
H : HasStrictFDerivAt (↑iso ∘ f) (comp (↑iso) f') x
⊢ f = fun x => ↑(ContinuousLinearEquiv.symm iso) ((↑iso ∘ f) x)
[PROOFSTEP]
ext z
[GOAL]
case h.e'_10
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type u_4
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
G' : Type u_5
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
x : G
f' : G →L[𝕜] E
H : HasStrictFDerivAt (↑iso ∘ f) (comp (↑iso) f') x
⊢ f' = comp (↑(ContinuousLinearEquiv.symm iso)) (comp (↑iso) f')
[PROOFSTEP]
ext z
[GOAL]
case h.e'_9.h
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type u_4
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
G' : Type u_5
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
x : G
f' : G →L[𝕜] E
H : HasStrictFDerivAt (↑iso ∘ f) (comp (↑iso) f') x
z : G
⊢ f z = ↑(ContinuousLinearEquiv.symm iso) ((↑iso ∘ f) z)
[PROOFSTEP]
apply (iso.symm_apply_apply _).symm
[GOAL]
case h.e'_10.h
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type u_4
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
G' : Type u_5
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
x : G
f' : G →L[𝕜] E
H : HasStrictFDerivAt (↑iso ∘ f) (comp (↑iso) f') x
z : G
⊢ ↑f' z = ↑(comp (↑(ContinuousLinearEquiv.symm iso)) (comp (↑iso) f')) z
[PROOFSTEP]
apply (iso.symm_apply_apply _).symm
[GOAL]
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type u_4
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
G' : Type u_5
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
x : G
f' : G →L[𝕜] E
⊢ HasFDerivAt (↑iso ∘ f) (comp (↑iso) f') x ↔ HasFDerivAt f f' x
[PROOFSTEP]
simp_rw [← hasFDerivWithinAt_univ, iso.comp_hasFDerivWithinAt_iff]
[GOAL]
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type u_4
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
G' : Type u_5
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
f' : G →L[𝕜] F
⊢ HasFDerivWithinAt (↑iso ∘ f) f' s x ↔ HasFDerivWithinAt f (comp (↑(ContinuousLinearEquiv.symm iso)) f') s x
[PROOFSTEP]
rw [← iso.comp_hasFDerivWithinAt_iff, ← ContinuousLinearMap.comp_assoc, iso.coe_comp_coe_symm,
  ContinuousLinearMap.id_comp]
[GOAL]
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type u_4
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
G' : Type u_5
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
x : G
f' : G →L[𝕜] F
⊢ HasFDerivAt (↑iso ∘ f) f' x ↔ HasFDerivAt f (comp (↑(ContinuousLinearEquiv.symm iso)) f') x
[PROOFSTEP]
simp_rw [← hasFDerivWithinAt_univ, iso.comp_hasFDerivWithinAt_iff']
[GOAL]
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type u_4
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
G' : Type u_5
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
hxs : UniqueDiffWithinAt 𝕜 s x
⊢ fderivWithin 𝕜 (↑iso ∘ f) s x = comp (↑iso) (fderivWithin 𝕜 f s x)
[PROOFSTEP]
by_cases h : DifferentiableWithinAt 𝕜 f s x
[GOAL]
case pos
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type u_4
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
G' : Type u_5
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
hxs : UniqueDiffWithinAt 𝕜 s x
h : DifferentiableWithinAt 𝕜 f s x
⊢ fderivWithin 𝕜 (↑iso ∘ f) s x = comp (↑iso) (fderivWithin 𝕜 f s x)
[PROOFSTEP]
rw [fderiv.comp_fderivWithin x iso.differentiableAt h hxs, iso.fderiv]
[GOAL]
case neg
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type u_4
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
G' : Type u_5
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
hxs : UniqueDiffWithinAt 𝕜 s x
h : ¬DifferentiableWithinAt 𝕜 f s x
⊢ fderivWithin 𝕜 (↑iso ∘ f) s x = comp (↑iso) (fderivWithin 𝕜 f s x)
[PROOFSTEP]
have : ¬DifferentiableWithinAt 𝕜 (iso ∘ f) s x := mt iso.comp_differentiableWithinAt_iff.1 h
[GOAL]
case neg
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type u_4
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
G' : Type u_5
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
hxs : UniqueDiffWithinAt 𝕜 s x
h : ¬DifferentiableWithinAt 𝕜 f s x
this : ¬DifferentiableWithinAt 𝕜 (↑iso ∘ f) s x
⊢ fderivWithin 𝕜 (↑iso ∘ f) s x = comp (↑iso) (fderivWithin 𝕜 f s x)
[PROOFSTEP]
rw [fderivWithin_zero_of_not_differentiableWithinAt h, fderivWithin_zero_of_not_differentiableWithinAt this,
  ContinuousLinearMap.comp_zero]
[GOAL]
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type u_4
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
G' : Type u_5
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
x : G
⊢ fderiv 𝕜 (↑iso ∘ f) x = comp (↑iso) (fderiv 𝕜 f x)
[PROOFSTEP]
rw [← fderivWithin_univ, ← fderivWithin_univ]
[GOAL]
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type u_4
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
G' : Type u_5
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
x : G
⊢ fderivWithin 𝕜 (↑iso ∘ f) univ x = comp (↑iso) (fderivWithin 𝕜 f univ x)
[PROOFSTEP]
exact iso.comp_fderivWithin uniqueDiffWithinAt_univ
[GOAL]
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type u_4
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
G' : Type u_5
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
⊢ DifferentiableWithinAt 𝕜 (f ∘ ↑iso) (↑iso ⁻¹' s) x ↔ DifferentiableWithinAt 𝕜 f s (↑iso x)
[PROOFSTEP]
refine' ⟨fun H => _, fun H => H.comp x iso.differentiableWithinAt (mapsTo_preimage _ s)⟩
[GOAL]
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type u_4
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
G' : Type u_5
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
H : DifferentiableWithinAt 𝕜 (f ∘ ↑iso) (↑iso ⁻¹' s) x
⊢ DifferentiableWithinAt 𝕜 f s (↑iso x)
[PROOFSTEP]
have : DifferentiableWithinAt 𝕜 ((f ∘ iso) ∘ iso.symm) s (iso x) :=
  by
  rw [← iso.symm_apply_apply x] at H
  apply H.comp (iso x) iso.symm.differentiableWithinAt
  intro y hy
  simpa only [mem_preimage, apply_symm_apply] using hy
[GOAL]
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type u_4
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
G' : Type u_5
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
H : DifferentiableWithinAt 𝕜 (f ∘ ↑iso) (↑iso ⁻¹' s) x
⊢ DifferentiableWithinAt 𝕜 ((f ∘ ↑iso) ∘ ↑(ContinuousLinearEquiv.symm iso)) s (↑iso x)
[PROOFSTEP]
rw [← iso.symm_apply_apply x] at H
[GOAL]
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type u_4
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
G' : Type u_5
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
H : DifferentiableWithinAt 𝕜 (f ∘ ↑iso) (↑iso ⁻¹' s) (↑(ContinuousLinearEquiv.symm iso) (↑iso x))
⊢ DifferentiableWithinAt 𝕜 ((f ∘ ↑iso) ∘ ↑(ContinuousLinearEquiv.symm iso)) s (↑iso x)
[PROOFSTEP]
apply H.comp (iso x) iso.symm.differentiableWithinAt
[GOAL]
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type u_4
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
G' : Type u_5
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
H : DifferentiableWithinAt 𝕜 (f ∘ ↑iso) (↑iso ⁻¹' s) (↑(ContinuousLinearEquiv.symm iso) (↑iso x))
⊢ MapsTo (↑(ContinuousLinearEquiv.symm iso)) s (↑iso ⁻¹' s)
[PROOFSTEP]
intro y hy
[GOAL]
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type u_4
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
G' : Type u_5
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
H : DifferentiableWithinAt 𝕜 (f ∘ ↑iso) (↑iso ⁻¹' s) (↑(ContinuousLinearEquiv.symm iso) (↑iso x))
y : F
hy : y ∈ s
⊢ ↑(ContinuousLinearEquiv.symm iso) y ∈ ↑iso ⁻¹' s
[PROOFSTEP]
simpa only [mem_preimage, apply_symm_apply] using hy
[GOAL]
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type u_4
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
G' : Type u_5
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
H : DifferentiableWithinAt 𝕜 (f ∘ ↑iso) (↑iso ⁻¹' s) x
this : DifferentiableWithinAt 𝕜 ((f ∘ ↑iso) ∘ ↑(ContinuousLinearEquiv.symm iso)) s (↑iso x)
⊢ DifferentiableWithinAt 𝕜 f s (↑iso x)
[PROOFSTEP]
rwa [Function.comp.assoc, iso.self_comp_symm] at this
[GOAL]
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type u_4
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
G' : Type u_5
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
x : E
⊢ DifferentiableAt 𝕜 (f ∘ ↑iso) x ↔ DifferentiableAt 𝕜 f (↑iso x)
[PROOFSTEP]
simp only [← differentiableWithinAt_univ, ← iso.comp_right_differentiableWithinAt_iff, preimage_univ]
[GOAL]
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type u_4
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
G' : Type u_5
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
⊢ DifferentiableOn 𝕜 (f ∘ ↑iso) (↑iso ⁻¹' s) ↔ DifferentiableOn 𝕜 f s
[PROOFSTEP]
refine' ⟨fun H y hy => _, fun H y hy => iso.comp_right_differentiableWithinAt_iff.2 (H _ hy)⟩
[GOAL]
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type u_4
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
G' : Type u_5
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
H : DifferentiableOn 𝕜 (f ∘ ↑iso) (↑iso ⁻¹' s)
y : F
hy : y ∈ s
⊢ DifferentiableWithinAt 𝕜 f s y
[PROOFSTEP]
rw [← iso.apply_symm_apply y, ← comp_right_differentiableWithinAt_iff]
[GOAL]
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type u_4
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
G' : Type u_5
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
H : DifferentiableOn 𝕜 (f ∘ ↑iso) (↑iso ⁻¹' s)
y : F
hy : y ∈ s
⊢ DifferentiableWithinAt 𝕜 (f ∘ ↑iso) (↑iso ⁻¹' s) (↑(ContinuousLinearEquiv.symm iso) y)
[PROOFSTEP]
apply H
[GOAL]
case a
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type u_4
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
G' : Type u_5
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
H : DifferentiableOn 𝕜 (f ∘ ↑iso) (↑iso ⁻¹' s)
y : F
hy : y ∈ s
⊢ ↑(ContinuousLinearEquiv.symm iso) y ∈ ↑iso ⁻¹' s
[PROOFSTEP]
simpa only [mem_preimage, apply_symm_apply] using hy
[GOAL]
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type u_4
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
G' : Type u_5
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
⊢ Differentiable 𝕜 (f ∘ ↑iso) ↔ Differentiable 𝕜 f
[PROOFSTEP]
simp only [← differentiableOn_univ, ← iso.comp_right_differentiableOn_iff, preimage_univ]
[GOAL]
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type u_4
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
G' : Type u_5
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
f' : F →L[𝕜] G
⊢ HasFDerivWithinAt (f ∘ ↑iso) (comp f' ↑iso) (↑iso ⁻¹' s) x ↔ HasFDerivWithinAt f f' s (↑iso x)
[PROOFSTEP]
refine' ⟨fun H => _, fun H => H.comp x iso.hasFDerivWithinAt (mapsTo_preimage _ s)⟩
[GOAL]
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type u_4
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
G' : Type u_5
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
f' : F →L[𝕜] G
H : HasFDerivWithinAt (f ∘ ↑iso) (comp f' ↑iso) (↑iso ⁻¹' s) x
⊢ HasFDerivWithinAt f f' s (↑iso x)
[PROOFSTEP]
rw [← iso.symm_apply_apply x] at H
[GOAL]
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type u_4
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
G' : Type u_5
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
f' : F →L[𝕜] G
H : HasFDerivWithinAt (f ∘ ↑iso) (comp f' ↑iso) (↑iso ⁻¹' s) (↑(ContinuousLinearEquiv.symm iso) (↑iso x))
⊢ HasFDerivWithinAt f f' s (↑iso x)
[PROOFSTEP]
have A : f = (f ∘ iso) ∘ iso.symm := by
  rw [Function.comp.assoc, iso.self_comp_symm]
  rfl
[GOAL]
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type u_4
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
G' : Type u_5
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
f' : F →L[𝕜] G
H : HasFDerivWithinAt (f ∘ ↑iso) (comp f' ↑iso) (↑iso ⁻¹' s) (↑(ContinuousLinearEquiv.symm iso) (↑iso x))
⊢ f = (f ∘ ↑iso) ∘ ↑(ContinuousLinearEquiv.symm iso)
[PROOFSTEP]
rw [Function.comp.assoc, iso.self_comp_symm]
[GOAL]
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type u_4
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
G' : Type u_5
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
f' : F →L[𝕜] G
H : HasFDerivWithinAt (f ∘ ↑iso) (comp f' ↑iso) (↑iso ⁻¹' s) (↑(ContinuousLinearEquiv.symm iso) (↑iso x))
⊢ f = f ∘ _root_.id
[PROOFSTEP]
rfl
[GOAL]
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type u_4
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
G' : Type u_5
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
f' : F →L[𝕜] G
H : HasFDerivWithinAt (f ∘ ↑iso) (comp f' ↑iso) (↑iso ⁻¹' s) (↑(ContinuousLinearEquiv.symm iso) (↑iso x))
A : f = (f ∘ ↑iso) ∘ ↑(ContinuousLinearEquiv.symm iso)
⊢ HasFDerivWithinAt f f' s (↑iso x)
[PROOFSTEP]
have B : f' = (f'.comp (iso : E →L[𝕜] F)).comp (iso.symm : F →L[𝕜] E) := by
  rw [ContinuousLinearMap.comp_assoc, iso.coe_comp_coe_symm, ContinuousLinearMap.comp_id]
[GOAL]
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type u_4
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
G' : Type u_5
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
f' : F →L[𝕜] G
H : HasFDerivWithinAt (f ∘ ↑iso) (comp f' ↑iso) (↑iso ⁻¹' s) (↑(ContinuousLinearEquiv.symm iso) (↑iso x))
A : f = (f ∘ ↑iso) ∘ ↑(ContinuousLinearEquiv.symm iso)
⊢ f' = comp (comp f' ↑iso) ↑(ContinuousLinearEquiv.symm iso)
[PROOFSTEP]
rw [ContinuousLinearMap.comp_assoc, iso.coe_comp_coe_symm, ContinuousLinearMap.comp_id]
[GOAL]
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type u_4
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
G' : Type u_5
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
f' : F →L[𝕜] G
H : HasFDerivWithinAt (f ∘ ↑iso) (comp f' ↑iso) (↑iso ⁻¹' s) (↑(ContinuousLinearEquiv.symm iso) (↑iso x))
A : f = (f ∘ ↑iso) ∘ ↑(ContinuousLinearEquiv.symm iso)
B : f' = comp (comp f' ↑iso) ↑(ContinuousLinearEquiv.symm iso)
⊢ HasFDerivWithinAt f f' s (↑iso x)
[PROOFSTEP]
rw [A, B]
[GOAL]
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type u_4
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
G' : Type u_5
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
f' : F →L[𝕜] G
H : HasFDerivWithinAt (f ∘ ↑iso) (comp f' ↑iso) (↑iso ⁻¹' s) (↑(ContinuousLinearEquiv.symm iso) (↑iso x))
A : f = (f ∘ ↑iso) ∘ ↑(ContinuousLinearEquiv.symm iso)
B : f' = comp (comp f' ↑iso) ↑(ContinuousLinearEquiv.symm iso)
⊢ HasFDerivWithinAt ((f ∘ ↑iso) ∘ ↑(ContinuousLinearEquiv.symm iso))
    (comp (comp f' ↑iso) ↑(ContinuousLinearEquiv.symm iso)) s (↑iso x)
[PROOFSTEP]
apply H.comp (iso x) iso.symm.hasFDerivWithinAt
[GOAL]
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type u_4
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
G' : Type u_5
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
f' : F →L[𝕜] G
H : HasFDerivWithinAt (f ∘ ↑iso) (comp f' ↑iso) (↑iso ⁻¹' s) (↑(ContinuousLinearEquiv.symm iso) (↑iso x))
A : f = (f ∘ ↑iso) ∘ ↑(ContinuousLinearEquiv.symm iso)
B : f' = comp (comp f' ↑iso) ↑(ContinuousLinearEquiv.symm iso)
⊢ MapsTo (↑(ContinuousLinearEquiv.symm iso)) s (↑iso ⁻¹' s)
[PROOFSTEP]
intro y hy
[GOAL]
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type u_4
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
G' : Type u_5
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
f' : F →L[𝕜] G
H : HasFDerivWithinAt (f ∘ ↑iso) (comp f' ↑iso) (↑iso ⁻¹' s) (↑(ContinuousLinearEquiv.symm iso) (↑iso x))
A : f = (f ∘ ↑iso) ∘ ↑(ContinuousLinearEquiv.symm iso)
B : f' = comp (comp f' ↑iso) ↑(ContinuousLinearEquiv.symm iso)
y : F
hy : y ∈ s
⊢ ↑(ContinuousLinearEquiv.symm iso) y ∈ ↑iso ⁻¹' s
[PROOFSTEP]
simpa only [mem_preimage, apply_symm_apply] using hy
[GOAL]
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type u_4
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
G' : Type u_5
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
x : E
f' : F →L[𝕜] G
⊢ HasFDerivAt (f ∘ ↑iso) (comp f' ↑iso) x ↔ HasFDerivAt f f' (↑iso x)
[PROOFSTEP]
simp only [← hasFDerivWithinAt_univ, ← comp_right_hasFDerivWithinAt_iff, preimage_univ]
[GOAL]
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type u_4
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
G' : Type u_5
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
f' : E →L[𝕜] G
⊢ HasFDerivWithinAt (f ∘ ↑iso) f' (↑iso ⁻¹' s) x ↔
    HasFDerivWithinAt f (comp f' ↑(ContinuousLinearEquiv.symm iso)) s (↑iso x)
[PROOFSTEP]
rw [← iso.comp_right_hasFDerivWithinAt_iff, ContinuousLinearMap.comp_assoc, iso.coe_symm_comp_coe,
  ContinuousLinearMap.comp_id]
[GOAL]
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type u_4
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
G' : Type u_5
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
x : E
f' : E →L[𝕜] G
⊢ HasFDerivAt (f ∘ ↑iso) f' x ↔ HasFDerivAt f (comp f' ↑(ContinuousLinearEquiv.symm iso)) (↑iso x)
[PROOFSTEP]
simp only [← hasFDerivWithinAt_univ, ← iso.comp_right_hasFDerivWithinAt_iff', preimage_univ]
[GOAL]
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type u_4
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
G' : Type u_5
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
[PROOFSTEP]
by_cases h : DifferentiableWithinAt 𝕜 f s (iso x)
[GOAL]
case pos
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type u_4
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
G' : Type u_5
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
[PROOFSTEP]
exact (iso.comp_right_hasFDerivWithinAt_iff.2 h.hasFDerivWithinAt).fderivWithin hxs
[GOAL]
case neg
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type u_4
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
G' : Type u_5
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
[PROOFSTEP]
have : ¬DifferentiableWithinAt 𝕜 (f ∘ iso) (iso ⁻¹' s) x :=
  by
  intro h'
  exact h (iso.comp_right_differentiableWithinAt_iff.1 h')
[GOAL]
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type u_4
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
G' : Type u_5
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
[PROOFSTEP]
intro h'
[GOAL]
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type u_4
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
G' : Type u_5
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
[PROOFSTEP]
exact h (iso.comp_right_differentiableWithinAt_iff.1 h')
[GOAL]
case neg
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type u_4
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
G' : Type u_5
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
[PROOFSTEP]
rw [fderivWithin_zero_of_not_differentiableWithinAt h, fderivWithin_zero_of_not_differentiableWithinAt this,
  ContinuousLinearMap.zero_comp]
[GOAL]
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type u_4
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
G' : Type u_5
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
x : E
⊢ fderiv 𝕜 (f ∘ ↑iso) x = comp (fderiv 𝕜 f (↑iso x)) ↑iso
[PROOFSTEP]
rw [← fderivWithin_univ, ← fderivWithin_univ, ← iso.comp_right_fderivWithin, preimage_univ]
[GOAL]
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type u_4
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
G' : Type u_5
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
x : E
⊢ UniqueDiffWithinAt 𝕜 (↑iso ⁻¹' univ) x
[PROOFSTEP]
exact uniqueDiffWithinAt_univ
[GOAL]
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type u_4
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
G' : Type u_5
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 → F
f' : E ≃L[𝕜] F
g : F → E
a : F
hg : ContinuousAt g a
hf : HasStrictFDerivAt f (↑f') (g a)
hfg : ∀ᶠ (y : F) in 𝓝 a, f (g y) = y
⊢ HasStrictFDerivAt g (↑(ContinuousLinearEquiv.symm f')) a
[PROOFSTEP]
replace hg := hg.prod_map' hg
[GOAL]
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type u_4
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
G' : Type u_5
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 → F
f' : E ≃L[𝕜] F
g : F → E
a : F
hf : HasStrictFDerivAt f (↑f') (g a)
hfg : ∀ᶠ (y : F) in 𝓝 a, f (g y) = y
hg : ContinuousAt (fun p => (g p.fst, g p.snd)) (a, a)
⊢ HasStrictFDerivAt g (↑(ContinuousLinearEquiv.symm f')) a
[PROOFSTEP]
replace hfg := hfg.prod_mk_nhds hfg
[GOAL]
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type u_4
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
G' : Type u_5
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 → F
f' : E ≃L[𝕜] F
g : F → E
a : F
hf : HasStrictFDerivAt f (↑f') (g a)
hg : ContinuousAt (fun p => (g p.fst, g p.snd)) (a, a)
hfg : ∀ᶠ (p : F × F) in 𝓝 (a, a), f (g p.fst) = p.fst ∧ f (g p.snd) = p.snd
⊢ HasStrictFDerivAt g (↑(ContinuousLinearEquiv.symm f')) a
[PROOFSTEP]
have :
  (fun p : F × F => g p.1 - g p.2 - f'.symm (p.1 - p.2)) =O[𝓝 (a, a)] fun p : F × F =>
    f' (g p.1 - g p.2) - (p.1 - p.2) :=
  by
  refine' ((f'.symm : F →L[𝕜] E).isBigO_comp _ _).congr (fun x => _) fun _ => rfl
  simp
[GOAL]
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type u_4
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
G' : Type u_5
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 → F
f' : E ≃L[𝕜] F
g : F → E
a : F
hf : HasStrictFDerivAt f (↑f') (g a)
hg : ContinuousAt (fun p => (g p.fst, g p.snd)) (a, a)
hfg : ∀ᶠ (p : F × F) in 𝓝 (a, a), f (g p.fst) = p.fst ∧ f (g p.snd) = p.snd
⊢ (fun p => g p.fst - g p.snd - ↑(ContinuousLinearEquiv.symm f') (p.fst - p.snd)) =O[𝓝 (a, a)] fun p =>
    ↑f' (g p.fst - g p.snd) - (p.fst - p.snd)
[PROOFSTEP]
refine' ((f'.symm : F →L[𝕜] E).isBigO_comp _ _).congr (fun x => _) fun _ => rfl
[GOAL]
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type u_4
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
G' : Type u_5
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 → F
f' : E ≃L[𝕜] F
g : F → E
a : F
hf : HasStrictFDerivAt f (↑f') (g a)
hg : ContinuousAt (fun p => (g p.fst, g p.snd)) (a, a)
hfg : ∀ᶠ (p : F × F) in 𝓝 (a, a), f (g p.fst) = p.fst ∧ f (g p.snd) = p.snd
x : F × F
⊢ ↑↑(ContinuousLinearEquiv.symm f') (↑f' (g x.fst - g x.snd) - (x.fst - x.snd)) =
    g x.fst - g x.snd - ↑(ContinuousLinearEquiv.symm f') (x.fst - x.snd)
[PROOFSTEP]
simp
[GOAL]
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type u_4
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
G' : Type u_5
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 → F
f' : E ≃L[𝕜] F
g : F → E
a : F
hf : HasStrictFDerivAt f (↑f') (g a)
hg : ContinuousAt (fun p => (g p.fst, g p.snd)) (a, a)
hfg : ∀ᶠ (p : F × F) in 𝓝 (a, a), f (g p.fst) = p.fst ∧ f (g p.snd) = p.snd
this :
  (fun p => g p.fst - g p.snd - ↑(ContinuousLinearEquiv.symm f') (p.fst - p.snd)) =O[𝓝 (a, a)] fun p =>
    ↑f' (g p.fst - g p.snd) - (p.fst - p.snd)
⊢ HasStrictFDerivAt g (↑(ContinuousLinearEquiv.symm f')) a
[PROOFSTEP]
refine' this.trans_isLittleO _
[GOAL]
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type u_4
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
G' : Type u_5
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 → F
f' : E ≃L[𝕜] F
g : F → E
a : F
hf : HasStrictFDerivAt f (↑f') (g a)
hg : ContinuousAt (fun p => (g p.fst, g p.snd)) (a, a)
hfg : ∀ᶠ (p : F × F) in 𝓝 (a, a), f (g p.fst) = p.fst ∧ f (g p.snd) = p.snd
this :
  (fun p => g p.fst - g p.snd - ↑(ContinuousLinearEquiv.symm f') (p.fst - p.snd)) =O[𝓝 (a, a)] fun p =>
    ↑f' (g p.fst - g p.snd) - (p.fst - p.snd)
⊢ (fun p => ↑f' (g p.fst - g p.snd) - (p.fst - p.snd)) =o[𝓝 (a, a)] fun p => p.fst - p.snd
[PROOFSTEP]
clear this
[GOAL]
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type u_4
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
G' : Type u_5
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 → F
f' : E ≃L[𝕜] F
g : F → E
a : F
hf : HasStrictFDerivAt f (↑f') (g a)
hg : ContinuousAt (fun p => (g p.fst, g p.snd)) (a, a)
hfg : ∀ᶠ (p : F × F) in 𝓝 (a, a), f (g p.fst) = p.fst ∧ f (g p.snd) = p.snd
⊢ (fun p => ↑f' (g p.fst - g p.snd) - (p.fst - p.snd)) =o[𝓝 (a, a)] fun p => p.fst - p.snd
[PROOFSTEP]
refine' ((hf.comp_tendsto hg).symm.congr' (hfg.mono _) (eventually_of_forall fun _ => rfl)).trans_isBigO _
[GOAL]
case refine'_1
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type u_4
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
G' : Type u_5
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 → F
f' : E ≃L[𝕜] F
g : F → E
a : F
hf : HasStrictFDerivAt f (↑f') (g a)
hg : ContinuousAt (fun p => (g p.fst, g p.snd)) (a, a)
hfg : ∀ᶠ (p : F × F) in 𝓝 (a, a), f (g p.fst) = p.fst ∧ f (g p.snd) = p.snd
⊢ ∀ (x : F × F),
    f (g x.fst) = x.fst ∧ f (g x.snd) = x.snd →
      (fun x =>
            ↑↑f' (((fun p => (g p.fst, g p.snd)) x).fst - ((fun p => (g p.fst, g p.snd)) x).snd) -
              (f ((fun p => (g p.fst, g p.snd)) x).fst - f ((fun p => (g p.fst, g p.snd)) x).snd))
          x =
        ↑f' (g x.fst - g x.snd) - (x.fst - x.snd)
[PROOFSTEP]
rintro p ⟨hp1, hp2⟩
[GOAL]
case refine'_1.intro
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type u_4
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
G' : Type u_5
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 → F
f' : E ≃L[𝕜] F
g : F → E
a : F
hf : HasStrictFDerivAt f (↑f') (g a)
hg : ContinuousAt (fun p => (g p.fst, g p.snd)) (a, a)
hfg : ∀ᶠ (p : F × F) in 𝓝 (a, a), f (g p.fst) = p.fst ∧ f (g p.snd) = p.snd
p : F × F
hp1 : f (g p.fst) = p.fst
hp2 : f (g p.snd) = p.snd
⊢ (fun x =>
        ↑↑f' (((fun p => (g p.fst, g p.snd)) x).fst - ((fun p => (g p.fst, g p.snd)) x).snd) -
          (f ((fun p => (g p.fst, g p.snd)) x).fst - f ((fun p => (g p.fst, g p.snd)) x).snd))
      p =
    ↑f' (g p.fst - g p.snd) - (p.fst - p.snd)
[PROOFSTEP]
simp [hp1, hp2]
[GOAL]
case refine'_2
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type u_4
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
G' : Type u_5
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 → F
f' : E ≃L[𝕜] F
g : F → E
a : F
hf : HasStrictFDerivAt f (↑f') (g a)
hg : ContinuousAt (fun p => (g p.fst, g p.snd)) (a, a)
hfg : ∀ᶠ (p : F × F) in 𝓝 (a, a), f (g p.fst) = p.fst ∧ f (g p.snd) = p.snd
⊢ (fun x => ((fun p => p.fst - p.snd) ∘ fun p => (g p.fst, g p.snd)) x) =O[𝓝 (a, a)] fun p => p.fst - p.snd
[PROOFSTEP]
refine (hf.isBigO_sub_rev.comp_tendsto hg).congr' (eventually_of_forall fun _ => rfl) (hfg.mono ?_)
[GOAL]
case refine'_2
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type u_4
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
G' : Type u_5
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 → F
f' : E ≃L[𝕜] F
g : F → E
a : F
hf : HasStrictFDerivAt f (↑f') (g a)
hg : ContinuousAt (fun p => (g p.fst, g p.snd)) (a, a)
hfg : ∀ᶠ (p : F × F) in 𝓝 (a, a), f (g p.fst) = p.fst ∧ f (g p.snd) = p.snd
⊢ ∀ (x : F × F),
    f (g x.fst) = x.fst ∧ f (g x.snd) = x.snd →
      ((fun p => f p.fst - f p.snd) ∘ fun p => (g p.fst, g p.snd)) x = (fun p => p.fst - p.snd) x
[PROOFSTEP]
rintro p ⟨hp1, hp2⟩
[GOAL]
case refine'_2.intro
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type u_4
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
G' : Type u_5
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 → F
f' : E ≃L[𝕜] F
g : F → E
a : F
hf : HasStrictFDerivAt f (↑f') (g a)
hg : ContinuousAt (fun p => (g p.fst, g p.snd)) (a, a)
hfg : ∀ᶠ (p : F × F) in 𝓝 (a, a), f (g p.fst) = p.fst ∧ f (g p.snd) = p.snd
p : F × F
hp1 : f (g p.fst) = p.fst
hp2 : f (g p.snd) = p.snd
⊢ ((fun p => f p.fst - f p.snd) ∘ fun p => (g p.fst, g p.snd)) p = (fun p => p.fst - p.snd) p
[PROOFSTEP]
simp only [(· ∘ ·), hp1, hp2]
[GOAL]
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type u_4
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
G' : Type u_5
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 → F
f' : E ≃L[𝕜] F
g : F → E
a : F
hg : ContinuousAt g a
hf : HasFDerivAt f (↑f') (g a)
hfg : ∀ᶠ (y : F) in 𝓝 a, f (g y) = y
⊢ HasFDerivAt g (↑(ContinuousLinearEquiv.symm f')) a
[PROOFSTEP]
have : (fun x : F => g x - g a - f'.symm (x - a)) =O[𝓝 a] fun x : F => f' (g x - g a) - (x - a) :=
  by
  refine' ((f'.symm : F →L[𝕜] E).isBigO_comp _ _).congr (fun x => _) fun _ => rfl
  simp
[GOAL]
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type u_4
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
G' : Type u_5
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 → F
f' : E ≃L[𝕜] F
g : F → E
a : F
hg : ContinuousAt g a
hf : HasFDerivAt f (↑f') (g a)
hfg : ∀ᶠ (y : F) in 𝓝 a, f (g y) = y
⊢ (fun x => g x - g a - ↑(ContinuousLinearEquiv.symm f') (x - a)) =O[𝓝 a] fun x => ↑f' (g x - g a) - (x - a)
[PROOFSTEP]
refine' ((f'.symm : F →L[𝕜] E).isBigO_comp _ _).congr (fun x => _) fun _ => rfl
[GOAL]
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type u_4
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
G' : Type u_5
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 → F
f' : E ≃L[𝕜] F
g : F → E
a : F
hg : ContinuousAt g a
hf : HasFDerivAt f (↑f') (g a)
hfg : ∀ᶠ (y : F) in 𝓝 a, f (g y) = y
x : F
⊢ ↑↑(ContinuousLinearEquiv.symm f') (↑f' (g x - g a) - (x - a)) = g x - g a - ↑(ContinuousLinearEquiv.symm f') (x - a)
[PROOFSTEP]
simp
[GOAL]
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type u_4
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
G' : Type u_5
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 → F
f' : E ≃L[𝕜] F
g : F → E
a : F
hg : ContinuousAt g a
hf : HasFDerivAt f (↑f') (g a)
hfg : ∀ᶠ (y : F) in 𝓝 a, f (g y) = y
this : (fun x => g x - g a - ↑(ContinuousLinearEquiv.symm f') (x - a)) =O[𝓝 a] fun x => ↑f' (g x - g a) - (x - a)
⊢ HasFDerivAt g (↑(ContinuousLinearEquiv.symm f')) a
[PROOFSTEP]
refine' this.trans_isLittleO _
[GOAL]
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type u_4
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
G' : Type u_5
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 → F
f' : E ≃L[𝕜] F
g : F → E
a : F
hg : ContinuousAt g a
hf : HasFDerivAt f (↑f') (g a)
hfg : ∀ᶠ (y : F) in 𝓝 a, f (g y) = y
this : (fun x => g x - g a - ↑(ContinuousLinearEquiv.symm f') (x - a)) =O[𝓝 a] fun x => ↑f' (g x - g a) - (x - a)
⊢ (fun x => ↑f' (g x - g a) - (x - a)) =o[𝓝 a] fun x' => x' - a
[PROOFSTEP]
clear this
[GOAL]
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type u_4
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
G' : Type u_5
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 → F
f' : E ≃L[𝕜] F
g : F → E
a : F
hg : ContinuousAt g a
hf : HasFDerivAt f (↑f') (g a)
hfg : ∀ᶠ (y : F) in 𝓝 a, f (g y) = y
⊢ (fun x => ↑f' (g x - g a) - (x - a)) =o[𝓝 a] fun x' => x' - a
[PROOFSTEP]
refine' ((hf.comp_tendsto hg).symm.congr' (hfg.mono _) (eventually_of_forall fun _ => rfl)).trans_isBigO _
[GOAL]
case refine'_1
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type u_4
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
G' : Type u_5
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 → F
f' : E ≃L[𝕜] F
g : F → E
a : F
hg : ContinuousAt g a
hf : HasFDerivAt f (↑f') (g a)
hfg : ∀ᶠ (y : F) in 𝓝 a, f (g y) = y
⊢ ∀ (x : F), f (g x) = x → (fun x => ↑↑f' (g x - g a) - (f (g x) - f (g a))) x = ↑f' (g x - g a) - (x - a)
[PROOFSTEP]
rintro p hp
[GOAL]
case refine'_1
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type u_4
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
G' : Type u_5
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 → F
f' : E ≃L[𝕜] F
g : F → E
a : F
hg : ContinuousAt g a
hf : HasFDerivAt f (↑f') (g a)
hfg : ∀ᶠ (y : F) in 𝓝 a, f (g y) = y
p : F
hp : f (g p) = p
⊢ (fun x => ↑↑f' (g x - g a) - (f (g x) - f (g a))) p = ↑f' (g p - g a) - (p - a)
[PROOFSTEP]
simp [hp, hfg.self_of_nhds]
[GOAL]
case refine'_2
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type u_4
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
G' : Type u_5
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 → F
f' : E ≃L[𝕜] F
g : F → E
a : F
hg : ContinuousAt g a
hf : HasFDerivAt f (↑f') (g a)
hfg : ∀ᶠ (y : F) in 𝓝 a, f (g y) = y
⊢ (fun x => ((fun x' => x' - g a) ∘ g) x) =O[𝓝 a] fun x' => x' - a
[PROOFSTEP]
refine' ((hf.isBigO_sub_rev f'.antilipschitz).comp_tendsto hg).congr' (eventually_of_forall fun _ => rfl) (hfg.mono _)
[GOAL]
case refine'_2
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type u_4
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
G' : Type u_5
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 → F
f' : E ≃L[𝕜] F
g : F → E
a : F
hg : ContinuousAt g a
hf : HasFDerivAt f (↑f') (g a)
hfg : ∀ᶠ (y : F) in 𝓝 a, f (g y) = y
⊢ ∀ (x : F), f (g x) = x → ((fun x' => f x' - f (g a)) ∘ g) x = (fun x' => x' - a) x
[PROOFSTEP]
rintro p hp
[GOAL]
case refine'_2
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type u_4
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
G' : Type u_5
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 → F
f' : E ≃L[𝕜] F
g : F → E
a : F
hg : ContinuousAt g a
hf : HasFDerivAt f (↑f') (g a)
hfg : ∀ᶠ (y : F) in 𝓝 a, f (g y) = y
p : F
hp : f (g p) = p
⊢ ((fun x' => f x' - f (g a)) ∘ g) p = (fun x' => x' - a) p
[PROOFSTEP]
simp only [(· ∘ ·), hp, hfg.self_of_nhds]
[GOAL]
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type u_4
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
G' : Type u_5
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
h : HasFDerivWithinAt f f' s x
hf' : ∃ C, ∀ (z : E), ‖z‖ ≤ C * ‖↑f' z‖
⊢ ∀ᶠ (z : E) in 𝓝[s \ {x}] x, f z ≠ f x
[PROOFSTEP]
rw [nhdsWithin, diff_eq, ← inf_principal, ← inf_assoc, eventually_inf_principal]
[GOAL]
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type u_4
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
G' : Type u_5
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
h : HasFDerivWithinAt f f' s x
hf' : ∃ C, ∀ (z : E), ‖z‖ ≤ C * ‖↑f' z‖
⊢ ∀ᶠ (x_1 : E) in 𝓝 x ⊓ 𝓟 s, x_1 ∈ {x}ᶜ → f x_1 ≠ f x
[PROOFSTEP]
have A : (fun z => z - x) =O[𝓝[s] x] fun z => f' (z - x) :=
  isBigO_iff.2 <| hf'.imp fun C hC => eventually_of_forall fun z => hC _
[GOAL]
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type u_4
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
G' : Type u_5
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
h : HasFDerivWithinAt f f' s x
hf' : ∃ C, ∀ (z : E), ‖z‖ ≤ C * ‖↑f' z‖
A : (fun z => z - x) =O[𝓝[s] x] fun z => ↑f' (z - x)
⊢ ∀ᶠ (x_1 : E) in 𝓝 x ⊓ 𝓟 s, x_1 ∈ {x}ᶜ → f x_1 ≠ f x
[PROOFSTEP]
have : (fun z => f z - f x) ~[𝓝[s] x] fun z => f' (z - x) := h.trans_isBigO A
[GOAL]
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type u_4
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
G' : Type u_5
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
h : HasFDerivWithinAt f f' s x
hf' : ∃ C, ∀ (z : E), ‖z‖ ≤ C * ‖↑f' z‖
A : (fun z => z - x) =O[𝓝[s] x] fun z => ↑f' (z - x)
this : (fun z => f z - f x) ~[𝓝[s] x] fun z => ↑f' (z - x)
⊢ ∀ᶠ (x_1 : E) in 𝓝 x ⊓ 𝓟 s, x_1 ∈ {x}ᶜ → f x_1 ≠ f x
[PROOFSTEP]
simpa [not_imp_not, sub_eq_zero] using (A.trans this.isBigO_symm).eq_zero_imp
[GOAL]
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type u_4
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
G' : Type u_5
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
h : HasFDerivAt f f' x
hf' : ∃ C, ∀ (z : E), ‖z‖ ≤ C * ‖↑f' z‖
⊢ ∀ᶠ (z : E) in 𝓝[{x}ᶜ] x, f z ≠ f x
[PROOFSTEP]
simpa only [compl_eq_univ_diff] using (hasFDerivWithinAt_univ.2 h).eventually_ne hf'
[GOAL]
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
f' : E →L[ℝ] F
x : E
L : Filter E
⊢ Tendsto (fun x' => ‖x' - x‖⁻¹ * ‖f x' - f x - ↑f' (x' - x)‖) L (𝓝 0) ↔
    Tendsto (fun x' => ‖x' - x‖⁻¹ • (f x' - f x - ↑f' (x' - x))) L (𝓝 0)
[PROOFSTEP]
symm
[GOAL]
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
f' : E →L[ℝ] F
x : E
L : Filter E
⊢ Tendsto (fun x' => ‖x' - x‖⁻¹ • (f x' - f x - ↑f' (x' - x))) L (𝓝 0) ↔
    Tendsto (fun x' => ‖x' - x‖⁻¹ * ‖f x' - f x - ↑f' (x' - x)‖) L (𝓝 0)
[PROOFSTEP]
rw [tendsto_iff_norm_tendsto_zero]
[GOAL]
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
f' : E →L[ℝ] F
x : E
L : Filter E
⊢ Tendsto (fun e => ‖‖e - x‖⁻¹ • (f e - f x - ↑f' (e - x)) - 0‖) L (𝓝 0) ↔
    Tendsto (fun x' => ‖x' - x‖⁻¹ * ‖f x' - f x - ↑f' (x' - x)‖) L (𝓝 0)
[PROOFSTEP]
refine' tendsto_congr fun x' => _
[GOAL]
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
f' : E →L[ℝ] F
x : E
L : Filter E
x' : E
⊢ ‖‖x' - x‖⁻¹ • (f x' - f x - ↑f' (x' - x)) - 0‖ = ‖x' - x‖⁻¹ * ‖f x' - f x - ↑f' (x' - x)‖
[PROOFSTEP]
simp [norm_smul]
[GOAL]
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
f' : E →L[ℝ] F
x : E
hf : HasFDerivAt f f' x
v : E
⊢ Tendsto (fun c => c • (f (x + c⁻¹ • v) - f x)) atTop (𝓝 (↑f' v))
[PROOFSTEP]
apply hf.lim v
[GOAL]
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
f' : E →L[ℝ] F
x : E
hf : HasFDerivAt f f' x
v : E
⊢ Tendsto (fun n => ‖n‖) atTop atTop
[PROOFSTEP]
rw [tendsto_atTop_atTop]
[GOAL]
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
f' : E →L[ℝ] F
x : E
hf : HasFDerivAt f f' x
v : E
⊢ ∀ (b : ℝ), ∃ i, ∀ (a : ℝ), i ≤ a → b ≤ ‖a‖
[PROOFSTEP]
exact fun b => ⟨b, fun a ha => le_trans ha (le_abs_self _)⟩
[GOAL]
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
s : Set E
f' : E →L[𝕜] F
x : E
h : HasFDerivWithinAt f f' s x
⊢ MapsTo (↑f') (tangentConeAt 𝕜 s x) (tangentConeAt 𝕜 (f '' s) (f x))
[PROOFSTEP]
rintro v ⟨c, d, dtop, clim, cdlim⟩
[GOAL]
case intro.intro.intro.intro
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
s : Set E
f' : E →L[𝕜] F
x : E
h : HasFDerivWithinAt f f' s x
v : E
c : ℕ → 𝕜
d : ℕ → E
dtop : ∀ᶠ (n : ℕ) in atTop, x + d n ∈ s
clim : Tendsto (fun n => ‖c n‖) atTop atTop
cdlim : Tendsto (fun n => c n • d n) atTop (𝓝 v)
⊢ ↑f' v ∈ tangentConeAt 𝕜 (f '' s) (f x)
[PROOFSTEP]
refine' ⟨c, fun n => f (x + d n) - f x, mem_of_superset dtop _, clim, h.lim atTop dtop clim cdlim⟩
[GOAL]
case intro.intro.intro.intro
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
s : Set E
f' : E →L[𝕜] F
x : E
h : HasFDerivWithinAt f f' s x
v : E
c : ℕ → 𝕜
d : ℕ → E
dtop : ∀ᶠ (n : ℕ) in atTop, x + d n ∈ s
clim : Tendsto (fun n => ‖c n‖) atTop atTop
cdlim : Tendsto (fun n => c n • d n) atTop (𝓝 v)
⊢ {x_1 | (fun n => x + d n ∈ s) x_1} ⊆ {x_1 | (fun n => f x + (fun n => f (x + d n) - f x) n ∈ f '' s) x_1}
[PROOFSTEP]
simp (config := { contextual := true }) [-mem_image, mem_image_of_mem]
[GOAL]
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
s : Set E
f' : E →L[𝕜] F
x : E
h : HasFDerivWithinAt f f' s x
hs : UniqueDiffWithinAt 𝕜 s x
h' : DenseRange ↑f'
⊢ UniqueDiffWithinAt 𝕜 (f '' s) (f x)
[PROOFSTEP]
refine' ⟨h'.dense_of_mapsTo f'.continuous hs.1 _, h.continuousWithinAt.mem_closure_image hs.2⟩
[GOAL]
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
s : Set E
f' : E →L[𝕜] F
x : E
h : HasFDerivWithinAt f f' s x
hs : UniqueDiffWithinAt 𝕜 s x
h' : DenseRange ↑f'
⊢ MapsTo ↑f' ↑(Submodule.span 𝕜 (tangentConeAt 𝕜 s x)) ↑(Submodule.span 𝕜 (tangentConeAt 𝕜 (f '' s) (f x)))
[PROOFSTEP]
show Submodule.span 𝕜 (tangentConeAt 𝕜 s x) ≤ (Submodule.span 𝕜 (tangentConeAt 𝕜 (f '' s) (f x))).comap f'
[GOAL]
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
s : Set E
f' : E →L[𝕜] F
x : E
h : HasFDerivWithinAt f f' s x
hs : UniqueDiffWithinAt 𝕜 s x
h' : DenseRange ↑f'
⊢ Submodule.span 𝕜 (tangentConeAt 𝕜 s x) ≤ Submodule.comap f' (Submodule.span 𝕜 (tangentConeAt 𝕜 (f '' s) (f x)))
[PROOFSTEP]
rw [Submodule.span_le]
[GOAL]
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
s : Set E
f' : E →L[𝕜] F
x : E
h : HasFDerivWithinAt f f' s x
hs : UniqueDiffWithinAt 𝕜 s x
h' : DenseRange ↑f'
⊢ tangentConeAt 𝕜 s x ⊆ ↑(Submodule.comap f' (Submodule.span 𝕜 (tangentConeAt 𝕜 (f '' s) (f x))))
[PROOFSTEP]
exact h.mapsTo_tangent_cone.mono Subset.rfl Submodule.subset_span
[GOAL]
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
s : Set E
f' : E →L[𝕜] F
e : F ≃L[𝕜] E
⊢ UniqueDiffOn 𝕜 (↑e ⁻¹' s) ↔ UniqueDiffOn 𝕜 s
[PROOFSTEP]
rw [← e.image_symm_eq_preimage, e.symm.uniqueDiffOn_image_iff]