-- 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
pos :
  ∀ (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₂ ⋯
⊢ (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 : ∀ (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 sorry).fst (β := fun (i : ι) ↦ M i) = x) ↦ M x)
                          ((w.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₁ ∈ 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') sorry) ∨
              w.fstIdx (M := M) ≠ some j ∧ m₁ = Eq.rec (motive := fun (x : ι) (h : j = x) ↦ M x) m₂ sorry
Tactic: by_cases hij : i = j