awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.MulP (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n k : ℕ
zero :
  (bind₁ (wittMulN p 0) : (a : MvPolynomial ℕ ℤ) → MvPolynomial ℕ ℤ) (wittPolynomial p ℤ k) =
    HMul.hMul (α := MvPolynomial ℕ ℤ) (↑0 : MvPolynomial ℕ ℤ) (wittPolynomial p ℤ k)
⊢ (bind₁ (wittMulN p n) : (a : MvPolynomial ℕ ℤ) → MvPolynomial ℕ ℤ) (wittPolynomial p ℤ k) =
    HMul.hMul (α := MvPolynomial ℕ ℤ) (↑n : MvPolynomial ℕ ℤ) (wittPolynomial p ℤ k)
have succ : ∀ (n : ℕ)
  (ih :
    (bind₁ (wittMulN p n) : (a : MvPolynomial ℕ ℤ) → MvPolynomial ℕ ℤ) (wittPolynomial p ℤ k) =
      HMul.hMul (α := MvPolynomial ℕ ℤ) (↑n : MvPolynomial ℕ ℤ) (wittPolynomial p ℤ k)),
  (bind₁ (wittMulN p (n + 1)) : (a : MvPolynomial ℕ ℤ) → MvPolynomial ℕ ℤ) (wittPolynomial p ℤ k) =
    HMul.hMul (α := MvPolynomial ℕ ℤ) (↑(n + 1) : MvPolynomial ℕ ℤ) (wittPolynomial p ℤ k)
Tactic: induction n with
  | zero => simp [wittMulN, zero_mul, bind₁_zero_wittPolynomial]
  | succ n ih =>
    rw [wittMulN, ← bind₁_bind₁, wittAdd, wittStructureInt_prop]
    simp only [map_add, Nat.cast_succ, bind₁_X_right]
    rw [add_mul, one_mul, bind₁_rename, bind₁_rename]
    simp only [ih, Function.uncurry, Function.comp_def, bind₁_X_left, AlgHom.id_apply,
      Matrix.cons_val_zero, Matrix.cons_val_one]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.StructurePolynomial (goal)
Goal:
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℚ
n : ℕ
⊢ Eq (α := MvPolynomial (idx × ℕ) ℚ)
    ((bind₁ (wittStructureRat p Φ) : (a : MvPolynomial ℕ ℚ) → MvPolynomial (idx × ℕ) ℚ) (W_ ℚ 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 × ℕ) ℚ)
        ((bind₁ (xInTermsOfW p ℚ) : (a : MvPolynomial ℕ ℚ) → MvPolynomial ℕ ℚ) (W_ ℚ n)) :
      MvPolynomial (idx × ℕ) ℚ)
have rw : Eq (α := MvPolynomial (idx × ℕ) ℚ)
  ((bind₁ (wittStructureRat p Φ) : (a : MvPolynomial ℕ ℚ) → MvPolynomial (idx × ℕ) ℚ) (W_ ℚ n) :
    MvPolynomial (idx × ℕ) ℚ)
  ((bind₁ fun (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 × ℕ) ℚ)
            (xInTermsOfW p ℚ i) :
        (a : MvPolynomial ℕ ℚ) → MvPolynomial (idx × ℕ) ℚ)
      (W_ ℚ n) :
    MvPolynomial (idx × ℕ) ℚ)
Tactic: rw [bind₁_bind₁]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.StructurePolynomial (goal)
Goal:
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℚ
n : ℕ
⊢ 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 × ℕ) ℚ)
        ((bind₁ (xInTermsOfW p ℚ) : (a : MvPolynomial ℕ ℚ) → MvPolynomial ℕ ℚ) (W_ ℚ n)) :
      MvPolynomial (idx × ℕ) ℚ)
    ((bind₁ fun (i : idx) ↦ (rename (Prod.mk i) : (a : MvPolynomial ℕ ℚ) → MvPolynomial (idx × ℕ) ℚ) (W_ ℚ n) :
          (a : MvPolynomial idx ℚ) → MvPolynomial (idx × ℕ) ℚ)
        Φ :
      MvPolynomial (idx × ℕ) ℚ)
have 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 × ℕ) ℚ)
      (X n) :
    MvPolynomial (idx × ℕ) ℚ)
  ((bind₁ fun (i : idx) ↦ (rename (Prod.mk i) : (a : MvPolynomial ℕ ℚ) → MvPolynomial (idx × ℕ) ℚ) (W_ ℚ n) :
        (a : MvPolynomial idx ℚ) → MvPolynomial (idx × ℕ) ℚ)
      Φ :
    MvPolynomial (idx × ℕ) ℚ)
Tactic: rw [bind₁_xInTermsOfW_wittPolynomial p _ n, bind₁_X_right]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.StructurePolynomial (goal)
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 × ℕ) ℚ)
        (X n) :
      MvPolynomial (idx × ℕ) ℚ)
    ((bind₁ fun (i : idx) ↦ (rename (Prod.mk i) : (a : MvPolynomial ℕ ℚ) → MvPolynomial (idx × ℕ) ℚ) (W_ ℚ n) :
          (a : MvPolynomial idx ℚ) → MvPolynomial (idx × ℕ) ℚ)
        Φ :
      MvPolynomial (idx × ℕ) ℚ)
⊢ 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 × ℕ) ℚ)
        ((bind₁ (xInTermsOfW p ℚ) : (a : MvPolynomial ℕ ℚ) → MvPolynomial ℕ ℚ) (W_ ℚ n)) :
      MvPolynomial (idx × ℕ) ℚ)
    ((bind₁ fun (i : idx) ↦ (rename (Prod.mk i) : (a : MvPolynomial ℕ ℚ) → MvPolynomial (idx × ℕ) ℚ) (W_ ℚ n) :
          (a : MvPolynomial idx ℚ) → MvPolynomial (idx × ℕ) ℚ)
        Φ :
      MvPolynomial (idx × ℕ) ℚ)
have rw₁ : Eq (α := 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 (i : idx) ↦ (rename (Prod.mk i) : (a : MvPolynomial ℕ ℚ) → MvPolynomial (idx × ℕ) ℚ) (W_ ℚ n) :
        (a : MvPolynomial idx ℚ) → MvPolynomial (idx × ℕ) ℚ)
      Φ :
    MvPolynomial (idx × ℕ) ℚ)
Tactic: rw [bind₁_xInTermsOfW_wittPolynomial p _ n, bind₁_X_right]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.StructurePolynomial (goal)
Goal:
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℚ
⊢ ∃! φ : ℕ → MvPolynomial (idx × ℕ) ℚ,
    ∀ (n : ℕ),
      Eq (α := MvPolynomial (idx × ℕ) ℚ)
        ((bind₁ φ : (a : MvPolynomial ℕ ℚ) → MvPolynomial (idx × ℕ) ℚ) (W_ ℚ n) : MvPolynomial (idx × ℕ) ℚ)
        ((bind₁ fun (i : idx) ↦ (rename (Prod.mk i) : (a : MvPolynomial ℕ ℚ) → MvPolynomial (idx × ℕ) ℚ) (W_ ℚ n) :
              (a : MvPolynomial idx ℚ) → MvPolynomial (idx × ℕ) ℚ)
            Φ :
          MvPolynomial (idx × ℕ) ℚ)
have refine_1 : (fun (φ : ℕ → MvPolynomial (idx × ℕ) ℚ) ↦
    ∀ (n : ℕ),
      Eq (α := MvPolynomial (idx × ℕ) ℚ)
        ((bind₁ φ : (a : MvPolynomial ℕ ℚ) → MvPolynomial (idx × ℕ) ℚ) (W_ ℚ n) : MvPolynomial (idx × ℕ) ℚ)
        ((bind₁ fun (i : idx) ↦ (rename (Prod.mk i) : (a : MvPolynomial ℕ ℚ) → MvPolynomial (idx × ℕ) ℚ) (W_ ℚ n) :
              (a : MvPolynomial idx ℚ) → MvPolynomial (idx × ℕ) ℚ)
            Φ :
          MvPolynomial (idx × ℕ) ℚ))
  (wittStructureRat p Φ)
Tactic: refine ⟨wittStructureRat p Φ, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.StructurePolynomial (goal)
Goal:
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℚ
refine_1 :
  (fun (φ : ℕ → MvPolynomial (idx × ℕ) ℚ) ↦
      ∀ (n : ℕ),
        Eq (α := MvPolynomial (idx × ℕ) ℚ)
          ((bind₁ φ : (a : MvPolynomial ℕ ℚ) → MvPolynomial (idx × ℕ) ℚ) (W_ ℚ n) : MvPolynomial (idx × ℕ) ℚ)
          ((bind₁ fun (i : idx) ↦ (rename (Prod.mk i) : (a : MvPolynomial ℕ ℚ) → MvPolynomial (idx × ℕ) ℚ) (W_ ℚ n) :
                (a : MvPolynomial idx ℚ) → MvPolynomial (idx × ℕ) ℚ)
              Φ :
            MvPolynomial (idx × ℕ) ℚ))
    (wittStructureRat p Φ)
⊢ ∃! φ : ℕ → MvPolynomial (idx × ℕ) ℚ,
    ∀ (n : ℕ),
      Eq (α := MvPolynomial (idx × ℕ) ℚ)
        ((bind₁ φ : (a : MvPolynomial ℕ ℚ) → MvPolynomial (idx × ℕ) ℚ) (W_ ℚ n) : MvPolynomial (idx × ℕ) ℚ)
        ((bind₁ fun (i : idx) ↦ (rename (Prod.mk i) : (a : MvPolynomial ℕ ℚ) → MvPolynomial (idx × ℕ) ℚ) (W_ ℚ n) :
              (a : MvPolynomial idx ℚ) → MvPolynomial (idx × ℕ) ℚ)
            Φ :
          MvPolynomial (idx × ℕ) ℚ)
have refine_2 : ∀ (y : ℕ → MvPolynomial (idx × ℕ) ℚ),
  (fun (φ : ℕ → MvPolynomial (idx × ℕ) ℚ) ↦
        ∀ (n : ℕ),
          Eq (α := MvPolynomial (idx × ℕ) ℚ)
            ((bind₁ φ : (a : MvPolynomial ℕ ℚ) → MvPolynomial (idx × ℕ) ℚ) (W_ ℚ n) : MvPolynomial (idx × ℕ) ℚ)
            ((bind₁ fun (i : idx) ↦ (rename (Prod.mk i) : (a : MvPolynomial ℕ ℚ) → MvPolynomial (idx × ℕ) ℚ) (W_ ℚ n) :
                  (a : MvPolynomial idx ℚ) → MvPolynomial (idx × ℕ) ℚ)
                Φ :
              MvPolynomial (idx × ℕ) ℚ))
      y →
    y = wittStructureRat p Φ
Tactic: refine ⟨wittStructureRat p Φ, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.StructurePolynomial (goal)
Goal:
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℚ
φ : ℕ → MvPolynomial (idx × ℕ) ℚ
H :
  ∀ (n : ℕ),
    Eq (α := MvPolynomial (idx × ℕ) ℚ)
      ((bind₁ φ : (a : MvPolynomial ℕ ℚ) → MvPolynomial (idx × ℕ) ℚ) (W_ ℚ n) : MvPolynomial (idx × ℕ) ℚ)
      ((bind₁ fun (i : idx) ↦ (rename (Prod.mk i) : (a : MvPolynomial ℕ ℚ) → MvPolynomial (idx × ℕ) ℚ) (W_ ℚ n) :
            (a : MvPolynomial idx ℚ) → MvPolynomial (idx × ℕ) ℚ)
          Φ :
        MvPolynomial (idx × ℕ) ℚ)
⊢ φ = wittStructureRat p Φ
have refine_2 : ∀ (n : ℕ), φ n = wittStructureRat p Φ n
Tactic: funext n
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.StructurePolynomial (goal)
Goal:
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℚ
φ : ℕ → MvPolynomial (idx × ℕ) ℚ
H :
  ∀ (n : ℕ),
    Eq (α := MvPolynomial (idx × ℕ) ℚ)
      ((bind₁ φ : (a : MvPolynomial ℕ ℚ) → MvPolynomial (idx × ℕ) ℚ) (W_ ℚ n) : MvPolynomial (idx × ℕ) ℚ)
      ((bind₁ fun (i : idx) ↦ (rename (Prod.mk i) : (a : MvPolynomial ℕ ℚ) → MvPolynomial (idx × ℕ) ℚ) (W_ ℚ n) :
            (a : MvPolynomial idx ℚ) → MvPolynomial (idx × ℕ) ℚ)
          Φ :
        MvPolynomial (idx × ℕ) ℚ)
n : ℕ
⊢ φ n =
    (bind₁ φ : (a : MvPolynomial ℕ ℚ) → MvPolynomial (idx × ℕ) ℚ)
      ((bind₁ (W_ ℚ) : (a : MvPolynomial ℕ ℚ) → MvPolynomial ℕ ℚ) (xInTermsOfW p ℚ n))
have rw : φ n = (bind₁ φ : (a : MvPolynomial ℕ ℚ) → MvPolynomial (idx × ℕ) ℚ) (X n)
Tactic: rw [bind₁_wittPolynomial_xInTermsOfW p, bind₁_X_right]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.StructurePolynomial (goal)
Goal:
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℚ
φ : ℕ → MvPolynomial (idx × ℕ) ℚ
H :
  ∀ (n : ℕ),
    Eq (α := MvPolynomial (idx × ℕ) ℚ)
      ((bind₁ φ : (a : MvPolynomial ℕ ℚ) → MvPolynomial (idx × ℕ) ℚ) (W_ ℚ n) : MvPolynomial (idx × ℕ) ℚ)
      ((bind₁ fun (i : idx) ↦ (rename (Prod.mk i) : (a : MvPolynomial ℕ ℚ) → MvPolynomial (idx × ℕ) ℚ) (W_ ℚ n) :
            (a : MvPolynomial idx ℚ) → MvPolynomial (idx × ℕ) ℚ)
          Φ :
        MvPolynomial (idx × ℕ) ℚ)
n : ℕ
rw : φ n = (bind₁ φ : (a : MvPolynomial ℕ ℚ) → MvPolynomial (idx × ℕ) ℚ) (X n)
⊢ φ n =
    (bind₁ φ : (a : MvPolynomial ℕ ℚ) → MvPolynomial (idx × ℕ) ℚ)
      ((bind₁ (W_ ℚ) : (a : MvPolynomial ℕ ℚ) → MvPolynomial ℕ ℚ) (xInTermsOfW p ℚ n))
have rw₁ : φ n = φ n
Tactic: rw [bind₁_wittPolynomial_xInTermsOfW p, bind₁_X_right]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.StructurePolynomial (goal)
Goal:
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℚ
φ : ℕ → MvPolynomial (idx × ℕ) ℚ
H :
  ∀ (n : ℕ),
    Eq (α := MvPolynomial (idx × ℕ) ℚ)
      ((bind₁ φ : (a : MvPolynomial ℕ ℚ) → MvPolynomial (idx × ℕ) ℚ) (W_ ℚ n) : MvPolynomial (idx × ℕ) ℚ)
      ((bind₁ fun (i : idx) ↦ (rename (Prod.mk i) : (a : MvPolynomial ℕ ℚ) → MvPolynomial (idx × ℕ) ℚ) (W_ ℚ n) :
            (a : MvPolynomial idx ℚ) → MvPolynomial (idx × ℕ) ℚ)
          Φ :
        MvPolynomial (idx × ℕ) ℚ)
n : ℕ
⊢ φ n = wittStructureRat p Φ n
have refine_2 : (bind₁ φ : (a : MvPolynomial ℕ ℚ) → MvPolynomial (idx × ℕ) ℚ)
    ((bind₁ (W_ ℚ) : (a : MvPolynomial ℕ ℚ) → MvPolynomial ℕ ℚ) (xInTermsOfW p ℚ n)) =
  wittStructureRat p Φ n
Tactic: rw [show φ n = bind₁ φ (bind₁ (W_ ℚ) (xInTermsOfW p ℚ n)) by
        rw [bind₁_wittPolynomial_xInTermsOfW p, bind₁_X_right]]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.StructurePolynomial (goal)
Goal:
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℚ
φ : ℕ → MvPolynomial (idx × ℕ) ℚ
H :
  ∀ (n : ℕ),
    Eq (α := MvPolynomial (idx × ℕ) ℚ)
      ((bind₁ φ : (a : MvPolynomial ℕ ℚ) → MvPolynomial (idx × ℕ) ℚ) (W_ ℚ n) : MvPolynomial (idx × ℕ) ℚ)
      ((bind₁ fun (i : idx) ↦ (rename (Prod.mk i) : (a : MvPolynomial ℕ ℚ) → MvPolynomial (idx × ℕ) ℚ) (W_ ℚ n) :
            (a : MvPolynomial idx ℚ) → MvPolynomial (idx × ℕ) ℚ)
          Φ :
        MvPolynomial (idx × ℕ) ℚ)
n : ℕ
⊢ (bind₁ φ : (a : MvPolynomial ℕ ℚ) → MvPolynomial (idx × ℕ) ℚ)
      ((bind₁ (W_ ℚ) : (a : MvPolynomial ℕ ℚ) → MvPolynomial ℕ ℚ) (xInTermsOfW p ℚ n)) =
    wittStructureRat p Φ n
have refine_2 : (bind₁ fun (i : ℕ) ↦ (bind₁ φ : (a : MvPolynomial ℕ ℚ) → MvPolynomial (idx × ℕ) ℚ) (W_ ℚ i) :
      (a : MvPolynomial ℕ ℚ) → MvPolynomial (idx × ℕ) ℚ)
    (xInTermsOfW p ℚ n) =
  wittStructureRat p Φ n
Tactic: rw [bind₁_bind₁]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.StructurePolynomial (hypothesis)
Goal:
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℚ
n : ℕ
⊢ HMul.hMul (β := MvPolynomial (idx × ℕ) ℚ) (wittStructureRat p Φ n)
      ((C : (a : ℚ) → MvPolynomial (idx × ℕ) ℚ) (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 × ℕ) ℚ)
have this : HMul.hMul (α := MvPolynomial ℕ ℚ) (β := MvPolynomial ℕ ℚ) (xInTermsOfW p ℚ n)
    ((C : (a : ℚ) → MvPolynomial ℕ ℚ) (HPow.hPow (α := ℚ) (↑p : ℚ) n) : MvPolynomial ℕ ℚ) =
  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: have := xInTermsOfW_aux p ℚ n
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.StructurePolynomial (hypothesis)
Goal:
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℚ
n : ℕ
this :
  HMul.hMul (α := MvPolynomial ℕ ℚ) (β := MvPolynomial ℕ ℚ) (xInTermsOfW p ℚ n)
      ((C : (a : ℚ) → MvPolynomial ℕ ℚ) (HPow.hPow (α := ℚ) (↑p : ℚ) n) : MvPolynomial ℕ ℚ) =
    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))))
⊢ HMul.hMul (β := MvPolynomial (idx × ℕ) ℚ) (wittStructureRat p Φ n)
      ((C : (a : ℚ) → MvPolynomial (idx × ℕ) ℚ) (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 × ℕ) ℚ)
have 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 × ℕ) ℚ)
Tactic: replace := congr_arg (bind₁ fun k : ℕ => bind₁ (fun i => rename (Prod.mk i) (W_ ℚ k)) Φ) this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.StructurePolynomial (goal)
Goal:
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℚ
n : ℕ
| (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)))))
have 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)))))
Tactic: simp only [map_sub, bind₁_X_right]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.StructurePolynomial (goal)
Goal:
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℚ
n : ℕ
⊢ (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 × ℕ) ℚ)
have 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 × ℕ) ℚ)
Tactic: conv_lhs => simp only [map_sub, bind₁_X_right]