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

Goal state before:
pp: case neg
σ : 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 : σ →₀ ℕ
hd : ¬(weight w) d = p + q
⊢ 0 = (coeff d) ((weightedHomogeneousComponent w p) f * (weightedHomogeneousComponent w q) g)

Tactic:
· symm
    apply IsWeightedHomogeneous.coeff_eq_zero _ hd
    exact IsWeightedHomogeneous.mul
      (isWeightedHomogeneous_weightedHomogeneousComponent w f p)
      (isWeightedHomogeneous_weightedHomogeneousComponent w g q)

Goal state after:
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:
·

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

Goal state before:
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:
·

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

Goal state before:
pp: case pos
σ : Type u_1
R : Type u_2
inst✝¹ : TopologicalSpace R
inst✝ : Semiring R
d : σ →₀ ℕ
h : ∃ i, d = Finsupp.single i 1
⊢ ∀ᶠ (x' : σ) in cofinite, (if d = Finsupp.single x' 1 then 1 else 0) = 0

pp: case neg
σ : Type u_1
R : Type u_2
inst✝¹ : TopologicalSpace R
inst✝ : Semiring R
d : σ →₀ ℕ
h : ∀ (i : σ), d ≠ Finsupp.single i 1
⊢ ∀ᶠ (x' : σ) in cofinite, (if d = Finsupp.single x' 1 then 1 else 0) = 0

Tactic:
·

Goal state after:
case pos
σ : Type u_1
R : Type u_2
inst✝¹ : TopologicalSpace R
inst✝ : Semiring R
d : σ →₀ ℕ
h : ∃ i, d = Finsupp.single i 1
⊢ ∀ᶠ (x' : σ) in cofinite, (if d = Finsupp.single x' 1 then 1 else 0) = 0
Module: Mathlib.RingTheory.MvPowerSeries.PiTopology

Goal state before:
pp: case neg
σ : Type u_1
R : Type u_2
inst✝¹ : TopologicalSpace R
inst✝ : Semiring R
d : σ →₀ ℕ
h : ∀ (i : σ), d ≠ Finsupp.single i 1
⊢ ∀ᶠ (x' : σ) in cofinite, (if d = Finsupp.single x' 1 then 1 else 0) = 0

Tactic:
·

Goal state after:
case neg
σ : Type u_1
R : Type u_2
inst✝¹ : TopologicalSpace R
inst✝ : Semiring R
d : σ →₀ ℕ
h : ∀ (i : σ), d ≠ Finsupp.single i 1
⊢ ∀ᶠ (x' : σ) in cofinite, (if d = Finsupp.single x' 1 then 1 else 0) = 0
Module: Mathlib.Topology.Algebra.LinearTopology

Goal state before:
pp: R : Type u_1
R' : Type u_2
M : Type u_3
inst✝⁸ : Ring R
inst✝⁷ : Ring R'
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : Module R' M
inst✝³ : SMulCommClass R R' M
inst✝² : TopologicalSpace M
inst✝¹ : IsLinearTopology R M
inst✝ : IsLinearTopology R' M
I : Submodule R M
hI : ↑I ∈ 𝓝 0
J : Submodule R' M
hJ : ↑J ∈ 𝓝 0
J_sub_I : ↑J ⊆ ↑I
uR : Set R := univ
uR' : Set R' := univ
hRR : uR * uR ⊆ uR
⊢ ∃ i', (↑i' ∈ 𝓝 0 ∧ (∀ (r : R), ∀ x ∈ i', r • x ∈ i') ∧ ∀ (r' : R'), ∀ x ∈ i', r' • x ∈ i') ∧ ↑i' ⊆ ↑I

Tactic:
have hRI : uR • (I : Set M) ⊆ I := smul_subset_iff.mpr fun x _ i hi ↦ I.smul_mem x hi

Goal state after:
R : Type u_1
R' : Type u_2
M : Type u_3
inst✝⁸ : Ring R
inst✝⁷ : Ring R'
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : Module R' M
inst✝³ : SMulCommClass R R' M
inst✝² : TopologicalSpace M
inst✝¹ : IsLinearTopology R M
inst✝ : IsLinearTopology R' M
I : Submodule R M
hI : ↑I ∈ 𝓝 0
J : Submodule R' M
hJ : ↑J ∈ 𝓝 0
J_sub_I : ↑J ⊆ ↑I
uR : Set R := univ
uR' : Set R' := univ
hRR : uR * uR ⊆ uR
hRI : uR • ↑I ⊆ ↑I
⊢ ∃ i', (↑i' ∈ 𝓝 0 ∧ (∀ (r : R), ∀ x ∈ i', r • x ∈ i') ∧ ∀ (r' : R'), ∀ x ∈ i', r' • x ∈ i') ∧ ↑i' ⊆ ↑I
Module: Mathlib.RingTheory.MvPowerSeries.PiTopology

Goal state before:
pp: case mp
σ : Type u_1
R : Type u_2
inst✝¹ : TopologicalSpace R
inst✝ : Semiring R
ι : Type u_3
f : ι → MvPowerSeries σ R
⊢ (∃ 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
σ : Type u_1
R : Type u_2
inst✝¹ : TopologicalSpace R
inst✝ : Semiring R
ι : Type u_3
f : ι → MvPowerSeries σ R
⊢ (∀ (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
σ : Type u_1
R : Type u_2
inst✝¹ : TopologicalSpace R
inst✝ : Semiring R
ι : Type u_3
f : ι → MvPowerSeries σ R
⊢ (∃ 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.MvPowerSeries.PiTopology

Goal state before:
pp: case mpr
σ : Type u_1
R : Type u_2
inst✝¹ : TopologicalSpace R
inst✝ : Semiring R
ι : Type u_3
f : ι → MvPowerSeries σ R
⊢ (∀ (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
σ : Type u_1
R : Type u_2
inst✝¹ : TopologicalSpace R
inst✝ : Semiring R
ι : Type u_3
f : ι → MvPowerSeries σ R
⊢ (∀ (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.MvPowerSeries.PiTopology

Goal state before:
pp: case inl
σ : Type u_1
R : Type u_2
inst✝³ : TopologicalSpace R
inst✝² : Semiring R
ι : Type u_3
f : ι → MvPowerSeries σ R
inst✝¹ : LinearOrder ι
inst✝ : LocallyFiniteOrderBot ι
w : σ → ℕ
h : Tendsto (fun i ↦ weightedOrder w (f i)) atTop (𝓝 ⊤)
hempty : IsEmpty ι
⊢ Summable f

pp: case inr
σ : Type u_1
R : Type u_2
inst✝³ : TopologicalSpace R
inst✝² : Semiring R
ι : Type u_3
f : ι → MvPowerSeries σ R
inst✝¹ : LinearOrder ι
inst✝ : LocallyFiniteOrderBot ι
w : σ → ℕ
h : Tendsto (fun i ↦ weightedOrder w (f i)) atTop (𝓝 ⊤)
hempty : Nonempty ι
⊢ Summable f

Tactic:
·

Goal state after:
case inl
σ : Type u_1
R : Type u_2
inst✝³ : TopologicalSpace R
inst✝² : Semiring R
ι : Type u_3
f : ι → MvPowerSeries σ R
inst✝¹ : LinearOrder ι
inst✝ : LocallyFiniteOrderBot ι
w : σ → ℕ
h : Tendsto (fun i ↦ weightedOrder w (f i)) atTop (𝓝 ⊤)
hempty : IsEmpty ι
⊢ Summable f
Module: Mathlib.RingTheory.PowerSeries.Order

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
φ : R⟦X⟧
n : ℕ
h : (coeff n) φ ≠ 0
⊢ ↑(Nat.find ⋯) ≤ ↑n

pp: case hnc
R : Type u_1
inst✝ : Semiring R
φ : R⟦X⟧
n : ℕ
h : (coeff n) φ ≠ 0
⊢ ¬φ = 0

Tactic:
·

Goal state after:
R : Type u_1
inst✝ : Semiring R
φ : R⟦X⟧
n : ℕ
h : (coeff n) φ ≠ 0
⊢ ↑(Nat.find ⋯) ≤ ↑n
Module: Mathlib.RingTheory.PowerSeries.Order

Goal state before:
pp: case hnc
R : Type u_1
inst✝ : Semiring R
φ : R⟦X⟧
n : ℕ
h : (coeff n) φ ≠ 0
⊢ ¬φ = 0

Tactic:
·

Goal state after:
case hnc
R : Type u_1
inst✝ : Semiring R
φ : R⟦X⟧
n : ℕ
h : (coeff n) φ ≠ 0
⊢ ¬φ = 0
Module: Mathlib.RingTheory.PowerSeries.Order

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

pp: case neg
R : Type u_1
inst✝ : Semiring R
φ : R⟦X⟧
n : ℕ
h : n < φ.order.toNat
h' : ¬φ = 0
⊢ (coeff n) φ = 0

Tactic:
·

Goal state after:
case pos
R : Type u_1
inst✝ : Semiring R
φ : R⟦X⟧
n : ℕ
h : n < φ.order.toNat
h' : φ = 0
⊢ (coeff n) φ = 0
Module: Mathlib.RingTheory.PowerSeries.Order

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

Tactic:
·

Goal state after:
case neg
R : Type u_1
inst✝ : Semiring R
φ : R⟦X⟧
n : ℕ
h : n < φ.order.toNat
h' : ¬φ = 0
⊢ (coeff n) φ = 0
Module: Mathlib.RingTheory.PowerSeries.Order

Goal state before:
pp: case pos
R : Type u_1
inst✝ : Semiring R
φ : R⟦X⟧
n : ℕ
h : ∀ i < n, (coeff i) φ = 0
h✝ : φ = 0
⊢ ↑n ≤ ⊤

pp: case neg
R : Type u_1
inst✝ : Semiring R
φ : R⟦X⟧
n : ℕ
h : ∀ i < n, (coeff i) φ = 0
h✝ : ¬φ = 0
⊢ ↑n ≤ ↑(Nat.find ⋯)

Tactic:
·

Goal state after:
case pos
R : Type u_1
inst✝ : Semiring R
φ : R⟦X⟧
n : ℕ
h : ∀ i < n, (coeff i) φ = 0
h✝ : φ = 0
⊢ ↑n ≤ ⊤
Module: Mathlib.RingTheory.PowerSeries.Order

Goal state before:
pp: case neg
R : Type u_1
inst✝ : Semiring R
φ : R⟦X⟧
n : ℕ
h : ∀ i < n, (coeff i) φ = 0
h✝ : ¬φ = 0
⊢ ↑n ≤ ↑(Nat.find ⋯)

Tactic:
·

Goal state after:
case neg
R : Type u_1
inst✝ : Semiring R
φ : R⟦X⟧
n : ℕ
h : ∀ i < n, (coeff i) φ = 0
h✝ : ¬φ = 0
⊢ ↑n ≤ ↑(Nat.find ⋯)
Module: Mathlib.RingTheory.MvPowerSeries.PiTopology

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

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

Goal state after:
case inl
σ : 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 : IsEmpty ι
⊢ Summable fun x ↦ ∏ i ∈ x, f i
Module: Mathlib.RingTheory.DedekindDomain.AdicValuation

Goal state before:
pp: case pos
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
a : adicCompletion K v
ha : a ∈ adicCompletionIntegers K v
⊢ ∃ b ∈ R⁰, a * ↑b ∈ adicCompletionIntegers K v

pp: case neg
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
a : adicCompletion K v
ha : a ∉ adicCompletionIntegers K v
⊢ ∃ b ∈ R⁰, a * ↑b ∈ adicCompletionIntegers K v

Tactic:
·

Goal state after:
case pos
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
a : adicCompletion K v
ha : a ∈ adicCompletionIntegers K v
⊢ ∃ b ∈ R⁰, a * ↑b ∈ adicCompletionIntegers K v
Module: Mathlib.RingTheory.PowerSeries.Order

Goal state before:
pp: case inl
R : Type u_1
inst✝ : Semiring R
n : ℕ
⊢ order 0 = ↑n ↔ (coeff n) 0 ≠ 0 ∧ ∀ i < n, (coeff i) 0 = 0

pp: case inr
R : Type u_1
inst✝ : Semiring R
φ : R⟦X⟧
n : ℕ
hφ : φ ≠ 0
⊢ φ.order = ↑n ↔ (coeff n) φ ≠ 0 ∧ ∀ i < n, (coeff i) φ = 0

Tactic:
·

Goal state after:
case inl
R : Type u_1
inst✝ : Semiring R
n : ℕ
⊢ order 0 = ↑n ↔ (coeff n) 0 ≠ 0 ∧ ∀ i < n, (coeff i) 0 = 0
Module: Mathlib.RingTheory.DedekindDomain.AdicValuation

Goal state before:
pp: case neg
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
a : adicCompletion K v
ha : a ∉ adicCompletionIntegers K v
⊢ ∃ b ∈ R⁰, a * ↑b ∈ adicCompletionIntegers K v

Tactic:
·

Goal state after:
case neg
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
a : adicCompletion K v
ha : a ∉ adicCompletionIntegers K v
⊢ ∃ b ∈ R⁰, a * ↑b ∈ adicCompletionIntegers K v
Module: Mathlib.RingTheory.PowerSeries.Order

Goal state before:
pp: case refine_1
R : Type u_1
inst✝ : Semiring R
φ : R⟦X⟧
⊢ φ.order ≤ MvPowerSeries.order φ

pp: case refine_2
R : Type u_1
inst✝ : Semiring R
φ : R⟦X⟧
⊢ MvPowerSeries.order φ ≤ φ.order

Tactic:
·

Goal state after:
case refine_1
R : Type u_1
inst✝ : Semiring R
φ : R⟦X⟧
⊢ φ.order ≤ MvPowerSeries.order φ
Module: Mathlib.RingTheory.PowerSeries.Order

Goal state before:
pp: case refine_2
R : Type u_1
inst✝ : Semiring R
φ : R⟦X⟧
⊢ MvPowerSeries.order φ ≤ φ.order

Tactic:
·

Goal state after:
case refine_2
R : Type u_1
inst✝ : Semiring R
φ : R⟦X⟧
⊢ MvPowerSeries.order φ ≤ φ.order
Module: Mathlib.RingTheory.PowerSeries.Trunc

Goal state before:
pp: case pos
R : Type u_1
inst✝ : Semiring R
n : ℕ
φ ψ : R⟦X⟧
m : ℕ
H : m < n
⊢ (coeff m) (φ + ψ) = (coeff m) φ + (coeff m) ψ

pp: case neg
R : Type u_1
inst✝ : Semiring R
n : ℕ
φ ψ : R⟦X⟧
m : ℕ
H : ¬m < n
⊢ 0 = 0 + 0

Tactic:
·

Goal state after:
case pos
R : Type u_1
inst✝ : Semiring R
n : ℕ
φ ψ : R⟦X⟧
m : ℕ
H : m < n
⊢ (coeff m) (φ + ψ) = (coeff m) φ + (coeff m) ψ
Module: Mathlib.RingTheory.PowerSeries.Trunc

Goal state before:
pp: case neg
R : Type u_1
inst✝ : Semiring R
n : ℕ
φ ψ : R⟦X⟧
m : ℕ
H : ¬m < n
⊢ 0 = 0 + 0

Tactic:
·

Goal state after:
case neg
R : Type u_1
inst✝ : Semiring R
n : ℕ
φ ψ : R⟦X⟧
m : ℕ
H : ¬m < n
⊢ 0 = 0 + 0
Module: Mathlib.RingTheory.PowerSeries.Order

Goal state before:
pp: case left
R : Type u_1
inst✝ : Semiring R
φ ψ : R⟦X⟧
H : φ.order < ψ.order
⊢ ∀ (i : ℕ), ↑i = φ.order → (coeff i) (φ + ψ) ≠ 0

pp: case right
R : Type u_1
inst✝ : Semiring R
φ ψ : R⟦X⟧
H : φ.order < ψ.order
⊢ ∀ (i : ℕ), ↑i < φ.order → (coeff i) (φ + ψ) = 0

Tactic:
·

Goal state after:
case left
R : Type u_1
inst✝ : Semiring R
φ ψ : R⟦X⟧
H : φ.order < ψ.order
⊢ ∀ (i : ℕ), ↑i = φ.order → (coeff i) (φ + ψ) ≠ 0
Module: Mathlib.RingTheory.PowerSeries.Order

Goal state before:
pp: case right
R : Type u_1
inst✝ : Semiring R
φ ψ : R⟦X⟧
H : φ.order < ψ.order
⊢ ∀ (i : ℕ), ↑i < φ.order → (coeff i) (φ + ψ) = 0

Tactic:
·

Goal state after:
case right
R : Type u_1
inst✝ : Semiring R
φ ψ : R⟦X⟧
H : φ.order < ψ.order
⊢ ∀ (i : ℕ), ↑i < φ.order → (coeff i) (φ + ψ) = 0
Module: Mathlib.RingTheory.PowerSeries.Order

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

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

Tactic:
·

Goal state after:
case inl
R : Type u_1
inst✝ : Semiring R
φ ψ : R⟦X⟧
h : φ.order ≠ ψ.order
φ_lt_ψ : φ.order < ψ.order
⊢ (φ + ψ).order ≤ min φ.order ψ.order
Module: Mathlib.RingTheory.PowerSeries.Order

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

Tactic:
·

Goal state after:
case inr
R : Type u_1
inst✝ : Semiring R
φ ψ : R⟦X⟧
h : φ.order ≠ ψ.order
ψ_lt_φ : ψ.order < φ.order
⊢ (φ + ψ).order ≤ min φ.order ψ.order
Module: Mathlib.RingTheory.PowerSeries.Order

Goal state before:
pp: case pos
R : Type u_1
inst✝ : Semiring R
φ ψ : R⟦X⟧
n : ℕ
hn : ↑n < φ.order + ψ.order
i j : ℕ
hij : (i, j) ∈ antidiagonal n
hi : ↑i < φ.order
⊢ (coeff (i, j).1) φ * (coeff (i, j).2) ψ = 0

pp: case neg
R : Type u_1
inst✝ : Semiring R
φ ψ : R⟦X⟧
n : ℕ
hn : ↑n < φ.order + ψ.order
i j : ℕ
hij : (i, j) ∈ antidiagonal n
hi : φ.order ≤ ↑i
⊢ (coeff (i, j).1) φ * (coeff (i, j).2) ψ = 0

Tactic:
·

Goal state after:
case pos
R : Type u_1
inst✝ : Semiring R
φ ψ : R⟦X⟧
n : ℕ
hn : ↑n < φ.order + ψ.order
i j : ℕ
hij : (i, j) ∈ antidiagonal n
hi : ↑i < φ.order
⊢ (coeff (i, j).1) φ * (coeff (i, j).2) ψ = 0
Module: Mathlib.RingTheory.PowerSeries.Order

Goal state before:
pp: case pos
R : Type u_1
inst✝ : Semiring R
φ ψ : R⟦X⟧
n : ℕ
hn : ↑n < φ.order + ψ.order
i j : ℕ
hij : (i, j) ∈ antidiagonal n
hi : φ.order ≤ ↑i
hj : ↑j < ψ.order
⊢ (coeff (i, j).1) φ * (coeff (i, j).2) ψ = 0

pp: case neg
R : Type u_1
inst✝ : Semiring R
φ ψ : R⟦X⟧
n : ℕ
hn : ↑n < φ.order + ψ.order
i j : ℕ
hij : (i, j) ∈ antidiagonal n
hi : φ.order ≤ ↑i
hj : ψ.order ≤ ↑j
⊢ (coeff (i, j).1) φ * (coeff (i, j).2) ψ = 0

Tactic:
·

Goal state after:
case pos
R : Type u_1
inst✝ : Semiring R
φ ψ : R⟦X⟧
n : ℕ
hn : ↑n < φ.order + ψ.order
i j : ℕ
hij : (i, j) ∈ antidiagonal n
hi : φ.order ≤ ↑i
hj : ↑j < ψ.order
⊢ (coeff (i, j).1) φ * (coeff (i, j).2) ψ = 0
Module: Mathlib.RingTheory.PowerSeries.Trunc

Goal state before:
pp: case pos
R : Type u_1
inst✝ : Semiring R
n d : ℕ
h₁ : d < n + 2
h₂ : d = 1
⊢ 1 = Polynomial.X.coeff d

pp: case neg
R : Type u_1
inst✝ : Semiring R
n d : ℕ
h₁ : d < n + 2
h₂ : ¬d = 1
⊢ 0 = Polynomial.X.coeff d

pp: case neg
R : Type u_1
inst✝ : Semiring R
n d : ℕ
h₁ : ¬d < n + 2
⊢ 0 = Polynomial.X.coeff d

Tactic:
·

Goal state after:
case pos
R : Type u_1
inst✝ : Semiring R
n d : ℕ
h₁ : d < n + 2
h₂ : d = 1
⊢ 1 = Polynomial.X.coeff d
Module: Mathlib.RingTheory.PowerSeries.Order

Goal state before:
pp: case cons
R : Type u_2
inst✝ : CommSemiring R
ι : Type u_3
φ : ι → R⟦X⟧
a : ι
s : Finset ι
ha : a ∉ s
ih : ∑ i ∈ s, (φ i).order ≤ (∏ i ∈ s, φ i).order
⊢ ∑ i ∈ Finset.cons a s ha, (φ i).order ≤ (∏ i ∈ Finset.cons a s ha, φ i).order

Tactic:
grw [Finset.sum_cons ha, Finset.prod_cons ha, ih, le_order_mul]

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

Goal state before:
pp: case neg
R : Type u_1
inst✝ : Semiring R
n d : ℕ
h₁ : d < n + 2
h₂ : ¬d = 1
⊢ 0 = Polynomial.X.coeff d

pp: case neg
R : Type u_1
inst✝ : Semiring R
n d : ℕ
h₁ : ¬d < n + 2
⊢ 0 = Polynomial.X.coeff d

Tactic:
·

Goal state after:
case neg
R : Type u_1
inst✝ : Semiring R
n d : ℕ
h₁ : d < n + 2
h₂ : ¬d = 1
⊢ 0 = Polynomial.X.coeff d
Module: Mathlib.RingTheory.PowerSeries.Trunc

Goal state before:
pp: case neg
R : Type u_1
inst✝ : Semiring R
n d : ℕ
h₁ : ¬d < n + 2
⊢ 0 = Polynomial.X.coeff d

Tactic:
·

Goal state after:
case neg
R : Type u_1
inst✝ : Semiring R
n d : ℕ
h₁ : ¬d < n + 2
⊢ 0 = Polynomial.X.coeff d
Module: Mathlib.RingTheory.PowerSeries.Order

Goal state before:
pp: case mp
R : Type u_1
inst✝ : Semiring R
φ : R⟦X⟧
⊢ 1 ≤ φ.order → constantCoeff φ = 0

pp: case mpr
R : Type u_1
inst✝ : Semiring R
φ : R⟦X⟧
⊢ constantCoeff φ = 0 → 1 ≤ φ.order

Tactic:
·

Goal state after:
case mp
R : Type u_1
inst✝ : Semiring R
φ : R⟦X⟧
⊢ 1 ≤ φ.order → constantCoeff φ = 0
Module: Mathlib.RingTheory.PowerSeries.Order

Goal state before:
pp: case mpr
R : Type u_1
inst✝ : Semiring R
φ : R⟦X⟧
⊢ constantCoeff φ = 0 → 1 ≤ φ.order

Tactic:
·

Goal state after:
case mpr
R : Type u_1
inst✝ : Semiring R
φ : R⟦X⟧
⊢ constantCoeff φ = 0 → 1 ≤ φ.order
Module: Mathlib.RingTheory.PowerSeries.Order

Goal state before:
pp: case pos
R : Type u_1
inst✝¹ : Semiring R
n : ℕ
a : R
inst✝ : Decidable (a = 0)
h : a = 0
⊢ ((monomial n) a).order = ⊤

pp: case neg
R : Type u_1
inst✝¹ : Semiring R
n : ℕ
a : R
inst✝ : Decidable (a = 0)
h : ¬a = 0
⊢ ((monomial n) a).order = ↑n

Tactic:
·

Goal state after:
case pos
R : Type u_1
inst✝¹ : Semiring R
n : ℕ
a : R
inst✝ : Decidable (a = 0)
h : a = 0
⊢ ((monomial n) a).order = ⊤
Module: Mathlib.RingTheory.PowerSeries.Order

Goal state before:
pp: case neg
R : Type u_1
inst✝¹ : Semiring R
n : ℕ
a : R
inst✝ : Decidable (a = 0)
h : ¬a = 0
⊢ ((monomial n) a).order = ↑n

Tactic:
·

Goal state after:
case neg
R : Type u_1
inst✝¹ : Semiring R
n : ℕ
a : R
inst✝ : Decidable (a = 0)
h : ¬a = 0
⊢ ((monomial n) a).order = ↑n
Module: Mathlib.RingTheory.PowerSeries.Order

Goal state before:
pp: case neg.left
R : Type u_1
inst✝¹ : Semiring R
n : ℕ
a : R
inst✝ : Decidable (a = 0)
h : ¬a = 0
i : ℕ
hi : ↑i = ↑n
⊢ (coeff i) ((monomial n) a) ≠ 0

pp: case neg.right
R : Type u_1
inst✝¹ : Semiring R
n : ℕ
a : R
inst✝ : Decidable (a = 0)
h : ¬a = 0
i : ℕ
hi : ↑i < ↑n
⊢ (coeff i) ((monomial n) a) = 0

Tactic:
·

Goal state after:
case neg.left
R : Type u_1
inst✝¹ : Semiring R
n : ℕ
a : R
inst✝ : Decidable (a = 0)
h : ¬a = 0
i : ℕ
hi : ↑i = ↑n
⊢ (coeff i) ((monomial n) a) ≠ 0
Module: Mathlib.RingTheory.PowerSeries.Order

Goal state before:
pp: case neg.right
R : Type u_1
inst✝¹ : Semiring R
n : ℕ
a : R
inst✝ : Decidable (a = 0)
h : ¬a = 0
i : ℕ
hi : ↑i < ↑n
⊢ (coeff i) ((monomial n) a) = 0

Tactic:
·

Goal state after:
case neg.right
R : Type u_1
inst✝¹ : Semiring R
n : ℕ
a : R
inst✝ : Decidable (a = 0)
h : ¬a = 0
i : ℕ
hi : ↑i < ↑n
⊢ (coeff i) ((monomial n) a) = 0
Module: Mathlib.RingTheory.PowerSeries.Trunc

Goal state before:
pp: case pos
R : Type u_2
inst✝ : CommSemiring R
n m : ℕ
f : R⟦X⟧
hnm : n ≤ m
d : ℕ
h : d < n
⊢ ((trunc m) f).coeff d = (coeff d) f

pp: case neg
R : Type u_2
inst✝ : CommSemiring R
n m : ℕ
f : R⟦X⟧
hnm : n ≤ m
d : ℕ
h : ¬d < n
⊢ 0 = 0

Tactic:
·

Goal state after:
case pos
R : Type u_2
inst✝ : CommSemiring R
n m : ℕ
f : R⟦X⟧
hnm : n ≤ m
d : ℕ
h : d < n
⊢ ((trunc m) f).coeff d = (coeff d) f
Module: Mathlib.RingTheory.PowerSeries.Trunc

Goal state before:
pp: case neg
R : Type u_2
inst✝ : CommSemiring R
n m : ℕ
f : R⟦X⟧
hnm : n ≤ m
d : ℕ
h : ¬d < n
⊢ 0 = 0

Tactic:
·

Goal state after:
case neg
R : Type u_2
inst✝ : CommSemiring R
n m : ℕ
f : R⟦X⟧
hnm : n ≤ m
d : ℕ
h : ¬d < n
⊢ 0 = 0
Module: Mathlib.RingTheory.PowerSeries.Trunc

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

pp: case neg
R : Type u_2
inst✝ : CommSemiring R
n : ℕ
f g : R⟦X⟧
m : ℕ
h : ¬m < n
⊢ 0 = 0

Tactic:
·

Goal state after:
case pos
R : Type u_2
inst✝ : CommSemiring R
n : ℕ
f g : R⟦X⟧
m : ℕ
h : m < n
⊢ (coeff m) (↑((trunc n) f) * g) = (coeff m) (f * g)
Module: Mathlib.RingTheory.PowerSeries.Trunc

Goal state before:
pp: case neg
R : Type u_2
inst✝ : CommSemiring R
n : ℕ
f g : R⟦X⟧
m : ℕ
h : ¬m < n
⊢ 0 = 0

Tactic:
·

Goal state after:
case neg
R : Type u_2
inst✝ : CommSemiring R
n : ℕ
f g : R⟦X⟧
m : ℕ
h : ¬m < n
⊢ 0 = 0
Module: Mathlib.RingTheory.PowerSeries.Order

Goal state before:
pp: case pos
R : Type u_1
inst✝ : Semiring R
f : R⟦X⟧
h : f = 0
⊢ constantCoeff f.divXPowOrder = 0 ↔ f = 0

pp: case neg
R : Type u_1
inst✝ : Semiring R
f : R⟦X⟧
h : ¬f = 0
⊢ constantCoeff f.divXPowOrder = 0 ↔ f = 0

Tactic:
·

Goal state after:
case pos
R : Type u_1
inst✝ : Semiring R
f : R⟦X⟧
h : f = 0
⊢ constantCoeff f.divXPowOrder = 0 ↔ f = 0
Module: Mathlib.RingTheory.PowerSeries.Order

Goal state before:
pp: case neg
R : Type u_1
inst✝ : Semiring R
f : R⟦X⟧
h : ¬f = 0
⊢ constantCoeff f.divXPowOrder = 0 ↔ f = 0

Tactic:
·

Goal state after:
case neg
R : Type u_1
inst✝ : Semiring R
f : R⟦X⟧
h : ¬f = 0
⊢ constantCoeff f.divXPowOrder = 0 ↔ f = 0
Module: Mathlib.Topology.Algebra.LinearTopology

Goal state before:
pp: case mp
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
H : IsLinearTopology Rᵐᵒᵖ M
⊢ IsLinearTopology R M

pp: case mpr
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
H : IsLinearTopology R M
⊢ IsLinearTopology Rᵐᵒᵖ M

Tactic:
·

Goal state after:
case mp
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
H : IsLinearTopology Rᵐᵒᵖ M
⊢ IsLinearTopology R M
Module: Mathlib.RingTheory.PowerSeries.Order

Goal state before:
pp: case pos
R : Type u_1
inst✝ : Semiring R
f : R⟦X⟧
n : ℕ
h : f.order.toNat ≤ n
⊢ (coeff (n - f.order.toNat)) f.divXPowOrder = (coeff n) f

pp: case neg
R : Type u_1
inst✝ : Semiring R
f : R⟦X⟧
n : ℕ
h : ¬f.order.toNat ≤ n
⊢ 0 = (coeff n) f

Tactic:
·

Goal state after:
case pos
R : Type u_1
inst✝ : Semiring R
f : R⟦X⟧
n : ℕ
h : f.order.toNat ≤ n
⊢ (coeff (n - f.order.toNat)) f.divXPowOrder = (coeff n) f
Module: Mathlib.RingTheory.PowerSeries.Order

Goal state before:
pp: case neg
R : Type u_1
inst✝ : Semiring R
f : R⟦X⟧
n : ℕ
h : ¬f.order.toNat ≤ n
⊢ 0 = (coeff n) f

Tactic:
·

Goal state after:
case neg
R : Type u_1
inst✝ : Semiring R
f : R⟦X⟧
n : ℕ
h : ¬f.order.toNat ≤ n
⊢ 0 = (coeff n) f
Module: Mathlib.Topology.Algebra.LinearTopology

Goal state before:
pp: case mpr
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
H : IsLinearTopology R M
⊢ IsLinearTopology Rᵐᵒᵖ M

Tactic:
·

Goal state after:
case mpr
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
H : IsLinearTopology R M
⊢ IsLinearTopology Rᵐᵒᵖ M