awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.WittVector.Identities
Goal:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst : CommRing R
inst_1 : CharP R p
x : 𝕎 R
n : ℕ
ih : ∀ {m : ℕ}, (x * HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) n).coeff (m + n) = x.coeff m ^ p ^ n
m : ℕ
succ : (x * HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) n).coeff (m + n) ^ p = (x.coeff m ^ p ^ n) ^ p
⊢ (x * HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) (n + 1)).coeff (m + (n + 1)) = x.coeff m ^ p ^ (n + 1)

Tactic:
rw [pow_succ, ← mul_assoc, ← add_assoc, mul_charP_coeff_succ, pow_succ, pow_mul]

Premises used: pow_succ, add_assoc, mul_assoc, pow_mul, WittVector.mul_charP_coeff_succ
-- Module: Mathlib.RingTheory.WittVector.Identities
Goal:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst : CommRing R
inst_1 : CharP R p
x : 𝕎 R
n : ℕ
ih : ∀ {m : ℕ}, (x * HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) n).coeff (m + n) = x.coeff m ^ p ^ n
m : ℕ
succ : (x * HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) n).coeff (m + n) = x.coeff m ^ p ^ n
⊢ (x * HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) n).coeff (m + n) ^ p = (x.coeff m ^ p ^ n) ^ p

Tactic:
congr
-- Module: Mathlib.RingTheory.WittVector.Identities
Goal:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst : CommRing R
inst_1 : CharP R p
x : 𝕎 R
n : ℕ
ih : ∀ {m : ℕ}, (x * HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) n).coeff (m + n) = x.coeff m ^ p ^ n
m : ℕ
⊢ (x * HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) n).coeff (m + n) = x.coeff m ^ p ^ n

Tactic:
ih
-- Module: Mathlib.RingTheory.WittVector.Identities
Goal:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst : CommRing R
inst_1 : CharP R p
x : 𝕎 R
n : ℕ
ih : ∀ {m : ℕ}, (x * HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) n).coeff (m + n) = x.coeff m ^ p ^ n
m : ℕ
⊢ (x * HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) n).coeff (m + n) = x.coeff m ^ p ^ n

Tactic:
exact ih
-- Module: Mathlib.RingTheory.WittVector.Identities
Goal:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst : CommRing R
inst_1 : CharP R p
x : 𝕎 R
m n : ℕ
zero : ∀ {m : ℕ}, (x * HPow.hPow (α := 𝕎 R) (β := ℕ) (↑p : 𝕎 R) 0).coeff (m + 0) = x.coeff m ^ HPow.hPow (β := ℕ) p 0
succ :
  ∀ (n : ℕ) (ih : ∀ {m : ℕ}, (x * HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) n).coeff (m + n) = x.coeff m ^ p ^ n) {m : ℕ},
    (x * HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) (n + 1)).coeff (m + (n + 1)) = x.coeff m ^ p ^ (n + 1)
⊢ (x * HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) n).coeff (m + n) = x.coeff m ^ p ^ n

Tactic:
induction n generalizing m with
  | zero => simp
  | succ n ih =>
    rw [pow_succ, ← mul_assoc, ← add_assoc, mul_charP_coeff_succ, pow_succ, pow_mul]
    congr
    exact ih

Premises used: pow_succ, add_assoc, mul_assoc, pow_mul, WittVector.mul_charP_coeff_succ
-- Module: Mathlib.RingTheory.WittVector.Identities
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
h₁ :
  ∀ (n : ℕ),
    coeff (p := p) ((verschiebung : (a : 𝕎 R) → 𝕎 R) ((frobenius : (a : 𝕎 R) → 𝕎 R) x : 𝕎 R)) (n + 1) =
      (x * (↑p : 𝕎 R)).coeff (n + 1)
⊢ (verschiebung : (a : 𝕎 R) → 𝕎 R) ((frobenius : (a : 𝕎 R) → 𝕎 R) x : 𝕎 R) = x * (↑p : 𝕎 R)

Tactic:
ext ⟨i⟩
-- Module: Mathlib.RingTheory.WittVector.Identities
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
h₁ h₂ : Eq.{u_1 + 1} (α := R) 0 0
⊢ coeff (p := p) ((verschiebung : (a : 𝕎 R) → 𝕎 R) ((frobenius : (a : 𝕎 R) → 𝕎 R) x : 𝕎 R)) 0 = (x * (↑p : 𝕎 R)).coeff 0

Tactic:
rw [mul_charP_coeff_zero, verschiebung_coeff_zero]

Premises used: WittVector.verschiebung_coeff_zero, WittVector.mul_charP_coeff_zero
-- Module: Mathlib.RingTheory.WittVector.Identities
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
h₂ h₃ : x.coeff n ^ p = 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)

Tactic:
rw [mul_charP_coeff_succ, verschiebung_coeff_succ, coeff_frobenius_charP]

Premises used: WittVector.verschiebung_coeff_succ, WittVector.coeff_frobenius_charP, WittVector.mul_charP_coeff_succ
-- Module: Mathlib.RingTheory.WittVector.Identities
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)
rw₁ rw₂ : x * (↑p : 𝕎 R) = x * (↑p : 𝕎 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)

Tactic:
rw [verschiebung_frobenius, frobenius_verschiebung]

Premises used: WittVector.verschiebung_frobenius, WittVector.frobenius_verschiebung
-- Module: Mathlib.RingTheory.WittVector.Identities
Goal:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst : CommRing R
x : 𝕎 R
m : ℕ
h : m < 0
⊢ ((⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[0] x).coeff m = 0

Tactic:
contradiction
-- Module: Mathlib.RingTheory.WittVector.Identities
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 :
  Eq.{u_1 + 1} (α := R) (coeff (p := p) ((verschiebung : (a : 𝕎 R) → 𝕎 R) ((⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[n] x)) m)
    0
⊢ ((⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[n + 1] x).coeff m = 0

Tactic:
rw [iterate_succ_apply']

Premises used: Function.iterate_succ_apply'
-- Module: Mathlib.RingTheory.WittVector.Identities
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
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:
verschiebung_coeff_zero _

Premises used: WittVector.verschiebung_coeff_zero
-- Module: Mathlib.RingTheory.WittVector.Identities
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
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:
exact verschiebung_coeff_zero _

Premises used: WittVector.verschiebung_coeff_zero
-- Module: Mathlib.RingTheory.WittVector.Identities
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
succ : m' < n
⊢ Eq.{u_1 + 1} (α := R)
    (coeff (p := p) ((verschiebung : (a : 𝕎 R) → 𝕎 R) ((⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[n] x)) (m' + 1)) 0

Tactic:
rw [verschiebung_coeff_succ, ih]

Premises used: WittVector.verschiebung_coeff_succ
-- Module: Mathlib.RingTheory.WittVector.Identities
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
⊢ m' < n

Tactic:
simpa using h
-- Module: Mathlib.RingTheory.WittVector.Identities
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
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
⊢ Eq.{u_1 + 1} (α := R) (coeff (p := p) ((verschiebung : (a : 𝕎 R) → 𝕎 R) ((⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[n] x)) m)
    0

Tactic:
cases m with
    | zero => exact verschiebung_coeff_zero _
    | succ m' =>
      rw [verschiebung_coeff_succ, ih]
      simpa using h

Premises used: WittVector.verschiebung_coeff_succ, WittVector.verschiebung_coeff_zero
-- Module: Mathlib.RingTheory.WittVector.Identities
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
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
⊢ ((⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[n] 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

Premises used: Function.iterate_succ_apply', WittVector.verschiebung_coeff_succ, WittVector.verschiebung_coeff_zero
-- Module: Mathlib.RingTheory.WittVector.Identities
Goal:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst : CommRing R
x : 𝕎 R
k : ℕ
⊢ ((⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[0] x).coeff (k + 0) = x.coeff k

Tactic:
simp
-- Module: Mathlib.RingTheory.WittVector.Identities
Goal:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst : CommRing R
x : 𝕎 R
k_1 k : ℕ
ih succ : ((⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[k] x).coeff (k_1 + k) = x.coeff k_1
⊢ ((⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[k + 1] x).coeff (k_1 + (k + 1)) = x.coeff k_1

Tactic:
rw [iterate_succ_apply', Nat.add_succ, verschiebung_coeff_succ]

Premises used: Function.iterate_succ_apply', WittVector.verschiebung_coeff_succ, Nat.add_succ
-- Module: Mathlib.RingTheory.WittVector.Identities
Goal:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst : CommRing R
x : 𝕎 R
k_1 k : ℕ
ih : ((⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[k] x).coeff (k_1 + k) = x.coeff k_1
⊢ ((⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[k] x).coeff (k_1 + k) = x.coeff k_1

Tactic:
ih
-- Module: Mathlib.RingTheory.WittVector.Identities
Goal:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst : CommRing R
x : 𝕎 R
k_1 k : ℕ
ih : ((⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[k] x).coeff (k_1 + k) = x.coeff k_1
⊢ ((⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[k] x).coeff (k_1 + k) = x.coeff k_1

Tactic:
exact ih
-- Module: Mathlib.RingTheory.WittVector.Identities
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
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
⊢ ((⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[n] x).coeff (k + n) = x.coeff k

Tactic:
induction n with
  | zero => simp
  | succ k ih => rw [iterate_succ_apply', Nat.add_succ, verschiebung_coeff_succ]; exact ih

Premises used: Function.iterate_succ_apply', WittVector.verschiebung_coeff_succ, Nat.add_succ
-- Module: Mathlib.RingTheory.WittVector.Identities
Goal:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst : CommRing R
x y : 𝕎 R
⊢ (⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[0] x * y =
    (⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[0] (x * (⇑frobenius : (a : 𝕎 R) → 𝕎 R)^[0] y)

Tactic:
simp
-- Module: Mathlib.RingTheory.WittVector.Identities
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)
succ₄ 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)
⊢ (⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[i + 1] x * 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]

Premises used: Function.iterate_succ_apply', WittVector.verschiebung_mul_frobenius, Function.iterate_succ_apply
-- Module: Mathlib.RingTheory.WittVector.Identities
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)
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)
⊢ (⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[i] x * y =
    (⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[i] (x * (⇑frobenius : (a : 𝕎 R) → 𝕎 R)^[i] 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]

Premises used: Function.iterate_succ_apply', WittVector.verschiebung_mul_frobenius, Function.iterate_succ_apply
-- Module: Mathlib.RingTheory.WittVector.Identities
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]
      (x * (⇑frobenius : (a : 𝕎 R) → 𝕎 R)^[i] ((⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[j] y))

Tactic:
?_
-- Module: Mathlib.RingTheory.WittVector.Identities
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))

Tactic:
?_
-- Module: Mathlib.RingTheory.WittVector.Identities
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)

Tactic:
?_
-- Module: Mathlib.RingTheory.WittVector.Identities
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))

Tactic:
?_
-- Module: Mathlib.RingTheory.WittVector.Identities
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)

Tactic:
?_
-- Module: Mathlib.RingTheory.WittVector.Identities
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)

Tactic:
?_
-- Module: Mathlib.RingTheory.WittVector.Identities
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)
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)
⊢ (⇑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)

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

Premises used: HMul.hMul, WittVector.frobenius, Nat.iterate, HAdd.hAdd, DFunLike.coe, WittVector.verschiebung
-- Module: Mathlib.RingTheory.WittVector.Identities
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]
      (x * (⇑frobenius : (a : 𝕎 R) → 𝕎 R)^[i] ((⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[j] y))

Tactic:
apply iterate_verschiebung_mul_left

Premises used: WittVector.iterate_verschiebung_mul_left
-- Module: Mathlib.RingTheory.WittVector.Identities
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_2 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))
⊢ (⇑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:
rw [verschiebung_frobenius_comm.iterate_iterate]

Premises used: Function.Commute.iterate_iterate, WittVector.verschiebung_frobenius_comm
-- Module: Mathlib.RingTheory.WittVector.Identities
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_3 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)
⊢ (⇑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:
rw [mul_comm]

Premises used: mul_comm
-- Module: Mathlib.RingTheory.WittVector.Identities
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_4 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))
⊢ (⇑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:
rw [iterate_verschiebung_mul_left]

Premises used: WittVector.iterate_verschiebung_mul_left
-- Module: Mathlib.RingTheory.WittVector.Identities
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_5 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))
⊢ (⇑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:
rw [iterate_add_apply]

Premises used: Function.iterate_add_apply