refactor(algebra/group): clean up PR commit

algebra/big_operators.lean

@@ -310,31 +310,15 @@ section group
 open list
 variables [group α] [group β]
 
-lemma mph_prod (f : α → β) (hom : is_group_hom f) (l : list α) :
-f (prod l) = prod (map f l) :=
-begin
-  induction l,
-  case nil :
-  { simp[group_hom.one hom] },
-  case cons : hd tl IH
-  { simp,
-    rw hom,
-    simp[IH] }
-end
+theorem is_group_hom.prod {f : α → β} (H : is_group_hom f) (l : list α) :
+  f (prod l) = prod (map f l) :=
+by induction l; simp [*, H.mul, H.one]
 
-lemma anti_mph_prod (f : α → β) (anti_mph : is_group_anti_hom f) (l : list α) :
-f (prod l) = prod (map f (reverse l)) :=
-begin
-  induction l,
-  case nil :
-  { simp [group_anti_hom.one anti_mph] },
-  case cons : hd tl IH
-  { simp,
-    rw anti_mph,
-    simp[IH] }
-end
+theorem is_group_anti_hom.prod {f : α → β} (H : is_group_anti_hom f) (l : list α) :
+  f (prod l) = prod (map f (reverse l)) :=
+by induction l; simp [*, H.mul, H.one]
+
+theorem inv_prod : ∀ l : list α, (prod l)⁻¹ = prod (map (λ x, x⁻¹) (reverse l)) :=
+inv_is_group_anti_hom.prod
 
--- Following lemma could also be proved directly by "by induction l; simp *"
-lemma inv_prod (l : list α) : (prod l)⁻¹ = prod (map (λ x, x⁻¹) (reverse l)) := 
-anti_mph_prod (λ x, x⁻¹) group_anti_hom.inv_is_group_anti_hom l
 end group

algebra/group.lean

@@ -323,49 +323,41 @@ by rw [add_comm]; exact ⟨le_add_of_sub_left_le, sub_left_le_of_le_add⟩
 
 end ordered_comm_group
 
+variables {β : Type*} [group α] [group β] {a b : α}
 
-variables { β : Type*} [group α] [group β] {a b : α}
-
-@[simp]
 def is_group_hom (f : α → β) : Prop :=
-∀ a b : α, f(a*b) = f(a)*f(b)
+∀ a b : α, f (a * b) = f a * f b
+
+namespace is_group_hom
+variables {f : α → β} (H : is_group_hom f)
+include H
+
+theorem mul : ∀ a b : α, f (a * b) = f a * f b := H
 
-namespace group_hom
-@[simp]
-lemma one { f : α → β } (H : is_group_hom f) : f 1 = 1 :=
-mul_self_iff_eq_one.1 (eq.symm (
-  calc f 1 = f (1*1)     : by simp
-       ... = (f 1)*(f 1) : by rw[H 1 1]))
+theorem one : f 1 = 1 :=
+mul_self_iff_eq_one.1 $ by simp [(H 1 1).symm]
 
-@[simp]
-lemma inv { f : α → β } (H : is_group_hom f) : (f a)⁻¹ = f (a⁻¹) :=
-inv_eq_of_mul_eq_one (
-  calc (f a) * (f a⁻¹) = f (a * a⁻¹) : by rw[H a a⁻¹]
-                  ...  = f 1 : by simp
-                  ...  = 1   : by rw[one H])
+theorem inv (a : α) : (f a)⁻¹ = f a⁻¹ :=
+inv_eq_of_mul_eq_one $ by simp [(H a a⁻¹).symm, one H]
 
-end group_hom
+end is_group_hom
 
-@[simp]
 def is_group_anti_hom (f : α → β) : Prop :=
-∀ a b : α, f(a*b) = f(b)*f(a)
+∀ a b : α, f (a * b) = f b * f a
 
-namespace group_anti_hom
-@[simp]
-lemma one { f : α → β } (H : is_group_anti_hom f) : f 1 = 1 :=
-mul_self_iff_eq_one.1 (eq.symm (
-  calc f 1 = f (1*1)     : by simp
-       ... = (f 1)*(f 1) : by rw[H 1 1]))
+namespace is_group_anti_hom
+variables {f : α → β} (H : is_group_anti_hom f)
+include H
 
-@[simp]
-lemma inv { f : α → β } (H : is_group_anti_hom f) : (f a)⁻¹ = f (a⁻¹) :=
-inv_eq_of_mul_eq_one (
-  calc (f a) * (f a⁻¹) = f (a⁻¹ * a) : by rw[H a⁻¹ a]
-                  ...  = f 1 : by simp
-                  ...  = 1   : by rw[one H])
+theorem mul : ∀ a b : α, f (a * b) = f b * f a := H
 
+theorem one : f 1 = 1 :=
+mul_self_iff_eq_one.1 $ by simp [(H 1 1).symm]
 
-lemma inv_is_group_anti_hom : is_group_anti_hom (λ x : α, x⁻¹) :=
-mul_inv_rev
+theorem inv (a : α) : (f a)⁻¹ = f a⁻¹ :=
+inv_eq_of_mul_eq_one $ by simp [(H a⁻¹ a).symm, one H]
+
+end is_group_anti_hom
 
-end group_anti_hom
+theorem inv_is_group_anti_hom : is_group_anti_hom (λ x : α, x⁻¹) :=
+mul_inv_rev