-- 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 head : ι
m : M head
w : Word M
h1 : w.fstIdx (M := M) ≠ some head
h2 : m ≠ 1
h :
  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)
pos :
  ∀ (hi : i = head),
    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)
            (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 ⋯).fst (β := fun (i : ι) ↦ M i) = x) ↦ M x)
            (((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 = 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)
          (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 ⋯).fst (β := fun (i : ι) ↦ M i) = x) ↦ M x)
          (((cons (M := M) m w h1 h2).toList (M := M).head ⋯).snd (β := fun (i : ι) ↦ M i)) ⋯
      else 1 :
      M i)
have neg : ∀ (hi : ¬i = head),
  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)
          (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: by_cases hi : i = head