feat(algebra/group_with_zero): generalize some lemmas (#15985)

* replace `*_hom.map_inv` by a generic lemma `map_inv₀` assuming `[monoid_with_zero_hom_class]`;
* replace `*_hom.map_div` by a generic lemma `map_div₀` assuming `[monoid_with_zero_hom_class]`;
* replace `*_hom.map_zpow` by a generic lemma `map_zpow₀` assuming `[monoid_with_zero_hom_class]`;
* replace `*_hom.map_units_inv` by a generic lemma `map_units_inv` assuming `[monoid_hom_class]`, `[monoid]`, and `[division_monoid]`.

src/algebra/algebra/basic.lean

@@ -758,19 +758,6 @@ protected lemma map_sub (x y) : φ (x - y) = φ x - φ y := map_sub _ _ _
 
 end ring
 
-section division_ring
-
-variables [comm_semiring R] [division_ring A] [division_ring B]
-variables [algebra R A] [algebra R B] (φ : A →ₐ[R] B)
-
-@[simp] lemma map_inv (x) : φ (x⁻¹) = (φ x)⁻¹ :=
-φ.to_ring_hom.map_inv x
-
-@[simp] lemma map_div (x y) : φ (x / y) = φ x / φ y :=
-φ.to_ring_hom.map_div x y
-
-end division_ring
-
 end alg_hom
 
 @[simp] lemma rat.smul_one_eq_coe {A : Type*} [division_ring A] [algebra ℚ A] (m : ℚ) :
@@ -1220,19 +1207,6 @@ protected lemma map_sub (x y) : e (x - y) = e x - e y := map_sub e x y
 
 end ring
 
-section division_ring
-
-variables [comm_ring R] [division_ring A₁] [division_ring A₂]
-variables [algebra R A₁] [algebra R A₂] (e : A₁ ≃ₐ[R] A₂)
-
-@[simp] lemma map_inv (x) : e (x⁻¹) = (e x)⁻¹ :=
-e.to_alg_hom.map_inv x
-
-@[simp] lemma map_div (x y) : e (x / y) = e x / e y :=
-e.to_alg_hom.map_div x y
-
-end division_ring
-
 end alg_equiv
 
 namespace mul_semiring_action

src/algebra/field/basic.lean

@@ -361,24 +361,13 @@ namespace ring_hom
 section semiring
 variables [semiring α] [division_semiring β]
 
-@[simp] lemma map_units_inv (f : α →+* β) (u : αˣ) : f ↑u⁻¹ = (f ↑u)⁻¹ :=
-(f : α →* β).map_units_inv u
-
 variables [nontrivial α] (f : β →+* α) {a : β}
 
-@[simp] lemma map_eq_zero : f a = 0 ↔ a = 0 := f.to_monoid_with_zero_hom.map_eq_zero
-lemma map_ne_zero : f a ≠ 0 ↔ a ≠ 0 := f.to_monoid_with_zero_hom.map_ne_zero
+@[simp] lemma map_eq_zero : f a = 0 ↔ a = 0 := monoid_with_zero_hom.map_eq_zero f
+lemma map_ne_zero : f a ≠ 0 ↔ a ≠ 0 := monoid_with_zero_hom.map_ne_zero f
 
 end semiring
 
-section division_semiring
-variables [division_semiring α] [division_semiring β] (f : α →+* β) (a b : α)
-
-lemma map_inv : f a⁻¹ = (f a)⁻¹ := f.to_monoid_with_zero_hom.map_inv _
-lemma map_div : f (a / b) = f a / f b := f.to_monoid_with_zero_hom.map_div _ _
-
-end division_semiring
-
 protected lemma injective [division_ring α] [semiring β] [nontrivial β] (f : α →+* β) :
   injective f :=
 (injective_iff_map_eq_zero f).2 $ λ x, f.map_eq_zero.1

src/algebra/field_power.lean

@@ -21,17 +21,11 @@ variables {α β : Type*}
 section division_ring
 variables [division_ring α] [division_ring β]
 
-@[simp] lemma ring_hom.map_zpow (f : α →+* β) : ∀ (a : α) (n : ℤ), f (a ^ n) = f a ^ n :=
-f.to_monoid_with_zero_hom.map_zpow
-
-@[simp] lemma ring_equiv.map_zpow (f : α ≃+* β) : ∀ (a : α) (n : ℤ), f (a ^ n) = f a ^ n :=
-f.to_ring_hom.map_zpow
-
 @[simp] lemma zpow_bit1_neg (x : α) (n : ℤ) : (-x) ^ bit1 n = - x ^ bit1 n :=
 by rw [zpow_bit1', zpow_bit1', neg_mul_neg, neg_mul_eq_mul_neg]
 
 @[simp, norm_cast] lemma rat.cast_zpow [char_zero α] (q : ℚ) (n : ℤ) : ((q ^ n : ℚ) : α) = q ^ n :=
-(rat.cast_hom α).map_zpow q n
+map_zpow₀ (rat.cast_hom α) q n
 
 end division_ring
 

src/algebra/group_ring_action.lean

@@ -103,7 +103,7 @@ attribute [simp] smul_one smul_mul' smul_zero smul_add
 /-- Note that `smul_inv'` refers to the group case, and `smul_inv` has an additional inverse
 on `x`. -/
 @[simp] lemma smul_inv'' [mul_semiring_action M F] (x : M) (m : F) : x • m⁻¹ = (x • m)⁻¹ :=
-(mul_semiring_action.to_ring_hom M F x).map_inv _
+map_inv₀ (mul_semiring_action.to_ring_hom M F x) _
 
 end simp_lemmas
 

src/algebra/group_with_zero/basic.lean

@@ -39,7 +39,7 @@ set_option old_structure_cmd true
 open_locale classical
 open function
 
-variables {M₀ G₀ M₀' G₀' : Type*}
+variables {M₀ G₀ M₀' G₀' F : Type*}
 
 section
 
@@ -973,38 +973,34 @@ end commute
 namespace monoid_with_zero_hom
 
 variables [group_with_zero G₀] [group_with_zero G₀'] [monoid_with_zero M₀] [nontrivial M₀]
-
-section monoid_with_zero
-
-variables (f : G₀ →*₀ M₀) {a : G₀}
+  [monoid_with_zero_hom_class F G₀ M₀] (f : F) {a : G₀}
+include M₀
 
 lemma map_ne_zero : f a ≠ 0 ↔ a ≠ 0 :=
-⟨λ hfa ha, hfa $ ha.symm ▸ f.map_zero, λ ha, ((is_unit.mk0 a ha).map f.to_monoid_hom).ne_zero⟩
+⟨λ hfa ha, hfa $ ha.symm ▸ map_zero f, λ ha, ((is_unit.mk0 a ha).map f).ne_zero⟩
 
-@[simp] lemma map_eq_zero : f a = 0 ↔ a = 0 :=
-not_iff_not.1 f.map_ne_zero
+@[simp] lemma map_eq_zero : f a = 0 ↔ a = 0 := not_iff_not.1 (map_ne_zero f)
 
-end monoid_with_zero
+end monoid_with_zero_hom
 
 section group_with_zero
 
-variables (f : G₀ →*₀ G₀') (a b : G₀)
+variables [group_with_zero G₀] [group_with_zero G₀'] [monoid_with_zero_hom_class F G₀ G₀']
+  (f : F) (a b : G₀)
+include G₀'
 
 /-- A monoid homomorphism between groups with zeros sending `0` to `0` sends `a⁻¹` to `(f a)⁻¹`. -/
-@[simp] lemma map_inv : f a⁻¹ = (f a)⁻¹ :=
+@[simp] lemma map_inv₀ : f a⁻¹ = (f a)⁻¹ :=
 begin
   by_cases h : a = 0, by simp [h],
   apply eq_inv_of_mul_eq_one_left,
-  rw [← f.map_mul, inv_mul_cancel h, f.map_one]
+  rw [← map_mul, inv_mul_cancel h, map_one]
 end
 
-@[simp] lemma map_div : f (a / b) = f a / f b :=
-by simpa only [div_eq_mul_inv] using ((f.map_mul _ _).trans $ _root_.congr_arg _ $ f.map_inv b)
+@[simp] lemma map_div₀ : f (a / b) = f a / f b := map_div' f (map_inv₀ f) a b
 
 end group_with_zero
 
-end monoid_with_zero_hom
-
 /-- We define the inverse as a `monoid_with_zero_hom` by extending the inverse map by zero
 on non-units. -/
 noncomputable
@@ -1028,14 +1024,6 @@ def inv_monoid_with_zero_hom {G₀ : Type*} [comm_group_with_zero G₀] : G₀ 
 { map_zero' := inv_zero,
   ..inv_monoid_hom }
 
-@[simp] lemma monoid_hom.map_units_inv {M G₀ : Type*} [monoid M] [group_with_zero G₀]
-  (f : M →* G₀) (u : Mˣ) : f ↑u⁻¹ = (f u)⁻¹ :=
-by rw [← units.coe_map, ← units.coe_map, ← units.coe_inv, monoid_hom.map_inv]
-
-@[simp] lemma monoid_with_zero_hom.map_units_inv {M G₀ : Type*} [monoid_with_zero M]
-  [group_with_zero G₀] (f : M →*₀ G₀) (u : Mˣ) : f ↑u⁻¹ = (f u)⁻¹ :=
-f.to_monoid_hom.map_units_inv u
-
 section noncomputable_defs
 
 variables {M : Type*} [nontrivial M]

src/algebra/group_with_zero/power.lean

@@ -164,11 +164,7 @@ end
 
 /-- If a monoid homomorphism `f` between two `group_with_zero`s maps `0` to `0`, then it maps `x^n`,
 `n : ℤ`, to `(f x)^n`. -/
-lemma monoid_with_zero_hom.map_zpow {G₀ G₀' : Type*} [group_with_zero G₀] [group_with_zero G₀']
-  (f : G₀ →*₀ G₀') (x : G₀) :
-  ∀ n : ℤ, f (x ^ n) = f x ^ n
-| (n : ℕ) := by { rw [zpow_coe_nat, zpow_coe_nat], exact f.to_monoid_hom.map_pow x n }
-| -[1+n] := begin
-    rw [zpow_neg_succ_of_nat, zpow_neg_succ_of_nat],
-    exact ((f.map_inv _).trans $ congr_arg _ $ f.to_monoid_hom.map_pow x _)
-  end
+@[simp] lemma map_zpow₀ {F G₀ G₀' : Type*} [group_with_zero G₀] [group_with_zero G₀']
+  [monoid_with_zero_hom_class F G₀ G₀'] (f : F) (x : G₀) (n : ℤ) :
+  f (x ^ n) = f x ^ n :=
+map_zpow' f (map_inv₀ f) x n

src/algebra/hom/units.lean

@@ -79,6 +79,11 @@ variables [division_monoid α]
 @[field_simps] lemma _root_.divp_eq_div (a : α) (u : αˣ) : a /ₚ u = a / u :=
 by rw [div_eq_mul_inv, divp, u.coe_inv]
 
+@[simp, to_additive]
+lemma _root_.map_units_inv {F : Type*} [monoid_hom_class F M α] (f : F) (u : units M) :
+  f ↑u⁻¹ = (f u)⁻¹ :=
+((f : M →* α).comp (units.coe_hom M)).map_inv u
+
 end division_monoid
 
 /-- If a map `g : M → Nˣ` agrees with a homomorphism `f : M →* N`, then

src/algebra/order/absolute_value.lean

@@ -141,22 +141,6 @@ end ring
 
 end linear_ordered_comm_ring
 
-section linear_ordered_field
-
-section field
-
-variables {R S : Type*} [division_ring R] [linear_ordered_field S] (abv : absolute_value R S)
-
-@[simp] protected theorem map_inv (a : R) : abv a⁻¹ = (abv a)⁻¹ :=
-abv.to_monoid_with_zero_hom.map_inv a
-
-@[simp] protected theorem map_div (a b : R) : abv (a / b) = abv a / abv b :=
-abv.to_monoid_with_zero_hom.map_div a b
-
-end field
-
-end linear_ordered_field
-
 end absolute_value
 
 section is_absolute_value
@@ -269,11 +253,8 @@ end ring
 section field
 variables {R : Type*} [division_ring R] (abv : R → S) [is_absolute_value abv]
 
-theorem abv_inv (a : R) : abv a⁻¹ = (abv a)⁻¹ :=
-(abv_hom abv).map_inv a
-
-theorem abv_div (a b : R) : abv (a / b) = abv a / abv b :=
-(abv_hom abv).map_div a b
+theorem abv_inv (a : R) : abv a⁻¹ = (abv a)⁻¹ := map_inv₀ (abv_hom abv) a
+theorem abv_div (a b : R) : abv (a / b) = abv a / abv b := map_div₀ (abv_hom abv) a b
 
 end field
 

src/algebra/order/field.lean

@@ -822,8 +822,8 @@ eq.symm $ antitone.map_max $ λ x y, div_le_div_of_nonpos_of_le hc
 lemma max_div_div_right_of_nonpos (hc : c ≤ 0) (a b : α) : max (a / c) (b / c) = (min a b) / c :=
 eq.symm $ antitone.map_min $ λ x y, div_le_div_of_nonpos_of_le hc
 
-lemma abs_inv (a : α) : |a⁻¹| = (|a|)⁻¹ := (abs_hom : α →*₀ α).map_inv a
-lemma abs_div (a b : α) : |a / b| = |a| / |b| := (abs_hom : α →*₀ α).map_div a b
+lemma abs_inv (a : α) : |a⁻¹| = (|a|)⁻¹ := map_inv₀ (abs_hom : α →*₀ α) a
+lemma abs_div (a b : α) : |a / b| = |a| / |b| := map_div₀ (abs_hom : α →*₀ α) a b
 lemma abs_one_div (a : α) : |1 / a| = 1 / |a| := by rw [abs_div, abs_one]
 
 lemma pow_minus_two_nonneg : 0 ≤ a^(-2 : ℤ) :=

src/algebra/quaternion.lean

@@ -593,11 +593,8 @@ instance : division_ring ℍ[R] :=
   .. quaternion.nontrivial,
   .. quaternion.ring }
 
-@[simp] lemma norm_sq_inv : norm_sq a⁻¹ = (norm_sq a)⁻¹ :=
-monoid_with_zero_hom.map_inv norm_sq _
-
-@[simp] lemma norm_sq_div : norm_sq (a / b) = norm_sq a / norm_sq b :=
-monoid_with_zero_hom.map_div norm_sq a b
+@[simp] lemma norm_sq_inv : norm_sq a⁻¹ = (norm_sq a)⁻¹ := map_inv₀ norm_sq _
+@[simp] lemma norm_sq_div : norm_sq (a / b) = norm_sq a / norm_sq b := map_div₀ norm_sq a b
 
 end field
 

src/algebra/ring/equiv.lean

@@ -559,17 +559,6 @@ map_sum g f s
 
 end big_operators
 
-section division_ring
-
-variables {K K' : Type*} [division_ring K] [division_ring K']
-  (g : K ≃+* K') (x y : K)
-
-lemma map_inv : g x⁻¹ = (g x)⁻¹ := g.to_ring_hom.map_inv x
-
-lemma map_div : g (x / y) = g x / g y := g.to_ring_hom.map_div x y
-
-end division_ring
-
 section group_power
 
 variables [semiring R] [semiring S]

src/algebra/star/basic.lean

@@ -148,15 +148,15 @@ op_injective $
 /-- When multiplication is commutative, `star` preserves division. -/
 @[simp] lemma star_div [comm_group R] [star_semigroup R] (x y : R) :
   star (x / y) = star x / star y :=
-(star_mul_aut : R ≃* R).to_monoid_hom.map_div _ _
+map_div (star_mul_aut : R ≃* R) _ _
 
 section
 open_locale big_operators
 
 @[simp] lemma star_prod [comm_monoid R] [star_semigroup R] {α : Type*}
   (s : finset α) (f : α → R):
   star (∏ x in s, f x) = ∏ x in s, star (f x) :=
-(star_mul_aut : R ≃* R).map_prod _ _
+map_prod (star_mul_aut : R ≃* R) _ _
 
 end
 
@@ -300,17 +300,15 @@ alias star_ring_end_self_apply ← complex.conj_conj
 alias star_ring_end_self_apply ← is_R_or_C.conj_conj
 
 @[simp] lemma star_inv' [division_ring R] [star_ring R] (x : R) : star (x⁻¹) = (star x)⁻¹ :=
-op_injective $
-  ((star_ring_equiv : R ≃+* Rᵐᵒᵖ).to_ring_hom.map_inv x).trans (op_inv (star x)).symm
+op_injective $ (map_inv₀ (star_ring_equiv : R ≃+* Rᵐᵒᵖ) x).trans (op_inv (star x)).symm
 
 @[simp] lemma star_zpow₀ [division_ring R] [star_ring R] (x : R) (z : ℤ) :
   star (x ^ z) = star x ^ z :=
-op_injective $
-  ((star_ring_equiv : R ≃+* Rᵐᵒᵖ).to_ring_hom.map_zpow x z).trans (op_zpow (star x) z).symm
+op_injective $ (map_zpow₀ (star_ring_equiv : R ≃+* Rᵐᵒᵖ) x z).trans (op_zpow (star x) z).symm
 
 /-- When multiplication is commutative, `star` preserves division. -/
 @[simp] lemma star_div' [field R] [star_ring R] (x y : R) : star (x / y) = star x / star y :=
-(star_ring_end R).map_div _ _
+map_div₀ (star_ring_end R) _ _
 
 @[simp] lemma star_bit0 [add_monoid R] [star_add_monoid R] (r : R) :
   star (bit0 r) = bit0 (star r) :=

src/analysis/box_integral/box/basic.lean

@@ -374,7 +374,7 @@ lemma distortion_eq_of_sub_eq_div {I J : box ι} {r : ℝ}
   (h : ∀ i, I.upper i - I.lower i = (J.upper i - J.lower i) / r) :
   distortion I = distortion J :=
 begin
-  simp only [distortion, nndist_pi_def, real.nndist_eq', h, real.nnabs.map_div],
+  simp only [distortion, nndist_pi_def, real.nndist_eq', h, map_div₀],
   congr' 1 with i,
   have : 0 < r,
   { by_contra hr,

src/analysis/inner_product_space/basic.lean

@@ -275,7 +275,7 @@ begin
       ... = re ⟪x, x⟫ - re (T† * ⟪y, x⟫) - re (T * ⟪x, y⟫) + re (T * T† * ⟪y, y⟫)
                   : by simp only [inner_smul_left, inner_smul_right, mul_assoc]
       ... = re ⟪x, x⟫ - re (⟪x, y⟫ / ⟪y, y⟫ * ⟪y, x⟫)
-                  : by field_simp [-mul_re, inner_conj_sym, hT, ring_hom.map_div, h₁, h₃]
+                  : by field_simp [-mul_re, inner_conj_sym, hT, map_div₀, h₁, h₃]
       ... = re ⟪x, x⟫ - re (⟪x, y⟫ * ⟪y, x⟫ / ⟪y, y⟫)
                   : by rw ←mul_div_right_comm
       ... = re ⟪x, x⟫ - re (⟪x, y⟫ * ⟪y, x⟫ / re ⟪y, y⟫)
@@ -647,7 +647,7 @@ begin
       ... = re ⟪x, x⟫ - re (T† * ⟪y, x⟫) - re (T * ⟪x, y⟫) + re (T * T† * ⟪y, y⟫)
                   : by simp only [inner_smul_left, inner_smul_right, mul_assoc]
       ... = re ⟪x, x⟫ - re (⟪x, y⟫ / ⟪y, y⟫ * ⟪y, x⟫)
-                  : by field_simp [-mul_re, hT, ring_hom.map_div, h₁, h₃, inner_conj_sym]
+                  : by field_simp [-mul_re, hT, map_div₀, h₁, h₃, inner_conj_sym]
       ... = re ⟪x, x⟫ - re (⟪x, y⟫ * ⟪y, x⟫ / ⟪y, y⟫)
                   : by rw ←mul_div_right_comm
       ... = re ⟪x, x⟫ - re (⟪x, y⟫ * ⟪y, x⟫ / re ⟪y, y⟫)

src/analysis/inner_product_space/dual.lean

@@ -125,7 +125,7 @@ begin
       exact sub_eq_zero.mp (eq.symm h₃) },
     have h₄ := calc
       ⟪((ℓ z)† / ⟪z, z⟫) • z, x⟫ = (ℓ z) / ⟪z, z⟫ * ⟪z, x⟫
-            : by simp [inner_smul_left, ring_hom.map_div, conj_conj]
+            : by simp [inner_smul_left, conj_conj]
                             ... = (ℓ z) * ⟪z, x⟫ / ⟪z, z⟫
             : by rw [←div_mul_eq_mul_div]
                             ... = (ℓ x) * ⟪z, z⟫ / ⟪z, z⟫

src/analysis/inner_product_space/projection.lean

@@ -541,7 +541,7 @@ begin
   { intros x hx,
     obtain ⟨c, rfl⟩ := submodule.mem_span_singleton.mp hx,
     have hv : ↑∥v∥ ^ 2 = ⟪v, v⟫ := by { norm_cast, simp [norm_sq_eq_inner] },
-    simp [inner_sub_left, inner_smul_left, inner_smul_right, ring_equiv.map_div, mul_comm, hv,
+    simp [inner_sub_left, inner_smul_left, inner_smul_right, map_div₀, mul_comm, hv,
       inner_product_space.conj_sym, hv] }
 end
 

src/analysis/normed/field/basic.lean

@@ -433,19 +433,19 @@ protected lemma list.norm_prod (l : list α) : ∥l.prod∥ = (l.map norm).prod
 protected lemma list.nnnorm_prod (l : list α) : ∥l.prod∥₊ = (l.map nnnorm).prod :=
 (nnnorm_hom.to_monoid_hom : α →* ℝ≥0).map_list_prod _
 
-@[simp] lemma norm_div (a b : α) : ∥a / b∥ = ∥a∥ / ∥b∥ := (norm_hom : α →*₀ ℝ).map_div a b
+@[simp] lemma norm_div (a b : α) : ∥a / b∥ = ∥a∥ / ∥b∥ := map_div₀ (norm_hom : α →*₀ ℝ) a b
 
-@[simp] lemma nnnorm_div (a b : α) : ∥a / b∥₊ = ∥a∥₊ / ∥b∥₊ := (nnnorm_hom : α →*₀ ℝ≥0).map_div a b
+@[simp] lemma nnnorm_div (a b : α) : ∥a / b∥₊ = ∥a∥₊ / ∥b∥₊ := map_div₀ (nnnorm_hom : α →*₀ ℝ≥0) a b
 
-@[simp] lemma norm_inv (a : α) : ∥a⁻¹∥ = ∥a∥⁻¹ := (norm_hom : α →*₀ ℝ).map_inv a
+@[simp] lemma norm_inv (a : α) : ∥a⁻¹∥ = ∥a∥⁻¹ := map_inv₀ (norm_hom : α →*₀ ℝ) a
 
 @[simp] lemma nnnorm_inv (a : α) : ∥a⁻¹∥₊ = ∥a∥₊⁻¹ :=
 nnreal.eq $ by simp
 
-@[simp] lemma norm_zpow : ∀ (a : α) (n : ℤ), ∥a^n∥ = ∥a∥^n := (norm_hom : α →*₀ ℝ).map_zpow
+@[simp] lemma norm_zpow : ∀ (a : α) (n : ℤ), ∥a^n∥ = ∥a∥^n := map_zpow₀ (norm_hom : α →*₀ ℝ)
 
 @[simp] lemma nnnorm_zpow : ∀ (a : α) (n : ℤ), ∥a ^ n∥₊ = ∥a∥₊ ^ n :=
-(nnnorm_hom : α →*₀ ℝ≥0).map_zpow
+map_zpow₀ (nnnorm_hom : α →*₀ ℝ≥0)
 
 /-- Multiplication on the left by a nonzero element of a normed division ring tends to infinity at
 infinity. TODO: use `bornology.cobounded` instead of `filter.comap has_norm.norm filter.at_top`. -/

src/analysis/normed_space/compact_operator.lean

@@ -345,7 +345,7 @@ begin
     rwa [mem_map, preimage_smul_setₛₗ _ _ _ f this, set_smul_mem_nhds_zero_iff (inv_ne_zero hcnz)],
     apply_instance },
   -- Since `σ₁₂ c⁻¹` = `(σ₁₂ c)⁻¹`, we have to prove that `K ⊆ σ₁₂ c • U`.
-  rw [σ₁₂.map_inv, ← subset_set_smul_iff₀ (σ₁₂.map_ne_zero.mpr hcnz)],
+  rw [map_inv₀, ← subset_set_smul_iff₀ (σ₁₂.map_ne_zero.mpr hcnz)],
   -- But `σ₁₂` is isometric, so `∥σ₁₂ c∥ = ∥c∥ > r`, which concludes the argument since
   -- `∀ a : 𝕜₂, r ≤ ∥a∥ → K ⊆ a • U`.
   refine hrU (σ₁₂ c) _,