-- 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
⊢ 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 = empty (M := M))
                        (Pair.mk (M := M) 1 (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 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 = empty (M := M))
                      (Pair.mk (M := M) 1 (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)
        (empty (M := M))) :
    M i)
  (if h :
        ∃ (h : Ne (α := List ((i : ι) × M i)) (toList (M := M) (empty (M := M))) []),
          (List.head (toList (M := M) (empty (M := M))) h).fst (β := fun (i : ι) ↦ M i) = i then
      Eq.rec (motive :=
        fun (x : ι) (h : (List.head (toList (M := M) (empty (M := M))) sorry).fst (β := fun (i : ι) ↦ M i) = x) ↦ M x)
        (Sigma.snd (β := fun (i : ι) ↦ M i) (List.head (toList (M := M) (empty (M := M))) sorry)) 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