awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Calculus.Deriv.Pow
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
s : Set 𝕜
n : ℕ
x : 𝕜
⊢ HasDerivWithinAt (fun (x : 𝕜) ↦ x ^ n) ((↑n : 𝕜) * x ^ (n - 1)) s x

Tactic:
simpa using (hasDerivWithinAt_id x s).pow n

Premises used: HasDerivWithinAt.pow, hasDerivWithinAt_id
-- Module: Mathlib.Analysis.Calculus.Deriv.Pow
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
n : ℕ
x : 𝕜
⊢ HasDerivAt (fun (x : 𝕜) ↦ x ^ n) ((↑n : 𝕜) * x ^ (n - 1)) x

Tactic:
simpa using (hasStrictDerivAt_pow n x).hasDerivAt

Premises used: HasStrictDerivAt.hasDerivAt, hasStrictDerivAt_pow
-- Module: Mathlib.Analysis.Calculus.Deriv.Pow
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
h : UniqueDiffWithinAt 𝕜 s x
n : ℕ
rw : (↑n : 𝕜) * x ^ (n - 1) * derivWithin (fun (x : 𝕜) ↦ x) s x = (↑n : 𝕜) * x ^ (n - 1)
rw₁ : (↑n : 𝕜) * x ^ (n - 1) * 1 = (↑n : 𝕜) * x ^ (n - 1)
rw₂ rw₃ : (↑n : 𝕜) * x ^ (n - 1) = (↑n : 𝕜) * x ^ (n - 1)
⊢ derivWithin (fun (x : 𝕜) ↦ x ^ n) s x = (↑n : 𝕜) * x ^ (n - 1)

Tactic:
rw [derivWithin_fun_pow (differentiableWithinAt_fun_id) n, derivWithin_id' _ _ h, mul_one]

Premises used: derivWithin_id', derivWithin_fun_pow, mul_one
-- Module: Mathlib.Analysis.Calculus.Deriv.Pow
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
x : 𝕜
n : ℕ
⊢ deriv (fun (x : 𝕜) ↦ x ^ n) x = (↑n : 𝕜) * x ^ (n - 1)

Tactic:
simp
-- Module: Mathlib.Analysis.Calculus.Deriv.Prod
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f₁ : 𝕜 → F
f₁' : F
L : Filter (𝕜 × 𝕜)
G : Type w
inst_3 : NormedAddCommGroup G
inst_4 : NormedSpace 𝕜 G
f₂ : 𝕜 → G
f₂' : G
hf₁ : HasDerivAtFilter f₁ f₁' L
hf₂ : HasDerivAtFilter f₂ f₂' L
⊢ HasDerivAtFilter (fun (x : 𝕜) ↦ (f₁ x, f₂ x)) (f₁', f₂') L

Tactic:
HasFDerivAtFilter.prodMk hf₁ hf₂

Premises used: HasFDerivAtFilter.prodMk, HasDerivAtFilter, ContinuousLinearMap.toSpanSingleton, Function.prod, ContinuousLinearMap.prod, LinearMap.prod, LinearMap.smulRight, LinearMap.toSpanSingleton
-- Module: Mathlib.Analysis.Calculus.Deriv.Prod
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f₁ : 𝕜 → F
f₁' : F
x : 𝕜
s : Set 𝕜
G : Type w
inst_3 : NormedAddCommGroup G
inst_4 : NormedSpace 𝕜 G
f₂ : 𝕜 → G
f₂' : G
hf₁ : HasDerivWithinAt f₁ f₁' s x
hf₂ : HasDerivWithinAt f₂ f₂' s x
⊢ HasDerivWithinAt (fun (x : 𝕜) ↦ (f₁ x, f₂ x)) (f₁', f₂') s x

Tactic:
HasDerivAtFilter.prodMk hf₁ hf₂

Premises used: HasDerivWithinAt, HasDerivAtFilter.prodMk
-- Module: Mathlib.Analysis.Calculus.Deriv.Prod
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f₁ : 𝕜 → F
f₁' : F
x : 𝕜
G : Type w
inst_3 : NormedAddCommGroup G
inst_4 : NormedSpace 𝕜 G
f₂ : 𝕜 → G
f₂' : G
hf₁ : HasDerivAt f₁ f₁' x
hf₂ : HasDerivAt f₂ f₂' x
⊢ HasDerivAt (fun (x : 𝕜) ↦ (f₁ x, f₂ x)) (f₁', f₂') x

Tactic:
HasDerivAtFilter.prodMk hf₁ hf₂

Premises used: HasDerivAt, HasDerivAtFilter.prodMk
-- Module: Mathlib.Analysis.Calculus.Deriv.Prod
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f₁ : 𝕜 → F
f₁' : F
x : 𝕜
G : Type w
inst_3 : NormedAddCommGroup G
inst_4 : NormedSpace 𝕜 G
f₂ : 𝕜 → G
f₂' : G
hf₁ : HasStrictDerivAt f₁ f₁' x
hf₂ : HasStrictDerivAt f₂ f₂' x
⊢ HasStrictDerivAt (fun (x : 𝕜) ↦ (f₁ x, f₂ x)) (f₁', f₂') x

Tactic:
HasDerivAtFilter.prodMk hf₁ hf₂

Premises used: HasDerivAtFilter.prodMk, HasStrictDerivAt
-- Module: Mathlib.Analysis.Calculus.Deriv.Prod
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
L : Filter (𝕜 × 𝕜)
ι : Type u_1
E' : ι → Type u_2
inst_1 : (i : ι) → NormedAddCommGroup (E' i)
inst_2 : (i : ι) → NormedSpace.{u, u_2} 𝕜 (E' i)
φ : 𝕜 → (i : ι) → E' i
φ' : (i : ι) → E' i
⊢ HasDerivAtFilter φ φ' L ↔ ∀ (i : ι), HasDerivAtFilter (fun (x : 𝕜) ↦ φ x i) (φ' i) L

Tactic:
hasFDerivAtFilter_pi'

Premises used: ContinuousLinearMap.comp, HasDerivAtFilter, ContinuousLinearMap.toSpanSingleton, LinearMap.smulRight, LinearMap.toSpanSingleton, hasFDerivAtFilter_pi'
-- Module: Mathlib.Analysis.Calculus.Deriv.Prod
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
ι : Type u_1
E' : ι → Type u_2
inst_1 : (i : ι) → NormedAddCommGroup (E' i)
inst_2 : (i : ι) → NormedSpace.{u, u_2} 𝕜 (E' i)
φ : 𝕜 → (i : ι) → E' i
φ' : (i : ι) → E' i
⊢ HasStrictDerivAt φ φ' x ↔ ∀ (i : ι), HasStrictDerivAt (fun (x : 𝕜) ↦ φ x i) (φ' i) x

Tactic:
hasDerivAtFilter_pi

Premises used: hasDerivAtFilter_pi, HasStrictDerivAt
-- Module: Mathlib.Analysis.Calculus.Deriv.Prod
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
ι : Type u_1
E' : ι → Type u_2
inst_1 : (i : ι) → NormedAddCommGroup (E' i)
inst_2 : (i : ι) → NormedSpace.{u, u_2} 𝕜 (E' i)
φ : 𝕜 → (i : ι) → E' i
φ' : (i : ι) → E' i
⊢ HasDerivAt φ φ' x ↔ ∀ (i : ι), HasDerivAt (fun (x : 𝕜) ↦ φ x i) (φ' i) x

Tactic:
hasDerivAtFilter_pi

Premises used: HasDerivAt, hasDerivAtFilter_pi
-- Module: Mathlib.Analysis.Calculus.Deriv.Prod
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
ι : Type u_1
E' : ι → Type u_2
inst_1 : (i : ι) → NormedAddCommGroup (E' i)
inst_2 : (i : ι) → NormedSpace.{u, u_2} 𝕜 (E' i)
φ : 𝕜 → (i : ι) → E' i
φ' : (i : ι) → E' i
⊢ HasDerivWithinAt φ φ' s x ↔ ∀ (i : ι), HasDerivWithinAt (fun (x : 𝕜) ↦ φ x i) (φ' i) s x

Tactic:
hasDerivAtFilter_pi

Premises used: HasDerivWithinAt, hasDerivAtFilter_pi
-- Module: Mathlib.Analysis.Calculus.Deriv.Prod
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
ι : Type u_1
E' : ι → Type u_2
inst_1 : (i : ι) → NormedAddCommGroup (E' i)
inst_2 : (i : ι) → NormedSpace.{u, u_2} 𝕜 (E' i)
φ : 𝕜 → (i : ι) → E' i
h : ∀ (i : ι), DifferentiableWithinAt.{u, u, u_2} 𝕜 (F := E' i) (fun (x : 𝕜) ↦ φ x i) s x
pos : ∀ (hsx : UniqueDiffWithinAt 𝕜 s x), derivWithin φ s x = fun (i : ι) ↦ derivWithin (fun (x : 𝕜) ↦ φ x i) s x
neg : ∀ (hsx : ¬UniqueDiffWithinAt 𝕜 s x), derivWithin φ s x = fun (i : ι) ↦ derivWithin (fun (x : 𝕜) ↦ φ x i) s x
⊢ derivWithin φ s x = fun (i : ι) ↦ derivWithin (fun (x : 𝕜) ↦ φ x i) s x

Tactic:
by_cases hsx : UniqueDiffWithinAt 𝕜 s x

Premises used: UniqueDiffWithinAt
-- Module: Mathlib.Analysis.Calculus.Deriv.Prod
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
ι : Type u_1
E' : ι → Type u_2
inst_1 : (i : ι) → NormedAddCommGroup (E' i)
inst_2 : (i : ι) → NormedSpace.{u, u_2} 𝕜 (E' i)
φ : 𝕜 → (i : ι) → E' i
h : ∀ (i : ι), DifferentiableWithinAt.{u, u, u_2} 𝕜 (F := E' i) (fun (x : 𝕜) ↦ φ x i) s x
hsx : UniqueDiffWithinAt 𝕜 s x
pos :
  Eq (α := (i : ι) → E' i)
    (((ContinuousLinearMap.pi (φ := E') fun (i : ι) ↦ fderivWithin 𝕜 (fun (x : 𝕜) ↦ φ x i) s x :
            𝕜 →L[𝕜] (i : ι) → E' i) :
          (a : 𝕜) → (i : ι) → E' i)
        1 :
      (i : ι) → E' i)
    fun (i : ι) ↦ (derivWithin (fun (x : 𝕜) ↦ φ x i) s x : E' i)
⊢ derivWithin φ s x = fun (i : ι) ↦ derivWithin (fun (x : 𝕜) ↦ φ x i) s x

Tactic:
rw [derivWithin, fderivWithin_pi h hsx]

Premises used: fderivWithin_pi, derivWithin
-- Module: Mathlib.Analysis.Calculus.Deriv.Prod
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
ι : Type u_1
E' : ι → Type u_2
inst_1 : (i : ι) → NormedAddCommGroup (E' i)
inst_2 : (i : ι) → NormedSpace.{u, u_2} 𝕜 (E' i)
φ : 𝕜 → (i : ι) → E' i
h : ∀ (i : ι), DifferentiableWithinAt.{u, u, u_2} 𝕜 (F := E' i) (fun (x : 𝕜) ↦ φ x i) s x
hsx : UniqueDiffWithinAt 𝕜 s x
⊢ Eq (α := (i : ι) → E' i)
    (((ContinuousLinearMap.pi (φ := E') fun (i : ι) ↦ fderivWithin 𝕜 (fun (x : 𝕜) ↦ φ x i) s x :
            𝕜 →L[𝕜] (i : ι) → E' i) :
          (a : 𝕜) → (i : ι) → E' i)
        1 :
      (i : ι) → E' i)
    fun (i : ι) ↦ (derivWithin (fun (x : 𝕜) ↦ φ x i) s x : E' i)

Tactic:
simp [derivWithin]

Premises used: derivWithin
-- Module: Mathlib.Analysis.Calculus.Deriv.Prod
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
ι : Type u_1
E' : ι → Type u_2
inst_1 : (i : ι) → NormedAddCommGroup (E' i)
inst_2 : (i : ι) → NormedSpace.{u, u_2} 𝕜 (E' i)
φ : 𝕜 → (i : ι) → E' i
h : ∀ (i : ι), DifferentiableWithinAt.{u, u, u_2} 𝕜 (F := E' i) (fun (x : 𝕜) ↦ φ x i) s x
hsx : ¬UniqueDiffWithinAt 𝕜 s x
⊢ ¬AccPt x (𝓟 s)

Tactic:
rw [uniqueDiffWithinAt_iff_accPt] at hsx

Premises used: uniqueDiffWithinAt_iff_accPt
-- Module: Mathlib.Analysis.Calculus.Deriv.Prod
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
ι : Type u_1
E' : ι → Type u_2
inst_1 : (i : ι) → NormedAddCommGroup (E' i)
inst_2 : (i : ι) → NormedSpace.{u, u_2} 𝕜 (E' i)
φ : 𝕜 → (i : ι) → E' i
h : ∀ (i : ι), DifferentiableWithinAt.{u, u, u_2} 𝕜 (F := E' i) (fun (x : 𝕜) ↦ φ x i) s x
hsx : ¬AccPt x (𝓟 s)
⊢ derivWithin φ s x = fun (i : ι) ↦ derivWithin (fun (x : 𝕜) ↦ φ x i) s x

Tactic:
simp [derivWithin, fderivWithin_zero_of_not_accPt hsx, Pi.zero_def]

Premises used: fderivWithin_zero_of_not_accPt, Pi.zero_def, derivWithin
-- Module: Mathlib.Analysis.Calculus.Deriv.Prod
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
ι : Type u_1
E' : ι → Type u_2
inst_1 : (i : ι) → NormedAddCommGroup (E' i)
inst_2 : (i : ι) → NormedSpace.{u, u_2} 𝕜 (E' i)
φ : 𝕜 → (i : ι) → E' i
h : ∀ (i : ι), DifferentiableAt.{u, u, u_2} 𝕜 (F := E' i) (fun (x : 𝕜) ↦ φ x i) x
simp :
  Eq (α := (i : ι) → E' i)
    (((ContinuousLinearMap.pi (φ := E') fun (i : ι) ↦ fderiv 𝕜 (fun (x : 𝕜) ↦ φ x i) x : 𝕜 →L[𝕜] (i : ι) → E' i) :
          (a : 𝕜) → (i : ι) → E' i)
        1 :
      (i : ι) → E' i)
    fun (i : ι) ↦
    (((fderiv.{u, u, u_2} 𝕜 (F := E' i) (fun (x : 𝕜) ↦ φ x i) x :
            ContinuousLinearMap.{u, u, u, u_2} (RingHom.id 𝕜) 𝕜 (E' i)) :
          (a : 𝕜) → E' i)
        1 :
      E' i)
⊢ deriv φ x = fun (i : ι) ↦ deriv (fun (x : 𝕜) ↦ φ x i) x

Tactic:
simp only [deriv, fderiv_pi h]

Premises used: deriv, fderiv_pi
-- Module: Mathlib.Analysis.Calculus.Deriv.Prod
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
ι : Type u_1
E' : ι → Type u_2
inst_1 : (i : ι) → NormedAddCommGroup (E' i)
inst_2 : (i : ι) → NormedSpace.{u, u_2} 𝕜 (E' i)
φ : 𝕜 → (i : ι) → E' i
h : ∀ (i : ι), DifferentiableAt.{u, u, u_2} 𝕜 (F := E' i) (fun (x : 𝕜) ↦ φ x i) x
⊢ Eq (α := (i : ι) → E' i)
    (((ContinuousLinearMap.pi (φ := E') fun (i : ι) ↦ fderiv 𝕜 (fun (x : 𝕜) ↦ φ x i) x : 𝕜 →L[𝕜] (i : ι) → E' i) :
          (a : 𝕜) → (i : ι) → E' i)
        1 :
      (i : ι) → E' i)
    fun (i : ι) ↦
    (((fderiv.{u, u, u_2} 𝕜 (F := E' i) (fun (x : 𝕜) ↦ φ x i) x :
            ContinuousLinearMap.{u, u, u, u_2} (RingHom.id 𝕜) 𝕜 (E' i)) :
          (a : 𝕜) → E' i)
        1 :
      E' i)

Tactic:
simp
-- Module: Mathlib.Analysis.Calculus.Deriv.Prod
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
n : ℕ
F' : Fin n.succ → Type u_1
inst_1 : (i : Fin n.succ) → NormedAddCommGroup (F' i)
inst_2 : (i : Fin n.succ) → NormedSpace.{u, u_1} 𝕜 (F' i)
φ : 𝕜 → F' 0
φs : 𝕜 → (i : Fin n) → F' i.succ
φ' : (i : Fin n.succ) → F' i
⊢ HasStrictDerivAt (fun (x : 𝕜) ↦ Fin.cons (α := F') (φ x) (φs x)) φ' x ↔
    HasStrictDerivAt φ (φ' 0) x ∧ HasStrictDerivAt φs (fun (i : Fin n) ↦ φ' i.succ) x

Tactic:
hasStrictFDerivAt_finCons

Premises used: ContinuousLinearMap.comp, hasStrictFDerivAt_finCons, HasDerivAtFilter, ContinuousLinearMap.toSpanSingleton, LinearMap.smulRight, HasStrictDerivAt, LinearMap.toSpanSingleton
-- Module: Mathlib.Analysis.Calculus.Deriv.Prod
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
n : ℕ
F' : Fin n.succ → Type u_1
inst_1 : (i : Fin n.succ) → NormedAddCommGroup (F' i)
inst_2 : (i : Fin n.succ) → NormedSpace.{u, u_1} 𝕜 (F' i)
φ : 𝕜 → F' 0
φs : 𝕜 → (i : Fin n) → F' i.succ
φ' : F' 0
φs' : (i : Fin n) → F' i.succ
⊢ HasStrictDerivAt (fun (x : 𝕜) ↦ Fin.cons (α := F') (φ x) (φs x)) (Fin.cons (α := F') φ' φs') x ↔
    HasStrictDerivAt φ φ' x ∧ HasStrictDerivAt φs φs' x

Tactic:
hasStrictDerivAt_finCons

Premises used: Eq.mpr, Fin.cons, Fin.induction.go, Fin.ofNat, hasStrictDerivAt_finCons, Fin.induction, Nat.mod, Fin.cases
-- Module: Mathlib.Analysis.Calculus.Deriv.Prod
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
n : ℕ
F' : Fin n.succ → Type u_1
inst_1 : (i : Fin n.succ) → NormedAddCommGroup (F' i)
inst_2 : (i : Fin n.succ) → NormedSpace.{u, u_1} 𝕜 (F' i)
φ : 𝕜 → F' 0
φs : 𝕜 → (i : Fin n) → F' i.succ
φ' : F' 0
φs' : (i : Fin n) → F' i.succ
h : HasStrictDerivAt φ φ' x
hs : HasStrictDerivAt φs φs' x
⊢ HasStrictDerivAt (fun (x : 𝕜) ↦ Fin.cons (α := F') (φ x) (φs x)) (Fin.cons (α := F') φ' φs') x

Tactic:
hasStrictDerivAt_finCons'.mpr ⟨h, hs⟩

Premises used: Iff.mpr, hasStrictDerivAt_finCons', And.intro
-- Module: Mathlib.Analysis.Calculus.Deriv.Prod
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
n : ℕ
F' : Fin n.succ → Type u_1
inst_1 : (i : Fin n.succ) → NormedAddCommGroup (F' i)
inst_2 : (i : Fin n.succ) → NormedSpace.{u, u_1} 𝕜 (F' i)
φ : 𝕜 → F' 0
φs : 𝕜 → (i : Fin n) → F' i.succ
φ' : (i : Fin n.succ) → F' i
l : Filter (𝕜 × 𝕜)
⊢ HasDerivAtFilter (fun (x : 𝕜) ↦ Fin.cons (α := F') (φ x) (φs x)) φ' l ↔
    HasDerivAtFilter φ (φ' 0) l ∧ HasDerivAtFilter φs (fun (i : Fin n) ↦ φ' i.succ) l

Tactic:
hasFDerivAtFilter_finCons

Premises used: ContinuousLinearMap.comp, HasDerivAtFilter, ContinuousLinearMap.toSpanSingleton, hasFDerivAtFilter_finCons, LinearMap.smulRight, LinearMap.toSpanSingleton
-- Module: Mathlib.Analysis.Calculus.Deriv.Prod
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
n : ℕ
F' : Fin n.succ → Type u_1
inst_1 : (i : Fin n.succ) → NormedAddCommGroup (F' i)
inst_2 : (i : Fin n.succ) → NormedSpace.{u, u_1} 𝕜 (F' i)
φ : 𝕜 → F' 0
φs : 𝕜 → (i : Fin n) → F' i.succ
φ' : F' 0
φs' : (i : Fin n) → F' i.succ
l : Filter (𝕜 × 𝕜)
⊢ HasDerivAtFilter (fun (x : 𝕜) ↦ Fin.cons (α := F') (φ x) (φs x)) (Fin.cons (α := F') φ' φs') l ↔
    HasDerivAtFilter φ φ' l ∧ HasDerivAtFilter φs φs' l

Tactic:
hasDerivAtFilter_finCons

Premises used: Eq.mpr, Fin.cons, Fin.induction.go, Fin.ofNat, Fin.induction, hasDerivAtFilter_finCons, Nat.mod, Fin.cases
-- Module: Mathlib.Analysis.Calculus.Deriv.Prod
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
n : ℕ
F' : Fin n.succ → Type u_1
inst_1 : (i : Fin n.succ) → NormedAddCommGroup (F' i)
inst_2 : (i : Fin n.succ) → NormedSpace.{u, u_1} 𝕜 (F' i)
φ : 𝕜 → F' 0
φs : 𝕜 → (i : Fin n) → F' i.succ
φ' : F' 0
φs' : (i : Fin n) → F' i.succ
l : Filter (𝕜 × 𝕜)
h : HasDerivAtFilter φ φ' l
hs : HasDerivAtFilter φs φs' l
⊢ HasDerivAtFilter (fun (x : 𝕜) ↦ Fin.cons (α := F') (φ x) (φs x)) (Fin.cons (α := F') φ' φs') l

Tactic:
hasDerivAtFilter_finCons'.mpr ⟨h, hs⟩

Premises used: Iff.mpr, hasDerivAtFilter_finCons', And.intro
-- Module: Mathlib.Analysis.Calculus.Deriv.Prod
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
n : ℕ
F' : Fin n.succ → Type u_1
inst_1 : (i : Fin n.succ) → NormedAddCommGroup (F' i)
inst_2 : (i : Fin n.succ) → NormedSpace.{u, u_1} 𝕜 (F' i)
φ : 𝕜 → F' 0
φs : 𝕜 → (i : Fin n) → F' i.succ
φ' : (i : Fin n.succ) → F' i
⊢ HasDerivAt (fun (x : 𝕜) ↦ Fin.cons (α := F') (φ x) (φs x)) φ' x ↔
    HasDerivAt φ (φ' 0) x ∧ HasDerivAt φs (fun (i : Fin n) ↦ φ' i.succ) x

Tactic:
hasDerivAtFilter_finCons

Premises used: HasDerivAt, hasDerivAtFilter_finCons
-- Module: Mathlib.Analysis.Calculus.Deriv.Prod
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
n : ℕ
F' : Fin n.succ → Type u_1
inst_1 : (i : Fin n.succ) → NormedAddCommGroup (F' i)
inst_2 : (i : Fin n.succ) → NormedSpace.{u, u_1} 𝕜 (F' i)
φ : 𝕜 → F' 0
φs : 𝕜 → (i : Fin n) → F' i.succ
φ' : F' 0
φs' : (i : Fin n) → F' i.succ
⊢ HasDerivAt (fun (x : 𝕜) ↦ Fin.cons (α := F') (φ x) (φs x)) (Fin.cons (α := F') φ' φs') x ↔
    HasDerivAt φ φ' x ∧ HasDerivAt φs φs' x

Tactic:
hasDerivAt_finCons

Premises used: Eq.mpr, Fin.cons, Fin.induction.go, Fin.ofNat, Fin.induction, Nat.mod, Fin.cases, hasDerivAt_finCons
-- Module: Mathlib.Analysis.Calculus.Deriv.Prod
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
n : ℕ
F' : Fin n.succ → Type u_1
inst_1 : (i : Fin n.succ) → NormedAddCommGroup (F' i)
inst_2 : (i : Fin n.succ) → NormedSpace.{u, u_1} 𝕜 (F' i)
φ : 𝕜 → F' 0
φs : 𝕜 → (i : Fin n) → F' i.succ
φ' : F' 0
φs' : (i : Fin n) → F' i.succ
h : HasDerivAt φ φ' x
hs : HasDerivAt φs φs' x
⊢ HasDerivAt (fun (x : 𝕜) ↦ Fin.cons (α := F') (φ x) (φs x)) (Fin.cons (α := F') φ' φs') x

Tactic:
hasDerivAt_finCons'.mpr ⟨h, hs⟩

Premises used: Iff.mpr, And.intro, hasDerivAt_finCons'
-- Module: Mathlib.Analysis.Calculus.Deriv.Prod
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
n : ℕ
F' : Fin n.succ → Type u_1
inst_1 : (i : Fin n.succ) → NormedAddCommGroup (F' i)
inst_2 : (i : Fin n.succ) → NormedSpace.{u, u_1} 𝕜 (F' i)
φ : 𝕜 → F' 0
φs : 𝕜 → (i : Fin n) → F' i.succ
φ' : (i : Fin n.succ) → F' i
⊢ HasDerivWithinAt (fun (x : 𝕜) ↦ Fin.cons (α := F') (φ x) (φs x)) φ' s x ↔
    HasDerivWithinAt φ (φ' 0) s x ∧ HasDerivWithinAt φs (fun (i : Fin n) ↦ φ' i.succ) s x

Tactic:
hasDerivAtFilter_finCons

Premises used: HasDerivWithinAt, hasDerivAtFilter_finCons
-- Module: Mathlib.Analysis.Calculus.Deriv.Prod
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
n : ℕ
F' : Fin n.succ → Type u_1
inst_1 : (i : Fin n.succ) → NormedAddCommGroup (F' i)
inst_2 : (i : Fin n.succ) → NormedSpace.{u, u_1} 𝕜 (F' i)
φ : 𝕜 → F' 0
φs : 𝕜 → (i : Fin n) → F' i.succ
φ' : F' 0
φs' : (i : Fin n) → F' i.succ
⊢ HasDerivWithinAt (fun (x : 𝕜) ↦ Fin.cons (α := F') (φ x) (φs x)) (Fin.cons (α := F') φ' φs') s x ↔
    HasDerivWithinAt φ φ' s x ∧ HasDerivWithinAt φs φs' s x

Tactic:
hasDerivAtFilter_finCons

Premises used: Eq.mpr, Fin.cons, HasDerivWithinAt, Fin.induction.go, Fin.ofNat, Fin.induction, hasDerivAtFilter_finCons, Nat.mod, Fin.cases
-- Module: Mathlib.Analysis.Calculus.Deriv.Prod
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
n : ℕ
F' : Fin n.succ → Type u_1
inst_1 : (i : Fin n.succ) → NormedAddCommGroup (F' i)
inst_2 : (i : Fin n.succ) → NormedSpace.{u, u_1} 𝕜 (F' i)
φ : 𝕜 → F' 0
φs : 𝕜 → (i : Fin n) → F' i.succ
φ' : F' 0
φs' : (i : Fin n) → F' i.succ
h : HasDerivWithinAt φ φ' s x
hs : HasDerivWithinAt φs φs' s x
⊢ HasDerivWithinAt (fun (x : 𝕜) ↦ Fin.cons (α := F') (φ x) (φs x)) (Fin.cons (α := F') φ' φs') s x

Tactic:
hasDerivWithinAt_finCons'.mpr ⟨h, hs⟩

Premises used: Iff.mpr, hasDerivWithinAt_finCons', And.intro
-- Module: Mathlib.Analysis.Calculus.Deriv.Shift
Goal:
𝕜 : Type u_1
F : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
f' : F
a x : 𝕜
hf : HasDerivAt f f' (a + x)
⊢ HasDerivAt (fun (x : 𝕜) ↦ f (a + x)) f' x

Tactic:
simpa [Function.comp_def] using HasDerivAt.scomp (𝕜 := 𝕜) x hf <| hasDerivAt_id' x |>.const_add a

Premises used: hasDerivAt_id', Function.comp_def, HasDerivAt.scomp, HasDerivAt.const_add
-- Module: Mathlib.Analysis.Calculus.Deriv.Shift
Goal:
𝕜 : Type u_1
F : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
f' : F
x a : 𝕜
hf : HasDerivAt f f' (x + a)
⊢ HasDerivAt (fun (x : 𝕜) ↦ f (x + a)) f' x

Tactic:
simpa [Function.comp_def] using HasDerivAt.scomp (𝕜 := 𝕜) x hf <| hasDerivAt_id' x |>.add_const a

Premises used: hasDerivAt_id', HasDerivAt.add_const, Function.comp_def, HasDerivAt.scomp
-- Module: Mathlib.Analysis.Calculus.Deriv.Shift
Goal:
𝕜 : Type u_1
F : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
f' : F
a x : 𝕜
hf : HasDerivAt f f' (a - x)
⊢ HasDerivAt (fun (x : 𝕜) ↦ f (a - x)) (-f') x

Tactic:
simpa [Function.comp_def] using HasDerivAt.scomp (𝕜 := 𝕜) x hf <| hasDerivAt_id' x |>.const_sub a

Premises used: HasDerivAt.const_sub, hasDerivAt_id', Function.comp_def, HasDerivAt.scomp
-- Module: Mathlib.Analysis.Calculus.Deriv.Shift
Goal:
𝕜 : Type u_1
F : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
f' : F
x a : 𝕜
hf : HasDerivAt f f' (x - a)
⊢ HasDerivAt (fun (x : 𝕜) ↦ f (x - a)) f' x

Tactic:
simpa [Function.comp_def] using HasDerivAt.scomp (𝕜 := 𝕜) x hf <| hasDerivAt_id' x |>.sub_const a

Premises used: hasDerivAt_id', HasDerivAt.sub_const, Function.comp_def, HasDerivAt.scomp
-- Module: Mathlib.Analysis.Calculus.Deriv.Shift
Goal:
𝕜 : Type u_1
F : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
s : Set 𝕜
x : 𝕜
⊢ derivWithin (fun (x : 𝕜) ↦ f (-x)) s x = -derivWithin f (-s) (-x)

Tactic:
simpa using derivWithin_comp_mul_left (-1) f s x

Premises used: derivWithin_comp_mul_left, OfNat.ofNat, Neg.neg
-- Module: Mathlib.Analysis.Calculus.Deriv.Shift
Goal:
𝕜 : Type u_1
F : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
x : 𝕜
⊢ deriv (fun (x : 𝕜) ↦ f (-x)) x = -deriv f (-x)

Tactic:
simpa using deriv_comp_mul_left (-1) f x

Premises used: deriv_comp_mul_left, OfNat.ofNat, Neg.neg
-- Module: Mathlib.Analysis.Calculus.Deriv.Shift
Goal:
𝕜 : Type u_1
F : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
a : 𝕜
s : Set 𝕜
x : 𝕜
⊢ derivWithin (fun (x : 𝕜) ↦ f (a + x)) s x = derivWithin f (a +ᵥ s) (a + x)

Tactic:
simp only [derivWithin, fderivWithin_comp_add_left]

Premises used: fderivWithin_comp_add_left, derivWithin
-- Module: Mathlib.Analysis.Calculus.Deriv.Shift
Goal:
𝕜 : Type u_1
F : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
a x : 𝕜
⊢ deriv (fun (x : 𝕜) ↦ f (a + x)) x = deriv f (a + x)

Tactic:
simp only [deriv, fderiv_comp_add_left]

Premises used: deriv, fderiv_comp_add_left
-- Module: Mathlib.Analysis.Calculus.Deriv.Shift
Goal:
𝕜 : Type u_1
F : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
a : 𝕜
s : Set 𝕜
x : 𝕜
⊢ derivWithin (fun (x : 𝕜) ↦ f (x + a)) s x = derivWithin f (a +ᵥ s) (x + a)

Tactic:
simp only [derivWithin, fderivWithin_comp_add_right]

Premises used: derivWithin, fderivWithin_comp_add_right
-- Module: Mathlib.Analysis.Calculus.Deriv.Shift
Goal:
𝕜 : Type u_1
F : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
a x : 𝕜
⊢ deriv (fun (x : 𝕜) ↦ f (x + a)) x = deriv f (x + a)

Tactic:
simpa [add_comm] using deriv_comp_const_add f a x

Premises used: add_comm, deriv_comp_const_add
-- Module: Mathlib.Analysis.Calculus.Deriv.Shift
Goal:
𝕜 : Type u_1
F : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
a : 𝕜
s : Set 𝕜
x : 𝕜
simp : derivWithin (fun (x : 𝕜) ↦ f (a + -x)) s x = -derivWithin f (a +ᵥ -s) (a + -x)
⊢ derivWithin (fun (x : 𝕜) ↦ f (a - x)) s x = -derivWithin f (a +ᵥ -s) (a - x)

Tactic:
simp only [sub_eq_add_neg]

Premises used: sub_eq_add_neg
-- Module: Mathlib.Analysis.Calculus.Deriv.Shift
Goal:
𝕜 : Type u_1
F : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
a : 𝕜
s : Set 𝕜
x : 𝕜
rw : -derivWithin (fun (x : 𝕜) ↦ f (a + x)) (-s) (-x) = -derivWithin f (a +ᵥ -s) (a + -x)
rw₁ rw₂ : -derivWithin f (a +ᵥ -s) (a + -x) = -derivWithin f (a +ᵥ -s) (a + -x)
⊢ derivWithin (fun (x : 𝕜) ↦ f (a + -x)) s x = -derivWithin f (a +ᵥ -s) (a + -x)

Tactic:
rw [derivWithin_comp_neg (f <| a + ·), derivWithin_comp_const_add]

Premises used: HAdd.hAdd, derivWithin_comp_const_add, derivWithin_comp_neg
-- Module: Mathlib.Analysis.Calculus.Deriv.Shift
Goal:
𝕜 : Type u_1
F : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
a x : 𝕜
simp_rw : deriv (fun (x : 𝕜) ↦ f (a + -x)) x = -deriv f (a + -x)
simp_rw₁ : -deriv (fun (x : 𝕜) ↦ f (a + x)) (-x) = -deriv f (a + -x)
⊢ deriv (fun (x : 𝕜) ↦ f (a - x)) x = -deriv f (a - x)

Tactic:
simp_rw [sub_eq_add_neg, deriv_comp_neg (f <| a + ·), deriv_comp_const_add]

Premises used: sub_eq_add_neg, HAdd.hAdd, deriv_comp_neg, deriv_comp_const_add
-- Module: Mathlib.Analysis.Calculus.Deriv.Shift
Goal:
𝕜 : Type u_1
F : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
a : 𝕜
s : Set 𝕜
x : 𝕜
simp_rw : derivWithin (fun (x : 𝕜) ↦ f (x + -a)) s x = derivWithin f (-a +ᵥ s) (x + -a)
⊢ derivWithin (fun (x : 𝕜) ↦ f (x - a)) s x = derivWithin f (-a +ᵥ s) (x - a)

Tactic:
simp_rw [sub_eq_add_neg, derivWithin_comp_add_const]

Premises used: sub_eq_add_neg, derivWithin_comp_add_const