-- Lean 4 proof step from Mathlib.GroupTheory.CoprodI (goal)
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 = 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 = cons (M := M) m w h1 h2)
                          (Pair.mk (M := M) 1 (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)
⊢ 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 = 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 = cons (M := M) m w h1 h2)
                          (Pair.mk (M := M) 1 (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)
have 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)) sorry) sorry)
                        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 = cons (M := M) m w h1 h2)
                            (Pair.mk (M := M) (Eq.rec (motive := fun (x : ι) (h : j = x) ↦ M x) m sorry) w sorry) sorry
                        else
                          Subtype.mk (p := fun (p : Pair M i) ↦ rcons (M := M) p = cons (M := M) m w h1 h2)
                            (Pair.mk (M := M) 1 (cons (M := M) m w h1 h2) sorry) sorry) :
                    Pair M i),
                invFun := rcons (M := M), left_inv := sorry, right_inv := sorry } :
              (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 sorry).fst (β := fun (i : ι) ↦ M i) = x) ↦ M x)
            ((w.toList (M := M).head sorry).snd (β := fun (i : ι) ↦ M i)) sorry
        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)) sorry) sorry)
                        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 = cons (M := M) m w h1 h2)
                            (Pair.mk (M := M) (Eq.rec (motive := fun (x : ι) (h : j = x) ↦ M x) m sorry) w sorry) sorry
                        else
                          Subtype.mk (p := fun (p : Pair M i) ↦ rcons (M := M) p = cons (M := M) m w h1 h2)
                            (Pair.mk (M := M) 1 (cons (M := M) m w h1 h2) sorry) sorry) :
                    Pair M i),
                invFun := rcons (M := M), left_inv := sorry, right_inv := sorry } :
              (a : Word M) → Pair M i)
            (cons (M := M) m w h1 h2)) :
        M i)
      (if h :
            ∃ (h : (cons (M := M) m w h1 h2).toList (M := M) ≠ []),
              ((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 : ((cons (M := M) m w h1 h2).toList (M := M).head sorry).fst (β := fun (i : ι) ↦ M i) = x) ↦ M x)
            (((cons (M := M) m w h1 h2).toList (M := M).head sorry).snd (β := fun (i : ι) ↦ M i)) sorry
        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]
Cleared hypotheses: w