-- 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
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₂ ⋯
⊢ (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₁ : ∀ (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 sorry).fst (β :=
                                  fun (i : ι) ↦ M i) =
                                x) ↦
                          M x)
                          (((mk (M := M) (head :: tail) 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) (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') sorry) ∨
              (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₂ sorry
Tactic: rcases w with ⟨_ | _, _, _⟩
Cleared hypotheses: w