Dependent version of congr_arg₂

Stream: lean4

[Geoffrey Irving]

Ignoring the dependent types this would be just simp [Vector.toList_length], but alas that does nothing. How can I prove this?

import Mathlib.Data.Vector.Basic

variable {α β : Type}

lemma congr_arg₂_vector (f : (n : ℕ) → Vector α n → β) (n : ℕ) (y : Vector α n) :
    ∀ h, f y.toList.length ⟨y.toList, h⟩ = f n y := by
  sorry

[Johan Commelin]

Does cases y help?

[Eric Wieser]

lemma congr_arg₂_vector (f : (n : ℕ) → Mathlib.Vector α n → β) (n : ℕ) (y : Mathlib.Vector α n) (h) :
    f y.toList.length ⟨y.toList, h⟩ = f n y := by
  obtain ⟨y, rfl⟩ := y
  rfl