feat(algebra/group/units): teach simps about units (#8204)

This also introduces `units.copy` to match `invertible.copy`, and uses it to make some lemmas in normed_space/units true by `rfl` (and generated by `simps`).

src/algebra/group/units.lean

@@ -39,6 +39,19 @@ variables [monoid α]
 
 @[to_additive] instance : has_coe (units α) α := ⟨val⟩
 
+@[to_additive] instance : has_inv (units α) := ⟨λ u, ⟨u.2, u.1, u.4, u.3⟩⟩
+
+/-- See Note [custom simps projection] -/
+@[to_additive /-" See Note [custom simps projection] "-/]
+def simps.coe (u : units α) : α := u
+
+/-- See Note [custom simps projection] -/
+@[to_additive /-" See Note [custom simps projection] "-/]
+def simps.coe_inv (u : units α) : α := ↑(u⁻¹)
+
+initialize_simps_projections units (val → coe as_prefix, inv → coe_inv as_prefix)
+initialize_simps_projections add_units (val → coe as_prefix, neg → coe_neg as_prefix)
+
 @[simp, to_additive] lemma coe_mk (a : α) (b h₁ h₂) : ↑(units.mk a b h₁ h₂) = a := rfl
 
 @[ext, to_additive] theorem ext :
@@ -60,6 +73,17 @@ variables [monoid α]
   mk (u : α) y h₁ h₂ = u :=
 ext rfl
 
+/-- Copy a unit, adjusting definition equalities. -/
+@[to_additive /-"Copy an `add_unit`, adjusting definitional equalities."-/, simps]
+def copy (u : units α) (val : α) (hv : val = u) (inv : α) (hi : inv = ↑(u⁻¹)) : units α :=
+{ val := val, inv := inv,
+  inv_val := hv.symm ▸ hi.symm ▸ u.inv_val, val_inv := hv.symm ▸ hi.symm ▸ u.val_inv }
+
+@[to_additive]
+lemma copy_eq (u : units α) (val hv inv hi) :
+  u.copy val hv inv hi = u :=
+ext hv
+
 /-- Units of a monoid form a group. -/
 @[to_additive] instance : group (units α) :=
 { mul := λ u₁ u₂, ⟨u₁.val * u₂.val, u₂.inv * u₁.inv,
@@ -69,7 +93,7 @@ ext rfl
   mul_one := λ u, ext $ mul_one u,
   one_mul := λ u, ext $ one_mul u,
   mul_assoc := λ u₁ u₂ u₃, ext $ mul_assoc u₁ u₂ u₃,
-  inv := λ u, ⟨u.2, u.1, u.4, u.3⟩,
+  inv := has_inv.inv,
   mul_left_inv := λ u, ext u.inv_val }
 
 variables (a b : units α) {c : units α}

src/algebra/invertible.lean

@@ -95,18 +95,13 @@ def invertible.copy [monoid α] {r : α} (hr : invertible r) (s : α) (hs : s =
   mul_inv_of_self := by rw [hs, mul_inv_of_self] }
 
 /-- An `invertible` element is a unit. -/
+@[simps]
 def unit_of_invertible [monoid α] (a : α) [invertible a] : units α :=
 { val     := a,
   inv     := ⅟a,
   val_inv := by simp,
   inv_val := by simp, }
 
-@[simp] lemma unit_of_invertible_val [monoid α] (a : α) [invertible a] :
-  (unit_of_invertible a : α) = a := rfl
-
-@[simp] lemma unit_of_invertible_inv [monoid α] (a : α) [invertible a] :
-  (↑(unit_of_invertible a)⁻¹ : α) = ⅟a := rfl
-
 lemma is_unit_of_invertible [monoid α] (a : α) [invertible a] : is_unit a :=
 ⟨unit_of_invertible a, rfl⟩
 

src/algebra/lie/classical.lean

@@ -276,7 +276,7 @@ begin
   apply (skew_adjoint_matrices_lie_subalgebra_equiv (JD l R) (PD l R) (is_unit_PD l R)).trans,
   apply lie_equiv.of_eq,
   ext A,
-  rw [JD_transform, ← unit_of_invertible_val (2 : R), ←units.smul_def, lie_subalgebra.mem_coe,
+  rw [JD_transform, ← coe_unit_of_invertible (2 : R), ←units.smul_def, lie_subalgebra.mem_coe,
       mem_skew_adjoint_matrices_lie_subalgebra_unit_smul],
   refl,
 end
@@ -363,7 +363,7 @@ begin
     (matrix.reindex_alg_equiv _ (equiv.sum_assoc punit l l)) (matrix.transpose_reindex _ _)).trans,
   apply lie_equiv.of_eq,
   ext A,
-  rw [JB_transform, ← unit_of_invertible_val (2 : R), ←units.smul_def, lie_subalgebra.mem_coe,
+  rw [JB_transform, ← coe_unit_of_invertible (2 : R), ←units.smul_def, lie_subalgebra.mem_coe,
       lie_subalgebra.mem_coe, mem_skew_adjoint_matrices_lie_subalgebra_unit_smul],
   simpa [indefinite_diagonal_assoc],
 end

src/analysis/normed_space/units.lean

@@ -36,38 +36,34 @@ namespace units
 
 /-- In a complete normed ring, a perturbation of `1` by an element `t` of distance less than `1`
 from `1` is a unit.  Here we construct its `units` structure.  -/
+@[simps coe]
 def one_sub (t : R) (h : ∥t∥ < 1) : units R :=
 { val := 1 - t,
   inv := ∑' n : ℕ, t ^ n,
   val_inv := mul_neg_geom_series t h,
   inv_val := geom_series_mul_neg t h }
 
-@[simp] lemma one_sub_coe (t : R) (h : ∥t∥ < 1) : ↑(one_sub t h) = 1 - t := rfl
-
 /-- In a complete normed ring, a perturbation of a unit `x` by an element `t` of distance less than
 `∥x⁻¹∥⁻¹` from `x` is a unit.  Here we construct its `units` structure. -/
+@[simps coe]
 def add (x : units R) (t : R) (h : ∥t∥ < ∥(↑x⁻¹ : R)∥⁻¹) : units R :=
-x * (units.one_sub (-(↑x⁻¹ * t))
-begin
-  nontriviality R using [zero_lt_one],
-  have hpos : 0 < ∥(↑x⁻¹ : R)∥ := units.norm_pos x⁻¹,
-  calc ∥-(↑x⁻¹ * t)∥
-      = ∥↑x⁻¹ * t∥                    : by { rw norm_neg }
-  ... ≤ ∥(↑x⁻¹ : R)∥ * ∥t∥            : norm_mul_le ↑x⁻¹ _
-  ... < ∥(↑x⁻¹ : R)∥ * ∥(↑x⁻¹ : R)∥⁻¹ : by nlinarith only [h, hpos]
-  ... = 1                             : mul_inv_cancel (ne_of_gt hpos)
-end)
-
-@[simp] lemma add_coe (x : units R) (t : R) (h : ∥t∥ < ∥(↑x⁻¹ : R)∥⁻¹) :
-  ((x.add t h) : R) = x + t := by { unfold units.add, simp [mul_add] }
+units.copy  -- to make `coe_add` true definitionally, for convenience
+  (x * (units.one_sub (-(↑x⁻¹ * t)) begin
+      nontriviality R using [zero_lt_one],
+      have hpos : 0 < ∥(↑x⁻¹ : R)∥ := units.norm_pos x⁻¹,
+      calc ∥-(↑x⁻¹ * t)∥
+          = ∥↑x⁻¹ * t∥                    : by { rw norm_neg }
+      ... ≤ ∥(↑x⁻¹ : R)∥ * ∥t∥            : norm_mul_le ↑x⁻¹ _
+      ... < ∥(↑x⁻¹ : R)∥ * ∥(↑x⁻¹ : R)∥⁻¹ : by nlinarith only [h, hpos]
+      ... = 1                             : mul_inv_cancel (ne_of_gt hpos)
+    end))
+  (x + t) (by simp [mul_add]) _ rfl
 
 /-- In a complete normed ring, an element `y` of distance less than `∥x⁻¹∥⁻¹` from `x` is a unit.
 Here we construct its `units` structure. -/
+@[simps coe]
 def unit_of_nearby (x : units R) (y : R) (h : ∥y - x∥ < ∥(↑x⁻¹ : R)∥⁻¹) : units R :=
-x.add ((y : R) - x) h
-
-@[simp] lemma unit_of_nearby_coe (x : units R) (y : R) (h : ∥y - x∥ < ∥(↑x⁻¹ : R)∥⁻¹) :
-  ↑(x.unit_of_nearby y h) = y := by { unfold units.unit_of_nearby, simp }
+units.copy (x.add (y - x : R) h) y (by simp) _ rfl
 
 /-- The group of units of a complete normed ring is an open subset of the ring. -/
 protected lemma is_open : is_open {x : R | is_unit x} :=
@@ -78,7 +74,7 @@ begin
   refine ⟨∥(↑x⁻¹ : R)∥⁻¹, inv_pos.mpr (units.norm_pos x⁻¹), _⟩,
   intros y hy,
   rw [metric.mem_ball, dist_eq_norm] at hy,
-  exact ⟨x.unit_of_nearby y hy, unit_of_nearby_coe _ _ _⟩
+  exact (x.unit_of_nearby y hy).is_unit
 end
 
 protected lemma nhds (x : units R) : {x : R | is_unit x} ∈ 𝓝 (x : R) :=
@@ -91,7 +87,7 @@ open_locale classical big_operators
 open asymptotics filter metric finset ring
 
 lemma inverse_one_sub (t : R) (h : ∥t∥ < 1) : inverse (1 - t) = ↑(units.one_sub t h)⁻¹ :=
-by rw [← inverse_unit (units.one_sub t h), units.one_sub_coe]
+by rw [← inverse_unit (units.one_sub t h), units.coe_one_sub]
 
 /-- The formula `inverse (x + t) = inverse (1 + x⁻¹ * t) * x⁻¹` holds for `t` sufficiently small. -/
 lemma inverse_add (x : units R) :
@@ -111,7 +107,7 @@ begin
   have hright := inverse_one_sub (-↑x⁻¹ * t) ht',
   have hleft := inverse_unit (x.add t ht),
   simp only [← neg_mul_eq_neg_mul, sub_neg_eq_add] at hright,
-  simp only [units.add_coe] at hleft,
+  simp only [units.coe_add] at hleft,
   simp [hleft, hright, units.add]
 end
 
@@ -124,14 +120,14 @@ begin
   simp only [mem_ball, dist_zero_right] at ht,
   simp only [inverse_one_sub t ht, set.mem_set_of_eq],
   have h : 1 = ((range n).sum (λ i, t ^ i)) * (units.one_sub t ht) + t ^ n,
-  { simp only [units.one_sub_coe],
+  { simp only [units.coe_one_sub],
     rw [← geom_sum, geom_sum_mul_neg],
     simp },
   rw [← one_mul ↑(units.one_sub t ht)⁻¹, h, add_mul],
   congr,
   { rw [mul_assoc, (units.one_sub t ht).mul_inv],
     simp },
-  { simp only [units.one_sub_coe],
+  { simp only [units.coe_one_sub],
     rw [← add_mul, ← geom_sum, geom_sum_mul_neg],
     simp }
 end
@@ -246,9 +242,8 @@ begin
   convert inverse_add_norm_diff_nth_order x 2,
   ext t,
   simp only [range_succ, range_one, sum_insert, mem_singleton, sum_singleton, not_false_iff,
-    one_ne_zero, pow_zero, add_mul],
-  abel,
-  simp
+    one_ne_zero, pow_zero, add_mul, pow_one, one_mul, neg_mul_eq_neg_mul_symm,
+    sub_add_eq_sub_sub_swap, sub_neg_eq_add],
 end
 
 /-- The function `inverse` is continuous at each unit of `R`. -/