awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Abs (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : E → ℝ
f' : StrongDual ℝ E
x : E
hf : HasFDerivAt f f' x
h₀ : f x < 0
⊢ HasFDerivAt (fun (x : E) ↦ |f x|) (-f') x
have h : instAddCommGroup = NormedAddCommGroup.toAddCommGroup →
  HEq (α := Module ℝ ℝ) Semiring.toModule (β := Module ℝ ℝ) NormedSpace.toModule →
    -f' = ContinuousLinearMap.toSpanSingleton ℝ (-1) ∘SL f'
Tactic: convert! (hasDerivAt_abs_neg h₀).hasFDerivAt.comp x hf using 1
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Abs (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : E → ℝ
f' : StrongDual ℝ E
x : E
hf : HasFDerivAt f f' x
h₀ : f x < 0
e_8 : instAddCommGroup = NormedAddCommGroup.toAddCommGroup
e_9 : HEq (α := Module ℝ ℝ) Semiring.toModule (β := Module ℝ ℝ) NormedSpace.toModule
⊢ -f' = ContinuousLinearMap.toSpanSingleton ℝ (-1) ∘SL f'
have h : ∀ (y : E),
  Eq (α := ℝ) ((-f' : (a : E) → ℝ) y : ℝ) ((ContinuousLinearMap.toSpanSingleton ℝ (-1) ∘SL f' : (a : E) → ℝ) y : ℝ)
Tactic: ext y
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Abs (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : E → ℝ
f' : StrongDual ℝ E
x : E
hf : HasStrictFDerivAt f f' x
h₀ : 0 < f x
⊢ HasStrictFDerivAt (fun (x : E) ↦ |f x|) f' x
have h : instAddCommGroup = NormedAddCommGroup.toAddCommGroup →
  HEq (α := Module ℝ ℝ) Semiring.toModule (β := Module ℝ ℝ) NormedSpace.toModule →
    f' = ContinuousLinearMap.toSpanSingleton ℝ 1 ∘SL f'
Tactic: convert! (hasStrictDerivAt_abs_pos h₀).hasStrictFDerivAt.comp x hf using 1
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Abs (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : E → ℝ
f' : StrongDual ℝ E
x : E
hf : HasStrictFDerivAt f f' x
h₀ : 0 < f x
e_8 : instAddCommGroup = NormedAddCommGroup.toAddCommGroup
e_9 : HEq (α := Module ℝ ℝ) Semiring.toModule (β := Module ℝ ℝ) NormedSpace.toModule
⊢ f' = ContinuousLinearMap.toSpanSingleton ℝ 1 ∘SL f'
have h : ∀ (y : E), Eq (α := ℝ) ((f' : (a : E) → ℝ) y : ℝ) ((ContinuousLinearMap.toSpanSingleton ℝ 1 ∘SL f' : (a : E) → ℝ) y : ℝ)
Tactic: ext y
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Abs (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : E → ℝ
f' : StrongDual ℝ E
x : E
hf : HasFDerivAt f f' x
h₀ : 0 < f x
⊢ HasFDerivAt (fun (x : E) ↦ |f x|) f' x
have h : instAddCommGroup = NormedAddCommGroup.toAddCommGroup →
  HEq (α := Module ℝ ℝ) Semiring.toModule (β := Module ℝ ℝ) NormedSpace.toModule →
    f' = ContinuousLinearMap.toSpanSingleton ℝ 1 ∘SL f'
Tactic: convert! (hasDerivAt_abs_pos h₀).hasFDerivAt.comp x hf using 1
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Abs (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : E → ℝ
f' : StrongDual ℝ E
x : E
hf : HasFDerivAt f f' x
h₀ : 0 < f x
e_8 : instAddCommGroup = NormedAddCommGroup.toAddCommGroup
e_9 : HEq (α := Module ℝ ℝ) Semiring.toModule (β := Module ℝ ℝ) NormedSpace.toModule
⊢ f' = ContinuousLinearMap.toSpanSingleton ℝ 1 ∘SL f'
have h : ∀ (y : E), Eq (α := ℝ) ((f' : (a : E) → ℝ) y : ℝ) ((ContinuousLinearMap.toSpanSingleton ℝ 1 ∘SL f' : (a : E) → ℝ) y : ℝ)
Tactic: ext y
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Abs (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : E → ℝ
f' : StrongDual ℝ E
x : E
hf : HasStrictFDerivAt f f' x
h₀ : f x ≠ 0
⊢ HasStrictFDerivAt (fun (x : E) ↦ |f x|) (HSMul.hSMul (α := ℝ) (↑((SignType.sign : (a : ℝ) → SignType) (f x)) : ℝ) f')
    x
have h : instAddCommGroup = NormedAddCommGroup.toAddCommGroup →
  HEq (α := Module ℝ ℝ) Semiring.toModule (β := Module ℝ ℝ) NormedSpace.toModule →
    HSMul.hSMul (α := ℝ) (↑((SignType.sign : (a : ℝ) → SignType) (f x)) : ℝ) f' =
      ContinuousLinearMap.toSpanSingleton ℝ (↑((SignType.sign : (a : ℝ) → SignType) (f x)) : ℝ) ∘SL f'
Tactic: convert! (hasStrictDerivAt_abs h₀).hasStrictFDerivAt.comp x hf using 1
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Abs (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : E → ℝ
f' : StrongDual ℝ E
x : E
hf : HasStrictFDerivAt f f' x
h₀ : f x ≠ 0
e_8 : instAddCommGroup = NormedAddCommGroup.toAddCommGroup
e_9 : HEq (α := Module ℝ ℝ) Semiring.toModule (β := Module ℝ ℝ) NormedSpace.toModule
⊢ HSMul.hSMul (α := ℝ) (↑((SignType.sign : (a : ℝ) → SignType) (f x)) : ℝ) f' =
    ContinuousLinearMap.toSpanSingleton ℝ (↑((SignType.sign : (a : ℝ) → SignType) (f x)) : ℝ) ∘SL f'
have h : ∀ (y : E),
  Eq (α := ℝ) ((HSMul.hSMul (α := ℝ) (↑((SignType.sign : (a : ℝ) → SignType) (f x)) : ℝ) f' : (a : E) → ℝ) y : ℝ)
    ((ContinuousLinearMap.toSpanSingleton ℝ (↑((SignType.sign : (a : ℝ) → SignType) (f x)) : ℝ) ∘SL f' : (a : E) → ℝ)
        y :
      ℝ)
Tactic: ext y
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Abs (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : E → ℝ
f' : StrongDual ℝ E
x : E
hf : HasFDerivAt f f' x
h₀ : f x ≠ 0
⊢ HasFDerivAt (fun (x : E) ↦ |f x|) (HSMul.hSMul (α := ℝ) (↑((SignType.sign : (a : ℝ) → SignType) (f x)) : ℝ) f') x
have h : instAddCommGroup = NormedAddCommGroup.toAddCommGroup →
  HEq (α := Module ℝ ℝ) Semiring.toModule (β := Module ℝ ℝ) NormedSpace.toModule →
    HSMul.hSMul (α := ℝ) (↑((SignType.sign : (a : ℝ) → SignType) (f x)) : ℝ) f' =
      ContinuousLinearMap.toSpanSingleton ℝ (↑((SignType.sign : (a : ℝ) → SignType) (f x)) : ℝ) ∘SL f'
Tactic: convert! (hasDerivAt_abs h₀).hasFDerivAt.comp x hf using 1
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Abs (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : E → ℝ
f' : StrongDual ℝ E
x : E
hf : HasFDerivAt f f' x
h₀ : f x ≠ 0
e_8 : instAddCommGroup = NormedAddCommGroup.toAddCommGroup
e_9 : HEq (α := Module ℝ ℝ) Semiring.toModule (β := Module ℝ ℝ) NormedSpace.toModule
⊢ HSMul.hSMul (α := ℝ) (↑((SignType.sign : (a : ℝ) → SignType) (f x)) : ℝ) f' =
    ContinuousLinearMap.toSpanSingleton ℝ (↑((SignType.sign : (a : ℝ) → SignType) (f x)) : ℝ) ∘SL f'
have h : ∀ (y : E),
  Eq (α := ℝ) ((HSMul.hSMul (α := ℝ) (↑((SignType.sign : (a : ℝ) → SignType) (f x)) : ℝ) f' : (a : E) → ℝ) y : ℝ)
    ((ContinuousLinearMap.toSpanSingleton ℝ (↑((SignType.sign : (a : ℝ) → SignType) (f x)) : ℝ) ∘SL f' : (a : E) → ℝ)
        y :
      ℝ)
Tactic: ext y
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Abs (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : E → ℝ
f' : StrongDual ℝ E
s : Set E
x : E
hf : HasFDerivWithinAt f f' s x
h₀ : f x < 0
⊢ HasFDerivWithinAt (fun (x : E) ↦ |f x|) (-f') s x
have h : instAddCommGroup = Ring.toAddCommGroup →
  HEq (α := Module ℝ ℝ) Semiring.toModule (β := Module ℝ ℝ) NormedSpace.toModule → -f' = HSMul.hSMul (α := ℝ) (-1) f'
Tactic: convert! (hasDerivAt_abs_neg h₀).comp_hasFDerivWithinAt x hf using 1
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Abs (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : E → ℝ
f' : StrongDual ℝ E
s : Set E
x : E
hf : HasFDerivWithinAt f f' s x
h₀ : 0 < f x
⊢ HasFDerivWithinAt (fun (x : E) ↦ |f x|) f' s x
have h : instAddCommGroup = Ring.toAddCommGroup →
  HEq (α := Module ℝ ℝ) Semiring.toModule (β := Module ℝ ℝ) NormedSpace.toModule → f' = HSMul.hSMul (α := ℝ) 1 f'
Tactic: convert! (hasDerivAt_abs_pos h₀).comp_hasFDerivWithinAt x hf using 1
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Abs (hypothesis)
Goal:
h : DifferentiableAt ℝ (E := ℝ) abs 0
⊢ False
have h₁ : Eq (α := ℝ) (deriv abs 0) 1
Tactic: have h₁ : deriv abs (0 : ℝ) = 1 :=
    (uniqueDiffOn_Ici _ _ Set.self_mem_Ici).eq_deriv _ h.hasDerivAt.hasDerivWithinAt <|
      (hasDerivWithinAt_id _ _).congr_of_mem (fun _ h ↦ abs_of_nonneg h) Set.self_mem_Ici
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Abs (hypothesis)
Goal:
h : DifferentiableAt ℝ (E := ℝ) abs 0
h₁ : Eq (α := ℝ) (deriv abs 0) 1
⊢ False
have h₂ : Eq (α := ℝ) (deriv abs 0) (-1)
Tactic: have h₂ : deriv abs (0 : ℝ) = -1 :=
    (uniqueDiffOn_Iic _ _ Set.self_mem_Iic).eq_deriv _ h.hasDerivAt.hasDerivWithinAt <|
      (hasDerivWithinAt_neg _ _).congr_of_mem (fun _ h ↦ abs_of_nonpos h) Set.self_mem_Iic
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Abs (goal)
Goal:
h : DifferentiableAt ℝ (E := ℝ) abs 0
h₁ : Eq (α := ℝ) (deriv abs 0) 1
h₂ : Eq (α := ℝ) (deriv abs 0) (-1)
⊢ False
have linarith : HMul.hMul (α := ℝ) 2 (-1) + -HSub.hSub (α := ℝ) (deriv abs 0) 1 + HSub.hSub (α := ℝ) (deriv abs 0) (-1) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Abs (goal)
Goal:
h : DifferentiableAt ℝ (E := ℝ) abs 0
h₁ : Eq (α := ℝ) (deriv abs 0) 1
h₂ : Eq (α := ℝ) (deriv abs 0) (-1)
linarith : HMul.hMul (α := ℝ) 2 (-1) + -HSub.hSub (α := ℝ) (deriv abs 0) 1 + HSub.hSub (α := ℝ) (deriv abs 0) (-1) = 0
⊢ False
have linarith₁ : GT.gt (α := ℝ) 2 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Abs (goal)
Goal:
x : ℝ
⊢ Eq (α := ℝ) (deriv (fun (x : ℝ) ↦ |x|) x) (↑((SignType.sign : (a : ℝ) → SignType) x) : ℝ)
have inl : Eq (α := ℝ) (deriv (fun (x : ℝ) ↦ |x|) 0) (↑((SignType.sign : (a : ℝ) → SignType) 0) : ℝ)
Tactic: obtain rfl | hx := eq_or_ne x 0
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Abs (goal)
Goal:
x : ℝ
inl : Eq (α := ℝ) (deriv (fun (x : ℝ) ↦ |x|) 0) (↑((SignType.sign : (a : ℝ) → SignType) 0) : ℝ)
⊢ Eq (α := ℝ) (deriv (fun (x : ℝ) ↦ |x|) x) (↑((SignType.sign : (a : ℝ) → SignType) x) : ℝ)
have inr : ∀ (hx : x ≠ 0), Eq (α := ℝ) (deriv (fun (x : ℝ) ↦ |x|) x) (↑((SignType.sign : (a : ℝ) → SignType) x) : ℝ)
Tactic: obtain rfl | hx := eq_or_ne x 0
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Add (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f g : 𝕜 → F
x : 𝕜
s : Set 𝕜
hf : DifferentiableWithinAt 𝕜 f s x
hg : DifferentiableWithinAt 𝕜 g s x
⊢ derivWithin (fun (y : 𝕜) ↦ f y + g y) s x = derivWithin f s x + derivWithin g s x
have pos : ∀ (hsx : UniqueDiffWithinAt 𝕜 s x), derivWithin (fun (y : 𝕜) ↦ f y + g y) s x = derivWithin f s x + derivWithin g s x
Tactic: by_cases hsx : UniqueDiffWithinAt 𝕜 s x
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Add (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f g : 𝕜 → F
x : 𝕜
s : Set 𝕜
hf : DifferentiableWithinAt 𝕜 f s x
hg : DifferentiableWithinAt 𝕜 g s x
pos :
  ∀ (hsx : UniqueDiffWithinAt 𝕜 s x), derivWithin (fun (y : 𝕜) ↦ f y + g y) s x = derivWithin f s x + derivWithin g s x
⊢ derivWithin (fun (y : 𝕜) ↦ f y + g y) s x = derivWithin f s x + derivWithin g s x
have neg : ∀ (hsx : ¬UniqueDiffWithinAt 𝕜 s x), derivWithin (fun (y : 𝕜) ↦ f y + g y) s x = derivWithin f s x + derivWithin g s x
Tactic: by_cases hsx : UniqueDiffWithinAt 𝕜 s x
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Add (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
c : F
⊢ (derivWithin fun (x : 𝕜) ↦ c + f x) = derivWithin f
have h : ∀ (x : Set 𝕜) (x_1 : 𝕜), derivWithin (fun (x : 𝕜) ↦ c + f x) x x_1 = derivWithin f x x_1
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Add (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x c : 𝕜
⊢ Eq (α := 𝕜) (deriv (fun (x : 𝕜) ↦ c + x) x) 1
have rw : Eq (α := 𝕜) (deriv (fun (x : 𝕜) ↦ x) x) 1
Tactic: rw [deriv_const_add c, deriv_id'']
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Add (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x c : 𝕜
rw : Eq (α := 𝕜) (deriv (fun (x : 𝕜) ↦ x) x) 1
⊢ Eq (α := 𝕜) (deriv (fun (x : 𝕜) ↦ c + x) x) 1
have rw₁ : Eq.{u + 1} (α := 𝕜) ((fun (x : 𝕜) ↦ (1 : 𝕜)) x) 1
Tactic: rw [deriv_const_add c, deriv_id'']
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Add (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
L : Filter (𝕜 × 𝕜)
ι : Type u_1
u : Finset ι
A : ι → 𝕜 → F
A' : ι → F
h : ∀ i ∈ u, HasDerivAtFilter (A i) (A' i) L
⊢ HasDerivAtFilter.{u, v} (F := F) (∑ i ∈ u, A i) (∑ i ∈ u, A' i) L
have h₁ : ∀ (x : 𝕜), Eq.{v + 1} (α := F) ((∑ i ∈ u, A i) x) (∑ i ∈ u, A i x)
Tactic: convert! HasDerivAtFilter.fun_sum h
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Add (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
x : 𝕜
s : Set 𝕜
ι : Type u_1
u : Finset ι
A : ι → 𝕜 → F
h : ∀ i ∈ u, DifferentiableWithinAt 𝕜 (A i) s x
⊢ Eq.{v + 1} (α := F) (derivWithin (fun (y : 𝕜) ↦ ∑ i ∈ u, A i y) s x) (∑ i ∈ u, derivWithin (A i) s x)
have pos : ∀ (hsx : UniqueDiffWithinAt 𝕜 s x),
  Eq.{v + 1} (α := F) (derivWithin (fun (y : 𝕜) ↦ ∑ i ∈ u, A i y) s x) (∑ i ∈ u, derivWithin (A i) s x)
Tactic: by_cases hsx : UniqueDiffWithinAt 𝕜 s x
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Add (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
x : 𝕜
s : Set 𝕜
ι : Type u_1
u : Finset ι
A : ι → 𝕜 → F
h : ∀ i ∈ u, DifferentiableWithinAt 𝕜 (A i) s x
pos :
  ∀ (hsx : UniqueDiffWithinAt 𝕜 s x),
    Eq.{v + 1} (α := F) (derivWithin (fun (y : 𝕜) ↦ ∑ i ∈ u, A i y) s x) (∑ i ∈ u, derivWithin (A i) s x)
⊢ Eq.{v + 1} (α := F) (derivWithin (fun (y : 𝕜) ↦ ∑ i ∈ u, A i y) s x) (∑ i ∈ u, derivWithin (A i) s x)
have neg : ∀ (hsx : ¬UniqueDiffWithinAt 𝕜 s x),
  Eq.{v + 1} (α := F) (derivWithin (fun (y : 𝕜) ↦ ∑ i ∈ u, A i y) s x) (∑ i ∈ u, derivWithin (A i) s x)
Tactic: by_cases hsx : UniqueDiffWithinAt 𝕜 s x
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Add (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
x : 𝕜
s : Set 𝕜
ι : Type u_1
u : Finset ι
A : ι → 𝕜 → F
h : ∀ i ∈ u, DifferentiableWithinAt 𝕜 (A i) s x
⊢ Eq.{v + 1} (α := F) (derivWithin (∑ i ∈ u, A i) s x) (∑ i ∈ u, derivWithin (A i) s x)
have pos : ∀ (hsx : UniqueDiffWithinAt 𝕜 s x),
  Eq.{v + 1} (α := F) (derivWithin (∑ i ∈ u, A i) s x) (∑ i ∈ u, derivWithin (A i) s x)
Tactic: by_cases hsx : UniqueDiffWithinAt 𝕜 s x
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Add (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
x : 𝕜
s : Set 𝕜
ι : Type u_1
u : Finset ι
A : ι → 𝕜 → F
h : ∀ i ∈ u, DifferentiableWithinAt 𝕜 (A i) s x
pos :
  ∀ (hsx : UniqueDiffWithinAt 𝕜 s x),
    Eq.{v + 1} (α := F) (derivWithin (∑ i ∈ u, A i) s x) (∑ i ∈ u, derivWithin (A i) s x)
⊢ Eq.{v + 1} (α := F) (derivWithin (∑ i ∈ u, A i) s x) (∑ i ∈ u, derivWithin (A i) s x)
have neg : ∀ (hsx : ¬UniqueDiffWithinAt 𝕜 s x),
  Eq.{v + 1} (α := F) (derivWithin (∑ i ∈ u, A i) s x) (∑ i ∈ u, derivWithin (A i) s x)
Tactic: by_cases hsx : UniqueDiffWithinAt 𝕜 s x
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Add (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
x : 𝕜
s : Set 𝕜
⊢ derivWithin (-f) s x = -derivWithin f s x
have pos : ∀ (hsx : UniqueDiffWithinAt 𝕜 s x), derivWithin (-f) s x = -derivWithin f s x
Tactic: by_cases hsx : UniqueDiffWithinAt 𝕜 s x
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Add (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
x : 𝕜
s : Set 𝕜
pos : ∀ (hsx : UniqueDiffWithinAt 𝕜 s x), derivWithin (-f) s x = -derivWithin f s x
⊢ derivWithin (-f) s x = -derivWithin f s x
have neg₁ : ∀ (hsx : ¬UniqueDiffWithinAt 𝕜 s x), derivWithin (-f) s x = -derivWithin f s x
Tactic: by_cases hsx : UniqueDiffWithinAt 𝕜 s x
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Add (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
a : 𝕜
⊢ DifferentiableAt.{u, u, v} 𝕜 (F := F) (fun (x : 𝕜) ↦ f (-x)) a ↔ DifferentiableAt 𝕜 f (-a)
have refine : ∀ (H : DifferentiableAt.{u, u, v} 𝕜 (F := F) (fun (x : 𝕜) ↦ f (-x)) a), DifferentiableAt 𝕜 f (-a)
Tactic: refine ⟨fun H ↦ ?_, fun H ↦ H.comp a differentiable_neg.differentiableAt⟩
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Add (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
a : 𝕜
H : DifferentiableAt.{u, u, v} 𝕜 (F := F) (fun (x : 𝕜) ↦ f (-x)) a
⊢ DifferentiableAt 𝕜 f (-a)
have h : f = (fun (x : 𝕜) ↦ f (-x)) ∘ Neg.neg
Tactic: convert! ((neg_neg a).symm ▸ H).comp (-a) differentiable_neg.differentiableAt
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Add (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
a : 𝕜
H : DifferentiableAt.{u, u, v} 𝕜 (F := F) (fun (x : 𝕜) ↦ f (-x)) a
⊢ f = (fun (x : 𝕜) ↦ f (-x)) ∘ Neg.neg
have h : ∀ (x : 𝕜), f x = ((fun (x : 𝕜) ↦ f (-x)) ∘ Neg.neg) x
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Add (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
a : 𝕜
⊢ DifferentiableAt 𝕜 f a ↔ DifferentiableAt.{u, u, v} 𝕜 (F := F) (fun (x : 𝕜) ↦ f (-x)) (-a)
have simp_rw : DifferentiableAt 𝕜 f a ↔ DifferentiableAt.{u, u, v} 𝕜 (F := F) (fun (x : 𝕜) ↦ f (- -x)) a
Tactic: simp_rw [← differentiableAt_comp_neg, neg_neg]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Add (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
c : F
⊢ (derivWithin fun (x : 𝕜) ↦ f x - c) = derivWithin f
have h : ∀ (x : Set 𝕜) (x_1 : 𝕜), derivWithin (fun (x : 𝕜) ↦ f x - c) x x_1 = derivWithin f x x_1
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Add (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
c : F
⊢ (deriv fun (x : 𝕜) ↦ f x - c) = deriv f
have h : ∀ (x : 𝕜), deriv (fun (x : 𝕜) ↦ f x - c) x = deriv f x
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Add (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x c : 𝕜
⊢ Eq (α := 𝕜) (deriv (fun (x : 𝕜) ↦ c - x) x) (-1)
have rw : Eq (α := 𝕜) (-deriv (fun (x : 𝕜) ↦ x) x) (-1)
Tactic: rw [deriv_const_sub c, deriv_id'']
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Add (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x c : 𝕜
rw : Eq (α := 𝕜) (-deriv (fun (x : 𝕜) ↦ x) x) (-1)
⊢ Eq (α := 𝕜) (deriv (fun (x : 𝕜) ↦ c - x) x) (-1)
have rw₁ : Eq.{u + 1} (α := 𝕜) (-(fun (x : 𝕜) ↦ (1 : 𝕜)) x) (-1)
Tactic: rw [deriv_const_sub c, deriv_id'']
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Add (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
a b : 𝕜
⊢ DifferentiableAt.{u, u, v} 𝕜 (F := F) (fun (x : 𝕜) ↦ f (b - x)) a ↔ DifferentiableAt 𝕜 f (b - a)
have refine : ∀ (H : DifferentiableAt.{u, u, v} 𝕜 (F := F) (fun (x : 𝕜) ↦ f (b - x)) a), DifferentiableAt 𝕜 f (b - a)
Tactic: refine ⟨fun H ↦ ?_, fun H ↦ H.comp a (differentiable_id.const_sub _).differentiableAt⟩
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Add (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
a b : 𝕜
H : DifferentiableAt.{u, u, v} 𝕜 (F := F) (fun (x : 𝕜) ↦ f (b - x)) a
⊢ DifferentiableAt 𝕜 f (b - a)
have h : f = (fun (x : 𝕜) ↦ f (b - x)) ∘ HSub.hSub b
Tactic: convert!
    ((sub_sub_cancel _ a).symm ▸ H).comp (b - a) (differentiable_id.const_sub _).differentiableAt
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Add (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
a b : 𝕜
H : DifferentiableAt.{u, u, v} 𝕜 (F := F) (fun (x : 𝕜) ↦ f (b - x)) a
⊢ f = (fun (x : 𝕜) ↦ f (b - x)) ∘ HSub.hSub b
have h : ∀ (x : 𝕜), f x = ((fun (x : 𝕜) ↦ f (b - x)) ∘ HSub.hSub b) x
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.AffineMap (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 →ᵃ[𝕜] E
L : Filter (𝕜 × 𝕜)
⊢ HasDerivAtFilter.{u_1, u_2} (F := E) ((⇑f : (a : 𝕜) → E) : (a : 𝕜) → E) ((f.linear : (a : 𝕜) → E) 1 : E) L
have rw : HasDerivAtFilter (HAdd.hAdd (α := (a : 𝕜) → E) (⇑f.linear : (a : 𝕜) → E) fun (x : 𝕜) ↦ (f : (a : 𝕜) → E) 0)
  ((f.linear : (a : 𝕜) → E) 1) L
Tactic: rw [f.decomp]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Basic (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : AddCommGroup F
inst_2 : Module 𝕜 F
inst_3 : TopologicalSpace F
f : 𝕜 → F
x : 𝕜
s : Set 𝕜
h : ¬DifferentiableWithinAt 𝕜 f s x
⊢ derivWithin f s x = 0
have unfold : Eq.{v + 1} (α := F) (((fderivWithin 𝕜 f s x : 𝕜 →L[𝕜] F) : (a : 𝕜) → F) 1 : F) (0 : F)
Tactic: unfold derivWithin
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Basic (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : AddCommGroup F
inst_2 : Module 𝕜 F
inst_3 : TopologicalSpace F
f : 𝕜 → F
x : 𝕜
s : Set 𝕜
h : ¬DifferentiableWithinAt 𝕜 f s x
⊢ Eq.{v + 1} (α := F) (((fderivWithin 𝕜 f s x : 𝕜 →L[𝕜] F) : (a : 𝕜) → F) 1 : F) (0 : F)
have rw : Eq.{v + 1} (α := F) ((0 : (a : 𝕜) → F) 1 : F) (0 : F)
Tactic: rw [fderivWithin_zero_of_not_differentiableWithinAt h]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Basic (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
x : 𝕜
s : Set 𝕜
h : ¬AccPt x (𝓟 s)
⊢ derivWithin f s x = 0
have rw : Eq.{v + 1} (α := F) (((fderivWithin 𝕜 f s x : 𝕜 →L[𝕜] F) : (a : 𝕜) → F) 1 : F) (0 : F)
Tactic: rw [derivWithin, fderivWithin_zero_of_not_accPt h, ContinuousLinearMap.zero_apply]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Basic (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
x : 𝕜
s : Set 𝕜
h : ¬AccPt x (𝓟 s)
rw : Eq.{v + 1} (α := F) (((fderivWithin 𝕜 f s x : 𝕜 →L[𝕜] F) : (a : 𝕜) → F) 1 : F) (0 : F)
⊢ derivWithin f s x = 0
have rw₁ : Eq.{v + 1} (α := F) ((0 : (a : 𝕜) → F) 1 : F) (0 : F)
Tactic: rw [derivWithin, fderivWithin_zero_of_not_accPt h, ContinuousLinearMap.zero_apply]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Basic (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
x : 𝕜
s : Set 𝕜
h : ¬AccPt x (𝓟 s)
rw : Eq.{v + 1} (α := F) (((fderivWithin 𝕜 f s x : 𝕜 →L[𝕜] F) : (a : 𝕜) → F) 1 : F) (0 : F)
rw₁ : Eq.{v + 1} (α := F) ((0 : (a : 𝕜) → F) 1 : F) (0 : F)
⊢ derivWithin f s x = 0
have rw₂ : Eq.{v + 1} (α := F) 0 0
Tactic: rw [derivWithin, fderivWithin_zero_of_not_accPt h, ContinuousLinearMap.zero_apply]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Basic (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
x : 𝕜
s : Set 𝕜
h : x ∉ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
⊢ derivWithin f s x = 0
have rw : Eq.{v + 1} (α := F) (((fderivWithin 𝕜 f s x : 𝕜 →L[𝕜] F) : (a : 𝕜) → F) 1 : F) (0 : F)
Tactic: rw [derivWithin, fderivWithin_zero_of_notMem_closure h, ContinuousLinearMap.zero_apply]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Basic (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
x : 𝕜
s : Set 𝕜
h : x ∉ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
rw : Eq.{v + 1} (α := F) (((fderivWithin 𝕜 f s x : 𝕜 →L[𝕜] F) : (a : 𝕜) → F) 1 : F) (0 : F)
⊢ derivWithin f s x = 0
have rw₁ : Eq.{v + 1} (α := F) ((0 : (a : 𝕜) → F) 1 : F) (0 : F)
Tactic: rw [derivWithin, fderivWithin_zero_of_notMem_closure h, ContinuousLinearMap.zero_apply]