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 : 𝕎 R
h :
  coeff (p := p) ((verschiebung : (a : 𝕎 R) → 𝕎 R) ((frobenius : (a : 𝕎 R) → 𝕎 R) x : 𝕎 R)) 0 = (x * (↑p : 𝕎 R)).coeff 0
⊢ (verschiebung : (a : 𝕎 R) → 𝕎 R) ((frobenius : (a : 𝕎 R) → 𝕎 R) x : 𝕎 R) = x * (↑p : 𝕎 R)
have h₁ : ∀ (n : ℕ),
  coeff (p := p) ((verschiebung : (a : 𝕎 R) → 𝕎 R) ((frobenius : (a : 𝕎 R) → 𝕎 R) x : 𝕎 R)) (n + 1) =
    (x * (↑p : 𝕎 R)).coeff (n + 1)
Tactic: ext ⟨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
⊢ coeff (p := p) ((verschiebung : (a : 𝕎 R) → 𝕎 R) ((frobenius : (a : 𝕎 R) → 𝕎 R) x : 𝕎 R)) 0 = (x * (↑p : 𝕎 R)).coeff 0
have h : Eq.{u_1 + 1} (α := R) (coeff (p := p) ((verschiebung : (a : 𝕎 R) → 𝕎 R) ((frobenius : (a : 𝕎 R) → 𝕎 R) x : 𝕎 R)) 0) 0
Tactic: rw [mul_charP_coeff_zero, verschiebung_coeff_zero]
-- 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
h :
  Eq.{u_1 + 1} (α := R) (coeff (p := p) ((verschiebung : (a : 𝕎 R) → 𝕎 R) ((frobenius : (a : 𝕎 R) → 𝕎 R) x : 𝕎 R)) 0) 0
⊢ coeff (p := p) ((verschiebung : (a : 𝕎 R) → 𝕎 R) ((frobenius : (a : 𝕎 R) → 𝕎 R) x : 𝕎 R)) 0 = (x * (↑p : 𝕎 R)).coeff 0
have h₁ : Eq.{u_1 + 1} (α := R) 0 0
Tactic: rw [mul_charP_coeff_zero, verschiebung_coeff_zero]
-- 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 : ℕ
⊢ coeff (p := p) ((verschiebung : (a : 𝕎 R) → 𝕎 R) ((frobenius : (a : 𝕎 R) → 𝕎 R) x : 𝕎 R)) (n + 1) =
    (x * (↑p : 𝕎 R)).coeff (n + 1)
have h : coeff (p := p) ((verschiebung : (a : 𝕎 R) → 𝕎 R) ((frobenius : (a : 𝕎 R) → 𝕎 R) x : 𝕎 R)) (n + 1) = x.coeff n ^ p
Tactic: rw [mul_charP_coeff_succ, verschiebung_coeff_succ, coeff_frobenius_charP]
-- 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 : ℕ
h : coeff (p := p) ((verschiebung : (a : 𝕎 R) → 𝕎 R) ((frobenius : (a : 𝕎 R) → 𝕎 R) x : 𝕎 R)) (n + 1) = x.coeff n ^ p
⊢ coeff (p := p) ((verschiebung : (a : 𝕎 R) → 𝕎 R) ((frobenius : (a : 𝕎 R) → 𝕎 R) x : 𝕎 R)) (n + 1) =
    (x * (↑p : 𝕎 R)).coeff (n + 1)
have h₁ : coeff (p := p) ((frobenius : (a : 𝕎 R) → 𝕎 R) x) n = x.coeff n ^ p
Tactic: rw [mul_charP_coeff_succ, verschiebung_coeff_succ, coeff_frobenius_charP]
-- 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 : ℕ
h : coeff (p := p) ((verschiebung : (a : 𝕎 R) → 𝕎 R) ((frobenius : (a : 𝕎 R) → 𝕎 R) x : 𝕎 R)) (n + 1) = x.coeff n ^ p
h₁ : coeff (p := p) ((frobenius : (a : 𝕎 R) → 𝕎 R) x) n = x.coeff n ^ p
⊢ coeff (p := p) ((verschiebung : (a : 𝕎 R) → 𝕎 R) ((frobenius : (a : 𝕎 R) → 𝕎 R) x : 𝕎 R)) (n + 1) =
    (x * (↑p : 𝕎 R)).coeff (n + 1)
have h₂ : x.coeff n ^ p = x.coeff n ^ p
Tactic: rw [mul_charP_coeff_succ, verschiebung_coeff_succ, coeff_frobenius_charP]
-- 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
⊢ Eq (α := 𝕎 R) ((verschiebung : (a : 𝕎 R) → 𝕎 R) ((frobenius : (a : 𝕎 R) → 𝕎 R) x : 𝕎 R) : 𝕎 R)
    ((frobenius : (a : 𝕎 R) → 𝕎 R) ((verschiebung : (a : 𝕎 R) → 𝕎 R) x : 𝕎 R) : 𝕎 R)
have rw : x * (↑p : 𝕎 R) = (frobenius : (a : 𝕎 R) → 𝕎 R) ((verschiebung : (a : 𝕎 R) → 𝕎 R) x : 𝕎 R)
Tactic: rw [verschiebung_frobenius, frobenius_verschiebung]
-- 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
rw : x * (↑p : 𝕎 R) = (frobenius : (a : 𝕎 R) → 𝕎 R) ((verschiebung : (a : 𝕎 R) → 𝕎 R) x : 𝕎 R)
⊢ Eq (α := 𝕎 R) ((verschiebung : (a : 𝕎 R) → 𝕎 R) ((frobenius : (a : 𝕎 R) → 𝕎 R) x : 𝕎 R) : 𝕎 R)
    ((frobenius : (a : 𝕎 R) → 𝕎 R) ((verschiebung : (a : 𝕎 R) → 𝕎 R) x : 𝕎 R) : 𝕎 R)
have rw₁ : x * (↑p : 𝕎 R) = x * (↑p : 𝕎 R)
Tactic: rw [verschiebung_frobenius, frobenius_verschiebung]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Identities (goal)
Goal:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst : CommRing R
x : 𝕎 R
n : ℕ
ih : ∀ {m : ℕ} (h : m < n), ((⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[n] x).coeff m = 0
m : ℕ
h : m < n + 1
⊢ ((⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[n + 1] x).coeff m = 0
have succ : Eq.{u_1 + 1} (α := R) (coeff (p := p) ((verschiebung : (a : 𝕎 R) → 𝕎 R) ((⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[n] x)) m) 0
Tactic: rw [iterate_succ_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
x : 𝕎 R
n : ℕ
ih : ∀ {m : ℕ} (h : m < n), ((⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[n] x).coeff m = 0
m' : ℕ
h : m' + 1 < n + 1
⊢ Eq.{u_1 + 1} (α := R)
    (coeff (p := p) ((verschiebung : (a : 𝕎 R) → 𝕎 R) ((⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[n] x)) (m' + 1)) 0
have succ : m' < n
Tactic: rw [verschiebung_coeff_succ, 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
x : 𝕎 R
n : ℕ
ih : ∀ {m : ℕ} (h : m < n), ((⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[n] x).coeff m = 0
m : ℕ
h : m < n + 1
⊢ Eq.{u_1 + 1} (α := R) (coeff (p := p) ((verschiebung : (a : 𝕎 R) → 𝕎 R) ((⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[n] x)) m)
    0
have succ : ∀ (h : 0 < n + 1),
  Eq.{u_1 + 1} (α := R) (coeff (p := p) ((verschiebung : (a : 𝕎 R) → 𝕎 R) ((⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[n] x)) 0)
    0
Tactic: cases m with
    | zero => exact verschiebung_coeff_zero _
    | succ m' =>
      rw [verschiebung_coeff_succ, ih]
      simpa using h
Cleared hypotheses: m, h
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Identities (goal)
Goal:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst : CommRing R
x : 𝕎 R
n : ℕ
ih : ∀ {m : ℕ} (h : m < n), ((⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[n] x).coeff m = 0
m : ℕ
h : m < n + 1
succ :
  ∀ (h : 0 < n + 1),
    Eq.{u_1 + 1} (α := R)
      (coeff (p := p) ((verschiebung : (a : 𝕎 R) → 𝕎 R) ((⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[n] x)) 0) 0
⊢ Eq.{u_1 + 1} (α := R) (coeff (p := p) ((verschiebung : (a : 𝕎 R) → 𝕎 R) ((⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[n] x)) m)
    0
have succ₁ : ∀ (m' : ℕ) (h : m' + 1 < n + 1),
  Eq.{u_1 + 1} (α := R)
    (coeff (p := p) ((verschiebung : (a : 𝕎 R) → 𝕎 R) ((⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[n] x)) (m' + 1)) 0
Tactic: cases m with
    | zero => exact verschiebung_coeff_zero _
    | succ m' =>
      rw [verschiebung_coeff_succ, ih]
      simpa using h
Cleared hypotheses: m, h
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Identities (goal)
Goal:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst : CommRing R
x : 𝕎 R
n m : ℕ
h : m < n
⊢ ((⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[n] x).coeff m = 0
have zero : ∀ {m : ℕ} (h : m < 0), ((⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[0] x).coeff m = 0
Tactic: induction n generalizing m with
  | zero => contradiction
  | succ n ih =>
    rw [iterate_succ_apply']
    cases m with
    | zero => exact verschiebung_coeff_zero _
    | succ m' =>
      rw [verschiebung_coeff_succ, ih]
      simpa using h
Cleared hypotheses: n, m, h
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Identities (goal)
Goal:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst : CommRing R
x : 𝕎 R
n m : ℕ
h : m < n
zero : ∀ {m : ℕ} (h : m < 0), ((⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[0] x).coeff m = 0
⊢ ((⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[n] x).coeff m = 0
have succ : ∀ (n : ℕ) (ih : ∀ {m : ℕ} (h : m < n), ((⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[n] x).coeff m = 0) {m : ℕ} (h : m < n + 1),
  ((⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[n + 1] x).coeff m = 0
Tactic: induction n generalizing m with
  | zero => contradiction
  | succ n ih =>
    rw [iterate_succ_apply']
    cases m with
    | zero => exact verschiebung_coeff_zero _
    | succ m' =>
      rw [verschiebung_coeff_succ, ih]
      simpa using h
Cleared hypotheses: n, m, h
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Identities (goal)
Goal:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst : CommRing R
x : 𝕎 R
n k : ℕ
⊢ ((⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[n] x).coeff (k + n) = x.coeff k
have zero : ((⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[0] x).coeff (k + 0) = x.coeff k
Tactic: induction n with
  | zero => simp
  | succ k ih => rw [iterate_succ_apply', Nat.add_succ, verschiebung_coeff_succ]; exact ih
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Identities (goal)
Goal:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst : CommRing R
x : 𝕎 R
n k : ℕ
zero : ((⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[0] x).coeff (k + 0) = x.coeff k
⊢ ((⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[n] x).coeff (k + n) = x.coeff k
have succ : ∀ (k_1 : ℕ) (ih : ((⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[k_1] x).coeff (k + k_1) = x.coeff k),
  ((⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[k_1 + 1] x).coeff (k + (k_1 + 1)) = x.coeff k
Tactic: induction n with
  | zero => simp
  | succ k ih => rw [iterate_succ_apply', Nat.add_succ, verschiebung_coeff_succ]; exact ih
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Identities (goal)
Goal:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst : CommRing R
x : 𝕎 R
i : ℕ
ih :
  ∀ (y : 𝕎 R),
    (⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[i] x * y =
      (⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[i] (x * (⇑frobenius : (a : 𝕎 R) → 𝕎 R)^[i] y)
y : 𝕎 R
⊢ (⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[i + 1] x * y =
    (⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[i + 1] (x * (⇑frobenius : (a : 𝕎 R) → 𝕎 R)^[i + 1] y)
have succ : HMul.hMul (α := 𝕎 R) ((verschiebung : (a : 𝕎 R) → 𝕎 R) ((⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[i] x) : 𝕎 R) y =
  (⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[i + 1] (x * (⇑frobenius : (a : 𝕎 R) → 𝕎 R)^[i + 1] y)
Tactic: rw [iterate_succ_apply', ← verschiebung_mul_frobenius, ih, iterate_succ_apply',
      iterate_succ_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
x : 𝕎 R
i : ℕ
ih :
  ∀ (y : 𝕎 R),
    (⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[i] x * y =
      (⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[i] (x * (⇑frobenius : (a : 𝕎 R) → 𝕎 R)^[i] y)
y : 𝕎 R
succ :
  HMul.hMul (α := 𝕎 R) ((verschiebung : (a : 𝕎 R) → 𝕎 R) ((⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[i] x) : 𝕎 R) y =
    (⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[i + 1] (x * (⇑frobenius : (a : 𝕎 R) → 𝕎 R)^[i + 1] y)
⊢ (⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[i + 1] x * y =
    (⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[i + 1] (x * (⇑frobenius : (a : 𝕎 R) → 𝕎 R)^[i + 1] y)
have succ₁ : (verschiebung : (a : 𝕎 R) → 𝕎 R)
    (HMul.hMul (β := 𝕎 R) ((⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[i] x) ((frobenius : (a : 𝕎 R) → 𝕎 R) y : 𝕎 R)) =
  (⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[i + 1] (x * (⇑frobenius : (a : 𝕎 R) → 𝕎 R)^[i + 1] y)
Tactic: rw [iterate_succ_apply', ← verschiebung_mul_frobenius, ih, iterate_succ_apply',
      iterate_succ_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
x : 𝕎 R
i : ℕ
ih :
  ∀ (y : 𝕎 R),
    (⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[i] x * y =
      (⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[i] (x * (⇑frobenius : (a : 𝕎 R) → 𝕎 R)^[i] y)
y : 𝕎 R
succ :
  HMul.hMul (α := 𝕎 R) ((verschiebung : (a : 𝕎 R) → 𝕎 R) ((⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[i] x) : 𝕎 R) y =
    (⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[i + 1] (x * (⇑frobenius : (a : 𝕎 R) → 𝕎 R)^[i + 1] y)
succ₁ :
  (verschiebung : (a : 𝕎 R) → 𝕎 R)
      (HMul.hMul (β := 𝕎 R) ((⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[i] x) ((frobenius : (a : 𝕎 R) → 𝕎 R) y : 𝕎 R)) =
    (⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[i + 1] (x * (⇑frobenius : (a : 𝕎 R) → 𝕎 R)^[i + 1] y)
⊢ (⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[i + 1] x * y =
    (⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[i + 1] (x * (⇑frobenius : (a : 𝕎 R) → 𝕎 R)^[i + 1] y)
have succ₂ : (verschiebung : (a : 𝕎 R) → 𝕎 R)
    ((⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[i]
      (HMul.hMul (β := 𝕎 R) x ((⇑frobenius : (a : 𝕎 R) → 𝕎 R)^[i] ((frobenius : (a : 𝕎 R) → 𝕎 R) y) : 𝕎 R))) =
  (⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[i + 1] (x * (⇑frobenius : (a : 𝕎 R) → 𝕎 R)^[i + 1] y)
Tactic: rw [iterate_succ_apply', ← verschiebung_mul_frobenius, ih, iterate_succ_apply',
      iterate_succ_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
x : 𝕎 R
i : ℕ
ih :
  ∀ (y : 𝕎 R),
    (⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[i] x * y =
      (⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[i] (x * (⇑frobenius : (a : 𝕎 R) → 𝕎 R)^[i] y)
y : 𝕎 R
succ :
  HMul.hMul (α := 𝕎 R) ((verschiebung : (a : 𝕎 R) → 𝕎 R) ((⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[i] x) : 𝕎 R) y =
    (⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[i + 1] (x * (⇑frobenius : (a : 𝕎 R) → 𝕎 R)^[i + 1] y)
succ₁ :
  (verschiebung : (a : 𝕎 R) → 𝕎 R)
      (HMul.hMul (β := 𝕎 R) ((⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[i] x) ((frobenius : (a : 𝕎 R) → 𝕎 R) y : 𝕎 R)) =
    (⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[i + 1] (x * (⇑frobenius : (a : 𝕎 R) → 𝕎 R)^[i + 1] y)
succ₂ :
  (verschiebung : (a : 𝕎 R) → 𝕎 R)
      ((⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[i]
        (HMul.hMul (β := 𝕎 R) x ((⇑frobenius : (a : 𝕎 R) → 𝕎 R)^[i] ((frobenius : (a : 𝕎 R) → 𝕎 R) y) : 𝕎 R))) =
    (⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[i + 1] (x * (⇑frobenius : (a : 𝕎 R) → 𝕎 R)^[i + 1] y)
⊢ (⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[i + 1] x * y =
    (⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[i + 1] (x * (⇑frobenius : (a : 𝕎 R) → 𝕎 R)^[i + 1] y)
have succ₃ : Eq (α := 𝕎 R)
  ((verschiebung : (a : 𝕎 R) → 𝕎 R)
      ((⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[i]
        (HMul.hMul (β := 𝕎 R) x ((⇑frobenius : (a : 𝕎 R) → 𝕎 R)^[i] ((frobenius : (a : 𝕎 R) → 𝕎 R) y) : 𝕎 R))) :
    𝕎 R)
  ((verschiebung : (a : 𝕎 R) → 𝕎 R)
      ((⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[i] (x * (⇑frobenius : (a : 𝕎 R) → 𝕎 R)^[i + 1] y)) :
    𝕎 R)
Tactic: rw [iterate_succ_apply', ← verschiebung_mul_frobenius, ih, iterate_succ_apply',
      iterate_succ_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
x : 𝕎 R
i : ℕ
ih :
  ∀ (y : 𝕎 R),
    (⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[i] x * y =
      (⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[i] (x * (⇑frobenius : (a : 𝕎 R) → 𝕎 R)^[i] y)
y : 𝕎 R
succ :
  HMul.hMul (α := 𝕎 R) ((verschiebung : (a : 𝕎 R) → 𝕎 R) ((⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[i] x) : 𝕎 R) y =
    (⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[i + 1] (x * (⇑frobenius : (a : 𝕎 R) → 𝕎 R)^[i + 1] y)
succ₁ :
  (verschiebung : (a : 𝕎 R) → 𝕎 R)
      (HMul.hMul (β := 𝕎 R) ((⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[i] x) ((frobenius : (a : 𝕎 R) → 𝕎 R) y : 𝕎 R)) =
    (⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[i + 1] (x * (⇑frobenius : (a : 𝕎 R) → 𝕎 R)^[i + 1] y)
succ₂ :
  (verschiebung : (a : 𝕎 R) → 𝕎 R)
      ((⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[i]
        (HMul.hMul (β := 𝕎 R) x ((⇑frobenius : (a : 𝕎 R) → 𝕎 R)^[i] ((frobenius : (a : 𝕎 R) → 𝕎 R) y) : 𝕎 R))) =
    (⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[i + 1] (x * (⇑frobenius : (a : 𝕎 R) → 𝕎 R)^[i + 1] y)
succ₃ :
  Eq (α := 𝕎 R)
    ((verschiebung : (a : 𝕎 R) → 𝕎 R)
        ((⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[i]
          (HMul.hMul (β := 𝕎 R) x ((⇑frobenius : (a : 𝕎 R) → 𝕎 R)^[i] ((frobenius : (a : 𝕎 R) → 𝕎 R) y) : 𝕎 R))) :
      𝕎 R)
    ((verschiebung : (a : 𝕎 R) → 𝕎 R)
        ((⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[i] (x * (⇑frobenius : (a : 𝕎 R) → 𝕎 R)^[i + 1] y)) :
      𝕎 R)
⊢ (⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[i + 1] x * y =
    (⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[i + 1] (x * (⇑frobenius : (a : 𝕎 R) → 𝕎 R)^[i + 1] y)
have succ₄ : Eq (α := 𝕎 R)
  ((verschiebung : (a : 𝕎 R) → 𝕎 R)
      ((⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[i]
        (HMul.hMul (β := 𝕎 R) x ((⇑frobenius : (a : 𝕎 R) → 𝕎 R)^[i] ((frobenius : (a : 𝕎 R) → 𝕎 R) y) : 𝕎 R))) :
    𝕎 R)
  ((verschiebung : (a : 𝕎 R) → 𝕎 R)
      ((⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[i]
        (HMul.hMul (β := 𝕎 R) x ((⇑frobenius : (a : 𝕎 R) → 𝕎 R)^[i] ((frobenius : (a : 𝕎 R) → 𝕎 R) y) : 𝕎 R))) :
    𝕎 R)
Tactic: rw [iterate_succ_apply', ← verschiebung_mul_frobenius, ih, iterate_succ_apply',
      iterate_succ_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
x y : 𝕎 R
i : ℕ
⊢ (⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[i] x * y =
    (⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[i] (x * (⇑frobenius : (a : 𝕎 R) → 𝕎 R)^[i] y)
have zero : ∀ (y : 𝕎 R),
  (⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[0] x * y =
    (⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[0] (x * (⇑frobenius : (a : 𝕎 R) → 𝕎 R)^[0] y)
Tactic: induction i generalizing y with
  | zero => simp
  | succ i ih =>
    rw [iterate_succ_apply', ← verschiebung_mul_frobenius, ih, iterate_succ_apply',
      iterate_succ_apply]
Cleared hypotheses: y, 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
x y : 𝕎 R
i : ℕ
zero :
  ∀ (y : 𝕎 R),
    (⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[0] x * y =
      (⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[0] (x * (⇑frobenius : (a : 𝕎 R) → 𝕎 R)^[0] y)
⊢ (⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[i] x * y =
    (⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[i] (x * (⇑frobenius : (a : 𝕎 R) → 𝕎 R)^[i] y)
have succ : ∀ (i : ℕ)
  (ih :
    ∀ (y : 𝕎 R),
      (⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[i] x * y =
        (⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[i] (x * (⇑frobenius : (a : 𝕎 R) → 𝕎 R)^[i] y))
  (y : 𝕎 R),
  (⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[i + 1] x * y =
    (⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[i + 1] (x * (⇑frobenius : (a : 𝕎 R) → 𝕎 R)^[i + 1] y)
Tactic: induction i generalizing y with
  | zero => simp
  | succ i ih =>
    rw [iterate_succ_apply', ← verschiebung_mul_frobenius, ih, iterate_succ_apply',
      iterate_succ_apply]
Cleared hypotheses: y, 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 =
    (⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[i + j]
      ((⇑frobenius : (a : 𝕎 R) → 𝕎 R)^[j] x * (⇑frobenius : (a : 𝕎 R) → 𝕎 R)^[i] y)
have 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))
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))
⊢ (⇑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_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))
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))
⊢ (⇑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_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)
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)
⊢ (⇑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_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))
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) := ?_
    _ = _ := ?_