awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Calculus.FDeriv.Congr
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
F : Type u_3
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : TopologicalSpace F
f f₁ : E → F
x : E
s t : Set E
inst_7 : ContinuousAdd E
inst_8 : ContinuousSMul 𝕜 E
inst_9 : ContinuousAdd F
inst_10 : ContinuousSMul 𝕜 F
inst_11 : T2Space F
h : DifferentiableWithinAt 𝕜 f s x
hs : EqOn f₁ f t
hx : f₁ x = f x
hxt : UniqueDiffWithinAt 𝕜 t x
h₁ : t ⊆ s
⊢ Eq (α := E →L[𝕜] F) (fderivWithin 𝕜 f₁ t x) (fderivWithin 𝕜 f s x)

Tactic:
(HasFDerivWithinAt.congr_mono h.hasFDerivWithinAt hs hx h₁).fderivWithin hxt

Premises used: HasFDerivWithinAt.fderivWithin, HasFDerivWithinAt.congr_mono, DifferentiableWithinAt.hasFDerivWithinAt
-- Module: Mathlib.Analysis.Calculus.FDeriv.Congr
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
F : Type u_3
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : TopologicalSpace F
f f₁ : E → F
x : E
s : Set E
hs : f₁ =ᶠ[𝓝[s] x] f
hx : f₁ x = f x
⊢ Eq (α := E →L[𝕜] F) (fderivWithin 𝕜 f₁ s x) (fderivWithin 𝕜 f s x)

Tactic:
simp only [fderivWithin, DifferentiableWithinAt, hs.hasFDerivWithinAt_iff hx]

Premises used: Filter.EventuallyEq.hasFDerivWithinAt_iff, fderivWithin, DifferentiableWithinAt
-- Module: Mathlib.Analysis.Calculus.FDeriv.Congr
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
F : Type u_3
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : TopologicalSpace F
f f₁ : E → F
x : E
s : Set E
hs : f₁ =ᶠ[𝓝[s] x] f
hx : f₁ x = f x
⊢ Eq (α := E →L[𝕜] F) (fderivWithin 𝕜 f₁ s x) (fderivWithin 𝕜 f s x)

Tactic:
classical
  simp only [fderivWithin, DifferentiableWithinAt, hs.hasFDerivWithinAt_iff hx]

Premises used: Filter.EventuallyEq.hasFDerivWithinAt_iff, fderivWithin, DifferentiableWithinAt
-- Module: Mathlib.Analysis.Calculus.FDeriv.Congr
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
F : Type u_3
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : TopologicalSpace F
f f₁ : E → F
x : E
s : Set E
hs : f₁ =ᶠ[𝓝[s] x] f
hx : x ∈ s
⊢ Eq (α := E →L[𝕜] F) (fderivWithin 𝕜 f₁ s x) (fderivWithin 𝕜 f s x)

Tactic:
hs.fderivWithin_eq (mem_of_mem_nhdsWithin hx hs :)

Premises used: Filter.EventuallyEq.fderivWithin_eq, mem_of_mem_nhdsWithin
-- Module: Mathlib.Analysis.Calculus.FDeriv.Congr
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
F : Type u_3
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : TopologicalSpace F
f f₁ : E → F
x : E
s : Set E
hs : f₁ =ᶠ[𝓝[insert x s] x] f
apply : f₁ x = f x
⊢ Eq (α := E →L[𝕜] F) (fderivWithin 𝕜 f₁ s x) (fderivWithin 𝕜 f s x)

Tactic:
apply Filter.EventuallyEq.fderivWithin_eq (nhdsWithin_mono _ (subset_insert x s) hs)

Premises used: Filter.EventuallyEq.fderivWithin_eq, Set.subset_insert, nhdsWithin_mono
-- Module: Mathlib.Analysis.Calculus.FDeriv.Congr
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
F : Type u_3
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : TopologicalSpace F
f f₁ : E → F
x : E
s : Set E
hs : f₁ =ᶠ[𝓝[insert x s] x] f
⊢ f₁ x = f x

Tactic:
(mem_of_mem_nhdsWithin (mem_insert x s) hs :)

Premises used: Set.Mem, setOf, mem_of_mem_nhdsWithin, Set.mem_insert
-- Module: Mathlib.Analysis.Calculus.FDeriv.Congr
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
F : Type u_3
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : TopologicalSpace F
f f₁ : E → F
x : E
s : Set E
hs : f₁ =ᶠ[𝓝[insert x s] x] f
⊢ f₁ x = f x

Tactic:
exact (mem_of_mem_nhdsWithin (mem_insert x s) hs :)

Premises used: mem_of_mem_nhdsWithin, Set.mem_insert
-- Module: Mathlib.Analysis.Calculus.FDeriv.Congr
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
F : Type u_3
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : TopologicalSpace F
f f₁ : E → F
x : E
s t : Set E
hs : f₁ =ᶠ[𝓝[s] x] f
ht : t ⊆ s
⊢ (𝓝[s] x).EventuallyEq (β := E →L[𝕜] F) (fderivWithin 𝕜 f₁ t) (fderivWithin 𝕜 f t)

Tactic:
(eventually_eventually_nhdsWithin.2 hs).mp <|
    eventually_mem_nhdsWithin.mono fun _y hys hs =>
      EventuallyEq.fderivWithin_eq (hs.filter_mono <| nhdsWithin_mono _ ht)
        (hs.self_of_nhdsWithin hys)

Premises used: Iff.mpr, Filter.Eventually.filter_mono, Filter.Eventually.self_of_nhdsWithin, Filter.EventuallyEq.fderivWithin_eq, eventually_mem_nhdsWithin, Filter.EventuallyEq, Filter.Eventually.mono, Filter.Eventually.mp, eventually_eventually_nhdsWithin, nhdsWithin_mono
-- Module: Mathlib.Analysis.Calculus.FDeriv.Congr
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
F : Type u_3
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : TopologicalSpace F
f f₁ : E → F
x : E
s : Set E
hs : f₁ =ᶠ[𝓝[s] x] f
⊢ (𝓝[s] x).EventuallyEq (β := E →L[𝕜] F) (fderivWithin 𝕜 f₁ s) (fderivWithin 𝕜 f s)

Tactic:
hs.fderivWithin' Subset.rfl

Premises used: Set.Subset.rfl, Filter.EventuallyEq.fderivWithin'
-- Module: Mathlib.Analysis.Calculus.FDeriv.Congr
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
F : Type u_3
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : TopologicalSpace F
f f₁ : E → F
x : E
s : Set E
h : f₁ =ᶠ[𝓝 x] f
⊢ Eq (α := E →L[𝕜] F) (fderivWithin 𝕜 f₁ s x) (fderivWithin 𝕜 f s x)

Tactic:
(h.filter_mono nhdsWithin_le_nhds).fderivWithin_eq h.self_of_nhds

Premises used: Filter.EventuallyEq.filter_mono, Filter.Eventually.self_of_nhds, Filter.EventuallyEq.fderivWithin_eq, nhdsWithin_le_nhds
-- Module: Mathlib.Analysis.Calculus.FDeriv.Congr
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
F : Type u_3
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : TopologicalSpace F
f f₁ : E → F
x : E
s : Set E
hs : EqOn f₁ f s
hx : f₁ x = f x
⊢ Eq (α := E →L[𝕜] F) (fderivWithin 𝕜 f₁ s x) (fderivWithin 𝕜 f s x)

Tactic:
(hs.eventuallyEq.filter_mono inf_le_right).fderivWithin_eq hx

Premises used: Filter.EventuallyEq.filter_mono, Filter.EventuallyEq.fderivWithin_eq, Set.EqOn.eventuallyEq, inf_le_right
-- Module: Mathlib.Analysis.Calculus.FDeriv.Congr
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
F : Type u_3
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : TopologicalSpace F
f f₁ : E → F
x : E
s : Set E
hs : EqOn f₁ f s
hx : x ∈ s
⊢ Eq (α := E →L[𝕜] F) (fderivWithin 𝕜 f₁ s x) (fderivWithin 𝕜 f s x)

Tactic:
fderivWithin_congr hs (hs hx)

Premises used: fderivWithin_congr
-- Module: Mathlib.Analysis.Calculus.FDeriv.Congr
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
F : Type u_3
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : TopologicalSpace F
f f₁ : E → F
x : E
h : f₁ =ᶠ[𝓝 x] f
rw : Eq (α := E →L[𝕜] F) (fderivWithin 𝕜 f₁ univ x) (fderiv 𝕜 f x)
rw₁ : Eq (α := E →L[𝕜] F) (fderivWithin 𝕜 f₁ univ x) (fderivWithin 𝕜 f univ x)
rw₂ rw₃ : Eq (α := E →L[𝕜] F) (fderivWithin 𝕜 f univ x) (fderivWithin 𝕜 f univ x)
⊢ Eq (α := E →L[𝕜] F) (fderiv 𝕜 f₁ x) (fderiv 𝕜 f x)

Tactic:
rw [← fderivWithin_univ, ← fderivWithin_univ, h.fderivWithin_eq_of_nhds]

Premises used: fderivWithin_univ, Filter.EventuallyEq.fderivWithin_eq_of_nhds
-- Module: Mathlib.Analysis.Calculus.FDeriv.Congr
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
F : Type u_3
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : TopologicalSpace F
f f₁ : E → F
x : E
h : f₁ =ᶠ[𝓝 x] f
⊢ (𝓝 x).EventuallyEq (β := E →L[𝕜] F) (fderiv 𝕜 f₁) (fderiv 𝕜 f)

Tactic:
h.eventuallyEq_nhds.mono fun _ h => h.fderiv_eq

Premises used: Filter.EventuallyEq.fderiv_eq, Filter.EventuallyEq, Filter.EventuallyEq.eventuallyEq_nhds, Filter.Eventually.mono
-- Module: Mathlib.Analysis.Calculus.FDeriv.Const
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
F : Type u_3
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : TopologicalSpace F
c : F
L : Filter (E × E)
x : E × E
⊢ 0 x = HSub.hSub (β := F) (c - c) ((0 : (a : E) → F) (x.1 - x.2) : F)

Tactic:
simp
-- Module: Mathlib.Analysis.Calculus.FDeriv.Const
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
F : Type u_3
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : TopologicalSpace F
L : Filter (E × E)
⊢ HasFDerivAtFilter.{u_1, u_2, u_3} (𝕜 := 𝕜) (F := F) 0 0 L

Tactic:
hasFDerivAtFilter_const _ _

Premises used: hasFDerivAtFilter_const
-- Module: Mathlib.Analysis.Calculus.FDeriv.Const
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
F : Type u_3
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : TopologicalSpace F
inst_7 : One F
L : Filter (E × E)
⊢ HasFDerivAtFilter.{u_1, u_2, u_3} (𝕜 := 𝕜) (F := F) 1 0 L

Tactic:
hasFDerivAtFilter_const _ _

Premises used: hasFDerivAtFilter_const
-- Module: Mathlib.Analysis.Calculus.FDeriv.Const
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
F : Type u_3
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : TopologicalSpace F
inst_7 : NatCast F
n : ℕ
L : Filter (E × E)
⊢ HasFDerivAtFilter.{u_1, u_2, u_3} (𝕜 := 𝕜) (F := F) (↑n : E → F) 0 L

Tactic:
hasFDerivAtFilter_const _ _

Premises used: hasFDerivAtFilter_const
-- Module: Mathlib.Analysis.Calculus.FDeriv.Const
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
F : Type u_3
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : TopologicalSpace F
inst_7 : IntCast F
z : ℤ
L : Filter (E × E)
⊢ HasFDerivAtFilter.{u_1, u_2, u_3} (𝕜 := 𝕜) (F := F) (↑z : E → F) 0 L

Tactic:
hasFDerivAtFilter_const _ _

Premises used: hasFDerivAtFilter_const
-- Module: Mathlib.Analysis.Calculus.FDeriv.Const
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
F : Type u_3
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : TopologicalSpace F
n : ℕ
inst_7 : OfNat F n
L : Filter (E × E)
⊢ HasFDerivAtFilter.{u_1, u_2, u_3} (𝕜 := 𝕜) (F := F) (OfNat.ofNat n) 0 L

Tactic:
hasFDerivAtFilter_const _ _

Premises used: hasFDerivAtFilter_const
-- Module: Mathlib.Analysis.Calculus.FDeriv.Const
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
F : Type u_3
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : TopologicalSpace F
c : F
x : E
⊢ HasStrictFDerivAt.{u_1, u_2, u_3} (𝕜 := 𝕜) (F := F) (fun (x : E) ↦ c) 0 x

Tactic:
hasFDerivAtFilter_const _ _

Premises used: hasFDerivAtFilter_const, HasStrictFDerivAt
-- Module: Mathlib.Analysis.Calculus.FDeriv.Const
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
F : Type u_3
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : TopologicalSpace F
x : E
⊢ HasStrictFDerivAt.{u_1, u_2, u_3} (𝕜 := 𝕜) (F := F) 0 0 x

Tactic:
hasStrictFDerivAt_const _ _

Premises used: hasStrictFDerivAt_const
-- Module: Mathlib.Analysis.Calculus.FDeriv.Const
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
F : Type u_3
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : TopologicalSpace F
inst_7 : One F
x : E
⊢ HasStrictFDerivAt.{u_1, u_2, u_3} (𝕜 := 𝕜) (F := F) 1 0 x

Tactic:
hasStrictFDerivAt_const _ _

Premises used: hasStrictFDerivAt_const
-- Module: Mathlib.Analysis.Calculus.FDeriv.Const
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
F : Type u_3
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : TopologicalSpace F
inst_7 : NatCast F
n : ℕ
x : E
⊢ HasStrictFDerivAt.{u_1, u_2, u_3} (𝕜 := 𝕜) (F := F) (↑n : E → F) 0 x

Tactic:
hasStrictFDerivAt_const _ _

Premises used: hasStrictFDerivAt_const
-- Module: Mathlib.Analysis.Calculus.FDeriv.Const
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
F : Type u_3
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : TopologicalSpace F
inst_7 : IntCast F
z : ℤ
x : E
⊢ HasStrictFDerivAt.{u_1, u_2, u_3} (𝕜 := 𝕜) (F := F) (↑z : E → F) 0 x

Tactic:
hasStrictFDerivAt_const _ _

Premises used: hasStrictFDerivAt_const
-- Module: Mathlib.Analysis.Calculus.FDeriv.Const
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
F : Type u_3
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : TopologicalSpace F
n : ℕ
inst_7 : OfNat F n
x : E
⊢ HasStrictFDerivAt.{u_1, u_2, u_3} (𝕜 := 𝕜) (F := F) (OfNat.ofNat n) 0 x

Tactic:
hasStrictFDerivAt_const _ _

Premises used: hasStrictFDerivAt_const
-- Module: Mathlib.Analysis.Calculus.FDeriv.Const
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
F : Type u_3
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : TopologicalSpace F
c : F
x : E
s : Set E
⊢ HasFDerivWithinAt.{u_1, u_2, u_3} (𝕜 := 𝕜) (F := F) (fun (x : E) ↦ c) 0 s x

Tactic:
hasFDerivAtFilter_const _ _

Premises used: hasFDerivAtFilter_const, HasFDerivWithinAt
-- Module: Mathlib.Analysis.Calculus.FDeriv.Const
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
F : Type u_3
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : TopologicalSpace F
x : E
s : Set E
⊢ HasFDerivWithinAt.{u_1, u_2, u_3} (𝕜 := 𝕜) (F := F) 0 0 s x

Tactic:
hasFDerivWithinAt_const _ _ _

Premises used: hasFDerivWithinAt_const
-- Module: Mathlib.Analysis.Calculus.FDeriv.Const
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
F : Type u_3
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : TopologicalSpace F
inst_7 : One F
x : E
s : Set E
⊢ HasFDerivWithinAt.{u_1, u_2, u_3} (𝕜 := 𝕜) (F := F) 1 0 s x

Tactic:
hasFDerivWithinAt_const _ _ _

Premises used: hasFDerivWithinAt_const
-- Module: Mathlib.Analysis.Calculus.FDeriv.Const
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
F : Type u_3
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : TopologicalSpace F
inst_7 : NatCast F
n : ℕ
x : E
s : Set E
⊢ HasFDerivWithinAt.{u_1, u_2, u_3} (𝕜 := 𝕜) (F := F) (↑n : E → F) 0 s x

Tactic:
hasFDerivWithinAt_const _ _ _

Premises used: hasFDerivWithinAt_const
-- Module: Mathlib.Analysis.Calculus.FDeriv.Const
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
F : Type u_3
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : TopologicalSpace F
inst_7 : IntCast F
z : ℤ
x : E
s : Set E
⊢ HasFDerivWithinAt.{u_1, u_2, u_3} (𝕜 := 𝕜) (F := F) (↑z : E → F) 0 s x

Tactic:
hasFDerivWithinAt_const _ _ _

Premises used: hasFDerivWithinAt_const
-- Module: Mathlib.Analysis.Calculus.FDeriv.Const
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
F : Type u_3
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : TopologicalSpace F
n : ℕ
inst_7 : OfNat F n
x : E
s : Set E
⊢ HasFDerivWithinAt.{u_1, u_2, u_3} (𝕜 := 𝕜) (F := F) (OfNat.ofNat n) 0 s x

Tactic:
hasFDerivWithinAt_const _ _ _

Premises used: hasFDerivWithinAt_const
-- Module: Mathlib.Analysis.Calculus.FDeriv.Const
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
F : Type u_3
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : TopologicalSpace F
c : F
x : E
⊢ HasFDerivAt.{u_1, u_2, u_3} (𝕜 := 𝕜) (F := F) (fun (x : E) ↦ c) 0 x

Tactic:
hasFDerivAtFilter_const _ _

Premises used: HasFDerivAt, hasFDerivAtFilter_const
-- Module: Mathlib.Analysis.Calculus.FDeriv.Const
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
F : Type u_3
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : TopologicalSpace F
x : E
⊢ HasFDerivAt.{u_1, u_2, u_3} (𝕜 := 𝕜) (F := F) 0 0 x

Tactic:
hasFDerivAt_const _ _

Premises used: hasFDerivAt_const
-- Module: Mathlib.Analysis.Calculus.FDeriv.Const
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
F : Type u_3
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : TopologicalSpace F
inst_7 : One F
x : E
⊢ HasFDerivAt.{u_1, u_2, u_3} (𝕜 := 𝕜) (F := F) 1 0 x

Tactic:
hasFDerivAt_const _ _

Premises used: hasFDerivAt_const
-- Module: Mathlib.Analysis.Calculus.FDeriv.Const
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
F : Type u_3
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : TopologicalSpace F
inst_7 : NatCast F
n : ℕ
x : E
⊢ HasFDerivAt.{u_1, u_2, u_3} (𝕜 := 𝕜) (F := F) (↑n : E → F) 0 x

Tactic:
hasFDerivAt_const _ _

Premises used: hasFDerivAt_const
-- Module: Mathlib.Analysis.Calculus.FDeriv.Const
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
F : Type u_3
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : TopologicalSpace F
inst_7 : IntCast F
z : ℤ
x : E
⊢ HasFDerivAt.{u_1, u_2, u_3} (𝕜 := 𝕜) (F := F) (↑z : E → F) 0 x

Tactic:
hasFDerivAt_const _ _

Premises used: hasFDerivAt_const
-- Module: Mathlib.Analysis.Calculus.FDeriv.Const
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
F : Type u_3
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : TopologicalSpace F
n : ℕ
inst_7 : OfNat F n
x : E
⊢ HasFDerivAt.{u_1, u_2, u_3} (𝕜 := 𝕜) (F := F) (OfNat.ofNat n) 0 x

Tactic:
hasFDerivAt_const _ _

Premises used: hasFDerivAt_const
-- Module: Mathlib.Analysis.Calculus.FDeriv.Const
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
F : Type u_3
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : TopologicalSpace F
x : E
c : F
⊢ DifferentiableAt.{u_1, u_2, u_3} 𝕜 (F := F) (fun (x : E) ↦ c) x

Tactic:
⟨0, hasFDerivAt_const c x⟩

Premises used: DifferentiableAt, hasFDerivAt_const, Exists.intro, OfNat.ofNat
-- Module: Mathlib.Analysis.Calculus.FDeriv.Const
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
F : Type u_3
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : TopologicalSpace F
x : E
⊢ DifferentiableAt.{u_1, u_2, u_3} 𝕜 (F := F) 0 x

Tactic:
differentiableAt_const _

Premises used: differentiableAt_const
-- Module: Mathlib.Analysis.Calculus.FDeriv.Const
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
F : Type u_3
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : TopologicalSpace F
inst_7 : One F
x : E
⊢ DifferentiableAt.{u_1, u_2, u_3} 𝕜 (F := F) 1 x

Tactic:
differentiableAt_const _

Premises used: differentiableAt_const
-- Module: Mathlib.Analysis.Calculus.FDeriv.Const
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
F : Type u_3
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : TopologicalSpace F
inst_7 : NatCast F
n : ℕ
x : E
⊢ DifferentiableAt.{u_1, u_2, u_3} 𝕜 (F := F) (↑n : E → F) x

Tactic:
differentiableAt_const _

Premises used: differentiableAt_const
-- Module: Mathlib.Analysis.Calculus.FDeriv.Const
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
F : Type u_3
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : TopologicalSpace F
inst_7 : IntCast F
z : ℤ
x : E
⊢ DifferentiableAt.{u_1, u_2, u_3} 𝕜 (F := F) (↑z : E → F) x

Tactic:
differentiableAt_const _

Premises used: differentiableAt_const
-- Module: Mathlib.Analysis.Calculus.FDeriv.Const
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
F : Type u_3
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : TopologicalSpace F
n : ℕ
inst_7 : OfNat F n
x : E
⊢ DifferentiableAt.{u_1, u_2, u_3} 𝕜 (F := F) (OfNat.ofNat n) x

Tactic:
differentiableAt_const _

Premises used: differentiableAt_const
-- Module: Mathlib.Analysis.Calculus.FDeriv.Const
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
F : Type u_3
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : TopologicalSpace F
x : E
s : Set E
c : F
⊢ DifferentiableWithinAt.{u_1, u_2, u_3} 𝕜 (F := F) (fun (x : E) ↦ c) s x

Tactic:
DifferentiableAt.differentiableWithinAt (differentiableAt_const _)

Premises used: DifferentiableAt.differentiableWithinAt, differentiableAt_const
-- Module: Mathlib.Analysis.Calculus.FDeriv.Const
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
F : Type u_3
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : TopologicalSpace F
x : E
s : Set E
⊢ DifferentiableWithinAt.{u_1, u_2, u_3} 𝕜 (F := F) 0 s x

Tactic:
differentiableWithinAt_const _

Premises used: differentiableWithinAt_const
-- Module: Mathlib.Analysis.Calculus.FDeriv.Const
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
F : Type u_3
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : TopologicalSpace F
x : E
s : Set E
inst_7 : One F
⊢ DifferentiableWithinAt.{u_1, u_2, u_3} 𝕜 (F := F) 1 s x

Tactic:
differentiableWithinAt_const _

Premises used: differentiableWithinAt_const
-- Module: Mathlib.Analysis.Calculus.FDeriv.Const
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
F : Type u_3
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : TopologicalSpace F
x : E
s : Set E
inst_7 : NatCast F
n : ℕ
⊢ DifferentiableWithinAt.{u_1, u_2, u_3} 𝕜 (F := F) (↑n : E → F) s x

Tactic:
differentiableWithinAt_const _

Premises used: differentiableWithinAt_const
-- Module: Mathlib.Analysis.Calculus.FDeriv.Const
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
F : Type u_3
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : TopologicalSpace F
x : E
s : Set E
inst_7 : IntCast F
z : ℤ
⊢ DifferentiableWithinAt.{u_1, u_2, u_3} 𝕜 (F := F) (↑z : E → F) s x

Tactic:
differentiableWithinAt_const _

Premises used: differentiableWithinAt_const