awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.WittVector.Frobenius
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
rw :
  HPow.hPow (α := MvPolynomial ℕ (ZMod p)) (X n) p +
      HMul.hMul (α := MvPolynomial ℕ (ZMod p)) (β := MvPolynomial ℕ (ZMod p))
        ((C : (a : ZMod p) → MvPolynomial ℕ (ZMod p)) ((Int.castRingHom (ZMod p) : (a : ℤ) → ZMod p) (↑p : ℤ)) :
          MvPolynomial ℕ (ZMod p))
        ((MvPolynomial.map (Int.castRingHom (ZMod p)) : (a : MvPolynomial ℕ ℤ) → MvPolynomial ℕ (ZMod p))
            (frobeniusPolyAux p n) :
          MvPolynomial ℕ (ZMod p)) =
    HPow.hPow (α := MvPolynomial ℕ (ZMod p)) (X n) p
⊢ (MvPolynomial.map (Int.castRingHom (ZMod p)) : (a : MvPolynomial ℕ ℤ) → MvPolynomial ℕ (ZMod p)) (frobeniusPoly p n) =
    HPow.hPow (α := MvPolynomial ℕ (ZMod p)) (X n) p

Tactic:
rw [frobeniusPoly, map_add, map_pow, map_mul, map_X, map_C]

Premises used: map_add, map_pow, map_mul, MvPolynomial.map_C, MvPolynomial.map_X, WittVector.frobeniusPoly
-- Module: Mathlib.RingTheory.WittVector.Frobenius
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ HPow.hPow (α := MvPolynomial ℕ (ZMod p)) (X n) p +
      HMul.hMul (α := MvPolynomial ℕ (ZMod p)) (β := MvPolynomial ℕ (ZMod p))
        ((C : (a : ZMod p) → MvPolynomial ℕ (ZMod p)) ((Int.castRingHom (ZMod p) : (a : ℤ) → ZMod p) (↑p : ℤ)) :
          MvPolynomial ℕ (ZMod p))
        ((MvPolynomial.map (Int.castRingHom (ZMod p)) : (a : MvPolynomial ℕ ℤ) → MvPolynomial ℕ (ZMod p))
            (frobeniusPolyAux p n) :
          MvPolynomial ℕ (ZMod p)) =
    HPow.hPow (α := MvPolynomial ℕ (ZMod p)) (X n) p

Tactic:
simp only [Int.cast_natCast, add_zero, eq_intCast, ZMod.natCast_self, zero_mul, C_0]

Premises used: Int.cast_natCast, ZMod.natCast_self, MulZeroClass.zero_mul, MvPolynomial.C_0, eq_intCast, add_zero
-- Module: Mathlib.RingTheory.WittVector.Frobenius
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
a :
  Eq (α := MvPolynomial ℕ ℚ)
    ((MvPolynomial.map (Int.castRingHom ℚ) : (a : MvPolynomial ℕ ℤ) → MvPolynomial ℕ ℚ)
        ((bind₁ (frobeniusPoly p) : (a : MvPolynomial ℕ ℤ) → MvPolynomial ℕ ℤ) (wittPolynomial p ℤ n)) :
      MvPolynomial ℕ ℚ)
    ((MvPolynomial.map (Int.castRingHom ℚ) : (a : MvPolynomial ℕ ℤ) → MvPolynomial ℕ ℚ) (wittPolynomial p ℤ (n + 1)) :
      MvPolynomial ℕ ℚ)
⊢ Eq (α := MvPolynomial ℕ ℤ)
    ((bind₁ (frobeniusPoly p) : (a : MvPolynomial ℕ ℤ) → MvPolynomial ℕ ℤ) (wittPolynomial p ℤ n) : MvPolynomial ℕ ℤ)
    (wittPolynomial p ℤ (n + 1) : MvPolynomial ℕ ℤ)

Tactic:
apply MvPolynomial.map_injective (Int.castRingHom ℚ) Int.cast_injective

Premises used: Rat, MvPolynomial.map_injective, Int.castRingHom, Int.cast_injective
-- Module: Mathlib.RingTheory.WittVector.Frobenius
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ Eq (α := MvPolynomial ℕ ℚ)
    ((MvPolynomial.map (Int.castRingHom ℚ) : (a : MvPolynomial ℕ ℤ) → MvPolynomial ℕ ℚ)
        ((bind₁ (frobeniusPoly p) : (a : MvPolynomial ℕ ℤ) → MvPolynomial ℕ ℤ) (wittPolynomial p ℤ n)) :
      MvPolynomial ℕ ℚ)
    ((MvPolynomial.map (Int.castRingHom ℚ) : (a : MvPolynomial ℕ ℤ) → MvPolynomial ℕ ℚ) (wittPolynomial p ℤ (n + 1)) :
      MvPolynomial ℕ ℚ)

Tactic:
simp only [map_bind₁, map_frobeniusPoly, bind₁_frobeniusPolyRat_wittPolynomial,
    map_wittPolynomial]

Premises used: MvPolynomial.map_bind₁, WittVector.map_frobeniusPoly, map_wittPolynomial, WittVector.bind₁_frobeniusPolyRat_wittPolynomial
-- Module: Mathlib.RingTheory.WittVector.Frobenius
Goal:
p : ℕ
R : Type u_1
inst : CommRing R
x : 𝕎 R
n : ℕ
rw :
  Eq (α := R)
    (coeff
        (mk p fun (n : ℕ) ↦
          ((aeval (R := ℤ) x.coeff : MvPolynomial ℕ ℤ →ₐ[ℤ] R) : (a : MvPolynomial ℕ ℤ) → R) (frobeniusPoly p n))
        n :
      R)
    (((aeval (R := ℤ) x.coeff : MvPolynomial ℕ ℤ →ₐ[ℤ] R) : (a : MvPolynomial ℕ ℤ) → R) (frobeniusPoly p n) : R)
rw₁ rw₂ :
  Eq (α := R)
    (((aeval (R := ℤ) x.coeff : MvPolynomial ℕ ℤ →ₐ[ℤ] R) : (a : MvPolynomial ℕ ℤ) → R) (frobeniusPoly p n) : R)
    (((aeval (R := ℤ) x.coeff : MvPolynomial ℕ ℤ →ₐ[ℤ] R) : (a : MvPolynomial ℕ ℤ) → R) (frobeniusPoly p n) : R)
⊢ x.frobeniusFun.coeff n =
    ((aeval (R := ℤ) x.coeff : MvPolynomial ℕ ℤ →ₐ[ℤ] R) : (a : MvPolynomial ℕ ℤ) → R) (frobeniusPoly p n)

Tactic:
rw [frobeniusFun, coeff_mk]

Premises used: WittVector.coeff_mk, WittVector.frobeniusFun
-- Module: Mathlib.RingTheory.WittVector.Frobenius
Goal:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst : CommRing R
R_1 : Type u_2
inst_1 : CommRing R_1
x : 𝕎 R_1
h :
  ∀ (n : ℕ),
    x.frobeniusFun.coeff n =
      ((aeval (R := ℤ) x.coeff : MvPolynomial ℕ ℤ →ₐ[ℤ] R_1) : (a : MvPolynomial ℕ ℤ) → R_1) (frobeniusPoly p n)
⊢ x.frobeniusFun.coeff = fun (n : ℕ) ↦
    ((aeval (R := ℤ) x.coeff : MvPolynomial ℕ ℤ →ₐ[ℤ] R_1) : (a : MvPolynomial ℕ ℤ) → R_1) (frobeniusPoly p n)

Tactic:
funext n
-- Module: Mathlib.RingTheory.WittVector.Frobenius
Goal:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst : CommRing R
R_1 : Type u_2
inst_1 : CommRing R_1
x : 𝕎 R_1
n : ℕ
⊢ x.frobeniusFun.coeff n =
    ((aeval (R := ℤ) x.coeff : MvPolynomial ℕ ℤ →ₐ[ℤ] R_1) : (a : MvPolynomial ℕ ℤ) → R_1) (frobeniusPoly p n)

Tactic:
apply coeff_frobeniusFun

Premises used: WittVector.coeff_frobeniusFun
-- Module: Mathlib.RingTheory.WittVector.Frobenius
Goal:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst : CommRing R
n : ℕ
x : 𝕎 R
⊢ Eq (α := R) ((ghostComponent n : (a : 𝕎 R) → R) x.frobeniusFun : R) ((ghostComponent (n + 1) : (a : 𝕎 R) → R) x : R)

Tactic:
simp only [ghostComponent_apply, frobeniusFun, coeff_mk, ← bind₁_frobeniusPoly_wittPolynomial,
    aeval_bind₁]

Premises used: WittVector.bind₁_frobeniusPoly_wittPolynomial, WittVector.ghostComponent_apply, MvPolynomial.aeval_bind₁, WittVector.coeff_mk, WittVector.frobeniusFun
-- Module: Mathlib.RingTheory.WittVector.Frobenius
Goal:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst : CommRing R
⊢ Eq.{u_1 + 1} (α := 𝕎 R) (frobeniusFun 1) 1

Tactic:
IsPoly.ext (IsPoly.comp (hg := frobeniusFun_isPoly p) (hf := WittVector.oneIsPoly))
        (IsPoly.comp (hg := WittVector.oneIsPoly) (hf := frobeniusFun_isPoly p)) ?_ _ 0

Premises used: WittVector.mk, WittVector.IsPoly.ext, WittVector.IsPoly.comp, OfNat.ofNat, WittVector.frobeniusFun
-- Module: Mathlib.RingTheory.WittVector.Frobenius
Goal:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst : CommRing R
frobeniusFun_isPoly :
  ∀ (R : Type u_1) [_Rcr : CommRing R] (x : 𝕎 R) (n : ℕ),
    Eq (α := R) ((ghostComponent n : (a : 𝕎 R) → R) (((fun (Rcr : 𝕎 R) ↦ Rcr.frobeniusFun) ∘ fun (x : 𝕎 R) ↦ 1) x) : R)
      ((ghostComponent n : (a : 𝕎 R) → R) (((fun (x : 𝕎 R) ↦ 1) ∘ fun (Rcr : 𝕎 R) ↦ Rcr.frobeniusFun) x) : R)
⊢ Eq.{u_1 + 1} (α := 𝕎 R) (frobeniusFun 1) 1

Tactic:
refine
      IsPoly.ext (IsPoly.comp (hg := frobeniusFun_isPoly p) (hf := WittVector.oneIsPoly))
        (IsPoly.comp (hg := WittVector.oneIsPoly) (hf := frobeniusFun_isPoly p)) ?_ _ 0

Premises used: WittVector.IsPoly.ext, WittVector.IsPoly.comp, OfNat.ofNat
-- Module: Mathlib.RingTheory.WittVector.Frobenius
Goal:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst : CommRing R
simp :
  ∀ (R : Type u_1) [_Rcr : CommRing R] (n : ℕ),
    Eq.{u_1 + 1} (α := R) ((ghostComponent n : (a : 𝕎 R) → R) (frobeniusFun 1) : R) (1 : R)
⊢ ∀ (R : Type u_1) [_Rcr : CommRing R] (x : 𝕎 R) (n : ℕ),
    Eq (α := R) ((ghostComponent n : (a : 𝕎 R) → R) (((fun (Rcr : 𝕎 R) ↦ Rcr.frobeniusFun) ∘ fun (x : 𝕎 R) ↦ 1) x) : R)
      ((ghostComponent n : (a : 𝕎 R) → R) (((fun (x : 𝕎 R) ↦ 1) ∘ fun (Rcr : 𝕎 R) ↦ Rcr.frobeniusFun) x) : R)

Tactic:
simp only [Function.comp_apply, map_one, forall_const]

Premises used: map_one, forall_const, Function.comp_apply
-- Module: Mathlib.RingTheory.WittVector.Frobenius
Goal:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst : CommRing R
⊢ ∀ (R : Type u_1) [_Rcr : CommRing R] (n : ℕ),
    Eq.{u_1 + 1} (α := R) ((ghostComponent n : (a : 𝕎 R) → R) (frobeniusFun 1) : R) (1 : R)

Tactic:
ghost_simp
-- Module: Mathlib.RingTheory.WittVector.Frobenius
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
R : Type u_1
R._inst : CommRing R
refine_3 :
  ∀ (x y : 𝕎 R) (n : ℕ),
    Eq (α := R) ((ghostComponent n : (a : 𝕎 R) → R) (x * y).frobeniusFun : R)
      ((ghostComponent n : (a : 𝕎 R) → R) (x.frobeniusFun * y.frobeniusFun) : R)
⊢ ∀ (x y : 𝕎 R) (n : ℕ),
    Eq (α := R) ((ghostComponent n : (a : 𝕎 R) → R) (x * y).frobeniusFun : R)
      ((ghostComponent n : (a : 𝕎 R) → R) (x.frobeniusFun * y.frobeniusFun) : R)

Tactic:
_
-- Module: Mathlib.RingTheory.WittVector.Frobenius
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
R : Type u_1
R._inst : CommRing R
x : 𝕎 R
refine_3 :
  ∀ (y : 𝕎 R) (n : ℕ),
    Eq (α := R) ((ghostComponent n : (a : 𝕎 R) → R) (x * y).frobeniusFun : R)
      ((ghostComponent n : (a : 𝕎 R) → R) (x.frobeniusFun * y.frobeniusFun) : R)
⊢ ∀ (y : 𝕎 R) (n : ℕ),
    Eq (α := R) ((ghostComponent n : (a : 𝕎 R) → R) (x * y).frobeniusFun : R)
      ((ghostComponent n : (a : 𝕎 R) → R) (x.frobeniusFun * y.frobeniusFun) : R)

Tactic:
_
-- Module: Mathlib.RingTheory.WittVector.Frobenius
Goal:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst : CommRing R
refine_3 :
  ∀ (R : Type u_1) [R._inst : CommRing R] (x y : 𝕎 R) (n : ℕ),
    Eq (α := R) ((ghostComponent n : (a : 𝕎 R) → R) (x * y).frobeniusFun : R)
      ((ghostComponent n : (a : 𝕎 R) → R) (x.frobeniusFun * y.frobeniusFun) : R)
⊢ ∀ (x y : 𝕎 R), (x * y).frobeniusFun = x.frobeniusFun * y.frobeniusFun

Tactic:
ghost_calc _ _
-- Module: Mathlib.RingTheory.WittVector.Frobenius
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
R : Type u_1
R._inst : CommRing R
x y : 𝕎 R
⊢ ∀ (n : ℕ),
    Eq (α := R) ((ghostComponent n : (a : 𝕎 R) → R) (x * y).frobeniusFun : R)
      ((ghostComponent n : (a : 𝕎 R) → R) (x.frobeniusFun * y.frobeniusFun) : R)

Tactic:
ghost_simp
-- Module: Mathlib.RingTheory.WittVector.Frobenius
Goal:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst : CommRing R
⊢ Eq.{u_1 + 1} (α := 𝕎 R) (frobeniusFun 0) 0

Tactic:
IsPoly.ext (IsPoly.comp (hg := frobeniusFun_isPoly p) (hf := WittVector.zeroIsPoly))
      (IsPoly.comp (hg := WittVector.zeroIsPoly) (hf := frobeniusFun_isPoly p))
      ?_ _ 0

Premises used: WittVector.mk, WittVector.IsPoly.ext, WittVector.IsPoly.comp, OfNat.ofNat, WittVector.frobeniusFun
-- Module: Mathlib.RingTheory.WittVector.Frobenius
Goal:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst : CommRing R
refine :
  ∀ (R : Type u_1) [_Rcr : CommRing R] (x : 𝕎 R) (n : ℕ),
    Eq (α := R) ((ghostComponent n : (a : 𝕎 R) → R) (((fun (Rcr : 𝕎 R) ↦ Rcr.frobeniusFun) ∘ fun (x : 𝕎 R) ↦ 0) x) : R)
      ((ghostComponent n : (a : 𝕎 R) → R) (((fun (x : 𝕎 R) ↦ 0) ∘ fun (Rcr : 𝕎 R) ↦ Rcr.frobeniusFun) x) : R)
⊢ Eq.{u_1 + 1} (α := 𝕎 R) (frobeniusFun 0) 0

Tactic:
refine IsPoly.ext (IsPoly.comp (hg := frobeniusFun_isPoly p) (hf := WittVector.zeroIsPoly))
      (IsPoly.comp (hg := WittVector.zeroIsPoly) (hf := frobeniusFun_isPoly p))
      ?_ _ 0

Premises used: WittVector.IsPoly.ext, WittVector.IsPoly.comp, OfNat.ofNat
-- Module: Mathlib.RingTheory.WittVector.Frobenius
Goal:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst : CommRing R
simp :
  ∀ (R : Type u_1) [_Rcr : CommRing R] (n : ℕ),
    Eq.{u_1 + 1} (α := R) ((ghostComponent n : (a : 𝕎 R) → R) (frobeniusFun 0) : R) (0 : R)
⊢ ∀ (R : Type u_1) [_Rcr : CommRing R] (x : 𝕎 R) (n : ℕ),
    Eq (α := R) ((ghostComponent n : (a : 𝕎 R) → R) (((fun (Rcr : 𝕎 R) ↦ Rcr.frobeniusFun) ∘ fun (x : 𝕎 R) ↦ 0) x) : R)
      ((ghostComponent n : (a : 𝕎 R) → R) (((fun (x : 𝕎 R) ↦ 0) ∘ fun (Rcr : 𝕎 R) ↦ Rcr.frobeniusFun) x) : R)

Tactic:
simp only [Function.comp_apply, map_zero, forall_const]

Premises used: map_zero, forall_const, Function.comp_apply
-- Module: Mathlib.RingTheory.WittVector.Frobenius
Goal:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst : CommRing R
⊢ ∀ (R : Type u_1) [_Rcr : CommRing R] (n : ℕ),
    Eq.{u_1 + 1} (α := R) ((ghostComponent n : (a : 𝕎 R) → R) (frobeniusFun 0) : R) (0 : R)

Tactic:
ghost_simp
-- Module: Mathlib.RingTheory.WittVector.Frobenius
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
R : Type u_1
R._inst : CommRing R
refine_3 :
  ∀ (x y : 𝕎 R) (n : ℕ),
    Eq (α := R) ((ghostComponent n : (a : 𝕎 R) → R) (x + y).frobeniusFun : R)
      ((ghostComponent n : (a : 𝕎 R) → R) (x.frobeniusFun + y.frobeniusFun) : R)
⊢ ∀ (x y : 𝕎 R) (n : ℕ),
    Eq (α := R) ((ghostComponent n : (a : 𝕎 R) → R) (x + y).frobeniusFun : R)
      ((ghostComponent n : (a : 𝕎 R) → R) (x.frobeniusFun + y.frobeniusFun) : R)

Tactic:
_
-- Module: Mathlib.RingTheory.WittVector.Frobenius
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
R : Type u_1
R._inst : CommRing R
x : 𝕎 R
refine_3 :
  ∀ (y : 𝕎 R) (n : ℕ),
    Eq (α := R) ((ghostComponent n : (a : 𝕎 R) → R) (x + y).frobeniusFun : R)
      ((ghostComponent n : (a : 𝕎 R) → R) (x.frobeniusFun + y.frobeniusFun) : R)
⊢ ∀ (y : 𝕎 R) (n : ℕ),
    Eq (α := R) ((ghostComponent n : (a : 𝕎 R) → R) (x + y).frobeniusFun : R)
      ((ghostComponent n : (a : 𝕎 R) → R) (x.frobeniusFun + y.frobeniusFun) : R)

Tactic:
_
-- Module: Mathlib.RingTheory.WittVector.Frobenius
Goal:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst : CommRing R
refine_3 :
  ∀ (R : Type u_1) [R._inst : CommRing R] (x y : 𝕎 R) (n : ℕ),
    Eq (α := R) ((ghostComponent n : (a : 𝕎 R) → R) (x + y).frobeniusFun : R)
      ((ghostComponent n : (a : 𝕎 R) → R) (x.frobeniusFun + y.frobeniusFun) : R)
⊢ ∀ (x y : 𝕎 R), (x + y).frobeniusFun = x.frobeniusFun + y.frobeniusFun

Tactic:
ghost_calc _ _
-- Module: Mathlib.RingTheory.WittVector.Frobenius
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
R : Type u_1
R._inst : CommRing R
x y : 𝕎 R
⊢ ∀ (n : ℕ),
    Eq (α := R) ((ghostComponent n : (a : 𝕎 R) → R) (x + y).frobeniusFun : R)
      ((ghostComponent n : (a : 𝕎 R) → R) (x.frobeniusFun + y.frobeniusFun) : R)

Tactic:
ghost_simp
-- Module: Mathlib.RingTheory.WittVector.Frobenius
Goal:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst : CommRing R
x : 𝕎 R
n : ℕ
⊢ Eq (α := R) (coeff (p := p) ((frobenius : (a : 𝕎 R) → 𝕎 R) x) n : R)
    (((aeval (R := ℤ) x.coeff : MvPolynomial ℕ ℤ →ₐ[ℤ] R) : (a : MvPolynomial ℕ ℤ) → R) (frobeniusPoly p n) : R)

Tactic:
coeff_frobeniusFun _ _

Premises used: WittVector.coeff_frobeniusFun
-- Module: Mathlib.RingTheory.WittVector.Frobenius
Goal:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst : CommRing R
n : ℕ
x : 𝕎 R
⊢ Eq (α := R) ((ghostComponent n : (a : 𝕎 R) → R) ((frobenius : (a : 𝕎 R) → 𝕎 R) x : 𝕎 R) : R)
    ((ghostComponent (n + 1) : (a : 𝕎 R) → R) x : R)

Tactic:
ghostComponent_frobeniusFun _ _

Premises used: WittVector.mk, WittVector.ghostComponent_frobeniusFun, WittVector.frobeniusFun
-- Module: Mathlib.RingTheory.WittVector.Frobenius
Goal:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst : CommRing R
⊢ IsPoly.{u_2} p fun (R : Type u_2) (_Rcr : CommRing R) ↦ (⇑frobenius : (a : 𝕎 R) → 𝕎 R)

Tactic:
frobeniusFun_isPoly _

Premises used: WittVector.mk, WittVector.frobeniusFun_isPoly, WittVector.frobeniusFun
-- Module: Mathlib.RingTheory.WittVector.Frobenius
Goal:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst : CommRing R
inst_1 : CharP R p
x : 𝕎 R
n : ℕ
rw :
  ((aeval (R := ℤ) x.coeff : MvPolynomial ℕ ℤ →ₐ[ℤ] R) : (a : MvPolynomial ℕ ℤ) → R) (frobeniusPoly p n) = x.coeff n ^ p
⊢ coeff (p := p) ((frobenius : (a : 𝕎 R) → 𝕎 R) x) n = x.coeff n ^ p

Tactic:
rw [coeff_frobenius]

Premises used: WittVector.coeff_frobenius
-- Module: Mathlib.RingTheory.WittVector.Frobenius
Goal:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst : CommRing R
inst_1 : CharP R p
x : 𝕎 R
n : ℕ
this : Algebra (ZMod p) R := ZMod.algebra R p
⊢ Eq.{u_1 + 1} (α := R)
    (((aeval.{0, u_1, 0} (R := ℤ) (S₁ := R) fun (k : ℕ) ↦ x.coeff k : MvPolynomial ℕ ℤ →ₐ[ℤ] R) :
          (a : MvPolynomial ℕ ℤ) → R)
        (frobeniusPoly p n) :
      R)
    ((aeval fun (k : ℕ) ↦ x.coeff k : (a : MvPolynomial ℕ (ZMod p)) → R)
        ((MvPolynomial.map (Int.castRingHom (ZMod p)) : (a : MvPolynomial ℕ ℤ) → MvPolynomial ℕ (ZMod p))
            (frobeniusPoly p n) :
          MvPolynomial ℕ (ZMod p)) :
      R)

Tactic:
?_
-- Module: Mathlib.RingTheory.WittVector.Frobenius
Goal:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst : CommRing R
inst_1 : CharP R p
x : 𝕎 R
n : ℕ
this : Algebra (ZMod p) R := ZMod.algebra R p
⊢ Eq.{u_1 + 1} (α := R)
    ((aeval fun (k : ℕ) ↦ x.coeff k : (a : MvPolynomial ℕ (ZMod p)) → R)
        ((MvPolynomial.map (Int.castRingHom (ZMod p)) : (a : MvPolynomial ℕ ℤ) → MvPolynomial ℕ (ZMod p))
            (frobeniusPoly p n) :
          MvPolynomial ℕ (ZMod p)) :
      R)
    ((aeval fun (k : ℕ) ↦ x.coeff k : (a : MvPolynomial ℕ (ZMod p)) → R)
        (HPow.hPow (α := MvPolynomial ℕ (ZMod p)) (X n) p) :
      R)

Tactic:
?_
-- Module: Mathlib.RingTheory.WittVector.Frobenius
Goal:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst : CommRing R
inst_1 : CharP R p
x : 𝕎 R
n : ℕ
this : Algebra (ZMod p) R := ZMod.algebra R p
⊢ (aeval fun (k : ℕ) ↦ x.coeff k : (a : MvPolynomial ℕ (ZMod p)) → R)
      (HPow.hPow (α := MvPolynomial ℕ (ZMod p)) (X n) p) =
    x.coeff n ^ p

Tactic:
?_
-- Module: Mathlib.RingTheory.WittVector.Frobenius
Goal:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst : CommRing R
inst_1 : CharP R p
x : 𝕎 R
n : ℕ
this : Algebra (ZMod p) R := ZMod.algebra R p
calc_1 :
  Eq.{u_1 + 1} (α := R)
    (((aeval.{0, u_1, 0} (R := ℤ) (S₁ := R) fun (k : ℕ) ↦ x.coeff k : MvPolynomial ℕ ℤ →ₐ[ℤ] R) :
          (a : MvPolynomial ℕ ℤ) → R)
        (frobeniusPoly p n) :
      R)
    ((aeval fun (k : ℕ) ↦ x.coeff k : (a : MvPolynomial ℕ (ZMod p)) → R)
        ((MvPolynomial.map (Int.castRingHom (ZMod p)) : (a : MvPolynomial ℕ ℤ) → MvPolynomial ℕ (ZMod p))
            (frobeniusPoly p n) :
          MvPolynomial ℕ (ZMod p)) :
      R)
calc_2 :
  Eq.{u_1 + 1} (α := R)
    ((aeval fun (k : ℕ) ↦ x.coeff k : (a : MvPolynomial ℕ (ZMod p)) → R)
        ((MvPolynomial.map (Int.castRingHom (ZMod p)) : (a : MvPolynomial ℕ ℤ) → MvPolynomial ℕ (ZMod p))
            (frobeniusPoly p n) :
          MvPolynomial ℕ (ZMod p)) :
      R)
    ((aeval fun (k : ℕ) ↦ x.coeff k : (a : MvPolynomial ℕ (ZMod p)) → R)
        (HPow.hPow (α := MvPolynomial ℕ (ZMod p)) (X n) p) :
      R)
calc_3 :
  (aeval fun (k : ℕ) ↦ x.coeff k : (a : MvPolynomial ℕ (ZMod p)) → R)
      (HPow.hPow (α := MvPolynomial ℕ (ZMod p)) (X n) p) =
    x.coeff n ^ p
⊢ ((aeval (R := ℤ) x.coeff : MvPolynomial ℕ ℤ →ₐ[ℤ] R) : (a : MvPolynomial ℕ ℤ) → R) (frobeniusPoly p n) = x.coeff n ^ p

Tactic:
calc
    aeval (fun k => x.coeff k) (frobeniusPoly p n) =
        aeval (fun k => x.coeff k)
          (MvPolynomial.map (Int.castRingHom (ZMod p)) (frobeniusPoly p n)) := ?_
    _ = aeval (fun k => x.coeff k) (X n ^ p : MvPolynomial ℕ (ZMod p)) := ?_
    _ = x.coeff n ^ p := ?_

Premises used: MvPolynomial.aeval, MvPolynomial.X, ZMod, HPow.hPow, Int.castRingHom, MvPolynomial.map, WittVector.coeff, DFunLike.coe, WittVector.frobeniusPoly
-- Module: Mathlib.RingTheory.WittVector.Frobenius
Goal:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst : CommRing R
inst_1 : CharP R p
x : 𝕎 R
n : ℕ
this : Algebra (ZMod p) R := ZMod.algebra R p
rw :
  ((eval₂Hom
          (@RingHom.comp _ (ZMod p) _ _ Semiring.toNonAssocSemiring _ (algebraMap (ZMod p) R)
            (Int.castRingHom (ZMod p)))
          fun (k : ℕ) ↦ x.coeff k :
        (a : MvPolynomial ℕ ℤ) → R)
      (frobeniusPoly p n) :
    R)
| ((aeval fun (k : ℕ) ↦ x.coeff k : (a : MvPolynomial ℕ (ZMod p)) → R)
      ((MvPolynomial.map (Int.castRingHom (ZMod p)) : (a : MvPolynomial ℕ ℤ) → MvPolynomial ℕ (ZMod p))
          (frobeniusPoly p n) :
        MvPolynomial ℕ (ZMod p)) :
    R)

Tactic:
rw [aeval_eq_eval₂Hom, eval₂Hom_map_hom]

Premises used: MvPolynomial.eval₂Hom_map_hom, MvPolynomial.aeval_eq_eval₂Hom
-- Module: Mathlib.RingTheory.WittVector.Frobenius
Goal:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst : CommRing R
inst_1 : CharP R p
x : 𝕎 R
n : ℕ
this : Algebra (ZMod p) R := ZMod.algebra R p
calc_1 :
  Eq (α := R)
    (((aeval.{0, u_1, 0} (R := ℤ) (S₁ := R) fun (k : ℕ) ↦ x.coeff k : MvPolynomial ℕ ℤ →ₐ[ℤ] R) :
          (a : MvPolynomial ℕ ℤ) → R)
        (frobeniusPoly p n) :
      R)
    ((eval₂Hom
            (@RingHom.comp _ (ZMod p) _ _ Semiring.toNonAssocSemiring _ (algebraMap (ZMod p) R)
              (Int.castRingHom (ZMod p)))
            fun (k : ℕ) ↦ x.coeff k :
          (a : MvPolynomial ℕ ℤ) → R)
        (frobeniusPoly p n) :
      R)
⊢ Eq.{u_1 + 1} (α := R)
    (((aeval.{0, u_1, 0} (R := ℤ) (S₁ := R) fun (k : ℕ) ↦ x.coeff k : MvPolynomial ℕ ℤ →ₐ[ℤ] R) :
          (a : MvPolynomial ℕ ℤ) → R)
        (frobeniusPoly p n) :
      R)
    ((aeval fun (k : ℕ) ↦ x.coeff k : (a : MvPolynomial ℕ (ZMod p)) → R)
        ((MvPolynomial.map (Int.castRingHom (ZMod p)) : (a : MvPolynomial ℕ ℤ) → MvPolynomial ℕ (ZMod p))
            (frobeniusPoly p n) :
          MvPolynomial ℕ (ZMod p)) :
      R)

Tactic:
conv_rhs => rw [aeval_eq_eval₂Hom, eval₂Hom_map_hom]

Premises used: MvPolynomial.eval₂Hom_map_hom, MvPolynomial.aeval_eq_eval₂Hom
-- Module: Mathlib.RingTheory.WittVector.Frobenius
Goal:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst : CommRing R
inst_1 : CharP R p
x : 𝕎 R
n : ℕ
this : Algebra (ZMod p) R := ZMod.algebra R p
⊢ Eq (α := R)
    (((aeval.{0, u_1, 0} (R := ℤ) (S₁ := R) fun (k : ℕ) ↦ x.coeff k : MvPolynomial ℕ ℤ →ₐ[ℤ] R) :
          (a : MvPolynomial ℕ ℤ) → R)
        (frobeniusPoly p n) :
      R)
    ((eval₂Hom
            (@RingHom.comp _ (ZMod p) _ _ Semiring.toNonAssocSemiring _ (algebraMap (ZMod p) R)
              (Int.castRingHom (ZMod p)))
            fun (k : ℕ) ↦ x.coeff k :
          (a : MvPolynomial ℕ ℤ) → R)
        (frobeniusPoly p n) :
      R)

Tactic:
apply eval₂Hom_congr (RingHom.ext_int _ _) rfl rfl

Premises used: MvPolynomial.eval₂Hom_congr, RingHom.ext_int, rfl
-- Module: Mathlib.RingTheory.WittVector.Frobenius
Goal:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst : CommRing R
inst_1 : CharP R p
x : 𝕎 R
n : ℕ
this : Algebra (ZMod p) R := ZMod.algebra R p
calc_2 calc_2₁ :
  Eq.{u_1 + 1} (α := R)
    ((aeval fun (k : ℕ) ↦ x.coeff k : (a : MvPolynomial ℕ (ZMod p)) → R)
        (HPow.hPow (α := MvPolynomial ℕ (ZMod p)) (X n) p) :
      R)
    ((aeval fun (k : ℕ) ↦ x.coeff k : (a : MvPolynomial ℕ (ZMod p)) → R)
        (HPow.hPow (α := MvPolynomial ℕ (ZMod p)) (X n) p) :
      R)
⊢ Eq.{u_1 + 1} (α := R)
    ((aeval fun (k : ℕ) ↦ x.coeff k : (a : MvPolynomial ℕ (ZMod p)) → R)
        ((MvPolynomial.map (Int.castRingHom (ZMod p)) : (a : MvPolynomial ℕ ℤ) → MvPolynomial ℕ (ZMod p))
            (frobeniusPoly p n) :
          MvPolynomial ℕ (ZMod p)) :
      R)
    ((aeval fun (k : ℕ) ↦ x.coeff k : (a : MvPolynomial ℕ (ZMod p)) → R)
        (HPow.hPow (α := MvPolynomial ℕ (ZMod p)) (X n) p) :
      R)

Tactic:
rw [frobeniusPoly_zmod]

Premises used: WittVector.frobeniusPoly_zmod
-- Module: Mathlib.RingTheory.WittVector.Frobenius
Goal:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst : CommRing R
inst_1 : CharP R p
x : 𝕎 R
n : ℕ
this : Algebra (ZMod p) R := ZMod.algebra R p
calc_3 :
  HPow.hPow (α := R) ((aeval fun (k : ℕ) ↦ x.coeff k : (a : MvPolynomial ℕ (ZMod p)) → R) (X n) : R) p = x.coeff n ^ p
calc_3₁ calc_3₂ : x.coeff n ^ p = x.coeff n ^ p
⊢ (aeval fun (k : ℕ) ↦ x.coeff k : (a : MvPolynomial ℕ (ZMod p)) → R)
      (HPow.hPow (α := MvPolynomial ℕ (ZMod p)) (X n) p) =
    x.coeff n ^ p

Tactic:
rw [map_pow, aeval_X]

Premises used: MvPolynomial.aeval_X, map_pow
-- Module: Mathlib.RingTheory.WittVector.Frobenius
Goal:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst : CommRing R
inst_1 : CharP R p
a :
  ∀ (x : 𝕎 R) (n : ℕ),
    Eq.{u_1 + 1} (α := R) (coeff (p := p) ((frobenius : (a : 𝕎 R) → 𝕎 R) x) n)
      (coeff (p := p) ((map (_root_.frobenius R p) : (a : 𝕎 R) → 𝕎 R) x) n)
⊢ Eq (α := 𝕎 R →+* 𝕎 R) frobenius (map (_root_.frobenius R p))

Tactic:
ext (x n)
-- Module: Mathlib.RingTheory.WittVector.Frobenius
Goal:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst : CommRing R
inst_1 : CharP R p
x : 𝕎 R
n : ℕ
⊢ Eq.{u_1 + 1} (α := R) (coeff (p := p) ((frobenius : (a : 𝕎 R) → 𝕎 R) x) n)
    (coeff (p := p) ((map (_root_.frobenius R p) : (a : 𝕎 R) → 𝕎 R) x) n)

Tactic:
simp only [coeff_frobenius_charP, map_coeff, frobenius_def]

Premises used: WittVector.map_coeff, WittVector.coeff_frobenius_charP, frobenius_def
-- Module: Mathlib.RingTheory.WittVector.Frobenius
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x : 𝕎 (ZMod p)
⊢ (frobenius : (a : 𝕎 (ZMod p)) → 𝕎 (ZMod p)) x = x

Tactic:
simp only [WittVector.ext_iff, coeff_frobenius_charP, ZMod.pow_card,
    forall_const]

Premises used: ZMod.pow_card, WittVector.coeff_frobenius_charP, forall_const, WittVector.ext_iff