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

Goal state before:
pp: case inl
R : Type u_2
inst✝ : Semiring R
⊢ order 0 = emultiplicity X 0

pp: case inr
R : Type u_2
inst✝ : Semiring R
φ : R⟦X⟧
hφ : φ ≠ 0
⊢ φ.order = emultiplicity X φ

Tactic:
·

Goal state after:
case inl
R : Type u_2
inst✝ : Semiring R
⊢ order 0 = emultiplicity X 0
Module: Mathlib.RingTheory.PowerSeries.Order

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

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

Tactic:
·

Goal state after:
case inr.coe
R : Type u_2
inst✝ : Semiring R
φ : R⟦X⟧
hφ : φ ≠ 0
n : ℕ
ho : φ.order = ↑n
hn : φ.order.toNat = n
⊢ ↑φ.order.toNat ≤ emultiplicity X φ
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
⊢ emultiplicity X φ ≤ ↑φ.order.toNat

Tactic:
·

Goal state after:
R : Type u_2
inst✝ : Semiring R
φ : R⟦X⟧
hφ : φ ≠ 0
n : ℕ
ho : φ.order = ↑n
hn : φ.order.toNat = n
⊢ emultiplicity X φ ≤ ↑φ.order.toNat
Module: Mathlib.RingTheory.PowerSeries.PiTopology

Goal state before:
pp: case e_f
R : Type u_1
inst✝¹ : TopologicalSpace R
inst✝ : Semiring R
ι : Type u_2
f : ι → R⟦X⟧
u : Filter ι
g : R⟦X⟧
d : Unit →₀ ℕ
⊢ (fun i ↦ (MvPowerSeries.coeff d) (f i)) = fun i ↦ (MvPowerSeries.coeff (Finsupp.single () (d ()))) (f i)

pp: case e_l₂
R : Type u_1
inst✝¹ : TopologicalSpace R
inst✝ : Semiring R
ι : Type u_2
f : ι → R⟦X⟧
u : Filter ι
g : R⟦X⟧
d : Unit →₀ ℕ
⊢ d = Finsupp.single () (d ())

Tactic:
·

Goal state after:
case e_f
R : Type u_1
inst✝¹ : TopologicalSpace R
inst✝ : Semiring R
ι : Type u_2
f : ι → R⟦X⟧
u : Filter ι
g : R⟦X⟧
d : Unit →₀ ℕ
⊢ (fun i ↦ (MvPowerSeries.coeff d) (f i)) = fun i ↦ (MvPowerSeries.coeff (Finsupp.single () (d ()))) (f i)
Module: Mathlib.RingTheory.PowerSeries.PiTopology

Goal state before:
pp: case e_l₂
R : Type u_1
inst✝¹ : TopologicalSpace R
inst✝ : Semiring R
ι : Type u_2
f : ι → R⟦X⟧
u : Filter ι
g : R⟦X⟧
d : Unit →₀ ℕ
⊢ d = Finsupp.single () (d ())

Tactic:
·

Goal state after:
case e_l₂
R : Type u_1
inst✝¹ : TopologicalSpace R
inst✝ : Semiring R
ι : Type u_2
f : ι → R⟦X⟧
u : Filter ι
g : R⟦X⟧
d : Unit →₀ ℕ
⊢ d = Finsupp.single () (d ())
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
ψ : R⟦X⟧
H : φ = X ^ (φ.order.toNat + 1) * ψ
this : (coeff φ.order.toNat) φ = 0
⊢ False

pp: 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) * ψ
this : (coeff n) φ = (coeff n) (ψ * X ^ (φ.order.toNat + 1))
⊢ ↑n < (X ^ (φ.order.toNat + 1)).order

Tactic:
·

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) * ψ
this : (coeff φ.order.toNat) φ = 0
⊢ False
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
ψ : R⟦X⟧
H : φ = X ^ (φ.order.toNat + 1) * ψ
this : (coeff n) φ = (coeff n) (ψ * X ^ (φ.order.toNat + 1))
⊢ ↑n < (X ^ (φ.order.toNat + 1)).order

Tactic:
·

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) * ψ
this : (coeff n) φ = (coeff n) (ψ * X ^ (φ.order.toNat + 1))
⊢ ↑n < (X ^ (φ.order.toNat + 1)).order
Module: Mathlib.RingTheory.PowerSeries.PiTopology

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

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:
·

Goal state after:
case mp
R : Type u_1
inst✝¹ : TopologicalSpace R
inst✝ : Semiring R
ι : Type u_2
f : ι → R⟦X⟧
⊢ (∃ a, ∀ (d : ℕ), HasSum (fun i ↦ (coeff d) (f i)) ((coeff d) a)) → ∀ (d : ℕ), ∃ a, HasSum (fun i ↦ (coeff d) (f i)) a
Module: Mathlib.RingTheory.PowerSeries.Order

Goal state before:
pp: case pos
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) * ψ
this : (coeff n) φ = (coeff n) (ψ * X ^ (φ.order.toNat + 1))
h✝ : 1 = 0
⊢ ↑n < ⊤

pp: case neg
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) * ψ
this : (coeff n) φ = (coeff n) (ψ * X ^ (φ.order.toNat + 1))
h✝ : ¬1 = 0
⊢ ↑n < ↑(φ.order.toNat + 1)

Tactic:
·

Goal state after:
case pos
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) * ψ
this : (coeff n) φ = (coeff n) (ψ * X ^ (φ.order.toNat + 1))
h✝ : 1 = 0
⊢ ↑n < ⊤
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:
·

Goal state after:
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)
Module: Mathlib.RingTheory.PowerSeries.Order

Goal state before:
pp: case neg
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) * ψ
this : (coeff n) φ = (coeff n) (ψ * X ^ (φ.order.toNat + 1))
h✝ : ¬1 = 0
⊢ ↑n < ↑(φ.order.toNat + 1)

Tactic:
·

Goal state after:
case neg
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) * ψ
this : (coeff n) φ = (coeff n) (ψ * X ^ (φ.order.toNat + 1))
h✝ : ¬1 = 0
⊢ ↑n < ↑(φ.order.toNat + 1)
Module: Mathlib.RingTheory.PowerSeries.PiTopology

Goal state before:
pp: case inl
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 (𝓝 ⊤)
hempty : IsEmpty ι
⊢ Summable f

pp: case inr
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 (𝓝 ⊤)
hempty : Nonempty ι
⊢ Summable f

Tactic:
·

Goal state after:
case inl
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 (𝓝 ⊤)
hempty : IsEmpty ι
⊢ Summable f
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:
apply le_antisymm _ (le_order_mul _ _)

Goal state after:
R : Type u_1
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
φ ψ : R⟦X⟧
⊢ (φ * ψ).order ≤ φ.order + ψ.order
Module: Mathlib.RingTheory.PowerSeries.Order

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

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

Tactic:
·

Goal state after:
case pos
R : Type u_1
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
φ ψ : R⟦X⟧
h : φ = 0 ∨ ψ = 0
⊢ (φ * ψ).order ≤ φ.order + ψ.order
Module: Mathlib.RingTheory.PowerSeries.Order

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

Tactic:
·

Goal state after:
case neg
R : Type u_1
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
φ ψ : R⟦X⟧
h : φ ≠ 0 ∧ ψ ≠ 0
⊢ (φ * ψ).order ≤ φ.order + ψ.order
Module: Mathlib.RingTheory.PowerSeries.PiTopology

Goal state before:
pp: case inl
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 (𝓝 ⊤)
hempty : IsEmpty ι
⊢ Summable fun x ↦ ∏ i ∈ x, f i

pp: case inr
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 (𝓝 ⊤)
hempty : Nonempty ι
⊢ Summable fun x ↦ ∏ i ∈ x, f i

Tactic:
·

Goal state after:
case inl
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 (𝓝 ⊤)
hempty : IsEmpty ι
⊢ Summable fun x ↦ ∏ i ∈ x, f i
Module: Mathlib.RingTheory.PowerSeries.Order

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

pp: case neg
R : Type u_1
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
φ ψ : R⟦X⟧
h : φ ≠ 0 ∧ ψ ≠ 0
⊢ ∀ b ∈ antidiagonal (φ.order.toNat + ψ.order.toNat),
    b ≠ (φ.order.toNat, ψ.order.toNat) → (coeff b.1) φ * (coeff b.2) ψ = 0

Tactic:
·

Goal state after:
case neg
R : Type u_1
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
φ ψ : R⟦X⟧
h : φ ≠ 0 ∧ ψ ≠ 0
⊢ (coeff (φ.order.toNat, ψ.order.toNat).1) φ * (coeff (φ.order.toNat, ψ.order.toNat).2) ψ ≠ 0
Module: Mathlib.RingTheory.PowerSeries.Order

Goal state before:
pp: case neg
R : Type u_1
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
φ ψ : R⟦X⟧
h : φ ≠ 0 ∧ ψ ≠ 0
⊢ ∀ b ∈ antidiagonal (φ.order.toNat + ψ.order.toNat),
    b ≠ (φ.order.toNat, ψ.order.toNat) → (coeff b.1) φ * (coeff b.2) ψ = 0

Tactic:
·

Goal state after:
case neg
R : Type u_1
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
φ ψ : R⟦X⟧
h : φ ≠ 0 ∧ ψ ≠ 0
⊢ ∀ b ∈ antidiagonal (φ.order.toNat + ψ.order.toNat),
    b ≠ (φ.order.toNat, ψ.order.toNat) → (coeff b.1) φ * (coeff b.2) ψ = 0
Module: Mathlib.RingTheory.PowerSeries.Order

Goal state before:
pp: case neg.inl
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
⊢ (coeff ij.1) φ * (coeff ij.2) ψ = 0

pp: case neg.inr.inl
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
⊢ (coeff ij.1) φ * (coeff ij.2) ψ = 0

pp: case neg.inr.inr
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.2 < ψ.order.toNat
⊢ (coeff ij.1) φ * (coeff ij.2) ψ = 0

Tactic:
·

Goal state after:
case neg.inl
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
⊢ (coeff ij.1) φ * (coeff ij.2) ψ = 0
Module: Mathlib.RingTheory.PowerSeries.Order

Goal state before:
pp: case neg.inr.inl
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
⊢ (coeff ij.1) φ * (coeff ij.2) ψ = 0

pp: case neg.inr.inr
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.2 < ψ.order.toNat
⊢ (coeff ij.1) φ * (coeff ij.2) ψ = 0

Tactic:
·

Goal state after:
case neg.inr.inl
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
⊢ (coeff ij.1) φ * (coeff ij.2) ψ = 0
Module: Mathlib.RingTheory.PowerSeries.Order

Goal state before:
pp: case neg.inr.inr
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.2 < ψ.order.toNat
⊢ (coeff ij.1) φ * (coeff ij.2) ψ = 0

Tactic:
·

Goal state after:
case neg.inr.inr
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.2 < ψ.order.toNat
⊢ (coeff ij.1) φ * (coeff ij.2) ψ = 0
Module: Mathlib.RingTheory.PowerSeries.Order

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

pp: case neg
R : Type u_1
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
f g : R⟦X⟧
h : f ≠ 0 ∧ g ≠ 0
⊢ (f * g).divXPowOrder = f.divXPowOrder * g.divXPowOrder

Tactic:
·

Goal state after:
case pos
R : Type u_1
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
f g : R⟦X⟧
h : f = 0 ∨ g = 0
⊢ (f * g).divXPowOrder = f.divXPowOrder * g.divXPowOrder
Module: Mathlib.RingTheory.PowerSeries.Order

Goal state before:
pp: case refine_1
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

pp: case refine_2
R : Type u_1
inst✝ : Ring R
p : R⟦X⟧
T : Subring R
hp : ∀ (n : ℕ), (coeff n) p ∈ T
⊢ p.order ≤ (p.toSubring T hp).order

Tactic:
·

Goal state after:
case refine_1
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
Module: Mathlib.RingTheory.PowerSeries.Order

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

Tactic:
·

Goal state after:
case refine_2
R : Type u_1
inst✝ : Ring R
p : R⟦X⟧
T : Subring R
hp : ∀ (n : ℕ), (coeff n) p ∈ T
⊢ p.order ≤ (p.toSubring T hp).order
Module: Mathlib.RingTheory.MvPowerSeries.LinearTopology

Goal state before:
pp: case mp
σ : 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

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

Tactic:
·

Goal state after:
case mp
σ : 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
Module: Mathlib.RingTheory.MvPowerSeries.LinearTopology

Goal state before:
pp: case mp.left
σ : 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
⊢ ↑J ⊆ ↑K

pp: case mp.right
σ : 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
⊢ e ≤ d

Tactic:
·

Goal state after:
case mp.left
σ : 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
⊢ ↑J ⊆ ↑K
Module: Mathlib.RingTheory.MvPowerSeries.Evaluation

Goal state before:
pp: case pos
σ : 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
this : ∀ᶠ (x : MvPolynomial σ R) in 𝓝 0, ∀ i ∈ D, φ (MvPolynomial.coeff i x) ∈ I
p : MvPolynomial σ R
hp : ∀ i ∈ D, φ (MvPolynomial.coeff i p) ∈ I
d : σ →₀ ℕ
a✝ : d ∈ p.support
hd : d ∈ D
⊢ φ (MvPolynomial.coeff d p) * ∏ i ∈ d.support, a i ^ d i ∈ I

pp: case neg
σ : 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
this : ∀ᶠ (x : MvPolynomial σ R) in 𝓝 0, ∀ i ∈ D, φ (MvPolynomial.coeff i x) ∈ I
p : MvPolynomial σ R
hp : ∀ i ∈ D, φ (MvPolynomial.coeff i p) ∈ I
d : σ →₀ ℕ
a✝ : d ∈ p.support
hd : d ∉ D
⊢ φ (MvPolynomial.coeff d p) * ∏ i ∈ d.support, a i ^ d i ∈ I

Tactic:
·

Goal state after:
case pos
σ : 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
this : ∀ᶠ (x : MvPolynomial σ R) in 𝓝 0, ∀ i ∈ D, φ (MvPolynomial.coeff i x) ∈ I
p : MvPolynomial σ R
hp : ∀ i ∈ D, φ (MvPolynomial.coeff i p) ∈ I
d : σ →₀ ℕ
a✝ : d ∈ p.support
hd : d ∈ D
⊢ φ (MvPolynomial.coeff d p) * ∏ i ∈ d.support, a i ^ d i ∈ I
Module: Mathlib.RingTheory.MvPowerSeries.Evaluation

Goal state before:
pp: case neg
σ : 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
this : ∀ᶠ (x : MvPolynomial σ R) in 𝓝 0, ∀ i ∈ D, φ (MvPolynomial.coeff i x) ∈ I
p : MvPolynomial σ R
hp : ∀ i ∈ D, φ (MvPolynomial.coeff i p) ∈ I
d : σ →₀ ℕ
a✝ : d ∈ p.support
hd : d ∉ D
⊢ φ (MvPolynomial.coeff d p) * ∏ i ∈ d.support, a i ^ d i ∈ I

Tactic:
·

Goal state after:
case neg
σ : 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
this : ∀ᶠ (x : MvPolynomial σ R) in 𝓝 0, ∀ i ∈ D, φ (MvPolynomial.coeff i x) ∈ I
p : MvPolynomial σ R
hp : ∀ i ∈ D, φ (MvPolynomial.coeff i p) ∈ I
d : σ →₀ ℕ
a✝ : d ∈ p.support
hd : d ∉ D
⊢ φ (MvPolynomial.coeff d p) * ∏ i ∈ d.support, a i ^ d i ∈ I
Module: Mathlib.RingTheory.MvPowerSeries.LinearTopology

Goal state before:
pp: case mp.right
σ : 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
⊢ e ≤ d

Tactic:
·

Goal state after:
case mp.right
σ : 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
⊢ e ≤ d
Module: Mathlib.RingTheory.MvPowerSeries.LinearTopology

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

Tactic:
·

Goal state after:
case mpr
σ : Type u_1
R : Type u_2
inst✝ : Ring R
J K : TwoSidedIdeal R
d e : σ →₀ ℕ
hK : K ≠ ⊤
⊢ J ≤ K ∧ e ≤ d → basis σ R (J, d) ≤ basis σ R (K, e)
Module: Mathlib.RingTheory.MvPowerSeries.LinearTopology

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

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

Tactic:
·

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

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

Tactic:
·

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