mathlib-initiative/mathlib-tactics huggingface dataset:
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
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
ine : ∀ {r : R}, r ≠ 0 → Ideal.span {r} ≠ ⊥
⊢ ∀ (a : { a // Irreducible a }),
    Multiset.count a (Associates.factors' (Ideal.span {d})) ≤ Multiset.count a (Associates.factors' (Ideal.span {n}))

Tactic:
]

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
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
ine : ∀ {r : R}, r ≠ 0 → Ideal.span {r} ≠ ⊥
⊢ ∀ (a : { a // Irreducible a }),
    Multiset.count a (Associates.factors' (Ideal.span {d})) ≤ Multiset.count a (Associates.factors' (Ideal.span {n}))
Module: Mathlib.RingTheory.PowerSeries.Basic

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

Tactic:
]

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

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

Tactic:
]

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
⊢ m + #(range n \ {i ∈ range n | k i = 0}) ≤ n

Tactic:
]

Goal state after:
σ : 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
⊢ m + #(range n \ {i ∈ range n | k i = 0}) ≤ n
Module: Mathlib.RingTheory.PowerSeries.Basic

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

Tactic:
]

Goal state after:
R : Type u_1
inst✝ : Semiring R
φ : R[X]
⊢ eval₂ PowerSeries.C PowerSeries.X φ = ↑(eval₂ C X φ)
Module: Mathlib.RingTheory.PowerSeries.Basic

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
φ : R[X]
⊢ ∑ i ∈ Finset.range (φ.natDegree + 1), PowerSeries.C (φ.coeff i) * PowerSeries.X ^ i =
    ∑ x ∈ Finset.range (φ.natDegree + 1), coeToPowerSeries.ringHom (C (φ.coeff x) * X ^ x)

Tactic:
]

Goal state after:
R : Type u_1
inst✝ : Semiring R
φ : R[X]
⊢ ∑ i ∈ Finset.range (φ.natDegree + 1), PowerSeries.C (φ.coeff i) * PowerSeries.X ^ i =
    ∑ x ∈ Finset.range (φ.natDegree + 1), coeToPowerSeries.ringHom (C (φ.coeff x) * X ^ x)
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
⊢ #(range n \ s) ≤ degree (∑ x ∈ range n \ s, k x)

Tactic:
]

Goal state after:
σ : 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
⊢ #(range n \ s) ≤ degree (∑ x ∈ range n \ s, k x)
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
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
ine : ∀ {r : R}, r ≠ 0 → Ideal.span {r} ≠ ⊥
v : Ideal R
hv✝ : Irreducible (Associates.mk v)
hv : Prime v
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:
]

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
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
ine : ∀ {r : R}, r ≠ 0 → Ideal.span {r} ≠ ⊥
v : Ideal R
hv✝ : Irreducible (Associates.mk v)
hv : Prime v
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}))
Module: Mathlib.RingTheory.PowerSeries.Basic

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
φ : R[X]
x✝ : ℕ
a✝ : x✝ ∈ Finset.range (φ.natDegree + 1)
⊢ PowerSeries.C (φ.coeff x✝) * PowerSeries.X ^ x✝ = PowerSeries.C (φ.coeff x✝) * PowerSeries.X ^ x✝

Tactic:
]

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) γ)}
this : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
x✝¹ : ∃ γ, {x | extensionValuation.restrict x < ↑γ} ⊆ s
γ : (ofClass extensionValuation).ValueGroup₀ˣ
h : {x | extensionValuation.restrict x < ↑γ} ⊆ s
x✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ extensionValuation.restrict x✝ <
      ↑((Units.map valueGroup₀_equiv_extensionValuation.toMonoidHom)
          ((Units.map valueGroup₀_equiv_extensionValuation.symm.toMonoidHom) γ)) ↔
    extensionValuation.restrict x✝ < ↑γ

Tactic:
]

Goal state after:
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) γ)}
this : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
x✝¹ : ∃ γ, {x | extensionValuation.restrict x < ↑γ} ⊆ s
γ : (ofClass extensionValuation).ValueGroup₀ˣ
h : {x | extensionValuation.restrict x < ↑γ} ⊆ s
x✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ extensionValuation.restrict x✝ <
      ↑((Units.map valueGroup₀_equiv_extensionValuation.toMonoidHom)
          ((Units.map valueGroup₀_equiv_extensionValuation.symm.toMonoidHom) γ)) ↔
    extensionValuation.restrict x✝ < ↑γ
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
i : ℕ
hi : i < n
hi' : i < n → ¬k i = 0
⊢ ¬k i = 0

Tactic:
]

Goal state after:
σ : 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
i : ℕ
hi : i < n
hi' : i < n → ¬k i = 0
⊢ ¬k i = 0
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
this : f = (MvPolynomial.uniqueAlgEquiv R PUnit.{1}) g
⊢ ↑((MvPolynomial.uniqueAlgEquiv R PUnit.{1}) g) = ↑((MvPolynomial.uniqueAlgEquiv R PUnit.{1}) g)

Tactic:
]

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

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

Tactic:
]

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 ≠ ⊤ ↔ weightedOrder w f ≠ ⊤

Tactic:
]

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
⊢ ↑(Nat.find ⋯) ≤ ↑((weight w) d)

pp: case hnc
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
f : MvPowerSeries σ R
d : σ →₀ ℕ
h : (coeff d) f ≠ 0
⊢ ¬f = 0

Tactic:
]

Goal state after:
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
f : MvPowerSeries σ R
d : σ →₀ ℕ
h : (coeff d) f ≠ 0
⊢ ↑(Nat.find ⋯) ≤ ↑((weight w) d)

case hnc
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
f : MvPowerSeries σ R
d : σ →₀ ℕ
h : (coeff d) f ≠ 0
⊢ ¬f = 0
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
⊢ ∃ x, ¬(x ∈ ⊥ ↔ x ∈ ⊤)

Tactic:
]

Goal state after:
σ : 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
⊢ ∃ x, ¬(x ∈ ⊥ ↔ x ∈ ⊤)
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:
]

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
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
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
  rw [weightedOrder, dif_neg]
  · simp only [ne_eq, Nat.cast_le, Nat.find_le_iff]
    exact ⟨weight w d, le_rfl, d, h, rfl⟩
  · exact (f.ne_zero_iff_exists_coeff_ne_zero_and_weight w).mpr ⟨weight w d, d, h, rfl⟩

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

Goal state before:
pp: σ : Type u_1
R : Type u_2
A : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring A
inst✝⁴ : Algebra R A
B : Type u_4
inst✝³ : Semiring B
inst✝² : Algebra R B
inst✝¹ : Nonempty σ
inst✝ : Nontrivial R
inhabited_h : Inhabited σ
x : R
⊢ ∃ x_1, ¬(coeff x_1) ((algebraMap R (MvPowerSeries σ R)) x) = (coeff x_1) (X default)

Tactic:
]

Goal state after:
σ : 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
inhabited_h : Inhabited σ
x : R
⊢ ∃ x_1, ¬(coeff x_1) ((algebraMap R (MvPowerSeries σ R)) x) = (coeff x_1) (X default)
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
  contrapose! h; exact weightedOrder_le w h

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 ≠ ⊤

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: σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n : σ →₀ ℕ
a : R
m : σ →₀ ℕ
⊢ (if n = m then a else 0) = if m = n then a else 0

Tactic:
]

Goal state after:
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n : σ →₀ ℕ
a : R
m : σ →₀ ℕ
⊢ (if n = m then a else 0) = if m = n then a else 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
a s : R
hs : s ∈ v.asIdeal.primeCompl
⊢ s ∉ v.asIdeal

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
a s : R
hs : s ∈ v.asIdeal.primeCompl
⊢ s ∉ v.asIdeal
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
this : ↑(weightedOrder w f).toNat = weightedOrder w f
d : σ →₀ ℕ
H : (weight w) d < n
hfd : (coeff d) f ≠ 0
hd : ↑((weight w) d) = weightedOrder w f
⊢ False

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
this : ↑(weightedOrder w f).toNat = weightedOrder w f
d : σ →₀ ℕ
H : (weight w) d < n
hfd : (coeff d) f ≠ 0
hd : ↑((weight w) d) = weightedOrder w f
⊢ False
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
⊢ f = 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
⊢ f = 0
Module: Mathlib.RingTheory.MvPowerSeries.Basic

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

Tactic:
]

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

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

Tactic:
]

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.C r * ∏ x ∈ e.support, MvPowerSeries.X x ^ (p • e) x =
    MvPowerSeries.C r * ∏ a ∈ e.support, (MvPowerSeries.X a ^ p) ^ e a

Tactic:
]

Goal state after:
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
e : σ →₀ ℕ
p : ℕ
r : R
⊢ MvPowerSeries.C r * ∏ x ∈ e.support, MvPowerSeries.X x ^ (p • e) x =
    MvPowerSeries.C r * ∏ a ∈ e.support, (MvPowerSeries.X a ^ p) ^ e a
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 ↦ (MvPowerSeries.C ((algebraMap A R) (a s)) * MvPowerSeries.X s) ^ n) =
    (e.prod fun s n ↦ a s ^ n) • (MvPowerSeries.monomial e) 1

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
⊢ ∀ x ∈ e.support,
    (a x • MvPowerSeries.X x) ^ e x = (MvPowerSeries.C ((algebraMap A R) (a x)) * MvPowerSeries.X x) ^ e x

Tactic:
]

Goal state after:
σ : 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 ↦ (MvPowerSeries.C ((algebraMap A R) (a s)) * MvPowerSeries.X s) ^ n) =
    (e.prod fun s n ↦ a s ^ n) • (MvPowerSeries.monomial e) 1

σ : Type u_1
R : Type u_2
inst✝² : CommSemiring R
A : Type u_4
inst✝¹ : CommSemiring A
inst✝ : Algebra A R
e : σ →₀ ℕ
a : σ → A
⊢ ∀ x ∈ e.support,
    (a x • MvPowerSeries.X x) ^ e x = (MvPowerSeries.C ((algebraMap A R) (a x)) * MvPowerSeries.X x) ^ e x
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 = a • f

Tactic:
]

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

Goal state before:
pp: case pos
σ : Type u_1
R : Type u_2
inst✝¹ : Semiring R
w : σ → ℕ
d : σ →₀ ℕ
a : R
inst✝ : Decidable (a = 0)
h : a = 0
⊢ 0 = 0

Tactic:
]

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

Goal state before:
pp: case neg
σ : Type u_1
R : Type u_2
inst✝¹ : Semiring R
w : σ → ℕ
d : σ →₀ ℕ
a : R
inst✝ : Decidable (a = 0)
h : ¬a = 0
⊢ (∃ d_1, (coeff d_1) ((monomial d) a) ≠ 0 ∧ (weight w) d_1 = (weight w) d) ∧
    ∀ (d_1 : σ →₀ ℕ), (weight w) d_1 < (weight w) d → (coeff d_1) ((monomial d) a) = 0

Tactic:
]

Goal state after:
case neg
σ : Type u_1
R : Type u_2
inst✝¹ : Semiring R
w : σ → ℕ
d : σ →₀ ℕ
a : R
inst✝ : Decidable (a = 0)
h : ¬a = 0
⊢ (∃ d_1, (coeff d_1) ((monomial d) a) ≠ 0 ∧ (weight w) d_1 = (weight w) d) ∧
    ∀ (d_1 : σ →₀ ℕ), (weight w) d_1 < (weight w) d → (coeff d_1) ((monomial d) a) = 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 Γ₀
h : Function.Surjective ⇑v
γ : Γ₀
H : ¬∃ x, v x = γ
hγ : γ ≠ 0
r : hat K
hr : v r = γ
⊢ ¬(ofClass v) r = embedding 0

Tactic:
]

Goal state after:
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 = γ
⊢ ¬(ofClass v) r = embedding 0
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
x : σ
a✝ : x ∈ e.support
⊢ (MvPowerSeries.C ((algebraMap A R) (a x)) * MvPowerSeries.X x) ^ e x =
    (MvPowerSeries.C ((algebraMap A R) (a x)) * MvPowerSeries.X x) ^ e x

Tactic:
]

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) = (MvPowerSeries.monomial e) (e.prod fun s n ↦ r s ^ n)

Tactic:
]

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) = (MvPowerSeries.monomial e) (e.prod fun s n ↦ r ^ n)

Tactic:
]

Goal state after:
σ : Type u_4
R : Type u_5
inst✝ : CommSemiring R
e : σ →₀ ℕ
r : R
⊢ (MvPowerSeries.monomial e) (r ^ e.sum fun x n ↦ n) = (MvPowerSeries.monomial e) (e.prod fun s n ↦ r ^ n)
Module: Mathlib.RingTheory.MvPowerSeries.Order

Goal state before:
pp: case neg.right
σ : Type u_1
R : Type u_2
inst✝¹ : Semiring R
w : σ → ℕ
d : σ →₀ ℕ
a : R
inst✝ : Decidable (a = 0)
h : ¬a = 0
b : σ →₀ ℕ
hb : (weight w) b < (weight w) d
⊢ 0 = 0

pp: case neg.right.hnc
σ : Type u_1
R : Type u_2
inst✝¹ : Semiring R
w : σ → ℕ
d : σ →₀ ℕ
a : R
inst✝ : Decidable (a = 0)
h : ¬a = 0
b : σ →₀ ℕ
hb : (weight w) b < (weight w) d
⊢ ¬b = d

Tactic:
]

Goal state after:
case neg.right.hnc
σ : Type u_1
R : Type u_2
inst✝¹ : Semiring R
w : σ → ℕ
d : σ →₀ ℕ
a : R
inst✝ : Decidable (a = 0)
h : ¬a = 0
b : σ →₀ ℕ
hb : (weight w) b < (weight w) d
⊢ ¬b = d
Module: Mathlib.RingTheory.MvPowerSeries.Order

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
d : σ →₀ ℕ
a : R
h : a ≠ 0
⊢ ↑((weight w) d) = ↑((weight w) d)

Tactic:
]

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 Γ₀
R : Type u_3
inst✝³ : CommSemiring R
inst✝² : Algebra R K
inst✝¹ : UniformContinuousConstSMul R K
inst✝ : FaithfulSMul R K
⊢ Function.Injective ⇑(algebraMap R (hat K))

Tactic:
]

Goal state after:
K : Type u_1
inst✝⁵ : Field K
Γ₀ : Type u_2
inst✝⁴ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
R : Type u_3
inst✝³ : CommSemiring R
inst✝² : Algebra R K
inst✝¹ : UniformContinuousConstSMul R K
inst✝ : FaithfulSMul R K
⊢ Function.Injective ⇑(algebraMap R (hat K))
Module: Mathlib.Data.Finset.Finsupp

Goal state before:
pp: case neg
ι : Type u_1
α : Type u_2
inst✝ : Zero α
s : Finset ι
f : ι →₀ α
t : ι →₀ Finset α
ht : t.support ⊆ s
i : ι
h : (i ∈ f.support → i ∈ s) ∧ (i ∈ s → f i ∈ t i)
hi : i ∉ s
⊢ 0 ∈ 0

Tactic:
]

Goal state after:
case neg
ι : Type u_1
α : Type u_2
inst✝ : Zero α
s : Finset ι
f : ι →₀ α
t : ι →₀ Finset α
ht : t.support ⊆ s
i : ι
h : (i ∈ f.support → i ∈ s) ∧ (i ∈ s → f i ∈ t i)
hi : i ∉ s
⊢ 0 ∈ 0
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
v : HeightOneSpectrum R
x : K
hv : (valuation K v) x ≤ 1
n : R
d : ↥v.asIdeal.primeCompl
hnd : x * (algebraMap R K) n = (algebraMap R K) ↑d
⊢ v.intValuation n = 1

Tactic:
]

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
v : HeightOneSpectrum R
x : K
hv : (valuation K v) x ≤ 1
n : R
d : ↥v.asIdeal.primeCompl
hnd : x * (algebraMap R K) n = (algebraMap R K) ↑d
⊢ v.intValuation n = 1