Module: Mathlib.GroupTheory.CoprodI

Goal state before:
pp: case neg
ι : Type u_1
M : ι → Type u_2
inst✝² : (i : ι) → Monoid (M i)
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (M i)
i j : ι
m₁ : M i
m₂ : M j
w : Word M
hij : ¬i = j
⊢ (⟨i, m₁⟩ ∈ w.toList.tail ∨
      (i ≠ j ∧ ∃ (h : w.toList ≠ []), w.toList.head h = ⟨i, m₁⟩) ∨
        m₁ ≠ 1 ∧
          ∃ (h : j = i),
            m₁ =
              h ▸
                (have __src := (equivPair j) w;
                  {
                    head :=
                      m₂ *
                        if h : ∃ (h : w.toList ≠ []), (w.toList.head h).fst = j then ⋯ ▸ (w.toList.head ⋯).snd else 1,
                    tail := __src.tail, fstIdx_ne := ⋯ }).head) ↔
    ¬i = j ∧ ⟨i, m₁⟩ ∈ w.toList ∨
      m₁ ≠ 1 ∧
        ∃ (hij : i = j),
          ⟨i, m₁⟩ ∈ w.toList.tail ∨
            (∃ m', ⟨j, m'⟩ ∈ w.toList.head? ∧ m₁ = ⋯ ▸ (m₂ * m')) ∨ w.fstIdx ≠ some j ∧ m₁ = ⋯ ▸ m₂

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

Goal state after:
case neg.nil
ι : Type u_1
M : ι → Type u_2
inst✝² : (i : ι) → Monoid (M i)
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (M i)
i j : ι
m₁ : M i
m₂ : M j
hij : ¬i = j
ne_one✝ : ∀ l ∈ [], l.snd ≠ 1
chain_ne✝ : List.IsChain (fun l l' ↦ l.fst ≠ l'.fst) []
⊢ (⟨i, m₁⟩ ∈ { toList := [], ne_one := ne_one✝, chain_ne := chain_ne✝ }.toList.tail ∨
      (i ≠ j ∧
          ∃ (h : { toList := [], ne_one := ne_one✝, chain_ne := chain_ne✝ }.toList ≠ []),
            { toList := [], ne_one := ne_one✝, chain_ne := chain_ne✝ }.toList.head h = ⟨i, m₁⟩) ∨
        m₁ ≠ 1 ∧
          ∃ (h : j = i),
            m₁ =
              h ▸
                (have __src := (equivPair j) { toList := [], ne_one := ne_one✝, chain_ne := chain_ne✝ };
                  {
                    head :=
                      m₂ *
                        if h :
                            ∃ (h : { toList := [], ne_one := ne_one✝, chain_ne := chain_ne✝ }.toList ≠ []),
                              ({ toList := [], ne_one := ne_one✝, chain_ne := chain_ne✝ }.toList.head h).fst = j then
                          ⋯ ▸ ({ toList := [], ne_one := ne_one✝, chain_ne := chain_ne✝ }.toList.head ⋯).snd
                        else 1,
                    tail := __src.tail, fstIdx_ne := ⋯ }).head) ↔
    ¬i = j ∧ ⟨i, m₁⟩ ∈ { toList := [], ne_one := ne_one✝, chain_ne := chain_ne✝ }.toList ∨
      m₁ ≠ 1 ∧
        ∃ (hij : i = j),
          ⟨i, m₁⟩ ∈ { toList := [], ne_one := ne_one✝, chain_ne := chain_ne✝ }.toList.tail ∨
            (∃ m',
                ⟨j, m'⟩ ∈ { toList := [], ne_one := ne_one✝, chain_ne := chain_ne✝ }.toList.head? ∧
                  m₁ = ⋯ ▸ (m₂ * m')) ∨
              { toList := [], ne_one := ne_one✝, chain_ne := chain_ne✝ }.fstIdx ≠ some j ∧ m₁ = ⋯ ▸ m₂

case neg.cons
ι : Type u_1
M : ι → Type u_2
inst✝² : (i : ι) → Monoid (M i)
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (M i)
i j : ι
m₁ : M i
m₂ : M j
hij : ¬i = j
head✝ : (i : ι) × M i
tail✝ : List ((i : ι) × M i)
ne_one✝ : ∀ l ∈ head✝ :: tail✝, l.snd ≠ 1
chain_ne✝ : List.IsChain (fun l l' ↦ l.fst ≠ l'.fst) (head✝ :: tail✝)
⊢ (⟨i, m₁⟩ ∈ { toList := head✝ :: tail✝, ne_one := ne_one✝, chain_ne := chain_ne✝ }.toList.tail ∨
      (i ≠ j ∧
          ∃ (h : { toList := head✝ :: tail✝, ne_one := ne_one✝, chain_ne := chain_ne✝ }.toList ≠ []),
            { toList := head✝ :: tail✝, ne_one := ne_one✝, chain_ne := chain_ne✝ }.toList.head h = ⟨i, m₁⟩) ∨
        m₁ ≠ 1 ∧
          ∃ (h : j = i),
            m₁ =
              h ▸
                (have __src := (equivPair j) { toList := head✝ :: tail✝, ne_one := ne_one✝, chain_ne := chain_ne✝ };
                  {
                    head :=
                      m₂ *
                        if h :
                            ∃ (h : { toList := head✝ :: tail✝, ne_one := ne_one✝, chain_ne := chain_ne✝ }.toList ≠ []),
                              ({ toList := head✝ :: tail✝, ne_one := ne_one✝, chain_ne := chain_ne✝ }.toList.head
                                    h).fst =
                                j then
                          ⋯ ▸ ({ toList := head✝ :: tail✝, ne_one := ne_one✝, chain_ne := chain_ne✝ }.toList.head ⋯).snd
                        else 1,
                    tail := __src.tail, fstIdx_ne := ⋯ }).head) ↔
    ¬i = j ∧ ⟨i, m₁⟩ ∈ { toList := head✝ :: tail✝, ne_one := ne_one✝, chain_ne := chain_ne✝ }.toList ∨
      m₁ ≠ 1 ∧
        ∃ (hij : i = j),
          ⟨i, m₁⟩ ∈ { toList := head✝ :: tail✝, ne_one := ne_one✝, chain_ne := chain_ne✝ }.toList.tail ∨
            (∃ m',
                ⟨j, m'⟩ ∈ { toList := head✝ :: tail✝, ne_one := ne_one✝, chain_ne := chain_ne✝ }.toList.head? ∧
                  m₁ = ⋯ ▸ (m₂ * m')) ∨
              { toList := head✝ :: tail✝, ne_one := ne_one✝, chain_ne := chain_ne✝ }.fstIdx ≠ some j ∧ m₁ = ⋯ ▸ m₂