[GOAL]
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
n : ℕ
⊢ ↑(bind₁ (frobeniusPolyRat p)) (wittPolynomial p ℚ n) = wittPolynomial p ℚ (n + 1)
[PROOFSTEP]
delta frobeniusPolyRat
[GOAL]
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
n : ℕ
⊢ ↑(bind₁ fun n => ↑(bind₁ (wittPolynomial p ℚ ∘ fun n => n + 1)) (xInTermsOfW p ℚ n)) (wittPolynomial p ℚ n) =
    wittPolynomial p ℚ (n + 1)
[PROOFSTEP]
rw [← bind₁_bind₁, bind₁_xInTermsOfW_wittPolynomial, bind₁_X_right, Function.comp_apply]
[GOAL]
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
n : ℕ
⊢ frobeniusPolyAux p n =
    X (n + 1) -
      ∑ i in range n,
        ∑ j in range (p ^ (n - i)),
          (X i ^ p) ^ (p ^ (n - i) - (j + 1)) * frobeniusPolyAux p i ^ (j + 1) *
            ↑C
              ↑(Nat.choose (p ^ (n - i)) (j + 1) /
                    p ^ (n - i - v p { val := j + 1, property := (_ : 0 < Nat.succ j) }) *
                  p ^ (j - v p { val := j + 1, property := (_ : 0 < Nat.succ j) }))
[PROOFSTEP]
rw [frobeniusPolyAux, ← Fin.sum_univ_eq_sum_range]
[GOAL]
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
n j : ℕ
hj : j < p ^ n
⊢ p ^ (n - v p { val := j + 1, property := (_ : 0 < Nat.succ j) }) ∣ Nat.choose (p ^ n) (j + 1)
[PROOFSTEP]
apply multiplicity.pow_dvd_of_le_multiplicity
[GOAL]
case a
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
n j : ℕ
hj : j < p ^ n
⊢ ↑(n - v p { val := j + 1, property := (_ : 0 < Nat.succ j) }) ≤ multiplicity p (Nat.choose (p ^ n) (j + 1))
[PROOFSTEP]
rw [hp.out.multiplicity_choose_prime_pow hj j.succ_ne_zero]
[GOAL]
case a
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
n j : ℕ
hj : j < p ^ n
⊢ ↑(n - v p { val := j + 1, property := (_ : 0 < Nat.succ j) }) ≤
    ↑(n - Part.get (multiplicity p (Nat.succ j)) (_ : multiplicity.Finite p (Nat.succ j)))
[PROOFSTEP]
rfl
[GOAL]
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
n i j : ℕ
hi : i ≤ n
hj : j < p ^ (n - i)
⊢ j - v p { val := j + 1, property := (_ : 0 < Nat.succ j) } + n =
    i + j + (n - i - v p { val := j + 1, property := (_ : 0 < Nat.succ j) })
[PROOFSTEP]
generalize h : v p ⟨j + 1, j.succ_pos⟩ = m
[GOAL]
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
n i j : ℕ
hi : i ≤ n
hj : j < p ^ (n - i)
m : ℕ
h : v p { val := j + 1, property := (_ : 0 < Nat.succ j) } = m
⊢ j - m + n = i + j + (n - i - m)
[PROOFSTEP]
rsuffices ⟨h₁, h₂⟩ : m ≤ n - i ∧ m ≤ j
[GOAL]
case intro
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
n i j : ℕ
hi : i ≤ n
hj : j < p ^ (n - i)
m : ℕ
h : v p { val := j + 1, property := (_ : 0 < Nat.succ j) } = m
h₁ : m ≤ n - i
h₂ : m ≤ j
⊢ j - m + n = i + j + (n - i - m)
[PROOFSTEP]
rw [tsub_add_eq_add_tsub h₂, add_comm i j, add_tsub_assoc_of_le (h₁.trans (Nat.sub_le n i)), add_assoc, tsub_right_comm,
  add_comm i, tsub_add_cancel_of_le (le_tsub_of_add_le_right ((le_tsub_iff_left hi).mp h₁))]
[GOAL]
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
n i j : ℕ
hi : i ≤ n
hj : j < p ^ (n - i)
m : ℕ
h : v p { val := j + 1, property := (_ : 0 < Nat.succ j) } = m
⊢ m ≤ n - i ∧ m ≤ j
[PROOFSTEP]
have hle : p ^ m ≤ j + 1 := h ▸ Nat.le_of_dvd j.succ_pos (multiplicity.pow_multiplicity_dvd _)
[GOAL]
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
n i j : ℕ
hi : i ≤ n
hj : j < p ^ (n - i)
m : ℕ
h : v p { val := j + 1, property := (_ : 0 < Nat.succ j) } = m
hle : p ^ m ≤ j + 1
⊢ m ≤ n - i ∧ m ≤ j
[PROOFSTEP]
exact ⟨(pow_le_pow_iff hp.1.one_lt).1 (hle.trans hj), Nat.le_of_lt_succ ((Nat.lt_pow_self hp.1.one_lt m).trans_le hle)⟩
[GOAL]
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
n : ℕ
⊢ ↑(MvPolynomial.map (Int.castRingHom ℚ)) (frobeniusPoly p n) = frobeniusPolyRat p n
[PROOFSTEP]
rw [frobeniusPoly, RingHom.map_add, RingHom.map_mul, RingHom.map_pow, map_C, map_X, eq_intCast, Int.cast_ofNat,
  frobeniusPolyRat]
[GOAL]
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
n : ℕ
⊢ X n ^ p + ↑C (↑(Int.castRingHom ℚ) ↑p) * ↑(MvPolynomial.map (Int.castRingHom ℚ)) (frobeniusPolyAux p n) =
    ↑(bind₁ (wittPolynomial p ℚ ∘ fun n => n + 1)) (xInTermsOfW p ℚ n)
[PROOFSTEP]
refine Nat.strong_induction_on n ?_
[GOAL]
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
n : ℕ
⊢ ∀ (n : ℕ),
    (∀ (m : ℕ),
        m < n →
          X m ^ p + ↑C (↑(Int.castRingHom ℚ) ↑p) * ↑(MvPolynomial.map (Int.castRingHom ℚ)) (frobeniusPolyAux p m) =
            ↑(bind₁ (wittPolynomial p ℚ ∘ fun n => n + 1)) (xInTermsOfW p ℚ m)) →
      X n ^ p + ↑C (↑(Int.castRingHom ℚ) ↑p) * ↑(MvPolynomial.map (Int.castRingHom ℚ)) (frobeniusPolyAux p n) =
        ↑(bind₁ (wittPolynomial p ℚ ∘ fun n => n + 1)) (xInTermsOfW p ℚ n)
[PROOFSTEP]
clear n
[GOAL]
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
⊢ ∀ (n : ℕ),
    (∀ (m : ℕ),
        m < n →
          X m ^ p + ↑C (↑(Int.castRingHom ℚ) ↑p) * ↑(MvPolynomial.map (Int.castRingHom ℚ)) (frobeniusPolyAux p m) =
            ↑(bind₁ (wittPolynomial p ℚ ∘ fun n => n + 1)) (xInTermsOfW p ℚ m)) →
      X n ^ p + ↑C (↑(Int.castRingHom ℚ) ↑p) * ↑(MvPolynomial.map (Int.castRingHom ℚ)) (frobeniusPolyAux p n) =
        ↑(bind₁ (wittPolynomial p ℚ ∘ fun n => n + 1)) (xInTermsOfW p ℚ n)
[PROOFSTEP]
intro n IH
[GOAL]
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
n : ℕ
IH :
  ∀ (m : ℕ),
    m < n →
      X m ^ p + ↑C (↑(Int.castRingHom ℚ) ↑p) * ↑(MvPolynomial.map (Int.castRingHom ℚ)) (frobeniusPolyAux p m) =
        ↑(bind₁ (wittPolynomial p ℚ ∘ fun n => n + 1)) (xInTermsOfW p ℚ m)
⊢ X n ^ p + ↑C (↑(Int.castRingHom ℚ) ↑p) * ↑(MvPolynomial.map (Int.castRingHom ℚ)) (frobeniusPolyAux p n) =
    ↑(bind₁ (wittPolynomial p ℚ ∘ fun n => n + 1)) (xInTermsOfW p ℚ n)
[PROOFSTEP]
rw [xInTermsOfW_eq]
[GOAL]
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
n : ℕ
IH :
  ∀ (m : ℕ),
    m < n →
      X m ^ p + ↑C (↑(Int.castRingHom ℚ) ↑p) * ↑(MvPolynomial.map (Int.castRingHom ℚ)) (frobeniusPolyAux p m) =
        ↑(bind₁ (wittPolynomial p ℚ ∘ fun n => n + 1)) (xInTermsOfW p ℚ m)
⊢ X n ^ p + ↑C (↑(Int.castRingHom ℚ) ↑p) * ↑(MvPolynomial.map (Int.castRingHom ℚ)) (frobeniusPolyAux p n) =
    ↑(bind₁ (wittPolynomial p ℚ ∘ fun n => n + 1))
      ((X n - ∑ i in range n, ↑C (↑p ^ i) * xInTermsOfW p ℚ i ^ p ^ (n - i)) * ↑C (⅟↑p ^ n))
[PROOFSTEP]
simp only [AlgHom.map_sum, AlgHom.map_sub, AlgHom.map_mul, AlgHom.map_pow, bind₁_C_right]
[GOAL]
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
n : ℕ
IH :
  ∀ (m : ℕ),
    m < n →
      X m ^ p + ↑C (↑(Int.castRingHom ℚ) ↑p) * ↑(MvPolynomial.map (Int.castRingHom ℚ)) (frobeniusPolyAux p m) =
        ↑(bind₁ (wittPolynomial p ℚ ∘ fun n => n + 1)) (xInTermsOfW p ℚ m)
⊢ X n ^ p + ↑C (↑(Int.castRingHom ℚ) ↑p) * ↑(MvPolynomial.map (Int.castRingHom ℚ)) (frobeniusPolyAux p n) =
    (↑(bind₁ (wittPolynomial p ℚ ∘ fun n => n + 1)) (X n) -
        ∑ x in range n,
          ↑C (↑p ^ x) * ↑(bind₁ (wittPolynomial p ℚ ∘ fun n => n + 1)) (xInTermsOfW p ℚ x) ^ p ^ (n - x)) *
      ↑C (⅟↑p ^ n)
[PROOFSTEP]
have h1 : (p : ℚ) ^ n * ⅟(p : ℚ) ^ n = 1 := by rw [← mul_pow, mul_invOf_self, one_pow]
[GOAL]
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
n : ℕ
IH :
  ∀ (m : ℕ),
    m < n →
      X m ^ p + ↑C (↑(Int.castRingHom ℚ) ↑p) * ↑(MvPolynomial.map (Int.castRingHom ℚ)) (frobeniusPolyAux p m) =
        ↑(bind₁ (wittPolynomial p ℚ ∘ fun n => n + 1)) (xInTermsOfW p ℚ m)
⊢ ↑p ^ n * ⅟↑p ^ n = 1
[PROOFSTEP]
rw [← mul_pow, mul_invOf_self, one_pow]
[GOAL]
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
n : ℕ
IH :
  ∀ (m : ℕ),
    m < n →
      X m ^ p + ↑C (↑(Int.castRingHom ℚ) ↑p) * ↑(MvPolynomial.map (Int.castRingHom ℚ)) (frobeniusPolyAux p m) =
        ↑(bind₁ (wittPolynomial p ℚ ∘ fun n => n + 1)) (xInTermsOfW p ℚ m)
h1 : ↑p ^ n * ⅟↑p ^ n = 1
⊢ X n ^ p + ↑C (↑(Int.castRingHom ℚ) ↑p) * ↑(MvPolynomial.map (Int.castRingHom ℚ)) (frobeniusPolyAux p n) =
    (↑(bind₁ (wittPolynomial p ℚ ∘ fun n => n + 1)) (X n) -
        ∑ x in range n,
          ↑C (↑p ^ x) * ↑(bind₁ (wittPolynomial p ℚ ∘ fun n => n + 1)) (xInTermsOfW p ℚ x) ^ p ^ (n - x)) *
      ↑C (⅟↑p ^ n)
[PROOFSTEP]
rw [bind₁_X_right, Function.comp_apply, wittPolynomial_eq_sum_C_mul_X_pow, sum_range_succ, sum_range_succ, tsub_self,
  add_tsub_cancel_left, pow_zero, pow_one, pow_one, sub_mul, add_mul, add_mul, mul_right_comm,
  mul_right_comm (C ((p : ℚ) ^ (n + 1))), ← C_mul, ← C_mul, pow_succ, mul_assoc (p : ℚ) ((p : ℚ) ^ n), h1, mul_one, C_1,
  one_mul, add_comm _ (X n ^ p), add_assoc, ← add_sub, add_right_inj, frobeniusPolyAux_eq, RingHom.map_sub, map_X,
  mul_sub, sub_eq_add_neg, add_comm _ (C (p : ℚ) * X (n + 1)), ← add_sub,
  show (Int.castRingHom ℚ) ↑p = (p : ℚ) from rfl, add_right_inj, neg_eq_iff_eq_neg, neg_sub, eq_comm]
[GOAL]
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
n : ℕ
IH :
  ∀ (m : ℕ),
    m < n →
      X m ^ p + ↑C (↑(Int.castRingHom ℚ) ↑p) * ↑(MvPolynomial.map (Int.castRingHom ℚ)) (frobeniusPolyAux p m) =
        ↑(bind₁ (wittPolynomial p ℚ ∘ fun n => n + 1)) (xInTermsOfW p ℚ m)
h1 : ↑p ^ n * ⅟↑p ^ n = 1
⊢ (∑ x in range n, ↑C (↑p ^ x) * ↑(bind₁ (wittPolynomial p ℚ ∘ fun n => n + 1)) (xInTermsOfW p ℚ x) ^ p ^ (n - x)) *
        ↑C (⅟↑p ^ n) -
      (∑ x in range n, ↑C (↑p ^ x) * X x ^ p ^ (n + 1 - x)) * ↑C (⅟↑p ^ n) =
    ↑C ↑p *
      ↑(MvPolynomial.map (Int.castRingHom ℚ))
        (∑ i in range n,
          ∑ j in range (p ^ (n - i)),
            (X i ^ p) ^ (p ^ (n - i) - (j + 1)) * frobeniusPolyAux p i ^ (j + 1) *
              ↑C
                ↑(Nat.choose (p ^ (n - i)) (j + 1) /
                      p ^ (n - i - v p { val := j + 1, property := (_ : 0 < Nat.succ j) }) *
                    p ^ (j - v p { val := j + 1, property := (_ : 0 < Nat.succ j) })))
[PROOFSTEP]
simp only [map_sum, mul_sum, sum_mul, ← sum_sub_distrib]
[GOAL]
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
n : ℕ
IH :
  ∀ (m : ℕ),
    m < n →
      X m ^ p + ↑C (↑(Int.castRingHom ℚ) ↑p) * ↑(MvPolynomial.map (Int.castRingHom ℚ)) (frobeniusPolyAux p m) =
        ↑(bind₁ (wittPolynomial p ℚ ∘ fun n => n + 1)) (xInTermsOfW p ℚ m)
h1 : ↑p ^ n * ⅟↑p ^ n = 1
⊢ ∑ x in range n,
      (↑C (↑p ^ x) * ↑(bind₁ (wittPolynomial p ℚ ∘ fun n => n + 1)) (xInTermsOfW p ℚ x) ^ p ^ (n - x) * ↑C (⅟↑p ^ n) -
        ↑C (↑p ^ x) * X x ^ p ^ (n + 1 - x) * ↑C (⅟↑p ^ n)) =
    ∑ x in range n,
      ∑ x_1 in range (p ^ (n - x)),
        ↑C ↑p *
          ↑(MvPolynomial.map (Int.castRingHom ℚ))
            ((X x ^ p) ^ (p ^ (n - x) - (x_1 + 1)) * frobeniusPolyAux p x ^ (x_1 + 1) *
              ↑C
                ↑(Nat.choose (p ^ (n - x)) (x_1 + 1) /
                      p ^ (n - x - v p { val := x_1 + 1, property := (_ : 0 < Nat.succ x_1) }) *
                    p ^ (x_1 - v p { val := x_1 + 1, property := (_ : 0 < Nat.succ x_1) })))
[PROOFSTEP]
apply sum_congr rfl
[GOAL]
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
n : ℕ
IH :
  ∀ (m : ℕ),
    m < n →
      X m ^ p + ↑C (↑(Int.castRingHom ℚ) ↑p) * ↑(MvPolynomial.map (Int.castRingHom ℚ)) (frobeniusPolyAux p m) =
        ↑(bind₁ (wittPolynomial p ℚ ∘ fun n => n + 1)) (xInTermsOfW p ℚ m)
h1 : ↑p ^ n * ⅟↑p ^ n = 1
⊢ ∀ (x : ℕ),
    x ∈ range n →
      ↑C (↑p ^ x) * ↑(bind₁ (wittPolynomial p ℚ ∘ fun n => n + 1)) (xInTermsOfW p ℚ x) ^ p ^ (n - x) * ↑C (⅟↑p ^ n) -
          ↑C (↑p ^ x) * X x ^ p ^ (n + 1 - x) * ↑C (⅟↑p ^ n) =
        ∑ x_1 in range (p ^ (n - x)),
          ↑C ↑p *
            ↑(MvPolynomial.map (Int.castRingHom ℚ))
              ((X x ^ p) ^ (p ^ (n - x) - (x_1 + 1)) * frobeniusPolyAux p x ^ (x_1 + 1) *
                ↑C
                  ↑(Nat.choose (p ^ (n - x)) (x_1 + 1) /
                        p ^ (n - x - v p { val := x_1 + 1, property := (_ : 0 < Nat.succ x_1) }) *
                      p ^ (x_1 - v p { val := x_1 + 1, property := (_ : 0 < Nat.succ x_1) })))
[PROOFSTEP]
intro i hi
[GOAL]
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
n : ℕ
IH :
  ∀ (m : ℕ),
    m < n →
      X m ^ p + ↑C (↑(Int.castRingHom ℚ) ↑p) * ↑(MvPolynomial.map (Int.castRingHom ℚ)) (frobeniusPolyAux p m) =
        ↑(bind₁ (wittPolynomial p ℚ ∘ fun n => n + 1)) (xInTermsOfW p ℚ m)
h1 : ↑p ^ n * ⅟↑p ^ n = 1
i : ℕ
hi : i ∈ range n
⊢ ↑C (↑p ^ i) * ↑(bind₁ (wittPolynomial p ℚ ∘ fun n => n + 1)) (xInTermsOfW p ℚ i) ^ p ^ (n - i) * ↑C (⅟↑p ^ n) -
      ↑C (↑p ^ i) * X i ^ p ^ (n + 1 - i) * ↑C (⅟↑p ^ n) =
    ∑ x in range (p ^ (n - i)),
      ↑C ↑p *
        ↑(MvPolynomial.map (Int.castRingHom ℚ))
          ((X i ^ p) ^ (p ^ (n - i) - (x + 1)) * frobeniusPolyAux p i ^ (x + 1) *
            ↑C
              ↑(Nat.choose (p ^ (n - i)) (x + 1) /
                    p ^ (n - i - v p { val := x + 1, property := (_ : 0 < Nat.succ x) }) *
                  p ^ (x - v p { val := x + 1, property := (_ : 0 < Nat.succ x) })))
[PROOFSTEP]
rw [mem_range] at hi 
[GOAL]
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
n : ℕ
IH :
  ∀ (m : ℕ),
    m < n →
      X m ^ p + ↑C (↑(Int.castRingHom ℚ) ↑p) * ↑(MvPolynomial.map (Int.castRingHom ℚ)) (frobeniusPolyAux p m) =
        ↑(bind₁ (wittPolynomial p ℚ ∘ fun n => n + 1)) (xInTermsOfW p ℚ m)
h1 : ↑p ^ n * ⅟↑p ^ n = 1
i : ℕ
hi : i < n
⊢ ↑C (↑p ^ i) * ↑(bind₁ (wittPolynomial p ℚ ∘ fun n => n + 1)) (xInTermsOfW p ℚ i) ^ p ^ (n - i) * ↑C (⅟↑p ^ n) -
      ↑C (↑p ^ i) * X i ^ p ^ (n + 1 - i) * ↑C (⅟↑p ^ n) =
    ∑ x in range (p ^ (n - i)),
      ↑C ↑p *
        ↑(MvPolynomial.map (Int.castRingHom ℚ))
          ((X i ^ p) ^ (p ^ (n - i) - (x + 1)) * frobeniusPolyAux p i ^ (x + 1) *
            ↑C
              ↑(Nat.choose (p ^ (n - i)) (x + 1) /
                    p ^ (n - i - v p { val := x + 1, property := (_ : 0 < Nat.succ x) }) *
                  p ^ (x - v p { val := x + 1, property := (_ : 0 < Nat.succ x) })))
[PROOFSTEP]
rw [← IH i hi]
[GOAL]
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
n : ℕ
IH :
  ∀ (m : ℕ),
    m < n →
      X m ^ p + ↑C (↑(Int.castRingHom ℚ) ↑p) * ↑(MvPolynomial.map (Int.castRingHom ℚ)) (frobeniusPolyAux p m) =
        ↑(bind₁ (wittPolynomial p ℚ ∘ fun n => n + 1)) (xInTermsOfW p ℚ m)
h1 : ↑p ^ n * ⅟↑p ^ n = 1
i : ℕ
hi : i < n
⊢ ↑C (↑p ^ i) *
          (X i ^ p + ↑C (↑(Int.castRingHom ℚ) ↑p) * ↑(MvPolynomial.map (Int.castRingHom ℚ)) (frobeniusPolyAux p i)) ^
            p ^ (n - i) *
        ↑C (⅟↑p ^ n) -
      ↑C (↑p ^ i) * X i ^ p ^ (n + 1 - i) * ↑C (⅟↑p ^ n) =
    ∑ x in range (p ^ (n - i)),
      ↑C ↑p *
        ↑(MvPolynomial.map (Int.castRingHom ℚ))
          ((X i ^ p) ^ (p ^ (n - i) - (x + 1)) * frobeniusPolyAux p i ^ (x + 1) *
            ↑C
              ↑(Nat.choose (p ^ (n - i)) (x + 1) /
                    p ^ (n - i - v p { val := x + 1, property := (_ : 0 < Nat.succ x) }) *
                  p ^ (x - v p { val := x + 1, property := (_ : 0 < Nat.succ x) })))
[PROOFSTEP]
clear IH
[GOAL]
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
n : ℕ
h1 : ↑p ^ n * ⅟↑p ^ n = 1
i : ℕ
hi : i < n
⊢ ↑C (↑p ^ i) *
          (X i ^ p + ↑C (↑(Int.castRingHom ℚ) ↑p) * ↑(MvPolynomial.map (Int.castRingHom ℚ)) (frobeniusPolyAux p i)) ^
            p ^ (n - i) *
        ↑C (⅟↑p ^ n) -
      ↑C (↑p ^ i) * X i ^ p ^ (n + 1 - i) * ↑C (⅟↑p ^ n) =
    ∑ x in range (p ^ (n - i)),
      ↑C ↑p *
        ↑(MvPolynomial.map (Int.castRingHom ℚ))
          ((X i ^ p) ^ (p ^ (n - i) - (x + 1)) * frobeniusPolyAux p i ^ (x + 1) *
            ↑C
              ↑(Nat.choose (p ^ (n - i)) (x + 1) /
                    p ^ (n - i - v p { val := x + 1, property := (_ : 0 < Nat.succ x) }) *
                  p ^ (x - v p { val := x + 1, property := (_ : 0 < Nat.succ x) })))
[PROOFSTEP]
rw [add_comm (X i ^ p), add_pow, sum_range_succ', pow_zero, tsub_zero, Nat.choose_zero_right, one_mul, Nat.cast_one,
  mul_one, mul_add, add_mul, Nat.succ_sub (le_of_lt hi), Nat.succ_eq_add_one (n - i), pow_succ, pow_mul, add_sub_cancel,
  mul_sum, sum_mul]
[GOAL]
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
n : ℕ
h1 : ↑p ^ n * ⅟↑p ^ n = 1
i : ℕ
hi : i < n
⊢ ∑ x in range (p ^ (n - i)),
      ↑C (↑p ^ i) *
          ((↑C (↑(Int.castRingHom ℚ) ↑p) * ↑(MvPolynomial.map (Int.castRingHom ℚ)) (frobeniusPolyAux p i)) ^ (x + 1) *
              (X i ^ p) ^ (p ^ (n - i) - (x + 1)) *
            ↑(Nat.choose (p ^ (n - i)) (x + 1))) *
        ↑C (⅟↑p ^ n) =
    ∑ x in range (p ^ (n - i)),
      ↑C ↑p *
        ↑(MvPolynomial.map (Int.castRingHom ℚ))
          ((X i ^ p) ^ (p ^ (n - i) - (x + 1)) * frobeniusPolyAux p i ^ (x + 1) *
            ↑C
              ↑(Nat.choose (p ^ (n - i)) (x + 1) /
                    p ^ (n - i - v p { val := x + 1, property := (_ : 0 < Nat.succ x) }) *
                  p ^ (x - v p { val := x + 1, property := (_ : 0 < Nat.succ x) })))
[PROOFSTEP]
apply sum_congr rfl
[GOAL]
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
n : ℕ
h1 : ↑p ^ n * ⅟↑p ^ n = 1
i : ℕ
hi : i < n
⊢ ∀ (x : ℕ),
    x ∈ range (p ^ (n - i)) →
      ↑C (↑p ^ i) *
            ((↑C (↑(Int.castRingHom ℚ) ↑p) * ↑(MvPolynomial.map (Int.castRingHom ℚ)) (frobeniusPolyAux p i)) ^ (x + 1) *
                (X i ^ p) ^ (p ^ (n - i) - (x + 1)) *
              ↑(Nat.choose (p ^ (n - i)) (x + 1))) *
          ↑C (⅟↑p ^ n) =
        ↑C ↑p *
          ↑(MvPolynomial.map (Int.castRingHom ℚ))
            ((X i ^ p) ^ (p ^ (n - i) - (x + 1)) * frobeniusPolyAux p i ^ (x + 1) *
              ↑C
                ↑(Nat.choose (p ^ (n - i)) (x + 1) /
                      p ^ (n - i - v p { val := x + 1, property := (_ : 0 < Nat.succ x) }) *
                    p ^ (x - v p { val := x + 1, property := (_ : 0 < Nat.succ x) })))
[PROOFSTEP]
intro j hj
[GOAL]
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
n : ℕ
h1 : ↑p ^ n * ⅟↑p ^ n = 1
i : ℕ
hi : i < n
j : ℕ
hj : j ∈ range (p ^ (n - i))
⊢ ↑C (↑p ^ i) *
        ((↑C (↑(Int.castRingHom ℚ) ↑p) * ↑(MvPolynomial.map (Int.castRingHom ℚ)) (frobeniusPolyAux p i)) ^ (j + 1) *
            (X i ^ p) ^ (p ^ (n - i) - (j + 1)) *
          ↑(Nat.choose (p ^ (n - i)) (j + 1))) *
      ↑C (⅟↑p ^ n) =
    ↑C ↑p *
      ↑(MvPolynomial.map (Int.castRingHom ℚ))
        ((X i ^ p) ^ (p ^ (n - i) - (j + 1)) * frobeniusPolyAux p i ^ (j + 1) *
          ↑C
            ↑(Nat.choose (p ^ (n - i)) (j + 1) / p ^ (n - i - v p { val := j + 1, property := (_ : 0 < Nat.succ j) }) *
                p ^ (j - v p { val := j + 1, property := (_ : 0 < Nat.succ j) })))
[PROOFSTEP]
rw [mem_range] at hj 
[GOAL]
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
n : ℕ
h1 : ↑p ^ n * ⅟↑p ^ n = 1
i : ℕ
hi : i < n
j : ℕ
hj : j < p ^ (n - i)
⊢ ↑C (↑p ^ i) *
        ((↑C (↑(Int.castRingHom ℚ) ↑p) * ↑(MvPolynomial.map (Int.castRingHom ℚ)) (frobeniusPolyAux p i)) ^ (j + 1) *
            (X i ^ p) ^ (p ^ (n - i) - (j + 1)) *
          ↑(Nat.choose (p ^ (n - i)) (j + 1))) *
      ↑C (⅟↑p ^ n) =
    ↑C ↑p *
      ↑(MvPolynomial.map (Int.castRingHom ℚ))
        ((X i ^ p) ^ (p ^ (n - i) - (j + 1)) * frobeniusPolyAux p i ^ (j + 1) *
          ↑C
            ↑(Nat.choose (p ^ (n - i)) (j + 1) / p ^ (n - i - v p { val := j + 1, property := (_ : 0 < Nat.succ j) }) *
                p ^ (j - v p { val := j + 1, property := (_ : 0 < Nat.succ j) })))
[PROOFSTEP]
rw [RingHom.map_mul, RingHom.map_mul, RingHom.map_pow, RingHom.map_pow, RingHom.map_pow, RingHom.map_pow,
  RingHom.map_pow, map_C, map_X, mul_pow]
[GOAL]
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
n : ℕ
h1 : ↑p ^ n * ⅟↑p ^ n = 1
i : ℕ
hi : i < n
j : ℕ
hj : j < p ^ (n - i)
⊢ ↑C ↑p ^ i *
        (↑C (↑(Int.castRingHom ℚ) ↑p) ^ (j + 1) *
              ↑(MvPolynomial.map (Int.castRingHom ℚ)) (frobeniusPolyAux p i) ^ (j + 1) *
            (X i ^ p) ^ (p ^ (n - i) - (j + 1)) *
          ↑(Nat.choose (p ^ (n - i)) (j + 1))) *
      ↑C ⅟↑p ^ n =
    ↑C ↑p *
      ((X i ^ p) ^ (p ^ (n - i) - (j + 1)) * ↑(MvPolynomial.map (Int.castRingHom ℚ)) (frobeniusPolyAux p i) ^ (j + 1) *
        ↑C
          (↑(Int.castRingHom ℚ)
            ↑(Nat.choose (p ^ (n - i)) (j + 1) / p ^ (n - i - v p { val := j + 1, property := (_ : 0 < Nat.succ j) }) *
                p ^ (j - v p { val := j + 1, property := (_ : 0 < Nat.succ j) }))))
[PROOFSTEP]
rw [mul_comm (C (p : ℚ) ^ i), mul_comm _ ((X i ^ p) ^ _), show (Int.castRingHom ℚ) ↑p = (p : ℚ) from rfl,
  mul_comm (C (p : ℚ) ^ (j + 1)), mul_comm (C (p : ℚ))]
[GOAL]
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
n : ℕ
h1 : ↑p ^ n * ⅟↑p ^ n = 1
i : ℕ
hi : i < n
j : ℕ
hj : j < p ^ (n - i)
⊢ (X i ^ p) ^ (p ^ (n - i) - (j + 1)) *
            (↑(MvPolynomial.map (Int.castRingHom ℚ)) (frobeniusPolyAux p i) ^ (j + 1) * ↑C ↑p ^ (j + 1)) *
          ↑(Nat.choose (p ^ (n - i)) (j + 1)) *
        ↑C ↑p ^ i *
      ↑C ⅟↑p ^ n =
    (X i ^ p) ^ (p ^ (n - i) - (j + 1)) * ↑(MvPolynomial.map (Int.castRingHom ℚ)) (frobeniusPolyAux p i) ^ (j + 1) *
        ↑C
          (↑(Int.castRingHom ℚ)
            ↑(Nat.choose (p ^ (n - i)) (j + 1) / p ^ (n - i - v p { val := j + 1, property := (_ : 0 < Nat.succ j) }) *
                p ^ (j - v p { val := j + 1, property := (_ : 0 < Nat.succ j) }))) *
      ↑C ↑p
[PROOFSTEP]
simp only [mul_assoc]
[GOAL]
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
n : ℕ
h1 : ↑p ^ n * ⅟↑p ^ n = 1
i : ℕ
hi : i < n
j : ℕ
hj : j < p ^ (n - i)
⊢ (X i ^ p) ^ (p ^ (n - i) - (j + 1)) *
      (↑(MvPolynomial.map (Int.castRingHom ℚ)) (frobeniusPolyAux p i) ^ (j + 1) *
        (↑C ↑p ^ (j + 1) * (↑(Nat.choose (p ^ (n - i)) (j + 1)) * (↑C ↑p ^ i * ↑C ⅟↑p ^ n)))) =
    (X i ^ p) ^ (p ^ (n - i) - (j + 1)) *
      (↑(MvPolynomial.map (Int.castRingHom ℚ)) (frobeniusPolyAux p i) ^ (j + 1) *
        (↑C
            (↑(Int.castRingHom ℚ)
              ↑(Nat.choose (p ^ (n - i)) (j + 1) /
                    p ^ (n - i - v p { val := j + 1, property := (_ : 0 < Nat.succ j) }) *
                  p ^ (j - v p { val := j + 1, property := (_ : 0 < Nat.succ j) }))) *
          ↑C ↑p))
[PROOFSTEP]
apply congr_arg
[GOAL]
case h
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
n : ℕ
h1 : ↑p ^ n * ⅟↑p ^ n = 1
i : ℕ
hi : i < n
j : ℕ
hj : j < p ^ (n - i)
⊢ ↑(MvPolynomial.map (Int.castRingHom ℚ)) (frobeniusPolyAux p i) ^ (j + 1) *
      (↑C ↑p ^ (j + 1) * (↑(Nat.choose (p ^ (n - i)) (j + 1)) * (↑C ↑p ^ i * ↑C ⅟↑p ^ n))) =
    ↑(MvPolynomial.map (Int.castRingHom ℚ)) (frobeniusPolyAux p i) ^ (j + 1) *
      (↑C
          (↑(Int.castRingHom ℚ)
            ↑(Nat.choose (p ^ (n - i)) (j + 1) / p ^ (n - i - v p { val := j + 1, property := (_ : 0 < Nat.succ j) }) *
                p ^ (j - v p { val := j + 1, property := (_ : 0 < Nat.succ j) }))) *
        ↑C ↑p)
[PROOFSTEP]
apply congr_arg
[GOAL]
case h.h
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
n : ℕ
h1 : ↑p ^ n * ⅟↑p ^ n = 1
i : ℕ
hi : i < n
j : ℕ
hj : j < p ^ (n - i)
⊢ ↑C ↑p ^ (j + 1) * (↑(Nat.choose (p ^ (n - i)) (j + 1)) * (↑C ↑p ^ i * ↑C ⅟↑p ^ n)) =
    ↑C
        (↑(Int.castRingHom ℚ)
          ↑(Nat.choose (p ^ (n - i)) (j + 1) / p ^ (n - i - v p { val := j + 1, property := (_ : 0 < Nat.succ j) }) *
              p ^ (j - v p { val := j + 1, property := (_ : 0 < Nat.succ j) }))) *
      ↑C ↑p
[PROOFSTEP]
rw [← C_eq_coe_nat]
[GOAL]
case h.h
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
n : ℕ
h1 : ↑p ^ n * ⅟↑p ^ n = 1
i : ℕ
hi : i < n
j : ℕ
hj : j < p ^ (n - i)
⊢ ↑C ↑p ^ (j + 1) * (↑C ↑(Nat.choose (p ^ (n - i)) (j + 1)) * (↑C ↑p ^ i * ↑C ⅟↑p ^ n)) =
    ↑C
        (↑(Int.castRingHom ℚ)
          ↑(Nat.choose (p ^ (n - i)) (j + 1) / p ^ (n - i - v p { val := j + 1, property := (_ : 0 < Nat.succ j) }) *
              p ^ (j - v p { val := j + 1, property := (_ : 0 < Nat.succ j) }))) *
      ↑C ↑p
[PROOFSTEP]
simp only [← RingHom.map_pow, ← C_mul]
[GOAL]
case h.h
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
n : ℕ
h1 : ↑p ^ n * ⅟↑p ^ n = 1
i : ℕ
hi : i < n
j : ℕ
hj : j < p ^ (n - i)
⊢ ↑C (↑p ^ (j + 1) * (↑(Nat.choose (p ^ (n - i)) (j + 1)) * (↑p ^ i * ⅟↑p ^ n))) =
    ↑C
      (↑(Int.castRingHom ℚ)
          ↑(Nat.choose (p ^ (n - i)) (j + 1) / p ^ (n - i - v p { val := j + 1, property := (_ : 0 < Nat.succ j) }) *
              p ^ (j - v p { val := j + 1, property := (_ : 0 < Nat.succ j) })) *
        ↑p)
[PROOFSTEP]
rw [C_inj]
[GOAL]
case h.h
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
n : ℕ
h1 : ↑p ^ n * ⅟↑p ^ n = 1
i : ℕ
hi : i < n
j : ℕ
hj : j < p ^ (n - i)
⊢ ↑p ^ (j + 1) * (↑(Nat.choose (p ^ (n - i)) (j + 1)) * (↑p ^ i * ⅟↑p ^ n)) =
    ↑(Int.castRingHom ℚ)
        ↑(Nat.choose (p ^ (n - i)) (j + 1) / p ^ (n - i - v p { val := j + 1, property := (_ : 0 < Nat.succ j) }) *
            p ^ (j - v p { val := j + 1, property := (_ : 0 < Nat.succ j) })) *
      ↑p
[PROOFSTEP]
simp only [invOf_eq_inv, eq_intCast, inv_pow, Int.cast_ofNat, Nat.cast_mul, Int.cast_mul]
[GOAL]
case h.h
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
n : ℕ
h1 : ↑p ^ n * ⅟↑p ^ n = 1
i : ℕ
hi : i < n
j : ℕ
hj : j < p ^ (n - i)
⊢ ↑p ^ (j + 1) * (↑(Nat.choose (p ^ (n - i)) (j + 1)) * (↑p ^ i * (↑p ^ n)⁻¹)) =
    ↑(Nat.choose (p ^ (n - i)) (j + 1) / p ^ (n - i - v p { val := j + 1, property := (_ : 0 < Nat.succ j) })) *
        ↑(p ^ (j - v p { val := j + 1, property := (_ : 0 < Nat.succ j) })) *
      ↑p
[PROOFSTEP]
rw [Rat.coe_nat_div _ _ (map_frobeniusPoly.key₁ p (n - i) j hj)]
[GOAL]
case h.h
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
n : ℕ
h1 : ↑p ^ n * ⅟↑p ^ n = 1
i : ℕ
hi : i < n
j : ℕ
hj : j < p ^ (n - i)
⊢ ↑p ^ (j + 1) * (↑(Nat.choose (p ^ (n - i)) (j + 1)) * (↑p ^ i * (↑p ^ n)⁻¹)) =
    ↑(Nat.choose (p ^ (n - i)) (j + 1)) / ↑(p ^ (n - i - v p { val := j + 1, property := (_ : 0 < Nat.succ j) })) *
        ↑(p ^ (j - v p { val := j + 1, property := (_ : 0 < Nat.succ j) })) *
      ↑p
[PROOFSTEP]
simp only [Nat.cast_pow, pow_add, pow_one]
[GOAL]
case h.h
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
n : ℕ
h1 : ↑p ^ n * ⅟↑p ^ n = 1
i : ℕ
hi : i < n
j : ℕ
hj : j < p ^ (n - i)
⊢ ↑p ^ j * ↑p * (↑(Nat.choose (p ^ (n - i)) (j + 1)) * (↑p ^ i * (↑p ^ n)⁻¹)) =
    ↑(Nat.choose (p ^ (n - i)) (j + 1)) / ↑p ^ (n - i - v p { val := j + 1, property := (_ : 0 < Nat.succ j) }) *
        ↑p ^ (j - v p { val := j + 1, property := (_ : 0 < Nat.succ j) }) *
      ↑p
[PROOFSTEP]
suffices
  (((p ^ (n - i)).choose (j + 1) : ℚ) * (p : ℚ) ^ (j - v p ⟨j + 1, j.succ_pos⟩) * ↑p * (p ^ n : ℚ)) =
    (p : ℚ) ^ j * p * ↑((p ^ (n - i)).choose (j + 1) * p ^ i) * (p : ℚ) ^ (n - i - v p ⟨j + 1, j.succ_pos⟩)
  by
  have aux : ∀ k : ℕ, (p : ℚ) ^ k ≠ 0 := by intro; apply pow_ne_zero; exact_mod_cast hp.1.ne_zero
  simpa [aux, -one_div, field_simps] using this.symm
[GOAL]
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
n : ℕ
h1 : ↑p ^ n * ⅟↑p ^ n = 1
i : ℕ
hi : i < n
j : ℕ
hj : j < p ^ (n - i)
this :
  ↑(Nat.choose (p ^ (n - i)) (j + 1)) * ↑p ^ (j - v p { val := j + 1, property := (_ : 0 < Nat.succ j) }) * ↑p *
      ↑(p ^ n) =
    ↑p ^ j * ↑p * ↑(Nat.choose (p ^ (n - i)) (j + 1) * p ^ i) *
      ↑p ^ (n - i - v p { val := j + 1, property := (_ : 0 < Nat.succ j) })
⊢ ↑p ^ j * ↑p * (↑(Nat.choose (p ^ (n - i)) (j + 1)) * (↑p ^ i * (↑p ^ n)⁻¹)) =
    ↑(Nat.choose (p ^ (n - i)) (j + 1)) / ↑p ^ (n - i - v p { val := j + 1, property := (_ : 0 < Nat.succ j) }) *
        ↑p ^ (j - v p { val := j + 1, property := (_ : 0 < Nat.succ j) }) *
      ↑p
[PROOFSTEP]
have aux : ∀ k : ℕ, (p : ℚ) ^ k ≠ 0 := by intro; apply pow_ne_zero; exact_mod_cast hp.1.ne_zero
[GOAL]
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
n : ℕ
h1 : ↑p ^ n * ⅟↑p ^ n = 1
i : ℕ
hi : i < n
j : ℕ
hj : j < p ^ (n - i)
this :
  ↑(Nat.choose (p ^ (n - i)) (j + 1)) * ↑p ^ (j - v p { val := j + 1, property := (_ : 0 < Nat.succ j) }) * ↑p *
      ↑(p ^ n) =
    ↑p ^ j * ↑p * ↑(Nat.choose (p ^ (n - i)) (j + 1) * p ^ i) *
      ↑p ^ (n - i - v p { val := j + 1, property := (_ : 0 < Nat.succ j) })
⊢ ∀ (k : ℕ), ↑p ^ k ≠ 0
[PROOFSTEP]
intro
[GOAL]
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
n : ℕ
h1 : ↑p ^ n * ⅟↑p ^ n = 1
i : ℕ
hi : i < n
j : ℕ
hj : j < p ^ (n - i)
this :
  ↑(Nat.choose (p ^ (n - i)) (j + 1)) * ↑p ^ (j - v p { val := j + 1, property := (_ : 0 < Nat.succ j) }) * ↑p *
      ↑(p ^ n) =
    ↑p ^ j * ↑p * ↑(Nat.choose (p ^ (n - i)) (j + 1) * p ^ i) *
      ↑p ^ (n - i - v p { val := j + 1, property := (_ : 0 < Nat.succ j) })
k✝ : ℕ
⊢ ↑p ^ k✝ ≠ 0
[PROOFSTEP]
apply pow_ne_zero
[GOAL]
case h
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
n : ℕ
h1 : ↑p ^ n * ⅟↑p ^ n = 1
i : ℕ
hi : i < n
j : ℕ
hj : j < p ^ (n - i)
this :
  ↑(Nat.choose (p ^ (n - i)) (j + 1)) * ↑p ^ (j - v p { val := j + 1, property := (_ : 0 < Nat.succ j) }) * ↑p *
      ↑(p ^ n) =
    ↑p ^ j * ↑p * ↑(Nat.choose (p ^ (n - i)) (j + 1) * p ^ i) *
      ↑p ^ (n - i - v p { val := j + 1, property := (_ : 0 < Nat.succ j) })
k✝ : ℕ
⊢ ↑p ≠ 0
[PROOFSTEP]
exact_mod_cast hp.1.ne_zero
[GOAL]
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
n : ℕ
h1 : ↑p ^ n * ⅟↑p ^ n = 1
i : ℕ
hi : i < n
j : ℕ
hj : j < p ^ (n - i)
this :
  ↑(Nat.choose (p ^ (n - i)) (j + 1)) * ↑p ^ (j - v p { val := j + 1, property := (_ : 0 < Nat.succ j) }) * ↑p *
      ↑(p ^ n) =
    ↑p ^ j * ↑p * ↑(Nat.choose (p ^ (n - i)) (j + 1) * p ^ i) *
      ↑p ^ (n - i - v p { val := j + 1, property := (_ : 0 < Nat.succ j) })
aux : ∀ (k : ℕ), ↑p ^ k ≠ 0
⊢ ↑p ^ j * ↑p * (↑(Nat.choose (p ^ (n - i)) (j + 1)) * (↑p ^ i * (↑p ^ n)⁻¹)) =
    ↑(Nat.choose (p ^ (n - i)) (j + 1)) / ↑p ^ (n - i - v p { val := j + 1, property := (_ : 0 < Nat.succ j) }) *
        ↑p ^ (j - v p { val := j + 1, property := (_ : 0 < Nat.succ j) }) *
      ↑p
[PROOFSTEP]
simpa [aux, -one_div, field_simps] using this.symm
[GOAL]
case h.h
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
n : ℕ
h1 : ↑p ^ n * ⅟↑p ^ n = 1
i : ℕ
hi : i < n
j : ℕ
hj : j < p ^ (n - i)
⊢ ↑(Nat.choose (p ^ (n - i)) (j + 1)) * ↑p ^ (j - v p { val := j + 1, property := (_ : 0 < Nat.succ j) }) * ↑p *
      ↑(p ^ n) =
    ↑p ^ j * ↑p * ↑(Nat.choose (p ^ (n - i)) (j + 1) * p ^ i) *
      ↑p ^ (n - i - v p { val := j + 1, property := (_ : 0 < Nat.succ j) })
[PROOFSTEP]
rw [mul_comm _ (p : ℚ), mul_assoc, Nat.cast_pow, mul_assoc, ← pow_add, map_frobeniusPoly.key₂ p hi.le hj, Nat.cast_mul,
  Nat.cast_pow]
[GOAL]
case h.h
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
n : ℕ
h1 : ↑p ^ n * ⅟↑p ^ n = 1
i : ℕ
hi : i < n
j : ℕ
hj : j < p ^ (n - i)
⊢ ↑p *
      (↑(Nat.choose (p ^ (n - i)) (j + 1)) *
        ↑p ^ (i + j + (n - i - v p { val := j + 1, property := (_ : 0 < Nat.succ j) }))) =
    ↑p ^ j * ↑p * (↑(Nat.choose (p ^ (n - i)) (j + 1)) * ↑p ^ i) *
      ↑p ^ (n - i - v p { val := j + 1, property := (_ : 0 < Nat.succ j) })
[PROOFSTEP]
ring
[GOAL]
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
n : ℕ
⊢ ↑(MvPolynomial.map (Int.castRingHom (ZMod p))) (frobeniusPoly p n) = X n ^ p
[PROOFSTEP]
rw [frobeniusPoly, RingHom.map_add, RingHom.map_pow, RingHom.map_mul, map_X, map_C]
[GOAL]
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
n : ℕ
⊢ X n ^ p +
      ↑C (↑(Int.castRingHom (ZMod p)) ↑p) * ↑(MvPolynomial.map (Int.castRingHom (ZMod p))) (frobeniusPolyAux p n) =
    X n ^ p
[PROOFSTEP]
simp only [Int.cast_ofNat, add_zero, eq_intCast, ZMod.nat_cast_self, zero_mul, C_0]
[GOAL]
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
n : ℕ
⊢ ↑(bind₁ (frobeniusPoly p)) (wittPolynomial p ℤ n) = wittPolynomial p ℤ (n + 1)
[PROOFSTEP]
apply MvPolynomial.map_injective (Int.castRingHom ℚ) Int.cast_injective
[GOAL]
case a
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
n : ℕ
⊢ ↑(MvPolynomial.map (Int.castRingHom ℚ)) (↑(bind₁ (frobeniusPoly p)) (wittPolynomial p ℤ n)) =
    ↑(MvPolynomial.map (Int.castRingHom ℚ)) (wittPolynomial p ℤ (n + 1))
[PROOFSTEP]
simp only [map_bind₁, map_frobeniusPoly, bind₁_frobeniusPolyRat_wittPolynomial, map_wittPolynomial]
[GOAL]
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
x : 𝕎 R
n : ℕ
⊢ coeff (frobeniusFun x) n = ↑(aeval x.coeff) (frobeniusPoly p n)
[PROOFSTEP]
rw [frobeniusFun, coeff_mk]
[GOAL]
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
⊢ ∀ ⦃R : Type ?u.420485⦄ [inst : CommRing R] (x : 𝕎 R),
    (frobeniusFun x).coeff = fun n => ↑(aeval x.coeff) (frobeniusPoly p n)
[PROOFSTEP]
intros
[GOAL]
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝² : CommRing R
inst✝¹ : CommRing S
R✝ : Type ?u.420485
inst✝ : CommRing R✝
x✝ : 𝕎 R✝
⊢ (frobeniusFun x✝).coeff = fun n => ↑(aeval x✝.coeff) (frobeniusPoly p n)
[PROOFSTEP]
funext n
[GOAL]
case h
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝² : CommRing R
inst✝¹ : CommRing S
R✝ : Type ?u.420485
inst✝ : CommRing R✝
x✝ : 𝕎 R✝
n : ℕ
⊢ coeff (frobeniusFun x✝) n = ↑(aeval x✝.coeff) (frobeniusPoly p n)
[PROOFSTEP]
apply coeff_frobeniusFun
[GOAL]
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
n : ℕ
x : 𝕎 R
⊢ ↑(ghostComponent n) (frobeniusFun x) = ↑(ghostComponent (n + 1)) x
[PROOFSTEP]
simp only [ghostComponent_apply, frobeniusFun, coeff_mk, ← bind₁_frobeniusPoly_wittPolynomial, aeval_bind₁]
[GOAL]
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
⊢ frobeniusFun 1 = 1
[PROOFSTEP]
refine
  -- Porting note: removing the placeholders give an errorIsPoly.ext
    (@IsPoly.comp p _ _ (frobeniusFun_isPoly p) WittVector.oneIsPoly)
    (@IsPoly.comp p _ _ WittVector.oneIsPoly (frobeniusFun_isPoly p)) ?_ _ 0
[GOAL]
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
⊢ ∀ (R : Type u_1) [_Rcr : CommRing R] (x : 𝕎 R) (n : ℕ),
    ↑(ghostComponent n) ((frobeniusFun ∘ fun x => 1) x) = ↑(ghostComponent n) (((fun x => 1) ∘ frobeniusFun) x)
[PROOFSTEP]
simp only [Function.comp_apply, map_one, forall_const]
[GOAL]
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
⊢ ∀ (R : Type u_1) [_Rcr : CommRing R] (n : ℕ), ↑(ghostComponent n) (frobeniusFun 1) = 1
[PROOFSTEP]
ghost_simp
[GOAL]
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
⊢ ∀ (x y : 𝕎 R),
    OneHom.toFun
        { toFun := frobeniusFun, map_one' := (_ : (frobeniusFun ∘ fun x => 1) 0 = ((fun x => 1) ∘ frobeniusFun) 0) }
        (x * y) =
      OneHom.toFun
          { toFun := frobeniusFun, map_one' := (_ : (frobeniusFun ∘ fun x => 1) 0 = ((fun x => 1) ∘ frobeniusFun) 0) }
          x *
        OneHom.toFun
          { toFun := frobeniusFun, map_one' := (_ : (frobeniusFun ∘ fun x => 1) 0 = ((fun x => 1) ∘ frobeniusFun) 0) } y
[PROOFSTEP]
ghost_calc _ _
[GOAL]
case refine_3
p : ℕ
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝ : CommRing S
R : Type u_1
R._inst : CommRing R
x✝ y✝ : 𝕎 R
⊢ ∀ (n : ℕ),
    ↑(ghostComponent n)
        (OneHom.toFun
          { toFun := frobeniusFun, map_one' := (_ : (frobeniusFun ∘ fun x => 1) 0 = ((fun x => 1) ∘ frobeniusFun) 0) }
          (x✝ * y✝)) =
      ↑(ghostComponent n)
        (OneHom.toFun
            { toFun := frobeniusFun, map_one' := (_ : (frobeniusFun ∘ fun x => 1) 0 = ((fun x => 1) ∘ frobeniusFun) 0) }
            x✝ *
          OneHom.toFun
            { toFun := frobeniusFun, map_one' := (_ : (frobeniusFun ∘ fun x => 1) 0 = ((fun x => 1) ∘ frobeniusFun) 0) }
            y✝)
[PROOFSTEP]
ghost_simp
[GOAL]
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
⊢ OneHom.toFun
      (↑{
          toOneHom :=
            { toFun := frobeniusFun,
              map_one' := (_ : (frobeniusFun ∘ fun x => 1) 0 = ((fun x => 1) ∘ frobeniusFun) 0) },
          map_mul' :=
            (_ :
              ∀ (x y : 𝕎 R),
                OneHom.toFun
                    { toFun := frobeniusFun,
                      map_one' := (_ : (frobeniusFun ∘ fun x => 1) 0 = ((fun x => 1) ∘ frobeniusFun) 0) }
                    (x * y) =
                  OneHom.toFun
                      { toFun := frobeniusFun,
                        map_one' := (_ : (frobeniusFun ∘ fun x => 1) 0 = ((fun x => 1) ∘ frobeniusFun) 0) }
                      x *
                    OneHom.toFun
                      { toFun := frobeniusFun,
                        map_one' := (_ : (frobeniusFun ∘ fun x => 1) 0 = ((fun x => 1) ∘ frobeniusFun) 0) }
                      y) })
      0 =
    0
[PROOFSTEP]
refine
  IsPoly.ext (@IsPoly.comp p _ _ (frobeniusFun_isPoly p) WittVector.zeroIsPoly)
    (@IsPoly.comp p _ _ WittVector.zeroIsPoly (frobeniusFun_isPoly p)) ?_ _ 0
[GOAL]
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
⊢ ∀ (R : Type u_1) [_Rcr : CommRing R] (x : 𝕎 R) (n : ℕ),
    ↑(ghostComponent n) ((frobeniusFun ∘ fun x => 0) x) = ↑(ghostComponent n) (((fun x => 0) ∘ frobeniusFun) x)
[PROOFSTEP]
simp only [Function.comp_apply, map_zero, forall_const]
[GOAL]
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
⊢ ∀ (R : Type u_1) [_Rcr : CommRing R] (n : ℕ), ↑(ghostComponent n) (frobeniusFun 0) = 0
[PROOFSTEP]
ghost_simp
[GOAL]
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
⊢ ∀ (x y : 𝕎 R),
    OneHom.toFun
        (↑{
            toOneHom :=
              { toFun := frobeniusFun,
                map_one' := (_ : (frobeniusFun ∘ fun x => 1) 0 = ((fun x => 1) ∘ frobeniusFun) 0) },
            map_mul' :=
              (_ :
                ∀ (x y : 𝕎 R),
                  OneHom.toFun
                      { toFun := frobeniusFun,
                        map_one' := (_ : (frobeniusFun ∘ fun x => 1) 0 = ((fun x => 1) ∘ frobeniusFun) 0) }
                      (x * y) =
                    OneHom.toFun
                        { toFun := frobeniusFun,
                          map_one' := (_ : (frobeniusFun ∘ fun x => 1) 0 = ((fun x => 1) ∘ frobeniusFun) 0) }
                        x *
                      OneHom.toFun
                        { toFun := frobeniusFun,
                          map_one' := (_ : (frobeniusFun ∘ fun x => 1) 0 = ((fun x => 1) ∘ frobeniusFun) 0) }
                        y) })
        (x + y) =
      OneHom.toFun
          (↑{
              toOneHom :=
                { toFun := frobeniusFun,
                  map_one' := (_ : (frobeniusFun ∘ fun x => 1) 0 = ((fun x => 1) ∘ frobeniusFun) 0) },
              map_mul' :=
                (_ :
                  ∀ (x y : 𝕎 R),
                    OneHom.toFun
                        { toFun := frobeniusFun,
                          map_one' := (_ : (frobeniusFun ∘ fun x => 1) 0 = ((fun x => 1) ∘ frobeniusFun) 0) }
                        (x * y) =
                      OneHom.toFun
                          { toFun := frobeniusFun,
                            map_one' := (_ : (frobeniusFun ∘ fun x => 1) 0 = ((fun x => 1) ∘ frobeniusFun) 0) }
                          x *
                        OneHom.toFun
                          { toFun := frobeniusFun,
                            map_one' := (_ : (frobeniusFun ∘ fun x => 1) 0 = ((fun x => 1) ∘ frobeniusFun) 0) }
                          y) })
          x +
        OneHom.toFun
          (↑{
              toOneHom :=
                { toFun := frobeniusFun,
                  map_one' := (_ : (frobeniusFun ∘ fun x => 1) 0 = ((fun x => 1) ∘ frobeniusFun) 0) },
              map_mul' :=
                (_ :
                  ∀ (x y : 𝕎 R),
                    OneHom.toFun
                        { toFun := frobeniusFun,
                          map_one' := (_ : (frobeniusFun ∘ fun x => 1) 0 = ((fun x => 1) ∘ frobeniusFun) 0) }
                        (x * y) =
                      OneHom.toFun
                          { toFun := frobeniusFun,
                            map_one' := (_ : (frobeniusFun ∘ fun x => 1) 0 = ((fun x => 1) ∘ frobeniusFun) 0) }
                          x *
                        OneHom.toFun
                          { toFun := frobeniusFun,
                            map_one' := (_ : (frobeniusFun ∘ fun x => 1) 0 = ((fun x => 1) ∘ frobeniusFun) 0) }
                          y) })
          y
[PROOFSTEP]
ghost_calc _ _
[GOAL]
case refine_3
p : ℕ
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝ : CommRing S
R : Type u_1
R._inst : CommRing R
x✝ y✝ : 𝕎 R
⊢ ∀ (n : ℕ),
    ↑(ghostComponent n)
        (OneHom.toFun
          (↑{
              toOneHom :=
                { toFun := frobeniusFun,
                  map_one' := (_ : (frobeniusFun ∘ fun x => 1) 0 = ((fun x => 1) ∘ frobeniusFun) 0) },
              map_mul' :=
                (_ :
                  ∀ (x y : 𝕎 R),
                    OneHom.toFun
                        { toFun := frobeniusFun,
                          map_one' := (_ : (frobeniusFun ∘ fun x => 1) 0 = ((fun x => 1) ∘ frobeniusFun) 0) }
                        (x * y) =
                      OneHom.toFun
                          { toFun := frobeniusFun,
                            map_one' := (_ : (frobeniusFun ∘ fun x => 1) 0 = ((fun x => 1) ∘ frobeniusFun) 0) }
                          x *
                        OneHom.toFun
                          { toFun := frobeniusFun,
                            map_one' := (_ : (frobeniusFun ∘ fun x => 1) 0 = ((fun x => 1) ∘ frobeniusFun) 0) }
                          y) })
          (x✝ + y✝)) =
      ↑(ghostComponent n)
        (OneHom.toFun
            (↑{
                toOneHom :=
                  { toFun := frobeniusFun,
                    map_one' := (_ : (frobeniusFun ∘ fun x => 1) 0 = ((fun x => 1) ∘ frobeniusFun) 0) },
                map_mul' :=
                  (_ :
                    ∀ (x y : 𝕎 R),
                      OneHom.toFun
                          { toFun := frobeniusFun,
                            map_one' := (_ : (frobeniusFun ∘ fun x => 1) 0 = ((fun x => 1) ∘ frobeniusFun) 0) }
                          (x * y) =
                        OneHom.toFun
                            { toFun := frobeniusFun,
                              map_one' := (_ : (frobeniusFun ∘ fun x => 1) 0 = ((fun x => 1) ∘ frobeniusFun) 0) }
                            x *
                          OneHom.toFun
                            { toFun := frobeniusFun,
                              map_one' := (_ : (frobeniusFun ∘ fun x => 1) 0 = ((fun x => 1) ∘ frobeniusFun) 0) }
                            y) })
            x✝ +
          OneHom.toFun
            (↑{
                toOneHom :=
                  { toFun := frobeniusFun,
                    map_one' := (_ : (frobeniusFun ∘ fun x => 1) 0 = ((fun x => 1) ∘ frobeniusFun) 0) },
                map_mul' :=
                  (_ :
                    ∀ (x y : 𝕎 R),
                      OneHom.toFun
                          { toFun := frobeniusFun,
                            map_one' := (_ : (frobeniusFun ∘ fun x => 1) 0 = ((fun x => 1) ∘ frobeniusFun) 0) }
                          (x * y) =
                        OneHom.toFun
                            { toFun := frobeniusFun,
                              map_one' := (_ : (frobeniusFun ∘ fun x => 1) 0 = ((fun x => 1) ∘ frobeniusFun) 0) }
                            x *
                          OneHom.toFun
                            { toFun := frobeniusFun,
                              map_one' := (_ : (frobeniusFun ∘ fun x => 1) 0 = ((fun x => 1) ∘ frobeniusFun) 0) }
                            y) })
            y✝)
[PROOFSTEP]
ghost_simp
[GOAL]
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CharP R p
x : 𝕎 R
n : ℕ
⊢ coeff (↑frobenius x) n = coeff x n ^ p
[PROOFSTEP]
rw [coeff_frobenius]
[GOAL]
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CharP R p
x : 𝕎 R
n : ℕ
⊢ ↑(aeval x.coeff) (frobeniusPoly p n) = coeff x n ^ p
[PROOFSTEP]
letI : Algebra (ZMod p) R :=
  ZMod.algebra _
    _
      -- outline of the calculation, proofs follow below
[GOAL]
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CharP R p
x : 𝕎 R
n : ℕ
this : Algebra (ZMod p) R := ZMod.algebra R p
⊢ ↑(aeval x.coeff) (frobeniusPoly p n) = coeff x n ^ p
[PROOFSTEP]
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 := ?_
[GOAL]
case calc_1
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CharP R p
x : 𝕎 R
n : ℕ
this : Algebra (ZMod p) R := ZMod.algebra R p
⊢ ↑(aeval fun k => coeff x k) (frobeniusPoly p n) =
    ↑(aeval fun k => coeff x k) (↑(MvPolynomial.map (Int.castRingHom (ZMod p))) (frobeniusPoly p n))
[PROOFSTEP]
conv_rhs => rw [aeval_eq_eval₂Hom, eval₂Hom_map_hom]
[GOAL]
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CharP R p
x : 𝕎 R
n : ℕ
this : Algebra (ZMod p) R := ZMod.algebra R p
| ↑(aeval fun k => coeff x k) (↑(MvPolynomial.map (Int.castRingHom (ZMod p))) (frobeniusPoly p n))
[PROOFSTEP]
rw [aeval_eq_eval₂Hom, eval₂Hom_map_hom]
[GOAL]
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CharP R p
x : 𝕎 R
n : ℕ
this : Algebra (ZMod p) R := ZMod.algebra R p
| ↑(aeval fun k => coeff x k) (↑(MvPolynomial.map (Int.castRingHom (ZMod p))) (frobeniusPoly p n))
[PROOFSTEP]
rw [aeval_eq_eval₂Hom, eval₂Hom_map_hom]
[GOAL]
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CharP R p
x : 𝕎 R
n : ℕ
this : Algebra (ZMod p) R := ZMod.algebra R p
| ↑(aeval fun k => coeff x k) (↑(MvPolynomial.map (Int.castRingHom (ZMod p))) (frobeniusPoly p n))
[PROOFSTEP]
rw [aeval_eq_eval₂Hom, eval₂Hom_map_hom]
[GOAL]
case calc_1
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CharP R p
x : 𝕎 R
n : ℕ
this : Algebra (ZMod p) R := ZMod.algebra R p
⊢ ↑(aeval fun k => coeff x k) (frobeniusPoly p n) =
    ↑(eval₂Hom (RingHom.comp (algebraMap (ZMod p) R) (Int.castRingHom (ZMod p))) fun k => coeff x k) (frobeniusPoly p n)
[PROOFSTEP]
apply eval₂Hom_congr (RingHom.ext_int _ _) rfl rfl
[GOAL]
case calc_2
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CharP R p
x : 𝕎 R
n : ℕ
this : Algebra (ZMod p) R := ZMod.algebra R p
⊢ ↑(aeval fun k => coeff x k) (↑(MvPolynomial.map (Int.castRingHom (ZMod p))) (frobeniusPoly p n)) =
    ↑(aeval fun k => coeff x k) (X n ^ p)
[PROOFSTEP]
rw [frobeniusPoly_zmod]
[GOAL]
case calc_3
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CharP R p
x : 𝕎 R
n : ℕ
this : Algebra (ZMod p) R := ZMod.algebra R p
⊢ ↑(aeval fun k => coeff x k) (X n ^ p) = coeff x n ^ p
[PROOFSTEP]
rw [map_pow, aeval_X]
[GOAL]
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CharP R p
⊢ frobenius = map (_root_.frobenius R p)
[PROOFSTEP]
ext (x n)
[GOAL]
case a.h
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CharP R p
x : 𝕎 R
n : ℕ
⊢ coeff (↑frobenius x) n = coeff (↑(map (_root_.frobenius R p)) x) n
[PROOFSTEP]
simp only [coeff_frobenius_charP, map_coeff, frobenius_def]
[GOAL]
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CharP R p
x : 𝕎 (ZMod p)
⊢ ↑frobenius x = x
[PROOFSTEP]
simp only [ext_iff, coeff_frobenius_charP, ZMod.pow_card, eq_self_iff_true, forall_const]
[GOAL]
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : CharP R p
inst✝ : PerfectRing R p
src✝ : 𝕎 R →+* 𝕎 R := frobenius
f : 𝕎 R
n : ℕ
⊢ coeff (↑(map ↑(RingEquiv.symm (_root_.frobeniusEquiv R p))) (↑frobenius f)) n = coeff f n
[PROOFSTEP]
rw [frobenius_eq_map_frobenius]
[GOAL]
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : CharP R p
inst✝ : PerfectRing R p
src✝ : 𝕎 R →+* 𝕎 R := frobenius
f : 𝕎 R
n : ℕ
⊢ coeff (↑(map ↑(RingEquiv.symm (_root_.frobeniusEquiv R p))) (↑(map (_root_.frobenius R p)) f)) n = coeff f n
[PROOFSTEP]
exact frobeniusEquiv_symm_apply_frobenius R p _
[GOAL]
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : CharP R p
inst✝ : PerfectRing R p
src✝ : 𝕎 R →+* 𝕎 R := frobenius
f : 𝕎 R
n : ℕ
⊢ coeff (↑frobenius (↑(map ↑(RingEquiv.symm (_root_.frobeniusEquiv R p))) f)) n = coeff f n
[PROOFSTEP]
rw [frobenius_eq_map_frobenius]
[GOAL]
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : CharP R p
inst✝ : PerfectRing R p
src✝ : 𝕎 R →+* 𝕎 R := frobenius
f : 𝕎 R
n : ℕ
⊢ coeff (↑(map (_root_.frobenius R p)) (↑(map ↑(RingEquiv.symm (_root_.frobeniusEquiv R p))) f)) n = coeff f n
[PROOFSTEP]
exact frobenius_apply_frobeniusEquiv_symm R p _
