awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Calculus.FDeriv.Equiv
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
x : E
iso : E ≃ₗᵢ[𝕜] F
⊢ DifferentiableAt.{u_1, u_2, u_3} 𝕜 (F := F) (⇑iso : (a : E) → F) x

Tactic:
iso.hasFDerivAt.differentiableAt

Premises used: LinearIsometryEquiv.hasFDerivAt, HasFDerivAt.differentiableAt
-- Module: Mathlib.Analysis.Calculus.FDeriv.Equiv
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
x : E
s : Set E
iso : E ≃ₗᵢ[𝕜] F
⊢ DifferentiableWithinAt.{u_1, u_2, u_3} 𝕜 (F := F) (⇑iso : (a : E) → F) s x

Tactic:
iso.differentiableAt.differentiableWithinAt

Premises used: DifferentiableAt.differentiableWithinAt, LinearIsometryEquiv.differentiableAt
-- Module: Mathlib.Analysis.Calculus.FDeriv.Equiv
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
x : E
iso : E ≃ₗᵢ[𝕜] F
⊢ fderiv 𝕜 (⇑iso : (a : E) → F) x = (↑(↑iso : E ≃L[𝕜] F) : E →L[𝕜] F)

Tactic:
iso.hasFDerivAt.fderiv

Premises used: LinearIsometryEquiv.hasFDerivAt, HasFDerivAt.fderiv
-- Module: Mathlib.Analysis.Calculus.FDeriv.Equiv
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
x : E
s : Set E
iso : E ≃ₗᵢ[𝕜] F
hxs : UniqueDiffWithinAt 𝕜 s x
⊢ fderivWithin 𝕜 (⇑iso : (a : E) → F) s x = (↑(↑iso : E ≃L[𝕜] F) : E →L[𝕜] F)

Tactic:
(iso : E ≃L[𝕜] F).fderivWithin hxs

Premises used: ContinuousLinearEquiv.fderivWithin, LinearIsometryEquiv.toContinuousLinearEquiv
-- Module: Mathlib.Analysis.Calculus.FDeriv.Equiv
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
iso : E ≃ₗᵢ[𝕜] F
⊢ Differentiable.{u_1, u_2, u_3} 𝕜 (E := E) (F := F) (⇑iso : (a : E) → F)

Tactic:
fun _ => iso.differentiableAt

Premises used: Differentiable, LinearIsometryEquiv.differentiableAt
-- Module: Mathlib.Analysis.Calculus.FDeriv.Equiv
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
s : Set E
iso : E ≃ₗᵢ[𝕜] F
⊢ DifferentiableOn.{u_1, u_2, u_3} 𝕜 (F := F) (⇑iso : (a : E) → F) s

Tactic:
iso.differentiable.differentiableOn

Premises used: Differentiable.differentiableOn, LinearIsometryEquiv.differentiable
-- Module: Mathlib.Analysis.Calculus.FDeriv.Equiv
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
iso : E ≃ₗᵢ[𝕜] F
f : G → E
s : Set G
x : G
⊢ DifferentiableWithinAt.{u_1, u_4, u_3} 𝕜 (F := F) ((⇑iso : (a : E) → F) ∘ f) s x ↔ DifferentiableWithinAt 𝕜 f s x

Tactic:
(iso : E ≃L[𝕜] F).comp_differentiableWithinAt_iff

Premises used: LinearIsometryEquiv.toContinuousLinearEquiv, ContinuousLinearEquiv.comp_differentiableWithinAt_iff
-- Module: Mathlib.Analysis.Calculus.FDeriv.Equiv
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
iso : E ≃ₗᵢ[𝕜] F
f : G → E
x : G
⊢ DifferentiableAt.{u_1, u_4, u_3} 𝕜 (F := F) ((⇑iso : (a : E) → F) ∘ f) x ↔ DifferentiableAt 𝕜 f x

Tactic:
(iso : E ≃L[𝕜] F).comp_differentiableAt_iff

Premises used: ContinuousLinearEquiv.comp_differentiableAt_iff, LinearIsometryEquiv.toContinuousLinearEquiv
-- Module: Mathlib.Analysis.Calculus.FDeriv.Equiv
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
iso : E ≃ₗᵢ[𝕜] F
f : G → E
s : Set G
⊢ DifferentiableOn.{u_1, u_4, u_3} 𝕜 (F := F) ((⇑iso : (a : E) → F) ∘ f) s ↔ DifferentiableOn 𝕜 f s

Tactic:
(iso : E ≃L[𝕜] F).comp_differentiableOn_iff

Premises used: ContinuousLinearEquiv.comp_differentiableOn_iff, LinearIsometryEquiv.toContinuousLinearEquiv
-- Module: Mathlib.Analysis.Calculus.FDeriv.Equiv
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
iso : E ≃ₗᵢ[𝕜] F
f : G → E
⊢ Differentiable.{u_1, u_4, u_3} 𝕜 (F := F) ((⇑iso : (a : E) → F) ∘ f) ↔ Differentiable 𝕜 f

Tactic:
(iso : E ≃L[𝕜] F).comp_differentiable_iff

Premises used: ContinuousLinearEquiv.comp_differentiable_iff, LinearIsometryEquiv.toContinuousLinearEquiv
-- Module: Mathlib.Analysis.Calculus.FDeriv.Equiv
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
iso : E ≃ₗᵢ[𝕜] F
f : G → E
s : Set G
x : G
f' : G →L[𝕜] E
⊢ HasFDerivWithinAt ((⇑iso : (a : E) → F) ∘ f) ((↑(↑iso : E ≃L[𝕜] F) : E →L[𝕜] F) ∘SL f') s x ↔
    HasFDerivWithinAt f f' s x

Tactic:
(iso : E ≃L[𝕜] F).comp_hasFDerivWithinAt_iff

Premises used: ContinuousLinearEquiv.comp_hasFDerivWithinAt_iff, LinearIsometryEquiv.toContinuousLinearEquiv
-- Module: Mathlib.Analysis.Calculus.FDeriv.Equiv
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
iso : E ≃ₗᵢ[𝕜] F
f : G → E
x : G
f' : G →L[𝕜] E
⊢ HasStrictFDerivAt ((⇑iso : (a : E) → F) ∘ f) ((↑(↑iso : E ≃L[𝕜] F) : E →L[𝕜] F) ∘SL f') x ↔ HasStrictFDerivAt f f' x

Tactic:
(iso : E ≃L[𝕜] F).comp_hasStrictFDerivAt_iff

Premises used: LinearIsometryEquiv.toContinuousLinearEquiv, ContinuousLinearEquiv.comp_hasStrictFDerivAt_iff
-- Module: Mathlib.Analysis.Calculus.FDeriv.Equiv
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
iso : E ≃ₗᵢ[𝕜] F
f : G → E
x : G
f' : G →L[𝕜] E
⊢ HasFDerivAt ((⇑iso : (a : E) → F) ∘ f) ((↑(↑iso : E ≃L[𝕜] F) : E →L[𝕜] F) ∘SL f') x ↔ HasFDerivAt f f' x

Tactic:
(iso : E ≃L[𝕜] F).comp_hasFDerivAt_iff

Premises used: ContinuousLinearEquiv.comp_hasFDerivAt_iff, LinearIsometryEquiv.toContinuousLinearEquiv
-- Module: Mathlib.Analysis.Calculus.FDeriv.Equiv
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
iso : E ≃ₗᵢ[𝕜] F
f : G → E
s : Set G
x : G
f' : G →L[𝕜] F
⊢ HasFDerivWithinAt ((⇑iso : (a : E) → F) ∘ f) f' s x ↔
    HasFDerivWithinAt f ((↑(↑iso.symm : F ≃L[𝕜] E) : F →L[𝕜] E) ∘SL f') s x

Tactic:
(iso : E ≃L[𝕜] F).comp_hasFDerivWithinAt_iff'

Premises used: ContinuousLinearEquiv.symm, LinearEquiv.symm, ContinuousLinearEquiv.comp_hasFDerivWithinAt_iff', LinearIsometryEquiv.toContinuousLinearEquiv
-- Module: Mathlib.Analysis.Calculus.FDeriv.Equiv
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
iso : E ≃ₗᵢ[𝕜] F
f : G → E
x : G
f' : G →L[𝕜] F
⊢ HasFDerivAt ((⇑iso : (a : E) → F) ∘ f) f' x ↔ HasFDerivAt f ((↑(↑iso.symm : F ≃L[𝕜] E) : F →L[𝕜] E) ∘SL f') x

Tactic:
(iso : E ≃L[𝕜] F).comp_hasFDerivAt_iff'

Premises used: ContinuousLinearEquiv.symm, LinearEquiv.symm, ContinuousLinearEquiv.comp_hasFDerivAt_iff', LinearIsometryEquiv.toContinuousLinearEquiv
-- Module: Mathlib.Analysis.Calculus.FDeriv.Equiv
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
iso : E ≃ₗᵢ[𝕜] F
f : G → E
s : Set G
x : G
hxs : UniqueDiffWithinAt 𝕜 s x
⊢ Eq (α := G →L[𝕜] F) (fderivWithin 𝕜 ((⇑iso : (a : E) → F) ∘ f) s x)
    ((↑(↑iso : E ≃L[𝕜] F) : E →L[𝕜] F) ∘SL fderivWithin 𝕜 f s x)

Tactic:
(iso : E ≃L[𝕜] F).comp_fderivWithin hxs

Premises used: LinearIsometryEquiv.toContinuousLinearEquiv, ContinuousLinearEquiv.comp_fderivWithin
-- Module: Mathlib.Analysis.Calculus.FDeriv.Equiv
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
iso : E ≃ₗᵢ[𝕜] F
f : G → E
x : G
⊢ Eq (α := G →L[𝕜] F) (fderiv 𝕜 ((⇑iso : (a : E) → F) ∘ f) x) ((↑(↑iso : E ≃L[𝕜] F) : E →L[𝕜] F) ∘SL fderiv 𝕜 f x)

Tactic:
(iso : E ≃L[𝕜] F).comp_fderiv

Premises used: ContinuousLinearEquiv.comp_fderiv, LinearIsometryEquiv.toContinuousLinearEquiv
-- Module: Mathlib.Analysis.Calculus.FDeriv.Equiv
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
iso : E ≃ₗᵢ[𝕜] F
f : G → E
h :
  ∀ (x : G),
    Eq (α := G →L[𝕜] F) (fderiv 𝕜 ((⇑iso : (a : E) → F) ∘ f) x) ((↑(↑iso : E ≃L[𝕜] F) : E →L[𝕜] F) ∘SL fderiv 𝕜 f x)
⊢ Eq (α := (x : G) → G →L[𝕜] F) (fderiv 𝕜 ((⇑iso : (a : E) → F) ∘ f)) fun (x : G) ↦
    (↑(↑iso : E ≃L[𝕜] F) : E →L[𝕜] F) ∘SL fderiv 𝕜 f x

Tactic:
ext x : 1
-- Module: Mathlib.Analysis.Calculus.FDeriv.Equiv
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
iso : E ≃ₗᵢ[𝕜] F
f : G → E
x : G
⊢ Eq (α := G →L[𝕜] F) (fderiv 𝕜 ((⇑iso : (a : E) → F) ∘ f) x) ((↑(↑iso : E ≃L[𝕜] F) : E →L[𝕜] F) ∘SL fderiv 𝕜 f x)

Tactic:
LinearIsometryEquiv.comp_fderiv iso

Premises used: LinearIsometryEquiv.comp_fderiv
-- Module: Mathlib.Analysis.Calculus.FDeriv.Equiv
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
iso : E ≃ₗᵢ[𝕜] F
f : G → E
x : G
⊢ Eq (α := G →L[𝕜] F) (fderiv 𝕜 ((⇑iso : (a : E) → F) ∘ f) x) ((↑(↑iso : E ≃L[𝕜] F) : E →L[𝕜] F) ∘SL fderiv 𝕜 f x)

Tactic:
exact LinearIsometryEquiv.comp_fderiv iso

Premises used: LinearIsometryEquiv.comp_fderiv
-- Module: Mathlib.Analysis.Calculus.FDeriv.Equiv
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
f' : E →L[𝕜] F
x : E
s : Set E
h : HasFDerivWithinAt f f' s x
hf' : ∃ (C : ℝ≥0), AntilipschitzWith.{u_2, u_3} (α := E) (β := F) C (⇑f' : (a : E) → F)
obtain :
  ∀ (C : ℝ≥0) (hC : AntilipschitzWith.{u_2, u_3} (α := E) (β := F) C (⇑f' : (a : E) → F)),
    ∃ (C : ℝ), ∀ (z : E), ‖z‖ ≤ C * norm.{u_3} (E := F) ((f' : (a : E) → F) z : F)
⊢ ∃ (C : ℝ), ∀ (z : E), ‖z‖ ≤ C * norm.{u_3} (E := F) ((f' : (a : E) → F) z : F)

Tactic:
obtain ⟨C, hC⟩ := hf'
-- Module: Mathlib.Analysis.Calculus.FDeriv.Equiv
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
f' : E →L[𝕜] F
x_1 : E
s : Set E
h : HasFDerivWithinAt f f' s x_1
C : ℝ≥0
hC : AntilipschitzWith.{u_2, u_3} (α := E) (β := F) C (⇑f' : (a : E) → F)
x : E
⊢ ‖x‖ ≤ (↑C : ℝ) * norm.{u_3} (E := F) ((f' : (a : E) → F) x : F)

Tactic:
simpa using hC.le_mul_dist 0 x

Premises used: AntilipschitzWith.le_mul_dist, OfNat.ofNat
-- Module: Mathlib.Analysis.Calculus.FDeriv.Equiv
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
f' : E →L[𝕜] F
x : E
s : Set E
h : HasFDerivWithinAt f f' s x
C : ℝ≥0
hC : AntilipschitzWith.{u_2, u_3} (α := E) (β := F) C (⇑f' : (a : E) → F)
⊢ ∃ (C : ℝ), ∀ (z : E), ‖z‖ ≤ C * norm.{u_3} (E := F) ((f' : (a : E) → F) z : F)

Tactic:
exact ⟨C, fun x ↦ by simpa using hC.le_mul_dist 0 x⟩
-- Module: Mathlib.Analysis.Calculus.FDeriv.Equiv
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
f' : E →L[𝕜] F
x : E
s : Set E
h : HasFDerivWithinAt f f' s x
hf' : ∃ (C : ℝ≥0), AntilipschitzWith.{u_2, u_3} (α := E) (β := F) C (⇑f' : (a : E) → F)
⊢ ∃ (C : ℝ), ∀ (z : E), ‖z‖ ≤ C * norm.{u_3} (E := F) ((f' : (a : E) → F) z : F)

Tactic:
replace hf' : ∃ C, ∀ z, ‖z‖ ≤ C * ‖f' z‖ := by
    obtain ⟨C, hC⟩ := hf'
    exact ⟨C, fun x ↦ by simpa using hC.le_mul_dist 0 x⟩
-- Module: Mathlib.Analysis.Calculus.FDeriv.Equiv
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : 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 * norm.{u_3} (E := F) ((f' : (a : E) → F) z : F)
⊢ IsBigO.{u_2, u_2, u_3} (E := E) (F := F) (𝓝[s] x) (fun (z : E) ↦ z - x) fun (z : E) ↦ (f' : (a : E) → F) (z - x)

Tactic:
have A : (fun z ↦ z - x) =O[𝓝[s] x] fun z ↦ f' (z - x) :=
    isBigO_iff.mpr <| hf'.imp fun C hC ↦ Eventually.of_forall fun z ↦ hC (z - x)
-- Module: Mathlib.Analysis.Calculus.FDeriv.Equiv
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : 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 * norm.{u_3} (E := F) ((f' : (a : E) → F) z : F)
A : IsBigO.{u_2, u_2, u_3} (E := E) (F := F) (𝓝[s] x) (fun (z : E) ↦ z - x) fun (z : E) ↦ (f' : (a : E) → F) (z - x)
⊢ IsEquivalent.{u_2, u_3} (E' := F) (𝓝[s] x) (fun (z : E) ↦ f z - f x) fun (z : E) ↦ (f' : (a : E) → F) (z - x)

Tactic:
have : (fun z ↦ f z - f x) ~[𝓝[s] x] fun z ↦ f' (z - x) := h.isLittleO.trans_isBigO A
-- Module: Mathlib.Analysis.Calculus.FDeriv.Equiv
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : 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 * norm.{u_3} (E := F) ((f' : (a : E) → F) z : F)
A : IsBigO.{u_2, u_2, u_3} (E := E) (F := F) (𝓝[s] x) (fun (z : E) ↦ z - x) fun (z : E) ↦ (f' : (a : E) → F) (z - x)
this : IsEquivalent.{u_2, u_3} (E' := F) (𝓝[s] x) (fun (z : E) ↦ f z - f x) fun (z : E) ↦ (f' : (a : E) → F) (z - x)
⊢ ∀ᶠ (x_1 : E) in 𝓝[s] x, Membership.mem (γ := Set E) {x}ᶜ x_1 → Membership.mem (γ := Set F) {f x}ᶜ (f x_1)

Tactic:
simpa [sub_eq_zero, not_imp_not] using (A.trans this.isBigO_symm).eq_zero_imp

Premises used: sub_eq_zero, Asymptotics.IsEquivalent.isBigO_symm, Asymptotics.IsBigO.trans, Asymptotics.IsBigO.eq_zero_imp, not_imp_not
-- Module: Mathlib.Analysis.Calculus.FDeriv.Equiv
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : 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 * norm.{u_3} (E := F) ((f' : (a : E) → F) z : F)
A : IsBigO.{u_2, u_2, u_3} (E := E) (F := F) (𝓝[s] x) (fun (z : E) ↦ z - x) fun (z : E) ↦ (f' : (a : E) → F) (z - x)
this : IsEquivalent.{u_2, u_3} (E' := F) (𝓝[s] x) (fun (z : E) ↦ f z - f x) fun (z : E) ↦ (f' : (a : E) → F) (z - x)
⊢ ∀ᶠ (x_1 : E) in 𝓝[s] x, Membership.mem (γ := Set E) {x}ᶜ x_1 → Membership.mem (γ := Set F) {f x}ᶜ (f x_1)

Tactic:
have : ∀ᶠ (x_1 : E) in 𝓝[s] x, x_1 ∈ ({x}ᶜ : Set E) → f x_1 ∈ ({f x}ᶜ : Set F) := by
    simpa [sub_eq_zero, not_imp_not] using (A.trans this.isBigO_symm).eq_zero_imp
-- Module: Mathlib.Analysis.Calculus.FDeriv.Equiv
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : 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 * norm.{u_3} (E := F) ((f' : (a : E) → F) z : F)
A : IsBigO.{u_2, u_2, u_3} (E := E) (F := F) (𝓝[s] x) (fun (z : E) ↦ z - x) fun (z : E) ↦ (f' : (a : E) → F) (z - x)
this_1 : IsEquivalent.{u_2, u_3} (E' := F) (𝓝[s] x) (fun (z : E) ↦ f z - f x) fun (z : E) ↦ (f' : (a : E) → F) (z - x)
this : ∀ᶠ (x_1 : E) in 𝓝[s] x, Membership.mem (γ := Set E) {x}ᶜ x_1 → Membership.mem (γ := Set F) {f x}ᶜ (f x_1)
apply : map f (𝓝[s \ {x}] x) ≤ 𝓟 {f x}ᶜ
⊢ Tendsto f (𝓝[s \ {x}] x) (𝓝[≠] f x)

Tactic:
apply le_inf ((map_mono (nhdsWithin_mono x diff_subset)).trans h.continuousWithinAt)

Premises used: Set.diff_subset, Filter.map_mono, le_inf, HasFDerivWithinAt.continuousWithinAt, LE.le.trans, nhdsWithin_mono
-- Module: Mathlib.Analysis.Calculus.FDeriv.Equiv
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : 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 * norm.{u_3} (E := F) ((f' : (a : E) → F) z : F)
A : IsBigO.{u_2, u_2, u_3} (E := E) (F := F) (𝓝[s] x) (fun (z : E) ↦ z - x) fun (z : E) ↦ (f' : (a : E) → F) (z - x)
this_1 : IsEquivalent.{u_2, u_3} (E' := F) (𝓝[s] x) (fun (z : E) ↦ f z - f x) fun (z : E) ↦ (f' : (a : E) → F) (z - x)
this : ∀ᶠ (x_1 : E) in 𝓝[s] x, Membership.mem (γ := Set E) {x}ᶜ x_1 → Membership.mem (γ := Set F) {f x}ᶜ (f x_1)
rwa : {f x}ᶜ ∈ map f (𝓝[s \ {x}] x)
rwa₁ : ∀ᶠ (x_1 : F) in map f (𝓝[s \ {x}] x), Membership.mem (γ := Set F) {f x}ᶜ x_1
rwa₂ : ∀ᶠ (a : E) in 𝓝[s \ {x}] x, Membership.mem (γ := Set F) {f x}ᶜ (f a)
rwa₃ : ∀ᶠ (a : E) in 𝓝[s ∩ {x}ᶜ] x, Membership.mem (γ := Set F) {f x}ᶜ (f a)
rwa₄ : ∀ᶠ (a : E) in 𝓝[s] x ⊓ 𝓟 {x}ᶜ, Membership.mem (γ := Set F) {f x}ᶜ (f a)
rwa₅ rwa₆ rwa₇ rwa₈ :
  ∀ᶠ (x_1 : E) in 𝓝[s] x, Membership.mem (γ := Set E) {x}ᶜ x_1 → Membership.mem (γ := Set F) {f x}ᶜ (f x_1)
⊢ map f (𝓝[s \ {x}] x) ≤ 𝓟 {f x}ᶜ

Tactic:
rwa [le_principal_iff, ← eventually_mem_set, eventually_map, diff_eq, nhdsWithin_inter',
    eventually_inf_principal]

Premises used: Filter.eventually_inf_principal, Filter.le_principal_iff, Set.diff_eq, Filter.eventually_map, nhdsWithin_inter', Filter.eventually_mem_set
-- Module: Mathlib.Analysis.Calculus.FDeriv.Equiv
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
f' : E →L[𝕜] F
x : E
s : Set E
c : F
h : HasFDerivWithinAt f f' s x
hf' : ∃ (C : ℝ≥0), AntilipschitzWith.{u_2, u_3} (α := E) (β := F) C (⇑f' : (a : E) → F)
rw : ∀ᶠ (b : F) in map f (𝓝[s \ {x}] x), b ≠ c
⊢ ∀ᶠ (z : E) in 𝓝[s \ {x}] x, f z ≠ c

Tactic:
rw [← eventually_map (m := f) (P := fun z ↦ z ≠ c)]

Premises used: Filter.eventually_map
-- Module: Mathlib.Analysis.Calculus.FDeriv.Equiv
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
f' : E →L[𝕜] F
x : E
s : Set E
c : F
h : HasFDerivWithinAt f f' s x
hf' : ∃ (C : ℝ≥0), AntilipschitzWith.{u_2, u_3} (α := E) (β := F) C (⇑f' : (a : E) → F)
apply : ∀ᶠ (x : F) in 𝓝[≠] f x, x ≠ c
⊢ ∀ᶠ (b : F) in map f (𝓝[s \ {x}] x), b ≠ c

Tactic:
apply Eventually.filter_mono (h.tendsto_nhdsWithin_nhdsNE hf')

Premises used: Filter.Eventually.filter_mono, HasFDerivWithinAt.tendsto_nhdsWithin_nhdsNE
-- Module: Mathlib.Analysis.Calculus.FDeriv.Equiv
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
f' : E →L[𝕜] F
x : E
s : Set E
c : F
h : HasFDerivWithinAt f f' s x
hf' : ∃ (C : ℝ≥0), AntilipschitzWith.{u_2, u_3} (α := E) (β := F) C (⇑f' : (a : E) → F)
inl : ∀ᶠ (x_1 : F) in 𝓝[≠] f x, x_1 ≠ f x
inr : ∀ (hc : f x ≠ c), ∀ᶠ (x : F) in 𝓝[≠] f x, x ≠ c
⊢ ∀ᶠ (x : F) in 𝓝[≠] f x, x ≠ c

Tactic:
rcases eq_or_ne (f x) c with rfl | hc

Premises used: eq_or_ne, rfl
-- Module: Mathlib.Analysis.Calculus.FDeriv.Equiv
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
f' : E →L[𝕜] F
x : E
s : Set E
h : HasFDerivWithinAt f f' s x
hf' : ∃ (C : ℝ≥0), AntilipschitzWith.{u_2, u_3} (α := E) (β := F) C (⇑f' : (a : E) → F)
⊢ ∀ᶠ (x_1 : F) in 𝓝[≠] f x, x_1 ≠ f x

Tactic:
eventually_mem_nhdsWithin

Premises used: eventually_mem_nhdsWithin, Set.Mem, setOf, Set.singleton, Not
-- Module: Mathlib.Analysis.Calculus.FDeriv.Equiv
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
f' : E →L[𝕜] F
x : E
s : Set E
h : HasFDerivWithinAt f f' s x
hf' : ∃ (C : ℝ≥0), AntilipschitzWith.{u_2, u_3} (α := E) (β := F) C (⇑f' : (a : E) → F)
⊢ ∀ᶠ (x_1 : F) in 𝓝[≠] f x, x_1 ≠ f x

Tactic:
exact eventually_mem_nhdsWithin

Premises used: eventually_mem_nhdsWithin
-- Module: Mathlib.Analysis.Calculus.FDeriv.Equiv
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
f' : E →L[𝕜] F
x : E
s : Set E
c : F
h : HasFDerivWithinAt f f' s x
hf' : ∃ (C : ℝ≥0), AntilipschitzWith.{u_2, u_3} (α := E) (β := F) C (⇑f' : (a : E) → F)
hc : f x ≠ c
⊢ ∀ᶠ (x : F) in 𝓝[≠] f x, x ≠ c

Tactic:
eventually_ne_nhdsWithin hc

Premises used: eventually_ne_nhdsWithin
-- Module: Mathlib.Analysis.Calculus.FDeriv.Equiv
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
f' : E →L[𝕜] F
x : E
s : Set E
c : F
h : HasFDerivWithinAt f f' s x
hf' : ∃ (C : ℝ≥0), AntilipschitzWith.{u_2, u_3} (α := E) (β := F) C (⇑f' : (a : E) → F)
hc : f x ≠ c
⊢ ∀ᶠ (x : F) in 𝓝[≠] f x, x ≠ c

Tactic:
exact eventually_ne_nhdsWithin hc

Premises used: eventually_ne_nhdsWithin
-- Module: Mathlib.Analysis.Calculus.FDeriv.Equiv
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
f' : E →L[𝕜] F
x : E
s : Set E
h : HasFDerivWithinAt f f' s x
hf' : ∃ (C : ℝ≥0), AntilipschitzWith.{u_2, u_3} (α := E) (β := F) C (⇑f' : (a : E) → F)
t : Set F
ht : ¬AccPt (f x) (𝓟 t)
⊢ ∀ᶠ (x : F) in 𝓝[≠] f x, x ∉ t

Tactic:
rw [accPt_iff_frequently_nhdsNE, not_frequently] at ht

Premises used: accPt_iff_frequently_nhdsNE, Filter.not_frequently