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

Goal state before:
pp: case left
K : Type u_2
inst✝ : Field K
ℱ : Filter K⸨X⸩
hℱ : Cauchy ℱ
D : ℤ
φ : ℤ → Set K⸨X⸩ := ⋯
intersec₁ : ⋂ n ∈ Set.Iio D, φ n ⊆ {x | ∀ d < D, coeff hℱ d = x.coeff d}
ℓ : ℤ := ⋯
N : ℤ := ⋯
intersec₂ : ⋂ n ∈ Set.Iio D, φ n ⊇ (⋂ n ∈ Set.Iio ℓ, φ n) ∩ ⋂ n ∈ Set.Icc ℓ N, φ n
⊢ ⋂ n, ⋂ (_ : n < ℓ), φ n ∈ ℱ

pp: case right
K : Type u_2
inst✝ : Field K
ℱ : Filter K⸨X⸩
hℱ : Cauchy ℱ
D : ℤ
φ : ℤ → Set K⸨X⸩ := ⋯
intersec₁ : ⋂ n ∈ Set.Iio D, φ n ⊆ {x | ∀ d < D, coeff hℱ d = x.coeff d}
ℓ : ℤ := ⋯
N : ℤ := ⋯
intersec₂ : ⋂ n ∈ Set.Iio D, φ n ⊇ (⋂ n ∈ Set.Iio ℓ, φ n) ∩ ⋂ n ∈ Set.Icc ℓ N, φ n
⊢ ⋂ n ∈ Set.Icc ℓ N, φ n ∈ ℱ

Tactic:
·

Goal state after:
case left
K : Type u_2
inst✝ : Field K
ℱ : Filter K⸨X⸩
hℱ : Cauchy ℱ
D : ℤ
φ : ℤ → Set K⸨X⸩ := ⋯
intersec₁ : ⋂ n ∈ Set.Iio D, φ n ⊆ {x | ∀ d < D, coeff hℱ d = x.coeff d}
ℓ : ℤ := ⋯
N : ℤ := ⋯
intersec₂ : ⋂ n ∈ Set.Iio D, φ n ⊇ (⋂ n ∈ Set.Iio ℓ, φ n) ∩ ⋂ n ∈ Set.Icc ℓ N, φ n
⊢ ⋂ n, ⋂ (_ : n < ℓ), φ n ∈ ℱ
Module: Mathlib.RingTheory.MvPolynomial.IrreducibleQuadratic

Goal state before:
pp: case hig
n : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : IsDomain R
f : MvPolynomial n R
nontrivial : f.support.Nontrivial
d : n →₀ ℕ
hd : d ∈ f.support
i : n
hdi : d i = 1
disjoint : (↑f.support).PairwiseDisjoint Finsupp.support
isPrimitive : ∀ (r : R), (∀ (d : n →₀ ℕ), r ∣ coeff d f) → IsUnit r
hfd : coeff d f ≠ 0
d₀ : n →₀ ℕ := ⋯
φ : MvPolynomial n R := ⋯
ψ : MvPolynomial n R := ⋯
hf : f = φ * X i + ψ
hφ : φ * X i = (monomial d) (coeff d f)
hdψ : ∀ (k : n →₀ ℕ), coeff k ψ = if d = k then 0 else coeff k f
⊢ i ∉ ψ.vars

pp: case h
n : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : IsDomain R
f : MvPolynomial n R
nontrivial : f.support.Nontrivial
d : n →₀ ℕ
hd : d ∈ f.support
i : n
hdi : d i = 1
disjoint : (↑f.support).PairwiseDisjoint Finsupp.support
isPrimitive : ∀ (r : R), (∀ (d : n →₀ ℕ), r ∣ coeff d f) → IsUnit r
hfd : coeff d f ≠ 0
d₀ : n →₀ ℕ := ⋯
φ : MvPolynomial n R := ⋯
ψ : MvPolynomial n R := ⋯
hf : f = φ * X i + ψ
hφ : φ * X i = (monomial d) (coeff d f)
hdψ : ∀ (k : n →₀ ℕ), coeff k ψ = if d = k then 0 else coeff k f
⊢ IsRelPrime φ ψ

Tactic:
·

Goal state after:
case hig
n : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : IsDomain R
f : MvPolynomial n R
nontrivial : f.support.Nontrivial
d : n →₀ ℕ
hd : d ∈ f.support
i : n
hdi : d i = 1
disjoint : (↑f.support).PairwiseDisjoint Finsupp.support
isPrimitive : ∀ (r : R), (∀ (d : n →₀ ℕ), r ∣ coeff d f) → IsUnit r
hfd : coeff d f ≠ 0
d₀ : n →₀ ℕ := ⋯
φ : MvPolynomial n R := ⋯
ψ : MvPolynomial n R := ⋯
hf : f = φ * X i + ψ
hφ : φ * X i = (monomial d) (coeff d f)
hdψ : ∀ (k : n →₀ ℕ), coeff k ψ = if d = k then 0 else coeff k f
⊢ i ∉ ψ.vars
Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem

Goal state before:
pp: case e'_3.e'_6.h
i n m : ℕ
hin : i < n
him : i + 1 < m
t : Fin n → ℕ
⊢ {x | i + 1 ≤ ↑x} = {x | i ≤ ↑x}.erase ⟨i, hin⟩

pp: case convert_3
i n m : ℕ
hin : i < n
him : i + 1 < m
t : Fin n → ℕ
⊢ DecidableEq (Fin n)

pp: case convert_7
i n m : ℕ
hin : i < n
him : i + 1 < m
t : Fin n → ℕ
⊢ ⟨i, hin⟩ ∈ {x | i ≤ ↑x}

Tactic:
·

Goal state after:
case e'_3.e'_6.h
i n m : ℕ
hin : i < n
him : i + 1 < m
t : Fin n → ℕ
⊢ {x | i + 1 ≤ ↑x} = {x | i ≤ ↑x}.erase ⟨i, hin⟩
Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem

Goal state before:
pp: case convert_7
i n m : ℕ
hin : i < n
him : i + 1 < m
t : Fin n → ℕ
⊢ ⟨i, hin⟩ ∈ {x | i ≤ ↑x}

Tactic:
·

Goal state after:
case convert_7
i n m : ℕ
hin : i < n
him : i + 1 < m
t : Fin n → ℕ
⊢ ⟨i, hin⟩ ∈ {x | i ≤ ↑x}
Module: Mathlib.RingTheory.MvPolynomial.IrreducibleQuadratic

Goal state before:
pp: case h
n : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : IsDomain R
f : MvPolynomial n R
nontrivial : f.support.Nontrivial
d : n →₀ ℕ
hd : d ∈ f.support
i : n
hdi : d i = 1
disjoint : (↑f.support).PairwiseDisjoint Finsupp.support
isPrimitive : ∀ (r : R), (∀ (d : n →₀ ℕ), r ∣ coeff d f) → IsUnit r
hfd : coeff d f ≠ 0
d₀ : n →₀ ℕ := ⋯
φ : MvPolynomial n R := ⋯
ψ : MvPolynomial n R := ⋯
hf : f = φ * X i + ψ
hφ : φ * X i = (monomial d) (coeff d f)
hdψ : ∀ (k : n →₀ ℕ), coeff k ψ = if d = k then 0 else coeff k f
⊢ IsRelPrime φ ψ

Tactic:
·

Goal state after:
case h
n : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : IsDomain R
f : MvPolynomial n R
nontrivial : f.support.Nontrivial
d : n →₀ ℕ
hd : d ∈ f.support
i : n
hdi : d i = 1
disjoint : (↑f.support).PairwiseDisjoint Finsupp.support
isPrimitive : ∀ (r : R), (∀ (d : n →₀ ℕ), r ∣ coeff d f) → IsUnit r
hfd : coeff d f ≠ 0
d₀ : n →₀ ℕ := ⋯
φ : MvPolynomial n R := ⋯
ψ : MvPolynomial n R := ⋯
hf : f = φ * X i + ψ
hφ : φ * X i = (monomial d) (coeff d f)
hdψ : ∀ (k : n →₀ ℕ), coeff k ψ = if d = k then 0 else coeff k f
⊢ IsRelPrime φ ψ
Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem

Goal state before:
pp: case h
i n m : ℕ
hin : i < n
hmi : m = i + 1
t : Fin n → ℕ
ht : ∀ (j : Fin n), m ≤ ↑j → t j = 0
⊢ ⟨i, hin⟩ ∈ {i_1 | ↑⟨i, ⋯⟩ ≤ ↑i_1}

pp: case h₀
i n m : ℕ
hin : i < n
hmi : m = i + 1
t : Fin n → ℕ
ht : ∀ (j : Fin n), m ≤ ↑j → t j = 0
⊢ ∀ b ∈ {i_1 | ↑⟨i, ⋯⟩ ≤ ↑i_1}, b ≠ ⟨i, hin⟩ → t b = 0

Tactic:
·

Goal state after:
case h
i n m : ℕ
hin : i < n
hmi : m = i + 1
t : Fin n → ℕ
ht : ∀ (j : Fin n), m ≤ ↑j → t j = 0
⊢ ⟨i, hin⟩ ∈ {i_1 | ↑⟨i, ⋯⟩ ≤ ↑i_1}
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: case right
K : Type u_2
inst✝ : Field K
ℱ : Filter K⸨X⸩
hℱ : Cauchy ℱ
D : ℤ
φ : ℤ → Set K⸨X⸩ := ⋯
intersec₁ : ⋂ n ∈ Set.Iio D, φ n ⊆ {x | ∀ d < D, coeff hℱ d = x.coeff d}
ℓ : ℤ := ⋯
N : ℤ := ⋯
intersec₂ : ⋂ n ∈ Set.Iio D, φ n ⊇ (⋂ n ∈ Set.Iio ℓ, φ n) ∩ ⋂ n ∈ Set.Icc ℓ N, φ n
⊢ ⋂ n ∈ Set.Icc ℓ N, φ n ∈ ℱ

Tactic:
·

Goal state after:
case right
K : Type u_2
inst✝ : Field K
ℱ : Filter K⸨X⸩
hℱ : Cauchy ℱ
D : ℤ
φ : ℤ → Set K⸨X⸩ := ⋯
intersec₁ : ⋂ n ∈ Set.Iio D, φ n ⊆ {x | ∀ d < D, coeff hℱ d = x.coeff d}
ℓ : ℤ := ⋯
N : ℤ := ⋯
intersec₂ : ⋂ n ∈ Set.Iio D, φ n ⊇ (⋂ n ∈ Set.Iio ℓ, φ n) ∩ ⋂ n ∈ Set.Icc ℓ N, φ n
⊢ ⋂ n ∈ Set.Icc ℓ N, φ n ∈ ℱ
Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem

Goal state before:
pp: case inl
n m : ℕ
hnm : n ≤ m
t s : Fin n → ℕ
he : (accumulate n m) t = (accumulate n m) s
i : Fin n
h : ↑i + 1 < m
⊢ t i = s i

pp: case inr
n m : ℕ
hnm : n ≤ m
t s : Fin n → ℕ
he : (accumulate n m) t = (accumulate n m) s
i : Fin n
h : m ≤ ↑i + 1
⊢ t i = s i

Tactic:
·

Goal state after:
case inl
n m : ℕ
hnm : n ≤ m
t s : Fin n → ℕ
he : (accumulate n m) t = (accumulate n m) s
i : Fin n
h : ↑i + 1 < m
⊢ t i = s i
Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem

Goal state before:
pp: case inr
n m : ℕ
hnm : n ≤ m
t s : Fin n → ℕ
he : (accumulate n m) t = (accumulate n m) s
i : Fin n
h : m ≤ ↑i + 1
⊢ t i = s i

Tactic:
·

Goal state after:
case inr
n m : ℕ
hnm : n ≤ m
t s : Fin n → ℕ
he : (accumulate n m) t = (accumulate n m) s
i : Fin n
h : m ≤ ↑i + 1
⊢ t i = s i
Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem

Goal state before:
pp: case refine_1
n m : ℕ
hmn : m ≤ n
s : Fin m → ℕ
hs : Antitone s
x✝¹ : Fin m
i✝ : ℕ
this : i✝ ≤ m - 1
i : ℕ
hi : i < m - 1
x✝ : i✝ ≤ i
ih : ∀ (hi : i + 1 < m), (accumulate n m) (invAccumulate n m s) ⟨i + 1, hi⟩ = s ⟨i + 1, hi⟩
him : i < m
⊢ (accumulate n m) (invAccumulate n m s) ⟨i, him⟩ = s ⟨i, him⟩

pp: case refine_2
n m : ℕ
hmn : m ≤ n
s : Fin m → ℕ
hs : Antitone s
x✝ : Fin m
i : ℕ
this : i ≤ m - 1
hm : m - 1 < m
⊢ (accumulate n m) (invAccumulate n m s) ⟨m - 1, hm⟩ = s ⟨m - 1, hm⟩

Tactic:
·

Goal state after:
case refine_1
n m : ℕ
hmn : m ≤ n
s : Fin m → ℕ
hs : Antitone s
x✝¹ : Fin m
i✝ : ℕ
this : i✝ ≤ m - 1
i : ℕ
hi : i < m - 1
x✝ : i✝ ≤ i
ih : ∀ (hi : i + 1 < m), (accumulate n m) (invAccumulate n m s) ⟨i + 1, hi⟩ = s ⟨i + 1, hi⟩
him : i < m
⊢ (accumulate n m) (invAccumulate n m s) ⟨i, him⟩ = s ⟨i, him⟩
Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem

Goal state before:
pp: case refine_1
n m : ℕ
hmn : m ≤ n
s : Fin m → ℕ
hs : Antitone s
x✝¹ : Fin m
i✝ : ℕ
this : i✝ ≤ m - 1
i : ℕ
hi : i < m.pred
x✝ : i✝ ≤ i
ih : ∀ (hi : i + 1 < m), (accumulate n m) (invAccumulate n m s) ⟨i + 1, hi⟩ = s ⟨i + 1, hi⟩
him : i < m
⊢ (accumulate n m) (invAccumulate n m s) ⟨i, him⟩ = s ⟨i, him⟩

Tactic:
Nat.lt_pred_iff,

Goal state after:
case refine_1
n m : ℕ
hmn : m ≤ n
s : Fin m → ℕ
hs : Antitone s
x✝¹ : Fin m
i✝ : ℕ
this : i✝ ≤ m - 1
i : ℕ
hi : i.succ < m
x✝ : i✝ ≤ i
ih : ∀ (hi : i + 1 < m), (accumulate n m) (invAccumulate n m s) ⟨i + 1, hi⟩ = s ⟨i + 1, hi⟩
him : i < m
⊢ (accumulate n m) (invAccumulate n m s) ⟨i, him⟩ = s ⟨i, him⟩
Module: Mathlib.RingTheory.MvPolynomial.IrreducibleQuadratic

Goal state before:
pp: case inr
n : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : MvPolynomial n R
hp : p.totalDegree = 1
hp' : ∀ (x : R), (∀ (i : n →₀ ℕ), x ∣ coeff i p) → IsUnit x
a b : MvPolynomial n R
hab : p = a * b
this : ∀ (a b : MvPolynomial n R), p = a * b → a.totalDegree ≤ b.totalDegree → IsUnit a ∨ IsUnit b
hle : ¬a.totalDegree ≤ b.totalDegree
⊢ IsUnit a ∨ IsUnit b

pp: n : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : MvPolynomial n R
hp : p.totalDegree = 1
hp' : ∀ (x : R), (∀ (i : n →₀ ℕ), x ∣ coeff i p) → IsUnit x
a b : MvPolynomial n R
hab : p = a * b
hle : a.totalDegree ≤ b.totalDegree
⊢ IsUnit a ∨ IsUnit b

Tactic:
·

Goal state after:
case inr
n : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : MvPolynomial n R
hp : p.totalDegree = 1
hp' : ∀ (x : R), (∀ (i : n →₀ ℕ), x ∣ coeff i p) → IsUnit x
a b : MvPolynomial n R
hab : p = a * b
this : ∀ (a b : MvPolynomial n R), p = a * b → a.totalDegree ≤ b.totalDegree → IsUnit a ∨ IsUnit b
hle : ¬a.totalDegree ≤ b.totalDegree
⊢ IsUnit a ∨ IsUnit b
Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem

Goal state before:
pp: case refine_2
n m : ℕ
hmn : m ≤ n
s : Fin m → ℕ
hs : Antitone s
x✝ : Fin m
i : ℕ
this : i ≤ m - 1
hm : m - 1 < m
⊢ (accumulate n m) (invAccumulate n m s) ⟨m - 1, hm⟩ = s ⟨m - 1, hm⟩

Tactic:
·

Goal state after:
case refine_2
n m : ℕ
hmn : m ≤ n
s : Fin m → ℕ
hs : Antitone s
x✝ : Fin m
i : ℕ
this : i ≤ m - 1
hm : m - 1 < m
⊢ (accumulate n m) (invAccumulate n m s) ⟨m - 1, hm⟩ = s ⟨m - 1, hm⟩
Module: Mathlib.RingTheory.MvPolynomial.IrreducibleQuadratic

Goal state before:
pp: n : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : MvPolynomial n R
hp : p.totalDegree = 1
hp' : ∀ (x : R), (∀ (i : n →₀ ℕ), x ∣ coeff i p) → IsUnit x
a b : MvPolynomial n R
hab : p = a * b
this : ∀ (a b : MvPolynomial n R), p = a * b → a.totalDegree ≤ b.totalDegree → IsUnit a ∨ IsUnit b
hle : ¬a.totalDegree ≤ b.totalDegree
⊢ b.totalDegree ≤ a.totalDegree

Tactic:
by lia

Goal state after:
Module: Mathlib.RingTheory.MvPolynomial.IrreducibleQuadratic

Goal state before:
pp: case inl
n : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : MvPolynomial n R
hp : p.totalDegree = 1
hp' : ∀ (x : R), (∀ (i : n →₀ ℕ), x ∣ coeff i p) → IsUnit x
b : MvPolynomial n R
hab : p = 0 * b
hle : totalDegree 0 ≤ b.totalDegree
⊢ IsUnit 0 ∨ IsUnit b

pp: case inr
n : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : MvPolynomial n R
hp : p.totalDegree = 1
hp' : ∀ (x : R), (∀ (i : n →₀ ℕ), x ∣ coeff i p) → IsUnit x
a b : MvPolynomial n R
hab : p = a * b
hle : a.totalDegree ≤ b.totalDegree
ha₀ : a ≠ 0
⊢ IsUnit a ∨ IsUnit b

Tactic:
·

Goal state after:
case inl
n : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : MvPolynomial n R
hp : p.totalDegree = 1
hp' : ∀ (x : R), (∀ (i : n →₀ ℕ), x ∣ coeff i p) → IsUnit x
b : MvPolynomial n R
hab : p = 0 * b
hle : totalDegree 0 ≤ b.totalDegree
⊢ IsUnit 0 ∨ IsUnit b
Module: Mathlib.RingTheory.MvPolynomial.IrreducibleQuadratic

Goal state before:
pp: case inr.inl
n : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : MvPolynomial n R
hp : p.totalDegree = 1
hp' : ∀ (x : R), (∀ (i : n →₀ ℕ), x ∣ coeff i p) → IsUnit x
a : MvPolynomial n R
ha₀ : a ≠ 0
hab : p = a * 0
hle : a.totalDegree ≤ totalDegree 0
⊢ IsUnit a ∨ IsUnit 0

pp: case inr.inr
n : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : MvPolynomial n R
hp : p.totalDegree = 1
hp' : ∀ (x : R), (∀ (i : n →₀ ℕ), x ∣ coeff i p) → IsUnit x
a b : MvPolynomial n R
hab : p = a * b
hle : a.totalDegree ≤ b.totalDegree
ha₀ : a ≠ 0
hb₀ : b ≠ 0
⊢ IsUnit a ∨ IsUnit b

Tactic:
·

Goal state after:
case inr.inl
n : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : MvPolynomial n R
hp : p.totalDegree = 1
hp' : ∀ (x : R), (∀ (i : n →₀ ℕ), x ∣ coeff i p) → IsUnit x
a : MvPolynomial n R
ha₀ : a ≠ 0
hab : p = a * 0
hle : a.totalDegree ≤ totalDegree 0
⊢ IsUnit a ∨ IsUnit 0
Module: Mathlib.RingTheory.MvPolynomial.IrreducibleQuadratic

Goal state before:
pp: n : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : MvPolynomial n R
hp : p.totalDegree = 1
hp' : ∀ (x : R), (∀ (i : n →₀ ℕ), x ∣ coeff i p) → IsUnit x
a b : MvPolynomial n R
hab : p = a * b
hle : a.totalDegree ≤ b.totalDegree
ha₀ : a ≠ 0
hb₀ : b ≠ 0
this : a.totalDegree + b.totalDegree = 1
⊢ a.totalDegree = 0

Tactic:
by lia

Goal state after:
Module: Mathlib.RingTheory.MvPolynomial.IrreducibleQuadratic

Goal state before:
pp: n : Type u_1
R : Type u_2
inst✝ : CommRing R
c : n →₀ R
i : n
⊢ coeff (Finsupp.single i 1) (c i • X i) = c i

pp: n : Type u_1
R : Type u_2
inst✝ : CommRing R
c : n →₀ R
i : n
⊢ ∀ b ∈ c.support, b ≠ i → coeff (Finsupp.single i 1) (c b • X b) = 0

Tactic:
·

Goal state after:
n : Type u_1
R : Type u_2
inst✝ : CommRing R
c : n →₀ R
i : n
⊢ coeff (Finsupp.single i 1) (c i • X i) = c i
Module: Mathlib.RingTheory.MvPolynomial.IrreducibleQuadratic

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

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

Goal state after:
n : Type u_1
R : Type u_2
inst✝ : CommRing R
c : n →₀ R
i j : n
hj : j ∈ c.support
hji : j ≠ i
⊢ c j • 0 = 0
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:
·

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
⊢ ¬Finsupp.single j 1 = Finsupp.single i 1
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ℱ)
⊢ ∀ᶠ (f : K⸨X⸩) in ℱ, f ∈ U

Tactic:
obtain ⟨γ, hU₁⟩ := Valued.mem_nhds.mp hU
  suffices ∀ᶠ f in ℱ, f ∈ {y : K⸨X⸩ | Valued.v (y - limit hℱ) < embedding γ.1} by
    simp_rw [← Valued.v.restrict_lt_iff_lt_embedding] at this
    apply this.mono fun _ hf ↦ hU₁ hf
  set D := -(log (embedding γ.1) - 1) with hD₀
  have hD : exp (-D) < embedding γ.1 := by
    rw [← lt_log_iff_exp_lt (by simp), hD₀]
    simp
  apply coeff_eventually_equal (D := D) hℱ |>.mono
  intro _ hf
  apply lt_of_le_of_lt (valuation_le_iff_coeff_lt_eq_zero K |>.mpr _) hD
  intro n hn
  rw [HahnSeries.coeff_sub, sub_eq_zero, eq_comm]
  exact hf _ hn

Goal state after:
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) (∑ j ∈ powersetCard (i + 1) univ, (monomial (∑ j ∈ j, fun₀ | j => 1)) 1) =
      supDegree (⇑toLex) ((monomial (∑ j ≤ ⟨i, him⟩, fun₀ | j => 1)) 1) ∧
    leadingCoeff (⇑toLex) (∑ j ∈ powersetCard (i + 1) univ, (monomial (∑ j ∈ j, fun₀ | j => 1)) 1) =
      leadingCoeff (⇑toLex) ((monomial (∑ j ≤ ⟨i, him⟩, fun₀ | j => 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))

pp: case refine_1
R : Type u_3
m : ℕ
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
i : ℕ
him : i < m
⊢ Iic ⟨i, him⟩ ∈ powersetCard (i + 1) univ

pp: case refine_2
R : Type u_3
m : ℕ
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
i : ℕ
him : i < m
⊢ ∀ j ∈ powersetCard (i + 1) univ,
    j ≠ Iic ⟨i, him⟩ →
      supDegree (⇑toLex) ((monomial (∑ j ∈ j, fun₀ | j => 1)) 1) <
        supDegree (⇑toLex) ((monomial (∑ j ≤ ⟨i, him⟩, fun₀ | j => 1)) 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) (∑ j ∈ powersetCard (i + 1) univ, (monomial (∑ j ∈ j, fun₀ | j => 1)) 1) =
      supDegree (⇑toLex) ((monomial (∑ j ≤ ⟨i, him⟩, fun₀ | j => 1)) 1) ∧
    leadingCoeff (⇑toLex) (∑ j ∈ powersetCard (i + 1) univ, (monomial (∑ j ∈ j, fun₀ | j => 1)) 1) =
      leadingCoeff (⇑toLex) ((monomial (∑ j ≤ ⟨i, him⟩, fun₀ | j => 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.LaurentSeries

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

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

Tactic:
·

Goal state after:
case pos
K : Type u_2
inst✝ : Field K
F : K⟦X⟧
η : (WithZero (Multiplicative ℤ))ˣ
h_neg : 1 < η
⊢ ∃ P, (PowerSeries.idealX K).intValuation (F - ↑P) < ↑η
Module: Mathlib.RingTheory.MvPolynomial.IrreducibleQuadratic

Goal state before:
pp: case hp
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
⊢ (sumSMulX c).totalDegree = 1

pp: case hp'
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
⊢ ∀ (x : R), (∀ (i : n →₀ ℕ), x ∣ coeff i (sumSMulX c)) → IsUnit x

Tactic:
·

Goal state after:
case hp
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
⊢ (sumSMulX c).totalDegree = 1
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: case neg
K : Type u_2
inst✝ : Field K
F : K⟦X⟧
η : (WithZero (Multiplicative ℤ))ˣ
h_neg : η ≤ 1
⊢ ∃ 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 : η ≤ 1
⊢ ∃ P, (PowerSeries.idealX K).intValuation (F - ↑P) < ↑η
Module: Mathlib.RingTheory.MvPolynomial.IrreducibleQuadratic

Goal state before:
pp: case hp.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
⊢ (sumSMulX c).totalDegree ≤ 1

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
⊢ 1 ≤ (sumSMulX c).totalDegree

Tactic:
·

Goal state after:
case hp.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
⊢ (sumSMulX c).totalDegree ≤ 1
Module: Mathlib.RingTheory.LaurentSeries

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

Tactic:
apply (intValuation_le_iff_coeff_lt_eq_zero K _).mpr

Goal state after:
K : Type u_2
inst✝ : Field K
F : K⟦X⟧
η : (WithZero (Multiplicative ℤ))ˣ
h_neg : Multiplicative.toAdd (unzero ⋯) ≤ 0
d : ℕ
hd : Multiplicative.toAdd (unzero ⋯) = -↑d
⊢ ∀ n < d + 1, (PowerSeries.coeff n) (F - ↑((trunc (d + 1)) F)) = 0
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
⊢ 1 ≤ (sumSMulX c).totalDegree

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
⊢ 1 ≤ (sumSMulX c).totalDegree
Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem

Goal state before:
pp: case refine_1
R : Type u_3
m : ℕ
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
i : ℕ
him : i < m
⊢ Iic ⟨i, him⟩ ∈ powersetCard (i + 1) univ

pp: case refine_2
R : Type u_3
m : ℕ
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
i : ℕ
him : i < m
⊢ ∀ j ∈ powersetCard (i + 1) univ,
    j ≠ Iic ⟨i, him⟩ →
      supDegree (⇑toLex) ((monomial (∑ j ∈ j, fun₀ | j => 1)) 1) <
        supDegree (⇑toLex) ((monomial (∑ j ≤ ⟨i, him⟩, fun₀ | j => 1)) 1)

Tactic:
·

Goal state after:
case refine_1
R : Type u_3
m : ℕ
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
i : ℕ
him : i < m
⊢ Iic ⟨i, him⟩ ∈ powersetCard (i + 1) univ
Module: Mathlib.RingTheory.MvPolynomial.IrreducibleQuadratic

Goal state before:
pp: case hp'
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
⊢ ∀ (x : R), (∀ (i : n →₀ ℕ), x ∣ coeff i (sumSMulX c)) → IsUnit x

Tactic:
·

Goal state after:
case hp'
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
⊢ ∀ (x : R), (∀ (i : n →₀ ℕ), x ∣ coeff i (sumSMulX c)) → IsUnit x
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: case ha
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 < ↑η

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))
⊢ ↑(Multiplicative.ofAdd (-1)) < 1

Tactic:
·

Goal state after:
case ha
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 < ↑η
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: case pos
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
⊢ ∃ Q, Valued.v (f - (algebraMap K⟮X⟯ K⸨X⸩) Q) < ↑γ

pp: case neg
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
⊢ ∃ Q, Valued.v (f - (algebraMap K⟮X⟯ K⸨X⸩) Q) < ↑γ

Tactic:
·

Goal state after:
case pos
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
⊢ ∃ Q, Valued.v (f - (algebraMap K⟮X⟯ K⸨X⸩) Q) < ↑γ