fix(algebra/hom/units): better defeq in is_unit.lift_right (#13508)

… and fix a timeout introduced by this change and remove some extraneous parentheses there.

src/algebra/hom/units.lean

@@ -109,7 +109,7 @@ to `f : M →* Nˣ`. See also `units.lift_right` for a computable version. -/
 lifted to `f : M →+ add_units N`. See also `add_units.lift_right` for a computable version."]
 noncomputable def is_unit.lift_right [monoid M] [monoid N] (f : M →* N)
   (hf : ∀ x, is_unit (f x)) : M →* Nˣ :=
-units.lift_right f (λ x, classical.some (hf x)) $ λ x, classical.some_spec (hf x)
+units.lift_right f (λ x, (hf x).unit) $ λ x, rfl
 
 @[to_additive] lemma is_unit.coe_lift_right [monoid M] [monoid N] (f : M →* N)
   (hf : ∀ x, is_unit (f x)) (x) :
@@ -118,10 +118,10 @@ units.coe_lift_right _ x
 
 @[simp, to_additive] lemma is_unit.mul_lift_right_inv [monoid M] [monoid N] (f : M →* N)
   (h : ∀ x, is_unit (f x)) (x) : f x * ↑(is_unit.lift_right f h x)⁻¹ = 1 :=
-units.mul_lift_right_inv (λ y, classical.some_spec $ h y) x
+units.mul_lift_right_inv (λ y, rfl) x
 
 @[simp, to_additive] lemma is_unit.lift_right_inv_mul [monoid M] [monoid N] (f : M →* N)
   (h : ∀ x, is_unit (f x)) (x) : ↑(is_unit.lift_right f h x)⁻¹ * f x = 1 :=
-units.lift_right_inv_mul (λ y, classical.some_spec $ h y) x
+units.lift_right_inv_mul (λ y, rfl) x
 
 end is_unit

src/algebraic_geometry/structure_sheaf.lean

@@ -857,9 +857,10 @@ instance to_basic_open_epi (r : R) : epi (to_open R (basic_open r)) :=
   swap 5, exact is_localization.to_basic_open R r, exact h }⟩
 
 @[elementwise] lemma to_global_factors : to_open R ⊤ =
-  (CommRing.of_hom (algebra_map R (localization.away (1 : R)))) ≫ (to_basic_open R (1 : R)) ≫
+  CommRing.of_hom (algebra_map R (localization.away (1 : R))) ≫ to_basic_open R (1 : R) ≫
   (structure_sheaf R).1.map (eq_to_hom (basic_open_one.symm)).op :=
 begin
+  rw ← category.assoc,
   change to_open R ⊤ = (to_basic_open R 1).comp _ ≫ _,
   unfold CommRing.of_hom,
   rw [localization_to_basic_open R, to_open_res],