mathlib-initiative/mathlib-tactics huggingface dataset:
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) *
      ((bind₁ fun b ↦ (rename fun i ↦ (b, i)) (W_ ℚ n)) Φ -
        ∑ i ∈ Finset.range n, C (↑p ^ i) * wittStructureRat p Φ i ^ p ^ (n - i)) =
    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:
]

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
algInst✝ : Algebra (MvPolynomial (Fin s) k) R := g.toAlgebra
algebraizeInst✝ : Algebra.IsIntegral (MvPolynomial (Fin s) k) R
⊢ g.comp (algebraMap k (MvPolynomial (Fin s) k)) = g.comp (algebraMap k (MvPolynomial (Fin s) k))

Tactic:
]

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 = wittStructureRat p Φ n

pp: case h
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℚ
n : ℕ
⊢ ↑p ^ n ≠ 0

Tactic:
]

Goal state after:
case h
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℚ
n : ℕ
⊢ ↑p ^ n ≠ 0
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) * (wittStructureRat p Φ n * C (↑p ^ n))

Tactic:
rw [mul_left_comm, ← C_mul, div_mul_cancel₀, C_1, mul_one]

Goal state after:
case h
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℚ
n : ℕ
⊢ ↑p ^ n ≠ 0
Module: Mathlib.RingTheory.WittVector.Defs

Goal state before:
pp: case h
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
IH : ∀ m < n, 0 < m → (bind₁ fun k ↦ 1) (xInTermsOfW p ℚ m) = 0
hn : 0 < n
⊢ (bind₁ fun k ↦ 1) (xInTermsOfW p ℚ n) = 0

Tactic:
| h n IH =>

Goal state after:
case h
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
IH : ∀ m < n, 0 < m → (bind₁ fun k ↦ 1) (xInTermsOfW p ℚ m) = 0
hn : 0 < n
⊢ (bind₁ fun k ↦ 1) (xInTermsOfW p ℚ n) = 0
Module: Mathlib.RingTheory.WittVector.Defs

Goal state before:
pp: case h
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
IH : ∀ m < n, 0 < m → (bind₁ fun k ↦ 1) (xInTermsOfW p ℚ m) = 0
hn : 0 < n
⊢ (bind₁ fun k ↦ 1) ((X n - ∑ i ∈ Finset.range n, C (↑p ^ i) * xInTermsOfW p ℚ i ^ p ^ (n - i)) * C (⅟↑p ^ n)) = 0

Tactic:
]

Goal state after:
case h
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
IH : ∀ m < n, 0 < m → (bind₁ fun k ↦ 1) (xInTermsOfW p ℚ m) = 0
hn : 0 < n
⊢ (bind₁ fun k ↦ 1) ((X n - ∑ i ∈ Finset.range n, C (↑p ^ i) * xInTermsOfW p ℚ i ^ p ^ (n - i)) * C (⅟↑p ^ n)) = 0
Module: Mathlib.RingTheory.WittVector.WittPolynomial

Goal state before:
pp: case ind.hpq
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
ih : ∀ m < n, m ∈ (xInTermsOfW p ℚ m).vars ∧ (xInTermsOfW p ℚ m).vars ⊆ range (m + 1)
H : ∃ a ∈ range n, n ∈ (C (↑p ^ a) * xInTermsOfW p ℚ a ^ p ^ (n - a)).vars
⊢ False

Tactic:
]

Goal state after:
case ind.hpq
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
ih : ∀ m < n, m ∈ (xInTermsOfW p ℚ m).vars ∧ (xInTermsOfW p ℚ m).vars ⊆ range (m + 1)
H : ∃ a ∈ range n, n ∈ (C (↑p ^ a) * xInTermsOfW p ℚ a ^ p ^ (n - a)).vars
⊢ False
Module: Mathlib.RingTheory.WittVector.Defs

Goal state before:
pp: case h
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
IH : ∀ m < n, 0 < m → (bind₁ fun k ↦ 1) (xInTermsOfW p ℚ m) = 0
hn : 0 < n
⊢ C ⅟↑p ^ n - (∑ x ∈ Finset.range n, C ↑p ^ x * (bind₁ fun k ↦ 1) (xInTermsOfW p ℚ x) ^ p ^ (n - x)) * C ⅟↑p ^ n = 0

Tactic:
]

Goal state after:
case h
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
IH : ∀ m < n, 0 < m → (bind₁ fun k ↦ 1) (xInTermsOfW p ℚ m) = 0
hn : 0 < n
⊢ C ⅟↑p ^ n - (∑ x ∈ Finset.range n, C ↑p ^ x * (bind₁ fun k ↦ 1) (xInTermsOfW p ℚ x) ^ p ^ (n - x)) * C ⅟↑p ^ n = 0
Module: Mathlib.RingTheory.WittVector.WittPolynomial

Goal state before:
pp: case ind.hpq
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
ih : ∀ m < n, m ∈ (xInTermsOfW p ℚ m).vars ∧ (xInTermsOfW p ℚ m).vars ⊆ range (m + 1)
j : ℕ
hj : j ∈ range n
H : n ∈ (xInTermsOfW p ℚ j ^ p ^ (n - j)).vars
⊢ False

pp: case ind.hpq.ha
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
ih : ∀ m < n, m ∈ (xInTermsOfW p ℚ m).vars ∧ (xInTermsOfW p ℚ m).vars ⊆ range (m + 1)
j : ℕ
hj : j ∈ range n
H : n ∈ (C (↑p ^ j) * xInTermsOfW p ℚ j ^ p ^ (n - j)).vars
⊢ ↑p ^ j ≠ 0

Tactic:
]

Goal state after:
case ind.hpq
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
ih : ∀ m < n, m ∈ (xInTermsOfW p ℚ m).vars ∧ (xInTermsOfW p ℚ m).vars ⊆ range (m + 1)
j : ℕ
hj : j ∈ range n
H : n ∈ (xInTermsOfW p ℚ j ^ p ^ (n - j)).vars
⊢ False

case ind.hpq.ha
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
ih : ∀ m < n, m ∈ (xInTermsOfW p ℚ m).vars ∧ (xInTermsOfW p ℚ m).vars ⊆ range (m + 1)
j : ℕ
hj : j ∈ range n
H : n ∈ (C (↑p ^ j) * xInTermsOfW p ℚ j ^ p ^ (n - j)).vars
⊢ ↑p ^ j ≠ 0
Module: Mathlib.RingTheory.WittVector.Defs

Goal state before:
pp: case h
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
IH : ∀ m < n, 0 < m → (bind₁ fun k ↦ 1) (xInTermsOfW p ℚ m) = 0
hn : 0 < n
⊢ C ⅟↑p ^ n - C ↑p ^ 0 * (bind₁ fun k ↦ 1) (xInTermsOfW p ℚ 0) ^ p ^ (n - 0) * C ⅟↑p ^ n = 0

pp: case h.h₀
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
IH : ∀ m < n, 0 < m → (bind₁ fun k ↦ 1) (xInTermsOfW p ℚ m) = 0
hn : 0 < n
⊢ ∀ b ∈ Finset.range n, b ≠ 0 → C ↑p ^ b * (bind₁ fun k ↦ 1) (xInTermsOfW p ℚ b) ^ p ^ (n - b) = 0

pp: case h.h₁
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
IH : ∀ m < n, 0 < m → (bind₁ fun k ↦ 1) (xInTermsOfW p ℚ m) = 0
hn : 0 < n
⊢ 0 ∉ Finset.range n → C ↑p ^ 0 * (bind₁ fun k ↦ 1) (xInTermsOfW p ℚ 0) ^ p ^ (n - 0) = 0

Tactic:
]

Goal state after:
case h
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
IH : ∀ m < n, 0 < m → (bind₁ fun k ↦ 1) (xInTermsOfW p ℚ m) = 0
hn : 0 < n
⊢ C ⅟↑p ^ n - C ↑p ^ 0 * (bind₁ fun k ↦ 1) (xInTermsOfW p ℚ 0) ^ p ^ (n - 0) * C ⅟↑p ^ n = 0

case h.h₀
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
IH : ∀ m < n, 0 < m → (bind₁ fun k ↦ 1) (xInTermsOfW p ℚ m) = 0
hn : 0 < n
⊢ ∀ b ∈ Finset.range n, b ≠ 0 → C ↑p ^ b * (bind₁ fun k ↦ 1) (xInTermsOfW p ℚ b) ^ p ^ (n - b) = 0

case h.h₁
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
IH : ∀ m < n, 0 < m → (bind₁ fun k ↦ 1) (xInTermsOfW p ℚ m) = 0
hn : 0 < n
⊢ 0 ∉ Finset.range n → C ↑p ^ 0 * (bind₁ fun k ↦ 1) (xInTermsOfW p ℚ 0) ^ p ^ (n - 0) = 0
Module: Mathlib.RingTheory.WittVector.WittPolynomial

Goal state before:
pp: case ind.hpq
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
ih : ∀ m < n, m ∈ (xInTermsOfW p ℚ m).vars ∧ (xInTermsOfW p ℚ m).vars ⊆ range (m + 1)
j : ℕ
hj : j < n
H : n ∈ (xInTermsOfW p ℚ j ^ p ^ (n - j)).vars
⊢ False

Tactic:
]

Goal state after:
case ind.hpq
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
ih : ∀ m < n, m ∈ (xInTermsOfW p ℚ m).vars ∧ (xInTermsOfW p ℚ m).vars ⊆ range (m + 1)
j : ℕ
hj : j < n
H : n ∈ (xInTermsOfW p ℚ j ^ p ^ (n - j)).vars
⊢ False
Module: Mathlib.RingTheory.WittVector.WittPolynomial

Goal state before:
pp: case ind.hpq
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
ih : ∀ m < n, m ∈ (xInTermsOfW p ℚ m).vars ∧ (xInTermsOfW p ℚ m).vars ⊆ range (m + 1)
j : ℕ
hj : j < n
H : n < j + 1
⊢ False

Tactic:
]

Goal state after:
case ind.hpq
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
ih : ∀ m < n, m ∈ (xInTermsOfW p ℚ m).vars ∧ (xInTermsOfW p ℚ m).vars ⊆ range (m + 1)
j : ℕ
hj : j < n
H : n < j + 1
⊢ False
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 j : ℕ
hj : j < n
H : i < j + 1
⊢ i < n

Tactic:
]

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 j : ℕ
hj : j < n
H : i < j + 1
⊢ i < n
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
key :
  (bind₁ fun i ↦ (expand p) ((rename (Prod.mk i)) (W_ ℚ n))) ((map (Int.castRingHom ℚ)) Φ) =
    (bind₁ fun i ↦ (expand p) (wittStructureRat p ((map (Int.castRingHom ℚ)) Φ) i)) (W_ ℚ n)
⊢ (bind₁ fun i ↦ (expand p) (wittStructureRat p ((map (Int.castRingHom ℚ)) Φ) i)) (W_ ℚ n) =
    (bind₁ fun i ↦ (expand p) ((map (Int.castRingHom ℚ)) (wittStructureInt p Φ i))) (W_ ℚ n)

Tactic:
]

Goal state after:
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
key :
  (bind₁ fun i ↦ (expand p) ((rename (Prod.mk i)) (W_ ℚ n))) ((map (Int.castRingHom ℚ)) Φ) =
    (bind₁ fun i ↦ (expand p) (wittStructureRat p ((map (Int.castRingHom ℚ)) Φ) i)) (W_ ℚ n)
⊢ (bind₁ fun i ↦ (expand p) (wittStructureRat p ((map (Int.castRingHom ℚ)) Φ) i)) (W_ ℚ n) =
    (bind₁ fun i ↦ (expand p) ((map (Int.castRingHom ℚ)) (wittStructureInt p Φ i))) (W_ ℚ n)
Module: Mathlib.RingTheory.WittVector.Defs

Goal state before:
pp: case h.h₀
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
IH : ∀ m < n, 0 < m → (bind₁ fun k ↦ 1) (xInTermsOfW p ℚ m) = 0
hn : 0 < n
i : ℕ
hin : i < n
hi0 : i ≠ 0
⊢ C ↑p ^ i * (bind₁ fun k ↦ 1) (xInTermsOfW p ℚ i) ^ p ^ (n - i) = 0

Tactic:
]

Goal state after:
case h.h₀
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
IH : ∀ m < n, 0 < m → (bind₁ fun k ↦ 1) (xInTermsOfW p ℚ m) = 0
hn : 0 < n
i : ℕ
hin : i < n
hi0 : i ≠ 0
⊢ C ↑p ^ i * (bind₁ fun k ↦ 1) (xInTermsOfW p ℚ i) ^ p ^ (n - i) = 0
Module: Mathlib.RingTheory.WittVector.Defs

Goal state before:
pp: case h.h₀
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
IH : ∀ m < n, 0 < m → (bind₁ fun k ↦ 1) (xInTermsOfW p ℚ m) = 0
hn : 0 < n
i : ℕ
hin : i < n
hi0 : i ≠ 0
⊢ 0 = 0

Tactic:
]

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
i : ℕ
hi : i < n + 1
⊢ (expand p) (wittStructureRat p ((map (Int.castRingHom ℚ)) Φ) i) =
    (expand p) ((map (Int.castRingHom ℚ)) (wittStructureInt p Φ i))

Tactic:
]

Goal state after:
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
i : ℕ
hi : i < n + 1
⊢ (expand p) (wittStructureRat p ((map (Int.castRingHom ℚ)) Φ) i) =
    (expand p) ((map (Int.castRingHom ℚ)) (wittStructureInt p Φ i))
Module: Mathlib.RingTheory.WittVector.WittPolynomial

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

Tactic:
]

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

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

Tactic:
]

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

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

Tactic:
]

Goal state after:
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Invertible ↑p
k : ℕ
⊢ X k - ∑ i ∈ range k, C (↑p ^ i) * xInTermsOfW p R i ^ p ^ (k - i) +
      ∑ x ∈ range k, C ↑p ^ x * (bind₁ (xInTermsOfW p R)) (X x) ^ p ^ (k - x) =
    X k
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:
simp [Neg.neg, eval, Matrix.cons_fin_one]

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

Goal state before:
pp: p : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Invertible ↑p
n : ℕ
H : ∀ m < n, (bind₁ (W_ R)) (xInTermsOfW p R m) = X m
⊢ X n = X n

Tactic:
]

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

Goal state before:
pp: case ind
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Invertible ↑p
n : ℕ
H : ∀ m < n, (bind₁ (W_ R)) (xInTermsOfW p R m) = X m
⊢ (W_ R n - ∑ x ∈ range n, (bind₁ (W_ R)) (C (↑p ^ x) * xInTermsOfW p R x ^ p ^ (n - x))) *
      (algebraMap R (MvPolynomial ℕ R)) (⅟↑p ^ n) =
    X n * C (↑p ^ n) * C (⅟↑p ^ n)

Tactic:
]

Goal state after:
case ind
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Invertible ↑p
n : ℕ
H : ∀ m < n, (bind₁ (W_ R)) (xInTermsOfW p R m) = X m
⊢ (W_ R n - ∑ x ∈ range n, (bind₁ (W_ R)) (C (↑p ^ x) * xInTermsOfW p R x ^ p ^ (n - x))) *
      (algebraMap R (MvPolynomial ℕ R)) (⅟↑p ^ n) =
    X n * C (↑p ^ n) * C (⅟↑p ^ n)
Module: Mathlib.RingTheory.WittVector.StructurePolynomial

Goal state before:
pp: case succ
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
key :
  (bind₁ fun i ↦ (rename fun i_1 ↦ (i, i_1)) ((expand p) (W_ (ZMod (p ^ (n + 1))) n)))
      ((map (Int.castRingHom (ZMod (p ^ (n + 1))))) Φ) =
    (map (Int.castRingHom (ZMod (p ^ (n + 1))))) ((bind₁ fun i ↦ (expand p) (wittStructureInt p Φ i)) (W_ ℤ n))
⊢ (bind₁ fun i ↦ (map (Int.castRingHom (ZMod (p ^ (n + 1))))) ((rename fun i_1 ↦ (i, i_1)) (W_ ℤ (n + 1))))
      ((map (Int.castRingHom (ZMod (p ^ (n + 1))))) Φ) =
    (map (Int.castRingHom (ZMod (p ^ (n + 1)))))
      (∑ i ∈ Finset.range (n + 1), C (↑p ^ i) * wittStructureInt p Φ i ^ p ^ (n + 1 - i))

Tactic:
]

Goal state after:
case succ
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
key :
  (bind₁ fun i ↦ (rename fun i_1 ↦ (i, i_1)) ((expand p) (W_ (ZMod (p ^ (n + 1))) n)))
      ((map (Int.castRingHom (ZMod (p ^ (n + 1))))) Φ) =
    (map (Int.castRingHom (ZMod (p ^ (n + 1))))) ((bind₁ fun i ↦ (expand p) (wittStructureInt p Φ i)) (W_ ℤ n))
⊢ (bind₁ fun i ↦ (map (Int.castRingHom (ZMod (p ^ (n + 1))))) ((rename fun i_1 ↦ (i, i_1)) (W_ ℤ (n + 1))))
      ((map (Int.castRingHom (ZMod (p ^ (n + 1))))) Φ) =
    (map (Int.castRingHom (ZMod (p ^ (n + 1)))))
      (∑ i ∈ Finset.range (n + 1), C (↑p ^ i) * wittStructureInt p Φ i ^ p ^ (n + 1 - i))
Module: Mathlib.RingTheory.WittVector.WittPolynomial

Goal state before:
pp: case ind.e_a
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Invertible ↑p
n : ℕ
H : ∀ m < n, (bind₁ (W_ R)) (xInTermsOfW p R m) = X m
⊢ ∑ x ∈ range n, C (↑p ^ x) * X x ^ p ^ (n - x) =
    ∑ x ∈ range n, (bind₁ (W_ R)) (C (↑p ^ x) * xInTermsOfW p R x ^ p ^ (n - x))

Tactic:
]

Goal state after:
case ind.e_a
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Invertible ↑p
n : ℕ
H : ∀ m < n, (bind₁ (W_ R)) (xInTermsOfW p R m) = X m
⊢ ∑ x ∈ range n, C (↑p ^ x) * X x ^ p ^ (n - x) =
    ∑ x ∈ range n, (bind₁ (W_ R)) (C (↑p ^ x) * xInTermsOfW p R x ^ p ^ (n - x))
Module: Mathlib.RingTheory.WittVector.WittPolynomial

Goal state before:
pp: case ind.e_a
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Invertible ↑p
n : ℕ
H : ∀ m < n, (bind₁ (W_ R)) (xInTermsOfW p R m) = X m
i : ℕ
h : i < n
⊢ C (↑p ^ i) * X i ^ p ^ (n - i) = (bind₁ (W_ R)) (C (↑p ^ i) * xInTermsOfW p R i ^ p ^ (n - i))

Tactic:
]

Goal state after:
case ind.e_a
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Invertible ↑p
n : ℕ
H : ∀ m < n, (bind₁ (W_ R)) (xInTermsOfW p R m) = X m
i : ℕ
h : i < n
⊢ C (↑p ^ i) * X i ^ p ^ (n - i) = (bind₁ (W_ R)) (C (↑p ^ i) * xInTermsOfW p R i ^ p ^ (n - i))
Module: Mathlib.RingTheory.WittVector.Basic

Goal state before:
pp: p : ℕ
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
α : Type u_3
β : Type u_4
inst✝ : Invertible ↑p
x : ℕ → R
n : ℕ
⊢ ((fun x ↦ mk p fun n ↦ (aeval x) (xInTermsOfW p R n)) x).ghostFun n = x n

Tactic:
have := bind₁_xInTermsOfW_wittPolynomial p R n

Goal state after:
p : ℕ
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
α : Type u_3
β : Type u_4
inst✝ : Invertible ↑p
x : ℕ → R
n : ℕ
this : (bind₁ (xInTermsOfW p R)) (W_ R n) = X n
⊢ ((fun x ↦ mk p fun n ↦ (aeval x) (xInTermsOfW p R n)) x).ghostFun n = x n
Module: Mathlib.RingTheory.WittVector.StructurePolynomial

Goal state before:
pp: case succ
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
key :
  (bind₁ fun i ↦ (rename fun i_1 ↦ (i, i_1)) ((expand p) (W_ (ZMod (p ^ (n + 1))) n)))
      ((map (Int.castRingHom (ZMod (p ^ (n + 1))))) Φ) =
    (map (Int.castRingHom (ZMod (p ^ (n + 1))))) ((bind₁ fun i ↦ (expand p) (wittStructureInt p Φ i)) (W_ ℤ n))
⊢ (map (Int.castRingHom (ZMod (p ^ (n + 1))))) ((bind₁ fun i ↦ (expand p) (wittStructureInt p Φ i)) (W_ ℤ n)) =
    (map (Int.castRingHom (ZMod (p ^ (n + 1)))))
      (∑ i ∈ Finset.range (n + 1), C (↑p ^ i) * wittStructureInt p Φ i ^ p ^ (n + 1 - i))

Tactic:
]

Goal state after:
case succ
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
key :
  (bind₁ fun i ↦ (rename fun i_1 ↦ (i, i_1)) ((expand p) (W_ (ZMod (p ^ (n + 1))) n)))
      ((map (Int.castRingHom (ZMod (p ^ (n + 1))))) Φ) =
    (map (Int.castRingHom (ZMod (p ^ (n + 1))))) ((bind₁ fun i ↦ (expand p) (wittStructureInt p Φ i)) (W_ ℤ n))
⊢ (map (Int.castRingHom (ZMod (p ^ (n + 1))))) ((bind₁ fun i ↦ (expand p) (wittStructureInt p Φ i)) (W_ ℤ n)) =
    (map (Int.castRingHom (ZMod (p ^ (n + 1)))))
      (∑ i ∈ Finset.range (n + 1), C (↑p ^ i) * wittStructureInt p Φ i ^ p ^ (n + 1 - i))
Module: Mathlib.RingTheory.WittVector.WittPolynomial

Goal state before:
pp: case ind.e_a
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Invertible ↑p
n : ℕ
H : ∀ m < n, (bind₁ (W_ R)) (xInTermsOfW p R m) = X m
i : ℕ
h : i < n
⊢ C (↑p ^ i) * X i ^ p ^ (n - i) = C (↑p ^ i) * X i ^ p ^ (n - i)

Tactic:
]

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

Goal state before:
pp: p : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Fact (Nat.Prime p)
x : 𝕎 R
n : ℕ
hx : ∀ i ≤ n, ↑p ∣ x.coeff i
⊢ ↑p ^ (n + 1) ∣ ∑ i ∈ Finset.range (n + 1), (aeval x.coeff) ((monomial (Finsupp.single i (p ^ (n - i)))) (↑p ^ i))

Tactic:
]

Goal state after:
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Fact (Nat.Prime p)
x : 𝕎 R
n : ℕ
hx : ∀ i ≤ n, ↑p ∣ x.coeff i
⊢ ↑p ^ (n + 1) ∣ ∑ i ∈ Finset.range (n + 1), (aeval x.coeff) ((monomial (Finsupp.single i (p ^ (n - i)))) (↑p ^ i))
Module: Mathlib.RingTheory.WittVector.Basic

Goal state before:
pp: p : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Fact (Nat.Prime p)
x : 𝕎 R
n : ℕ
hx : ∀ i ≤ n, ↑p ∣ x.coeff i
i : ℕ
hi : i < n + 1
this : (aeval x.coeff) ((monomial (Finsupp.single i (p ^ (n - i)))) (↑p ^ i)) = ↑p ^ i * x.coeff i ^ p ^ (n - i)
⊢ ↑p ^ i * ↑p ^ (n - i + 1) ∣ ↑p ^ i * x.coeff i ^ p ^ (n - i)

Tactic:
]

Goal state after:
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Fact (Nat.Prime p)
x : 𝕎 R
n : ℕ
hx : ∀ i ≤ n, ↑p ∣ x.coeff i
i : ℕ
hi : i < n + 1
this : (aeval x.coeff) ((monomial (Finsupp.single i (p ^ (n - i)))) (↑p ^ i)) = ↑p ^ i * x.coeff i ^ p ^ (n - i)
⊢ ↑p ^ i * ↑p ^ (n - i + 1) ∣ ↑p ^ i * x.coeff i ^ p ^ (n - i)
Module: Mathlib.RingTheory.WittVector.StructurePolynomial

Goal state before:
pp: case succ
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n : ℕ
⊢ (Finset.range (n + 1)).sum ?m.282 =
    ∑ x ∈ Finset.range (n + 1),
      (map (Int.castRingHom (ZMod (p ^ (n + 1))))) (C (↑p ^ x) * wittStructureInt p Φ x ^ p ^ (n + 1 - x))

pp: case succ
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n : ℕ
⊢ ∀ x ∈ Finset.range (n + 1),
    (map (Int.castRingHom (ZMod (p ^ (n + 1))))) (↑p ^ x * (expand p) (wittStructureInt p Φ x) ^ p ^ (n - x)) = ?m.282 x

pp: p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n : ℕ
⊢ ℕ → MvPolynomial (idx × ℕ) (ZMod (p ^ (n + 1)))

Tactic:
]

Goal state after:
case succ
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n : ℕ
⊢ ∀ x ∈ Finset.range (n + 1),
    (map (Int.castRingHom (ZMod (p ^ (n + 1))))) (↑p ^ x * (expand p) (wittStructureInt p Φ x) ^ p ^ (n - x)) =
      (map (Int.castRingHom (ZMod (p ^ (n + 1))))) (C (↑p ^ x) * wittStructureInt p Φ x ^ p ^ (n + 1 - x))
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
⊢ (map (Int.castRingHom (ZMod (p ^ (n + 1))))) (↑p ^ k * (expand p) (wittStructureInt p Φ k) ^ p ^ (n - k)) =
    (map (Int.castRingHom (ZMod (p ^ (n + 1))))) (C (↑p ^ k) * wittStructureInt p Φ k ^ p ^ (n + 1 - k))

Tactic:
]

Goal state after:
case succ
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n k : ℕ
hk : k ≤ n
⊢ (map (Int.castRingHom (ZMod (p ^ (n + 1))))) (↑p ^ k * (expand p) (wittStructureInt p Φ k) ^ p ^ (n - k)) =
    (map (Int.castRingHom (ZMod (p ^ (n + 1))))) (C (↑p ^ k) * wittStructureInt p Φ k ^ p ^ (n + 1 - 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
⊢ ↑(p ^ (n + 1)) ∣
    ↑(p ^ k) * ((expand p) (wittStructureInt p Φ k) ^ p ^ (n - k) - wittStructureInt p Φ k ^ p ^ (n + 1 - k))

Tactic:
]

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

Goal state before:
pp: p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n k : ℕ
hk : k ≤ n
⊢ p ^ (n + 1) = p ^ (k + (n - k) + 1)

Tactic:
]

Goal state after:
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n k : ℕ
hk : k ≤ n
⊢ p ^ (n + 1) = p ^ (k + (n - k) + 1)
Module: Mathlib.RingTheory.WittVector.StructurePolynomial

Goal state before:
pp: case e_a.e_a
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n k : ℕ
hk : k ≤ n
⊢ n - k = n - k

Tactic:
]

Goal state after:
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 ^ k * p ^ (n - k + 1)) ∣
    ↑(p ^ k) * ((expand p) (wittStructureInt p Φ k) ^ p ^ (n - k) - wittStructureInt p Φ k ^ p ^ (n + 1 - k))

Tactic:
]

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.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 ^ k * ↑p ^ (n - k + 1) ∣
    ↑p ^ k * ((expand p) (wittStructureInt p Φ k) ^ p ^ (n - k) - wittStructureInt p Φ k ^ p ^ (n + 1 - k))

Tactic:
]

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.WittVector.StructurePolynomial

Goal state before:
pp: 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 - k + 1) = p ^ (n - k + 1)

Tactic:
]

Goal state after: