mathlib-initiative/mathlib-tactics huggingface dataset:
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:
simpa using

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.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
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 i ↦ ‖f i‖ * |C| i) cofinite (𝓝 0)

Tactic:
simpa using

Goal state after:
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 i ↦ ‖f i‖ * |C i|) cofinite (𝓝 0)
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
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 i ↦ ‖g i‖ * |C| i) cofinite (𝓝 0)

Tactic:
simpa using

Goal state after:
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 i ↦ ‖g i‖ * |C i|) cofinite (𝓝 0)
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) →₀ ℕ
⊢ (T1 f (-1)).comp (T1 f 1) = AlgHom.id k (MvPolynomial (Fin (n + 1)) k)

Tactic:
simpa using

Goal state after:
k : Type u_1
inst✝ : Field k
n : ℕ
f : MvPolynomial (Fin (n + 1)) k
v w : Fin (n + 1) →₀ ℕ
⊢ (bind₁ fun i ↦ if i = 0 then MvPolynomial.X 0 else MvPolynomial.X i + -MvPolynomial.X 0 ^ up ^ ↑i).comp
      (bind₁ fun i ↦ if i = 0 then MvPolynomial.X 0 else MvPolynomial.X i + MvPolynomial.X 0 ^ up ^ ↑i) =
    AlgHom.id k (MvPolynomial (Fin (n + 1)) k)
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:
simpa using

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
⊢ ∑ x, v x.succ * (Polynomial.C (MvPolynomial.X x) + Polynomial.X ^ up ^ ↑x.succ).natDegree =
    ∑ i, up ^ ↑i.succ * v i.succ
Module: Mathlib.RingTheory.WittVector.WittPolynomial

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

Tactic:
by
  simp only [wittPolynomial, map_sum, constantCoeff_monomial]
  rw [sum_eq_zero]
  rintro i _
  rw [if_neg]
  rw [Finsupp.single_eq_zero]
  exact ne_of_gt (pow_pos hp.1.pos _)

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,
    ((MvPolynomial.finSuccEquiv k n) ((T f) ((MvPolynomial.monomial x') (MvPolynomial.coeff x' f)))).natDegree ≤
      ((MvPolynomial.finSuccEquiv k n) ((T f) ((MvPolynomial.monomial v) (MvPolynomial.coeff v f)))).natDegree
x : Fin (n + 1) →₀ ℕ
hx : x ∈ f.support \ {v}
h1 : x ∈ f.support
h2 : x ∉ {v}
⊢ ((MvPolynomial.finSuccEquiv k n) ((T f) ((MvPolynomial.monomial x) (MvPolynomial.coeff x f)))).natDegree ≠
    ((MvPolynomial.finSuccEquiv k n) ((T f) ((MvPolynomial.monomial v) (MvPolynomial.coeff v f)))).natDegree

Tactic:
simpa using

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,
    ((MvPolynomial.finSuccEquiv k n) ((T f) ((MvPolynomial.monomial x') (MvPolynomial.coeff x' f)))).natDegree ≤
      ((MvPolynomial.finSuccEquiv k n) ((T f) ((MvPolynomial.monomial v) (MvPolynomial.coeff v f)))).natDegree
x : Fin (n + 1) →₀ ℕ
hx : x ∈ f.support \ {v}
h1 : x ∈ f.support
h2 : x ∉ {v}
⊢ degreeOf 0 ((T f) ((MvPolynomial.monomial x) (MvPolynomial.coeff x f))) ≠
    degreeOf 0 ((T f) ((MvPolynomial.monomial v) (MvPolynomial.coeff v f)))
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
⊢ h v ≠ 0

Tactic:
simpa using

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
⊢ ¬MvPolynomial.coeff v f = 0
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:
simpa using

Goal state after:
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]
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:
simpa using

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

Tactic:
simpa using

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.C (MvPolynomial.coeff v f))
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:
have := teichmuller_sModEq <| Ideal.Quotient.mk_out <| coeff _ p 0 x

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

Tactic:
simpa using

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]
⊢ (Ideal.Quotient.mk I) ((teichmuller₀ p I) x) = (coeff (R ⧸ I) p 0) x
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
      rw [← Ideal.map_map, Ideal.map_coe, Ideal.map_coe]
      exact congrArg _ rfl

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 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:
simp only [C_pow, bind₁_X_right, sub_add_cancel]

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

Goal state before:
pp: case refine_1
p : ℕ
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Fact (Nat.Prime p)
f : R →+* S
x : 𝕎 R
n : ℕ
h : ((map f) x).coeff n = coeff 0 n
⊢ f (x.coeff n) = 0

Tactic:
simpa using

Goal state after:
case refine_1
p : ℕ
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Fact (Nat.Prime p)
f : R →+* S
x : 𝕎 R
n : ℕ
h : ((map f) x).coeff n = coeff 0 n
⊢ f (x.coeff n) = 0
Module: Mathlib.RingTheory.WittVector.Basic

Goal state before:
pp: case refine_2
p : ℕ
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Fact (Nat.Prime p)
f : R →+* S
x : 𝕎 R
h : ∀ (n : ℕ), f (x.coeff n) = 0
n : ℕ
⊢ ((map f) x).coeff n = coeff 0 n

Tactic:
simpa using

Goal state after:
case refine_2
p : ℕ
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Fact (Nat.Prime p)
f : R →+* S
x : 𝕎 R
h : ∀ (n : ℕ), f (x.coeff n) = 0
n : ℕ
⊢ f (x.coeff n) = 0
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, (map (Int.castRingHom ℚ)) (wittStructureInt p Φ m) = wittStructureRat p ((map (Int.castRingHom ℚ)) Φ) m
⊢ C ↑(p ^ n) ∣
    (bind₁ fun b ↦ (rename fun i ↦ (b, i)) (W_ ℤ n)) Φ -
      ∑ i ∈ Finset.range n, C (↑p ^ i) * wittStructureInt p Φ i ^ p ^ (n - i)

Tactic:
by
  rcases n with - | n
  · simp
  -- prepare a useful equation for rewriting
  have key := bind₁_rename_expand_wittPolynomial Φ n IH
  apply_fun map (Int.castRingHom (ZMod (p ^ (n + 1)))) at key
  conv_lhs at key => simp only [map_bind₁, map_rename, map_expand, map_wittPolynomial]
  -- clean up and massage
  rw [C_dvd_iff_zmod, map_sub, sub_eq_zero, map_bind₁]
  simp only [map_rename, map_wittPolynomial, wittPolynomial_zmod_self]
  rw [key]; clear key IH
  rw [bind₁, aeval_wittPolynomial, map_sum, map_sum, Finset.sum_congr rfl]
  intro k hk
  rw [Finset.mem_range, Nat.lt_succ_iff] at hk
  rw [← sub_eq_zero, ← map_sub, ← C_dvd_iff_zmod, C_eq_coe_nat, ← Nat.cast_pow,
    ← Nat.cast_pow, C_eq_coe_nat, ← mul_sub]
  have : p ^ (n + 1) = p ^ k * p ^ (n - k + 1) := by
    rw [← pow_add, ← add_assoc]; congr 2; rw [add_comm, ← tsub_eq_iff_eq_add_of_le hk]
  rw [this]
  rw [Nat.cast_mul, Nat.cast_pow, Nat.cast_pow]
  apply mul_dvd_mul_left ((p : MvPolynomial (idx × ℕ) ℤ) ^ k)
  rw [show p ^ (n + 1 - k) = p * p ^ (n - k) by rw [← pow_succ', ← tsub_add_eq_add_tsub hk]]
  rw [pow_mul]
  -- the machine!
  apply dvd_sub_pow_of_dvd_sub
  rw [← C_eq_coe_nat, C_dvd_iff_zmod, map_sub, sub_eq_zero, map_expand, map_pow,
    MvPolynomial.expand_zmod]

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

Goal state before:
pp: p : ℕ
idx : Type u_1
inst✝ : Fact (Nat.Prime p)
f g : ℕ → MvPolynomial (idx × ℕ) ℤ
n : ℕ
h :
  (bind₁ (⇑(MvPolynomial.map (Int.castRingHom ℚ)) ∘ fun n ↦ (bind₁ f) (wittPolynomial p ℤ n))) (xInTermsOfW p ℚ n) =
    (bind₁ (⇑(MvPolynomial.map (Int.castRingHom ℚ)) ∘ fun n ↦ (bind₁ g) (wittPolynomial p ℤ n))) (xInTermsOfW p ℚ n)
⊢ (MvPolynomial.map (Int.castRingHom ℚ)) (f n) = (MvPolynomial.map (Int.castRingHom ℚ)) (g n)

Tactic:
simpa using

Goal state after:
p : ℕ
idx : Type u_1
inst✝ : Fact (Nat.Prime p)
f g : ℕ → MvPolynomial (idx × ℕ) ℤ
n : ℕ
h :
  (bind₁ (⇑(MvPolynomial.map (Int.castRingHom ℚ)) ∘ fun n ↦ (bind₁ f) (wittPolynomial p ℤ n))) (xInTermsOfW p ℚ n) =
    (bind₁ (⇑(MvPolynomial.map (Int.castRingHom ℚ)) ∘ fun n ↦ (bind₁ g) (wittPolynomial p ℤ n))) (xInTermsOfW p ℚ n)
⊢ (MvPolynomial.map (Int.castRingHom ℚ)) (f n) = (MvPolynomial.map (Int.castRingHom ℚ)) (g n)
Module: Mathlib.RingTheory.WittVector.IsPoly

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
f g : ℕ → MvPolynomial ℕ ℤ
n : ℕ
h :
  (bind₁ (⇑(MvPolynomial.map (Int.castRingHom ℚ)) ∘ fun n ↦ (bind₁ f) (wittPolynomial p ℤ n))) (xInTermsOfW p ℚ n) =
    (bind₁ (⇑(MvPolynomial.map (Int.castRingHom ℚ)) ∘ fun n ↦ (bind₁ g) (wittPolynomial p ℤ n))) (xInTermsOfW p ℚ n)
⊢ (MvPolynomial.map (Int.castRingHom ℚ)) (f n) = (MvPolynomial.map (Int.castRingHom ℚ)) (g n)

Tactic:
simpa using

Goal state after:
p : ℕ
inst✝ : Fact (Nat.Prime p)
f g : ℕ → MvPolynomial ℕ ℤ
n : ℕ
h :
  (bind₁ (⇑(MvPolynomial.map (Int.castRingHom ℚ)) ∘ fun n ↦ (bind₁ f) (wittPolynomial p ℤ n))) (xInTermsOfW p ℚ n) =
    (bind₁ (⇑(MvPolynomial.map (Int.castRingHom ℚ)) ∘ fun n ↦ (bind₁ g) (wittPolynomial p ℤ n))) (xInTermsOfW p ℚ n)
⊢ (MvPolynomial.map (Int.castRingHom ℚ)) (f n) = (MvPolynomial.map (Int.castRingHom ℚ)) (g n)
Module: Mathlib.RingTheory.Perfection

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
p : ℕ
f : Perfection M p
n m : ℕ
⊢ (coeffMonoidHom M p n) ((⇑(powMulEquiv (Perfection M p) p).symm)^[m] f) = (coeffMonoidHom M p (n + m)) f

Tactic:
induction m generalizing n with

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

Goal state before:
pp: case py₁
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
φ : ℕ → MvPolynomial (idx × ℕ) ℤ
n : ℕ
h :
  (map (Int.castRingHom ℚ)) ((bind₁ φ) (W_ ℤ n)) =
    (map (Int.castRingHom ℚ)) ((bind₁ fun i ↦ (rename (Prod.mk i)) (W_ ℤ n)) Φ)
⊢ (bind₁ fun k ↦ (map (Int.castRingHom ℚ)) (φ k)) (W_ ℚ n) =
    (bind₁ fun i ↦ (rename (Prod.mk i)) (W_ ℚ n)) ((map (Int.castRingHom ℚ)) Φ)

Tactic:
simpa using

Goal state after:
case py₁
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
φ : ℕ → MvPolynomial (idx × ℕ) ℤ
n : ℕ
h :
  (map (Int.castRingHom ℚ)) ((bind₁ φ) (W_ ℤ n)) =
    (map (Int.castRingHom ℚ)) ((bind₁ fun i ↦ (rename (Prod.mk i)) (W_ ℤ n)) Φ)
⊢ (bind₁ fun k ↦ (map (Int.castRingHom ℚ)) (φ k)) (W_ ℚ n) =
    (bind₁ fun i ↦ (rename (Prod.mk i)) (W_ ℚ n)) ((map (Int.castRingHom ℚ)) Φ)
Module: Mathlib.RingTheory.Perfection

Goal state before:
pp: R : Type u_1
inst✝¹ : CommSemiring R
p : ℕ
hp : Fact (Nat.Prime p)
inst✝ : CharP R p
x✝ : Perfection R p
⊢ (pthRoot R p) x✝ = ↑(frobeniusEquiv (Perfection R p) p).symm x✝

Tactic:
simpa using

Goal state after:
R : Type u_1
inst✝¹ : CommSemiring R
p : ℕ
hp : Fact (Nat.Prime p)
inst✝ : CharP R p
x✝ : Perfection R p
⊢ (frobenius (Perfection R p) p) ((pthRoot R p) x✝) = x✝
Module: Mathlib.RingTheory.WittVector.Identities

Goal state before:
pp: case pos
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CharP R p
i : ℕ
hi : i = 1
⊢ (↑p).coeff i = 1

Tactic:
simpa using

Goal state after:
case pos
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CharP R p
i : ℕ
hi : i = 1
⊢ (↑p).coeff 1 = 1
Module: Mathlib.RingTheory.WittVector.Identities

Goal state before:
pp: case neg
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CharP R p
i : ℕ
hi : ¬i = 1
⊢ (↑p).coeff i = 0

Tactic:
simpa using

Goal state after:
case neg
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CharP R p
i : ℕ
hi : ¬i = 1
⊢ (↑p).coeff i = 0
Module: Mathlib.RingTheory.WittVector.Identities

Goal state before:
pp: p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝² : CommRing R
inst✝¹ : Nontrivial R
inst✝ : CharP R p
h : ↑p = 0
⊢ False

Tactic:
simpa using

Goal state after:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝² : CommRing R
inst✝¹ : Nontrivial R
inst✝ : CharP R p
h : ↑p = 0
⊢ False
Module: Mathlib.RingTheory.WittVector.Identities

Goal state before:
pp: p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝² : CommRing R
inst✝¹ : Nontrivial R
inst✝ : CharP R p
⊢ ↑p ≠ 0

Tactic:
simpa using

Goal state after:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝² : CommRing R
inst✝¹ : Nontrivial R
inst✝ : CharP R p
⊢ ¬↑p = 0
Module: Mathlib.RingTheory.WittVector.Identities

Goal state before:
pp: case succ.succ
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CharP R p
x : 𝕎 R
n : ℕ
ih : ∀ {m : ℕ}, m < n → (x * ↑p ^ n).coeff m = 0
m' : ℕ
h : m' + 1 < n + 1
⊢ m' < n

Tactic:
simpa using

Goal state after:
case succ.succ
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CharP R p
x : 𝕎 R
n : ℕ
ih : ∀ {m : ℕ}, m < n → (x * ↑p ^ n).coeff m = 0
m' : ℕ
h : m' + 1 < n + 1
⊢ m' < n
Module: Mathlib.RingTheory.WittVector.Identities

Goal state before:
pp: case succ.succ
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
x : 𝕎 R
n : ℕ
ih : ∀ {m : ℕ}, m < n → ((⇑verschiebung)^[n] x).coeff m = 0
m' : ℕ
h : m' + 1 < n + 1
⊢ m' < n

Tactic:
simpa using

Goal state after:
case succ.succ
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
x : 𝕎 R
n : ℕ
ih : ∀ {m : ℕ}, m < n → ((⇑verschiebung)^[n] x).coeff m = 0
m' : ℕ
h : m' + 1 < n + 1
⊢ m' < n
Module: Mathlib.RingTheory.WittVector.IsPoly

Goal state before:
pp: p : ℕ
R S : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Fact (Nat.Prime p)
f : ⦃R : Type u⦄ → [CommRing R] → 𝕎 R → 𝕎 R → 𝕎 R
hf : IsPoly₂ p f
g : R →+* S
x y : 𝕎 R
⊢ (WittVector.map g) (f x y) = f ((WittVector.map g) x) ((WittVector.map g) y)

Tactic:
obtain ⟨φ, hf⟩ := hf
  ext n
  simp +unfoldPartialApp only [map_coeff, hf, map_aeval, peval, uncurry]
  apply eval₂Hom_congr (RingHom.ext_int _ _) _ rfl
  ext ⟨i, k⟩
  fin_cases i <;> simp

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

Goal state before:
pp: p n : ℕ
R : Type u_1
inst✝ : CommRing R
x y : TruncatedWittVector p n R
h : ∀ (n_1 : ℕ), x.out.coeff n_1 = y.out.coeff n_1
i : Fin n
⊢ coeff i x = coeff i y

Tactic:
simpa using

Goal state after:
p n : ℕ
R : Type u_1
inst✝ : CommRing R
x y : TruncatedWittVector p n R
h : ∀ (n_1 : ℕ), x.out.coeff n_1 = y.out.coeff n_1
i : Fin n
⊢ coeff i x = coeff i y
Module: Mathlib.RingTheory.WittVector.Complete

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : CommRing k
inst✝¹ : CharP k p
inst✝ : PerfectRing k p
x : 𝕎 k
h : x.coeff 0 = 0
⊢ x = verschiebung (x.shift 1)

Tactic:
simpa using

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : CommRing k
inst✝¹ : CharP k p
inst✝ : PerfectRing k p
x : 𝕎 k
h : x.coeff 0 = 0
⊢ x = verschiebung (x.shift 1)
Module: Mathlib.RingTheory.WittVector.Complete

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : CommRing k
inst✝¹ : CharP k p
inst✝ : PerfectRing k p
x : 𝕎 k
n : ℕ
h : ∀ m < n, x.coeff m = 0
⊢ x = (⇑verschiebung)^[n] (x.shift n)

Tactic:
simpa using

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : CommRing k
inst✝¹ : CharP k p
inst✝ : PerfectRing k p
x : 𝕎 k
n : ℕ
h : ∀ m < n, x.coeff m = 0
⊢ x = (⇑verschiebung)^[n] (x.shift n)