-- Mathlib/RingTheory/WittVector/Identities.lean
theorem iterate_verschiebung_mul_coeff (x y : 𝕎 R) (i j : ℕ) :
    (verschiebung^[i] x * verschiebung^[j] y).coeff (i + j) =
      x.coeff 0 ^ p ^ j * y.coeff 0 ^ p ^ i

Proof state:
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).coeff (i + j) =
    ((⇑verschiebung)^[i + j] ((⇑frobenius)^[j] x * (⇑frobenius)^[i] y)).coeff (i + j)

Tactic:
rw [iterate_verschiebung_mul]

Result:
no goals

Proof state:
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).coeff (i + j) = x.coeff 0 ^ p ^ j * y.coeff 0 ^ p ^ i

Tactic:
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 := ?_
  _ = _ := ?_

Result:
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).coeff (i + j) =
    ((⇑verschiebung)^[i + j] ((⇑frobenius)^[j] x * (⇑frobenius)^[i] y)).coeff (i + j)

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 + j] ((⇑frobenius)^[j] x * (⇑frobenius)^[i] y)).coeff (i + j) =
    ((⇑frobenius)^[j] x * (⇑frobenius)^[i] y).coeff 0

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 : ℕ
⊢ ((⇑frobenius)^[j] x * (⇑frobenius)^[i] y).coeff 0 = ((⇑frobenius)^[j] x).coeff 0 * ((⇑frobenius)^[i] y).coeff 0

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 : ℕ
⊢ ((⇑frobenius)^[j] x).coeff 0 * ((⇑frobenius)^[i] y).coeff 0 = x.coeff 0 ^ p ^ j * y.coeff 0 ^ p ^ i

Proof state:
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)

Tactic:
rw [zero_add]

Result:
no goals

Proof state:
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 : ℕ
⊢ ((⇑frobenius)^[j] x).coeff 0 * ((⇑frobenius)^[i] y).coeff 0 = x.coeff 0 ^ p ^ j * y.coeff 0 ^ p ^ i

Tactic:
simp only [iterate_frobenius_coeff]

Result:
no goals

Proof state:
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 + j] ((⇑frobenius)^[j] x * (⇑frobenius)^[i] y)).coeff (i + j) =
    ((⇑frobenius)^[j] x * (⇑frobenius)^[i] y).coeff 0

Tactic:
convert iterate_verschiebung_coeff (p := p) (R := R) _ _ _ using 2

Result:
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)

Proof state:
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 : ℕ
⊢ ((⇑frobenius)^[j] x * (⇑frobenius)^[i] y).coeff 0 = ((⇑frobenius)^[j] x).coeff 0 * ((⇑frobenius)^[i] y).coeff 0

Tactic:
apply mul_coeff_zero

Result:
no goals