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

Goal state before:
pp: R : Type u_2
inst✝ : CommSemiring R
f : R⟦X⟧
n a : ℕ
⊢ (trunc n) (↑((trunc n) f) ^ a) = (trunc n) (f ^ a)

Tactic:
by

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

Goal state before:
pp: R : Type u_4
inst✝³ : CommRing R
inst✝² : IsDedekindDomain R
inst✝¹ : Algebra R ℚ
inst✝ : IsFractionRing R ℚ
𝔭 : HeightOneSpectrum R
x : ℚ
⊢ (valuation ℚ 𝔭) x ≤ 1 ↔ ↑x.den ∉ 𝔭.asIdeal

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
f : R⟦X⟧
⊢ X ^ f.order.toNat * f.divXPowOrder = f

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
φ : R⟦X⟧
⊢ X ^ φ.order.toNat ∣ φ

Tactic:
by

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

Goal state before:
pp: R : Type u_2
inst✝ : CommSemiring R
n : ℕ
f : R[X]
hn : f.natDegree < n
⊢ (trunc n) ↑f = f

Tactic:
by

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

Goal state before:
pp: R : Type u_2
inst✝ : Semiring R
φ : R⟦X⟧
hφ : φ ≠ 0
n : ℕ
ho : φ.order = ↑n
⊢ φ.order.toNat = n

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.LinearTopology

Goal state before:
pp: R : Type u_1
M : Type u_3
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : TopologicalSpace M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : IsCentralScalar R M
⊢ IsLinearTopology Rᵐᵒᵖ M ↔ IsLinearTopology R M

Tactic:
by

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

Goal state before:
pp: R : Type u_2
inst✝ : CommSemiring R
n m : ℕ
f : R⟦X⟧
h : n < m
⊢ (coeff n) ↑((trunc m) f) = (coeff n) f

Tactic:
by

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

Goal state before:
pp: R : Type u_2
inst✝ : CommSemiring R
n a b : ℕ
f g : R⟦X⟧
ha : n < a
hb : n < b
⊢ (coeff n) (f * g) = (coeff n) (↑((trunc a) f) * ↑((trunc b) g))

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.LinearTopology

Goal state before:
pp: R : Type u_1
inst✝³ : Ring R
inst✝² : TopologicalSpace R
inst✝¹ : IsLinearTopology R R
inst✝ : IsLinearTopology Rᵐᵒᵖ R
I : AddSubgroup R
x✝ : ↑I ∈ 𝓝 0 ∧ (∀ (r x : R), x ∈ I → r • x ∈ I) ∧ ∀ (r' : Rᵐᵒᵖ), ∀ x ∈ I, r' • x ∈ I
hI : ↑I ∈ 𝓝 0
hRI : ∀ (r x : R), x ∈ I → r • x ∈ I
hRI' : ∀ (r' : Rᵐᵒᵖ), ∀ x ∈ I, r' • x ∈ I
⊢ ↑(TwoSidedIdeal.mk' ↑I ⋯ ⋯ ⋯ ⋯ ⋯) ∈ 𝓝 0

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
n : ℕ
φ ψ : R⟦X⟧
⊢ (trunc n) (φ - ψ) = (trunc n) φ - (trunc n) ψ

Tactic:
by

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

Goal state before:
pp: R : Type u_2
inst✝ : Semiring R
φ : R⟦X⟧
hφ : φ ≠ 0
n : ℕ
ho : φ.order = ↑n
hn : φ.order.toNat = n
⊢ ¬X ^ (φ.order.toNat + 1) ∣ φ

Tactic:
rintro ⟨ψ, H⟩

Goal state after:
R : Type u_2
inst✝ : Semiring R
φ : R⟦X⟧
hφ : φ ≠ 0
n : ℕ
ho : φ.order = ↑n
hn : φ.order.toNat = n
ψ : R⟦X⟧
H : φ = X ^ (φ.order.toNat + 1) * ψ
⊢ False
Module: Mathlib.RingTheory.PowerSeries.Trunc

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
p : R⟦X⟧
n : ℕ
⊢ (trunc n) ((map f) p) = Polynomial.map f ((trunc n) p)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.LinearTopology

Goal state before:
pp: R : Type u_1
inst✝³ : Ring R
inst✝² : TopologicalSpace R
inst✝¹ : IsLinearTopology R R
inst✝ : IsLinearTopology Rᵐᵒᵖ R
I : AddSubgroup R
x✝ : ↑I ∈ 𝓝 0 ∧ (∀ (r x : R), x ∈ I → r • x ∈ I) ∧ ∀ (r' : Rᵐᵒᵖ), ∀ x ∈ I, r' • x ∈ I
hI : ↑I ∈ 𝓝 0
hRI : ∀ (r x : R), x ∈ I → r • x ∈ I
hRI' : ∀ (r' : Rᵐᵒᵖ), ∀ x ∈ I, r' • x ∈ I
⊢ ↑(TwoSidedIdeal.mk' ↑I ⋯ ⋯ ⋯ ⋯ ⋯) ⊆ ↑I

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.LinearTopology

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : TopologicalSpace R
inst✝ : IsLinearTopology R R
⊢ IsLinearTopology Rᵐᵒᵖ R

Tactic:
by

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⟧
u : Filter ι
g : R⟦X⟧
⊢ Tendsto f u (𝓝 g) ↔ ∀ (d : ℕ), Tendsto (fun i ↦ (coeff d) (f i)) u (𝓝 ((coeff d) g))

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝¹ : TopologicalSpace R
inst✝ : CommSemiring R
f : R⟦X⟧
d n : ℕ
hdn : d < n
⊢ (coeff d) ↑((trunc n) f) = (coeff d) f

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝¹ : TopologicalSpace R
inst✝ : CommSemiring R
f : R⟦X⟧
⊢ Tendsto (fun d ↦ ↑((trunc d) f)) atTop (𝓝 f)

Tactic:
by

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⟧
g : R⟦X⟧
⊢ HasSum f g ↔ ∀ (d : ℕ), HasSum (fun i ↦ (coeff d) (f i)) ((coeff d) g)

Tactic:
by

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⟧
a : ℕ → R
h : ∀ (d : ℕ), HasSum (fun i ↦ (coeff d) (f i)) (a d)
⊢ ∀ (d : ℕ), HasSum (fun i ↦ (coeff d) (f i)) ((coeff d) (mk a))

Tactic:
by

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⟧
⊢ Summable f ↔ ∀ (d : ℕ), Summable fun i ↦ (coeff d) (f i)

Tactic:
by

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

Goal state before:
pp: R : Type u_2
inst✝ : Semiring R
φ : R⟦X⟧
⊢ φ.order = emultiplicity X φ

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
inst✝ : Nontrivial R
⊢ order 1 = 0

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
inst✝ : Nontrivial R
f : R⟦X⟧
⊢ IsUnit f → f.order = 0

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
inst✝ : Nontrivial R
⊢ X.order = 1

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
inst✝ : Nontrivial R
n : ℕ
⊢ (X ^ n).order = ↑n

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
inst✝ : Nontrivial R
⊢ X.divXPowOrder = 1

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
inst✝ : Nontrivial R
⊢ divXPowOrder 1 = 1

Tactic:
by

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 ι
hempty : Nonempty ι
n : ℕ
h : ∀ (n : ℕ), ∃ a, ∀ (b : ι), a ≤ b → ↑n < (f b).order
i : ι
hi : ∀ (b : ι), i ≤ b → ↑n < (f b).order
k : ι
hk : i < k
⊢ ↑n < (f k).order

Tactic:
by

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

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

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
φ ψ : R⟦X⟧
h : φ ≠ 0 ∧ ψ ≠ 0
⊢ (φ.order.toNat, ψ.order.toNat) ∈ antidiagonal (φ.order.toNat + ψ.order.toNat)

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝³ : TopologicalSpace R
inst✝² : CommSemiring R
ι : Type u_2
inst✝¹ : LinearOrder ι
inst✝ : LocallyFiniteOrderBot ι
f : ι → R⟦X⟧
hempty : Nonempty ι
n : ℕ
h : ∀ (n : ℕ), ∃ a, ∀ (b : ι), a ≤ b → ↑n < (f b).order
i : ι
hi : ∀ (b : ι), i ≤ b → ↑n < (f b).order
this : ∀ (s : Finset ι), (coeff n) (∏ i ∈ s, f i) ≠ 0 → ↑s ⊆ Set.Iio i
⊢ (support fun i ↦ (coeff n) (∏ i ∈ i, f i)) ⊆ ↑(Finset.Iio i).powerset

Tactic:
by

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

Goal state before:
pp: σ : Type u_1
S : Type u_3
inst✝³ : CommRing S
inst✝² : TopologicalSpace S
inst✝¹ : ContinuousAdd S
inst✝ : IsLinearTopology S S
a b : σ → S
ha : HasEval a
hb : HasEval b
⊢ Tendsto (a + b) cofinite (𝓝 0)

Tactic:
by

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

Goal state before:
pp: σ : Type u_1
S : Type u_3
inst✝³ : CommRing S
inst✝² : TopologicalSpace S
inst✝¹ : IsTopologicalRing S
inst✝ : IsLinearTopology S S
a : σ → S
⊢ a ∈ hasEvalIdeal ↔ HasEval a

Tactic:
by

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}
s : σ
⊢ {n | a s ^ n.succ ∈ I}.Nonempty

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
φ ψ : R⟦X⟧
h✝ : φ ≠ 0 ∧ ψ ≠ 0
ij : ℕ × ℕ
hij : ij ∈ antidiagonal (φ.order.toNat + ψ.order.toNat)
h : ij ≠ (φ.order.toNat, ψ.order.toNat)
h' : ij.1 = φ.order.toNat ∧ ij.2 = ψ.order.toNat
⊢ ij = (φ.order.toNat, ψ.order.toNat)

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝³ : TopologicalSpace R
inst✝² : CommSemiring R
ι : Type u_2
inst✝¹ : LinearOrder ι
inst✝ : LocallyFiniteOrderBot ι
f : ι → R⟦X⟧
hempty : Nonempty ι
n : ℕ
h : ∀ (n : ℕ), ∃ a, ∀ (b : ι), a ≤ b → ↑n < (f b).order
i : ι
hi : ∀ (b : ι), i ≤ b → ↑n < (f b).order
s : Finset ι
hs : ¬↑s ⊆ Set.Iio i
x : ι
hxs : x ∈ ↑s
hxi : i ≤ x
⊢ ∀ i ∈ s, 0 ≤ (f i).order

Tactic:
by

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

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

Tactic:
by

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
⊢ (Function.support n).Finite

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
φ ψ : R⟦X⟧
⊢ (φ * ψ).order = φ.order + ψ.order

Tactic:
by

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

Goal state before:
pp: R : Type u_2
inst✝¹ : CommRing R
inst✝ : TopologicalSpace R
⊢ Multipliable fun n ↦ 1 - X ^ (n + 1)

Tactic:
by

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

Goal state before:
pp: R : Type u_2
inst✝³ : CommRing R
inst✝² : TopologicalSpace R
inst✝¹ : T2Space R
inst✝ : Nontrivial R
h : ∏' (i : ℕ), (1 - X ^ (i + 1)) = 0
⊢ False

Tactic:
obtain h := PowerSeries.ext_iff.mp h 0

Goal state after:
R : Type u_2
inst✝³ : CommRing R
inst✝² : TopologicalSpace R
inst✝¹ : T2Space R
inst✝ : Nontrivial R
h✝ : ∏' (i : ℕ), (1 - X ^ (i + 1)) = 0
h : (coeff 0) (∏' (i : ℕ), (1 - X ^ (i + 1))) = (coeff 0) 0
⊢ False
Module: Mathlib.RingTheory.PowerSeries.PiTopology

Goal state before:
pp: R : Type u_2
inst✝³ : CommRing R
inst✝² : TopologicalSpace R
inst✝¹ : T2Space R
inst✝ : Nontrivial R
⊢ ∏' (i : ℕ), (1 - X ^ (i + 1)) ≠ 0

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
f g : R⟦X⟧
h : f ≠ 0 ∧ g ≠ 0
⊢ X ^ (f.order.toNat + g.order.toNat) * (f * g).divXPowOrder = X ^ (f * g).order.toNat * (f * g).divXPowOrder

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
inst✝ : TopologicalSpace R
f : R⟦X⟧
⊢ HasSum (fun d ↦ (monomial d) ((coeff d) f)) f

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
f g : R⟦X⟧
h : f ≠ 0 ∧ g ≠ 0
⊢ X ^ (f * g).order.toNat * (f * g).divXPowOrder = f * g

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
f g : R⟦X⟧
h : f ≠ 0 ∧ g ≠ 0
⊢ f * g = X ^ f.order.toNat * f.divXPowOrder * (X ^ g.order.toNat * g.divXPowOrder)

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
f g : R⟦X⟧
h : f ≠ 0 ∧ g ≠ 0
⊢ X ^ f.order.toNat * f.divXPowOrder * (X ^ g.order.toNat * g.divXPowOrder) =
    f.divXPowOrder * g.divXPowOrder * X ^ (g.order.toNat + f.order.toNat)

Tactic:
by

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

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

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
f g : R⟦X⟧
h : f ≠ 0 ∧ g ≠ 0
⊢ f.divXPowOrder * g.divXPowOrder * X ^ (g.order.toNat + f.order.toNat) =
    X ^ (f.order.toNat + g.order.toNat) * (f.divXPowOrder * g.divXPowOrder)

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
f g : R⟦X⟧
⊢ (f * g).divXPowOrder = f.divXPowOrder * g.divXPowOrder

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
p : R⟦X⟧
T : Subring R
hp : ∀ (n : ℕ), (coeff n) p ∈ T
d : ℕ
hd : ↑d < (p.toSubring T hp).order
⊢ (coeff d) p = 0

Tactic:
by

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

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : Ring R
Jd : TwoSidedIdeal R × (σ →₀ ℕ)
⊢ 0 ∈ {f | ∀ e ≤ Jd.2, (coeff e) f ∈ Jd.1}

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
p : R⟦X⟧
T : Subring R
hp : ∀ (n : ℕ), (coeff n) p ∈ T
d : ℕ
hd : ↑d < p.order
⊢ (coeff d) (p.toSubring T hp) = 0

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
p : R⟦X⟧
T : Subring R
hp : ∀ (n : ℕ), (coeff n) p ∈ T
⊢ (p.toSubring T hp).order = p.order

Tactic:
by

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

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : Ring R
Jd : TwoSidedIdeal R × (σ →₀ ℕ)
x✝ y✝ : MvPowerSeries σ R
hf : x✝ ∈ {f | ∀ e ≤ Jd.2, (coeff e) f ∈ Jd.1}
hg : y✝ ∈ {f | ∀ e ≤ Jd.2, (coeff e) f ∈ Jd.1}
e : σ →₀ ℕ
he : e ≤ Jd.2
⊢ (coeff e) (x✝ + y✝) ∈ Jd.1

Tactic:
by

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

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : Ring R
Jd : TwoSidedIdeal R × (σ →₀ ℕ)
f : MvPowerSeries σ R
hf : f ∈ {f | ∀ e ≤ Jd.2, (coeff e) f ∈ Jd.1}
e : σ →₀ ℕ
he : e ≤ Jd.2
⊢ (coeff e) (-f) ∈ Jd.1

Tactic:
by

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

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : Ring R
Jd : TwoSidedIdeal R × (σ →₀ ℕ)
f g : MvPowerSeries σ R
hg : g ∈ {f | ∀ e ≤ Jd.2, (coeff e) f ∈ Jd.1}
e : σ →₀ ℕ
he : e ≤ Jd.2
⊢ (coeff e) (f * g) ∈ Jd.1

Tactic:
by

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

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : Ring R
Jd : TwoSidedIdeal R × (σ →₀ ℕ)
f g : MvPowerSeries σ R
hf : f ∈ {f | ∀ e ≤ Jd.2, (coeff e) f ∈ Jd.1}
e : σ →₀ ℕ
he : e ≤ Jd.2
⊢ (coeff e) (f * g) ∈ Jd.1

Tactic:
by

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

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : Ring R
f : MvPowerSeries σ R
Jd : TwoSidedIdeal R × (σ →₀ ℕ)
⊢ f ∈ basis σ R Jd ↔ ∀ e ≤ Jd.2, (coeff e) f ∈ Jd.1

Tactic:
by

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

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : Ring R
J K : TwoSidedIdeal R
d e : σ →₀ ℕ
hK : K ≠ ⊤
h : ∀ (a : MvPowerSeries σ R), (∀ e ≤ d, (coeff e) a ∈ J) → ∀ e_1 ≤ e, (coeff e_1) a ∈ K
x : R
hx : x ∈ ↑J
d' : σ →₀ ℕ
⊢ (coeff d') (C x) ∈ J

Tactic:
by

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

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : Ring R
J K : TwoSidedIdeal R
d e : σ →₀ ℕ
hK : K ≠ ⊤
h : ∀ (a : MvPowerSeries σ R), (∀ e ≤ d, (coeff e) a ∈ J) → ∀ e_1 ≤ e, (coeff e_1) a ∈ K
h' : ¬e ≤ d
x : R
a✝ : x ∈ ⊤
d' : σ →₀ ℕ
hd'_le : d' ≤ d
⊢ (coeff d') ((monomial e) x) ∈ J

Tactic:
by

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

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : Ring R
J K : TwoSidedIdeal R
d e : σ →₀ ℕ
hK : K ≠ ⊤
⊢ basis σ R (J, d) ≤ basis σ R (K, e) ↔ J ≤ K ∧ e ≤ d

Tactic:
by

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
⊢ UniformContinuous ⇑(eval₂Hom φ a)

Tactic:
by

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
f : MvPolynomial σ R
⊢ eval₂ φ a ↑f = MvPolynomial.eval₂ φ a f

Tactic:
by

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
r : R
⊢ eval₂ φ a (C r) = φ r

Tactic:
by

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

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝³ : Ring R
inst✝² : TopologicalSpace R
inst✝¹ : IsLinearTopology R R
inst✝ : IsLinearTopology Rᵐᵒᵖ R
⊢ (𝓝 0).HasBasis (fun Id ↦ ↑Id.1 ∈ 𝓝 0) fun Id ↦ ↑(basis σ R Id)

Tactic:
by

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
s : σ
⊢ eval₂ φ a (X s) = a s

Tactic:
by

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

Goal state before:
pp: S : Type u_2
inst✝¹ : CommRing S
inst✝ : TopologicalSpace S
a : S
ha : HasEval a
⊢ Filter.Tendsto (fun x ↦ a) Filter.cofinite (nhds 0)

Tactic:
by

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

Goal state before:
pp: S : Type u_3
inst✝ : CommRing S
a : S
t u : TopologicalSpace S
h : t ≤ u
ha : HasEval a
⊢ HasEval a

Tactic:
by

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

Goal state before:
pp: S : Type u_2
inst✝¹ : CommRing S
inst✝ : TopologicalSpace S
⊢ HasEval 0

Tactic:
by

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

Goal state before:
pp: S : Type u_2
inst✝³ : CommRing S
inst✝² : TopologicalSpace S
inst✝¹ : ContinuousAdd S
inst✝ : IsLinearTopology S S
a b : S
ha : HasEval a
hb : HasEval b
⊢ HasEval (a + b)

Tactic:
by

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

Goal state before:
pp: S : Type u_2
inst✝² : CommRing S
inst✝¹ : TopologicalSpace S
inst✝ : IsLinearTopology S S
c x : S
hx : HasEval x
⊢ HasEval (c * x)

Tactic:
by

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

Goal state before:
pp: S : Type u_2
inst✝² : CommRing S
inst✝¹ : TopologicalSpace S
inst✝ : IsLinearTopology S S
c x : S
hx : HasEval x
⊢ HasEval (x * c)

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
S : Type u_2
inst✝² : CommRing S
φ : R →+* S
inst✝¹ : TopologicalSpace R
inst✝ : TopologicalSpace S
hφ : Continuous ⇑φ
a : R
ha : HasEval a
⊢ HasEval (φ a)

Tactic:
by

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

Goal state before:
pp: σ : Type u_1
R : Type u_3
inst✝² : CommRing R
inst✝¹ : TopologicalSpace R
inst✝ : IsLinearTopology R R
f : MvPowerSeries σ R
hf : IsTopologicallyNilpotent (constantCoeff f)
⊢ IsTopologicallyNilpotent f

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : TopologicalSpace R
⊢ HasEval X

Tactic:
by

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

Goal state before:
pp: S : Type u_2
inst✝³ : CommRing S
inst✝² : TopologicalSpace S
inst✝¹ : IsTopologicalRing S
inst✝ : IsLinearTopology S S
a : S
⊢ a ∈ hasEvalIdeal ↔ HasEval a

Tactic:
by

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

Goal state before:
pp: σ : Type u_1
R : Type u_3
inst✝² : CommRing R
inst✝¹ : TopologicalSpace R
inst✝ : IsLinearTopology R R
f : MvPowerSeries σ R
⊢ Tendsto (fun n ↦ f ^ n) atTop (𝓝 0) ↔ IsTopologicallyNilpotent (constantCoeff f)

Tactic:
by

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✝⁶ : IsTopologicalSemiring R
inst✝⁵ : IsUniformAddGroup R
inst✝⁴ : IsUniformAddGroup S
inst✝³ : CompleteSpace S
inst✝² : T2Space S
inst✝¹ : IsTopologicalRing S
inst✝ : IsLinearTopology S S
hφ : Continuous[inst✝⁹.toTopologicalSpace, inst✝⁷.toTopologicalSpace] ⇑φ
ha : HasEval a
⊢ ⇑(eval₂Hom hφ ha) = eval₂ φ a

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
S : Type u_2
inst✝² : CommRing S
φ : R →+* S
a : S
inst✝¹ : UniformSpace R
inst✝ : UniformSpace S
f : Polynomial R
⊢ eval₂ φ a ↑f = Polynomial.eval₂ φ a f

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
S : Type u_2
inst✝² : CommRing S
φ : R →+* S
a : S
inst✝¹ : UniformSpace R
inst✝ : UniformSpace S
r : R
⊢ eval₂ φ a (C r) = φ r

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
S : Type u_2
inst✝² : CommRing S
φ : R →+* S
a : S
inst✝¹ : UniformSpace R
inst✝ : UniformSpace S
⊢ eval₂ φ a X = a

Tactic:
by

Goal state after: