Lean Groupoids A first-order implementation of groupoids for Lean. Includes tactics for working with setoids, including equality.