-- Lean 4 proof step from Mathlib.LinearAlgebra.Lagrange (goal)
Goal:
F : Type u_1
inst : Field F
ι : Type u_2
inst_1 : DecidableEq ι
s : Finset ι
v r : ι → F
hvs : Set.InjOn v (↑s : Set ι)
k : ℕ
hk : k < #s
simp_rw :
  (⇑derivative : (a : F[X]) → F[X])^[k]
      (∑ i ∈ s,
        HMul.hMul (α := F[X]) (β := F[X]) ((C : (a : F) → F[X]) (r i / ∏ j ∈ s.erase i, (v i - v j)) : F[X])
          (∏ j ∈ s.erase i, HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) (v j) : F[X]) : F[X])) =
    HMul.hMul (α := F[X]) (↑k.factorial : F[X])
      (∑ i ∈ s,
        HMul.hMul (α := F[X]) (β := F[X]) ((C : (a : F) → F[X]) (r i / ∏ j ∈ s.erase i, (v i - v j)) : F[X])
          (∑ t ∈ powersetCard (#s - (k + 1)) (s.erase i),
              ∏ j ∈ t, HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) (v j) : F[X]) :
            F[X]))
simp_rw₁ :
  ∑ b ∈ s,
      (⇑derivative : (a : F[X]) → F[X])^[k]
        (HMul.hMul (α := F[X]) (β := F[X]) ((C : (a : F) → F[X]) (r b / ∏ j ∈ s.erase b, (v b - v j)) : F[X])
          (∏ j ∈ s.erase b, HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) (v j) : F[X]) : F[X])) =
    HMul.hMul (α := F[X]) (↑k.factorial : F[X])
      (∑ i ∈ s,
        HMul.hMul (α := F[X]) (β := F[X]) ((C : (a : F) → F[X]) (r i / ∏ j ∈ s.erase i, (v i - v j)) : F[X])
          (∑ t ∈ powersetCard (#s - (k + 1)) (s.erase i),
              ∏ j ∈ t, HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) (v j) : F[X]) :
            F[X]))
simp_rw₂ :
  ∑ x ∈ s,
      HMul.hMul (α := F[X]) (β := F[X]) ((C : (a : F) → F[X]) (r x / ∏ j ∈ s.erase x, (v x - v j)) : F[X])
        ((⇑derivative : (a : F[X]) → F[X])^[k]
            (∏ j ∈ s.erase x, HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) (v j) : F[X])) :
          F[X]) =
    HMul.hMul (α := F[X]) (↑k.factorial : F[X])
      (∑ i ∈ s,
        HMul.hMul (α := F[X]) (β := F[X]) ((C : (a : F) → F[X]) (r i / ∏ j ∈ s.erase i, (v i - v j)) : F[X])
          (∑ t ∈ powersetCard (#s - (k + 1)) (s.erase i),
              ∏ j ∈ t, HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) (v j) : F[X]) :
            F[X]))
⊢ (⇑derivative : (a : F[X]) → F[X])^[k] ((interpolate s v : (a : ι → F) → F[X]) r) =
    HMul.hMul (α := F[X]) (↑k.factorial : F[X])
      (∑ i ∈ s,
        HMul.hMul (α := F[X]) (β := F[X]) ((C : (a : F) → F[X]) (r i / ∏ j ∈ s.erase i, (v i - v j)) : F[X])
          (∑ t ∈ powersetCard (#s - (k + 1)) (s.erase i),
              ∏ a ∈ t, HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) (v a) : F[X]) :
            F[X]))
have simp_rw₃ : Eq.{u_1 + 1} (α := F[X])
  (∑ x ∈ s,
    HMul.hMul (α := F[X]) (β := F[X]) ((C : (a : F) → F[X]) (r x / ∏ j ∈ s.erase x, (v x - v j)) : F[X])
      ((⇑derivative : (a : F[X]) → F[X])^[k]
          (∏ j ∈ s.erase x, HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) (v j) : F[X])) :
        F[X]))
  (∑ i ∈ s,
    (↑k.factorial : F[X]) *
      HMul.hMul (α := F[X]) (β := F[X]) ((C : (a : F) → F[X]) (r i / ∏ j ∈ s.erase i, (v i - v j)) : F[X])
        (∑ t ∈ powersetCard (#s - (k + 1)) (s.erase i),
            ∏ j ∈ t, HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) (v j) : F[X]) :
          F[X]))
Tactic: classical
  simp_rw [interpolate_eq_sum, iterate_derivative_sum, iterate_derivative_C_mul, mul_sum s,
    ← mul_assoc, mul_comm (k.factorial : F[X]), mul_assoc]
  congr! 2 with i hi
  have hvs' := hvs.mono (coe_subset.mpr (erase_subset i s))
  calc
    derivative^[k] (∏ j ∈ s.erase i, (X - C (v j))) =
    derivative^[k] (∏ vj ∈ (s.erase i).image v, (X - C vj)) := by rw [Finset.prod_image hvs']
    _ = k.factorial * ∑ t ∈ ((s.erase i).image v).powersetCard (#s - (k + 1)),
          ∏ va ∈ t, (X - C va) := by
        grind [iterate_derivative_prod_X_sub_C]
    _ = k.factorial * ∑ t ∈ (s.erase i).powersetCard (#s - (k + 1)), ∏ a ∈ t, (X - C (v a)) := by
        rw [powersetCard_eq_filter, powerset_image, eq_comm]
        congrm k.factorial * ?_
        refine sum_nbij (·.image v) (fun a ha ↦ ?hi) ?i_inj (fun t ht ↦ ?i_surj) fun a ha ↦ ?h
        case hi => grind [card_image_of_injOn, hvs'.mono]
        case i_inj => exact (image_injOn_powerset_of_injOn hvs').mono (by grind)
        case i_surj => grind [card_image_of_injOn, hvs'.mono]
        case h => exact eq_comm.mp <| prod_image <| by grind [hvs'.mono]