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
i : ℕ
h : (HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) i).coeff i = 1
succ : (HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) i * (↑p : 𝕎 R)).coeff (i + 1) = 1
succ₁ :
  Eq.{u_1 + 1} (α := R)
    (coeff (p := p)
      ((frobenius : (a : 𝕎 R) → 𝕎 R) ((verschiebung : (a : 𝕎 R) → 𝕎 R) (HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) i) : 𝕎 R))
      (i + 1))
    1
succ₂ :
  HPow.hPow (α := R) (coeff (p := p) ((verschiebung : (a : 𝕎 R) → 𝕎 R) (HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) i)) (i + 1)) p =
    1
succ₃ : (HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) i).coeff i ^ p = 1
⊢ (HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) (i + 1)).coeff (i + 1) = 1
have succ₄ : HPow.hPow (α := R) 1 p = 1
Tactic: rw [pow_succ, ← frobenius_verschiebung, coeff_frobenius_charP,
      verschiebung_coeff_succ, h, one_pow]
-- 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
i : ℕ
h : (HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) i).coeff i = 1
succ : (HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) i * (↑p : 𝕎 R)).coeff (i + 1) = 1
succ₁ :
  Eq.{u_1 + 1} (α := R)
    (coeff (p := p)
      ((frobenius : (a : 𝕎 R) → 𝕎 R) ((verschiebung : (a : 𝕎 R) → 𝕎 R) (HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) i) : 𝕎 R))
      (i + 1))
    1
succ₂ :
  HPow.hPow (α := R) (coeff (p := p) ((verschiebung : (a : 𝕎 R) → 𝕎 R) (HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) i)) (i + 1)) p =
    1
succ₃ : (HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) i).coeff i ^ p = 1
succ₄ : HPow.hPow (α := R) 1 p = 1
⊢ (HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) (i + 1)).coeff (i + 1) = 1
have succ₅ : Eq.{u_1 + 1} (α := R) 1 1
Tactic: rw [pow_succ, ← frobenius_verschiebung, coeff_frobenius_charP,
      verschiebung_coeff_succ, h, one_pow]
-- 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
i : ℕ
⊢ (HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) i).coeff i = 1
have zero : (HPow.hPow (α := 𝕎 R) (β := ℕ) (↑p : 𝕎 R) 0).coeff 0 = 1
Tactic: induction i with
  | zero => simp only [one_coeff_zero, pow_zero]
  | succ i h =>
    rw [pow_succ, ← frobenius_verschiebung, coeff_frobenius_charP,
      verschiebung_coeff_succ, h, one_pow]
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
i : ℕ
zero : (HPow.hPow (α := 𝕎 R) (β := ℕ) (↑p : 𝕎 R) 0).coeff 0 = 1
⊢ (HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) i).coeff i = 1
have succ : ∀ (i : ℕ) (h : (HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) i).coeff i = 1),
  (HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) (i + 1)).coeff (i + 1) = 1
Tactic: induction i with
  | zero => simp only [one_coeff_zero, pow_zero]
  | succ i h =>
    rw [pow_succ, ← frobenius_verschiebung, coeff_frobenius_charP,
      verschiebung_coeff_succ, h, one_pow]
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
j : ℕ
hj : j ≠ 0
⊢ (HPow.hPow (α := 𝕎 R) (β := ℕ) (↑p : 𝕎 R) 0).coeff j = 0
have zero : 0 < j
Tactic: rw [pow_zero, one_coeff_eq_of_pos]
-- 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
i : ℕ
hi : ∀ {j : ℕ} (hj : j ≠ i), (HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) i).coeff j = 0
j : ℕ
hj : j ≠ i + 1
⊢ (HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) (i + 1)).coeff j = 0
have succ : HPow.hPow (α := R) (coeff (p := p) ((verschiebung : (a : 𝕎 R) → 𝕎 R) (HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) i)) j) p = 0
Tactic: rw [pow_succ, ← frobenius_verschiebung, 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
i : ℕ
hi : ∀ {j : ℕ} (hj : j ≠ i), (HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) i).coeff j = 0
j : ℕ
hj : j ≠ i + 1
⊢ HPow.hPow (α := R) (coeff (p := p) ((verschiebung : (a : 𝕎 R) → 𝕎 R) (HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) i)) j) p = 0
have succ : ∀ (hj : 0 ≠ i + 1),
  HPow.hPow (α := R) (coeff (p := p) ((verschiebung : (a : 𝕎 R) → 𝕎 R) (HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) i)) 0) p = 0
Tactic: cases j
Cleared hypotheses: j, hj
-- 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
i : ℕ
hi : ∀ {j : ℕ} (hj : j ≠ i), (HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) i).coeff j = 0
j : ℕ
hj : j ≠ i + 1
succ :
  ∀ (hj : 0 ≠ i + 1),
    HPow.hPow (α := R) (coeff (p := p) ((verschiebung : (a : 𝕎 R) → 𝕎 R) (HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) i)) 0) p = 0
⊢ HPow.hPow (α := R) (coeff (p := p) ((verschiebung : (a : 𝕎 R) → 𝕎 R) (HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) i)) j) p = 0
have succ₁ : ∀ (n : ℕ) (hj : n + 1 ≠ i + 1),
  HPow.hPow (α := R) (coeff (p := p) ((verschiebung : (a : 𝕎 R) → 𝕎 R) (HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) i)) (n + 1)) p =
    0
Tactic: cases j
Cleared hypotheses: j, hj
-- 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
i : ℕ
hi : ∀ {j : ℕ} (hj : j ≠ i), (HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) i).coeff j = 0
hj : 0 ≠ i + 1
⊢ HPow.hPow (α := R) (coeff (p := p) ((verschiebung : (a : 𝕎 R) → 𝕎 R) (HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) i)) 0) p = 0
have succ : HPow.hPow (α := R) 0 p = 0
Tactic: rw [verschiebung_coeff_zero, zero_pow hp.out.ne_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
i : ℕ
hi : ∀ {j : ℕ} (hj : j ≠ i), (HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) i).coeff j = 0
hj : 0 ≠ i + 1
succ : HPow.hPow (α := R) 0 p = 0
⊢ HPow.hPow (α := R) (coeff (p := p) ((verschiebung : (a : 𝕎 R) → 𝕎 R) (HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) i)) 0) p = 0
have succ₁ : Eq.{u_1 + 1} (α := R) 0 0
Tactic: rw [verschiebung_coeff_zero, zero_pow hp.out.ne_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
i : ℕ
hi : ∀ {j : ℕ} (hj : j ≠ i), (HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) i).coeff j = 0
n : ℕ
hj : n + 1 ≠ i + 1
⊢ HPow.hPow (α := R) (coeff (p := p) ((verschiebung : (a : 𝕎 R) → 𝕎 R) (HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) i)) (n + 1)) p =
    0
have succ : (HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) i).coeff n ^ p = 0
Tactic: rw [verschiebung_coeff_succ, hi (ne_of_apply_ne _ hj), zero_pow hp.out.ne_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
i : ℕ
hi : ∀ {j : ℕ} (hj : j ≠ i), (HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) i).coeff j = 0
n : ℕ
hj : n + 1 ≠ i + 1
succ : (HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) i).coeff n ^ p = 0
⊢ HPow.hPow (α := R) (coeff (p := p) ((verschiebung : (a : 𝕎 R) → 𝕎 R) (HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) i)) (n + 1)) p =
    0
have succ₁ : HPow.hPow (α := R) 0 p = 0
Tactic: rw [verschiebung_coeff_succ, hi (ne_of_apply_ne _ hj), zero_pow hp.out.ne_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
i : ℕ
hi : ∀ {j : ℕ} (hj : j ≠ i), (HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) i).coeff j = 0
n : ℕ
hj : n + 1 ≠ i + 1
succ : (HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) i).coeff n ^ p = 0
succ₁ : HPow.hPow (α := R) 0 p = 0
⊢ HPow.hPow (α := R) (coeff (p := p) ((verschiebung : (a : 𝕎 R) → 𝕎 R) (HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) i)) (n + 1)) p =
    0
have succ₂ : Eq.{u_1 + 1} (α := R) 0 0
Tactic: rw [verschiebung_coeff_succ, hi (ne_of_apply_ne _ hj), zero_pow hp.out.ne_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
i j : ℕ
hj : j ≠ i
⊢ (HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) i).coeff j = 0
have zero : ∀ {j : ℕ} (hj : j ≠ 0), (HPow.hPow (α := 𝕎 R) (β := ℕ) (↑p : 𝕎 R) 0).coeff j = 0
Tactic: induction i generalizing j with
  | zero =>
    rw [pow_zero, one_coeff_eq_of_pos]
    exact Nat.pos_of_ne_zero hj
  | succ i hi =>
    rw [pow_succ, ← frobenius_verschiebung, coeff_frobenius_charP]
    cases j
    · rw [verschiebung_coeff_zero, zero_pow hp.out.ne_zero]
    · rw [verschiebung_coeff_succ, hi (ne_of_apply_ne _ hj), zero_pow hp.out.ne_zero]
Cleared hypotheses: i, j, hj
-- 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
i j : ℕ
hj : j ≠ i
zero : ∀ {j : ℕ} (hj : j ≠ 0), (HPow.hPow (α := 𝕎 R) (β := ℕ) (↑p : 𝕎 R) 0).coeff j = 0
⊢ (HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) i).coeff j = 0
have succ : ∀ (i : ℕ) (hi : ∀ {j : ℕ} (hj : j ≠ i), (HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) i).coeff j = 0) {j : ℕ} (hj : j ≠ i + 1),
  (HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) (i + 1)).coeff j = 0
Tactic: induction i generalizing j with
  | zero =>
    rw [pow_zero, one_coeff_eq_of_pos]
    exact Nat.pos_of_ne_zero hj
  | succ i hi =>
    rw [pow_succ, ← frobenius_verschiebung, coeff_frobenius_charP]
    cases j
    · rw [verschiebung_coeff_zero, zero_pow hp.out.ne_zero]
    · rw [verschiebung_coeff_succ, hi (ne_of_apply_ne _ hj), zero_pow hp.out.ne_zero]
Cleared hypotheses: i, j, hj
-- 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
i : ℕ
⊢ Eq.{u_1 + 1} (α := R) (coeff (p := p) (↑p : 𝕎 R) i) (if i = 1 then 1 else 0)
have pos : ∀ (hi : i = 1), Eq.{u_1 + 1} (α := R) (coeff (p := p) (↑p : 𝕎 R) i) 1
Tactic: split_ifs with hi
-- 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
i : ℕ
pos : ∀ (hi : i = 1), Eq.{u_1 + 1} (α := R) (coeff (p := p) (↑p : 𝕎 R) i) 1
⊢ Eq.{u_1 + 1} (α := R) (coeff (p := p) (↑p : 𝕎 R) i) (if i = 1 then 1 else 0)
have neg : ∀ (hi : ¬i = 1), Eq.{u_1 + 1} (α := R) (coeff (p := p) (↑p : 𝕎 R) i) 0
Tactic: split_ifs with hi
-- 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
⊢ Eq.{u_1 + 1} (α := R) (coeff (p := p) (↑p : 𝕎 R) 0) 0
have hnc : ¬Eq (α := ℕ) 0 1
Tactic: rw [coeff_p, if_neg]
-- 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
⊢ Eq.{u_1 + 1} (α := R) (coeff (p := p) (↑p : 𝕎 R) 1) 1
have rw : Eq.{u_1 + 1} (α := R) (if Eq (α := ℕ) 1 1 then 1 else 0) 1
Tactic: rw [coeff_p, if_pos rfl]
-- 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
rw : Eq.{u_1 + 1} (α := R) (if Eq (α := ℕ) 1 1 then 1 else 0) 1
⊢ Eq.{u_1 + 1} (α := R) (coeff (p := p) (↑p : 𝕎 R) 1) 1
have rw₁ : Eq.{u_1 + 1} (α := R) 1 1
Tactic: rw [coeff_p, if_pos rfl]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Identities (hypothesis)
Goal:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst : CommRing R
x y : 𝕎 R
⊢ (verschiebung : (a : 𝕎 R) → 𝕎 R) (HMul.hMul (β := 𝕎 R) x ((frobenius : (a : 𝕎 R) → 𝕎 R) y : 𝕎 R)) =
    HMul.hMul (α := 𝕎 R) ((verschiebung : (a : 𝕎 R) → 𝕎 R) x : 𝕎 R) y
have this : IsPoly₂.{u_1} p fun {R : Type u_1} [CommRing R] (x y : 𝕎 R) ↦
  (verschiebung : (a : 𝕎 R) → 𝕎 R) (HMul.hMul (β := 𝕎 R) x ((frobenius : (a : 𝕎 R) → 𝕎 R) y : 𝕎 R))
Tactic: 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))
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Identities (hypothesis)
Goal:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst : CommRing R
x y : 𝕎 R
this :
  IsPoly₂.{u_1} p fun {R : Type u_1} [CommRing R] (x y : 𝕎 R) ↦
    (verschiebung : (a : 𝕎 R) → 𝕎 R) (HMul.hMul (β := 𝕎 R) x ((frobenius : (a : 𝕎 R) → 𝕎 R) y : 𝕎 R))
⊢ (verschiebung : (a : 𝕎 R) → 𝕎 R) (HMul.hMul (β := 𝕎 R) x ((frobenius : (a : 𝕎 R) → 𝕎 R) y : 𝕎 R)) =
    HMul.hMul (α := 𝕎 R) ((verschiebung : (a : 𝕎 R) → 𝕎 R) x : 𝕎 R) y
have this₁ : IsPoly₂.{u_1} p fun {R : Type u_1} [CommRing R] (x y : 𝕎 R) ↦
  HMul.hMul (α := 𝕎 R) ((verschiebung : (a : 𝕎 R) → 𝕎 R) x : 𝕎 R) y
Tactic: have : IsPoly₂ p fun {R} [CommRing R] x y ↦ verschiebung x * y :=
    IsPoly₂.comp (hh := mulIsPoly₂) (hf := verschiebung_isPoly) (hg := idIsPolyI' p)
-- 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
this_1 :
  IsPoly₂.{u_1} p fun {R : Type u_1} [CommRing R] (x y : 𝕎 R) ↦
    (verschiebung : (a : 𝕎 R) → 𝕎 R) (HMul.hMul (β := 𝕎 R) x ((frobenius : (a : 𝕎 R) → 𝕎 R) y : 𝕎 R))
this :
  IsPoly₂.{u_1} p fun {R : Type u_1} [CommRing R] (x y : 𝕎 R) ↦
    HMul.hMul (α := 𝕎 R) ((verschiebung : (a : 𝕎 R) → 𝕎 R) x : 𝕎 R) y
⊢ (verschiebung : (a : 𝕎 R) → 𝕎 R) (HMul.hMul (β := 𝕎 R) x ((frobenius : (a : 𝕎 R) → 𝕎 R) y : 𝕎 R)) =
    HMul.hMul (α := 𝕎 R) ((verschiebung : (a : 𝕎 R) → 𝕎 R) x : 𝕎 R) y
have refine_3 : ∀ (R : Type u_1) [R._inst : CommRing R] (x y : 𝕎 R) (n : ℕ),
  Eq (α := R)
    ((ghostComponent n : (a : 𝕎 R) → R)
        ((verschiebung : (a : 𝕎 R) → 𝕎 R) (HMul.hMul (β := 𝕎 R) x ((frobenius : (a : 𝕎 R) → 𝕎 R) y : 𝕎 R)) : 𝕎 R) :
      R)
    ((ghostComponent n : (a : 𝕎 R) → R) (HMul.hMul (α := 𝕎 R) ((verschiebung : (a : 𝕎 R) → 𝕎 R) x : 𝕎 R) y) : R)
Tactic: ghost_calc x y
Cleared hypotheses: R, inst, x, y
-- 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
⊢ (x * (↑p : 𝕎 R)).coeff 0 = 0
have rw : Eq.{u_1 + 1} (α := R) (coeff (p := p) ((frobenius : (a : 𝕎 R) → 𝕎 R) ((verschiebung : (a : 𝕎 R) → 𝕎 R) x : 𝕎 R)) 0) 0
Tactic: rw [← frobenius_verschiebung, coeff_frobenius_charP, verschiebung_coeff_zero,
    zero_pow hp.out.ne_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
rw :
  Eq.{u_1 + 1} (α := R) (coeff (p := p) ((frobenius : (a : 𝕎 R) → 𝕎 R) ((verschiebung : (a : 𝕎 R) → 𝕎 R) x : 𝕎 R)) 0) 0
⊢ (x * (↑p : 𝕎 R)).coeff 0 = 0
have rw₁ : HPow.hPow (α := R) (coeff (p := p) ((verschiebung : (a : 𝕎 R) → 𝕎 R) x) 0) p = 0
Tactic: rw [← frobenius_verschiebung, coeff_frobenius_charP, verschiebung_coeff_zero,
    zero_pow hp.out.ne_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
rw :
  Eq.{u_1 + 1} (α := R) (coeff (p := p) ((frobenius : (a : 𝕎 R) → 𝕎 R) ((verschiebung : (a : 𝕎 R) → 𝕎 R) x : 𝕎 R)) 0) 0
rw₁ : HPow.hPow (α := R) (coeff (p := p) ((verschiebung : (a : 𝕎 R) → 𝕎 R) x) 0) p = 0
⊢ (x * (↑p : 𝕎 R)).coeff 0 = 0
have rw₂ : HPow.hPow (α := R) 0 p = 0
Tactic: rw [← frobenius_verschiebung, coeff_frobenius_charP, verschiebung_coeff_zero,
    zero_pow hp.out.ne_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
rw :
  Eq.{u_1 + 1} (α := R) (coeff (p := p) ((frobenius : (a : 𝕎 R) → 𝕎 R) ((verschiebung : (a : 𝕎 R) → 𝕎 R) x : 𝕎 R)) 0) 0
rw₁ : HPow.hPow (α := R) (coeff (p := p) ((verschiebung : (a : 𝕎 R) → 𝕎 R) x) 0) p = 0
rw₂ : HPow.hPow (α := R) 0 p = 0
⊢ (x * (↑p : 𝕎 R)).coeff 0 = 0
have rw₃ : Eq.{u_1 + 1} (α := R) 0 0
Tactic: rw [← frobenius_verschiebung, coeff_frobenius_charP, verschiebung_coeff_zero,
    zero_pow hp.out.ne_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
i : ℕ
⊢ (x * (↑p : 𝕎 R)).coeff (i + 1) = x.coeff i ^ p
have rw : coeff (p := p) ((frobenius : (a : 𝕎 R) → 𝕎 R) ((verschiebung : (a : 𝕎 R) → 𝕎 R) x : 𝕎 R)) (i + 1) = x.coeff i ^ p
Tactic: rw [← frobenius_verschiebung, coeff_frobenius_charP, verschiebung_coeff_succ]
-- 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 : ℕ
rw : coeff (p := p) ((frobenius : (a : 𝕎 R) → 𝕎 R) ((verschiebung : (a : 𝕎 R) → 𝕎 R) x : 𝕎 R)) (i + 1) = x.coeff i ^ p
⊢ (x * (↑p : 𝕎 R)).coeff (i + 1) = x.coeff i ^ p
have rw₁ : HPow.hPow (α := R) (coeff (p := p) ((verschiebung : (a : 𝕎 R) → 𝕎 R) x) (i + 1)) p = x.coeff i ^ p
Tactic: rw [← frobenius_verschiebung, coeff_frobenius_charP, verschiebung_coeff_succ]
-- 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 : ℕ
rw : coeff (p := p) ((frobenius : (a : 𝕎 R) → 𝕎 R) ((verschiebung : (a : 𝕎 R) → 𝕎 R) x : 𝕎 R)) (i + 1) = x.coeff i ^ p
rw₁ : HPow.hPow (α := R) (coeff (p := p) ((verschiebung : (a : 𝕎 R) → 𝕎 R) x) (i + 1)) p = x.coeff i ^ p
⊢ (x * (↑p : 𝕎 R)).coeff (i + 1) = x.coeff i ^ p
have rw₂ : x.coeff i ^ p = x.coeff i ^ p
Tactic: rw [← frobenius_verschiebung, coeff_frobenius_charP, verschiebung_coeff_succ]
-- 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 : ∀ {m : ℕ} (h : m < n), (x * HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) n).coeff m = 0
m : ℕ
h : m < n + 1
⊢ (x * HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) (n + 1)).coeff m = 0
have succ : (x * HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) n * (↑p : 𝕎 R)).coeff m = 0
Tactic: rw [pow_succ, ← 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 : ∀ {m : ℕ} (h : m < n), (x * HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) n).coeff m = 0
m' : ℕ
h : m' + 1 < n + 1
⊢ (x * HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) n * (↑p : 𝕎 R)).coeff (m' + 1) = 0
have succ : m' < n
Tactic: rw [mul_charP_coeff_succ, ih, zero_pow hp.out.ne_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 : ℕ
ih : ∀ {m : ℕ} (h : m < n), (x * HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) n).coeff m = 0
m : ℕ
h : m < n + 1
⊢ (x * HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) n * (↑p : 𝕎 R)).coeff m = 0
have succ : ∀ (h : 0 < n + 1), (x * HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) n * (↑p : 𝕎 R)).coeff 0 = 0
Tactic: cases m with
    | zero => exact mul_charP_coeff_zero _
    | succ m' =>
      rw [mul_charP_coeff_succ, ih, zero_pow hp.out.ne_zero]
      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
inst_1 : CharP R p
x : 𝕎 R
n : ℕ
ih : ∀ {m : ℕ} (h : m < n), (x * HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) n).coeff m = 0
m : ℕ
h : m < n + 1
succ : ∀ (h : 0 < n + 1), (x * HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) n * (↑p : 𝕎 R)).coeff 0 = 0
⊢ (x * HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) n * (↑p : 𝕎 R)).coeff m = 0
have succ₁ : ∀ (m' : ℕ) (h : m' + 1 < n + 1), (x * HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) n * (↑p : 𝕎 R)).coeff (m' + 1) = 0
Tactic: cases m with
    | zero => exact mul_charP_coeff_zero _
    | succ m' =>
      rw [mul_charP_coeff_succ, ih, zero_pow hp.out.ne_zero]
      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
inst_1 : CharP R p
x : 𝕎 R
m n : ℕ
h : m < n
⊢ (x * HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) n).coeff m = 0
have zero : ∀ {m : ℕ} (h : m < 0), (x * HPow.hPow (α := 𝕎 R) (β := ℕ) (↑p : 𝕎 R) 0).coeff m = 0
Tactic: induction n generalizing m with
  | zero => contradiction
  | succ n ih =>
    rw [pow_succ, ← mul_assoc]
    cases m with
    | zero => exact mul_charP_coeff_zero _
    | succ m' =>
      rw [mul_charP_coeff_succ, ih, zero_pow hp.out.ne_zero]
      simpa using h
Cleared hypotheses: m, n, 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
inst_1 : CharP R p
x : 𝕎 R
m n : ℕ
h : m < n
zero : ∀ {m : ℕ} (h : m < 0), (x * HPow.hPow (α := 𝕎 R) (β := ℕ) (↑p : 𝕎 R) 0).coeff m = 0
⊢ (x * HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) n).coeff m = 0
have succ : ∀ (n : ℕ) (ih : ∀ {m : ℕ} (h : m < n), (x * HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) n).coeff m = 0) {m : ℕ} (h : m < n + 1),
  (x * HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) (n + 1)).coeff m = 0
Tactic: induction n generalizing m with
  | zero => contradiction
  | succ n ih =>
    rw [pow_succ, ← mul_assoc]
    cases m with
    | zero => exact mul_charP_coeff_zero _
    | succ m' =>
      rw [mul_charP_coeff_succ, ih, zero_pow hp.out.ne_zero]
      simpa using h
Cleared hypotheses: m, n, 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
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 + 1)).coeff (m + (n + 1)) = x.coeff m ^ p ^ (n + 1)
have succ : (x * HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) n).coeff (m + n) ^ p = (x.coeff m ^ p ^ n) ^ p
Tactic: rw [pow_succ, ← mul_assoc, ← add_assoc, mul_charP_coeff_succ, pow_succ, pow_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 : 𝕎 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) ^ p = (x.coeff m ^ p ^ n) ^ p
have succ : (x * HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) n).coeff (m + n) = x.coeff m ^ p ^ n
Tactic: congr
-- 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
m n : ℕ
⊢ (x * HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) n).coeff (m + n) = x.coeff m ^ p ^ n
have zero : ∀ {m : ℕ}, (x * HPow.hPow (α := 𝕎 R) (β := ℕ) (↑p : 𝕎 R) 0).coeff (m + 0) = x.coeff m ^ HPow.hPow (β := ℕ) p 0
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
Cleared hypotheses: m, 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
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
⊢ (x * HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) n).coeff (m + n) = x.coeff m ^ p ^ n
have 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)
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
Cleared hypotheses: m, 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
inst_1 : CharP R p
x : 𝕎 R
⊢ (verschiebung : (a : 𝕎 R) → 𝕎 R) ((frobenius : (a : 𝕎 R) → 𝕎 R) x : 𝕎 R) = x * (↑p : 𝕎 R)
have h : coeff (p := p) ((verschiebung : (a : 𝕎 R) → 𝕎 R) ((frobenius : (a : 𝕎 R) → 𝕎 R) x : 𝕎 R)) 0 = (x * (↑p : 𝕎 R)).coeff 0
Tactic: ext ⟨i⟩