From c0cd72fc8da07eeed67ee947188119d23af4a6f0 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 16 Jul 2015 22:50:02 -0400
Subject: [PATCH] chore(library/theories/group_theory): remove dangling
 "check"s

---
 library/theories/group_theory/hom.lean  | 2 --
 library/theories/group_theory/perm.lean | 1 -
 2 files changed, 3 deletions(-)

diff --git a/library/theories/group_theory/hom.lean b/library/theories/group_theory/hom.lean
index 1b13cc000..e13ae3f9f 100644
--- a/library/theories/group_theory/hom.lean
+++ b/library/theories/group_theory/hom.lean
@@ -36,7 +36,6 @@ definition is_hom (f : A → B) [h : is_hom_class f] : homomorphic f :=
            @is_hom_class.is_hom A B s1 s2 f h
 
 definition ker (f : A → B) [h : is_hom_class f] : set A := {a : A | f a = 1}
-check @ker
 
 definition isomorphic (f : A → B) := injective f ∧ homomorphic f
 structure is_iso_class [class] (f : A → B) extends is_hom_class f : Type :=
@@ -174,7 +173,6 @@ lemma ker_map_is_hom : homomorphic (ker_natural_map : coset_of (ker f) → B) :=
   take aK bK,
       quot.ind (λ a, quot.ind (λ b, ker_coset_hom a b) bK) aK
 
-check @subg_in_lcoset_same_lcoset
 lemma ker_coset_inj (a b : A) : (ker_natural_map ⟦a⟧ = ker_natural_map ⟦b⟧) → ⟦a⟧ = ⟦b⟧ :=
       assume Pfeq : f a = f b,
       assert Painb : a ∈ b ∘> ker f, from calc
diff --git a/library/theories/group_theory/perm.lean b/library/theories/group_theory/perm.lean
index f683d0aa6..b415bd686 100644
--- a/library/theories/group_theory/perm.lean
+++ b/library/theories/group_theory/perm.lean
@@ -42,7 +42,6 @@ end perm
 structure perm (A : Type) [h : fintype A] : Type :=
   (f : A → A) (inj : injective f)
 local attribute perm.f [coercion]
-check perm.mk
 
 section perm
 variable {A : Type}