mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Calculus.FDeriv.Add

Goal state before:
pp: 𝕜 : 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
f' : E →L[𝕜] F
x : E
c : F
⊢ HasStrictFDerivAt (fun x ↦ c + f x) f' x ↔ HasStrictFDerivAt f f' x

Tactic:
simpa using

Goal state after:
𝕜 : 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
f' : E →L[𝕜] F
x : E
c : F
⊢ HasStrictFDerivAt (fun x ↦ c + f x) f' x ↔ HasStrictFDerivAt f f' x
Module: Mathlib.Analysis.Calculus.FDeriv.Add

Goal state before:
pp: 𝕜 : 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
x : E
s : Set E
c : F
⊢ fderivWithin 𝕜 (fun y ↦ c + f y) s x = fderivWithin 𝕜 f s x

Tactic:
simpa using

Goal state after:
𝕜 : 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
x : E
s : Set E
c : F
⊢ fderivWithin 𝕜 (fun y ↦ c + f y) s x = fderivWithin 𝕜 f s x
Module: Mathlib.Analysis.Calculus.FDeriv.Add

Goal state before:
pp: 𝕜 : 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
x : E
s : Set E
h : DifferentiableWithinAt 𝕜 (fun y ↦ -f y) s x
⊢ DifferentiableWithinAt 𝕜 f s x

Tactic:
simpa using

Goal state after:
𝕜 : 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
x : E
s : Set E
h : DifferentiableWithinAt 𝕜 (fun y ↦ -f y) s x
⊢ DifferentiableWithinAt 𝕜 f s x
Module: Mathlib.Analysis.Calculus.FDeriv.Add

Goal state before:
pp: 𝕜 : 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
x : E
s : Set E
h : DifferentiableWithinAt 𝕜 (-f) s x
⊢ DifferentiableWithinAt 𝕜 f s x

Tactic:
simpa using

Goal state after:
𝕜 : 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
x : E
s : Set E
h : DifferentiableWithinAt 𝕜 (-f) s x
⊢ DifferentiableWithinAt 𝕜 f s x
Module: Mathlib.Analysis.Calculus.FDeriv.Add

Goal state before:
pp: 𝕜 : 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
x : E
h : DifferentiableAt 𝕜 (fun y ↦ -f y) x
⊢ DifferentiableAt 𝕜 f x

Tactic:
simpa using

Goal state after:
𝕜 : 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
x : E
h : DifferentiableAt 𝕜 (fun y ↦ -f y) x
⊢ DifferentiableAt 𝕜 f x
Module: Mathlib.Analysis.Calculus.FDeriv.Add

Goal state before:
pp: 𝕜 : 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
x : E
h : DifferentiableAt 𝕜 (-f) x
⊢ DifferentiableAt 𝕜 f x

Tactic:
simpa using

Goal state after:
𝕜 : 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
x : E
h : DifferentiableAt 𝕜 (-f) x
⊢ DifferentiableAt 𝕜 f x
Module: Mathlib.Analysis.Calculus.FDeriv.Add

Goal state before:
pp: 𝕜 : 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
h : DifferentiableOn 𝕜 (fun y ↦ -f y) s
⊢ DifferentiableOn 𝕜 f s

Tactic:
simpa using

Goal state after:
𝕜 : 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
h : DifferentiableOn 𝕜 (fun y ↦ -f y) s
⊢ DifferentiableOn 𝕜 f s
Module: Mathlib.Analysis.Calculus.FDeriv.Add

Goal state before:
pp: 𝕜 : 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
h : DifferentiableOn 𝕜 (-f) s
⊢ DifferentiableOn 𝕜 f s

Tactic:
simpa using

Goal state after:
𝕜 : 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
h : DifferentiableOn 𝕜 (-f) s
⊢ DifferentiableOn 𝕜 f s
Module: Mathlib.Analysis.Calculus.FDeriv.Add

Goal state before:
pp: 𝕜 : 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
h : Differentiable 𝕜 fun y ↦ -f y
⊢ Differentiable 𝕜 f

Tactic:
simpa using

Goal state after:
𝕜 : 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
h : Differentiable 𝕜 fun y ↦ -f y
⊢ Differentiable 𝕜 f
Module: Mathlib.Analysis.Calculus.FDeriv.Add

Goal state before:
pp: 𝕜 : 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
h : Differentiable 𝕜 (-f)
⊢ Differentiable 𝕜 f

Tactic:
simpa using

Goal state after:
𝕜 : 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
h : Differentiable 𝕜 (-f)
⊢ Differentiable 𝕜 f
Module: Mathlib.Analysis.Calculus.FDeriv.Add

Goal state before:
pp: 𝕜 : 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 g : E → F
f' g' : E →L[𝕜] F
L : Filter (E × E)
hf : HasFDerivAtFilter f f' L
hg : HasFDerivAtFilter g g' L
⊢ HasFDerivAtFilter (f - g) (f' - g') L

Tactic:
simpa using

Goal state after:
𝕜 : 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 g : E → F
f' g' : E →L[𝕜] F
L : Filter (E × E)
hf : HasFDerivAtFilter f f' L
hg : HasFDerivAtFilter g g' L
⊢ HasFDerivAtFilter (f + -g) (f' + -g') L
Module: Mathlib.Analysis.Calculus.FDeriv.Add

Goal state before:
pp: 𝕜 : 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 g : E → F
x : E
hg : DifferentiableAt 𝕜 g x
h : DifferentiableAt 𝕜 (f + g) x
⊢ DifferentiableAt 𝕜 f x

Tactic:
simpa using

Goal state after:
𝕜 : 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 g : E → F
x : E
hg : DifferentiableAt 𝕜 g x
h : DifferentiableAt 𝕜 (f + g) x
⊢ DifferentiableAt 𝕜 f x
Module: Mathlib.Analysis.Calculus.FDeriv.Add

Goal state before:
pp: 𝕜 : 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 g : E → F
s : Set E
hg : DifferentiableOn 𝕜 g s
h : DifferentiableOn 𝕜 (f + g) s
⊢ DifferentiableOn 𝕜 f s

Tactic:
simpa using

Goal state after:
𝕜 : 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 g : E → F
s : Set E
hg : DifferentiableOn 𝕜 g s
h : DifferentiableOn 𝕜 (f + g) s
⊢ DifferentiableOn 𝕜 f s
Module: Mathlib.Analysis.Calculus.FDeriv.Add

Goal state before:
pp: 𝕜 : 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 g : E → F
hg : Differentiable 𝕜 g
h : Differentiable 𝕜 (f + g)
⊢ Differentiable 𝕜 f

Tactic:
simpa using

Goal state after:
𝕜 : 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 g : E → F
hg : Differentiable 𝕜 g
h : Differentiable 𝕜 (f + g)
⊢ Differentiable 𝕜 f
Module: Mathlib.Analysis.Calculus.FDeriv.Add

Goal state before:
pp: 𝕜 : 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
f' : E →L[𝕜] F
L : Filter (E × E)
c : F
⊢ HasFDerivAtFilter (fun x ↦ f x - c) f' L ↔ HasFDerivAtFilter f f' L

Tactic:
simp only [sub_eq_add_neg, hasFDerivAtFilter_add_const_iff]

Goal state after:
Module: Mathlib.Analysis.Calculus.FDeriv.Add

Goal state before:
pp: 𝕜 : 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
f' : E →L[𝕜] F
x : E
s : Set E
a : E
⊢ HasFDerivWithinAt (fun x ↦ f (x + a)) f' s x ↔ HasFDerivWithinAt f f' (a +ᵥ s) (x + a)

Tactic:
simpa using

Goal state after:
𝕜 : 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
f' : E →L[𝕜] F
x : E
s : Set E
a : E
⊢ HasFDerivWithinAt (fun x ↦ f (x + a)) f' s x ↔ HasFDerivWithinAt f f' (a +ᵥ s) (x + a)
Module: Mathlib.Analysis.Calculus.FDeriv.Add

Goal state before:
pp: 𝕜 : 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
f' : E →L[𝕜] F
x a : E
⊢ HasFDerivAt (fun x ↦ f (a + x)) f' x ↔ HasFDerivAt f f' (a + x)

Tactic:
simpa using

Goal state after:
𝕜 : 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
f' : E →L[𝕜] F
x a : E
⊢ HasFDerivAt (fun x ↦ f (x + a)) f' x ↔ HasFDerivAt f f' (x + a)
Module: Mathlib.Analysis.Calculus.FDeriv.Add

Goal state before:
pp: 𝕜 : 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
x a : E
⊢ fderiv 𝕜 (fun x ↦ f (a + x)) x = fderiv 𝕜 f (a + x)

Tactic:
simpa using

Goal state after:
𝕜 : 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
x a : E
⊢ fderiv 𝕜 (fun x ↦ f (x + a)) x = fderiv 𝕜 f (x + a)
Module: Mathlib.Analysis.Calculus.FDeriv.Add

Goal state before:
pp: 𝕜 : 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
f' : E →L[𝕜] F
x : E
s : Set E
a : E
⊢ HasFDerivWithinAt (fun x ↦ f (x - a)) f' s x ↔ HasFDerivWithinAt f f' (-a +ᵥ s) (x - a)

Tactic:
simpa using

Goal state after:
𝕜 : 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
f' : E →L[𝕜] F
x : E
s : Set E
a : E
⊢ HasFDerivWithinAt (fun x ↦ f (x + -a)) f' s x ↔ HasFDerivWithinAt f f' (-a +ᵥ s) (x + -a)
Module: Mathlib.Analysis.Calculus.FDeriv.Equiv

Goal state before:
pp: 𝕜 : 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
iso : E ≃L[𝕜] F
f : F → G
s : Set F
x : E
H : DifferentiableWithinAt 𝕜 (f ∘ ⇑iso) (⇑iso ⁻¹' s) (iso.symm (iso x))
y : F
hy : y ∈ s
⊢ iso.symm y ∈ ⇑iso ⁻¹' s

Tactic:
simpa using

Goal state after:
𝕜 : 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
iso : E ≃L[𝕜] F
f : F → G
s : Set F
x : E
H : DifferentiableWithinAt 𝕜 (f ∘ ⇑iso) (⇑iso ⁻¹' s) (iso.symm (iso x))
y : F
hy : y ∈ s
⊢ y ∈ s
Module: Mathlib.Analysis.Calculus.FDeriv.Add

Goal state before:
pp: 𝕜 : 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
x : E
s : Set E
a : E
⊢ fderivWithin 𝕜 (fun x ↦ f (x - a)) s x = fderivWithin 𝕜 f (-a +ᵥ s) (x - a)

Tactic:
simpa using

Goal state after:
𝕜 : 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
x : E
s : Set E
a : E
⊢ fderivWithin 𝕜 (fun x ↦ f (x + -a)) s x = fderivWithin 𝕜 f (-a +ᵥ s) (x + -a)
Module: Mathlib.Analysis.Calculus.FDeriv.Equiv

Goal state before:
pp: 𝕜 : 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
iso : E ≃L[𝕜] F
f : F → G
s : Set F
H : DifferentiableOn 𝕜 (f ∘ ⇑iso) (⇑iso ⁻¹' s)
y : F
hy : y ∈ s
⊢ iso.symm y ∈ ⇑iso ⁻¹' s

Tactic:
simpa using

Goal state after:
𝕜 : 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
iso : E ≃L[𝕜] F
f : F → G
s : Set F
H : DifferentiableOn 𝕜 (f ∘ ⇑iso) (⇑iso ⁻¹' s)
y : F
hy : y ∈ s
⊢ y ∈ s
Module: Mathlib.Analysis.Calculus.FDeriv.Equiv

Goal state before:
pp: 𝕜 : 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
iso : E ≃L[𝕜] F
f : F → G
s : Set F
x : E
f' : F →L[𝕜] G
H : HasFDerivWithinAt (f ∘ ⇑iso) (f' ∘SL ↑iso) (⇑iso ⁻¹' s) (iso.symm (iso x))
A : f = (f ∘ ⇑iso) ∘ ⇑iso.symm
B : f' = (f' ∘SL ↑iso) ∘SL ↑iso.symm
y : F
hy : y ∈ s
⊢ iso.symm y ∈ ⇑iso ⁻¹' s

Tactic:
simpa using

Goal state after:
𝕜 : 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
iso : E ≃L[𝕜] F
f : F → G
s : Set F
x : E
f' : F →L[𝕜] G
H : HasFDerivWithinAt (f ∘ ⇑iso) (f' ∘SL ↑iso) (⇑iso ⁻¹' s) (iso.symm (iso x))
A : f = (f ∘ ⇑iso) ∘ ⇑iso.symm
B : f' = (f' ∘SL ↑iso) ∘SL ↑iso.symm
y : F
hy : y ∈ s
⊢ y ∈ s
Module: Mathlib.Topology.Algebra.Module.Alternating.Basic

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
ι : Type u_4
inst✝⁹ : Semiring R
inst✝⁸ : AddCommMonoid M
inst✝⁷ : Module R M
inst✝⁶ : TopologicalSpace M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
inst✝³ : TopologicalSpace N
inst✝² : IsTopologicalAddGroup N
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
f✝ f : ContinuousMultilinearMap R (fun x ↦ M) N
v : ι → M
i j : ι
hv : v i = v j
hne : i ≠ j
⊢ (∑ σ, Equiv.Perm.sign σ • domDomCongr σ f).toFun v = 0

Tactic:
simpa using

Goal state after:
R : Type u_1
M : Type u_2
N : Type u_3
ι : Type u_4
inst✝⁹ : Semiring R
inst✝⁸ : AddCommMonoid M
inst✝⁷ : Module R M
inst✝⁶ : TopologicalSpace M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
inst✝³ : TopologicalSpace N
inst✝² : IsTopologicalAddGroup N
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
f✝ f : ContinuousMultilinearMap R (fun x ↦ M) N
v : ι → M
i j : ι
hv : v i = v j
hne : i ≠ j
⊢ (∑ x, Equiv.Perm.sign x • f fun i ↦ v (x i)) = 0
Module: Mathlib.Analysis.Calculus.FDeriv.Equiv

Goal state before:
pp: 𝕜 : 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
f' : E →L[𝕜] F
x✝ : E
s : Set E
h : HasFDerivWithinAt f f' s x✝
C : ℝ≥0
hC : AntilipschitzWith C ⇑f'
x : E
⊢ ‖x‖ ≤ ↑C * ‖f' x‖

Tactic:
simpa using

Goal state after:
𝕜 : 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
f' : E →L[𝕜] F
x✝ : E
s : Set E
h : HasFDerivWithinAt f f' s x✝
C : ℝ≥0
hC : AntilipschitzWith C ⇑f'
x : E
⊢ ‖x‖ ≤ ↑C * ‖f' x‖
Module: Mathlib.Analysis.Calculus.FDeriv.Equiv

Goal state before:
pp: 𝕜 : 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
f' : E →L[𝕜] F
x : E
s : Set 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 𝓝[s] x, x_1 ∈ {x}ᶜ → f x_1 ∈ {f x}ᶜ

Tactic:
simpa using

Goal state after:
𝕜 : 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
f' : E →L[𝕜] F
x : E
s : Set 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 𝓝[s] x, f x_1 = f x → x_1 = x
Module: Mathlib.Analysis.Calculus.FDeriv.Equiv

Goal state before:
pp: 𝕜 : 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
f' : E →L[𝕜] F
x : E
h : HasFDerivAt f f' x
hf' : ∃ C, AntilipschitzWith C ⇑f'
⊢ Tendsto f (𝓝[≠] x) (𝓝[≠] f x)

Tactic:
simpa using

Goal state after:
𝕜 : 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
f' : E →L[𝕜] F
x : E
h : HasFDerivAt f f' x
hf' : ∃ C, AntilipschitzWith C ⇑f'
⊢ Tendsto f (𝓝[univ \ {x}] x) (𝓝[univ \ {f x}] f x)
Module: Mathlib.Analysis.Calculus.FDeriv.Equiv

Goal state before:
pp: 𝕜 : 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
f' : E →L[𝕜] F
x : E
c : F
h : HasFDerivAt f f' x
hf' : ∃ C, AntilipschitzWith C ⇑f'
⊢ ∀ᶠ (z : E) in 𝓝[≠] x, f z ≠ c

Tactic:
simpa using

Goal state after:
𝕜 : 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
f' : E →L[𝕜] F
x : E
c : F
h : HasFDerivAt f f' x
hf' : ∃ C, AntilipschitzWith C ⇑f'
⊢ ∀ᶠ (z : E) in 𝓝[univ \ {x}] x, f z ≠ c
Module: Mathlib.Analysis.Calculus.FDeriv.Equiv

Goal state before:
pp: 𝕜 : 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
f' : E →L[𝕜] F
x : E
h : HasFDerivAt f f' x
hf' : ∃ C, AntilipschitzWith C ⇑f'
t : Set F
ht : ¬AccPt (f x) (𝓟 t)
⊢ ∀ᶠ (z : E) in 𝓝[≠] x, f z ∉ t

Tactic:
simpa using

Goal state after:
𝕜 : 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
f' : E →L[𝕜] F
x : E
h : HasFDerivAt f f' x
hf' : ∃ C, AntilipschitzWith C ⇑f'
t : Set F
ht : ¬AccPt (f x) (𝓟 t)
⊢ ∀ᶠ (z : E) in 𝓝[univ \ {x}] x, f z ∉ t
Module: Mathlib.Analysis.Calculus.FDeriv.Equiv

Goal state before:
pp: case hd₀
𝕜 : 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
y : E
hy : y ∈ tangentConeAt 𝕜 s x
ι : Type (max u_1 u_2)
l : Filter ι
hl : l.NeBot
c : ι → 𝕜
d : ι → E
hd₀ : Tendsto d l (𝓝 0)
hds : ∀ᶠ (n : ι) in l, x + d n ∈ s
hcd : Tendsto (fun n ↦ c n • d n) l (𝓝 y)
⊢ Tendsto (fun n ↦ x + d n) l (𝓝 x)

Tactic:
simpa using

Goal state after:
case hd₀
𝕜 : 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
y : E
hy : y ∈ tangentConeAt 𝕜 s x
ι : Type (max u_1 u_2)
l : Filter ι
hl : l.NeBot
c : ι → 𝕜
d : ι → E
hd₀ : Tendsto d l (𝓝 0)
hds : ∀ᶠ (n : ι) in l, x + d n ∈ s
hcd : Tendsto (fun n ↦ c n • d n) l (𝓝 y)
⊢ Tendsto (fun n ↦ x + d n) l (𝓝 x)
Module: Mathlib.Analysis.Calculus.FDeriv.Equiv

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
s : Set E
x : E
G : Type u_4
inst✝³ : GroupWithZero G
inst✝² : DistribMulAction G E
inst✝¹ : ContinuousConstSMul G E
inst✝ : SMulCommClass G 𝕜 E
c : G
hc : c ≠ 0
h : UniqueDiffWithinAt 𝕜 (c • s) (c • x)
⊢ UniqueDiffWithinAt 𝕜 s x

Tactic:
simpa using

Goal state after:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
s : Set E
x : E
G : Type u_4
inst✝³ : GroupWithZero G
inst✝² : DistribMulAction G E
inst✝¹ : ContinuousConstSMul G E
inst✝ : SMulCommClass G 𝕜 E
c : G
hc : c ≠ 0
h : UniqueDiffWithinAt 𝕜 (c • s) (c • x)
⊢ UniqueDiffWithinAt 𝕜 s x
Module: Mathlib.Analysis.Calculus.FDeriv.Equiv

Goal state before:
pp: 𝕜 : 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
c : 𝕜
⊢ HasFDerivWithinAt (fun x ↦ f (c • x)) (c • f') s x ↔ HasFDerivWithinAt f f' (c • s) (c • x)

Tactic:
by
  rcases eq_or_ne c 0 with rfl | hc
  · simp [hasFDerivWithinAt_const, HasFDerivWithinAt.of_subsingleton (subsingleton_zero_smul_set _)]
  · lift c to 𝕜ˣ using IsUnit.mk0 c hc
    have A : f'.comp ((ContinuousLinearEquiv.smulLeft c : E ≃L[𝕜] E) : E →L[𝕜] E) = c • f' := by
      ext; simp
    rw [← Units.smul_def c x, ← ContinuousLinearEquiv.smulLeft_apply_apply (R₁ := 𝕜),
      ← ContinuousLinearEquiv.comp_right_hasFDerivWithinAt_iff, A]
    simp [Function.comp_def, ← Units.smul_def, ← preimage_smul_inv, preimage_preimage]

Goal state after: