fix(algebra/group/pi): Fix apply-simp-lemmas for monoid_hom.single (#…

…12474)

so that the simp-normal form really is `pi.mul_single`.

While adjusting related lemmas in `group_theory.subgroup.basic`, add a
few missing `to_additive` attributes.

src/algebra/group/pi.lean

@@ -189,23 +189,31 @@ This is the `one_hom` version of `pi.mul_single`. -/
 @[to_additive zero_hom.single "The zero-preserving homomorphism including a single value
 into a dependent family of values, as functions supported at a point.
 
-This is the `zero_hom` version of `pi.single`.", simps]
+This is the `zero_hom` version of `pi.single`."]
 def one_hom.single [Π i, has_one $ f i] (i : I) : one_hom (f i) (Π i, f i) :=
 { to_fun := mul_single i,
   map_one' := mul_single_one i }
 
+@[to_additive, simp]
+lemma one_hom.single_apply [Π i, has_one $ f i] (i : I) (x : f i) :
+  one_hom.single f i x = mul_single i x := rfl
+
 /-- The monoid homomorphism including a single monoid into a dependent family of additive monoids,
 as functions supported at a point.
 
 This is the `monoid_hom` version of `pi.mul_single`. -/
 @[to_additive "The additive monoid homomorphism including a single additive
 monoid into a dependent family of additive monoids, as functions supported at a point.
 
-This is the `add_monoid_hom` version of `pi.single`.", simps]
+This is the `add_monoid_hom` version of `pi.single`."]
 def monoid_hom.single [Π i, mul_one_class $ f i] (i : I) : f i →* Π i, f i :=
 { map_mul' := mul_single_op₂ (λ _, (*)) (λ _, one_mul _) _,
   .. (one_hom.single f i) }
 
+@[to_additive, simp]
+lemma monoid_hom.single_apply [Π i, mul_one_class $ f i] (i : I) (x : f i) :
+  monoid_hom.single f i x = mul_single i x := rfl
+
 /-- The multiplicative homomorphism including a single `mul_zero_class`
 into a dependent family of `mul_zero_class`es, as functions supported at a point.
 

src/group_theory/subgroup/basic.lean

@@ -1197,10 +1197,10 @@ begin
   { intros h x hx i hi, refine h i hi ⟨_, hx, rfl⟩, }
 end
 
-@[simp]
-lemma single_mem_pi [decidable_eq η] {I : set η} {H : Π i, subgroup (f i)}
+@[simp, to_additive]
+lemma mul_single_mem_pi [decidable_eq η] {I : set η} {H : Π i, subgroup (f i)}
   (i : η) (x : f i) :
-  monoid_hom.single f i x ∈ pi I H ↔ (i ∈ I → x ∈ H i) :=
+  pi.mul_single i x ∈ pi I H ↔ (i ∈ I → x ∈ H i) :=
 begin
   split,
   { intros h hi, simpa using h i hi, },
@@ -1210,7 +1210,8 @@ begin
     { simp [heq, one_mem], }, }
 end
 
-lemma pi_mem_of_single_mem_aux [decidable_eq η] (I : finset η) {H : subgroup (Π i, f i) }
+@[to_additive]
+lemma pi_mem_of_mul_single_mem_aux [decidable_eq η] (I : finset η) {H : subgroup (Π i, f i) }
   (x : Π i, f i) (h1 : ∀ i, i ∉ I → x i = 1) (h2 : ∀ i, i ∈ I → pi.mul_single i (x i) ∈ H ) :
   x ∈ H :=
 begin
@@ -1237,19 +1238,23 @@ begin
     { apply h2, simp, } }
 end
 
-lemma pi_mem_of_single_mem [fintype η] [decidable_eq η] {H : subgroup (Π i, f i) } (x : Π i, f i)
-  (h : ∀ i, pi.mul_single i (x i) ∈ H) : x ∈ H :=
-pi_mem_of_single_mem_aux finset.univ x (by simp) (λ i _, h i)
+@[to_additive]
+lemma pi_mem_of_mul_single_mem [fintype η] [decidable_eq η] {H : subgroup (Π i, f i)}
+  (x : Π i, f i) (h : ∀ i, pi.mul_single i (x i) ∈ H) : x ∈ H :=
+pi_mem_of_mul_single_mem_aux finset.univ x (by simp) (λ i _, h i)
 
 /-- For finite index types, the `subgroup.pi` is generated by the embeddings of the groups.  -/
+@[to_additive "For finite index types, the `subgroup.pi` is generated by the embeddings of the
+additive groups."]
 lemma pi_le_iff [decidable_eq η] [fintype η] {H : Π i, subgroup (f i)} {J : subgroup (Π i, f i)} :
   pi univ H ≤ J ↔ (∀ i : η, map (monoid_hom.single f i) (H i) ≤ J) :=
 begin
   split,
   { rintros h i _ ⟨x, hx, rfl⟩, apply h, simpa using hx },
-  { exact λ h x hx, pi_mem_of_single_mem  x (λ i, h i (mem_map_of_mem _ (hx i trivial))), }
+  { exact λ h x hx, pi_mem_of_mul_single_mem  x (λ i, h i (mem_map_of_mem _ (hx i trivial))), }
 end
 
+@[to_additive]
 lemma pi_eq_bot_iff (H : Π i, subgroup (f i)) :
   pi set.univ H = ⊥ ↔ ∀ i, H i = ⊥ :=
 begin
@@ -1258,7 +1263,7 @@ begin
   split,
   { intros h i x hx,
     have : monoid_hom.single f i x = 1 :=
-    h (monoid_hom.single f i x) ((single_mem_pi i x).mpr (λ _, hx)),
+    h (monoid_hom.single f i x) ((mul_single_mem_pi i x).mpr (λ _, hx)),
     simpa using congr_fun this i, },
   { exact λ h x hx, funext (λ i, h _ _ (hx i trivial)), },
 end