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
v : HeightOneSpectrum R
x y : R
hx : ¬x = 0
hy : ¬y = 0
hxy : ¬x + y = 0
nmin : ℕ :=
  min ((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {x})).factors)
    ((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {y})).factors)
h_dvd_x : x ∈ v.asIdeal ^ nmin
⊢ nmin ≤ (Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {y})).factors

pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
x y : R
hx : ¬x = 0
hy : ¬y = 0
hxy : ¬x + y = 0
nmin : ℕ :=
  min ((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {x})).factors)
    ((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {y})).factors)
h_dvd_x : x ∈ v.asIdeal ^ nmin
⊢ Irreducible (Associates.mk v.asIdeal)

Tactic:
]

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
x y : R
hx : ¬x = 0
hy : ¬y = 0
hxy : ¬x + y = 0
nmin : ℕ :=
  min ((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {x})).factors)
    ((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {y})).factors)
h_dvd_x : x ∈ v.asIdeal ^ nmin
⊢ nmin ≤ (Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {y})).factors

R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
x y : R
hx : ¬x = 0
hy : ¬y = 0
hxy : ¬x + y = 0
nmin : ℕ :=
  min ((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {x})).factors)
    ((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {y})).factors)
h_dvd_x : x ∈ v.asIdeal ^ nmin
⊢ Irreducible (Associates.mk v.asIdeal)
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 i j : σ →₀ ℕ
a✝ : (i, j) ∈ antidiagonal n
⊢ f ((coeff (i, j).1) φ) * f ((coeff (i, j).2) ψ) =
    ((coeff (i, j).1) fun n ↦ f ((coeff n) φ)) * (coeff (i, j).2) fun n ↦ f ((coeff n) ψ)

Tactic:
]

Goal state after:
σ : 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 i j : σ →₀ ℕ
a✝ : (i, j) ∈ antidiagonal n
⊢ f ((coeff (i, j).1) φ) * f ((coeff (i, j).2) ψ) =
    ((coeff (i, j).1) fun n ↦ f ((coeff n) φ)) * (coeff (i, j).2) fun n ↦ f ((coeff n) ψ)
Module: Mathlib.RingTheory.PowerSeries.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
a : R
f g : R⟦X⟧
n✝ : ℕ
⊢ ∑ i ∈ antidiagonal n✝, a ^ n✝ * ((coeff i.1) f * (coeff i.2) g) =
    ∑ p ∈ antidiagonal n✝, (coeff p.1) (mk fun n ↦ a ^ n * (coeff n) f) * (coeff p.2) (mk fun n ↦ a ^ n * (coeff n) g)

Tactic:
]

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
a : R
f g : R⟦X⟧
n✝ : ℕ
⊢ ∑ i ∈ antidiagonal n✝, a ^ n✝ * ((coeff i.1) f * (coeff i.2) g) =
    ∑ p ∈ antidiagonal n✝, (coeff p.1) (mk fun n ↦ a ^ n * (coeff n) f) * (coeff p.2) (mk fun n ↦ a ^ n * (coeff n) g)
Module: Mathlib.RingTheory.DedekindDomain.AdicValuation

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
x y : R
hx : ¬x = 0
hy : ¬y = 0
hxy : ¬x + y = 0
nmin : ℕ :=
  min ((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {x})).factors)
    ((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {y})).factors)
h_dvd_x : x ∈ v.asIdeal ^ nmin
h_dvd_y : y ∈ v.asIdeal ^ nmin
⊢ x + y ∈ v.asIdeal ^ nmin

Tactic:
]

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
x y : R
hx : ¬x = 0
hy : ¬y = 0
hxy : ¬x + y = 0
nmin : ℕ :=
  min ((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {x})).factors)
    ((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {y})).factors)
h_dvd_x : x ∈ v.asIdeal ^ nmin
h_dvd_y : y ∈ v.asIdeal ^ nmin
⊢ x + y ∈ v.asIdeal ^ nmin
Module: Mathlib.RingTheory.MvPowerSeries.Basic

Goal state before:
pp: case mp
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
s : σ
n : ℕ
φ : MvPowerSeries σ R
m : σ →₀ ℕ
h : m s < n
⊢ 0 = 0

pp: case mp
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
s : σ
n : ℕ
φ : MvPowerSeries σ R
m : σ →₀ ℕ
h : m s < n
⊢ ∀ x ∈ antidiagonal m, (coeff x.1) (X s ^ n) * (coeff x.2) φ = 0

Tactic:
]

Goal state after:
case mp
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
s : σ
n : ℕ
φ : MvPowerSeries σ R
m : σ →₀ ℕ
h : m s < n
⊢ ∀ x ∈ antidiagonal m, (coeff x.1) (X s ^ n) * (coeff x.2) φ = 0
Module: Mathlib.RingTheory.PowerSeries.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
a : R
f g : R⟦X⟧
n✝ b c : ℕ
H : b + c = n✝
⊢ a ^ b * (coeff b) f * (a ^ c * (coeff c) g) = a ^ b * (coeff b) f * (a ^ c * (coeff c) g)

Tactic:
]

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

Goal state before:
pp: case mp
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
s : σ
n : ℕ
φ : MvPowerSeries σ R
m : σ →₀ ℕ
h : m s < n
i j : σ →₀ ℕ
hij : (i, j) ∈ antidiagonal m
⊢ 0 = 0

pp: case mp.hnc
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
s : σ
n : ℕ
φ : MvPowerSeries σ R
m : σ →₀ ℕ
h : m s < n
i j : σ →₀ ℕ
hij : (i, j) ∈ antidiagonal m
⊢ ¬(i, j).1 = single s n

Tactic:
]

Goal state after:
case mp.hnc
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
s : σ
n : ℕ
φ : MvPowerSeries σ R
m : σ →₀ ℕ
h : m s < n
i j : σ →₀ ℕ
hij : (i, j) ∈ antidiagonal m
⊢ ¬(i, j).1 = single s n
Module: Mathlib.RingTheory.MvPowerSeries.Basic

Goal state before:
pp: case mp.hnc
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
s : σ
n : ℕ
φ : MvPowerSeries σ R
m j : σ →₀ ℕ
hij : (single s n, j).1 + (single s n, j).2 = m
⊢ n ≤ m s

Tactic:
]

Goal state after:
case mp.hnc
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
s : σ
n : ℕ
φ : MvPowerSeries σ R
m j : σ →₀ ℕ
hij : (single s n, j).1 + (single s n, j).2 = m
⊢ n ≤ m s
Module: Mathlib.RingTheory.DedekindDomain.AdicValuation

Goal state before:
pp: case neg
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
x y : R
hx : ¬x = 0
hy : ¬y = 0
hxy : ¬x + y = 0
nmin : ℕ :=
  min ((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {x})).factors)
    ((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {y})).factors)
h_dvd_x : x ∈ v.asIdeal ^ nmin
h_dvd_y : y ∈ v.asIdeal ^ nmin
h_dvd_xy : nmin ≤ (Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {x + y})).factors
⊢ nmin ≤ (Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {x + y})).factors

pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
x y : R
hx : ¬x = 0
hy : ¬y = 0
hxy : ¬x + y = 0
nmin : ℕ :=
  min ((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {x})).factors)
    ((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {y})).factors)
h_dvd_x : x ∈ v.asIdeal ^ nmin
h_dvd_y : y ∈ v.asIdeal ^ nmin
h_dvd_xy : Associates.mk v.asIdeal ^ nmin ≤ Associates.mk (Ideal.span {x + y})
⊢ Irreducible (Associates.mk v.asIdeal)

Tactic:
]

Goal state after:
case neg
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
x y : R
hx : ¬x = 0
hy : ¬y = 0
hxy : ¬x + y = 0
nmin : ℕ :=
  min ((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {x})).factors)
    ((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {y})).factors)
h_dvd_x : x ∈ v.asIdeal ^ nmin
h_dvd_y : y ∈ v.asIdeal ^ nmin
h_dvd_xy : nmin ≤ (Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {x + y})).factors
⊢ nmin ≤ (Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {x + y})).factors

R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
x y : R
hx : ¬x = 0
hy : ¬y = 0
hxy : ¬x + y = 0
nmin : ℕ :=
  min ((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {x})).factors)
    ((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {y})).factors)
h_dvd_x : x ∈ v.asIdeal ^ nmin
h_dvd_y : y ∈ v.asIdeal ^ nmin
h_dvd_xy : Associates.mk v.asIdeal ^ nmin ≤ Associates.mk (Ideal.span {x + y})
⊢ Irreducible (Associates.mk v.asIdeal)
Module: Mathlib.RingTheory.MvPowerSeries.Basic

Goal state before:
pp: case mp.hnc
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
s : σ
n : ℕ
φ : MvPowerSeries σ R
m j : σ →₀ ℕ
hij : (single s n, j).1 + (single s n, j).2 = m
⊢ n ≤ n + (single s n, j).2 s

Tactic:
]

Goal state after:
case mp.hnc
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
s : σ
n : ℕ
φ : MvPowerSeries σ R
m j : σ →₀ ℕ
hij : (single s n, j).1 + (single s n, j).2 = m
⊢ n ≤ n + (single s n, j).2 s
Module: Mathlib.RingTheory.DedekindDomain.AdicValuation

Goal state before:
pp: case neg
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
x y : R
hx : ¬x = 0
⊢ v.intValuationDef (x + y) ≤ max (v.intValuationDef x) (v.intValuationDef y)

Tactic:
by_cases hy : y = 0
    · rw [hy, add_zero]
      order
    · by_cases hxy : x + y = 0
      · rw [intValuationDef, if_pos hxy]; exact zero_le
      · rw [v.intValuationDef_if_neg hxy, v.intValuationDef_if_neg hx, v.intValuationDef_if_neg hy,
          le_max_iff]
        simp only [exp_le_exp, neg_le_neg_iff, Nat.cast_le, ← min_le_iff]
        set nmin :=
          min ((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {x})).factors)
            ((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {y})).factors)
        have h_dvd_x : x ∈ v.asIdeal ^ nmin := by
          rw [← Associates.le_singleton_iff x nmin _,
            Associates.prime_pow_dvd_iff_le (Associates.mk_ne_zero'.mpr hx) _]
          · exact min_le_left _ _
          exact v.associates_irreducible
        have h_dvd_y : y ∈ v.asIdeal ^ nmin := by
          rw [← Associates.le_singleton_iff y nmin _,
            Associates.prime_pow_dvd_iff_le (Associates.mk_ne_zero'.mpr hy) _]
          · exact min_le_right _ _
          exact v.associates_irreducible
        have h_dvd_xy : Associates.mk v.asIdeal ^ nmin ≤ Associates.mk (Ideal.span {x + y}) := by
          rw [Associates.le_singleton_iff]
          exact Ideal.add_mem (v.asIdeal ^ nmin) h_dvd_x h_dvd_y
        rw [Associates.prime_pow_dvd_iff_le (Associates.mk_ne_zero'.mpr hxy) _] at h_dvd_xy
        · exact h_dvd_xy
        exact v.associates_irreducible

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

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
f : ℕ → R
a : R
n✝ : ℕ
⊢ a ^ n✝ * f n✝ = a ^ n✝ * f n✝

Tactic:
]

Goal state after:
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
⊢ (coeff m) φ =
    (coeff (single s n, m - single s n).1) (X s ^ n) *
      (coeff (single s n, m - single s n).2) fun m ↦ (coeff (m + single s n)) φ

pp: case pos.h₀
σ : 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
⊢ ∀ b ∈ antidiagonal m,
    b ≠ (single s n, m - single s n) → ((coeff b.1) (X s ^ n) * (coeff b.2) fun m ↦ (coeff (m + single s n)) φ) = 0

pp: case pos.h₁
σ : 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
⊢ (single s n, m - single s n) ∉ antidiagonal m →
    ((coeff (single s n, m - single s n).1) (X s ^ n) *
        (coeff (single s n, m - single s n).2) fun m ↦ (coeff (m + single s n)) φ) =
      0

Tactic:
]

Goal state after:
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
⊢ (coeff m) φ =
    (coeff (single s n, m - single s n).1) (X s ^ n) *
      (coeff (single s n, m - single s n).2) fun m ↦ (coeff (m + single s n)) φ

case pos.h₀
σ : 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
⊢ ∀ b ∈ antidiagonal m,
    b ≠ (single s n, m - single s n) → ((coeff b.1) (X s ^ n) * (coeff b.2) fun m ↦ (coeff (m + single s n)) φ) = 0

case pos.h₁
σ : 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
⊢ (single s n, m - single s n) ∉ antidiagonal m →
    ((coeff (single s n, m - single s n).1) (X s ^ n) *
        (coeff (single s n, m - single s n).2) fun m ↦ (coeff (m + single s n)) φ) =
      0
Module: Mathlib.RingTheory.PowerSeries.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
f : R⟦X⟧
a b : R
n : ℕ
⊢ b ^ n * (a ^ n * (coeff n) f) = b ^ n * (a ^ n * (coeff n) f)

Tactic:
]

Goal state after:
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
⊢ (coeff m) φ = (coeff (single s n, m - single s n).2) fun m ↦ (coeff (m + single s n)) φ

Tactic:
]

Goal state after:
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
⊢ (coeff m) φ = (coeff (single s n, m - single s n).2) fun m ↦ (coeff (m + single s n)) φ
Module: Mathlib.RingTheory.DedekindDomain.AdicValuation

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
r : R
hr : r ≠ 0
hsr : Ideal.span {r} ≠ 0
hfm : FiniteMultiplicity v.asIdeal (Ideal.span {r})
⊢ ↑(Multiset.count v.asIdeal (UniqueFactorizationMonoid.normalizedFactors (Ideal.span {r}))) =
    ↑(Multiset.count v.asIdeal (UniqueFactorizationMonoid.normalizedFactors (Ideal.span {r})))

Tactic:
]

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

Goal state before:
pp: case pos.h₀
σ : 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)
⊢ ((coeff (i, j).1) (X s ^ n) * (coeff (i, j).2) fun m ↦ (coeff (m + single s n)) φ) = 0

Tactic:
]

Goal state after:
case pos.h₀
σ : 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)
⊢ ((coeff (i, j).1) (X s ^ n) * (coeff (i, j).2) fun m ↦ (coeff (m + single s n)) φ) = 0
Module: Mathlib.RingTheory.DedekindDomain.AdicValuation

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
x : R
hx : x ≠ 0
⊢ exp (-↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {x})).factors)) ≠ 0

Tactic:
]

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
x : R
hx : x ≠ 0
⊢ exp (-↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {x})).factors)) ≠ 0
Module: Mathlib.RingTheory.MvPowerSeries.Basic

Goal state before:
pp: case pos.h₀
σ : 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)
⊢ ((if (i, j).1 = single s n then 1 else 0) * (coeff (i, j).2) fun m ↦ (coeff (m + single s n)) φ) = 0

Tactic:
]

Goal state after:
case pos.h₀
σ : 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)
⊢ ((if (i, j).1 = single s n then 1 else 0) * (coeff (i, j).2) fun m ↦ (coeff (m + single s n)) φ) = 0
Module: Mathlib.RingTheory.DedekindDomain.AdicValuation

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
x : ↥(nonZeroDivisors R)
⊢ 0 < exp (-↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {↑x})).factors))

Tactic:
]

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
x : ↥(nonZeroDivisors R)
⊢ 0 < exp (-↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {↑x})).factors))
Module: Mathlib.RingTheory.PowerSeries.Basic

Goal state before:
pp: R : Type u_2
inst✝¹ : CommSemiring R
ι : Type u_3
inst✝ : DecidableEq ι
f : ι → R⟦X⟧
d : ℕ
s : Finset ι
⊢ ∑ x ∈ s.finsuppAntidiag d,
      ∏ i ∈ s,
        (MvPowerSeries.coeff (((Finsupp.mapRange.addEquiv (Finsupp.uniqueAddEquiv ()).symm).toEmbedding x) i)) (f i) =
    ∑ l ∈ s.finsuppAntidiag d, ∏ i ∈ s, (MvPowerSeries.coeff (single () (l i))) (f i)

Tactic:
]

Goal state after:
R : Type u_2
inst✝¹ : CommSemiring R
ι : Type u_3
inst✝ : DecidableEq ι
f : ι → R⟦X⟧
d : ℕ
s : Finset ι
⊢ ∑ x ∈ s.finsuppAntidiag d,
      ∏ i ∈ s,
        (MvPowerSeries.coeff (((Finsupp.mapRange.addEquiv (Finsupp.uniqueAddEquiv ()).symm).toEmbedding x) i)) (f i) =
    ∑ l ∈ s.finsuppAntidiag d, ∏ i ∈ s, (MvPowerSeries.coeff (single () (l i))) (f i)
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
⊢ i = (i, j).1 ∧ j = (i, j).1 + (i, j).2 - (i, j).1

Tactic:
]

Goal state after:
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
⊢ i = (i, j).1 ∧ j = (i, j).1 + (i, j).2 - (i, j).1
Module: Mathlib.RingTheory.DedekindDomain.AdicValuation

Goal state before:
pp: case inr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
x : R
hx : x ≠ 0
⊢ 0 ≤ ↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {x})).factors)

Tactic:
]

Goal state after:
case inr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
x : R
hx : x ≠ 0
⊢ 0 ≤ ↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {x})).factors)
Module: Mathlib.RingTheory.MvPowerSeries.Basic

Goal state before:
pp: case pos.h₁
σ : 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
hni : (single s n, m - single s n) ∉ antidiagonal m
⊢ (single s n, m - single s n).2 + (single s n, m - single s n).1 = m

Tactic:
]

Goal state after:
case pos.h₁
σ : 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
hni : (single s n, m - single s n) ∉ antidiagonal m
⊢ (single s n, m - single s n).2 + (single s n, m - single s n).1 = m
Module: Mathlib.RingTheory.MvPowerSeries.Basic

Goal state before:
pp: case neg
σ : 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
⊢ 0 = 0

pp: case neg
σ : 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
⊢ ∀ x ∈ antidiagonal m, ((coeff x.1) (X s ^ n) * (coeff x.2) fun m ↦ (coeff (m + single s n)) φ) = 0

pp: case neg.a
σ : 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
⊢ m s < n

Tactic:
]

Goal state after:
case neg
σ : 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
⊢ ∀ x ∈ antidiagonal m, ((coeff x.1) (X s ^ n) * (coeff x.2) fun m ↦ (coeff (m + single s n)) φ) = 0

case neg.a
σ : 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
⊢ m s < n
Module: Mathlib.RingTheory.PowerSeries.Basic

Goal state before:
pp: R : Type u_2
inst✝ : CommSemiring R
k n : ℕ
φ : R⟦X⟧
h₁ : ∀ (i : ℕ), Function.const ℕ φ i = φ
h₂ : ∀ (i : ℕ), ∏ j ∈ range i, Function.const ℕ φ j = φ ^ i
⊢ (coeff n) (∏ j ∈ range k, Function.const ℕ (Function.const ℕ φ k) j) =
    ∑ l ∈ (range k).finsuppAntidiag n, ∏ i ∈ range k, (coeff (l i)) (Function.const ℕ φ k)

Tactic:
]

Goal state after:
R : Type u_2
inst✝ : CommSemiring R
k n : ℕ
φ : R⟦X⟧
h₁ : ∀ (i : ℕ), Function.const ℕ φ i = φ
h₂ : ∀ (i : ℕ), ∏ j ∈ range i, Function.const ℕ φ j = φ ^ i
⊢ (coeff n) (∏ j ∈ range k, Function.const ℕ (Function.const ℕ φ k) j) =
    ∑ l ∈ (range k).finsuppAntidiag n, ∏ i ∈ range k, (coeff (l i)) (Function.const ℕ φ k)
Module: Mathlib.RingTheory.MvPowerSeries.Basic

Goal state before:
pp: case neg
σ : 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
⊢ ((coeff (i, j).1) (X s ^ n) * (coeff (i, j).2) fun m ↦ (coeff (m + single s n)) φ) = 0

Tactic:
]

Goal state after:
case neg
σ : 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
⊢ ((coeff (i, j).1) (X s ^ n) * (coeff (i, j).2) fun m ↦ (coeff (m + single s n)) φ) = 0
Module: Mathlib.RingTheory.DedekindDomain.AdicValuation

Goal state before:
pp: case neg
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
r : R
hr : ¬r = 0
⊢ (Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {r})).factors ≠ 0 ↔ v.asIdeal ∣ Ideal.span {r}

Tactic:
]

Goal state after:
case neg
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
r : R
hr : ¬r = 0
⊢ (Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {r})).factors ≠ 0 ↔ v.asIdeal ∣ Ideal.span {r}
Module: Mathlib.RingTheory.MvPowerSeries.Basic

Goal state before:
pp: case neg
σ : 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
⊢ ((if (i, j).1 = single s n then 1 else 0) * (coeff (i, j).2) fun m ↦ (coeff (m + single s n)) φ) = 0

Tactic:
]

Goal state after:
case neg
σ : 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
⊢ ((if (i, j).1 = single s n then 1 else 0) * (coeff (i, j).2) fun m ↦ (coeff (m + single s n)) φ) = 0
Module: Mathlib.RingTheory.DedekindDomain.AdicValuation

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
r : R
hr : ¬r = 0
⊢ ¬r = 0

Tactic:
]

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
r : R
hr : ¬r = 0
⊢ ¬r = 0