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

Goal state before:
pp: case e'_4
σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
f : MvPowerSeries σ R
m : ℕ
hf : constantCoeff f ^ m = 0
d : σ →₀ ℕ
n : ℕ
hn : m + degree d ≤ n
k : ℕ →₀ σ →₀ ℕ
hk : (range n).sum ⇑k = d ∧ k.support ⊆ range n
s : Finset ℕ := {i ∈ range n | k i = 0}
hs_def : s = {i ∈ range n | k i = 0}
hs : s ⊆ range n
hs' : ∀ i ∈ s, (coeff (k i)) f = constantCoeff f
hs'' : ∀ i ∈ s, k i = 0
⊢ degree (∑ x ∈ range n \ s, k x) = ∑ x ∈ range n \ s, degree (k x)

pp: σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
f : MvPowerSeries σ R
m : ℕ
hf : constantCoeff f ^ m = 0
d : σ →₀ ℕ
n : ℕ
hn : m + degree d ≤ n
k : ℕ →₀ σ →₀ ℕ
hk : (range n).sum ⇑k = d ∧ k.support ⊆ range n
s : Finset ℕ := {i ∈ range n | k i = 0}
hs_def : s = {i ∈ range n | k i = 0}
hs : s ⊆ range n
hs' : ∀ i ∈ s, (coeff (k i)) f = constantCoeff f
hs'' : ∀ i ∈ s, k i = 0
⊢ ∀ x ∈ range n \ s, 1 ≤ degree (k x)

Tactic:
· simp only [degree_eq_weight_one, map_sum]

Goal state after:
σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
f : MvPowerSeries σ R
m : ℕ
hf : constantCoeff f ^ m = 0
d : σ →₀ ℕ
n : ℕ
hn : m + degree d ≤ n
k : ℕ →₀ σ →₀ ℕ
hk : (range n).sum ⇑k = d ∧ k.support ⊆ range n
s : Finset ℕ := {i ∈ range n | k i = 0}
hs_def : s = {i ∈ range n | k i = 0}
hs : s ⊆ range n
hs' : ∀ i ∈ s, (coeff (k i)) f = constantCoeff f
hs'' : ∀ i ∈ s, k i = 0
⊢ ∀ x ∈ range n \ s, 1 ≤ degree (k x)
Module: Mathlib.RingTheory.DedekindDomain.AdicValuation

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
p q : HeightOneSpectrum R
hpq : (valuation K p).IsEquiv (valuation K q)
⊢ p = q

Tactic:
by
  simp_all [Valuation.isEquiv_iff_val_lt_one, HeightOneSpectrum.ext_iff, Ideal.ext_iff,
    ← valuation_lt_one_iff_mem (K := K)]

Goal state after:
Module: Mathlib.RingTheory.MvPowerSeries.Order

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
f : MvPowerSeries σ R
n : ℕ
h : ∀ (d : σ →₀ ℕ), (weight w) d < n → (coeff d) f = 0
this : ↑(weightedOrder w f).toNat = weightedOrder w f
d : σ →₀ ℕ
H : ↑((weight w) d) < ↑n
hfd : (coeff d) f ≠ 0
hd : ↑((weight w) d) = weightedOrder w f
⊢ False

Tactic:
Nat.cast_lt

Goal state after:
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
f : MvPowerSeries σ R
n : ℕ
h : ∀ (d : σ →₀ ℕ), (weight w) d < n → (coeff d) f = 0
this : ↑(weightedOrder w f).toNat = weightedOrder w f
d : σ →₀ ℕ
H : (weight w) d < n
hfd : (coeff d) f ≠ 0
hd : ↑((weight w) d) = weightedOrder w f
⊢ False
Module: Mathlib.RingTheory.MvPowerSeries.Order

Goal state before:
pp: case right
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
f g : MvPowerSeries σ R
H : weightedOrder w f < weightedOrder w g
n : ℕ
hn : ↑n = weightedOrder w f
d : σ →₀ ℕ
hd' : (coeff d) f ≠ 0
hd : (weight w) d = n
b : σ →₀ ℕ
hb : (weight w) b < n
⊢ ↑((weight w) b) < ↑n

Tactic:
Nat.cast_lt

Goal state after:
case right
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
f g : MvPowerSeries σ R
H : weightedOrder w f < weightedOrder w g
n : ℕ
hn : ↑n = weightedOrder w f
d : σ →₀ ℕ
hd' : (coeff d) f ≠ 0
hd : (weight w) d = n
b : σ →₀ ℕ
hb : (weight w) b < n
⊢ (weight w) b < n
Module: Mathlib.RingTheory.DedekindDomain.AdicValuation

Goal state before:
pp: case neg
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
a b : R
hv : v.intValuation b ≤ v.intValuation a
γ : Multiplicative ℤ
ha : ¬a = 0
hvaz : v.intValuation a ≠ 0
hγz : ↑γ ≠ 0
n : ℕ
hna : exp (-↑n) < v.intValuation a
hnγ : exp (-↑n) < ↑γ
hvn : emultiplicity v.asIdeal (Ideal.span {a}) ≤ ↑n
hb : b ∈ v.asIdeal ^ multiplicity v.asIdeal (Ideal.span {a})
hnz : Ideal.span {a} ≠ ⊥
⊢ ∃ a_1, v.intValuation (b - a_1 * a) ≤ exp (-↑n)

Tactic:
simpa [← Ideal.irreducible_pow_sup_of_ge hnz v.irreducible n hvn, Submodule.mem_sup,
      ← eq_sub_iff_add_eq, ← intValuation_le_pow_iff_mem, Ideal.mem_span_singleton'] using hb

Goal state after:
Module: Mathlib.RingTheory.MvPowerSeries.Order

Goal state before:
pp: case cons
σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
ι : Type u_4
w : σ → ℕ
f : ι → MvPowerSeries σ R
a : ι
s : Finset ι
ha : a ∉ s
ih : ∑ i ∈ s, weightedOrder w (f i) ≤ weightedOrder w (∏ i ∈ s, f i)
⊢ ∑ i ∈ Finset.cons a s ha, weightedOrder w (f i) ≤ weightedOrder w (∏ i ∈ Finset.cons a s ha, f i)

Tactic:
grw [Finset.sum_cons ha, Finset.prod_cons ha, ih, le_weightedOrder_mul]

Goal state after:
Module: Mathlib.RingTheory.DedekindDomain.AdicValuation

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDedekindDomain R
K : Type u_2
S : Type u_3
inst✝³ : Field K
inst✝² : CommSemiring S
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
x : (ofClass (valuation K v)).ValueGroup₀
⊢ (map' ↑(valueGroupEquiv K v).symm) ((map' ↑(valueGroupEquiv K v)) x) = x

Tactic:
by match x with | 0 => simp | .coe a => simp

Goal state after:
Module: Mathlib.Topology.Instances.ENat

Goal state before:
pp: a b✝ : ℕ∞
h : a ≠ ⊤ ∨ b✝ ≠ ⊤
b : ℕ
x✝ : ⊤ ≠ ⊤ ∨ ↑b ≠ ⊤
this : ∀ (n : ℕ), ∀ᶠ (a : ℕ∞) in 𝓝 ⊤, ↑b + ↑n < a
⊢ ContinuousAt (Function.uncurry fun x1 x2 ↦ x1 - x2) (⊤, ↑b)

Tactic:
simpa [ContinuousAt, nhds_prod_eq, (· ∘ ·), lt_tsub_iff_left, tendsto_nhds_top_iff_natCast_lt]

Goal state after:
Module: Mathlib.RingTheory.DedekindDomain.AdicValuation

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
g : (ofClass (valuation K v)).ValueGroup₀
a : ↥(ofClass (valuation K v)).valueGroup
⊢ embedding ((valueGroupOrderIso K v) ↑a) = embedding ↑a

Tactic:
simp [coe_valueGroupOrderIso_coe, embedding_apply, coe_valueGroupEquiv]

Goal state after:
Module: Mathlib.RingTheory.MvPowerSeries.Order

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
f g : MvPowerSeries σ R
p : ℕ
hf : IsWeightedHomogeneous w f p
hg : IsWeightedHomogeneous w g p
d : σ →₀ ℕ
hd : ¬(weight w) d = p
⊢ (coeff d) f + (coeff d) g = 0

Tactic:
hf.coeff_eq_zero hd,

Goal state after:
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
f g : MvPowerSeries σ R
p : ℕ
hf : IsWeightedHomogeneous w f p
hg : IsWeightedHomogeneous w g p
d : σ →₀ ℕ
hd : ¬(weight w) d = p
⊢ 0 + (coeff d) g = 0
Module: Mathlib.RingTheory.MvPowerSeries.Order

Goal state before:
pp: case pos.inr.inr
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
f g : MvPowerSeries σ R
p q : ℕ
hf : ↑p ≤ weightedOrder w f
hg : ↑q ≤ weightedOrder w g
d : σ →₀ ℕ
x : (σ →₀ ℕ) × (σ →₀ ℕ)
hd : (weight w) x.1 + (weight w) x.2 = p + q
hx : x.1 + x.2 = d
h : ↑((weight w) x.2) < ↑q
⊢ (coeff x.1) f * (coeff x.2) g = 0

Tactic:
rw [coeff_eq_zero_of_lt_weightedOrder w (lt_of_lt_of_le h hg), mul_zero]

Goal state after:
Module: Mathlib.RingTheory.DedekindDomain.AdicValuation

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDedekindDomain R
K : Type u_2
S : Type u_3
inst✝³ : Field K
inst✝² : CommSemiring S
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
x : R
y : ↥(adicCompletionIntegers K v)
z : adicCompletion K v
⊢ (x • y) • z = x • y • z

Tactic:
simp only [Algebra.smul_def]

Goal state after:
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDedekindDomain R
K : Type u_2
S : Type u_3
inst✝³ : Field K
inst✝² : CommSemiring S
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
x : R
y : ↥(adicCompletionIntegers K v)
z : adicCompletion K v
⊢ (algebraMap (↥(adicCompletionIntegers K v)) (adicCompletion K v))
        ((algebraMap R ↥(adicCompletionIntegers K v)) x * y) *
      z =
    (algebraMap R (adicCompletion K v)) x * ((algebraMap (↥(adicCompletionIntegers K v)) (adicCompletion K v)) y * z)
Module: Mathlib.RingTheory.PowerSeries.Order

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
φ : R⟦X⟧
n : ℕ∞
⊢ φ.order = n ↔ (∀ (i : ℕ), ↑i = n → (coeff i) φ ≠ 0) ∧ ∀ (i : ℕ), ↑i < n → (coeff i) φ = 0

Tactic:
cases n with
  | top => simp
  | coe n => simp [order_eq_nat]

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
n : ℕ
f : R⟦X⟧
⊢ f = (X ^ n * mk fun i ↦ (coeff (i + n)) f) + ↑((trunc n) f)

Tactic:
by
  rw [← (commute_X_pow _ n).eq, ← eq_shift_mul_X_pow_add_trunc]

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

Goal state before:
pp: case neg
R : Type u_1
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
φ ψ : R⟦X⟧
h : φ ≠ 0 ∧ ψ ≠ 0
⊢ (φ * ψ).order ≤ φ.order + ψ.order

Tactic:
· rw [← coe_toNat_order h.1, ← coe_toNat_order h.2, ← ENat.natCast_add]
    apply order_le
    rw [coeff_mul, Finset.sum_eq_single_of_mem ⟨φ.order.toNat, ψ.order.toNat⟩ (by simp)]
    · exact mul_ne_zero (coeff_order h.1) (coeff_order h.2)
    · intro ij hij h
      rcases trichotomy_of_add_eq_add (mem_antidiagonal.mp hij) with h' | h' | h'
      · exact False.elim (h (by simp [Prod.ext_iff, h'.1, h'.2]))
      · rw [coeff_of_lt_order_toNat ij.1 h', zero_mul]
      · rw [coeff_of_lt_order_toNat ij.2 h', mul_zero]

Goal state after:
Module: Mathlib.RingTheory.MvPowerSeries.LinearTopology

Goal state before:
pp: case refine_1
σ : Type u_1
R : Type u_2
inst✝³ : Ring R
inst✝² : TopologicalSpace R
inst✝¹ : IsLinearTopology R R
inst✝ : IsLinearTopology Rᵐᵒᵖ R
⊢ ∀ (i : Set (σ →₀ ℕ) × TwoSidedIdeal R),
    i.1.Finite ∧ ↑i.2 ∈ 𝓝 0 → ∃ i', ↑i'.1 ∈ 𝓝 0 ∧ ↑(basis σ R i') ⊆ i.1.pi fun x ↦ ↑i.2

Tactic:
intro ⟨D, I⟩

Goal state after:
case refine_1
σ : Type u_1
R : Type u_2
inst✝³ : Ring R
inst✝² : TopologicalSpace R
inst✝¹ : IsLinearTopology R R
inst✝ : IsLinearTopology Rᵐᵒᵖ R
D : Set (σ →₀ ℕ)
I : TwoSidedIdeal R
⊢ (D, I).1.Finite ∧ ↑(D, I).2 ∈ 𝓝 0 → ∃ i', ↑i'.1 ∈ 𝓝 0 ∧ ↑(basis σ R i') ⊆ (D, I).1.pi fun x ↦ ↑(D, I).2
Module: Mathlib.RingTheory.MvPowerSeries.Evaluation

Goal state before:
pp: case e_p
σ : Type u_1
R : Type u_2
inst✝³ : CommRing R
inst✝² : UniformSpace R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : UniformSpace S
φ : R →+* S
a : σ → S
f : MvPolynomial σ R
this : ∃ p, ↑p = ↑f
⊢ ↑this.choose = ↑f

Tactic:
this.choose_spec

Goal state after:
case e_p
σ : Type u_1
R : Type u_2
inst✝³ : CommRing R
inst✝² : UniformSpace R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : UniformSpace S
φ : R →+* S
a : σ → S
f : MvPolynomial σ R
this : ∃ p, ↑p = ↑f
⊢ ↑f = ↑f
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
inst✝³ : UniformSpace R
inst✝² : DiscreteUniformity R
inst✝¹ : UniformSpace S
inst✝ : DiscreteUniformity S
⊢ Continuous (subst a)

Tactic:
rw [subst_eq_eval₂]
  exact continuous_eval₂ (continuous_algebraMap _ _) ha.hasEval

Goal state after:
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
⊢ constantCoeff (subst a f) = ∑ᶠ (d : σ →₀ ℕ), (coeff d) f • constantCoeff (d.prod fun s e ↦ a s ^ e)

Tactic:
by
  simp only [← coeff_zero_eq_constantCoeff_apply, coeff_subst ha f 0]

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
n' : ℕ
hn' : n' ≤ n
m : ℕ
hm : k * (n + 1) + m ∈ Set.Ici (k * (n + 1))
⊢ ↑n' < ↑(n + 1) + (f ^ m).order

Tactic:
← _root_.le_add_right le_rfl,

Goal state after:
A : Type u_1
inst✝ : CommRing A
f : A⟦X⟧
hf : HasSubst f
n k : ℕ
hk : MvPowerSeries.constantCoeff f ^ k = 0
n' : ℕ
hn' : n' ≤ n
m : ℕ
hm : k * (n + 1) + m ∈ Set.Ici (k * (n + 1))
⊢ ↑n' < ↑(n + 1)
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
n' : ℕ
hn' : n' ≤ n
m : ℕ
hm : k * (n + 1) + m ∈ Set.Ici (k * (n + 1))
⊢ ↑n' < ↑(n + 1)

Tactic:
Nat.cast_lt

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

Goal state before:
pp: case pos
σ : 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
f : MvPowerSeries σ R
inst✝ : Finite τ
k : ℕ
ha : HasSubst a
ha₁ : ∀ (i : σ), constantCoeff (a i) = 0
d : τ →₀ ℕ
hd : Finsupp.degree d < k
h1 : Function.HasFiniteSupport fun d_1 ↦ (coeff d_1) f • (coeff d) (d_1.prod fun s e ↦ a s ^ e)
⊢ ∑ᶠ (d_1 : σ →₀ ℕ), (coeff d_1) f • (coeff d) (d_1.prod fun s e ↦ a s ^ e) =
    ∑ᶠ (d_1 : σ →₀ ℕ), (coeff d_1) (∑ i ∈ range k, (homogeneousComponent i) f) • (coeff d) (d_1.prod fun s e ↦ a s ^ e)

Tactic:
have h2 := coeff_subst_finite ha (∑ i ∈ range k, (homogeneousComponent i) f) d

Goal state after:
case pos
σ : 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
f : MvPowerSeries σ R
inst✝ : Finite τ
k : ℕ
ha : HasSubst a
ha₁ : ∀ (i : σ), constantCoeff (a i) = 0
d : τ →₀ ℕ
hd : Finsupp.degree d < k
h1 : Function.HasFiniteSupport fun d_1 ↦ (coeff d_1) f • (coeff d) (d_1.prod fun s e ↦ a s ^ e)
h2 :
  Function.HasFiniteSupport fun d_1 ↦
    (coeff d_1) (∑ i ∈ range k, (homogeneousComponent i) f) • (coeff d) (d_1.prod fun s e ↦ a s ^ e)
⊢ ∑ᶠ (d_1 : σ →₀ ℕ), (coeff d_1) f • (coeff d) (d_1.prod fun s e ↦ a s ^ e) =
    ∑ᶠ (d_1 : σ →₀ ℕ), (coeff d_1) (∑ i ∈ range k, (homogeneousComponent i) f) • (coeff d) (d_1.prod fun s e ↦ a s ^ e)
Module: Mathlib.Analysis.Calculus.TangentCone.Real

Goal state before:
pp: a b : ℝ
hab : a < b
⊢ (interior (Ioc a b)).Nonempty

Tactic:
simp only [interior_Ioc, nonempty_Ioo, hab]

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

Goal state before:
pp: 𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f f₁ : 𝕜 → F
x : 𝕜
h : ∀ᶠ (y : 𝕜) in 𝓝[≠] x, ∀ᶠ (x : 𝕜) in 𝓝 y, f₁ x = f x
⊢ ∀ᶠ (y : 𝕜) in 𝓝[≠] x, ∀ᶠ (x : 𝕜) in 𝓝 y, deriv f₁ x = deriv f x

Tactic:
filter_upwards [h] with y hy

Goal state after:
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f f₁ : 𝕜 → F
x : 𝕜
h : ∀ᶠ (y : 𝕜) in 𝓝[≠] x, ∀ᶠ (x : 𝕜) in 𝓝 y, f₁ x = f x
y : 𝕜
hy : ∀ᶠ (x : 𝕜) in 𝓝 y, f₁ x = f x
⊢ ∀ᶠ (x : 𝕜) in 𝓝 y, deriv f₁ x = deriv f x
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
r r' : ℝ≥0
hr : ↑r + ↑r' < p.radius
⊢ Summable fun s ↦ ‖p (s.fst + s.snd.fst)‖₊ * r ^ s.snd.fst * r' ^ s.fst

Tactic:
by
  rw [← changeOriginIndexEquiv.symm.summable_iff]
  dsimp only [Function.comp_def, changeOriginIndexEquiv_symm_apply_fst,
    changeOriginIndexEquiv_symm_apply_snd_fst]
  have : ∀ n : ℕ,
      HasSum (fun s : Finset (Fin n) => ‖p (n - s.card + s.card)‖₊ * r ^ s.card * r' ^ (n - s.card))
        (‖p n‖₊ * (r + r') ^ n) := by
    intro n
    -- TODO: why `simp only [tsub_add_cancel_of_le (card_finset_fin_le _)]` fails?
    convert_to HasSum (fun s : Finset (Fin n) => ‖p n‖₊ * (r ^ s.card * r' ^ (n - s.card))) _
    · ext1 s
      rw [tsub_add_cancel_of_le (card_finset_fin_le _), mul_assoc]
    rw [← Fin.sum_pow_mul_eq_add_pow]
    exact (hasSum_fintype _).mul_left _
  refine NNReal.summable_sigma.2 ⟨fun n => (this n).summable, ?_⟩
  simp only [(this _).tsum_eq]
  exact p.summable_nnnorm_mul_pow hr

Goal state after:
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 q : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0
hr : ↑r < p.radius ∧ ↑r < q.radius
this : (fun x ↦ ‖p x‖ * ↑r ^ x + ‖q x‖ * ↑r ^ x) =O[atTop] fun x ↦ 1
n : ℕ
⊢ ‖‖(p + q) n‖ * ↑r ^ n‖ ≤ ‖‖p n‖ * ↑r ^ n + ‖q n‖ * ↑r ^ n‖

Tactic:
rw [← add_mul, norm_mul, norm_mul, norm_norm]

Goal state after:
𝕜 : 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 q : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0
hr : ↑r < p.radius ∧ ↑r < q.radius
this : (fun x ↦ ‖p x‖ * ↑r ^ x + ‖q x‖ * ↑r ^ x) =O[atTop] fun x ↦ 1
n : ℕ
⊢ ‖(p + q) n‖ * ‖↑r ^ n‖ ≤ ‖‖p n‖ + ‖q n‖‖ * ‖↑r ^ n‖
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
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 : ℕ
⊢ HasSum (fun c ↦ f ⟨k, c⟩) ((p.changeOrigin x k) fun x ↦ y)

Tactic:
dsimp +instances only [f]

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
hsf : Summable f
k : ℕ
⊢ HasSum (fun c ↦ ((p.changeOriginSeriesTerm k c.fst ↑c.snd ⋯) fun x_1 ↦ x) fun x ↦ y) ((p.changeOrigin x k) fun x ↦ y)
Module: Mathlib.Analysis.Normed.Module.Multilinear.Curry

Goal state before:
pp: 𝕜 : Type u
n : ℕ
Ei : Fin n.succ → Type wEi
G : Type wG
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : (i : Fin n.succ) → NormedAddCommGroup (Ei i)
inst✝² : (i : Fin n.succ) → NormedSpace 𝕜 (Ei i)
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : ContinuousMultilinearMap 𝕜 Ei G
m : (i : Fin n) → Ei i.castSucc
x : Ei (last n)
⊢ ‖f (snoc m x)‖ ≤ (‖f‖ * ∏ i, ‖m i‖) * ‖x‖

Tactic:
by
  simpa [prod_univ_castSucc, mul_assoc] using f.le_opNorm (snoc m x)

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

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

Tactic:
filter_upwards [eventually_cofinite_ne 0] with n hn
    simp only [norm_mul, norm_norm, norm_pow, NNReal.norm_eq]
    gcongr
    exact ofScalars_norm_le E c n (Nat.pos_iff_ne_zero.mpr hn)

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
x : E
⊢ AnalyticWithinAt 𝕜 f univ x ↔ AnalyticAt 𝕜 f x

Tactic:
simp [AnalyticWithinAt, AnalyticAt]

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 → ℝ := 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) =
    (((p 0) fun x_1 ↦ y.1 - x) - (p 0) fun x_1 ↦ y.2 - x) + (((p 1) fun x_1 ↦ y.1 - x) - (p 1) fun x_1 ↦ y.2 - x)

Tactic:
hf.coeff_zero,

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) = (f x - (p 0) fun x_1 ↦ y.2 - x) + (((p 1) fun x_1 ↦ y.1 - x) - (p 1) 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' : 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) = (f x - (p 0) fun x_1 ↦ y.2 - x) + (((p 1) fun x_1 ↦ y.1 - x) - (p 1) fun x_1 ↦ y.2 - x)

Tactic:
hf.coeff_zero,

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) = f x - f x + (((p 1) fun x_1 ↦ y.1 - x) - (p 1) fun x_1 ↦ y.2 - x)