awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.WittVector.Frobenius
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
IH :
  ∀ m < n,
    HPow.hPow (α := MvPolynomial ℕ ℚ) (X m) p +
        HMul.hMul (α := MvPolynomial ℕ ℚ) (β := MvPolynomial ℕ ℚ)
          ((C : (a : ℚ) → MvPolynomial ℕ ℚ) (↑p : ℚ) : MvPolynomial ℕ ℚ)
          ((MvPolynomial.map (Int.castRingHom ℚ) : (a : MvPolynomial ℕ ℤ) → MvPolynomial ℕ ℚ) (frobeniusPolyAux p m) :
            MvPolynomial ℕ ℚ) =
      (bind₁ (wittPolynomial p ℚ ∘ fun (n : ℕ) ↦ n + 1) : (a : MvPolynomial ℕ ℚ) → MvPolynomial ℕ ℚ) (xInTermsOfW p ℚ m)
rw : HMul.hMul (α := ℚ) (↑p : ℚ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑p : ℚ) _) ^ n = 1
rw₁ : HPow.hPow (α := ℚ) 1 n = 1
rw₂ rw₃ : Eq (α := ℚ) 1 1
⊢ HPow.hPow (α := ℚ) (↑p : ℚ) n *
      HPow.hPow (α := ℚ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑p : ℚ) _) n =
    1

Tactic:
rw [← mul_pow, mul_invOf_self, one_pow]

Premises used: one_pow, mul_invOf_self, mul_pow
-- Module: Mathlib.RingTheory.WittVector.Frobenius
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
IH :
  ∀ m < n,
    HPow.hPow (α := MvPolynomial ℕ ℚ) (X m) p +
        HMul.hMul (α := MvPolynomial ℕ ℚ) (β := MvPolynomial ℕ ℚ)
          ((C : (a : ℚ) → MvPolynomial ℕ ℚ) (↑p : ℚ) : MvPolynomial ℕ ℚ)
          ((MvPolynomial.map (Int.castRingHom ℚ) : (a : MvPolynomial ℕ ℤ) → MvPolynomial ℕ ℚ) (frobeniusPolyAux p m) :
            MvPolynomial ℕ ℚ) =
      (bind₁ (wittPolynomial p ℚ ∘ fun (n : ℕ) ↦ n + 1) : (a : MvPolynomial ℕ ℚ) → MvPolynomial ℕ ℚ) (xInTermsOfW p ℚ m)
⊢ HPow.hPow (α := ℚ) (↑p : ℚ) n *
      HPow.hPow (α := ℚ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑p : ℚ) _) n =
    1

Tactic:
have h1 : (p : ℚ) ^ n * ⅟(p : ℚ) ^ n = 1 := by rw [← mul_pow, mul_invOf_self, one_pow]
-- Module: Mathlib.RingTheory.WittVector.Frobenius
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
IH :
  ∀ m < n,
    HPow.hPow (α := MvPolynomial ℕ ℚ) (X m) p +
        HMul.hMul (α := MvPolynomial ℕ ℚ) (β := MvPolynomial ℕ ℚ)
          ((C : (a : ℚ) → MvPolynomial ℕ ℚ) (↑p : ℚ) : MvPolynomial ℕ ℚ)
          ((MvPolynomial.map (Int.castRingHom ℚ) : (a : MvPolynomial ℕ ℤ) → MvPolynomial ℕ ℚ) (frobeniusPolyAux p m) :
            MvPolynomial ℕ ℚ) =
      (bind₁ (wittPolynomial p ℚ ∘ fun (n : ℕ) ↦ n + 1) : (a : MvPolynomial ℕ ℚ) → MvPolynomial ℕ ℚ) (xInTermsOfW p ℚ m)
h1 :
  HPow.hPow (α := ℚ) (↑p : ℚ) n *
      HPow.hPow (α := ℚ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑p : ℚ) _) n =
    1
i : ℕ
hi : i ∈ range n
⊢ i < n

Tactic:
rw [mem_range] at hi

Premises used: Finset.mem_range
-- Module: Mathlib.RingTheory.WittVector.Frobenius
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 ∈ range (p ^ (n - i))
⊢ j < p ^ (n - i)

Tactic:
rw [mem_range] at hj

Premises used: Finset.mem_range
-- Module: Mathlib.RingTheory.WittVector.Frobenius
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)
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 ℕ ℚ)
⊢ 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 ℕ ℚ)

Tactic:
rw [map_mul, map_mul, map_pow, map_pow, map_pow, map_pow, map_pow, map_C, map_X, mul_pow]

Premises used: map_pow, map_mul, MvPolynomial.map_C, mul_pow, MvPolynomial.map_X
-- Module: Mathlib.RingTheory.WittVector.Frobenius
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)
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 ℕ ℚ))
⊢ 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:
simp only [mul_assoc]

Premises used: mul_assoc
-- Module: Mathlib.RingTheory.WittVector.Frobenius
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)
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 ℕ ℚ)
⊢ 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:
apply congr_arg

Premises used: congr_arg
-- Module: Mathlib.RingTheory.WittVector.Frobenius
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)
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 ℕ ℚ)
⊢ 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

Premises used: congr_arg
-- Module: Mathlib.RingTheory.WittVector.Frobenius
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)
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 ℕ ℚ)
⊢ 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 ℕ ℚ)

Tactic:
simp only [← map_pow, ← C_mul]

Premises used: map_pow, MvPolynomial.C_mul
-- Module: Mathlib.RingTheory.WittVector.Frobenius
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)
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 : ℚ) : ℚ)
⊢ 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:
rw [C_inj]

Premises used: MvPolynomial.C_inj
-- Module: Mathlib.RingTheory.WittVector.Frobenius
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)
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 : ℚ)
⊢ 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:
simp only [invOf_eq_inv, eq_intCast, inv_pow, Int.cast_natCast, Nat.cast_mul, Int.cast_mul]

Premises used: Int.cast_natCast, eq_intCast, inv_pow, Int.cast_mul, Nat.cast_mul, invOf_eq_inv
-- Module: Mathlib.RingTheory.WittVector.Frobenius
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)
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 : ℚ)
⊢ 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:
rw [Rat.natCast_div _ _ (map_frobeniusPoly.key₁ p (n - i) j hj)]

Premises used: Rat.natCast_div, HSub.hSub, WittVector.map_frobeniusPoly.key₁
-- Module: Mathlib.RingTheory.WittVector.Frobenius
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)
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 : ℚ)
⊢ 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:
push_cast
-- Module: Mathlib.RingTheory.WittVector.Frobenius
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)
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
⊢ 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:
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))

Premises used: WittVector.map_frobeniusPoly.key₂, Nat.choose, HSub.hSub, LT.lt.le, Nat.cast, multiplicity, HPow.hPow, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.RingTheory.WittVector.Frobenius
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 : ℚ) / 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:
field [hp.1.ne_zero]

Premises used: Nat.Prime.ne_zero, Fact.out