-- 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 :
  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 × ℕ) ℚ) (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 (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
Cleared hypotheses: this