mathlib

3187c8da - Eliminate `finish` from `semilattice_inf.inv`