diff --git a/library/theories/group_theory/basic.lean b/library/theories/group_theory/basic.lean
index b1bfe3d16..abade3c0a 100644
--- a/library/theories/group_theory/basic.lean
+++ b/library/theories/group_theory/basic.lean
@@ -11,7 +11,7 @@ For notation a^b and S^a, open the namespace "conj_notation".
 
 TODO: homomorphisms on sets should be refactored and moved to algebra.
 -/
-import data.set algebra.homomorphism theories.topology.basic theories.move
+import data.set algebra.homomorphism theories.move
 open eq.ops set function
 
 namespace group_theory
diff --git a/library/theories/group_theory/quotient.lean b/library/theories/group_theory/quotient.lean
index f265af55a..ca11ea196 100644
--- a/library/theories/group_theory/quotient.lean
+++ b/library/theories/group_theory/quotient.lean
@@ -140,12 +140,12 @@ take y, quot.induction_on y (λ a, exists.intro a rfl)
 variable {H}
 
 proposition quotient_induction {P : quotient H → Prop} (h : ∀ a, P (a '* H)) : ∀ a, P a :=
-surjective_induction (surjective_qproj H) h
+quot.ind h
 
 proposition quotient_induction₂ {P : quotient H → quotient H → Prop}
     (h : ∀ a₁ a₂, P (a₁ '* H) (a₂ '* H)) :
   ∀ a₁ a₂, P a₁ a₂ :=
-surjective_induction₂ (surjective_qproj H) h
+quot.ind₂ h
 
 variable (H)