awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Frobenius (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
h1 :
  HPow.hPow (α := ℚ) (↑p : ℚ) n *
      HPow.hPow (α := ℚ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑p : ℚ) _) n =
    1
i : ℕ
hi : i < n
j : ℕ
hj : j < p ^ (n - i)
⊢ HMul.hMul (β := MvPolynomial ℕ ℚ)
      (HMul.hMul (α := MvPolynomial ℕ ℚ)
        ((C : (a : ℚ) → MvPolynomial ℕ ℚ) (HPow.hPow (α := ℚ) (↑p : ℚ) i) : MvPolynomial ℕ ℚ)
        (HMul.hMul (α := MvPolynomial ℕ ℚ) (β := MvPolynomial ℕ ℚ)
                ((C : (a : ℚ) → MvPolynomial ℕ ℚ) (↑p : ℚ) : MvPolynomial ℕ ℚ)
                ((MvPolynomial.map (Int.castRingHom ℚ) : (a : MvPolynomial ℕ ℤ) → MvPolynomial ℕ ℚ)
                    (frobeniusPolyAux p i) :
                  MvPolynomial ℕ ℚ) ^
              (j + 1) *
            HPow.hPow (α := MvPolynomial ℕ ℚ) (X i) p ^ (p ^ (n - i) - (j + 1)) *
          (↑((p ^ (n - i)).choose (j + 1)) : MvPolynomial ℕ ℚ)))
      ((C : (a : ℚ) → MvPolynomial ℕ ℚ)
          (HPow.hPow (α := ℚ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑p : ℚ) _) n) :
        MvPolynomial ℕ ℚ) =
    HMul.hMul (α := MvPolynomial ℕ ℚ) (β := MvPolynomial ℕ ℚ)
      ((C : (a : ℚ) → MvPolynomial ℕ ℚ) (↑p : ℚ) : MvPolynomial ℕ ℚ)
      ((MvPolynomial.map (Int.castRingHom ℚ) : (a : MvPolynomial ℕ ℤ) → MvPolynomial ℕ ℚ)
          (HPow.hPow (α := MvPolynomial ℕ ℤ) (X i) p ^ (p ^ (n - i) - (j + 1)) * frobeniusPolyAux p i ^ (j + 1) *
            (C : (a : ℤ) → MvPolynomial ℕ ℤ)
              (↑((p ^ (n - i)).choose (j + 1) / p ^ (n - i - v p (j + 1)) * p ^ (j - v p (j + 1))) : ℤ)) :
        MvPolynomial ℕ ℚ)
have rw : HPow.hPow (α := MvPolynomial ℕ ℚ) ((C : (a : ℚ) → MvPolynomial ℕ ℚ) (↑p : ℚ)) i *
      (HPow.hPow (α := MvPolynomial ℕ ℚ) ((C : (a : ℚ) → MvPolynomial ℕ ℚ) (↑p : ℚ)) (j + 1) *
            HPow.hPow (α := MvPolynomial ℕ ℚ)
              ((MvPolynomial.map (Int.castRingHom ℚ) : (a : MvPolynomial ℕ ℤ) → MvPolynomial ℕ ℚ)
                  (frobeniusPolyAux p i) :
                MvPolynomial ℕ ℚ)
              (j + 1) *
          HPow.hPow (α := MvPolynomial ℕ ℚ) (X i) p ^ (p ^ (n - i) - (j + 1)) *
        (↑((p ^ (n - i)).choose (j + 1)) : MvPolynomial ℕ ℚ)) *
    HPow.hPow (α := MvPolynomial ℕ ℚ)
      ((C : (a : ℚ) → MvPolynomial ℕ ℚ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑p : ℚ) _)) n =
  (C : (a : ℚ) → MvPolynomial ℕ ℚ) (↑p : ℚ) *
    HMul.hMul (β := MvPolynomial ℕ ℚ)
      (HPow.hPow (α := MvPolynomial ℕ ℚ) (X i) p ^ (p ^ (n - i) - (j + 1)) *
        HPow.hPow (α := MvPolynomial ℕ ℚ)
          ((MvPolynomial.map (Int.castRingHom ℚ) : (a : MvPolynomial ℕ ℤ) → MvPolynomial ℕ ℚ) (frobeniusPolyAux p i) :
            MvPolynomial ℕ ℚ)
          (j + 1))
      ((C : (a : ℚ) → MvPolynomial ℕ ℚ)
          ((Int.castRingHom ℚ : (a : ℤ) → ℚ)
            (↑((p ^ (n - i)).choose (j + 1) / p ^ (n - i - v p (j + 1)) * p ^ (j - v p (j + 1))) : ℤ)) :
        MvPolynomial ℕ ℚ)
Tactic: rw [map_mul, map_mul, map_pow, map_pow, map_pow, map_pow, map_pow, map_C, map_X, mul_pow]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Frobenius (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
h1 :
  HPow.hPow (α := ℚ) (↑p : ℚ) n *
      HPow.hPow (α := ℚ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑p : ℚ) _) n =
    1
i : ℕ
hi : i < n
j : ℕ
hj : j < p ^ (n - i)
⊢ HPow.hPow (α := MvPolynomial ℕ ℚ) ((C : (a : ℚ) → MvPolynomial ℕ ℚ) (↑p : ℚ)) i *
        (HPow.hPow (α := MvPolynomial ℕ ℚ) ((C : (a : ℚ) → MvPolynomial ℕ ℚ) (↑p : ℚ)) (j + 1) *
              HPow.hPow (α := MvPolynomial ℕ ℚ)
                ((MvPolynomial.map (Int.castRingHom ℚ) : (a : MvPolynomial ℕ ℤ) → MvPolynomial ℕ ℚ)
                    (frobeniusPolyAux p i) :
                  MvPolynomial ℕ ℚ)
                (j + 1) *
            HPow.hPow (α := MvPolynomial ℕ ℚ) (X i) p ^ (p ^ (n - i) - (j + 1)) *
          (↑((p ^ (n - i)).choose (j + 1)) : MvPolynomial ℕ ℚ)) *
      HPow.hPow (α := MvPolynomial ℕ ℚ)
        ((C : (a : ℚ) → MvPolynomial ℕ ℚ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑p : ℚ) _)) n =
    (C : (a : ℚ) → MvPolynomial ℕ ℚ) (↑p : ℚ) *
      HMul.hMul (β := MvPolynomial ℕ ℚ)
        (HPow.hPow (α := MvPolynomial ℕ ℚ) (X i) p ^ (p ^ (n - i) - (j + 1)) *
          HPow.hPow (α := MvPolynomial ℕ ℚ)
            ((MvPolynomial.map (Int.castRingHom ℚ) : (a : MvPolynomial ℕ ℤ) → MvPolynomial ℕ ℚ) (frobeniusPolyAux p i) :
              MvPolynomial ℕ ℚ)
            (j + 1))
        ((C : (a : ℚ) → MvPolynomial ℕ ℚ)
            ((Int.castRingHom ℚ : (a : ℤ) → ℚ)
              (↑((p ^ (n - i)).choose (j + 1) / p ^ (n - i - v p (j + 1)) * p ^ (j - v p (j + 1))) : ℤ)) :
          MvPolynomial ℕ ℚ)
have rw : HPow.hPow (α := MvPolynomial ℕ ℚ) (X i) p ^ (p ^ (n - i) - (j + 1)) *
          (HPow.hPow (α := MvPolynomial ℕ ℚ)
              ((MvPolynomial.map (Int.castRingHom ℚ) : (a : MvPolynomial ℕ ℤ) → MvPolynomial ℕ ℚ)
                  (frobeniusPolyAux p i) :
                MvPolynomial ℕ ℚ)
              (j + 1) *
            HPow.hPow (α := MvPolynomial ℕ ℚ) ((C : (a : ℚ) → MvPolynomial ℕ ℚ) (↑p : ℚ)) (j + 1)) *
        (↑((p ^ (n - i)).choose (j + 1)) : MvPolynomial ℕ ℚ) *
      HPow.hPow (α := MvPolynomial ℕ ℚ) ((C : (a : ℚ) → MvPolynomial ℕ ℚ) (↑p : ℚ)) i *
    HPow.hPow (α := MvPolynomial ℕ ℚ)
      ((C : (a : ℚ) → MvPolynomial ℕ ℚ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑p : ℚ) _)) n =
  HMul.hMul (β := MvPolynomial ℕ ℚ)
      (HPow.hPow (α := MvPolynomial ℕ ℚ) (X i) p ^ (p ^ (n - i) - (j + 1)) *
        HPow.hPow (α := MvPolynomial ℕ ℚ)
          ((MvPolynomial.map (Int.castRingHom ℚ) : (a : MvPolynomial ℕ ℤ) → MvPolynomial ℕ ℚ) (frobeniusPolyAux p i) :
            MvPolynomial ℕ ℚ)
          (j + 1))
      ((C : (a : ℚ) → MvPolynomial ℕ ℚ)
          ((Int.castRingHom ℚ : (a : ℤ) → ℚ)
            (↑((p ^ (n - i)).choose (j + 1) / p ^ (n - i - v p (j + 1)) * p ^ (j - v p (j + 1))) : ℤ)) :
        MvPolynomial ℕ ℚ) *
    (C : (a : ℚ) → MvPolynomial ℕ ℚ) (↑p : ℚ)
Tactic: rw [mul_comm (C (p : ℚ) ^ i), mul_comm _ ((X i ^ p) ^ _), mul_comm (C (p : ℚ) ^ (j + 1)),
    mul_comm (C (p : ℚ))]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Frobenius (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
h1 :
  HPow.hPow (α := ℚ) (↑p : ℚ) n *
      HPow.hPow (α := ℚ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑p : ℚ) _) n =
    1
i : ℕ
hi : i < n
j : ℕ
hj : j < p ^ (n - i)
⊢ HPow.hPow (α := MvPolynomial ℕ ℚ) (X i) p ^ (p ^ (n - i) - (j + 1)) *
            (HPow.hPow (α := MvPolynomial ℕ ℚ)
                ((MvPolynomial.map (Int.castRingHom ℚ) : (a : MvPolynomial ℕ ℤ) → MvPolynomial ℕ ℚ)
                    (frobeniusPolyAux p i) :
                  MvPolynomial ℕ ℚ)
                (j + 1) *
              HPow.hPow (α := MvPolynomial ℕ ℚ) ((C : (a : ℚ) → MvPolynomial ℕ ℚ) (↑p : ℚ)) (j + 1)) *
          (↑((p ^ (n - i)).choose (j + 1)) : MvPolynomial ℕ ℚ) *
        HPow.hPow (α := MvPolynomial ℕ ℚ) ((C : (a : ℚ) → MvPolynomial ℕ ℚ) (↑p : ℚ)) i *
      HPow.hPow (α := MvPolynomial ℕ ℚ)
        ((C : (a : ℚ) → MvPolynomial ℕ ℚ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑p : ℚ) _)) n =
    HMul.hMul (β := MvPolynomial ℕ ℚ)
        (HPow.hPow (α := MvPolynomial ℕ ℚ) (X i) p ^ (p ^ (n - i) - (j + 1)) *
          HPow.hPow (α := MvPolynomial ℕ ℚ)
            ((MvPolynomial.map (Int.castRingHom ℚ) : (a : MvPolynomial ℕ ℤ) → MvPolynomial ℕ ℚ) (frobeniusPolyAux p i) :
              MvPolynomial ℕ ℚ)
            (j + 1))
        ((C : (a : ℚ) → MvPolynomial ℕ ℚ)
            ((Int.castRingHom ℚ : (a : ℤ) → ℚ)
              (↑((p ^ (n - i)).choose (j + 1) / p ^ (n - i - v p (j + 1)) * p ^ (j - v p (j + 1))) : ℤ)) :
          MvPolynomial ℕ ℚ) *
      (C : (a : ℚ) → MvPolynomial ℕ ℚ) (↑p : ℚ)
have simp : HPow.hPow (α := MvPolynomial ℕ ℚ) (X i) p ^ (p ^ (n - i) - (j + 1)) *
    (HPow.hPow (α := MvPolynomial ℕ ℚ)
        ((MvPolynomial.map (Int.castRingHom ℚ) : (a : MvPolynomial ℕ ℤ) → MvPolynomial ℕ ℚ) (frobeniusPolyAux p i) :
          MvPolynomial ℕ ℚ)
        (j + 1) *
      (HPow.hPow (α := MvPolynomial ℕ ℚ) ((C : (a : ℚ) → MvPolynomial ℕ ℚ) (↑p : ℚ)) (j + 1) *
        ((↑((p ^ (n - i)).choose (j + 1)) : MvPolynomial ℕ ℚ) *
          (HPow.hPow (α := MvPolynomial ℕ ℚ) ((C : (a : ℚ) → MvPolynomial ℕ ℚ) (↑p : ℚ)) i *
            HPow.hPow (α := MvPolynomial ℕ ℚ)
              ((C : (a : ℚ) → MvPolynomial ℕ ℚ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑p : ℚ) _))
              n)))) =
  HPow.hPow (α := MvPolynomial ℕ ℚ) (X i) p ^ (p ^ (n - i) - (j + 1)) *
    (HPow.hPow (α := MvPolynomial ℕ ℚ)
        ((MvPolynomial.map (Int.castRingHom ℚ) : (a : MvPolynomial ℕ ℤ) → MvPolynomial ℕ ℚ) (frobeniusPolyAux p i) :
          MvPolynomial ℕ ℚ)
        (j + 1) *
      HMul.hMul (α := MvPolynomial ℕ ℚ) (β := MvPolynomial ℕ ℚ)
        ((C : (a : ℚ) → MvPolynomial ℕ ℚ)
            ((Int.castRingHom ℚ : (a : ℤ) → ℚ)
              (↑((p ^ (n - i)).choose (j + 1) / p ^ (n - i - v p (j + 1)) * p ^ (j - v p (j + 1))) : ℤ)) :
          MvPolynomial ℕ ℚ)
        ((C : (a : ℚ) → MvPolynomial ℕ ℚ) (↑p : ℚ) : MvPolynomial ℕ ℚ))
Tactic: simp only [mul_assoc]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Frobenius (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
h1 :
  HPow.hPow (α := ℚ) (↑p : ℚ) n *
      HPow.hPow (α := ℚ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑p : ℚ) _) n =
    1
i : ℕ
hi : i < n
j : ℕ
hj : j < p ^ (n - i)
⊢ HPow.hPow (α := MvPolynomial ℕ ℚ) (X i) p ^ (p ^ (n - i) - (j + 1)) *
      (HPow.hPow (α := MvPolynomial ℕ ℚ)
          ((MvPolynomial.map (Int.castRingHom ℚ) : (a : MvPolynomial ℕ ℤ) → MvPolynomial ℕ ℚ) (frobeniusPolyAux p i) :
            MvPolynomial ℕ ℚ)
          (j + 1) *
        (HPow.hPow (α := MvPolynomial ℕ ℚ) ((C : (a : ℚ) → MvPolynomial ℕ ℚ) (↑p : ℚ)) (j + 1) *
          ((↑((p ^ (n - i)).choose (j + 1)) : MvPolynomial ℕ ℚ) *
            (HPow.hPow (α := MvPolynomial ℕ ℚ) ((C : (a : ℚ) → MvPolynomial ℕ ℚ) (↑p : ℚ)) i *
              HPow.hPow (α := MvPolynomial ℕ ℚ)
                ((C : (a : ℚ) → MvPolynomial ℕ ℚ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑p : ℚ) _))
                n)))) =
    HPow.hPow (α := MvPolynomial ℕ ℚ) (X i) p ^ (p ^ (n - i) - (j + 1)) *
      (HPow.hPow (α := MvPolynomial ℕ ℚ)
          ((MvPolynomial.map (Int.castRingHom ℚ) : (a : MvPolynomial ℕ ℤ) → MvPolynomial ℕ ℚ) (frobeniusPolyAux p i) :
            MvPolynomial ℕ ℚ)
          (j + 1) *
        HMul.hMul (α := MvPolynomial ℕ ℚ) (β := MvPolynomial ℕ ℚ)
          ((C : (a : ℚ) → MvPolynomial ℕ ℚ)
              ((Int.castRingHom ℚ : (a : ℤ) → ℚ)
                (↑((p ^ (n - i)).choose (j + 1) / p ^ (n - i - v p (j + 1)) * p ^ (j - v p (j + 1))) : ℤ)) :
            MvPolynomial ℕ ℚ)
          ((C : (a : ℚ) → MvPolynomial ℕ ℚ) (↑p : ℚ) : MvPolynomial ℕ ℚ))
have h : HPow.hPow (α := MvPolynomial ℕ ℚ)
      ((MvPolynomial.map (Int.castRingHom ℚ) : (a : MvPolynomial ℕ ℤ) → MvPolynomial ℕ ℚ) (frobeniusPolyAux p i) :
        MvPolynomial ℕ ℚ)
      (j + 1) *
    (HPow.hPow (α := MvPolynomial ℕ ℚ) ((C : (a : ℚ) → MvPolynomial ℕ ℚ) (↑p : ℚ)) (j + 1) *
      ((↑((p ^ (n - i)).choose (j + 1)) : MvPolynomial ℕ ℚ) *
        (HPow.hPow (α := MvPolynomial ℕ ℚ) ((C : (a : ℚ) → MvPolynomial ℕ ℚ) (↑p : ℚ)) i *
          HPow.hPow (α := MvPolynomial ℕ ℚ)
            ((C : (a : ℚ) → MvPolynomial ℕ ℚ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑p : ℚ) _))
            n))) =
  HPow.hPow (α := MvPolynomial ℕ ℚ)
      ((MvPolynomial.map (Int.castRingHom ℚ) : (a : MvPolynomial ℕ ℤ) → MvPolynomial ℕ ℚ) (frobeniusPolyAux p i) :
        MvPolynomial ℕ ℚ)
      (j + 1) *
    HMul.hMul (α := MvPolynomial ℕ ℚ) (β := MvPolynomial ℕ ℚ)
      ((C : (a : ℚ) → MvPolynomial ℕ ℚ)
          ((Int.castRingHom ℚ : (a : ℤ) → ℚ)
            (↑((p ^ (n - i)).choose (j + 1) / p ^ (n - i - v p (j + 1)) * p ^ (j - v p (j + 1))) : ℤ)) :
        MvPolynomial ℕ ℚ)
      ((C : (a : ℚ) → MvPolynomial ℕ ℚ) (↑p : ℚ) : MvPolynomial ℕ ℚ)
Tactic: apply congr_arg
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Frobenius (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
h1 :
  HPow.hPow (α := ℚ) (↑p : ℚ) n *
      HPow.hPow (α := ℚ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑p : ℚ) _) n =
    1
i : ℕ
hi : i < n
j : ℕ
hj : j < p ^ (n - i)
⊢ HPow.hPow (α := MvPolynomial ℕ ℚ)
        ((MvPolynomial.map (Int.castRingHom ℚ) : (a : MvPolynomial ℕ ℤ) → MvPolynomial ℕ ℚ) (frobeniusPolyAux p i) :
          MvPolynomial ℕ ℚ)
        (j + 1) *
      (HPow.hPow (α := MvPolynomial ℕ ℚ) ((C : (a : ℚ) → MvPolynomial ℕ ℚ) (↑p : ℚ)) (j + 1) *
        ((↑((p ^ (n - i)).choose (j + 1)) : MvPolynomial ℕ ℚ) *
          (HPow.hPow (α := MvPolynomial ℕ ℚ) ((C : (a : ℚ) → MvPolynomial ℕ ℚ) (↑p : ℚ)) i *
            HPow.hPow (α := MvPolynomial ℕ ℚ)
              ((C : (a : ℚ) → MvPolynomial ℕ ℚ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑p : ℚ) _))
              n))) =
    HPow.hPow (α := MvPolynomial ℕ ℚ)
        ((MvPolynomial.map (Int.castRingHom ℚ) : (a : MvPolynomial ℕ ℤ) → MvPolynomial ℕ ℚ) (frobeniusPolyAux p i) :
          MvPolynomial ℕ ℚ)
        (j + 1) *
      HMul.hMul (α := MvPolynomial ℕ ℚ) (β := MvPolynomial ℕ ℚ)
        ((C : (a : ℚ) → MvPolynomial ℕ ℚ)
            ((Int.castRingHom ℚ : (a : ℤ) → ℚ)
              (↑((p ^ (n - i)).choose (j + 1) / p ^ (n - i - v p (j + 1)) * p ^ (j - v p (j + 1))) : ℤ)) :
          MvPolynomial ℕ ℚ)
        ((C : (a : ℚ) → MvPolynomial ℕ ℚ) (↑p : ℚ) : MvPolynomial ℕ ℚ)
have h : HPow.hPow (α := MvPolynomial ℕ ℚ) ((C : (a : ℚ) → MvPolynomial ℕ ℚ) (↑p : ℚ)) (j + 1) *
    ((↑((p ^ (n - i)).choose (j + 1)) : MvPolynomial ℕ ℚ) *
      (HPow.hPow (α := MvPolynomial ℕ ℚ) ((C : (a : ℚ) → MvPolynomial ℕ ℚ) (↑p : ℚ)) i *
        HPow.hPow (α := MvPolynomial ℕ ℚ)
          ((C : (a : ℚ) → MvPolynomial ℕ ℚ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑p : ℚ) _)) n)) =
  HMul.hMul (α := MvPolynomial ℕ ℚ) (β := MvPolynomial ℕ ℚ)
    ((C : (a : ℚ) → MvPolynomial ℕ ℚ)
        ((Int.castRingHom ℚ : (a : ℤ) → ℚ)
          (↑((p ^ (n - i)).choose (j + 1) / p ^ (n - i - v p (j + 1)) * p ^ (j - v p (j + 1))) : ℤ)) :
      MvPolynomial ℕ ℚ)
    ((C : (a : ℚ) → MvPolynomial ℕ ℚ) (↑p : ℚ) : MvPolynomial ℕ ℚ)
Tactic: apply congr_arg
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Frobenius (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
h1 :
  HPow.hPow (α := ℚ) (↑p : ℚ) n *
      HPow.hPow (α := ℚ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑p : ℚ) _) n =
    1
i : ℕ
hi : i < n
j : ℕ
hj : j < p ^ (n - i)
⊢ HPow.hPow (α := MvPolynomial ℕ ℚ) ((C : (a : ℚ) → MvPolynomial ℕ ℚ) (↑p : ℚ)) (j + 1) *
      ((C : (a : ℚ) → MvPolynomial ℕ ℚ) (↑((p ^ (n - i)).choose (j + 1)) : ℚ) *
        (HPow.hPow (α := MvPolynomial ℕ ℚ) ((C : (a : ℚ) → MvPolynomial ℕ ℚ) (↑p : ℚ)) i *
          HPow.hPow (α := MvPolynomial ℕ ℚ)
            ((C : (a : ℚ) → MvPolynomial ℕ ℚ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑p : ℚ) _))
            n)) =
    HMul.hMul (α := MvPolynomial ℕ ℚ) (β := MvPolynomial ℕ ℚ)
      ((C : (a : ℚ) → MvPolynomial ℕ ℚ)
          ((Int.castRingHom ℚ : (a : ℤ) → ℚ)
            (↑((p ^ (n - i)).choose (j + 1) / p ^ (n - i - v p (j + 1)) * p ^ (j - v p (j + 1))) : ℤ)) :
        MvPolynomial ℕ ℚ)
      ((C : (a : ℚ) → MvPolynomial ℕ ℚ) (↑p : ℚ) : MvPolynomial ℕ ℚ)
have h : Eq (α := MvPolynomial ℕ ℚ)
  ((C : (a : ℚ) → MvPolynomial ℕ ℚ)
      (HPow.hPow (α := ℚ) (↑p : ℚ) (j + 1) *
        ((↑((p ^ (n - i)).choose (j + 1)) : ℚ) *
          (HPow.hPow (α := ℚ) (↑p : ℚ) i *
            HPow.hPow (α := ℚ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑p : ℚ) _) n))) :
    MvPolynomial ℕ ℚ)
  ((C : (a : ℚ) → MvPolynomial ℕ ℚ)
      (HMul.hMul (α := ℚ) (β := ℚ)
        ((Int.castRingHom ℚ : (a : ℤ) → ℚ)
            (↑((p ^ (n - i)).choose (j + 1) / p ^ (n - i - v p (j + 1)) * p ^ (j - v p (j + 1))) : ℤ) :
          ℚ)
        ((↑p : ℚ) : ℚ)) :
    MvPolynomial ℕ ℚ)
Tactic: simp only [← map_pow, ← C_mul]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Frobenius (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
h1 :
  HPow.hPow (α := ℚ) (↑p : ℚ) n *
      HPow.hPow (α := ℚ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑p : ℚ) _) n =
    1
i : ℕ
hi : i < n
j : ℕ
hj : j < p ^ (n - i)
⊢ Eq (α := MvPolynomial ℕ ℚ)
    ((C : (a : ℚ) → MvPolynomial ℕ ℚ)
        (HPow.hPow (α := ℚ) (↑p : ℚ) (j + 1) *
          ((↑((p ^ (n - i)).choose (j + 1)) : ℚ) *
            (HPow.hPow (α := ℚ) (↑p : ℚ) i *
              HPow.hPow (α := ℚ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑p : ℚ) _) n))) :
      MvPolynomial ℕ ℚ)
    ((C : (a : ℚ) → MvPolynomial ℕ ℚ)
        (HMul.hMul (α := ℚ) (β := ℚ)
          ((Int.castRingHom ℚ : (a : ℤ) → ℚ)
              (↑((p ^ (n - i)).choose (j + 1) / p ^ (n - i - v p (j + 1)) * p ^ (j - v p (j + 1))) : ℤ) :
            ℚ)
          ((↑p : ℚ) : ℚ)) :
      MvPolynomial ℕ ℚ)
have h : HPow.hPow (α := ℚ) (↑p : ℚ) (j + 1) *
    ((↑((p ^ (n - i)).choose (j + 1)) : ℚ) *
      (HPow.hPow (α := ℚ) (↑p : ℚ) i *
        HPow.hPow (α := ℚ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑p : ℚ) _) n)) =
  HMul.hMul (α := ℚ) (β := ℚ)
    ((Int.castRingHom ℚ : (a : ℤ) → ℚ)
        (↑((p ^ (n - i)).choose (j + 1) / p ^ (n - i - v p (j + 1)) * p ^ (j - v p (j + 1))) : ℤ) :
      ℚ)
    ((↑p : ℚ) : ℚ)
Tactic: rw [C_inj]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Frobenius (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
h1 :
  HPow.hPow (α := ℚ) (↑p : ℚ) n *
      HPow.hPow (α := ℚ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑p : ℚ) _) n =
    1
i : ℕ
hi : i < n
j : ℕ
hj : j < p ^ (n - i)
⊢ HPow.hPow (α := ℚ) (↑p : ℚ) (j + 1) *
      ((↑((p ^ (n - i)).choose (j + 1)) : ℚ) *
        (HPow.hPow (α := ℚ) (↑p : ℚ) i *
          HPow.hPow (α := ℚ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑p : ℚ) _) n)) =
    HMul.hMul (α := ℚ) (β := ℚ)
      ((Int.castRingHom ℚ : (a : ℤ) → ℚ)
          (↑((p ^ (n - i)).choose (j + 1) / p ^ (n - i - v p (j + 1)) * p ^ (j - v p (j + 1))) : ℤ) :
        ℚ)
      ((↑p : ℚ) : ℚ)
have h : HPow.hPow (α := ℚ) (↑p : ℚ) (j + 1) *
    ((↑((p ^ (n - i)).choose (j + 1)) : ℚ) * (HPow.hPow (α := ℚ) (↑p : ℚ) i * (HPow.hPow (α := ℚ) (↑p : ℚ) n)⁻¹)) =
  HMul.hMul (α := ℚ) (↑((p ^ (n - i)).choose (j + 1) / p ^ (n - i - v p (j + 1))) : ℚ) (↑(p ^ (j - v p (j + 1))) : ℚ) *
    (↑p : ℚ)
Tactic: simp only [invOf_eq_inv, eq_intCast, inv_pow, Int.cast_natCast, Nat.cast_mul, Int.cast_mul]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Frobenius (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
h1 :
  HPow.hPow (α := ℚ) (↑p : ℚ) n *
      HPow.hPow (α := ℚ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑p : ℚ) _) n =
    1
i : ℕ
hi : i < n
j : ℕ
hj : j < p ^ (n - i)
⊢ HPow.hPow (α := ℚ) (↑p : ℚ) (j + 1) *
      ((↑((p ^ (n - i)).choose (j + 1)) : ℚ) * (HPow.hPow (α := ℚ) (↑p : ℚ) i * (HPow.hPow (α := ℚ) (↑p : ℚ) n)⁻¹)) =
    HMul.hMul (α := ℚ) (↑((p ^ (n - i)).choose (j + 1) / p ^ (n - i - v p (j + 1))) : ℚ)
        (↑(p ^ (j - v p (j + 1))) : ℚ) *
      (↑p : ℚ)
have h : HPow.hPow (α := ℚ) (↑p : ℚ) (j + 1) *
    ((↑((p ^ (n - i)).choose (j + 1)) : ℚ) * (HPow.hPow (α := ℚ) (↑p : ℚ) i * (HPow.hPow (α := ℚ) (↑p : ℚ) n)⁻¹)) =
  HDiv.hDiv (α := ℚ) (↑((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)]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Frobenius (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
h1 :
  HPow.hPow (α := ℚ) (↑p : ℚ) n *
      HPow.hPow (α := ℚ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑p : ℚ) _) n =
    1
i : ℕ
hi : i < n
j : ℕ
hj : j < p ^ (n - i)
⊢ HPow.hPow (α := ℚ) (↑p : ℚ) (j + 1) *
      ((↑((p ^ (n - i)).choose (j + 1)) : ℚ) * (HPow.hPow (α := ℚ) (↑p : ℚ) i * (HPow.hPow (α := ℚ) (↑p : ℚ) n)⁻¹)) =
    HDiv.hDiv (α := ℚ) (↑((p ^ (n - i)).choose (j + 1)) : ℚ) (↑(p ^ (n - i - v p (j + 1))) : ℚ) *
        (↑(p ^ (j - v p (j + 1))) : ℚ) *
      (↑p : ℚ)
have h : HPow.hPow (α := ℚ) (↑p : ℚ) (j + 1) *
    ((↑((p ^ (n - i)).choose (j + 1)) : ℚ) * (HPow.hPow (α := ℚ) (↑p : ℚ) i * (HPow.hPow (α := ℚ) (↑p : ℚ) n)⁻¹)) =
  (↑((p ^ (n - i)).choose (j + 1)) : ℚ) / HPow.hPow (α := ℚ) (↑p : ℚ) (n - i - v p (j + 1)) *
      HPow.hPow (α := ℚ) (↑p : ℚ) (j - v p (j + 1)) *
    (↑p : ℚ)
Tactic: push_cast
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Frobenius (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
h1 :
  HPow.hPow (α := ℚ) (↑p : ℚ) n *
      HPow.hPow (α := ℚ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑p : ℚ) _) n =
    1
i : ℕ
hi : i < n
j : ℕ
hj : j < p ^ (n - i)
⊢ HPow.hPow (α := ℚ) (↑p : ℚ) (j + 1) *
      ((↑((p ^ (n - i)).choose (j + 1)) : ℚ) * (HPow.hPow (α := ℚ) (↑p : ℚ) i * (HPow.hPow (α := ℚ) (↑p : ℚ) n)⁻¹)) =
    (↑((p ^ (n - i)).choose (j + 1)) : ℚ) / HPow.hPow (α := ℚ) (↑p : ℚ) (n - i - v p (j + 1)) *
        HPow.hPow (α := ℚ) (↑p : ℚ) (j - v p (j + 1)) *
      (↑p : ℚ)
have a : HPow.hPow (α := ℚ) (↑p : ℚ) (j + 1) *
        ((↑((p ^ (n - i)).choose (j + 1)) : ℚ) * (HPow.hPow (α := ℚ) (↑p : ℚ) i * (HPow.hPow (α := ℚ) (↑p : ℚ) n)⁻¹)) +
      -(↑p : ℚ) / HPow.hPow (α := ℚ) (↑p : ℚ) n / HPow.hPow (α := ℚ) (↑p : ℚ) (n - i - v p (j + 1)) *
          (↑((p ^ (n - i)).choose (j + 1)) : ℚ) *
        HPow.hPow (α := ℚ) (↑p : ℚ) (i + j + (n - i - v p (j + 1))) -
    ((↑((p ^ (n - i)).choose (j + 1)) : ℚ) / HPow.hPow (α := ℚ) (↑p : ℚ) (n - i - v p (j + 1)) *
          HPow.hPow (α := ℚ) (↑p : ℚ) (j - v p (j + 1)) *
        (↑p : ℚ) +
      -(↑p : ℚ) / HPow.hPow (α := ℚ) (↑p : ℚ) n / HPow.hPow (α := ℚ) (↑p : ℚ) (n - i - v p (j + 1)) *
          (↑((p ^ (n - i)).choose (j + 1)) : ℚ) *
        HPow.hPow (α := ℚ) (↑p : ℚ) (j - v p (j + 1) + n)) =
  0
Tactic: linear_combination (norm := skip) -p / p ^ n / p ^ (n - i - v p (j + 1))
    * (p ^ (n - i)).choose (j + 1) * congr((p : ℚ) ^ $(map_frobeniusPoly.key₂ p hi.le hj))
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Frobenius (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ (MvPolynomial.map (Int.castRingHom (ZMod p)) : (a : MvPolynomial ℕ ℤ) → MvPolynomial ℕ (ZMod p)) (frobeniusPoly p n) =
    HPow.hPow (α := MvPolynomial ℕ (ZMod p)) (X n) p
have 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
Tactic: rw [frobeniusPoly, map_add, map_pow, map_mul, map_X, map_C]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Frobenius (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ Eq (α := MvPolynomial ℕ ℤ)
    ((bind₁ (frobeniusPoly p) : (a : MvPolynomial ℕ ℤ) → MvPolynomial ℕ ℤ) (wittPolynomial p ℤ n) : MvPolynomial ℕ ℤ)
    (wittPolynomial p ℤ (n + 1) : MvPolynomial ℕ ℤ)
have 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 ℕ ℚ)
Tactic: apply MvPolynomial.map_injective (Int.castRingHom ℚ) Int.cast_injective
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Frobenius (goal)
Goal:
p : ℕ
R : Type u_1
inst : CommRing R
x : 𝕎 R
n : ℕ
⊢ x.frobeniusFun.coeff n =
    ((aeval (R := ℤ) x.coeff : MvPolynomial ℕ ℤ →ₐ[ℤ] R) : (a : MvPolynomial ℕ ℤ) → R) (frobeniusPoly p n)
have 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)
Tactic: rw [frobeniusFun, coeff_mk]