Commit 2026-09-08 19:42 501d6fc6

View on Github →

perf(Basic/Rel): use grind instead of aesop (#42405) Most of the elaboration time of Mathlib/Basic/Rel.lean goes into its 55 aesop calls. Speed them up by using grind instead (or, in one case, simp). Add a few more grind annotations to make this ergonomic. This reduces the elaboration time of the file by more than 40%.

Estimated changes

modified theorem Function.graph_id
modified theorem Function.mem_graph
modified theorem SetRel.cod_empty
modified theorem SetRel.cod_eq_empty_iff
modified theorem SetRel.comp_empty
modified theorem SetRel.comp_iUnion
modified theorem SetRel.comp_id
modified theorem SetRel.comp_sUnion
modified theorem SetRel.core_comp
modified theorem SetRel.core_id
modified theorem SetRel.core_inter
modified theorem SetRel.core_univ
modified theorem SetRel.dom_empty
modified theorem SetRel.dom_eq_empty_iff
modified theorem SetRel.empty_comp
modified theorem SetRel.iUnion_comp
modified theorem SetRel.id_comp
modified theorem SetRel.image_comp
modified theorem SetRel.image_empty_left
modified theorem SetRel.image_empty_right
modified theorem SetRel.image_eq_biUnion
modified theorem SetRel.image_iUnion
modified theorem SetRel.image_id
modified theorem SetRel.image_inter_dom
modified theorem SetRel.image_sUnion
modified theorem SetRel.image_subset_iff
modified theorem SetRel.image_union
modified theorem SetRel.image_univ_right
modified theorem SetRel.inv_id
modified theorem SetRel.mem_cod
modified theorem SetRel.mem_comp
modified theorem SetRel.mem_core
modified theorem SetRel.mem_dom
modified theorem SetRel.mem_id
modified theorem SetRel.mem_image
modified theorem SetRel.mem_inv
modified theorem SetRel.mem_preimage
modified theorem SetRel.preimage_comp
modified theorem SetRel.preimage_empty_left
modified theorem SetRel.preimage_empty_right
modified theorem SetRel.preimage_eq_biUnion
modified theorem SetRel.preimage_iUnion
modified theorem SetRel.preimage_id
modified theorem SetRel.preimage_inter_cod
modified theorem SetRel.preimage_sUnion
modified theorem SetRel.preimage_union
modified theorem SetRel.preimage_univ_right
modified theorem SetRel.sUnion_comp