awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
n : ℕ
inst_7 : OfNat F n
⊢ DifferentiableWithinAt.{u_1, u_2, u_3} 𝕜 (F := F) (OfNat.ofNat n) 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
c : F
hc : HasFDerivWithinAt.{u_1, u_2, u_3} (𝕜 := 𝕜) (F := F) (fun (x : E) ↦ c) 0 s x
⊢ Eq (α := E →L[𝕜] F) (fderivWithin 𝕜 (fun (x : E) ↦ c) s x) 0

Tactic:
rw [fderivWithin, if_pos]

Premises used: if_pos, fderivWithin
-- 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
⊢ HasFDerivWithinAt.{u_1, u_2, u_3} (𝕜 := 𝕜) (F := F) (fun (x : E) ↦ c) 0 s x

Tactic:
apply 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
s : Set E
c : F
h :
  ∀ (x x_1 : E),
    Eq.{u_3 + 1} (α := F) ((fderivWithin 𝕜 (fun (x : E) ↦ c) s x : (a : E) → F) x_1 : F) ((0 x : (a : E) → F) x_1 : F)
⊢ Eq (α := (x : E) → E →L[𝕜] F) (fderivWithin 𝕜 (fun (x : E) ↦ c) s) 0

Tactic:
ext
-- 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
s : Set E
c : F
x x_1 : E
h : Eq.{u_3 + 1} (α := F) ((0 : (a : E) → F) x_1 : F) ((0 x : (a : E) → F) x_1 : F)
h₁ h₂ : Eq.{u_3 + 1} (α := F) ((0 : (a : E) → F) x_1 : F) ((0 : (a : E) → F) x_1 : F)
⊢ Eq.{u_3 + 1} (α := F) ((fderivWithin 𝕜 (fun (x : E) ↦ c) s x : (a : E) → F) x_1 : F) ((0 x : (a : E) → F) x_1 : F)

Tactic:
rw [fderivWithin_const_apply, Pi.zero_apply]

Premises used: Pi.zero_apply, fderivWithin_const_apply
-- 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
s : Set E
c : F
⊢ Eq (α := (x : E) → E →L[𝕜] F) (fderivWithin 𝕜 (const E c) s) 0

Tactic:
fderivWithin_fun_const c

Premises used: fderivWithin_fun_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
s : Set E
⊢ Eq (α := (x : E) → E →L[𝕜] F) (fderivWithin 𝕜 0 s) 0

Tactic:
fderivWithin_const _

Premises used: fderivWithin_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
s : Set E
inst_7 : One F
⊢ Eq (α := (x : E) → E →L[𝕜] F) (fderivWithin 𝕜 1 s) 0

Tactic:
fderivWithin_const _

Premises used: fderivWithin_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
s : Set E
inst_7 : NatCast F
n : ℕ
⊢ Eq (α := (x : E) → E →L[𝕜] F) (fderivWithin 𝕜 (↑n : E → F) s) 0

Tactic:
fderivWithin_const _

Premises used: fderivWithin_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
s : Set E
inst_7 : IntCast F
z : ℤ
⊢ Eq (α := (x : E) → E →L[𝕜] F) (fderivWithin 𝕜 (↑z : E → F) s) 0

Tactic:
fderivWithin_const _

Premises used: fderivWithin_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
s : Set E
n : ℕ
inst_7 : OfNat F n
⊢ Eq (α := (x : E) → E →L[𝕜] F) (fderivWithin 𝕜 (OfNat.ofNat n) s) 0

Tactic:
fderivWithin_const _

Premises used: fderivWithin_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
rw : Eq (α := E →L[𝕜] F) (fderivWithin 𝕜 (fun (x : E) ↦ c) univ x) 0
rw₁ rw₂ : Eq (α := E →L[𝕜] F) 0 0
⊢ Eq (α := E →L[𝕜] F) (fderiv 𝕜 (fun (x : E) ↦ c) x) 0

Tactic:
rw [fderiv, fderivWithin_const_apply]

Premises used: fderiv, fderivWithin_const_apply
-- 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
rw : Eq (α := (x : E) → E →L[𝕜] F) (fderivWithin 𝕜 (fun (x : E) ↦ c) univ) 0
rw₁ rw₂ : Eq (α := (x : E) → E →L[𝕜] F) 0 0
⊢ Eq (α := (x : E) → E →L[𝕜] F) (fderiv 𝕜 fun (x : E) ↦ c) 0

Tactic:
rw [← fderivWithin_univ, fderivWithin_fun_const]

Premises used: fderivWithin_univ, fderivWithin_fun_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
⊢ Eq (α := (x : E) → E →L[𝕜] F) (fderiv 𝕜 (const E c)) 0

Tactic:
fderiv_fun_const c

Premises used: fderiv_fun_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
⊢ Eq (α := (x : E) → E →L[𝕜] F) (fderiv 𝕜 0) 0

Tactic:
fderiv_const _

Premises used: fderiv_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
⊢ Eq (α := (x : E) → E →L[𝕜] F) (fderiv 𝕜 1) 0

Tactic:
fderiv_const _

Premises used: fderiv_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 : ℕ
⊢ Eq (α := (x : E) → E →L[𝕜] F) (fderiv 𝕜 (↑n : E → F)) 0

Tactic:
fderiv_const _

Premises used: fderiv_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 : ℤ
⊢ Eq (α := (x : E) → E →L[𝕜] F) (fderiv 𝕜 (↑z : E → F)) 0

Tactic:
fderiv_const _

Premises used: fderiv_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
⊢ Eq (α := (x : E) → E →L[𝕜] F) (fderiv 𝕜 (OfNat.ofNat n)) 0

Tactic:
fderiv_const _

Premises used: fderiv_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
⊢ Differentiable.{u_1, u_2, u_3} 𝕜 (F := F) fun (x : E) ↦ c

Tactic:
fun _ =>
  differentiableAt_const _

Premises used: Differentiable, 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
⊢ Differentiable.{u_1, u_2, u_3} 𝕜 (E := E) (F := F) 0

Tactic:
differentiable_const _

Premises used: differentiable_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
⊢ Differentiable.{u_1, u_2, u_3} 𝕜 (E := E) (F := F) 1

Tactic:
differentiable_const _

Premises used: differentiable_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 : ℕ
⊢ Differentiable.{u_1, u_2, u_3} 𝕜 (E := E) (F := F) (↑n : E → F)

Tactic:
differentiable_const _

Premises used: differentiable_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 : ℤ
⊢ Differentiable.{u_1, u_2, u_3} 𝕜 (E := E) (F := F) (↑z : E → F)

Tactic:
differentiable_const _

Premises used: differentiable_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
⊢ Differentiable.{u_1, u_2, u_3} 𝕜 (E := E) (F := F) (OfNat.ofNat n)

Tactic:
differentiable_const _

Premises used: differentiable_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
s : Set E
c : F
⊢ DifferentiableOn.{u_1, u_2, u_3} 𝕜 (F := F) (fun (x : E) ↦ c) s

Tactic:
(differentiable_const _).differentiableOn

Premises used: differentiable_const, Differentiable.differentiableOn
-- 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
s : Set E
⊢ DifferentiableOn.{u_1, u_2, u_3} 𝕜 (F := F) 0 s

Tactic:
differentiableOn_const _

Premises used: differentiableOn_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
s : Set E
inst_7 : One F
⊢ DifferentiableOn.{u_1, u_2, u_3} 𝕜 (F := F) 1 s

Tactic:
differentiableOn_const _

Premises used: differentiableOn_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
s : Set E
inst_7 : NatCast F
n : ℕ
⊢ DifferentiableOn.{u_1, u_2, u_3} 𝕜 (F := F) (↑n : E → F) s

Tactic:
differentiableOn_const _

Premises used: differentiableOn_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
s : Set E
inst_7 : IntCast F
z : ℤ
⊢ DifferentiableOn.{u_1, u_2, u_3} 𝕜 (F := F) (↑z : E → F) s

Tactic:
differentiableOn_const _

Premises used: differentiableOn_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
s : Set E
n : ℕ
inst_7 : OfNat F n
⊢ DifferentiableOn.{u_1, u_2, u_3} 𝕜 (F := F) (OfNat.ofNat n) s

Tactic:
differentiableOn_const _

Premises used: differentiableOn_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
f : E → F
x : E
⊢ HasFDerivWithinAt.{u_1, u_2, u_3} (𝕜 := 𝕜) f 0 {x} x

Tactic:
.of_not_accPt ?_

Premises used: HasFDerivWithinAt.of_not_accPt
-- 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
f : E → F
x : E
refine : ¬AccPt x (𝓟 {x})
⊢ HasFDerivWithinAt.{u_1, u_2, u_3} (𝕜 := 𝕜) f 0 {x} x

Tactic:
refine .of_not_accPt ?_
-- 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
f : E → F
x : E
rw : ¬ClusterPt x (𝓟 ({x}ᶜ ∩ {x}))
⊢ ¬AccPt x (𝓟 {x})

Tactic:
rw [accPt_iff_clusterPt, inf_principal]

Premises used: Filter.inf_principal, accPt_iff_clusterPt
-- 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
f : E → F
x : E
⊢ ¬ClusterPt x (𝓟 ({x}ᶜ ∩ {x}))

Tactic:
simp [ClusterPt]

Premises used: ClusterPt
-- 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
h : Subsingleton E
f : E → F
s : Set E
x : E
inl : HasFDerivWithinAt.{u_1, u_2, u_3} (𝕜 := 𝕜) f 0 ∅ x
inr : ∀ (a : E), HasFDerivWithinAt.{u_1, u_2, u_3} (𝕜 := 𝕜) f 0 {a} x
⊢ HasFDerivWithinAt.{u_1, u_2, u_3} (𝕜 := 𝕜) f 0 s x

Tactic:
obtain rfl | ⟨a, rfl⟩ := s.eq_empty_or_singleton_of_subsingleton

Premises used: Set.eq_empty_or_singleton_of_subsingleton, rfl
-- 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
h : Subsingleton E
f : E → F
x : E
⊢ HasFDerivWithinAt.{u_1, u_2, u_3} (𝕜 := 𝕜) f 0 ∅ x

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
h : Subsingleton E
f : E → F
x a : E
⊢ HasFDerivWithinAt.{u_1, u_2, u_3} (𝕜 := 𝕜) f 0 {a} x

Tactic:
HasFDerivWithinAt.singleton

Premises used: HasFDerivWithinAt.singleton
-- 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
h : Subsingleton E
f : E → F
x a : E
⊢ HasFDerivWithinAt.{u_1, u_2, u_3} (𝕜 := 𝕜) f 0 {a} x

Tactic:
exact HasFDerivWithinAt.singleton

Premises used: HasFDerivWithinAt.singleton
-- 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
h : Subsingleton E
f : E → F
x : E
rw : HasFDerivWithinAt.{u_1, u_2, u_3} (𝕜 := 𝕜) f 0 {x} x
⊢ HasFDerivAt.{u_1, u_2, u_3} (𝕜 := 𝕜) f 0 x

Tactic:
rw [← hasFDerivWithinAt_univ, subsingleton_univ.eq_singleton_of_mem (mem_univ x)]

Premises used: Set.subsingleton_univ, Set.Subsingleton.eq_singleton_of_mem, Set.mem_univ, hasFDerivWithinAt_univ
-- 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
h : Subsingleton E
f : E → F
x : E
⊢ HasFDerivWithinAt.{u_1, u_2, u_3} (𝕜 := 𝕜) f 0 {x} x

Tactic:
hasFDerivWithinAt_singleton f x

Premises used: hasFDerivWithinAt_singleton
-- 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
h : Subsingleton E
f : E → F
x : E
⊢ HasFDerivWithinAt.{u_1, u_2, u_3} (𝕜 := 𝕜) f 0 {x} x

Tactic:
exact hasFDerivWithinAt_singleton f x

Premises used: hasFDerivWithinAt_singleton
-- 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 : Subsingleton E
f : E → F
⊢ Differentiable 𝕜 f

Tactic:
fun x ↦ (hasFDerivAt_of_subsingleton f x (𝕜 := 𝕜)).differentiableAt

Premises used: Differentiable, hasFDerivAt_of_subsingleton, HasFDerivAt.differentiableAt
-- 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
f : E → F
x : E
s : Set E
inst_7 : Subsingleton E
⊢ DifferentiableWithinAt 𝕜 f s x

Tactic:
(differentiable_of_subsingleton x).differentiableWithinAt

Premises used: DifferentiableAt.differentiableWithinAt, differentiable_of_subsingleton
-- 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
f : E → F
x : E
⊢ DifferentiableOn 𝕜 f {x}

Tactic:
forall_eq.2 (hasFDerivWithinAt_singleton f x).differentiableWithinAt

Premises used: Iff.mpr, Set.Mem, setOf, forall_eq, hasFDerivWithinAt_singleton, HasFDerivWithinAt.differentiableWithinAt, DifferentiableOn, Set.singleton
-- 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
f : E → F
s : Set E
hs : s.Subsingleton
⊢ DifferentiableOn 𝕜 f s

Tactic:
hs.induction_on differentiableOn_empty fun _ => differentiableOn_singleton

Premises used: differentiableOn_singleton, Set.Subsingleton.induction_on, differentiableOn_empty
-- 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
f : E → F
x : E
c : F
hf : f =ᶠ[𝓝 x] fun (x : E) ↦ c
⊢ HasFDerivAt.{u_1, u_2, u_3} (𝕜 := 𝕜) f 0 x

Tactic:
(hasFDerivAt_const _ _).congr_of_eventuallyEq hf

Premises used: HasFDerivAt.congr_of_eventuallyEq, 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
f : E → F
x : E
s : Set E
hf : Injective.{u_2 + 1, u_3 + 1} (α := E) (β := F) (⇑(fderivWithin 𝕜 f s x) : (a : E) → F)
⊢ Nontrivial E

Tactic:
nontriviality E
-- 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
f : E → F
x : E
s : Set E
hf : Injective.{u_2 + 1, u_3 + 1} (α := E) (β := F) (⇑(fderivWithin 𝕜 f s x) : (a : E) → F)
h : Nontrivial E
contrapose :
  ∀ (hf : ¬DifferentiableWithinAt 𝕜 f s x),
    ¬Injective.{u_2 + 1, u_3 + 1} (α := E) (β := F) (⇑(fderivWithin 𝕜 f s x) : (a : E) → F)
⊢ DifferentiableWithinAt 𝕜 f s x

Tactic:
contrapose hf
-- 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
f : E → F
x : E
s : Set E
h : Nontrivial E
hf : ¬DifferentiableWithinAt 𝕜 f s x
rw : ¬Injective.{u_2 + 1, u_3 + 1} (α := E) (β := F) (⇑0 : (a : E) → F)
⊢ ¬Injective.{u_2 + 1, u_3 + 1} (α := E) (β := F) (⇑(fderivWithin 𝕜 f s x) : (a : E) → F)

Tactic:
rw [fderivWithin_zero_of_not_differentiableWithinAt hf]

Premises used: fderivWithin_zero_of_not_differentiableWithinAt
-- 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
f : E → F
x : E
s : Set E
h : Nontrivial E
hf : ¬DifferentiableWithinAt 𝕜 f s x
⊢ ¬Injective.{u_2 + 1, u_3 + 1} (α := E) (β := F) (⇑0 : (a : E) → F)

Tactic:
not_injective_const

Premises used: Function.not_injective_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
f : E → F
x : E
s : Set E
h : Nontrivial E
hf : ¬DifferentiableWithinAt 𝕜 f s x
⊢ ¬Injective.{u_2 + 1, u_3 + 1} (α := E) (β := F) (⇑0 : (a : E) → F)

Tactic:
exact not_injective_const

Premises used: Function.not_injective_const