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

Goal state before:
pp: σ : Type u_1
R : Type u_3
inst✝² : CommRing R
τ : Type u_4
S : Type u_5
inst✝¹ : CommRing S
inst✝ : Algebra R S
a : σ → MvPowerSeries τ S
ha : HasSubst a
this✝ : UniformSpace R := ⊥
this : UniformSpace S := ⊥
⊢ ⇑(substAlgHom ha) = subst a

Tactic:
substAlgHom_eq_aeval,

Goal state after:
σ : Type u_1
R : Type u_3
inst✝² : CommRing R
τ : Type u_4
S : Type u_5
inst✝¹ : CommRing S
inst✝ : Algebra R S
a : σ → MvPowerSeries τ S
ha : HasSubst a
this✝ : UniformSpace R := ⊥
this : UniformSpace S := ⊥
⊢ ⇑(aeval ⋯) = subst a
Module: Mathlib.Analysis.Real.Cardinality

Goal state before:
pp: case a
⊢ #ℝ ≤ 𝔠

Tactic:
rw [Real.equivCauchy.cardinal_eq]
    apply mk_quotient_le.trans
    apply (mk_subtype_le _).trans_eq
    rw [← power_def, mk_nat, mkRat, aleph0_power_aleph0]

Goal state after:
Module: Mathlib.NumberTheory.LSeries.Basic

Goal state before:
pp: s : ℂ
hs : s ≠ 0
f : ℕ → ℂ
n : ℕ
⊢ term f s n = f n / ↑n ^ s

Tactic:
rcases eq_or_ne n 0 with rfl | hn

Goal state after:
case inl
s : ℂ
hs : s ≠ 0
f : ℕ → ℂ
⊢ term f s 0 = f 0 / ↑0 ^ s

case inr
s : ℂ
hs : s ≠ 0
f : ℕ → ℂ
n : ℕ
hn : n ≠ 0
⊢ term f s n = f n / ↑n ^ s
Module: Mathlib.NumberTheory.LSeries.Basic

Goal state before:
pp: f : ℕ → ℂ
s : ℂ
n : ℕ
⊢ ‖term f s n‖ = if n = 0 then 0 else ‖f n‖ / ↑n ^ s.re

Tactic:
rcases eq_or_ne n 0 with rfl | hn

Goal state after:
case inl
f : ℕ → ℂ
s : ℂ
⊢ ‖term f s 0‖ = if 0 = 0 then 0 else ‖f 0‖ / ↑0 ^ s.re

case inr
f : ℕ → ℂ
s : ℂ
n : ℕ
hn : n ≠ 0
⊢ ‖term f s n‖ = if n = 0 then 0 else ‖f n‖ / ↑n ^ s.re
Module: Mathlib.RingTheory.MvPowerSeries.Substitution

Goal state before:
pp: σ : Type u_1
R : Type u_3
inst✝² : CommRing R
τ : Type u_4
S : Type u_5
inst✝¹ : CommRing S
inst✝ : Algebra R S
a : σ → MvPowerSeries τ S
w : τ → ℕ
ha : HasSubst a
ha0 : ∀ (i : σ), a i ≠ 0
f : MvPowerSeries σ R
⊢ weightedOrder (ENat.toNat ∘ weightedOrder w ∘ a) f ≤
    ⨅ d, ⨅ (_ : (coeff d) f ≠ 0), (Finsupp.weight (weightedOrder w ∘ a)) d

Tactic:
simp only [ne_eq, le_iInf_iff]

Goal state after:
σ : Type u_1
R : Type u_3
inst✝² : CommRing R
τ : Type u_4
S : Type u_5
inst✝¹ : CommRing S
inst✝ : Algebra R S
a : σ → MvPowerSeries τ S
w : τ → ℕ
ha : HasSubst a
ha0 : ∀ (i : σ), a i ≠ 0
f : MvPowerSeries σ R
⊢ ∀ (i : σ →₀ ℕ),
    ¬(coeff i) f = 0 → weightedOrder (ENat.toNat ∘ weightedOrder w ∘ a) f ≤ (Finsupp.weight (weightedOrder w ∘ a)) i
Module: Mathlib.RingTheory.MvPowerSeries.Substitution

Goal state before:
pp: σ : Type u_1
R : Type u_3
inst✝² : CommRing R
τ : Type u_4
S : Type u_5
inst✝¹ : CommRing S
inst✝ : Algebra R S
a : σ → MvPowerSeries τ S
ha : HasSubst a
f : MvPowerSeries σ R
⊢ (⨅ i, (a i).order) * f.order ≤ ⨅ d, ⨅ (_ : (coeff d) f ≠ 0), (Finsupp.weight ((weightedOrder fun x ↦ 1) ∘ a)) d

Tactic:
simp only [ne_eq, le_iInf_iff]

Goal state after:
σ : Type u_1
R : Type u_3
inst✝² : CommRing R
τ : Type u_4
S : Type u_5
inst✝¹ : CommRing S
inst✝ : Algebra R S
a : σ → MvPowerSeries τ S
ha : HasSubst a
f : MvPowerSeries σ R
⊢ ∀ (i : σ →₀ ℕ), ¬(coeff i) f = 0 → (⨅ i, (a i).order) * f.order ≤ (Finsupp.weight ((weightedOrder fun x ↦ 1) ∘ a)) i
Module: Mathlib.NumberTheory.LSeries.Basic

Goal state before:
pp: s : ℂ
n : ℕ
⊢ term δ s n = if n = 1 then 1 else 0

Tactic:
rcases eq_or_ne n 0 with rfl | hn

Goal state after:
case inl
s : ℂ
⊢ term δ s 0 = if 0 = 1 then 1 else 0

case inr
s : ℂ
n : ℕ
hn : n ≠ 0
⊢ term δ s n = if n = 1 then 1 else 0
Module: Mathlib.RingTheory.PowerSeries.Substitution

Goal state before:
pp: R : Type u_2
inst✝ : CommRing R
τ : Type u_3
f g : MvPowerSeries τ R
hf : HasSubst f
⊢ HasSubst (g * f)

Tactic:
by
  simp only [HasSubst, map_mul]
  exact (Commute.all _ _).isNilpotent_mul_left hf

Goal state after:
Module: Mathlib.RingTheory.PowerSeries.Substitution

Goal state before:
pp: A : Type u_1
inst✝ : CommRing A
f : A⟦X⟧
hf : HasSubst f
n k : ℕ
hk : MvPowerSeries.constantCoeff f ^ k = 0
⊢ ∀ᶠ (m : ℕ) in Filter.atTop, ∀ n' ≤ n, (coeff n') (f ^ m) = 0

Tactic:
refine Filter.eventually_of_mem (Filter.Ici_mem_atTop (k * (n + 1))) fun m hm n' hn' ↦
    coeff_of_lt_order _ ?_

Goal state after:
A : Type u_1
inst✝ : CommRing A
f : A⟦X⟧
hf : HasSubst f
n k : ℕ
hk : MvPowerSeries.constantCoeff f ^ k = 0
m : ℕ
hm : m ∈ Set.Ici (k * (n + 1))
n' : ℕ
hn' : n' ≤ n
⊢ ↑n' < (f ^ m).order
Module: Mathlib.Analysis.Convex.EGauge

Goal state before:
pp: 𝕜 : Type u_1
inst✝³ : NormedDivisionRing 𝕜
E : Type u_2
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
s : Set E
x : E
inst✝ : (𝓝[≠] 0).NeBot
r : ℝ≥0∞
hs₀ : 0 ∈ s
h : ∀ (c : 𝕜), c ≠ 0 → x ∈ c • s → r ≤ ‖c‖ₑ
⊢ ∀ (c : 𝕜), x ∈ c • s → r ≤ ‖c‖ₑ

Tactic:
intro c hc

Goal state after:
𝕜 : Type u_1
inst✝³ : NormedDivisionRing 𝕜
E : Type u_2
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
s : Set E
x : E
inst✝ : (𝓝[≠] 0).NeBot
r : ℝ≥0∞
hs₀ : 0 ∈ s
h : ∀ (c : 𝕜), c ≠ 0 → x ∈ c • s → r ≤ ‖c‖ₑ
c : 𝕜
hc : x ∈ c • s
⊢ r ≤ ‖c‖ₑ
Module: Mathlib.Analysis.Convex.EGauge

Goal state before:
pp: 𝕜 : Type u_1
inst✝³ : NormedDivisionRing 𝕜
E : Type u_2
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
s : Set E
x : E
inst✝ : (𝓝[≠] 0).NeBot
r : ℝ≥0∞
hs₀ : 0 ∈ s
h : ∀ (c : 𝕜), c ≠ 0 → x ∈ c • s → r ≤ ‖c‖ₑ
hc : x ∈ 0 • s
⊢ x = 0

Tactic:
grw [zero_smul_set_subset, Set.mem_zero] at hc
    exact hc

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

Goal state before:
pp: case refine_2
R : Type u
E : Type v
inst✝² : AddCommGroup E
inst✝¹ : SMul R E
inst✝ : TopologicalSpace E
s : Set E
x y : E
h : (comap (fun p ↦ p.1 • p.2) (𝓝 y) ⊓ ⊤ ×ˢ 𝓝[(fun x_1 ↦ x + x_1) ⁻¹' s] 0).NeBot
⊢ ∀ᶠ (x_1 : R × E) in comap Prod.snd (𝓝[(fun x_1 ↦ x + x_1) ⁻¹' s] 0), x + x_1.2 ∈ s

Tactic:
eventually_comap

Goal state after:
case refine_2
R : Type u
E : Type v
inst✝² : AddCommGroup E
inst✝¹ : SMul R E
inst✝ : TopologicalSpace E
s : Set E
x y : E
h : (comap (fun p ↦ p.1 • p.2) (𝓝 y) ⊓ ⊤ ×ˢ 𝓝[(fun x_1 ↦ x + x_1) ⁻¹' s] 0).NeBot
⊢ ∀ᶠ (b : E) in 𝓝[(fun x_1 ↦ x + x_1) ⁻¹' s] 0, ∀ (a : R × E), a.2 = b → x + a.2 ∈ s
Module: Mathlib.RingTheory.PowerSeries.Substitution

Goal state before:
pp: R : Type u_2
inst✝¹ : CommRing R
P : R⟦X⟧
hP : constantCoeff P = 0
inst✝ : Invertible ((coeff 1) P)
n : ℕ
this : (coeff n) (subst (∑ i, C (P.substInvFun ↑i) * X ^ ↑i) P) = (coeff n) X
m : ℕ
B : R⟦X⟧
hB : ∑ i, C (P.substInvFun ↑i) * X ^ ↑i = B
⊢ X ^ (n + 1) ∣ mk P.substInvFun - B

Tactic:
rw [X_pow_dvd_iff]

Goal state after:
R : Type u_2
inst✝¹ : CommRing R
P : R⟦X⟧
hP : constantCoeff P = 0
inst✝ : Invertible ((coeff 1) P)
n : ℕ
this : (coeff n) (subst (∑ i, C (P.substInvFun ↑i) * X ^ ↑i) P) = (coeff n) X
m : ℕ
B : R⟦X⟧
hB : ∑ i, C (P.substInvFun ↑i) * X ^ ↑i = B
⊢ ∀ m < n + 1, (coeff m) (mk P.substInvFun - B) = 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
hb' : b ≠ (single 0 (e 0), single 1 (e 1))
hmul_ne_zero : ¬(MvPowerSeries.coeff b.1) (subst X₀ f) * (MvPowerSeries.coeff b.2) (subst X₁ f) = 0
h0 : b.1 = single 0 (b.1 0) ∧ ¬(coeff (b.1 0)) f = 0
h1 : b.2 = single 1 (b.2 1) ∧ ¬(coeff (b.2 1)) f = 0
⊢ b = (single 0 (e 0), single 1 (e 1))

Tactic:
Prod.ext_iff,

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))
hmul_ne_zero : ¬(MvPowerSeries.coeff b.1) (subst X₀ f) * (MvPowerSeries.coeff b.2) (subst X₁ f) = 0
h0 : b.1 = single 0 (b.1 0) ∧ ¬(coeff (b.1 0)) f = 0
h1 : b.2 = single 1 (b.2 1) ∧ ¬(coeff (b.2 1)) f = 0
⊢ b.1 = (single 0 (e 0), single 1 (e 1)).1 ∧ b.2 = (single 0 (e 0), single 1 (e 1)).2
Module: Mathlib.Analysis.Calculus.TangentCone.Basic

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁴ : AddCommGroup E
inst✝³ : Semiring 𝕜
inst✝² : Module 𝕜 E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousAdd E
s t : Set E
x : E
h : UniqueDiffWithinAt 𝕜 s x
st : 𝓝[s] x ≤ 𝓝[t] x
⊢ UniqueDiffWithinAt 𝕜 t x

Tactic:
simp only [uniqueDiffWithinAt_iff] at *

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : AddCommGroup E
inst✝³ : Semiring 𝕜
inst✝² : Module 𝕜 E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousAdd E
s t : Set E
x : E
st : 𝓝[s] x ≤ 𝓝[t] x
h : Dense ↑(Submodule.span 𝕜 (tangentConeAt 𝕜 s x)) ∧ x ∈ closure[inst✝¹] s
⊢ Dense ↑(Submodule.span 𝕜 (tangentConeAt 𝕜 t x)) ∧ x ∈ closure[inst✝¹] t
Module: Mathlib.Analysis.Calculus.TangentCone.Basic

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁶ : DivisionSemiring 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : TopologicalSpace 𝕜
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousSMul 𝕜 E
s : Set E
x y : E
α : Type u_3
l : Filter α
inst✝ : l.NeBot
c : α → 𝕜
hc₀ : Tendsto c l (𝓝[≠] 0)
hmem : ∀ᶠ (n : α) in l, x + c n • y ∈ s
⊢ y ∈ tangentConeAt 𝕜 s x

Tactic:
by
  rw [tendsto_nhdsWithin_iff] at hc₀
  refine mem_tangentConeAt_of_seq l c⁻¹ (c · • y) ?_ hmem ?_
  · simpa using hc₀.1.smul (tendsto_const_nhds (x := y))
  · refine tendsto_nhds_of_eventually_eq <| hc₀.2.mono fun n hn ↦ ?_
    simp_all

Goal state after:
Module: Mathlib.Analysis.Asymptotics.TVS

Goal state before:
pp: α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : AddCommGroup E
inst✝⁵ : TopologicalSpace E
inst✝⁴ : Module 𝕜 E
inst✝³ : AddCommGroup F
inst✝² : TopologicalSpace F
inst✝¹ : Module 𝕜 F
f : α → E
g : α → F
inst✝ : TopologicalSpace α
x : α
s : Set α
h : f x = 0
⊢ f =o[𝕜; 𝓝[insert x s] x] g ↔ f =o[𝕜; 𝓝[s] x] g

Tactic:
by
  rw [nhdsWithin_insert, isLittleOTVS_sup, and_iff_right]
  exact .congr' (.zero g _) h.symm .rfl

Goal state after:
Module: Mathlib.Analysis.Asymptotics.TVS

Goal state before:
pp: α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : AddCommGroup E
inst✝⁵ : TopologicalSpace E
inst✝⁴ : Module 𝕜 E
inst✝³ : AddCommGroup F
inst✝² : TopologicalSpace F
inst✝¹ : Module 𝕜 F
l : Filter α
f : α → E
g : α → F
inst✝ : ContinuousNeg F
h : f =O[𝕜; l] g
⊢ g =O[𝕜; l] (-g)

Tactic:
by simpa using (IsBigOTVS.refl (-g) l).neg_left

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

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

Tactic:
induction k generalizing p with
  | zero => rfl
  | succ k ih => simp [ih, add_assoc]

Goal state after:
Module: Mathlib.Analysis.Asymptotics.TVS

Goal state before:
pp: case h₂
α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : SeminormedAddCommGroup E
inst✝² : SeminormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace 𝕜 F
f : α → E
g : α → F
l : Filter α
c : 𝕜
hc : 1 < ‖c‖₊
hc₀ : 0 < ‖c‖₊
h : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖
δ : ℝ≥0
hδ : δ ≠ 0
x : α
ε : ℝ≥0
hε : 0 < ↑ε
hx : ↑‖f x‖₊ ≤ ↑ε * ↑δ / ↑‖c‖₊ * ↑‖g x‖₊
⊢ ↑‖g x‖₊ ≤ egauge 𝕜 (ball 0 1) (g x)

Tactic:
apply le_egauge_ball_one

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
p : FormalMultilinearSeries 𝕜 E F
x y : E
r : ℝ≥0
⊢ Function.RightInverse (fun s ↦ ⟨s.fst - s.snd.card, ⟨s.snd.card, ⟨Finset.map (finCongr ⋯).toEmbedding s.snd, ⋯⟩⟩⟩)
    fun s ↦ ⟨s.fst + s.snd.fst, ↑s.snd.snd⟩

Tactic:
rintro ⟨n, s⟩

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
x y : E
r : ℝ≥0
n : ℕ
s : Finset (Fin n)
⊢ (fun s ↦ ⟨s.fst + s.snd.fst, ↑s.snd.snd⟩)
      ((fun s ↦ ⟨s.fst - s.snd.card, ⟨s.snd.card, ⟨Finset.map (finCongr ⋯).toEmbedding s.snd, ⋯⟩⟩⟩) ⟨n, s⟩) =
    ⟨n, s⟩
Module: Mathlib.Analysis.Analytic.ConvergenceRadius

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_3
F : Type u_4
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
h : 0 < p.radius
r : ℝ≥0
r0 : 0 < ↑r
rlt : ↑r < p.radius
rpos : 0 < ↑r
C : ℝ
Cpos : C > 0
hCp : ∀ (n : ℕ), ‖p n‖ ≤ C / ↑r ^ n
⊢ 0 < (↑r)⁻¹

Tactic:
simp only [inv_pos, rpos]

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

Goal state before:
pp: case refine_2
𝕜 : 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
hsf : Summable f
k : ℕ
this : HasSum (fun n ↦ (p.changeOriginSeries k n) fun x_1 ↦ x) (p.changeOrigin x k)
⊢ Summable fun c ↦ (p.changeOriginSeriesTerm k c.fst ↑c.snd ⋯) fun x_1 ↦ x

Tactic:
· refine .of_nnnorm_bounded
          (p.changeOriginSeries_summable_aux₂ (mem_eball_zero_iff.1 x_mem_ball) k)
            fun s => ?_
        refine (ContinuousMultilinearMap.le_opNNNorm _ _).trans_eq ?_
        simp

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

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
s : Set E
g : F →L[𝕜] G
h : CPolynomialOn 𝕜 f s
⊢ CPolynomialOn 𝕜 (⇑g ∘ f) s

Tactic:
rintro x hx
  rcases h x hx with ⟨p, n, r, hp⟩
  exact ⟨g.compFormalMultilinearSeries p, n, r, g.comp_hasFiniteFPowerSeriesOnBall hp⟩

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
x : E
r : ℝ≥0∞
n : ℕ
hf : HasFiniteFPowerSeriesOnBall f p x n r
y : E
hy : edist y x < r
m : ℕ
hm : n ≤ m
⊢ f y = p.partialSum m (y - x)

Tactic:
edist_eq_enorm_sub,

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
x : E
r : ℝ≥0∞
n : ℕ
hf : HasFiniteFPowerSeriesOnBall f p x n r
y : E
hy : ‖y - x‖ₑ < r
m : ℕ
hm : n ≤ m
⊢ f y = p.partialSum m (y - x)
Module: Mathlib.Analysis.Analytic.CPolynomialDef

Goal state before:
pp: case refine_2
𝕜 : 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
x : E
r : ℝ≥0∞
hf : ∀ y ∈ Metric.eball x r, f y = 0
r_pos : 0 < r
hp : ∀ (n : ℕ), p n = 0
y : E
hy : y ∈ Metric.eball 0 r
⊢ edist (x + y) x < r

Tactic:
edist_eq_enorm_sub,

Goal state after:
case refine_2
𝕜 : 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
x : E
r : ℝ≥0∞
hf : ∀ y ∈ Metric.eball x r, f y = 0
r_pos : 0 < r
hp : ∀ (n : ℕ), p n = 0
y : E
hy : y ∈ Metric.eball 0 r
⊢ ‖x + y - x‖ₑ < r
Module: Mathlib.Analysis.Analytic.OfScalars

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : Ring E
inst✝² : Algebra 𝕜 E
inst✝¹ : TopologicalSpace E
inst✝ : IsTopologicalRing E
c : ℕ → 𝕜
f : E →L[𝕜] E
⊢ (ofScalars E c).compContinuousLinearMap (-f) = (ofScalars E fun k ↦ (-1) ^ k * c k).compContinuousLinearMap f

Tactic:
by
  conv => lhs; rw [← ContinuousLinearMap.id_comp f, ← ContinuousLinearMap.neg_comp]
  rw [← FormalMultilinearSeries.compContinuousLinearMap_comp, ofScalars_comp_neg_id]

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
k : ℕ
⊢ (p.changeOriginSeries k).sum = (p.changeOriginSeries k).partialSum (n - k)

Tactic:
ext x

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
k : ℕ
x : E
x✝ : Fin k → E
⊢ ((p.changeOriginSeries k).sum x) x✝ = ((p.changeOriginSeries k).partialSum (n - k) x) x✝
Module: Mathlib.Analysis.Analytic.Basic

Goal state before:
pp: case inl
𝕜 : 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 g : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
h : HasFPowerSeriesWithinOnBall f p s x r
h' : EqOn g f (s ∩ Metric.eball x r)
h'' : g x = f x
h'y : 0 ∈ Metric.eball 0 r
⊢ g (x + 0) = f (x + 0)

Tactic:
simpa using h''

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

Goal state before:
pp: case neg.refine_1
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedRing E
inst✝ : NormedAlgebra 𝕜 E
c : ℕ → 𝕜
hc : ∀ᶠ (n : ℕ) in atTop, c n ≠ 0
hc' : Tendsto (fun n ↦ ‖c n.succ‖ / ‖c n‖) atTop (𝓝 0)
r' : ℝ≥0
hrz : ¬r' = 0
⊢ Summable fun n ↦ ‖‖c n‖ * ↑r' ^ n‖

pp: case neg.refine_2
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedRing E
inst✝ : NormedAlgebra 𝕜 E
c : ℕ → 𝕜
hc : ∀ᶠ (n : ℕ) in atTop, c n ≠ 0
hc' : Tendsto (fun n ↦ ‖c n.succ‖ / ‖c n‖) atTop (𝓝 0)
r' : ℝ≥0
hrz : ¬r' = 0
⊢ ∀ᶠ (i : ℕ) in cofinite, ‖‖ofScalars E c i‖ * ↑r' ^ i‖ ≤ ‖‖c i‖ * ↑r' ^ i‖

Tactic:
· apply summable_of_ratio_test_tendsto_lt_one zero_lt_one (hc.mp (Eventually.of_forall ?_))
      · simp only [norm_norm]
        exact mul_zero (_ : ℝ) ▸ tendsto_succ_norm_div_norm _ hrz (NNReal.coe_zero ▸ hc')
      · simp_all

Goal state after:
case neg.refine_2
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedRing E
inst✝ : NormedAlgebra 𝕜 E
c : ℕ → 𝕜
hc : ∀ᶠ (n : ℕ) in atTop, c n ≠ 0
hc' : Tendsto (fun n ↦ ‖c n.succ‖ / ‖c n‖) atTop (𝓝 0)
r' : ℝ≥0
hrz : ¬r' = 0
⊢ ∀ᶠ (i : ℕ) in cofinite, ‖‖ofScalars E c i‖ * ↑r' ^ i‖ ≤ ‖‖c i‖ * ↑r' ^ i‖
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 → ℝ := 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 ∈ Metric.eball (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
⊢ HasSum (fun n ↦ A (n + 2)) (f y.1 - f y.2 - (p 1) fun x ↦ y.1 - y.2)

Tactic:
convert
        (hasSum_nat_add_iff' 2).2
          ((hf.hasSum_sub ⟨ys.1, hy.1⟩).sub (hf.hasSum_sub ⟨ys.2, hy.2⟩))

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 ∈ Metric.eball (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
⊢ ((p 1) fun x ↦ y.1 - y.2) = ∑ i ∈ Finset.range 2, (((p i) fun x_1 ↦ y.1 - x) - (p i) fun x_1 ↦ y.2 - x)
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 → ℝ := fun y ↦ C * (a / ↑r') ^ 2 * (‖y - (x, x)‖ * ‖y.1 - y.2‖) * (a / (1 - a) ^ 2 + 2 / (1 - a))
y : E × E
hy' : edist 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)
⊢ ‖f y.1 - f y.2 - (p 1) fun x ↦ y.1 - y.2‖ ≤ L y

Tactic:
edist_eq_enorm_sub,

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)
⊢ ‖f y.1 - f y.2 - (p 1) fun x ↦ y.1 - y.2‖ ≤ L y
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
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
hq : 0 < q.radius
hp : 0 < p.radius
rq rp : ℝ≥0
hrp : rp < 1 ∧ ↑rp < p.radius
hrq : rq < 1 ∧ ↑rq < q.radius
rp_pos : 0 < rp
rq_pos : 0 < rq
Cq : ℝ≥0
_hCq0 : Cq > 0
hCq : ∀ (n : ℕ), ‖q n‖₊ * rq ^ n ≤ Cq
Cp : ℝ≥0
hCp1 : Cp ≥ 1
hCp : ∀ (n : ℕ), ‖p n‖₊ * rp ^ n ≤ Cp
r0 : ℝ≥0 := (4 * Cp)⁻¹
r0_pos : 0 < r0
r : ℝ≥0 := rp * rq * r0
r_pos : 0 < r
n : ℕ
c : Composition n
A : ‖q c.length‖₊ * rq ^ n ≤ Cq
⊢ (∏ i, ‖p (c.blocksFun i)‖₊) * rp ^ n = ∏ i, ‖p (c.blocksFun i)‖₊ * rp ^ c.blocksFun i

Tactic:
by
        simp only [Finset.prod_mul_distrib, Finset.prod_pow_eq_pow_sum, c.sum_blocksFun]

Goal state after: