awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.WittVector.StructurePolynomial
Goal:
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℚ
n : ℕ
this :
  Eq.{u_2 + 1} (α := MvPolynomial (idx × ℕ) ℚ)
    ((bind₁ fun (k : ℕ) ↦
            (bind₁ fun (i : idx) ↦ (rename (Prod.mk i) : (a : MvPolynomial ℕ ℚ) → MvPolynomial (idx × ℕ) ℚ) (W_ ℚ k) :
                (a : MvPolynomial idx ℚ) → MvPolynomial (idx × ℕ) ℚ)
              Φ :
          (a : MvPolynomial ℕ ℚ) → MvPolynomial (idx × ℕ) ℚ)
        (HMul.hMul (α := MvPolynomial ℕ ℚ) (β := MvPolynomial ℕ ℚ) (xInTermsOfW p ℚ n)
          ((C : (a : ℚ) → MvPolynomial ℕ ℚ) (HPow.hPow (α := ℚ) (↑p : ℚ) n) : MvPolynomial ℕ ℚ)) :
      MvPolynomial (idx × ℕ) ℚ)
    ((bind₁ fun (k : ℕ) ↦
            (bind₁ fun (i : idx) ↦ (rename (Prod.mk i) : (a : MvPolynomial ℕ ℚ) → MvPolynomial (idx × ℕ) ℚ) (W_ ℚ k) :
                (a : MvPolynomial idx ℚ) → MvPolynomial (idx × ℕ) ℚ)
              Φ :
          (a : MvPolynomial ℕ ℚ) → MvPolynomial (idx × ℕ) ℚ)
        (HSub.hSub (α := MvPolynomial ℕ ℚ) (X n)
          (∑ i ∈ Finset.range n,
            HMul.hMul (α := MvPolynomial ℕ ℚ)
              ((C : (a : ℚ) → MvPolynomial ℕ ℚ) (HPow.hPow (α := ℚ) (↑p : ℚ) i) : MvPolynomial ℕ ℚ)
              (HPow.hPow (α := MvPolynomial ℕ ℚ) (xInTermsOfW p ℚ i) (p ^ (n - i))))) :
      MvPolynomial (idx × ℕ) ℚ)
⊢ HMul.hMul (α := MvPolynomial (idx × ℕ) ℚ) (β := MvPolynomial (idx × ℕ) ℚ)
      ((bind₁ fun (k : ℕ) ↦
              (bind₁ fun (i : idx) ↦ (rename (Prod.mk i) : (a : MvPolynomial ℕ ℚ) → MvPolynomial (idx × ℕ) ℚ) (W_ ℚ k) :
                  (a : MvPolynomial idx ℚ) → MvPolynomial (idx × ℕ) ℚ)
                Φ :
            (a : MvPolynomial ℕ ℚ) → MvPolynomial (idx × ℕ) ℚ)
          (xInTermsOfW p ℚ n) :
        MvPolynomial (idx × ℕ) ℚ)
      ((C : (a : ℚ) → MvPolynomial (idx × ℕ) ℚ) (HPow.hPow (α := ℚ) (↑p : ℚ) n) : MvPolynomial (idx × ℕ) ℚ) =
    (bind₁ fun (k : ℕ) ↦
          (bind₁ fun (i : idx) ↦ (rename (Prod.mk i) : (a : MvPolynomial ℕ ℚ) → MvPolynomial (idx × ℕ) ℚ) (W_ ℚ k) :
              (a : MvPolynomial idx ℚ) → MvPolynomial (idx × ℕ) ℚ)
            Φ :
        (a : MvPolynomial ℕ ℚ) → MvPolynomial (idx × ℕ) ℚ)
      (HSub.hSub (α := MvPolynomial ℕ ℚ) (X n)
        (∑ i ∈ Finset.range n,
          HMul.hMul (α := MvPolynomial ℕ ℚ)
            ((C : (a : ℚ) → MvPolynomial ℕ ℚ) (HPow.hPow (α := ℚ) (↑p : ℚ) i) : MvPolynomial ℕ ℚ)
            (HPow.hPow (α := MvPolynomial ℕ ℚ) (xInTermsOfW p ℚ i) (p ^ (n - i)))))

Tactic:
rw [map_mul, bind₁_C_right] at this

Premises used: MvPolynomial.bind₁_C_right, map_mul
-- Module: Mathlib.RingTheory.WittVector.StructurePolynomial
Goal:
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℚ
n : ℕ
simp :
  HSub.hSub (α := MvPolynomial (idx × ℕ) ℚ) (β := MvPolynomial (idx × ℕ) ℚ)
    ((bind₁ fun (i : idx) ↦ (rename (Prod.mk i) : (a : MvPolynomial ℕ ℚ) → MvPolynomial (idx × ℕ) ℚ) (W_ ℚ n) :
          (a : MvPolynomial idx ℚ) → MvPolynomial (idx × ℕ) ℚ)
        Φ :
      MvPolynomial (idx × ℕ) ℚ)
    ((bind₁ fun (k : ℕ) ↦
          (bind₁ fun (i : idx) ↦ (rename (Prod.mk i) : (a : MvPolynomial ℕ ℚ) → MvPolynomial (idx × ℕ) ℚ) (W_ ℚ k) :
              (a : MvPolynomial idx ℚ) → MvPolynomial (idx × ℕ) ℚ)
            Φ :
        (a : MvPolynomial ℕ ℚ) → MvPolynomial (idx × ℕ) ℚ)
      (∑ i ∈ Finset.range n,
        HMul.hMul (α := MvPolynomial ℕ ℚ)
          ((C : (a : ℚ) → MvPolynomial ℕ ℚ) (HPow.hPow (α := ℚ) (↑p : ℚ) i) : MvPolynomial ℕ ℚ)
          (HPow.hPow (α := MvPolynomial ℕ ℚ) (xInTermsOfW p ℚ i) (p ^ (n - i)))))
| (bind₁ fun (k : ℕ) ↦
        (bind₁ fun (i : idx) ↦ (rename (Prod.mk i) : (a : MvPolynomial ℕ ℚ) → MvPolynomial (idx × ℕ) ℚ) (W_ ℚ k) :
            (a : MvPolynomial idx ℚ) → MvPolynomial (idx × ℕ) ℚ)
          Φ :
      (a : MvPolynomial ℕ ℚ) → MvPolynomial (idx × ℕ) ℚ)
    (HSub.hSub (α := MvPolynomial ℕ ℚ) (X n)
      (∑ i ∈ Finset.range n,
        HMul.hMul (α := MvPolynomial ℕ ℚ)
          ((C : (a : ℚ) → MvPolynomial ℕ ℚ) (HPow.hPow (α := ℚ) (↑p : ℚ) i) : MvPolynomial ℕ ℚ)
          (HPow.hPow (α := MvPolynomial ℕ ℚ) (xInTermsOfW p ℚ i) (p ^ (n - i)))))

Tactic:
simp only [map_sub, bind₁_X_right]

Premises used: map_sub, MvPolynomial.bind₁_X_right
-- Module: Mathlib.RingTheory.WittVector.StructurePolynomial
Goal:
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℚ
n : ℕ
conv_lhs :
  HSub.hSub (α := MvPolynomial (idx × ℕ) ℚ) (β := MvPolynomial (idx × ℕ) ℚ)
      ((bind₁ fun (i : idx) ↦ (rename (Prod.mk i) : (a : MvPolynomial ℕ ℚ) → MvPolynomial (idx × ℕ) ℚ) (W_ ℚ n) :
            (a : MvPolynomial idx ℚ) → MvPolynomial (idx × ℕ) ℚ)
          Φ :
        MvPolynomial (idx × ℕ) ℚ)
      ((bind₁ fun (k : ℕ) ↦
            (bind₁ fun (i : idx) ↦ (rename (Prod.mk i) : (a : MvPolynomial ℕ ℚ) → MvPolynomial (idx × ℕ) ℚ) (W_ ℚ k) :
                (a : MvPolynomial idx ℚ) → MvPolynomial (idx × ℕ) ℚ)
              Φ :
          (a : MvPolynomial ℕ ℚ) → MvPolynomial (idx × ℕ) ℚ)
        (∑ i ∈ Finset.range n,
          HMul.hMul (α := MvPolynomial ℕ ℚ)
            ((C : (a : ℚ) → MvPolynomial ℕ ℚ) (HPow.hPow (α := ℚ) (↑p : ℚ) i) : MvPolynomial ℕ ℚ)
            (HPow.hPow (α := MvPolynomial ℕ ℚ) (xInTermsOfW p ℚ i) (p ^ (n - i))))) =
    HSub.hSub (α := MvPolynomial (idx × ℕ) ℚ) (β := MvPolynomial (idx × ℕ) ℚ)
      ((bind₁ fun (b : idx) ↦
              (rename fun (i : ℕ) ↦ (b, i) : (a : MvPolynomial ℕ ℚ) → MvPolynomial (idx × ℕ) ℚ) (W_ ℚ n) :
            (a : MvPolynomial idx ℚ) → MvPolynomial (idx × ℕ) ℚ)
          Φ :
        MvPolynomial (idx × ℕ) ℚ)
      (∑ i ∈ Finset.range n,
          HMul.hMul (α := MvPolynomial (idx × ℕ) ℚ)
            ((C : (a : ℚ) → MvPolynomial (idx × ℕ) ℚ) (HPow.hPow (α := ℚ) (↑p : ℚ) i) : MvPolynomial (idx × ℕ) ℚ)
            (wittStructureRat p Φ i ^ p ^ (n - i)) :
        MvPolynomial (idx × ℕ) ℚ)
⊢ (bind₁ fun (k : ℕ) ↦
          (bind₁ fun (i : idx) ↦ (rename (Prod.mk i) : (a : MvPolynomial ℕ ℚ) → MvPolynomial (idx × ℕ) ℚ) (W_ ℚ k) :
              (a : MvPolynomial idx ℚ) → MvPolynomial (idx × ℕ) ℚ)
            Φ :
        (a : MvPolynomial ℕ ℚ) → MvPolynomial (idx × ℕ) ℚ)
      (HSub.hSub (α := MvPolynomial ℕ ℚ) (X n)
        (∑ i ∈ Finset.range n,
          HMul.hMul (α := MvPolynomial ℕ ℚ)
            ((C : (a : ℚ) → MvPolynomial ℕ ℚ) (HPow.hPow (α := ℚ) (↑p : ℚ) i) : MvPolynomial ℕ ℚ)
            (HPow.hPow (α := MvPolynomial ℕ ℚ) (xInTermsOfW p ℚ i) (p ^ (n - i))))) =
    HSub.hSub (α := MvPolynomial (idx × ℕ) ℚ) (β := MvPolynomial (idx × ℕ) ℚ)
      ((bind₁ fun (b : idx) ↦
              (rename fun (i : ℕ) ↦ (b, i) : (a : MvPolynomial ℕ ℚ) → MvPolynomial (idx × ℕ) ℚ) (W_ ℚ n) :
            (a : MvPolynomial idx ℚ) → MvPolynomial (idx × ℕ) ℚ)
          Φ :
        MvPolynomial (idx × ℕ) ℚ)
      (∑ i ∈ Finset.range n,
          HMul.hMul (α := MvPolynomial (idx × ℕ) ℚ)
            ((C : (a : ℚ) → MvPolynomial (idx × ℕ) ℚ) (HPow.hPow (α := ℚ) (↑p : ℚ) i) : MvPolynomial (idx × ℕ) ℚ)
            (wittStructureRat p Φ i ^ p ^ (n - i)) :
        MvPolynomial (idx × ℕ) ℚ)

Tactic:
conv_lhs => simp only [map_sub, bind₁_X_right]

Premises used: map_sub, MvPolynomial.bind₁_X_right
-- Module: Mathlib.RingTheory.WittVector.StructurePolynomial
Goal:
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℚ
n : ℕ
rw :
  Eq.{u_2 + 1} (α := MvPolynomial (idx × ℕ) ℚ)
    ((bind₁ fun (k : ℕ) ↦
          (bind₁ fun (i : idx) ↦ (rename (Prod.mk i) : (a : MvPolynomial ℕ ℚ) → MvPolynomial (idx × ℕ) ℚ) (W_ ℚ k) :
              (a : MvPolynomial idx ℚ) → MvPolynomial (idx × ℕ) ℚ)
            Φ :
        (a : MvPolynomial ℕ ℚ) → MvPolynomial (idx × ℕ) ℚ)
      (∑ i ∈ Finset.range n,
        HMul.hMul (α := MvPolynomial ℕ ℚ)
          ((C : (a : ℚ) → MvPolynomial ℕ ℚ) (HPow.hPow (α := ℚ) (↑p : ℚ) i) : MvPolynomial ℕ ℚ)
          (HPow.hPow (α := MvPolynomial ℕ ℚ) (xInTermsOfW p ℚ i) (p ^ (n - i)))))
    (∑ i ∈ Finset.range n,
      HMul.hMul (α := MvPolynomial (idx × ℕ) ℚ)
        ((C : (a : ℚ) → MvPolynomial (idx × ℕ) ℚ) (HPow.hPow (α := ℚ) (↑p : ℚ) i) : MvPolynomial (idx × ℕ) ℚ)
        (wittStructureRat p Φ i ^ p ^ (n - i)))
⊢ HSub.hSub (α := MvPolynomial (idx × ℕ) ℚ) (β := MvPolynomial (idx × ℕ) ℚ)
      ((bind₁ fun (i : idx) ↦ (rename (Prod.mk i) : (a : MvPolynomial ℕ ℚ) → MvPolynomial (idx × ℕ) ℚ) (W_ ℚ n) :
            (a : MvPolynomial idx ℚ) → MvPolynomial (idx × ℕ) ℚ)
          Φ :
        MvPolynomial (idx × ℕ) ℚ)
      ((bind₁ fun (k : ℕ) ↦
            (bind₁ fun (i : idx) ↦ (rename (Prod.mk i) : (a : MvPolynomial ℕ ℚ) → MvPolynomial (idx × ℕ) ℚ) (W_ ℚ k) :
                (a : MvPolynomial idx ℚ) → MvPolynomial (idx × ℕ) ℚ)
              Φ :
          (a : MvPolynomial ℕ ℚ) → MvPolynomial (idx × ℕ) ℚ)
        (∑ i ∈ Finset.range n,
          HMul.hMul (α := MvPolynomial ℕ ℚ)
            ((C : (a : ℚ) → MvPolynomial ℕ ℚ) (HPow.hPow (α := ℚ) (↑p : ℚ) i) : MvPolynomial ℕ ℚ)
            (HPow.hPow (α := MvPolynomial ℕ ℚ) (xInTermsOfW p ℚ i) (p ^ (n - i))))) =
    HSub.hSub (α := MvPolynomial (idx × ℕ) ℚ) (β := MvPolynomial (idx × ℕ) ℚ)
      ((bind₁ fun (b : idx) ↦
              (rename fun (i : ℕ) ↦ (b, i) : (a : MvPolynomial ℕ ℚ) → MvPolynomial (idx × ℕ) ℚ) (W_ ℚ n) :
            (a : MvPolynomial idx ℚ) → MvPolynomial (idx × ℕ) ℚ)
          Φ :
        MvPolynomial (idx × ℕ) ℚ)
      (∑ i ∈ Finset.range n,
          HMul.hMul (α := MvPolynomial (idx × ℕ) ℚ)
            ((C : (a : ℚ) → MvPolynomial (idx × ℕ) ℚ) (HPow.hPow (α := ℚ) (↑p : ℚ) i) : MvPolynomial (idx × ℕ) ℚ)
            (wittStructureRat p Φ i ^ p ^ (n - i)) :
        MvPolynomial (idx × ℕ) ℚ)

Tactic:
rw [sub_right_inj]

Premises used: sub_right_inj
-- Module: Mathlib.RingTheory.WittVector.StructurePolynomial
Goal:
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℚ
n : ℕ
simp :
  Eq.{u_2 + 1} (α := MvPolynomial (idx × ℕ) ℚ)
    (∑ x ∈ Finset.range n,
      HPow.hPow (α := MvPolynomial (idx × ℕ) ℚ) ((C : (a : ℚ) → MvPolynomial (idx × ℕ) ℚ) (↑p : ℚ)) x *
        HPow.hPow (α := MvPolynomial (idx × ℕ) ℚ)
          ((bind₁ fun (k : ℕ) ↦
                  (bind₁ fun (i : idx) ↦
                        (rename (Prod.mk i) : (a : MvPolynomial ℕ ℚ) → MvPolynomial (idx × ℕ) ℚ) (W_ ℚ k) :
                      (a : MvPolynomial idx ℚ) → MvPolynomial (idx × ℕ) ℚ)
                    Φ :
                (a : MvPolynomial ℕ ℚ) → MvPolynomial (idx × ℕ) ℚ)
              (xInTermsOfW p ℚ x) :
            MvPolynomial (idx × ℕ) ℚ)
          (p ^ (n - x)))
    (∑ x ∈ Finset.range n,
      HPow.hPow (α := MvPolynomial (idx × ℕ) ℚ) ((C : (a : ℚ) → MvPolynomial (idx × ℕ) ℚ) (↑p : ℚ)) x *
        wittStructureRat p Φ x ^ p ^ (n - x))
⊢ Eq.{u_2 + 1} (α := MvPolynomial (idx × ℕ) ℚ)
    ((bind₁ fun (k : ℕ) ↦
          (bind₁ fun (i : idx) ↦ (rename (Prod.mk i) : (a : MvPolynomial ℕ ℚ) → MvPolynomial (idx × ℕ) ℚ) (W_ ℚ k) :
              (a : MvPolynomial idx ℚ) → MvPolynomial (idx × ℕ) ℚ)
            Φ :
        (a : MvPolynomial ℕ ℚ) → MvPolynomial (idx × ℕ) ℚ)
      (∑ i ∈ Finset.range n,
        HMul.hMul (α := MvPolynomial ℕ ℚ)
          ((C : (a : ℚ) → MvPolynomial ℕ ℚ) (HPow.hPow (α := ℚ) (↑p : ℚ) i) : MvPolynomial ℕ ℚ)
          (HPow.hPow (α := MvPolynomial ℕ ℚ) (xInTermsOfW p ℚ i) (p ^ (n - i)))))
    (∑ i ∈ Finset.range n,
      HMul.hMul (α := MvPolynomial (idx × ℕ) ℚ)
        ((C : (a : ℚ) → MvPolynomial (idx × ℕ) ℚ) (HPow.hPow (α := ℚ) (↑p : ℚ) i) : MvPolynomial (idx × ℕ) ℚ)
        (wittStructureRat p Φ i ^ p ^ (n - i)))

Tactic:
simp only [map_sum, map_mul, bind₁_C_right, map_pow]

Premises used: MvPolynomial.bind₁_C_right, map_pow, map_sum, map_mul
-- Module: Mathlib.RingTheory.WittVector.StructurePolynomial
Goal:
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℚ
n : ℕ
⊢ Eq.{u_2 + 1} (α := MvPolynomial (idx × ℕ) ℚ)
    (∑ x ∈ Finset.range n,
      HPow.hPow (α := MvPolynomial (idx × ℕ) ℚ) ((C : (a : ℚ) → MvPolynomial (idx × ℕ) ℚ) (↑p : ℚ)) x *
        HPow.hPow (α := MvPolynomial (idx × ℕ) ℚ)
          ((bind₁ fun (k : ℕ) ↦
                  (bind₁ fun (i : idx) ↦
                        (rename (Prod.mk i) : (a : MvPolynomial ℕ ℚ) → MvPolynomial (idx × ℕ) ℚ) (W_ ℚ k) :
                      (a : MvPolynomial idx ℚ) → MvPolynomial (idx × ℕ) ℚ)
                    Φ :
                (a : MvPolynomial ℕ ℚ) → MvPolynomial (idx × ℕ) ℚ)
              (xInTermsOfW p ℚ x) :
            MvPolynomial (idx × ℕ) ℚ)
          (p ^ (n - x)))
    (∑ x ∈ Finset.range n,
      HPow.hPow (α := MvPolynomial (idx × ℕ) ℚ) ((C : (a : ℚ) → MvPolynomial (idx × ℕ) ℚ) (↑p : ℚ)) x *
        wittStructureRat p Φ x ^ p ^ (n - x))

Tactic:
rfl
-- Module: Mathlib.RingTheory.WittVector.StructurePolynomial
Goal:
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℚ
n : ℕ
⊢ wittStructureRat p Φ n =
    HMul.hMul (α := MvPolynomial (idx × ℕ) ℚ)
      ((C : (a : ℚ) → MvPolynomial (idx × ℕ) ℚ) (1 / HPow.hPow (α := ℚ) (↑p : ℚ) n) : MvPolynomial (idx × ℕ) ℚ)
      (HMul.hMul (β := MvPolynomial (idx × ℕ) ℚ) (wittStructureRat p Φ n)
        ((C : (a : ℚ) → MvPolynomial (idx × ℕ) ℚ) (HPow.hPow (α := ℚ) (↑p : ℚ) n) : MvPolynomial (idx × ℕ) ℚ))

Tactic:
?_
-- Module: Mathlib.RingTheory.WittVector.StructurePolynomial
Goal:
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℚ
n : ℕ
rw rw₁ :
  HMul.hMul (α := MvPolynomial (idx × ℕ) ℚ)
      ((C : (a : ℚ) → MvPolynomial (idx × ℕ) ℚ) (1 / HPow.hPow (α := ℚ) (↑p : ℚ) n) : MvPolynomial (idx × ℕ) ℚ)
      (HSub.hSub (α := MvPolynomial (idx × ℕ) ℚ) (β := MvPolynomial (idx × ℕ) ℚ)
        ((bind₁ fun (b : idx) ↦
                (rename fun (i : ℕ) ↦ (b, i) : (a : MvPolynomial ℕ ℚ) → MvPolynomial (idx × ℕ) ℚ) (W_ ℚ n) :
              (a : MvPolynomial idx ℚ) → MvPolynomial (idx × ℕ) ℚ)
            Φ :
          MvPolynomial (idx × ℕ) ℚ)
        (∑ i ∈ Finset.range n,
            HMul.hMul (α := MvPolynomial (idx × ℕ) ℚ)
              ((C : (a : ℚ) → MvPolynomial (idx × ℕ) ℚ) (HPow.hPow (α := ℚ) (↑p : ℚ) i) : MvPolynomial (idx × ℕ) ℚ)
              (wittStructureRat p Φ i ^ p ^ (n - i)) :
          MvPolynomial (idx × ℕ) ℚ)) =
    HMul.hMul (α := MvPolynomial (idx × ℕ) ℚ)
      ((C : (a : ℚ) → MvPolynomial (idx × ℕ) ℚ) (1 / HPow.hPow (α := ℚ) (↑p : ℚ) n) : MvPolynomial (idx × ℕ) ℚ)
      (HSub.hSub (α := MvPolynomial (idx × ℕ) ℚ) (β := MvPolynomial (idx × ℕ) ℚ)
        ((bind₁ fun (b : idx) ↦
                (rename fun (i : ℕ) ↦ (b, i) : (a : MvPolynomial ℕ ℚ) → MvPolynomial (idx × ℕ) ℚ) (W_ ℚ n) :
              (a : MvPolynomial idx ℚ) → MvPolynomial (idx × ℕ) ℚ)
            Φ :
          MvPolynomial (idx × ℕ) ℚ)
        (∑ i ∈ Finset.range n,
            HMul.hMul (α := MvPolynomial (idx × ℕ) ℚ)
              ((C : (a : ℚ) → MvPolynomial (idx × ℕ) ℚ) (HPow.hPow (α := ℚ) (↑p : ℚ) i) : MvPolynomial (idx × ℕ) ℚ)
              (wittStructureRat p Φ i ^ p ^ (n - i)) :
          MvPolynomial (idx × ℕ) ℚ))
⊢ HMul.hMul (α := MvPolynomial (idx × ℕ) ℚ)
      ((C : (a : ℚ) → MvPolynomial (idx × ℕ) ℚ) (1 / HPow.hPow (α := ℚ) (↑p : ℚ) n) : MvPolynomial (idx × ℕ) ℚ)
      (HMul.hMul (β := MvPolynomial (idx × ℕ) ℚ) (wittStructureRat p Φ n)
        ((C : (a : ℚ) → MvPolynomial (idx × ℕ) ℚ) (HPow.hPow (α := ℚ) (↑p : ℚ) n) : MvPolynomial (idx × ℕ) ℚ)) =
    HMul.hMul (α := MvPolynomial (idx × ℕ) ℚ)
      ((C : (a : ℚ) → MvPolynomial (idx × ℕ) ℚ) (1 / HPow.hPow (α := ℚ) (↑p : ℚ) n) : MvPolynomial (idx × ℕ) ℚ)
      (HSub.hSub (α := MvPolynomial (idx × ℕ) ℚ) (β := MvPolynomial (idx × ℕ) ℚ)
        ((bind₁ fun (b : idx) ↦
                (rename fun (i : ℕ) ↦ (b, i) : (a : MvPolynomial ℕ ℚ) → MvPolynomial (idx × ℕ) ℚ) (W_ ℚ n) :
              (a : MvPolynomial idx ℚ) → MvPolynomial (idx × ℕ) ℚ)
            Φ :
          MvPolynomial (idx × ℕ) ℚ)
        (∑ i ∈ Finset.range n,
            HMul.hMul (α := MvPolynomial (idx × ℕ) ℚ)
              ((C : (a : ℚ) → MvPolynomial (idx × ℕ) ℚ) (HPow.hPow (α := ℚ) (↑p : ℚ) i) : MvPolynomial (idx × ℕ) ℚ)
              (wittStructureRat p Φ i ^ p ^ (n - i)) :
          MvPolynomial (idx × ℕ) ℚ))

Tactic:
rw [wittStructureRat_rec_aux]

Premises used: wittStructureRat_rec_aux
-- Module: Mathlib.RingTheory.WittVector.StructurePolynomial
Goal:
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℚ
n : ℕ
wittStructureRat :
  _root_.wittStructureRat p Φ n =
    HMul.hMul (α := MvPolynomial (idx × ℕ) ℚ)
      ((C : (a : ℚ) → MvPolynomial (idx × ℕ) ℚ) (1 / HPow.hPow (α := ℚ) (↑p : ℚ) n) : MvPolynomial (idx × ℕ) ℚ)
      (HMul.hMul (β := MvPolynomial (idx × ℕ) ℚ) (_root_.wittStructureRat p Φ n)
        ((C : (a : ℚ) → MvPolynomial (idx × ℕ) ℚ) (HPow.hPow (α := ℚ) (↑p : ℚ) n) : MvPolynomial (idx × ℕ) ℚ))
⊢ _root_.wittStructureRat p Φ n =
    HMul.hMul (α := MvPolynomial (idx × ℕ) ℚ)
      ((C : (a : ℚ) → MvPolynomial (idx × ℕ) ℚ) (1 / HPow.hPow (α := ℚ) (↑p : ℚ) n) : MvPolynomial (idx × ℕ) ℚ)
      (HSub.hSub (α := MvPolynomial (idx × ℕ) ℚ) (β := MvPolynomial (idx × ℕ) ℚ)
        ((bind₁ fun (b : idx) ↦
                (rename fun (i : ℕ) ↦ (b, i) : (a : MvPolynomial ℕ ℚ) → MvPolynomial (idx × ℕ) ℚ) (W_ ℚ n) :
              (a : MvPolynomial idx ℚ) → MvPolynomial (idx × ℕ) ℚ)
            Φ :
          MvPolynomial (idx × ℕ) ℚ)
        (∑ i ∈ Finset.range n,
            HMul.hMul (α := MvPolynomial (idx × ℕ) ℚ)
              ((C : (a : ℚ) → MvPolynomial (idx × ℕ) ℚ) (HPow.hPow (α := ℚ) (↑p : ℚ) i) : MvPolynomial (idx × ℕ) ℚ)
              (_root_.wittStructureRat p Φ i ^ p ^ (n - i)) :
          MvPolynomial (idx × ℕ) ℚ))

Tactic:
calc
    wittStructureRat p Φ n = C (1 / (p : ℚ) ^ n) * (wittStructureRat p Φ n * C ((p : ℚ) ^ n)) := ?_
    _ = _ := by rw [wittStructureRat_rec_aux]

Premises used: HMul.hMul, HDiv.hDiv, wittStructureRat, Nat.cast, HPow.hPow, OfNat.ofNat, MvPolynomial.C, DFunLike.coe
-- Module: Mathlib.RingTheory.WittVector.StructurePolynomial
Goal:
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℚ
n : ℕ
h : HPow.hPow (α := ℚ) (↑p : ℚ) n ≠ 0
⊢ wittStructureRat p Φ n =
    HMul.hMul (α := MvPolynomial (idx × ℕ) ℚ)
      ((C : (a : ℚ) → MvPolynomial (idx × ℕ) ℚ) (1 / HPow.hPow (α := ℚ) (↑p : ℚ) n) : MvPolynomial (idx × ℕ) ℚ)
      (HMul.hMul (β := MvPolynomial (idx × ℕ) ℚ) (wittStructureRat p Φ n)
        ((C : (a : ℚ) → MvPolynomial (idx × ℕ) ℚ) (HPow.hPow (α := ℚ) (↑p : ℚ) n) : MvPolynomial (idx × ℕ) ℚ))

Tactic:
rw [mul_left_comm, ← C_mul, div_mul_cancel₀, C_1, mul_one]

Premises used: div_mul_cancel₀, MvPolynomial.C_1, mul_left_comm, MvPolynomial.C_mul, mul_one
-- Module: Mathlib.RingTheory.WittVector.StructurePolynomial
Goal:
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℚ
n : ℕ
⊢ HPow.hPow (α := ℚ) (↑p : ℚ) n ≠ 0

Tactic:
pow_ne_zero _ (Nat.cast_ne_zero.2 hp.1.ne_zero)

Premises used: Iff.mpr, pow_ne_zero, Nat.Prime.ne_zero, Fact.out, Nat.cast_ne_zero
-- Module: Mathlib.RingTheory.WittVector.StructurePolynomial
Goal:
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℚ
n : ℕ
⊢ HPow.hPow (α := ℚ) (↑p : ℚ) n ≠ 0

Tactic:
exact pow_ne_zero _ (Nat.cast_ne_zero.2 hp.1.ne_zero)

Premises used: pow_ne_zero
-- Module: Mathlib.RingTheory.WittVector.StructurePolynomial
Goal:
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n : ℕ
IH :
  ∀ m < n + 1,
    Eq (α := MvPolynomial (idx × ℕ) ℚ)
      ((map (Int.castRingHom ℚ) : (a : MvPolynomial (idx × ℕ) ℤ) → MvPolynomial (idx × ℕ) ℚ) (wittStructureInt p Φ m) :
        MvPolynomial (idx × ℕ) ℚ)
      (wittStructureRat p ((map (Int.castRingHom ℚ) : (a : MvPolynomial idx ℤ) → MvPolynomial idx ℚ) Φ) m :
        MvPolynomial (idx × ℕ) ℚ)
a :
  Eq (α := MvPolynomial (idx × ℕ) ℚ)
    ((map (Int.castRingHom ℚ) : (a : MvPolynomial (idx × ℕ) ℤ) → MvPolynomial (idx × ℕ) ℚ)
        ((bind₁ fun (b : idx) ↦
                (rename fun (i : ℕ) ↦ (b, i) : (a : MvPolynomial ℕ ℤ) → MvPolynomial (idx × ℕ) ℤ)
                  ((expand p : (a : MvPolynomial ℕ ℤ) → MvPolynomial ℕ ℤ) (W_ ℤ n)) :
              (a : MvPolynomial idx ℤ) → MvPolynomial (idx × ℕ) ℤ)
            Φ :
          MvPolynomial (idx × ℕ) ℤ) :
      MvPolynomial (idx × ℕ) ℚ)
    ((map (Int.castRingHom ℚ) : (a : MvPolynomial (idx × ℕ) ℤ) → MvPolynomial (idx × ℕ) ℚ)
        ((bind₁ fun (i : ℕ) ↦
                (expand p : (a : MvPolynomial (idx × ℕ) ℤ) → MvPolynomial (idx × ℕ) ℤ) (wittStructureInt p Φ i) :
              (a : MvPolynomial ℕ ℤ) → MvPolynomial (idx × ℕ) ℤ)
            (W_ ℤ n) :
          MvPolynomial (idx × ℕ) ℤ) :
      MvPolynomial (idx × ℕ) ℚ)
⊢ Eq (α := MvPolynomial (idx × ℕ) ℤ)
    ((bind₁ fun (b : idx) ↦
            (rename fun (i : ℕ) ↦ (b, i) : (a : MvPolynomial ℕ ℤ) → MvPolynomial (idx × ℕ) ℤ)
              ((expand p : (a : MvPolynomial ℕ ℤ) → MvPolynomial ℕ ℤ) (W_ ℤ n)) :
          (a : MvPolynomial idx ℤ) → MvPolynomial (idx × ℕ) ℤ)
        Φ :
      MvPolynomial (idx × ℕ) ℤ)
    ((bind₁ fun (i : ℕ) ↦
            (expand p : (a : MvPolynomial (idx × ℕ) ℤ) → MvPolynomial (idx × ℕ) ℤ) (wittStructureInt p Φ i) :
          (a : MvPolynomial ℕ ℤ) → MvPolynomial (idx × ℕ) ℤ)
        (W_ ℤ n) :
      MvPolynomial (idx × ℕ) ℤ)

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

Premises used: Rat, MvPolynomial.map_injective, Int.castRingHom, Int.cast_injective
-- Module: Mathlib.RingTheory.WittVector.StructurePolynomial
Goal:
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n : ℕ
IH :
  ∀ m < n + 1,
    Eq (α := MvPolynomial (idx × ℕ) ℚ)
      ((map (Int.castRingHom ℚ) : (a : MvPolynomial (idx × ℕ) ℤ) → MvPolynomial (idx × ℕ) ℚ) (wittStructureInt p Φ m) :
        MvPolynomial (idx × ℕ) ℚ)
      (wittStructureRat p ((map (Int.castRingHom ℚ) : (a : MvPolynomial idx ℤ) → MvPolynomial idx ℚ) Φ) m :
        MvPolynomial (idx × ℕ) ℚ)
a :
  Eq (α := MvPolynomial (idx × ℕ) ℚ)
    ((bind₁ fun (i : idx) ↦
            (expand p : (a : MvPolynomial (idx × ℕ) ℚ) → MvPolynomial (idx × ℕ) ℚ)
              ((rename fun (i_1 : ℕ) ↦ (i, i_1) : (a : MvPolynomial ℕ ℚ) → MvPolynomial (idx × ℕ) ℚ) (W_ ℚ n) :
                MvPolynomial (idx × ℕ) ℚ) :
          (a : MvPolynomial idx ℚ) → MvPolynomial (idx × ℕ) ℚ)
        ((map (Int.castRingHom ℚ) : (a : MvPolynomial idx ℤ) → MvPolynomial idx ℚ) Φ : MvPolynomial idx ℚ) :
      MvPolynomial (idx × ℕ) ℚ)
    ((bind₁ fun (i : ℕ) ↦
            (expand p : (a : MvPolynomial (idx × ℕ) ℚ) → MvPolynomial (idx × ℕ) ℚ)
              ((map (Int.castRingHom ℚ) : (a : MvPolynomial (idx × ℕ) ℤ) → MvPolynomial (idx × ℕ) ℚ)
                  (wittStructureInt p Φ i) :
                MvPolynomial (idx × ℕ) ℚ) :
          (a : MvPolynomial ℕ ℚ) → MvPolynomial (idx × ℕ) ℚ)
        (W_ ℚ n) :
      MvPolynomial (idx × ℕ) ℚ)
⊢ Eq (α := MvPolynomial (idx × ℕ) ℚ)
    ((map (Int.castRingHom ℚ) : (a : MvPolynomial (idx × ℕ) ℤ) → MvPolynomial (idx × ℕ) ℚ)
        ((bind₁ fun (b : idx) ↦
                (rename fun (i : ℕ) ↦ (b, i) : (a : MvPolynomial ℕ ℤ) → MvPolynomial (idx × ℕ) ℤ)
                  ((expand p : (a : MvPolynomial ℕ ℤ) → MvPolynomial ℕ ℤ) (W_ ℤ n)) :
              (a : MvPolynomial idx ℤ) → MvPolynomial (idx × ℕ) ℤ)
            Φ :
          MvPolynomial (idx × ℕ) ℤ) :
      MvPolynomial (idx × ℕ) ℚ)
    ((map (Int.castRingHom ℚ) : (a : MvPolynomial (idx × ℕ) ℤ) → MvPolynomial (idx × ℕ) ℚ)
        ((bind₁ fun (i : ℕ) ↦
                (expand p : (a : MvPolynomial (idx × ℕ) ℤ) → MvPolynomial (idx × ℕ) ℤ) (wittStructureInt p Φ i) :
              (a : MvPolynomial ℕ ℤ) → MvPolynomial (idx × ℕ) ℤ)
            (W_ ℤ n) :
          MvPolynomial (idx × ℕ) ℤ) :
      MvPolynomial (idx × ℕ) ℚ)

Tactic:
simp only [map_bind₁, map_rename, map_expand, rename_expand, map_wittPolynomial]

Premises used: MvPolynomial.map_bind₁, MvPolynomial.map_expand, MvPolynomial.map_rename, map_wittPolynomial, MvPolynomial.rename_expand