awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Basic (goal)
Goal:
p : ℕ
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
α : Type u_3
β : Type u_4
inst_2 : Invertible (α := R) (↑p : R)
x : ℕ → R
⊢ ghostFun (p := p)
      ((fun (x : ℕ → R) ↦ (mk p fun (n : ℕ) ↦ (aeval x : (a : MvPolynomial ℕ R) → R) (xInTermsOfW p R n) : 𝕎 R)) x) =
    x
have h : ∀ (n : ℕ),
  ghostFun (p := p)
      ((fun (x : ℕ → R) ↦ (mk p fun (n : ℕ) ↦ (aeval x : (a : MvPolynomial ℕ R) → R) (xInTermsOfW p R n) : 𝕎 R)) x) n =
    x n
Tactic: ext n
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Basic (hypothesis)
Goal:
p : ℕ
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
α : Type u_3
β : Type u_4
inst_2 : Invertible (α := R) (↑p : R)
x : ℕ → R
n : ℕ
⊢ ghostFun (p := p)
      ((fun (x : ℕ → R) ↦ (mk p fun (n : ℕ) ↦ (aeval x : (a : MvPolynomial ℕ R) → R) (xInTermsOfW p R n) : 𝕎 R)) x) n =
    x n
have this : Eq (α := MvPolynomial ℕ R)
  ((bind₁ (xInTermsOfW p R) : (a : MvPolynomial ℕ R) → MvPolynomial ℕ R) (W_ R n) : MvPolynomial ℕ R)
  (X n : MvPolynomial ℕ R)
Tactic: have := bind₁_xInTermsOfW_wittPolynomial p R n
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Basic (hypothesis)
Goal:
p : ℕ
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
α : Type u_3
β : Type u_4
inst_2 : Invertible (α := R) (↑p : R)
x : ℕ → R
n : ℕ
this :
  Eq (α := MvPolynomial ℕ R)
    ((bind₁ (xInTermsOfW p R) : (a : MvPolynomial ℕ R) → MvPolynomial ℕ R) (W_ R n) : MvPolynomial ℕ R)
    (X n : MvPolynomial ℕ R)
⊢ ghostFun (p := p)
      ((fun (x : ℕ → R) ↦ (mk p fun (n : ℕ) ↦ (aeval x : (a : MvPolynomial ℕ R) → R) (xInTermsOfW p R n) : 𝕎 R)) x) n =
    x n
have this₁ : Eq (α := R)
  ((aeval x : (a : MvPolynomial ℕ R) → R)
      ((bind₁ (xInTermsOfW p R) : (a : MvPolynomial ℕ R) → MvPolynomial ℕ R) (W_ R n) : MvPolynomial ℕ R) :
    R)
  ((aeval x : (a : MvPolynomial ℕ R) → R) (X n) : R)
Tactic: apply_fun aeval x at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Basic (goal)
Goal:
p : ℕ
R : Type u_1
inst : CommRing R
inst_1 : Fact (Nat.Prime p)
⊢ Eq (α := 𝕎 R →+* 𝕎 R) (map (RingHom.id R)) (RingHom.id (𝕎 R))
have a : ∀ (x : 𝕎 R) (n : ℕ),
  Eq.{u_1 + 1} (α := R) (coeff (p := p) ((map (RingHom.id R) : (a : 𝕎 R) → 𝕎 R) x) n)
    (coeff (p := p) ((RingHom.id (𝕎 R) : (a : 𝕎 R) → 𝕎 R) x) n)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Basic (goal)
Goal:
p : ℕ
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Fact (Nat.Prime p)
f : R →+* S
x : 𝕎 R
⊢ Eq.{u_2 + 1} (α := 𝕎 S) (((map f : RingHom.{u_1, u_2} (𝕎 R) (𝕎 S)) : (a : 𝕎 R) → 𝕎 S) x : 𝕎 S) (0 : 𝕎 S) ↔
    ∀ (n : ℕ), Eq.{u_2 + 1} (α := S) ((f : (a : R) → S) (x.coeff n) : S) (0 : S)
have refine_1 : ∀ (h : Eq.{u_2 + 1} (α := 𝕎 S) (((map f : RingHom.{u_1, u_2} (𝕎 R) (𝕎 S)) : (a : 𝕎 R) → 𝕎 S) x : 𝕎 S) (0 : 𝕎 S))
  (n : ℕ), Eq.{u_2 + 1} (α := S) ((f : (a : R) → S) (x.coeff n) : S) (0 : S)
Tactic: refine ⟨fun h n ↦ ?_, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Basic (goal)
Goal:
p : ℕ
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Fact (Nat.Prime p)
f : R →+* S
x : 𝕎 R
refine_1 :
  ∀ (h : Eq.{u_2 + 1} (α := 𝕎 S) (((map f : RingHom.{u_1, u_2} (𝕎 R) (𝕎 S)) : (a : 𝕎 R) → 𝕎 S) x : 𝕎 S) (0 : 𝕎 S))
    (n : ℕ), Eq.{u_2 + 1} (α := S) ((f : (a : R) → S) (x.coeff n) : S) (0 : S)
⊢ Eq.{u_2 + 1} (α := 𝕎 S) (((map f : RingHom.{u_1, u_2} (𝕎 R) (𝕎 S)) : (a : 𝕎 R) → 𝕎 S) x : 𝕎 S) (0 : 𝕎 S) ↔
    ∀ (n : ℕ), Eq.{u_2 + 1} (α := S) ((f : (a : R) → S) (x.coeff n) : S) (0 : S)
have refine_2 : ∀ (h : ∀ (n : ℕ), Eq.{u_2 + 1} (α := S) ((f : (a : R) → S) (x.coeff n) : S) (0 : S)),
  Eq.{u_2 + 1} (α := 𝕎 S) (((map f : RingHom.{u_1, u_2} (𝕎 R) (𝕎 S)) : (a : 𝕎 R) → 𝕎 S) x : 𝕎 S) (0 : 𝕎 S)
Tactic: refine ⟨fun h n ↦ ?_, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Basic (hypothesis)
Goal:
p : ℕ
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Fact (Nat.Prime p)
f : R →+* S
x : 𝕎 R
h : Eq.{u_2 + 1} (α := 𝕎 S) (((map f : RingHom.{u_1, u_2} (𝕎 R) (𝕎 S)) : (a : 𝕎 R) → 𝕎 S) x : 𝕎 S) (0 : 𝕎 S)
n : ℕ
⊢ Eq.{u_2 + 1} (α := S) ((f : (a : R) → S) (x.coeff n) : S) (0 : S)
have h₁ : Eq.{u_2 + 1} (α := S) (coeff (p := p) (((map f : RingHom.{u_1, u_2} (𝕎 R) (𝕎 S)) : (a : 𝕎 R) → 𝕎 S) x) n)
  (coeff (p := p) 0 n)
Tactic: apply_fun (·.coeff n) at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Basic (goal)
Goal:
p : ℕ
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Fact (Nat.Prime p)
f : R →+* S
x : 𝕎 R
h : ∀ (n : ℕ), Eq.{u_2 + 1} (α := S) ((f : (a : R) → S) (x.coeff n) : S) (0 : S)
⊢ Eq.{u_2 + 1} (α := 𝕎 S) (((map f : RingHom.{u_1, u_2} (𝕎 R) (𝕎 S)) : (a : 𝕎 R) → 𝕎 S) x : 𝕎 S) (0 : 𝕎 S)
have refine_2 : ∀ (n : ℕ),
  Eq.{u_2 + 1} (α := S) (coeff (p := p) (((map f : RingHom.{u_1, u_2} (𝕎 R) (𝕎 S)) : (a : 𝕎 R) → 𝕎 S) x) n)
    (coeff (p := p) 0 n)
Tactic: ext n
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Basic (goal)
Goal:
p : ℕ
R : Type u_1
inst : CommRing R
inst_1 : Fact (Nat.Prime p)
x : 𝕎 R
n : ℕ
hx : ∀ i ≤ n, (↑p : R) ∣ x.coeff i
⊢ HPow.hPow (α := R) (↑p : R) (n + 1) ∣ (ghostComponent n : (a : 𝕎 R) → R) x
have rw : HPow.hPow (α := R) (↑p : R) (n + 1) ∣
  ∑ i ∈ Finset.range (n + 1),
    ((aeval (R := ℤ) x.coeff : MvPolynomial ℕ ℤ →ₐ[ℤ] R) : (a : MvPolynomial ℕ ℤ) → R)
      ((monomial (Finsupp.single i (p ^ (n - i))) : (a : ℤ) → MvPolynomial ℕ ℤ) (HPow.hPow (α := ℤ) (↑p : ℤ) i) :
        MvPolynomial ℕ ℤ)
Tactic: rw [WittVector.ghostComponent_apply, wittPolynomial, MvPolynomial.aeval_sum]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Basic (goal)
Goal:
p : ℕ
R : Type u_1
inst : CommRing R
inst_1 : Fact (Nat.Prime p)
x : 𝕎 R
n : ℕ
hx : ∀ i ≤ n, (↑p : R) ∣ x.coeff i
⊢ HPow.hPow (α := R) (↑p : R) (n + 1) ∣
    ∑ i ∈ Finset.range (n + 1),
      ((aeval (R := ℤ) x.coeff : MvPolynomial ℕ ℤ →ₐ[ℤ] R) : (a : MvPolynomial ℕ ℤ) → R)
        ((monomial (Finsupp.single i (p ^ (n - i))) : (a : ℤ) → MvPolynomial ℕ ℤ) (HPow.hPow (α := ℤ) (↑p : ℤ) i) :
          MvPolynomial ℕ ℤ)
have h : ∀ i ∈ Finset.range (n + 1),
  HPow.hPow (α := R) (↑p : R) (n + 1) ∣
    ((aeval (R := ℤ) x.coeff : MvPolynomial ℕ ℤ →ₐ[ℤ] R) : (a : MvPolynomial ℕ ℤ) → R)
      ((monomial (Finsupp.single i (p ^ (n - i))) : (a : ℤ) → MvPolynomial ℕ ℤ) (HPow.hPow (α := ℤ) (↑p : ℤ) i) :
        MvPolynomial ℕ ℤ)
Tactic: apply Finset.dvd_sum
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Basic (hypothesis)
Goal:
p : ℕ
R : Type u_1
inst : CommRing R
inst_1 : Fact (Nat.Prime p)
x : 𝕎 R
n : ℕ
hx : ∀ i ≤ n, (↑p : R) ∣ x.coeff i
i : ℕ
hi : i ∈ Finset.range (n + 1)
⊢ HPow.hPow (α := R) (↑p : R) (n + 1) ∣
    ((aeval (R := ℤ) x.coeff : MvPolynomial ℕ ℤ →ₐ[ℤ] R) : (a : MvPolynomial ℕ ℤ) → R)
      ((monomial (Finsupp.single i (p ^ (n - i))) : (a : ℤ) → MvPolynomial ℕ ℤ) (HPow.hPow (α := ℤ) (↑p : ℤ) i) :
        MvPolynomial ℕ ℤ)
have hi₁ : i < n + 1
Tactic: simp only [Finset.mem_range] at hi
Cleared hypotheses: hi
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Basic (hypothesis)
Goal:
p : ℕ
R : Type u_1
inst : CommRing R
inst_1 : Fact (Nat.Prime p)
x : 𝕎 R
n : ℕ
hx : ∀ i ≤ n, (↑p : R) ∣ x.coeff i
i : ℕ
hi : i < n + 1
⊢ HPow.hPow (α := R) (↑p : R) (n + 1) ∣
    ((aeval (R := ℤ) x.coeff : MvPolynomial ℕ ℤ →ₐ[ℤ] R) : (a : MvPolynomial ℕ ℤ) → R)
      ((monomial (Finsupp.single i (p ^ (n - i))) : (a : ℤ) → MvPolynomial ℕ ℤ) (HPow.hPow (α := ℤ) (↑p : ℤ) i) :
        MvPolynomial ℕ ℤ)
have this : ((aeval (R := ℤ) x.coeff : MvPolynomial ℕ ℤ →ₐ[ℤ] R) : (a : MvPolynomial ℕ ℤ) → R)
    ((monomial (Finsupp.single i (p ^ (n - i))) : (a : ℤ) → MvPolynomial ℕ ℤ) (HPow.hPow (α := ℤ) (↑p : ℤ) i) :
      MvPolynomial ℕ ℤ) =
  HPow.hPow (α := R) (↑p : R) i * x.coeff i ^ p ^ (n - i)
Tactic: have : (MvPolynomial.aeval x.coeff) ((MvPolynomial.monomial (R := ℤ)
      (Finsupp.single i (p ^ (n - i)))) (p ^ i)) = ((p : R) ^ i) * (x.coeff i) ^ (p ^ (n - i)) := by
    simp [MvPolynomial.aeval_monomial, map_pow]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Basic (goal)
Goal:
p : ℕ
R : Type u_1
inst : CommRing R
inst_1 : Fact (Nat.Prime p)
x : 𝕎 R
n : ℕ
hx : ∀ i ≤ n, (↑p : R) ∣ x.coeff i
i : ℕ
hi : i < n + 1
this :
  ((aeval (R := ℤ) x.coeff : MvPolynomial ℕ ℤ →ₐ[ℤ] R) : (a : MvPolynomial ℕ ℤ) → R)
      ((monomial (Finsupp.single i (p ^ (n - i))) : (a : ℤ) → MvPolynomial ℕ ℤ) (HPow.hPow (α := ℤ) (↑p : ℤ) i) :
        MvPolynomial ℕ ℤ) =
    HPow.hPow (α := R) (↑p : R) i * x.coeff i ^ p ^ (n - i)
⊢ HPow.hPow (α := R) (↑p : R) (n + 1) ∣
    ((aeval (R := ℤ) x.coeff : MvPolynomial ℕ ℤ →ₐ[ℤ] R) : (a : MvPolynomial ℕ ℤ) → R)
      ((monomial (Finsupp.single i (p ^ (n - i))) : (a : ℤ) → MvPolynomial ℕ ℤ) (HPow.hPow (α := ℤ) (↑p : ℤ) i) :
        MvPolynomial ℕ ℤ)
have h : HPow.hPow (α := R) (↑p : R) i * HPow.hPow (α := R) (↑p : R) (n - i + 1) ∣
  HPow.hPow (α := R) (↑p : R) i * x.coeff i ^ p ^ (n - i)
Tactic: rw [this, show n + 1 = (n - i) + 1 + i by lia, pow_add, mul_comm]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Basic (goal)
Goal:
p : ℕ
R : Type u_1
inst : CommRing R
inst_1 : Fact (Nat.Prime p)
x : 𝕎 R
n : ℕ
hx : ∀ i ≤ n, (↑p : R) ∣ x.coeff i
i : ℕ
hi : i < n + 1
this :
  ((aeval (R := ℤ) x.coeff : MvPolynomial ℕ ℤ →ₐ[ℤ] R) : (a : MvPolynomial ℕ ℤ) → R)
      ((monomial (Finsupp.single i (p ^ (n - i))) : (a : ℤ) → MvPolynomial ℕ ℤ) (HPow.hPow (α := ℤ) (↑p : ℤ) i) :
        MvPolynomial ℕ ℤ) =
    HPow.hPow (α := R) (↑p : R) i * x.coeff i ^ p ^ (n - i)
⊢ HPow.hPow (α := R) (↑p : R) i * HPow.hPow (α := R) (↑p : R) (n - i + 1) ∣
    HPow.hPow (α := R) (↑p : R) i * x.coeff i ^ p ^ (n - i)
have h : (↑p : R) ∣ x.coeff i
Tactic: gcongr
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Basic (goal)
Goal:
p : ℕ
R : Type u_1
inst : CommRing R
inst_1 : Fact (Nat.Prime p)
x : 𝕎 R
n : ℕ
hx : ∀ i ≤ n, (↑p : R) ∣ x.coeff i
i : ℕ
hi : i < n + 1
this :
  ((aeval (R := ℤ) x.coeff : MvPolynomial ℕ ℤ →ₐ[ℤ] R) : (a : MvPolynomial ℕ ℤ) → R)
      ((monomial (Finsupp.single i (p ^ (n - i))) : (a : ℤ) → MvPolynomial ℕ ℤ) (HPow.hPow (α := ℤ) (↑p : ℤ) i) :
        MvPolynomial ℕ ℤ) =
    HPow.hPow (α := R) (↑p : R) i * x.coeff i ^ p ^ (n - i)
h : (↑p : R) ∣ x.coeff i
⊢ HPow.hPow (α := R) (↑p : R) i * HPow.hPow (α := R) (↑p : R) (n - i + 1) ∣
    HPow.hPow (α := R) (↑p : R) i * x.coeff i ^ p ^ (n - i)
have h₁ : n - i + 1 ≤ p ^ (n - i)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Compare (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
R : Type u_1
inst : CommRing R
inst_1 : CharP R p
i : ℕ
hin : i ≤ n
hpi : HPow.hPow (α := TruncatedWittVector p n R) (↑p : TruncatedWittVector p n R) i = 0
⊢ i = n
have contrapose! : ∀ (hpi : i ≠ n), HPow.hPow (α := TruncatedWittVector p n R) (↑p : TruncatedWittVector p n R) i ≠ 0
Tactic: contrapose! hpi
Cleared hypotheses: hpi
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Compare (hypothesis)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
R : Type u_1
inst : CommRing R
inst_1 : CharP R p
i : ℕ
hin : i ≤ n
hpi : i ≠ n
⊢ HPow.hPow (α := TruncatedWittVector p n R) (↑p : TruncatedWittVector p n R) i ≠ 0
have hin₁ : i < n
Tactic: replace hin := lt_of_le_of_ne hin hpi
Cleared hypotheses: hin
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Compare (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
R : Type u_1
inst : CommRing R
inst_1 : CharP R p
i : ℕ
hin : i < n
⊢ HPow.hPow (α := TruncatedWittVector p n R) (↑p : TruncatedWittVector p n R) i =
    (WittVector.truncate n : (a : 𝕎 R) → TruncatedWittVector p n R) (HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) i)
have rw : HPow.hPow (α := TruncatedWittVector p n R) (↑p : TruncatedWittVector p n R) i =
  HPow.hPow (α := TruncatedWittVector p n R)
    ((WittVector.truncate n : (a : 𝕎 R) → TruncatedWittVector p n R) (↑p : 𝕎 R) : TruncatedWittVector p n R) i
Tactic: rw [map_pow, map_natCast]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Compare (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
R : Type u_1
inst : CommRing R
inst_1 : CharP R p
i : ℕ
hin : i < n
rw :
  HPow.hPow (α := TruncatedWittVector p n R) (↑p : TruncatedWittVector p n R) i =
    HPow.hPow (α := TruncatedWittVector p n R)
      ((WittVector.truncate n : (a : 𝕎 R) → TruncatedWittVector p n R) (↑p : 𝕎 R) : TruncatedWittVector p n R) i
⊢ HPow.hPow (α := TruncatedWittVector p n R) (↑p : TruncatedWittVector p n R) i =
    (WittVector.truncate n : (a : 𝕎 R) → TruncatedWittVector p n R) (HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) i)
have rw₁ : HPow.hPow (α := TruncatedWittVector p n R) (↑p : TruncatedWittVector p n R) i =
  HPow.hPow (α := TruncatedWittVector p n R) (↑p : TruncatedWittVector p n R) i
Tactic: rw [map_pow, map_natCast]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Compare (hypothesis)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
R : Type u_1
inst : CommRing R
inst_1 : CharP R p
i : ℕ
hin : i < n
⊢ HPow.hPow (α := TruncatedWittVector p n R) (↑p : TruncatedWittVector p n R) i ≠ 0
have this : HPow.hPow (α := TruncatedWittVector p n R) (↑p : TruncatedWittVector p n R) i =
  (WittVector.truncate n : (a : 𝕎 R) → TruncatedWittVector p n R) (HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) i)
Tactic: have : (p : TruncatedWittVector p n R) ^ i = WittVector.truncate n ((p : 𝕎 R) ^ i) := by
    rw [map_pow, map_natCast]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Compare (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
R : Type u_1
inst : CommRing R
inst_1 : CharP R p
i : ℕ
hin : i < n
this :
  HPow.hPow (α := TruncatedWittVector p n R) (↑p : TruncatedWittVector p n R) i =
    (WittVector.truncate n : (a : 𝕎 R) → TruncatedWittVector p n R) (HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) i)
⊢ HPow.hPow (α := TruncatedWittVector p n R) (↑p : TruncatedWittVector p n R) i ≠ 0
have rw : ∃ (x : Fin n),
  ¬Eq.{u_1 + 1} (α := R)
      (coeff (p := p) x
        ((WittVector.truncate n : (a : 𝕎 R) → TruncatedWittVector p n R) (HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) i)))
      (coeff (p := p) x 0)
Tactic: rw [this, ne_eq, TruncatedWittVector.ext_iff, not_forall]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Compare (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
R : Type u_1
inst : CommRing R
inst_1 : CharP R p
i : ℕ
hin : i < n
⊢ ∃ (x : Fin n),
    ¬Eq.{u_1 + 1} (α := R)
        (coeff (p := p) x
          ((WittVector.truncate n : (a : 𝕎 R) → TruncatedWittVector p n R) (HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) i)))
        (coeff (p := p) x 0)
have h : ¬Eq.{u_1 + 1} (α := R)
    (coeff (p := p) (⟨i, hin⟩ : Fin n)
      ((WittVector.truncate n : (a : 𝕎 R) → TruncatedWittVector p n R) (HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) i)))
    (coeff (p := p) (⟨i, hin⟩ : Fin n) 0)
Tactic: use ⟨i, hin⟩
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Compare (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
R : Type u_1
inst : CommRing R
inst_1 : CharP R p
i : ℕ
hin : i < n
⊢ ¬Eq.{u_1 + 1} (α := R)
      (coeff (p := p) (⟨i, hin⟩ : Fin n)
        ((WittVector.truncate n : (a : 𝕎 R) → TruncatedWittVector p n R) (HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) i)))
      (coeff (p := p) (⟨i, hin⟩ : Fin n) 0)
have h : ¬Eq.{u_1 + 1} (α := R) 1 0
Tactic: rw [WittVector.coeff_truncate, coeff_zero, Fin.val_mk, WittVector.coeff_p_pow]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Compare (hypothesis)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
R : Type u_1
inst : CommRing R
inst_1 : CharP R p
i : ℕ
hin : i < n
⊢ ¬Eq.{u_1 + 1} (α := R) 1 0
have this : Nontrivial R
Tactic: haveI : Nontrivial R := CharP.nontrivial_of_char_ne_one hp.1.ne_one
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Compare (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ Fintype.card (TruncatedWittVector p n (ZMod p)) = p ^ n
have rw : Fintype.card (ZMod p) ^ n = p ^ n
Tactic: rw [card, ZMod.card]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Compare (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
rw : Fintype.card (ZMod p) ^ n = p ^ n
⊢ Fintype.card (TruncatedWittVector p n (ZMod p)) = p ^ n
have rw₁ : p ^ n = p ^ n
Tactic: rw [card, ZMod.card]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Compare (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n m : ℕ
hm : n ≤ m
x : ZMod (p ^ m)
⊢ Eq (α := TruncatedWittVector p n (ZMod p))
    ((RingHom.comp (truncate hm) (RingEquiv.toRingHom (zmodEquivTrunc p m)) :
          (a : ZMod (p ^ m)) → TruncatedWittVector p n (ZMod p))
        x :
      TruncatedWittVector p n (ZMod p))
    ((zmodEquivTrunc p n : (a : ZMod (p ^ n)) → TruncatedWittVector p n (ZMod p))
        ((ZMod.castHom ⋯ (ZMod (p ^ n)) : (a : ZMod (p ^ m)) → ZMod (p ^ n)) x : ZMod (p ^ n)) :
      TruncatedWittVector p n (ZMod p))
have rw : Eq (α := TruncatedWittVector p n (ZMod p))
  ((@RingHom.comp _ (ZMod (p ^ n)) _ _ Semiring.toNonAssocSemiring _ (RingEquiv.toRingHom (zmodEquivTrunc p n))
          (ZMod.castHom sorry (ZMod (p ^ n))) :
        (a : ZMod (p ^ m)) → TruncatedWittVector p n (ZMod p))
      x :
    TruncatedWittVector p n (ZMod p))
  ((zmodEquivTrunc p n : (a : ZMod (p ^ n)) → TruncatedWittVector p n (ZMod p))
      ((ZMod.castHom sorry (ZMod (p ^ n)) : (a : ZMod (p ^ m)) → ZMod (p ^ n)) x : ZMod (p ^ n)) :
    TruncatedWittVector p n (ZMod p))
Tactic: rw [commutes _ _ hm]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Compare (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n m : ℕ
hm : n ≤ m
x : TruncatedWittVector p m (ZMod p)
⊢ Eq (α := ZMod (p ^ n))
    ((RingEquiv.symm (zmodEquivTrunc p n) : (a : TruncatedWittVector p n (ZMod p)) → ZMod (p ^ n))
        ((truncate hm : (a : TruncatedWittVector p m (ZMod p)) → TruncatedWittVector p n (ZMod p)) x) :
      ZMod (p ^ n))
    ((ZMod.castHom ⋯ (ZMod (p ^ n)) : (a : ZMod (p ^ m)) → ZMod (p ^ n))
        ((RingEquiv.symm (zmodEquivTrunc p m) : (a : TruncatedWittVector p m (ZMod p)) → ZMod (p ^ m)) x) :
      ZMod (p ^ n))
have a : Eq (α := TruncatedWittVector p n (ZMod p))
  ((zmodEquivTrunc p n : (a : ZMod (p ^ n)) → TruncatedWittVector p n (ZMod p))
      ((RingEquiv.symm (zmodEquivTrunc p n) : (a : TruncatedWittVector p n (ZMod p)) → ZMod (p ^ n))
          ((truncate hm : (a : TruncatedWittVector p m (ZMod p)) → TruncatedWittVector p n (ZMod p)) x) :
        ZMod (p ^ n)) :
    TruncatedWittVector p n (ZMod p))
  ((zmodEquivTrunc p n : (a : ZMod (p ^ n)) → TruncatedWittVector p n (ZMod p))
      ((ZMod.castHom sorry (ZMod (p ^ n)) : (a : ZMod (p ^ m)) → ZMod (p ^ n))
          ((RingEquiv.symm (zmodEquivTrunc p m) : (a : TruncatedWittVector p m (ZMod p)) → ZMod (p ^ m)) x) :
        ZMod (p ^ n)) :
    TruncatedWittVector p n (ZMod p))
Tactic: apply (zmodEquivTrunc p n).injective
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Compare (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n m : ℕ
hm : n ≤ m
x : TruncatedWittVector p m (ZMod p)
⊢ Eq (α := TruncatedWittVector p n (ZMod p))
    ((zmodEquivTrunc p n : (a : ZMod (p ^ n)) → TruncatedWittVector p n (ZMod p))
        ((RingEquiv.symm (zmodEquivTrunc p n) : (a : TruncatedWittVector p n (ZMod p)) → ZMod (p ^ n))
            ((truncate hm : (a : TruncatedWittVector p m (ZMod p)) → TruncatedWittVector p n (ZMod p)) x) :
          ZMod (p ^ n)) :
      TruncatedWittVector p n (ZMod p))
    ((zmodEquivTrunc p n : (a : ZMod (p ^ n)) → TruncatedWittVector p n (ZMod p))
        ((ZMod.castHom ⋯ (ZMod (p ^ n)) : (a : ZMod (p ^ m)) → ZMod (p ^ n))
            ((RingEquiv.symm (zmodEquivTrunc p m) : (a : TruncatedWittVector p m (ZMod p)) → ZMod (p ^ m)) x) :
          ZMod (p ^ n)) :
      TruncatedWittVector p n (ZMod p))
have a : Eq (α := TruncatedWittVector p n (ZMod p))
  ((zmodEquivTrunc p n : (a : ZMod (p ^ n)) → TruncatedWittVector p n (ZMod p))
      ((RingEquiv.symm (zmodEquivTrunc p n) : (a : TruncatedWittVector p n (ZMod p)) → ZMod (p ^ n))
          ((truncate hm : (a : TruncatedWittVector p m (ZMod p)) → TruncatedWittVector p n (ZMod p)) x) :
        ZMod (p ^ n)) :
    TruncatedWittVector p n (ZMod p))
  ((truncate hm : (a : TruncatedWittVector p m (ZMod p)) → TruncatedWittVector p n (ZMod p))
      ((zmodEquivTrunc p m : (a : ZMod (p ^ m)) → TruncatedWittVector p m (ZMod p))
          ((RingEquiv.symm (zmodEquivTrunc p m) : (a : TruncatedWittVector p m (ZMod p)) → ZMod (p ^ m)) x :
            ZMod (p ^ m)) :
        TruncatedWittVector p m (ZMod p)) :
    TruncatedWittVector p n (ZMod p))
Tactic: rw [← commutes' _ _ hm]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Compare (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n m : ℕ
hm : n ≤ m
⊢ Eq (α := TruncatedWittVector p m (ZMod p) →+* ZMod (p ^ n))
    (RingHom.comp (RingEquiv.toRingHom (RingEquiv.symm (zmodEquivTrunc p n))) (truncate hm))
    (RingHom.comp (ZMod.castHom ⋯ (ZMod (p ^ n))) (RingEquiv.toRingHom (RingEquiv.symm (zmodEquivTrunc p m))))
have a : ∀ (x : TruncatedWittVector p m (ZMod p)),
  Eq (α := ZMod (p ^ n))
    ((RingHom.comp (RingEquiv.toRingHom (RingEquiv.symm (zmodEquivTrunc p n))) (truncate hm) :
          (a : TruncatedWittVector p m (ZMod p)) → ZMod (p ^ n))
        x :
      ZMod (p ^ n))
    ((RingHom.comp (ZMod.castHom sorry (ZMod (p ^ n))) (RingEquiv.toRingHom (RingEquiv.symm (zmodEquivTrunc p m))) :
          (a : TruncatedWittVector p m (ZMod p)) → ZMod (p ^ n))
        x :
      ZMod (p ^ n))
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Compare (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
m n : ℕ
h : m ≤ n
⊢ Eq (α := 𝕎 (ZMod p) →+* ZMod (p ^ m))
    (RingHom.comp (ZMod.castHom ⋯ (ZMod (p ^ m)))
      (RingHom.comp (RingEquiv.toRingHom (RingEquiv.symm (zmodEquivTrunc p n))) (truncate n)))
    (RingHom.comp
      (RingHom.comp (RingEquiv.toRingHom (RingEquiv.symm (zmodEquivTrunc p m))) (TruncatedWittVector.truncate h))
      (truncate n))
have rw : Eq (α := 𝕎 (ZMod p) →+* ZMod (p ^ m))
  (RingHom.comp (ZMod.castHom sorry (ZMod (p ^ m)))
    (RingHom.comp (RingEquiv.toRingHom (RingEquiv.symm (zmodEquivTrunc p n))) (truncate n)))
  (RingHom.comp
    (RingHom.comp (ZMod.castHom sorry (ZMod (p ^ m))) (RingEquiv.toRingHom (RingEquiv.symm (zmodEquivTrunc p n))))
    (truncate n))
Tactic: rw [commutes_symm, RingHom.comp_assoc]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Compare (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
m n : ℕ
h : m ≤ n
rw :
  Eq (α := 𝕎 (ZMod p) →+* ZMod (p ^ m))
    (RingHom.comp (ZMod.castHom ⋯ (ZMod (p ^ m)))
      (RingHom.comp (RingEquiv.toRingHom (RingEquiv.symm (zmodEquivTrunc p n))) (truncate n)))
    (RingHom.comp
      (RingHom.comp (ZMod.castHom ⋯ (ZMod (p ^ m))) (RingEquiv.toRingHom (RingEquiv.symm (zmodEquivTrunc p n))))
      (truncate n))
⊢ Eq (α := 𝕎 (ZMod p) →+* ZMod (p ^ m))
    (RingHom.comp (ZMod.castHom ⋯ (ZMod (p ^ m)))
      (RingHom.comp (RingEquiv.toRingHom (RingEquiv.symm (zmodEquivTrunc p n))) (truncate n)))
    (RingHom.comp
      (RingHom.comp (RingEquiv.toRingHom (RingEquiv.symm (zmodEquivTrunc p m))) (TruncatedWittVector.truncate h))
      (truncate n))
have rw₁ : Eq (α := 𝕎 (ZMod p) →+* ZMod (p ^ m))
  (RingHom.comp (ZMod.castHom sorry (ZMod (p ^ m)))
    (RingHom.comp (RingEquiv.toRingHom (RingEquiv.symm (zmodEquivTrunc p n))) (truncate n)))
  (RingHom.comp (ZMod.castHom sorry (ZMod (p ^ m)))
    (RingHom.comp (RingEquiv.toRingHom (RingEquiv.symm (zmodEquivTrunc p n))) (truncate n)))
Tactic: rw [commutes_symm, RingHom.comp_assoc]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Compare (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
m n : ℕ
h : m ≤ n
⊢ Eq (α := 𝕎 (ZMod p) →+* ZMod (p ^ m))
    (RingHom.comp
      (RingHom.comp (RingEquiv.toRingHom (RingEquiv.symm (zmodEquivTrunc p m))) (TruncatedWittVector.truncate h))
      (truncate n))
    (RingHom.comp (RingEquiv.toRingHom (RingEquiv.symm (zmodEquivTrunc p m))) (truncate m))
have rw : Eq (α := 𝕎 (ZMod p) →+* ZMod (p ^ m))
  (RingHom.comp (RingEquiv.toRingHom (RingEquiv.symm (zmodEquivTrunc p m)))
    (RingHom.comp (TruncatedWittVector.truncate h) (truncate n)))
  (RingHom.comp (RingEquiv.toRingHom (RingEquiv.symm (zmodEquivTrunc p m))) (truncate m))
Tactic: rw [RingHom.comp_assoc, truncate_comp_wittVector_truncate]