-- Module: Mathlib.GroupTheory.CoprodI
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
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 ⋯).fst (β := fun (i : ι) ↦ M i) =
                                  x) ↦
                            M x)
                            (((mk (M := M) [] ne_one chain_ne).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₁ ∈ (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') ⋯) ∨
                (mk (M := M) [] ne_one chain_ne).fstIdx (M := M) ≠ some j ∧
                  m₁ = Eq.rec (motive := fun (x : ι) (h : j = x) ↦ M x) m₂ ⋯
neg₁ :
  ∀ (head : (i : ι) × M i) (tail : List ((i : ι) × M i))
    (ne_one : ∀ l ∈ head :: tail, 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))
        (head :: tail)),
    (Sigma.mk (β := fun (i : ι) ↦ M i) i m₁ ∈ (mk (M := M) (head :: tail) ne_one chain_ne).toList (M := M).tail ∨
        (i ≠ j ∧
            ∃ (h : (mk (M := M) (head :: tail) ne_one chain_ne).toList (M := M) ≠ []),
              (mk (M := M) (head :: tail) 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) (head :: tail) ne_one chain_ne);
                    Pair.mk (M := M)
                      (m₂ *
                        if h :
                            ∃ (h : (mk (M := M) (head :: tail) ne_one chain_ne).toList (M := M) ≠ []),
                              ((mk (M := M) (head :: tail) 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) (head :: tail) ne_one chain_ne).toList (M := M).head ⋯).fst (β :=
                                    fun (i : ι) ↦ M i) =
                                  x) ↦
                            M x)
                            (((mk (M := M) (head :: tail) ne_one chain_ne).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₁ ∈ (mk (M := M) (head :: tail) ne_one chain_ne).toList (M := M) ∨
        m₁ ≠ 1 ∧
          ∃ (hij : i = j),
            Sigma.mk (β := fun (i : ι) ↦ M i) i m₁ ∈ (mk (M := M) (head :: tail) ne_one chain_ne).toList (M := M).tail ∨
              (∃ (m' : M j),
                  Sigma.mk (β := fun (i : ι) ↦ M i) j m' ∈
                      (mk (M := M) (head :: tail) ne_one chain_ne).toList (M := M).head? ∧
                    m₁ = Eq.rec (motive := fun (x : ι) (h : j = x) ↦ M x) (m₂ * m') ⋯) ∨
                (mk (M := M) (head :: tail) ne_one chain_ne).fstIdx (M := M) ≠ some j ∧
                  m₁ = Eq.rec (motive := fun (x : ι) (h : j = x) ↦ M x) m₂ ⋯
⊢ (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₂ ⋯

Tactic:
rcases w with ⟨_ | _, _, _⟩