[GOAL]
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
x : 𝕎 R
⊢ ↑frobenius (↑verschiebung x) = x * ↑p
[PROOFSTEP]
simp only []
[GOAL]
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
x : 𝕎 R
⊢ ↑frobenius (↑verschiebung x) = x * ↑p
[PROOFSTEP]
have : IsPoly p fun {R} [CommRing R] x ↦ frobenius (verschiebung x) :=
  IsPoly.comp (hg := frobenius_isPoly p) (hf := verschiebung_isPoly)
[GOAL]
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
x : 𝕎 R
this : IsPoly p fun {R} [CommRing R] x => ↑frobenius (↑verschiebung x)
⊢ ↑frobenius (↑verschiebung x) = x * ↑p
[PROOFSTEP]
have : IsPoly p fun {R} [CommRing R] x ↦ x * p := mulN_isPoly p p
[GOAL]
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
x : 𝕎 R
this✝ : IsPoly p fun {R} [CommRing R] x => ↑frobenius (↑verschiebung x)
this : IsPoly p fun {R} [CommRing R] x => x * ↑p
⊢ ↑frobenius (↑verschiebung x) = x * ↑p
[PROOFSTEP]
ghost_calc x
[GOAL]
case refine_3
p : ℕ
hp : Fact (Nat.Prime p)
this✝ : IsPoly p fun {R} [CommRing R] x => ↑frobenius (↑verschiebung x)
this : IsPoly p fun {R} [CommRing R] x => x * ↑p
R : Type u_1
R._inst : CommRing R
x : 𝕎 R
⊢ ∀ (n : ℕ), ↑(ghostComponent n) (↑frobenius (↑verschiebung x)) = ↑(ghostComponent n) (x * ↑p)
[PROOFSTEP]
ghost_simp [mul_comm]
[GOAL]
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
x : 𝕎 (ZMod p)
⊢ ↑verschiebung x = x * ↑p
[PROOFSTEP]
rw [← frobenius_verschiebung, frobenius_zmodp]
[GOAL]
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CharP R p
i : ℕ
⊢ coeff (↑p ^ i) i = 1
[PROOFSTEP]
induction' i with i h
[GOAL]
case zero
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CharP R p
⊢ coeff (↑p ^ Nat.zero) Nat.zero = 1
[PROOFSTEP]
simp only [Nat.zero_eq, one_coeff_zero, Ne.def, pow_zero]
[GOAL]
case succ
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CharP R p
i : ℕ
h : coeff (↑p ^ i) i = 1
⊢ coeff (↑p ^ Nat.succ i) (Nat.succ i) = 1
[PROOFSTEP]
rw [pow_succ', ← frobenius_verschiebung, coeff_frobenius_charP, verschiebung_coeff_succ, h, one_pow]
[GOAL]
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CharP R p
i j : ℕ
hj : j ≠ i
⊢ coeff (↑p ^ i) j = 0
[PROOFSTEP]
induction' i with i hi generalizing j
[GOAL]
case zero
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CharP R p
i j✝ : ℕ
hj✝ : j✝ ≠ i
j : ℕ
hj : j ≠ Nat.zero
⊢ coeff (↑p ^ Nat.zero) j = 0
[PROOFSTEP]
rw [Nat.zero_eq, pow_zero, one_coeff_eq_of_pos]
[GOAL]
case zero.hn
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CharP R p
i j✝ : ℕ
hj✝ : j✝ ≠ i
j : ℕ
hj : j ≠ Nat.zero
⊢ 0 < j
[PROOFSTEP]
exact Nat.pos_of_ne_zero hj
[GOAL]
case succ
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CharP R p
i✝ j✝ : ℕ
hj✝ : j✝ ≠ i✝
i : ℕ
hi : ∀ {j : ℕ}, j ≠ i → coeff (↑p ^ i) j = 0
j : ℕ
hj : j ≠ Nat.succ i
⊢ coeff (↑p ^ Nat.succ i) j = 0
[PROOFSTEP]
rw [pow_succ', ← frobenius_verschiebung, coeff_frobenius_charP]
[GOAL]
case succ
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CharP R p
i✝ j✝ : ℕ
hj✝ : j✝ ≠ i✝
i : ℕ
hi : ∀ {j : ℕ}, j ≠ i → coeff (↑p ^ i) j = 0
j : ℕ
hj : j ≠ Nat.succ i
⊢ coeff (↑verschiebung (↑p ^ i)) j ^ p = 0
[PROOFSTEP]
cases j
[GOAL]
case succ.zero
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CharP R p
i✝ j : ℕ
hj✝ : j ≠ i✝
i : ℕ
hi : ∀ {j : ℕ}, j ≠ i → coeff (↑p ^ i) j = 0
hj : Nat.zero ≠ Nat.succ i
⊢ coeff (↑verschiebung (↑p ^ i)) Nat.zero ^ p = 0
[PROOFSTEP]
rw [verschiebung_coeff_zero, zero_pow]
[GOAL]
case succ.zero
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CharP R p
i✝ j : ℕ
hj✝ : j ≠ i✝
i : ℕ
hi : ∀ {j : ℕ}, j ≠ i → coeff (↑p ^ i) j = 0
hj : Nat.zero ≠ Nat.succ i
⊢ 0 < p
[PROOFSTEP]
exact Nat.Prime.pos hp.out
[GOAL]
case succ.succ
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CharP R p
i✝ j : ℕ
hj✝ : j ≠ i✝
i : ℕ
hi : ∀ {j : ℕ}, j ≠ i → coeff (↑p ^ i) j = 0
n✝ : ℕ
hj : Nat.succ n✝ ≠ Nat.succ i
⊢ coeff (↑verschiebung (↑p ^ i)) (Nat.succ n✝) ^ p = 0
[PROOFSTEP]
rw [verschiebung_coeff_succ, hi, zero_pow]
[GOAL]
case succ.succ
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CharP R p
i✝ j : ℕ
hj✝ : j ≠ i✝
i : ℕ
hi : ∀ {j : ℕ}, j ≠ i → coeff (↑p ^ i) j = 0
n✝ : ℕ
hj : Nat.succ n✝ ≠ Nat.succ i
⊢ 0 < p
[PROOFSTEP]
exact Nat.Prime.pos hp.out
[GOAL]
case succ.succ
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CharP R p
i✝ j : ℕ
hj✝ : j ≠ i✝
i : ℕ
hi : ∀ {j : ℕ}, j ≠ i → coeff (↑p ^ i) j = 0
n✝ : ℕ
hj : Nat.succ n✝ ≠ Nat.succ i
⊢ n✝ ≠ i
[PROOFSTEP]
exact ne_of_apply_ne (fun j : ℕ => j.succ) hj
[GOAL]
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CharP R p
i : ℕ
⊢ coeff (↑p) i = if i = 1 then 1 else 0
[PROOFSTEP]
split_ifs with hi
[GOAL]
case pos
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CharP R p
i : ℕ
hi : i = 1
⊢ coeff (↑p) i = 1
[PROOFSTEP]
simpa only [hi, pow_one] using coeff_p_pow p R 1
[GOAL]
case neg
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CharP R p
i : ℕ
hi : ¬i = 1
⊢ coeff (↑p) i = 0
[PROOFSTEP]
simpa only [pow_one] using coeff_p_pow_eq_zero p R hi
[GOAL]
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CharP R p
⊢ coeff (↑p) 0 = 0
[PROOFSTEP]
rw [coeff_p, if_neg]
[GOAL]
case hnc
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CharP R p
⊢ ¬0 = 1
[PROOFSTEP]
exact zero_ne_one
[GOAL]
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CharP R p
⊢ coeff (↑p) 1 = 1
[PROOFSTEP]
rw [coeff_p, if_pos rfl]
[GOAL]
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝² : CommRing R
inst✝¹ : Nontrivial R
inst✝ : CharP R p
⊢ ↑p ≠ 0
[PROOFSTEP]
intro h
[GOAL]
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝² : CommRing R
inst✝¹ : Nontrivial R
inst✝ : CharP R p
h : ↑p = 0
⊢ False
[PROOFSTEP]
simpa only [h, zero_coeff, zero_ne_one] using coeff_p_one p R
[GOAL]
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝² : CommRing R
inst✝¹ : Nontrivial R
inst✝ : CharP R p
⊢ ↑p ≠ 0
[PROOFSTEP]
simpa using (IsFractionRing.injective (𝕎 R) (FractionRing (𝕎 R))).ne (WittVector.p_nonzero _ _)
[GOAL]
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
x y : 𝕎 R
⊢ ↑verschiebung (x * ↑frobenius y) = ↑verschiebung x * y
[PROOFSTEP]
simp only []
[GOAL]
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
x y : 𝕎 R
⊢ ↑verschiebung (x * ↑frobenius y) = ↑verschiebung x * y
[PROOFSTEP]
have : IsPoly₂ p fun {R} [Rcr : CommRing R] x y ↦ verschiebung (x * frobenius y) :=
  IsPoly.comp₂ (hg := verschiebung_isPoly) (hf :=
    IsPoly₂.comp (hh := mulIsPoly₂) (hf := idIsPolyI' p) (hg := frobenius_isPoly p))
[GOAL]
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
x y : 𝕎 R
this : IsPoly₂ p fun {R} [CommRing R] x y => ↑verschiebung (x * ↑frobenius y)
⊢ ↑verschiebung (x * ↑frobenius y) = ↑verschiebung x * y
[PROOFSTEP]
have : IsPoly₂ p fun {R} [CommRing R] x y ↦ verschiebung x * y :=
  IsPoly₂.comp (hh := mulIsPoly₂) (hf := verschiebung_isPoly) (hg := idIsPolyI' p)
[GOAL]
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
x y : 𝕎 R
this✝ : IsPoly₂ p fun {R} [CommRing R] x y => ↑verschiebung (x * ↑frobenius y)
this : IsPoly₂ p fun {R} [CommRing R] x y => ↑verschiebung x * y
⊢ ↑verschiebung (x * ↑frobenius y) = ↑verschiebung x * y
[PROOFSTEP]
ghost_calc x y
[GOAL]
case refine_3
p : ℕ
hp : Fact (Nat.Prime p)
this✝ : IsPoly₂ p fun {R} [CommRing R] x y => ↑verschiebung (x * ↑frobenius y)
this : IsPoly₂ p fun {R} [CommRing R] x y => ↑verschiebung x * y
R : Type u_1
R._inst : CommRing R
x y : 𝕎 R
⊢ ∀ (n : ℕ), ↑(ghostComponent n) (↑verschiebung (x * ↑frobenius y)) = ↑(ghostComponent n) (↑verschiebung x * y)
[PROOFSTEP]
rintro ⟨⟩
[GOAL]
case refine_3.zero
p : ℕ
hp : Fact (Nat.Prime p)
this✝ : IsPoly₂ p fun {R} [CommRing R] x y => ↑verschiebung (x * ↑frobenius y)
this : IsPoly₂ p fun {R} [CommRing R] x y => ↑verschiebung x * y
R : Type u_1
R._inst : CommRing R
x y : 𝕎 R
⊢ ↑(ghostComponent Nat.zero) (↑verschiebung (x * ↑frobenius y)) = ↑(ghostComponent Nat.zero) (↑verschiebung x * y)
[PROOFSTEP]
ghost_simp [mul_assoc]
[GOAL]
case refine_3.succ
p : ℕ
hp : Fact (Nat.Prime p)
this✝ : IsPoly₂ p fun {R} [CommRing R] x y => ↑verschiebung (x * ↑frobenius y)
this : IsPoly₂ p fun {R} [CommRing R] x y => ↑verschiebung x * y
R : Type u_1
R._inst : CommRing R
x y : 𝕎 R
n✝ : ℕ
⊢ ↑(ghostComponent (Nat.succ n✝)) (↑verschiebung (x * ↑frobenius y)) =
    ↑(ghostComponent (Nat.succ n✝)) (↑verschiebung x * y)
[PROOFSTEP]
ghost_simp [mul_assoc]
[GOAL]
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CharP R p
x : 𝕎 R
⊢ coeff (x * ↑p) 0 = 0
[PROOFSTEP]
rw [← frobenius_verschiebung, coeff_frobenius_charP, verschiebung_coeff_zero, zero_pow]
[GOAL]
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CharP R p
x : 𝕎 R
⊢ 0 < p
[PROOFSTEP]
exact Nat.Prime.pos hp.out
[GOAL]
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CharP R p
x : 𝕎 R
i : ℕ
⊢ coeff (x * ↑p) (i + 1) = coeff x i ^ p
[PROOFSTEP]
rw [← frobenius_verschiebung, coeff_frobenius_charP, verschiebung_coeff_succ]
[GOAL]
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CharP R p
x : 𝕎 R
⊢ ↑verschiebung (↑frobenius x) = x * ↑p
[PROOFSTEP]
ext ⟨i⟩
[GOAL]
case h.zero
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CharP R p
x : 𝕎 R
⊢ coeff (↑verschiebung (↑frobenius x)) Nat.zero = coeff (x * ↑p) Nat.zero
[PROOFSTEP]
rw [mul_charP_coeff_zero, verschiebung_coeff_zero]
[GOAL]
case h.succ
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CharP R p
x : 𝕎 R
n✝ : ℕ
⊢ coeff (↑verschiebung (↑frobenius x)) (Nat.succ n✝) = coeff (x * ↑p) (Nat.succ n✝)
[PROOFSTEP]
rw [mul_charP_coeff_succ, verschiebung_coeff_succ, coeff_frobenius_charP]
[GOAL]
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CharP R p
x : 𝕎 R
⊢ ↑verschiebung (↑frobenius x) = ↑frobenius (↑verschiebung x)
[PROOFSTEP]
rw [verschiebung_frobenius, frobenius_verschiebung]
[GOAL]
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
x : 𝕎 R
n k : ℕ
⊢ coeff ((↑verschiebung)^[n] x) (k + n) = coeff x k
[PROOFSTEP]
induction' n with k ih
[GOAL]
case zero
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
x : 𝕎 R
k : ℕ
⊢ coeff ((↑verschiebung)^[Nat.zero] x) (k + Nat.zero) = coeff x k
[PROOFSTEP]
simp
[GOAL]
case succ
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
x : 𝕎 R
k✝ k : ℕ
ih : coeff ((↑verschiebung)^[k] x) (k✝ + k) = coeff x k✝
⊢ coeff ((↑verschiebung)^[Nat.succ k] x) (k✝ + Nat.succ k) = coeff x k✝
[PROOFSTEP]
rw [iterate_succ_apply', Nat.add_succ, verschiebung_coeff_succ]
[GOAL]
case succ
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
x : 𝕎 R
k✝ k : ℕ
ih : coeff ((↑verschiebung)^[k] x) (k✝ + k) = coeff x k✝
⊢ coeff ((↑verschiebung)^[k] x) (k✝ + k) = coeff x k✝
[PROOFSTEP]
exact ih
[GOAL]
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
x y : 𝕎 R
i : ℕ
⊢ (↑verschiebung)^[i] x * y = (↑verschiebung)^[i] (x * (↑frobenius)^[i] y)
[PROOFSTEP]
induction' i with i ih generalizing y
[GOAL]
case zero
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
x y✝ y : 𝕎 R
⊢ (↑verschiebung)^[Nat.zero] x * y = (↑verschiebung)^[Nat.zero] (x * (↑frobenius)^[Nat.zero] y)
[PROOFSTEP]
simp
[GOAL]
case succ
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
x y✝ : 𝕎 R
i : ℕ
ih : ∀ (y : 𝕎 R), (↑verschiebung)^[i] x * y = (↑verschiebung)^[i] (x * (↑frobenius)^[i] y)
y : 𝕎 R
⊢ (↑verschiebung)^[Nat.succ i] x * y = (↑verschiebung)^[Nat.succ i] (x * (↑frobenius)^[Nat.succ i] y)
[PROOFSTEP]
rw [iterate_succ_apply', ← verschiebung_mul_frobenius, ih, iterate_succ_apply']
[GOAL]
case succ
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
x y✝ : 𝕎 R
i : ℕ
ih : ∀ (y : 𝕎 R), (↑verschiebung)^[i] x * y = (↑verschiebung)^[i] (x * (↑frobenius)^[i] y)
y : 𝕎 R
⊢ ↑verschiebung ((↑verschiebung)^[i] (x * (↑frobenius)^[i] (↑frobenius y))) =
    ↑verschiebung ((↑verschiebung)^[i] (x * (↑frobenius)^[Nat.succ i] y))
[PROOFSTEP]
rfl
[GOAL]
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CharP R p
x y : 𝕎 R
i j : ℕ
⊢ (↑verschiebung)^[i] x * (↑verschiebung)^[j] y = (↑verschiebung)^[i + j] ((↑frobenius)^[j] x * (↑frobenius)^[i] y)
[PROOFSTEP]
calc
  _ = verschiebung^[i] (x * frobenius^[i] (verschiebung^[j] y)) := ?_
  _ = verschiebung^[i] (x * verschiebung^[j] (frobenius^[i] y)) := ?_
  _ = verschiebung^[i] (verschiebung^[j] (frobenius^[i] y) * x) := ?_
  _ = verschiebung^[i] (verschiebung^[j] (frobenius^[i] y * frobenius^[j] x)) := ?_
  _ = verschiebung^[i + j] (frobenius^[i] y * frobenius^[j] x) := ?_
  _ = _ := ?_
[GOAL]
case calc_1
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CharP R p
x y : 𝕎 R
i j : ℕ
⊢ (↑verschiebung)^[i] x * (↑verschiebung)^[j] y = (↑verschiebung)^[i] (x * (↑frobenius)^[i] ((↑verschiebung)^[j] y))
[PROOFSTEP]
apply iterate_verschiebung_mul_left
[GOAL]
case calc_2
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CharP R p
x y : 𝕎 R
i j : ℕ
⊢ (↑verschiebung)^[i] (x * (↑frobenius)^[i] ((↑verschiebung)^[j] y)) =
    (↑verschiebung)^[i] (x * (↑verschiebung)^[j] ((↑frobenius)^[i] y))
[PROOFSTEP]
rw [verschiebung_frobenius_comm.iterate_iterate]
[GOAL]
case calc_3
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CharP R p
x y : 𝕎 R
i j : ℕ
⊢ (↑verschiebung)^[i] (x * (↑verschiebung)^[j] ((↑frobenius)^[i] y)) =
    (↑verschiebung)^[i] ((↑verschiebung)^[j] ((↑frobenius)^[i] y) * x)
[PROOFSTEP]
rw [mul_comm]
[GOAL]
case calc_4
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CharP R p
x y : 𝕎 R
i j : ℕ
⊢ (↑verschiebung)^[i] ((↑verschiebung)^[j] ((↑frobenius)^[i] y) * x) =
    (↑verschiebung)^[i] ((↑verschiebung)^[j] ((↑frobenius)^[i] y * (↑frobenius)^[j] x))
[PROOFSTEP]
rw [iterate_verschiebung_mul_left]
[GOAL]
case calc_5
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CharP R p
x y : 𝕎 R
i j : ℕ
⊢ (↑verschiebung)^[i] ((↑verschiebung)^[j] ((↑frobenius)^[i] y * (↑frobenius)^[j] x)) =
    (↑verschiebung)^[i + j] ((↑frobenius)^[i] y * (↑frobenius)^[j] x)
[PROOFSTEP]
rw [iterate_add_apply]
[GOAL]
case calc_6
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CharP R p
x y : 𝕎 R
i j : ℕ
⊢ (↑verschiebung)^[i + j] ((↑frobenius)^[i] y * (↑frobenius)^[j] x) =
    (↑verschiebung)^[i + j] ((↑frobenius)^[j] x * (↑frobenius)^[i] y)
[PROOFSTEP]
rw [mul_comm]
[GOAL]
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CharP R p
x : 𝕎 R
i k : ℕ
⊢ coeff ((↑frobenius)^[i] x) k = coeff x k ^ p ^ i
[PROOFSTEP]
induction' i with i ih
[GOAL]
case zero
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CharP R p
x : 𝕎 R
k : ℕ
⊢ coeff ((↑frobenius)^[Nat.zero] x) k = coeff x k ^ p ^ Nat.zero
[PROOFSTEP]
simp
[GOAL]
case succ
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CharP R p
x : 𝕎 R
k i : ℕ
ih : coeff ((↑frobenius)^[i] x) k = coeff x k ^ p ^ i
⊢ coeff ((↑frobenius)^[Nat.succ i] x) k = coeff x k ^ p ^ Nat.succ i
[PROOFSTEP]
rw [iterate_succ_apply', coeff_frobenius_charP, ih, Nat.pow_succ]
[GOAL]
case succ
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CharP R p
x : 𝕎 R
k i : ℕ
ih : coeff ((↑frobenius)^[i] x) k = coeff x k ^ p ^ i
⊢ (coeff x k ^ p ^ i) ^ p = coeff x k ^ (p ^ i * p)
[PROOFSTEP]
ring_nf
[GOAL]
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CharP R p
x y : 𝕎 R
i j : ℕ
⊢ coeff ((↑verschiebung)^[i] x * (↑verschiebung)^[j] y) (i + j) = coeff x 0 ^ p ^ j * coeff y 0 ^ p ^ i
[PROOFSTEP]
calc
  _ = (verschiebung^[i + j] (frobenius^[j] x * frobenius^[i] y)).coeff (i + j) := ?_
  _ = (frobenius^[j] x * frobenius^[i] y).coeff 0 := ?_
  _ = (frobenius^[j] x).coeff 0 * (frobenius^[i] y).coeff 0 := ?_
  _ = _ := ?_
[GOAL]
case calc_1
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CharP R p
x y : 𝕎 R
i j : ℕ
⊢ coeff ((↑verschiebung)^[i] x * (↑verschiebung)^[j] y) (i + j) =
    coeff ((↑verschiebung)^[i + j] ((↑frobenius)^[j] x * (↑frobenius)^[i] y)) (i + j)
[PROOFSTEP]
rw [iterate_verschiebung_mul]
[GOAL]
case calc_2
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CharP R p
x y : 𝕎 R
i j : ℕ
⊢ coeff ((↑verschiebung)^[i + j] ((↑frobenius)^[j] x * (↑frobenius)^[i] y)) (i + j) =
    coeff ((↑frobenius)^[j] x * (↑frobenius)^[i] y) 0
[PROOFSTEP]
convert iterate_verschiebung_coeff (p := p) (R := R) _ _ _ using 2
[GOAL]
case h.e'_2.h.e'_4
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CharP R p
x y : 𝕎 R
i j : ℕ
⊢ i + j = 0 + (i + j)
[PROOFSTEP]
rw [zero_add]
[GOAL]
case calc_3
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CharP R p
x y : 𝕎 R
i j : ℕ
⊢ coeff ((↑frobenius)^[j] x * (↑frobenius)^[i] y) 0 = coeff ((↑frobenius)^[j] x) 0 * coeff ((↑frobenius)^[i] y) 0
[PROOFSTEP]
apply mul_coeff_zero
[GOAL]
case calc_4
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CharP R p
x y : 𝕎 R
i j : ℕ
⊢ coeff ((↑frobenius)^[j] x) 0 * coeff ((↑frobenius)^[i] y) 0 = coeff x 0 ^ p ^ j * coeff y 0 ^ p ^ i
[PROOFSTEP]
simp only [iterate_frobenius_coeff]
