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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
H : Type u_5
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
inst✝¹ : NormedAddCommGroup H
inst✝ : NormedSpace 𝕜 H
r : FormalMultilinearSeries 𝕜 G H
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
⊢ (r.comp q).comp p = r.comp (q.comp p)

Tactic:
by
  ext n v
  /- First, rewrite the two compositions appearing in the theorem as two sums over complicated
    sigma types, as in the description of the proof above. -/
  let f : (Σ a : Composition n, Composition a.length) → H := fun c =>
    r c.2.length (applyComposition q c.2 (applyComposition p c.1 v))
  let g : (Σ c : Composition n, ∀ i : Fin c.length, Composition (c.blocksFun i)) → H := fun c =>
    r c.1.length fun i : Fin c.1.length =>
      q (c.2 i).length (applyComposition p (c.2 i) (v ∘ c.1.embedding i))
  suffices ∑ c, f c = ∑ c, g c by
    simpa +unfoldPartialApp only [FormalMultilinearSeries.comp, sum_apply,
      compAlongComposition_apply, Finset.sum_sigma', applyComposition,
      ContinuousMultilinearMap.map_sum]
  /- Now, we use `Composition.sigmaEquivSigmaPi n` to change
    variables in the second sum, and check that we get exactly the same sums. -/
  rw [← (sigmaEquivSigmaPi n).sum_comp]
  /- To check that we have the same terms, we should check that we apply the same component of
    `r`, and the same component of `q`, and the same component of `p`, to the same coordinate of
    `v`. This is true by definition, but at each step one needs to convince Lean that the types
    one considers are the same, using a suitable congruence lemma to avoid dependent type issues.
    This dance has to be done three times, one for `r`, one for `q` and one for `p`. -/
  apply Finset.sum_congr rfl
  rintro ⟨a, b⟩ _
  dsimp [sigmaEquivSigmaPi]
  -- check that the `r` components are the same. Based on `Composition.length_gather`
  apply r.congr (Composition.length_gather a b).symm
  intro i hi1 hi2
  -- check that the `q` components are the same. Based on `length_sigmaCompositionAux`
  apply q.congr (length_sigmaCompositionAux a b _).symm
  intro j hj1 hj2
  -- check that the `p` components are the same. Based on `blocksFun_sigmaCompositionAux`
  apply p.congr (blocksFun_sigmaCompositionAux a b _ _).symm
  intro k hk1 hk2
  -- finally, check that the coordinates of `v` one is using are the same. Based on
  -- `sizeUpTo_sizeUpTo_add`.
  refine congr_arg v (Fin.ext ?_)
  dsimp [Composition.embedding]
  rw [← add_assoc, ← sizeUpTo_sizeUpTo_add _ _ hi1 hj1]

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

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 : E → F
x : E
s : Set E
R : Type u_4
inst✝⁴ : Monoid R
inst✝³ : DistribMulAction R F
inst✝² : SMulCommClass 𝕜 R F
inst✝¹ : ContinuousConstSMul R F
c : R
inst✝ : Invertible c
⊢ DifferentiableWithinAt 𝕜 (c • f) s x ↔ DifferentiableWithinAt 𝕜 f s x

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ h.const_smul c⟩

Goal state after:
𝕜 : 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 : E → F
x : E
s : Set E
R : Type u_4
inst✝⁴ : Monoid R
inst✝³ : DistribMulAction R F
inst✝² : SMulCommClass 𝕜 R F
inst✝¹ : ContinuousConstSMul R F
c : R
inst✝ : Invertible c
h : DifferentiableWithinAt 𝕜 (c • f) s x
⊢ DifferentiableWithinAt 𝕜 f s x
Module: Mathlib.Analysis.Calculus.FDeriv.Prod

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
n : ℕ
F' : Fin n.succ → Type u_6
inst✝¹ : (i : Fin n.succ) → NormedAddCommGroup (F' i)
inst✝ : (i : Fin n.succ) → NormedSpace 𝕜 (F' i)
φ : E → F' 0
φs : E → (i : Fin n) → F' i.succ
φ' : E →L[𝕜] (i : Fin n.succ) → F' i
l : Filter (E × E)
⊢ HasFDerivAtFilter (fun x ↦ Fin.cons (φ x) (φs x)) φ' l ↔
    HasFDerivAtFilter φ (proj 0 ∘SL φ') l ∧ HasFDerivAtFilter φs (Pi.compRightL 𝕜 F' Fin.succ ∘SL φ') l

Tactic:
hasFDerivAtFilter_pi',

Goal state after:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
n : ℕ
F' : Fin n.succ → Type u_6
inst✝¹ : (i : Fin n.succ) → NormedAddCommGroup (F' i)
inst✝ : (i : Fin n.succ) → NormedSpace 𝕜 (F' i)
φ : E → F' 0
φs : E → (i : Fin n) → F' i.succ
φ' : E →L[𝕜] (i : Fin n.succ) → F' i
l : Filter (E × E)
⊢ (∀ (i : Fin (n + 1)), HasFDerivAtFilter (fun x ↦ Fin.cons (φ x) (φs x) i) (proj i ∘SL φ') l) ↔
    HasFDerivAtFilter φ (proj 0 ∘SL φ') l ∧ HasFDerivAtFilter φs (Pi.compRightL 𝕜 F' Fin.succ ∘SL φ') l
Module: Mathlib.Analysis.Calculus.FDeriv.Prod

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
n : ℕ
F' : Fin n.succ → Type u_6
inst✝¹ : (i : Fin n.succ) → NormedAddCommGroup (F' i)
inst✝ : (i : Fin n.succ) → NormedSpace 𝕜 (F' i)
φ : E → F' 0
φs : E → (i : Fin n) → F' i.succ
φ' : E →L[𝕜] (i : Fin n.succ) → F' i
l : Filter (E × E)
⊢ HasFDerivAtFilter (fun x ↦ Fin.cons (φ x) (φs x)) φ' l ↔
    HasFDerivAtFilter φ (proj 0 ∘SL φ') l ∧ HasFDerivAtFilter φs (Pi.compRightL 𝕜 F' Fin.succ ∘SL φ') l

Tactic:
by
  rw [hasFDerivAtFilter_pi', Fin.forall_fin_succ, hasFDerivAtFilter_pi']
  dsimp [ContinuousLinearMap.comp, LinearMap.comp, Function.comp_def]
  simp only [Fin.cons_zero, Fin.cons_succ]

Goal state after:
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
x : E
f : E → F
⊢ ‖iteratedFDeriv 𝕜 1 f x‖ = ‖fderiv 𝕜 f x‖

Tactic:
rw [← iteratedFDerivWithin_univ, ← fderivWithin_univ]

Goal state after:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
x : E
f : E → F
⊢ ‖iteratedFDerivWithin 𝕜 1 f univ x‖ = ‖fderivWithin 𝕜 f univ x‖
Module: Mathlib.LinearAlgebra.AffineSpace.Slope

Goal state before:
pp: k : Type u_1
E : Type u_2
inst✝⁷ : Field k
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module k E
inst✝⁴ : LinearOrder k
inst✝³ : IsStrictOrderedRing k
inst✝² : PartialOrder E
inst✝¹ : IsOrderedAddMonoid E
inst✝ : PosSMulMono k E
f : k → E
x y : k
s : Set k
hf : AntitoneOn f s
hx : x ∈ s
hy : y ∈ s
⊢ slope f x y ≤ 0

Tactic:
by
  simpa using hf.neg.slope_nonneg hx hy

Goal state after:
Module: Mathlib.Topology.Algebra.Module.PerfectSpace

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : Nontrivial E
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousAdd E
inst✝ : ContinuousSMul 𝕜 E
x : E
hx : x ∈ univ
r : 𝕜
hr₀ : 0 < ‖r‖
hr : ‖r‖ < 1
c : E
hc : c ≠ 0
A : Tendsto (fun n ↦ x + r ^ n • c) atTop (𝓝 (x + 0 • c))
⊢ Tendsto (fun n ↦ x + r ^ n • c) atTop (𝓝[univ \ {x}] x)

Tactic:
simp only [zero_smul, add_zero] at A

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : Nontrivial E
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousAdd E
inst✝ : ContinuousSMul 𝕜 E
x : E
hx : x ∈ univ
r : 𝕜
hr₀ : 0 < ‖r‖
hr : ‖r‖ < 1
c : E
hc : c ≠ 0
A : Tendsto (fun n ↦ x + r ^ n • c) atTop (𝓝 x)
⊢ Tendsto (fun n ↦ x + r ^ n • c) atTop (𝓝[univ \ {x}] x)
Module: Mathlib.Analysis.Calculus.Deriv.Slope

Goal state before:
pp: case refine_2
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
s t : Set 𝕜
h : s ⊆ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (s ∩ t)
x : 𝕜
H : UniqueDiffWithinAt 𝕜 s x
H' : DifferentiableWithinAt 𝕜 f s x
I : (𝓝[(s ∩ t) \ {x}] x).NeBot
this : Tendsto (slope f x) (𝓝[(s ∩ t) \ {x}] x) (𝓝 (derivWithin f s x))
y : 𝕜
hy : y ∈ (s ∩ t) \ {x}
⊢ f x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (f '' (s ∩ t))

Tactic:
apply ContinuousWithinAt.mem_closure_image

Goal state after:
case refine_2.h
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
s t : Set 𝕜
h : s ⊆ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (s ∩ t)
x : 𝕜
H : UniqueDiffWithinAt 𝕜 s x
H' : DifferentiableWithinAt 𝕜 f s x
I : (𝓝[(s ∩ t) \ {x}] x).NeBot
this : Tendsto (slope f x) (𝓝[(s ∩ t) \ {x}] x) (𝓝 (derivWithin f s x))
y : 𝕜
hy : y ∈ (s ∩ t) \ {x}
⊢ ContinuousWithinAt f (s ∩ t) x

case refine_2.hx
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
s t : Set 𝕜
h : s ⊆ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (s ∩ t)
x : 𝕜
H : UniqueDiffWithinAt 𝕜 s x
H' : DifferentiableWithinAt 𝕜 f s x
I : (𝓝[(s ∩ t) \ {x}] x).NeBot
this : Tendsto (slope f x) (𝓝[(s ∩ t) \ {x}] x) (𝓝 (derivWithin f s x))
y : 𝕜
hy : y ∈ (s ∩ t) \ {x}
⊢ x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (s ∩ t)
Module: Mathlib.Analysis.Calculus.FDeriv.Analytic

Goal state before:
pp: case zero
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
x : E
r : ℝ≥0∞
y : E
F : Type (max u v)
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace F
p : FormalMultilinearSeries 𝕜 E F
f : E → F
h : HasFPowerSeriesOnBall f p x r
⊢ (0! • (p 0) fun x ↦ y) = (iteratedFDeriv 𝕜 0 f x) fun x ↦ y

pp: case succ
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
x : E
r : ℝ≥0∞
y : E
n : ℕ
ih :
  ∀ {F : Type (max u v)} [inst : NormedAddCommGroup F] [inst_1 : NormedSpace 𝕜 F] [CompleteSpace F]
    {p : FormalMultilinearSeries 𝕜 E F} {f : E → F},
    HasFPowerSeriesOnBall f p x r → (n ! • (p n) fun x ↦ y) = (iteratedFDeriv 𝕜 n f x) fun x ↦ y
F : Type (max u v)
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace F
p : FormalMultilinearSeries 𝕜 E F
f : E → F
h : HasFPowerSeriesOnBall f p x r
⊢ ((n + 1)! • (p (n + 1)) fun x ↦ y) = (iteratedFDeriv 𝕜 (n + 1) f x) fun x ↦ y

Tactic:
· rw [factorial_zero, one_smul, h.iteratedFDeriv_zero_apply_diag]

Goal state after:
case succ
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
x : E
r : ℝ≥0∞
y : E
n : ℕ
ih :
  ∀ {F : Type (max u v)} [inst : NormedAddCommGroup F] [inst_1 : NormedSpace 𝕜 F] [CompleteSpace F]
    {p : FormalMultilinearSeries 𝕜 E F} {f : E → F},
    HasFPowerSeriesOnBall f p x r → (n ! • (p n) fun x ↦ y) = (iteratedFDeriv 𝕜 n f x) fun x ↦ y
F : Type (max u v)
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace F
p : FormalMultilinearSeries 𝕜 E F
f : E → F
h : HasFPowerSeriesOnBall f p x r
⊢ ((n + 1)! • (p (n + 1)) fun x ↦ y) = (iteratedFDeriv 𝕜 (n + 1) f x) fun x ↦ y
Module: Mathlib.Analysis.Calculus.FDeriv.Analytic

Goal state before:
pp: case zero
𝕜 : 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
f : E → F
x : E
r : ℝ≥0∞
h : HasFPowerSeriesOnBall f p x r
y : E
inst✝ : CompleteSpace F
⊢ (0! • (p 0) fun x ↦ y) = (iteratedFDeriv 𝕜 0 f x) fun x ↦ y

pp: case succ
𝕜 : 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
f : E → F
x : E
r : ℝ≥0∞
h : HasFPowerSeriesOnBall f p x r
y : E
inst✝ : CompleteSpace F
n✝ : ℕ
⊢ ((n✝ + 1)! • (p (n✝ + 1)) fun x ↦ y) = (iteratedFDeriv 𝕜 (n✝ + 1) f x) fun x ↦ y

Tactic:
· rw [factorial_zero, one_smul, h.iteratedFDeriv_zero_apply_diag]

Goal state after:
case succ
𝕜 : 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
f : E → F
x : E
r : ℝ≥0∞
h : HasFPowerSeriesOnBall f p x r
y : E
inst✝ : CompleteSpace F
n✝ : ℕ
⊢ ((n✝ + 1)! • (p (n✝ + 1)) fun x ↦ y) = (iteratedFDeriv 𝕜 (n✝ + 1) f x) fun x ↦ y
Module: Mathlib.Analysis.Calculus.FDeriv.Mul

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
ι : Type u_5
𝔸' : Type u_7
inst✝² : NormedCommRing 𝔸'
inst✝¹ : NormedAlgebra 𝕜 𝔸'
g : ι → E → 𝔸'
g' : ι → E →L[𝕜] 𝔸'
inst✝ : DecidableEq ι
u : Multiset ι
x : E
h : ∀ i ∈ u, HasFDerivAt (fun x ↦ g i x) (g' i) x
⊢ HasFDerivAt (fun x ↦ (Multiset.map ((fun x_1 ↦ g x_1 x) ∘ Subtype.val) u.attach).prod)
    (Multiset.map
        ((fun x_1 ↦ (Multiset.map (fun x_2 ↦ g x_2 x) ((Multiset.map Subtype.val u.attach).erase x_1)).prod •> g' x_1) ∘
          Subtype.val)
        u.attach).sum
    x

Tactic:
exact .congr_fderiv
    (hasFDerivAt_multiset_prod.comp x <| hasFDerivAt_pi.mpr fun i ↦ h (Subtype.val i) i.prop :)
    (by ext; simp [Finset.sum_multiset_map_count, u.erase_attach_map (g · x)])

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

Goal state before:
pp: 𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
x : 𝕜
𝕜' : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
c d : 𝕜 → 𝕜'
c' d' : 𝕜'
hc : HasStrictDerivAt c c' x
hd : HasStrictDerivAt d d' x
hx : d x ≠ 0
⊢ HasStrictDerivAt (fun y ↦ c y / d y) ((c' * d x - c x * d') / d x ^ 2) x

Tactic:
convert hc.fun_mul ((hasStrictDerivAt_inv hx).comp x hd)

Goal state after:
case e'_8
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
x : 𝕜
𝕜' : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
c d : 𝕜 → 𝕜'
c' d' : 𝕜'
hc : HasStrictDerivAt c c' x
hd : HasStrictDerivAt d d' x
hx : d x ≠ 0
x✝ : 𝕜
⊢ c x✝ / d x✝ = c x✝ * (Inv.inv ∘ d) x✝

case e'_9
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
x : 𝕜
𝕜' : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
c d : 𝕜 → 𝕜'
c' d' : 𝕜'
hc : HasStrictDerivAt c c' x
hd : HasStrictDerivAt d d' x
hx : d x ≠ 0
⊢ (c' * d x - c x * d') / d x ^ 2 = c' * (Inv.inv ∘ d) x + c x * (-(d x ^ 2)⁻¹ * d')
Module: Mathlib.Analysis.Calculus.Deriv.Comp

Goal state before:
pp: 𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type w
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
𝕜' : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
h₂ : 𝕜' → 𝕜'
h₂' y : 𝕜'
f : E → 𝕜'
f' : E →L[𝕜] 𝕜'
x : E
hh : HasDerivAt h₂ h₂' y
hf : HasFDerivAt f f' x
hy : y = f x
⊢ HasFDerivAt (h₂ ∘ f) (h₂' • f') x

Tactic:
rw [hy] at hh; exact hh.comp_hasFDerivAt x hf

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
c : 𝕜
f : 𝕜 → E
s : Set 𝕜
x : 𝕜
⊢ derivWithin (fun x ↦ f (c * x)) s x = c • derivWithin f (c • s) (c * x)

Tactic:
simp only [← smul_eq_mul]
  rw [← derivWithin_const_smul_field, derivWithin, derivWithin,
    fderivWithin_comp_smul_eq_fderivWithin_smul, Pi.smul_def]

Goal state after:
Module: Mathlib.Analysis.Analytic.IsolatedZeros

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
z₀ : 𝕜
m n : ℤ
hm : ∃ g, AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] z₀, f z = (z - z₀) ^ m • g z
hn : ∃ g, AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] z₀, f z = (z - z₀) ^ n • g z
h_le : n ≤ m
g : 𝕜 → E
hg_an : AnalyticAt 𝕜 g z₀
left✝ : g z₀ ≠ 0
hg_eq : ∀ᶠ (z : 𝕜) in 𝓝[≠] z₀, f z = (z - z₀) ^ m • g z
j : 𝕜 → E
hj_an : AnalyticAt 𝕜 j z₀
hj_eq : ∀ᶠ (z : 𝕜) in 𝓝[≠] z₀, f z = (z - z₀) ^ n • j z
hj_ne : m ≠ n
⊢ ∃ᶠ (z : 𝕜) in 𝓝[≠] z₀, j z = (z - z₀) ^ (m - n) • g z

Tactic:
apply Filter.Eventually.frequently

Goal state after:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
z₀ : 𝕜
m n : ℤ
hm : ∃ g, AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] z₀, f z = (z - z₀) ^ m • g z
hn : ∃ g, AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] z₀, f z = (z - z₀) ^ n • g z
h_le : n ≤ m
g : 𝕜 → E
hg_an : AnalyticAt 𝕜 g z₀
left✝ : g z₀ ≠ 0
hg_eq : ∀ᶠ (z : 𝕜) in 𝓝[≠] z₀, f z = (z - z₀) ^ m • g z
j : 𝕜 → E
hj_an : AnalyticAt 𝕜 j z₀
hj_eq : ∀ᶠ (z : 𝕜) in 𝓝[≠] z₀, f z = (z - z₀) ^ n • j z
hj_ne : m ≠ n
⊢ ∀ᶠ (x : 𝕜) in 𝓝[≠] z₀, j x = (x - z₀) ^ (m - n) • g x
Module: Mathlib.Analysis.Calculus.ContDiff.Basic

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : E → F
n : ℕ∞ω
e : F ≃L[𝕜] G
⊢ ContDiff 𝕜 n (⇑e ∘ f) ↔ ContDiff 𝕜 n f

Tactic:
simp only [← contDiffOn_univ, e.comp_contDiffOn_iff]

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

Goal state before:
pp: 𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
f' : F
x : 𝕜
c : F
h : HasDerivAt f f' x
hf' : f' ≠ 0
⊢ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z ≠ c

Tactic:
simpa only [compl_eq_univ_sdiff] using (hasDerivWithinAt_univ.2 h).eventually_ne hf'

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

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
n : ℕ∞
f' : E → FormalMultilinearSeries 𝕜 E F
hf : HasFTaylorSeriesUpToOn (↑n) f f' s
x : E
hx : x ∈ s
⊢ ContDiffWithinAt 𝕜 (↑n) f s x

Tactic:
m

Goal state after:
𝕜 : 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 : ℕ∞
f' : E → FormalMultilinearSeries 𝕜 E F
hf : HasFTaylorSeriesUpToOn (↑n) f f' s
x : E
hx : x ∈ s
m : ℕ
⊢ ↑m ≤ n → ∃ u ∈ 𝓝[insert x s] x, ∃ p, HasFTaylorSeriesUpToOn (↑m) f p u
Module: Mathlib.Analysis.Calculus.ContDiff.Defs

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
n : ℕ∞
Hcont : ∀ (m : ℕ), ↑m ≤ n → ContinuousOn (fun x ↦ iteratedFDerivWithin 𝕜 m f s x) s
Hdiff : ∀ (m : ℕ), ↑m < n → DifferentiableOn 𝕜 (fun x ↦ iteratedFDerivWithin 𝕜 m f s x) s
x : E
hx : x ∈ s
⊢ ContDiffWithinAt 𝕜 (↑n) f s x

Tactic:
m

Goal state after:
𝕜 : 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 : ℕ∞
Hcont : ∀ (m : ℕ), ↑m ≤ n → ContinuousOn (fun x ↦ iteratedFDerivWithin 𝕜 m f s x) s
Hdiff : ∀ (m : ℕ), ↑m < n → DifferentiableOn 𝕜 (fun x ↦ iteratedFDerivWithin 𝕜 m f s x) s
x : E
hx : x ∈ s
m : ℕ
⊢ ↑m ≤ n → ∃ u ∈ 𝓝[insert x s] x, ∃ p, HasFTaylorSeriesUpToOn (↑m) f p u
Module: Mathlib.Analysis.Calculus.ContDiff.Defs

Goal state before:
pp: case inl
𝕜 : 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
hf : DifferentiableOn 𝕜 f s
h' : ∞ = ω → AnalyticOn 𝕜 f s
h : ContDiffOn 𝕜 ∞ (fun y ↦ fderivWithin 𝕜 f s y) s
⊢ ContDiffOn 𝕜 (∞ + 1) f s

Tactic:
rw [ENat.coe_top_add_one, contDiffOn_infty]

Goal state after:
case inl
𝕜 : 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
hf : DifferentiableOn 𝕜 f s
h' : ∞ = ω → AnalyticOn 𝕜 f s
h : ContDiffOn 𝕜 ∞ (fun y ↦ fderivWithin 𝕜 f s y) s
⊢ ∀ (n : ℕ), ContDiffOn 𝕜 (↑n) f s
Module: Mathlib.Analysis.Calculus.ContDiff.Defs

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
f : E → F
n : ℕ∞ω
hf : ContDiff 𝕜 n f
⊢ HasFTaylorSeriesUpTo n f (_root_.ftaylorSeries 𝕜 f)

Tactic:
simp only [← contDiffOn_univ, ← hasFTaylorSeriesUpToOn_univ_iff, ← ftaylorSeriesWithin_univ]
    at hf ⊢
  exact ContDiffOn.ftaylorSeriesWithin hf uniqueDiffOn_univ

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

Goal state before:
pp: case inl.refine_2
𝕜 : 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
s : Set E
t : Set F
q : F → FormalMultilinearSeries 𝕜 F G
p : E → FormalMultilinearSeries 𝕜 E F
n : ℕ
c✝ : OrderedFinpartition n
c : OrderedFinpartition (n + 1)
hc : range (c.emb 0) ≠ {0}
x : Fin n
j : Fin (c.partSize (c.index 0))
hij : c.emb (c.index 0) j = x.succ
j_ne : j ≠ 0
je_ne' : ↑j ≠ 0
A : c.partSize (c.index 0) - 1 + 1 = c.partSize (c.index 0)
B : update c.partSize (c.index 0) (c.partSize (c.index 0) - 1) (c.index 0) = c.partSize (c.index 0) - 1
this : x = x.succ.pred ⋯
⊢ Fin.cast ⋯ (Fin.cast ⋯ ((Fin.cast ⋯ j).pred ⋯)).succ = j

Tactic:
rw [← val_eq_val]

Goal state after:
case inl.refine_2
𝕜 : 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
s : Set E
t : Set F
q : F → FormalMultilinearSeries 𝕜 F G
p : E → FormalMultilinearSeries 𝕜 E F
n : ℕ
c✝ : OrderedFinpartition n
c : OrderedFinpartition (n + 1)
hc : range (c.emb 0) ≠ {0}
x : Fin n
j : Fin (c.partSize (c.index 0))
hij : c.emb (c.index 0) j = x.succ
j_ne : j ≠ 0
je_ne' : ↑j ≠ 0
A : c.partSize (c.index 0) - 1 + 1 = c.partSize (c.index 0)
B : update c.partSize (c.index 0) (c.partSize (c.index 0) - 1) (c.index 0) = c.partSize (c.index 0) - 1
this : x = x.succ.pred ⋯
⊢ ↑(Fin.cast ⋯ (Fin.cast ⋯ ((Fin.cast ⋯ j).pred ⋯)).succ) = ↑j
Module: Mathlib.Analysis.Normed.Algebra.Exponential

Goal state before:
pp: 𝔸 : Type u_2
inst✝³ : Ring 𝔸
inst✝² : TopologicalSpace 𝔸
inst✝¹ : IsTopologicalRing 𝔸
inst✝ : T2Space 𝔸
x : 𝔸
⊢ exp (MulOpposite.op x) = MulOpposite.op (exp x)

Tactic:
by
  obtain h | ⟨⟨_⟩⟩ := isEmpty_or_nonempty (Algebra ℚ 𝔸)
  · have : IsEmpty (Algebra ℚ 𝔸ᵐᵒᵖ) := ⟨fun _ => h.elim <| (RingEquiv.opOp 𝔸).algebra ℚ⟩
    simp
  · rw [exp_eq_tsum ℚ, exp_eq_tsum ℚ]
    simp_rw [← MulOpposite.op_pow, ← MulOpposite.op_smul, tsum_op]

Goal state after:
Module: Mathlib.Analysis.Normed.Algebra.Exponential

Goal state before:
pp: 𝕂 : Type u_1
𝔸 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕂
inst✝³ : NormedRing 𝔸
inst✝² : NormedAlgebra 𝕂 𝔸
inst✝¹ : CompleteSpace 𝔸
inst✝ : CharZero 𝕂
x : 𝔸
hx : x ∈ Metric.eball 0 (expSeries 𝕂 𝔸).radius
⊢ HasSum (fun n ↦ (expSeries 𝕂 𝔸 n) fun x_1 ↦ x) (exp x)

Tactic:
exact expSeries_hasSum_exp_of_mem_ball x hx

Goal state after:
Module: Mathlib.Analysis.Normed.Algebra.Exponential

Goal state before:
pp: 𝕂 : Type u_1
𝔸 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕂
inst✝³ : NormedDivisionRing 𝔸
inst✝² : NormedAlgebra 𝕂 𝔸
inst✝¹ : CharZero 𝕂
inst✝ : CompleteSpace 𝔸
x : 𝔸
hx : x ∈ Metric.eball 0 (expSeries 𝕂 𝔸).radius
⊢ HasSum (fun n ↦ (expSeries 𝕂 𝔸 n) fun x_1 ↦ x) (exp x)

Tactic:
exact expSeries_hasSum_exp_of_mem_ball x hx

Goal state after: