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

Goal state before:
pp: case neg
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
⊢ ∃ γ,
    {y | Valued.v.restrict (y - a) < ↑γ} ⊆
      {x |
        ∀ (a_1 : K⟮X⟯),
          { toCompletion := ↑((WithVal.equiv (valuation K⟮X⟯ (idealX K))).symm a_1) } = x → Valued.v a_1 = Valued.v a}

Tactic:
]

Goal state after:
case neg
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
⊢ ∃ γ,
    {y | Valued.v.restrict (y - a) < ↑γ} ⊆
      {x |
        ∀ (a_1 : K⟮X⟯),
          { toCompletion := ↑((WithVal.equiv (valuation K⟮X⟯ (idealX K))).symm a_1) } = x → Valued.v a_1 = Valued.v a}
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
B : Type u_3
inst✝² : Ring B
inst✝¹ : Algebra k B
f : A →ₐ[k] B
hf : Function.Injective ⇑f
inst✝ : IsGeometricallyReduced k B
⊢ IsReduced (AlgebraicClosure k ⊗[k] A)

Tactic:
]

Goal state after:
k : Type u_1
A : Type u_2
inst✝⁵ : Field k
inst✝⁴ : Ring A
inst✝³ : Algebra k A
B : Type u_3
inst✝² : Ring B
inst✝¹ : Algebra k B
f : A →ₐ[k] B
hf : Function.Injective ⇑f
inst✝ : IsGeometricallyReduced k B
⊢ IsReduced (AlgebraicClosure k ⊗[k] A)
Module: Mathlib.RingTheory.MvPowerSeries.Restricted

Goal state before:
pp: case inr
M : Type u_3
S : Type u_4
inst✝³ : AddMonoid M
inst✝² : Finset.HasAntidiagonal M
inst✝¹ : NormedRing S
inst✝ : IsUltrametricDist S
C : M → ℝ
hC : ∀ (a b : M), C (a + b) = C a * C b
f g : M → S
hf : Tendsto (fun i ↦ ‖f i‖ * C i) cofinite (𝓝 0)
hg : Tendsto (fun i ↦ ‖g i‖ * C i) cofinite (𝓝 0)
this :
  ∀ {C : M → ℝ},
    (∀ (a b : M), C (a + b) = C a * C b) →
      Tendsto (fun i ↦ ‖f i‖ * C i) cofinite (𝓝 0) →
        Tendsto (fun i ↦ ‖g i‖ * C i) cofinite (𝓝 0) →
          0 ≤ C → Tendsto (fun a ↦ ‖∑ p ∈ antidiagonal a, f p.1 * g p.2‖ * C a) cofinite (𝓝 0)
hC' : ¬0 ≤ C
⊢ Tendsto (fun x ↦ ‖‖∑ p ∈ antidiagonal x, f p.1 * g p.2‖ * C x‖) cofinite (𝓝 0)

Tactic:
]

Goal state after:
case inr
M : Type u_3
S : Type u_4
inst✝³ : AddMonoid M
inst✝² : Finset.HasAntidiagonal M
inst✝¹ : NormedRing S
inst✝ : IsUltrametricDist S
C : M → ℝ
hC : ∀ (a b : M), C (a + b) = C a * C b
f g : M → S
hf : Tendsto (fun i ↦ ‖f i‖ * C i) cofinite (𝓝 0)
hg : Tendsto (fun i ↦ ‖g i‖ * C i) cofinite (𝓝 0)
this :
  ∀ {C : M → ℝ},
    (∀ (a b : M), C (a + b) = C a * C b) →
      Tendsto (fun i ↦ ‖f i‖ * C i) cofinite (𝓝 0) →
        Tendsto (fun i ↦ ‖g i‖ * C i) cofinite (𝓝 0) →
          0 ≤ C → Tendsto (fun a ↦ ‖∑ p ∈ antidiagonal a, f p.1 * g p.2‖ * C a) cofinite (𝓝 0)
hC' : ¬0 ≤ C
⊢ Tendsto (fun x ↦ ‖‖∑ p ∈ antidiagonal x, f p.1 * g p.2‖ * C x‖) cofinite (𝓝 0)
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: case h
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
b : K⟮X⟯
val_y :
  Valued.v.restrict ({ toCompletion := ↑((WithVal.equiv (valuation K⟮X⟯ (idealX K))).symm b) } - a) <
    Valued.v.restrict a
⊢ Valued.v { toCompletion := ↑((WithVal.equiv (valuation K⟮X⟯ (idealX K))).symm b) } = Valued.v a

Tactic:
]

Goal state after:
case h
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
b : K⟮X⟯
val_y :
  Valued.v.restrict ({ toCompletion := ↑((WithVal.equiv (valuation K⟮X⟯ (idealX K))).symm b) } - a) <
    Valued.v.restrict a
⊢ Valued.v { toCompletion := ↑((WithVal.equiv (valuation K⟮X⟯ (idealX K))).symm b) } = Valued.v a
Module: Mathlib.RingTheory.MvPowerSeries.Expand

Goal state before:
pp: case h
σ : Type u_1
R : Type u_3
inst✝¹ : CommRing R
p : ℕ
hp : p ≠ 0
inst✝ : ExpChar R p
f : MvPowerSeries σ R
n : σ →₀ ℕ
this :
  ↑((MvPolynomial.map (frobenius R p)) ((MvPolynomial.expand p) ((trunc' R (p • n)) f))) =
    (map (frobenius R p)) ↑((MvPolynomial.expand p) ((trunc' R (p • n)) f))
⊢ (MvPolynomial.map (frobenius R p)) ((trunc' R (p • n)) ↑((MvPolynomial.expand p) ((trunc' R (p • n)) f))) =
    (MvPolynomial.map (frobenius R p)) ((trunc' R (p • n)) ↑((MvPolynomial.expand p) ((trunc' R (p • n)) f)))

Tactic:
]

Goal state after:
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: K : Type u_2
inst✝ : Field K
f : K⸨X⸩
⊢ Valued.v ((LaurentSeriesPkg K).compare ratfuncAdicComplPkg f) = Valued.v f

Tactic:
]

Goal state after:
K : Type u_2
inst✝ : Field K
f : K⸨X⸩
⊢ Valued.v ((LaurentSeriesPkg K).compare ratfuncAdicComplPkg f) = Valued.v f
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: K : Type u_2
inst✝ : Field K
f : K⸨X⸩
this : UniformSpace ratfuncAdicComplPkg.space := ratfuncAdicComplPkg.uniformStruct
raw_surj : Function.Surjective ⇑Valued.v
⊢ Valued.v ((LaurentSeriesPkg K).compare ratfuncAdicComplPkg f) =
    (⋯.extend ⇑Valued.v ∘ (LaurentSeriesPkg K).compare ratfuncAdicComplPkg) f

pp: case cont_f
K : Type u_2
inst✝ : Field K
f : K⸨X⸩
this : UniformSpace ratfuncAdicComplPkg.space := ratfuncAdicComplPkg.uniformStruct
raw_surj : Function.Surjective ⇑Valued.v
⊢ Continuous ⇑Valued.v

pp: case a
K : Type u_2
inst✝ : Field K
f : K⸨X⸩
this : UniformSpace ratfuncAdicComplPkg.space := ratfuncAdicComplPkg.uniformStruct
raw_surj : Function.Surjective ⇑Valued.v
⊢ ∀ (a : ratfuncAdicComplPkg.space),
    Tendsto (⇑Valued.v) (Filter.comap ratfuncAdicComplPkg.coe (𝓝 a)) (𝓝 (⋯.extend (⇑Valued.v) a))

Tactic:
]

Goal state after:
K : Type u_2
inst✝ : Field K
f : K⸨X⸩
this : UniformSpace ratfuncAdicComplPkg.space := ratfuncAdicComplPkg.uniformStruct
raw_surj : Function.Surjective ⇑Valued.v
⊢ Valued.v ((LaurentSeriesPkg K).compare ratfuncAdicComplPkg f) =
    (⋯.extend ⇑Valued.v ∘ (LaurentSeriesPkg K).compare ratfuncAdicComplPkg) f

case cont_f
K : Type u_2
inst✝ : Field K
f : K⸨X⸩
this : UniformSpace ratfuncAdicComplPkg.space := ratfuncAdicComplPkg.uniformStruct
raw_surj : Function.Surjective ⇑Valued.v
⊢ Continuous ⇑Valued.v

case a
K : Type u_2
inst✝ : Field K
f : K⸨X⸩
this : UniformSpace ratfuncAdicComplPkg.space := ratfuncAdicComplPkg.uniformStruct
raw_surj : Function.Surjective ⇑Valued.v
⊢ ∀ (a : ratfuncAdicComplPkg.space),
    Tendsto (⇑Valued.v) (Filter.comap ratfuncAdicComplPkg.coe (𝓝 a)) (𝓝 (⋯.extend (⇑Valued.v) a))
Module: Mathlib.RingTheory.MvPowerSeries.Restricted

Goal state before:
pp: M : Type u_3
S : Type u_4
inst✝³ : AddMonoid M
inst✝² : Finset.HasAntidiagonal M
inst✝¹ : NormedRing S
inst✝ : IsUltrametricDist S
f g : M → S
C : M → ℝ
hC : ∀ (a b : M), C (a + b) = C a * C b
hf : Tendsto (fun i ↦ ‖f i‖ * C i) cofinite (𝓝 0)
hg : Tendsto (fun i ↦ ‖g i‖ * C i) cofinite (𝓝 0)
hC' : 0 ≤ C
a : M
this : 0 ≤ C a
⊢ ((antidiagonal a).sup' ⋯ fun i ↦ ‖f i.1 * g i.2‖ * C a) ≤
    (antidiagonal a).sup' ⋯ fun i ↦ ‖f i.1‖ * C i.1 * (‖g i.2‖ * C i.2)

Tactic:
]

Goal state after:
M : Type u_3
S : Type u_4
inst✝³ : AddMonoid M
inst✝² : Finset.HasAntidiagonal M
inst✝¹ : NormedRing S
inst✝ : IsUltrametricDist S
f g : M → S
C : M → ℝ
hC : ∀ (a b : M), C (a + b) = C a * C b
hf : Tendsto (fun i ↦ ‖f i‖ * C i) cofinite (𝓝 0)
hg : Tendsto (fun i ↦ ‖g i‖ * C i) cofinite (𝓝 0)
hC' : 0 ≤ C
a : M
this : 0 ≤ C a
⊢ ((antidiagonal a).sup' ⋯ fun i ↦ ‖f i.1 * g i.2‖ * C a) ≤
    (antidiagonal a).sup' ⋯ fun i ↦ ‖f i.1‖ * C i.1 * (‖g i.2‖ * C i.2)
Module: Mathlib.RingTheory.MvPowerSeries.Restricted

Goal state before:
pp: M : Type u_3
S : Type u_4
inst✝³ : AddMonoid M
inst✝² : Finset.HasAntidiagonal M
inst✝¹ : NormedRing S
inst✝ : IsUltrametricDist S
f g : M → S
C : M → ℝ
hC : ∀ (a b : M), C (a + b) = C a * C b
hf : Tendsto (fun i ↦ ‖f i‖ * C i) cofinite (𝓝 0)
hg : Tendsto (fun i ↦ ‖g i‖ * C i) cofinite (𝓝 0)
hC' : 0 ≤ C
a : M
this : 0 ≤ C a
x : M × M
hx : x ∈ antidiagonal a
⊢ ‖f x.1 * g x.2‖ * C a ≤ ‖f x.1 * g x.2‖ * C a

Tactic:
]

Goal state after:
Module: Mathlib.RingTheory.MvPowerSeries.Restricted

Goal state before:
pp: R : Type u_1
inst✝¹ : NormedRing R
σ : Type u_2
inst✝ : IsUltrametricDist R
c : σ → ℝ
f g : MvPowerSeries σ R
hf : Tendsto (fun t ↦ ‖(coeff t) f‖ * t.prod fun x1 x2 ↦ |c| x1 ^ x2) cofinite (𝓝 0)
hg : Tendsto (fun t ↦ ‖(coeff t) g‖ * t.prod fun x1 x2 ↦ |c| x1 ^ x2) cofinite (𝓝 0)
⊢ Tendsto (fun t ↦ ‖(coeff t) (f * g)‖ * t.prod fun x1 x2 ↦ |c| x1 ^ x2) cofinite (𝓝 0)

Tactic:
]

Goal state after:
R : Type u_1
inst✝¹ : NormedRing R
σ : Type u_2
inst✝ : IsUltrametricDist R
c : σ → ℝ
f g : MvPowerSeries σ R
hf : Tendsto (fun t ↦ ‖(coeff t) f‖ * t.prod fun x1 x2 ↦ |c| x1 ^ x2) cofinite (𝓝 0)
hg : Tendsto (fun t ↦ ‖(coeff t) g‖ * t.prod fun x1 x2 ↦ |c| x1 ^ x2) cofinite (𝓝 0)
⊢ Tendsto (fun t ↦ ‖(coeff t) (f * g)‖ * t.prod fun x1 x2 ↦ |c| x1 ^ x2) cofinite (𝓝 0)
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: case a
K : Type u_2
inst✝ : Field K
f : K⸨X⸩
this : UniformSpace ratfuncAdicComplPkg.space := ratfuncAdicComplPkg.uniformStruct
raw_surj : Function.Surjective ⇑Valued.v
x : ratfuncAdicComplPkg.space
h_cont : Continuous ⇑Valued.v
⊢ Tendsto (⇑Valued.v) (Filter.comap ratfuncAdicComplPkg.coe (𝓝 x)) (𝓝 (Valued.v x))

Tactic:
]

Goal state after:
case a
K : Type u_2
inst✝ : Field K
f : K⸨X⸩
this : UniformSpace ratfuncAdicComplPkg.space := ratfuncAdicComplPkg.uniformStruct
raw_surj : Function.Surjective ⇑Valued.v
x : ratfuncAdicComplPkg.space
h_cont : Continuous ⇑Valued.v
⊢ Tendsto (⇑Valued.v) (Filter.comap ratfuncAdicComplPkg.coe (𝓝 x)) (𝓝 (Valued.v x))
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: K : Type u_2
inst✝ : Field K
F : K⟦X⟧
⊢ ∃ F_1, (ofPowerSeries ℤ K) F_1 = (ofPowerSeries ℤ K) F

Tactic:
]

Goal state after:
K : Type u_2
inst✝ : Field K
F : K⟦X⟧
⊢ ∃ F_1, (ofPowerSeries ℤ K) F_1 = (ofPowerSeries ℤ K) F
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: K : Type u_2
inst✝ : Field K
x : RatFuncAdicCompl K
hx : x ∈ adicCompletionIntegers K⟮X⟯ (idealX K)
f : K⸨X⸩ := (ratfuncAdicComplRingEquiv K) x
hf : f = (ratfuncAdicComplRingEquiv K) x
⊢ x ∈ adicCompletionIntegers K⟮X⟯ (idealX K)

Tactic:
]

Goal state after:
K : Type u_2
inst✝ : Field K
x : RatFuncAdicCompl K
hx : x ∈ adicCompletionIntegers K⟮X⟯ (idealX K)
f : K⸨X⸩ := (ratfuncAdicComplRingEquiv K) x
hf : f = (ratfuncAdicComplRingEquiv K) x
⊢ x ∈ adicCompletionIntegers K⟮X⟯ (idealX K)
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: K : Type u_2
inst✝ : Field K
x : RatFuncAdicCompl K
hx : x ∈ adicCompletionIntegers K⟮X⟯ (idealX K)
f : K⸨X⸩ := (ratfuncAdicComplRingEquiv K) x
hf : f = (ratfuncAdicComplRingEquiv K) x
hval : Valued.v f ≤ 1
F : K⟦X⟧
hF : (ofPowerSeries ℤ K) F = f
⊢ x = x

Tactic:
]

Goal state after:
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: K : Type u_2
inst✝ : Field K
f : K⟦X⟧
⊢ ∃ F, (ofPowerSeries ℤ K) F = (ofPowerSeries ℤ K) f

Tactic:
]

Goal state after:
K : Type u_2
inst✝ : Field K
f : K⟦X⟧
⊢ ∃ F, (ofPowerSeries ℤ K) F = (ofPowerSeries ℤ K) f
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: R : Type u_1
K : Type u_2
inst✝ : Field K
a : K
⊢ (LaurentSeriesRingEquiv K) ((ofPowerSeries ℤ K) (PowerSeries.C a)) =
    ((LaurentSeriesRingEquiv K).toRingHom.comp HahnSeries.C) a

Tactic:
]

Goal state after:
R : Type u_1
K : Type u_2
inst✝ : Field K
a : K
⊢ (LaurentSeriesRingEquiv K) ((ofPowerSeries ℤ K) (PowerSeries.C a)) =
    ((LaurentSeriesRingEquiv K).toRingHom.comp HahnSeries.C) a
Module: Mathlib.RingTheory.NoetherNormalization

Goal state before:
pp: k : Type u_1
inst✝ : Field k
n : ℕ
f : MvPolynomial (Fin (n + 1)) k
c : k
⊢ (MvPolynomial.aeval fun i ↦
      (T1 f c) (if i = 0 then MvPolynomial.X 0 else MvPolynomial.X i + -c • MvPolynomial.X 0 ^ r i)) =
    MvPolynomial.aeval MvPolynomial.X

Tactic:
]

Goal state after:
k : Type u_1
inst✝ : Field k
n : ℕ
f : MvPolynomial (Fin (n + 1)) k
c : k
⊢ (MvPolynomial.aeval fun i ↦
      (T1 f c) (if i = 0 then MvPolynomial.X 0 else MvPolynomial.X i + -c • MvPolynomial.X 0 ^ r i)) =
    MvPolynomial.aeval MvPolynomial.X
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, ((leftMulMatrix b) (1 + a • x)).det = 1 + (trace A B) x * a + r * a ^ 2

Tactic:
Algebra.trace_eq_matrix_trace b

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, ((leftMulMatrix b) (1 + a • x)).det = 1 + ((leftMulMatrix b) x).trace * 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
v : Fin (n + 1) →₀ ℕ
a : k
ha : a ≠ 0
⊢ ((MvPolynomial.finSuccEquiv k n) ((T f) (MvPolynomial.C a * ∏ a, MvPolynomial.X a ^ v a))).natDegree = ∑ i, r i * v i

Tactic:
]

Goal state after:
k : Type u_1
inst✝ : Field k
n : ℕ
f : MvPolynomial (Fin (n + 1)) k
v : Fin (n + 1) →₀ ℕ
a : k
ha : a ≠ 0
⊢ ((MvPolynomial.finSuccEquiv k n) ((T f) (MvPolynomial.C a * ∏ a, MvPolynomial.X a ^ v a))).natDegree = ∑ i, r i * v i
Module: Mathlib.RingTheory.NoetherNormalization

Goal state before:
pp: k : Type u_1
inst✝ : Field k
n : ℕ
f : MvPolynomial (Fin (n + 1)) k
v : Fin (n + 1) →₀ ℕ
a : k
ha : a ≠ 0
h : ∀ (i : Fin n), (Polynomial.C (MvPolynomial.X i) + Polynomial.X ^ r i.succ) ^ v i.succ ≠ 0
⊢ 0 +
      ((Polynomial.X ^ v 0).natDegree +
        ∑ i, ((Polynomial.C (MvPolynomial.X i) + Polynomial.X ^ r i.succ) ^ v i.succ).natDegree) =
    up ^ ↑0 * v 0 + ∑ i, up ^ ↑i.succ * v i.succ

Tactic:
]

Goal state after:
k : Type u_1
inst✝ : Field k
n : ℕ
f : MvPolynomial (Fin (n + 1)) k
v : Fin (n + 1) →₀ ℕ
a : k
ha : a ≠ 0
h : ∀ (i : Fin n), (Polynomial.C (MvPolynomial.X i) + Polynomial.X ^ r i.succ) ^ v i.succ ≠ 0
⊢ 0 +
      ((Polynomial.X ^ v 0).natDegree +
        ∑ i, ((Polynomial.C (MvPolynomial.X i) + Polynomial.X ^ r i.succ) ^ v i.succ).natDegree) =
    up ^ ↑0 * v 0 + ∑ i, up ^ ↑i.succ * v i.succ
Module: Mathlib.RingTheory.NoetherNormalization

Goal state before:
pp: k : Type u_1
inst✝ : Field k
n : ℕ
f : MvPolynomial (Fin (n + 1)) k
v : Fin (n + 1) →₀ ℕ
a : k
ha : a ≠ 0
h : ∀ (i : Fin n), (Polynomial.C (MvPolynomial.X i) + Polynomial.X ^ r i.succ) ^ v i.succ ≠ 0
i : Fin n
x✝ : i ∈ Finset.univ
⊢ up ^ ↑i.succ * v i.succ = up ^ ↑i.succ * v i.succ

Tactic:
]

Goal state after:
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) →₀ ℕ
hv : v ∈ f.support
hw : w ∈ f.support
ne : v ≠ w
⊢ ∑ i, r i * v i ≠ ∑ i, r i * w i

Tactic:
]

Goal state after:
k : Type u_1
inst✝ : Field k
n : ℕ
f : MvPolynomial (Fin (n + 1)) k
v w : Fin (n + 1) →₀ ℕ
hv : v ∈ f.support
hw : w ∈ f.support
ne : v ≠ w
⊢ ∑ i, r i * v i ≠ ∑ i, r i * w i
Module: Mathlib.RingTheory.NoetherNormalization

Goal state before:
pp: k : Type u_1
inst✝ : Field k
n : ℕ
f : MvPolynomial (Fin (n + 1)) k
v : Fin (n + 1) →₀ ℕ
⊢ ((MvPolynomial.finSuccEquiv k n)
        ((T f) (MvPolynomial.C (MvPolynomial.coeff v f) * ∏ i, MvPolynomial.X i ^ v i))).leadingCoeff =
    (algebraMap k (MvPolynomial (Fin n) k)) (MvPolynomial.coeff v f)

pp: case h
k : Type u_1
inst✝ : Field k
n : ℕ
f : MvPolynomial (Fin (n + 1)) k
v : Fin (n + 1) →₀ ℕ
⊢ ∀ (i : Fin (n + 1)), MvPolynomial.X i ^ 0 = 1

Tactic:
]

Goal state after:
k : Type u_1
inst✝ : Field k
n : ℕ
f : MvPolynomial (Fin (n + 1)) k
v : Fin (n + 1) →₀ ℕ
⊢ ((MvPolynomial.finSuccEquiv k n)
        ((T f) (MvPolynomial.C (MvPolynomial.coeff v f) * ∏ i, MvPolynomial.X i ^ v i))).leadingCoeff =
    (algebraMap k (MvPolynomial (Fin n) k)) (MvPolynomial.coeff v f)

case h
k : Type u_1
inst✝ : Field k
n : ℕ
f : MvPolynomial (Fin (n + 1)) k
v : Fin (n + 1) →₀ ℕ
⊢ ∀ (i : Fin (n + 1)), MvPolynomial.X i ^ 0 = 1
Module: Mathlib.RingTheory.NoetherNormalization

Goal state before:
pp: k : Type u_1
inst✝ : Field k
n : ℕ
f : MvPolynomial (Fin (n + 1)) k
v : Fin (n + 1) →₀ ℕ
⊢ ((⇑Polynomial.C ∘ ⇑MvPolynomial.C) (MvPolynomial.coeff v f)).leadingCoeff *
      ∏ i, ((MvPolynomial.finSuccEquiv k n) ((T f) (MvPolynomial.X i ^ v i))).leadingCoeff =
    (algebraMap k (MvPolynomial (Fin n) k)) (MvPolynomial.coeff v f)

Tactic:
]

Goal state after:
k : Type u_1
inst✝ : Field k
n : ℕ
f : MvPolynomial (Fin (n + 1)) k
v : Fin (n + 1) →₀ ℕ
⊢ ((⇑Polynomial.C ∘ ⇑MvPolynomial.C) (MvPolynomial.coeff v f)).leadingCoeff *
      ∏ i, ((MvPolynomial.finSuccEquiv k n) ((T f) (MvPolynomial.X i ^ v i))).leadingCoeff =
    (algebraMap k (MvPolynomial (Fin n) k)) (MvPolynomial.coeff v f)
Module: Mathlib.RingTheory.WittVector.WittPolynomial

Goal state before:
pp: p : ℕ
R : Type u_1
inst✝ : CommRing R
n i : ℕ
⊢ C (↑p ^ i) * X i ^ p ^ (n - i) = C (↑p ^ i) * X i ^ p ^ (n - i)

pp: p : ℕ
R : Type u_1
inst✝ : CommRing R
n i : ℕ
⊢ X i ^ 0 = 1

Tactic:
]

Goal state after:
p : ℕ
R : Type u_1
inst✝ : CommRing R
n i : ℕ
⊢ X i ^ 0 = 1
Module: Mathlib.RingTheory.WittVector.WittPolynomial

Goal state before:
pp: p : ℕ
R : Type u_1
inst✝ : CommRing R
n i : ℕ
⊢ 1 = 1

Tactic:
]

Goal state after:
Module: Mathlib.RingTheory.WittVector.WittPolynomial

Goal state before:
pp: p : ℕ
R : Type u_1
inst✝¹ : CommRing R
S : Type u_2
inst✝ : CommRing S
f : R →+* S
n : ℕ
⊢ ∑ x ∈ range (n + 1), (map f) ((monomial (single x (p ^ (n - x)))) (↑p ^ x)) =
    ∑ i ∈ range (n + 1), (monomial (single i (p ^ (n - i)))) (↑p ^ i)

Tactic:
]

Goal state after:
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
S : Type u_2
inst✝ : CommRing S
f : R →+* S
n : ℕ
⊢ ∑ x ∈ range (n + 1), (map f) ((monomial (single x (p ^ (n - x)))) (↑p ^ x)) =
    ∑ i ∈ range (n + 1), (monomial (single i (p ^ (n - i)))) (↑p ^ i)
Module: Mathlib.RingTheory.WittVector.WittPolynomial

Goal state before:
pp: p : ℕ
R : Type u_1
inst✝¹ : CommRing R
S : Type u_2
inst✝ : CommRing S
f : R →+* S
n i : ℕ
x✝ : i ∈ range (n + 1)
⊢ (monomial (single i (p ^ (n - i)))) (↑p ^ i) = (monomial (single i (p ^ (n - i)))) (↑p ^ i)

Tactic:
]

Goal state after:
Module: Mathlib.RingTheory.WittVector.WittPolynomial

Goal state before:
pp: p : ℕ
R : Type u_1
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
n : ℕ
⊢ 0 = 0

pp: p : ℕ
R : Type u_1
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
n : ℕ
⊢ ∀ x ∈ range (n + 1), (if single x (p ^ (n - x)) = 0 then ↑p ^ x else 0) = 0

Tactic:
]

Goal state after:
p : ℕ
R : Type u_1
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
n : ℕ
⊢ ∀ x ∈ range (n + 1), (if single x (p ^ (n - x)) = 0 then ↑p ^ x else 0) = 0
Module: Mathlib.RingTheory.WittVector.WittPolynomial

Goal state before:
pp: p : ℕ
R : Type u_1
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
n i : ℕ
a✝ : i ∈ range (n + 1)
⊢ 0 = 0

pp: case hnc
p : ℕ
R : Type u_1
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
n i : ℕ
a✝ : i ∈ range (n + 1)
⊢ ¬single i (p ^ (n - i)) = 0

Tactic:
]

Goal state after:
case hnc
p : ℕ
R : Type u_1
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
n i : ℕ
a✝ : i ∈ range (n + 1)
⊢ ¬single i (p ^ (n - i)) = 0
Module: Mathlib.RingTheory.WittVector.WittPolynomial

Goal state before:
pp: case hnc
p : ℕ
R : Type u_1
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
n i : ℕ
a✝ : i ∈ range (n + 1)
⊢ ¬p ^ (n - i) = 0

Tactic:
]

Goal state after:
case hnc
p : ℕ
R : Type u_1
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
n i : ℕ
a✝ : i ∈ range (n + 1)
⊢ ¬p ^ (n - i) = 0
Module: Mathlib.RingTheory.WittVector.WittPolynomial

Goal state before:
pp: p n : ℕ
⊢ (range (n + 1)).sum ?m.99 = ∑ x ∈ range (n + 1), (expand p) (C (↑p ^ x) * X x ^ p ^ (n - x))

pp: p n : ℕ
⊢ ∀ x ∈ range (n + 1), C (↑p ^ x) * X x ^ p ^ (n + 1 - x) = ?m.99 x

pp: p n : ℕ
⊢ ℕ → MvPolynomial ℕ (ZMod (p ^ (n + 1)))

Tactic:
]

Goal state after:
p n : ℕ
⊢ ∀ x ∈ range (n + 1), C (↑p ^ x) * X x ^ p ^ (n + 1 - x) = (expand p) (C (↑p ^ x) * X x ^ p ^ (n - x))
Module: Mathlib.RingTheory.WittVector.WittPolynomial

Goal state before:
pp: p n k : ℕ
hk : k ∈ range (n + 1)
⊢ C (↑p ^ k) * X k ^ p ^ (n + 1 - k) =
    (algebraMap (ZMod (p ^ (n + 1))) (MvPolynomial ℕ (ZMod (p ^ (n + 1))))) (↑p ^ k) * X k ^ p ^ (n - k + 1)

Tactic:
]

Goal state after:
p n k : ℕ
hk : k ∈ range (n + 1)
⊢ C (↑p ^ k) * X k ^ p ^ (n + 1 - k) =
    (algebraMap (ZMod (p ^ (n + 1))) (MvPolynomial ℕ (ZMod (p ^ (n + 1))))) (↑p ^ k) * X k ^ p ^ (n - k + 1)
Module: Mathlib.RingTheory.WittVector.WittPolynomial

Goal state before:
pp: case e_a.e_a.e_a
p n k : ℕ
hk : k < n + 1
⊢ n + 1 - k = n - k + 1

Tactic:
]

Goal state after:
case e_a.e_a.e_a
p n k : ℕ
hk : k < n + 1
⊢ n + 1 - k = n - k + 1
Module: Mathlib.RingTheory.WittVector.WittPolynomial

Goal state before:
pp: case e_a.e_a.e_a
p n k : ℕ
hk : k < n + 1
⊢ n - k + 1 = n - k + 1

Tactic:
]

Goal state after:
Module: Mathlib.RingTheory.WittVector.WittPolynomial

Goal state before:
pp: p : ℕ
R : Type u_1
inst✝¹ : CommRing R
hp : NeZero p
inst✝ : CharZero R
n : ℕ
this : ∀ (i : ℕ), ((monomial (single i (p ^ (n - i)))) (↑p ^ i)).vars = {i}
⊢ ((range (n + 1)).biUnion fun i ↦ ((monomial (single i (p ^ (n - i)))) (↑p ^ i)).vars) = range (n + 1)

pp: case h
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
hp : NeZero p
inst✝ : CharZero R
n : ℕ
this : ∀ (i : ℕ), ((monomial (single i (p ^ (n - i)))) (↑p ^ i)).vars = {i}
⊢ Pairwise (Function.onFun Disjoint fun i ↦ ((monomial (single i (p ^ (n - i)))) (↑p ^ i)).vars)

Tactic:
]

Goal state after:
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
hp : NeZero p
inst✝ : CharZero R
n : ℕ
this : ∀ (i : ℕ), ((monomial (single i (p ^ (n - i)))) (↑p ^ i)).vars = {i}
⊢ ((range (n + 1)).biUnion fun i ↦ ((monomial (single i (p ^ (n - i)))) (↑p ^ i)).vars) = range (n + 1)

case h
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
hp : NeZero p
inst✝ : CharZero R
n : ℕ
this : ∀ (i : ℕ), ((monomial (single i (p ^ (n - i)))) (↑p ^ i)).vars = {i}
⊢ Pairwise (Function.onFun Disjoint fun i ↦ ((monomial (single i (p ^ (n - i)))) (↑p ^ i)).vars)
Module: Mathlib.RingTheory.WittVector.WittPolynomial

Goal state before:
pp: p : ℕ
R : Type u_1
inst✝¹ : CommRing R
hp : NeZero p
inst✝ : CharZero R
n : ℕ
this : ∀ (i : ℕ), ((monomial (single i (p ^ (n - i)))) (↑p ^ i)).vars = {i}
⊢ ((range (n + 1)).biUnion fun i ↦ ((monomial (single i (p ^ (n - i)))) (↑p ^ i)).vars) = range (n + 1)

pp: case h
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
hp : NeZero p
inst✝ : CharZero R
n : ℕ
this : ∀ (i : ℕ), ((monomial (single i (p ^ (n - i)))) (↑p ^ i)).vars = {i}
⊢ Pairwise (Function.onFun Disjoint fun i ↦ ((monomial (single i (p ^ (n - i)))) (↑p ^ i)).vars)

Tactic:
· simp only [this, biUnion_singleton_eq_self]

Goal state after:
case h
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
hp : NeZero p
inst✝ : CharZero R
n : ℕ
this : ∀ (i : ℕ), ((monomial (single i (p ^ (n - i)))) (↑p ^ i)).vars = {i}
⊢ Pairwise (Function.onFun Disjoint fun i ↦ ((monomial (single i (p ^ (n - i)))) (↑p ^ i)).vars)
Module: Mathlib.RingTheory.WittVector.WittPolynomial

Goal state before:
pp: case h
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
hp : NeZero p
inst✝ : CharZero R
n : ℕ
this : ∀ (i : ℕ), ((monomial (single i (p ^ (n - i)))) (↑p ^ i)).vars = {i}
a b : ℕ
h : a ≠ b
⊢ ¬a = b

Tactic:
]

Goal state after:
case h
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
hp : NeZero p
inst✝ : CharZero R
n : ℕ
this : ∀ (i : ℕ), ((monomial (single i (p ^ (n - i)))) (↑p ^ i)).vars = {i}
a b : ℕ
h : a ≠ b
⊢ ¬a = b
Module: Mathlib.RingTheory.WittVector.WittPolynomial

Goal state before:
pp: case h
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
hp : NeZero p
inst✝ : CharZero R
n : ℕ
this : ∀ (i : ℕ), ((monomial (single i (p ^ (n - i)))) (↑p ^ i)).vars = {i}
a b : ℕ
h : a ≠ b
⊢ a ∉ (fun i ↦ {i}) b

Tactic:
rwa [mem_singleton]

Goal state after:
Module: Mathlib.RingTheory.WittVector.WittPolynomial

Goal state before:
pp: p : ℕ
R : Type u_1
inst✝ : CommRing R
hp : NeZero p
n : ℕ
⊢ ((map (Int.castRingHom R)) (W_ ℤ n)).vars ⊆ (W_ ℤ n).vars

Tactic:
]

Goal state after:
p : ℕ
R : Type u_1
inst✝ : CommRing R
hp : NeZero p
n : ℕ
⊢ ((map (Int.castRingHom R)) (W_ ℤ n)).vars ⊆ (W_ ℤ n).vars
Module: Mathlib.RingTheory.WittVector.WittPolynomial

Goal state before:
pp: p : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Invertible ↑p
n : ℕ
⊢ (X n - ∑ i, C (↑p ^ ↑i) * xInTermsOfW p R ↑i ^ p ^ (n - ↑i)) * C (⅟↑p ^ n) =
    (X n - ∑ i, C (↑p ^ ↑i) * xInTermsOfW p R ↑i ^ p ^ (n - ↑i)) * C (⅟↑p ^ n)

Tactic:
]

Goal state after: