feat(algebra/group/basic|topology/connected): add two lemmas (#13345)

* from the sphere eversion project

src/algebra/group/basic.lean

@@ -481,7 +481,9 @@ end
 end group
 
 section comm_group
-variables {G : Type u} [comm_group G]
+variables {G : Type u} [comm_group G] {a b c d : G}
+
+local attribute [simp] mul_assoc mul_comm mul_left_comm div_eq_mul_inv
 
 @[to_additive neg_add]
 lemma mul_inv (a b : G) : (a * b)⁻¹ = a⁻¹ * b⁻¹ :=
@@ -492,13 +494,12 @@ lemma div_eq_of_eq_mul' {a b c : G} (h : a = b * c) : a / b = c :=
 by rw [h, div_eq_mul_inv, mul_comm, inv_mul_cancel_left]
 
 @[to_additive]
-lemma div_mul_div_comm (a b c d : G) : a / b * (c / d) = a * c / (b * d) :=
-by rw [div_eq_mul_inv, div_eq_mul_inv, div_eq_mul_inv, mul_inv_rev, mul_assoc, mul_assoc,
-  mul_left_cancel_iff, mul_comm, mul_assoc]
-
-variables {a b c d : G}
+lemma mul_div_left_comm {x y z : G} : x * (y / z) = y * (x / z) :=
+by simp_rw [div_eq_mul_inv, mul_left_comm]
 
-local attribute [simp] mul_assoc mul_comm mul_left_comm div_eq_mul_inv
+@[to_additive]
+lemma div_mul_div_comm (a b c d : G) : a / b * (c / d) = a * c / (b * d) :=
+by simp
 
 @[to_additive]
 lemma div_mul_eq_div_div (a b c : G) : a / (b * c) = a / b / c :=

src/topology/connected.lean

@@ -640,6 +640,9 @@ class connected_space (α : Type u) [topological_space α] extends preconnected_
 
 attribute [instance, priority 50] connected_space.to_nonempty -- see Note [lower instance priority]
 
+lemma is_connected_univ [connected_space α] : is_connected (univ : set α) :=
+⟨univ_nonempty, is_preconnected_univ⟩
+
 lemma is_preconnected_range [topological_space β] [preconnected_space α] {f : α → β}
   (h : continuous f) : is_preconnected (range f) :=
 @image_univ _ _ f ▸ is_preconnected_univ.image _ h.continuous_on