mathlib-initiative/mathlib-tactics huggingface dataset:
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
a b : R
hb : b ≠ 0
h : b ∈ v.asIdeal → a ∉ v.asIdeal
⊢ (valuation K v) (↑a / ↑b) ≤ 1 ↔ b ∉ v.asIdeal

Tactic:
by

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) ↑π = exp (-1)

Tactic:
by

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) π = exp (-1)

Tactic:
by

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
π : K
hπ : (valuation K v) π = exp (-1)
⊢ (valuation K v) π ≠ 0 ∧ (valuation K v) π ≠ 1

Tactic:
by

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

Goal state before:
pp: σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
f : MvPowerSeries σ R
m : ℕ
hf : constantCoeff f ^ m = 0
d : σ →₀ ℕ
n : ℕ
hn : m + degree d ≤ n
k : ℕ →₀ σ →₀ ℕ
hk : (range n).sum ⇑k = d ∧ k.support ⊆ range n
s : Finset ℕ := {i ∈ range n | k i = 0}
hs_def : s = {i ∈ range n | k i = 0}
hs : s ⊆ range n
hs' : ∀ i ∈ s, (coeff (k i)) f = constantCoeff f
i : ℕ
hi : i ∈ s
⊢ k i = 0

Tactic:
by

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
⊢ Function.Surjective ⇑(valuation K v)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.Valued.ValuedField

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
s : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
this : (𝓝 0).HasBasis (fun x ↦ True) fun γ ↦ {x | extensionValuation x < ↑((Units.map ↑embedding) γ)}
x : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
γ : (ofClass v).ValueGroup₀ˣ
⊢ extensionValuation.restrict x < ↑((Units.map valueGroup₀_equiv_extensionValuation.toMonoidHom) γ) ↔
    embedding (extension x) < embedding ↑γ

Tactic:
by

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

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

Tactic:
by

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
d : R
hd : d ∈ nonZeroDivisors R
hd0 : d ≠ 0
z : R
h✝ : ∀ (v : HeightOneSpectrum R), (valuation K v) (IsLocalization.mk' K (d * z) ⟨d, hd⟩) ≤ 1
hx : IsLocalization.mk' K (d * z) ⟨d, hd⟩ = (algebraMap R K) z ∨ (algebraMap R K) ↑(d * z, ⟨d, hd⟩).2 = 0
hn0 : d * z ≠ 0
this : Ideal.span {d} ∣ Ideal.span {d * z}
h : (algebraMap R K) ↑(d * z, ⟨d, hd⟩).2 = 0
⊢ False

Tactic:
by

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

Goal state before:
pp: σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
f : MvPowerSeries σ R
m : ℕ
hf : constantCoeff f ^ m = 0
d : σ →₀ ℕ
n : ℕ
hn : m + degree d ≤ n
k : ℕ →₀ σ →₀ ℕ
hk : (range n).sum ⇑k = d ∧ k.support ⊆ range n
s : Finset ℕ := {i ∈ range n | k i = 0}
hs_def : s = {i ∈ range n | k i = 0}
hs : s ⊆ range n
hs' : ∀ i ∈ s, (coeff (k i)) f = constantCoeff f
hs'' : ∀ i ∈ s, k i = 0
this : m ≤ #s
⊢ constantCoeff f ^ #s = 0

Tactic:
by

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

Tactic:
by

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

Goal state before:
pp: case neg
A : Type u_2
inst✝ : CommRing A
hA : ¬Subsingleton A
⊢ ¬IsField A⟦X⟧

Tactic:
· nontriviality A
    rw [Ring.not_isField_iff_exists_ideal_bot_lt_and_lt_top]
    use Ideal.span {X}
    constructor
    · rw [bot_lt_iff_ne_bot, Ne, Ideal.span_singleton_eq_bot]
      exact X_ne_zero
    · rw [lt_top_iff_ne_top, Ne, Ideal.eq_top_iff_one, Ideal.mem_span_singleton,
        X_dvd_iff, constantCoeff_one]
      exact one_ne_zero

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

Goal state before:
pp: A : Type u_2
inst✝ : CommRing A
⊢ ¬IsField A⟦X⟧

Tactic:
by

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

Goal state before:
pp: A : Type u_2
inst✝ : CommRing A
a : A
⊢ (rescale a) X = C a * X

Tactic:
by

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

Goal state before:
pp: A : Type u_2
inst✝ : CommRing A
⊢ (rescale (-1)) X = -X

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
n : ℕ
a : R
⊢ ↑((monomial n) a) = (PowerSeries.monomial n) a

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
this : ↑((monomial 0) 1) = (PowerSeries.monomial 0) 1
⊢ ↑1 = 1

Tactic:
rwa [PowerSeries.monomial_zero_eq_C_apply] at this

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
⊢ ↑1 = 1

Tactic:
by

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

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

Tactic:
by

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

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
a : R
this : ↑((monomial 0) a) = (PowerSeries.monomial 0) a
⊢ ↑(C a) = PowerSeries.C a

Tactic:
rwa [PowerSeries.monomial_zero_eq_C_apply] at this

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
a : R
⊢ ↑(C a) = PowerSeries.C a

Tactic:
by

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]
⊢ ↑(map φ f) = (PowerSeries.map φ) ↑f

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
x y : R[X]
h : ↑x = ↑y
⊢ x = y

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
φ : R[X]
⊢ ↑φ = 0 ↔ φ = 0

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
φ : R[X]
⊢ ↑φ = 1 ↔ φ = 1

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
φ : R[X]
⊢ eval₂ PowerSeries.C PowerSeries.X φ = ↑φ

Tactic:
by

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

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.Valued.ValuedField

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
s : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
this : (𝓝 0).HasBasis (fun x ↦ True) fun γ ↦ {x | extensionValuation x < ↑((Units.map ↑embedding) γ)}
⊢ s ∈ 𝓝 0 ↔ ∃ γ, {x | extensionValuation.restrict x < ↑γ} ⊆ s

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
f : MvPolynomial PUnit.{1} R
⊢ ↑f = ↑((MvPolynomial.uniqueAlgEquiv R PUnit.{1}) f)

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
f : R[X]
g : MvPolynomial PUnit.{1} R := (MvPolynomial.uniqueAlgEquiv R PUnit.{1}).symm f
⊢ f = (MvPolynomial.uniqueAlgEquiv R PUnit.{1}) g

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
f : R[X]
⊢ ↑f = ↑((MvPolynomial.uniqueAlgEquiv R PUnit.{1}).symm f)

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝² : CommSemiring R
φ ψ : R[X]
A : Type u_2
inst✝¹ : Semiring A
inst✝ : Algebra R A
r : R
⊢ (↑↑((PowerSeries.map (algebraMap R A)).comp ringHom)).toFun ((algebraMap R R[X]) r) = (algebraMap R (PowerSeries A)) r

Tactic:
by

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

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
f : MvPowerSeries σ R
⊢ f ≠ 0 ↔ ∃ n d, (coeff d) f ≠ 0 ∧ (weight w) d = n

Tactic:
by

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

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
f✝ g f : MvPowerSeries σ R
⊢ ℕ∞

Tactic:
by

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

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

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
f : MvPowerSeries σ R
⊢ f ≠ 0 ↔ ↑(weightedOrder w f).toNat = weightedOrder w f

Tactic:
by

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

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

Tactic:
by

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
x : K
h : ∀ (v : HeightOneSpectrum R), (valuation K v) x ≤ 1
⊢ x ∈ (algebraMap R K).range

Tactic:
by

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

Goal state before:
pp: σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
f : MvPowerSeries σ R
m : ℕ
hf : constantCoeff f ^ m = 0
d : σ →₀ ℕ
n : ℕ
hn : m + degree d ≤ n
⊢ (coeff d) (f ^ n) = 0

Tactic:
by

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
p q : HeightOneSpectrum R
hpq : (valuation K p).IsEquiv (valuation K q)
⊢ p = q

Tactic:
by

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
B : Type u_4
inst✝¹ : Semiring B
inst✝ : Algebra R B
a : R
φ : MvPowerSeries σ A
⊢ ((map (algebraMap R A)).comp C) a * φ = φ * ((map (algebraMap R A)).comp C) a

Tactic:
by

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

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
f : MvPowerSeries σ R
h : ↑(weightedOrder w f).toNat = weightedOrder w f
⊢ ∃ d, (coeff d) f ≠ 0 ∧ ↑((weight w) d) = weightedOrder w f

Tactic:
by

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
B : Type u_4
inst✝¹ : Semiring B
inst✝ : Algebra R B
a : R
σ : MvPowerSeries σ✝ A
⊢ a • σ = ((map (algebraMap R A)).comp C) a * σ

Tactic:
by

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
⊢ (algebraMap R (MvPowerSeries σ A)) r = C ((algebraMap R A) r)

Tactic:
by

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 : K
⊢ x ∈ (subalgebra.ofField K v.asIdeal.primeCompl ⋯).toSubring ∨
    x⁻¹ ∈ (subalgebra.ofField K v.asIdeal.primeCompl ⋯).toSubring

Tactic:
by

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
B : Type u_4
inst✝¹ : Semiring B
inst✝ : Algebra R B
φ : A →ₐ[R] B
r : R
⊢ (↑↑(map ↑φ)).toFun ((algebraMap R (MvPowerSeries σ A)) r) = (algebraMap R (MvPowerSeries σ B)) r

Tactic:
by

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

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
f : MvPowerSeries σ R
d : σ →₀ ℕ
h : (coeff d) f ≠ 0
⊢ weightedOrder w f ≤ ↑((weight w) d)

Tactic:
by

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

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
f : MvPowerSeries σ R
d : σ →₀ ℕ
h : ↑((weight w) d) < weightedOrder w f
⊢ (coeff d) f = 0

Tactic:
by

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
a s : R
hs : s ∈ v.asIdeal.primeCompl
this : (valuation K v) (↑a / ↑s) ≤ 1
⊢ (algebraMap R K) a * ((algebraMap R K) s)⁻¹ ∈ (valuation K v).valuationSubring

Tactic:
by

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
B : Type u_4
inst✝³ : Semiring B
inst✝² : Algebra R B
inst✝¹ : Nonempty σ
inst✝ : Nontrivial R
⊢ ⊥ ≠ ⊤

Tactic:
by

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

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
f : MvPowerSeries σ R
n : ℕ
h : ∀ (d : σ →₀ ℕ), (weight w) d < n → (coeff d) f = 0
H : weightedOrder w f < ↑n
⊢ ↑(weightedOrder w f).toNat = weightedOrder w f

Tactic:
by

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
a s : R
hs : s ∈ v.asIdeal.primeCompl
⊢ s ≠ 0

Tactic:
by

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
a s : R
hs : s ∈ v.asIdeal.primeCompl
x✝ : s ∈ v.asIdeal
⊢ a ∉ v.asIdeal

Tactic:
by

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
⊢ valuationSubringAtPrime K v ≤ (valuation K v).valuationSubring

Tactic:
by

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

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
f : MvPowerSeries σ R
n : ℕ
h : ∀ (d : σ →₀ ℕ), (weight w) d < n → (coeff d) f = 0
⊢ ↑n ≤ weightedOrder w f

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.Valued.ValuedField

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
s : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ s ∈ 𝓝 0 ↔ ∃ γ, {x | extensionValuation.restrict x < ↑γ} ⊆ s

Tactic:
by

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

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n : σ →₀ ℕ
a : R
m : σ →₀ ℕ
⊢ (MvPowerSeries.coeff m) ↑((monomial n) a) = (MvPowerSeries.coeff m) ((MvPowerSeries.monomial n) a)

Tactic:
by

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

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
φ ψ : MvPolynomial σ R
n : σ →₀ ℕ
⊢ (MvPowerSeries.coeff n) ↑(φ * ψ) = (MvPowerSeries.coeff n) (↑φ * ↑ψ)

Tactic:
by

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

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

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
⊢ Function.Injective toMvPowerSeries

Tactic:
by

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

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
φ : MvPolynomial σ R
⊢ ↑φ = 0 ↔ φ = 0

Tactic:
by

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

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
φ : MvPolynomial σ R
⊢ ↑φ = 1 ↔ φ = 1

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.Valued.ValuedField

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
x : K
⊢ v ↑x = v x

Tactic:
by

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

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
e : σ →₀ ℕ
⊢ (MvPowerSeries.monomial e) 1 = e.prod fun s n ↦ MvPowerSeries.X s ^ n

Tactic:
by

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

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
e : σ →₀ ℕ
⊢ (MvPowerSeries.monomial e) 1 = e.prod fun s n ↦ MvPowerSeries.X s ^ n

Tactic:
by
  simp only [← coe_X, ← coe_pow, ← coe_monomial, monomial_eq, map_one, one_mul]
  simp only [← coeToMvPowerSeries.ringHom_apply, ← map_finsuppProd]

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

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
f : MvPowerSeries σ R
n : ℕ∞
h : ∀ (d : σ →₀ ℕ), ↑((weight w) d) < n → (coeff d) f = 0
⊢ n ≤ weightedOrder w f

Tactic:
by

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

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
e : σ →₀ ℕ
r : R
⊢ (MvPowerSeries.monomial e) r = MvPowerSeries.C r * e.prod fun s e ↦ MvPowerSeries.X s ^ e

Tactic:
by

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

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

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
f : MvPowerSeries σ R
n : ℕ
h : weightedOrder w f = ↑n
⊢ ↑(weightedOrder w f).toNat = weightedOrder w f

Tactic:
by

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
⊢ (MvPowerSeries.monomial (p • e)) r = MvPowerSeries.C r * e.prod fun s e ↦ (MvPowerSeries.X s ^ p) ^ e

Tactic:
by

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

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
f : MvPowerSeries σ R
n : ℕ
h : weightedOrder w f = ↑n
d : σ →₀ ℕ
hd : (coeff d) f ≠ 0 ∧ ↑((weight w) d) = weightedOrder w f
⊢ (coeff d) f ≠ 0 ∧ (weight w) d = n

Tactic:
by

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

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
τ : Type u_3
d : σ →₀ ℕ
f : σ → τ
⊢ (MvPowerSeries.monomial (mapDomain f d)) 1 = d.prod fun s e ↦ MvPowerSeries.X (f s) ^ e

Tactic:
by

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

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝² : CommSemiring R
φ ψ : MvPolynomial σ R
A : Type u_3
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
r : R
⊢ (↑↑((MvPowerSeries.map (algebraMap R A)).comp ringHom)).toFun ((algebraMap R (MvPolynomial σ R)) r) =
    (algebraMap R (MvPowerSeries σ A)) r

Tactic:
by

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

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
f : MvPowerSeries σ R
n : ℕ
h : weightedOrder w f = ↑n
d : σ →₀ ℕ
hd : (coeff d) f ≠ 0 ∧ ↑((weight w) d) = weightedOrder w f
e : σ →₀ ℕ
he : (weight w) e < n
⊢ ↑((weight w) e) < weightedOrder w f

Tactic:
by

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

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝² : CommSemiring R
A : Type u_4
inst✝¹ : CommSemiring A
inst✝ : Algebra A R
e : σ →₀ ℕ
a✝ : σ → A
a : A
f : MvPowerSeries σ R
⊢ a • f = MvPowerSeries.C ((algebraMap A R) a) * f

Tactic:
by

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

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
f : MvPowerSeries σ R
n : ℕ
⊢ weightedOrder w f = ↑n ↔
    (∃ d, (coeff d) f ≠ 0 ∧ (weight w) d = n) ∧ ∀ (d : σ →₀ ℕ), (weight w) d < n → (coeff d) f = 0

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.Valued.ValuedField

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
h : Function.Surjective ⇑v
γ : Γ₀
H : ¬∃ x, v x = γ
hγ : γ ≠ 0
r : hat K
hr : v r = γ
⊢ (restrict₀ (ofClass v)) r ≠ 0

Tactic:
by

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

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝² : CommSemiring R
A : Type u_4
inst✝¹ : CommSemiring A
inst✝ : Algebra A R
e : σ →₀ ℕ
a : σ → A
⊢ (e.prod fun s n ↦ (a s • MvPowerSeries.X s) ^ n) = (e.prod fun s n ↦ a s ^ n) • (MvPowerSeries.monomial e) 1

Tactic:
by

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

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
e : σ →₀ ℕ
r : σ → R
⊢ (MvPowerSeries.monomial e) (e.prod fun s n ↦ r s ^ n) = e.prod fun s e ↦ (r s • MvPowerSeries.X s) ^ e

Tactic:
by

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

Goal state before:
pp: σ : Type u_4
R : Type u_5
inst✝ : CommSemiring R
e : σ →₀ ℕ
r : R
⊢ (MvPowerSeries.monomial e) (r ^ e.sum fun x n ↦ n) = e.prod fun s e ↦ (r • MvPowerSeries.X s) ^ e

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.Valued.ValuedField

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
h : Function.Surjective ⇑v
γ : Γ₀
a✝ : K
ha : v ↑a✝ = γ
⊢ v ?m.243 = γ

Tactic:
by

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
x : K
⊢ ∃ n d, x * (algebraMap R K) ↑d = (algebraMap R K) n ∨ x * (algebraMap R K) n = (algebraMap R K) ↑d

Tactic:
by

Goal state after: