mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.MvPowerSeries.Substitution

Goal state before:
pp: case e_a.e_a
σ : Type u_1
A : Type u_2
inst✝²¹ : CommSemiring A
R✝ : Type u_3
inst✝²⁰ : CommRing R✝
inst✝¹⁹ : Algebra A R✝
τ : Type u_4
S : Type u_5
inst✝¹⁸ : CommRing S
inst✝¹⁷ : Algebra A S
inst✝¹⁶ : Algebra R✝ S
inst✝¹⁵ : IsScalarTower A R✝ S
a✝¹ a✝ : σ → MvPowerSeries τ S
T✝ : Type u_6
inst✝¹⁴ : CommRing T✝
inst✝¹³ : UniformSpace T✝
inst✝¹² : T2Space T✝
inst✝¹¹ : CompleteSpace T✝
inst✝¹⁰ : IsUniformAddGroup T✝
inst✝⁹ : IsTopologicalRing T✝
inst✝⁸ : IsLinearTopology T✝ T✝
inst✝⁷ : Algebra R✝ T✝
ε : MvPowerSeries τ S →ₐ[R✝] T✝
inst✝⁶ : Algebra S T✝
inst✝⁵ : IsScalarTower R✝ S T✝
υ : Type u_7
T : Type u_8
inst✝⁴ : CommRing T
inst✝³ : Algebra R✝ T
inst✝² : Algebra S T
inst✝¹ : IsScalarTower R✝ S T
b : τ → MvPowerSeries υ T
R : Type u_9
inst✝ : CommSemiring R
a : σ → R
f g : MvPowerSeries σ R
n : σ →₀ ℕ
x : (σ →₀ ℕ) × (σ →₀ ℕ)
hx : x.1 + x.2 = n
⊢ ∏ x_1 ∈ x.1.support ∪ x.2.support, a x_1 ^ (x.1 + x.2) x_1 =
    (∏ x_1 ∈ x.1.support ∪ ?m.185, a x_1 ^ x.1 x_1) * ∏ x_1 ∈ ?m.199 ∪ x.2.support, a x_1 ^ x.2 x_1

Tactic:
← Finset.prod_mul_distrib

Goal state after:
case e_a.e_a
σ : Type u_1
A : Type u_2
inst✝²¹ : CommSemiring A
R✝ : Type u_3
inst✝²⁰ : CommRing R✝
inst✝¹⁹ : Algebra A R✝
τ : Type u_4
S : Type u_5
inst✝¹⁸ : CommRing S
inst✝¹⁷ : Algebra A S
inst✝¹⁶ : Algebra R✝ S
inst✝¹⁵ : IsScalarTower A R✝ S
a✝¹ a✝ : σ → MvPowerSeries τ S
T✝ : Type u_6
inst✝¹⁴ : CommRing T✝
inst✝¹³ : UniformSpace T✝
inst✝¹² : T2Space T✝
inst✝¹¹ : CompleteSpace T✝
inst✝¹⁰ : IsUniformAddGroup T✝
inst✝⁹ : IsTopologicalRing T✝
inst✝⁸ : IsLinearTopology T✝ T✝
inst✝⁷ : Algebra R✝ T✝
ε : MvPowerSeries τ S →ₐ[R✝] T✝
inst✝⁶ : Algebra S T✝
inst✝⁵ : IsScalarTower R✝ S T✝
υ : Type u_7
T : Type u_8
inst✝⁴ : CommRing T
inst✝³ : Algebra R✝ T
inst✝² : Algebra S T
inst✝¹ : IsScalarTower R✝ S T
b : τ → MvPowerSeries υ T
R : Type u_9
inst✝ : CommSemiring R
a : σ → R
f g : MvPowerSeries σ R
n : σ →₀ ℕ
x : (σ →₀ ℕ) × (σ →₀ ℕ)
hx : x.1 + x.2 = n
⊢ ∏ x_1 ∈ x.1.support ∪ x.2.support, a x_1 ^ (x.1 + x.2) x_1 =
    ∏ x_1 ∈ x.1.support ∪ x.2.support, a x_1 ^ x.1 x_1 * a x_1 ^ x.2 x_1
Module: Mathlib.RingTheory.PowerSeries.Substitution

Goal state before:
pp: case succ.succ
R : Type u_2
inst✝¹ : CommRing R
P : R⟦X⟧
hP : constantCoeff P = 0
inst✝ : Invertible ((coeff 1) P)
n : ℕ
⊢ (coeff (n + 1 + 1))
      (subst
          (∑ i, C (P.substInvFun ↑i.castSucc) * X ^ ↑i.castSucc +
            C (P.substInvFun ↑(Fin.last (n + 2))) * X ^ ↑(Fin.last (n + 2)))
          P -
        X) =
    0

Tactic:
simp only [Fin.val_castSucc, Fin.val_last, map_sub, substInvFun]

Goal state after:
case succ.succ
R : Type u_2
inst✝¹ : CommRing R
P : R⟦X⟧
hP : constantCoeff P = 0
inst✝ : Invertible ((coeff 1) P)
n : ℕ
⊢ (coeff (n + 1 + 1))
        (subst
          (∑ x, C (P.substInvFun ↑x) * X ^ ↑x +
            C (-⅟((coeff 1) P) * (coeff (n + 1 + 1)) (subst (∑ i, C (P.substInvFun ↑i) * X ^ ↑i) P)) * X ^ (n + 2))
          P) -
      (coeff (n + 1 + 1)) X =
    0
Module: Mathlib.RingTheory.PowerSeries.Substitution

Goal state before:
pp: R : Type u_2
inst✝ : CommRing R
f : R⟦X⟧
e : Fin 2 →₀ ℕ
b : (Fin 2 →₀ ℕ) × (Fin 2 →₀ ℕ)
hb : b ∈ antidiagonal e
⊢ b ≠ (single 0 (e 0), single 1 (e 1)) →
    (MvPowerSeries.coeff b.1) (subst X₀ f) * (MvPowerSeries.coeff b.2) (subst X₁ f) = 0

Tactic:
hb'

Goal state after:
R : Type u_2
inst✝ : CommRing R
f : R⟦X⟧
e : Fin 2 →₀ ℕ
b : (Fin 2 →₀ ℕ) × (Fin 2 →₀ ℕ)
hb : b ∈ antidiagonal e
hb' : b ≠ (single 0 (e 0), single 1 (e 1))
⊢ (MvPowerSeries.coeff b.1) (subst X₀ f) * (MvPowerSeries.coeff b.2) (subst X₁ f) = 0
Module: Mathlib.Analysis.Calculus.FDeriv.Basic

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : TopologicalSpace E
F : Type u_3
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 F
inst✝ : TopologicalSpace F
f : E → F
x : E
h : ¬DifferentiableAt 𝕜 f x
⊢ fderiv 𝕜 f x = 0

Tactic:
rw [fderiv, fderivWithin_zero_of_not_differentiableWithinAt]

Goal state after:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : TopologicalSpace E
F : Type u_3
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 F
inst✝ : TopologicalSpace F
f : E → F
x : E
h : ¬DifferentiableAt 𝕜 f x
⊢ ¬DifferentiableWithinAt 𝕜 f univ x
Module: Mathlib.Analysis.Calculus.FDeriv.Basic

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module 𝕜 E
inst✝⁴ : TopologicalSpace E
F : Type u_3
inst✝³ : AddCommGroup F
inst✝² : Module 𝕜 F
inst✝¹ : TopologicalSpace F
f : E → F
f' : E →L[𝕜] F
x : E
s : Set E
inst✝ : T1Space E
y : E
⊢ HasFDerivWithinAt f f' (s \ {y}) x ↔ HasFDerivWithinAt f f' s x

Tactic:
rw [← hasFDerivWithinAt_insert, insert_sdiff_singleton, hasFDerivWithinAt_insert]

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : TopologicalSpace E
F : Type u_3
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 F
inst✝ : TopologicalSpace F
f : E → F
f' : E →L[𝕜] F
x : E
hf : HasStrictFDerivAt f f' x
⊢ (fun x' ↦ f x' - f x - f' (x' - x)) =o[𝕜; 𝓝 x] fun x' ↦ x' - x

Tactic:
simpa only using! hf.isLittleOTVS.comp_tendsto (tendsto_id.prodMk_nhds tendsto_const_nhds)

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

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
f' : E →L[𝕜] F
x₀ : E
hf : HasFDerivAt f f' x₀
C : ℝ
hC₀ : 0 ≤ C
hlip : ∀ᶠ (a : E) in 𝓝 0, ‖f (x₀ + a) - f x₀‖ ≤ C * ‖x₀ + a - x₀‖
ε : ℝ
ε0 : 0 < ε
y : E
hy : ‖f (x₀ + y) - f x₀ - f' y‖ ≤ ε * ‖y‖
⊢ ‖f (x₀ + y) - f x₀‖ ≤ C * ‖x₀ + y - x₀‖ → ‖f' y‖ ≤ (C + ε) * ‖y‖

Tactic:
hyC

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
f' : E →L[𝕜] F
x₀ : E
hf : HasFDerivAt f f' x₀
C : ℝ
hC₀ : 0 ≤ C
hlip : ∀ᶠ (a : E) in 𝓝 0, ‖f (x₀ + a) - f x₀‖ ≤ C * ‖x₀ + a - x₀‖
ε : ℝ
ε0 : 0 < ε
y : E
hy : ‖f (x₀ + y) - f x₀ - f' y‖ ≤ ε * ‖y‖
hyC : ‖f (x₀ + y) - f x₀‖ ≤ C * ‖x₀ + y - x₀‖
⊢ ‖f' y‖ ≤ (C + ε) * ‖y‖
Module: Mathlib.Analysis.Calculus.FDeriv.Basic

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
f' : E →L[𝕜] F
x₀ : E
hf : HasFDerivAt f f' x₀
C : ℝ
hC₀ : 0 ≤ C
hlip : ∀ᶠ (x : E) in 𝓝 x₀, ‖f x - f x₀‖ ≤ C * ‖x - x₀‖
⊢ ‖f'‖ ≤ C

Tactic:
refine le_of_forall_pos_le_add fun ε ε0 => opNorm_le_of_nhds_zero ?_ ?_
  · exact add_nonneg hC₀ ε0.le
  rw [← map_add_left_nhds_zero x₀, eventually_map] at hlip
  filter_upwards [isLittleO_iff.1 (hasFDerivAt_iff_isLittleO_nhds_zero.1 hf) ε0, hlip] with y hy hyC
  rw [add_sub_cancel_left] at hyC
  calc
    ‖f' y‖ ≤ ‖f (x₀ + y) - f x₀‖ + ‖f (x₀ + y) - f x₀ - f' y‖ := norm_le_insert _ _
    _ ≤ C * ‖y‖ + ε * ‖y‖ := add_le_add hyC hy
    _ = (C + ε) * ‖y‖ := (add_mul _ _ _).symm

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

Goal state before:
pp: case zero
𝕜 : Type u
E : Type v
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
n : ℕ
p : FormalMultilinearSeries 𝕜 𝕜 E
⊢ (fslope^[0] p).coeff n = p.coeff (n + 0)

Tactic:
| zero =>

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

Goal state before:
pp: case zero
𝕜 : Type u
E : Type v
F : Type w
G : Type x
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
p : FormalMultilinearSeries 𝕜 F G
v : Fin 0 → E
⊢ (p.compContinuousLinearMap 0 0) v = (constFormalMultilinearSeries 𝕜 E ((p 0) 0) 0) v

Tactic:
| zero =>

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

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
inst✝ : CompleteSpace F
p : FormalMultilinearSeries 𝕜 E F
x y : E
h : ↑‖x‖₊ + ↑‖y‖₊ < p.radius
x_mem_ball : x ∈ Metric.eball 0 p.radius
y_mem_ball : y ∈ Metric.eball 0 (p.changeOrigin x).radius
x_add_y_mem_ball : x + y ∈ Metric.eball 0 p.radius
⊢ (p.changeOrigin x).sum y = p.sum (x + y)

Tactic:
set f : (Σ k l : ℕ, { s : Finset (Fin (k + l)) // s.card = l }) → F := fun s =>
    p.changeOriginSeriesTerm s.1 s.2.1 s.2.2 s.2.2.2 (fun _ => x) fun _ => y

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
inst✝ : CompleteSpace F
p : FormalMultilinearSeries 𝕜 E F
x y : E
h : ↑‖x‖₊ + ↑‖y‖₊ < p.radius
x_mem_ball : x ∈ Metric.eball 0 p.radius
y_mem_ball : y ∈ Metric.eball 0 (p.changeOrigin x).radius
x_add_y_mem_ball : x + y ∈ Metric.eball 0 p.radius
f : (k : ℕ) × (l : ℕ) × { s // s.card = l } → F :=
  fun s ↦ ((p.changeOriginSeriesTerm s.fst s.snd.fst ↑s.snd.snd ⋯) fun x_1 ↦ x) fun x ↦ y
⊢ (p.changeOrigin x).sum y = p.sum (x + y)
Module: Mathlib.Analysis.Analytic.ConvergenceRadius

Goal state before:
pp: case inr
𝕜 : Type u_1
E : Type u_3
F : Type u_4
G : Type u_5
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
p : FormalMultilinearSeries 𝕜 F G
u : E →L[𝕜] F
h_zero : 0 < ‖u‖₊
⊢ p.radius ≤ (p.compContinuousLinearMap u).radius * ‖u‖ₑ

Tactic:
refine le_of_forall_nnreal_lt fun r hr ↦ ?_

Goal state after:
case inr
𝕜 : Type u_1
E : Type u_3
F : Type u_4
G : Type u_5
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
p : FormalMultilinearSeries 𝕜 F G
u : E →L[𝕜] F
h_zero : 0 < ‖u‖₊
r : ℝ≥0
hr : ↑r < p.radius
⊢ ↑r ≤ (p.compContinuousLinearMap u).radius * ‖u‖ₑ
Module: Mathlib.Analysis.Analytic.CPolynomialDef

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
p : FormalMultilinearSeries 𝕜 E F
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → p m = 0
k : ℕ
⊢ ∀ {m : ℕ}, n ≤ k + m → p.changeOriginSeries k m = 0

Tactic:
intro m hm
  rw [changeOriginSeries]
  exact Finset.sum_eq_zero (fun _ _ => p.changeOriginSeriesTerm_bound hn _ _ _ hm)

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

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
x : E
p : FormalMultilinearSeries 𝕜 E F
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → p m = 0
k : ℕ
hk : n ≤ k
⊢ p.changeOrigin x k = 0

Tactic:
changeOrigin,

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
x : E
p : FormalMultilinearSeries 𝕜 E F
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → p m = 0
k : ℕ
hk : n ≤ k
⊢ (p.changeOriginSeries k).sum x = 0
Module: Mathlib.Analysis.Analytic.OfScalars

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedRing E
inst✝¹ : NormedAlgebra 𝕜 E
c : ℕ → 𝕜
inst✝ : NormOneClass E
r : ℝ≥0
hr : r ≠ 0
hc : Tendsto (fun n ↦ ‖c n‖ / ‖c n.succ‖) atTop (𝓝 ↑r)
this : Tendsto (fun n ↦ ‖c n.succ‖ / ‖c n‖) atTop (𝓝 (↑r)⁻¹)
⊢ (ofScalars E c).radius = ↑r

Tactic:
convert! ofScalars_radius_eq_inv_of_tendsto E c (inv_ne_zero hr) this
    simp

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

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
p : FormalMultilinearSeries 𝕜 E F
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → p m = 0
x y : E
f : (k : ℕ) × (l : ℕ) × { s // s.card = l } → F :=
  fun s ↦ ((p.changeOriginSeriesTerm s.fst s.snd.fst ↑s.snd.snd ⋯) fun x_1 ↦ x) fun x ↦ y
finsupp : (Function.support f).Finite
k l : ℕ
⊢ HasSum (fun x ↦ f ⟨k, ⟨l, x⟩⟩) (((∑ s, p.changeOriginSeriesTerm k l ↑s ⋯) fun x_1 ↦ x) fun x ↦ y)

Tactic:
sum_apply

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
p : FormalMultilinearSeries 𝕜 E F
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → p m = 0
x y : E
f : (k : ℕ) × (l : ℕ) × { s // s.card = l } → F :=
  fun s ↦ ((p.changeOriginSeriesTerm s.fst s.snd.fst ↑s.snd.snd ⋯) fun x_1 ↦ x) fun x ↦ y
finsupp : (Function.support f).Finite
k l : ℕ
⊢ HasSum (fun x ↦ f ⟨k, ⟨l, x⟩⟩) (∑ i, ((p.changeOriginSeriesTerm k l ↑i ⋯) fun x_1 ↦ x) fun x ↦ y)
Module: Mathlib.Analysis.Analytic.CPolynomialDef

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
p : FormalMultilinearSeries 𝕜 E F
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → p m = 0
x y : E
f : (k : ℕ) × (l : ℕ) × { s // s.card = l } → F :=
  fun s ↦ ((p.changeOriginSeriesTerm s.fst s.snd.fst ↑s.snd.snd ⋯) fun x_1 ↦ x) fun x ↦ y
finsupp : (Function.support f).Finite
hfkl : ∀ (k l : ℕ), HasSum (fun x ↦ f ⟨k, ⟨l, x⟩⟩) (((p.changeOriginSeries k l) fun x_1 ↦ x) fun x ↦ y)
k : ℕ
this : ∀ m ∉ Finset.range n, ((p.changeOriginSeries k m) fun x_1 ↦ x) = 0
⊢ HasSum (fun x ↦ f ⟨k, x⟩) ((p.changeOrigin x k) fun x ↦ y)

Tactic:
changeOrigin,

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
p : FormalMultilinearSeries 𝕜 E F
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → p m = 0
x y : E
f : (k : ℕ) × (l : ℕ) × { s // s.card = l } → F :=
  fun s ↦ ((p.changeOriginSeriesTerm s.fst s.snd.fst ↑s.snd.snd ⋯) fun x_1 ↦ x) fun x ↦ y
finsupp : (Function.support f).Finite
hfkl : ∀ (k l : ℕ), HasSum (fun x ↦ f ⟨k, ⟨l, x⟩⟩) (((p.changeOriginSeries k l) fun x_1 ↦ x) fun x ↦ y)
k : ℕ
this : ∀ m ∉ Finset.range n, ((p.changeOriginSeries k m) fun x_1 ↦ x) = 0
⊢ HasSum (fun x ↦ f ⟨k, x⟩) (((p.changeOriginSeries k).sum x) fun x ↦ y)
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
hf : HasFPowerSeriesAt f p x
⊢ HasFPowerSeriesWithinAt f p s x

Tactic:
rw [← hasFPowerSeriesWithinAt_univ] at hf
  apply hf.mono (subset_univ _)

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

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
r : ℝ≥0∞
n : ℕ
x y : E
hf : HasFiniteFPowerSeriesOnBall f p x n r
h : ↑‖y‖₊ < r
z : E
hz : ↑‖y‖₊ + ‖z‖ₑ < r
⊢ f (x + y + z) = (p.changeOrigin y).sum z

Tactic:
rw [p.changeOrigin_eval_of_finite hf.finite, add_assoc, hf.sum]

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
r : ℝ≥0∞
n : ℕ
x y : E
hf : HasFiniteFPowerSeriesOnBall f p x n r
h : ↑‖y‖₊ < r
z : E
hz : ↑‖y‖₊ + ‖z‖ₑ < r
⊢ y + z ∈ Metric.eball 0 r
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∞
y : E
hf : HasFPowerSeriesWithinOnBall f p s x r
hy : y ∈ Metric.eball 0 r
h'y : x + y ∈ insert x s
A✝ : Tendsto (fun z ↦ p.partialSum z.1 y) (atTop ×ˢ 𝓝 y) (𝓝 (f (x + y)))
ε : ℝ
εpos : ε > 0
r' : ℝ≥0
yr' : ‖y‖₊ < r'
r'r : ↑r' < r
yr'_2 : ‖y‖ < ↑r'
S : Summable fun n ↦ ‖p n‖ * ↑r' ^ n
k : ℕ
hk : ∑' (n : ℕ), ‖p (n + k)‖ * ↑r' ^ (n + k) < ε / 4
A : ∀ᶠ (z : ℕ × E) in atTop ×ˢ 𝓝 y, dist (p.partialSum k z.2) (p.partialSum k y) < ε / 4
B : ∀ᶠ (z : ℕ × E) in atTop ×ˢ 𝓝 y, ‖z.2‖₊ < r'
C : ∀ᶠ (z : ℕ × E) in atTop ×ˢ 𝓝 y, k ≤ z.1
n : ℕ
z : E
h'z : ‖(n, z).2‖₊ < r'
hkn : k ≤ (n, z).1
hz : ‖p.partialSum k z - p.partialSum k y‖ < ε / 4
I : ∀ (w : E), ‖w‖₊ < r' → ‖∑ i ∈ Finset.Ico k n, (p i) fun x ↦ w‖ ≤ ε / 4
⊢ ‖((∑ i ∈ Finset.range k, (p i) fun x ↦ z) + ∑ i ∈ Finset.Ico k n, (p i) fun x ↦ z) -
        ((∑ i ∈ Finset.range k, (p i) fun x ↦ y) + ∑ i ∈ Finset.Ico k n, (p i) fun x ↦ y)‖ =
    ‖(p.partialSum k z - p.partialSum k y + ∑ i ∈ Finset.Ico k n, (p i) fun x ↦ z) +
        -∑ i ∈ Finset.Ico k n, (p i) fun x ↦ y‖

Tactic:
congr 1
    simp only [FormalMultilinearSeries.partialSum]
    abel

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

Goal state before:
pp: 𝕜 : Type u_1
F : Type u_3
G : Type u_4
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜 F
inst✝⁴ : NormedAddCommGroup G
inst✝³ : NormedSpace 𝕜 G
ι : Type u_5
Em : ι → Type u_6
inst✝² : (i : ι) → NormedAddCommGroup (Em i)
inst✝¹ : (i : ι) → NormedSpace 𝕜 (Em i)
inst✝ : Fintype ι
f : G →L[𝕜] ContinuousMultilinearMap 𝕜 Em F
⊢ ∀ (m : ℕ), Fintype.card (Option ι) + 1 ≤ m → f.toFormalMultilinearSeriesOfMultilinear m = 0

Tactic:
intro m hm
    apply dif_neg
    exact Nat.ne_of_lt hm

Goal state after:
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∞
hf : HasFPowerSeriesWithinOnBall f p s x r
r' : ℝ≥0
hr : ↑r' < r
hr'0 : 0 < r'
a : ℝ
ha : a ∈ Ioo 0 1
C : ℝ
hC : 0 < C
hp : ∀ (n : ℕ), ‖p n‖ ≤ C * a ^ n / ↑r' ^ n
L : E × E → ℝ := ⋯
y : E × E
hy' : ‖y - (x, x)‖₊ < r'
ys : y ∈ insert x s ×ˢ insert x s
hy : y ∈ Metric.eball x r ×ˢ Metric.eball x r
A : ℕ → F := ⋯
hA : HasSum (fun n ↦ A (n + 2)) (f y.1 - f y.2 - (p 1) fun x ↦ y.1 - y.2)
B : ℕ → ℝ := ⋯
hAB : ∀ (n : ℕ), ‖A (n + 2)‖ ≤ B n
⊢ HasSum (fun i ↦ (↑i + 2) * a ^ i) (a / (1 - a) ^ 2 + 2 / (1 - a))

Tactic:
simp only [add_mul]

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∞
hf : HasFPowerSeriesWithinOnBall f p s x r
r' : ℝ≥0
hr : ↑r' < r
hr'0 : 0 < r'
a : ℝ
ha : a ∈ Ioo 0 1
C : ℝ
hC : 0 < C
hp : ∀ (n : ℕ), ‖p n‖ ≤ C * a ^ n / ↑r' ^ n
L : E × E → ℝ := fun y ↦ C * (a / ↑r') ^ 2 * (‖y - (x, x)‖ * ‖y.1 - y.2‖) * (a / (1 - a) ^ 2 + 2 / (1 - a))
y : E × E
hy' : ‖y - (x, x)‖₊ < r'
ys : y ∈ insert x s ×ˢ insert x s
hy : y ∈ Metric.eball x r ×ˢ Metric.eball x r
A : ℕ → F := fun n ↦ ((p n) fun x_1 ↦ y.1 - x) - (p n) fun x_1 ↦ y.2 - x
hA : HasSum (fun n ↦ A (n + 2)) (f y.1 - f y.2 - (p 1) fun x ↦ y.1 - y.2)
B : ℕ → ℝ := fun n ↦ C * (a / ↑r') ^ 2 * (‖y - (x, x)‖ * ‖y.1 - y.2‖) * ((↑n + 2) * a ^ n)
hAB : ∀ (n : ℕ), ‖A (n + 2)‖ ≤ B n
⊢ HasSum (fun i ↦ ↑i * a ^ i + 2 * a ^ i) (a / (1 - a) ^ 2 + 2 / (1 - a))
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
p : FormalMultilinearSeries 𝕜 E F
i : E ≃L[𝕜] F
x : E
n : ℕ
v : Fin (n + 2) → F
⊢ ∑ c ∈ {c | 1 < c.length}.toFinset,
      (p c.length) (applyComposition (fun k ↦ if k < n + 2 then p.rightInv i x k else 0) c v) =
    ∑ c ∈ {c | 1 < c.length}.toFinset, (p c.length) ((p.rightInv i x).applyComposition c v)

Tactic:
have N : 0 < n + 2 := by simp

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
p : FormalMultilinearSeries 𝕜 E F
i : E ≃L[𝕜] F
x : E
n : ℕ
v : Fin (n + 2) → F
N : 0 < n + 2
⊢ ∑ c ∈ {c | 1 < c.length}.toFinset,
      (p c.length) (applyComposition (fun k ↦ if k < n + 2 then p.rightInv i x k else 0) c v) =
    ∑ c ∈ {c | 1 < c.length}.toFinset, (p c.length) ((p.rightInv i x).applyComposition c v)
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
p : FormalMultilinearSeries 𝕜 E F
i : E ≃L[𝕜] F
x : E
h : p 1 = (continuousMultilinearCurryFin1 𝕜 E F).symm ↑i
n✝ n : ℕ
v : Fin (n + 2) → F
⊢ (p.comp (p.rightInv i x) (n + 2)) v = (id 𝕜 F ((p 0) 0) (n + 2)) v

Tactic:
have N : 0 < n + 2 := by simp

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
p : FormalMultilinearSeries 𝕜 E F
i : E ≃L[𝕜] F
x : E
h : p 1 = (continuousMultilinearCurryFin1 𝕜 E F).symm ↑i
n✝ n : ℕ
v : Fin (n + 2) → F
N : 0 < n + 2
⊢ (p.comp (p.rightInv i x) (n + 2)) v = (id 𝕜 F ((p 0) 0) (n + 2)) v
Module: Mathlib.Analysis.Analytic.Inverse

Goal state before:
pp: case e_f
𝕜 : 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
p : FormalMultilinearSeries 𝕜 E F
i : E ≃L[𝕜] F
x : E
n✝ n : ℕ
hn : 2 ≤ n + 2
v : Fin (n + 2) → F
⊢ (p.comp (fun k ↦ if k < n + 2 then p.rightInv i x k else 0) (n + 2)) v =
    (∑ c ∈ {c | 1 < c.length}.toFinset, p.compAlongComposition (p.rightInv i x) c) v

Tactic:
have N : 0 < n + 2 := by simp

Goal state after:
case e_f
𝕜 : 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
p : FormalMultilinearSeries 𝕜 E F
i : E ≃L[𝕜] F
x : E
n✝ n : ℕ
hn : 2 ≤ n + 2
v : Fin (n + 2) → F
N : 0 < n + 2
⊢ (p.comp (fun k ↦ if k < n + 2 then p.rightInv i x k else 0) (n + 2)) v =
    (∑ c ∈ {c | 1 < c.length}.toFinset, p.compAlongComposition (p.rightInv i x) c) v