mathlib-initiative/mathlib-tactics huggingface dataset:
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
x : Perfection (R ⧸ I) p
⊢ ∀ (n : ℕ), x.teichmullerAux n ≡ x.teichmullerAux (n + 1) [SMOD I ^ n • ⊤]

Tactic:
by

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
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
h2 : h v ≠ 0
eq : (MvPolynomial.finSuccEquiv k n) ((T f) (h v)) = 0
⊢ h v = 0

Tactic:
by

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✝ : IsPrecomplete I R
x : Perfection (R ⧸ I) p
y : R
n : ℕ
h : (Ideal.Quotient.mk I) y = (coeff (R ⧸ I) p n) x
this : x.teichmullerAux (n + 1) ≡ ⋯.choose [SMOD I ^ (n + 1)]
⊢ Quotient.out ((coeff (R ⧸ I) p n) x) ≡ y [SMOD I]

Tactic:
by

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✝ : IsPrecomplete I R
x : Perfection (R ⧸ I) p
y : R
n : ℕ
h : (Ideal.Quotient.mk I) y = (coeff (R ⧸ I) p n) x
⊢ x.teichmullerFun ≡ y ^ p ^ n [SMOD I ^ (n + 1)]

Tactic:
by

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
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
⊢ ((MvPolynomial.finSuccEquiv k n) ((T f) (h v + ∑ x ∈ f.support \ {v}, h x))).leadingCoeff =
    ((MvPolynomial.finSuccEquiv k n) ((T f) (h v))).leadingCoeff

Tactic:
by

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
y : R
N : ℕ
h : ∀ n ≥ N, ∃ z, (Ideal.Quotient.mk I) z = (coeff (R ⧸ I) p n) x ∧ z ^ p ^ n ≡ y [SMOD I ^ (n + 1)]
n : ℕ
hn : n ≤ N
z : R
hz₁ : (Ideal.Quotient.mk I) z = (coeff (R ⧸ I) p N) x
hz₂ : z ^ p ^ N ≡ y [SMOD I ^ (N + 1)]
⊢ n ≤ N + 1

Tactic:
by

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)
inst✝ : Invertible ↑p
n : ℕ
⊢ constantCoeff (xInTermsOfW p R n) = 0

Tactic:
by

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
y : R
N : ℕ
h : ∀ n ≥ N, ∃ z, (Ideal.Quotient.mk I) z = (coeff (R ⧸ I) p n) x ∧ z ^ p ^ n ≡ y [SMOD I ^ (n + 1)]
n : ℕ
hn : N ≤ n
z : R
hz₁ : (Ideal.Quotient.mk I) z = (coeff (R ⧸ I) p n) x
hz₂ : z ^ p ^ n ≡ y [SMOD I ^ (n + 1)]
⊢ n ≤ n + 1

Tactic:
by

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

Goal state before:
pp: p : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Invertible ↑p
⊢ xInTermsOfW p R 0 = X 0

Tactic:
by

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
y : R
h : ∃ N, ∀ n ≥ N, ∃ z, (Ideal.Quotient.mk I) z = (coeff (R ⧸ I) p n) x ∧ z ^ p ^ n ≡ y [SMOD I ^ (n + 1)]
⊢ x.teichmullerFun = y

Tactic:
by

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✝ : ℕ
⊢ (Ideal.Quotient.mk I) 1 = (coeff (R ⧸ I) p x✝) 1 ∧ 1 ^ p ^ x✝ ≡ 1 [SMOD I ^ (x✝ + 1)]

Tactic:
by

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 y : Perfection (R ⧸ I) p
n : ℕ
⊢ (Ideal.Quotient.mk I) (Quotient.out ((coeff (R ⧸ I) p n) x) * Quotient.out ((coeff (R ⧸ I) p n) y)) =
    (coeff (R ⧸ I) p n) (x * y)

Tactic:
by

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
fne : f ≠ 0
⊢ IsUnit ((MvPolynomial.finSuccEquiv k n) ((T f) f)).leadingCoeff

Tactic:
by

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
I : Ideal (MvPolynomial (Fin (n + 1)) k)
fne : f ≠ 0
fi : f ∈ I
⊢ (hom1 f I).IsIntegral

Tactic:
by

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) →₀ ℕ
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

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 y : Perfection (R ⧸ I) p
⊢ (x * y).teichmullerFun = x.teichmullerFun * y.teichmullerFun

Tactic:
by

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) →₀ ℕ
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 ((RingHom.id (MvPolynomial (Fin (n + 1)) k)).comp ↑(T f)) I =
    Ideal.map (RingHom.id (MvPolynomial (Fin (n + 1)) k)) (Ideal.map (T f) I)

Tactic:
by

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
this : p ≠ 0
n : ℕ
⊢ (Ideal.Quotient.mk I) 0 = (coeff (R ⧸ I) p n) 0 ∧ 0 ^ p ^ n ≡ 0 [SMOD I ^ (n + 1)]

Tactic:
by

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) →₀ ℕ
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 ((↑g.symm).comp ↑g) (Ideal.map (T f) I) = Ideal.map (↑g.symm) (Ideal.map g (Ideal.map (T f) I))

Tactic:
by

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) →₀ ℕ
I : Ideal (MvPolynomial (Fin (n + 1)) k)
⊢ Ideal.map (T f) I =
    Ideal.map (↑(MvPolynomial.finSuccEquiv k n).symm) (Ideal.map (MvPolynomial.finSuccEquiv k n) (Ideal.map (T f) I))

Tactic:
by

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 p
n : ℕ
⊢ (Ideal.Quotient.mk I) ((coeffMonoidHom R p n) x) = (coeff (R ⧸ I) p n) ((mapMonoidHom p ↑(Ideal.Quotient.mk I)) x) ∧
    (coeffMonoidHom R p n) x ^ p ^ n ≡ (coeffMonoidHom R p 0) x [SMOD I ^ (n + 1)]

Tactic:
by

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) →₀ ℕ
I : Ideal (MvPolynomial (Fin (n + 1)) k)
⊢ I = Ideal.map ((T f).symm.toRingEquiv.toRingHom.comp ↑(T f)) I

Tactic:
by

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
⊢ (Ideal.Quotient.mk I) ((teichmuller p I) x) = (coeff (R ⧸ I) p 0) x

Tactic:
by

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) →₀ ℕ
I : Ideal (MvPolynomial (Fin (n + 1)) k)
⊢ Ideal.map ((T f).symm.toRingEquiv.toRingHom.comp ↑(T f)) I = Ideal.map (↑(T f).symm) (Ideal.map (T f) I)

Tactic:
by

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) →₀ ℕ
I : Ideal (MvPolynomial (Fin (n + 1)) k)
⊢ I = Ideal.map (↑(T f).symm) (Ideal.map (T f) I)

Tactic:
by

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✝
p : ℕ
inst✝³ : Fact (Nat.Prime p)
R : Type u_2
inst✝² : CommRing R
I : Ideal R
inst✝¹ : CharP (R ⧸ I) p
inst✝ : IsAdicComplete I R
⊢ (liftMonoidHom p (Perfection R p) R).symm
      (((liftMonoidHom p (Perfection (R ⧸ I) p) R) (teichmuller p I)).comp (mapMonoidHom p ↑(Ideal.Quotient.mk I))) =
    (liftMonoidHom p (Perfection R p) R).symm (MonoidHom.id (Perfection R p))

Tactic:
by

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✝
p : ℕ
inst✝³ : Fact (Nat.Prime p)
R : Type u_2
inst✝² : CommRing R
I : Ideal R
inst✝¹ : CharP (R ⧸ I) p
inst✝ : IsAdicComplete I R
⊢ (liftMonoidHom p (Perfection (R ⧸ I) p) (R ⧸ I)).symm
      ((mapMonoidHom p ↑(Ideal.Quotient.mk I)).comp ((liftMonoidHom p (Perfection (R ⧸ I) p) R) (teichmuller p I))) =
    (liftMonoidHom p (Perfection (R ⧸ I) p) (R ⧸ I)).symm (MonoidHom.id (Perfection (R ⧸ I) p))

Tactic:
by

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
⊢ (coeffMonoidHom R p 0) ((quotientMulEquiv p I).symm x) = (teichmuller₀ p I) x

Tactic:
by

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

Goal state before:
pp: p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℚ
n : ℕ
⊢ (bind₁ (wittStructureRat p Φ)) (W_ ℚ n) =
    (bind₁ fun k ↦ (bind₁ fun i ↦ (rename (Prod.mk i)) (W_ ℚ k)) Φ) ((bind₁ (xInTermsOfW p ℚ)) (W_ ℚ n))

Tactic:
by

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

Goal state before:
pp: p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℚ
n : ℕ
⊢ (bind₁ fun k ↦ (bind₁ fun i ↦ (rename (Prod.mk i)) (W_ ℚ k)) Φ) ((bind₁ (xInTermsOfW p ℚ)) (W_ ℚ n)) =
    (bind₁ fun i ↦ (rename (Prod.mk i)) (W_ ℚ n)) Φ

Tactic:
by

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

Goal state before:
pp: case ind
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
ih : ∀ m < n, m ∈ (xInTermsOfW p ℚ m).vars ∧ (xInTermsOfW p ℚ m).vars ⊆ range (m + 1)
i : ℕ
⊢ i ∈ {n} ∪ (∑ i ∈ range n, C (↑p ^ i) * xInTermsOfW p ℚ i ^ p ^ (n - i)).vars → i ∈ {n} ∪ range n

Tactic:
rw [mem_union, mem_union]

Goal state after:
case ind
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
ih : ∀ m < n, m ∈ (xInTermsOfW p ℚ m).vars ∧ (xInTermsOfW p ℚ m).vars ⊆ range (m + 1)
i : ℕ
⊢ i ∈ {n} ∨ i ∈ (∑ i ∈ range n, C (↑p ^ i) * xInTermsOfW p ℚ i ^ p ^ (n - i)).vars → i ∈ {n} ∨ i ∈ range n
Module: Mathlib.RingTheory.NoetherNormalization

Goal state before:
pp: k : Type u_1
inst✝ : Field k
n : ℕ
I : Ideal (MvPolynomial (Fin 0) k)
hi : I ≠ ⊤
a b : MvPolynomial (Fin 0) k
hab : a - b ∈ I
ne✝ : ¬a = b
eq : a - b = MvPolynomial.C (MvPolynomial.coeff 0 (a - b))
ne : MvPolynomial.coeff 0 (a - b) ≠ 0
c : k
left✝ : MvPolynomial.coeff 0 (a - b) * c = 1
eqr : c * MvPolynomial.coeff 0 (a - b) = 1
⊢ c • (a - b) = 1

Tactic:
by

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

Goal state before:
pp: p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℚ
⊢ ∃! φ, ∀ (n : ℕ), (bind₁ φ) (W_ ℚ n) = (bind₁ fun i ↦ (rename (Prod.mk i)) (W_ ℚ n)) Φ

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.NoetherNormalization

Goal state before:
pp: k : Type u_1
inst✝ : Field k
n d : ℕ
hd : ∀ (I : Ideal (MvPolynomial (Fin d) k)), I ≠ ⊤ → ∃ s ≤ d, ∃ g, Function.Injective ⇑g ∧ g.IsIntegral
I : Ideal (MvPolynomial (Fin (d + 1)) k)
hi : I ≠ ⊤
eqi : ¬I = 0
f : MvPolynomial (Fin (d + 1)) k
fi : f ∈ I
fne : f ≠ 0
ϕ : MvPolynomial (Fin d) k ⧸ ker (hom2 f I) →ₐ[k] MvPolynomial (Fin (d + 1)) k ⧸ I := kerLiftAlg (hom2 f I)
this : Nontrivial (MvPolynomial (Fin (d + 1)) k ⧸ I)
s : ℕ
left✝ : s ≤ d
g : MvPolynomial (Fin s) k →ₐ[k] MvPolynomial (Fin d) k ⧸ ker (hom2 f I)
injg : Function.Injective ⇑g
intg : g.IsIntegral
a : MvPolynomial (Fin d) k
⊢ ((kerLiftAlg (hom2 f I)).comp (Quotient.mkₐ k (ker (hom2 f I)))) a = (hom2 f I) a

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.NoetherNormalization

Goal state before:
pp: k : Type u_1
inst✝ : Field k
n d : ℕ
hd : ∀ (I : Ideal (MvPolynomial (Fin d) k)), I ≠ ⊤ → ∃ s ≤ d, ∃ g, Function.Injective ⇑g ∧ g.IsIntegral
I : Ideal (MvPolynomial (Fin (d + 1)) k)
hi : I ≠ ⊤
eqi : ¬I = 0
f : MvPolynomial (Fin (d + 1)) k
fi : f ∈ I
fne : f ≠ 0
ϕ : MvPolynomial (Fin d) k ⧸ ker (hom2 f I) →ₐ[k] MvPolynomial (Fin (d + 1)) k ⧸ I := kerLiftAlg (hom2 f I)
this : Nontrivial (MvPolynomial (Fin (d + 1)) k ⧸ I)
s : ℕ
left✝ : s ≤ d
g : MvPolynomial (Fin s) k →ₐ[k] MvPolynomial (Fin d) k ⧸ ker (hom2 f I)
injg : Function.Injective ⇑g
intg : g.IsIntegral
comp : (kerLiftAlg (hom2 f I)).comp (Quotient.mkₐ k (ker (hom2 f I))) = hom2 f I
⊢ s ≤ d + 1

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.NoetherNormalization

Goal state before:
pp: k : Type u_1
inst✝ : Field k
n : ℕ
I : Ideal (MvPolynomial (Fin n) k)
hi : I ≠ ⊤
⊢ ∃ s ≤ n, ∃ g, Function.Injective ⇑g ∧ g.IsIntegral

Tactic:
by

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

Goal state before:
pp: p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℚ
n : ℕ
⊢ wittStructureRat 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:
by

Goal state after:
Module: Mathlib.RingTheory.NoetherNormalization

Goal state before:
pp: k : Type u_2
R : Type u_3
inst✝² : Field k
inst✝¹ : CommRing R
inst✝ : Nontrivial R
a : Algebra k R
fin : Algebra.FiniteType k R
⊢ ∃ s g, Function.Injective ⇑g ∧ g.IsIntegral

Tactic:
by

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

Goal state before:
pp: p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℚ
n : ℕ
⊢ C (1 / ↑p ^ n) * (wittStructureRat p Φ n * C (↑p ^ n)) =
    C (1 / ↑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:
by

Goal state after:
Module: Mathlib.RingTheory.NoetherNormalization

Goal state before:
pp: k : Type u_2
R : Type u_3
inst✝² : Field k
inst✝¹ : CommRing R
inst✝ : Nontrivial R
a : Algebra k R
fin : Algebra.FiniteType k R
s : ℕ
g : MvPolynomial (Fin s) k →ₐ[k] R
inj : Function.Injective ⇑g
int : g.IsIntegral
⊢ algebraMap k R = g.comp (algebraMap k (MvPolynomial (Fin s) k))

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.NoetherNormalization

Goal state before:
pp: k : Type u_2
R : Type u_3
inst✝² : Field k
inst✝¹ : CommRing R
inst✝ : Nontrivial R
a : Algebra k R
fin : Algebra.FiniteType k R
⊢ ∃ s g, Function.Injective ⇑g ∧ g.Finite

Tactic:
by

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

Goal state before:
pp: p : ℕ
R : Type u_1
x y : 𝕎 R
h : ∀ (n : ℕ), x.coeff n = y.coeff n
⊢ x = y

Tactic:
by

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ wittZero p n = 0

Tactic:
by

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
⊢ wittOne p 0 = 1

Tactic:
by

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

Goal state before:
pp: p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℚ
n : ℕ
⊢ wittStructureRat p Φ n =
    C (1 / ↑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:
by

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ n ∈ (xInTermsOfW p ℚ n).vars ∧ (xInTermsOfW p ℚ n).vars ⊆ range (n + 1)

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
hn : 0 < n
⊢ wittOne p n = 0

Tactic:
by

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

Goal state before:
pp: p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n : ℕ
IH :
  ∀ m < n + 1, (map (Int.castRingHom ℚ)) (wittStructureInt p Φ m) = wittStructureRat p ((map (Int.castRingHom ℚ)) Φ) m
⊢ (bind₁ fun b ↦ (rename fun i ↦ (b, i)) ((expand p) (W_ ℤ n))) Φ =
    (bind₁ fun i ↦ (expand p) (wittStructureInt p Φ i)) (W_ ℤ n)

Tactic:
by

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
⊢ wittAdd p 0 = X (0, 0) + X (1, 0)

Tactic:
by

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
⊢ wittSub p 0 = X (0, 0) - X (1, 0)

Tactic:
by

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
⊢ wittMul p 0 = X (0, 0) * X (1, 0)

Tactic:
by

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
⊢ wittNeg p 0 = -X (0, 0)

Tactic:
by

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ constantCoeff (wittAdd p n) = 0

Tactic:
by

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ constantCoeff (wittSub p n) = 0

Tactic:
by

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ constantCoeff (wittMul p n) = 0

Tactic:
by

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ constantCoeff (wittNeg p n) = 0

Tactic:
by

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
m n : ℕ
⊢ constantCoeff (wittNSMul p m n) = 0

Tactic:
by

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
z : ℤ
n : ℕ
⊢ constantCoeff (wittZSMul p z n) = 0

Tactic:
by

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

Goal state before:
pp: p : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Invertible ↑p
k : ℕ
⊢ (bind₁ (xInTermsOfW p R)) (W_ R k) = X k

Tactic:
by

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

Goal state before:
pp: p' : ℕ
R' : Type u_2
x y : WittVector p' R'
i : Fin 2
⊢ (![x, y] i).coeff = ![x.coeff, y.coeff] i

Tactic:
by

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

Goal state before:
pp: p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
x y : 𝕎 R
n : ℕ
⊢ (x + y).coeff n = peval (wittAdd p n) ![x.coeff, y.coeff]

Tactic:
by

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

Goal state before:
pp: p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
x y : 𝕎 R
n : ℕ
⊢ (x - y).coeff n = peval (wittSub p n) ![x.coeff, y.coeff]

Tactic:
by

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

Goal state before:
pp: p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
x y : 𝕎 R
n : ℕ
⊢ (x * y).coeff n = peval (wittMul p n) ![x.coeff, y.coeff]

Tactic:
by

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

Goal state before:
pp: p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
x : 𝕎 R
n : ℕ
⊢ (-x).coeff n = peval (wittNeg p n) ![x.coeff]

Tactic:
by

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

Goal state before:
pp: p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
m : ℕ
x : 𝕎 R
n : ℕ
⊢ (m • x).coeff n = peval (wittNSMul p m n) ![x.coeff]

Tactic:
by

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

Goal state before:
pp: p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
m : ℤ
x : 𝕎 R
n : ℕ
⊢ (m • x).coeff n = peval (wittZSMul p m n) ![x.coeff]

Tactic:
by

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

Goal state before:
pp: p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
m : ℕ
x : 𝕎 R
n : ℕ
⊢ (x ^ m).coeff n = peval (wittPow p m n) ![x.coeff]

Tactic:
by

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

Goal state before:
pp: p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
x y : 𝕎 R
⊢ (x + y).coeff 0 = x.coeff 0 + y.coeff 0

Tactic:
by

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

Goal state before:
pp: p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
x y : 𝕎 R
⊢ (x * y).coeff 0 = x.coeff 0 * y.coeff 0

Tactic:
by

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

Goal state before:
pp: p : ℕ
α : Type u_3
β : Type u_4
f : α → β
hf : Surjective f
x : 𝕎 β
⊢ mapFun f (mk p fun n ↦ Classical.choose ⋯) = x

Tactic:
by

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

Goal state before:
pp: p : ℕ
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Fact (Nat.Prime p)
f : R →+* S
⊢ mapFun (⇑f) 0 = 0

Tactic:
by

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

Goal state before:
pp: p : ℕ
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Fact (Nat.Prime p)
f : R →+* S
⊢ mapFun (⇑f) 1 = 1

Tactic:
by

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

Goal state before:
pp: p : ℕ
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Fact (Nat.Prime p)
f : R →+* S
x y : 𝕎 R
⊢ mapFun (⇑f) (x + y) = mapFun (⇑f) x + mapFun (⇑f) y

Tactic:
by

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

Goal state before:
pp: p : ℕ
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Fact (Nat.Prime p)
f : R →+* S
x y : 𝕎 R
⊢ mapFun (⇑f) (x - y) = mapFun (⇑f) x - mapFun (⇑f) y

Tactic:
by

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

Goal state before:
pp: p : ℕ
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Fact (Nat.Prime p)
f : R →+* S
x y : 𝕎 R
⊢ mapFun (⇑f) (x * y) = mapFun (⇑f) x * mapFun (⇑f) y

Tactic:
by

Goal state after: