-- Mathlib/GroupTheory/CoprodI.lean
theorem mem_smul_iff {i j : ι} {m₁ : M i} {m₂ : M j} {w : Word M} :
    ⟨_, m₁⟩ ∈ (of m₂ • w).toList ↔
      (¬i = j ∧ ⟨i, m₁⟩ ∈ w.toList)
      ∨ (m₁ ≠ 1 ∧ ∃ (hij : i = j),(⟨i, m₁⟩ ∈ w.toList.tail) ∨
        (∃ m', ⟨j, m'⟩ ∈ w.toList.head? ∧ m₁ = hij ▸ (m₂ * m')) ∨
        (w.fstIdx ≠ some j ∧ m₁ = hij ▸ m₂))

Proof state:
case neg
ι : Type u_1
M : ι → Type u_2
inst✝² : (i : ι) → Monoid (M i)
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (M i)
j : ι
m₂ : M j
w : Word M
m₁ : M j
hw : ⟨j, m₁⟩ ∉ w.toList.tail
⊢ (⟨j, m₁⟩ ∈ w.toList.tail ∨
      ¬m₁ = 1 ∧
        m₁ = m₂ * if h : ∃ (h : ¬w.toList = []), (w.toList.head h).fst = j then ⋯ ▸ (w.toList.head ⋯).snd else 1) ↔
    ¬m₁ = 1 ∧ (⟨j, m₁⟩ ∈ w.toList.tail ∨ (∃ m', ⟨j, m'⟩ ∈ w.toList.head? ∧ m₁ = m₂ * m') ∨ ¬w.fstIdx = some j ∧ m₁ = m₂)

Tactic:
simp only [hw, false_or, Option.mem_def, ne_eq, and_congr_right_iff]

Result:
case neg
ι : Type u_1
M : ι → Type u_2
inst✝² : (i : ι) → Monoid (M i)
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (M i)
j : ι
m₂ : M j
w : Word M
m₁ : M j
hw : ⟨j, m₁⟩ ∉ w.toList.tail
⊢ ¬m₁ = 1 →
    ((m₁ = m₂ * if h : ∃ (h : ¬w.toList = []), (w.toList.head h).fst = j then ⋯ ▸ (w.toList.head ⋯).snd else 1) ↔
      (∃ m', w.toList.head? = some ⟨j, m'⟩ ∧ m₁ = m₂ * m') ∨ ¬w.fstIdx = some j ∧ m₁ = m₂)

Proof state:
ι : Type u_1
M : ι → Type u_2
inst✝² : (i : ι) → Monoid (M i)
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (M i)
w : Word M
hnil : ¬w.toList = []
m₂ m₁ : M (w.toList.head hnil).fst
hw : ⟨(w.toList.head hnil).fst, m₁⟩ ∉ w.toList.tail
hm1 : ¬m₁ = 1
hm' : (∀ (x : M (w.toList.head hnil).fst), ¬w.toList.head? = some ⟨(w.toList.head hnil).fst, x⟩) ∧ m₁ = m₂
⊢ w.toList.head? = some ⟨(w.toList.head hnil).fst, (w.toList.head hnil).snd⟩

Tactic:
rw [List.head?_eq_head]

Result:
no goals

Proof state:
ι : 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
⊢ ⟨i, m₁⟩ ∈ (of m₂ • w).toList ↔
    ¬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:
rw [of_smul_def, mem_rcons_iff, mem_equivPair_tail_iff, equivPair_head, or_assoc]

Result:
ι : 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
⊢ (⟨i, m₁⟩ ∈ w.toList.tail ∨
      (i ≠ j ∧ ∃ (h : w.toList ≠ []), w.toList.head h = ⟨i, m₁⟩) ∨
        m₁ ≠ 1 ∧
          ∃ (h : j = i),
            m₁ =
              h ▸
                (let __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₂

Proof state:
case pos
ι : 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 ▸
                (let __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:
subst i

Result:
case pos
ι : Type u_1
M : ι → Type u_2
inst✝² : (i : ι) → Monoid (M i)
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (M i)
j : ι
m₂ : M j
w : Word M
m₁ : M j
⊢ (⟨j, m₁⟩ ∈ w.toList.tail ∨
      (j ≠ j ∧ ∃ (h : w.toList ≠ []), w.toList.head h = ⟨j, m₁⟩) ∨
        m₁ ≠ 1 ∧
          ∃ (h : j = j),
            m₁ =
              h ▸
                (let __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) ↔
    ¬j = j ∧ ⟨j, m₁⟩ ∈ w.toList ∨
      m₁ ≠ 1 ∧
        ∃ (hij : j = j),
          ⟨j, m₁⟩ ∈ w.toList.tail ∨
            (∃ m', ⟨j, m'⟩ ∈ w.toList.head? ∧ m₁ = ⋯ ▸ (m₂ * m')) ∨ w.fstIdx ≠ some j ∧ m₁ = ⋯ ▸ m₂

Proof state:
case pos.intro.mpr.inl.intro.intro
ι : Type u_1
M : ι → Type u_2
inst✝² : (i : ι) → Monoid (M i)
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (M i)
w : Word M
hnil : ¬w.toList = []
m₂ w✝ : M (w.toList.head hnil).fst
hw : ⟨(w.toList.head hnil).fst, m₂ * w✝⟩ ∉ w.toList.tail
hm1 : ¬m₂ * w✝ = 1
h : (w.toList.head hnil).snd = w✝
⊢ m₂ * w✝ = m₂ * (w.toList.head ⋯).snd

Tactic:
subst h

Result:
case pos.intro.mpr.inl.intro.intro
ι : Type u_1
M : ι → Type u_2
inst✝² : (i : ι) → Monoid (M i)
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (M i)
w : Word M
hnil : ¬w.toList = []
m₂ : M (w.toList.head hnil).fst
hw : ⟨(w.toList.head hnil).fst, m₂ * (w.toList.head hnil).snd⟩ ∉ w.toList.tail
hm1 : ¬m₂ * (w.toList.head hnil).snd = 1
⊢ m₂ * (w.toList.head hnil).snd = m₂ * (w.toList.head ⋯).snd

Proof state:
case neg
ι : Type u_1
M : ι → Type u_2
inst✝² : (i : ι) → Monoid (M i)
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (M i)
j : ι
m₂ : M j
w : Word M
m₁ : M j
hw : ⟨j, m₁⟩ ∉ w.toList.tail
hm1 : ¬m₁ = 1
⊢ (m₁ = m₂ * if h : ∃ (h : ¬w.toList = []), (w.toList.head h).fst = j then ⋯ ▸ (w.toList.head ⋯).snd else 1) ↔
    (∃ m', w.toList.head? = some ⟨j, m'⟩ ∧ m₁ = m₂ * m') ∨ ¬w.fstIdx = some j ∧ m₁ = m₂

Tactic:
split_ifs with h

Result:
case pos
ι : Type u_1
M : ι → Type u_2
inst✝² : (i : ι) → Monoid (M i)
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (M i)
j : ι
m₂ : M j
w : Word M
m₁ : M j
hw : ⟨j, m₁⟩ ∉ w.toList.tail
hm1 : ¬m₁ = 1
h : ∃ (h : ¬w.toList = []), (w.toList.head h).fst = j
⊢ m₁ = m₂ * ⋯ ▸ (w.toList.head ⋯).snd ↔
    (∃ m', w.toList.head? = some ⟨j, m'⟩ ∧ m₁ = m₂ * m') ∨ ¬w.fstIdx = some j ∧ m₁ = m₂

case neg
ι : Type u_1
M : ι → Type u_2
inst✝² : (i : ι) → Monoid (M i)
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (M i)
j : ι
m₂ : M j
w : Word M
m₁ : M j
hw : ⟨j, m₁⟩ ∉ w.toList.tail
hm1 : ¬m₁ = 1
h : ¬∃ (h : ¬w.toList = []), (w.toList.head h).fst = j
⊢ m₁ = m₂ * 1 ↔ (∃ m', w.toList.head? = some ⟨j, m'⟩ ∧ m₁ = m₂ * m') ∨ ¬w.fstIdx = some j ∧ m₁ = m₂

Proof state:
case pos.intro.mp
ι : Type u_1
M : ι → Type u_2
inst✝² : (i : ι) → Monoid (M i)
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (M i)
w : Word M
hnil : ¬w.toList = []
m₂ m₁ : M (w.toList.head hnil).fst
hw : ⟨(w.toList.head hnil).fst, m₁⟩ ∉ w.toList.tail
hm1 : ¬m₁ = 1
⊢ m₁ = m₂ * (w.toList.head ⋯).snd →
    (∃ m', w.toList.head hnil = ⟨(w.toList.head hnil).fst, m'⟩ ∧ m₁ = m₂ * m') ∨
      ¬w.fstIdx = some (w.toList.head hnil).fst ∧ m₁ = m₂

Tactic:
rintro rfl

Result:
case pos.intro.mp
ι : Type u_1
M : ι → Type u_2
inst✝² : (i : ι) → Monoid (M i)
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (M i)
w : Word M
hnil : ¬w.toList = []
m₂ : M (w.toList.head hnil).fst
hw : ⟨(w.toList.head hnil).fst, m₂ * (w.toList.head ⋯).snd⟩ ∉ w.toList.tail
hm1 : ¬m₂ * (w.toList.head ⋯).snd = 1
⊢ (∃ m', w.toList.head hnil = ⟨(w.toList.head hnil).fst, m'⟩ ∧ m₂ * (w.toList.head ⋯).snd = m₂ * m') ∨
    ¬w.fstIdx = some (w.toList.head hnil).fst ∧ m₂ * (w.toList.head ⋯).snd = m₂