mathlib

f78a012d - feat(group_theory/subgroup): Add `mem_infi` and `coe_infi` (#3634)

feat(group_theory/subgroup): Add `mem_infi` and `coe_infi` (#3634) These already existed for submonoid, but were not lifted to subgroup. Also adds some missing `norm_cast` attributes to similar lemmas.