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

Goal state before:
pp: case a
𝕜 : Type u_2
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
G : Type u_5
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
p : FormalMultilinearSeries 𝕜 E F
q : FormalMultilinearSeries 𝕜 E G
⊢ min p.radius q.radius ≤ (p.prod q).radius

Tactic:
refine ENNReal.le_of_forall_nnreal_lt fun r hr => ?_
    rw [lt_min_iff] at hr
    have := ((p.isLittleO_one_of_lt_radius hr.1).add
      (q.isLittleO_one_of_lt_radius hr.2)).isBigO
    refine (p.prod q).le_radius_of_isBigO ((isBigO_of_le _ fun n ↦ ?_).trans this)
    rw [norm_mul, norm_norm, ← add_mul, norm_mul]
    refine mul_le_mul_of_nonneg_right ?_ (norm_nonneg _)
    rw [FormalMultilinearSeries.prod, ContinuousMultilinearMap.opNorm_prod]
    refine (max_le_add_of_nonneg (norm_nonneg _) (norm_nonneg _)).trans ?_
    apply Real.le_norm_self

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

Goal state before:
pp: 𝕜 : Type u_2
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
G : Type u_5
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
e : E
f : E → F
g : E → G
r s : ℝ≥0∞
t : Set E
p : FormalMultilinearSeries 𝕜 E F
q : FormalMultilinearSeries 𝕜 E G
hf : HasFPowerSeriesWithinOnBall f p t e r
hg : HasFPowerSeriesWithinOnBall g q t e s
⊢ min r s ≤ (p.prod q).radius

Tactic:
p.radius_prod_eq_min

Goal state after:
𝕜 : Type u_2
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
G : Type u_5
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
e : E
f : E → F
g : E → G
r s : ℝ≥0∞
t : Set E
p : FormalMultilinearSeries 𝕜 E F
q : FormalMultilinearSeries 𝕜 E G
hf : HasFPowerSeriesWithinOnBall f p t e r
hg : HasFPowerSeriesWithinOnBall g q t e s
⊢ min r s ≤ min p.radius q.radius
Module: Mathlib.Analysis.Analytic.Constructions

Goal state before:
pp: 𝕜 : Type u_2
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
G : Type u_5
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
u : E →L[𝕜] F
f : F → G
pf : FormalMultilinearSeries 𝕜 F G
x : E
r : ℝ≥0∞
hf : HasFPowerSeriesOnBall f pf (u x) r
⊢ HasFPowerSeriesOnBall (f ∘ ⇑u) (pf.compContinuousLinearMap u) x (r / ‖u‖ₑ)

Tactic:
rw [← hasFPowerSeriesWithinOnBall_univ] at hf ⊢
  exact hf.compContinuousLinearMap

Goal state after:
Module: Mathlib.Analysis.Normed.Module.Alternating.Basic

Goal state before:
pp: 𝕜 : Type u
n : ℕ
E : Type wE
F : Type wF
G : Type wG
ι : Type v
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : SeminormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : SeminormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
inst✝³ : SeminormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
f : F [⋀^ι]→L[𝕜] G
g dg : E →L[𝕜] F
v : ι → E
a b : ι
heq : v a = v b
hne : a ≠ b
⊢ (∑ i, f fun j ↦ (Function.update (fun x ↦ g) i dg j) (v j)) = 0

Tactic:
rw [← Finset.sum_add_sum_compl {a, b}, Finset.sum_pair hne, Finset.sum_eq_zero, add_zero]

Goal state after:
𝕜 : Type u
n : ℕ
E : Type wE
F : Type wF
G : Type wG
ι : Type v
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : SeminormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : SeminormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
inst✝³ : SeminormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
f : F [⋀^ι]→L[𝕜] G
g dg : E →L[𝕜] F
v : ι → E
a b : ι
heq : v a = v b
hne : a ≠ b
⊢ ((f fun j ↦ (Function.update (fun x ↦ g) a dg j) (v j)) + f fun j ↦ (Function.update (fun x ↦ g) b dg j) (v j)) = 0

𝕜 : Type u
n : ℕ
E : Type wE
F : Type wF
G : Type wG
ι : Type v
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : SeminormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : SeminormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
inst✝³ : SeminormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
f : F [⋀^ι]→L[𝕜] G
g dg : E →L[𝕜] F
v : ι → E
a b : ι
heq : v a = v b
hne : a ≠ b
⊢ ∀ x ∈ {a, b}ᶜ, (f fun j ↦ (Function.update (fun x ↦ g) x dg j) (v j)) = 0
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

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:
Module: Mathlib.Analysis.Calculus.FDeriv.Analytic

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
ι : Type u_2
E : ι → Type u_3
inst✝² : (i : ι) → NormedAddCommGroup (E i)
inst✝¹ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝ : Fintype ι
f : ContinuousMultilinearMap 𝕜 E F
k l : ℕ
h : k + l ≠ Fintype.card ι
x✝¹ : { s // s.card = l }
x✝ : x✝¹ ∈ Finset.univ
⊢ f.toFormalMultilinearSeries.changeOriginSeriesTerm k l ↑x✝¹ ⋯ = 0

Tactic:
simp_rw [FormalMultilinearSeries.changeOriginSeriesTerm,
      toFormalMultilinearSeries, dif_neg h.symm, LinearIsometryEquiv.map_zero]

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
x : 𝕜
G : Type u_2
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
c : 𝕜 → F →L[𝕜] G
c' : F →L[𝕜] G
u : 𝕜 → F
u' : F
hc : HasDerivAt c c' x
hu : HasDerivAt u u' x
⊢ HasDerivAt (fun y ↦ (c y) (u y)) (c' (u x) + (c x) u') x

Tactic:
by
  simpa [add_comm] using (hc.hasFDerivAt.clm_apply hu.hasFDerivAt).hasDerivAt

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

Goal state before:
pp: case inr
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
ι : Type u_2
E : ι → Type u_3
inst✝³ : (i : ι) → NormedAddCommGroup (E i)
inst✝² : (i : ι) → NormedSpace 𝕜 (E i)
inst✝¹ : Fintype ι
f : ContinuousMultilinearMap 𝕜 E F
x : (i : ι) → E i
inst✝ : DecidableEq ι
y : (i : ι) → E i
h✝ : Nonempty ι
⊢ ((f.toFormalMultilinearSeries.changeOriginSeries 1 (Fintype.card ι - 1)) fun x_1 ↦ x) (Fin.snoc 0 y) =
    ∑ i, f (Function.update x i (y i))

pp: case inr
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
ι : Type u_2
E : ι → Type u_3
inst✝³ : (i : ι) → NormedAddCommGroup (E i)
inst✝² : (i : ι) → NormedSpace 𝕜 (E i)
inst✝¹ : Fintype ι
f : ContinuousMultilinearMap 𝕜 E F
x : (i : ι) → E i
inst✝ : DecidableEq ι
y : (i : ι) → E i
h✝ : Nonempty ι
⊢ ∀ (b' : ℕ), b' ≠ Fintype.card ι - 1 → ((f.toFormalMultilinearSeries.changeOriginSeries 1 b') fun x_1 ↦ x) = 0

Tactic:
changeOriginSeries

Goal state after:
case inr
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
ι : Type u_2
E : ι → Type u_3
inst✝³ : (i : ι) → NormedAddCommGroup (E i)
inst✝² : (i : ι) → NormedSpace 𝕜 (E i)
inst✝¹ : Fintype ι
f : ContinuousMultilinearMap 𝕜 E F
x : (i : ι) → E i
inst✝ : DecidableEq ι
y : (i : ι) → E i
h✝ : Nonempty ι
⊢ ((∑ s, f.toFormalMultilinearSeries.changeOriginSeriesTerm 1 (Fintype.card ι - 1) ↑s ⋯) fun x_1 ↦ x) (Fin.snoc 0 y) =
    ∑ i, f (Function.update x i (y i))

case inr
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
ι : Type u_2
E : ι → Type u_3
inst✝³ : (i : ι) → NormedAddCommGroup (E i)
inst✝² : (i : ι) → NormedSpace 𝕜 (E i)
inst✝¹ : Fintype ι
f : ContinuousMultilinearMap 𝕜 E F
x : (i : ι) → E i
inst✝ : DecidableEq ι
y : (i : ι) → E i
h✝ : Nonempty ι
⊢ ∀ (b' : ℕ), b' ≠ Fintype.card ι - 1 → ((f.toFormalMultilinearSeries.changeOriginSeries 1 b') fun x_1 ↦ x) = 0
Module: Mathlib.Analysis.Calculus.Deriv.Slope

Goal state before:
pp: 𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
f' : F
x : 𝕜
L : Filter 𝕜
⊢ Tendsto (fun y ↦ slope f x y - f') (L ⊓ 𝓟 {x}ᶜ) (𝓝 0) ↔
    Tendsto (slope f x) (L ⊓ 𝓟 {x}ᶜ) (comap (fun x ↦ x - f') (𝓝 0))

Tactic:
tendsto_comap_iff

Goal state after:
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
f' : F
x : 𝕜
L : Filter 𝕜
⊢ Tendsto (fun y ↦ slope f x y - f') (L ⊓ 𝓟 {x}ᶜ) (𝓝 0) ↔ Tendsto ((fun x ↦ x - f') ∘ slope f x) (L ⊓ 𝓟 {x}ᶜ) (𝓝 0)
Module: Mathlib.Analysis.Calculus.Deriv.Slope

Goal state before:
pp: case pos
𝕜 : 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))
⊢ ∀ᶠ (x_1 : 𝕜) in 𝓝[(s ∩ t) \ {x}] x, slope f x x_1 ∈ ↑(Submodule.span 𝕜 (f '' t)).topologicalClosure

Tactic:
filter_upwards [self_mem_nhdsWithin] with y hy

Goal state after:
𝕜 : 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}
⊢ slope f x y ∈ ↑(Submodule.span 𝕜 (f '' t)).topologicalClosure
Module: Mathlib.Analysis.Calculus.Deriv.Slope

Goal state before:
pp: 𝕜 : Type u
inst✝³ : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
inst✝ : OrderTopology 𝕜
g : 𝕜 → 𝕜
g' : 𝕜
hx : AccPt x (𝓟 s)
hd : HasDerivWithinAt g g' s x
hg : MonotoneOn g s
this✝ : (𝓝[s \ {x}] x).NeBot
h'g : MonotoneOn g (insert x s)
this : Tendsto (slope g x) (𝓝[s \ {x}] x) (𝓝 g')
⊢ ∀ᶠ (c : 𝕜) in 𝓝[s \ {x}] x, 0 ≤ slope g x c

Tactic:
filter_upwards [self_mem_nhdsWithin] with y hy

Goal state after:
𝕜 : Type u
inst✝³ : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
inst✝ : OrderTopology 𝕜
g : 𝕜 → 𝕜
g' : 𝕜
hx : AccPt x (𝓟 s)
hd : HasDerivWithinAt g g' s x
hg : MonotoneOn g s
this✝ : (𝓝[s \ {x}] x).NeBot
h'g : MonotoneOn g (insert x s)
this : Tendsto (slope g x) (𝓝[s \ {x}] x) (𝓝 g')
y : 𝕜
hy : y ∈ s \ {x}
⊢ 0 ≤ slope g x y
Module: Mathlib.Analysis.Calculus.Deriv.Slope

Goal state before:
pp: E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
f' : E
x r : ℝ
hf : HasDerivWithinAt f f' (Ici x) x
hr : ‖f'‖ < r
⊢ ∃ᶠ (z : ℝ) in 𝓝[>] x, (z - x)⁻¹ * (‖f z‖ - ‖f x‖) < r

Tactic:
by
  have := (hf.Ioi_of_Ici.limsup_slope_norm_le hr).frequently
  refine this.mp (Eventually.mono self_mem_nhdsWithin fun z hxz hz ↦ ?_)
  rwa [Real.norm_eq_abs, abs_of_pos (sub_pos_of_lt hxz)] at hz

Goal state after:
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_6
inst✝¹ : NormedRing 𝔸
inst✝ : NormedAlgebra 𝕜 𝔸
f : ι → E → 𝔸
f' : ι → E →L[𝕜] 𝔸
l : List ι
x : E
h : ∀ i ∈ l, HasStrictFDerivAt (fun x ↦ f i x) (f' i) x
⊢ HasStrictFDerivAt (fun x ↦ (List.map (fun x_1 ↦ f x_1 x) l).prod)
    (∑ x_1,
      (List.map (fun x_2 ↦ f x_2 x) (List.take (↑x_1) l)).prod •>
        (f' (l.get x_1) <• (List.map (fun x_2 ↦ f x_2 x) (List.drop (↑x_1).succ l)).prod))
    x

Tactic:
← List.map_get_finRange l,

Goal state after:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
ι : Type u_5
𝔸 : Type u_6
inst✝¹ : NormedRing 𝔸
inst✝ : NormedAlgebra 𝕜 𝔸
f : ι → E → 𝔸
f' : ι → E →L[𝕜] 𝔸
l : List ι
x : E
h : ∀ i ∈ l, HasStrictFDerivAt (fun x ↦ f i x) (f' i) x
⊢ HasStrictFDerivAt (fun x ↦ (List.map (fun x_1 ↦ f x_1 x) (List.map l.get (List.finRange l.length))).prod)
    (∑ x_1,
      (List.map (fun x_2 ↦ f x_2 x) (List.take (↑x_1) (List.map l.get (List.finRange l.length)))).prod •>
        (f' (l.get x_1) <•
          (List.map (fun x_2 ↦ f x_2 x) (List.drop (↑x_1).succ (List.map l.get (List.finRange l.length)))).prod))
    x
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_6
inst✝¹ : NormedRing 𝔸
inst✝ : NormedAlgebra 𝕜 𝔸
f : ι → E → 𝔸
f' : ι → E →L[𝕜] 𝔸
l : List ι
x : E
h : ∀ i ∈ l, HasFDerivAt (fun x ↦ f i x) (f' i) x
⊢ HasFDerivAt (fun x ↦ (List.map (fun x_1 ↦ f x_1 x) l).prod)
    (∑ x_1,
      (List.map (fun x_2 ↦ f x_2 x) (List.take (↑x_1) l)).prod •>
        (f' (l.get x_1) <• (List.map (fun x_2 ↦ f x_2 x) (List.drop (↑x_1).succ l)).prod))
    x

Tactic:
← List.map_get_finRange l,

Goal state after:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
ι : Type u_5
𝔸 : Type u_6
inst✝¹ : NormedRing 𝔸
inst✝ : NormedAlgebra 𝕜 𝔸
f : ι → E → 𝔸
f' : ι → E →L[𝕜] 𝔸
l : List ι
x : E
h : ∀ i ∈ l, HasFDerivAt (fun x ↦ f i x) (f' i) x
⊢ HasFDerivAt (fun x ↦ (List.map (fun x_1 ↦ f x_1 x) (List.map l.get (List.finRange l.length))).prod)
    (∑ x_1,
      (List.map (fun x_2 ↦ f x_2 x) (List.take (↑x_1) (List.map l.get (List.finRange l.length)))).prod •>
        (f' (l.get x_1) <•
          (List.map (fun x_2 ↦ f x_2 x) (List.drop (↑x_1).succ (List.map l.get (List.finRange l.length)))).prod))
    x
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_6
inst✝¹ : NormedRing 𝔸
inst✝ : NormedAlgebra 𝕜 𝔸
f : ι → E → 𝔸
f' : ι → E →L[𝕜] 𝔸
l : List ι
x : E
h : ∀ i ∈ l, HasFDerivAt (fun x ↦ f i x) (f' i) x
⊢ HasFDerivAt (fun x ↦ (List.map ((fun x_1 ↦ f x_1 x) ∘ l.get) (List.finRange l.length)).prod)
    (∑ x_1,
      (List.map (fun x_2 ↦ f x_2 x) (List.take (↑x_1) (List.map l.get (List.finRange l.length)))).prod •>
        (f' (l.get x_1) <•
          (List.map (fun x_2 ↦ f x_2 x) (List.drop (↑x_1).succ (List.map l.get (List.finRange l.length)))).prod))
    x

Tactic:
refine .congr_fderiv (hasFDerivAt_list_prod_finRange'.comp x
    (hasFDerivAt_pi.mpr fun i ↦ h (l.get i) (l.get_mem i)) :) ?_

Goal state after:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
ι : Type u_5
𝔸 : Type u_6
inst✝¹ : NormedRing 𝔸
inst✝ : NormedAlgebra 𝕜 𝔸
f : ι → E → 𝔸
f' : ι → E →L[𝕜] 𝔸
l : List ι
x : E
h : ∀ i ∈ l, HasFDerivAt (fun x ↦ f i x) (f' i) x
⊢ ((∑ i,
        (List.map (fun i ↦ f (l.get i) x) (List.take (↑i) (List.finRange l.length))).prod •>
          (proj i <• (List.map (fun i ↦ f (l.get i) x) (List.drop (↑i).succ (List.finRange l.length))).prod)) ∘SL
      pi fun i ↦ f' (l.get i)) =
    ∑ x_1,
      (List.map (fun x_2 ↦ f x_2 x) (List.take (↑x_1) (List.map l.get (List.finRange l.length)))).prod •>
        (f' (l.get x_1) <•
          (List.map (fun x_2 ↦ f x_2 x) (List.drop (↑x_1).succ (List.map l.get (List.finRange l.length)))).prod)
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
s : Set E
ι : Type u_5
𝔸 : Type u_6
inst✝¹ : NormedRing 𝔸
inst✝ : NormedAlgebra 𝕜 𝔸
f : ι → E → 𝔸
f' : ι → E →L[𝕜] 𝔸
l : List ι
x : E
h : ∀ i ∈ l, HasFDerivWithinAt (fun x ↦ f i x) (f' i) s x
⊢ HasFDerivWithinAt (fun x ↦ (List.map (fun x_1 ↦ f x_1 x) l).prod)
    (∑ x_1,
      (List.map (fun x_2 ↦ f x_2 x) (List.take (↑x_1) l)).prod •>
        (f' (l.get x_1) <• (List.map (fun x_2 ↦ f x_2 x) (List.drop (↑x_1).succ l)).prod))
    s x

Tactic:
← List.map_get_finRange l,

Goal state after:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
s : Set E
ι : Type u_5
𝔸 : Type u_6
inst✝¹ : NormedRing 𝔸
inst✝ : NormedAlgebra 𝕜 𝔸
f : ι → E → 𝔸
f' : ι → E →L[𝕜] 𝔸
l : List ι
x : E
h : ∀ i ∈ l, HasFDerivWithinAt (fun x ↦ f i x) (f' i) s x
⊢ HasFDerivWithinAt (fun x ↦ (List.map (fun x_1 ↦ f x_1 x) (List.map l.get (List.finRange l.length))).prod)
    (∑ x_1,
      (List.map (fun x_2 ↦ f x_2 x) (List.take (↑x_1) (List.map l.get (List.finRange l.length)))).prod •>
        (f' (l.get x_1) <•
          (List.map (fun x_2 ↦ f x_2 x) (List.drop (↑x_1).succ (List.map l.get (List.finRange l.length)))).prod))
    s x
Module: Mathlib.Analysis.Analytic.IsolatedZeros

Goal state before:
pp: case pos
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
p : FormalMultilinearSeries 𝕜 𝕜 E
f : 𝕜 → E
z₀ : 𝕜
hpd : deriv f z₀ = p.coeff 1
hp0 : p.coeff 0 = f z₀
hp : ∀ᶠ (z : 𝕜) in 𝓝 0, HasSum (fun n ↦ z ^ n • p.coeff n) (f (z₀ + z))
x : 𝕜
hx : HasSum (fun n ↦ x ^ n • p.coeff n) (f (z₀ + x))
h : x = 0
⊢ HasSum (fun n ↦ x ^ n • p.coeff (n + 1)) (dslope f z₀ (z₀ + x))

pp: case neg
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
p : FormalMultilinearSeries 𝕜 𝕜 E
f : 𝕜 → E
z₀ : 𝕜
hpd : deriv f z₀ = p.coeff 1
hp0 : p.coeff 0 = f z₀
hp : ∀ᶠ (z : 𝕜) in 𝓝 0, HasSum (fun n ↦ z ^ n • p.coeff n) (f (z₀ + z))
x : 𝕜
hx : HasSum (fun n ↦ x ^ n • p.coeff n) (f (z₀ + x))
h : ¬x = 0
⊢ HasSum (fun n ↦ x ^ n • p.coeff (n + 1)) (dslope f z₀ (z₀ + x))

Tactic:
· convert! hasSum_single (α := E) 0 _ <;> intros <;> simp [*]

Goal state after:
case neg
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
p : FormalMultilinearSeries 𝕜 𝕜 E
f : 𝕜 → E
z₀ : 𝕜
hpd : deriv f z₀ = p.coeff 1
hp0 : p.coeff 0 = f z₀
hp : ∀ᶠ (z : 𝕜) in 𝓝 0, HasSum (fun n ↦ z ^ n • p.coeff n) (f (z₀ + z))
x : 𝕜
hx : HasSum (fun n ↦ x ^ n • p.coeff n) (f (z₀ + x))
h : ¬x = 0
⊢ HasSum (fun n ↦ x ^ n • p.coeff (n + 1)) (dslope f z₀ (z₀ + x))
Module: Mathlib.Analysis.Calculus.Deriv.Comp

Goal state before:
pp: 𝕜 : Type u
inst✝⁶ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
x : 𝕜
𝕜' : Type u_1
inst✝³ : NontriviallyNormedField 𝕜'
inst✝² : NormedAlgebra 𝕜 𝕜'
inst✝¹ : NormedSpace 𝕜' F
inst✝ : IsScalarTower 𝕜 𝕜' F
h : 𝕜 → 𝕜'
h' : 𝕜'
g₁ : 𝕜' → F
g₁' : F
y : 𝕜'
hg : HasDerivAt g₁ g₁' y
hh : HasDerivAt h h' x
hy : y = h x
⊢ HasDerivAt (g₁ ∘ h) (h' • g₁') x

Tactic:
rw [hy] at hg; exact hg.scomp x hh

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

Goal state before:
pp: 𝕜 : Type u
inst✝⁶ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
x : 𝕜
𝕜' : Type u_1
inst✝³ : NontriviallyNormedField 𝕜'
inst✝² : NormedAlgebra 𝕜 𝕜'
inst✝¹ : NormedSpace 𝕜' F
inst✝ : IsScalarTower 𝕜 𝕜' F
h : 𝕜 → 𝕜'
h' : 𝕜'
g₁ : 𝕜' → F
g₁' : F
y : 𝕜'
hg : HasStrictDerivAt g₁ g₁' y
hh : HasStrictDerivAt h h' x
hy : y = h x
⊢ HasStrictDerivAt (g₁ ∘ h) (h' • g₁') x

Tactic:
rw [hy] at hg; exact hg.scomp x hh

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 : ∀ᶠ (x : 𝕜) in 𝓝 z₀, x ∈ {z₀}ᶜ → f x = (x - z₀) ^ m • g x
j : 𝕜 → E
hj_an : AnalyticAt 𝕜 j z₀
hj_eq : ∀ᶠ (x : 𝕜) in 𝓝 z₀, x ∈ {z₀}ᶜ → f x = (x - z₀) ^ n • j x
hj_ne : m ≠ n
z : 𝕜
hfz : z ∈ {z₀}ᶜ → f z = (z - z₀) ^ m • g z
hfz' : z ∈ {z₀}ᶜ → f z = (z - z₀) ^ n • j z
hz : z ∈ {z₀}ᶜ
⊢ j z = (z - z₀) ^ (m - n) • g z

Tactic:
rw [← add_sub_cancel_left n m, add_sub_assoc, zpow_add₀ <| sub_ne_zero.mpr hz, mul_smul,
      hfz' hz, smul_right_inj <| zpow_ne_zero _ <| sub_ne_zero.mpr hz] at hfz

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 : ∀ᶠ (x : 𝕜) in 𝓝 z₀, x ∈ {z₀}ᶜ → f x = (x - z₀) ^ m • g x
j : 𝕜 → E
hj_an : AnalyticAt 𝕜 j z₀
hj_eq : ∀ᶠ (x : 𝕜) in 𝓝 z₀, x ∈ {z₀}ᶜ → f x = (x - z₀) ^ n • j x
hj_ne : m ≠ n
z : 𝕜
hfz : z ∈ {z₀}ᶜ → j z = (z - z₀) ^ (m - n) • g z
hfz' : z ∈ {z₀}ᶜ → f z = (z - z₀) ^ n • j z
hz : z ∈ {z₀}ᶜ
⊢ j z = (z - z₀) ^ (m - n) • g z
Module: Mathlib.Analysis.Analytic.IsolatedZeros

Goal state before:
pp: case pos
𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
U : Set 𝕜
A : Type u_3
inst✝⁶ : NormedRing A
inst✝⁵ : IsDomain A
inst✝⁴ : NormedAlgebra 𝕜 A
B : Type u_4
inst✝³ : NormedAddCommGroup B
inst✝² : NormedSpace 𝕜 B
inst✝¹ : Module A B
inst✝ : IsTorsionFree A B
f : 𝕜 → A
g : 𝕜 → B
hf : AnalyticOnNhd 𝕜 f U
hg : AnalyticOnNhd 𝕜 g U
hfg : ∀ z ∈ U, f z • g z = 0
hU : IsPreconnected U
hU' : ¬U = ∅
z : 𝕜
hz : z ∈ U
hU'' : U = {z}
⊢ (∀ z ∈ U, f z = 0) ∨ ∀ z ∈ U, g z = 0

Tactic:
simpa [hU''] using hfg z hz

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

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
hxs : UniqueDiffWithinAt 𝕜 s x
⊢ fderivWithin 𝕜 (⇑f) s x = f.contLinear

Tactic:
rw [DifferentiableAt.fderivWithin f.differentiableAt hxs]
  exact f.fderiv

Goal state after:
Module: Mathlib.Analysis.Calculus.MeanValue

Goal state before:
pp: case inr
f f' : ℝ → ℝ
a b : ℝ
hf : ContinuousOn f (Icc a b)
B B' : ℝ → ℝ
ha : f a ≤ B a
hB : ContinuousOn B (Icc a b)
hB' : ∀ x ∈ Ico a b, HasDerivWithinAt B (B' x) (Ici x) x
bound : ∀ x ∈ Ico a b, f x = B x → f' x < B' x
s : Set ℝ := {x | f x ≤ B x} ∩ Icc a b
A : ContinuousOn (fun x ↦ (f x, B x)) (Icc a b)
this : IsClosed s
x : ℝ
hxB✝ : f x ≤ B x
xab : x ∈ Ico a b
y : ℝ
hy : y ∈ Ioi x
hxB : f x = B x
r : ℝ
hf' : ∃ᶠ (z : ℝ) in 𝓝[>] x, slope f x z < r
hfr : f' x < r
hrB : r < B' x
⊢ ({x | f x ≤ B x} ∩ Ioc x y).Nonempty

Tactic:
have HB : ∀ᶠ z in 𝓝[>] x, r < slope B x z :=
      (hasDerivWithinAt_iff_tendsto_slope' <| lt_irrefl x).1 (hB' x xab).Ioi_of_Ici
        (Ioi_mem_nhds hrB)

Goal state after:
case inr
f f' : ℝ → ℝ
a b : ℝ
hf : ContinuousOn f (Icc a b)
B B' : ℝ → ℝ
ha : f a ≤ B a
hB : ContinuousOn B (Icc a b)
hB' : ∀ x ∈ Ico a b, HasDerivWithinAt B (B' x) (Ici x) x
bound : ∀ x ∈ Ico a b, f x = B x → f' x < B' x
s : Set ℝ := {x | f x ≤ B x} ∩ Icc a b
A : ContinuousOn (fun x ↦ (f x, B x)) (Icc a b)
this : IsClosed s
x : ℝ
hxB✝ : f x ≤ B x
xab : x ∈ Ico a b
y : ℝ
hy : y ∈ Ioi x
hxB : f x = B x
r : ℝ
hf' : ∃ᶠ (z : ℝ) in 𝓝[>] x, slope f x z < r
hfr : f' x < r
hrB : r < B' x
HB : ∀ᶠ (z : ℝ) in 𝓝[>] x, r < slope B x z
⊢ ({x | f x ≤ B x} ∩ Ioc x y).Nonempty