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

Goal state before:
pp: case inr.succ.inl
R : Type u_2
inst✝ : CommSemiring R
φ : R⟦X⟧
n' : ℕ
ih : n' > 0 → (coeff 1) (φ ^ n') = ↑n' * (coeff 1) φ * constantCoeff φ ^ (n' - 1)
hn : n' + 1 > 0
h₁ : ∀ (m : ℕ), φ ^ (m + 1) = φ ^ m * φ
h₂ : antidiagonal 1 = {(0, 1), (1, 0)}
h' : n' = 0
h'' :
  ¬constantCoeff φ ^ n' * (coeff 1) φ + (coeff 1) (φ ^ n') * constantCoeff φ =
      (↑n' + 1) * (coeff 1) φ * constantCoeff φ ^ n'
⊢ False

Tactic:
rw [h'] at h''

Goal state after:
case inr.succ.inl
R : Type u_2
inst✝ : CommSemiring R
φ : R⟦X⟧
n' : ℕ
ih : n' > 0 → (coeff 1) (φ ^ n') = ↑n' * (coeff 1) φ * constantCoeff φ ^ (n' - 1)
hn : n' + 1 > 0
h₁ : ∀ (m : ℕ), φ ^ (m + 1) = φ ^ m * φ
h₂ : antidiagonal 1 = {(0, 1), (1, 0)}
h' : n' = 0
h'' :
  ¬constantCoeff φ ^ 0 * (coeff 1) φ + (coeff 1) (φ ^ 0) * constantCoeff φ =
      (↑0 + 1) * (coeff 1) φ * constantCoeff φ ^ 0
⊢ False
Module: Mathlib.RingTheory.PowerSeries.Basic

Goal state before:
pp: case h.left
A : Type u_2
inst✝ : CommRing A
hA : ¬Subsingleton A
a✝ : Nontrivial A
⊢ ¬Ideal.span {X} = ⊥

Tactic:
Ideal.span_singleton_eq_bot

Goal state after:
case h.left
A : Type u_2
inst✝ : CommRing A
hA : ¬Subsingleton A
a✝ : Nontrivial A
⊢ ¬X = 0
Module: Mathlib.Data.Finset.Finsupp

Goal state before:
pp: case refine_1
ι : Type u_1
α : Type u_2
inst✝ : Zero α
s : Finset ι
f : ι →₀ α
t : ι → Finset α
⊢ (∃ a ∈ s.pi t, { toFun := indicator s, inj' := ⋯ } a = f) → f.support ⊆ s ∧ ∀ i ∈ s, f i ∈ t i

Tactic:
rintro ⟨f, hf, rfl⟩
    refine ⟨support_indicator_subset _ _, fun i hi => ?_⟩
    convert! mem_pi.1 hf i hi
    exact indicator_of_mem hi _

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

Goal state before:
pp: 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})
⊢ ¬Ideal.span {a} = ⊥

Tactic:
Ideal.span_singleton_eq_bot

Goal state after:
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})
⊢ ¬a = 0
Module: Mathlib.RingTheory.MvPowerSeries.Order

Goal state before:
pp: case refine_1
σ : Type u_1
w : σ → ℕ
R : Type u_3
inst✝ : Ring R
p : MvPowerSeries σ R
T : Subring R
hp : ∀ (n : σ →₀ ℕ), (coeff n) p ∈ T
⊢ weightedOrder w (p.toSubring T hp) ≤ weightedOrder w p

pp: case refine_2
σ : Type u_1
w : σ → ℕ
R : Type u_3
inst✝ : Ring R
p : MvPowerSeries σ R
T : Subring R
hp : ∀ (n : σ →₀ ℕ), (coeff n) p ∈ T
⊢ weightedOrder w p ≤ weightedOrder w (p.toSubring T hp)

Tactic:
· refine le_weightedOrder w fun d hd => by
      simp [coeff_eq_zero_of_lt_weightedOrder w hd, ← p.coeff_toSubring T hp]

Goal state after:
case refine_2
σ : Type u_1
w : σ → ℕ
R : Type u_3
inst✝ : Ring R
p : MvPowerSeries σ R
T : Subring R
hp : ∀ (n : σ →₀ ℕ), (coeff n) p ∈ T
⊢ weightedOrder w p ≤ weightedOrder w (p.toSubring T hp)
Module: Mathlib.RingTheory.MvPowerSeries.Order

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : Semiring R
f : MvPowerSeries σ R
d : σ →₀ ℕ
h : (coeff d) f ≠ 0
⊢ f.order ≤ ↑(degree d)

Tactic:
rw [degree_eq_weight_one]
  exact weightedOrder_le _ h

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

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
p : ℕ
a : R
f : MvPowerSeries σ R
d : σ →₀ ℕ
⊢ ((coeff d) fun d ↦ if (weight w) d = p then (coeff d) (a • f) else 0) =
    (coeff d) ((RingHom.id R) a • fun d ↦ if (weight w) d = p then (coeff d) f else 0)

Tactic:
simp only [map_smul,
      smul_eq_mul, RingHom.id_apply, coeff_apply, mul_ite, mul_zero]

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

Goal state before:
pp: case pos
σ : 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
⊢ (coeff x.1) f * (coeff x.2) g =
    (coeff x.1) ((weightedHomogeneousComponent w p) f) * (coeff x.2) ((weightedHomogeneousComponent w q) g)

Tactic:
simp only [coeff_weightedHomogeneousComponent]

Goal state after:
case pos
σ : 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
⊢ (coeff x.1) f * (coeff x.2) g =
    (if (weight w) x.1 = p then (coeff x.1) f else 0) * if (weight w) x.2 = q then (coeff x.2) g else 0
Module: Mathlib.RingTheory.DedekindDomain.AdicValuation

Goal state before:
pp: case hp
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
inst✝ : Algebra S K
r : S
⊢ IsClosed {a | r • a = (Completion.coeRingHom.comp (algebraMap S (WithVal (valuation K v)))) r * a}

Tactic:
exact isClosed_eq (continuous_const_smul _) (continuous_const_mul _)

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
φ : R⟦X⟧
⊢ (∃ n, (coeff n) φ ≠ 0) ↔ φ ≠ 0

Tactic:
contrapose!

Goal state after:
R : Type u_1
inst✝ : Semiring R
φ : R⟦X⟧
⊢ (∀ (n : ℕ), (coeff n) φ = 0) ↔ φ = 0
Module: Mathlib.RingTheory.MvPowerSeries.PiTopology

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝¹ : TopologicalSpace R
inst✝ : Semiring R
f : MvPowerSeries σ R
h : constantCoeff f = 0
⊢ ∀ (n : ℕ), ∃ a, ∀ (b : ℕ), a ≤ b → ↑n < (f ^ b).order

Tactic:
refine fun n ↦ ⟨n + 1, fun m hm ↦ lt_of_lt_of_le ?_ (le_order_pow _)⟩

Goal state after:
σ : Type u_1
R : Type u_2
inst✝¹ : TopologicalSpace R
inst✝ : Semiring R
f : MvPowerSeries σ R
h : constantCoeff f = 0
n m : ℕ
hm : n + 1 ≤ m
⊢ ↑n < m • f.order
Module: Mathlib.RingTheory.PowerSeries.Order

Goal state before:
pp: case inl
R : Type u_1
inst✝ : Semiring R
φ ψ : R⟦X⟧
h : φ.order ≠ ψ.order
φ_lt_ψ : φ.order < ψ.order
⊢ (φ + ψ).order ≤ min φ.order ψ.order

Tactic:
apply order_add_of_order_ne.aux _ _ φ_lt_ψ

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

Goal state before:
pp: R : Type u_2
inst✝ : Ring R
φ : R⟦X⟧
h : (-φ).order ≠ φ.order
⊢ False

Tactic:
have : φ = 0 := by simpa using (order_add_of_order_ne _ _ h).symm

Goal state after:
R : Type u_2
inst✝ : Ring R
φ : R⟦X⟧
h : (-φ).order ≠ φ.order
this : φ = 0
⊢ False
Module: Mathlib.RingTheory.PowerSeries.PiTopology

Goal state before:
pp: case mpr
R : Type u_1
inst✝¹ : TopologicalSpace R
inst✝ : Semiring R
ι : Type u_2
f : ι → R⟦X⟧
⊢ (∀ (d : ℕ), ∃ a, HasSum (fun i ↦ (coeff d) (f i)) a) → ∃ a, ∀ (d : ℕ), HasSum (fun i ↦ (coeff d) (f i)) ((coeff d) a)

Tactic:
intro h
    choose a h using h
    exact ⟨mk a, by simpa using h⟩

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

Goal state before:
pp: σ : Type u_1
τ : Type u_4
S : Type u_5
inst✝¹ : CommRing S
a : σ → MvPowerSeries τ S
x : σ → ℕ
inst✝ : Finite τ
ha : HasSubst a
d : τ →₀ ℕ
i : σ
⊢ i ∉ {s | (coeff d) (a s) ≠ 0} → i ∉ {s | (coeff d) ↑((MvPowerSeries.truncTotal (x s)) (a s)) ≠ 0}

Tactic:
simp +contextual [coeff_truncTotal_eq_ite]

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
e : τ →₀ ℕ
this✝ : UniformSpace R := ⊥
this : UniformSpace S := ⊥
⊢ (coeff e) (subst a f) = ∑ᶠ (d : σ →₀ ℕ), (coeff d) f • (coeff e) (d.prod fun s e ↦ a s ^ e)

Tactic:
have := ((hasSum_aeval ha.hasEval f).map (coeff e) (continuous_coeff S e))

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
e : τ →₀ ℕ
this✝¹ : UniformSpace R := ⊥
this✝ : UniformSpace S := ⊥
this : HasSum (⇑(coeff e) ∘ fun d ↦ (coeff d) f • d.prod fun s e ↦ a s ^ e) ((coeff e) ((aeval ⋯) f))
⊢ (coeff e) (subst a f) = ∑ᶠ (d : σ →₀ ℕ), (coeff d) f • (coeff e) (d.prod fun s e ↦ a s ^ e)
Module: Mathlib.Analysis.Real.Cardinality

Goal state before:
pp: c : ℝ
h1 : 0 < c
h2 : c < 1 / 2
f g : ℕ → Bool
h : ¬f = g
this : ∃ n, f n ≠ g n
⊢ ¬cantorFunction c f = cantorFunction c g

Tactic:
let n := Nat.find this

Goal state after:
c : ℝ
h1 : 0 < c
h2 : c < 1 / 2
f g : ℕ → Bool
h : ¬f = g
this : ∃ n, f n ≠ g n
n : ℕ := Nat.find this
⊢ ¬cantorFunction c f = cantorFunction c g
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
f : MvPowerSeries σ R
n : τ →₀ ℕ
d : σ →₀ ℕ
hd : d ≠ 0
⊢ (coeff d) f • (coeff n) (d.prod fun s e ↦ 0 s ^ e) = 0

Tactic:
obtain ⟨i, hi⟩ : d.support.Nonempty := d.support_nonempty_iff.mpr hd

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
f : MvPowerSeries σ R
n : τ →₀ ℕ
d : σ →₀ ℕ
hd : d ≠ 0
i : σ
hi : i ∈ d.support
⊢ (coeff d) f • (coeff n) (d.prod fun s e ↦ 0 s ^ e) = 0
Module: Mathlib.RingTheory.MvPowerSeries.Substitution

Goal state before:
pp: case neg
σ : 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
hf : IsNilpotent (constantCoeff f)
d : σ →₀ ℕ
hd : ¬d = 0
⊢ IsNilpotent ((coeff d) f • constantCoeff (d.prod fun s e ↦ a s ^ e))

Tactic:
obtain ⟨i, hi⟩ : d.support.Nonempty := d.support_nonempty_iff.mpr hd

Goal state after:
case neg
σ : 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
hf : IsNilpotent (constantCoeff f)
d : σ →₀ ℕ
hd : ¬d = 0
i : σ
hi : i ∈ d.support
⊢ IsNilpotent ((coeff d) f • constantCoeff (d.prod fun s e ↦ a s ^ e))
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
υ : 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
ha : HasSubst a
hb : HasSubst b
⊢ (AlgHom.restrictScalars R (substAlgHom hb)).comp (substAlgHom ha) = substAlgHom ⋯

Tactic:
by
  let : UniformSpace R := ⊥
  let : UniformSpace S := ⊥
  let : UniformSpace T := ⊥
  apply comp_aeval (R := R) (ε := (substAlgHom hb).restrictScalars R) ha.hasEval
  simpa [AlgHom.coe_restrictScalars'] using continuous_subst (R := S) hb

Goal state after:
Module: Mathlib.NumberTheory.ArithmeticFunction.LFunction

Goal state before:
pp: case pos
R : Type u_1
inst✝ : CommRing R
q k : ℕ
hk : k ≠ 0
f : PowerSeries R
hq : 1 < q
n : ℕ
hn : ∃ i, q ^ i = n
⊢ ((ofPowerSeries (q ^ k)) f) n = ((ofPowerSeries q) (PowerSeries.subst (PowerSeries.X ^ k) f)) n

Tactic:
obtain ⟨i, rfl⟩ := hn

Goal state after:
case pos
R : Type u_1
inst✝ : CommRing R
q k : ℕ
hk : k ≠ 0
f : PowerSeries R
hq : 1 < q
i : ℕ
⊢ ((ofPowerSeries (q ^ k)) f) (q ^ i) = ((ofPowerSeries q) (PowerSeries.subst (PowerSeries.X ^ k) f)) (q ^ i)
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)
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)
⊢ ∑ i ∈ Set.Finite.toFinset h1, (coeff i) f • (coeff d) (i.prod fun s e ↦ a s ^ e) =
    ∑ i ∈ Set.Finite.toFinset h2,
      (coeff i) (∑ i ∈ range k, (homogeneousComponent i) f) • (coeff d) (i.prod fun s e ↦ a s ^ e)

Tactic:
have : h2.toFinset ⊆ h1.toFinset := by simp +contextual [coeff_homogeneousComponent]

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)
this : Set.Finite.toFinset h2 ⊆ Set.Finite.toFinset h1
⊢ ∑ i ∈ Set.Finite.toFinset h1, (coeff i) f • (coeff d) (i.prod fun s e ↦ a s ^ e) =
    ∑ i ∈ Set.Finite.toFinset h2,
      (coeff i) (∑ i ∈ range k, (homogeneousComponent i) f) • (coeff d) (i.prod fun s e ↦ a s ^ e)
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
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)
this : Set.Finite.toFinset h2 ⊆ Set.Finite.toFinset h1
n : σ →₀ ℕ
⊢ (coeff d) (n.prod fun s e ↦ a s ^ e) ≠ 0 → Finsupp.degree n ≤ Finsupp.degree d

Tactic:
contrapose!

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
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)
this : Set.Finite.toFinset h2 ⊆ Set.Finite.toFinset h1
n : σ →₀ ℕ
⊢ Finsupp.degree d < Finsupp.degree n → (coeff d) (n.prod fun s e ↦ a s ^ e) = 0
Module: Mathlib.NumberTheory.LSeries.Basic

Goal state before:
pp: f : ℕ → ℂ
x : ℝ
s : ℂ
hs : x < s.re
h : ∃ C, ∀ (n : ℕ), n ≠ 0 → ‖f n‖ ≤ C * ↑n ^ (x - 1)
⊢ LSeriesSummable f s

Tactic:
by
  obtain ⟨C, hC⟩ := h
  have hC₀ : 0 ≤ C := (norm_nonneg <| f 1).trans <| by simpa using hC 1 one_ne_zero
  have hsum : Summable fun n : ℕ ↦ ‖(C : ℂ) / n ^ (s + (1 - x))‖ := by
    simp_rw [div_eq_mul_inv, norm_mul, ← cpow_neg]
    have hsx : -s.re + x - 1 < -1 := by linarith only [hs]
    refine Summable.mul_left _ <|
      Summable.of_norm_bounded_eventually_nat (g := fun n ↦ (n : ℝ) ^ (-s.re + x - 1)) ?_ ?_
    · simpa
    · simp only [norm_norm, Filter.eventually_atTop]
      refine ⟨1, fun n hn ↦ le_of_eq ?_⟩
      simp only [norm_natCast_cpow_of_pos hn, add_re, sub_re, neg_re, ofReal_re, one_re]
      ring_nf
  refine Summable.of_norm <| hsum.of_nonneg_of_le (fun _ ↦ norm_nonneg _) (fun n ↦ ?_)
  rcases n.eq_zero_or_pos with rfl | hn
  · simpa only [term_zero, norm_zero] using norm_nonneg _
  have hn' : 0 < (n : ℝ) ^ s.re := Real.rpow_pos_of_pos (Nat.cast_pos.mpr hn) _
  simp_rw [term_of_ne_zero hn.ne', norm_div, norm_natCast_cpow_of_pos hn, div_le_iff₀ hn',
    norm_real, Real.norm_of_nonneg hC₀, div_eq_mul_inv, mul_assoc,
    ← Real.rpow_neg <| Nat.cast_nonneg _, ← Real.rpow_add <| Nat.cast_pos.mpr hn]
  simpa using hC n <| Nat.pos_iff_ne_zero.mp hn

Goal state after:
Module: Mathlib.NumberTheory.ArithmeticFunction.LFunction

Goal state before:
pp: case neg.hb
R : Type u_1
inst✝ : CommRing R
q k : ℕ
hk : k ≠ 0
f : PowerSeries R
hq : 1 < q
n : ℕ
hn : ∃ a, (q ^ k) ^ a = n
⊢ ∃ i, q ^ i = n

Tactic:
obtain ⟨i, rfl⟩ := hn

Goal state after:
case neg.hb
R : Type u_1
inst✝ : CommRing R
q k : ℕ
hk : k ≠ 0
f : PowerSeries R
hq : 1 < q
i : ℕ
⊢ ∃ i_1, q ^ i_1 = (q ^ k) ^ i
Module: Mathlib.RingTheory.PowerSeries.Substitution

Goal state before:
pp: R : Type u_2
inst✝² : CommRing R
τ : Type u_3
S : Type u_4
inst✝¹ : CommRing S
inst✝ : Algebra R S
a : MvPowerSeries τ S
ha : HasSubst a
p : Polynomial R
⊢ (substAlgHom ha) ↑p = (Polynomial.aeval a) p

Tactic:
p.toPowerSeries_toMvPowerSeries,

Goal state after:
R : Type u_2
inst✝² : CommRing R
τ : Type u_3
S : Type u_4
inst✝¹ : CommRing S
inst✝ : Algebra R S
a : MvPowerSeries τ S
ha : HasSubst a
p : Polynomial R
⊢ (substAlgHom ha) ↑((Polynomial.aeval (MvPolynomial.X ())) p) = (Polynomial.aeval a) p
Module: Mathlib.RingTheory.PowerSeries.Substitution

Goal state before:
pp: R : Type u_2
inst✝ : CommRing R
r : R
f : R⟦X⟧
⊢ (rescale r) f = subst (r • X) f

Tactic:
rescale_eq,

Goal state after:
R : Type u_2
inst✝ : CommRing R
r : R
f : R⟦X⟧
⊢ (MvPowerSeries.rescale fun x ↦ r) f = subst (r • X) f
Module: Mathlib.RingTheory.PowerSeries.Substitution

Goal state before:
pp: R : Type u_2
inst✝ : CommRing R
r : R
f : R⟦X⟧
n✝ : ℕ
⊢ (coeff n✝) (↑(rescaleAlgHom r) f) = (coeff n✝) ((rescale r) f)

Tactic:
rescale_eq,

Goal state after:
R : Type u_2
inst✝ : CommRing R
r : R
f : R⟦X⟧
n✝ : ℕ
⊢ (coeff n✝) (↑(rescaleAlgHom r) f) = (coeff n✝) ((MvPowerSeries.rescale fun x ↦ r) f)
Module: Mathlib.RingTheory.MvPowerSeries.Substitution

Goal state before:
pp: σ : 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 : σ →₀ ℕ
⊢ ((coeff n) fun n ↦ (n.prod fun s m ↦ a s ^ m) * (coeff n) (f * g)) =
    (coeff n) ((fun n ↦ (n.prod fun s m ↦ a s ^ m) * (coeff n) f) * fun n ↦ (n.prod fun s m ↦ a s ^ m) * (coeff n) g)

Tactic:
classical
    rw [coeff_apply, coeff_mul, coeff_mul, Finset.mul_sum]
    apply Finset.sum_congr rfl
    intro x hx
    simp only [Finset.mem_antidiagonal] at hx
    rw [← hx]
    simp only [coeff_apply]
    rw [Finsupp.prod_of_support_subset _ Finsupp.support_add,
      Finsupp.prod_of_support_subset x.1 Finset.subset_union_left,
      Finsupp.prod_of_support_subset x.2 Finset.subset_union_right]
    · simp only [← mul_assoc]
      congr 1
      rw [mul_assoc, mul_comm (f x.1), ← mul_assoc]
      congr 1
      rw [← Finset.prod_mul_distrib]
      apply Finset.prod_congr rfl
      simp [pow_add]
    all_goals {simp}

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

Goal state before:
pp: case e_a.succ.succ
R : Type u_2
inst✝¹ : CommRing R
P : R⟦X⟧
hP : constantCoeff P = 0
inst✝ : Invertible ((coeff 1) P)
n : ℕ
B : R⟦X⟧
hB : ∑ i, C (P.substInvFun ↑i) * X ^ ↑i = B
hB' : constantCoeff B = 0
k : R
hk : ⅟((coeff 1) P) * (coeff (n + 1 + 1)) (subst B P) = k
i : ℕ
⊢ (coeff (n + 1 + 1)) ((B + -(C k * X ^ (n + 2))) ^ (i + 1 + 1)) =
    (coeff (n + 1 + 1)) (B ^ (i + 1 + 1)) - if i + 1 + 1 = 1 then k else 0

Tactic:
simp only [add_assoc, Nat.reduceAdd]
            rw [add_comm B, add_pow, map_sum, Finset.sum_eq_single (a := 0)]
            · simp
            · rintro (_ | _ | j) hj hj'
              · simp at hj'
              · simp [mul_comm (C k), hB', mul_assoc, coeff_X_pow_mul']
              · rw [← neg_mul, mul_pow, ← pow_mul, mul_comm (_ ^ _)]
                simp [mul_assoc, coeff_X_pow_mul']
            · simp

Goal state after:
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)
⊢ subst P.substInv P = X

Tactic:
by
  ext n
  have := coeff_subst_sum_C_substInvFun_mul_X_pow_sub_X P hP n
  rw [map_sub, sub_eq_zero] at this
  rw [← this, coeff_subst', coeff_subst']
  · congr! 3 with m
    generalize hB : (∑ i : Fin (n + 1), C (substInvFun P ↑i) * X ^ i.1) = B
    have : X ^ (n + 1) ∣ mk (substInvFun P) - B := by
      rw [X_pow_dvd_iff]
      intro m hm
      simp +contextual [← hB, coeff_X_pow, Finset.sum_eq_single (⟨m, hm⟩ : Fin (n + 1)),
        Fin.ext_iff, @eq_comm _ m]
    obtain ⟨Q, hQ⟩ := this.trans (sub_dvd_pow_sub_pow _ _ m)
    simp [substInv, sub_eq_iff_eq_add.mp hQ, coeff_X_pow_mul']
  · simp [HasSubst, X, zero_pow_eq, C, substInvFun]
  · simp [HasSubst, ← constantCoeff.eq_def, substInvFun, substInv]

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

Goal state before:
pp: R : Type u_2
inst✝ : CommRing R
P : R⟦X⟧
hP : constantCoeff P = 0
hP' : IsUnit ((coeff 1) P)
⊢ subst (P.substInvOfIsUnit hP') P = X

Tactic:
by
  let := hP'.invertible
  rw [P.substInvOfIsUnit_eq_substInv hP', P.subst_substInv_right hP]

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 : f₁ =ᶠ[𝓝[≠] x] f
⊢ deriv f₁ =ᶠ[𝓝[≠] x] deriv f

Tactic:
Filter.EventuallyEq,

Goal state after:
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f f₁ : 𝕜 → F
x : 𝕜
h : ∀ᶠ (x : 𝕜) in 𝓝[≠] x, f₁ x = f x
⊢ ∀ᶠ (x : 𝕜) in 𝓝[≠] x, deriv f₁ x = deriv f x
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 : ∀ᶠ (x : 𝕜) in 𝓝[≠] x, f₁ x = f x
⊢ ∀ᶠ (x : 𝕜) in 𝓝[≠] x, deriv f₁ x = deriv f x

Tactic:
← eventually_nhdsNE_eventually_nhds_iff

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 : 𝕜) in 𝓝[≠] x, ∀ᶠ (x : 𝕜) in 𝓝 y, deriv f₁ x = deriv f 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 t : Set E
hs : (fun x' ↦ f x' - f x - f' (x' - x)) =o[𝕜; 𝓝[s] x] fun x' ↦ x' - x
ht : (fun x' ↦ f x' - f x - f' (x' - x)) =o[𝕜; 𝓝[t] x] fun x' ↦ x' - x
⊢ (fun x' ↦ f x' - f x - f' (x' - x)) =o[𝕜; 𝓝[s] x ⊔ 𝓝[t] x] fun x' ↦ x' - x

Tactic:
exact hs.sup ht

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
x : E
s t : Set E
st : s ⊆ t
f' : E →L[𝕜] F
hf' : HasFDerivWithinAt f f' t x
⊢ DifferentiableWithinAt 𝕜 f s x

Tactic:
exact ⟨f', hf'.mono st⟩

Goal state after: