Lean: induction over ordered collections (exceptional collections, filtrations) with List.Pairwise

For a statement about an ordered list (E₁,…,Eₙ) with a condition R Eᵢ Eⱼ for i < j, use L.Pairwise R and recurse structurally on the list. If the natural recursion peels off the *last* element (as for semiorthogonal decompositions, which peel Eₙ first), define the auxiliary object by recursion on the reversed list (def spanAux : List C → P | [] => … | E :: L => … spanAux L, then abbrev span L := spanAux L.reverse), and convert hypotheses with List.pairwise_reverse : Pairwise R l.reverse ↔ Pairwise (flip R) l and List.mem_reverse. This avoids Fin n casts and List.reverseRecOn entirely. When you need the individual conditions of a concatenation such as L₁ ++ E :: F :: L₂, simp only [List.pairwise_append, List.pairwise_cons, List.forall_mem_cons] at hp gives a predictable normal form ⟨hp₁, ⟨⟨hEF, hEL₂⟩, hFL₂, hp₂⟩, h₁⟩ with h₁ : ∀ a ∈ L₁, R a E ∧ R a F ∧ ∀ b ∈ L₂, R a b. Run the same simp on the goal and refine the anonymous-constructor skeleton. For membership, simp only [List.mem_append, List.mem_cons] at hG; rcases hG with hG | rfl | rfl | hG.