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.

src/group_theory/subgroup.lean

@@ -363,6 +363,16 @@ attribute [norm_cast] coe_Inf add_subgroup.coe_Inf
 @[simp, to_additive]
 lemma mem_Inf {S : set (subgroup G)} {x : G} : x ∈ Inf S ↔ ∀ p ∈ S, x ∈ p := set.mem_bInter_iff
 
+@[to_additive]
+lemma mem_infi {ι : Sort*} {S : ι → subgroup G} {x : G} : (x ∈ ⨅ i, S i) ↔ ∀ i, x ∈ S i :=
+by simp only [infi, mem_Inf, set.forall_range_iff]
+
+@[simp, to_additive]
+lemma coe_infi {ι : Sort*} {S : ι → subgroup G} : (↑(⨅ i, S i) : set G) = ⋂ i, S i :=
+by simp only [infi, coe_Inf, set.bInter_range]
+
+attribute [norm_cast] coe_infi add_subgroup.coe_infi
+
 /-- Subgroups of a group form a complete lattice. -/
 @[to_additive "The `add_subgroup`s of an `add_group` form a complete lattice."]
 instance : complete_lattice (subgroup G) :=

src/group_theory/submonoid/basic.lean

@@ -213,6 +213,8 @@ instance : has_Inf (submonoid M) :=
 @[simp, to_additive]
 lemma coe_Inf (S : set (submonoid M)) : ((Inf S : submonoid M) : set M) = ⋂ s ∈ S, ↑s := rfl
 
+attribute [norm_cast] coe_Inf add_submonoid.coe_Inf
+
 @[to_additive]
 lemma mem_Inf {S : set (submonoid M)} {x : M} : x ∈ Inf S ↔ ∀ p ∈ S, x ∈ p := set.mem_bInter_iff
 
@@ -224,7 +226,7 @@ by simp only [infi, mem_Inf, set.forall_range_iff]
 lemma coe_infi {ι : Sort*} {S : ι → submonoid M} : (↑(⨅ i, S i) : set M) = ⋂ i, S i :=
 by simp only [infi, coe_Inf, set.bInter_range]
 
-attribute [norm_cast] coe_Inf coe_infi
+attribute [norm_cast] coe_infi add_submonoid.coe_infi
 
 /-- Submonoids of a monoid form a complete lattice. -/
 @[to_additive "The `add_submonoid`s of an `add_monoid` form a complete lattice."]