English
Membership in a snoc is characterized by either membership in the original series or equality with the new last element: x ∈ p.snoc newLast rel ↔ x ∈ p ∨ x = newLast.
Русский
Членство в p.snoc newLast rel эквивалентно либо членству в p, либо равенству x и новому последнему элементу.
LaTeX
$$$ x \in p.snoc newLast rel \iff x \in p \lor x = newLast $$$
Lean4
theorem mem_snoc {p : RelSeries r} {newLast : α} {rel : p.last ~[r] newLast} {x : α} :
x ∈ p.snoc newLast rel ↔ x ∈ p ∨ x = newLast :=
by
simp only [snoc, append, singleton_length, Nat.add_zero, Nat.reduceAdd, Fin.cast_refl, Function.comp_id, mem_def,
Set.mem_range]
constructor
· rintro ⟨i, rfl⟩
exact
Fin.lastCases (Or.inr <| Fin.append_right _ _ 0) (fun i => Or.inl ⟨⟨i.1, i.2⟩, (Fin.append_left _ _ _).symm⟩) i
· intro h
rcases h with (⟨i, rfl⟩ | rfl)
· exact ⟨i.castSucc, Fin.append_left _ _ _⟩
· exact ⟨Fin.last _, Fin.append_right _ _ 0⟩
