mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.MvPolynomial.IrreducibleQuadratic

Goal state before:
pp: case hnc
n : Type u_1
R : Type u_2
inst✝ : CommRing R
c : n →₀ R
i j : n
hj : j ∈ c.support
hji : j ≠ i
⊢ ¬j = i

Tactic:
]

Goal state after:
case hnc
n : Type u_1
R : Type u_2
inst✝ : CommRing R
c : n →₀ R
i j : n
hj : j ∈ c.support
hji : j ≠ i
⊢ ¬j = i
Module: Mathlib.RingTheory.MvPolynomial.IrreducibleQuadratic

Goal state before:
pp: case hnc
n : Type u_1
R : Type u_2
inst✝ : CommRing R
c : n →₀ R
i j : n
hj : j ∈ c.support
hji : j ≠ i
⊢ ¬Finsupp.single j 1 = Finsupp.single i 1

Tactic:
rwa [Finsupp.single_left_inj Nat.one_ne_zero]

Goal state after:
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: K : Type u_2
inst✝ : Field K
ℱ : Filter K⸨X⸩
hℱ : Cauchy ℱ
U : Set K⸨X⸩
hU : U ∈ 𝓝 (limit hℱ)
γ : (MonoidWithZeroHom.ofClass Valued.v).ValueGroup₀ˣ
hU₁ : {y | Valued.v.restrict (y - limit hℱ) < ↑γ} ⊆ U
D : ℤ := -((embedding ↑γ).log - 1)
hD₀ : D = -((embedding ↑γ).log - 1)
hD : exp (-D) < embedding ↑γ
x✝ : K⸨X⸩
hf : ∀ d < D, coeff hℱ d = x✝.coeff d
n : ℤ
hn : n < D
⊢ (limit hℱ).coeff n = x✝.coeff n

Tactic:
]

Goal state after:
K : Type u_2
inst✝ : Field K
ℱ : Filter K⸨X⸩
hℱ : Cauchy ℱ
U : Set K⸨X⸩
hU : U ∈ 𝓝 (limit hℱ)
γ : (MonoidWithZeroHom.ofClass Valued.v).ValueGroup₀ˣ
hU₁ : {y | Valued.v.restrict (y - limit hℱ) < ↑γ} ⊆ U
D : ℤ := -((embedding ↑γ).log - 1)
hD₀ : D = -((embedding ↑γ).log - 1)
hD : exp (-D) < embedding ↑γ
x✝ : K⸨X⸩
hf : ∀ d < D, coeff hℱ d = x✝.coeff d
n : ℤ
hn : n < D
⊢ (limit hℱ).coeff n = x✝.coeff n
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: case neg
K : Type u_2
inst✝ : Field K
F : K⟦X⟧
η : (WithZero (Multiplicative ℤ))ˣ
h_neg : Multiplicative.toAdd (unzero ⋯) ≤ 0
⊢ ∃ P, (PowerSeries.idealX K).intValuation (F - ↑P) < ↑η

Tactic:
]

Goal state after:
case neg
K : Type u_2
inst✝ : Field K
F : K⟦X⟧
η : (WithZero (Multiplicative ℤ))ˣ
h_neg : Multiplicative.toAdd (unzero ⋯) ≤ 0
⊢ ∃ P, (PowerSeries.idealX K).intValuation (F - ↑P) < ↑η
Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem

Goal state before:
pp: case refine_3
R : Type u_3
m : ℕ
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
i : ℕ
him : i < m
this :
  supDegree (⇑toLex) (esymm (Fin m) R (i + 1)) = toLex (Finsupp.indicator (Iic ⟨i, him⟩) fun x x_1 ↦ 1) ∧
    leadingCoeff (⇑toLex) (esymm (Fin m) R (i + 1)) = 1
⊢ supDegree (⇑toLex) (esymm (Fin m) R (i + 1)) = toLex (Finsupp.indicator (Iic ⟨i, him⟩) fun x x_1 ↦ 1) ∧
    Monic (⇑toLex) (esymm (Fin m) R (i + 1))

Tactic:
]

Goal state after:
case refine_3
R : Type u_3
m : ℕ
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
i : ℕ
him : i < m
this :
  supDegree (⇑toLex) (esymm (Fin m) R (i + 1)) = toLex (Finsupp.indicator (Iic ⟨i, him⟩) fun x x_1 ↦ 1) ∧
    leadingCoeff (⇑toLex) (esymm (Fin m) R (i + 1)) = 1
⊢ supDegree (⇑toLex) (esymm (Fin m) R (i + 1)) = toLex (Finsupp.indicator (Iic ⟨i, him⟩) fun x x_1 ↦ 1) ∧
    Monic (⇑toLex) (esymm (Fin m) R (i + 1))
Module: Mathlib.RingTheory.MvPolynomial.IrreducibleQuadratic

Goal state before:
pp: case a
n : Type u_1
R : Type u_2
inst✝¹ : CommRing R
c : n →₀ R
inst✝ : IsDomain R
hc_nonempty : c.support.Nonempty
hc_gcd : ∀ (r : R), (∀ (i : n), r ∣ c i) → IsUnit r
⊢ ¬∀ m ∈ (sumSMulX c).support, ∀ (x : n), m x = 0

Tactic:
]

Goal state after:
case a
n : Type u_1
R : Type u_2
inst✝¹ : CommRing R
c : n →₀ R
inst✝ : IsDomain R
hc_nonempty : c.support.Nonempty
hc_gcd : ∀ (r : R), (∀ (i : n), r ∣ c i) → IsUnit r
⊢ ¬∀ m ∈ (sumSMulX c).support, ∀ (x : n), m x = 0
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: case h
K : Type u_2
inst✝ : Field K
F : K⟦X⟧
η : (WithZero (Multiplicative ℤ))ˣ
h_neg : Multiplicative.toAdd (unzero ⋯) ≤ 0
d : ℕ
hd : Multiplicative.toAdd (unzero ⋯) = -↑d
this : Valued.v ((algebraMap K⟦X⟧ K⸨X⸩) (F - ↑((trunc (d + 1)) F))) ≤ ↑η * ↑(Multiplicative.ofAdd (-1))
⊢ (PowerSeries.idealX K).intValuation (F - ↑((trunc (d + 1)) F)) < ↑η

Tactic:
]

Goal state after:
case h
K : Type u_2
inst✝ : Field K
F : K⟦X⟧
η : (WithZero (Multiplicative ℤ))ˣ
h_neg : Multiplicative.toAdd (unzero ⋯) ≤ 0
d : ℕ
hd : Multiplicative.toAdd (unzero ⋯) = -↑d
this : Valued.v ((algebraMap K⟦X⟧ K⸨X⸩) (F - ↑((trunc (d + 1)) F))) ≤ ↑η * ↑(Multiplicative.ofAdd (-1))
⊢ (PowerSeries.idealX K).intValuation (F - ↑((trunc (d + 1)) F)) < ↑η
Module: Mathlib.RingTheory.MvPolynomial.IrreducibleQuadratic

Goal state before:
pp: n : Type u_1
R : Type u_2
inst✝¹ : CommRing R
c : n →₀ R
inst✝ : IsDomain R
hc_gcd : ∀ (r : R), (∀ (i : n), r ∣ c i) → IsUnit r
h : ∀ m ∈ (sumSMulX c).support, ∀ (x : n), m x = 0
i : n
hi : c i ≠ 0
⊢ c i ≠ 0

Tactic:
]

Goal state after:
n : Type u_1
R : Type u_2
inst✝¹ : CommRing R
c : n →₀ R
inst✝ : IsDomain R
hc_gcd : ∀ (r : R), (∀ (i : n), r ∣ c i) → IsUnit r
h : ∀ m ∈ (sumSMulX c).support, ∀ (x : n), m x = 0
i : n
hi : c i ≠ 0
⊢ c i ≠ 0
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: case h
K : Type u_2
inst✝ : Field K
F : K⟦X⟧
η : (WithZero (Multiplicative ℤ))ˣ
h_neg : Multiplicative.toAdd (unzero ⋯) ≤ 0
d : ℕ
hd : Multiplicative.toAdd (unzero ⋯) = -↑d
this : Valued.v ((algebraMap K⟦X⟧ K⸨X⸩) (F - ↑((trunc (d + 1)) F))) ≤ ↑η * ↑(Multiplicative.ofAdd (-1))
⊢ (valuation K⸨X⸩ (PowerSeries.idealX K)) ↑(F - ↑((trunc (d + 1)) F)) < ↑η

Tactic:
]

Goal state after:
case h
K : Type u_2
inst✝ : Field K
F : K⟦X⟧
η : (WithZero (Multiplicative ℤ))ˣ
h_neg : Multiplicative.toAdd (unzero ⋯) ≤ 0
d : ℕ
hd : Multiplicative.toAdd (unzero ⋯) = -↑d
this : Valued.v ((algebraMap K⟦X⟧ K⸨X⸩) (F - ↑((trunc (d + 1)) F))) ≤ ↑η * ↑(Multiplicative.ofAdd (-1))
⊢ (valuation K⸨X⸩ (PowerSeries.idealX K)) ↑(F - ↑((trunc (d + 1)) F)) < ↑η
Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem

Goal state before:
pp: R : Type u_3
m : ℕ
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
i : ℕ
him : i < m
t : Finset (Fin m)
ht : t ∈ powersetCard (i + 1) univ
hne : t ≠ Iic ⟨i, him⟩
⊢ i + 1 = ↑⟨i, him⟩ + 1

Tactic:
]

Goal state after:
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: case h
K : Type u_2
inst✝ : Field K
F : K⟦X⟧
η : (WithZero (Multiplicative ℤ))ˣ
h_neg : Multiplicative.toAdd (unzero ⋯) ≤ 0
d : ℕ
hd : Multiplicative.toAdd (unzero ⋯) = -↑d
this : Valued.v ((algebraMap K⟦X⟧ K⸨X⸩) (F - ↑((trunc (d + 1)) F))) ≤ ↑η * ↑(Multiplicative.ofAdd (-1))
⊢ ↑η * ↑(Multiplicative.ofAdd (-1)) < ↑η * 1

Tactic:
]

Goal state after:
case h
K : Type u_2
inst✝ : Field K
F : K⟦X⟧
η : (WithZero (Multiplicative ℤ))ˣ
h_neg : Multiplicative.toAdd (unzero ⋯) ≤ 0
d : ℕ
hd : Multiplicative.toAdd (unzero ⋯) = -↑d
this : Valued.v ((algebraMap K⟦X⟧ K⸨X⸩) (F - ↑((trunc (d + 1)) F))) ≤ ↑η * ↑(Multiplicative.ofAdd (-1))
⊢ ↑η * ↑(Multiplicative.ofAdd (-1)) < ↑η * 1
Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem

Goal state before:
pp: case refine_2
R : Type u_3
m : ℕ
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
i : ℕ
him : i < m
t : Finset (Fin m)
ht : t ∈ powersetCard (i + 1) univ
hne : ∃ x ∈ Iic ⟨i, him⟩, x ∉ t
ht' : #t = #(Iic ⟨i, him⟩)
⊢ toLex (Finsupp.indicator t fun x x_1 ↦ 1) < toLex (Finsupp.indicator (Iic ⟨i, him⟩) fun x x_1 ↦ 1)

Tactic:
]

Goal state after:
case refine_2
R : Type u_3
m : ℕ
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
i : ℕ
him : i < m
t : Finset (Fin m)
ht : t ∈ powersetCard (i + 1) univ
hne : ∃ x ∈ Iic ⟨i, him⟩, x ∉ t
ht' : #t = #(Iic ⟨i, him⟩)
⊢ toLex (Finsupp.indicator t fun x x_1 ↦ 1) < toLex (Finsupp.indicator (Iic ⟨i, him⟩) fun x x_1 ↦ 1)
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: case hbc
K : Type u_2
inst✝ : Field K
F : K⟦X⟧
η : (WithZero (Multiplicative ℤ))ˣ
h_neg : Multiplicative.toAdd (unzero ⋯) ≤ 0
d : ℕ
hd : Multiplicative.toAdd (unzero ⋯) = -↑d
this : Valued.v ((algebraMap K⟦X⟧ K⸨X⸩) (F - ↑((trunc (d + 1)) F))) ≤ ↑η * ↑(Multiplicative.ofAdd (-1))
⊢ 0 < 1

Tactic:
]

Goal state after:
case hbc
K : Type u_2
inst✝ : Field K
F : K⟦X⟧
η : (WithZero (Multiplicative ℤ))ˣ
h_neg : Multiplicative.toAdd (unzero ⋯) ≤ 0
d : ℕ
hd : Multiplicative.toAdd (unzero ⋯) = -↑d
this : Valued.v ((algebraMap K⟦X⟧ K⸨X⸩) (F - ↑((trunc (d + 1)) F))) ≤ ↑η * ↑(Multiplicative.ofAdd (-1))
⊢ 0 < 1
Module: Mathlib.RingTheory.MvPolynomial.IrreducibleQuadratic

Goal state before:
pp: n : Type u_1
R : Type u_2
inst✝¹ : CommRing R
c : n →₀ R
inst✝ : IsDomain R
hc : c.support.Nontrivial
h_dvd : ∀ (r : R), (∀ (i : n), r ∣ c i) → IsUnit r
ι : n ↪ n ⊕ n →₀ ℕ := { toFun := fun i ↦ Finsupp.single (Sum.inl i) 1 + Finsupp.single (Sum.inr i) 1, inj' := ⋯ }
⊢ sumSMulXSMulY c = AddMonoidAlgebra.ofCoeff ((Finsupp.embDomain ι c).sum Finsupp.single)

Tactic:
]

Goal state after:
n : Type u_1
R : Type u_2
inst✝¹ : CommRing R
c : n →₀ R
inst✝ : IsDomain R
hc : c.support.Nontrivial
h_dvd : ∀ (r : R), (∀ (i : n), r ∣ c i) → IsUnit r
ι : n ↪ n ⊕ n →₀ ℕ := { toFun := fun i ↦ Finsupp.single (Sum.inl i) 1 + Finsupp.single (Sum.inr i) 1, inj' := ⋯ }
⊢ sumSMulXSMulY c = AddMonoidAlgebra.ofCoeff ((Finsupp.embDomain ι c).sum Finsupp.single)
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: case h
K : Type u_2
inst✝ : Field K
f : K⸨X⸩
γ : (WithZero (Multiplicative ℤ))ˣ
F : K⟦X⟧ := f.powerSeriesPart
hF : F = f.powerSeriesPart
ord_nonpos : HahnSeries.order f < 0
η : (WithZero (Multiplicative ℤ))ˣ := Units.mk0 (exp (HahnSeries.order f)) ⋯
hη : η = Units.mk0 (exp (HahnSeries.order f)) ⋯
P : K[X]
hP : (PowerSeries.idealX K).intValuation (F - ↑P) < ↑(η * γ)
s : ℕ
F_mul : ((ofPowerSeries ℤ K) (PowerSeries.X ^ s))⁻¹ * (ofPowerSeries ℤ K) F = f
hs : HahnSeries.order f = -↑s
⊢ Valued.v (f - (algebraMap K⟮X⟯ K⸨X⸩) (RatFunc.X ^ HahnSeries.order f * ↑P)) < ↑γ

pp: case h
K : Type u_2
inst✝ : Field K
f : K⸨X⸩
γ : (WithZero (Multiplicative ℤ))ˣ
F : K⟦X⟧ := f.powerSeriesPart
hF : F = f.powerSeriesPart
ord_nonpos : HahnSeries.order f < 0
η : (WithZero (Multiplicative ℤ))ˣ := Units.mk0 (exp (HahnSeries.order f)) ⋯
hη : η = Units.mk0 (exp (HahnSeries.order f)) ⋯
P : K[X]
hP : (PowerSeries.idealX K).intValuation (F - ↑P) < ↑(η * γ)
s : ℕ
F_mul : (ofPowerSeries ℤ K) F = (ofPowerSeries ℤ K) (PowerSeries.X ^ s) * f
hs : HahnSeries.order f = -↑s
⊢ (ofPowerSeries ℤ K) (PowerSeries.X ^ s) ≠ 0

Tactic:
]

Goal state after:
case h
K : Type u_2
inst✝ : Field K
f : K⸨X⸩
γ : (WithZero (Multiplicative ℤ))ˣ
F : K⟦X⟧ := f.powerSeriesPart
hF : F = f.powerSeriesPart
ord_nonpos : HahnSeries.order f < 0
η : (WithZero (Multiplicative ℤ))ˣ := Units.mk0 (exp (HahnSeries.order f)) ⋯
hη : η = Units.mk0 (exp (HahnSeries.order f)) ⋯
P : K[X]
hP : (PowerSeries.idealX K).intValuation (F - ↑P) < ↑(η * γ)
s : ℕ
F_mul : ((ofPowerSeries ℤ K) (PowerSeries.X ^ s))⁻¹ * (ofPowerSeries ℤ K) F = f
hs : HahnSeries.order f = -↑s
⊢ Valued.v (f - (algebraMap K⟮X⟯ K⸨X⸩) (RatFunc.X ^ HahnSeries.order f * ↑P)) < ↑γ

case h
K : Type u_2
inst✝ : Field K
f : K⸨X⸩
γ : (WithZero (Multiplicative ℤ))ˣ
F : K⟦X⟧ := f.powerSeriesPart
hF : F = f.powerSeriesPart
ord_nonpos : HahnSeries.order f < 0
η : (WithZero (Multiplicative ℤ))ˣ := Units.mk0 (exp (HahnSeries.order f)) ⋯
hη : η = Units.mk0 (exp (HahnSeries.order f)) ⋯
P : K[X]
hP : (PowerSeries.idealX K).intValuation (F - ↑P) < ↑(η * γ)
s : ℕ
F_mul : (ofPowerSeries ℤ K) F = (ofPowerSeries ℤ K) (PowerSeries.X ^ s) * f
hs : HahnSeries.order f = -↑s
⊢ (ofPowerSeries ℤ K) (PowerSeries.X ^ s) ≠ 0
Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem

Goal state before:
pp: case refine_2.refine_1
R : Type u_3
m : ℕ
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
i : ℕ
him : i < m
t : Finset (Fin m)
ht : t ∈ powersetCard (i + 1) univ
ht' : #t = #(Iic ⟨i, him⟩)
hne : ∃ x, x ∈ Iic ⟨i, him⟩ \ t
hkm : (Iic ⟨i, him⟩ \ t).min' hne ∈ Iic ⟨i, him⟩ ∧ (Iic ⟨i, him⟩ \ t).min' hne ∉ t
k : Fin m
hk : (fun x1 x2 ↦ x1 < x2) k ((Iic ⟨i, him⟩ \ t).min' hne)
hki : k ∈ Iic ⟨i, him⟩
⊢ 1 = 1

pp: case refine_2.refine_1.hc
R : Type u_3
m : ℕ
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
i : ℕ
him : i < m
t : Finset (Fin m)
ht : t ∈ powersetCard (i + 1) univ
ht' : #t = #(Iic ⟨i, him⟩)
hne : ∃ x, x ∈ Iic ⟨i, him⟩ \ t
hkm : (Iic ⟨i, him⟩ \ t).min' hne ∈ Iic ⟨i, him⟩ ∧ (Iic ⟨i, him⟩ \ t).min' hne ∉ t
k : Fin m
hk : (fun x1 x2 ↦ x1 < x2) k ((Iic ⟨i, him⟩ \ t).min' hne)
hki : k ∈ Iic ⟨i, him⟩
⊢ k ∈ t

Tactic:
]

Goal state after:
case refine_2.refine_1.hc
R : Type u_3
m : ℕ
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
i : ℕ
him : i < m
t : Finset (Fin m)
ht : t ∈ powersetCard (i + 1) univ
ht' : #t = #(Iic ⟨i, him⟩)
hne : ∃ x, x ∈ Iic ⟨i, him⟩ \ t
hkm : (Iic ⟨i, him⟩ \ t).min' hne ∈ Iic ⟨i, him⟩ ∧ (Iic ⟨i, him⟩ \ t).min' hne ∉ t
k : Fin m
hk : (fun x1 x2 ↦ x1 < x2) k ((Iic ⟨i, him⟩ \ t).min' hne)
hki : k ∈ Iic ⟨i, him⟩
⊢ k ∈ t
Module: Mathlib.RingTheory.MvPolynomial.IrreducibleQuadratic

Goal state before:
pp: case nontrivial
n : Type u_1
R : Type u_2
inst✝¹ : CommRing R
c : n →₀ R
inst✝ : IsDomain R
hc : c.support.Nontrivial
h_dvd : ∀ (r : R), (∀ (i : n), r ∣ c i) → IsUnit r
ι : n ↪ n ⊕ n →₀ ℕ := { toFun := fun i ↦ Finsupp.single (Sum.inl i) 1 + Finsupp.single (Sum.inr i) 1, inj' := ⋯ }
aux : sumSMulXSMulY c = AddMonoidAlgebra.ofCoeff (Finsupp.embDomain ι c)
hcoeff : ∀ (i : n), coeff (ι i) (sumSMulXSMulY c) = c i
hsupp : (sumSMulXSMulY c).support = Finset.map ι c.support
a : n
ha : a ∈ c.support
⊢ c.support.Nontrivial

Tactic:
]

Goal state after:
case nontrivial
n : Type u_1
R : Type u_2
inst✝¹ : CommRing R
c : n →₀ R
inst✝ : IsDomain R
hc : c.support.Nontrivial
h_dvd : ∀ (r : R), (∀ (i : n), r ∣ c i) → IsUnit r
ι : n ↪ n ⊕ n →₀ ℕ := { toFun := fun i ↦ Finsupp.single (Sum.inl i) 1 + Finsupp.single (Sum.inr i) 1, inj' := ⋯ }
aux : sumSMulXSMulY c = AddMonoidAlgebra.ofCoeff (Finsupp.embDomain ι c)
hcoeff : ∀ (i : n), coeff (ι i) (sumSMulXSMulY c) = c i
hsupp : (sumSMulXSMulY c).support = Finset.map ι c.support
a : n
ha : a ∈ c.support
⊢ c.support.Nontrivial
Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem

Goal state before:
pp: case refine_2.refine_2
R : Type u_3
m : ℕ
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
i : ℕ
him : i < m
t : Finset (Fin m)
ht : t ∈ powersetCard (i + 1) univ
ht' : #t = #(Iic ⟨i, him⟩)
hne : ∃ x, x ∈ Iic ⟨i, him⟩ \ t
hkm : (Iic ⟨i, him⟩ \ t).min' hne ∈ Iic ⟨i, him⟩ ∧ (Iic ⟨i, him⟩ \ t).min' hne ∉ t
⊢ 0 < 1

Tactic:
]

Goal state after:
case refine_2.refine_2
R : Type u_3
m : ℕ
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
i : ℕ
him : i < m
t : Finset (Fin m)
ht : t ∈ powersetCard (i + 1) univ
ht' : #t = #(Iic ⟨i, him⟩)
hne : ∃ x, x ∈ Iic ⟨i, him⟩ \ t
hkm : (Iic ⟨i, him⟩ \ t).min' hne ∈ Iic ⟨i, him⟩ ∧ (Iic ⟨i, him⟩ \ t).min' hne ∉ t
⊢ 0 < 1
Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem

Goal state before:
pp: R : Type u_3
n m : ℕ
inst✝¹ : CommSemiring R
i : Fin n
inst✝ : Nontrivial R
him : ↑i < m
⊢ ⇑(Finsupp.indicator (Iic ⟨↑i, him⟩) fun x x_1 ↦ 1) = (accumulate n m) ⇑fun₀ | i => 1

Tactic:
]

Goal state after:
R : Type u_3
n m : ℕ
inst✝¹ : CommSemiring R
i : Fin n
inst✝ : Nontrivial R
him : ↑i < m
⊢ ⇑(Finsupp.indicator (Iic ⟨↑i, him⟩) fun x x_1 ↦ 1) = (accumulate n m) ⇑fun₀ | i => 1
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: case h
K : Type u_2
inst✝ : Field K
f : K⸨X⸩
γ : (WithZero (Multiplicative ℤ))ˣ
F : K⟦X⟧ := f.powerSeriesPart
hF : F = f.powerSeriesPart
ord_nonpos : HahnSeries.order f < 0
η : (WithZero (Multiplicative ℤ))ˣ := Units.mk0 (exp (HahnSeries.order f)) ⋯
hη : η = Units.mk0 (exp (HahnSeries.order f)) ⋯
P : K[X]
hP : (PowerSeries.idealX K).intValuation (F - ↑P) < ↑(η * γ)
s : ℕ
F_mul : ((ofPowerSeries ℤ K) (PowerSeries.X ^ s))⁻¹ * (ofPowerSeries ℤ K) F = f
hs : HahnSeries.order f = -↑s
this : (algebraMap K⟮X⟯ K⸨X⸩) 1 = 1
⊢ Valued.v
      (((single 1) 1 ^ s)⁻¹ * (ofPowerSeries ℤ K) F -
        (algebraMap K⟮X⟯ K⸨X⸩) 1 / (single 1) 1 ^ s * (algebraMap K⟮X⟯ K⸨X⸩) ↑P) <
    ↑γ

Tactic:
]

Goal state after:
case h
K : Type u_2
inst✝ : Field K
f : K⸨X⸩
γ : (WithZero (Multiplicative ℤ))ˣ
F : K⟦X⟧ := f.powerSeriesPart
hF : F = f.powerSeriesPart
ord_nonpos : HahnSeries.order f < 0
η : (WithZero (Multiplicative ℤ))ˣ := Units.mk0 (exp (HahnSeries.order f)) ⋯
hη : η = Units.mk0 (exp (HahnSeries.order f)) ⋯
P : K[X]
hP : (PowerSeries.idealX K).intValuation (F - ↑P) < ↑(η * γ)
s : ℕ
F_mul : ((ofPowerSeries ℤ K) (PowerSeries.X ^ s))⁻¹ * (ofPowerSeries ℤ K) F = f
hs : HahnSeries.order f = -↑s
this : (algebraMap K⟮X⟯ K⸨X⸩) 1 = 1
⊢ Valued.v
      (((single 1) 1 ^ s)⁻¹ * (ofPowerSeries ℤ K) F -
        (algebraMap K⟮X⟯ K⸨X⸩) 1 / (single 1) 1 ^ s * (algebraMap K⟮X⟯ K⸨X⸩) ↑P) <
    ↑γ
Module: Mathlib.RingTheory.MvPolynomial.IrreducibleQuadratic

Goal state before:
pp: case hd
n : Type u_1
R : Type u_2
inst✝¹ : CommRing R
c : n →₀ R
inst✝ : IsDomain R
hc : c.support.Nontrivial
h_dvd : ∀ (r : R), (∀ (i : n), r ∣ c i) → IsUnit r
ι : n ↪ n ⊕ n →₀ ℕ := { toFun := fun i ↦ Finsupp.single (Sum.inl i) 1 + Finsupp.single (Sum.inr i) 1, inj' := ⋯ }
aux : sumSMulXSMulY c = AddMonoidAlgebra.ofCoeff (Finsupp.embDomain ι c)
hcoeff : ∀ (i : n), coeff (ι i) (sumSMulXSMulY c) = c i
hsupp : (sumSMulXSMulY c).support = Finset.map ι c.support
a : n
ha : a ∈ c.support
⊢ a ∈ c.support

Tactic:
]

Goal state after:
case hd
n : Type u_1
R : Type u_2
inst✝¹ : CommRing R
c : n →₀ R
inst✝ : IsDomain R
hc : c.support.Nontrivial
h_dvd : ∀ (r : R), (∀ (i : n), r ∣ c i) → IsUnit r
ι : n ↪ n ⊕ n →₀ ℕ := { toFun := fun i ↦ Finsupp.single (Sum.inl i) 1 + Finsupp.single (Sum.inr i) 1, inj' := ⋯ }
aux : sumSMulXSMulY c = AddMonoidAlgebra.ofCoeff (Finsupp.embDomain ι c)
hcoeff : ∀ (i : n), coeff (ι i) (sumSMulXSMulY c) = c i
hsupp : (sumSMulXSMulY c).support = Finset.map ι c.support
a : n
ha : a ∈ c.support
⊢ a ∈ c.support
Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem

Goal state before:
pp: case zero
R : Type u_3
m : ℕ
inst✝ : CommSemiring R
him : 0 ≤ m
⊢ Monic (⇑toLex) 1

Tactic:
]

Goal state after:
case zero
R : Type u_3
m : ℕ
inst✝ : CommSemiring R
him : 0 ≤ m
⊢ Monic (⇑toLex) 1
Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem

Goal state before:
pp: case zero
R : Type u_3
n m : ℕ
inst✝ : CommSemiring R
r : R
hnm : n ≤ m
⊢ r = r

Tactic:
]

Goal state after:
Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem

Goal state before:
pp: case add_single
R : Type u_3
n m : ℕ
inst✝ : CommSemiring R
r : R
hnm : n ≤ m
i : Fin n
b✝ : ℕ
f✝ : Fin n →₀ ℕ
a✝¹ : i ∉ f✝.support
a✝ : b✝ ≠ 0
ih : leadingCoeff (⇑toLex) (esymmAlgHomMonomial (Fin m) f✝ r) = r
⊢ r = r

pp: case add_single.hD
R : Type u_3
n m : ℕ
inst✝ : CommSemiring R
r : R
hnm : n ≤ m
i : Fin n
b✝ : ℕ
f✝ : Fin n →₀ ℕ
a✝¹ : i ∉ f✝.support
a✝ : b✝ ≠ 0
ih : leadingCoeff (⇑toLex) (esymmAlgHomMonomial (Fin m) f✝ r) = r
⊢ Function.Injective ⇑toLex

pp: case add_single.hadd
R : Type u_3
n m : ℕ
inst✝ : CommSemiring R
r : R
hnm : n ≤ m
i : Fin n
b✝ : ℕ
f✝ : Fin n →₀ ℕ
a✝¹ : i ∉ f✝.support
a✝ : b✝ ≠ 0
ih : leadingCoeff (⇑toLex) (esymmAlgHomMonomial (Fin m) f✝ r) = r
⊢ ∀ (a1 a2 : Fin m →₀ ℕ), toLex (a1 + a2) = toLex a1 + toLex a2

Tactic:
]

Goal state after:
case add_single.hD
R : Type u_3
n m : ℕ
inst✝ : CommSemiring R
r : R
hnm : n ≤ m
i : Fin n
b✝ : ℕ
f✝ : Fin n →₀ ℕ
a✝¹ : i ∉ f✝.support
a✝ : b✝ ≠ 0
ih : leadingCoeff (⇑toLex) (esymmAlgHomMonomial (Fin m) f✝ r) = r
⊢ Function.Injective ⇑toLex

case add_single.hadd
R : Type u_3
n m : ℕ
inst✝ : CommSemiring R
r : R
hnm : n ≤ m
i : Fin n
b✝ : ℕ
f✝ : Fin n →₀ ℕ
a✝¹ : i ∉ f✝.support
a✝ : b✝ ≠ 0
ih : leadingCoeff (⇑toLex) (esymmAlgHomMonomial (Fin m) f✝ r) = r
⊢ ∀ (a1 a2 : Fin m →₀ ℕ), toLex (a1 + a2) = toLex a1 + toLex a2
Module: Mathlib.RingTheory.MvPolynomial.IrreducibleQuadratic

Goal state before:
pp: case disjoint
n : Type u_1
R : Type u_2
inst✝¹ : CommRing R
c : n →₀ R
inst✝ : IsDomain R
hc : c.support.Nontrivial
h_dvd : ∀ (r : R), (∀ (i : n), r ∣ c i) → IsUnit r
ι : n ↪ n ⊕ n →₀ ℕ := { toFun := fun i ↦ Finsupp.single (Sum.inl i) 1 + Finsupp.single (Sum.inr i) 1, inj' := ⋯ }
aux : sumSMulXSMulY c = AddMonoidAlgebra.ofCoeff (Finsupp.embDomain ι c)
hcoeff : ∀ (i : n), coeff (ι i) (sumSMulXSMulY c) = c i
hsupp : (sumSMulXSMulY c).support = Finset.map ι c.support
a : n
ha : a ∈ c.support
⊢ (↑c.support).PairwiseDisjoint (Finsupp.support ∘ ⇑ι)

Tactic:
]

Goal state after:
case disjoint
n : Type u_1
R : Type u_2
inst✝¹ : CommRing R
c : n →₀ R
inst✝ : IsDomain R
hc : c.support.Nontrivial
h_dvd : ∀ (r : R), (∀ (i : n), r ∣ c i) → IsUnit r
ι : n ↪ n ⊕ n →₀ ℕ := { toFun := fun i ↦ Finsupp.single (Sum.inl i) 1 + Finsupp.single (Sum.inr i) 1, inj' := ⋯ }
aux : sumSMulXSMulY c = AddMonoidAlgebra.ofCoeff (Finsupp.embDomain ι c)
hcoeff : ∀ (i : n), coeff (ι i) (sumSMulXSMulY c) = c i
hsupp : (sumSMulXSMulY c).support = Finset.map ι c.support
a : n
ha : a ∈ c.support
⊢ (↑c.support).PairwiseDisjoint (Finsupp.support ∘ ⇑ι)
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: case h
K : Type u_2
inst✝ : Field K
f : K⸨X⸩
γ : (WithZero (Multiplicative ℤ))ˣ
F : K⟦X⟧ := f.powerSeriesPart
hF : F = f.powerSeriesPart
ord_nonpos : HahnSeries.order f < 0
η : (WithZero (Multiplicative ℤ))ˣ := Units.mk0 (exp (HahnSeries.order f)) ⋯
hη : η = Units.mk0 (exp (HahnSeries.order f)) ⋯
P : K[X]
hP : (PowerSeries.idealX K).intValuation (F - ↑P) < ↑(η * γ)
s : ℕ
F_mul : ((ofPowerSeries ℤ K) (PowerSeries.X ^ s))⁻¹ * (ofPowerSeries ℤ K) F = f
hs : HahnSeries.order f = -↑s
this : (algebraMap K⟮X⟯ K⸨X⸩) 1 = 1
⊢ (↑η)⁻¹ * (PowerSeries.idealX K).intValuation (F - ↑P) < ↑γ

Tactic:
]

Goal state after:
case h
K : Type u_2
inst✝ : Field K
f : K⸨X⸩
γ : (WithZero (Multiplicative ℤ))ˣ
F : K⟦X⟧ := f.powerSeriesPart
hF : F = f.powerSeriesPart
ord_nonpos : HahnSeries.order f < 0
η : (WithZero (Multiplicative ℤ))ˣ := Units.mk0 (exp (HahnSeries.order f)) ⋯
hη : η = Units.mk0 (exp (HahnSeries.order f)) ⋯
P : K[X]
hP : (PowerSeries.idealX K).intValuation (F - ↑P) < ↑(η * γ)
s : ℕ
F_mul : ((ofPowerSeries ℤ K) (PowerSeries.X ^ s))⁻¹ * (ofPowerSeries ℤ K) F = f
hs : HahnSeries.order f = -↑s
this : (algebraMap K⟮X⟯ K⸨X⸩) 1 = 1
⊢ (↑η)⁻¹ * (PowerSeries.idealX K).intValuation (F - ↑P) < ↑γ
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: case h
K : Type u_2
inst✝ : Field K
f : K⸨X⸩
γ : (WithZero (Multiplicative ℤ))ˣ
F : K⟦X⟧ := f.powerSeriesPart
hF : F = f.powerSeriesPart
ord_nonpos : HahnSeries.order f < 0
η : (WithZero (Multiplicative ℤ))ˣ := Units.mk0 (exp (HahnSeries.order f)) ⋯
hη : η = Units.mk0 (exp (HahnSeries.order f)) ⋯
P : K[X]
hP : (PowerSeries.idealX K).intValuation (F - ↑P) < ↑(η * γ)
s : ℕ
F_mul : ((ofPowerSeries ℤ K) (PowerSeries.X ^ s))⁻¹ * (ofPowerSeries ℤ K) F = f
hs : HahnSeries.order f = -↑s
this : (algebraMap K⟮X⟯ K⸨X⸩) 1 = 1
⊢ (PowerSeries.idealX K).intValuation (F - ↑P) < ↑(η * γ)

Tactic:
]

Goal state after:
case h
K : Type u_2
inst✝ : Field K
f : K⸨X⸩
γ : (WithZero (Multiplicative ℤ))ˣ
F : K⟦X⟧ := f.powerSeriesPart
hF : F = f.powerSeriesPart
ord_nonpos : HahnSeries.order f < 0
η : (WithZero (Multiplicative ℤ))ˣ := Units.mk0 (exp (HahnSeries.order f)) ⋯
hη : η = Units.mk0 (exp (HahnSeries.order f)) ⋯
P : K[X]
hP : (PowerSeries.idealX K).intValuation (F - ↑P) < ↑(η * γ)
s : ℕ
F_mul : ((ofPowerSeries ℤ K) (PowerSeries.X ^ s))⁻¹ * (ofPowerSeries ℤ K) F = f
hs : HahnSeries.order f = -↑s
this : (algebraMap K⟮X⟯ K⸨X⸩) 1 = 1
⊢ (PowerSeries.idealX K).intValuation (F - ↑P) < ↑(η * γ)