Module: Mathlib.GroupTheory.CoprodI

Goal state before:
pp: 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₂

pp: 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₂

Tactic:
<;>

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₂