-- Mathlib/RingTheory/WittVector/Frobenius.lean
theorem map_frobeniusPoly (n : ℕ) :
    MvPolynomial.map (Int.castRingHom ℚ) (frobeniusPoly p n) = frobeniusPolyRat p n

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ ∀ (n : ℕ),
    (∀ m < n,
        X m ^ p + C ↑p * (MvPolynomial.map (Int.castRingHom ℚ)) (frobeniusPolyAux p m) =
          (bind₁ (wittPolynomial p ℚ ∘ fun n => n + 1)) (xInTermsOfW p ℚ m)) →
      X n ^ p + C ↑p * (MvPolynomial.map (Int.castRingHom ℚ)) (frobeniusPolyAux p n) =
        (bind₁ (wittPolynomial p ℚ ∘ fun n => n + 1)) (xInTermsOfW p ℚ n)

Tactic:
clear n

Result:
p : ℕ
hp : Fact (Nat.Prime p)
⊢ ∀ (n : ℕ),
    (∀ m < n,
        X m ^ p + C ↑p * (MvPolynomial.map (Int.castRingHom ℚ)) (frobeniusPolyAux p m) =
          (bind₁ (wittPolynomial p ℚ ∘ fun n => n + 1)) (xInTermsOfW p ℚ m)) →
      X n ^ p + C ↑p * (MvPolynomial.map (Int.castRingHom ℚ)) (frobeniusPolyAux p n) =
        (bind₁ (wittPolynomial p ℚ ∘ fun n => n + 1)) (xInTermsOfW p ℚ n)

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
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)) *
          ↑((p ^ (n - i)).choose (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 ℚ) ↑((p ^ (n - i)).choose (j + 1) / p ^ (n - i - v p (j + 1)) * p ^ (j - v p (j + 1)))) *
      C ↑p

Tactic:
simp only [mul_assoc]

Result:
p : ℕ
hp : Fact (Nat.Prime p)
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) * (↑((p ^ (n - i)).choose (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 ℚ) ↑((p ^ (n - i)).choose (j + 1) / p ^ (n - i - v p (j + 1)) * p ^ (j - v p (j + 1)))) *
          C ↑p))

Proof state:
case h
p : ℕ
hp : Fact (Nat.Prime p)
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) * (↑((p ^ (n - i)).choose (j + 1)) * (C ↑p ^ i * C ⅟↑p ^ n))) =
    (MvPolynomial.map (Int.castRingHom ℚ)) (frobeniusPolyAux p i) ^ (j + 1) *
      (C ((Int.castRingHom ℚ) ↑((p ^ (n - i)).choose (j + 1) / p ^ (n - i - v p (j + 1)) * p ^ (j - v p (j + 1)))) *
        C ↑p)

Tactic:
apply congr_arg

Result:
case h.h
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
h1 : ↑p ^ n * ⅟↑p ^ n = 1
i : ℕ
hi : i < n
j : ℕ
hj : j < p ^ (n - i)
⊢ C ↑p ^ (j + 1) * (↑((p ^ (n - i)).choose (j + 1)) * (C ↑p ^ i * C ⅟↑p ^ n)) =
    C ((Int.castRingHom ℚ) ↑((p ^ (n - i)).choose (j + 1) / p ^ (n - i - v p (j + 1)) * p ^ (j - v p (j + 1)))) * C ↑p

Proof state:
case h.h
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
h1 : ↑p ^ n * ⅟↑p ^ n = 1
i : ℕ
hi : i < n
j : ℕ
hj : j < p ^ (n - i)
⊢ ↑p ^ (j + 1) * (↑((p ^ (n - i)).choose (j + 1)) * (↑p ^ i * (↑p ^ n)⁻¹)) =
    ↑((p ^ (n - i)).choose (j + 1)) / ↑(p ^ (n - i - v p (j + 1))) * ↑(p ^ (j - v p (j + 1))) * ↑p

Tactic:
simp only [Nat.cast_pow, pow_add, pow_one]

Result:
case h.h
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
h1 : ↑p ^ n * ⅟↑p ^ n = 1
i : ℕ
hi : i < n
j : ℕ
hj : j < p ^ (n - i)
⊢ ↑p ^ j * ↑p * (↑((p ^ (n - i)).choose (j + 1)) * (↑p ^ i * (↑p ^ n)⁻¹)) =
    ↑((p ^ (n - i)).choose (j + 1)) / ↑p ^ (n - i - v p (j + 1)) * ↑p ^ (j - v p (j + 1)) * ↑p

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
IH :
  ∀ m < n,
    X m ^ p + C ↑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 ∈ 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 ∈ range n,
      ∑ i ∈ range (p ^ (n - x)),
        C ↑p *
          (MvPolynomial.map (Int.castRingHom ℚ))
            ((X x ^ p) ^ (p ^ (n - x) - (i + 1)) * frobeniusPolyAux p x ^ (i + 1) *
              C ↑((p ^ (n - x)).choose (i + 1) / p ^ (n - x - v p (i + 1)) * p ^ (i - v p (i + 1))))

Tactic:
apply sum_congr rfl

Result:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
IH :
  ∀ m < n,
    X m ^ p + C ↑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 ∈ 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) =
      ∑ i ∈ range (p ^ (n - x)),
        C ↑p *
          (MvPolynomial.map (Int.castRingHom ℚ))
            ((X x ^ p) ^ (p ^ (n - x) - (i + 1)) * frobeniusPolyAux p x ^ (i + 1) *
              C ↑((p ^ (n - x)).choose (i + 1) / p ^ (n - x - v p (i + 1)) * p ^ (i - v p (i + 1))))

Proof state:
case h.h
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
h1 : ↑p ^ n * ⅟↑p ^ n = 1
i : ℕ
hi : i < n
j : ℕ
hj : j < p ^ (n - i)
⊢ ↑p * (↑((p ^ (n - i)).choose (j + 1)) * ↑p ^ (i + j + (n - i - v p (j + 1)))) =
    ↑p ^ j * ↑p * (↑((p ^ (n - i)).choose (j + 1)) * ↑p ^ i) * ↑p ^ (n - i - v p (j + 1))

Tactic:
ring

Result:
no goals

Proof state:
case h.h
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
h1 : ↑p ^ n * ⅟↑p ^ n = 1
i : ℕ
hi : i < n
j : ℕ
hj : j < p ^ (n - i)
⊢ ↑p ^ (j + 1) * (↑((p ^ (n - i)).choose (j + 1)) * (↑p ^ i * (↑p ^ n)⁻¹)) =
    ↑((p ^ (n - i)).choose (j + 1) / p ^ (n - i - v p (j + 1))) * ↑(p ^ (j - v p (j + 1))) * ↑p

Tactic:
rw [Rat.natCast_div _ _ (map_frobeniusPoly.key₁ p (n - i) j hj)]

Result:
case h.h
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
h1 : ↑p ^ n * ⅟↑p ^ n = 1
i : ℕ
hi : i < n
j : ℕ
hj : j < p ^ (n - i)
⊢ ↑p ^ (j + 1) * (↑((p ^ (n - i)).choose (j + 1)) * (↑p ^ i * (↑p ^ n)⁻¹)) =
    ↑((p ^ (n - i)).choose (j + 1)) / ↑(p ^ (n - i - v p (j + 1))) * ↑(p ^ (j - v p (j + 1))) * ↑p

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
h1 : ↑p ^ n * ⅟↑p ^ n = 1
i : ℕ
hi : i < n
j : ℕ
hj : j < p ^ (n - i)
this :
  ↑((p ^ (n - i)).choose (j + 1)) * ↑p ^ (j - v p (j + 1)) * ↑p * ↑p ^ n =
    ↑p ^ j * ↑p * ↑((p ^ (n - i)).choose (j + 1) * p ^ i) * ↑p ^ (n - i - v p (j + 1))
aux : ∀ (k : ℕ), ↑p ^ k ≠ 0
⊢ ↑p ^ j * ↑p * (↑((p ^ (n - i)).choose (j + 1)) * (↑p ^ i * (↑p ^ n)⁻¹)) =
    ↑((p ^ (n - i)).choose (j + 1)) / ↑p ^ (n - i - v p (j + 1)) * ↑p ^ (j - v p (j + 1)) * ↑p

Tactic:
simpa [aux, -one_div, -pow_eq_zero_iff', field_simps] using this.symm

Result:
no goals