Eliminator for functors out of discrete categories

Stream: mathlib4

[Robin Carlier]

Would having the following in CategoryTheory.DiscreteCategory be reasonable (as well as something similar for natural transforms/iso)?

import Mathlib.CategoryTheory.DiscreteCategory

namespace CategoryTheory.Discrete

@[elab_as_elim, cases_eliminator, induction_eliminator]
def discreteFunctorInduction {C J: Type*} [Category C] {motive : (Discrete J ⥤ C) → Sort*}
    (h : (f : J → C) → motive (Discrete.functor f)) (f : Discrete J ⥤ C) : motive f := by
  have necessary_evil : f = Discrete.functor (f.obj ∘ Discrete.mk) := by
    apply Functor.ext
    · rintro ⟨x⟩ ⟨y⟩ f
      obtain rfl : x = y := Discrete.eq_of_hom f
      obtain rfl : f = 𝟙 _ := rfl
      simp
    · rintro ⟨x⟩
      rfl
  rw [necessary_evil]
  exact h _

@[simp]
lemma discreteFunctorInduction_functor {C J: Type*} [Category C]
    {motive : (Discrete J ⥤ C) → Sort*}
    (h : (f : J → C) → motive (Discrete.functor f)) (f : J → C) :
    discreteFunctorInduction h (Discrete.functor f) = h f :=
  rfl

def asFunctorFromDiscrete {C J: Type*} [Category C] {motive : (J → C) → Sort*}
    (h : (f : Discrete J ⥤ C) → motive (f.obj ∘ Discrete.mk)) (f : J → C) : motive f := by
  exact h (Discrete.functor f)

@[simp]
lemma asFunctorFromDiscrete_obj_mk {C J: Type*} [Category C]
    {motive : (J → C) → Sort*}
    (h : (f : Discrete J ⥤ C) → motive (f.obj ∘ Discrete.mk))
    (f : Discrete J ⥤ C) :
    asFunctorFromDiscrete h (f.obj ∘ Discrete.mk) = h f := by
  have necessary_evil : f = Discrete.functor (f.obj ∘ Discrete.mk) := by
    sorry
  rw [necessary_evil]
  rfl

end CategoryTheory.Discrete

Context: I am thinking about generalizing some of the API (like cons, snoc, insertNth, contractNth...) present in Data.Fin.Tuple to functors out of Discrete Fin _, and it looks like there will be quite a lot of back and forth between the Fin _ -> C and "functors out of Discrete" points of view.