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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
r' : ℝ≥0
hf : HasFPowerSeriesWithinOnBall f p s x r
h : ↑r' < r
a : ℝ
ha : a ∈ Ioo 0 1
C : ℝ
hp : ∀ y ∈ Metric.ball 0 ↑r', ∀ (n : ℕ), x + y ∈ insert x s → ‖f (x + y) - p.partialSum n y‖ ≤ C * a ^ n
⊢ TendstoUniformlyOn (fun n y ↦ p.partialSum n y) (fun y ↦ f (x + y)) atTop
    ((fun x_1 ↦ x + x_1) ⁻¹' insert x s ∩ Metric.ball 0 ↑r')

Tactic:
refine Metric.tendstoUniformlyOn_iff.2 fun ε εpos => ?_

Goal state after:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
r' : ℝ≥0
hf : HasFPowerSeriesWithinOnBall f p s x r
h : ↑r' < r
a : ℝ
ha : a ∈ Ioo 0 1
C : ℝ
hp : ∀ y ∈ Metric.ball 0 ↑r', ∀ (n : ℕ), x + y ∈ insert x s → ‖f (x + y) - p.partialSum n y‖ ≤ C * a ^ n
ε : ℝ
εpos : ε > 0
⊢ ∀ᶠ (n : ℕ) in atTop,
    ∀ x_1 ∈ (fun x_2 ↦ x + x_2) ⁻¹' insert x s ∩ Metric.ball 0 ↑r', dist (f (x + x_1)) (p.partialSum n x_1) < ε
Module: Mathlib.Analysis.Analytic.Composition

Goal state before:
pp: case h'
⊢ ∀ (x : (n : ℕ) × Composition n), ∃ n, x ∈ compPartialSumTarget 0 n.1 n.2

Tactic:
· rintro ⟨n, c⟩
    simp only [mem_compPartialSumTarget_iff]
    obtain ⟨n, hn⟩ : BddAbove ((Finset.univ.image fun i : Fin c.length => c.blocksFun i) : Set ℕ) :=
      Finset.bddAbove _
    refine
      ⟨max n c.length + 1, bot_le, lt_of_le_of_lt (le_max_right n c.length) (lt_add_one _), fun j =>
        lt_of_le_of_lt (le_trans ?_ (le_max_left _ _)) (lt_add_one _)⟩
    apply hn
    simp only [Finset.mem_image_of_mem, Finset.mem_coe, Finset.mem_univ]

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

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
g : F → G
f : E → F
x : E
s : Set E
hg : AnalyticAt 𝕜 g (f x)
hf : AnalyticWithinAt 𝕜 f s x
⊢ AnalyticWithinAt 𝕜 (g ∘ f) s x

Tactic:
by
  rw [← analyticWithinAt_univ] at hg
  exact hg.comp hf (Set.mapsTo_univ _ _)

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
G' : Type u_5
inst✝¹ : NormedAddCommGroup G'
inst✝ : NormedSpace 𝕜 G'
L : G ≃L[𝕜] G'
f : E → F →L[𝕜] G
x : E
⊢ fderiv 𝕜 (⇑((ContinuousLinearEquiv.refl 𝕜 F).arrowCongr L) ∘ f) x =
    ↑((ContinuousLinearEquiv.refl 𝕜 F).arrowCongr L) ∘SL fderiv 𝕜 f x

Tactic:
rw [ContinuousLinearEquiv.comp_fderiv]

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:
← Finset.sum_add_sum_compl {a, b},

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
⊢ ((∑ i ∈ {a, b}, f fun j ↦ (Function.update (fun x ↦ g) i dg j) (v j)) +
      ∑ i ∈ {a, b}ᶜ, f fun j ↦ (Function.update (fun x ↦ g) i dg j) (v j)) =
    0
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
f : E → F
n : ℕ∞ω
p : E → FormalMultilinearSeries 𝕜 E F
⊢ HasFTaylorSeriesUpToOn n f p univ ↔ HasFTaylorSeriesUpTo n f p

Tactic:
constructor <;> refine fun H ↦ ⟨by simpa using H.zero_eq, ?_, by simpa using H.cont⟩

Goal state after:
case mp
𝕜 : 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 : ℕ∞ω
p : E → FormalMultilinearSeries 𝕜 E F
H : HasFTaylorSeriesUpToOn n f p univ
⊢ ∀ (m : ℕ), ↑m < n → ∀ (x : E), HasFDerivAt (fun y ↦ p y m) (p x m.succ).curryLeft x

case mpr
𝕜 : 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 : ℕ∞ω
p : E → FormalMultilinearSeries 𝕜 E F
H : HasFTaylorSeriesUpTo n f p
⊢ ∀ (m : ℕ), ↑m < n → ∀ x ∈ univ, HasFDerivWithinAt (fun x ↦ p x m) (p x m.succ).curryLeft univ x
Module: Mathlib.Analysis.Calculus.Deriv.Mul

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

Tactic:
by
  rw [← hasDerivWithinAt_univ] at *
  exact hc.mul_const d

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 ι
⊢ ∑ i, ((f.toFormalMultilinearSeries.changeOriginSeriesTerm 1 (Fintype.card ι - 1) ↑i ⋯) fun x_1 ↦ x) (Fin.snoc 0 y) =
    ∑ i, f (Function.update x i (y i))

Tactic:
Fin.snoc_zero

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 ι
⊢ (∑ i, ((f.toFormalMultilinearSeries.changeOriginSeriesTerm 1 (Fintype.card ι - 1) ↑i ⋯) fun x_1 ↦ x) fun x ↦ y) =
    ∑ i, f (Function.update x i (y i))
Module: Mathlib.Analysis.Analytic.Uniqueness

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
y : E
c : ℝ
c_pos : c > 0
t : Set E
t_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t
δ : ℝ
δ_pos : δ > 0
δε : Metric.ball 0 δ ⊆ t
n : ℕ
p : E [×n + 1]→L[𝕜] F
ht : ∀ y ∈ t, ‖p fun x ↦ y‖ ≤ c * ‖‖y‖ ^ (n + 1 + 1)‖
hy : 0 < ‖y‖
ε : ℝ
ε_pos : 0 < ε
h₀ : 0 < c * ‖y‖ ^ (n.succ + 1)
k : 𝕜
k_pos : 0 < ‖k‖
k_norm : ‖k‖ < min (δ * ‖y‖⁻¹) (ε * (c * ‖y‖ ^ (n.succ + 1))⁻¹)
h₁ : ‖k • y‖ < δ
h₂ : ‖p fun x ↦ k • y‖ ≤ ‖k‖ ^ n.succ * (‖k‖ * (c * ‖y‖ ^ (n.succ + 1)))
h₃ : ‖k‖ * (c * ‖y‖ ^ (n.succ + 1)) < ε
⊢ ‖(k⁻¹ * k) ^ n.succ‖ * (‖k‖ * (c * ‖y‖ ^ (n.succ + 1))) ≤ 0 + ε

Tactic:
rw [inv_mul_cancel₀ (norm_pos_iff.mp k_pos)]
        simpa using! h₃.le

Goal state after:
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 𝕜
⊢ HasDerivAtFilter f f' (L ×ˢ pure x) ↔ Tendsto (fun y ↦ slope f x y - (y - x)⁻¹ • (y - x) • f') L (𝓝 0)

Tactic:
by
      simp only [hasDerivAtFilter_iff_tendsto, prod_pure, tendsto_map'_iff, Function.comp_def,
        ← norm_inv, ← norm_smul, ← tendsto_zero_iff_norm_tendsto_zero, slope_def_module, smul_sub]

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

Goal state before:
pp: 𝕜 : Type u
inst✝³ : NontriviallyNormedField 𝕜
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : SeparableSpace 𝕜
f : 𝕜 → F
s t : Set 𝕜
ts : t ⊆ s
t_count : t.Countable
ht : s ⊆ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t
⊢ IsSeparable (range (derivWithin f s))

Tactic:
have : s ⊆ closure (s ∩ t) := by rwa [inter_eq_self_of_subset_right ts]

Goal state after:
𝕜 : Type u
inst✝³ : NontriviallyNormedField 𝕜
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : SeparableSpace 𝕜
f : 𝕜 → F
s t : Set 𝕜
ts : t ⊆ s
t_count : t.Countable
ht : s ⊆ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t
this : s ⊆ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (s ∩ t)
⊢ IsSeparable (range (derivWithin f s))
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_7
inst✝² : NormedCommRing 𝔸'
inst✝¹ : NormedAlgebra 𝕜 𝔸'
g : ι → E → 𝔸'
g' : ι → E →L[𝕜] 𝔸'
inst✝ : DecidableEq ι
u : Multiset ι
x : E
h : ∀ i ∈ u, HasFDerivWithinAt (fun x ↦ g i x) (g' i) s x
⊢ HasFDerivWithinAt (fun x ↦ (Multiset.map (fun x_1 ↦ g x_1 x) u).prod)
    (Multiset.map (fun i ↦ (Multiset.map (fun x_1 ↦ g x_1 x) (u.erase i)).prod •> g' i) u).sum s x

Tactic:
by
  simp only [← Multiset.attach_map_val u, Multiset.map_map]
  exact .congr_fderiv
    (hasFDerivAt_multiset_prod.comp_hasFDerivWithinAt x <|
      hasFDerivWithinAt_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.ZPow

Goal state before:
pp: case e'_9
𝕜 : Type u
inst✝ : NontriviallyNormedField 𝕜
m : ℤ
x : 𝕜
h : x ≠ 0 ∨ 0 ≤ m
this✝ : ∀ (m : ℤ), 0 < m → HasStrictDerivAt (fun x ↦ x ^ m) (↑m * x ^ (m - 1)) x
hm : m < 0
hx : x ≠ 0
this : HasStrictDerivAt (fun x ↦ x ^ m) (↑(-m) * x ^ (-m - 1) * -((x ^ m)⁻¹ ^ 2)⁻¹) x
⊢ ↑m * x ^ (m - 1) = ↑(-m) * x ^ (-m - 1) * -((x ^ m)⁻¹ ^ 2)⁻¹

Tactic:
sq,

Goal state after:
case e'_9
𝕜 : Type u
inst✝ : NontriviallyNormedField 𝕜
m : ℤ
x : 𝕜
h : x ≠ 0 ∨ 0 ≤ m
this✝ : ∀ (m : ℤ), 0 < m → HasStrictDerivAt (fun x ↦ x ^ m) (↑m * x ^ (m - 1)) x
hm : m < 0
hx : x ≠ 0
this : HasStrictDerivAt (fun x ↦ x ^ m) (↑(-m) * x ^ (-m - 1) * -((x ^ m)⁻¹ ^ 2)⁻¹) x
⊢ ↑m * x ^ (m - 1) = ↑(-m) * x ^ (-m - 1) * -((x ^ m)⁻¹ * (x ^ m)⁻¹)⁻¹
Module: Mathlib.Analysis.Calculus.Deriv.AffineMap

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 →ᵃ[𝕜] E
L : Filter (𝕜 × 𝕜)
⊢ HasDerivAtFilter (⇑f) (f.linear 1) L

Tactic:
f.decomp

Goal state after:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 →ᵃ[𝕜] E
L : Filter (𝕜 × 𝕜)
⊢ HasDerivAtFilter (⇑f.linear + fun x ↦ f 0) (f.linear 1) L
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
s : Set E
x : E
n : ℕ∞ω
f : E → F
g : F →ₗᵢ[𝕜] G
hf : ContDiffWithinAt 𝕜 n f s x
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
i : ℕ
hi : ↑i ≤ n
⊢ ‖iteratedFDerivWithin 𝕜 i (⇑g ∘ f) s x‖ = ‖iteratedFDerivWithin 𝕜 i f s x‖

Tactic:
by
  have :
    iteratedFDerivWithin 𝕜 i (g ∘ f) s x =
      g.toContinuousLinearMap.compContinuousMultilinearMap (iteratedFDerivWithin 𝕜 i f s x) :=
    g.toContinuousLinearMap.iteratedFDerivWithin_comp_left hf hs hx hi
  rw [this]
  apply LinearIsometry.norm_compContinuousMultilinearMap

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

Goal state before:
pp: 𝕜 : Type u_3
inst✝⁴ : RCLike 𝕜
G : Type u_4
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
H : Type u_5
inst✝¹ : NormedAddCommGroup H
inst✝ : NormedSpace 𝕜 H
f : G → H
f' : G → G →L[𝕜] H
x : G
hder : ∀ᶠ (y : G) in 𝓝 x, HasFDerivAt f (f' y) y
hcont : ContinuousAt f' x
⊢ HasStrictFDerivAt f (f' x) x

Tactic:
rw [hasStrictFDerivAt_iff_isLittleO, isLittleO_iff]
  refine fun c hc => Metric.eventually_nhds_iff_ball.mpr ?_
  -- the correct ε is the modulus of continuity of f'
  rcases Metric.mem_nhds_iff.mp (inter_mem hder (hcont <| ball_mem_nhds _ hc)) with ⟨ε, ε0, hε⟩
  refine ⟨ε, ε0, ?_⟩
  -- simplify formulas involving the product E × E
  rintro ⟨a, b⟩ h
  rw [← ball_prod_same, prodMk_mem_set_prod_eq] at h
  -- exploit the choice of ε as the modulus of continuity of f'
  have hf' : ∀ x' ∈ ball x ε, ‖f' x' - f' x‖ ≤ c := fun x' H' => by
    rw [← dist_eq_norm]
    exact le_of_lt (hε H').2
  -- apply mean value theorem
  let : NormedSpace ℝ G := .restrictScalars ℝ 𝕜 G
  refine (convex_ball _ _).norm_image_sub_le_of_norm_hasFDerivWithin_le' ?_ hf' h.2 h.1
  exact fun y hy => (hε hy).1.hasFDerivWithinAt

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

Goal state before:
pp: case h₁
𝕜 : 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
s : Set E
x : E
n : ℕ∞ω
f : E → F
g : E → G
hf : ContDiffWithinAt 𝕜 n f s x
hg : ContDiffWithinAt 𝕜 n g s x
hs : UniqueDiffOn 𝕜 s
ha : x ∈ s
i : ℕ
hi : ↑i ≤ n
x✝ : Fin i → E
⊢ ((ContinuousLinearMap.fst 𝕜 F G).compContinuousMultilinearMap (iteratedFDerivWithin 𝕜 i (fun x ↦ (f x, g x)) s x))
      x✝ =
    ((ContinuousLinearMap.fst 𝕜 F G).compContinuousMultilinearMap
        ((iteratedFDerivWithin 𝕜 i f s x).prod (iteratedFDerivWithin 𝕜 i g s x)))
      x✝

Tactic:
rw [← ContinuousLinearMap.iteratedFDerivWithin_comp_left _ (hf.prodMk hg) hs ha hi]
    simp [Function.comp_def]

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

Goal state before:
pp: case h₂
𝕜 : 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
s : Set E
x : E
n : ℕ∞ω
f : E → F
g : E → G
hf : ContDiffWithinAt 𝕜 n f s x
hg : ContDiffWithinAt 𝕜 n g s x
hs : UniqueDiffOn 𝕜 s
ha : x ∈ s
i : ℕ
hi : ↑i ≤ n
x✝ : Fin i → E
⊢ ((ContinuousLinearMap.snd 𝕜 F G).compContinuousMultilinearMap (iteratedFDerivWithin 𝕜 i (fun x ↦ (f x, g x)) s x))
      x✝ =
    ((ContinuousLinearMap.snd 𝕜 F G).compContinuousMultilinearMap
        ((iteratedFDerivWithin 𝕜 i f s x).prod (iteratedFDerivWithin 𝕜 i g s x)))
      x✝

Tactic:
rw [← ContinuousLinearMap.iteratedFDerivWithin_comp_left _ (hf.prodMk hg) hs ha hi]
    simp [Function.comp_def]

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

Goal state before:
pp: n : ℕ
c : OrderedFinpartition n
m : Fin c.length
r r' : Fin (c.partSize m)
h : c.emb m r = c.emb m r'
⊢ ⟨m, r⟩ = ⟨m, r'⟩

Tactic:
simpa using (c.emb_strictMono m).injective h

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

Goal state before:
pp: case inr
n : ℕ
c : OrderedFinpartition (n + 1)
hc : range (c.emb 0) ≠ {0}
this✝ : c.partSize (c.index 0) = Nat.card ↑(range (c.emb (c.index 0)))
h : c.index 0 ≠ 0
this : {c.emb (c.index 0) 0, c.emb (c.index 0) ⟨c.partSize (c.index 0) - 1, ⋯⟩} ⊆ range (c.emb (c.index 0))
⊢ 2 ≤ Nat.card ↑(range (c.emb (c.index 0)))

Tactic:
simp only [emb_zero] at this

Goal state after:
case inr
n : ℕ
c : OrderedFinpartition (n + 1)
hc : range (c.emb 0) ≠ {0}
this✝ : c.partSize (c.index 0) = Nat.card ↑(range (c.emb (c.index 0)))
h : c.index 0 ≠ 0
this : {0, c.emb (c.index 0) ⟨c.partSize (c.index 0) - 1, ⋯⟩} ⊆ range (c.emb (c.index 0))
⊢ 2 ≤ Nat.card ↑(range (c.emb (c.index 0)))
Module: Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno

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
s : Set E
t : Set F
q : F → FormalMultilinearSeries 𝕜 F G
p : E → FormalMultilinearSeries 𝕜 E F
n : ℕ
c✝ c : OrderedFinpartition n
⊢ ∀ (i : Fin c.length), 0 < cons 1 c.partSize i.succ

Tactic:
by simp [c.partSize_pos]

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

Goal state before:
pp: case succ
𝕜 : 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✝ c : OrderedFinpartition n
i : Fin (c.length + 1)
j : Fin c.length
a✝ :
  i < j.castSucc →
    (fun m ↦
          cases (motive := fun x ↦ Fin (cons 1 c.partSize x) → Fin (n + 1)) (fun x ↦ 0) (fun m ↦ succ ∘ c.emb m) m
            ⟨cons 1 c.partSize m - 1, ⋯⟩)
        i <
      (fun m ↦
          cases (motive := fun x ↦ Fin (cons 1 c.partSize x) → Fin (n + 1)) (fun x ↦ 0) (fun m ↦ succ ∘ c.emb m) m
            ⟨cons 1 c.partSize m - 1, ⋯⟩)
        j.castSucc
hij : i < j.succ
⊢ (fun m ↦
        cases (motive := fun x ↦ Fin (cons 1 c.partSize x) → Fin (n + 1)) (fun x ↦ 0) (fun m ↦ succ ∘ c.emb m) m
          ⟨cons 1 c.partSize m - 1, ⋯⟩)
      i <
    (fun m ↦
        cases (motive := fun x ↦ Fin (cons 1 c.partSize x) → Fin (n + 1)) (fun x ↦ 0) (fun m ↦ succ ∘ c.emb m) m
          ⟨cons 1 c.partSize m - 1, ⋯⟩)
      j.succ

Tactic:
induction i using Fin.induction with
      | zero => simp
      | succ i =>
        simp only [cons_succ, cases_succ, comp_apply, succ_lt_succ_iff]
        exact c.parts_strictMono (by simpa using hij)

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

Goal state before:
pp: 𝕂 : Type u_1
𝔸 : Type u_2
𝔹 : Type u_3
inst✝⁵ : NontriviallyNormedField 𝕂
inst✝⁴ : NormedRing 𝔸
inst✝³ : NormedRing 𝔹
inst✝² : NormedAlgebra 𝕂 𝔸
inst✝¹ : CompleteSpace 𝔸
inst✝ : CharZero 𝕂
x : 𝔸
hx : x ∈ Metric.eball 0 (expSeries 𝕂 𝔸).radius
⊢ exp (-x) * exp x = 1

Tactic:
by
    have hnx : -x ∈ Metric.eball (0 : 𝔸) (expSeries 𝕂 𝔸).radius := by
      rw [Metric.mem_eball, ← neg_zero, edist_neg_neg]
      exact hx
    rw [← exp_add_of_commute_of_mem_ball (Commute.neg_left <| Commute.refl x) hnx hx,
      neg_add_cancel, exp_zero]

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

Goal state before:
pp: 𝔸 : Type u_1
inst✝² : NormedRing 𝔸
inst✝¹ : NormedAlgebra ℚ 𝔸
inst✝ : CompleteSpace 𝔸
x a b : 𝔸
h : SemiconjBy x a b
⊢ SemiconjBy x (exp a) (exp b)

Tactic:
by
  rw [exp_eq_tsum ℚ]
  apply SemiconjBy.tsum_right x (expSeries_summable' _) (expSeries_summable' _)
  exact fun _ ↦ h.pow_right _ |>.smul_right _

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

Goal state before:
pp: case insert
𝔸 : Type u_1
inst✝² : NormedRing 𝔸
inst✝¹ : NormedAlgebra ℚ 𝔸
inst✝ : CompleteSpace 𝔸
ι : Type u_3
f : ι → 𝔸
a : ι
s : Finset ι
ha : a ∉ s
ih : ∀ (h : (↑s).Pairwise (Commute on f)), exp (∑ i ∈ s, f i) = s.noncommProd (fun i ↦ exp (f i)) ⋯
h : (↑(insert a s)).Pairwise (Commute on f)
⊢ Commute (f a) (∑ x ∈ s, f x)

Tactic:
refine Commute.sum_right _ _ _ fun i hi => ?_

Goal state after:
case insert
𝔸 : Type u_1
inst✝² : NormedRing 𝔸
inst✝¹ : NormedAlgebra ℚ 𝔸
inst✝ : CompleteSpace 𝔸
ι : Type u_3
f : ι → 𝔸
a : ι
s : Finset ι
ha : a ∉ s
ih : ∀ (h : (↑s).Pairwise (Commute on f)), exp (∑ i ∈ s, f i) = s.noncommProd (fun i ↦ exp (f i)) ⋯
h : (↑(insert a s)).Pairwise (Commute on f)
i : ι
hi : i ∈ s
⊢ Commute (f a) (f i)
Module: Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno

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
s : Set E
t : Set F
q : F → FormalMultilinearSeries 𝕜 F G
p : E → FormalMultilinearSeries 𝕜 E F
n : ℕ
c : OrderedFinpartition n
⊢ (F [×c.length]→L[𝕜] G) →L[𝕜] (E [×c.partSize i]→L[𝕜] F) [×c.length]→L[𝕜] E [×n]→L[𝕜] G

Tactic:
refine MultilinearMap.mkContinuousLinear c.compAlongOrderedFinpartitionₗ 1 fun f p ↦ ?_
  simp only [one_mul, compAlongOrderedFinpartitionₗ_apply_apply]
  apply norm_compAlongOrderedFinpartition_le

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

Goal state before:
pp: case left
β : Type v
inst✝ : NormedField β
f : CauSeq β norm
s : Set (β × β)
hs : s ∈ uniformity β
ε : ℝ
hε : ε > 0
hεs : ∀ ⦃a b : β⦄, dist a b < ε → (a, b) ∈ s
N : ℕ
hN : ∀ j ≥ N, ∀ k ≥ N, ‖↑f j - ↑f k‖ < ε
b : ℕ
hb : N ≤ b
⊢ b ∈ ↑f ⁻¹' ↑f '' {n | n ≥ N}

Tactic:
exists b

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

Goal state before:
pp: case hg
𝕜 : 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
hq : ∀ (n : ℕ), AnalyticOn 𝕜 (fun x ↦ q x n) t
hp : ∀ (n : ℕ), AnalyticOn 𝕜 (fun x ↦ p x n) s
f : E → F
hf : AnalyticOn 𝕜 f s
h : MapsTo f s t
n : ℕ
c : OrderedFinpartition n
x✝ : c ∈ Finset.univ
B : (F [×c.length]→L[𝕜] G) →L[𝕜] (E [×c.partSize i]→L[𝕜] F) [×c.length]→L[𝕜] E [×n]→L[𝕜] G := ⋯
⊢ AnalyticOn 𝕜 (fun x m ↦ p x (c.partSize m)) s

Tactic:
exact AnalyticOn.pi (fun i ↦ hp _)

Goal state after:
Module: Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas

Goal state before:
pp: case succ.hf
𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
F : Type u_2
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜 F
n✝ : ℕ
x : 𝕜
s : Set 𝕜
hx : x ∈ s
h : UniqueDiffOn 𝕜 s
𝔸 : Type u_5
inst✝⁴ : NormedRing 𝔸
inst✝³ : NormedAlgebra 𝕜 𝔸
inst✝² : Module 𝔸 F
inst✝¹ : IsBoundedSMul 𝔸 F
inst✝ : IsScalarTower 𝕜 𝔸 F
n : ℕ
IH :
  ∀ {f : 𝕜 → 𝔸} {g : 𝕜 → F},
    ContDiffWithinAt 𝕜 (↑n) f s x →
      ContDiffWithinAt 𝕜 (↑n) g s x →
        iteratedDerivWithin n (f • g) s x =
          ∑ i ∈ Finset.range (n + 1), n.choose i • iteratedDerivWithin i f s x • iteratedDerivWithin (n - i) g s x
f : 𝕜 → 𝔸
g : 𝕜 → F
hf : ContDiffWithinAt 𝕜 (↑(n + 1)) f s x
hg : ContDiffWithinAt 𝕜 (↑(n + 1)) g s x
U : Set 𝕜
hU : U ∈ 𝓝[insert x s] x
H : ∀ y ∈ U, ContDiffWithinAt 𝕜 (↑(n + 1)) f s y ∧ ContDiffWithinAt 𝕜 (↑(n + 1)) g s y
⊢ ContDiffWithinAt 𝕜 (↑n) (derivWithin f s) s x

Tactic:
clear IH H U hU

Goal state after:
case succ.hf
𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
F : Type u_2
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜 F
n✝ : ℕ
x : 𝕜
s : Set 𝕜
hx : x ∈ s
h : UniqueDiffOn 𝕜 s
𝔸 : Type u_5
inst✝⁴ : NormedRing 𝔸
inst✝³ : NormedAlgebra 𝕜 𝔸
inst✝² : Module 𝔸 F
inst✝¹ : IsBoundedSMul 𝔸 F
inst✝ : IsScalarTower 𝕜 𝔸 F
n : ℕ
f : 𝕜 → 𝔸
g : 𝕜 → F
hf : ContDiffWithinAt 𝕜 (↑(n + 1)) f s x
hg : ContDiffWithinAt 𝕜 (↑(n + 1)) g s x
⊢ ContDiffWithinAt 𝕜 (↑n) (derivWithin f s) s x