-- Lean 4 proof step from Mathlib.GroupTheory.CoprodI (goal)
Goal:
ι : Type u_1
M : ι → Type u_2
inst : (i : ι) → Monoid (M i)
x : (i : ι) × M i
l : List ((i : ι) × M i)
hi :
  ∀ (hnot1 : ∀ l_1 ∈ l, l_1.snd (β := fun (i : ι) ↦ M i) ≠ 1)
    (hchain :
      List.IsChain (fun (l l' : (i : ι) × M i) ↦ l.fst (β := fun (i : ι) ↦ M i) ≠ l'.fst (β := fun (i : ι) ↦ M i)) l)
    (h : Word.mk (M := M) l hnot1 hchain ≠ empty (M := M)),
    ∃ (i : ι) (j : ι) (w' : NeWord M i j),
      w'.toWord (M := M).toList (M := M) = (Word.mk (M := M) l hnot1 hchain).toList (M := M)
hnot1_1 : ∀ l_1 ∈ x :: l, l_1.snd (β := fun (i : ι) ↦ M i) ≠ 1
hnot1 : x.snd (β := fun (i : ι) ↦ M i) ≠ 1 ∧ ∀ x ∈ l, x.snd (β := fun (i : ι) ↦ M i) ≠ 1
hchain :
  List.IsChain (fun (l l' : (i : ι) × M i) ↦ l.fst (β := fun (i : ι) ↦ M i) ≠ l'.fst (β := fun (i : ι) ↦ M i)) (x :: l)
h : Word.mk (M := M) (x :: l) hnot1_1 hchain ≠ empty (M := M)
cons :
  ∀
    (hi :
      ∀
        (hnot1 :
          ∀ (l : (i : ι) × M i), Membership.mem (γ := List ((i : ι) × M i)) [] l → l.snd (β := fun (i : ι) ↦ M i) ≠ 1)
        (hchain :
          List.IsChain (fun (l l' : (i : ι) × M i) ↦ l.fst (β := fun (i : ι) ↦ M i) ≠ l'.fst (β := fun (i : ι) ↦ M i))
            [])
        (h : Word.mk (M := M) [] hnot1 hchain ≠ empty (M := M)),
        ∃ (i : ι) (j : ι) (w' : NeWord M i j),
          w'.toWord (M := M).toList (M := M) = (Word.mk (M := M) [] hnot1 hchain).toList (M := M))
    (hnot1 : ∀ l ∈ [x], l.snd (β := fun (i : ι) ↦ M i) ≠ 1)
    (hnot1_2 :
      x.snd (β := fun (i : ι) ↦ M i) ≠ 1 ∧
        ∀ (x : (i : ι) × M i), Membership.mem (γ := List ((i : ι) × M i)) [] x → x.snd (β := fun (i : ι) ↦ M i) ≠ 1)
    (hchain :
      List.IsChain (fun (l l' : (i : ι) × M i) ↦ l.fst (β := fun (i : ι) ↦ M i) ≠ l'.fst (β := fun (i : ι) ↦ M i)) [x])
    (h : Word.mk (M := M) [x] hnot1 hchain ≠ empty (M := M)),
    ∃ (i : ι) (j : ι) (w' : NeWord M i j),
      w'.toWord (M := M).toList (M := M) = (Word.mk (M := M) [x] hnot1 hchain).toList (M := M)
⊢ ∃ (i : ι) (j : ι) (w' : NeWord M i j),
    w'.toWord (M := M).toList (M := M) = (Word.mk (M := M) (x :: l) hnot1_1 hchain).toList (M := M)
have cons₁ : ∀ (y : (i : ι) × M i) (l : List ((i : ι) × M i))
  (hi :
    ∀ (hnot1 : ∀ l_1 ∈ y :: l, l_1.snd (β := fun (i : ι) ↦ M i) ≠ 1)
      (hchain :
        List.IsChain (fun (l l' : (i : ι) × M i) ↦ l.fst (β := fun (i : ι) ↦ M i) ≠ l'.fst (β := fun (i : ι) ↦ M i))
          (y :: l))
      (h : Word.mk (M := M) (y :: l) hnot1 hchain ≠ empty (M := M)),
      ∃ (i : ι) (j : ι) (w' : NeWord M i j),
        w'.toWord (M := M).toList (M := M) = (Word.mk (M := M) (y :: l) hnot1 hchain).toList (M := M))
  (hnot1 : ∀ l_1 ∈ x :: y :: l, l_1.snd (β := fun (i : ι) ↦ M i) ≠ 1)
  (hnot1_2 : x.snd (β := fun (i : ι) ↦ M i) ≠ 1 ∧ ∀ x ∈ y :: l, x.snd (β := fun (i : ι) ↦ M i) ≠ 1)
  (hchain :
    List.IsChain (fun (l l' : (i : ι) × M i) ↦ l.fst (β := fun (i : ι) ↦ M i) ≠ l'.fst (β := fun (i : ι) ↦ M i))
      (x :: y :: l))
  (h : Word.mk (M := M) (x :: y :: l) hnot1 hchain ≠ empty (M := M)),
  ∃ (i : ι) (j : ι) (w' : NeWord M i j),
    w'.toWord (M := M).toList (M := M) = (Word.mk (M := M) (x :: y :: l) hnot1 hchain).toList (M := M)
Tactic: rcases l with - | ⟨y, l⟩
Cleared hypotheses: l, hi, hnot1_1, hnot1, hchain, h