-- Lean 4 proof step from Mathlib.RingTheory.WittVector.StructurePolynomial (hypothesis)
Goal:
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n : ℕ
IH :
  ∀ m < n,
    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 × ℕ) ℚ)
c : idx × ℕ →₀ ℕ
⊢ (fun (x : ℤ) ↦ ((↑x : ℚ) : ℚ))
      (coeff c
            (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 × ℕ) ℚ)
                  ((map (Int.castRingHom ℚ) : (a : MvPolynomial idx ℤ) → MvPolynomial idx ℚ) Φ : MvPolynomial idx ℚ) :
                MvPolynomial (idx × ℕ) ℚ)
              (∑ i ∈ Finset.range n,
                  HMul.hMul (α := MvPolynomial (idx × ℕ) ℚ)
                    ((C : (a : ℚ) → MvPolynomial (idx × ℕ) ℚ) (HPow.hPow (α := ℚ) (↑p : ℚ) i) :
                      MvPolynomial (idx × ℕ) ℚ)
                    (HPow.hPow (α := MvPolynomial (idx × ℕ) ℚ)
                      (wittStructureRat p ((map (Int.castRingHom ℚ) : (a : MvPolynomial idx ℤ) → MvPolynomial idx ℚ) Φ)
                        i)
                      (p ^ (n - i))) :
                MvPolynomial (idx × ℕ) ℚ)) /
          HPow.hPow (α := ℚ) (↑p : ℚ) n).num =
    coeff c
        (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 × ℕ) ℚ)
              ((map (Int.castRingHom ℚ) : (a : MvPolynomial idx ℤ) → MvPolynomial idx ℚ) Φ : MvPolynomial idx ℚ) :
            MvPolynomial (idx × ℕ) ℚ)
          (∑ i ∈ Finset.range n,
              HMul.hMul (α := MvPolynomial (idx × ℕ) ℚ)
                ((C : (a : ℚ) → MvPolynomial (idx × ℕ) ℚ) (HPow.hPow (α := ℚ) (↑p : ℚ) i) : MvPolynomial (idx × ℕ) ℚ)
                (HPow.hPow (α := MvPolynomial (idx × ℕ) ℚ)
                  (wittStructureRat p ((map (Int.castRingHom ℚ) : (a : MvPolynomial idx ℤ) → MvPolynomial idx ℚ) Φ) i)
                  (p ^ (n - i))) :
            MvPolynomial (idx × ℕ) ℚ)) /
      HPow.hPow (α := ℚ) (↑p : ℚ) n
have sum_induction_steps : Eq.{u_2 + 1} (α := MvPolynomial (idx × ℕ) ℚ)
  ((map (Int.castRingHom ℚ) : (a : MvPolynomial (idx × ℕ) ℤ) → MvPolynomial (idx × ℕ) ℚ)
      (∑ i ∈ Finset.range n,
        HMul.hMul (α := MvPolynomial (idx × ℕ) ℤ)
          ((C : (a : ℤ) → MvPolynomial (idx × ℕ) ℤ) (HPow.hPow (α := ℤ) (↑p : ℤ) i) : MvPolynomial (idx × ℕ) ℤ)
          (wittStructureInt p Φ i ^ p ^ (n - i))) :
    MvPolynomial (idx × ℕ) ℚ)
  (∑ i ∈ Finset.range n,
      HMul.hMul (α := MvPolynomial (idx × ℕ) ℚ)
        ((C : (a : ℚ) → MvPolynomial (idx × ℕ) ℚ) (HPow.hPow (α := ℚ) (↑p : ℚ) i) : MvPolynomial (idx × ℕ) ℚ)
        (HPow.hPow (α := MvPolynomial (idx × ℕ) ℚ)
          (wittStructureRat p ((map (Int.castRingHom ℚ) : (a : MvPolynomial idx ℤ) → MvPolynomial idx ℚ) Φ) i)
          (p ^ (n - i))) :
    MvPolynomial (idx × ℕ) ℚ)
Tactic: have sum_induction_steps :
      map (Int.castRingHom ℚ)
        (∑ i ∈ range n, C ((p : ℤ) ^ i) * wittStructureInt p Φ i ^ p ^ (n - i)) =
      ∑ i ∈ range n,
        C ((p : ℚ) ^ i) * wittStructureRat p (map (Int.castRingHom ℚ) Φ) i ^ p ^ (n - i) := by
    rw [map_sum]
    apply Finset.sum_congr rfl
    intro i hi
    rw [Finset.mem_range] at hi
    simp only [IH i hi, map_mul, map_pow, map_C]
    rfl