mathlib

ed183f95 - chore(group_theory/submonoid): use `complete_lattice_of_Inf` (#2661)

chore(group_theory/submonoid): use `complete_lattice_of_Inf` (#2661) * Use `complete_lattice_of_Inf` for `submonoid` and `subgroup` lattices. * Add `sub*.copy`. * Add a few `@[simp]` lemmas.