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

Goal state before:
pp: case add_single
R : Type u_3
n m : ℕ
inst✝¹ : CommSemiring R
r : R
hr : r ≠ 0
hnm : n ≤ m
inst✝ : Nontrivial R
i : Fin n
b✝ : ℕ
f✝ : Fin n →₀ ℕ
a✝¹ : i ∉ f✝.support
a✝ : b✝ ≠ 0
ih : ⇑(ofLex (supDegree (⇑toLex) (esymmAlgHomMonomial (Fin m) f✝ r))) = (accumulate n m) ⇑f✝
this : ↑i < m
⊢ ((accumulate n m) ⇑f✝ + (accumulate n m) ⇑fun₀ | i => b✝) = (accumulate n m) ⇑f✝ + (accumulate n m) ⇑fun₀ | i => b✝

pp: case add_single
R : Type u_3
n m : ℕ
inst✝¹ : CommSemiring R
r : R
hr : r ≠ 0
hnm : n ≤ m
inst✝ : Nontrivial R
i : Fin n
b✝ : ℕ
f✝ : Fin n →₀ ℕ
a✝¹ : i ∉ f✝.support
a✝ : b✝ ≠ 0
ih : ⇑(ofLex (supDegree (⇑toLex) (esymmAlgHomMonomial (Fin m) f✝ r))) = (accumulate n m) ⇑f✝
this : ↑i < m
⊢ Monic (⇑toLex) (esymm (Fin m) R (↑i + 1))

pp: case add_single.hq
R : Type u_3
n m : ℕ
inst✝¹ : CommSemiring R
r : R
hr : r ≠ 0
hnm : n ≤ m
inst✝ : Nontrivial R
i : Fin n
b✝ : ℕ
f✝ : Fin n →₀ ℕ
a✝¹ : i ∉ f✝.support
a✝ : b✝ ≠ 0
ih : ⇑(ofLex (supDegree (⇑toLex) (esymmAlgHomMonomial (Fin m) f✝ r))) = (accumulate n m) ⇑f✝
this : ↑i < m
⊢ Monic (⇑toLex) (esymm (Fin m) R (↑i + 1) ^ b✝)

pp: case add_single.hp
R : Type u_3
n m : ℕ
inst✝¹ : CommSemiring R
r : R
hr : r ≠ 0
hnm : n ≤ m
inst✝ : Nontrivial R
i : Fin n
b✝ : ℕ
f✝ : Fin n →₀ ℕ
a✝¹ : i ∉ f✝.support
a✝ : b✝ ≠ 0
ih : ⇑(ofLex (supDegree (⇑toLex) (esymmAlgHomMonomial (Fin m) f✝ r))) = (accumulate n m) ⇑f✝
this : ↑i < m
⊢ esymmAlgHomMonomial (Fin m) f✝ r ≠ 0

Tactic:
]

Goal state after:
case add_single
R : Type u_3
n m : ℕ
inst✝¹ : CommSemiring R
r : R
hr : r ≠ 0
hnm : n ≤ m
inst✝ : Nontrivial R
i : Fin n
b✝ : ℕ
f✝ : Fin n →₀ ℕ
a✝¹ : i ∉ f✝.support
a✝ : b✝ ≠ 0
ih : ⇑(ofLex (supDegree (⇑toLex) (esymmAlgHomMonomial (Fin m) f✝ r))) = (accumulate n m) ⇑f✝
this : ↑i < m
⊢ Monic (⇑toLex) (esymm (Fin m) R (↑i + 1))

case add_single.hq
R : Type u_3
n m : ℕ
inst✝¹ : CommSemiring R
r : R
hr : r ≠ 0
hnm : n ≤ m
inst✝ : Nontrivial R
i : Fin n
b✝ : ℕ
f✝ : Fin n →₀ ℕ
a✝¹ : i ∉ f✝.support
a✝ : b✝ ≠ 0
ih : ⇑(ofLex (supDegree (⇑toLex) (esymmAlgHomMonomial (Fin m) f✝ r))) = (accumulate n m) ⇑f✝
this : ↑i < m
⊢ Monic (⇑toLex) (esymm (Fin m) R (↑i + 1) ^ b✝)

case add_single.hp
R : Type u_3
n m : ℕ
inst✝¹ : CommSemiring R
r : R
hr : r ≠ 0
hnm : n ≤ m
inst✝ : Nontrivial R
i : Fin n
b✝ : ℕ
f✝ : Fin n →₀ ℕ
a✝¹ : i ∉ f✝.support
a✝ : b✝ ≠ 0
ih : ⇑(ofLex (supDegree (⇑toLex) (esymmAlgHomMonomial (Fin m) f✝ r))) = (accumulate n m) ⇑f✝
this : ↑i < m
⊢ esymmAlgHomMonomial (Fin m) f✝ r ≠ 0
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 : 0 ≤ HahnSeries.order f
s : ℕ
hs : -HahnSeries.order f = -↑s
P : K[X]
hP : (PowerSeries.idealX K).intValuation (PowerSeries.X ^ s * F - ↑P) < ↑γ
⊢ (PowerSeries.idealX K).intValuation (PowerSeries.X ^ s * f.powerSeriesPart - ↑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 : 0 ≤ HahnSeries.order f
s : ℕ
hs : -HahnSeries.order f = -↑s
P : K[X]
hP : (PowerSeries.idealX K).intValuation (PowerSeries.X ^ s * F - ↑P) < ↑γ
⊢ (PowerSeries.idealX K).intValuation (PowerSeries.X ^ s * f.powerSeriesPart - ↑P) < ↑γ
Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem

Goal state before:
pp: case add_single.hp
R : Type u_3
n m : ℕ
inst✝¹ : CommSemiring R
r : R
hr : r ≠ 0
hnm : n ≤ m
inst✝ : Nontrivial R
i : Fin n
b✝ : ℕ
f✝ : Fin n →₀ ℕ
a✝¹ : i ∉ f✝.support
a✝ : b✝ ≠ 0
ih : ⇑(ofLex (supDegree (⇑toLex) (esymmAlgHomMonomial (Fin m) f✝ r))) = (accumulate n m) ⇑f✝
this : ↑i < m
⊢ ¬r = 0

Tactic:
]

Goal state after:
case add_single.hp
R : Type u_3
n m : ℕ
inst✝¹ : CommSemiring R
r : R
hr : r ≠ 0
hnm : n ≤ m
inst✝ : Nontrivial R
i : Fin n
b✝ : ℕ
f✝ : Fin n →₀ ℕ
a✝¹ : i ∉ f✝.support
a✝ : b✝ ≠ 0
ih : ⇑(ofLex (supDegree (⇑toLex) (esymmAlgHomMonomial (Fin m) f✝ r))) = (accumulate n m) ⇑f✝
this : ↑i < m
⊢ ¬r = 0
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: K : Type u_2
inst✝ : Field K
⊢ closure (Set.range ⇑(algebraMap K⟮X⟯ K⸨X⸩)) = Set.univ

Tactic:
]

Goal state after:
K : Type u_2
inst✝ : Field K
⊢ closure (Set.range ⇑(algebraMap K⟮X⟯ K⸨X⸩)) = Set.univ
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: K : Type u_2
inst✝ : Field K
f : K⸨X⸩
V : Set (K⸨X⸩ × K⸨X⸩)
hV : V ∈ Filter.comap (fun x ↦ -x.2 + x.1) (nhds 0)
h_symm : SetRel.IsSymm V
⊢ ∃ a, (algebraMap K⟮X⟯ K⸨X⸩) a ∈ UniformSpace.ball f V

Tactic:
]

Goal state after:
K : Type u_2
inst✝ : Field K
f : K⸨X⸩
V : Set (K⸨X⸩ × K⸨X⸩)
hV : V ∈ Filter.comap (fun x ↦ -x.2 + x.1) (nhds 0)
h_symm : SetRel.IsSymm V
⊢ ∃ a, (algebraMap K⟮X⟯ K⸨X⸩) a ∈ UniformSpace.ball f V
Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem

Goal state before:
pp: case inl
σ : Type u_1
R : Type u_3
inst✝¹ : CommSemiring R
inst✝ : LinearOrder σ
hp : IsSymmetric 0
⊢ Antitone ⇑(ofLex 0)

Tactic:
]

Goal state after:
case inl
σ : Type u_1
R : Type u_3
inst✝¹ : CommSemiring R
inst✝ : LinearOrder σ
hp : IsSymmetric 0
⊢ Antitone ⇑(ofLex 0)
Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem

Goal state before:
pp: case inr
σ : Type u_1
R : Type u_3
inst✝¹ : CommSemiring R
inst✝ : LinearOrder σ
p : MvPolynomial σ R
hp : p.IsSymmetric
h0 : p ≠ 0
⊢ ∀ ⦃a b : σ⦄, a ≤ b → (ofLex (supDegree (⇑toLex) p)) b ≤ (ofLex (supDegree (⇑toLex) p)) a

Tactic:
]

Goal state after:
case inr
σ : Type u_1
R : Type u_3
inst✝¹ : CommSemiring R
inst✝ : LinearOrder σ
p : MvPolynomial σ R
hp : p.IsSymmetric
h0 : p ≠ 0
⊢ ∀ ⦃a b : σ⦄, a ≤ b → (ofLex (supDegree (⇑toLex) p)) b ≤ (ofLex (supDegree (⇑toLex) p)) a
Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem

Goal state before:
pp: σ : Type u_1
R : Type u_3
inst✝¹ : CommSemiring R
inst✝ : LinearOrder σ
p : MvPolynomial σ R
hp : p.IsSymmetric
h0 : p ≠ 0
i j : σ
hle : i ≤ j
hlt : (ofLex (supDegree (⇑toLex) p)) i < (ofLex (supDegree (⇑toLex) p)) j
⊢ coeff ?d p ≠ 0

pp: case d
σ : Type u_1
R : Type u_3
inst✝¹ : CommSemiring R
inst✝ : LinearOrder σ
p : MvPolynomial σ R
hp : p.IsSymmetric
h0 : p ≠ 0
i j : σ
hle : i ≤ j
hlt : (ofLex (supDegree (⇑toLex) p)) i < (ofLex (supDegree (⇑toLex) p)) j
⊢ σ →₀ ℕ

Tactic:
]

Goal state after:
σ : Type u_1
R : Type u_3
inst✝¹ : CommSemiring R
inst✝ : LinearOrder σ
p : MvPolynomial σ R
hp : p.IsSymmetric
h0 : p ≠ 0
i j : σ
hle : i ≤ j
hlt : (ofLex (supDegree (⇑toLex) p)) i < (ofLex (supDegree (⇑toLex) p)) j
⊢ coeff ?d p ≠ 0

case d
σ : Type u_1
R : Type u_3
inst✝¹ : CommSemiring R
inst✝ : LinearOrder σ
p : MvPolynomial σ R
hp : p.IsSymmetric
h0 : p ≠ 0
i j : σ
hle : i ≤ j
hlt : (ofLex (supDegree (⇑toLex) p)) i < (ofLex (supDegree (⇑toLex) p)) j
⊢ σ →₀ ℕ
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: case h
K : Type u_2
inst✝ : Field K
x : K⸨X⸩
hx : ¬Valued.v x = 0
⊢ exp (-((Valued.v x).log • -1)) = Valued.v x

Tactic:
]

Goal state after:
case h
K : Type u_2
inst✝ : Field K
x : K⸨X⸩
hx : ¬Valued.v x = 0
⊢ exp (-((Valued.v x).log • -1)) = Valued.v x
Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem

Goal state before:
pp: σ : Type u_1
R : Type u_3
inst✝¹ : CommSemiring R
inst✝ : LinearOrder σ
p : MvPolynomial σ R
hp : p.IsSymmetric
h0✝ : p ≠ 0
h0 : ¬coeff (ofLex (supDegree (⇑toLex) p)) p = 0
i j : σ
hle : i ≤ j
hlt : (ofLex (supDegree (⇑toLex) p)) i < (ofLex (supDegree (⇑toLex) p)) j
⊢ coeff (?m.142 i j hle hlt) p ≠ 0

Tactic:
]

Goal state after:
σ : Type u_1
R : Type u_3
inst✝¹ : CommSemiring R
inst✝ : LinearOrder σ
p : MvPolynomial σ R
hp : p.IsSymmetric
h0✝ : p ≠ 0
h0 : ¬coeff (ofLex (supDegree (⇑toLex) p)) p = 0
i j : σ
hle : i ≤ j
hlt : (ofLex (supDegree (⇑toLex) p)) i < (ofLex (supDegree (⇑toLex) p)) j
⊢ coeff (?m.142 i j hle hlt) p ≠ 0
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: K : Type u_2
inst✝ : Field K
⊢ { sets := {s | ∃ t ∈ uniformity K⸨X⸩, (fun x ↦ ((algebraMap K⟮X⟯ K⸨X⸩) x.1, (algebraMap K⟮X⟯ K⸨X⸩) x.2)) ⁻¹' t ⊆ s},
      univ_sets := ⋯, sets_of_superset := ⋯, inter_sets := ⋯ } =
    uniformity K⟮X⟯

Tactic:
]

Goal state after:
K : Type u_2
inst✝ : Field K
⊢ { sets := {s | ∃ t ∈ uniformity K⸨X⸩, (fun x ↦ ((algebraMap K⟮X⟯ K⸨X⸩) x.1, (algebraMap K⟮X⟯ K⸨X⸩) x.2)) ⁻¹' t ⊆ s},
      univ_sets := ⋯, sets_of_superset := ⋯, inter_sets := ⋯ } =
    uniformity K⟮X⟯
Module: Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities

Goal state before:
pp: σ : Type u_1
inst✝ : DecidableEq σ
t : Finset σ × σ
⊢ (if h : t.2 ∈ t.1 then (t.1.erase t.2, t.2) else (cons t.2 t.1 h, t.2)) ≠ t

Tactic:
]

Goal state after:
σ : Type u_1
inst✝ : DecidableEq σ
t : Finset σ × σ
⊢ (if h : t.2 ∈ t.1 then (t.1.erase t.2, t.2) else (cons t.2 t.1 h, t.2)) ≠ t
Module: Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities

Goal state before:
pp: case pos
σ : Type u_1
inst✝ : DecidableEq σ
t : Finset σ × σ
h1 : (t.1.erase t.2, t.2).2 ∈ (t.1.erase t.2, t.2).1
ht : (t.1.erase t.2, t.2) = t
⊢ False

Tactic:
]

Goal state after:
case pos
σ : Type u_1
inst✝ : DecidableEq σ
t : Finset σ × σ
h1 : (t.1.erase t.2, t.2).2 ∈ (t.1.erase t.2, t.2).1
ht : (t.1.erase t.2, t.2) = t
⊢ False
Module: Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities

Goal state before:
pp: case neg
σ : Type u_1
inst✝ : DecidableEq σ
t : Finset σ × σ
h1✝ : t.2 ∉ t.1
h1 : (cons t.2 t.1 h1✝, t.2).2 ∉ (cons t.2 t.1 h1✝, t.2).1
ht : (cons t.2 t.1 h1✝, t.2) = t
⊢ False

Tactic:
]

Goal state after:
case neg
σ : Type u_1
inst✝ : DecidableEq σ
t : Finset σ × σ
h1✝ : t.2 ∉ t.1
h1 : (cons t.2 t.1 h1✝, t.2).2 ∉ (cons t.2 t.1 h1✝, t.2).1
ht : (cons t.2 t.1 h1✝, t.2) = t
⊢ False
Module: Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities

Goal state before:
pp: σ : Type u_1
inst✝ : DecidableEq σ
t : Finset σ × σ
⊢ (if h :
        (if h : t.2 ∈ t.1 then (t.1.erase t.2, t.2) else (cons t.2 t.1 h, t.2)).2 ∈
          (if h : t.2 ∈ t.1 then (t.1.erase t.2, t.2) else (cons t.2 t.1 h, t.2)).1 then
      ((if h : t.2 ∈ t.1 then (t.1.erase t.2, t.2) else (cons t.2 t.1 h, t.2)).1.erase
          (if h : t.2 ∈ t.1 then (t.1.erase t.2, t.2) else (cons t.2 t.1 h, t.2)).2,
        (if h : t.2 ∈ t.1 then (t.1.erase t.2, t.2) else (cons t.2 t.1 h, t.2)).2)
    else
      (cons (if h : t.2 ∈ t.1 then (t.1.erase t.2, t.2) else (cons t.2 t.1 h, t.2)).2
          (if h : t.2 ∈ t.1 then (t.1.erase t.2, t.2) else (cons t.2 t.1 h, t.2)).1 h,
        (if h : t.2 ∈ t.1 then (t.1.erase t.2, t.2) else (cons t.2 t.1 h, t.2)).2)) =
    t

Tactic:
]

Goal state after:
σ : Type u_1
inst✝ : DecidableEq σ
t : Finset σ × σ
⊢ (if h :
        (if h : t.2 ∈ t.1 then (t.1.erase t.2, t.2) else (cons t.2 t.1 h, t.2)).2 ∈
          (if h : t.2 ∈ t.1 then (t.1.erase t.2, t.2) else (cons t.2 t.1 h, t.2)).1 then
      ((if h : t.2 ∈ t.1 then (t.1.erase t.2, t.2) else (cons t.2 t.1 h, t.2)).1.erase
          (if h : t.2 ∈ t.1 then (t.1.erase t.2, t.2) else (cons t.2 t.1 h, t.2)).2,
        (if h : t.2 ∈ t.1 then (t.1.erase t.2, t.2) else (cons t.2 t.1 h, t.2)).2)
    else
      (cons (if h : t.2 ∈ t.1 then (t.1.erase t.2, t.2) else (cons t.2 t.1 h, t.2)).2
          (if h : t.2 ∈ t.1 then (t.1.erase t.2, t.2) else (cons t.2 t.1 h, t.2)).1 h,
        (if h : t.2 ∈ t.1 then (t.1.erase t.2, t.2) else (cons t.2 t.1 h, t.2)).2)) =
    t
Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem

Goal state before:
pp: case inr.refine_1
σ : Type u_1
R : Type u_3
inst✝¹ : CommSemiring R
inst✝ : LinearOrder σ
p : MvPolynomial σ R
hp : p.IsSymmetric
h0 : p ≠ 0
i j : σ
hle : i ≤ j
hlt : (ofLex (supDegree (⇑toLex) p)) i < (ofLex (supDegree (⇑toLex) p)) j
k : σ
hk : (fun x1 x2 ↦ x1 < x2) k i
⊢ (ofLex (p.support.sup ⇑toLex)) k = (ofLex (p.coeff.support.sup ⇑toLex)) k

Tactic:
]

Goal state after:
case inr.refine_1
σ : Type u_1
R : Type u_3
inst✝¹ : CommSemiring R
inst✝ : LinearOrder σ
p : MvPolynomial σ R
hp : p.IsSymmetric
h0 : p ≠ 0
i j : σ
hle : i ≤ j
hlt : (ofLex (supDegree (⇑toLex) p)) i < (ofLex (supDegree (⇑toLex) p)) j
k : σ
hk : (fun x1 x2 ↦ x1 < x2) k i
⊢ (ofLex (p.support.sup ⇑toLex)) k = (ofLex (p.coeff.support.sup ⇑toLex)) k
Module: Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities

Goal state before:
pp: σ : Type u_1
inst✝¹ : DecidableEq σ
inst✝ : Fintype σ
k : ℕ
t : Finset σ × σ
h : #t.1 ≤ k ∧ (#t.1 = k → t.2 ∈ t.1)
⊢ #(pairMap σ t).1 ≤ k ∧ (#(pairMap σ t).1 = k → (pairMap σ t).2 ∈ (pairMap σ t).1)

Tactic:
]

Goal state after:
σ : Type u_1
inst✝¹ : DecidableEq σ
inst✝ : Fintype σ
k : ℕ
t : Finset σ × σ
h : #t.1 ≤ k ∧ (#t.1 = k → t.2 ∈ t.1)
⊢ #(pairMap σ t).1 ≤ k ∧ (#(pairMap σ t).1 = k → (pairMap σ t).2 ∈ (pairMap σ t).1)
Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem

Goal state before:
pp: R : Type u_3
n m : ℕ
inst✝ : CommRing R
h : n ≤ m
⊢ ∀ (a : MvPolynomial (Fin n) R), (esymmAlgHom (Fin m) R n) a = 0 → a = 0

Tactic:
]

Goal state after:
R : Type u_3
n m : ℕ
inst✝ : CommRing R
h : n ≤ m
⊢ ∀ (a : MvPolynomial (Fin n) R), (esymmAlgHom (Fin m) R n) a = 0 → a = 0
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: K : Type u_2
inst✝ : Field K
S : Set (K⟮X⟯ × K⟮X⟯)
T : Set (K⸨X⸩ × K⸨X⸩)
pre_T : (fun x ↦ ((algebraMap K⟮X⟯ K⸨X⸩) x.1, (algebraMap K⟮X⟯ K⸨X⸩) x.2)) ⁻¹' T ⊆ S
R : Set K⸨X⸩
hR : R ∈ nhds 0
pre_R : (fun x ↦ x.2 - x.1) ⁻¹' R ⊆ T
d : (MonoidWithZeroHom.ofClass Valued.v).ValueGroup₀ˣ
hd : {y | Valued.v.restrict (y - 0) < ↑d} ⊆ R
x : K⟮X⟯
hx : Valued.v x = embedding ↑d
⊢ ¬(MonoidWithZeroHom.ofClass Valued.v) x = 0

Tactic:
]

Goal state after:
K : Type u_2
inst✝ : Field K
S : Set (K⟮X⟯ × K⟮X⟯)
T : Set (K⸨X⸩ × K⸨X⸩)
pre_T : (fun x ↦ ((algebraMap K⟮X⟯ K⸨X⸩) x.1, (algebraMap K⟮X⟯ K⸨X⸩) x.2)) ⁻¹' T ⊆ S
R : Set K⸨X⸩
hR : R ∈ nhds 0
pre_R : (fun x ↦ x.2 - x.1) ⁻¹' R ⊆ T
d : (MonoidWithZeroHom.ofClass Valued.v).ValueGroup₀ˣ
hd : {y | Valued.v.restrict (y - 0) < ↑d} ⊆ R
x : K⟮X⟯
hx : Valued.v x = embedding ↑d
⊢ ¬(MonoidWithZeroHom.ofClass Valued.v) x = 0
Module: Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities

Goal state before:
pp: case inl
σ : Type u_1
inst✝¹ : DecidableEq σ
inst✝ : Fintype σ
k : ℕ
t : Finset σ × σ
h : #t.1 ≤ k ∧ (#t.1 = k → t.2 ∈ t.1)
h1 : t.2 ∈ t.1
⊢ #(t.1.erase t.2, t.2).1 ≤ k ∧ (#(t.1.erase t.2, t.2).1 = k → (t.1.erase t.2, t.2).2 ∈ (t.1.erase t.2, t.2).1)

Tactic:
]

Goal state after:
case inl
σ : Type u_1
inst✝¹ : DecidableEq σ
inst✝ : Fintype σ
k : ℕ
t : Finset σ × σ
h : #t.1 ≤ k ∧ (#t.1 = k → t.2 ∈ t.1)
h1 : t.2 ∈ t.1
⊢ #(t.1.erase t.2, t.2).1 ≤ k ∧ (#(t.1.erase t.2, t.2).1 = k → (t.1.erase t.2, t.2).2 ∈ (t.1.erase t.2, t.2).1)
Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem

Goal state before:
pp: R : Type u_3
n m : ℕ
inst✝ : CommRing R
h : n ≤ m
p : MvPolynomial (Fin n) R
hp : ¬p = 0
⊢ ¬∑ i ∈ p.support, ↑((esymmAlgHom (Fin m) R n) ((monomial i) (coeff i p))) = 0

Tactic:
]

Goal state after:
R : Type u_3
n m : ℕ
inst✝ : CommRing R
h : n ≤ m
p : MvPolynomial (Fin n) R
hp : ¬p = 0
⊢ ¬∑ i ∈ p.support, ↑((esymmAlgHom (Fin m) R n) ((monomial i) (coeff i p))) = 0
Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem

Goal state before:
pp: case refine_1
R : Type u_3
n m : ℕ
inst✝ : CommRing R
h : n ≤ m
p : MvPolynomial (Fin n) R
hp : ¬p = 0
t : Fin n →₀ ℕ
ht : t ∈ p.support
⊢ ¬coeff t p = 0

Tactic:
]

Goal state after:
case refine_1
R : Type u_3
n m : ℕ
inst✝ : CommRing R
h : n ≤ m
p : MvPolynomial (Fin n) R
hp : ¬p = 0
t : Fin n →₀ ℕ
ht : t ∈ p.support
⊢ ¬coeff t p = 0
Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem

Goal state before:
pp: case refine_1
R : Type u_3
n m : ℕ
inst✝ : CommRing R
h : n ≤ m
p : MvPolynomial (Fin n) R
hp : ¬p = 0
t : Fin n →₀ ℕ
ht : coeff t p ≠ 0
⊢ ¬coeff t p = 0

Tactic:
]

Goal state after:
case refine_1
R : Type u_3
n m : ℕ
inst✝ : CommRing R
h : n ≤ m
p : MvPolynomial (Fin n) R
hp : ¬p = 0
t : Fin n →₀ ℕ
ht : coeff t p ≠ 0
⊢ ¬coeff t p = 0
Module: Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities

Goal state before:
pp: case inl
σ : Type u_1
inst✝¹ : DecidableEq σ
inst✝ : Fintype σ
k : ℕ
t : Finset σ × σ
h1 : t.2 ∈ t.1
h : #t.1 ≤ #t.1 - 1
h2 : #t.1 - 1 = k
⊢ False

Tactic:
]

Goal state after:
case inl
σ : Type u_1
inst✝¹ : DecidableEq σ
inst✝ : Fintype σ
k : ℕ
t : Finset σ × σ
h1 : t.2 ∈ t.1
h : #t.1 ≤ #t.1 - 1
h2 : #t.1 - 1 = k
⊢ False
Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem

Goal state before:
pp: case refine_2
R : Type u_3
n m : ℕ
inst✝ : CommRing R
h : n ≤ m
p : MvPolynomial (Fin n) R
hp : ¬p = 0
t : Fin n →₀ ℕ
ht : coeff t p ≠ 0
s : Fin n →₀ ℕ
hs : coeff s p ≠ 0
he :
  (supDegree ⇑toLex ∘ fun i ↦ ↑((esymmAlgHom (Fin m) R n) ((monomial i) (coeff i p)))) t =
    (supDegree ⇑toLex ∘ fun i ↦ ↑((esymmAlgHom (Fin m) R n) ((monomial i) (coeff i p)))) s
⊢ (accumulate n m) ⇑t = (accumulate n m) ⇑s

Tactic:
]

Goal state after:
case refine_2
R : Type u_3
n m : ℕ
inst✝ : CommRing R
h : n ≤ m
p : MvPolynomial (Fin n) R
hp : ¬p = 0
t : Fin n →₀ ℕ
ht : coeff t p ≠ 0
s : Fin n →₀ ℕ
hs : coeff s p ≠ 0
he :
  (supDegree ⇑toLex ∘ fun i ↦ ↑((esymmAlgHom (Fin m) R n) ((monomial i) (coeff i p)))) t =
    (supDegree ⇑toLex ∘ fun i ↦ ↑((esymmAlgHom (Fin m) R n) ((monomial i) (coeff i p)))) s
⊢ (accumulate n m) ⇑t = (accumulate n m) ⇑s
Module: Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities

Goal state before:
pp: case inr
σ : Type u_1
inst✝¹ : DecidableEq σ
inst✝ : Fintype σ
k : ℕ
t : Finset σ × σ
h : #t.1 ≤ k ∧ (#t.1 = k → t.2 ∈ t.1)
h1 : t.2 ∉ t.1
⊢ #(cons t.2 t.1 h1, t.2).1 ≤ k ∧ (#(cons t.2 t.1 h1, t.2).1 = k → (cons t.2 t.1 h1, t.2).2 ∈ (cons t.2 t.1 h1, t.2).1)

Tactic:
]

Goal state after:
case inr
σ : Type u_1
inst✝¹ : DecidableEq σ
inst✝ : Fintype σ
k : ℕ
t : Finset σ × σ
h : #t.1 ≤ k ∧ (#t.1 = k → t.2 ∈ t.1)
h1 : t.2 ∉ t.1
⊢ #(cons t.2 t.1 h1, t.2).1 ≤ k ∧ (#(cons t.2 t.1 h1, t.2).1 = k → (cons t.2 t.1 h1, t.2).2 ∈ (cons t.2 t.1 h1, t.2).1)
Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem

Goal state before:
pp: case refine_2
R : Type u_3
n m : ℕ
inst✝ : CommRing R
h : n ≤ m
p : MvPolynomial (Fin n) R
hp : ¬p = 0
t : Fin n →₀ ℕ
ht : coeff t p ≠ 0
s : Fin n →₀ ℕ
hs : coeff s p ≠ 0
he : (accumulate n m) ⇑t = (accumulate n m) ⇑s
⊢ (accumulate n m) ⇑t = (accumulate n m) ⇑s

Tactic:
]

Goal state after:
case refine_2
R : Type u_3
n m : ℕ
inst✝ : CommRing R
h : n ≤ m
p : MvPolynomial (Fin n) R
hp : ¬p = 0
t : Fin n →₀ ℕ
ht : coeff t p ≠ 0
s : Fin n →₀ ℕ
hs : coeff s p ≠ 0
he : (accumulate n m) ⇑t = (accumulate n m) ⇑s
⊢ (accumulate n m) ⇑t = (accumulate n m) ⇑s
Module: Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities

Goal state before:
pp: σ : Type u_1
inst✝¹ : DecidableEq σ
inst✝ : Fintype σ
k : ℕ
t : Finset σ × σ
h : t ∈ pairs σ k
⊢ pairMap σ t ∈ pairs σ k

Tactic:
rw [mem_pairs] at h ⊢
  rcases (em (t.snd ∈ t.fst)) with h1 | h1
  · rw [pairMap_of_snd_mem_fst σ h1]
    simp only [h1, implies_true, and_true] at h
    simp only [card_erase_of_mem h1, tsub_le_iff_right, mem_erase, ne_eq, h1]
    refine ⟨le_succ_of_le h, ?_⟩
    by_contra h2
    simp only [not_true_eq_false, and_true, not_forall, not_false_eq_true, exists_prop] at h2
    rw [← h2] at h
    exact not_le_of_gt (sub_lt (card_pos.mpr ⟨t.snd, h1⟩) zero_lt_one) h
  · rw [pairMap_of_snd_notMem_fst σ h1]
    simp only [h1] at h
    simp only [card_cons, mem_cons, true_or, implies_true, and_true]
    exact (le_iff_eq_or_lt.mp h.left).resolve_left h.right

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

Goal state before:
pp: σ : Type u_1
R : Type u_3
n : ℕ
inst✝¹ : Fintype σ
inst✝ : CommRing R
hn : n ≤ Fintype.card σ
⊢ Function.Injective
    (⇑↑(renameSymmetricSubalgebra (Fintype.equivFin σ).symm) ∘ ⇑(esymmAlgHom (Fin (Fintype.card σ)) R n))

Tactic:
]

Goal state after:
σ : Type u_1
R : Type u_3
n : ℕ
inst✝¹ : Fintype σ
inst✝ : CommRing R
hn : n ≤ Fintype.card σ
⊢ Function.Injective
    (⇑↑(renameSymmetricSubalgebra (Fintype.equivFin σ).symm) ∘ ⇑(esymmAlgHom (Fin (Fintype.card σ)) R n))
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: case h.refine_2
K : Type u_2
inst✝ : Field K
S : Set (K⟮X⟯ × K⟮X⟯)
T : Set (K⸨X⸩ × K⸨X⸩)
pre_T : (fun x ↦ ((algebraMap K⟮X⟯ K⸨X⸩) x.1, (algebraMap K⟮X⟯ K⸨X⸩) x.2)) ⁻¹' T ⊆ S
R : Set K⸨X⸩
hR : R ∈ nhds 0
pre_R : (fun x ↦ x.2 - x.1) ⁻¹' R ⊆ T
d : (MonoidWithZeroHom.ofClass Valued.v).ValueGroup₀ˣ
hd : {y | Valued.v.restrict (y - 0) < ↑d} ⊆ R
x✝¹ : K⟮X⟯ × K⟮X⟯
x✝ : x✝¹ ∈ (fun x ↦ x.2 - x.1) ⁻¹' {P | Valued.v P < embedding ↑d}
⊢ Valued.v ((algebraMap K⟮X⟯ K⸨X⸩) (x✝¹.2 - x✝¹.1)) < embedding ↑d

Tactic:
]

Goal state after:
case h.refine_2
K : Type u_2
inst✝ : Field K
S : Set (K⟮X⟯ × K⟮X⟯)
T : Set (K⸨X⸩ × K⸨X⸩)
pre_T : (fun x ↦ ((algebraMap K⟮X⟯ K⸨X⸩) x.1, (algebraMap K⟮X⟯ K⸨X⸩) x.2)) ⁻¹' T ⊆ S
R : Set K⸨X⸩
hR : R ∈ nhds 0
pre_R : (fun x ↦ x.2 - x.1) ⁻¹' R ⊆ T
d : (MonoidWithZeroHom.ofClass Valued.v).ValueGroup₀ˣ
hd : {y | Valued.v.restrict (y - 0) < ↑d} ⊆ R
x✝¹ : K⟮X⟯ × K⟮X⟯
x✝ : x✝¹ ∈ (fun x ↦ x.2 - x.1) ⁻¹' {P | Valued.v P < embedding ↑d}
⊢ Valued.v ((algebraMap K⟮X⟯ K⸨X⸩) (x✝¹.2 - x✝¹.1)) < embedding ↑d
Module: Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝² : CommRing R
inst✝¹ : DecidableEq σ
inst✝ : Fintype σ
k : ℕ
t : Finset σ × σ
h : t ∈ pairs σ k
⊢ (-1) ^ #t.1 * ((∏ a ∈ t.1, X a) * X t.2 ^ (k - #t.1)) +
      (-1) ^ #(pairMap σ t).1 * ((∏ a ∈ (pairMap σ t).1, X a) * X (pairMap σ t).2 ^ (k - #(pairMap σ t).1)) =
    0

Tactic:
]

Goal state after:
σ : Type u_1
R : Type u_2
inst✝² : CommRing R
inst✝¹ : DecidableEq σ
inst✝ : Fintype σ
k : ℕ
t : Finset σ × σ
h : t ∈ pairs σ k
⊢ (-1) ^ #t.1 * ((∏ a ∈ t.1, X a) * X t.2 ^ (k - #t.1)) +
      (-1) ^ #(pairMap σ t).1 * ((∏ a ∈ (pairMap σ t).1, X a) * X (pairMap σ t).2 ^ (k - #(pairMap σ t).1)) =
    0
Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem

Goal state before:
pp: case right
R : Type u_3
inst✝ : CommRing R
n : ℕ
p : MvPolynomial (Fin n) R
hp : p ∈ symmetricSubalgebra (Fin n) R
⊢ ⟨p, hp⟩ ∈ (esymmAlgHom (Fin n) R n).range

Tactic:
]

Goal state after:
case right
R : Type u_3
inst✝ : CommRing R
n : ℕ
p : MvPolynomial (Fin n) R
hp : p ∈ symmetricSubalgebra (Fin n) R
⊢ ⟨p, hp⟩ ∈ (esymmAlgHom (Fin n) R n).range
Module: Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝² : CommRing R
inst✝¹ : DecidableEq σ
inst✝ : Fintype σ
k : ℕ
t : Finset σ × σ
h : #t.1 ≤ k ∧ (#t.1 = k → t.2 ∈ t.1)
⊢ (-1) ^ #t.1 * ((∏ a ∈ t.1, X a) * X t.2 ^ (k - #t.1)) +
      (-1) ^ #(pairMap σ t).1 * ((∏ a ∈ (pairMap σ t).1, X a) * X (pairMap σ t).2 ^ (k - #(pairMap σ t).1)) =
    0

Tactic:
]

Goal state after:
σ : Type u_1
R : Type u_2
inst✝² : CommRing R
inst✝¹ : DecidableEq σ
inst✝ : Fintype σ
k : ℕ
t : Finset σ × σ
h : #t.1 ≤ k ∧ (#t.1 = k → t.2 ∈ t.1)
⊢ (-1) ^ #t.1 * ((∏ a ∈ t.1, X a) * X t.2 ^ (k - #t.1)) +
      (-1) ^ #(pairMap σ t).1 * ((∏ a ∈ (pairMap σ t).1, X a) * X (pairMap σ t).2 ^ (k - #(pairMap σ t).1)) =
    0
Module: Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝² : CommRing R
inst✝¹ : DecidableEq σ
inst✝ : Fintype σ
k : ℕ
t : Finset σ × σ
h : #t.1 ≤ k ∧ (#t.1 = k → t.2 ∈ t.1)
n : ℕ
⊢ (-1) ^ n * -1 = (-1) ^ n * -1

Tactic:
]

Goal state after:
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: case h.refine_2
K : Type u_2
inst✝ : Field K
S : Set (K⟮X⟯ × K⟮X⟯)
T : Set (K⸨X⸩ × K⸨X⸩)
pre_T : (fun x ↦ ((algebraMap K⟮X⟯ K⸨X⸩) x.1, (algebraMap K⟮X⟯ K⸨X⸩) x.2)) ⁻¹' T ⊆ S
R : Set K⸨X⸩
hR : R ∈ nhds 0
pre_R : (fun x ↦ x.2 - x.1) ⁻¹' R ⊆ T
d : (MonoidWithZeroHom.ofClass Valued.v).ValueGroup₀ˣ
hd : {y | Valued.v.restrict (y - 0) < ↑d} ⊆ R
x✝¹ : K⟮X⟯ × K⟮X⟯
x✝ : x✝¹ ∈ (fun x ↦ x.2 - x.1) ⁻¹' {P | Valued.v P < embedding ↑d}
⊢ (polynomialValuationX K) (x✝¹.2 - x✝¹.1) < embedding ↑d

Tactic:
]

Goal state after:
case h.refine_2
K : Type u_2
inst✝ : Field K
S : Set (K⟮X⟯ × K⟮X⟯)
T : Set (K⸨X⸩ × K⸨X⸩)
pre_T : (fun x ↦ ((algebraMap K⟮X⟯ K⸨X⸩) x.1, (algebraMap K⟮X⟯ K⸨X⸩) x.2)) ⁻¹' T ⊆ S
R : Set K⸨X⸩
hR : R ∈ nhds 0
pre_R : (fun x ↦ x.2 - x.1) ⁻¹' R ⊆ T
d : (MonoidWithZeroHom.ofClass Valued.v).ValueGroup₀ˣ
hd : {y | Valued.v.restrict (y - 0) < ↑d} ⊆ R
x✝¹ : K⟮X⟯ × K⟮X⟯
x✝ : x✝¹ ∈ (fun x ↦ x.2 - x.1) ⁻¹' {P | Valued.v P < embedding ↑d}
⊢ (polynomialValuationX K) (x✝¹.2 - x✝¹.1) < embedding ↑d