awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Calculus.DifferentialForm.VectorField (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
n : ℕ
s : Set E
x : E
ω : E → E [⋀^Fin n]→L[𝕜] F
V : Fin (n + 1) → E → E
hω : DifferentiableWithinAt 𝕜 ω s x
hV : ∀ (i : Fin (n + 1)), DifferentiableWithinAt 𝕜 (V i) s x
hsx : UniqueDiffWithinAt 𝕜 s x
hcomm : Pairwise fun (i j : Fin (n + 1)) ↦ lieBracketWithin 𝕜 (V i) (V j) s x = 0
⊢ Eq.{u_3 + 1} (α := F) ((extDerivWithin ω s x : (a : Fin (n + 1) → E) → F) fun (x_1 : Fin (n + 1)) ↦ V x_1 x : F)
    (∑ i : Fin (n + 1),
        HSMul.hSMul (β := F) (HPow.hPow (α := ℤ) (-1) (↑i : ℕ))
          ((fderivWithin 𝕜
                  (fun (x : E) ↦
                    (ω x : (a : Fin n → E) → F)
                      (i.removeNth (α := fun (x : Fin (n + 1)) ↦ E) fun (x_1 : Fin (n + 1)) ↦ V x_1 x :
                        (i : Fin n) → E))
                  s x :
                (a : E) → F)
              (V i x) :
            F) :
      F)
have zero : ∀ {ω : E → E [⋀^Fin 0]→L[𝕜] F} {V : Fin (HAdd.hAdd (α := ℕ) 0 1) → E → E} (hω : DifferentiableWithinAt 𝕜 ω s x)
  (hV : ∀ (i : Fin (HAdd.hAdd (α := ℕ) 0 1)), DifferentiableWithinAt 𝕜 (V i) s x)
  (hcomm : Pairwise fun (i j : Fin (HAdd.hAdd (α := ℕ) 0 1)) ↦ lieBracketWithin 𝕜 (V i) (V j) s x = 0),
  Eq.{u_3 + 1} (α := F)
    ((extDerivWithin ω s x : (a : Fin (0 + 1) → E) → F) fun (x_1 : Fin (HAdd.hAdd (α := ℕ) 0 1)) ↦ V x_1 x : F)
    (∑ i : Fin (0 + 1),
        HSMul.hSMul (β := F) (HPow.hPow (α := ℤ) (-1) (↑i : ℕ))
          ((fderivWithin 𝕜
                  (fun (x : E) ↦
                    (ω x : (a : Fin 0 → E) → F)
                      (i.removeNth (α := fun (x : Fin (HAdd.hAdd (α := ℕ) 0 1)) ↦ E)
                          fun (x_1 : Fin (HAdd.hAdd (α := ℕ) 0 1)) ↦ V x_1 x :
                        (i : Fin 0) → E))
                  s x :
                (a : E) → F)
              (V i x) :
            F) :
      F)
Tactic: cases n with
  | zero =>
    simp [extDerivWithin_apply, fderivWithin_continuousAlternatingMap_apply_const_apply,
      fderivWithin_continuousAlternatingMap_apply_apply, *]
  | succ n =>
    rw [extDerivWithin_apply_vectorField hω hV hsx, sub_eq_self]
    refine Fintype.sum_eq_zero _ fun i ↦ sum_eq_zero fun j hj ↦ ?_
    rw [hcomm (ne_of_lt <| by simpa using hj), (ω x).map_coord_zero 0] <;>
      simp
Cleared hypotheses: n, ω, V, hω, hV, hcomm
-- Lean 4 proof step from Mathlib.Analysis.Calculus.DifferentialForm.VectorField (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
n : ℕ
x : E
ω : E → E [⋀^Fin n]→L[𝕜] F
V : Fin (n + 1) → E → E
hω : DifferentiableAt 𝕜 ω x
hV : ∀ (i : Fin (n + 1)), DifferentiableAt 𝕜 (V i) x
hcomm : Pairwise fun (i j : Fin (n + 1)) ↦ lieBracket 𝕜 (V i) (V j) x = 0
⊢ Eq.{u_3 + 1} (α := F) ((extDeriv ω x : (a : Fin (n + 1) → E) → F) fun (x_1 : Fin (n + 1)) ↦ V x_1 x : F)
    (∑ i : Fin (n + 1),
        HSMul.hSMul (β := F) (HPow.hPow (α := ℤ) (-1) (↑i : ℕ))
          ((fderiv 𝕜
                  (fun (x : E) ↦
                    (ω x : (a : Fin n → E) → F)
                      (i.removeNth (α := fun (x : Fin (n + 1)) ↦ E) fun (x_1 : Fin (n + 1)) ↦ V x_1 x :
                        (i : Fin n) → E))
                  x :
                (a : E) → F)
              (V i x) :
            F) :
      F)
have simp : ∀ (hω : DifferentiableWithinAt 𝕜 ω Set.univ x) (hV : ∀ (i : Fin (n + 1)), DifferentiableWithinAt 𝕜 (V i) Set.univ x)
  (hcomm : Pairwise fun (i j : Fin (n + 1)) ↦ lieBracketWithin 𝕜 (V i) (V j) Set.univ x = 0),
  Eq.{u_3 + 1} (α := F)
    ((extDerivWithin ω Set.univ x : (a : Fin (n + 1) → E) → F) fun (x_1 : Fin (n + 1)) ↦ V x_1 x : F)
    (∑ x_1 : Fin (n + 1),
        HSMul.hSMul (β := F) (HPow.hPow (α := ℤ) (-1) (↑x_1 : ℕ))
          ((fderivWithin 𝕜
                  (fun (x : E) ↦
                    (ω x : (a : Fin n → E) → F)
                      (x_1.removeNth (α := fun (x : Fin (n + 1)) ↦ E) fun (x_2 : Fin (n + 1)) ↦ V x_2 x :
                        (i : Fin n) → E))
                  Set.univ x :
                (a : E) → F)
              (V x_1 x) :
            F) :
      F)
Tactic: simp only [← differentiableWithinAt_univ, ← lieBracketWithin_univ, ← extDerivWithin_univ,
    ← fderivWithin_univ] at *
Cleared hypotheses: hω, hV, hcomm
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Add (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
x : E
s : Set E
R : Type u_4
inst_5 : Monoid R
inst_6 : DistribMulAction R F
inst_7 : SMulCommClass 𝕜 R F
inst_8 : ContinuousConstSMul R F
c : R
inst_9 : Invertible c
⊢ DifferentiableWithinAt 𝕜 (c • f) s x ↔ DifferentiableWithinAt 𝕜 f s x
have refine : ∀ (h : DifferentiableWithinAt 𝕜 (c • f) s x), DifferentiableWithinAt 𝕜 f s x
Tactic: refine ⟨fun h ↦ ?_, fun h ↦ h.const_smul c⟩
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Add (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
x : E
s : Set E
R : Type u_4
inst_5 : Monoid R
inst_6 : DistribMulAction R F
inst_7 : SMulCommClass 𝕜 R F
inst_8 : ContinuousConstSMul R F
c : R
inst_9 : Invertible c
h : DifferentiableWithinAt 𝕜 (c • f) s x
⊢ DifferentiableWithinAt 𝕜 f s x
have apply : f =ᶠ[nhdsWithin x s] @Invertible.invOf _ MulOne.toMul MulOne.toOne c _ • c • f
Tactic: apply (h.const_smul ⅟c).congr_of_eventuallyEq ?_ (by simp)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Add (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
x : E
s : Set E
R : Type u_4
inst_5 : Monoid R
inst_6 : DistribMulAction R F
inst_7 : SMulCommClass 𝕜 R F
inst_8 : ContinuousConstSMul R F
c : R
inst_9 : Invertible c
h : DifferentiableWithinAt 𝕜 (c • f) s x
⊢ f =ᶠ[nhdsWithin x s] @Invertible.invOf _ MulOne.toMul MulOne.toOne c _ • c • f
have h₁ : ∀ (a : E),
  Membership.mem (γ := Set E)
    {x : E | (fun (x : E) ↦ f x = (@Invertible.invOf _ MulOne.toMul MulOne.toOne c _ • c • f) x) x} a
Tactic: filter_upwards with x using by simp
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Add (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
x : E
s : Set E
R : Type u_4
inst_5 : Monoid R
inst_6 : DistribMulAction R F
inst_7 : SMulCommClass 𝕜 R F
inst_8 : ContinuousConstSMul R F
c : R
inst_9 : Invertible c
h : DifferentiableWithinAt 𝕜 (c • f) s x
h₁ :
  ∀ (a : E),
    Membership.mem (γ := Set E)
      {x : E | (fun (x : E) ↦ f x = (@Invertible.invOf _ MulOne.toMul MulOne.toOne c _ • c • f) x) x} a
⊢ f =ᶠ[nhdsWithin x s] @Invertible.invOf _ MulOne.toMul MulOne.toOne c _ • c • f
have h₂ : ∀ (a : E), f a = (@Invertible.invOf _ MulOne.toMul MulOne.toOne c _ • c • f) a
Tactic: filter_upwards with x using by simp
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Add (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
x : E
s : Set E
R : Type u_4
inst_5 : Monoid R
inst_6 : DistribMulAction R F
inst_7 : SMulCommClass 𝕜 R F
inst_8 : ContinuousConstSMul R F
c : R
inst_9 : Invertible c
hs : UniqueDiffWithinAt 𝕜 s x
⊢ fderivWithin 𝕜 (c • f) s x = HSMul.hSMul (β := E →L[𝕜] F) c (fderivWithin 𝕜 f s x)
have pos : ∀ (h : DifferentiableWithinAt 𝕜 f s x),
  fderivWithin 𝕜 (c • f) s x = HSMul.hSMul (β := E →L[𝕜] F) c (fderivWithin 𝕜 f s x)
Tactic: by_cases h : DifferentiableWithinAt 𝕜 f s x
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Add (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
x : E
s : Set E
R : Type u_4
inst_5 : Monoid R
inst_6 : DistribMulAction R F
inst_7 : SMulCommClass 𝕜 R F
inst_8 : ContinuousConstSMul R F
c : R
inst_9 : Invertible c
hs : UniqueDiffWithinAt 𝕜 s x
pos :
  ∀ (h : DifferentiableWithinAt 𝕜 f s x),
    fderivWithin 𝕜 (c • f) s x = HSMul.hSMul (β := E →L[𝕜] F) c (fderivWithin 𝕜 f s x)
⊢ fderivWithin 𝕜 (c • f) s x = HSMul.hSMul (β := E →L[𝕜] F) c (fderivWithin 𝕜 f s x)
have neg : ∀ (h : ¬DifferentiableWithinAt 𝕜 f s x),
  fderivWithin 𝕜 (c • f) s x = HSMul.hSMul (β := E →L[𝕜] F) c (fderivWithin 𝕜 f s x)
Tactic: by_cases h : DifferentiableWithinAt 𝕜 f s x
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Add (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
x : E
s : Set E
R : Type u_4
inst_5 : Monoid R
inst_6 : DistribMulAction R F
inst_7 : SMulCommClass 𝕜 R F
inst_8 : ContinuousConstSMul R F
c : R
inst_9 : Invertible c
hs : UniqueDiffWithinAt 𝕜 s x
h : ¬DifferentiableWithinAt 𝕜 f s x
⊢ ¬DifferentiableWithinAt 𝕜 (c • f) s x
have contrapose : ∀ (h : DifferentiableWithinAt 𝕜 (c • f) s x), DifferentiableWithinAt 𝕜 f s x
Tactic: contrapose h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Add (hypothesis)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
x : E
s : Set E
R : Type u_4
inst_5 : Monoid R
inst_6 : DistribMulAction R F
inst_7 : SMulCommClass 𝕜 R F
inst_8 : ContinuousConstSMul R F
c : R
inst_9 : Invertible c
hs : UniqueDiffWithinAt 𝕜 s x
h : ¬DifferentiableWithinAt 𝕜 f s x
⊢ fderivWithin 𝕜 (c • f) s x = HSMul.hSMul (β := E →L[𝕜] F) c (fderivWithin 𝕜 f s x)
have this : ¬DifferentiableWithinAt 𝕜 (c • f) s x
Tactic: have : ¬DifferentiableWithinAt 𝕜 (c • f) s x := by
      contrapose h
      exact (differentiableWithinAt_smul_iff c).mp h
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Add (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
x : E
R : Type u_4
inst_5 : Monoid R
inst_6 : DistribMulAction R F
inst_7 : SMulCommClass 𝕜 R F
inst_8 : ContinuousConstSMul R F
c : R
inst_9 : Invertible c
⊢ DifferentiableAt 𝕜 (c • f) x ↔ DifferentiableAt 𝕜 f x
have rw : DifferentiableWithinAt 𝕜 (c • f) Set.univ x ↔ DifferentiableAt 𝕜 f x
Tactic: rw [← differentiableWithinAt_univ, differentiableWithinAt_smul_iff, differentiableWithinAt_univ]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Add (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
x : E
R : Type u_4
inst_5 : Monoid R
inst_6 : DistribMulAction R F
inst_7 : SMulCommClass 𝕜 R F
inst_8 : ContinuousConstSMul R F
c : R
inst_9 : Invertible c
rw : DifferentiableWithinAt 𝕜 (c • f) Set.univ x ↔ DifferentiableAt 𝕜 f x
⊢ DifferentiableAt 𝕜 (c • f) x ↔ DifferentiableAt 𝕜 f x
have rw₁ : DifferentiableWithinAt 𝕜 f Set.univ x ↔ DifferentiableAt 𝕜 f x
Tactic: rw [← differentiableWithinAt_univ, differentiableWithinAt_smul_iff, differentiableWithinAt_univ]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Add (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
x : E
R : Type u_4
inst_5 : Monoid R
inst_6 : DistribMulAction R F
inst_7 : SMulCommClass 𝕜 R F
inst_8 : ContinuousConstSMul R F
c : R
inst_9 : Invertible c
rw : DifferentiableWithinAt 𝕜 (c • f) Set.univ x ↔ DifferentiableAt 𝕜 f x
rw₁ : DifferentiableWithinAt 𝕜 f Set.univ x ↔ DifferentiableAt 𝕜 f x
⊢ DifferentiableAt 𝕜 (c • f) x ↔ DifferentiableAt 𝕜 f x
have rw₂ : DifferentiableAt 𝕜 f x ↔ DifferentiableAt 𝕜 f x
Tactic: rw [← differentiableWithinAt_univ, differentiableWithinAt_smul_iff, differentiableWithinAt_univ]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Add (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
x : E
s : Set E
R : Type u_4
inst_5 : DivisionSemiring R
inst_6 : Module R F
inst_7 : SMulCommClass 𝕜 R F
inst_8 : ContinuousConstSMul R F
c : R
hs : UniqueDiffWithinAt 𝕜 s x
⊢ fderivWithin 𝕜 (c • f) s x = HSMul.hSMul (β := E →L[𝕜] F) c (fderivWithin 𝕜 f s x)
have inl : fderivWithin 𝕜 (HSMul.hSMul (α := R) 0 f) s x = HSMul.hSMul (α := R) (β := E →L[𝕜] F) 0 (fderivWithin 𝕜 f s x)
Tactic: obtain (rfl | ha) := eq_or_ne c 0
Cleared hypotheses: c
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Add (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
x : E
s : Set E
R : Type u_4
inst_5 : DivisionSemiring R
inst_6 : Module R F
inst_7 : SMulCommClass 𝕜 R F
inst_8 : ContinuousConstSMul R F
c : R
hs : UniqueDiffWithinAt 𝕜 s x
inl : fderivWithin 𝕜 (HSMul.hSMul (α := R) 0 f) s x = HSMul.hSMul (α := R) (β := E →L[𝕜] F) 0 (fderivWithin 𝕜 f s x)
⊢ fderivWithin 𝕜 (c • f) s x = HSMul.hSMul (β := E →L[𝕜] F) c (fderivWithin 𝕜 f s x)
have inr : ∀ (ha : c ≠ 0), fderivWithin 𝕜 (c • f) s x = HSMul.hSMul (β := E →L[𝕜] F) c (fderivWithin 𝕜 f s x)
Tactic: obtain (rfl | ha) := eq_or_ne c 0
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Add (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
x : E
s : Set E
R : Type u_4
inst_5 : DivisionSemiring R
inst_6 : Module R F
inst_7 : SMulCommClass 𝕜 R F
inst_8 : ContinuousConstSMul R F
c : R
hs : UniqueDiffWithinAt 𝕜 s x
ha : c ≠ 0
⊢ fderivWithin 𝕜 (c • f) s x = HSMul.hSMul (β := E →L[𝕜] F) c (fderivWithin 𝕜 f s x)
have inr : ∀ (this : Invertible c), fderivWithin 𝕜 (c • f) s x = HSMul.hSMul (β := E →L[𝕜] F) c (fderivWithin 𝕜 f s x)
Tactic: have : Invertible c := invertibleOfNonzero ha
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Add (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_3
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
R : Type u_4
inst_3 : DivisionSemiring R
inst_4 : Module R F
inst_5 : SMulCommClass 𝕜 R F
inst_6 : ContinuousConstSMul R F
s : Set 𝕜
f : 𝕜 → F
x : 𝕜
c : R
⊢ fderivWithin 𝕜 (c • f) s x = HSMul.hSMul (β := 𝕜 →L[𝕜] F) c (fderivWithin 𝕜 f s x : 𝕜 →L[𝕜] F)
have pos : ∀ (hsx : UniqueDiffWithinAt 𝕜 s x),
  fderivWithin 𝕜 (c • f) s x = HSMul.hSMul (β := 𝕜 →L[𝕜] F) c (fderivWithin 𝕜 f s x : 𝕜 →L[𝕜] F)
Tactic: by_cases hsx : UniqueDiffWithinAt 𝕜 s x
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Add (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_3
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
R : Type u_4
inst_3 : DivisionSemiring R
inst_4 : Module R F
inst_5 : SMulCommClass 𝕜 R F
inst_6 : ContinuousConstSMul R F
s : Set 𝕜
f : 𝕜 → F
x : 𝕜
c : R
pos :
  ∀ (hsx : UniqueDiffWithinAt 𝕜 s x),
    fderivWithin 𝕜 (c • f) s x = HSMul.hSMul (β := 𝕜 →L[𝕜] F) c (fderivWithin 𝕜 f s x : 𝕜 →L[𝕜] F)
⊢ fderivWithin 𝕜 (c • f) s x = HSMul.hSMul (β := 𝕜 →L[𝕜] F) c (fderivWithin 𝕜 f s x : 𝕜 →L[𝕜] F)
have neg : ∀ (hsx : ¬UniqueDiffWithinAt 𝕜 s x),
  fderivWithin 𝕜 (c • f) s x = HSMul.hSMul (β := 𝕜 →L[𝕜] F) c (fderivWithin 𝕜 f s x : 𝕜 →L[𝕜] F)
Tactic: by_cases hsx : UniqueDiffWithinAt 𝕜 s x
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Add (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
R : Type u_4
inst_5 : DivisionSemiring R
inst_6 : Module R F
inst_7 : SMulCommClass 𝕜 R F
inst_8 : ContinuousConstSMul R F
c : R
⊢ fderiv 𝕜 (c • f) = HSMul.hSMul (β := (x : E) → E →L[𝕜] F) c (fderiv 𝕜 f)
have simp_rw : fderivWithin 𝕜 (c • f) Set.univ = HSMul.hSMul (β := (x : E) → E →L[𝕜] F) c (fderivWithin 𝕜 f Set.univ)
Tactic: simp_rw [← fderivWithin_univ]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Add (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
R : Type u_4
inst_5 : DivisionSemiring R
inst_6 : Module R F
inst_7 : SMulCommClass 𝕜 R F
inst_8 : ContinuousConstSMul R F
c : R
⊢ fderivWithin 𝕜 (c • f) Set.univ = HSMul.hSMul (β := (x : E) → E →L[𝕜] F) c (fderivWithin 𝕜 f Set.univ)
have h : ∀ (x x_1 : E),
  Eq.{u_3 + 1} (α := F) ((fderivWithin 𝕜 (c • f) Set.univ x : (a : E) → F) x_1 : F)
    ((HSMul.hSMul (β := (x : E) → E →L[𝕜] F) c (fderivWithin 𝕜 f Set.univ) x : (a : E) → F) x_1 : F)
Tactic: ext x
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Add (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
x : E
ι : Type u_4
u : Finset ι
A : ι → E → F
A' : ι → E →L[𝕜] F
h : ∀ i ∈ u, HasStrictFDerivAt (A i) (A' i) x
⊢ HasStrictFDerivAt.{u_1, u_2, u_3} (𝕜 := 𝕜) (F := F) (fun (y : E) ↦ ∑ i ∈ u, A i y) (∑ i ∈ u, A' i) x
have simp : ∀
  (h :
    ∀ i ∈ u,
      IsLittleO.{u_2, u_3, u_2} (E := F) (F := E) (nhds (x, x))
        (fun (p : E × E) ↦ HSub.hSub (β := F) (A i p.1 - A i p.2) ((A' i : (a : E) → F) (p.1 - p.2) : F))
        fun (p : E × E) ↦ p.1 - p.2),
  IsLittleO.{u_2, u_3, u_2} (E := F) (F := E) (nhds (x, x))
    (fun (p : E × E) ↦
      HSub.hSub (β := F) (HSub.hSub (α := F) (∑ i ∈ u, A i p.1) (∑ i ∈ u, A i p.2))
        ((∑ i ∈ u, A' i : (a : E) → F) (p.1 - p.2) : F))
    fun (p : E × E) ↦ p.1 - p.2
Tactic: simp only [hasStrictFDerivAt_iff_isLittleO] at *
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Add (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
x : E
ι : Type u_4
u : Finset ι
A : ι → E → F
A' : ι → E →L[𝕜] F
h :
  ∀ i ∈ u,
    IsLittleO.{u_2, u_3, u_2} (E := F) (F := E) (nhds (x, x))
      (fun (p : E × E) ↦ HSub.hSub (β := F) (A i p.1 - A i p.2) ((A' i : (a : E) → F) (p.1 - p.2) : F))
      fun (p : E × E) ↦ p.1 - p.2
⊢ IsLittleO.{u_2, u_3, u_2} (E := F) (F := E) (nhds (x, x))
    (fun (p : E × E) ↦
      HSub.hSub (β := F) (HSub.hSub (α := F) (∑ i ∈ u, A i p.1) (∑ i ∈ u, A i p.2))
        ((∑ i ∈ u, A' i : (a : E) → F) (p.1 - p.2) : F))
    fun (p : E × E) ↦ p.1 - p.2
have h₁ : ∀ (x : E × E),
  HSub.hSub (β := F) (HSub.hSub (α := F) (∑ i ∈ u, A i x.1) (∑ i ∈ u, A i x.2))
      ((∑ i ∈ u, A' i : (a : E) → F) (x.1 - x.2) : F) =
    ∑ i ∈ u, HSub.hSub (β := F) (A i x.1 - A i x.2) ((A' i : (a : E) → F) (x.1 - x.2) : F)
Tactic: convert! IsLittleO.sum h
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Add (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
x : E
ι : Type u_4
u : Finset ι
A : ι → E → F
A' : ι → E →L[𝕜] F
h : ∀ i ∈ u, HasStrictFDerivAt (A i) (A' i) x
⊢ HasStrictFDerivAt.{u_1, u_2, u_3} (𝕜 := 𝕜) (F := F) (∑ i ∈ u, A i) (∑ i ∈ u, A' i) x
have h₁ : ∀ (x : E), Eq.{u_3 + 1} (α := F) ((∑ i ∈ u, A i) x) (∑ i ∈ u, A i x)
Tactic: convert! HasStrictFDerivAt.fun_sum h
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Add (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
L : Filter (E × E)
ι : Type u_4
u : Finset ι
A : ι → E → F
A' : ι → E →L[𝕜] F
h : ∀ i ∈ u, HasFDerivAtFilter (A i) (A' i) L
⊢ HasFDerivAtFilter.{u_1, u_2, u_3} (𝕜 := 𝕜) (F := F) (fun (y : E) ↦ ∑ i ∈ u, A i y) (∑ i ∈ u, A' i) L
have simp : ∀
  (h :
    ∀ i ∈ u,
      IsLittleO.{u_2, u_3, u_2} (E := F) (F := E) L
        (fun (p : E × E) ↦ HSub.hSub (β := F) (A i p.1 - A i p.2) ((A' i : (a : E) → F) (p.1 - p.2) : F))
        fun (p : E × E) ↦ p.1 - p.2),
  IsLittleO.{u_2, u_3, u_2} (E := F) (F := E) L
    (fun (p : E × E) ↦
      HSub.hSub (β := F) (HSub.hSub (α := F) (∑ i ∈ u, A i p.1) (∑ i ∈ u, A i p.2))
        ((∑ i ∈ u, A' i : (a : E) → F) (p.1 - p.2) : F))
    fun (p : E × E) ↦ p.1 - p.2
Tactic: simp only [hasFDerivAtFilter_iff_isLittleO] at *
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Add (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
L : Filter (E × E)
ι : Type u_4
u : Finset ι
A : ι → E → F
A' : ι → E →L[𝕜] F
h :
  ∀ i ∈ u,
    IsLittleO.{u_2, u_3, u_2} (E := F) (F := E) L
      (fun (p : E × E) ↦ HSub.hSub (β := F) (A i p.1 - A i p.2) ((A' i : (a : E) → F) (p.1 - p.2) : F))
      fun (p : E × E) ↦ p.1 - p.2
⊢ IsLittleO.{u_2, u_3, u_2} (E := F) (F := E) L
    (fun (p : E × E) ↦
      HSub.hSub (β := F) (HSub.hSub (α := F) (∑ i ∈ u, A i p.1) (∑ i ∈ u, A i p.2))
        ((∑ i ∈ u, A' i : (a : E) → F) (p.1 - p.2) : F))
    fun (p : E × E) ↦ p.1 - p.2
have h₁ : ∀ (x : E × E),
  HSub.hSub (β := F) (HSub.hSub (α := F) (∑ i ∈ u, A i x.1) (∑ i ∈ u, A i x.2))
      ((∑ i ∈ u, A' i : (a : E) → F) (x.1 - x.2) : F) =
    ∑ i ∈ u, HSub.hSub (β := F) (A i x.1 - A i x.2) ((A' i : (a : E) → F) (x.1 - x.2) : F)
Tactic: convert! IsLittleO.sum h
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Add (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
L : Filter (E × E)
ι : Type u_4
u : Finset ι
A : ι → E → F
A' : ι → E →L[𝕜] F
h : ∀ i ∈ u, HasFDerivAtFilter (A i) (A' i) L
⊢ HasFDerivAtFilter.{u_1, u_2, u_3} (𝕜 := 𝕜) (F := F) (∑ i ∈ u, A i) (∑ i ∈ u, A' i) L
have h₁ : ∀ (x : E), Eq.{u_3 + 1} (α := F) ((∑ i ∈ u, A i) x) (∑ i ∈ u, A i x)
Tactic: convert! HasFDerivAtFilter.fun_sum h
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Add (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
x : E
s : Set E
hxs : UniqueDiffWithinAt 𝕜 s x
⊢ Eq (α := E →L[𝕜] F) (fderivWithin 𝕜 (fun (y : E) ↦ -f y) s x) (-fderivWithin 𝕜 f s x)
have pos : ∀ (h : DifferentiableWithinAt 𝕜 f s x),
  Eq (α := E →L[𝕜] F) (fderivWithin 𝕜 (fun (y : E) ↦ -f y) s x) (-fderivWithin 𝕜 f s x)
Tactic: by_cases h : DifferentiableWithinAt 𝕜 f s x
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Add (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
x : E
s : Set E
hxs : UniqueDiffWithinAt 𝕜 s x
pos :
  ∀ (h : DifferentiableWithinAt 𝕜 f s x),
    Eq (α := E →L[𝕜] F) (fderivWithin 𝕜 (fun (y : E) ↦ -f y) s x) (-fderivWithin 𝕜 f s x)
⊢ Eq (α := E →L[𝕜] F) (fderivWithin 𝕜 (fun (y : E) ↦ -f y) s x) (-fderivWithin 𝕜 f s x)
have neg : ∀ (h : ¬DifferentiableWithinAt 𝕜 f s x),
  Eq (α := E →L[𝕜] F) (fderivWithin 𝕜 (fun (y : E) ↦ -f y) s x) (-fderivWithin 𝕜 f s x)
Tactic: by_cases h : DifferentiableWithinAt 𝕜 f s x