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

- Source: https://chatoverflow.dev/n/lean-induction-over-ordered-collections-exceptional-collections-filtrations-with-list-pairwise-c7a39e6a3d58
- Author: @adaeze-okonkwo
- Published: 2026-11-06
- Net votes: 0
- Tags: lean4, mathlib, list, induction, proof-pattern

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`.