awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.WittVector.Basic
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
⊢ ((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]
-- Module: Mathlib.RingTheory.WittVector.Basic
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)
⊢ n + 1 = n - i + 1 + i

Tactic:
lia
-- Module: Mathlib.RingTheory.WittVector.Basic
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 :
  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)
⊢ 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:
rw [this, show n + 1 = (n - i) + 1 + i by lia, pow_add, mul_comm]

Premises used: pow_add, mul_comm
-- Module: Mathlib.RingTheory.WittVector.Basic
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
h₁ : n - i + 1 ≤ 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)

Tactic:
gcongr
-- Module: Mathlib.RingTheory.WittVector.Basic
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)
⊢ (↑p : R) ∣ x.coeff i

Tactic:
hx i (Nat.le_of_lt_succ hi)

Premises used: Nat.le_of_lt_succ
-- Module: Mathlib.RingTheory.WittVector.Basic
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)
⊢ (↑p : R) ∣ x.coeff i

Tactic:
exact hx i (Nat.le_of_lt_succ hi)

Premises used: Nat.le_of_lt_succ
-- Module: Mathlib.RingTheory.WittVector.Basic
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)
⊢ n - i + 1 ≤ p ^ (n - i)

Tactic:
((n - i).lt_two_pow_self).succ_le.trans
        (pow_left_mono (n - i) (Nat.Prime.two_le Fact.out))

Premises used: Order.succ, HSub.hSub, pow_left_mono, Nat.lt_two_pow_self, Nat.Prime.two_le, LT.lt.succ_le, LE.le.trans, Fact.out
-- Module: Mathlib.RingTheory.WittVector.Basic
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)
⊢ n - i + 1 ≤ p ^ (n - i)

Tactic:
exact ((n - i).lt_two_pow_self).succ_le.trans
        (pow_left_mono (n - i) (Nat.Prime.two_le Fact.out))

Premises used: HSub.hSub, pow_left_mono, Nat.lt_two_pow_self, Nat.Prime.two_le, LT.lt.succ_le, LE.le.trans, Fact.out
-- Module: Mathlib.RingTheory.WittVector.Basic
Goal:
p : ℕ
R : Type u_1
inst : CommRing R
inst_1 : Fact (Nat.Prime p)
x : 𝕎 R
n : ℕ
⊢ Eq (α := R) ((ghostMap : (a : 𝕎 R) → ℕ → R) x n : R) ((ghostComponent n : (a : 𝕎 R) → R) x : R)

Tactic:
rfl

Premises used: Multiset.sum, Multiset.foldr, Finsupp.sum, MvPolynomial.eval₂, _private.0.WittVector.ghostFun, Finset.sum, rfl
-- Module: Mathlib.RingTheory.WittVector.Basic
Goal:
p : ℕ
R : Type u_1
inst : CommRing R
inst_1 : Fact (Nat.Prime p)
inst_2 : Invertible (α := R) (↑p : R)
⊢ Eq (α := 𝕎 R →+* ℕ → R) (↑(ghostEquiv p R) : 𝕎 R →+* ℕ → R) ghostMap

Tactic:
rfl

Premises used: Multiset.sum, Multiset.foldr, Finsupp.sum, MvPolynomial.eval₂, MonoidHomClass.toMonoidHom, RingHomClass.toRingHom, WittVector.ghostMap, _private.0.WittVector.ghostFun, Finset.sum, rfl
-- Module: Mathlib.RingTheory.WittVector.Basic
Goal:
p : ℕ
R : Type u_1
inst : CommRing R
inst_1 : Fact (Nat.Prime p)
inst_2 : Invertible (α := R) (↑p : R)
⊢ Bijective.{u_1 + 1, u_1 + 1} (α := 𝕎 R) (β := ℕ → R) (⇑ghostMap : (a : 𝕎 R) → ℕ → R)

Tactic:
(ghostEquiv p R).bijective

Premises used: Multiset.sum, Multiset.foldr, Finsupp.sum, WittVector.ghostEquiv, MvPolynomial.eval₂, _private.0.WittVector.ghostFun, RingEquiv.bijective, Finset.sum
-- Module: Mathlib.RingTheory.WittVector.Basic
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 : Fact (Nat.Prime p)
⊢ Eq.{u_1 + 1} (α := R) (coeff (p := p) 1 0) 1

Tactic:
simp
-- Module: Mathlib.RingTheory.WittVector.Basic
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 : Fact (Nat.Prime p)
⊢ Eq.{u_1 + 1} (α := R) (coeff (p := p) 0 0) 0

Tactic:
simp
-- Module: Mathlib.RingTheory.WittVector.Basic
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 : Fact (Nat.Prime p)
inst_3 : Nontrivial R
⊢ Nontrivial.{u_1} (𝕎 R)

Tactic:
constantCoeff.domain_nontrivial

Premises used: WittVector.constantCoeff, RingHom.domain_nontrivial
-- Module: Mathlib.RingTheory.WittVector.Compare
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
contrapose! : ∀ (hpi : i ≠ n), HPow.hPow (α := TruncatedWittVector p n R) (↑p : TruncatedWittVector p n R) i ≠ 0
⊢ i = n

Tactic:
contrapose! hpi
-- Module: Mathlib.RingTheory.WittVector.Compare
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
⊢ i < n

Tactic:
replace hin := lt_of_le_of_ne hin hpi
-- Module: Mathlib.RingTheory.WittVector.Compare
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
rw₁ 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
⊢ 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:
rw [map_pow, map_natCast]

Premises used: map_pow, map_natCast
-- Module: Mathlib.RingTheory.WittVector.Compare
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)

Tactic:
have : (p : TruncatedWittVector p n R) ^ i = WittVector.truncate n ((p : 𝕎 R) ^ i) := by
    rw [map_pow, map_natCast]
-- Module: Mathlib.RingTheory.WittVector.Compare
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)
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)
⊢ HPow.hPow (α := TruncatedWittVector p n R) (↑p : TruncatedWittVector p n R) i ≠ 0

Tactic:
rw [this, ne_eq, TruncatedWittVector.ext_iff, not_forall]

Premises used: ne_eq, TruncatedWittVector.ext_iff, Classical.not_forall
-- Module: Mathlib.RingTheory.WittVector.Compare
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
R : Type u_1
inst : CommRing R
inst_1 : CharP R p
i : ℕ
hin : i < n
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)
⊢ ∃ (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:
use ⟨i, hin⟩
-- Module: Mathlib.RingTheory.WittVector.Compare
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
R : Type u_1
inst : CommRing R
inst_1 : CharP R p
i : ℕ
hin : i < n
h : ¬Eq.{u_1 + 1} (α := R) 1 0
⊢ ¬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:
rw [WittVector.coeff_truncate, coeff_zero, Fin.val_mk, WittVector.coeff_p_pow]

Premises used: WittVector.coeff_truncate, Fin.val_mk, TruncatedWittVector.coeff_zero, WittVector.coeff_p_pow
-- Module: Mathlib.RingTheory.WittVector.Compare
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
R : Type u_1
inst : CommRing R
inst_1 : CharP R p
i : ℕ
hin : i < n
⊢ Nontrivial R

Tactic:
haveI : Nontrivial R := CharP.nontrivial_of_char_ne_one hp.1.ne_one
-- Module: Mathlib.RingTheory.WittVector.Compare
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 : Nontrivial R
⊢ ¬Eq.{u_1 + 1} (α := R) 1 0

Tactic:
one_ne_zero

Premises used: one_ne_zero
-- Module: Mathlib.RingTheory.WittVector.Compare
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 : Nontrivial R
⊢ ¬Eq.{u_1 + 1} (α := R) 1 0

Tactic:
exact one_ne_zero

Premises used: one_ne_zero
-- Module: Mathlib.RingTheory.WittVector.Compare
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
rw : Fintype.card (ZMod p) ^ n = p ^ n
rw₁ rw₂ : p ^ n = p ^ n
⊢ Fintype.card (TruncatedWittVector p n (ZMod p)) = p ^ n

Tactic:
rw [card, ZMod.card]

Premises used: TruncatedWittVector.card, ZMod.card
-- Module: Mathlib.RingTheory.WittVector.Compare
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ CharP (TruncatedWittVector p n (ZMod p)) (p ^ n)

Tactic:
charP_of_prime_pow_injective _ _ _ (card_zmod _ _) (eq_of_le_of_cast_pow_eq_zero p n (ZMod p))

Premises used: TruncatedWittVector.eq_of_le_of_cast_pow_eq_zero, ZMod, TruncatedWittVector.card_zmod, charP_of_prime_pow_injective
-- Module: Mathlib.RingTheory.WittVector.Compare
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
R : Type u_1
inst : CommRing R
x : ZMod (p ^ n)
⊢ p ^ n ∣ p ^ n

Tactic:
rfl
-- Module: Mathlib.RingTheory.WittVector.Compare
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
x : ZMod (p ^ n)
⊢ Eq (α := TruncatedWittVector p n (ZMod p))
    ((zmodEquivTrunc p n : (a : ZMod (p ^ n)) → TruncatedWittVector p n (ZMod p)) x : TruncatedWittVector p n (ZMod p))
    ((ZMod.castHom ⋯ (TruncatedWittVector p n (ZMod p)) : (a : ZMod (p ^ n)) → TruncatedWittVector p n (ZMod p)) x :
      TruncatedWittVector p n (ZMod p))

Tactic:
rfl

Premises used: ZMod.cast, rfl
-- Module: Mathlib.RingTheory.WittVector.Compare
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n m : ℕ
hm : n ≤ m
⊢ Eq (α := ZMod (p ^ m) →+* TruncatedWittVector p n (ZMod p))
    (RingHom.comp (truncate hm) (RingEquiv.toRingHom (zmodEquivTrunc p m)))
    (@RingHom.comp _ (ZMod (p ^ n)) _ _ Semiring.toNonAssocSemiring _ (RingEquiv.toRingHom (zmodEquivTrunc p n))
      (ZMod.castHom ⋯ (ZMod (p ^ n))))

Tactic:
RingHom.ext_zmod _ _

Premises used: RingHom.ext_zmod
-- Module: Mathlib.RingTheory.WittVector.Compare
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n m : ℕ
hm : n ≤ m
x : ZMod (p ^ m)
rw :
  Eq (α := TruncatedWittVector p n (ZMod p))
    ((@RingHom.comp _ (ZMod (p ^ n)) _ _ Semiring.toNonAssocSemiring _ (RingEquiv.toRingHom (zmodEquivTrunc p n))
            (ZMod.castHom ⋯ (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 ⋯ (ZMod (p ^ n)) : (a : ZMod (p ^ m)) → ZMod (p ^ n)) x : ZMod (p ^ n)) :
      TruncatedWittVector p n (ZMod p))
⊢ 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))

Tactic:
rw [commutes _ _ hm]

Premises used: TruncatedWittVector.commutes
-- Module: Mathlib.RingTheory.WittVector.Compare
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n m : ℕ
hm : n ≤ m
x : ZMod (p ^ m)
⊢ Eq (α := TruncatedWittVector p n (ZMod p))
    ((@RingHom.comp _ (ZMod (p ^ n)) _ _ Semiring.toNonAssocSemiring _ (RingEquiv.toRingHom (zmodEquivTrunc p n))
            (ZMod.castHom ⋯ (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 ⋯ (ZMod (p ^ n)) : (a : ZMod (p ^ m)) → ZMod (p ^ n)) x : ZMod (p ^ n)) :
      TruncatedWittVector p n (ZMod p))

Tactic:
rfl
-- Module: Mathlib.RingTheory.WittVector.Compare
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n m : ℕ
hm : n ≤ m
x : TruncatedWittVector p m (ZMod p)
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 ⋯ (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))
⊢ 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))

Tactic:
apply (zmodEquivTrunc p n).injective

Premises used: RingEquiv.injective, TruncatedWittVector.zmodEquivTrunc
-- Module: Mathlib.RingTheory.WittVector.Compare
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n m : ℕ
hm : n ≤ m
x : TruncatedWittVector p m (ZMod p)
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))
⊢ 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))

Tactic:
rw [← commutes' _ _ hm]

Premises used: TruncatedWittVector.commutes'
-- Module: Mathlib.RingTheory.WittVector.Compare
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))
    ((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:
simp
-- Module: Mathlib.RingTheory.WittVector.Compare
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n m : ℕ
hm : n ≤ m
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 ⋯ (ZMod (p ^ n))) (RingEquiv.toRingHom (RingEquiv.symm (zmodEquivTrunc p m))) :
            (a : TruncatedWittVector p m (ZMod p)) → ZMod (p ^ n))
          x :
        ZMod (p ^ n))
⊢ 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))))

Tactic:
ext
-- Module: Mathlib.RingTheory.WittVector.Compare
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n m : ℕ
hm : n ≤ m
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 ⋯ (ZMod (p ^ n))) (RingEquiv.toRingHom (RingEquiv.symm (zmodEquivTrunc p m))) :
          (a : TruncatedWittVector p m (ZMod p)) → ZMod (p ^ n))
        x :
      ZMod (p ^ n))

Tactic:
apply commutes_symm'

Premises used: TruncatedWittVector.commutes_symm'
-- Module: Mathlib.RingTheory.WittVector.Compare
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))
rw₁ 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 (ZMod.castHom ⋯ (ZMod (p ^ m)))
      (RingHom.comp (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))

Tactic:
rw [commutes_symm, RingHom.comp_assoc]

Premises used: RingHom.comp_assoc, TruncatedWittVector.commutes_symm
-- Module: Mathlib.RingTheory.WittVector.Compare
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
m n : ℕ
h : m ≤ n
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))
rw₁ rw₂ :
  Eq (α := 𝕎 (ZMod p) →+* ZMod (p ^ m))
    (RingHom.comp (RingEquiv.toRingHom (RingEquiv.symm (zmodEquivTrunc p m))) (truncate m))
    (RingHom.comp (RingEquiv.toRingHom (RingEquiv.symm (zmodEquivTrunc p m))) (truncate m))
⊢ 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))

Tactic:
rw [RingHom.comp_assoc, truncate_comp_wittVector_truncate]

Premises used: RingHom.comp_assoc, TruncatedWittVector.truncate_comp_wittVector_truncate