refactor(linear_algebra/matrix/nonsingular_inverse): clean up (#10175)

This file is a mess, and switches back and forth between three different inverses, proving the same things over and over again.

This pulls all the `invertible` versions of these statements to the top, and uses them here and there to golf proofs.

The lemmas `nonsing_inv_left_right` and `nonsing_inv_right_left` are merged into a single lemma `mul_eq_one_comm`.
The lemma `inv_eq_nonsing_inv_of_invertible` has been renamed to `inv_of_eq_nonsing_inv`

This also adds two new lemmas `inv_of_eq` and `det_inv_of`, both of which have trivial proofs.

src/algebra/invertible.lean

@@ -202,6 +202,15 @@ lemma commute_inv_of {M : Type*} [has_one M] [has_mul M] (m : M) [invertible m]
 calc m * ⅟m = 1       : mul_inv_of_self m
         ... = ⅟ m * m : (inv_of_mul_self m).symm
 
+section monoid_with_zero
+variable [monoid_with_zero α]
+
+/-- A variant of `ring.inverse_unit`. -/
+@[simp] lemma ring.inverse_invertible (x : α) [invertible x] : ring.inverse x = ⅟x :=
+ring.inverse_unit (unit_of_invertible _)
+
+end monoid_with_zero
+
 section group_with_zero
 
 variable [group_with_zero α]

src/algebra/lie/classical.lean

@@ -172,11 +172,7 @@ begin
 end
 
 lemma is_unit_Pso {i : R} (hi : i*i = -1) : is_unit (Pso p q R i) :=
-⟨{ val     := Pso p q R i,
-   inv     := Pso p q R (-i),
-   val_inv := Pso_inv p q R hi,
-   inv_val := by { apply matrix.nonsing_inv_left_right, exact Pso_inv p q R hi, }, },
-rfl⟩
+@is_unit_of_invertible _ _ _ (invertible_of_right_inverse _ _ (Pso_inv p q R hi))
 
 lemma indefinite_diagonal_transform {i : R} (hi : i*i = -1) :
   (Pso p q R i)ᵀ ⬝ (indefinite_diagonal p q R) ⬝ (Pso p q R i) = 1 :=
@@ -258,11 +254,7 @@ begin
 end
 
 lemma is_unit_PD [fintype l] [invertible (2 : R)] : is_unit (PD l R) :=
-⟨{ val     := PD l R,
-   inv     := ⅟(2 : R) • (PD l R)ᵀ,
-   val_inv := PD_inv l R,
-   inv_val := by { apply matrix.nonsing_inv_left_right, exact PD_inv l R, }, },
-rfl⟩
+@is_unit_of_invertible _ _ _ (invertible_of_right_inverse _ _ (PD_inv l R))
 
 /-- An equivalence between two possible definitions of the classical Lie algebra of type D. -/
 noncomputable def type_D_equiv_so' [fintype l] [invertible (2 : R)] :
@@ -322,11 +314,7 @@ begin
 end
 
 lemma is_unit_PB [invertible (2 : R)] : is_unit (PB l R) :=
-⟨{ val     := PB l R,
-   inv     := matrix.from_blocks 1 0 0 (PD l R)⁻¹,
-   val_inv := PB_inv l R,
-   inv_val := by { apply matrix.nonsing_inv_left_right, exact PB_inv l R, }, },
-rfl⟩
+@is_unit_of_invertible _ _ _ (invertible_of_right_inverse _ _ (PB_inv l R))
 
 lemma JB_transform : (PB l R)ᵀ ⬝ (JB l R) ⬝ (PB l R) = (2 : R) • matrix.from_blocks 1 0 0 (S l R) :=
 by simp [PB, JB, JD_transform, matrix.from_blocks_transpose, matrix.from_blocks_multiply,

src/linear_algebra/general_linear_group.lean

@@ -83,7 +83,7 @@ variables (A B : GL n R)
 lemma coe_inv : ↑(A⁻¹) = (↑A : matrix n n R)⁻¹ :=
 begin
   letI := A.invertible,
-  exact inv_eq_nonsing_inv_of_invertible (↑A : matrix n n R),
+  exact inv_of_eq_nonsing_inv (↑A : matrix n n R),
 end
 
 end coe_lemmas