-- Mathlib/GroupTheory/CoprodI.lean
theorem mem_rcons_iff {i j : ι} (p : Pair M i) (m : M j) :
    ⟨_, m⟩ ∈ (rcons p).toList ↔ ⟨_, m⟩ ∈ p.tail.toList ∨
      m ≠ 1 ∧ (∃ h : i = j, m = h ▸ p.head)

Proof state:
case pos
ι : Type u_1
M : ι → Type u_2
inst✝¹ : (i : ι) → Monoid (M i)
inst✝ : (i : ι) → DecidableEq (M i)
j : ι
m : M j
p : Pair M j
⊢ ⟨j, m⟩ ∈
      (if h : p.head = 1 then p.tail
        else { toList := ⟨j, p.head⟩ :: p.tail.toList, ne_one := ⋯, chain_ne := ⋯ }).toList ↔
    ⟨j, m⟩ ∈ p.tail.toList ∨ ¬m = 1 ∧ ∃ (h : j = j), m = h ▸ p.head

Tactic:
by_cases hm : m = p.head

Result:
case pos
ι : Type u_1
M : ι → Type u_2
inst✝¹ : (i : ι) → Monoid (M i)
inst✝ : (i : ι) → DecidableEq (M i)
j : ι
m : M j
p : Pair M j
hm : m = p.head
⊢ ⟨j, m⟩ ∈
      (if h : p.head = 1 then p.tail
        else { toList := ⟨j, p.head⟩ :: p.tail.toList, ne_one := ⋯, chain_ne := ⋯ }).toList ↔
    ⟨j, m⟩ ∈ p.tail.toList ∨ ¬m = 1 ∧ ∃ (h : j = j), m = h ▸ p.head

case neg
ι : Type u_1
M : ι → Type u_2
inst✝¹ : (i : ι) → Monoid (M i)
inst✝ : (i : ι) → DecidableEq (M i)
j : ι
m : M j
p : Pair M j
hm : ¬m = p.head
⊢ ⟨j, m⟩ ∈
      (if h : p.head = 1 then p.tail
        else { toList := ⟨j, p.head⟩ :: p.tail.toList, ne_one := ⋯, chain_ne := ⋯ }).toList ↔
    ⟨j, m⟩ ∈ p.tail.toList ∨ ¬m = 1 ∧ ∃ (h : j = j), m = h ▸ p.head

Proof state:
case pos
ι : Type u_1
M : ι → Type u_2
inst✝¹ : (i : ι) → Monoid (M i)
inst✝ : (i : ι) → DecidableEq (M i)
j : ι
p : Pair M j
⊢ ⟨j, p.head⟩ ∈
      (if h : p.head = 1 then p.tail
        else { toList := ⟨j, p.head⟩ :: p.tail.toList, ne_one := ⋯, chain_ne := ⋯ }).toList ↔
    ⟨j, p.head⟩ ∈ p.tail.toList ∨ ¬p.head = 1 ∧ ∃ (h : j = j), p.head = h ▸ p.head

Tactic:
split_ifs <;> simp_all

Result:
no goals

Proof state:
ι : Type u_1
M : ι → Type u_2
inst✝¹ : (i : ι) → Monoid (M i)
inst✝ : (i : ι) → DecidableEq (M i)
i j : ι
p : Pair M i
m : M j
⊢ ⟨j, m⟩ ∈
      (if h : p.head = 1 then p.tail
        else { toList := ⟨i, p.head⟩ :: p.tail.toList, ne_one := ⋯, chain_ne := ⋯ }).toList ↔
    ⟨j, m⟩ ∈ p.tail.toList ∨ ¬m = 1 ∧ ∃ (h : i = j), m = h ▸ p.head

Tactic:
by_cases hij : i = j

Result:
case pos
ι : Type u_1
M : ι → Type u_2
inst✝¹ : (i : ι) → Monoid (M i)
inst✝ : (i : ι) → DecidableEq (M i)
i j : ι
p : Pair M i
m : M j
hij : i = j
⊢ ⟨j, m⟩ ∈
      (if h : p.head = 1 then p.tail
        else { toList := ⟨i, p.head⟩ :: p.tail.toList, ne_one := ⋯, chain_ne := ⋯ }).toList ↔
    ⟨j, m⟩ ∈ p.tail.toList ∨ ¬m = 1 ∧ ∃ (h : i = j), m = h ▸ p.head

case neg
ι : Type u_1
M : ι → Type u_2
inst✝¹ : (i : ι) → Monoid (M i)
inst✝ : (i : ι) → DecidableEq (M i)
i j : ι
p : Pair M i
m : M j
hij : ¬i = j
⊢ ⟨j, m⟩ ∈
      (if h : p.head = 1 then p.tail
        else { toList := ⟨i, p.head⟩ :: p.tail.toList, ne_one := ⋯, chain_ne := ⋯ }).toList ↔
    ⟨j, m⟩ ∈ p.tail.toList ∨ ¬m = 1 ∧ ∃ (h : i = j), m = h ▸ p.head

Proof state:
case pos
ι : Type u_1
M : ι → Type u_2
inst✝¹ : (i : ι) → Monoid (M i)
inst✝ : (i : ι) → DecidableEq (M i)
i j : ι
p : Pair M i
m : M j
hij : i = j
⊢ ⟨j, m⟩ ∈
      (if h : p.head = 1 then p.tail
        else { toList := ⟨i, p.head⟩ :: p.tail.toList, ne_one := ⋯, chain_ne := ⋯ }).toList ↔
    ⟨j, m⟩ ∈ p.tail.toList ∨ ¬m = 1 ∧ ∃ (h : i = j), m = h ▸ p.head

Tactic:
subst i

Result:
case pos
ι : Type u_1
M : ι → Type u_2
inst✝¹ : (i : ι) → Monoid (M i)
inst✝ : (i : ι) → DecidableEq (M i)
j : ι
m : M j
p : Pair M j
⊢ ⟨j, m⟩ ∈
      (if h : p.head = 1 then p.tail
        else { toList := ⟨j, p.head⟩ :: p.tail.toList, ne_one := ⋯, chain_ne := ⋯ }).toList ↔
    ⟨j, m⟩ ∈ p.tail.toList ∨ ¬m = 1 ∧ ∃ (h : j = j), m = h ▸ p.head

Proof state:
case pos
ι : Type u_1
M : ι → Type u_2
inst✝¹ : (i : ι) → Monoid (M i)
inst✝ : (i : ι) → DecidableEq (M i)
j : ι
m : M j
p : Pair M j
hm : m = p.head
⊢ ⟨j, m⟩ ∈
      (if h : p.head = 1 then p.tail
        else { toList := ⟨j, p.head⟩ :: p.tail.toList, ne_one := ⋯, chain_ne := ⋯ }).toList ↔
    ⟨j, m⟩ ∈ p.tail.toList ∨ ¬m = 1 ∧ ∃ (h : j = j), m = h ▸ p.head

Tactic:
subst m

Result:
case pos
ι : Type u_1
M : ι → Type u_2
inst✝¹ : (i : ι) → Monoid (M i)
inst✝ : (i : ι) → DecidableEq (M i)
j : ι
p : Pair M j
⊢ ⟨j, p.head⟩ ∈
      (if h : p.head = 1 then p.tail
        else { toList := ⟨j, p.head⟩ :: p.tail.toList, ne_one := ⋯, chain_ne := ⋯ }).toList ↔
    ⟨j, p.head⟩ ∈ p.tail.toList ∨ ¬p.head = 1 ∧ ∃ (h : j = j), p.head = h ▸ p.head

Proof state:
case neg
ι : Type u_1
M : ι → Type u_2
inst✝¹ : (i : ι) → Monoid (M i)
inst✝ : (i : ι) → DecidableEq (M i)
i j : ι
p : Pair M i
m : M j
hij : ¬i = j
⊢ ⟨j, m⟩ ∈
      (if h : p.head = 1 then p.tail
        else { toList := ⟨i, p.head⟩ :: p.tail.toList, ne_one := ⋯, chain_ne := ⋯ }).toList ↔
    ⟨j, m⟩ ∈ p.tail.toList ∨ ¬m = 1 ∧ ∃ (h : i = j), m = h ▸ p.head

Tactic:
split_ifs <;> simp_all [Ne.symm hij]

Result:
no goals

Proof state:
case neg
ι : Type u_1
M : ι → Type u_2
inst✝¹ : (i : ι) → Monoid (M i)
inst✝ : (i : ι) → DecidableEq (M i)
j : ι
m : M j
p : Pair M j
hm : ¬m = p.head
⊢ ⟨j, m⟩ ∈
      (if h : p.head = 1 then p.tail
        else { toList := ⟨j, p.head⟩ :: p.tail.toList, ne_one := ⋯, chain_ne := ⋯ }).toList ↔
    ⟨j, m⟩ ∈ p.tail.toList ∨ ¬m = 1 ∧ ∃ (h : j = j), m = h ▸ p.head

Tactic:
split_ifs <;> simp_all

Result:
no goals

Proof state:
ι : Type u_1
M : ι → Type u_2
inst✝¹ : (i : ι) → Monoid (M i)
inst✝ : (i : ι) → DecidableEq (M i)
i j : ι
p : Pair M i
m : M j
⊢ ⟨j, m⟩ ∈ (rcons p).toList ↔ ⟨j, m⟩ ∈ p.tail.toList ∨ m ≠ 1 ∧ ∃ (h : i = j), m = h ▸ p.head

Tactic:
simp only [rcons, cons, ne_eq]

Result:
ι : Type u_1
M : ι → Type u_2
inst✝¹ : (i : ι) → Monoid (M i)
inst✝ : (i : ι) → DecidableEq (M i)
i j : ι
p : Pair M i
m : M j
⊢ ⟨j, m⟩ ∈
      (if h : p.head = 1 then p.tail
        else { toList := ⟨i, p.head⟩ :: p.tail.toList, ne_one := ⋯, chain_ne := ⋯ }).toList ↔
    ⟨j, m⟩ ∈ p.tail.toList ∨ ¬m = 1 ∧ ∃ (h : i = j), m = h ▸ p.head