mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.DedekindDomain.AdicValuation

Goal state before:
pp: case h
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}
⊢ (algebraMap R K) z = IsLocalization.mk' K (d * z) ⟨d, hd⟩

Tactic:
exact (hx.resolve_right fun h => by simp [hd0] at h).symm

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

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
d : PUnit.{1} →₀ ℕ
r : R
⊢ (single () (d ())) default = d default
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
h : (valuation K { asIdeal := v, isPrime := ⋯, ne_bot := ⋯ }) (IsLocalization.mk' K n ⟨d, hd⟩) ≤ 1
hv' : Irreducible (Associates.mk v)
⊢ Multiset.count ⟨Associates.mk v, hv✝⟩ (Associates.factors' (Ideal.span {d})) ≤
    Multiset.count ⟨Associates.mk v, hv✝⟩ (Associates.factors' (Ideal.span {n}))

Tactic:
valuation_of_mk',

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 :
  { asIdeal := v, isPrime := ⋯, ne_bot := ⋯ }.intValuation n /
      { asIdeal := v, isPrime := ⋯, ne_bot := ⋯ }.intValuation d ≤
    1
⊢ 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.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:
simp_all [Valuation.isEquiv_iff_val_lt_one, HeightOneSpectrum.ext_iff, Ideal.ext_iff,
    ← valuation_lt_one_iff_mem (K := K)]

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

Goal state before:
pp: case e'_5
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)
x✝¹ : (ofClass v).ValueGroup₀ˣ
x✝ : K
⊢ v x✝ < ↑embedding ↑x✝¹ ↔ v x✝ < embedding ↑x✝¹

Tactic:
;

Goal state after:
case e'_5
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)
x✝¹ : (ofClass v).ValueGroup₀ˣ
x✝ : K
⊢ v x✝ < ↑embedding ↑x✝¹ ↔ v x✝ < embedding ↑x✝¹
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:
rwa [division_def (a : K) s] at this

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

Goal state after:
σ : 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)
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 ≠ ⊤

Tactic:
;

Goal state after:
σ : 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 ≠ ⊤
Module: Mathlib.RingTheory.MvPowerSeries.Basic

Goal state before:
pp: case neg
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n : σ →₀ ℕ
a : R
h₂ : ¬n = n
⊢ a = 0

Tactic:
;

Goal state after:
case neg
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n : σ →₀ ℕ
a : R
h₂ : ¬n = n
⊢ a = 0
Module: Mathlib.RingTheory.MvPowerSeries.Basic

Goal state before:
pp: case pos
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n : σ →₀ ℕ
a : R
h₁ : ¬n = n
⊢ 0 = a

Tactic:
;

Goal state after:
case pos
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n : σ →₀ ℕ
a : R
h₁ : ¬n = n
⊢ 0 = a
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).IsNontrivial

Tactic:
;

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
⊢ (valuation K v).IsNontrivial
Module: Mathlib.RingTheory.MvPowerSeries.Order

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

Tactic:
;

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

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.Trunc

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
s : Finset (σ →₀ ℕ)
x : σ →₀ ℕ
r : R
h : x ∉ s
m✝ : σ →₀ ℕ
⊢ MvPolynomial.coeff m✝ ((truncFinset R s) ((monomial x) r)) = MvPolynomial.coeff m✝ 0

Tactic:
;

Goal state after:
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
s : Finset (σ →₀ ℕ)
x : σ →₀ ℕ
r : R
h : x ∉ s
m✝ : σ →₀ ℕ
⊢ MvPolynomial.coeff m✝ ((truncFinset R s) ((monomial x) r)) = MvPolynomial.coeff m✝ 0
Module: Mathlib.Data.Finsupp.Interval

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝² : Lattice α
inst✝¹ : Zero α
inst✝ : LocallyFiniteOrder α
f g : ι →₀ α
⊢ #(uIcc f g) = ∏ i ∈ (f ⊓ g).support ∪ (f ⊔ g).support, #(uIcc (f i) (g i))

Tactic:
;

Goal state after:
ι : Type u_1
α : Type u_2
inst✝² : Lattice α
inst✝¹ : Zero α
inst✝ : LocallyFiniteOrder α
f g : ι →₀ α
⊢ #(uIcc f g) = ∏ i ∈ (f ⊓ g).support ∪ (f ⊔ g).support, #(uIcc (f i) (g i))
Module: Mathlib.RingTheory.MvPowerSeries.Order

Goal state before:
pp: case inr
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
f g : MvPowerSeries σ R
h : weightedOrder w f ≠ weightedOrder w g
this :
  ∀ {σ : Type u_1} {R : Type u_2} [inst : Semiring R] (w : σ → ℕ) {f g : MvPowerSeries σ R},
    weightedOrder w f ≠ weightedOrder w g →
      weightedOrder w f < weightedOrder w g → weightedOrder w (f + g) ≤ min (weightedOrder w f) (weightedOrder w g)
H₁ : ¬weightedOrder w f < weightedOrder w g
⊢ weightedOrder w (g + f) ≤ min (weightedOrder w f) (weightedOrder w g)

Tactic:
inf_comm

Goal state after:
case inr
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
f g : MvPowerSeries σ R
h : weightedOrder w f ≠ weightedOrder w g
this :
  ∀ {σ : Type u_1} {R : Type u_2} [inst : Semiring R] (w : σ → ℕ) {f g : MvPowerSeries σ R},
    weightedOrder w f ≠ weightedOrder w g →
      weightedOrder w f < weightedOrder w g → weightedOrder w (f + g) ≤ min (weightedOrder w f) (weightedOrder w g)
H₁ : ¬weightedOrder w f < weightedOrder w g
⊢ weightedOrder w (g + f) ≤ min (weightedOrder w g) (weightedOrder w f)
Module: Mathlib.RingTheory.MvPowerSeries.Trunc

Goal state before:
pp: case succ
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
s : Finset (σ →₀ ℕ)
hs : IsLowerSet ↑s
k : ℕ
p : MvPowerSeries σ R
n : ℕ
hmn : 1 ≤ n
ih : (truncFinset R s) (↑((truncFinset R s) p) ^ n) = (truncFinset R s) (p ^ n)
x : σ →₀ ℕ
⊢ MvPolynomial.coeff x ((truncFinset R s) (↑((truncFinset R s) p) ^ (n + 1))) =
    MvPolynomial.coeff x ((truncFinset R s) (p ^ (n + 1)))

Tactic:
;

Goal state after:
case succ
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
s : Finset (σ →₀ ℕ)
hs : IsLowerSet ↑s
k : ℕ
p : MvPowerSeries σ R
n : ℕ
hmn : 1 ≤ n
ih : (truncFinset R s) (↑((truncFinset R s) p) ^ n) = (truncFinset R s) (p ^ n)
x : σ →₀ ℕ
⊢ MvPolynomial.coeff x ((truncFinset R s) (↑((truncFinset R s) p) ^ (n + 1))) =
    MvPolynomial.coeff x ((truncFinset R s) (p ^ (n + 1)))
Module: Mathlib.RingTheory.MvPowerSeries.Order

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

Tactic:
by
  induction n with
  | zero => simp
  | succ n hn => grw [succ_nsmul, pow_succ, hn, le_weightedOrder_mul]

Goal state after:
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✝ ∈ ((truncFinset R s) p).support → x✝ ∈ s

Tactic:
;

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

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝¹ : DecidableEq σ
inst✝ : CommSemiring R
n : σ →₀ ℕ
a : R
p : MvPowerSeries σ R
m : σ →₀ ℕ
⊢ MvPolynomial.coeff m ((trunc R n) (C a * p)) = MvPolynomial.coeff m (MvPolynomial.C a * (trunc R n) p)

Tactic:
;

Goal state after:
σ : Type u_1
R : Type u_2
inst✝¹ : DecidableEq σ
inst✝ : CommSemiring R
n : σ →₀ ℕ
a : R
p : MvPowerSeries σ R
m : σ →₀ ℕ
⊢ MvPolynomial.coeff m ((trunc R n) (C a * p)) = MvPolynomial.coeff m (MvPolynomial.C a * (trunc R n) p)
Module: Mathlib.RingTheory.MvPowerSeries.Trunc

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝¹ : DecidableEq σ
inst✝ : CommSemiring R
n : σ →₀ ℕ
k : ℕ
hk : 1 ≤ k
φ : MvPowerSeries σ R
a✝ : σ →₀ ℕ
⊢ ∀ ⦃b : σ →₀ ℕ⦄, b ≤ a✝ → a✝ ∈ ↑(Iic n) → b ∈ ↑(Iic n)

Tactic:
;

Goal state after:
σ : Type u_1
R : Type u_2
inst✝¹ : DecidableEq σ
inst✝ : CommSemiring R
n : σ →₀ ℕ
k : ℕ
hk : 1 ≤ k
φ : MvPowerSeries σ R
a✝ : σ →₀ ℕ
⊢ ∀ ⦃b : σ →₀ ℕ⦄, b ≤ a✝ → a✝ ∈ ↑(Iic n) → b ∈ ↑(Iic n)
Module: Mathlib.RingTheory.MvPowerSeries.Trunc

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝¹ : DecidableEq σ
inst✝ : CommSemiring R
n : σ →₀ ℕ
a : R
p : MvPowerSeries σ R
m : σ →₀ ℕ
⊢ MvPolynomial.coeff m ((trunc' R n) (C a * p)) = MvPolynomial.coeff m (MvPolynomial.C a * (trunc' R n) p)

Tactic:
;

Goal state after:
σ : Type u_1
R : Type u_2
inst✝¹ : DecidableEq σ
inst✝ : CommSemiring R
n : σ →₀ ℕ
a : R
p : MvPowerSeries σ R
m : σ →₀ ℕ
⊢ MvPolynomial.coeff m ((trunc' R n) (C a * p)) = MvPolynomial.coeff m (MvPolynomial.C a * (trunc' R n) 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
⊢ Subgroup.closure (Units.val ⁻¹' Set.range ⇑(Valuation.comap (↑(equiv K v)) Valued.v)) =
    Subgroup.closure (Units.val ⁻¹' Set.range (⇑Valued.v ∘ toCompletion))

Tactic:
;

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
⊢ Subgroup.closure (Units.val ⁻¹' Set.range ⇑(Valuation.comap (↑(equiv K v)) Valued.v)) =
    Subgroup.closure (Units.val ⁻¹' Set.range (⇑Valued.v ∘ toCompletion))
Module: Mathlib.Topology.Instances.ENat

Goal state before:
pp: α : Type u_1
l : Filter α
f : α → ℕ∞
⊢ Tendsto f l (⨅ l, ⨅ (_ : l ≠ ⊤), 𝓟 (Ioi l)) ↔ ∀ (n : ℕ), ∀ᶠ (a : α) in l, ↑n < f a

Tactic:
tendsto_iInf,

Goal state after:
α : Type u_1
l : Filter α
f : α → ℕ∞
⊢ (∀ (i : ℕ∞), i ≠ ⊤ → Tendsto f l (𝓟 (Ioi i))) ↔ ∀ (n : ℕ), ∀ᶠ (a : α) in l, ↑n < f a
Module: Mathlib.RingTheory.MvPowerSeries.Trunc

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

Tactic:
;

Goal state after:
σ : Type u_1
R : Type u_2
n : ℕ
inst✝¹ : Finite σ
inst✝ : CommSemiring R
⊢ n ≠ 0 → 0 ∈ ⋯.toFinset
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:
;

Goal state after:
σ : Type u_1
R : Type u_2
n : ℕ
inst✝¹ : Finite σ
inst✝ : CommSemiring R
⊢ 0 ∉ ⋯.toFinset → n = 0
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✝¹
⊢ degree x✝¹ < n → degree x✝ < n

Tactic:
;

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
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
x : adicCompletion K v
⊢ (valuation K v) x = Valued.v x.toCompletion

Tactic:
;

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
x : adicCompletion K v
⊢ (valuation K v) x = Valued.v x.toCompletion
Module: Mathlib.RingTheory.MvPowerSeries.Order

Goal state before:
pp: case pos
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
f : MvPowerSeries σ R
p : ℕ
hf : ↑p < weightedOrder w f
d : σ →₀ ℕ
hd : (weight w) d = p
⊢ ↑((weight w) d) < weightedOrder w f

Tactic:
rw [hd]

Goal state after:
case pos
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
f : MvPowerSeries σ R
p : ℕ
hf : ↑p < weightedOrder w f
d : σ →₀ ℕ
hd : (weight w) d = p
⊢ ↑p < weightedOrder w f
Module: Mathlib.RingTheory.DedekindDomain.AdicValuation

Goal state before:
pp: case ofCompletion
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
y : adicCompletion K v
toCompletion✝ : (HeightOneSpectrum.valuation K v).Completion
h : { toCompletion := toCompletion✝ }.toCompletion = y.toCompletion
⊢ { toCompletion := toCompletion✝ } = y

Tactic:
;

Goal state after:
case ofCompletion
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
y : adicCompletion K v
toCompletion✝ : (HeightOneSpectrum.valuation K v).Completion
h : { toCompletion := toCompletion✝ }.toCompletion = y.toCompletion
⊢ { toCompletion := toCompletion✝ } = y
Module: Mathlib.RingTheory.DedekindDomain.AdicValuation

Goal state before:
pp: case ofCompletion.ofCompletion
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✝¹ toCompletion✝ : (HeightOneSpectrum.valuation K v).Completion
h : { toCompletion := toCompletion✝¹ }.toCompletion = { toCompletion := toCompletion✝ }.toCompletion
⊢ { toCompletion := toCompletion✝¹ } = { toCompletion := toCompletion✝ }

Tactic:
;

Goal state after:
case ofCompletion.ofCompletion
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✝¹ toCompletion✝ : (HeightOneSpectrum.valuation K v).Completion
h : { toCompletion := toCompletion✝¹ }.toCompletion = { toCompletion := toCompletion✝ }.toCompletion
⊢ { toCompletion := toCompletion✝¹ } = { toCompletion := toCompletion✝ }
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:
;

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

Tactic:
;

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
⊢ { toCompletion := ↑((WithVal.equiv (HeightOneSpectrum.valuation K v)).symm 1) }.toCompletion = toCompletion 1
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 y : K
⊢ { toCompletion := ↑((WithVal.equiv (HeightOneSpectrum.valuation K v)).symm (x + y)) }.toCompletion =
    ({ toCompletion := ↑((WithVal.equiv (HeightOneSpectrum.valuation K v)).symm x) } +
        { toCompletion := ↑((WithVal.equiv (HeightOneSpectrum.valuation K v)).symm y) }).toCompletion

Tactic:
;

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
x y : K
⊢ { toCompletion := ↑((WithVal.equiv (HeightOneSpectrum.valuation K v)).symm (x + y)) }.toCompletion =
    ({ toCompletion := ↑((WithVal.equiv (HeightOneSpectrum.valuation K v)).symm x) } +
        { toCompletion := ↑((WithVal.equiv (HeightOneSpectrum.valuation K v)).symm y) }).toCompletion
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 y : K
⊢ { toCompletion := ↑((WithVal.equiv (HeightOneSpectrum.valuation K v)).symm (x * y)) }.toCompletion =
    ({ toCompletion := ↑((WithVal.equiv (HeightOneSpectrum.valuation K v)).symm x) } *
        { toCompletion := ↑((WithVal.equiv (HeightOneSpectrum.valuation K v)).symm y) }).toCompletion

Tactic:
;

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
x y : K
⊢ { toCompletion := ↑((WithVal.equiv (HeightOneSpectrum.valuation K v)).symm (x * y)) }.toCompletion =
    ({ toCompletion := ↑((WithVal.equiv (HeightOneSpectrum.valuation K v)).symm x) } *
        { toCompletion := ↑((WithVal.equiv (HeightOneSpectrum.valuation K v)).symm y) }).toCompletion
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, ¬Valued.v a = 0 ∧ ∃ x, Valued.v a * ↑n = Valued.v x
a : adicCompletion K v
ha0 : ¬Valued.v a = 0
x : adicCompletion K v
hx : Valued.v a * ↑n = Valued.v x
b : K
hb : (valuation K v) b = Valued.v a
y : K
hy : (valuation K v) y = Valued.v x
⊢ ¬Valued.v a = 0

Tactic:
;

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, ¬Valued.v a = 0 ∧ ∃ x, Valued.v a * ↑n = Valued.v x
a : adicCompletion K v
ha0 : ¬Valued.v a = 0
x : adicCompletion K v
hx : Valued.v a * ↑n = Valued.v x
b : K
hb : (valuation K v) b = Valued.v a
y : K
hy : (valuation K v) y = Valued.v x
⊢ ¬Valued.v 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, ¬Valued.v a = 0 ∧ ∃ x, Valued.v a * ↑n = Valued.v x
a : adicCompletion K v
ha0 : ¬Valued.v a = 0
x : adicCompletion K v
hx : Valued.v a * ↑n = Valued.v x
b : K
hb : (valuation K v) b = Valued.v a
y : K
hy : (valuation K v) y = Valued.v x
⊢ Valued.v a * ↑n = Valued.v x

Tactic:
;

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, ¬Valued.v a = 0 ∧ ∃ x, Valued.v a * ↑n = Valued.v x
a : adicCompletion K v
ha0 : ¬Valued.v a = 0
x : adicCompletion K v
hx : Valued.v a * ↑n = Valued.v x
b : K
hb : (valuation K v) b = Valued.v a
y : K
hy : (valuation K v) y = Valued.v x
⊢ Valued.v a * ↑n = Valued.v x
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:
;

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