How to prove the equality of polynomial coefficients?

Stream: new members

[oishi]

image.png
Does anyone know how to prove the equality of coefficients here in Lean4? In other words, how should I complete the proof following split_ifs here?

import Mathlib

open BigOperators Nat Finset

def lah_number (n k : ℕ) : ℕ :=
  match n, k with
  | 0, 0 => 1
  | 0, _ => 0
  | _, 0 => 0
  | n+1, k+1 => choose n k * lah_number n (k+1) + choose n (k+1) * lah_number n k


theorem idt_237 (n : ℕ) (x : ℝ) : Polynomial.eval x (ascPochhammer ℝ n)
                                  = ∑ k in range (n+1), lah_number n k * Polynomial.eval x (descPochhammer ℝ k) := by
  sorry


theorem idt_273 (n : ℕ) (x : ℝ) : Polynomial.eval x (descPochhammer ℝ n)
                                  = ∑ k in range (n+1), lah_number n k * Polynomial.eval x (ascPochhammer ℝ k) * (-1:ℝ)^(n-k) := by
  sorry

theorem idt_240 (n m: ℕ) : ∑ k in range (n+1), lah_number n k * lah_number k m * (-1:ℝ)^(k+m)
                          = if n = m then 1 else 0 := by
  have h1 : ∀ x:ℝ , Polynomial.eval x (ascPochhammer ℝ n) = ∑ k in range (n+1), lah_number n k * Polynomial.eval x (descPochhammer ℝ k) := by
    exact idt_237 n
  have h2 : ∀ x:ℝ, Polynomial.eval x (ascPochhammer ℝ n)
        = ∑ k ∈ range (n + 1), ↑(lah_number n k) * ∑ m in range (k+1), lah_number k m * Polynomial.eval x (ascPochhammer ℝ m) * (-1:ℝ)^(k-m) := by
    intro x
    rw [h1]
    apply sum_congr rfl
    intro k hk
    congr
    rw [idt_273 k x]
  have h3 : ∀ x:ℝ, ∑ k ∈ range (n + 1), ↑(lah_number n k) * ∑ m ∈ range (k + 1), ↑(lah_number k m) * Polynomial.eval x (ascPochhammer ℝ m) * (-1:ℝ) ^ (k - m)
          = ∑ m ∈ range (n + 1), Polynomial.eval x (ascPochhammer ℝ m) * ∑ k ∈ Ico m (n + 1), ↑(lah_number n k) * ↑(lah_number k m) * (-1:ℝ) ^ (k - m) := by
    sorry
  have h4 : ∀ x:ℝ, ∑ m ∈ range (n + 1), Polynomial.eval x (ascPochhammer ℝ m) * ∑ k ∈ Ico m (n + 1), ↑(lah_number n k) * ↑(lah_number k m) * (-1:ℝ) ^ (k - m)
          = ∑ m ∈ range (n + 1), Polynomial.eval x (ascPochhammer ℝ m) * ∑ k ∈ range (n + 1), ↑(lah_number n k) * ↑(lah_number k m) * (-1:ℝ) ^ (k + m) := by
    sorry
  have h5 : ∀ x:ℝ, Polynomial.eval x (ascPochhammer ℝ n)
          = ∑ m ∈ range (n + 1), Polynomial.eval x (ascPochhammer ℝ m) * ∑ k ∈ range (n + 1), ↑(lah_number n k) * ↑(lah_number k m) * (-1:ℝ) ^ (k + m) := by
    intro x
    rw [h2, h3, h4]
  split_ifs with h
  .
    sorry
  .
    sorry