mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Algebra.Valued.ValuedField

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

Tactic:
·

Goal state after:
case neg
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
s : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
this : (𝓝 0).HasBasis (fun x ↦ True) fun γ ↦ {x | extensionValuation x < ↑((Units.map ↑embedding) γ)}
x : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
γ : (ofClass v).ValueGroup₀ˣ
hx0 : ¬x = 0
⊢ ↑⟨Units.mk0 ((ofClass extensionValuation) x) ⋯, ⋯⟩ < valueGroup₀_equiv_extensionValuation ↑γ ↔ extension 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
⊢ ∃ π, (valuation K v) π = exp (-1)

Tactic:
obtain ⟨r, hr⟩ := v.valuation_exists_uniformizer' K

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
hr : (valuation K v) ↑r = exp (-1)
⊢ ∃ π, (valuation K v) π = exp (-1)
Module: Mathlib.RingTheory.DedekindDomain.AdicValuation

Goal state before:
pp: case inl
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, (valuation K v) a = 0

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 : (WithZero (Multiplicative ℤ))ˣ
⊢ ∃ a, (valuation K v) a = ↑x

Tactic:
·

Goal state after:
case inl
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, (valuation K v) a = 0
Module: Mathlib.Topology.Algebra.Valued.ValuedField

Goal state before:
pp: case neg
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
s : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
this : (𝓝 0).HasBasis (fun x ↦ True) fun γ ↦ {x | extensionValuation x < ↑((Units.map ↑embedding) γ)}
x : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
γ : (ofClass v).ValueGroup₀ˣ
hx0 : ¬x = 0
y : K := ⋯.choose
hy_def : y = ⋯.choose
hy : v y = embedding ↑γ
⊢ ↑⟨Units.mk0 (embedding (extension x)) ⋯, ⋯⟩ < ↑⟨Units.mk0 ((ofClass extensionValuation) ↑y) ?neg.hnc✝, ⋯⟩ ↔
    extension x < ↑γ

pp: case neg.hnc
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
s : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
this : (𝓝 0).HasBasis (fun x ↦ True) fun γ ↦ {x | extensionValuation x < ↑((Units.map ↑embedding) γ)}
x : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
γ : (ofClass v).ValueGroup₀ˣ
hx0 : ¬x = 0
y : K := ⋯.choose
hy_def : y = ⋯.choose
hy : v y = embedding ↑γ
⊢ ¬(ofClass extensionValuation) ↑y = 0

Tactic:
·

Goal state after:
case neg
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
s : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
this : (𝓝 0).HasBasis (fun x ↦ True) fun γ ↦ {x | extensionValuation x < ↑((Units.map ↑embedding) γ)}
x : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
γ : (ofClass v).ValueGroup₀ˣ
hx0 : ¬x = 0
y : K := ⋯.choose
hy_def : y = ⋯.choose
hy : v y = embedding ↑γ
⊢ ↑⟨Units.mk0 (embedding (extension x)) ⋯, ⋯⟩ < ↑⟨Units.mk0 ((ofClass extensionValuation) ↑y) ?neg.hnc✝, ⋯⟩ ↔
    extension 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
v : HeightOneSpectrum R
x : (WithZero (Multiplicative ℤ))ˣ
⊢ ∃ a, (valuation K v) a = ↑x

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 : (WithZero (Multiplicative ℤ))ˣ
⊢ ∃ a, (valuation K v) a = ↑x
Module: Mathlib.RingTheory.DedekindDomain.AdicValuation

Goal state before:
pp: case inl
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
h : ∀ (v : HeightOneSpectrum R), (valuation K v) (IsLocalization.mk' K 0 ⟨d, hd⟩) ≤ 1
hx : IsLocalization.mk' K 0 ⟨d, hd⟩ * (algebraMap R K) ↑(0, ⟨d, hd⟩).2 = (algebraMap R K) (0, ⟨d, hd⟩).1
⊢ IsLocalization.mk' K 0 ⟨d, hd⟩ ∈ (algebraMap R K).range

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
⊢ IsLocalization.mk' K n ⟨d, hd⟩ ∈ (algebraMap R K).range

Tactic:
·

Goal state after:
case inl
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
h : ∀ (v : HeightOneSpectrum R), (valuation K v) (IsLocalization.mk' K 0 ⟨d, hd⟩) ≤ 1
hx : IsLocalization.mk' K 0 ⟨d, hd⟩ * (algebraMap R K) ↑(0, ⟨d, hd⟩).2 = (algebraMap R K) (0, ⟨d, hd⟩).1
⊢ IsLocalization.mk' K 0 ⟨d, hd⟩ ∈ (algebraMap R K).range
Module: Mathlib.Topology.Algebra.Valued.ValuedField

Goal state before:
pp: case neg.hnc
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
s : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
this : (𝓝 0).HasBasis (fun x ↦ True) fun γ ↦ {x | extensionValuation x < ↑((Units.map ↑embedding) γ)}
x : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
γ : (ofClass v).ValueGroup₀ˣ
hx0 : ¬x = 0
y : K := ⋯.choose
hy_def : y = ⋯.choose
hy : v y = embedding ↑γ
⊢ ¬(ofClass extensionValuation) ↑y = 0

Tactic:
·

Goal state after:
case neg.hnc
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
s : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
this : (𝓝 0).HasBasis (fun x ↦ True) fun γ ↦ {x | extensionValuation x < ↑((Units.map ↑embedding) γ)}
x : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
γ : (ofClass v).ValueGroup₀ˣ
hx0 : ¬x = 0
y : K := ⋯.choose
hy_def : y = ⋯.choose
hy : v y = embedding ↑γ
⊢ ¬(ofClass extensionValuation) ↑y = 0
Module: Mathlib.RingTheory.PowerSeries.Basic

Goal state before:
pp: case inr.succ
R : Type u_2
inst✝ : CommSemiring R
φ : R⟦X⟧
n' : ℕ
ih : n' > 0 → (coeff 1) (φ ^ n') = ↑n' * (coeff 1) φ * constantCoeff φ ^ (n' - 1)
hn : n' + 1 > 0
h₁ : ∀ (m : ℕ), φ ^ (m + 1) = φ ^ m * φ
h₂ : antidiagonal 1 = {(0, 1), (1, 0)}
⊢ (0, 1) ∉ {(1, 0)}

Tactic:
·

Goal state after:
case inr.succ
R : Type u_2
inst✝ : CommSemiring R
φ : R⟦X⟧
n' : ℕ
ih : n' > 0 → (coeff 1) (φ ^ n') = ↑n' * (coeff 1) φ * constantCoeff φ ^ (n' - 1)
hn : n' + 1 > 0
h₁ : ∀ (m : ℕ), φ ^ (m + 1) = φ ^ m * φ
h₂ : antidiagonal 1 = {(0, 1), (1, 0)}
⊢ (0, 1) ∉ {(1, 0)}
Module: Mathlib.RingTheory.PowerSeries.Basic

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

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

Tactic:
·

Goal state after:
case pos
A : Type u_2
inst✝ : CommRing A
hA : Subsingleton A
⊢ ¬IsField A⟦X⟧
Module: Mathlib.RingTheory.PowerSeries.Basic

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

Tactic:
·

Goal state after:
case neg
A : Type u_2
inst✝ : CommRing A
hA : ¬Subsingleton A
⊢ ¬IsField A⟦X⟧
Module: Mathlib.RingTheory.PowerSeries.Basic

Goal state before:
pp: case h.left
A : Type u_2
inst✝ : CommRing A
hA : ¬Subsingleton A
a✝ : Nontrivial A
⊢ ⊥ < Ideal.span {X}

pp: case h.right
A : Type u_2
inst✝ : CommRing A
hA : ¬Subsingleton A
a✝ : Nontrivial A
⊢ Ideal.span {X} < ⊤

Tactic:
·

Goal state after:
case h.left
A : Type u_2
inst✝ : CommRing A
hA : ¬Subsingleton A
a✝ : Nontrivial A
⊢ ⊥ < Ideal.span {X}
Module: Mathlib.RingTheory.PowerSeries.Basic

Goal state before:
pp: case h.right
A : Type u_2
inst✝ : CommRing A
hA : ¬Subsingleton A
a✝ : Nontrivial A
⊢ Ideal.span {X} < ⊤

Tactic:
·

Goal state after:
case h.right
A : Type u_2
inst✝ : CommRing A
hA : ¬Subsingleton A
a✝ : Nontrivial A
⊢ Ideal.span {X} < ⊤
Module: Mathlib.Topology.Algebra.Valued.ValuedField

Goal state before:
pp: case refine_1
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✝ : ∃ i, {x | embedding (extension x) < embedding ↑i} ⊆ s
γ : (ofClass v).ValueGroup₀ˣ
h : {x | embedding (extension x) < embedding ↑γ} ⊆ s
⊢ ∃ γ, {x | extensionValuation.restrict x < ↑γ} ⊆ s

pp: case refine_2
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
⊢ ∃ i, {x | embedding (extension x) < embedding ↑i} ⊆ s

Tactic:
·

Goal state after:
case refine_1
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✝ : ∃ i, {x | embedding (extension x) < embedding ↑i} ⊆ s
γ : (ofClass v).ValueGroup₀ˣ
h : {x | embedding (extension x) < embedding ↑γ} ⊆ s
⊢ ∃ γ, {x | extensionValuation.restrict x < ↑γ} ⊆ s
Module: Mathlib.Topology.Algebra.Valued.ValuedField

Goal state before:
pp: case refine_2
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
⊢ ∃ i, {x | embedding (extension x) < embedding ↑i} ⊆ s

Tactic:
·

Goal state after:
case refine_2
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
⊢ ∃ i, {x | embedding (extension x) < embedding ↑i} ⊆ s
Module: Mathlib.RingTheory.MvPowerSeries.Basic

Goal state before:
pp: case e'_3
σ : 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) = #(range n \ s) • 1

pp: case e'_4
σ : 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
⊢ degree (∑ x ∈ range n \ s, k x) = ∑ x ∈ range n \ s, degree (k x)

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
⊢ ∀ x ∈ range n \ s, 1 ≤ degree (k x)

Tactic:
·

Goal state after:
case e'_3
σ : 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) = #(range n \ s) • 1
Module: Mathlib.RingTheory.MvPowerSeries.Basic

Goal state before:
pp: case e'_4
σ : 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
⊢ degree (∑ x ∈ range n \ s, k x) = ∑ x ∈ range n \ s, degree (k x)

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
⊢ ∀ x ∈ range n \ s, 1 ≤ degree (k x)

Tactic:
·

Goal state after:
case e'_4
σ : 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
⊢ degree (∑ x ∈ range n \ s, k x) = ∑ x ∈ range n \ s, degree (k 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
⊢ ∀ x ∈ range n \ s, 1 ≤ degree (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
⊢ ∀ x ∈ range n \ s, 1 ≤ degree (k x)
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)
Module: Mathlib.RingTheory.MvPowerSeries.Order

Goal state before:
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:
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.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
this : ↑(weightedOrder w f).toNat = weightedOrder w f
⊢ False

Tactic:
obtain ⟨d, hfd, hd⟩ := exists_coeff_ne_zero_and_weightedOrder w this

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

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

Tactic:
classical
    rw [coeff_coe, coeff_monomial, MvPowerSeries.coeff_monomial]
    split_ifs with h₁ h₂ <;> first | rfl | subst m; contradiction

Goal state after:
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
⊢ ⊤ ≤ weightedOrder w f

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
⊢ ↑a✝ ≤ weightedOrder w f

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
⊢ ⊤ ≤ weightedOrder w f
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
⊢ ↑a✝ ≤ weightedOrder w f

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
⊢ ↑a✝ ≤ weightedOrder w f
Module: Mathlib.RingTheory.MvPowerSeries.Order

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

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

Tactic:
·

Goal state after:
case mp
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
f : MvPowerSeries σ R
n : ℕ
⊢ weightedOrder w f = ↑n →
    (∃ d, (coeff d) f ≠ 0 ∧ (weight w) d = n) ∧ ∀ (d : σ →₀ ℕ), (weight w) d < n → (coeff d) f = 0
Module: Mathlib.Topology.Algebra.Valued.ValuedField

Goal state before:
pp: case mp
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
h : Function.Surjective ⇑v
γ : Γ₀
a : hat K
ha : v a = γ
⊢ ∃ a, v a = γ

pp: case mpr
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
h : Function.Surjective ⇑v
γ : Γ₀
a : K
ha : v a = γ
⊢ ∃ a, v a = γ

Tactic:
·

Goal state after:
case mp
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
h : Function.Surjective ⇑v
γ : Γ₀
a : hat K
ha : v a = γ
⊢ ∃ a, v a = γ
Module: Mathlib.Topology.Algebra.Valued.ValuedField

Goal state before:
pp: case mp.hp
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
h : Function.Surjective ⇑v
γ : Γ₀
⊢ IsClosed {a | v a = γ → ∃ a, v a = γ}

pp: case mp.ih
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
h : Function.Surjective ⇑v
γ : Γ₀
a✝ : K
ha : v ↑a✝ = γ
⊢ ∃ a, v a = γ

Tactic:
·

Goal state after:
case mp.hp
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
h : Function.Surjective ⇑v
γ : Γ₀
⊢ IsClosed {a | v a = γ → ∃ a, v a = γ}
Module: Mathlib.RingTheory.MvPowerSeries.Order

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

Tactic:
·

Goal state after:
case mpr
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
f : MvPowerSeries σ R
n : ℕ
⊢ ((∃ d, (coeff d) f ≠ 0 ∧ (weight w) d = n) ∧ ∀ (d : σ →₀ ℕ), (weight w) d < n → (coeff d) f = 0) →
    weightedOrder w f = ↑n
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