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

Goal state before:
pp: case inr.succ.inr
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' : 1 ≤ n'
⊢ constantCoeff φ ^ n' * (coeff 1) φ + (coeff 1) (φ ^ n') * constantCoeff φ =
    (↑n' + 1) * (coeff 1) φ * constantCoeff φ ^ n'

Tactic:
ih

Goal state after:
case inr.succ.inr
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' : 1 ≤ n'
⊢ constantCoeff φ ^ n' * (coeff 1) φ + ↑n' * (coeff 1) φ * constantCoeff φ ^ (n' - 1) * constantCoeff φ =
    (↑n' + 1) * (coeff 1) φ * constantCoeff φ ^ n'

case inr.succ.inr
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' : 1 ≤ n'
⊢ n' > 0
Module: Mathlib.RingTheory.PowerSeries.Basic

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
this : ↑((monomial 0) 1) = (PowerSeries.monomial 0) 1
⊢ ↑1 = 1

Tactic:
PowerSeries.monomial_zero_eq_C_apply

Goal state after:
R : Type u_1
inst✝ : Semiring R
this : ↑((monomial 0) 1) = PowerSeries.C 1
⊢ ↑1 = 1
Module: Mathlib.RingTheory.PowerSeries.Basic

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
a : R
this : ↑((monomial 0) a) = (PowerSeries.monomial 0) a
⊢ ↑(C a) = PowerSeries.C a

Tactic:
PowerSeries.monomial_zero_eq_C_apply

Goal state after:
R : Type u_1
inst✝ : Semiring R
a : R
this : ↑((monomial 0) a) = PowerSeries.C a
⊢ ↑(C a) = PowerSeries.C a
Module: Mathlib.RingTheory.MvPowerSeries.Basic

Goal state before:
pp: case e'_3
σ : 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
⊢ #(range n \ s) = #(range n \ s) • 1

Tactic:
simp only [smul_eq_mul, mul_one]

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
⊢ ↑n ≤ weightedOrder w f

Tactic:
by
  by_contra! H
  have : (f.weightedOrder w).toNat = f.weightedOrder w := by
    rw [natCast_toNat_eq_self]; exact ne_top_of_lt H
  obtain ⟨d, hfd, hd⟩ := exists_coeff_ne_zero_and_weightedOrder w this
  rw [← hd, Nat.cast_lt] at H
  exact hfd (h d H)

Goal state after:
Module: Mathlib.Data.Finset.Finsupp

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

Tactic:
· refine fun h => ⟨fun i _ => f i, mem_pi.2 h.2, ?_⟩
    ext i
    exact ite_eq_left_iff.2 fun hi => (notMem_support_iff.1 fun H => hi <| h.1 H).symm

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
H : weightedOrder w f < weightedOrder w g
⊢ weightedOrder w (f + g) = weightedOrder w f

Tactic:
obtain ⟨n, hn : (n : ℕ∞) = _⟩ := ENat.ne_top_iff_exists.mp (ne_top_of_lt H)

Goal state after:
σ : 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
⊢ weightedOrder w (f + g) = weightedOrder w f
Module: Mathlib.RingTheory.MvPowerSeries.Order

Goal state before:
pp: σ✝ : Type u_1
R✝ : Type u_2
inst✝¹ : Semiring R✝
w✝ : σ✝ → ℕ
f✝ g✝ : MvPowerSeries σ✝ R✝
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
f g : MvPowerSeries σ R
h : weightedOrder w f ≠ weightedOrder w g
H₁ : weightedOrder w f < weightedOrder w g
⊢ weightedOrder w (f + g) ≤ min (weightedOrder w f) (weightedOrder w g)

Tactic:
simp only [le_inf_iff, weightedOrder_add_of_weightedOrder_lt.aux w H₁]

Goal state after:
σ✝ : Type u_1
R✝ : Type u_2
inst✝¹ : Semiring R✝
w✝ : σ✝ → ℕ
f✝ g✝ : MvPowerSeries σ✝ R✝
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
f g : MvPowerSeries σ R
h : weightedOrder w f ≠ weightedOrder w g
H₁ : weightedOrder w f < weightedOrder w g
⊢ weightedOrder w f ≤ weightedOrder w f ∧ weightedOrder w f ≤ weightedOrder w g
Module: Mathlib.RingTheory.MvPowerSeries.Order

Goal state before:
pp: case succ
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
f : MvPowerSeries σ R
n : ℕ
hn : n • weightedOrder w f ≤ weightedOrder w (f ^ n)
⊢ (n + 1) • weightedOrder w f ≤ weightedOrder w (f ^ (n + 1))

Tactic:
succ_nsmul,

Goal state after:
case succ
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
f : MvPowerSeries σ R
n : ℕ
hn : n • weightedOrder w f ≤ weightedOrder w (f ^ n)
⊢ n • weightedOrder w f + weightedOrder w f ≤ weightedOrder w (f ^ (n + 1))
Module: Mathlib.RingTheory.DedekindDomain.AdicValuation

Goal state before:
pp: case h
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
x : K
hv : (valuation K v) x ≤ 1
γ : (WithZero (Multiplicative ℤ))ˣ
n d : R
hd✝ : d ∈ v.asIdeal.primeCompl
hd : v.intValuation d = 1
hnd : x * (algebraMap R K) ↑⟨d, hd✝⟩ = (algebraMap R K) n
hd' : v.intValuation n ≤ v.intValuation d
a : R
hval : v.intValuation (n - a * d) < ↑γ
⊢ (valuation K v) ((algebraMap R K) a - x) =
    (valuation K v) (x * (algebraMap R K) ↑⟨d, hd✝⟩ - (algebraMap R K) a * (algebraMap R K) d)

Tactic:
← sub_mul,

Goal state after:
case h
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
x : K
hv : (valuation K v) x ≤ 1
γ : (WithZero (Multiplicative ℤ))ˣ
n d : R
hd✝ : d ∈ v.asIdeal.primeCompl
hd : v.intValuation d = 1
hnd : x * (algebraMap R K) ↑⟨d, hd✝⟩ = (algebraMap R K) n
hd' : v.intValuation n ≤ v.intValuation d
a : R
hval : v.intValuation (n - a * d) < ↑γ
⊢ (valuation K v) ((algebraMap R K) a - x) = (valuation K v) ((x - (algebraMap R K) a) * (algebraMap R K) ↑⟨d, hd✝⟩)
Module: Mathlib.RingTheory.MvPowerSeries.Trunc

Goal state before:
pp: case neg
σ : Type u_1
R : Type u_2
n : ℕ
inst✝¹ : Finite σ
inst✝ : CommSemiring R
p : MvPowerSeries σ R
x : σ →₀ ℕ
h : ¬degree x < n
⊢ MvPolynomial.coeff x ((truncTotal n) p) = if degree x < n then (coeff x) p else 0

Tactic:
rw [if_neg h, coeff_truncTotal_eq_zero _ (not_lt.mp h)]

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

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : Semiring R
f : MvPowerSeries σ R
⊢ f ≠ 0 ↔ ∃ n d, (coeff d) f ≠ 0 ∧ (weight fun x ↦ 1) d = n

Tactic:
exact ne_zero_iff_exists_coeff_ne_zero_and_weight (fun _ => 1)

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

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : Semiring R
f : MvPowerSeries σ R
n : ℕ
hf : constantCoeff f = 0
⊢ ↑n ≤ (f ^ n).order

Tactic:
by
  refine .trans ?_ (le_order_pow n)
  simpa using le_mul_of_one_le_right' (one_le_order_iff_constCoeff_eq_zero.mpr hf)

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

Goal state before:
pp: case pos
σ : Type u_1
R : Type u_2
n m : ℕ
inst✝¹ : Finite σ
inst✝ : CommSemiring R
p : MvPowerSeries σ R
d : σ →₀ ℕ
hd : degree d < n
⊢ MvPolynomial.coeff d ((truncTotal n) (p ^ m)) = MvPolynomial.coeff d ((truncTotal n) (↑((truncTotal n) p) ^ m))

Tactic:
coeff_truncTotal _ hd

Goal state after:
case pos
σ : Type u_1
R : Type u_2
n m : ℕ
inst✝¹ : Finite σ
inst✝ : CommSemiring R
p : MvPowerSeries σ R
d : σ →₀ ℕ
hd : degree d < n
⊢ (coeff d) (p ^ m) = (coeff d) (↑((truncTotal n) p) ^ m)
Module: Mathlib.RingTheory.MvPowerSeries.Order

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
f : MvPowerSeries σ R
p : ℕ
hf : ↑p = weightedOrder w f
hf' : (weightedHomogeneousComponent w p) f = 0
⊢ False

Tactic:
obtain ⟨d, hd⟩ := f.exists_coeff_ne_zero_and_weightedOrder w (by rw [← hf, toNat_natCast])

Goal state after:
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
f : MvPowerSeries σ R
p : ℕ
hf : ↑p = weightedOrder w f
hf' : (weightedHomogeneousComponent w p) f = 0
d : σ →₀ ℕ
hd : (coeff d) f ≠ 0 ∧ ↑((weight w) d) = weightedOrder w f
⊢ False
Module: Mathlib.RingTheory.MvPowerSeries.Order

Goal state before:
pp: case pos.inr.inl
σ : 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.1 < p
⊢ (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

Tactic:
rw [if_neg (ne_of_lt h), zero_mul]

Goal state after:
case pos.inr.inl
σ : 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.1 < p
⊢ (coeff x.1) f * (coeff x.2) g = 0
Module: Mathlib.RingTheory.PowerSeries.Order

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
φ : R⟦X⟧
n : ℕ
h : ↑n < φ.order
⊢ (coeff n) φ = 0

Tactic:
by
  contrapose! h
  exact order_le _ h

Goal state after:
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
⊢ Summable fun x ↦ f ^ x

Tactic:
apply summable_of_tendsto_order_atTop_nhds_top

Goal state after:
σ : Type u_1
R : Type u_2
inst✝¹ : TopologicalSpace R
inst✝ : Semiring R
f : MvPowerSeries σ R
h : constantCoeff f = 0
⊢ Tendsto (fun i ↦ (f ^ i).order) atTop (𝓝 ⊤)
Module: Mathlib.RingTheory.DedekindDomain.AdicValuation

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
b : ℝ≥0
hb : 1 < b
r : R
⊢ ¬(v.intAdicAbv hb) r = 1 ↔ r ∈ v.asIdeal

Tactic:
← v.intAdicAbv_lt_one_iff hb,

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
b : ℝ≥0
hb : 1 < b
r : R
⊢ ¬(v.intAdicAbv hb) r = 1 ↔ (v.intAdicAbv hb) r < 1
Module: Mathlib.RingTheory.PowerSeries.Order

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
φ : R⟦X⟧
n : ℕ
hf : constantCoeff φ = 0
⊢ ↑n ≤ (φ ^ n).order

Tactic:
by
  refine .trans ?_ (le_order_pow _ n)
  simpa using le_mul_of_one_le_right' (one_le_order_iff_constCoeff_eq_zero.mpr hf)

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

Goal state before:
pp: R : Type u_1
inst✝³ : TopologicalSpace R
inst✝² : Semiring R
ι : Type u_2
f : ι → R⟦X⟧
inst✝¹ : LinearOrder ι
inst✝ : LocallyFiniteOrderBot ι
h : Tendsto (fun i ↦ (f i).order) atTop (𝓝 ⊤)
⊢ Summable f

Tactic:
by
  rcases isEmpty_or_nonempty ι with hempty | hempty
  · apply summable_empty
  rw [summable_iff_summable_coeff]
  intro n
  simp_rw [ENat.tendsto_nhds_top_iff_natCast_lt, Filter.eventually_atTop] at h
  obtain ⟨i, hi⟩ := h n
  refine summable_of_hasFiniteSupport <| (Set.finite_Iic i).subset ?_
  simp_rw [Function.support_subset_iff, Set.mem_Iic]
  intro k hk
  contrapose! hk
  exact coeff_of_lt_order _ <| by simpa using (hi k hk.le)

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

Goal state before:
pp: σ : 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
inst✝² : IsUniformAddGroup R
inst✝¹ : IsUniformAddGroup S
inst✝ : IsLinearTopology S S
hφ : Continuous[inst✝⁵.toTopologicalSpace, inst✝³.toTopologicalSpace] ⇑φ
ha : HasEval a
I : Ideal S
hI : ↑I ∈ 𝓝 0
n : σ → ℕ := fun s ↦ sInf {n | a s ^ n.succ ∈ I}
hn_ne : ∀ (s : σ), {n | a s ^ n.succ ∈ I}.Nonempty
hn : (Function.support n).Finite
n₀ : σ →₀ ℕ := Finsupp.ofSupportFinite n hn
D : Set (σ →₀ ℕ) := Iic n₀
hD : D.Finite
d : σ →₀ ℕ
hd : d ∈ D
⊢ ∀ᶠ (p : MvPolynomial σ R) in 𝓝 0, φ (MvPolynomial.coeff d p) ∈ I

Tactic:
by
    have : Tendsto (φ ∘ coeff d ∘ toMvPowerSeries) (𝓝 0) (𝓝 0) :=
      hφ.comp (continuous_coeff R d) |>.comp continuous_induced_dom |>.tendsto' 0 0 (map_zero _)
    filter_upwards [this.eventually_mem hI] with f hf
    simpa using hf

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
i : σ
⊢ IsNilpotent (constantCoeff ↑((MvPowerSeries.truncTotal (x i)) (a i)))

Tactic:
rw [← coeff_zero_eq_constantCoeff_apply, MvPolynomial.coeff_coe,
      ← MvPolynomial.constantCoeff_eq, constantCoeff_truncTotal_eq_ite]

Goal state after:
σ : Type u_1
τ : Type u_4
S : Type u_5
inst✝¹ : CommRing S
a : σ → MvPowerSeries τ S
x : σ → ℕ
inst✝ : Finite τ
ha : HasSubst a
i : σ
⊢ IsNilpotent (if 0 < x i then constantCoeff (a i) else 0)
Module: Mathlib.Analysis.Real.Cardinality

Goal state before:
pp: case false
c : ℝ
f : ℕ → Bool
n : ℕ
h : f (n + 1) = false
⊢ cantorFunctionAux c f (n + 1) = c * cantorFunctionAux c (fun n ↦ f (n + 1)) n

Tactic:
simp [h, _root_.pow_succ']

Goal state after:
Module: Mathlib.Analysis.Real.Cardinality

Goal state before:
pp: case true
c : ℝ
f : ℕ → Bool
n : ℕ
h : f (n + 1) = true
⊢ cantorFunctionAux c f (n + 1) = c * cantorFunctionAux c (fun n ↦ f (n + 1)) n

Tactic:
simp [h, _root_.pow_succ']

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

Goal state before:
pp: σ : Type u_1
R : Type u_3
inst✝² : CommRing R
S : Type u_5
inst✝¹ : CommRing S
inst✝ : Algebra R S
f : MvPowerSeries σ R
⊢ (map (algebraMap R S)) f = subst X f

Tactic:
by
  ext e
  rw [coeff_map, coeff_subst HasSubst.X f e, finsum_eq_single _ e]
  · rw [← MvPowerSeries.monomial_one_eq, coeff_monomial_same,
      algebra_compatible_smul S, smul_eq_mul, mul_one]
  · intro d hd
    rw [← MvPowerSeries.monomial_one_eq, coeff_monomial_ne hd.symm, smul_zero]

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
hf : IsNilpotent (constantCoeff f)
⊢ IsNilpotent (constantCoeff (subst a f))

Tactic:
constantCoeff_subst ha

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
hf : IsNilpotent (constantCoeff f)
⊢ IsNilpotent (∑ᶠ (d : σ →₀ ℕ), (coeff d) f • constantCoeff (d.prod fun s e ↦ a s ^ e))
Module: Mathlib.NumberTheory.LSeries.Basic

Goal state before:
pp: case h
f : ℕ → ℂ
s : ℂ
h : Summable fun x ↦ ‖term f s x‖
n : ℕ
hn₀ : n ≠ 0
hn : (∑' (n : ℕ), ‖term f s n‖) * ↑n ^ s.re < ‖f n‖
this : ‖f n‖ ≤ (∑' (i : ℕ), ‖term f s i‖) * ↑n ^ s.re
⊢ False

Tactic:
exact (this.trans_lt hn).false.elim

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

Goal state before:
pp: case refine_2
f : ℕ → ℂ
x : ℝ
s : ℂ
hs : x < s.re
C : ℝ
hC : ∀ (n : ℕ), n ≠ 0 → ‖f n‖ ≤ C * ↑n ^ (x - 1)
hC₀ : 0 ≤ C
hsx : -s.re + x - 1 < -1
⊢ ∃ a, ∀ (b : ℕ), a ≤ b → ‖↑b ^ (-(s + (1 - ↑x)))‖ ≤ ↑b ^ (-s.re + x - 1)

Tactic:
refine ⟨1, fun n hn ↦ le_of_eq ?_⟩

Goal state after:
case refine_2
f : ℕ → ℂ
x : ℝ
s : ℂ
hs : x < s.re
C : ℝ
hC : ∀ (n : ℕ), n ≠ 0 → ‖f n‖ ≤ C * ↑n ^ (x - 1)
hC₀ : 0 ≤ C
hsx : -s.re + x - 1 < -1
n : ℕ
hn : 1 ≤ n
⊢ ‖↑n ^ (-(s + (1 - ↑x)))‖ = ↑n ^ (-s.re + x - 1)
Module: Mathlib.NumberTheory.ArithmeticFunction.LFunction

Goal state before:
pp: case pos
R : Type u_1
inst✝ : CommSemiring R
q : ℕ
f g : PowerSeries R
n : ℕ
hq : 1 < q
h : ∃ a, q ^ a = n
⊢ { toFun := Function.extend (fun x ↦ q ^ x) (fun x ↦ (PowerSeries.coeff x) (f + g)) 0, map_zero' := ⋯ } n =
    ({ toFun := Function.extend (fun x ↦ q ^ x) (fun x ↦ (PowerSeries.coeff x) f) 0, map_zero' := ⋯ } +
        { toFun := Function.extend (fun x ↦ q ^ x) (fun x ↦ (PowerSeries.coeff x) g) 0, map_zero' := ⋯ })
      n

pp: case neg
R : Type u_1
inst✝ : CommSemiring R
q : ℕ
f g : PowerSeries R
n : ℕ
hq : 1 < q
h : ¬∃ a, q ^ a = n
⊢ { toFun := Function.extend (fun x ↦ q ^ x) (fun x ↦ (PowerSeries.coeff x) (f + g)) 0, map_zero' := ⋯ } n =
    ({ toFun := Function.extend (fun x ↦ q ^ x) (fun x ↦ (PowerSeries.coeff x) f) 0, map_zero' := ⋯ } +
        { toFun := Function.extend (fun x ↦ q ^ x) (fun x ↦ (PowerSeries.coeff x) g) 0, map_zero' := ⋯ })
      n

Tactic:
· obtain ⟨a, rfl⟩ := h
        simp [(Nat.pow_right_injective hq).extend_apply]

Goal state after:
case neg
R : Type u_1
inst✝ : CommSemiring R
q : ℕ
f g : PowerSeries R
n : ℕ
hq : 1 < q
h : ¬∃ a, q ^ a = n
⊢ { toFun := Function.extend (fun x ↦ q ^ x) (fun x ↦ (PowerSeries.coeff x) (f + g)) 0, map_zero' := ⋯ } n =
    ({ toFun := Function.extend (fun x ↦ q ^ x) (fun x ↦ (PowerSeries.coeff x) f) 0, map_zero' := ⋯ } +
        { toFun := Function.extend (fun x ↦ q ^ x) (fun x ↦ (PowerSeries.coeff x) g) 0, map_zero' := ⋯ })
      n
Module: Mathlib.NumberTheory.LSeries.Basic

Goal state before:
pp: f : ℕ → ℂ
x : ℝ
s : ℂ
hs : x < s.re
h : f =O[atTop] fun n ↦ ↑n ^ (x - 1)
C : ℝ
hC : ∀ᶠ (x_1 : ℕ) in atTop, ‖f x_1‖ ≤ C * ‖↑x_1 ^ (x - 1)‖
m : ℕ
hm : ∀ (b : ℕ), m ≤ b → ‖f b‖ ≤ C * ‖↑b ^ (x - 1)‖
C' : ℝ := max C ((insert 0 (image (fun n ↦ ‖f n‖ / ↑n ^ (x - 1)) (range m))).max' ⋯)
hC'₀ : 0 ≤ C'
hCC' : C ≤ C'
⊢ LSeriesSummable f s

Tactic:
refine LSeriesSummable_of_le_const_mul_rpow hs ⟨C', fun n hn₀ ↦ ?_⟩

Goal state after:
f : ℕ → ℂ
x : ℝ
s : ℂ
hs : x < s.re
h : f =O[atTop] fun n ↦ ↑n ^ (x - 1)
C : ℝ
hC : ∀ᶠ (x_1 : ℕ) in atTop, ‖f x_1‖ ≤ C * ‖↑x_1 ^ (x - 1)‖
m : ℕ
hm : ∀ (b : ℕ), m ≤ b → ‖f b‖ ≤ C * ‖↑b ^ (x - 1)‖
C' : ℝ := max C ((insert 0 (image (fun n ↦ ‖f n‖ / ↑n ^ (x - 1)) (range m))).max' ⋯)
hC'₀ : 0 ≤ C'
hCC' : C ≤ C'
n : ℕ
hn₀ : n ≠ 0
⊢ ‖f n‖ ≤ C' * ↑n ^ (x - 1)
Module: Mathlib.RingTheory.PowerSeries.Substitution

Goal state before:
pp: R : Type u_2
inst✝ : CommRing R
r : R
⊢ ↑(rescaleAlgHom r) = rescale r

Tactic:
ext f
  rw [rescale_eq, RingHom.coe_coe, MvPowerSeries.rescaleAlgHom_apply]

Goal state after:
Module: Mathlib.Analysis.Convex.EGauge

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NormedDivisionRing 𝕜
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
c : 𝕜
hc : c ≠ 0
s : Set E
x : E
⊢ egauge 𝕜 (c • s) x ≤ egauge 𝕜 s x / ‖c‖ₑ

Tactic:
ENNReal.le_div_iff_mul_le (by simp [*]) (by simp)

Goal state after:
𝕜 : Type u_1
inst✝² : NormedDivisionRing 𝕜
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
c : 𝕜
hc : c ≠ 0
s : Set E
x : E
⊢ egauge 𝕜 (c • s) x * ‖c‖ₑ ≤ egauge 𝕜 s x
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 : ℕ
B : R⟦X⟧
hB : ∑ i, C (P.substInvFun ↑i) * X ^ ↑i = B
⊢ (coeff (n + 1 + 1)) (subst (B + C (-⅟((coeff 1) P) * (coeff (n + 1 + 1)) (subst B P)) * X ^ (n + 2)) P) -
      (coeff (n + 1 + 1)) X =
    0

Tactic:
have hB' : B.constantCoeff = 0 := by simp [← hB, zero_pow_eq, 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 : ℕ
B : R⟦X⟧
hB : ∑ i, C (P.substInvFun ↑i) * X ^ ↑i = B
hB' : constantCoeff B = 0
⊢ (coeff (n + 1 + 1)) (subst (B + C (-⅟((coeff 1) P) * (coeff (n + 1 + 1)) (subst B 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
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
⊢ ∑ᶠ (d : ℕ), (coeff d) P * ((coeff (n + 1 + 1)) (B ^ d) - if d = 1 then k else 0) = 0

Tactic:
mul_sub

Goal state after:
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
⊢ ∑ᶠ (d : ℕ), ((coeff d) P * (coeff (n + 1 + 1)) (B ^ d) - (coeff d) P * if d = 1 then k else 0) = 0
Module: Mathlib.Analysis.Calculus.TangentCone.Defs

Goal state before:
pp: case refine_3
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
⊢ Tendsto (fun n ↦ n.1 • n.2) (comap (fun p ↦ p.1 • p.2) (𝓝 y) ⊓ ⊤ ×ˢ 𝓝[(fun x_1 ↦ x + x_1) ⁻¹' s] 0) (𝓝 y)

Tactic:
· exact tendsto_comap.mono_left inf_le_left

Goal state after:
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 : Set E
x : E
hx : ∃ᶠ (x : E) in 𝓝 x, x ∈ s
⊢ 0 ∈ tangentConeAt 𝕜 s x

Tactic:
apply mem_tangentConeAt_of_frequently (𝓝 x) 1 (· + (-x))

Goal state after:
case hd₀
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : AddCommGroup E
inst✝³ : Semiring 𝕜
inst✝² : Module 𝕜 E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousAdd E
s : Set E
x : E
hx : ∃ᶠ (x : E) in 𝓝 x, x ∈ s
⊢ Tendsto (fun x_1 ↦ x_1 + -x) (𝓝 x) (𝓝 0)

case hds
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : AddCommGroup E
inst✝³ : Semiring 𝕜
inst✝² : Module 𝕜 E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousAdd E
s : Set E
x : E
hx : ∃ᶠ (x : E) in 𝓝 x, x ∈ s
⊢ ∃ᶠ (n : E) in 𝓝 x, x + (n + -x) ∈ s

case hcd
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : AddCommGroup E
inst✝³ : Semiring 𝕜
inst✝² : Module 𝕜 E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousAdd E
s : Set E
x : E
hx : ∃ᶠ (x : E) in 𝓝 x, x ∈ s
⊢ Tendsto (fun n ↦ 1 n • (n + -x)) (𝓝 x) (𝓝 0)
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[𝕜; pure x] g ∧ f =o[𝕜; 𝓝[s] x] g ↔ f =o[𝕜; 𝓝[s] x] g

Tactic:
and_iff_right

Goal state after:
α : 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[𝕜; 𝓝[s] x] g ↔ f =o[𝕜; 𝓝[s] x] g

α : 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[𝕜; pure x] g
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
x y : 𝕜
⊢ (fderiv 𝕜 f x) y = (fderiv 𝕜 f x) (y • 1)

Tactic:
simp only [smul_eq_mul, mul_one]

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

Goal state before:
pp: case h₁
α : Type u_1
𝕜 : Type u_3
E : Type u_4
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : TopologicalSpace E
inst✝² : Module 𝕜 E
l : Filter α
f : α → E
inst✝¹ : ContinuousAdd E
inst✝ : ContinuousSMul 𝕜 E
x : E
h : Tendsto (fun x_1 ↦ f x_1 - x) l (𝓝 0)
U : Set E
hU₀ : U ∈ 𝓝 0
hUb : Balanced 𝕜 U
r : ℝ≥0
hr₀ : 0 < r
hr₁ : r ≤ 1
hr : ↑r ≤ (egauge 𝕜 U x)⁻¹
a : α
ha : f a - x ∈ U
⊢ 1 ≤ (↑r)⁻¹

Tactic:
simp [hr₁]

Goal state after: