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

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : Semiring R
a b : R
⊢ (monomial 0).toFun (a * b) = (monomial (0 + 0)) (a * b)

Tactic:
simp

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

Goal state before:
pp: case zero
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
s : σ
⊢ X s ^ 0 = (monomial (single s 0)) 1

Tactic:
simp

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

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : Semiring R
f : MvPowerSeries σ R
a : R
n✝ : σ →₀ ℕ
⊢ (coeff n✝) (a • f) = (coeff n✝) (C a * f)

Tactic:
simp

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

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

Tactic:
simp

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

Goal state before:
pp: σ : Type u_1
R : Type u_2
S : Type u_3
T : Type u_4
inst✝² : Semiring R
inst✝¹ : Semiring S
inst✝ : Semiring T
f : R →+* S
g : S →+* T
φ ψ : MvPowerSeries σ R
n : σ →₀ ℕ
⊢ f ((coeff n) (φ + ψ)) = f ((coeff n) φ) + f ((coeff n) ψ)

Tactic:
simp

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

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝² : Semiring R
S₁ : Type u_5
S₂ : Type u_6
inst✝¹ : CommSemiring S₁
inst✝ : CommSemiring S₂
f : R →+* S₁
g : S₁ →+* S₂
p : MvPowerSeries σ R
n : σ →₀ ℕ
⊢ (coeff n) ((map g) ((map f) p)) = (coeff n) ((map (g.comp f)) p)

Tactic:
simp

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

Goal state before:
pp: σ : Type u_1
R : Type u_2
S : Type u_3
inst✝² : DivisionSemiring R
inst✝¹ : Semiring S
inst✝ : Nontrivial S
φ : MvPowerSeries σ R
f : R →+* S
n : σ →₀ ℕ
⊢ (coeff n) ((map f) φ) = (coeff n) 0 ↔ (coeff n) φ = (coeff n) 0

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
f : R⟦X⟧
⊢ (rescale 0) f = C (constantCoeff f)

Tactic:
simp

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

Goal state before:
pp: case e'_2.e'_5
R : Type u_1
inst✝⁴ : CommSemiring R
A : Type u_2
S : Type u_3
inst✝³ : CommSemiring A
inst✝² : Algebra A R
inst✝¹ : CommSemiring S
inst✝ : Algebra A S
φ : R →ₐ[A] S
a : A
f : R⟦X⟧
⊢ (algebraMap A S) a = ↑φ ((algebraMap A R) a)

Tactic:
simp

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

Goal state before:
pp: case inl
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
⊢ v.intValuation 0 ≤ 1

Tactic:
simp

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

Goal state before:
pp: R : Type u_2
inst✝ : CommSemiring R
φ ψ : R⟦X⟧
this : antidiagonal 1 = {(0, 1), (1, 0)}
⊢ (0, 1) ∉ {(1, 0)}

Tactic:
simp

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

Goal state before:
pp: case inl
R : Type u_2
inst✝ : CommSemiring R
φ : R⟦X⟧
⊢ (coeff 1) (φ ^ 0) = ↑0 * (coeff 1) φ * constantCoeff φ ^ (0 - 1)

Tactic:
simp

Goal state after:
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 : ℕ
⊢ 0 < exp 1

Tactic:
simp

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

Goal state before:
pp: case empty
σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
ι : Type u_4
f : ι → σ →₀ ℕ
g : ι → R
⊢ ∏ i ∈ ∅, (monomial (f i)) (g i) = (monomial (∑ i ∈ ∅, f i)) (∏ i ∈ ∅, g i)

Tactic:
simp

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

Goal state before:
pp: case inl
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, (valuation K v) a = 0

Tactic:
simp

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

Goal state before:
pp: case inl
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
d : R
hd : d ∈ nonZeroDivisors R
h : ∀ (v : HeightOneSpectrum R), (valuation K v) (IsLocalization.mk' K 0 ⟨d, hd⟩) ≤ 1
hx : IsLocalization.mk' K 0 ⟨d, hd⟩ * (algebraMap R K) ↑(0, ⟨d, hd⟩).2 = (algebraMap R K) (0, ⟨d, hd⟩).1
⊢ IsLocalization.mk' K 0 ⟨d, hd⟩ ∈ (algebraMap R K).range

Tactic:
simp

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

Goal state before:
pp: A : Type u_2
inst✝ : CommRing A
hA : ¬Subsingleton A
a✝ : Nontrivial A
⊢ ∃ I, ⊥ < I ∧ I < ⊤

Tactic:
(Mathlib.Tactic.useSyntax
 "use"
 []
 (group)
 [(Term.app
   `Ideal.span
   [(choice
     («term{_}» "{" [`X] "}")
     (Term.structInst
      "{"
      []
      (Term.structInstFields [(Term.structInstField (Term.structInstLVal `X []) [])])
      (Term.optEllipsis [])
      []
      "}"))])])

Goal state after:
case h
A : Type u_2
inst✝ : CommRing A
hA : ¬Subsingleton A
a✝ : Nontrivial A
⊢ ⊥ < Ideal.span {X} ∧ Ideal.span {X} < ⊤
Module: Mathlib.RingTheory.PowerSeries.Basic

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
φ ψ : R[X]
n✝ : ℕ
⊢ (PowerSeries.coeff n✝) ↑(φ + ψ) = (PowerSeries.coeff n✝) (↑φ + ↑ψ)

Tactic:
simp

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

Goal state before:
pp: U : Type u_2
V : Type u_3
inst✝¹ : CommSemiring U
inst✝ : CommSemiring V
φ : U →+* V
f : U[X]
n✝ : ℕ
⊢ (PowerSeries.coeff n✝) ↑(map φ f) = (PowerSeries.coeff n✝) ((PowerSeries.map φ) ↑f)

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
d : PUnit.{1} →₀ ℕ
r : R
⊢ (single () (d ())) default = d default

Tactic:
simp

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

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
⊢ weightedOrder w 0 = ⊤

Tactic:
by
  rw [weightedOrder, dif_pos rfl]

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

Goal state before:
pp: σ : Type u_1
R : Type u_2
A : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
r : R
⊢ ((map (algebraMap R A)).comp C) r = C ((algebraMap R A) r)

Tactic:
simp

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

Goal state before:
pp: 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
⊢ (valuation K v).valuationSubring ≠ ⊤

Tactic:
simp only [ne_eq, Valuation.valuationSubring_eq_top_iff, not_not]; infer_instance

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

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
e : σ →₀ ℕ
p : ℕ
r : R
⊢ ∀ i ∈ e.support, MvPowerSeries.X i ^ 0 = 1

Tactic:
simp

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

Goal state before:
pp: case zero
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
f : MvPowerSeries σ R
⊢ 0 • weightedOrder w f ≤ weightedOrder w (f ^ 0)

Tactic:
simp

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

Goal state before:
pp: case empty
σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
ι : Type u_4
w : σ → ℕ
f : ι → MvPowerSeries σ R
⊢ ∑ i ∈ ∅, weightedOrder w (f i) ≤ weightedOrder w (∏ i ∈ ∅, f i)

Tactic:
simp

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

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝¹ : DecidableEq σ
inst✝ : CommSemiring R
n : σ →₀ ℕ
⊢ 0 ∈ Iic n

Tactic:
simp

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

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝¹ : DecidableEq σ
inst✝ : CommSemiring R
n : σ →₀ ℕ
a : R
⊢ 0 ∈ Iic n

Tactic:
simp

Goal state after:
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 : (ofClass (valuation K v)).ValueGroup₀
⊢ (map' ↑(valueGroupEquiv K v).symm) ((map' ↑(valueGroupEquiv K v)) 0) = 0

Tactic:
simp

Goal state after:
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 : (ofClass (valuation K v)).ValueGroup₀
a : ↥(ofClass (valuation K v)).valueGroup
⊢ (map' ↑(valueGroupEquiv K v).symm) ((map' ↑(valueGroupEquiv K v)) ↑a) = ↑a

Tactic:
simp

Goal state after:
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
y : (ofClass Valued.v).ValueGroup₀
⊢ (map' ↑(valueGroupEquiv K v)) ((map' ↑(valueGroupEquiv K v).symm) 0) = 0

Tactic:
simp

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

Goal state before:
pp: σ : Type u_1
R : Type u_2
n : ℕ
inst✝¹ : Finite σ
inst✝ : CommSemiring R
⊢ 0 ∉ ⋯.toFinset → n = 0

Tactic:
simp

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

Goal state before:
pp: σ : Type u_1
R : Type u_2
n : ℕ
inst✝¹ : Finite σ
inst✝ : CommSemiring R
p q : MvPowerSeries σ R
x : σ →₀ ℕ
hx : degree x < n
x✝¹ x✝ : σ →₀ ℕ
h : x✝ ≤ x✝¹
⊢ x✝¹ ∈ ↑⋯.toFinset → x✝ ∈ ↑⋯.toFinset

Tactic:
simp

Goal state after:
σ : Type u_1
R : Type u_2
n : ℕ
inst✝¹ : Finite σ
inst✝ : CommSemiring R
p q : MvPowerSeries σ R
x : σ →₀ ℕ
hx : degree x < n
x✝¹ x✝ : σ →₀ ℕ
h : x✝ ≤ x✝¹
⊢ degree x✝¹ < n → degree x✝ < n
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
y : (ofClass Valued.v).ValueGroup₀
b : ↥(ofClass Valued.v).valueGroup
⊢ (map' ↑(valueGroupEquiv K v)) ((map' ↑(valueGroupEquiv K v).symm) ↑b) = ↑b

Tactic:
simp

Goal state after:
Module: Mathlib.Topology.Instances.ENat

Goal state before:
pp: key : ∀ (a : ℕ∞), ContinuousAt (Function.uncurry fun x1 x2 ↦ x1 * x2) (a, ⊤)
a b : ℕ
⊢ ContinuousAt (fun p ↦ p.1 * p.2) (↑a, ↑b)

Tactic:
by
        simp [ContinuousAt, nhds_prod_eq, tendsto_pure_nhds]

Goal state after:
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 : (ofClass (valuation K v)).ValueGroup₀),
    (map' ↑(valueGroupEquiv K v)) (x * y) = (map' ↑(valueGroupEquiv K v)) x * (map' ↑(valueGroupEquiv K v)) y

Tactic:
simp

Goal state after:
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
a b : (ofClass (valuation K v)).ValueGroup₀
⊢ (map' ↑(valueGroupEquiv K v)) 0 ≤ (map' ↑(valueGroupEquiv K v)) 0 ↔ 0 ≤ 0

Tactic:
simp

Goal state after:
Module: Mathlib.Topology.Instances.ENat

Goal state before:
pp: a b : ℕ∞
h : a ≠ ⊤ ∨ b ≠ ⊤
⊢ ContinuousAt (Function.uncurry fun x1 x2 ↦ x1 - x2) (a, b)

Tactic:
match a, b, h with
  | (a : ℕ), (b : ℕ), _ => simp [ContinuousAt, nhds_prod_eq]
  | (a : ℕ), ⊤, _ =>
    suffices ∀ᶠ b in 𝓝 ⊤, (a - b : ℕ∞) = 0 by
      simpa [ContinuousAt, nhds_prod_eq, tsub_eq_zero_of_le]
    filter_upwards [le_mem_nhds (WithTop.coe_lt_top a)] with b using tsub_eq_zero_of_le
  | ⊤, (b : ℕ), _ =>
    suffices ∀ n : ℕ, ∀ᶠ a : ℕ∞ in 𝓝 ⊤, b + n < a by
      simpa [ContinuousAt, nhds_prod_eq, (· ∘ ·), lt_tsub_iff_left, tendsto_nhds_top_iff_natCast_lt]
    exact fun n ↦ lt_mem_nhds <| WithTop.coe_lt_top (b + n)

Goal state after:
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
a b : (ofClass (valuation K v)).ValueGroup₀
val✝ : ↥(ofClass (valuation K v)).valueGroup
⊢ (map' ↑(valueGroupEquiv K v)) 0 ≤ (map' ↑(valueGroupEquiv K v)) ↑val✝ ↔ 0 ≤ ↑val✝

Tactic:
simp

Goal state after:
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
a b : (ofClass (valuation K v)).ValueGroup₀
val✝ : ↥(ofClass (valuation K v)).valueGroup
⊢ (map' ↑(valueGroupEquiv K v)) ↑val✝ ≤ (map' ↑(valueGroupEquiv K v)) 0 ↔ ↑val✝ ≤ 0

Tactic:
simp

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

Goal state before:
pp: case mp
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
f : MvPowerSeries σ R
h : 1 ≤ f.order
⊢ constantCoeff f = 0

Tactic:
apply coeff_of_lt_order

Goal state after:
case mp
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
f : MvPowerSeries σ R
h : 1 ≤ f.order
⊢ ↑(degree 0) < f.order
Module: Mathlib.RingTheory.MvPowerSeries.Order

Goal state before:
pp: case mpr
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
f : MvPowerSeries σ R
p : ℕ
hf : f = (weightedHomogeneousComponent w p) f
⊢ IsWeightedHomogeneous w f p

Tactic:
hf

Goal state after:
case mpr
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
f : MvPowerSeries σ R
p : ℕ
hf : f = (weightedHomogeneousComponent w p) f
⊢ IsWeightedHomogeneous w ((weightedHomogeneousComponent w p) f) p
Module: Mathlib.RingTheory.DedekindDomain.AdicValuation

Goal state before:
pp: 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
k : K
⊢ Valued.v { toCompletion := ↑((WithVal.equiv (HeightOneSpectrum.valuation K v)).symm k) } =
    (HeightOneSpectrum.valuation K v) k

Tactic:
simp

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

Goal state before:
pp: 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
⊢ { toCompletion := ↑((WithVal.equiv (HeightOneSpectrum.valuation K v)).symm 0) }.toCompletion = toCompletion 0

Tactic:
simp

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

Goal state before:
pp: 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
⊢ { toCompletion := ↑((WithVal.equiv (HeightOneSpectrum.valuation K v)).symm 1) }.toCompletion = toCompletion 1

Tactic:
simp

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

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝³ : TopologicalSpace R
inst✝² : DecidableEq σ
inst✝¹ : CommSemiring R
inst✝ : Nonempty σ
f : MvPowerSeries σ R
d : σ →₀ ℕ
s : σ
h✝ : True
n : σ →₀ ℕ
hn : n ≥ d + Finsupp.single s 1
⊢ 0 < (Finsupp.single s 1) s

Tactic:
simp

Goal state after:
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
inst✝ : Algebra S K
r : S
x : (valuation K v).Completion
⊢ (Completion.coeRingHom.comp (algebraMap S (WithVal (valuation K v)))) r * x =
    x * (Completion.coeRingHom.comp (algebraMap S (WithVal (valuation K v)))) r

Tactic:
by
    induction x using Completion.induction_on with
    | hp =>
      exact isClosed_eq (continuous_const_mul _) (continuous_mul_const _)
    | ih x => rw [mul_comm]

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

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝¹ : TopologicalSpace R
inst✝ : CommSemiring R
f : MvPowerSeries σ R
hf : constantCoeff f = 0
⊢ IsNilpotent (constantCoeff f)

Tactic:
hf

Goal state after:
σ : Type u_1
R : Type u_2
inst✝¹ : TopologicalSpace R
inst✝ : CommSemiring R
f : MvPowerSeries σ R
hf : constantCoeff f = 0
⊢ IsNilpotent 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
⊢ (↑⟨{ toCompletion := ↑((WithVal.equiv (valuation K v)).symm ((algebraMap R K) 1)) }, ⋯⟩).toCompletion =
    (↑1).toCompletion

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
φ : R⟦X⟧
⊢ (∀ (n : ℕ), (coeff n) φ = 0) ↔ φ = 0

Tactic:
simp

Goal state after:
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
⊢ (↑⟨{ toCompletion := ↑((WithVal.equiv (valuation K v)).symm ((algebraMap R K) 0)) }, ⋯⟩).toCompletion =
    (↑0).toCompletion

Tactic:
simp

Goal state after:
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
inst✝ : FaithfulSMul R K
x y : R
⊢ ↑((algebraMap R ↥(adicCompletionIntegers K v)) x) = ↑((algebraMap R ↥(adicCompletionIntegers K v)) y) → x = y

Tactic:
simp

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

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

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

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

Tactic:
simp

Goal state after:
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
⊢ ∀ (r : R) (m : ↥(adicCompletionIntegers K v)), r • m = 0 → r = 0 ∨ m = 0

Tactic:
simp

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

Tactic:
simp

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

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

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
φ : R⟦X⟧
d : Unit →₀ ℕ
hd : ↑(Finsupp.degree d) < φ.order
this : (coeff (Finsupp.degree d)) φ = 0
⊢ ∀ b ∈ d.support, b ≠ () → d b = 0

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
φ : R⟦X⟧
d : Unit →₀ ℕ
hd : ↑(Finsupp.degree d) < φ.order
this : (coeff (Finsupp.degree d)) φ = 0
⊢ () ∉ d.support → d () = 0

Tactic:
simp

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

Goal state before:
pp: σ : Type u_3
R : Type u_4
inst✝³ : TopologicalSpace R
inst✝² : CommSemiring R
ι : Type u_5
f : ι → MvPowerSeries σ R
inst✝¹ : LinearOrder ι
inst✝ : LocallyFiniteOrderBot ι
w : σ → ℕ
hempty : Nonempty ι
d : σ →₀ ℕ
h : ∀ (n : ℕ), ∃ a, ∀ (b : ι), a ≤ b → ↑n < weightedOrder w (f b)
i : ι
hi : ∀ (b : ι), i ≤ b → ↑((Finsupp.weight w) d) < weightedOrder w (f b)
s : Finset ι
hs : ¬↑s ⊆ Set.Iio i
x : ι
hxs : x ∈ ↑s
hxi : i ≤ x
⊢ ∀ i ∈ s, 0 ≤ weightedOrder w (f i)

Tactic:
simp

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

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

Tactic:
rcases isEmpty_or_nonempty ι with hempty | hempty
  · apply Summable.of_finite
  refine summable_iff_summable_coeff.mpr fun d ↦ summable_of_hasFiniteSupport ?_
  simp_rw [ENat.tendsto_nhds_top_iff_natCast_lt, eventually_atTop] at h
  obtain ⟨i, hi⟩ := h (Finsupp.weight w d)
  apply (Finset.Iio i).powerset.finite_toSet.subset
  suffices ∀ s : Finset ι, coeff d (∏ i ∈ s, f i) ≠ 0 → ↑s ⊆ Set.Iio i by simpa
  intro s hs
  contrapose hs
  obtain ⟨x, hxs, hxi⟩ := Set.not_subset.mp hs
  rw [Set.mem_Iio, not_lt] at hxi
  refine coeff_eq_zero_of_lt_weightedOrder w <| (hi x hxi).trans_le <| ?_
  apply le_trans (Finset.single_le_sum (by simp) hxs) (le_weightedOrder_prod w _ _)

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
f : R⟦X⟧
n : ℕ
⊢ ((trunc (n + 1)) f).natDegree < n + 1

Tactic:
simp +contextual [natDegree_le_iff_coeff_eq_zero, coeff_trunc]

Goal state after:
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:
· rw [coeff_of_lt_order j hj, mul_zero]

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

Goal state before:
pp: case zero
R : Type u_1
inst✝ : Semiring R
φ : R⟦X⟧
⊢ 0 • φ.order ≤ (φ ^ 0).order

Tactic:
simp

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

Goal state before:
pp: case empty
R : Type u_2
inst✝ : CommSemiring R
ι : Type u_3
φ : ι → R⟦X⟧
⊢ ∑ i ∈ ∅, (φ i).order ≤ (∏ i ∈ ∅, φ i).order

Tactic:
simp

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

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

Tactic:
apply coeff_of_lt_order

Goal state after:
case mp
R : Type u_1
inst✝ : Semiring R
φ : R⟦X⟧
h : 1 ≤ φ.order
⊢ ↑0 < φ.order
Module: Mathlib.RingTheory.PowerSeries.Trunc

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
⊢ (trunc 1) X = 0

Tactic:
simp

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

Goal state before:
pp: case empty
R : Type u_2
ι : Type u_3
inst✝ : CommRing R
k : ℕ
φ : R⟦X⟧
f : ι → R⟦X⟧
⊢ (∀ i ∈ ∅, ↑k < (f i).order) → (coeff k) (φ * ∏ i ∈ ∅, (1 - f i)) = (coeff k) φ

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
n✝ : ℕ
⊢ (coeff n✝) (divXPowOrder 0) = (coeff n✝) 0

Tactic:
simp

Goal state after: