mathlib-initiative/mathlib-tactics huggingface dataset:
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 Γ₀
a b : (ofClass v).ValueGroup₀
hab : extensionValuation.restrict ↑⋯.choose = extensionValuation.restrict ↑⋯.choose
x : K := ⋯.choose
hx_def : x = ⋯.choose
y : K := ⋯.choose
hy_def : y = ⋯.choose
hx : v x = embedding a
hy : v y = embedding b
this : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
ha0 : a = 0
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
simpa using

Goal state after:
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
a b : (ofClass v).ValueGroup₀
hab : extensionValuation.restrict ↑⋯.choose = extensionValuation.restrict ↑⋯.choose
x : K := ⋯.choose
hx_def : x = ⋯.choose
y : K := ⋯.choose
hy_def : y = ⋯.choose
hx : v x = embedding a
hy : v y = embedding b
this : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
ha0 : a = 0
⊢ x = 0
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 Γ₀
a b : (ofClass v).ValueGroup₀
x : K := ⋯.choose
hx_def : x = ⋯.choose
y : K := ⋯.choose
hy_def : y = ⋯.choose
hx : v x = embedding a
hy : v y = embedding b
this : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
ha0 : embedding a ≠ embedding 0
h0 : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
hab : v x = v y
⊢ b ≠ 0

Tactic:
simpa using

Goal state after:
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
a b : (ofClass v).ValueGroup₀
x : K := ⋯.choose
hx_def : x = ⋯.choose
y : K := ⋯.choose
hy_def : y = ⋯.choose
hx : v x = embedding a
hy : v y = embedding b
this : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
ha0 : embedding a ≠ embedding 0
h0 : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
hab : v x = v y
⊢ ¬b = 0
Module: Mathlib.RingTheory.MvPowerSeries.Basic

Goal state before:
pp: case pos
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
s : σ
n : ℕ
φ : MvPowerSeries σ R
h : ∀ (m : σ →₀ ℕ), m s < n → (coeff m) φ = 0
m : σ →₀ ℕ
H : m - single s n + single s n = m
i j : σ →₀ ℕ
hij : (i, j).1 + (i, j).2 = m
hne : (i, j) ≠ (single s n, m - single s n)
hi : (i, j).1 = single s n
⊢ (1 * (coeff (i, j).2) fun m ↦ (coeff (m + single s n)) φ) = 0

Tactic:
exfalso
          apply hne
          rw [← hij, ← hi, Prod.mk_inj]
          refine ⟨rfl, ?_⟩
          ext t
          simp only [add_tsub_cancel_left]

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

Goal state before:
pp: R : Type u_2
inst✝ : CommSemiring R
ι : Type u_3
f : ι → ℕ
g : ι → R
s : Finset ι
⊢ ∏ i ∈ s, (monomial (f i)) (g i) = (monomial (∑ i ∈ s, f i)) (∏ i ∈ s, g i)

Tactic:
simpa using

Goal state after:
R : Type u_2
inst✝ : CommSemiring R
ι : Type u_3
f : ι → ℕ
g : ι → R
s : Finset ι
⊢ ∏ i ∈ s, (MvPowerSeries.monomial (single () (f i))) (g i) =
    (MvPowerSeries.monomial (∑ b ∈ s, single () (f b))) (∏ i ∈ s, g i)
Module: Mathlib.RingTheory.PowerSeries.Basic

Goal state before:
pp: R : Type u_2
inst✝ : CommSemiring R
m : ℕ
a : R
n : ℕ
⊢ (monomial m) a ^ n = (monomial (n * m)) (a ^ n)

Tactic:
simpa using

Goal state after:
R : Type u_2
inst✝ : CommSemiring R
m : ℕ
a : R
n : ℕ
⊢ (MvPowerSeries.monomial (single () m)) a ^ n = (MvPowerSeries.monomial (single () (n * m))) (a ^ n)
Module: Mathlib.RingTheory.MvPowerSeries.Basic

Goal state before:
pp: case pos
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
s : σ
n : ℕ
φ : MvPowerSeries σ R
h : ∀ (m : σ →₀ ℕ), m s < n → (coeff m) φ = 0
m : σ →₀ ℕ
H : n ≤ m s
t : σ
hst : s = t
⊢ (m - single s n + single s n) t = m t

Tactic:
subst t
          simpa using! tsub_add_cancel_of_le H

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

Goal state before:
pp: case h
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
x : (ofClass extensionValuation).ValueGroup₀
k' : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
hk' : (restrict₀ (ofClass extensionValuation)) k' = x
this : embedding ((restrict₀ (ofClass v)) ⋯.choose) = embedding (extension k')
⊢ valueGroup₀_hom_extensionValuation (extension k') = x

Tactic:
simpa using

Goal state after:
case h
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
x : (ofClass extensionValuation).ValueGroup₀
k' : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
hk' : (restrict₀ (ofClass extensionValuation)) k' = x
this : embedding ((restrict₀ (ofClass v)) ⋯.choose) = embedding (extension k')
⊢ v ⋯.choose = extensionValuation k'
Module: Mathlib.RingTheory.DedekindDomain.AdicValuation

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
hv : Irreducible (Associates.mk v.asIdeal)
hlt : v.asIdeal ^ 2 < v.asIdeal
⊢ ∃ π, v.intValuation π = exp (-1)

Tactic:
obtain ⟨π, mem, notMem⟩ := SetLike.exists_of_lt hlt

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
hv : Irreducible (Associates.mk v.asIdeal)
hlt : v.asIdeal ^ 2 < v.asIdeal
π : R
mem : π ∈ v.asIdeal
notMem : π ∉ v.asIdeal ^ 2
⊢ ∃ π, v.intValuation π = exp (-1)
Module: Mathlib.RingTheory.MvPowerSeries.Basic

Goal state before:
pp: σ : Type u_1
R : Type u_3
inst✝² : CommSemiring R
ι : Type u_4
inst✝¹ : DecidableEq ι
inst✝ : DecidableEq σ
f : ι → MvPowerSeries σ R
a : ι
s : Finset ι
ha : a ∉ s
ih : ∀ (d : σ →₀ ℕ), (coeff d) (∏ j ∈ s, f j) = ∑ l ∈ s.finsuppAntidiag d, ∏ i ∈ s, (coeff (l i)) (f i)
u v u' v' : σ →₀ ℕ
huv : u' + v' = u + v
h : u = u' → ¬v = v'
k l : ι →₀ σ →₀ ℕ
hkl : l.update a u' = k.update a u
⊢ u' = u

Tactic:
simpa using

Goal state after:
σ : Type u_1
R : Type u_3
inst✝² : CommSemiring R
ι : Type u_4
inst✝¹ : DecidableEq ι
inst✝ : DecidableEq σ
f : ι → MvPowerSeries σ R
a : ι
s : Finset ι
ha : a ∉ s
ih : ∀ (d : σ →₀ ℕ), (coeff d) (∏ j ∈ s, f j) = ∑ l ∈ s.finsuppAntidiag d, ∏ i ∈ s, (coeff (l i)) (f i)
u v u' v' : σ →₀ ℕ
huv : u' + v' = u + v
h : u = u' → ¬v = v'
k l : ι →₀ σ →₀ ℕ
hkl : l.update a u' = k.update a u
⊢ u' = u
Module: Mathlib.RingTheory.DedekindDomain.AdicValuation

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
π : v.intValuation.Uniformizer
⊢ v.intValuation ↑π.val = exp (-1)

Tactic:
simpa using

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
π : v.intValuation.Uniformizer
⊢ ↑(Valuation.IsRankOneDiscrete.generator v.intValuation) = (exp 1)⁻¹
Module: Mathlib.RingTheory.DedekindDomain.AdicValuation

Goal state before:
pp: case inr
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
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
ine : ∀ {r : R}, r ≠ 0 → Ideal.span {r} ≠ ⊥
v : Ideal R
hv✝ : Irreducible (Associates.mk v)
hv : Prime v
hv' : Irreducible (Associates.mk v)
h :
  -↑(Multiset.count ⟨Associates.mk v, hv'⟩ (Associates.factors' (Ideal.span {n}))) -
      -↑(Multiset.count ⟨Associates.mk v, hv'⟩ (Associates.factors' (Ideal.span {d}))) ≤
    0
⊢ Multiset.count ⟨Associates.mk v, hv✝⟩ (Associates.factors' (Ideal.span {d})) ≤
    Multiset.count ⟨Associates.mk v, hv✝⟩ (Associates.factors' (Ideal.span {n}))

Tactic:
simpa using

Goal state after:
case inr
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
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
ine : ∀ {r : R}, r ≠ 0 → Ideal.span {r} ≠ ⊥
v : Ideal R
hv✝ : Irreducible (Associates.mk v)
hv : Prime v
hv' : Irreducible (Associates.mk v)
h :
  -↑(Multiset.count ⟨Associates.mk v, hv'⟩ (Associates.factors' (Ideal.span {n}))) -
      -↑(Multiset.count ⟨Associates.mk v, hv'⟩ (Associates.factors' (Ideal.span {d}))) ≤
    0
⊢ Multiset.count ⟨Associates.mk v, hv✝⟩ (Associates.factors' (Ideal.span {d})) ≤
    Multiset.count ⟨Associates.mk v, hv✝⟩ (Associates.factors' (Ideal.span {n}))
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:
simpa using

Goal state after:
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
f : MvPowerSeries σ R
⊢ ¬f = 0 ↔ ∃ d, ¬(coeff d) f = 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
x : K
⊢ x ∈ (subalgebra.ofField K v.asIdeal.primeCompl ⋯).toSubring ∨
    x⁻¹ ∈ (subalgebra.ofField K v.asIdeal.primeCompl ⋯).toSubring

Tactic:
simpa using

Goal state after:
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 ⋯ ∨ x⁻¹ ∈ subalgebra.ofField K v.asIdeal.primeCompl ⋯
Module: Mathlib.RingTheory.MvPowerSeries.Order

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

Tactic:
simpa using

Goal state after:
case coe
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
f : MvPowerSeries σ R
a✝ : ℕ
h : ∀ (d : σ →₀ ℕ), ↑((weight w) d) < ↑a✝ → (coeff d) f = 0
⊢ ∀ (d : σ →₀ ℕ), (weight w) d < a✝ → (coeff d) f = 0
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:
simpa using

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

Goal state after:
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 = γ
Module: Mathlib.RingTheory.DedekindDomain.AdicValuation

Goal state before:
pp: case pos
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
a b : R
hv : v.intValuation b ≤ v.intValuation a
γ : Multiplicative ℤ
ha : a = 0
⊢ ∃ y, v.intValuation (b - y * a) < ↑γ

pp: case neg
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
a b : R
hv : v.intValuation b ≤ v.intValuation a
γ : Multiplicative ℤ
ha : ¬a = 0
⊢ ∃ y, v.intValuation (b - y * a) < ↑γ

Tactic:
· subst ha
    rw [map_zero, le_zero_iff] at hv
    exact ⟨0, by simp [hv]⟩

Goal state after:
case neg
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
a b : R
hv : v.intValuation b ≤ v.intValuation a
γ : Multiplicative ℤ
ha : ¬a = 0
⊢ ∃ y, v.intValuation (b - y * a) < ↑γ
Module: Mathlib.RingTheory.DedekindDomain.AdicValuation

Goal state before:
pp: case neg
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
a b : R
hv : v.intValuation b ≤ v.intValuation a
γ : Multiplicative ℤ
ha : ¬a = 0
hvaz : v.intValuation a ≠ 0
hγz : ↑γ ≠ 0
n : ℕ
hna : exp (-↑n) < v.intValuation a
hnγ : exp (-↑n) < ↑γ
hvn : emultiplicity v.asIdeal (Ideal.span {a}) ≤ ↑n
hb : b ∈ v.asIdeal ^ multiplicity v.asIdeal (Ideal.span {a})
hnz : Ideal.span {a} ≠ ⊥
⊢ ∃ a_1, v.intValuation (b - a_1 * a) ≤ exp (-↑n)

Tactic:
simpa using

Goal state after:
case neg
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
a b : R
hv : v.intValuation b ≤ v.intValuation a
γ : Multiplicative ℤ
ha : ¬a = 0
hvaz : v.intValuation a ≠ 0
hγz : ↑γ ≠ 0
n : ℕ
hna : exp (-↑n) < v.intValuation a
hnγ : exp (-↑n) < ↑γ
hvn : emultiplicity v.asIdeal (Ideal.span {a}) ≤ ↑n
hb : b ∈ v.asIdeal ^ multiplicity v.asIdeal (Ideal.span {a})
hnz : Ideal.span {a} ≠ ⊥
⊢ ∃ a_1, v.intValuation (b - a_1 * a) ≤ (exp ↑n)⁻¹
Module: Mathlib.RingTheory.MvPowerSeries.Trunc

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
s : Finset (σ →₀ ℕ)
p : MvPowerSeries σ R
x✝ : σ →₀ ℕ
⊢ x✝ ∉ s → x✝ ∉ ((truncFinset R s) p).support

Tactic:
simpa using

Goal state after:
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
s : Finset (σ →₀ ℕ)
p : MvPowerSeries σ R
x✝ : σ →₀ ℕ
⊢ x✝ ∉ s → MvPolynomial.coeff x✝ ((truncFinset R s) p) = 0
Module: Mathlib.RingTheory.MvPowerSeries.Trunc

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

Tactic:
simpa using

Goal state after:
σ : Type u_1
R : Type u_2
inst✝¹ : DecidableEq σ
inst✝ : CommSemiring R
n : σ →₀ ℕ
hnn : n ≠ 0
⊢ 0 < n
Module: Mathlib.RingTheory.MvPowerSeries.Trunc

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

Tactic:
simpa using

Goal state after:
σ : Type u_1
R : Type u_2
inst✝¹ : DecidableEq σ
inst✝ : CommSemiring R
n : σ →₀ ℕ
hnn : n ≠ 0
a : R
⊢ 0 < n
Module: Mathlib.RingTheory.MvPowerSeries.Order

Goal state before:
pp: σ : Type u_1
w : σ → ℕ
R : Type u_3
inst✝ : Ring R
f : MvPowerSeries σ R
h : weightedOrder w (-f) ≠ weightedOrder w f
⊢ f = 0

Tactic:
simpa using

Goal state after:
σ : Type u_1
w : σ → ℕ
R : Type u_3
inst✝ : Ring R
f : MvPowerSeries σ R
h : weightedOrder w (-f) ≠ weightedOrder w f
⊢ f = 0
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
⊢ ↑(degree 0) < f.order

Tactic:
simpa using

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

Goal state before:
pp: case mpr
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
f : MvPowerSeries σ R
h : constantCoeff f = 0
d : σ →₀ ℕ
hd : degree d = 0
⊢ (coeff d) f = 0

Tactic:
simp [(degree_eq_zero_iff d).mp hd, h]

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

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : Semiring R
f : MvPowerSeries σ R
n : ℕ
hf : constantCoeff f = 0
⊢ ↑n ≤ n • f.order

Tactic:
simpa using

Goal state after:
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
f : MvPowerSeries σ R
n : ℕ
hf : constantCoeff f = 0
⊢ ↑n ≤ ↑n * f.order
Module: Mathlib.RingTheory.MvPowerSeries.Order

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
f : MvPowerSeries σ R
p : ℕ
hf : IsWeightedHomogeneous w f p
d : σ →₀ ℕ
hd : (weight w) d ≠ p
⊢ (coeff d) f = 0

Tactic:
simpa using

Goal state after:
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
f : MvPowerSeries σ R
p : ℕ
hf : IsWeightedHomogeneous w f p
d : σ →₀ ℕ
hd : (weight w) d ≠ p
⊢ (coeff d) f = 0
Module: Mathlib.RingTheory.DedekindDomain.AdicValuation

Goal state before:
pp: case refine_1
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
s : Set (adicCompletion K v)
x✝ : ∃ t ∈ 𝓝 0, toCompletion ⁻¹' t ⊆ s
t : Set (HeightOneSpectrum.valuation K v).Completion
ht : t ∈ 𝓝 0
hts : toCompletion ⁻¹' t ⊆ s
δ : (ofClass Valued.v).ValueGroup₀ˣ
hδ : {x | Valued.v.restrict x < ↑δ} ⊆ t
x : adicCompletion K v
hx : (valuation K v).restrict x < ↑((Units.mapEquiv (valueGroupOrderIso K v).symm.toMulEquiv) δ)
⊢ Valued.v.restrict x.toCompletion < ↑δ

Tactic:
simpa using

Goal state after:
case refine_1
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
s : Set (adicCompletion K v)
x✝ : ∃ t ∈ 𝓝 0, toCompletion ⁻¹' t ⊆ s
t : Set (HeightOneSpectrum.valuation K v).Completion
ht : t ∈ 𝓝 0
hts : toCompletion ⁻¹' t ⊆ s
δ : (ofClass Valued.v).ValueGroup₀ˣ
hδ : {x | Valued.v.restrict x < ↑δ} ⊆ t
x : adicCompletion K v
hx : (valuation K v).restrict x < ↑((Units.mapEquiv (valueGroupOrderIso K v).symm.toMulEquiv) δ)
⊢ Valued.v.restrict x.toCompletion < ↑δ
Module: Mathlib.RingTheory.DedekindDomain.AdicValuation

Goal state before:
pp: case refine_2.refine_2
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
s : Set (adicCompletion K v)
x✝ : ∃ γ, {x | (valuation K v).restrict x < ↑γ} ⊆ s
γ : (ofClass (valuation K v)).ValueGroup₀ˣ
hγ : {x | (valuation K v).restrict x < ↑γ} ⊆ s
x : adicCompletion K v
hx : x ∈ toCompletion ⁻¹' {y | Valued.v.restrict y < ↑((Units.mapEquiv (valueGroupOrderIso K v).toMulEquiv) γ)}
⊢ Valued.v.restrict x.toCompletion < (valueGroupOrderIso K v) ↑γ

Tactic:
simpa using

Goal state after:
case refine_2.refine_2
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
s : Set (adicCompletion K v)
x✝ : ∃ γ, {x | (valuation K v).restrict x < ↑γ} ⊆ s
γ : (ofClass (valuation K v)).ValueGroup₀ˣ
hγ : {x | (valuation K v).restrict x < ↑γ} ⊆ s
x : adicCompletion K v
hx : x ∈ toCompletion ⁻¹' {y | Valued.v.restrict y < ↑((Units.mapEquiv (valueGroupOrderIso K v).toMulEquiv) γ)}
⊢ Valued.v.restrict x.toCompletion < (valueGroupOrderIso K v) ↑γ
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
n : (WithZero (Multiplicative ℤ))ˣ
x✝ : ∃ a, ¬(valuation K v) a = 0 ∧ ∃ x, (valuation K v) a * ↑n = (valuation K v) x
a : K
ha0 : ¬(valuation K v) a = 0
x : K
hx : (valuation K v) a * ↑n = (valuation K v) x
⊢ ¬Valued.v { toCompletion := ↑((WithVal.equiv (valuation K v)).symm a) } = 0

Tactic:
simpa using

Goal state after:
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
n : (WithZero (Multiplicative ℤ))ˣ
x✝ : ∃ a, ¬(valuation K v) a = 0 ∧ ∃ x, (valuation K v) a * ↑n = (valuation K v) x
a : K
ha0 : ¬(valuation K v) a = 0
x : K
hx : (valuation K v) a * ↑n = (valuation K v) x
⊢ ¬a = 0
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
n : (WithZero (Multiplicative ℤ))ˣ
x✝ : ∃ a, ¬(valuation K v) a = 0 ∧ ∃ x, (valuation K v) a * ↑n = (valuation K v) x
a : K
ha0 : ¬(valuation K v) a = 0
x : K
hx : (valuation K v) a * ↑n = (valuation K v) x
⊢ Valued.v { toCompletion := ↑((WithVal.equiv (valuation K v)).symm a) } * ↑n =
    Valued.v { toCompletion := ↑((WithVal.equiv (valuation K v)).symm x) }

Tactic:
simpa using

Goal state after:
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
n : (WithZero (Multiplicative ℤ))ˣ
x✝ : ∃ a, ¬(valuation K v) a = 0 ∧ ∃ x, (valuation K v) a * ↑n = (valuation K v) x
a : K
ha0 : ¬(valuation K v) a = 0
x : K
hx : (valuation K v) a * ↑n = (valuation K v) x
⊢ (valuation K v) a * ↑n = (valuation K v) x
Module: Mathlib.RingTheory.MvPowerSeries.Order

Goal state before:
pp: case pos.inr.inr
σ : 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 : σ →₀ ℕ
x : (σ →₀ ℕ) × (σ →₀ ℕ)
hd : (weight w) x.1 + (weight w) x.2 = p + q
hx : x.1 + x.2 = d
h : (weight w) x.2 < q
⊢ (coeff x.1) f * (coeff x.2) g =
    (if (weight w) x.1 = p then (coeff x.1) f else 0) * if (weight w) x.2 = q then (coeff x.2) g else 0

Tactic:
rw [if_neg (ne_of_lt h), mul_zero]
      rw [← ENat.natCast_lt_natCast] at h
      rw [coeff_eq_zero_of_lt_weightedOrder w (lt_of_lt_of_le h hg), mul_zero]

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
⊢ d < d + Finsupp.single s 1

Tactic:
simpa using

Goal state after:
σ : 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
⊢ ∃ i, 0 < (Finsupp.single s 1) i
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:
simpa using

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, d = Finsupp.single x' 1 → 1 = 0
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
r : R
⊢ Valued.v ((WithVal.equiv (valuation K v)).symm ((algebraMap R K) r)) ≤ 1

Tactic:
simpa using

Goal state after:
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
r : R
⊢ (valuation K v) ((algebraMap R K) r) ≤ 1
Module: Mathlib.RingTheory.PowerSeries.Order

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
φ : R⟦X⟧
⊢ φ.order = ⊤ ↔ φ = 0

Tactic:
simpa using

Goal state after:
R : Type u_1
inst✝ : Semiring R
φ : R⟦X⟧
⊢ φ.order = ⊤ ↔ φ = 0
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

Tactic:
simpa using

Goal state after:
R : Type u_1
inst✝ : Semiring R
φ : R⟦X⟧
n : ℕ
h : (coeff n) φ ≠ 0
⊢ ∃ m ≤ n, ¬(coeff m) φ = 0
Module: Mathlib.RingTheory.MvPowerSeries.PiTopology

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝¹ : TopologicalSpace R
inst✝ : Semiring R
f : MvPowerSeries σ R
h : constantCoeff f = 0
n m : ℕ
hm : n + 1 ≤ m
⊢ ↑m ≤ m • f.order

Tactic:
simpa using

Goal state after:
σ : Type u_1
R : Type u_2
inst✝¹ : TopologicalSpace R
inst✝ : Semiring R
f : MvPowerSeries σ R
h : constantCoeff f = 0
n m : ℕ
hm : n + 1 ≤ m
⊢ ↑m ≤ ↑m * f.order
Module: Mathlib.RingTheory.PowerSeries.Order

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

Tactic:
simpa using

Goal state after:
case top
R : Type u_1
inst✝ : Semiring R
φ : R⟦X⟧
h : ∀ (i : ℕ), ↑i < ⊤ → (coeff i) φ = 0
⊢ φ = 0