mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.GroupTheory.ArchimedeanDensely

Goal state before:
pp: case mp
G : Type u_1
inst✝² : CommGroup G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedMonoid G
a b : G
ha : a ≠ 1
⊢ (∃ n, a ^ n = b) → ∃! k, a ^ k = b

Tactic:
suffices Function.Injective (a ^ · : ℤ → G) by
      rintro ⟨m, rfl⟩
      exact ⟨m, rfl, fun k hk ↦ this hk⟩

Goal state after:
case mp
G : Type u_1
inst✝² : CommGroup G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedMonoid G
a b : G
ha : a ≠ 1
⊢ Function.Injective fun x ↦ a ^ x
Module: Mathlib.Topology.Algebra.Valued.ValuedField

Goal state before:
pp: case inr
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
x₀ : hat K
h : x₀ ≠ 0
preimage_one : ⇑v ⁻¹' {1} ∈ 𝓝 1
⊢ ∃ c, Tendsto (⇑v.restrict) (Filter.comap Completion.coe' (𝓝 x₀)) (𝓝 c)

Tactic:
obtain ⟨V, V_in, hV⟩ : ∃ V ∈ 𝓝 (1 : hat K), ∀ x : K, (x : hat K) ∈ V → (v x : Γ₀) = 1 := by
      rwa [Completion.isDenseInducing_coe.nhds_eq_comap, mem_comap] at preimage_one

Goal state after:
case inr
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
x₀ : hat K
h : x₀ ≠ 0
preimage_one : ⇑v ⁻¹' {1} ∈ 𝓝 1
V : Set (hat K)
V_in : V ∈ 𝓝 1
hV : ∀ (x : K), ↑x ∈ V → v x = 1
⊢ ∃ c, Tendsto (⇑v.restrict) (Filter.comap Completion.coe' (𝓝 x₀)) (𝓝 c)
Module: Mathlib.GroupTheory.ArchimedeanDensely

Goal state before:
pp: G : Type u_1
inst✝³ : CommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedMonoid G
inst✝ : MulArchimedean G
⊢ Nonempty (G ≃*o Multiplicative ℤ) ↔ ¬DenselyOrdered G

Tactic:
let e : G ≃o Additive G := .refl G

Goal state after:
G : Type u_1
inst✝³ : CommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedMonoid G
inst✝ : MulArchimedean G
e : G ≃o Additive G := OrderIso.refl G
⊢ Nonempty (G ≃*o Multiplicative ℤ) ↔ ¬DenselyOrdered G
Module: Mathlib.RingTheory.PowerSeries.Basic

Goal state before:
pp: case h₀
R : Type u_1
inst✝ : Semiring R
p : R⟦X⟧
n d : ℕ
⊢ ∀ b ∈ antidiagonal (d + n), b ≠ (n, d) → (coeff b.1) (X ^ n) * (coeff b.2) p = 0

pp: case h₁
R : Type u_1
inst✝ : Semiring R
p : R⟦X⟧
n d : ℕ
⊢ (n, d) ∉ antidiagonal (d + n) → (coeff (n, d).1) (X ^ n) * (coeff (n, d).2) p = 0

Tactic:
· rintro ⟨i, j⟩ h1 h2
    rw [coeff_X_pow, if_neg, zero_mul]
    rintro rfl
    apply h2
    rw [mem_antidiagonal, add_comm, add_right_cancel_iff] at h1
    subst h1
    rfl

Goal state after:
case h₁
R : Type u_1
inst✝ : Semiring R
p : R⟦X⟧
n d : ℕ
⊢ (n, d) ∉ antidiagonal (d + n) → (coeff (n, d).1) (X ^ n) * (coeff (n, d).2) p = 0
Module: Mathlib.Topology.Algebra.Valued.ValuedField

Goal state before:
pp: case refine_1
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
a b : (ofClass v).ValueGroup₀
hab : valueGroup₀_hom_extensionValuation a = valueGroup₀_hom_extensionValuation b
x : K := ⋯.choose
hx_def : x = ⋯.choose
y : K := ⋯.choose
hy_def : y = ⋯.choose
hx : v x = embedding a
hy : v y = embedding b
⊢ embedding a = embedding b

Tactic:
simp only [valueGroup₀_hom_extensionValuation, coe_mk, ZeroHom.coe_mk] at hab

Goal state after:
case refine_1
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
a b : (ofClass v).ValueGroup₀
hab : extensionValuation.restrict ↑⋯.choose = extensionValuation.restrict ↑⋯.choose
x : K := ⋯.choose
hx_def : x = ⋯.choose
y : K := ⋯.choose
hy_def : y = ⋯.choose
hx : v x = embedding a
hy : v y = embedding b
⊢ embedding a = embedding b
Module: Mathlib.RingTheory.PowerSeries.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
a : R
f g : R⟦X⟧
n✝ : ℕ
⊢ (coeff n✝) (mk fun n ↦ a ^ n * (coeff n) (f * g)) =
    (coeff n✝) ((mk fun n ↦ a ^ n * (coeff n) f) * mk fun n ↦ a ^ n * (coeff n) g)

Tactic:
rw [PowerSeries.coeff_mul, PowerSeries.coeff_mk, PowerSeries.coeff_mul, Finset.mul_sum]

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
a : R
f g : R⟦X⟧
n✝ : ℕ
⊢ ∑ i ∈ antidiagonal n✝, a ^ n✝ * ((coeff i.1) f * (coeff i.2) g) =
    ∑ p ∈ antidiagonal n✝, (coeff p.1) (mk fun n ↦ a ^ n * (coeff n) f) * (coeff p.2) (mk fun n ↦ a ^ n * (coeff n) g)
Module: Mathlib.RingTheory.MvPowerSeries.Basic

Goal state before:
pp: case insert
σ : Type u_1
R : Type u_3
inst✝² : CommSemiring R
ι : Type u_4
inst✝¹ : DecidableEq ι
inst✝ : DecidableEq σ
f : ι → MvPowerSeries σ R
a : ι
s : Finset ι
ha : a ∉ s
ih : ∀ (d : σ →₀ ℕ), (coeff d) (∏ j ∈ s, f j) = ∑ l ∈ s.finsuppAntidiag d, ∏ i ∈ s, (coeff (l i)) (f i)
d : σ →₀ ℕ
⊢ (coeff d) (∏ j ∈ insert a s, f j) =
    ∑
      l ∈
        (antidiagonal d).biUnion fun p ↦
          Finset.map { toFun := fun f ↦ (↑f).update a p.1, inj' := ⋯ } (s.finsuppAntidiag p.2).attach,
      ∏ i ∈ insert a s, (coeff (l i)) (f i)

Tactic:
prod_insert ha,

Goal state after:
case insert
σ : Type u_1
R : Type u_3
inst✝² : CommSemiring R
ι : Type u_4
inst✝¹ : DecidableEq ι
inst✝ : DecidableEq σ
f : ι → MvPowerSeries σ R
a : ι
s : Finset ι
ha : a ∉ s
ih : ∀ (d : σ →₀ ℕ), (coeff d) (∏ j ∈ s, f j) = ∑ l ∈ s.finsuppAntidiag d, ∏ i ∈ s, (coeff (l i)) (f i)
d : σ →₀ ℕ
⊢ (coeff d) (f a * ∏ x ∈ s, f x) =
    ∑
      l ∈
        (antidiagonal d).biUnion fun p ↦
          Finset.map { toFun := fun f ↦ (↑f).update a p.1, inj' := ⋯ } (s.finsuppAntidiag p.2).attach,
      ∏ i ∈ insert a s, (coeff (l i)) (f i)
Module: Mathlib.RingTheory.DedekindDomain.AdicValuation

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
r : R
n : ℕ
⊢ exp (-↑n) ≤ v.intValuation r ↔ ¬v.intValuation r ≤ exp (-↑(n + 1))

Tactic:
not_le,

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
r : R
n : ℕ
⊢ exp (-↑n) ≤ v.intValuation r ↔ exp (-↑(n + 1)) < v.intValuation r
Module: Mathlib.RingTheory.DedekindDomain.AdicValuation

Goal state before:
pp: case inr
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
n d : R
hd : d ∈ nonZeroDivisors R
h : ∀ (v : HeightOneSpectrum R), (valuation K v) (IsLocalization.mk' K n ⟨d, hd⟩) ≤ 1
hx : IsLocalization.mk' K n ⟨d, hd⟩ * (algebraMap R K) ↑(n, ⟨d, hd⟩).2 = (algebraMap R K) (n, ⟨d, hd⟩).1
hn0 : n ≠ 0
hd0 : d ≠ 0
ine : ∀ {r : R}, r ≠ 0 → Ideal.span {r} ≠ ⊥
⊢ Ideal.span {d} ∣ Ideal.span {n}

Tactic:
← Associates.mk_le_mk_iff_dvd,

Goal state after:
case inr
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
n d : R
hd : d ∈ nonZeroDivisors R
h : ∀ (v : HeightOneSpectrum R), (valuation K v) (IsLocalization.mk' K n ⟨d, hd⟩) ≤ 1
hx : IsLocalization.mk' K n ⟨d, hd⟩ * (algebraMap R K) ↑(n, ⟨d, hd⟩).2 = (algebraMap R K) (n, ⟨d, hd⟩).1
hn0 : n ≠ 0
hd0 : d ≠ 0
ine : ∀ {r : R}, r ≠ 0 → Ideal.span {r} ≠ ⊥
⊢ Associates.mk (Ideal.span {d}) ≤ Associates.mk (Ideal.span {n})
Module: Mathlib.RingTheory.MvPowerSeries.Trunc

Goal state before:
pp: σ : Type u_1
R : Type u_2
n : ℕ
inst✝¹ : Finite σ
inst✝ : CommSemiring R
p : MvPolynomial σ R
h : n ≠ 0
⊢ ↑p.support ⊆ {f | degree f < n} ↔ p.totalDegree < n

Tactic:
MvPolynomial.totalDegree,

Goal state after:
σ : Type u_1
R : Type u_2
n : ℕ
inst✝¹ : Finite σ
inst✝ : CommSemiring R
p : MvPolynomial σ R
h : n ≠ 0
⊢ ↑p.support ⊆ {f | degree f < n} ↔ (p.support.sup fun s ↦ s.sum fun x e ↦ e) < n
Module: Mathlib.Topology.Algebra.TopologicallyNilpotent

Goal state before:
pp: R : Type u_1
inst✝² : TopologicalSpace R
inst✝¹ : CommRing R
inst✝ : IsLinearTopology R R
a : R
⊢ a ∈ topologicalNilradical R ↔ IsTopologicallyNilpotent a

Tactic:
simp [topologicalNilradical]

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

Goal state before:
pp: case pos.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 ∧ (weight w) x.2 = q
⊢ (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

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

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 =
    (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_pos h.1, if_pos h.2]

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 =
    (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

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 =
    (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.MvPowerSeries.PiTopology

Goal state before:
pp: case pos
σ : Type u_1
R : Type u_2
inst✝¹ : TopologicalSpace R
inst✝ : Semiring R
r : R
d : σ →₀ ℕ
h✝ : d = 0
⊢ Tendsto (fun i ↦ i) (𝓝 r) (𝓝 r)

pp: case neg
σ : Type u_1
R : Type u_2
inst✝¹ : TopologicalSpace R
inst✝ : Semiring R
r : R
d : σ →₀ ℕ
h✝ : ¬d = 0
⊢ Tendsto (fun i ↦ 0) (𝓝 r) (𝓝 0)

Tactic:
· exact tendsto_id

Goal state after:
case neg
σ : Type u_1
R : Type u_2
inst✝¹ : TopologicalSpace R
inst✝ : Semiring R
r : R
d : σ →₀ ℕ
h✝ : ¬d = 0
⊢ Tendsto (fun i ↦ 0) (𝓝 r) (𝓝 0)
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 y : R
⊢ ⟨{ toCompletion := ↑((WithVal.equiv (valuation K v)).symm ((algebraMap R K) (x + y))) }, ⋯⟩ =
    ⟨{ toCompletion := ↑((WithVal.equiv (valuation K v)).symm ((algebraMap R K) x)) }, ⋯⟩ +
      ⟨{ toCompletion := ↑((WithVal.equiv (valuation K v)).symm ((algebraMap R K) y)) }, ⋯⟩

Tactic:
ext
      simp [map_add, UniformSpace.Completion.coe_add]

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

Goal state before:
pp: case inr
σ : Type u_3
R : Type u_4
inst✝³ : TopologicalSpace R
inst✝² : CommSemiring R
ι : Type u_5
f : ι → MvPowerSeries σ R
inst✝¹ : LinearOrder ι
inst✝ : LocallyFiniteOrderBot ι
w : σ → ℕ
h : Tendsto (fun i ↦ weightedOrder w (f i)) atTop (𝓝 ⊤)
hempty : Nonempty ι
⊢ Summable fun x ↦ ∏ i ∈ x, f i

Tactic:
refine summable_iff_summable_coeff.mpr fun d ↦ summable_of_hasFiniteSupport ?_

Goal state after:
case inr
σ : Type u_3
R : Type u_4
inst✝³ : TopologicalSpace R
inst✝² : CommSemiring R
ι : Type u_5
f : ι → MvPowerSeries σ R
inst✝¹ : LinearOrder ι
inst✝ : LocallyFiniteOrderBot ι
w : σ → ℕ
h : Tendsto (fun i ↦ weightedOrder w (f i)) atTop (𝓝 ⊤)
hempty : Nonempty ι
d : σ →₀ ℕ
⊢ HasFiniteSupport fun i ↦ (coeff d) (∏ i ∈ i, f i)
Module: Mathlib.Analysis.Real.Cardinality

Goal state before:
pp: a : ℝ
⊢ 𝔠 ≤ #↑(Ioi a)

Tactic:
rw [← not_lt]

Goal state after:
a : ℝ
⊢ ¬#↑(Ioi a) < 𝔠
Module: Mathlib.Analysis.Real.Cardinality

Goal state before:
pp: x y : ℝ
⊢ (Ioc x y).Countable ↔ y ≤ x

Tactic:
by
  refine ⟨fun h ↦ ?_, fun h ↦ by simp [h]⟩
  contrapose! h
  rw [← Cardinal.le_aleph0_iff_set_countable, Cardinal.mk_Ioc_real h, not_le]
  exact Cardinal.aleph0_lt_continuum

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

Goal state before:
pp: ⊢ ¬#↑Set.univ ≤ ℵ₀

Tactic:
not_le,

Goal state after:
⊢ ℵ₀ < #↑Set.univ
Module: Mathlib.NumberTheory.ArithmeticFunction.LFunction

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
q : ℕ
hq : 1 < q
f : PowerSeries R
k : ℕ
⊢ ((ofPowerSeries q) f) (q ^ k) = (PowerSeries.coeff k) f

Tactic:
ofPowerSeries_apply hq,

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
q : ℕ
hq : 1 < q
f : PowerSeries R
k : ℕ
⊢ Function.extend (fun x ↦ q ^ x) (fun x ↦ (PowerSeries.coeff x) f) 0 (q ^ k) = (PowerSeries.coeff k) 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
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 : σ →₀ ℕ
hc : Finsupp.degree d < Finsupp.degree n
⊢ ↑(Finsupp.degree n) ≤ ∑ i ∈ n.support, (a i ^ n i).order

Tactic:
exact_mod_cast sum_le_sum fun i hi => le_order_pow_of_constantCoeff_eq_zero _ (ha₁ i)

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

Goal state before:
pp: case neg
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:
ofPowerSeries_apply hq,

Goal state after:
case neg
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 =
    Function.extend (fun x ↦ q ^ x) (fun x ↦ (PowerSeries.coeff x) (PowerSeries.subst (PowerSeries.X ^ k) f)) 0 n
Module: Mathlib.NumberTheory.LSeries.Basic

Goal state before:
pp: case inl
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
hn : m ≤ n
⊢ ‖f n‖ ≤ C' * ↑n ^ (x - 1)

pp: case inr
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
hn : n < m
⊢ ‖f n‖ ≤ C' * ↑n ^ (x - 1)

Tactic:
· refine (hm n hn).trans ?_
    have hn₀ : (0 : ℝ) ≤ n := cast_nonneg _
    gcongr
    rw [Real.norm_eq_abs, abs_rpow_of_nonneg hn₀, abs_of_nonneg hn₀]

Goal state after:
case inr
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
hn : n < m
⊢ ‖f n‖ ≤ C' * ↑n ^ (x - 1)
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
⊢ (fun n ↦ (n.prod fun s m ↦ a s ^ m) * (coeff n) 0) = 0

Tactic:
ext
    simp [map_zero, coeff_apply]

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

Goal state before:
pp: 𝕜 : Type u
E : Type v
F : Type w
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E (E →L[𝕜] F)
z : F
n : ℕ
⊢ (p.unshift z).shift n = p n

Tactic:
simp only [shift, Nat.succ_eq_add_one, unshift]

Goal state after:
𝕜 : Type u
E : Type v
F : Type w
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E (E →L[𝕜] F)
z : F
n : ℕ
⊢ ((continuousMultilinearCurryRightEquiv' 𝕜 n E F).symm (p n)).curryRight = p 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
p : FormalMultilinearSeries 𝕜 E F
k l : ℕ
⊢ ∑ a, ‖p.changeOriginSeriesTerm k l ↑a ⋯‖₊ = ∑' (x : { s // s.card = l }), ‖p (k + l)‖₊

Tactic:
tsum_fintype,

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
k l : ℕ
⊢ ∑ a, ‖p.changeOriginSeriesTerm k l ↑a ⋯‖₊ = ∑ x, ‖p (k + l)‖₊
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
r : ℝ≥0
h : ↑r < p.radius
a : ℝ
ha : a ∈ Ioo 0 1
C : ℝ
hC : C > 0
H : ∀ (n : ℕ), |‖p n‖ * ↑r ^ n| ≤ C * a ^ n
⊢ ∃ a ∈ Ioo 0 1, ∃ C > 0, ∀ (n : ℕ), ‖p n‖ * ↑r ^ n ≤ C * a ^ n

Tactic:
exact ⟨a, ha, C, hC, fun n => (le_abs_self _).trans (H n)⟩

Goal state after:
Module: Mathlib.Analysis.Normed.Module.Multilinear.Curry

Goal state before:
pp: 𝕜 : Type u
G : Type wG
G' : Type wG'
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
inst✝¹ : NormedAddCommGroup G'
inst✝ : NormedSpace 𝕜 G'
f : G [×0]→L[𝕜] G'
m : Fin 0 → G
⊢ ‖(uncurry0 𝕜 G f.curry0) m‖ ≤ ‖f.curry0‖ * ∏ i, ‖m i‖

Tactic:
by
      simp [-ContinuousMultilinearMap.apply_zero_uncurry0]

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
pf : FormalMultilinearSeries 𝕜 E F
x : E
r : ℝ≥0∞
hf : HasFiniteFPowerSeriesOnBall f pf x 1 r
y : E
hy : y ∈ Metric.eball x r
⊢ edist x x < r

Tactic:
edist_self

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
pf : FormalMultilinearSeries 𝕜 E F
x : E
r : ℝ≥0∞
hf : HasFiniteFPowerSeriesOnBall f pf x 1 r
y : E
hy : y ∈ Metric.eball x r
⊢ 0 < 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 ((-ContinuousLinearMap.id 𝕜 E) ∘SL f) =
    (ofScalars E fun k ↦ (-1) ^ k * c k).compContinuousLinearMap f

Tactic:
rw [← FormalMultilinearSeries.compContinuousLinearMap_comp, ofScalars_comp_neg_id]

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
y z : E
hz1 : x + y + z ∈ insert (x + y) (s + {y})
hz2 : z ∈ Metric.eball 0 r
⊢ HasSum (fun n ↦ (p n) fun x ↦ z) (f (x + y + z - y))

Tactic:
have : x + z ∈ insert x s := by
      simp only [add_singleton, image_add_right, mem_insert_iff, add_eq_left, mem_preimage] at hz1 ⊢
      abel_nf at hz1
      assumption

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
y z : E
hz1 : x + y + z ∈ insert (x + y) (s + {y})
hz2 : z ∈ Metric.eball 0 r
this : x + z ∈ insert x s
⊢ HasSum (fun n ↦ (p n) fun x ↦ z) (f (x + y + z - y))
Module: Mathlib.Analysis.Analytic.CPolynomialDef

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → p m = 0
x y : E
f : (k : ℕ) × (l : ℕ) × { s // s.card = l } → F :=
  fun s ↦ ((p.changeOriginSeriesTerm s.fst s.snd.fst ↑s.snd.snd ⋯) fun x_1 ↦ x) fun x ↦ y
finsupp : (Function.support f).Finite
hfkl : ∀ (k l : ℕ), HasSum (fun x ↦ f ⟨k, ⟨l, x⟩⟩) (((p.changeOriginSeries k l) fun x_1 ↦ x) fun x ↦ y)
k : ℕ
this : ∀ m ∉ Finset.range n, ((p.changeOriginSeries k m) fun x_1 ↦ x) = 0
⊢ HasSum (fun x ↦ f ⟨k, x⟩) ((p.changeOrigin x k) fun x ↦ y)

Tactic:
rw [changeOrigin, FormalMultilinearSeries.sum,
      ContinuousMultilinearMap.tsum_eval (summable_of_ne_finset_zero this)]

Goal state after:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → p m = 0
x y : E
f : (k : ℕ) × (l : ℕ) × { s // s.card = l } → F :=
  fun s ↦ ((p.changeOriginSeriesTerm s.fst s.snd.fst ↑s.snd.snd ⋯) fun x_1 ↦ x) fun x ↦ y
finsupp : (Function.support f).Finite
hfkl : ∀ (k l : ℕ), HasSum (fun x ↦ f ⟨k, ⟨l, x⟩⟩) (((p.changeOriginSeries k l) fun x_1 ↦ x) fun x ↦ y)
k : ℕ
this : ∀ m ∉ Finset.range n, ((p.changeOriginSeries k m) fun x_1 ↦ x) = 0
⊢ HasSum (fun x ↦ f ⟨k, x⟩) (∑' (a : ℕ), ((p.changeOriginSeries k a) fun x_1 ↦ x) fun x ↦ y)
Module: Mathlib.Analysis.Analytic.Basic

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
p : FormalMultilinearSeries 𝕜 E F
x : E
r : ℝ≥0∞
g : F →L[𝕜] G
h : HasFPowerSeriesOnBall f p x r
⊢ HasFPowerSeriesOnBall (⇑g ∘ f) (g.compFormalMultilinearSeries p) x r

Tactic:
rw [← hasFPowerSeriesWithinOnBall_univ] at h ⊢
  exact g.comp_hasFPowerSeriesWithinOnBall h

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
x : E
r : ℝ≥0∞
hr : HasFPowerSeriesOnBall f p x r
y : E
hy : y ∈ Metric.eball 0 r
⊢ Tendsto (fun n ↦ p.partialSum n y) atTop (𝓝 (f (x + y)))

Tactic:
exact hr.tendsto_partialSum hy

Goal state after: