-- Lean 4 proof step from Mathlib.LinearAlgebra.Lagrange (goal)
Goal:
F : Type u_1
inst : Field F
ι : Type u_3
inst_1 : Finite ι
x y : ι → F
hwd : ∀ (i j : ι), x i = x j → y i = y j
have have₁ have₂ : ∀ (this : Fintype ι), ∃ (q : F[X]), ∀ (i : ι), eval (x i) q = y i
have₃ :
  ∀ (this : Fintype ι) (hinj : Set.InjOn (β := F) (fun (d : F) ↦ d) (↑(image x univ) : Set F)),
    ∃ (q : F[X]), ∀ (i : ι), eval (x i) q = y i
have₄ :
  ∀ (this : Fintype ι) (hinj : Set.InjOn (β := F) (fun (d : F) ↦ d) (↑(image x univ) : Set F)),
    let v : F → F := fun (z : F) ↦ if h : ∃ (i : ι), x i = z then y (h.choose (p := fun (i : ι) ↦ x i = z)) else 0;
    ∀ (v_def : v = fun (z : F) ↦ if h : ∃ (i : ι), x i = z then y (h.choose (p := fun (i : ι) ↦ x i = z)) else 0),
      ∃ (q : F[X]), ∀ (i : ι), eval (x i) q = y i
have₅ :
  ∀ (this : Fintype ι) (hinj : Set.InjOn (β := F) (fun (d : F) ↦ d) (↑(image x univ) : Set F)),
    let v : F → F := fun (z : F) ↦ if h : ∃ (i : ι), x i = z then y (h.choose (p := fun (i : ι) ↦ x i = z)) else 0;
    ∀ (v_def : v = fun (z : F) ↦ if h : ∃ (i : ι), x i = z then y (h.choose (p := fun (i : ι) ↦ x i = z)) else 0)
      (i : ι), eval (x i) ((interpolate (image x univ) fun (d : F) ↦ d : (a : F → F) → F[X]) v) = y i
have₆ :
  ∀ (this : Fintype ι) (hinj : Set.InjOn (β := F) (fun (d : F) ↦ d) (↑(image x univ) : Set F)),
    let v : F → F := fun (z : F) ↦ if h : ∃ (i : ι), x i = z then y (h.choose (p := fun (i : ι) ↦ x i = z)) else 0;
    ∀ (v_def : v = fun (z : F) ↦ if h : ∃ (i : ι), x i = z then y (h.choose (p := fun (i : ι) ↦ x i = z)) else 0)
      (i : ι),
      (fun (z : F) ↦ (if h : ∃ (i : ι), x i = z then y (h.choose (p := fun (i : ι) ↦ x i = z)) else 0 : F)) (x i) = y i
have₇ :
  ∀ (this : Fintype ι) (hinj : Set.InjOn (β := F) (fun (d : F) ↦ d) (↑(image x univ) : Set F)),
    let v : F → F := fun (z : F) ↦ if h : ∃ (i : ι), x i = z then y (h.choose (p := fun (i : ι) ↦ x i = z)) else 0;
    ∀ (v_def : v = fun (z : F) ↦ if h : ∃ (i : ι), x i = z then y (h.choose (p := fun (i : ι) ↦ x i = z)) else 0)
      (i : ι), (if h : ∃ (i_1 : ι), x i_1 = x i then y (h.choose (p := fun (i_1 : ι) ↦ x i_1 = x i)) else 0) = y i
pos :
  ∀ (this : Fintype ι) (hinj : Set.InjOn (β := F) (fun (d : F) ↦ d) (↑(image x univ) : Set F)),
    let v : F → F := fun (z : F) ↦ if h : ∃ (i : ι), x i = z then y (h.choose (p := fun (i : ι) ↦ x i = z)) else 0;
    ∀ (v_def : v = fun (z : F) ↦ if h : ∃ (i : ι), x i = z then y (h.choose (p := fun (i : ι) ↦ x i = z)) else 0)
      (i : ι) (h : ∃ (i_1 : ι), x i_1 = x i), y (h.choose (p := fun (i_1 : ι) ↦ x i_1 = x i)) = y i
⊢ ∃ (q : F[X]), ∀ (i : ι), eval (x i) q = y i
have neg : ∀ (this : Fintype ι) (hinj : Set.InjOn (β := F) (fun (d : F) ↦ d) (↑(image x univ) : Set F)),
  let v : F → F := fun (z : F) ↦ if h : ∃ (i : ι), x i = z then y (h.choose (p := fun (i : ι) ↦ x i = z)) else 0;
  ∀ (v_def : v = fun (z : F) ↦ if h : ∃ (i : ι), x i = z then y (h.choose (p := fun (i : ι) ↦ x i = z)) else 0) (i : ι)
    (h : ¬∃ (i_1 : ι), x i_1 = x i), 0 = y i
Tactic: classical
  have : Fintype ι := Fintype.ofFinite ι
  have hinj : Set.InjOn (fun d : F ↦ d) (Finset.univ.image x) := Function.injective_id.injOn
  set v : F → F := fun z ↦ if h : ∃ i, x i = z then y h.choose else 0 with v_def
  refine ⟨Lagrange.interpolate (Finset.univ.image x) (fun d : F ↦ d) v, fun i ↦ ?_⟩
  rw [Lagrange.eval_interpolate_at_node _ hinj (by simp), v_def]
  simp only
  split_ifs with h
  · exact hwd _ _ h.choose_spec
  · aesop