-- Mathlib/Order/RelSeries.lean
lemma mem_snoc {p : RelSeries r} {newLast : α} {rel : r p.last newLast} {x : α} :
    x ∈ p.snoc newLast rel ↔ x ∈ p ∨ x = newLast

Proof state:
case mpr
α : Type u_1
r : Rel α α
p : RelSeries r
newLast : α
rel : r p.last newLast
x : α
h : (∃ y, p.toFun y = x) ∨ x = newLast
⊢ ∃ y, Fin.append p.toFun (singleton r newLast).toFun y = x

Tactic:
rcases h with (⟨i, rfl⟩ | rfl)

Result:
case mpr.inl.intro
α : Type u_1
r : Rel α α
p : RelSeries r
newLast : α
rel : r p.last newLast
i : Fin (p.length + 1)
⊢ ∃ y, Fin.append p.toFun (singleton r newLast).toFun y = p.toFun i

case mpr.inr
α : Type u_1
r : Rel α α
p : RelSeries r
x : α
rel : r p.last x
⊢ ∃ y, Fin.append p.toFun (singleton r x).toFun y = x

Proof state:
α : Type u_1
r : Rel α α
p : RelSeries r
newLast : α
rel : r p.last newLast
x : α
⊢ x ∈ p.snoc newLast rel ↔ x ∈ p ∨ x = newLast

Tactic:
simp only [snoc, append, singleton_length, Nat.add_zero, Nat.reduceAdd, Fin.cast_refl,
  Function.comp_id, mem_def, id_eq, Set.mem_range]

Result:
α : Type u_1
r : Rel α α
p : RelSeries r
newLast : α
rel : r p.last newLast
x : α
⊢ (∃ y, Fin.append p.toFun (singleton r newLast).toFun y = x) ↔ (∃ y, p.toFun y = x) ∨ x = newLast

Proof state:
case mp
α : Type u_1
r : Rel α α
p : RelSeries r
newLast : α
rel : r p.last newLast
x : α
⊢ (∃ y, Fin.append p.toFun (singleton r newLast).toFun y = x) → (∃ y, p.toFun y = x) ∨ x = newLast

Tactic:
rintro ⟨i, rfl⟩

Result:
case mp.intro
α : Type u_1
r : Rel α α
p : RelSeries r
newLast : α
rel : r p.last newLast
i : Fin (p.length + 1 + 1)
⊢ (∃ y, p.toFun y = Fin.append p.toFun (singleton r newLast).toFun i) ∨
    Fin.append p.toFun (singleton r newLast).toFun i = newLast

Proof state:
case mp.intro
α : Type u_1
r : Rel α α
p : RelSeries r
newLast : α
rel : r p.last newLast
i : Fin (p.length + 1 + 1)
⊢ (∃ y, p.toFun y = Fin.append p.toFun (singleton r newLast).toFun i) ∨
    Fin.append p.toFun (singleton r newLast).toFun i = newLast

Tactic:
exact Fin.lastCases (Or.inr <| Fin.append_right _ _ 0) (fun i => Or.inl ⟨⟨i.1, i.2⟩,
  (Fin.append_left _ _ _).symm⟩) i

Result:
no goals

Proof state:
case mpr.inr
α : Type u_1
r : Rel α α
p : RelSeries r
x : α
rel : r p.last x
⊢ ∃ y, Fin.append p.toFun (singleton r x).toFun y = x

Tactic:
exact ⟨Fin.last _, Fin.append_right _ _ 0⟩

Result:
no goals

Proof state:
α : Type u_1
r : Rel α α
p : RelSeries r
newLast : α
rel : r p.last newLast
x : α
⊢ (∃ y, Fin.append p.toFun (singleton r newLast).toFun y = x) ↔ (∃ y, p.toFun y = x) ∨ x = newLast

Tactic:
constructor

Result:
case mp
α : Type u_1
r : Rel α α
p : RelSeries r
newLast : α
rel : r p.last newLast
x : α
⊢ (∃ y, Fin.append p.toFun (singleton r newLast).toFun y = x) → (∃ y, p.toFun y = x) ∨ x = newLast

case mpr
α : Type u_1
r : Rel α α
p : RelSeries r
newLast : α
rel : r p.last newLast
x : α
⊢ (∃ y, p.toFun y = x) ∨ x = newLast → ∃ y, Fin.append p.toFun (singleton r newLast).toFun y = x

Proof state:
case mpr.inl.intro
α : Type u_1
r : Rel α α
p : RelSeries r
newLast : α
rel : r p.last newLast
i : Fin (p.length + 1)
⊢ ∃ y, Fin.append p.toFun (singleton r newLast).toFun y = p.toFun i

Tactic:
exact ⟨i.castSucc, Fin.append_left _ _ _⟩

Result:
no goals

Proof state:
case mpr
α : Type u_1
r : Rel α α
p : RelSeries r
newLast : α
rel : r p.last newLast
x : α
⊢ (∃ y, p.toFun y = x) ∨ x = newLast → ∃ y, Fin.append p.toFun (singleton r newLast).toFun y = x

Tactic:
intro h

Result:
case mpr
α : Type u_1
r : Rel α α
p : RelSeries r
newLast : α
rel : r p.last newLast
x : α
h : (∃ y, p.toFun y = x) ∨ x = newLast
⊢ ∃ y, Fin.append p.toFun (singleton r newLast).toFun y = x