-- 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
hm1 : ¬m₁ = 1
⊢ (¬∃ (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₂)

Tactic:
rw [fstIdx]

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
hm1 : ¬m₁ = 1
⊢ (¬∃ (h : ¬w.toList = []), (w.toList.head h).fst = j) →
    (m₁ = m₂ * 1 ↔
      (∃ m', w.toList.head? = some ⟨j, m'⟩ ∧ m₁ = m₂ * m') ∨ ¬Option.map Sigma.fst w.toList.head? = some j ∧ m₁ = 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
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₂

Tactic:
revert h

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
hm1 : ¬m₁ = 1
⊢ (¬∃ (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 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 ▸
                (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:
rcases w with ⟨_ | _, _, _⟩ <;>
simp [or_comm, hij, Ne.symm hij]

Result:
case neg.mk.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.Chain' (fun l l' => l.fst ≠ l'.fst) (head✝ :: tail✝)
⊢ head✝ = ⟨i, m₁⟩ ∨ ⟨i, m₁⟩ ∈ tail✝ ↔ ⟨i, m₁⟩ = head✝ ∨ ⟨i, m₁⟩ ∈ tail✝

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
h : w.toList.head hnil = ⟨(w.toList.head hnil).fst, w✝⟩
hw : ⟨(w.toList.head hnil).fst, m₂ * w✝⟩ ∉ w.toList.tail
hm1 : ¬m₂ * w✝ = 1
⊢ m₂ * w✝ = m₂ * (w.toList.head ⋯).snd

Tactic:
simp only [Sigma.ext_iff, heq_eq_eq, true_and] at 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₂ 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

Proof state:
case pos.intro.mpr
ι : 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', w.toList.head hnil = ⟨(w.toList.head hnil).fst, m'⟩ ∧ m₁ = m₂ * m') ∨
      ¬w.fstIdx = some (w.toList.head hnil).fst ∧ m₁ = m₂ →
    m₁ = m₂ * (w.toList.head ⋯).snd

Tactic:
rintro (⟨_, h, rfl⟩ | hm')

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₂ w✝ : M (w.toList.head hnil).fst
h : w.toList.head hnil = ⟨(w.toList.head hnil).fst, w✝⟩
hw : ⟨(w.toList.head hnil).fst, m₂ * w✝⟩ ∉ w.toList.tail
hm1 : ¬m₂ * w✝ = 1
⊢ m₂ * w✝ = m₂ * (w.toList.head ⋯).snd

case pos.intro.mpr.inr
ι : 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' : ¬w.fstIdx = some (w.toList.head hnil).fst ∧ m₁ = m₂
⊢ m₁ = m₂ * (w.toList.head ⋯).snd

Proof state:
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₂

Tactic:
rcases h with ⟨hnil, rfl⟩

Result:
case pos.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₁ : 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? = some ⟨(w.toList.head hnil).fst, m'⟩ ∧ m₁ = m₂ * m') ∨
      ¬w.fstIdx = some (w.toList.head hnil).fst ∧ m₁ = m₂

Proof state:
case pos.intro.mpr.inr
ι : 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' : ¬w.fstIdx = some (w.toList.head hnil).fst ∧ m₁ = m₂
⊢ m₁ = m₂ * (w.toList.head ⋯).snd

Tactic:
simp only [fstIdx, Option.map_eq_some', Sigma.exists,
  exists_and_right, exists_eq_right, not_exists, ne_eq] at hm'

Result:
case pos.intro.mpr.inr
ι : 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₂
⊢ m₁ = m₂ * (w.toList.head ⋯).snd

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

Tactic:
rfl

Result:
no goals