fix(linear_algebra/quadratic_form/basic): align diamonds in the nat- and int- action (#12541)

This also provides `fun_like` and `zero_hom_class` instances.

The `has_scalar` code has been moved unchanged from further down in the file.

This change makes `coe_fn_sub` eligible for `dsimp`, since it can now be proved by `rfl`.

Author: eric-wieser

src/linear_algebra/quadratic_form/basic.lean

@@ -103,10 +103,16 @@ namespace quadratic_form
 
 variables {Q : quadratic_form R M}
 
+instance fun_like : fun_like (quadratic_form R M) M (λ _, R) :=
+{ coe := to_fun,
+  coe_injective' := λ x y h, by cases x; cases y; congr' }
+
+/-- Helper instance for when there's too many metavariables to apply
+`fun_like.has_coe_to_fun` directly. -/
 instance : has_coe_to_fun (quadratic_form R M) (λ _, M → R) := ⟨to_fun⟩
 
 /-- The `simp` normal form for a quadratic form is `coe_fn`, not `to_fun`. -/
-@[simp] lemma to_fun_eq_apply : Q.to_fun = ⇑ Q := rfl
+@[simp] lemma to_fun_eq_coe : Q.to_fun = ⇑ Q := rfl
 
 lemma map_smul (a : R) (x : M) : Q (a • x) = a * a * Q x := Q.to_fun_smul a x
 
@@ -116,6 +122,10 @@ by { rw [←one_smul R x, ←add_smul, map_smul], norm_num }
 @[simp] lemma map_zero : Q 0 = 0 :=
 by rw [←@zero_smul R _ _ _ _ (0 : M), map_smul, zero_mul, zero_mul]
 
+instance zero_hom_class : zero_hom_class (quadratic_form R M) M R :=
+{ map_zero := λ _, map_zero,
+  ..quadratic_form.fun_like }
+
 @[simp] lemma map_neg (x : M) : Q (-x) = Q x :=
 by rw [←@neg_one_smul R _ _ _ _ x, map_smul, neg_one_mul, neg_neg, one_mul]
 
@@ -200,12 +210,48 @@ end of_tower
 
 variable {Q' : quadratic_form R M}
 
-@[ext] lemma ext (H : ∀ (x : M), Q x = Q' x) : Q = Q' :=
-by { cases Q, cases Q', congr, funext, apply H }
+@[ext] lemma ext (H : ∀ (x : M), Q x = Q' x) : Q = Q' := fun_like.ext _ _ H
+
+lemma congr_fun (h : Q = Q') (x : M) : Q x = Q' x := fun_like.congr_fun h _
 
-lemma congr_fun (h : Q = Q') (x : M) : Q x = Q' x := h ▸ rfl
+lemma ext_iff : Q = Q' ↔ (∀ x, Q x = Q' x) := fun_like.ext_iff
 
-lemma ext_iff : Q = Q' ↔ (∀ x, Q x = Q' x) := ⟨congr_fun, ext⟩
+/-- Copy of a `quadratic_form` with a new `to_fun` equal to the old one. Useful to fix definitional
+equalities. -/
+protected def copy (Q : quadratic_form R M) (Q' : M → R) (h : Q' = ⇑Q) : quadratic_form R M :=
+{ to_fun := Q',
+  to_fun_smul := h.symm ▸ Q.to_fun_smul,
+  polar_add_left' := h.symm ▸ Q.polar_add_left',
+  polar_smul_left' := h.symm ▸ Q.polar_smul_left',
+  polar_add_right' := h.symm ▸ Q.polar_add_right',
+  polar_smul_right' := h.symm ▸ Q.polar_smul_right' }
+
+section has_scalar
+
+variables [monoid S] [distrib_mul_action S R] [smul_comm_class S R R]
+
+/-- `quadratic_form R M` inherits the scalar action from any algebra over `R`.
+
+When `R` is commutative, this provides an `R`-action via `algebra.id`. -/
+instance : has_scalar S (quadratic_form R M) :=
+⟨ λ a Q,
+  { to_fun := a • Q,
+    to_fun_smul := λ b x, by rw [pi.smul_apply, map_smul, pi.smul_apply, mul_smul_comm],
+    polar_add_left' := λ x x' y, by simp only [polar_smul, polar_add_left, smul_add],
+    polar_smul_left' := λ b x y, begin
+      simp only [polar_smul, polar_smul_left, ←mul_smul_comm, smul_eq_mul],
+    end,
+    polar_add_right' := λ x y y', by simp only [polar_smul, polar_add_right, smul_add],
+    polar_smul_right' := λ b x y, begin
+      simp only [polar_smul, polar_smul_right, ←mul_smul_comm, smul_eq_mul],
+    end } ⟩
+
+@[simp] lemma coe_fn_smul (a : S) (Q : quadratic_form R M) : ⇑(a • Q) = a • Q := rfl
+
+@[simp] lemma smul_apply (a : S) (Q : quadratic_form R M) (x : M) :
+  (a • Q) x = a • Q x := rfl
+
+end has_scalar
 
 instance : has_zero (quadratic_form R M) :=
 ⟨ { to_fun := λ x, 0,
@@ -242,36 +288,31 @@ instance : has_add (quadratic_form R M) :=
 instance : has_neg (quadratic_form R M) :=
 ⟨ λ Q,
   { to_fun := -Q,
-  to_fun_smul := λ a x,
-    by simp only [pi.neg_apply, map_smul, mul_neg],
-  polar_add_left' := λ x x' y,
-    by simp only [polar_neg, polar_add_left, neg_add],
-  polar_smul_left' := λ a x y,
-    by simp only [polar_neg, polar_smul_left, mul_neg, smul_eq_mul],
-  polar_add_right' := λ x y y',
-    by simp only [polar_neg, polar_add_right, neg_add],
-  polar_smul_right' := λ a x y,
-    by simp only [polar_neg, polar_smul_right, mul_neg, smul_eq_mul] } ⟩
+    to_fun_smul := λ a x,
+      by simp only [pi.neg_apply, map_smul, mul_neg],
+    polar_add_left' := λ x x' y,
+      by simp only [polar_neg, polar_add_left, neg_add],
+    polar_smul_left' := λ a x y,
+      by simp only [polar_neg, polar_smul_left, mul_neg, smul_eq_mul],
+    polar_add_right' := λ x y y',
+      by simp only [polar_neg, polar_add_right, neg_add],
+    polar_smul_right' := λ a x y,
+      by simp only [polar_neg, polar_smul_right, mul_neg, smul_eq_mul] } ⟩
 
 @[simp] lemma coe_fn_neg (Q : quadratic_form R M) : ⇑(-Q) = -Q := rfl
 
 @[simp] lemma neg_apply (Q : quadratic_form R M) (x : M) : (-Q) x = -Q x := rfl
 
-instance : add_comm_group (quadratic_form R M) :=
-{ add := (+),
-  zero := 0,
-  neg := has_neg.neg,
-  add_comm := λ Q Q', by { ext, simp only [add_apply, add_comm] },
-  add_assoc := λ Q Q' Q'', by { ext, simp only [add_apply, add_assoc] },
-  add_left_neg := λ Q, by { ext, simp only [add_apply, neg_apply, zero_apply, add_left_neg] },
-  add_zero := λ Q, by { ext, simp only [zero_apply, add_apply, add_zero] },
-  zero_add := λ Q, by { ext, simp only [zero_apply, add_apply, zero_add] } }
+instance : has_sub (quadratic_form R M) :=
+⟨ λ Q Q', (Q + -Q').copy (Q - Q') (sub_eq_add_neg _ _) ⟩
+
+@[simp] lemma coe_fn_sub (Q Q' : quadratic_form R M) : ⇑(Q - Q') = Q - Q' := rfl
 
-@[simp] lemma coe_fn_sub (Q Q' : quadratic_form R M) : ⇑(Q - Q') = Q - Q' :=
-by simp only [quadratic_form.coe_fn_neg, add_left_inj, quadratic_form.coe_fn_add, sub_eq_add_neg]
+@[simp] lemma sub_apply (Q Q' : quadratic_form R M) (x : M) : (Q - Q') x = Q x - Q' x := rfl
 
-@[simp] lemma sub_apply (Q Q' : quadratic_form R M) (x : M) : (Q - Q') x = Q x - Q' x :=
-by simp only [quadratic_form.neg_apply, add_left_inj, quadratic_form.add_apply, sub_eq_add_neg]
+instance : add_comm_group (quadratic_form R M) :=
+fun_like.coe_injective.add_comm_group _
+  coe_fn_zero coe_fn_add coe_fn_neg coe_fn_sub (λ _ _, coe_fn_smul _ _) (λ _ _, coe_fn_smul _ _)
 
 /-- `@coe_fn (quadratic_form R M)` as an `add_monoid_hom`.
 
@@ -299,38 +340,17 @@ open_locale big_operators
 
 end sum
 
-section has_scalar
+section distrib_mul_action
 
 variables [monoid S] [distrib_mul_action S R] [smul_comm_class S R R]
 
-/-- `quadratic_form R M` inherits the scalar action from any algebra over `R`.
-
-When `R` is commutative, this provides an `R`-action via `algebra.id`. -/
-instance : has_scalar S (quadratic_form R M) :=
-⟨ λ a Q,
-  { to_fun := a • Q,
-    to_fun_smul := λ b x, by rw [pi.smul_apply, map_smul, pi.smul_apply, mul_smul_comm],
-    polar_add_left' := λ x x' y, by simp only [polar_smul, polar_add_left, smul_add],
-    polar_smul_left' := λ b x y, begin
-      simp only [polar_smul, polar_smul_left, ←mul_smul_comm, smul_eq_mul],
-    end,
-    polar_add_right' := λ x y y', by simp only [polar_smul, polar_add_right, smul_add],
-    polar_smul_right' := λ b x y, begin
-      simp only [polar_smul, polar_smul_right, ←mul_smul_comm, smul_eq_mul],
-    end } ⟩
-
-@[simp] lemma coe_fn_smul (a : S) (Q : quadratic_form R M) : ⇑(a • Q) = a • Q := rfl
-
-@[simp] lemma smul_apply (a : S) (Q : quadratic_form R M) (x : M) :
-  (a • Q) x = a • Q x := rfl
-
 instance : distrib_mul_action S (quadratic_form R M) :=
 { mul_smul := λ a b Q, ext (λ x, by simp only [smul_apply, mul_smul]),
   one_smul := λ Q, ext (λ x, by simp only [quadratic_form.smul_apply, one_smul]),
   smul_add := λ a Q Q', by { ext, simp only [add_apply, smul_apply, smul_add] },
   smul_zero := λ a, by { ext, simp only [zero_apply, smul_apply, smul_zero] }, }
 
-end has_scalar
+end distrib_mul_action
 
 section module