awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Identities (goal)
Goal:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst : CommRing R
inst_1 : CharP R p
x y : 𝕎 R
i j : ℕ
calc_1 :
  (⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[i] x * (⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[j] y =
    (⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[i]
      (x * (⇑frobenius : (a : 𝕎 R) → 𝕎 R)^[i] ((⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[j] y))
calc_2 :
  (⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[i]
      (x * (⇑frobenius : (a : 𝕎 R) → 𝕎 R)^[i] ((⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[j] y)) =
    (⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[i]
      (x * (⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[j] ((⇑frobenius : (a : 𝕎 R) → 𝕎 R)^[i] y))
calc_3 :
  (⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[i]
      (x * (⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[j] ((⇑frobenius : (a : 𝕎 R) → 𝕎 R)^[i] y)) =
    (⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[i]
      ((⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[j] ((⇑frobenius : (a : 𝕎 R) → 𝕎 R)^[i] y) * x)
calc_4 :
  (⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[i]
      ((⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[j] ((⇑frobenius : (a : 𝕎 R) → 𝕎 R)^[i] y) * x) =
    (⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[i]
      ((⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[j]
        ((⇑frobenius : (a : 𝕎 R) → 𝕎 R)^[i] y * (⇑frobenius : (a : 𝕎 R) → 𝕎 R)^[j] x))
⊢ (⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[i] x * (⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[j] y =
    (⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[i + j]
      ((⇑frobenius : (a : 𝕎 R) → 𝕎 R)^[j] x * (⇑frobenius : (a : 𝕎 R) → 𝕎 R)^[i] y)
have calc_5 : (⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[i]
    ((⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[j]
      ((⇑frobenius : (a : 𝕎 R) → 𝕎 R)^[i] y * (⇑frobenius : (a : 𝕎 R) → 𝕎 R)^[j] x)) =
  (⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[i + j]
    ((⇑frobenius : (a : 𝕎 R) → 𝕎 R)^[i] y * (⇑frobenius : (a : 𝕎 R) → 𝕎 R)^[j] x)
Tactic: 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) := ?_
    _ = _ := ?_
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Identities (goal)
Goal:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst : CommRing R
inst_1 : CharP R p
x y : 𝕎 R
i j : ℕ
calc_1 :
  (⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[i] x * (⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[j] y =
    (⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[i]
      (x * (⇑frobenius : (a : 𝕎 R) → 𝕎 R)^[i] ((⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[j] y))
calc_2 :
  (⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[i]
      (x * (⇑frobenius : (a : 𝕎 R) → 𝕎 R)^[i] ((⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[j] y)) =
    (⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[i]
      (x * (⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[j] ((⇑frobenius : (a : 𝕎 R) → 𝕎 R)^[i] y))
calc_3 :
  (⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[i]
      (x * (⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[j] ((⇑frobenius : (a : 𝕎 R) → 𝕎 R)^[i] y)) =
    (⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[i]
      ((⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[j] ((⇑frobenius : (a : 𝕎 R) → 𝕎 R)^[i] y) * x)
calc_4 :
  (⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[i]
      ((⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[j] ((⇑frobenius : (a : 𝕎 R) → 𝕎 R)^[i] y) * x) =
    (⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[i]
      ((⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[j]
        ((⇑frobenius : (a : 𝕎 R) → 𝕎 R)^[i] y * (⇑frobenius : (a : 𝕎 R) → 𝕎 R)^[j] x))
calc_5 :
  (⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[i]
      ((⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[j]
        ((⇑frobenius : (a : 𝕎 R) → 𝕎 R)^[i] y * (⇑frobenius : (a : 𝕎 R) → 𝕎 R)^[j] x)) =
    (⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[i + j]
      ((⇑frobenius : (a : 𝕎 R) → 𝕎 R)^[i] y * (⇑frobenius : (a : 𝕎 R) → 𝕎 R)^[j] x)
⊢ (⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[i] x * (⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[j] y =
    (⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[i + j]
      ((⇑frobenius : (a : 𝕎 R) → 𝕎 R)^[j] x * (⇑frobenius : (a : 𝕎 R) → 𝕎 R)^[i] y)
have calc_6 : (⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[i + j]
    ((⇑frobenius : (a : 𝕎 R) → 𝕎 R)^[i] y * (⇑frobenius : (a : 𝕎 R) → 𝕎 R)^[j] x) =
  (⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[i + j]
    ((⇑frobenius : (a : 𝕎 R) → 𝕎 R)^[j] x * (⇑frobenius : (a : 𝕎 R) → 𝕎 R)^[i] y)
Tactic: 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) := ?_
    _ = _ := ?_
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Identities (goal)
Goal:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst : CommRing R
inst_1 : CharP R p
x y : 𝕎 R
i j : ℕ
⊢ (⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[i]
      (x * (⇑frobenius : (a : 𝕎 R) → 𝕎 R)^[i] ((⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[j] y)) =
    (⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[i]
      (x * (⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[j] ((⇑frobenius : (a : 𝕎 R) → 𝕎 R)^[i] y))
have calc_2 : (⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[i]
    (x * (⇑frobenius : (a : 𝕎 R) → 𝕎 R)^[i] ((⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[j] y)) =
  (⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[i]
    (x * (⇑frobenius : (a : 𝕎 R) → 𝕎 R)^[i] ((⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[j] y))
Tactic: rw [verschiebung_frobenius_comm.iterate_iterate]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Identities (goal)
Goal:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst : CommRing R
inst_1 : CharP R p
x y : 𝕎 R
i j : ℕ
⊢ (⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[i]
      (x * (⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[j] ((⇑frobenius : (a : 𝕎 R) → 𝕎 R)^[i] y)) =
    (⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[i]
      ((⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[j] ((⇑frobenius : (a : 𝕎 R) → 𝕎 R)^[i] y) * x)
have calc_3 : (⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[i]
    ((⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[j] ((⇑frobenius : (a : 𝕎 R) → 𝕎 R)^[i] y) * x) =
  (⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[i]
    ((⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[j] ((⇑frobenius : (a : 𝕎 R) → 𝕎 R)^[i] y) * x)
Tactic: rw [mul_comm]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Identities (goal)
Goal:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst : CommRing R
inst_1 : CharP R p
x y : 𝕎 R
i j : ℕ
⊢ (⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[i]
      ((⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[j] ((⇑frobenius : (a : 𝕎 R) → 𝕎 R)^[i] y) * x) =
    (⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[i]
      ((⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[j]
        ((⇑frobenius : (a : 𝕎 R) → 𝕎 R)^[i] y * (⇑frobenius : (a : 𝕎 R) → 𝕎 R)^[j] x))
have calc_4 : (⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[i]
    ((⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[j]
      ((⇑frobenius : (a : 𝕎 R) → 𝕎 R)^[i] y * (⇑frobenius : (a : 𝕎 R) → 𝕎 R)^[j] x)) =
  (⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[i]
    ((⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[j]
      ((⇑frobenius : (a : 𝕎 R) → 𝕎 R)^[i] y * (⇑frobenius : (a : 𝕎 R) → 𝕎 R)^[j] x))
Tactic: rw [iterate_verschiebung_mul_left]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Identities (goal)
Goal:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst : CommRing R
inst_1 : CharP R p
x y : 𝕎 R
i j : ℕ
⊢ (⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[i]
      ((⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[j]
        ((⇑frobenius : (a : 𝕎 R) → 𝕎 R)^[i] y * (⇑frobenius : (a : 𝕎 R) → 𝕎 R)^[j] x)) =
    (⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[i + j]
      ((⇑frobenius : (a : 𝕎 R) → 𝕎 R)^[i] y * (⇑frobenius : (a : 𝕎 R) → 𝕎 R)^[j] x)
have calc_5 : (⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[i]
    ((⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[j]
      ((⇑frobenius : (a : 𝕎 R) → 𝕎 R)^[i] y * (⇑frobenius : (a : 𝕎 R) → 𝕎 R)^[j] x)) =
  (⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[i]
    ((⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[j]
      ((⇑frobenius : (a : 𝕎 R) → 𝕎 R)^[i] y * (⇑frobenius : (a : 𝕎 R) → 𝕎 R)^[j] x))
Tactic: rw [iterate_add_apply]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Identities (goal)
Goal:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst : CommRing R
inst_1 : CharP R p
x y : 𝕎 R
i j : ℕ
⊢ (⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[i + j]
      ((⇑frobenius : (a : 𝕎 R) → 𝕎 R)^[i] y * (⇑frobenius : (a : 𝕎 R) → 𝕎 R)^[j] x) =
    (⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[i + j]
      ((⇑frobenius : (a : 𝕎 R) → 𝕎 R)^[j] x * (⇑frobenius : (a : 𝕎 R) → 𝕎 R)^[i] y)
have calc_6 : (⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[i + j]
    ((⇑frobenius : (a : 𝕎 R) → 𝕎 R)^[j] x * (⇑frobenius : (a : 𝕎 R) → 𝕎 R)^[i] y) =
  (⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[i + j]
    ((⇑frobenius : (a : 𝕎 R) → 𝕎 R)^[j] x * (⇑frobenius : (a : 𝕎 R) → 𝕎 R)^[i] y)
Tactic: rw [mul_comm]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Identities (goal)
Goal:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst : CommRing R
inst_1 : CharP R p
x : 𝕎 R
k i : ℕ
ih : ((⇑frobenius : (a : 𝕎 R) → 𝕎 R)^[i] x).coeff k = x.coeff k ^ p ^ i
⊢ ((⇑frobenius : (a : 𝕎 R) → 𝕎 R)^[i + 1] x).coeff k = x.coeff k ^ p ^ (i + 1)
have succ : (x.coeff k ^ p ^ i) ^ p = x.coeff k ^ p ^ (i + 1)
Tactic: rw [iterate_succ_apply', coeff_frobenius_charP, ih]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Identities (goal)
Goal:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst : CommRing R
inst_1 : CharP R p
x : 𝕎 R
i k : ℕ
⊢ ((⇑frobenius : (a : 𝕎 R) → 𝕎 R)^[i] x).coeff k = x.coeff k ^ p ^ i
have zero : ((⇑frobenius : (a : 𝕎 R) → 𝕎 R)^[0] x).coeff k = x.coeff k ^ HPow.hPow (β := ℕ) p 0
Tactic: induction i with
  | zero => simp
  | succ i ih => rw [iterate_succ_apply', coeff_frobenius_charP, ih]; ring_nf
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Identities (goal)
Goal:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst : CommRing R
inst_1 : CharP R p
x : 𝕎 R
i k : ℕ
zero : ((⇑frobenius : (a : 𝕎 R) → 𝕎 R)^[0] x).coeff k = x.coeff k ^ HPow.hPow (β := ℕ) p 0
⊢ ((⇑frobenius : (a : 𝕎 R) → 𝕎 R)^[i] x).coeff k = x.coeff k ^ p ^ i
have succ : ∀ (i : ℕ) (ih : ((⇑frobenius : (a : 𝕎 R) → 𝕎 R)^[i] x).coeff k = x.coeff k ^ p ^ i),
  ((⇑frobenius : (a : 𝕎 R) → 𝕎 R)^[i + 1] x).coeff k = x.coeff k ^ p ^ (i + 1)
Tactic: induction i with
  | zero => simp
  | succ i ih => rw [iterate_succ_apply', coeff_frobenius_charP, ih]; ring_nf
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Identities (goal)
Goal:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst : CommRing R
inst_1 : CharP R p
x y : 𝕎 R
i j : ℕ
⊢ ((⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[i] x * (⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[j] y).coeff (i + j) =
    x.coeff 0 ^ p ^ j * y.coeff 0 ^ p ^ i
have calc_1 : ((⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[i] x * (⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[j] y).coeff (i + j) =
  ((⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[i + j]
        ((⇑frobenius : (a : 𝕎 R) → 𝕎 R)^[j] x * (⇑frobenius : (a : 𝕎 R) → 𝕎 R)^[i] y)).coeff
    (i + j)
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 := ?_
    _ = _ := ?_
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Identities (goal)
Goal:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst : CommRing R
inst_1 : CharP R p
x y : 𝕎 R
i j : ℕ
calc_1 :
  ((⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[i] x * (⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[j] y).coeff (i + j) =
    ((⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[i + j]
          ((⇑frobenius : (a : 𝕎 R) → 𝕎 R)^[j] x * (⇑frobenius : (a : 𝕎 R) → 𝕎 R)^[i] y)).coeff
      (i + j)
⊢ ((⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[i] x * (⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[j] y).coeff (i + j) =
    x.coeff 0 ^ p ^ j * y.coeff 0 ^ p ^ i
have calc_2 : ((⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[i + j]
        ((⇑frobenius : (a : 𝕎 R) → 𝕎 R)^[j] x * (⇑frobenius : (a : 𝕎 R) → 𝕎 R)^[i] y)).coeff
    (i + j) =
  ((⇑frobenius : (a : 𝕎 R) → 𝕎 R)^[j] x * (⇑frobenius : (a : 𝕎 R) → 𝕎 R)^[i] y).coeff 0
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 := ?_
    _ = _ := ?_
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Identities (goal)
Goal:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst : CommRing R
inst_1 : CharP R p
x y : 𝕎 R
i j : ℕ
calc_1 :
  ((⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[i] x * (⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[j] y).coeff (i + j) =
    ((⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[i + j]
          ((⇑frobenius : (a : 𝕎 R) → 𝕎 R)^[j] x * (⇑frobenius : (a : 𝕎 R) → 𝕎 R)^[i] y)).coeff
      (i + j)
calc_2 :
  ((⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[i + j]
          ((⇑frobenius : (a : 𝕎 R) → 𝕎 R)^[j] x * (⇑frobenius : (a : 𝕎 R) → 𝕎 R)^[i] y)).coeff
      (i + j) =
    ((⇑frobenius : (a : 𝕎 R) → 𝕎 R)^[j] x * (⇑frobenius : (a : 𝕎 R) → 𝕎 R)^[i] y).coeff 0
⊢ ((⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[i] x * (⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[j] y).coeff (i + j) =
    x.coeff 0 ^ p ^ j * y.coeff 0 ^ p ^ i
have calc_3 : ((⇑frobenius : (a : 𝕎 R) → 𝕎 R)^[j] x * (⇑frobenius : (a : 𝕎 R) → 𝕎 R)^[i] y).coeff 0 =
  ((⇑frobenius : (a : 𝕎 R) → 𝕎 R)^[j] x).coeff 0 * ((⇑frobenius : (a : 𝕎 R) → 𝕎 R)^[i] y).coeff 0
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 := ?_
    _ = _ := ?_
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Identities (goal)
Goal:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst : CommRing R
inst_1 : CharP R p
x y : 𝕎 R
i j : ℕ
calc_1 :
  ((⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[i] x * (⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[j] y).coeff (i + j) =
    ((⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[i + j]
          ((⇑frobenius : (a : 𝕎 R) → 𝕎 R)^[j] x * (⇑frobenius : (a : 𝕎 R) → 𝕎 R)^[i] y)).coeff
      (i + j)
calc_2 :
  ((⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[i + j]
          ((⇑frobenius : (a : 𝕎 R) → 𝕎 R)^[j] x * (⇑frobenius : (a : 𝕎 R) → 𝕎 R)^[i] y)).coeff
      (i + j) =
    ((⇑frobenius : (a : 𝕎 R) → 𝕎 R)^[j] x * (⇑frobenius : (a : 𝕎 R) → 𝕎 R)^[i] y).coeff 0
calc_3 :
  ((⇑frobenius : (a : 𝕎 R) → 𝕎 R)^[j] x * (⇑frobenius : (a : 𝕎 R) → 𝕎 R)^[i] y).coeff 0 =
    ((⇑frobenius : (a : 𝕎 R) → 𝕎 R)^[j] x).coeff 0 * ((⇑frobenius : (a : 𝕎 R) → 𝕎 R)^[i] y).coeff 0
⊢ ((⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[i] x * (⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[j] y).coeff (i + j) =
    x.coeff 0 ^ p ^ j * y.coeff 0 ^ p ^ i
have calc_4 : ((⇑frobenius : (a : 𝕎 R) → 𝕎 R)^[j] x).coeff 0 * ((⇑frobenius : (a : 𝕎 R) → 𝕎 R)^[i] y).coeff 0 =
  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 := ?_
    _ = _ := ?_
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Identities (goal)
Goal:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst : CommRing R
inst_1 : CharP R p
x y : 𝕎 R
i j : ℕ
⊢ ((⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[i] x * (⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[j] y).coeff (i + j) =
    ((⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[i + j]
          ((⇑frobenius : (a : 𝕎 R) → 𝕎 R)^[j] x * (⇑frobenius : (a : 𝕎 R) → 𝕎 R)^[i] y)).coeff
      (i + j)
have calc_1 : ((⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[i + j]
        ((⇑frobenius : (a : 𝕎 R) → 𝕎 R)^[j] x * (⇑frobenius : (a : 𝕎 R) → 𝕎 R)^[i] y)).coeff
    (i + j) =
  ((⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[i + j]
        ((⇑frobenius : (a : 𝕎 R) → 𝕎 R)^[j] x * (⇑frobenius : (a : 𝕎 R) → 𝕎 R)^[i] y)).coeff
    (i + j)
Tactic: rw [iterate_verschiebung_mul]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Identities (goal)
Goal:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst : CommRing R
inst_1 : CharP R p
x y : 𝕎 R
i j : ℕ
⊢ ((⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[i + j]
          ((⇑frobenius : (a : 𝕎 R) → 𝕎 R)^[j] x * (⇑frobenius : (a : 𝕎 R) → 𝕎 R)^[i] y)).coeff
      (i + j) =
    ((⇑frobenius : (a : 𝕎 R) → 𝕎 R)^[j] x * (⇑frobenius : (a : 𝕎 R) → 𝕎 R)^[i] y).coeff 0
have h : i + j = 0 + (i + j)
Tactic: convert! iterate_verschiebung_coeff (p := p) (R := R) _ _ _ using 2
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Identities (goal)
Goal:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst : CommRing R
inst_1 : CharP R p
x y : 𝕎 R
i j : ℕ
⊢ i + j = 0 + (i + j)
have h : i + j = i + j
Tactic: rw [zero_add]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Identities (goal)
Goal:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst : CommRing R
inst_1 : CharP R p
x : 𝕎 R
n : ℕ
⊢ (⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[n] ((⇑frobenius : (a : 𝕎 R) → 𝕎 R)^[n] x) = x * HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) n
have rw : (comp (β := 𝕎 R) (⇑verschiebung : (a : 𝕎 R) → 𝕎 R) (⇑frobenius : (a : 𝕎 R) → 𝕎 R))^[n] x =
  x * HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) n
Tactic: rw [← comp_apply (f := verschiebung^[n]),
      ← Function.Commute.comp_iterate verschiebung_frobenius_comm]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Identities (goal)
Goal:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst : CommRing R
inst_1 : CharP R p
x : 𝕎 R
n : ℕ
ih :
  (comp (β := 𝕎 R) (⇑verschiebung : (a : 𝕎 R) → 𝕎 R) (⇑frobenius : (a : 𝕎 R) → 𝕎 R))^[n] x =
    x * HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) n
⊢ (comp (β := 𝕎 R) (⇑verschiebung : (a : 𝕎 R) → 𝕎 R) (⇑frobenius : (a : 𝕎 R) → 𝕎 R))^[n + 1] x =
    x * HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) (n + 1)
have succ : comp (β := 𝕎 R) (⇑verschiebung : (a : 𝕎 R) → 𝕎 R) (⇑frobenius : (a : 𝕎 R) → 𝕎 R)
    ((comp (β := 𝕎 R) (⇑verschiebung : (a : 𝕎 R) → 𝕎 R) (⇑frobenius : (a : 𝕎 R) → 𝕎 R))^[n] x) =
  x * HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) (n + 1)
Tactic: rw [iterate_succ_apply', ih, pow_succ, comp_apply, verschiebung_frobenius, mul_assoc]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Identities (goal)
Goal:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst : CommRing R
inst_1 : CharP R p
x : 𝕎 R
n : ℕ
ih :
  (comp (β := 𝕎 R) (⇑verschiebung : (a : 𝕎 R) → 𝕎 R) (⇑frobenius : (a : 𝕎 R) → 𝕎 R))^[n] x =
    x * HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) n
succ :
  comp (β := 𝕎 R) (⇑verschiebung : (a : 𝕎 R) → 𝕎 R) (⇑frobenius : (a : 𝕎 R) → 𝕎 R)
      ((comp (β := 𝕎 R) (⇑verschiebung : (a : 𝕎 R) → 𝕎 R) (⇑frobenius : (a : 𝕎 R) → 𝕎 R))^[n] x) =
    x * HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) (n + 1)
⊢ (comp (β := 𝕎 R) (⇑verschiebung : (a : 𝕎 R) → 𝕎 R) (⇑frobenius : (a : 𝕎 R) → 𝕎 R))^[n + 1] x =
    x * HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) (n + 1)
have succ₁ : comp (β := 𝕎 R) (⇑verschiebung : (a : 𝕎 R) → 𝕎 R) (⇑frobenius : (a : 𝕎 R) → 𝕎 R)
    (x * HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) n) =
  x * HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) (n + 1)
Tactic: rw [iterate_succ_apply', ih, pow_succ, comp_apply, verschiebung_frobenius, mul_assoc]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Identities (goal)
Goal:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst : CommRing R
inst_1 : CharP R p
x : 𝕎 R
n : ℕ
ih :
  (comp (β := 𝕎 R) (⇑verschiebung : (a : 𝕎 R) → 𝕎 R) (⇑frobenius : (a : 𝕎 R) → 𝕎 R))^[n] x =
    x * HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) n
succ :
  comp (β := 𝕎 R) (⇑verschiebung : (a : 𝕎 R) → 𝕎 R) (⇑frobenius : (a : 𝕎 R) → 𝕎 R)
      ((comp (β := 𝕎 R) (⇑verschiebung : (a : 𝕎 R) → 𝕎 R) (⇑frobenius : (a : 𝕎 R) → 𝕎 R))^[n] x) =
    x * HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) (n + 1)
succ₁ :
  comp (β := 𝕎 R) (⇑verschiebung : (a : 𝕎 R) → 𝕎 R) (⇑frobenius : (a : 𝕎 R) → 𝕎 R)
      (x * HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) n) =
    x * HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) (n + 1)
⊢ (comp (β := 𝕎 R) (⇑verschiebung : (a : 𝕎 R) → 𝕎 R) (⇑frobenius : (a : 𝕎 R) → 𝕎 R))^[n + 1] x =
    x * HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) (n + 1)
have succ₂ : comp (β := 𝕎 R) (⇑verschiebung : (a : 𝕎 R) → 𝕎 R) (⇑frobenius : (a : 𝕎 R) → 𝕎 R)
    (x * HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) n) =
  x * (HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) n * (↑p : 𝕎 R))
Tactic: rw [iterate_succ_apply', ih, pow_succ, comp_apply, verschiebung_frobenius, mul_assoc]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Identities (goal)
Goal:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst : CommRing R
inst_1 : CharP R p
x : 𝕎 R
n : ℕ
ih :
  (comp (β := 𝕎 R) (⇑verschiebung : (a : 𝕎 R) → 𝕎 R) (⇑frobenius : (a : 𝕎 R) → 𝕎 R))^[n] x =
    x * HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) n
succ :
  comp (β := 𝕎 R) (⇑verschiebung : (a : 𝕎 R) → 𝕎 R) (⇑frobenius : (a : 𝕎 R) → 𝕎 R)
      ((comp (β := 𝕎 R) (⇑verschiebung : (a : 𝕎 R) → 𝕎 R) (⇑frobenius : (a : 𝕎 R) → 𝕎 R))^[n] x) =
    x * HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) (n + 1)
succ₁ :
  comp (β := 𝕎 R) (⇑verschiebung : (a : 𝕎 R) → 𝕎 R) (⇑frobenius : (a : 𝕎 R) → 𝕎 R)
      (x * HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) n) =
    x * HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) (n + 1)
succ₂ :
  comp (β := 𝕎 R) (⇑verschiebung : (a : 𝕎 R) → 𝕎 R) (⇑frobenius : (a : 𝕎 R) → 𝕎 R)
      (x * HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) n) =
    x * (HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) n * (↑p : 𝕎 R))
⊢ (comp (β := 𝕎 R) (⇑verschiebung : (a : 𝕎 R) → 𝕎 R) (⇑frobenius : (a : 𝕎 R) → 𝕎 R))^[n + 1] x =
    x * HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) (n + 1)
have succ₃ : (verschiebung : (a : 𝕎 R) → 𝕎 R) ((frobenius : (a : 𝕎 R) → 𝕎 R) (x * HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) n) : 𝕎 R) =
  x * (HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) n * (↑p : 𝕎 R))
Tactic: rw [iterate_succ_apply', ih, pow_succ, comp_apply, verschiebung_frobenius, mul_assoc]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Identities (goal)
Goal:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst : CommRing R
inst_1 : CharP R p
x : 𝕎 R
n : ℕ
ih :
  (comp (β := 𝕎 R) (⇑verschiebung : (a : 𝕎 R) → 𝕎 R) (⇑frobenius : (a : 𝕎 R) → 𝕎 R))^[n] x =
    x * HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) n
succ :
  comp (β := 𝕎 R) (⇑verschiebung : (a : 𝕎 R) → 𝕎 R) (⇑frobenius : (a : 𝕎 R) → 𝕎 R)
      ((comp (β := 𝕎 R) (⇑verschiebung : (a : 𝕎 R) → 𝕎 R) (⇑frobenius : (a : 𝕎 R) → 𝕎 R))^[n] x) =
    x * HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) (n + 1)
succ₁ :
  comp (β := 𝕎 R) (⇑verschiebung : (a : 𝕎 R) → 𝕎 R) (⇑frobenius : (a : 𝕎 R) → 𝕎 R)
      (x * HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) n) =
    x * HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) (n + 1)
succ₂ :
  comp (β := 𝕎 R) (⇑verschiebung : (a : 𝕎 R) → 𝕎 R) (⇑frobenius : (a : 𝕎 R) → 𝕎 R)
      (x * HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) n) =
    x * (HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) n * (↑p : 𝕎 R))
succ₃ :
  (verschiebung : (a : 𝕎 R) → 𝕎 R) ((frobenius : (a : 𝕎 R) → 𝕎 R) (x * HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) n) : 𝕎 R) =
    x * (HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) n * (↑p : 𝕎 R))
⊢ (comp (β := 𝕎 R) (⇑verschiebung : (a : 𝕎 R) → 𝕎 R) (⇑frobenius : (a : 𝕎 R) → 𝕎 R))^[n + 1] x =
    x * HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) (n + 1)
have succ₄ : x * HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) n * (↑p : 𝕎 R) = x * (HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) n * (↑p : 𝕎 R))
Tactic: rw [iterate_succ_apply', ih, pow_succ, comp_apply, verschiebung_frobenius, mul_assoc]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Identities (goal)
Goal:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst : CommRing R
inst_1 : CharP R p
x : 𝕎 R
n : ℕ
ih :
  (comp (β := 𝕎 R) (⇑verschiebung : (a : 𝕎 R) → 𝕎 R) (⇑frobenius : (a : 𝕎 R) → 𝕎 R))^[n] x =
    x * HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) n
succ :
  comp (β := 𝕎 R) (⇑verschiebung : (a : 𝕎 R) → 𝕎 R) (⇑frobenius : (a : 𝕎 R) → 𝕎 R)
      ((comp (β := 𝕎 R) (⇑verschiebung : (a : 𝕎 R) → 𝕎 R) (⇑frobenius : (a : 𝕎 R) → 𝕎 R))^[n] x) =
    x * HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) (n + 1)
succ₁ :
  comp (β := 𝕎 R) (⇑verschiebung : (a : 𝕎 R) → 𝕎 R) (⇑frobenius : (a : 𝕎 R) → 𝕎 R)
      (x * HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) n) =
    x * HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) (n + 1)
succ₂ :
  comp (β := 𝕎 R) (⇑verschiebung : (a : 𝕎 R) → 𝕎 R) (⇑frobenius : (a : 𝕎 R) → 𝕎 R)
      (x * HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) n) =
    x * (HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) n * (↑p : 𝕎 R))
succ₃ :
  (verschiebung : (a : 𝕎 R) → 𝕎 R) ((frobenius : (a : 𝕎 R) → 𝕎 R) (x * HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) n) : 𝕎 R) =
    x * (HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) n * (↑p : 𝕎 R))
succ₄ : x * HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) n * (↑p : 𝕎 R) = x * (HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) n * (↑p : 𝕎 R))
⊢ (comp (β := 𝕎 R) (⇑verschiebung : (a : 𝕎 R) → 𝕎 R) (⇑frobenius : (a : 𝕎 R) → 𝕎 R))^[n + 1] x =
    x * HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) (n + 1)
have succ₅ : x * (HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) n * (↑p : 𝕎 R)) = x * (HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) n * (↑p : 𝕎 R))
Tactic: rw [iterate_succ_apply', ih, pow_succ, comp_apply, verschiebung_frobenius, mul_assoc]