-- 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 j : ι
m₁ : M i
m₂ : M j
w : Word M
hij : ¬i = j
⊢ (Sigma.mk (β := fun (i : ι) ↦ M i) i m₁ ∈ w.toList (M := M).tail ∨
      (i ≠ j ∧ ∃ (h : w.toList (M := M) ≠ []), w.toList (M := M).head h = Sigma.mk (β := fun (i : ι) ↦ M i) i m₁) ∨
        m₁ ≠ 1 ∧
          ∃ (h : j = i),
            m₁ =
              Eq.rec (motive := fun (x : ι) (h : j = x) ↦ M x)
                (Pair.head (M := M)
                  (have __src : Pair M j := (equivPair (M := M) j : (a : Word M) → Pair M j) w;
                  Pair.mk (M := M)
                    (m₂ *
                      if h :
                          ∃ (h : w.toList (M := M) ≠ []),
                            (w.toList (M := M).head h).fst (β := fun (i : ι) ↦ M i) = j 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)
                    (__src.tail (M := M)) ⋯))
                h) ↔
    ¬i = j ∧ Sigma.mk (β := fun (i : ι) ↦ M i) i m₁ ∈ w.toList (M := M) ∨
      m₁ ≠ 1 ∧
        ∃ (hij : i = j),
          Sigma.mk (β := fun (i : ι) ↦ M i) i m₁ ∈ w.toList (M := M).tail ∨
            (∃ (m' : M j),
                Sigma.mk (β := fun (i : ι) ↦ M i) j m' ∈ w.toList (M := M).head? ∧
                  m₁ = Eq.rec (motive := fun (x : ι) (h : j = x) ↦ M x) (m₂ * m') ⋯) ∨
              w.fstIdx (M := M) ≠ some j ∧ m₁ = Eq.rec (motive := fun (x : ι) (h : j = x) ↦ M x) m₂ ⋯
have neg : ∀ (ne_one : ∀ (l : (i : ι) × M i), Membership.mem (γ := List ((i : ι) × M i)) [] l → l.snd (β := fun (i : ι) ↦ M i) ≠ 1)
  (chain_ne :
    List.IsChain (fun (l l' : (i : ι) × M i) ↦ l.fst (β := fun (i : ι) ↦ M i) ≠ l'.fst (β := fun (i : ι) ↦ M i)) []),
  (Sigma.mk (β := fun (i : ι) ↦ M i) i m₁ ∈ (mk (M := M) [] ne_one chain_ne).toList (M := M).tail ∨
      (i ≠ j ∧
          ∃ (h : (mk (M := M) [] ne_one chain_ne).toList (M := M) ≠ []),
            (mk (M := M) [] ne_one chain_ne).toList (M := M).head h = Sigma.mk (β := fun (i : ι) ↦ M i) i m₁) ∨
        m₁ ≠ 1 ∧
          ∃ (h : j = i),
            m₁ =
              Eq.rec (motive := fun (x : ι) (h : j = x) ↦ M x)
                (Pair.head (M := M)
                  (have __src : Pair M j :=
                    (equivPair (M := M) j : (a : Word M) → Pair M j) (mk (M := M) [] ne_one chain_ne);
                  Pair.mk (M := M)
                    (m₂ *
                      if h :
                          ∃ (h : (mk (M := M) [] ne_one chain_ne).toList (M := M) ≠ []),
                            ((mk (M := M) [] ne_one chain_ne).toList (M := M).head h).fst (β := fun (i : ι) ↦ M i) =
                              j then
                        Eq.rec (motive :=
                          fun (x : ι)
                            (h :
                              ((mk (M := M) [] ne_one chain_ne).toList (M := M).head sorry).fst (β := fun (i : ι) ↦ M i) =
                                x) ↦
                          M x) (((mk (M := M) [] ne_one chain_ne).toList (M := M).head sorry).snd (β := fun (i : ι) ↦ M i))
                          sorry
                      else 1)
                    (__src.tail (M := M)) sorry))
                h) ↔
    ¬i = j ∧ Sigma.mk (β := fun (i : ι) ↦ M i) i m₁ ∈ (mk (M := M) [] ne_one chain_ne).toList (M := M) ∨
      m₁ ≠ 1 ∧
        ∃ (hij : i = j),
          Sigma.mk (β := fun (i : ι) ↦ M i) i m₁ ∈ (mk (M := M) [] ne_one chain_ne).toList (M := M).tail ∨
            (∃ (m' : M j),
                Sigma.mk (β := fun (i : ι) ↦ M i) j m' ∈ (mk (M := M) [] ne_one chain_ne).toList (M := M).head? ∧
                  m₁ = Eq.rec (motive := fun (x : ι) (h : j = x) ↦ M x) (m₂ * m') sorry) ∨
              (mk (M := M) [] ne_one chain_ne).fstIdx (M := M) ≠ some j ∧
                m₁ = Eq.rec (motive := fun (x : ι) (h : j = x) ↦ M x) m₂ sorry
Tactic: rcases w with ⟨_ | _, _, _⟩
Cleared hypotheses: w