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

Goal state before:
pp: case refine_1
R : Type u_1
σ : Type u_2
inst✝¹ : CommSemiring R
φ : MvPolynomial σ R
inst✝ : Fintype σ
n : ℕ
w : σ → ℕ
h : φ ∈ Submodule.span R ((fun m ↦ AddMonoidAlgebra.single m 1) '' {d | (weight w) d = n})
m : σ →₀ ℕ
hm : m ∈ {d | (weight w) d = n}
⊢ ∑ x, w x • (X x * (pderiv x) (AddMonoidAlgebra.single m 1)) = n • AddMonoidAlgebra.single m 1

Tactic:
[

Goal state after:
case refine_1
R : Type u_1
σ : Type u_2
inst✝¹ : CommSemiring R
φ : MvPolynomial σ R
inst✝ : Fintype σ
n : ℕ
w : σ → ℕ
h : φ ∈ Submodule.span R ((fun m ↦ AddMonoidAlgebra.single m 1) '' {d | (weight w) d = n})
m : σ →₀ ℕ
hm : m ∈ {d | (weight w) d = n}
⊢ ∑ x, w x • (X x * (pderiv x) (AddMonoidAlgebra.single m 1)) = n • AddMonoidAlgebra.single m 1
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: case h
K : Type u_2
inst✝ : Field K
n : WithZero (Multiplicative ℤ)
hn0 : n = 0
⊢ Valued.v 0 = n

Tactic:
simp [hn0]

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

Goal state before:
pp: case refine_3
R : Type u_1
σ : Type u_2
inst✝¹ : CommSemiring R
φ : MvPolynomial σ R
inst✝ : Fintype σ
n : ℕ
w : σ → ℕ
h : φ ∈ Submodule.span R ((fun m ↦ AddMonoidAlgebra.single m 1) '' {d | (weight w) d = n})
p q : MvPolynomial σ R
x✝¹ : p ∈ Submodule.span R ((fun m ↦ AddMonoidAlgebra.single m 1) '' {d | (weight w) d = n})
x✝ : q ∈ Submodule.span R ((fun m ↦ AddMonoidAlgebra.single m 1) '' {d | (weight w) d = n})
hp : ∑ i, w i • (X i * (pderiv i) p) = n • p
hq : ∑ i, w i • (X i * (pderiv i) q) = n • q
⊢ ∑ i, w i • (X i * (pderiv i) (p + q)) = n • (p + q)

Tactic:
[

Goal state after:
case refine_3
R : Type u_1
σ : Type u_2
inst✝¹ : CommSemiring R
φ : MvPolynomial σ R
inst✝ : Fintype σ
n : ℕ
w : σ → ℕ
h : φ ∈ Submodule.span R ((fun m ↦ AddMonoidAlgebra.single m 1) '' {d | (weight w) d = n})
p q : MvPolynomial σ R
x✝¹ : p ∈ Submodule.span R ((fun m ↦ AddMonoidAlgebra.single m 1) '' {d | (weight w) d = n})
x✝ : q ∈ Submodule.span R ((fun m ↦ AddMonoidAlgebra.single m 1) '' {d | (weight w) d = n})
hp : ∑ i, w i • (X i * (pderiv i) p) = n • p
hq : ∑ i, w i • (X i * (pderiv i) q) = n • q
⊢ ∑ i, w i • (X i * (pderiv i) (p + q)) = n • (p + q)
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: case h.refine_1
K : Type u_2
inst✝ : Field K
uK : UniformSpace K
d : ℤ
S : Set (K × K)
hS : S ∈ uniformity K
γ : (WithZero (Multiplicative ℤ))ˣ := Units.mk0 (exp (-(d + 1))) ⋯
x : K⸨X⸩
hx : Valued.v x = ↑γ
this : Valued.v.restrict x ≠ 0
⊢ {P |
      Valued.v (P.2 - P.1) <
        MonoidWithZeroHom.ValueGroup₀.embedding
          ((MonoidWithZeroHom.ValueGroup₀.restrict₀ (MonoidWithZeroHom.ofClass Valued.v)) x)} ∈
    uniformity K⸨X⸩

Tactic:
[

Goal state after:
case h.refine_1
K : Type u_2
inst✝ : Field K
uK : UniformSpace K
d : ℤ
S : Set (K × K)
hS : S ∈ uniformity K
γ : (WithZero (Multiplicative ℤ))ˣ := Units.mk0 (exp (-(d + 1))) ⋯
x : K⸨X⸩
hx : Valued.v x = ↑γ
this : Valued.v.restrict x ≠ 0
⊢ {P |
      Valued.v (P.2 - P.1) <
        MonoidWithZeroHom.ValueGroup₀.embedding
          ((MonoidWithZeroHom.ValueGroup₀.restrict₀ (MonoidWithZeroHom.ofClass Valued.v)) x)} ∈
    uniformity K⸨X⸩
Module: Mathlib.RingTheory.MvPolynomial.EulerIdentity

Goal state before:
pp: case refine_4
R : Type u_1
σ : Type u_2
inst✝¹ : CommSemiring R
φ : MvPolynomial σ R
inst✝ : Fintype σ
n : ℕ
w : σ → ℕ
h✝ : φ ∈ Submodule.span R ((fun m ↦ AddMonoidAlgebra.single m 1) '' {d | (weight w) d = n})
r : R
p : MvPolynomial σ R
x✝ : p ∈ Submodule.span R ((fun m ↦ AddMonoidAlgebra.single m 1) '' {d | (weight w) d = n})
h : ∑ i, w i • (X i * (pderiv i) p) = n • p
⊢ ∑ i, w i • (X i * (pderiv i) (r • p)) = n • r • p

Tactic:
[

Goal state after:
case refine_4
R : Type u_1
σ : Type u_2
inst✝¹ : CommSemiring R
φ : MvPolynomial σ R
inst✝ : Fintype σ
n : ℕ
w : σ → ℕ
h✝ : φ ∈ Submodule.span R ((fun m ↦ AddMonoidAlgebra.single m 1) '' {d | (weight w) d = n})
r : R
p : MvPolynomial σ R
x✝ : p ∈ Submodule.span R ((fun m ↦ AddMonoidAlgebra.single m 1) '' {d | (weight w) d = n})
h : ∑ i, w i • (X i * (pderiv i) p) = n • p
⊢ ∑ i, w i • (X i * (pderiv i) (r • p)) = n • r • p
Module: Mathlib.RingTheory.MvPolynomial.EulerIdentity

Goal state before:
pp: R : Type u_1
σ : Type u_2
inst✝¹ : CommSemiring R
φ : MvPolynomial σ R
inst✝ : Fintype σ
n : ℕ
h : φ.IsHomogeneous n
⊢ ∑ i, X i * (pderiv i) φ = n • φ

Tactic:
[

Goal state after:
R : Type u_1
σ : Type u_2
inst✝¹ : CommSemiring R
φ : MvPolynomial σ R
inst✝ : Fintype σ
n : ℕ
h : φ.IsHomogeneous n
⊢ ∑ i, X i * (pderiv i) φ = n • φ
Module: Mathlib.RingTheory.MvPolynomial.Expand

Goal state before:
pp: case succ
σ : Type u_1
R : Type u_2
inst✝¹ : CommSemiring R
p : ℕ
inst✝ : ExpChar R p
f : MvPolynomial σ R
k : ℕ
n_ih : (map (iterateFrobenius R p k)) ((expand (p ^ k)) f) = f ^ p ^ k
⊢ (map (iterateFrobenius R p k)) ((expand (p ^ k)) f) ^ p =
    (map (iterateFrobenius R p (k + 1))) ((expand (p ^ (k + 1))) f)

Tactic:
[

Goal state after:
case succ
σ : Type u_1
R : Type u_2
inst✝¹ : CommSemiring R
p : ℕ
inst✝ : ExpChar R p
f : MvPolynomial σ R
k : ℕ
n_ih : (map (iterateFrobenius R p k)) ((expand (p ^ k)) f) = f ^ p ^ k
⊢ (map (iterateFrobenius R p k)) ((expand (p ^ k)) f) ^ p =
    (map (iterateFrobenius R p (k + 1))) ((expand (p ^ (k + 1))) f)
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: K : Type u_2
inst✝ : Field K
ℱ : Filter K⸨X⸩
hℱ : Cauchy ℱ
N₁ : ℤ
hN₁ : ∀ᶠ (f : K⸨X⸩) in ℱ, ∀ n < N₁, f.coeff n = 0
N₂ : ℤ
hN₂ : ∀ n < N₂, coeff hℱ n = 0
x✝ : K⸨X⸩
hf : x✝ ∈ {x | (fun f ↦ ∀ n < N₁, f.coeff n = 0) x}
d : ℤ
hd : d < min N₁ N₂
⊢ coeff hℱ d = x✝.coeff d

Tactic:
hf d (lt_of_lt_of_le hd (min_le_left _ _)),

Goal state after:
K : Type u_2
inst✝ : Field K
ℱ : Filter K⸨X⸩
hℱ : Cauchy ℱ
N₁ : ℤ
hN₁ : ∀ᶠ (f : K⸨X⸩) in ℱ, ∀ n < N₁, f.coeff n = 0
N₂ : ℤ
hN₂ : ∀ n < N₂, coeff hℱ n = 0
x✝ : K⸨X⸩
hf : x✝ ∈ {x | (fun f ↦ ∀ n < N₁, f.coeff n = 0) x}
d : ℤ
hd : d < min N₁ N₂
⊢ coeff hℱ d = 0
Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem

Goal state before:
pp: i n m : ℕ
hin : i < n
him : i + 1 < m
t : Fin n → ℕ
⊢ (accumulate n m) t ⟨i, ⋯⟩ = t ⟨i, hin⟩ + (accumulate n m) t ⟨i + 1, him⟩

Tactic:
[

Goal state after:
i n m : ℕ
hin : i < n
him : i + 1 < m
t : Fin n → ℕ
⊢ (accumulate n m) t ⟨i, ⋯⟩ = t ⟨i, hin⟩ + (accumulate n m) t ⟨i + 1, him⟩
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 → ℕ
a✝ : Fin n
⊢ a✝ ∈ {x | i + 1 ≤ ↑x} ↔ a✝ ≠ ⟨i, hin⟩ ∧ a✝ ∈ {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 → ℕ
a✝ : Fin n
⊢ a✝ ∈ {x | i + 1 ≤ ↑x} ↔ a✝ ≠ ⟨i, hin⟩ ∧ a✝ ∈ {x | i ≤ ↑x}
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
this : ∀ᶠ (f : K⸨X⸩) in ℱ, f ∈ {y | Valued.v (y - limit hℱ) < embedding ↑γ}
⊢ ∀ᶠ (f : K⸨X⸩) in ℱ, f ∈ U

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
this : ∀ᶠ (f : K⸨X⸩) in ℱ, f ∈ {y | Valued.v (y - limit hℱ) < embedding ↑γ}
⊢ ∀ᶠ (f : K⸨X⸩) in ℱ, f ∈ U
Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem

Goal state before:
pp: σ : Type u_1
τ : Type u_2
R : Type u_3
n : ℕ
inst✝² : CommSemiring R
inst✝¹ : Fintype σ
inst✝ : Fintype τ
e : σ ≃ τ
i : Fin n
⊢ ↑(((↑(renameSymmetricSubalgebra e)).comp (esymmAlgHom σ R n)) (X i)) = ↑((esymmAlgHom τ R n) (X i))

Tactic:
[

Goal state after:
σ : Type u_1
τ : Type u_2
R : Type u_3
n : ℕ
inst✝² : CommSemiring R
inst✝¹ : Fintype σ
inst✝ : Fintype τ
e : σ ≃ τ
i : Fin n
⊢ ↑(((↑(renameSymmetricSubalgebra e)).comp (esymmAlgHom σ R n)) (X i)) = ↑((esymmAlgHom τ R n) (X i))
Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem

Goal state before:
pp: σ : Type u_1
R : Type u_3
n : ℕ
inst✝¹ : CommSemiring R
inst✝ : Fintype σ
r : R
t s : Fin n →₀ ℕ
⊢ esymmAlgHomMonomial σ (t + s) r = esymmAlgHomMonomial σ t r * esymmAlgHomMonomial σ s 1

Tactic:
[

Goal state after:
σ : Type u_1
R : Type u_3
n : ℕ
inst✝¹ : CommSemiring R
inst✝ : Fintype σ
r : R
t s : Fin n →₀ ℕ
⊢ esymmAlgHomMonomial σ (t + s) r = esymmAlgHomMonomial σ t r * esymmAlgHomMonomial σ s 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 : t ≠ Iic ⟨i, him⟩
ht' : #t = #(Iic ⟨i, him⟩)
⊢ supDegree (⇑toLex) ((monomial (∑ j ∈ t, fun₀ | j => 1)) 1) <
    supDegree (⇑toLex) ((monomial (∑ j ≤ ⟨i, him⟩, fun₀ | j => 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 : t ≠ Iic ⟨i, him⟩
ht' : #t = #(Iic ⟨i, him⟩)
⊢ supDegree (⇑toLex) ((monomial (∑ j ∈ t, fun₀ | j => 1)) 1) <
    supDegree (⇑toLex) ((monomial (∑ j ≤ ⟨i, him⟩, fun₀ | j => 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))
⊢ (Multiplicative.ofAdd 1)⁻¹ < 1

Tactic:
Right.inv_lt_one_iff,

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))
⊢ 1 < Multiplicative.ofAdd 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
j : Fin m
⊢ (Finsupp.indicator (Iic ⟨↑i, him⟩) fun x x_1 ↦ 1) j = (accumulate n m) (⇑fun₀ | i => 1) j

Tactic:
[

Goal state after:
R : Type u_3
n m : ℕ
inst✝¹ : CommSemiring R
i : Fin n
inst✝ : Nontrivial R
him : ↑i < m
j : Fin m
⊢ (Finsupp.indicator (Iic ⟨↑i, him⟩) fun x x_1 ↦ 1) j = (accumulate n m) (⇑fun₀ | i => 1) j
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) (esymm (Fin m) R 0)

Tactic:
rw [esymm_zero]

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
hr : r ≠ 0
hnm : n ≤ m
inst✝ : Nontrivial R
⊢ ⇑(ofLex (supDegree (⇑toLex) (esymmAlgHomMonomial (Fin m) 0 r))) = (accumulate n m) ⇑0

Tactic:
[

Goal state after:
case zero
R : Type u_3
n m : ℕ
inst✝¹ : CommSemiring R
r : R
hr : r ≠ 0
hnm : n ≤ m
inst✝ : Nontrivial R
⊢ ⇑(ofLex (supDegree (⇑toLex) (esymmAlgHomMonomial (Fin m) 0 r))) = (accumulate n m) ⇑0
Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem

Goal state before:
pp: case inr.refine_2
σ : 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
⊢ (ofLex (supDegree (⇑toLex) p)) j = (Finsupp.mapDomain (⇑(Equiv.swap i j)) (ofLex (supDegree (⇑toLex) p))) i

Tactic:
[

Goal state after:
case inr.refine_2
σ : 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
⊢ (ofLex (supDegree (⇑toLex) p)) j = (Finsupp.mapDomain (⇑(Equiv.swap i j)) (ofLex (supDegree (⇑toLex) p))) i
Module: Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities

Goal state before:
pp: case inr
σ : 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)
h2 : ∀ (n : ℕ), -(-1) ^ n = (-1) ^ (n + 1)
h1 : t.2 ∉ t.1
⊢ (-1) ^ #t.1 * ((∏ a ∈ t.1, X a) * X t.2 ^ (k - #t.1)) +
      (-1) ^ #(cons t.2 t.1 h1, t.2).1 *
        ((∏ a ∈ (cons t.2 t.1 h1, t.2).1, X a) * X (cons t.2 t.1 h1, t.2).2 ^ (k - #(cons t.2 t.1 h1, t.2).1)) =
    0

Tactic:
simp only [mul_comm, mul_assoc (∏ a ∈ t.fst, X a), card_cons, prod_cons]

Goal state after:
case inr
σ : 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)
h2 : ∀ (n : ℕ), -(-1) ^ n = (-1) ^ (n + 1)
h1 : t.2 ∉ t.1
⊢ (∏ a ∈ t.1, X a) * (X t.2 ^ (k - #t.1) * (-1) ^ #t.1) +
      (∏ a ∈ t.1, X a) * (X t.2 * X t.2 ^ (k - (#t.1 + 1)) * (-1) ^ (#t.1 + 1)) =
    0
Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem

Goal state before:
pp: case mul_X
R : Type u_3
n m : ℕ
inst✝ : CommRing R
h : m ≤ n
p : MvPolynomial (Fin m) R
i : Fin m
hp : (esymmAlgHom (Fin m) R m) p ∈ (esymmAlgHom (Fin m) R n).range
⊢ (esymmAlgHom (Fin m) R n) (X ⟨↑i, ⋯⟩) = (esymmAlgHom (Fin m) R m) (X i)

Tactic:
[

Goal state after:
case mul_X
R : Type u_3
n m : ℕ
inst✝ : CommRing R
h : m ≤ n
p : MvPolynomial (Fin m) R
i : Fin m
hp : (esymmAlgHom (Fin m) R m) p ∈ (esymmAlgHom (Fin m) R n).range
⊢ (esymmAlgHom (Fin m) R n) (X ⟨↑i, ⋯⟩) = (esymmAlgHom (Fin m) R m) (X i)
Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem

Goal state before:
pp: σ : Type u_1
R : Type u_3
n : ℕ
inst✝¹ : Fintype σ
inst✝ : CommRing R
hn : Fintype.card σ = n
i : Fin n
⊢ (esymmAlgHom σ R n) ((esymmAlgEquiv σ R hn).symm ⟨esymm σ R (↑i + 1), ⋯⟩) = (esymmAlgHom σ R n) (X i)

Tactic:
[

Goal state after:
σ : Type u_1
R : Type u_3
n : ℕ
inst✝¹ : Fintype σ
inst✝ : CommRing R
hn : Fintype.card σ = n
i : Fin n
⊢ (esymmAlgHom σ R n) ((esymmAlgEquiv σ R hn).symm ⟨esymm σ R (↑i + 1), ⋯⟩) = (esymmAlgHom σ R n) (X i)
Module: Mathlib.RingTheory.MvPowerSeries.Expand

Goal state before:
pp: case neg.a
σ : Type u_1
R : Type u_3
inst✝ : CommRing R
p : ℕ
hp : p ≠ 0
φ : MvPowerSeries σ R
hφ : φ ≠ 0
d : σ →₀ ℕ
hd₁ : (coeff d) φ ≠ 0
hd₂ : ↑(Finsupp.degree d) = φ.order
this : p • φ.order = ↑(Finsupp.degree (p • d))
⊢ ((expand p hp) φ).order ≤ p • φ.order

Tactic:
this

Goal state after:
case neg.a
σ : Type u_1
R : Type u_3
inst✝ : CommRing R
p : ℕ
hp : p ≠ 0
φ : MvPowerSeries σ R
hφ : φ ≠ 0
d : σ →₀ ℕ
hd₁ : (coeff d) φ ≠ 0
hd₂ : ↑(Finsupp.degree d) = φ.order
this : p • φ.order = ↑(Finsupp.degree (p • d))
⊢ ((expand p hp) φ).order ≤ ↑(Finsupp.degree (p • d))
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: case h.left
K : Type u_2
inst✝ : Field K
a : adicCompletion K⟮X⟯ (idealX K)
this : ∀ (s : Set (adicCompletion K⟮X⟯ (idealX K))), s ∈ 𝓝 0 ↔ ∃ γ, {x | Valued.v.restrict x < ↑γ} ⊆ s
ha : a = 0
S : Set (WithZero (Multiplicative ℤ))
γ : WithZero (Multiplicative ℤ)
γ_ne_zero : γ ≠ 0
γ_le : Set.Iio γ ⊆ S
⊢ {t | Valued.v t < γ} ∈ 𝓝 0

Tactic:
this

Goal state after:
case h.left
K : Type u_2
inst✝ : Field K
a : adicCompletion K⟮X⟯ (idealX K)
this : ∀ (s : Set (adicCompletion K⟮X⟯ (idealX K))), s ∈ 𝓝 0 ↔ ∃ γ, {x | Valued.v.restrict x < ↑γ} ⊆ s
ha : a = 0
S : Set (WithZero (Multiplicative ℤ))
γ : WithZero (Multiplicative ℤ)
γ_ne_zero : γ ≠ 0
γ_le : Set.Iio γ ⊆ S
⊢ ∃ γ_1, {x | Valued.v.restrict x < ↑γ_1} ⊆ {t | Valued.v t < γ}
Module: Mathlib.RingTheory.Nilpotent.GeometricallyReduced

Goal state before:
pp: k : Type u_1
A : Type u_2
inst✝² : Field k
inst✝¹ : Ring A
inst✝ : Algebra k A
h : ∀ (B : Subalgebra k A), B.FG → IsGeometricallyReduced k ↥B
⊢ IsGeometricallyReduced k A

Tactic:
[

Goal state after:
k : Type u_1
A : Type u_2
inst✝² : Field k
inst✝¹ : Ring A
inst✝ : Algebra k A
h : ∀ (B : Subalgebra k A), B.FG → IsGeometricallyReduced k ↥B
⊢ IsGeometricallyReduced k A
Module: Mathlib.RingTheory.MvPowerSeries.Expand

Goal state before:
pp: case succ
σ : Type u_1
R : Type u_3
inst✝¹ : CommRing R
p : ℕ
hp : p ≠ 0
inst✝ : ExpChar R p
f : MvPowerSeries σ R
k : ℕ
n_ih : (map (iterateFrobenius R p k)) ((expand (p ^ k) ⋯) f) = f ^ p ^ k
⊢ (map (iterateFrobenius R p k)) ((expand (p ^ k) ⋯) f) ^ p =
    (map (iterateFrobenius R p (k + 1))) ((expand (p ^ (k + 1)) ⋯) f)

Tactic:
[

Goal state after:
case succ
σ : Type u_1
R : Type u_3
inst✝¹ : CommRing R
p : ℕ
hp : p ≠ 0
inst✝ : ExpChar R p
f : MvPowerSeries σ R
k : ℕ
n_ih : (map (iterateFrobenius R p k)) ((expand (p ^ k) ⋯) f) = f ^ p ^ k
⊢ (map (iterateFrobenius R p k)) ((expand (p ^ k) ⋯) f) ^ p =
    (map (iterateFrobenius R p (k + 1))) ((expand (p ^ (k + 1)) ⋯) f)
Module: Mathlib.RingTheory.Noetherian.Filter

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : IsNoetherian R M
f : ℕ →o Submodule R M
⊢ EventuallyConst (⇑f) atTop

Tactic:
[

Goal state after:
R : Type u_1
M : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : IsNoetherian R M
f : ℕ →o Submodule R M
⊢ EventuallyConst (⇑f) atTop
Module: Mathlib.RingTheory.NormTrace

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Algebra A B
inst✝¹ : Free A B
inst✝ : Module.Finite A B
a : A
x : B
ι : Type u_2
b : Basis ι A B
this : Fintype ι
⊢ ∃ r, (norm A) (1 + a • x) = 1 + (trace A B) x * a + r * a ^ 2

Tactic:
[

Goal state after:
A : Type u_1
B : Type u_2
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Algebra A B
inst✝¹ : Free A B
inst✝ : Module.Finite A B
a : A
x : B
ι : Type u_2
b : Basis ι A B
this : Fintype ι
⊢ ∃ r, (norm A) (1 + a • x) = 1 + (trace A B) x * a + r * a ^ 2
Module: Mathlib.RingTheory.NoetherNormalization

Goal state before:
pp: k : Type u_1
inst✝ : Field k
n : ℕ
f : MvPolynomial (Fin (n + 1)) k
fne : f ≠ 0
v : Fin (n + 1) →₀ ℕ
vin : v ∈ f.support
h : (Fin (n + 1) →₀ ℕ) → MvPolynomial (Fin (n + 1)) k := fun w ↦ (MvPolynomial.monomial w) (MvPolynomial.coeff w f)
vs :
  ∀ x ∈ f.support \ {v},
    ((MvPolynomial.finSuccEquiv k n) ((T f) (h x))).degree < ((MvPolynomial.finSuccEquiv k n) ((T f) (h v))).degree
coeff :
  ((MvPolynomial.finSuccEquiv k n) ((T f) (h v + ∑ x ∈ f.support \ {v}, h x))).leadingCoeff =
    ((MvPolynomial.finSuccEquiv k n) ((T f) (h v))).leadingCoeff
⊢ IsUnit ((MvPolynomial.finSuccEquiv k n) ((T f) (h v + ∑ x ∈ f.support \ {v}, h x))).leadingCoeff

Tactic:
leadingCoeff_finSuccEquiv_t

Goal state after:
k : Type u_1
inst✝ : Field k
n : ℕ
f : MvPolynomial (Fin (n + 1)) k
fne : f ≠ 0
v : Fin (n + 1) →₀ ℕ
vin : v ∈ f.support
h : (Fin (n + 1) →₀ ℕ) → MvPolynomial (Fin (n + 1)) k := fun w ↦ (MvPolynomial.monomial w) (MvPolynomial.coeff w f)
vs :
  ∀ x ∈ f.support \ {v},
    ((MvPolynomial.finSuccEquiv k n) ((T f) (h x))).degree < ((MvPolynomial.finSuccEquiv k n) ((T f) (h v))).degree
coeff :
  ((MvPolynomial.finSuccEquiv k n) ((T f) (h v + ∑ x ∈ f.support \ {v}, h x))).leadingCoeff =
    (algebraMap k (MvPolynomial (Fin n) k)) (MvPolynomial.coeff v f)
⊢ IsUnit ((MvPolynomial.finSuccEquiv k n) ((T f) (h v + ∑ x ∈ f.support \ {v}, h x))).leadingCoeff
Module: Mathlib.RingTheory.NoetherNormalization

Goal state before:
pp: k : Type u_1
inst✝ : Field k
n : ℕ
f : MvPolynomial (Fin (n + 1)) k
v w : Fin (n + 1) →₀ ℕ
I : Ideal (MvPolynomial (Fin (n + 1)) k)
g : MvPolynomial (Fin (n + 1)) k ≃ₐ[k] (MvPolynomial (Fin n) k)[X] := MvPolynomial.finSuccEquiv k n
this : g.symm.toRingEquiv.toRingHom.comp ↑g = RingHom.id (MvPolynomial (Fin (n + 1)) k)
⊢ Ideal.map (T f) I = Ideal.map ((RingHom.id (MvPolynomial (Fin (n + 1)) k)).comp ↑(T f)) I

Tactic:
by rw [id_comp, Ideal.map_coe]

Goal state after:
Module: Mathlib.RingTheory.Teichmuller

Goal state before:
pp: p : ℕ
inst✝³ : Fact (Nat.Prime p)
R : Type u_1
inst✝² : CommRing R
I : Ideal R
inst✝¹ : CharP (R ⧸ I) p
inst✝ : IsAdicComplete I R
x : Perfection (R ⧸ I) p
this : (teichmuller p I) x ≡ Quotient.out ((coeff (R ⧸ I) p 0) x) ^ p ^ 0 [SMOD I ^ (0 + 1)]
⊢ (Ideal.Quotient.mk I) ((teichmuller p I) x) = (coeff (R ⧸ I) p 0) x

Tactic:
[

Goal state after:
p : ℕ
inst✝³ : Fact (Nat.Prime p)
R : Type u_1
inst✝² : CommRing R
I : Ideal R
inst✝¹ : CharP (R ⧸ I) p
inst✝ : IsAdicComplete I R
x : Perfection (R ⧸ I) p
this : (teichmuller p I) x ≡ Quotient.out ((coeff (R ⧸ I) p 0) x) ^ p ^ 0 [SMOD I ^ (0 + 1)]
⊢ (Ideal.Quotient.mk I) ((teichmuller p I) x) = (coeff (R ⧸ I) p 0) x
Module: Mathlib.RingTheory.WittVector.StructurePolynomial

Goal state before:
pp: p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℚ
n : ℕ
this :
  (bind₁ fun k ↦ (bind₁ fun i ↦ (rename (Prod.mk i)) (W_ ℚ k)) Φ) (xInTermsOfW p ℚ n) * C (↑p ^ n) =
    (bind₁ fun k ↦ (bind₁ fun i ↦ (rename (Prod.mk i)) (W_ ℚ k)) Φ)
      (X n - ∑ i ∈ Finset.range n, C (↑p ^ i) * xInTermsOfW p ℚ i ^ p ^ (n - i))
⊢ (bind₁ fun k ↦ (bind₁ fun i ↦ (rename (Prod.mk i)) (W_ ℚ k)) Φ) (xInTermsOfW p ℚ n) * C (↑p ^ n) =
    (bind₁ fun b ↦ (rename fun i ↦ (b, i)) (W_ ℚ n)) Φ -
      ∑ i ∈ Finset.range n, C (↑p ^ i) * wittStructureRat p Φ i ^ p ^ (n - i)

Tactic:
this

Goal state after:
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℚ
n : ℕ
this :
  (bind₁ fun k ↦ (bind₁ fun i ↦ (rename (Prod.mk i)) (W_ ℚ k)) Φ) (xInTermsOfW p ℚ n) * C (↑p ^ n) =
    (bind₁ fun k ↦ (bind₁ fun i ↦ (rename (Prod.mk i)) (W_ ℚ k)) Φ)
      (X n - ∑ i ∈ Finset.range n, C (↑p ^ i) * xInTermsOfW p ℚ i ^ p ^ (n - i))
⊢ (bind₁ fun k ↦ (bind₁ fun i ↦ (rename (Prod.mk i)) (W_ ℚ k)) Φ)
      (X n - ∑ i ∈ Finset.range n, C (↑p ^ i) * xInTermsOfW p ℚ i ^ p ^ (n - i)) =
    (bind₁ fun b ↦ (rename fun i ↦ (b, i)) (W_ ℚ n)) Φ -
      ∑ i ∈ Finset.range n, C (↑p ^ i) * wittStructureRat p Φ i ^ p ^ (n - i)
Module: Mathlib.RingTheory.WittVector.WittPolynomial

Goal state before:
pp: p : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Invertible ↑p
k : ℕ
⊢ xInTermsOfW p R k * C ↑p ^ k + ∑ x ∈ range k, C ↑p ^ x * (bind₁ (xInTermsOfW p R)) (X x) ^ p ^ (k - x) = X k

Tactic:
← C_pow,

Goal state after:
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Invertible ↑p
k : ℕ
⊢ xInTermsOfW p R k * C (↑p ^ k) + ∑ x ∈ range k, C ↑p ^ x * (bind₁ (xInTermsOfW p R)) (X x) ^ p ^ (k - x) = X k
Module: Mathlib.RingTheory.WittVector.StructurePolynomial

Goal state before:
pp: case succ
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n k : ℕ
hk : k ≤ n
this : p ^ (n + 1) = p ^ k * p ^ (n - k + 1)
⊢ ↑(p ^ (n + 1)) ∣
    ↑(p ^ k) * ((expand p) (wittStructureInt p Φ k) ^ p ^ (n - k) - wittStructureInt p Φ k ^ p ^ (n + 1 - k))

Tactic:
this

Goal state after:
case succ
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n k : ℕ
hk : k ≤ n
this : p ^ (n + 1) = p ^ k * p ^ (n - k + 1)
⊢ ↑(p ^ k * p ^ (n - k + 1)) ∣
    ↑(p ^ k) * ((expand p) (wittStructureInt p Φ k) ^ p ^ (n - k) - wittStructureInt p Φ k ^ p ^ (n + 1 - k))
Module: Mathlib.RingTheory.Perfection

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
p : ℕ
f : Perfection M p
n m : ℕ
hmn : m ≤ n
⊢ (coeffMonoidHom M p n) ((⇑(powMonoidHom p))^[m] f) = (coeffMonoidHom M p (n - m)) f

Tactic:
rw [← coeffMonoidHom_iterate_powMonoidHom f (n - m) m, Nat.sub_add_cancel hmn]

Goal state after: