chore(data/finsupp/pointwise): golf using injective lemmas (#12086)

src/data/finsupp/pointwise.lean

@@ -32,6 +32,8 @@ variables [mul_zero_class β]
   whose value at `a` is `f a * g a`. -/
 instance : has_mul (α →₀ β) := ⟨zip_with (*) (mul_zero 0)⟩
 
+lemma coe_mul (g₁ g₂ : α →₀ β) : ⇑(g₁ * g₂) = g₁ * g₂ := rfl
+
 @[simp] lemma mul_apply {g₁ g₂ : α →₀ β} {a : α} : (g₁ * g₂) a = g₁ a * g₂ a :=
 rfl
 
@@ -47,59 +49,48 @@ begin
 end
 
 instance : mul_zero_class (α →₀ β) :=
-{ zero      := 0,
-  mul       := (*),
-  mul_zero  := λ f, by { ext, simp only [mul_apply, zero_apply, mul_zero], },
-  zero_mul  := λ f, by { ext, simp only [mul_apply, zero_apply, zero_mul], }, }
+finsupp.coe_fn_injective.mul_zero_class _ coe_zero coe_mul
 
 end
 
 instance [semigroup_with_zero β] : semigroup_with_zero (α →₀ β) :=
-{ mul       := (*),
-  mul_assoc := λ f g h, by { ext, simp only [mul_apply, mul_assoc], },
-  ..(infer_instance : mul_zero_class (α →₀ β)) }
+finsupp.coe_fn_injective.semigroup_with_zero _ coe_zero coe_mul
 
+-- note we cannot use `function.injective.non_unital_non_assoc_semiring` here as it creates
+-- a conflicting `nsmul` field
 instance [non_unital_non_assoc_semiring β] : non_unital_non_assoc_semiring (α →₀ β) :=
-{ left_distrib := λ f g h, by { ext, simp only [mul_apply, add_apply, left_distrib] {proj := ff} },
-  right_distrib := λ f g h,
-    by { ext, simp only [mul_apply, add_apply, right_distrib] {proj := ff} },
-  ..(infer_instance : mul_zero_class (α →₀ β)),
-  ..(infer_instance : add_comm_monoid (α →₀ β)) }
+{ ..(function.injective.distrib _ finsupp.coe_fn_injective coe_add coe_mul : distrib (α →₀ β)),
+  ..(finsupp.mul_zero_class : mul_zero_class (α →₀ β)),
+  ..(finsupp.add_comm_monoid : add_comm_monoid (α →₀ β)) }
 
 instance [non_unital_semiring β] : non_unital_semiring (α →₀ β) :=
 { ..(infer_instance : semigroup (α →₀ β)),
   ..(infer_instance : non_unital_non_assoc_semiring (α →₀ β)) }
 
 instance [non_unital_non_assoc_ring β] : non_unital_non_assoc_ring (α →₀ β) :=
-{ left_distrib := λ f g h, by { ext, simp only [mul_apply, add_apply, left_distrib] {proj := ff} },
-  right_distrib := λ f g h,
-    by { ext, simp only [mul_apply, add_apply, right_distrib] {proj := ff} },
-  ..(infer_instance : mul_zero_class (α →₀ β)),
+{ ..(infer_instance : non_unital_non_assoc_semiring (α →₀ β)),
   ..(infer_instance : add_comm_group (α →₀ β)) }
 
+
 -- TODO can this be generalized in the direction of `pi.has_scalar'`
 -- (i.e. dependent functions and finsupps)
 -- TODO in theory this could be generalised, we only really need `smul_zero` for the definition
-/-- The pointwise multiplicative action of functions on finitely supported functions -/
-instance pointwise_module [semiring β] : module (α → β) (α →₀ β) :=
+instance pointwise_scalar [semiring β] : has_scalar (α → β) (α →₀ β) :=
 { smul := λ f g, finsupp.of_support_finite (λ a, f a • g a) begin
     apply set.finite.subset g.finite_support,
     simp only [function.support_subset_iff, finsupp.mem_support_iff, ne.def,
       finsupp.fun_support_eq, finset.mem_coe],
     intros x hx h,
     apply hx,
     rw [h, smul_zero],
-  end,
-  one_smul := λ b,
-    by { ext a, simp only [one_smul, pi.one_apply, finsupp.of_support_finite_coe], },
-  mul_smul := λ x y b, by simp [finsupp.of_support_finite_coe, mul_smul],
-  smul_add := λ r x y, finsupp.ext (λ a, by simpa only [smul_add, pi.add_apply, coe_add]),
-  smul_zero := λ b, finsupp.ext (by simp [finsupp.of_support_finite_coe, smul_zero]),
-  zero_smul := λ a, finsupp.ext (λ b, by simp [finsupp.of_support_finite_coe]),
-  add_smul := λ r s x, finsupp.ext (λ b, by simp [finsupp.of_support_finite_coe, add_smul]) }
+  end }
 
 @[simp]
-lemma coe_pointwise_module [semiring β] (f : α → β) (g : α →₀ β) :
+lemma coe_pointwise_smul [semiring β] (f : α → β) (g : α →₀ β) :
   ⇑(f • g) = f • g := rfl
 
+/-- The pointwise multiplicative action of functions on finitely supported functions -/
+instance pointwise_module [semiring β] : module (α → β) (α →₀ β) :=
+function.injective.module _ coe_fn_add_hom coe_fn_injective coe_pointwise_smul
+
 end finsupp