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

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : TopologicalSpace E
F : Type u_3
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 F
inst✝ : TopologicalSpace F
f : E → F
x : E
h : f =ᶠ[𝓝 x] 0
⊢ HasStrictFDerivAt f 0 x

Tactic:
]

Goal state after:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : TopologicalSpace E
F : Type u_3
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 F
inst✝ : TopologicalSpace F
f : E → F
x : E
h : f =ᶠ[𝓝 x] 0
⊢ HasStrictFDerivAt f 0 x
Module: Mathlib.Analysis.Calculus.FDeriv.Const

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : TopologicalSpace E
F : Type u_3
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 F
inst✝ : TopologicalSpace F
f : E → F
x : E
h : f =ᶠ[𝓝 x] 0
⊢ fderiv 𝕜 f x = 0

Tactic:
]

Goal state after:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : TopologicalSpace E
F : Type u_3
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 F
inst✝ : TopologicalSpace F
f : E → F
x : E
h : f =ᶠ[𝓝 x] 0
⊢ fderiv 𝕜 f x = 0
Module: Mathlib.Analysis.Calculus.FDeriv.Const

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : TopologicalSpace E
F : Type u_3
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 F
inst✝ : TopologicalSpace F
f : E → F
x : E
⊢ x ∉ tsupport f → fderiv 𝕜 f x = 0

Tactic:
]

Goal state after:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : TopologicalSpace E
F : Type u_3
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 F
inst✝ : TopologicalSpace F
f : E → F
x : E
⊢ x ∉ tsupport f → fderiv 𝕜 f x = 0
Module: Mathlib.Analysis.Calculus.Deriv.Support

Goal state before:
pp: 𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
E : Type v
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
h : f =ᶠ[nhds x] 0
⊢ HasStrictDerivAt f 0 x

Tactic:
]

Goal state after:
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
E : Type v
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
h : f =ᶠ[nhds x] 0
⊢ HasStrictDerivAt f 0 x
Module: Mathlib.Analysis.Calculus.Deriv.Support

Goal state before:
pp: 𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
E : Type v
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
h : f =ᶠ[nhds x] 0
⊢ deriv f x = 0

Tactic:
]

Goal state after:
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
E : Type v
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
h : f =ᶠ[nhds x] 0
⊢ deriv f x = 0
Module: Mathlib.Analysis.Calculus.Deriv.Support

Goal state before:
pp: 𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
E : Type v
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
⊢ x ∉ tsupport f → deriv f x = 0

Tactic:
]

Goal state after:
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
E : Type v
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
⊢ x ∉ tsupport f → deriv f x = 0
Module: Mathlib.Analysis.Asymptotics.TVS

Goal state before:
pp: α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : TopologicalSpace E
inst✝³ : Module 𝕜 E
inst✝² : AddCommGroup F
inst✝¹ : TopologicalSpace F
inst✝ : Module 𝕜 F
f : α → E
g : α → F
l : Filter α
h : f =o[𝕜; l] g
U : Set E
hU : U ∈ 𝓝 0
V : Set F
hV₀ : V ∈ 𝓝 0
hV : ∀ (ε : ℝ≥0), ε ≠ 0 → (fun x ↦ egauge 𝕜 U (f x)) ≤ᶠ[l] fun x ↦ ↑ε * egauge 𝕜 V (g x)
hε : ∞ ≠ 0
x✝ : α
⊢ 1 * egauge 𝕜 V (g x✝) ≤ ?m.137 * egauge 𝕜 V (g x✝)

pp: α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : TopologicalSpace E
inst✝³ : Module 𝕜 E
inst✝² : AddCommGroup F
inst✝¹ : TopologicalSpace F
inst✝ : Module 𝕜 F
f : α → E
g : α → F
l : Filter α
h : f =o[𝕜; l] g
U : Set E
hU : U ∈ 𝓝 0
V : Set F
hV₀ : V ∈ 𝓝 0
hV : ∀ (ε : ℝ≥0), ε ≠ 0 → (fun x ↦ egauge 𝕜 U (f x)) ≤ᶠ[l] fun x ↦ ↑ε * egauge 𝕜 V (g x)
hε : ∞ ≠ 0
x✝ : α
⊢ ℝ≥0∞

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.Asymptotics.TVS

Goal state before:
pp: α : Type u_1
𝕜 : Type u_3
E : Type u_4
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : TopologicalSpace E
inst✝ : Module 𝕜 E
f : α → E
l : Filter α
⊢ ∀ U ∈ 𝓝 0, ∃ V ∈ 𝓝 0, (fun x ↦ egauge 𝕜 U (f x)) ≤ᶠ[l] fun x ↦ egauge 𝕜 V (f x)

Tactic:
]

Goal state after:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : TopologicalSpace E
inst✝ : Module 𝕜 E
f : α → E
l : Filter α
⊢ ∀ U ∈ 𝓝 0, ∃ V ∈ 𝓝 0, (fun x ↦ egauge 𝕜 U (f x)) ≤ᶠ[l] fun x ↦ egauge 𝕜 V (f x)
Module: Mathlib.Analysis.Asymptotics.TVS

Goal state before:
pp: α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : TopologicalSpace E
inst✝³ : Module 𝕜 E
inst✝² : AddCommGroup F
inst✝¹ : TopologicalSpace F
inst✝ : Module 𝕜 F
l : Filter α
f : α → E
g : α → F
ιE : Sort u_7
ιF : Sort u_8
pE : ιE → Prop
pF : ιF → Prop
sE : ιE → Set E
sF : ιF → Set F
hE : (𝓝 0).HasBasis pE sE
hF : (𝓝 0).HasBasis pF sF
⊢ (∀ U ∈ 𝓝 0, ∃ V ∈ 𝓝 0, ∀ (ε : ℝ≥0), ε ≠ 0 → (fun x ↦ egauge 𝕜 U (f x)) ≤ᶠ[l] fun x ↦ ↑ε * egauge 𝕜 V (g x)) ↔
    ∀ (i : ιE),
      pE i → ∃ j, pF j ∧ ∀ (ε : ℝ≥0), ε ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 (sE i) (f x) ≤ ↑ε * egauge 𝕜 (sF j) (g x)

Tactic:
]

Goal state after:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : TopologicalSpace E
inst✝³ : Module 𝕜 E
inst✝² : AddCommGroup F
inst✝¹ : TopologicalSpace F
inst✝ : Module 𝕜 F
l : Filter α
f : α → E
g : α → F
ιE : Sort u_7
ιF : Sort u_8
pE : ιE → Prop
pF : ιF → Prop
sE : ιE → Set E
sF : ιF → Set F
hE : (𝓝 0).HasBasis pE sE
hF : (𝓝 0).HasBasis pF sF
⊢ (∀ U ∈ 𝓝 0, ∃ V ∈ 𝓝 0, ∀ (ε : ℝ≥0), ε ≠ 0 → (fun x ↦ egauge 𝕜 U (f x)) ≤ᶠ[l] fun x ↦ ↑ε * egauge 𝕜 V (g x)) ↔
    ∀ (i : ιE),
      pE i → ∃ j, pF j ∧ ∀ (ε : ℝ≥0), ε ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 (sE i) (f x) ≤ ↑ε * egauge 𝕜 (sF j) (g x)
Module: Mathlib.Analysis.Asymptotics.TVS

Goal state before:
pp: case refine_2
α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : TopologicalSpace E
inst✝³ : Module 𝕜 E
inst✝² : AddCommGroup F
inst✝¹ : TopologicalSpace F
inst✝ : Module 𝕜 F
l : Filter α
f : α → E
g : α → F
ιE : Sort u_7
ιF : Sort u_8
pE : ιE → Prop
pF : ιF → Prop
sE : ιE → Set E
sF : ιF → Set F
hE : (𝓝 0).HasBasis pE sE
hF : (𝓝 0).HasBasis pF sF
x✝¹ : ιE
x✝ : pE x✝¹
⊢ ∀ ⦃s t : Set F⦄,
    s ⊆ t →
      (∀ (ε : ℝ≥0), ε ≠ 0 → (fun x ↦ egauge 𝕜 (sE x✝¹) (f x)) ≤ᶠ[l] fun x ↦ ↑ε * egauge 𝕜 t (g x)) →
        ∀ (ε : ℝ≥0), ε ≠ 0 → (fun x ↦ egauge 𝕜 (sE x✝¹) (f x)) ≤ᶠ[l] fun x ↦ ↑ε * egauge 𝕜 s (g x)

Tactic:
refine fun s t hsub h ε hε ↦ (h ε hε).mono fun x hx ↦ hx.trans ?_

Goal state after:
case refine_2
α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : TopologicalSpace E
inst✝³ : Module 𝕜 E
inst✝² : AddCommGroup F
inst✝¹ : TopologicalSpace F
inst✝ : Module 𝕜 F
l : Filter α
f : α → E
g : α → F
ιE : Sort u_7
ιF : Sort u_8
pE : ιE → Prop
pF : ιF → Prop
sE : ιE → Set E
sF : ιF → Set F
hE : (𝓝 0).HasBasis pE sE
hF : (𝓝 0).HasBasis pF sF
x✝¹ : ιE
x✝ : pE x✝¹
s t : Set F
hsub : s ⊆ t
h : ∀ (ε : ℝ≥0), ε ≠ 0 → (fun x ↦ egauge 𝕜 (sE x✝¹) (f x)) ≤ᶠ[l] fun x ↦ ↑ε * egauge 𝕜 t (g x)
ε : ℝ≥0
hε : ε ≠ 0
x : α
hx : (fun x ↦ egauge 𝕜 (sE x✝¹) (f x)) x ≤ (fun x ↦ ↑ε * egauge 𝕜 t (g x)) x
⊢ (fun x ↦ ↑ε * egauge 𝕜 t (g x)) x ≤ (fun x ↦ ↑ε * egauge 𝕜 s (g x)) x
Module: Mathlib.Analysis.Asymptotics.TVS

Goal state before:
pp: α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : TopologicalSpace E
inst✝³ : Module 𝕜 E
inst✝² : AddCommGroup F
inst✝¹ : TopologicalSpace F
inst✝ : Module 𝕜 F
l : Filter α
f : α → E
g : α → F
ιE : Sort u_7
ιF : Sort u_8
pE : ιE → Prop
pF : ιF → Prop
sE : ιE → Set E
sF : ιF → Set F
hE : (𝓝 0).HasBasis pE sE
hF : (𝓝 0).HasBasis pF sF
⊢ (∀ U ∈ 𝓝 0, ∃ V ∈ 𝓝 0, (fun x ↦ egauge 𝕜 U (f x)) ≤ᶠ[l] fun x ↦ egauge 𝕜 V (g x)) ↔
    ∀ (i : ιE), pE i → ∃ j, pF j ∧ ∀ᶠ (x : α) in l, egauge 𝕜 (sE i) (f x) ≤ egauge 𝕜 (sF j) (g x)

Tactic:
]

Goal state after:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : TopologicalSpace E
inst✝³ : Module 𝕜 E
inst✝² : AddCommGroup F
inst✝¹ : TopologicalSpace F
inst✝ : Module 𝕜 F
l : Filter α
f : α → E
g : α → F
ιE : Sort u_7
ιF : Sort u_8
pE : ιE → Prop
pF : ιF → Prop
sE : ιE → Set E
sF : ιF → Set F
hE : (𝓝 0).HasBasis pE sE
hF : (𝓝 0).HasBasis pF sF
⊢ (∀ U ∈ 𝓝 0, ∃ V ∈ 𝓝 0, (fun x ↦ egauge 𝕜 U (f x)) ≤ᶠ[l] fun x ↦ egauge 𝕜 V (g x)) ↔
    ∀ (i : ιE), pE i → ∃ j, pF j ∧ ∀ᶠ (x : α) in l, egauge 𝕜 (sE i) (f x) ≤ egauge 𝕜 (sF j) (g x)
Module: Mathlib.Analysis.Asymptotics.TVS

Goal state before:
pp: α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : AddCommGroup E
inst✝⁵ : TopologicalSpace E
inst✝⁴ : Module 𝕜 E
inst✝³ : AddCommGroup F
inst✝² : TopologicalSpace F
inst✝¹ : Module 𝕜 F
l : Filter α
f : α → E
g : α → F
inst✝ : ContinuousConstSMul 𝕜 F
ι : Sort u_7
p : ι → Prop
U : ι → Set E
hb : (𝓝 0).HasBasis p U
h : ∀ (i : ι), p i → ∃ C, ∃ V ∈ 𝓝 0, (fun x ↦ egauge 𝕜 (U i) (f x)) ≤ᶠ[l] fun x ↦ ↑C * egauge 𝕜 V (g x)
⊢ ∀ (i : ι), p i → ∃ j ∈ 𝓝 0, ∀ᶠ (x : α) in l, egauge 𝕜 (U i) (f x) ≤ egauge 𝕜 (id j) (g x)

Tactic:
]

Goal state after:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : AddCommGroup E
inst✝⁵ : TopologicalSpace E
inst✝⁴ : Module 𝕜 E
inst✝³ : AddCommGroup F
inst✝² : TopologicalSpace F
inst✝¹ : Module 𝕜 F
l : Filter α
f : α → E
g : α → F
inst✝ : ContinuousConstSMul 𝕜 F
ι : Sort u_7
p : ι → Prop
U : ι → Set E
hb : (𝓝 0).HasBasis p U
h : ∀ (i : ι), p i → ∃ C, ∃ V ∈ 𝓝 0, (fun x ↦ egauge 𝕜 (U i) (f x)) ≤ᶠ[l] fun x ↦ ↑C * egauge 𝕜 V (g x)
⊢ ∀ (i : ι), p i → ∃ j ∈ 𝓝 0, ∀ᶠ (x : α) in l, egauge 𝕜 (U i) (f x) ≤ egauge 𝕜 (id j) (g x)
Module: Mathlib.Analysis.Asymptotics.TVS

Goal state before:
pp: α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : AddCommGroup E
inst✝⁵ : TopologicalSpace E
inst✝⁴ : Module 𝕜 E
inst✝³ : AddCommGroup F
inst✝² : TopologicalSpace F
inst✝¹ : Module 𝕜 F
l : Filter α
f : α → E
g : α → F
inst✝ : ContinuousConstSMul 𝕜 F
ι : Sort u_7
p : ι → Prop
U : ι → Set E
hb : (𝓝 0).HasBasis p U
h : ∀ (i : ι), p i → ∃ C, ∃ V ∈ 𝓝 0, (fun x ↦ egauge 𝕜 (U i) (f x)) ≤ᶠ[l] fun x ↦ ↑C * egauge 𝕜 V (g x)
i : ι
hi : p i
C : ℝ≥0
V : Set F
hV₀ : V ∈ 𝓝 0
hV : (fun x ↦ egauge 𝕜 (U i) (f x)) ≤ᶠ[l] fun x ↦ ↑C * egauge 𝕜 V (g x)
c : 𝕜
hc : C < ‖c‖₊
hc₀ : c ≠ 0
x : α
⊢ ↑‖c‖₊ * egauge 𝕜 V (g x) ≤ egauge 𝕜 (id (c⁻¹ • V)) (g x)

Tactic:
]

Goal state after:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : AddCommGroup E
inst✝⁵ : TopologicalSpace E
inst✝⁴ : Module 𝕜 E
inst✝³ : AddCommGroup F
inst✝² : TopologicalSpace F
inst✝¹ : Module 𝕜 F
l : Filter α
f : α → E
g : α → F
inst✝ : ContinuousConstSMul 𝕜 F
ι : Sort u_7
p : ι → Prop
U : ι → Set E
hb : (𝓝 0).HasBasis p U
h : ∀ (i : ι), p i → ∃ C, ∃ V ∈ 𝓝 0, (fun x ↦ egauge 𝕜 (U i) (f x)) ≤ᶠ[l] fun x ↦ ↑C * egauge 𝕜 V (g x)
i : ι
hi : p i
C : ℝ≥0
V : Set F
hV₀ : V ∈ 𝓝 0
hV : (fun x ↦ egauge 𝕜 (U i) (f x)) ≤ᶠ[l] fun x ↦ ↑C * egauge 𝕜 V (g x)
c : 𝕜
hc : C < ‖c‖₊
hc₀ : c ≠ 0
x : α
⊢ ↑‖c‖₊ * egauge 𝕜 V (g x) ≤ egauge 𝕜 (id (c⁻¹ • V)) (g x)
Module: Mathlib.Analysis.Asymptotics.TVS

Goal state before:
pp: case right
α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : TopologicalSpace E
inst✝³ : Module 𝕜 E
inst✝² : AddCommGroup F
inst✝¹ : TopologicalSpace F
inst✝ : Module 𝕜 F
l : Filter α
f : α → E
g : E →ₗ[𝕜] F
hg : comap (⇑g) (𝓝 0) ≤ 𝓝 0
U : Set E
hU : U ∈ 𝓝 0
V : Set F
hV : V ∈ 𝓝 0
hgV : ⇑g ⁻¹' V ⊆ U
a : α
c : 𝕜
hc₀ : c ≠ 0
hc : (⇑g ∘ f) a ∈ c • V
⊢ f a ∈ ⇑g ⁻¹' (c • V)

Tactic:
]

Goal state after:
case right
α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : TopologicalSpace E
inst✝³ : Module 𝕜 E
inst✝² : AddCommGroup F
inst✝¹ : TopologicalSpace F
inst✝ : Module 𝕜 F
l : Filter α
f : α → E
g : E →ₗ[𝕜] F
hg : comap (⇑g) (𝓝 0) ≤ 𝓝 0
U : Set E
hU : U ∈ 𝓝 0
V : Set F
hV : V ∈ 𝓝 0
hgV : ⇑g ⁻¹' V ⊆ U
a : α
c : 𝕜
hc₀ : c ≠ 0
hc : (⇑g ∘ f) a ∈ c • V
⊢ f a ∈ ⇑g ⁻¹' (c • V)
Module: Mathlib.Analysis.Asymptotics.TVS

Goal state before:
pp: α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : AddCommGroup E
inst✝⁵ : TopologicalSpace E
inst✝⁴ : Module 𝕜 E
inst✝³ : AddCommGroup F
inst✝² : TopologicalSpace F
inst✝¹ : Module 𝕜 F
f : α → E
g : α → F
inst✝ : TopologicalSpace α
x : α
s : Set α
h : f x = 0
⊢ f =o[𝕜; 𝓝[s] x] g ↔ f =o[𝕜; 𝓝[s] x] g

pp: α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : AddCommGroup E
inst✝⁵ : TopologicalSpace E
inst✝⁴ : Module 𝕜 E
inst✝³ : AddCommGroup F
inst✝² : TopologicalSpace F
inst✝¹ : Module 𝕜 F
f : α → E
g : α → F
inst✝ : TopologicalSpace α
x : α
s : Set α
h : f x = 0
⊢ f =o[𝕜; pure x] g

Tactic:
]

Goal state after:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : AddCommGroup E
inst✝⁵ : TopologicalSpace E
inst✝⁴ : Module 𝕜 E
inst✝³ : AddCommGroup F
inst✝² : TopologicalSpace F
inst✝¹ : Module 𝕜 F
f : α → E
g : α → F
inst✝ : TopologicalSpace α
x : α
s : Set α
h : f x = 0
⊢ f =o[𝕜; pure x] g
Module: Mathlib.Analysis.Asymptotics.TVS

Goal state before:
pp: α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝¹¹ : NontriviallyNormedField 𝕜
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : TopologicalSpace E
inst✝⁸ : Module 𝕜 E
inst✝⁷ : AddCommGroup F
inst✝⁶ : TopologicalSpace F
inst✝⁵ : Module 𝕜 F
inst✝⁴ : AddCommGroup G
inst✝³ : TopologicalSpace G
inst✝² : Module 𝕜 G
l : Filter α
f : α → E
g : α → F
inst✝¹ : ContinuousSMul 𝕜 E
inst✝ : ContinuousSMul 𝕜 F
k : α → G
hf : f =o[𝕜; l] k
hg : g =o[𝕜; l] k
⊢ ∀ (i : Set E × Set F),
    (i.1 ∈ 𝓝 0 ∧ Balanced 𝕜 i.1) ∧ i.2 ∈ 𝓝 0 ∧ Balanced 𝕜 i.2 →
      ∃ j ∈ 𝓝 0,
        ∀ (ε : ℝ≥0), ε ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 (id i.1 ×ˢ id i.2) (f x, g x) ≤ ↑ε * egauge 𝕜 (id j) (k x)

Tactic:
]

Goal state after:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝¹¹ : NontriviallyNormedField 𝕜
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : TopologicalSpace E
inst✝⁸ : Module 𝕜 E
inst✝⁷ : AddCommGroup F
inst✝⁶ : TopologicalSpace F
inst✝⁵ : Module 𝕜 F
inst✝⁴ : AddCommGroup G
inst✝³ : TopologicalSpace G
inst✝² : Module 𝕜 G
l : Filter α
f : α → E
g : α → F
inst✝¹ : ContinuousSMul 𝕜 E
inst✝ : ContinuousSMul 𝕜 F
k : α → G
hf : f =o[𝕜; l] k
hg : g =o[𝕜; l] k
⊢ ∀ (i : Set E × Set F),
    (i.1 ∈ 𝓝 0 ∧ Balanced 𝕜 i.1) ∧ i.2 ∈ 𝓝 0 ∧ Balanced 𝕜 i.2 →
      ∃ j ∈ 𝓝 0,
        ∀ (ε : ℝ≥0), ε ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 (id i.1 ×ˢ id i.2) (f x, g x) ≤ ↑ε * egauge 𝕜 (id j) (k x)
Module: Mathlib.Analysis.Asymptotics.TVS

Goal state before:
pp: α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝¹¹ : NontriviallyNormedField 𝕜
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : TopologicalSpace E
inst✝⁸ : Module 𝕜 E
inst✝⁷ : AddCommGroup F
inst✝⁶ : TopologicalSpace F
inst✝⁵ : Module 𝕜 F
inst✝⁴ : AddCommGroup G
inst✝³ : TopologicalSpace G
inst✝² : Module 𝕜 G
l : Filter α
f : α → E
g : α → F
inst✝¹ : ContinuousSMul 𝕜 E
inst✝ : ContinuousSMul 𝕜 F
k : α → G
hf : f =O[𝕜; l] k
hg : g =O[𝕜; l] k
⊢ ∀ (i : Set E × Set F),
    (i.1 ∈ 𝓝 0 ∧ Balanced 𝕜 i.1) ∧ i.2 ∈ 𝓝 0 ∧ Balanced 𝕜 i.2 →
      ∃ j ∈ 𝓝 0, ∀ᶠ (x : α) in l, egauge 𝕜 (id i.1 ×ˢ id i.2) (f x, g x) ≤ egauge 𝕜 (id j) (k x)

Tactic:
]

Goal state after:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝¹¹ : NontriviallyNormedField 𝕜
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : TopologicalSpace E
inst✝⁸ : Module 𝕜 E
inst✝⁷ : AddCommGroup F
inst✝⁶ : TopologicalSpace F
inst✝⁵ : Module 𝕜 F
inst✝⁴ : AddCommGroup G
inst✝³ : TopologicalSpace G
inst✝² : Module 𝕜 G
l : Filter α
f : α → E
g : α → F
inst✝¹ : ContinuousSMul 𝕜 E
inst✝ : ContinuousSMul 𝕜 F
k : α → G
hf : f =O[𝕜; l] k
hg : g =O[𝕜; l] k
⊢ ∀ (i : Set E × Set F),
    (i.1 ∈ 𝓝 0 ∧ Balanced 𝕜 i.1) ∧ i.2 ∈ 𝓝 0 ∧ Balanced 𝕜 i.2 →
      ∃ j ∈ 𝓝 0, ∀ᶠ (x : α) in l, egauge 𝕜 (id i.1 ×ˢ id i.2) (f x, g x) ≤ egauge 𝕜 (id j) (k x)
Module: Mathlib.Analysis.Calculus.Deriv.Basic

Goal state before:
pp: 𝕜 : Type u
inst✝³ : NontriviallyNormedField 𝕜
F : Type v
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 F
inst✝ : TopologicalSpace F
f : 𝕜 → F
x : 𝕜
s : Set 𝕜
h : ¬DifferentiableWithinAt 𝕜 f s x
⊢ 0 1 = 0

Tactic:
]

Goal state after:
𝕜 : Type u
inst✝³ : NontriviallyNormedField 𝕜
F : Type v
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 F
inst✝ : TopologicalSpace F
f : 𝕜 → F
x : 𝕜
s : Set 𝕜
h : ¬DifferentiableWithinAt 𝕜 f s x
⊢ 0 1 = 0
Module: Mathlib.Analysis.Calculus.Deriv.Basic

Goal state before:
pp: 𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
x : 𝕜
s : Set 𝕜
h : ¬AccPt x (𝓟 s)
⊢ 0 = 0

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.Calculus.Deriv.Basic

Goal state before:
pp: 𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
x : 𝕜
s : Set 𝕜
h : x ∉ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
⊢ 0 = 0

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.Calculus.Deriv.Basic

Goal state before:
pp: 𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
x : 𝕜
h : ¬DifferentiableAt 𝕜 f x
⊢ 0 1 = 0

Tactic:
]

Goal state after:
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
x : 𝕜
h : ¬DifferentiableAt 𝕜 f x
⊢ 0 1 = 0
Module: Mathlib.Analysis.Calculus.Deriv.Basic

Goal state before:
pp: 𝕜 : Type u
inst✝³ : NontriviallyNormedField 𝕜
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
f : 𝕜 → F
f' : F
x : 𝕜
inst✝ : PartialOrder 𝕜
⊢ HasDerivWithinAt f f' (Ici x) x ↔ HasDerivWithinAt f f' (Ici x) x

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.Calculus.Deriv.Basic

Goal state before:
pp: 𝕜 : Type u
inst✝³ : NontriviallyNormedField 𝕜
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
f : 𝕜 → F
f' : F
x : 𝕜
inst✝ : PartialOrder 𝕜
⊢ HasDerivWithinAt f f' (Iic x) x ↔ HasDerivWithinAt f f' (Iic x) x

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.Calculus.Deriv.Basic

Goal state before:
pp: 𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
x y : 𝕜
⊢ (fderiv 𝕜 f x) y = (fderiv 𝕜 f x) (y • 1)

Tactic:
]

Goal state after:
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
x y : 𝕜
⊢ (fderiv 𝕜 f x) y = (fderiv 𝕜 f x) (y • 1)
Module: Mathlib.Analysis.Calculus.Deriv.Basic

Goal state before:
pp: 𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
x : 𝕜
s : Set 𝕜
h : DifferentiableAt 𝕜 f x
hxs : UniqueDiffWithinAt 𝕜 s x
⊢ _root_.derivWithin f s x = deriv f x

Tactic:
unfold _root_.derivWithin deriv

Goal state after:
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
x : 𝕜
s : Set 𝕜
h : DifferentiableAt 𝕜 f x
hxs : UniqueDiffWithinAt 𝕜 s x
⊢ (fderivWithin 𝕜 f s x) 1 = (fderiv 𝕜 f x) 1
Module: Mathlib.Analysis.Calculus.Deriv.Basic

Goal state before:
pp: 𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
x : 𝕜
s : Set 𝕜
h : DifferentiableAt 𝕜 f x
hxs : UniqueDiffWithinAt 𝕜 s x
⊢ (fderiv 𝕜 f x) 1 = (fderiv 𝕜 f x) 1

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.Calculus.Deriv.Basic

Goal state before:
pp: 𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
x✝ : 𝕜
⊢ (fderiv 𝕜 f x✝) 1 = (fderiv 𝕜 f x✝) 1

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.Calculus.Deriv.Basic

Goal state before:
pp: 𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
x : 𝕜
s t : Set 𝕜
ht : t ∈ 𝓝 x
⊢ (fderivWithin 𝕜 f s x) 1 = (fderivWithin 𝕜 f s x) 1

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.Calculus.Deriv.Basic

Goal state before:
pp: 𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
s : Set 𝕜
f' : 𝕜 → F
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hf' : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x
x : 𝕜
hx : x ∈ s
⊢ f' x = f' x

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.Calculus.Deriv.Basic

Goal state before:
pp: case neg
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
x : ℝ
H : ¬DifferentiableWithinAt ℝ f (Ioi x) x
⊢ 0 = 0

pp: case neg
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
x : ℝ
H : ¬DifferentiableWithinAt ℝ f (Ioi x) x
⊢ ¬DifferentiableWithinAt ℝ f (Ici x) x

Tactic:
]

Goal state after:
case neg
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
x : ℝ
H : ¬DifferentiableWithinAt ℝ f (Ioi x) x
⊢ ¬DifferentiableWithinAt ℝ f (Ici x) x
Module: Mathlib.Analysis.Calculus.Deriv.Basic

Goal state before:
pp: case neg
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
x : ℝ
H : ¬DifferentiableWithinAt ℝ f (Ici x) x
⊢ ¬DifferentiableWithinAt ℝ f (Ici x) x

Tactic:
]

Goal state after:
case neg
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
x : ℝ
H : ¬DifferentiableWithinAt ℝ f (Ici x) x
⊢ ¬DifferentiableWithinAt ℝ f (Ici x) x
Module: Mathlib.Analysis.Calculus.Deriv.Basic

Goal state before:
pp: 𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f f₁ : 𝕜 → F
f' : F
L : Filter (𝕜 × 𝕜)
h : HasDerivAtFilter f f' L
hL : Prod.map f₁ f₁ =ᶠ[L] Prod.map f f
⊢ HasDerivAtFilter f f' L

Tactic:
]

Goal state after:
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f f₁ : 𝕜 → F
f' : F
L : Filter (𝕜 × 𝕜)
h : HasDerivAtFilter f f' L
hL : Prod.map f₁ f₁ =ᶠ[L] Prod.map f f
⊢ HasDerivAtFilter f f' L
Module: Mathlib.Analysis.Calculus.Deriv.Basic

Goal state before:
pp: 𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f f₁ : 𝕜 → F
x : 𝕜
s : Set 𝕜
hs : f₁ =ᶠ[𝓝[s] x] f
hx : f₁ x = f x
⊢ (fderivWithin 𝕜 f s x) 1 = (fderivWithin 𝕜 f s x) 1

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.Calculus.Deriv.Basic

Goal state before:
pp: 𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f f₁ : 𝕜 → F
x : 𝕜
s : Set 𝕜
hs : EqOn f₁ f s
hx : f₁ x = f x
⊢ (fderivWithin 𝕜 f s x) 1 = (fderivWithin 𝕜 f s x) 1

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.Calculus.Deriv.Basic

Goal state before:
pp: 𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f g : 𝕜 → F
s : Set 𝕜
hfg : EqOn f g s
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
x : 𝕜
hx : x ∈ s
⊢ derivWithin f s x = derivWithin g s x

Tactic:
]

Goal state after:
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f g : 𝕜 → F
s : Set 𝕜
hfg : EqOn f g s
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
x : 𝕜
hx : x ∈ s
⊢ derivWithin f s x = derivWithin g s x