chore(data/pi,algebra/group/pi): reorganize proofs (#6869)

Add `pi.single_op` and `pi.single_binop` and use them in the proofs.



Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

Author: urkud

src/algebra/group/pi.lean

@@ -154,38 +154,27 @@ into a dependent family of values, as functions supported at a point.
 This is the `zero_hom` version of `pi.single`. -/
 @[simps] def zero_hom.single [Π i, has_zero $ f i] (i : I) : zero_hom (f i) (Π i, f i) :=
 { to_fun := single i,
-  map_zero' := function.update_eq_self i 0 }
+  map_zero' := single_zero i }
 
 /-- 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] def add_monoid_hom.single [Π i, add_monoid $ f i] (i : I) : f i →+ Π i, f i :=
 { to_fun := single i,
-  map_add' := λ x y, funext $ λ j, begin
-    refine (apply_single₂ _ (λ _, _) i x y j).symm,
-    exact zero_add 0,
-  end,
+  map_add' := single_op₂ (λ _, (+)) (λ _, zero_add _) _,
   .. (zero_hom.single f i) }
 
-/-- The multiplicative homomorphism including a single `monoid_with_zero`
-into a dependent family of monoid_with_zeros, as functions supported at a point.
+/-- The multiplicative homomorphism including a single `mul_zero_class`
+into a dependent family of `mul_zero_class`es, as functions supported at a point.
 
 This is the `mul_hom` version of `pi.single`. -/
-@[simps] def mul_hom.single [Π i, monoid_with_zero $ f i] (i : I) : mul_hom (f i) (Π i, f i) :=
+@[simps] def mul_hom.single [Π i, mul_zero_class $ f i] (i : I) : mul_hom (f i) (Π i, f i) :=
 { to_fun := single i,
-  map_mul' := λ x y, funext $ λ j, begin
-    refine (apply_single₂ _ (λ _, _) i x y j).symm,
-    exact zero_mul 0,
-  end, }
+  map_mul' := single_op₂ (λ _, (*)) (λ _, zero_mul _) _, }
 
 variables {f}
 
-@[simp]
-lemma pi.single_zero [Π i, has_zero $ f i] (i : I) :
-  single i (0 : f i) = 0 :=
-(zero_hom.single f i).map_zero
-
 lemma pi.single_add [Π i, add_monoid $ f i] (i : I) (x y : f i) :
   single i (x + y) = single i x + single i y :=
 (add_monoid_hom.single f i).map_add x y
@@ -198,7 +187,7 @@ lemma pi.single_sub [Π i, add_group $ f i] (i : I) (x y : f i) :
   single i (x - y) = single i x - single i y :=
 (add_monoid_hom.single f i).map_sub x y
 
-lemma pi.single_mul [Π i, monoid_with_zero $ f i] (i : I) (x y : f i) :
+lemma pi.single_mul [Π i, mul_zero_class $ f i] (i : I) (x y : f i) :
   single i (x * y) = single i x * single i y :=
 (mul_hom.single f i).map_mul x y
 

src/algebra/module/pi.lean

@@ -91,20 +91,12 @@ instance distrib_mul_action' {g : I → Type*} {m : Π i, monoid (f i)} {n : Π
 lemma single_smul {α} [monoid α] [Π i, add_monoid $ f i]
   [Π i, distrib_mul_action α $ f i] [decidable_eq I] (i : I) (r : α) (x : f i) :
   single i (r • x) = r • single i x :=
-begin
-  ext j,
-  refine (apply_single _ (λ _, _) i x j).symm,
-  exact smul_zero _,
-end
+single_op (λ i : I, ((•) r : f i → f i)) (λ j, smul_zero _) _ _
 
 lemma single_smul' {g : I → Type*} [Π i, monoid_with_zero (f i)] [Π i, add_monoid (g i)]
   [Π i, distrib_mul_action (f i) (g i)] [decidable_eq I] (i : I) (r : f i) (x : g i) :
   single i (r • x) = single i r • single i x :=
-begin
-  ext j,
-  refine (apply_single₂ _ (λ _, _) i r x j).symm,
-  exact smul_zero _,
-end
+single_op₂ (λ i : I, ((•) : f i → g i → g i)) (λ j, smul_zero _) _ _ _
 
 variables (I f)
 

src/data/pi.lean

@@ -38,6 +38,8 @@ instance has_mul [∀ i, has_mul $ f i] :
 ⟨λ f g i, f i * g i⟩
 @[simp, to_additive] lemma mul_apply [∀ i, has_mul $ f i] : (x * y) i = x i * y i := rfl
 
+@[to_additive] lemma mul_def [Π i, has_mul $ f i] : x * y = λ i, x i * y i := rfl
+
 @[to_additive] instance has_inv [∀ i, has_inv $ f i] :
   has_inv (Π i : I, f i) :=
   ⟨λ f i, (f i)⁻¹⟩
@@ -58,14 +60,15 @@ variables [Π i, has_zero (f i)] [Π i, has_zero (g i)] [Π i, has_zero (h i)]
 def single (i : I) (x : f i) : Π i, f i :=
 function.update 0 i x
 
-@[simp]
-lemma single_eq_same (i : I) (x : f i) : single i x i = x :=
+@[simp] lemma single_eq_same (i : I) (x : f i) : single i x i = x :=
 function.update_same i x _
 
-@[simp]
-lemma single_eq_of_ne {i i' : I} (h : i' ≠ i) (x : f i) : single i x i' = 0 :=
+@[simp] lemma single_eq_of_ne {i i' : I} (h : i' ≠ i) (x : f i) : single i x i' = 0 :=
 function.update_noteq h x _
 
+@[simp] lemma single_zero (i : I) : single i (0 : f i) = 0 :=
+function.update_eq_self _ _
+
 lemma apply_single (f' : Π i, f i → g i) (hf' : ∀ i, f' i 0 = 0) (i : I) (x : f i) (j : I):
   f' j (single i x j) = single i (f' i x) j :=
 by simpa only [pi.zero_apply, hf', single] using function.apply_update f' 0 i x j
@@ -75,10 +78,20 @@ lemma apply_single₂ (f' : Π i, f i → g i → h i) (hf' : ∀ i, f' i 0 0 =
   f' j (single i x j) (single i y j) = single i (f' i x y) j :=
 begin
   by_cases h : j = i,
-  { subst h, simp only [single_eq_same], },
-  { simp only [h, single_eq_of_ne, ne.def, not_false_iff, hf'], },
+  { subst h, simp only [single_eq_same] },
+  { simp only [single_eq_of_ne h, hf'] },
 end
 
+lemma single_op {g : I → Type*} [Π i, has_zero (g i)] (op : Π i, f i → g i) (h : ∀ i, op i 0 = 0)
+  (i : I) (x : f i) :
+  single i (op i x) = λ j, op j (single i x j) :=
+eq.symm $ funext $ apply_single op h i x
+
+lemma single_op₂ {g₁ g₂ : I → Type*} [Π i, has_zero (g₁ i)] [Π i, has_zero (g₂ i)]
+  (op : Π i, g₁ i → g₂ i → f i) (h : ∀ i, op i 0 0 = 0) (i : I) (x₁ : g₁ i) (x₂ : g₂ i) :
+  single i (op i x₁ x₂) = λ j, op j (single i x₁ j) (single i x₂ j) :=
+eq.symm $ funext $ apply_single₂ op h i x₁ x₂
+
 variables (f)
 
 lemma single_injective (i : I) : function.injective (single i : f i → Π i, f i) :=