mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Analytic.Constructions

Goal state before:
pp: 𝕜 : Type u_2
inst✝² : NontriviallyNormedField 𝕜
A : Type u_7
inst✝¹ : NormedRing A
inst✝ : NormedAlgebra 𝕜 A
⊢ 1 ≤ (formalMultilinearSeries_geometric 𝕜 A).radius

Tactic:
convert!
    formalMultilinearSeries_geometric_eq_ofScalars 𝕜 A ▸
      FormalMultilinearSeries.inv_le_ofScalars_radius_of_tendsto A _ one_ne_zero (by simp)

Goal state after:
𝕜 : Type u_2
inst✝² : NontriviallyNormedField 𝕜
A : Type u_7
inst✝¹ : NormedRing A
inst✝ : NormedAlgebra 𝕜 A
⊢ 1 = ↑1⁻¹
Module: Mathlib.Analysis.Analytic.Inverse

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : OpenPartialHomeomorph E F
a : E
i : E ≃L[𝕜] F
h0 : a ∈ f.source
p : FormalMultilinearSeries 𝕜 E F
h : HasFPowerSeriesAt (↑f) p a
hp : p 1 = (continuousMultilinearCurryFin1 𝕜 E F).symm ↑i
A : HasFPowerSeriesAt (↑f.symm ∘ ↑f) ((p.leftInv i a).comp p) a
⊢ ∀ᶠ (y : E) in 𝓝 0, HasSum (fun n ↦ (p.leftInv i a n) fun x ↦ ↑f (a + y) - ↑f a) (↑f.symm (↑f (a + y)))

Tactic:
simpa using! A.eventually_hasSum_of_comp h (radius_leftInv_pos_of_radius_pos h.radius_pos hp)

Goal state after:
Module: Mathlib.Analysis.Calculus.FDeriv.Add

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
F : Type u_3
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
R : Type u_4
inst✝³ : DivisionSemiring R
inst✝² : Module R F
inst✝¹ : SMulCommClass 𝕜 R F
inst✝ : ContinuousConstSMul R F
s : Set 𝕜
f : 𝕜 → F
x : 𝕜
c : R
⊢ fderivWithin 𝕜 (c • f) s x = c • fderivWithin 𝕜 f s x

Tactic:
by_cases hsx : UniqueDiffWithinAt 𝕜 s x

Goal state after:
case pos
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
F : Type u_3
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
R : Type u_4
inst✝³ : DivisionSemiring R
inst✝² : Module R F
inst✝¹ : SMulCommClass 𝕜 R F
inst✝ : ContinuousConstSMul R F
s : Set 𝕜
f : 𝕜 → F
x : 𝕜
c : R
hsx : UniqueDiffWithinAt 𝕜 s x
⊢ fderivWithin 𝕜 (c • f) s x = c • fderivWithin 𝕜 f s x

case neg
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
F : Type u_3
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
R : Type u_4
inst✝³ : DivisionSemiring R
inst✝² : Module R F
inst✝¹ : SMulCommClass 𝕜 R F
inst✝ : ContinuousConstSMul R F
s : Set 𝕜
f : 𝕜 → F
x : 𝕜
c : R
hsx : ¬UniqueDiffWithinAt 𝕜 s x
⊢ fderivWithin 𝕜 (c • f) s x = c • fderivWithin 𝕜 f s x
Module: Mathlib.Topology.Algebra.Module.Alternating.Basic

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_4
ι : Type u_6
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : TopologicalSpace M
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
inst✝ : TopologicalSpace N
f g : M [⋀^ι]→L[R] N
h : f.toAlternatingMap = g.toAlternatingMap
⊢ ⇑f = ⇑g

Tactic:
by convert! DFunLike.ext'_iff.1 h

Goal state after:
Module: Mathlib.Analysis.Calculus.FDeriv.Equiv

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
iso : E ≃L[𝕜] F
f : F → G
x : E
⊢ UniqueDiffWithinAt 𝕜 (⇑iso ⁻¹' univ) x

Tactic:
exact uniqueDiffWithinAt_univ

Goal state after:
Module: Mathlib.Topology.MetricSpace.Completion

Goal state before:
pp: case refine_2
α : Type u
inst✝ : PseudoMetricSpace α
x y z : Completion α
a b c : α
⊢ dist a c ≤ dist a b + dist ↑b ↑c

Tactic:
Completion.dist_eq

Goal state after:
case refine_2
α : Type u
inst✝ : PseudoMetricSpace α
x y z : Completion α
a b c : α
⊢ dist a c ≤ dist a b + dist b c
Module: Mathlib.Topology.MetricSpace.Completion

Goal state before:
pp: case refine_2
α : Type u
inst✝ : PseudoMetricSpace α
s : Set (Completion α × Completion α)
hs : s ∈ 𝓤 (Completion α)
t : Set (Completion α × Completion α)
ht : t ∈ 𝓤 (Completion α)
tclosed : IsClosed t
ts : t ⊆ s
A : {x | (↑x.1, ↑x.2) ∈ t} ∈ 𝓤 α
ε : ℝ
εpos : ε > 0
hε : ∀ ⦃a b : α⦄, dist a b < ε → (a, b) ∈ {x | (↑x.1, ↑x.2) ∈ t}
x✝ y✝ : Completion α
hxy : dist x✝ y✝ < ε
x y : α
⊢ ε ≤ dist ↑x ↑y ∨ (↑x, ↑y) ∈ t

Tactic:
Completion.dist_eq

Goal state after:
case refine_2
α : Type u
inst✝ : PseudoMetricSpace α
s : Set (Completion α × Completion α)
hs : s ∈ 𝓤 (Completion α)
t : Set (Completion α × Completion α)
ht : t ∈ 𝓤 (Completion α)
tclosed : IsClosed t
ts : t ⊆ s
A : {x | (↑x.1, ↑x.2) ∈ t} ∈ 𝓤 α
ε : ℝ
εpos : ε > 0
hε : ∀ ⦃a b : α⦄, dist a b < ε → (a, b) ∈ {x | (↑x.1, ↑x.2) ∈ t}
x✝ y✝ : Completion α
hxy : dist x✝ y✝ < ε
x y : α
⊢ ε ≤ dist x y ∨ (↑x, ↑y) ∈ t
Module: Mathlib.Topology.MetricSpace.Completion

Goal state before:
pp: case mpr
α : Type u
inst✝ : PseudoMetricSpace α
s : Set (Completion α × Completion α)
⊢ (∃ ε > 0, ∀ {a b : Completion α}, dist a b < ε → (a, b) ∈ s) → s ∈ 𝓤 (Completion α)

Tactic:
rintro ⟨ε, εpos, hε⟩
    let r : Set (ℝ × ℝ) := { p | dist p.1 p.2 < ε }
    have : r ∈ uniformity ℝ := Metric.dist_mem_uniformity εpos
    have T := uniformContinuous_def.1 (@Completion.uniformContinuous_dist α _) r this
    simp only [uniformity_prod_eq_prod, mem_prod_iff, Filter.mem_map] at T
    rcases T with ⟨t1, ht1, t2, ht2, ht⟩
    refine mem_of_superset ht1 ?_
    have A : ∀ a b : Completion α, (a, b) ∈ t1 → dist a b < ε := by
      intro a b hab
      have : ((a, b), (a, a)) ∈ t1 ×ˢ t2 := ⟨hab, refl_mem_uniformity ht2⟩
      exact lt_of_le_of_lt (le_abs_self _)
        (by simpa [r, Completion.dist_self, Real.dist_eq, Completion.dist_comm] using ht this)
    grind

Goal state after:
Module: Mathlib.Topology.MetricSpace.Completion

Goal state before:
pp: case ih
α : Type u
β : Type v
inst✝⁵ : PseudoMetricSpace α
M : Type u_1
inst✝⁴ : Zero M
inst✝³ : Zero α
inst✝² : SMul M α
inst✝¹ : PseudoMetricSpace M
inst✝ : IsBoundedSMul M α
c : M
x₁ x₂ : α
⊢ dist (c • x₁) (c • x₂) ≤ dist c 0 * dist ↑x₁ ↑x₂

Tactic:
Completion.dist_eq

Goal state after:
case ih
α : Type u
β : Type v
inst✝⁵ : PseudoMetricSpace α
M : Type u_1
inst✝⁴ : Zero M
inst✝³ : Zero α
inst✝² : SMul M α
inst✝¹ : PseudoMetricSpace M
inst✝ : IsBoundedSMul M α
c : M
x₁ x₂ : α
⊢ dist (c • x₁) (c • x₂) ≤ dist c 0 * dist x₁ x₂
Module: Mathlib.Topology.MetricSpace.Completion

Goal state before:
pp: case ih
α : Type u
β : Type v
inst✝⁵ : PseudoMetricSpace α
M : Type u_1
inst✝⁴ : Zero M
inst✝³ : Zero α
inst✝² : SMul M α
inst✝¹ : PseudoMetricSpace M
inst✝ : IsBoundedSMul M α
c₁ c₂ : M
x : α
⊢ dist (c₁ • x) (c₂ • x) ≤ dist c₁ c₂ * dist ↑x ↑0

Tactic:
Completion.dist_eq

Goal state after:
case ih
α : Type u
β : Type v
inst✝⁵ : PseudoMetricSpace α
M : Type u_1
inst✝⁴ : Zero M
inst✝³ : Zero α
inst✝² : SMul M α
inst✝¹ : PseudoMetricSpace M
inst✝ : IsBoundedSMul M α
c₁ c₂ : M
x : α
⊢ dist (c₁ • x) (c₂ • x) ≤ dist c₁ c₂ * dist x 0
Module: Mathlib.Analysis.Calculus.FDeriv.CompCLM

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
G : Type u_4
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
x : E
s : Set E
ι : Type u_5
c : E → F [⋀^ι]→L[𝕜] G
inst✝ : Finite ι
hxs : UniqueDiffWithinAt 𝕜 s x
hc : DifferentiableWithinAt 𝕜 c s x
u : ι → F
m : E
⊢ (fderivWithin 𝕜 (fun y ↦ (c y) u) s x) m = ((fderivWithin 𝕜 c s x) m) u

Tactic:
by
  have := Fintype.ofFinite ι
  simp [fderivWithin_continuousAlternatingMap_apply_const hxs hc]

Goal state after:
Module: Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries

Goal state before:
pp: case fderivWithin.zero
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
p : E → FormalMultilinearSeries 𝕜 E F
n : ℕ
Hzero_eq : ∀ x ∈ s, (p x 0).curry0 = f x
Hfderiv_zero : ∀ x ∈ s, HasFDerivWithinAt (fun y ↦ p y 0) (p x 1).curryLeft s x
Htaylor : HasFTaylorSeriesUpToOn (↑n) (fun x ↦ (continuousMultilinearCurryFin1 𝕜 E F) (p x 1)) (fun x ↦ (p x).shift) s
x : E
hx : x ∈ s
hm : ↑0 < ↑n.succ
⊢ HasFDerivWithinAt (fun x ↦ p x 0) (p x (Nat.succ 0)).curryLeft s x

Tactic:
exact Hfderiv_zero x hx

Goal state after:
Module: Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries

Goal state before:
pp: case refine_1
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
N : ℕ∞ω
p : E → FormalMultilinearSeries 𝕜 E F
hN : ∞ ≤ N
h : HasFTaylorSeriesUpToOn N f p s
⊢ (∀ x ∈ s, (p x 0).curry0 = f x) ∧
    (∀ x ∈ s, HasFDerivWithinAt (fun y ↦ p y 0) (p x 1).curryLeft s x) ∧
      HasFTaylorSeriesUpToOn N (fun x ↦ (continuousMultilinearCurryFin1 𝕜 E F) (p x 1)) (fun x ↦ (p x).shift) s

pp: case refine_2
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
N : ℕ∞ω
p : E → FormalMultilinearSeries 𝕜 E F
hN : ∞ ≤ N
h :
  (∀ x ∈ s, (p x 0).curry0 = f x) ∧
    (∀ x ∈ s, HasFDerivWithinAt (fun y ↦ p y 0) (p x 1).curryLeft s x) ∧
      HasFTaylorSeriesUpToOn N (fun x ↦ (continuousMultilinearCurryFin1 𝕜 E F) (p x 1)) (fun x ↦ (p x).shift) s
⊢ HasFTaylorSeriesUpToOn N f p s

Tactic:
· rw [hasFTaylorSeriesUpToOn_top_iff_add hN 1] at h
    rw [hasFTaylorSeriesUpToOn_top_iff hN]
    exact ⟨(hasFTaylorSeriesUpToOn_succ_nat_iff_right.1 (h 1)).1,
      (hasFTaylorSeriesUpToOn_succ_nat_iff_right.1 (h 1)).2.1,
      fun n ↦ (hasFTaylorSeriesUpToOn_succ_nat_iff_right.1 (h n)).2.2⟩

Goal state after:
case refine_2
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
N : ℕ∞ω
p : E → FormalMultilinearSeries 𝕜 E F
hN : ∞ ≤ N
h :
  (∀ x ∈ s, (p x 0).curry0 = f x) ∧
    (∀ x ∈ s, HasFDerivWithinAt (fun y ↦ p y 0) (p x 1).curryLeft s x) ∧
      HasFTaylorSeriesUpToOn N (fun x ↦ (continuousMultilinearCurryFin1 𝕜 E F) (p x 1)) (fun x ↦ (p x).shift) s
⊢ HasFTaylorSeriesUpToOn N f p s
Module: Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries

Goal state before:
pp: 𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
x : E
n : ℕ
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
m : Fin (n + 1) → E
⊢ (iteratedFDerivWithin 𝕜 (n + 1) f s x) m =
    ((iteratedFDerivWithin 𝕜 n (fun y ↦ fderivWithin 𝕜 f s y) s x) (init m)) (m (last n))

Tactic:
induction n generalizing x with
  | zero =>
    rw [iteratedFDerivWithin_succ_eq_comp_left, iteratedFDerivWithin_zero_eq_comp,
      iteratedFDerivWithin_zero_apply, Function.comp_apply,
      LinearIsometryEquiv.comp_fderivWithin _ (hs x hx)]
    simp
  | succ n IH =>
    let I := (continuousMultilinearCurryRightEquiv' 𝕜 n E F).symm
    have A : ∀ y ∈ s, iteratedFDerivWithin 𝕜 n.succ f s y =
        (I ∘ iteratedFDerivWithin 𝕜 n (fun y => fderivWithin 𝕜 f s y) s) y := fun y hy ↦ by
      ext m
      simp [IH hy m, I]
    calc
      (iteratedFDerivWithin 𝕜 (n + 2) f s x : (Fin (n + 2) → E) → F) m =
          (fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 n.succ f s) s x : E → E [×n + 1]→L[𝕜] F) (m 0)
            (tail m) := by
        simp [iteratedFDerivWithin_succ_eq_comp_left]
      _ = (fderivWithin 𝕜 (I ∘ iteratedFDerivWithin 𝕜 n (fderivWithin 𝕜 f s) s) s x :
              E → E [×n + 1]→L[𝕜] F) (m 0) (tail m) := by
        rw [fderivWithin_congr A (A x hx)]
      _ = (I ∘ fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 n (fderivWithin 𝕜 f s) s) s x :
              E → E [×n + 1]→L[𝕜] F) (m 0) (tail m) := by
        simp [LinearIsometryEquiv.comp_fderivWithin _ (hs x hx)]
      _ = (fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 n (fun y => fderivWithin 𝕜 f s y) s) s x :
              E → E [×n]→L[𝕜] E →L[𝕜] F) (m 0) (init (tail m)) ((tail m) (last n)) := by
        simp [I]
      _ = iteratedFDerivWithin 𝕜 (Nat.succ n) (fun y => fderivWithin 𝕜 f s y) s x (init m)
            (m (last (n + 1))) := by
        rw [iteratedFDerivWithin_succ_apply_left, tail_init_eq_init_tail]
        simp [init, tail]

Goal state after:
Module: Mathlib.Analysis.Calculus.FDeriv.Analytic

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0∞
f : E → F
x : E
s : Set E
inst✝ : CompleteSpace F
h : HasFPowerSeriesWithinOnBall f p s x r
⊢ DifferentiableOn 𝕜 f (insert x s ∩ Metric.eball x r)

Tactic:
intro y hy
  have Z := (h.analyticWithinAt_of_mem hy).differentiableWithinAt
  rcases eq_or_ne y x with rfl | hy
  · exact Z.mono inter_subset_left
  · apply (Z.mono (subset_insert _ _)).mono_of_mem_nhdsWithin
    suffices s ∈ 𝓝[insert x s] y from nhdsWithin_mono _ inter_subset_left this
    rw [nhdsWithin_insert_of_ne hy]
    exact self_mem_nhdsWithin

Goal state after:
Module: Mathlib.Analysis.Calculus.Deriv.Mul

Goal state before:
pp: 𝕜 : Type u
inst✝⁶ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
E : Type w
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
G : Type u_1
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
x : 𝕜
s : Set 𝕜
B : E →L[𝕜] F →L[𝕜] G
u : 𝕜 → E
v : 𝕜 → F
hu : DifferentiableWithinAt 𝕜 u s x
hv : DifferentiableWithinAt 𝕜 v s x
⊢ derivWithin (fun y ↦ (B (u y)) (v y)) s x = (B (u x)) (derivWithin v s x) + (B (derivWithin u s x)) (v x)

Tactic:
by_cases hsx : UniqueDiffWithinAt 𝕜 s x

Goal state after:
case pos
𝕜 : Type u
inst✝⁶ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
E : Type w
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
G : Type u_1
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
x : 𝕜
s : Set 𝕜
B : E →L[𝕜] F →L[𝕜] G
u : 𝕜 → E
v : 𝕜 → F
hu : DifferentiableWithinAt 𝕜 u s x
hv : DifferentiableWithinAt 𝕜 v s x
hsx : UniqueDiffWithinAt 𝕜 s x
⊢ derivWithin (fun y ↦ (B (u y)) (v y)) s x = (B (u x)) (derivWithin v s x) + (B (derivWithin u s x)) (v x)

case neg
𝕜 : Type u
inst✝⁶ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
E : Type w
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
G : Type u_1
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
x : 𝕜
s : Set 𝕜
B : E →L[𝕜] F →L[𝕜] G
u : 𝕜 → E
v : 𝕜 → F
hu : DifferentiableWithinAt 𝕜 u s x
hv : DifferentiableWithinAt 𝕜 v s x
hsx : ¬UniqueDiffWithinAt 𝕜 s x
⊢ derivWithin (fun y ↦ (B (u y)) (v y)) s x = (B (u x)) (derivWithin v s x) + (B (derivWithin u s x)) (v x)
Module: Mathlib.Analysis.Calculus.Deriv.Mul

Goal state before:
pp: 𝕜 : Type u
inst✝⁷ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜 F
f : 𝕜 → F
x : 𝕜
s : Set 𝕜
𝕜' : Type u_2
inst✝⁴ : NormedRing 𝕜'
inst✝³ : NormedAlgebra 𝕜 𝕜'
inst✝² : Module 𝕜' F
inst✝¹ : IsBoundedSMul 𝕜' F
inst✝ : IsScalarTower 𝕜 𝕜' F
c : 𝕜 → 𝕜'
hc : DifferentiableWithinAt 𝕜 c s x
hf : DifferentiableWithinAt 𝕜 f s x
⊢ derivWithin (fun y ↦ c y • f y) s x = c x • derivWithin f s x + derivWithin c s x • f x

Tactic:
by_cases hsx : UniqueDiffWithinAt 𝕜 s x

Goal state after:
case pos
𝕜 : Type u
inst✝⁷ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜 F
f : 𝕜 → F
x : 𝕜
s : Set 𝕜
𝕜' : Type u_2
inst✝⁴ : NormedRing 𝕜'
inst✝³ : NormedAlgebra 𝕜 𝕜'
inst✝² : Module 𝕜' F
inst✝¹ : IsBoundedSMul 𝕜' F
inst✝ : IsScalarTower 𝕜 𝕜' F
c : 𝕜 → 𝕜'
hc : DifferentiableWithinAt 𝕜 c s x
hf : DifferentiableWithinAt 𝕜 f s x
hsx : UniqueDiffWithinAt 𝕜 s x
⊢ derivWithin (fun y ↦ c y • f y) s x = c x • derivWithin f s x + derivWithin c s x • f x

case neg
𝕜 : Type u
inst✝⁷ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜 F
f : 𝕜 → F
x : 𝕜
s : Set 𝕜
𝕜' : Type u_2
inst✝⁴ : NormedRing 𝕜'
inst✝³ : NormedAlgebra 𝕜 𝕜'
inst✝² : Module 𝕜' F
inst✝¹ : IsBoundedSMul 𝕜' F
inst✝ : IsScalarTower 𝕜 𝕜' F
c : 𝕜 → 𝕜'
hc : DifferentiableWithinAt 𝕜 c s x
hf : DifferentiableWithinAt 𝕜 f s x
hsx : ¬UniqueDiffWithinAt 𝕜 s x
⊢ derivWithin (fun y ↦ c y • f y) s x = c x • derivWithin f s x + derivWithin c s x • f x
Module: Mathlib.Analysis.Calculus.Deriv.Mul

Goal state before:
pp: 𝕜 : Type u
inst✝⁷ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜 F
x : 𝕜
s : Set 𝕜
𝕜' : Type u_2
inst✝⁴ : NormedRing 𝕜'
inst✝³ : NormedAlgebra 𝕜 𝕜'
inst✝² : Module 𝕜' F
inst✝¹ : IsBoundedSMul 𝕜' F
inst✝ : IsScalarTower 𝕜 𝕜' F
c : 𝕜 → 𝕜'
hc : DifferentiableWithinAt 𝕜 c s x
f : F
⊢ derivWithin (fun y ↦ c y • f) s x = derivWithin c s x • f

Tactic:
by_cases hsx : UniqueDiffWithinAt 𝕜 s x

Goal state after:
case pos
𝕜 : Type u
inst✝⁷ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜 F
x : 𝕜
s : Set 𝕜
𝕜' : Type u_2
inst✝⁴ : NormedRing 𝕜'
inst✝³ : NormedAlgebra 𝕜 𝕜'
inst✝² : Module 𝕜' F
inst✝¹ : IsBoundedSMul 𝕜' F
inst✝ : IsScalarTower 𝕜 𝕜' F
c : 𝕜 → 𝕜'
hc : DifferentiableWithinAt 𝕜 c s x
f : F
hsx : UniqueDiffWithinAt 𝕜 s x
⊢ derivWithin (fun y ↦ c y • f) s x = derivWithin c s x • f

case neg
𝕜 : Type u
inst✝⁷ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜 F
x : 𝕜
s : Set 𝕜
𝕜' : Type u_2
inst✝⁴ : NormedRing 𝕜'
inst✝³ : NormedAlgebra 𝕜 𝕜'
inst✝² : Module 𝕜' F
inst✝¹ : IsBoundedSMul 𝕜' F
inst✝ : IsScalarTower 𝕜 𝕜' F
c : 𝕜 → 𝕜'
hc : DifferentiableWithinAt 𝕜 c s x
f : F
hsx : ¬UniqueDiffWithinAt 𝕜 s x
⊢ derivWithin (fun y ↦ c y • f) s x = derivWithin c s x • f
Module: Mathlib.Analysis.Calculus.Deriv.Mul

Goal state before:
pp: 𝕜 : Type u
inst✝⁶ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
f : 𝕜 → F
f' : F
L : Filter (𝕜 × 𝕜)
R : Type u_2
inst✝³ : Monoid R
inst✝² : DistribMulAction R F
inst✝¹ : SMulCommClass 𝕜 R F
inst✝ : ContinuousConstSMul R F
c : R
hf : HasDerivAtFilter f f' L
⊢ HasDerivAtFilter (c • f) (c • f') L

Tactic:
simpa using (HasFDerivAtFilter.const_smul hf c).hasDerivAtFilter

Goal state after:
Module: Mathlib.Analysis.Calculus.Deriv.Mul

Goal state before:
pp: 𝕜 : Type u
inst✝⁶ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
f : 𝕜 → F
x : 𝕜
s : Set 𝕜
R : Type u_2
inst✝³ : Monoid R
inst✝² : DistribMulAction R F
inst✝¹ : SMulCommClass 𝕜 R F
inst✝ : ContinuousConstSMul R F
c : R
hf : DifferentiableWithinAt 𝕜 f s x
⊢ derivWithin (fun y ↦ c • f y) s x = c • derivWithin f s x

Tactic:
by_cases hsx : UniqueDiffWithinAt 𝕜 s x

Goal state after:
case pos
𝕜 : Type u
inst✝⁶ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
f : 𝕜 → F
x : 𝕜
s : Set 𝕜
R : Type u_2
inst✝³ : Monoid R
inst✝² : DistribMulAction R F
inst✝¹ : SMulCommClass 𝕜 R F
inst✝ : ContinuousConstSMul R F
c : R
hf : DifferentiableWithinAt 𝕜 f s x
hsx : UniqueDiffWithinAt 𝕜 s x
⊢ derivWithin (fun y ↦ c • f y) s x = c • derivWithin f s x

case neg
𝕜 : Type u
inst✝⁶ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
f : 𝕜 → F
x : 𝕜
s : Set 𝕜
R : Type u_2
inst✝³ : Monoid R
inst✝² : DistribMulAction R F
inst✝¹ : SMulCommClass 𝕜 R F
inst✝ : ContinuousConstSMul R F
c : R
hf : DifferentiableWithinAt 𝕜 f s x
hsx : ¬UniqueDiffWithinAt 𝕜 s x
⊢ derivWithin (fun y ↦ c • f y) s x = c • derivWithin f s x
Module: Mathlib.Analysis.Calculus.Deriv.Mul

Goal state before:
pp: 𝕜 : Type u
inst✝⁶ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
x : 𝕜
s : Set 𝕜
𝕝 : Type u_3
inst✝³ : DivisionSemiring 𝕝
inst✝² : Module 𝕝 F
inst✝¹ : SMulCommClass 𝕜 𝕝 F
inst✝ : ContinuousConstSMul 𝕝 F
c : 𝕝
f : 𝕜 → F
⊢ derivWithin (fun y ↦ c • f y) s x = c • derivWithin f s x

Tactic:
by_cases hsx : UniqueDiffWithinAt 𝕜 s x

Goal state after:
case pos
𝕜 : Type u
inst✝⁶ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
x : 𝕜
s : Set 𝕜
𝕝 : Type u_3
inst✝³ : DivisionSemiring 𝕝
inst✝² : Module 𝕝 F
inst✝¹ : SMulCommClass 𝕜 𝕝 F
inst✝ : ContinuousConstSMul 𝕝 F
c : 𝕝
f : 𝕜 → F
hsx : UniqueDiffWithinAt 𝕜 s x
⊢ derivWithin (fun y ↦ c • f y) s x = c • derivWithin f s x

case neg
𝕜 : Type u
inst✝⁶ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
x : 𝕜
s : Set 𝕜
𝕝 : Type u_3
inst✝³ : DivisionSemiring 𝕝
inst✝² : Module 𝕝 F
inst✝¹ : SMulCommClass 𝕜 𝕝 F
inst✝ : ContinuousConstSMul 𝕝 F
c : 𝕝
f : 𝕜 → F
hsx : ¬UniqueDiffWithinAt 𝕜 s x
⊢ derivWithin (fun y ↦ c • f y) s x = c • derivWithin f s x
Module: Mathlib.Analysis.Calculus.Deriv.Mul

Goal state before:
pp: 𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
𝔸 : Type u_3
inst✝¹ : NormedRing 𝔸
inst✝ : NormedAlgebra 𝕜 𝔸
c d : 𝕜 → 𝔸
hc : DifferentiableWithinAt 𝕜 c s x
hd : DifferentiableWithinAt 𝕜 d s x
⊢ derivWithin (fun y ↦ c y * d y) s x = derivWithin c s x * d x + c x * derivWithin d s x

Tactic:
by_cases hsx : UniqueDiffWithinAt 𝕜 s x

Goal state after:
case pos
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
𝔸 : Type u_3
inst✝¹ : NormedRing 𝔸
inst✝ : NormedAlgebra 𝕜 𝔸
c d : 𝕜 → 𝔸
hc : DifferentiableWithinAt 𝕜 c s x
hd : DifferentiableWithinAt 𝕜 d s x
hsx : UniqueDiffWithinAt 𝕜 s x
⊢ derivWithin (fun y ↦ c y * d y) s x = derivWithin c s x * d x + c x * derivWithin d s x

case neg
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
𝔸 : Type u_3
inst✝¹ : NormedRing 𝔸
inst✝ : NormedAlgebra 𝕜 𝔸
c d : 𝕜 → 𝔸
hc : DifferentiableWithinAt 𝕜 c s x
hd : DifferentiableWithinAt 𝕜 d s x
hsx : ¬UniqueDiffWithinAt 𝕜 s x
⊢ derivWithin (fun y ↦ c y * d y) s x = derivWithin c s x * d x + c x * derivWithin d s x
Module: Mathlib.Analysis.Calculus.Deriv.Mul

Goal state before:
pp: 𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
𝔸 : Type u_3
inst✝¹ : NormedRing 𝔸
inst✝ : NormedAlgebra 𝕜 𝔸
c : 𝕜 → 𝔸
hc : DifferentiableWithinAt 𝕜 c s x
d : 𝔸
⊢ derivWithin (fun y ↦ c y * d) s x = derivWithin c s x * d

Tactic:
by_cases hsx : UniqueDiffWithinAt 𝕜 s x

Goal state after:
case pos
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
𝔸 : Type u_3
inst✝¹ : NormedRing 𝔸
inst✝ : NormedAlgebra 𝕜 𝔸
c : 𝕜 → 𝔸
hc : DifferentiableWithinAt 𝕜 c s x
d : 𝔸
hsx : UniqueDiffWithinAt 𝕜 s x
⊢ derivWithin (fun y ↦ c y * d) s x = derivWithin c s x * d

case neg
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
𝔸 : Type u_3
inst✝¹ : NormedRing 𝔸
inst✝ : NormedAlgebra 𝕜 𝔸
c : 𝕜 → 𝔸
hc : DifferentiableWithinAt 𝕜 c s x
d : 𝔸
hsx : ¬UniqueDiffWithinAt 𝕜 s x
⊢ derivWithin (fun y ↦ c y * d) s x = derivWithin c s x * d
Module: Mathlib.Analysis.Calculus.Deriv.Pow

Goal state before:
pp: 𝕜 : Type u_1
𝔸 : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedRing 𝔸
inst✝ : NormedAlgebra 𝕜 𝔸
f : 𝕜 → 𝔸
x : 𝕜
s : Set 𝕜
h : DifferentiableWithinAt 𝕜 f s x
n : ℕ
⊢ derivWithin (fun x ↦ f x ^ n) s x = ∑ i ∈ Finset.range n, f x ^ (n.pred - i) * derivWithin f s x * f x ^ i

Tactic:
by_cases hsx : UniqueDiffWithinAt 𝕜 s x

Goal state after:
case pos
𝕜 : Type u_1
𝔸 : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedRing 𝔸
inst✝ : NormedAlgebra 𝕜 𝔸
f : 𝕜 → 𝔸
x : 𝕜
s : Set 𝕜
h : DifferentiableWithinAt 𝕜 f s x
n : ℕ
hsx : UniqueDiffWithinAt 𝕜 s x
⊢ derivWithin (fun x ↦ f x ^ n) s x = ∑ i ∈ Finset.range n, f x ^ (n.pred - i) * derivWithin f s x * f x ^ i

case neg
𝕜 : Type u_1
𝔸 : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedRing 𝔸
inst✝ : NormedAlgebra 𝕜 𝔸
f : 𝕜 → 𝔸
x : 𝕜
s : Set 𝕜
h : DifferentiableWithinAt 𝕜 f s x
n : ℕ
hsx : ¬UniqueDiffWithinAt 𝕜 s x
⊢ derivWithin (fun x ↦ f x ^ n) s x = ∑ i ∈ Finset.range n, f x ^ (n.pred - i) * derivWithin f s x * f x ^ i