mathlib

569de76b - Partial progress in rewriting `extend_to_fin`