-- Module: Mathlib.GroupTheory.CoprodI
Goal:
ι : Type u_1
M : ι → Type u_2
inst : (i : ι) → Monoid (M i)
inst_1 : DecidableEq ι
inst_2 : (i : ι) → DecidableEq (M i)
i : ι
w : Word M
empty :
  Eq.{u_2 + 1} (α := M i)
    (Pair.head (M := M)
        (({
              toFun := fun (w : Word M) ↦
                (↑(consRecOn (M := M) (motive := fun (x : Word M) ↦ { p : Pair M i // rcons (M := M) p = x }) w
                      (Subtype.mk (p := fun (p : Pair M i) ↦ rcons (M := M) p = Word.empty (M := M))
                        (Pair.mk (M := M) 1 (Word.empty (M := M)) ⋯) ⋯)
                      fun (j : ι) (m : M j) (w : Word M) (h1 : w.fstIdx (M := M) ≠ some j) (h2 : m ≠ 1)
                        (x : { p : Pair M i // rcons (M := M) p = w }) ↦
                      if ij : i = j then
                        Subtype.mk (p := fun (p : Pair M i) ↦ rcons (M := M) p = Word.cons (M := M) m w h1 h2)
                          (Pair.mk (M := M) (Eq.rec (motive := fun (x : ι) (h : j = x) ↦ M x) m ⋯) w ⋯) ⋯
                      else
                        Subtype.mk (p := fun (p : Pair M i) ↦ rcons (M := M) p = Word.cons (M := M) m w h1 h2)
                          (Pair.mk (M := M) 1 (Word.cons (M := M) m w h1 h2) ⋯) ⋯) :
                  Pair M i),
              invFun := rcons (M := M), left_inv := ⋯, right_inv := ⋯ } :
            (a : Word M) → Pair M i)
          (Word.empty (M := M))) :
      M i)
    (if h :
          ∃ (h : Ne (α := List ((i : ι) × M i)) (toList (M := M) (Word.empty (M := M))) []),
            (List.head (toList (M := M) (Word.empty (M := M))) h).fst (β := fun (i : ι) ↦ M i) = i then
        Eq.rec (motive :=
          fun (x : ι) (h : (List.head (toList (M := M) (Word.empty (M := M))) ⋯).fst (β := fun (i : ι) ↦ M i) = x) ↦
          M x) (Sigma.snd (β := fun (i : ι) ↦ M i) (List.head (toList (M := M) (Word.empty (M := M))) ⋯)) ⋯
      else 1 :
      M i)
cons :
  ∀ (head : ι) (m : M head) (w : Word M) (h1 : w.fstIdx (M := M) ≠ some head) (h2 : m ≠ 1),
    Eq.{u_2 + 1} (α := M i)
        (Pair.head (M := M)
            (({
                  toFun := fun (w : Word M) ↦
                    (↑(consRecOn (M := M) (motive := fun (x : Word M) ↦ { p : Pair M i // rcons (M := M) p = x }) w
                          (Subtype.mk (p := fun (p : Pair M i) ↦ rcons (M := M) p = Word.empty (M := M))
                            (Pair.mk (M := M) 1 (Word.empty (M := M)) ⋯) ⋯)
                          fun (j : ι) (m : M j) (w : Word M) (h1 : w.fstIdx (M := M) ≠ some j) (h2 : m ≠ 1)
                            (x : { p : Pair M i // rcons (M := M) p = w }) ↦
                          if ij : i = j then
                            Subtype.mk (p := fun (p : Pair M i) ↦ rcons (M := M) p = Word.cons (M := M) m w h1 h2)
                              (Pair.mk (M := M) (Eq.rec (motive := fun (x : ι) (h : j = x) ↦ M x) m ⋯) w ⋯) ⋯
                          else
                            Subtype.mk (p := fun (p : Pair M i) ↦ rcons (M := M) p = Word.cons (M := M) m w h1 h2)
                              (Pair.mk (M := M) 1 (Word.cons (M := M) m w h1 h2) ⋯) ⋯) :
                      Pair M i),
                  invFun := rcons (M := M), left_inv := ⋯, right_inv := ⋯ } :
                (a : Word M) → Pair M i)
              w) :
          M i)
        (if h : ∃ (h : w.toList (M := M) ≠ []), (w.toList (M := M).head h).fst (β := fun (i : ι) ↦ M i) = i then
            Eq.rec (motive := fun (x : ι) (h : (w.toList (M := M).head ⋯).fst (β := fun (i : ι) ↦ M i) = x) ↦ M x)
              ((w.toList (M := M).head ⋯).snd (β := fun (i : ι) ↦ M i)) ⋯
          else 1 :
          M i) →
      Eq.{u_2 + 1} (α := M i)
        (Pair.head (M := M)
            (({
                  toFun := fun (w : Word M) ↦
                    (↑(consRecOn (M := M) (motive := fun (x : Word M) ↦ { p : Pair M i // rcons (M := M) p = x }) w
                          (Subtype.mk (p := fun (p : Pair M i) ↦ rcons (M := M) p = Word.empty (M := M))
                            (Pair.mk (M := M) 1 (Word.empty (M := M)) ⋯) ⋯)
                          fun (j : ι) (m : M j) (w : Word M) (h1 : w.fstIdx (M := M) ≠ some j) (h2 : m ≠ 1)
                            (x : { p : Pair M i // rcons (M := M) p = w }) ↦
                          if ij : i = j then
                            Subtype.mk (p := fun (p : Pair M i) ↦ rcons (M := M) p = Word.cons (M := M) m w h1 h2)
                              (Pair.mk (M := M) (Eq.rec (motive := fun (x : ι) (h : j = x) ↦ M x) m ⋯) w ⋯) ⋯
                          else
                            Subtype.mk (p := fun (p : Pair M i) ↦ rcons (M := M) p = Word.cons (M := M) m w h1 h2)
                              (Pair.mk (M := M) 1 (Word.cons (M := M) m w h1 h2) ⋯) ⋯) :
                      Pair M i),
                  invFun := rcons (M := M), left_inv := ⋯, right_inv := ⋯ } :
                (a : Word M) → Pair M i)
              (Word.cons (M := M) m w h1 h2)) :
          M i)
        (if h :
              ∃ (h : (Word.cons (M := M) m w h1 h2).toList (M := M) ≠ []),
                ((Word.cons (M := M) m w h1 h2).toList (M := M).head h).fst (β := fun (i : ι) ↦ M i) = i then
            Eq.rec (motive :=
              fun (x : ι)
                (h : ((Word.cons (M := M) m w h1 h2).toList (M := M).head ⋯).fst (β := fun (i : ι) ↦ M i) = x) ↦
              M x) (((Word.cons (M := M) m w h1 h2).toList (M := M).head ⋯).snd (β := fun (i : ι) ↦ M i)) ⋯
          else 1 :
          M i)
⊢ Eq.{u_2 + 1} (α := M i)
    (Pair.head (M := M)
        (({
              toFun := fun (w : Word M) ↦
                (↑(consRecOn (M := M) (motive := fun (x : Word M) ↦ { p : Pair M i // rcons (M := M) p = x }) w
                      (Subtype.mk (p := fun (p : Pair M i) ↦ rcons (M := M) p = Word.empty (M := M))
                        (Pair.mk (M := M) 1 (Word.empty (M := M)) ⋯) ⋯)
                      fun (j : ι) (m : M j) (w : Word M) (h1 : w.fstIdx (M := M) ≠ some j) (h2 : m ≠ 1)
                        (x : { p : Pair M i // rcons (M := M) p = w }) ↦
                      if ij : i = j then
                        Subtype.mk (p := fun (p : Pair M i) ↦ rcons (M := M) p = Word.cons (M := M) m w h1 h2)
                          (Pair.mk (M := M) (Eq.rec (motive := fun (x : ι) (h : j = x) ↦ M x) m ⋯) w ⋯) ⋯
                      else
                        Subtype.mk (p := fun (p : Pair M i) ↦ rcons (M := M) p = Word.cons (M := M) m w h1 h2)
                          (Pair.mk (M := M) 1 (Word.cons (M := M) m w h1 h2) ⋯) ⋯) :
                  Pair M i),
              invFun := rcons (M := M), left_inv := ⋯, right_inv := ⋯ } :
            (a : Word M) → Pair M i)
          w) :
      M i)
    (if h : ∃ (h : w.toList (M := M) ≠ []), (w.toList (M := M).head h).fst (β := fun (i : ι) ↦ M i) = i then
        Eq.rec (motive := fun (x : ι) (h : (w.toList (M := M).head ⋯).fst (β := fun (i : ι) ↦ M i) = x) ↦ M x)
          ((w.toList (M := M).head ⋯).snd (β := fun (i : ι) ↦ M i)) ⋯
      else 1 :
      M i)

Tactic:
induction w using consRecOn with
  | empty => simp
  | cons head =>
    by_cases hi : i = head
    · subst hi; simp
    · simp [hi, Ne.symm hi]

Premises used: Monoid.CoprodI.Word.empty, Monoid.CoprodI.Word.cons