Support for mutual and nested inductive types as `DecidableEq` instance generator

We currently have to manually write DecidableEq instances for nested and mutual inductive datatypes. Here is an example.

namespace Example

inductive Min where
  | Base
  | Const (a : List Min)

mutual
def decMin (a b : Min) : Decidable (a = b) :=
  match a, b with
  | .Base, .Base         => isTrue rfl
  | .Base, .Const ..     => isFalse (by intro; contradiction)
  | .Const .., .Base     => isFalse (by intro; contradiction)
  | .Const as, .Const bs => match decMinList as bs with
    | isTrue h => isTrue (by rw [h])
    | isFalse _ => isFalse (by intro h; injection h; contradiction)

def decMinList (as bs : List Min) : Decidable (as = bs) :=
  match as, bs with
  | [], [] => isTrue rfl
  | _::_, [] => isFalse (by intro; contradiction)
  | [], _::_ => isFalse (by intro; contradiction)
  | a::as, b::bs =>
    match decMin a b with
    | isTrue h₁ => match decMinList as bs with
      | isTrue h₂ => isTrue (by rw [h₁, h₂])
      | isFalse _ => isFalse (by intro h; injection h; contradiction)
    | isFalse _ => isFalse (by intro h; injection h; contradiction)
end

instance : DecidableEq Min :=
  decMin

Start with the nested and mutual inductive example in the issue and identify the existing DecidableEq instance generator entry point that handles ordinary inductive types. Trace how generated instances are constructed for recursive cases, then determine what support for the shown Min and List Min pattern would require. Done means the generator can produce the equivalent DecidableEq instance without manual definitions.