chore(*): fix various issues reported by sanity_check_mathlib (#1469)

* chore(*): fix various issues reported by `sanity_check_mathlib`

* Drop a misleading comment, fix the proof

Author: urkud

src/algebra/direct_limit.lean

@@ -195,7 +195,7 @@ namespace direct_limit
 variables (f : Π i j, i ≤ j → G i → G j)
 variables [Π i j hij, is_add_group_hom (f i j hij)] [directed_system G f]
 
-def directed_system : module.directed_system G (λ i j hij, is_add_group_hom.to_linear_map $ f i j hij) :=
+lemma directed_system : module.directed_system G (λ i j hij, is_add_group_hom.to_linear_map $ f i j hij) :=
 ⟨directed_system.map_self f, directed_system.map_map f⟩
 
 local attribute [instance] directed_system

src/algebra/field.lean

@@ -39,7 +39,7 @@ def mk0 (a : α) (ha : a ≠ 0) : units α :=
 @[simp] lemma mk0_coe (u : units α) (h : (u : α) ≠ 0) : mk0 (u : α) h = u :=
 units.ext rfl
 
-@[simp] lemma units.mk0_inj {a b : α} (ha : a ≠ 0) (hb : b ≠ 0) :
+@[simp] lemma mk0_inj {a b : α} (ha : a ≠ 0) (hb : b ≠ 0) :
   units.mk0 a ha = units.mk0 b hb ↔ a = b :=
 ⟨λ h, by injection h, λ h, units.ext h⟩
 

src/algebra/group/basic.lean

@@ -140,8 +140,6 @@ section add_group
 
   local attribute [simp] sub_eq_add_neg
 
-  def sub_sub_cancel := @sub_sub_self
-
   @[simp] lemma sub_left_inj : a - b = a - c ↔ b = c :=
   (add_left_inj _).trans neg_inj'
 
@@ -187,6 +185,8 @@ end add_group
 section add_comm_group
   variables [add_comm_group α] {a b c : α}
 
+  lemma sub_sub_cancel (a b : α) : a - (a - b) = b := sub_sub_self a b
+
   lemma sub_eq_neg_add (a b : α) : a - b = -b + a :=
   add_comm _ _
 

src/algebra/group/with_one.lean

@@ -187,7 +187,7 @@ variables [group α]
 @[simp] lemma inv_one : (1 : with_zero α)⁻¹ = 1 :=
 show ((1⁻¹ : α) : with_zero α) = 1, by simp [coe_one]
 
-definition with_zero.div (x y : with_zero α) : with_zero α :=
+definition div (x y : with_zero α) : with_zero α :=
 x * y⁻¹
 
 instance : has_div (with_zero α) := ⟨with_zero.div⟩

src/algebra/ordered_field.lean

@@ -8,7 +8,7 @@ import algebra.ordered_ring algebra.field
 section linear_ordered_field
 variables {α : Type*} [linear_ordered_field α] {a b c d : α}
 
-def div_pos := @div_pos_of_pos_of_pos
+lemma div_pos : 0 < a → 0 < b → 0 < a / b := div_pos_of_pos_of_pos
 
 lemma inv_pos {a : α} : 0 < a → 0 < a⁻¹ :=
 by rw [inv_eq_one_div]; exact div_pos zero_lt_one
@@ -87,7 +87,7 @@ lt_iff_lt_of_le_iff_le (inv_le hb ha)
 lemma one_div_lt_one_div (ha : 0 < a) (hb : 0 < b) : 1 / a < 1 / b ↔ b < a :=
 lt_iff_lt_of_le_iff_le (one_div_le_one_div hb ha)
 
-def div_nonneg := @div_nonneg_of_nonneg_of_pos
+lemma div_nonneg : 0 ≤ a → 0 < b → 0 ≤ a / b := div_nonneg_of_nonneg_of_pos
 
 lemma div_lt_div_right (hc : 0 < c) : a / c < b / c ↔ a < b :=
 ⟨lt_imp_lt_of_le_imp_le (λ h, div_le_div_of_le_of_pos h hc),
@@ -125,7 +125,7 @@ lemma half_pos {a : α} (h : 0 < a) : 0 < a / 2 := div_pos h two_pos
 
 lemma one_half_pos : (0:α) < 1 / 2 := half_pos zero_lt_one
 
-def half_lt_self := @div_two_lt_of_pos
+lemma half_lt_self : 0 < a → a / 2 < a := div_two_lt_of_pos
 
 lemma one_half_lt_one : (1 / 2 : α) < 1 := half_lt_self zero_lt_one
 

src/algebra/ordered_ring.lean

@@ -252,7 +252,7 @@ instance to_ordered_ring : ordered_ring α :=
   mul_pos := λ a b, by simp [pos_def.symm]; exact mul_pos,
   ..s }
 
-def nonneg_ring.to_linear_nonneg_ring
+def to_linear_nonneg_ring
   (nonneg_total : ∀ a : α, nonneg a ∨ nonneg (-a))
   : linear_nonneg_ring α :=
 { nonneg_total := nonneg_total,

src/algebra/pointwise.lean

@@ -75,11 +75,11 @@ def pointwise_mul_monoid [monoid α] : monoid (set α) :=
 local attribute [instance] pointwise_mul_monoid
 
 @[to_additive]
-def singleton.is_mul_hom [has_mul α] : is_mul_hom (singleton : α → set α) :=
+lemma singleton.is_mul_hom [has_mul α] : is_mul_hom (singleton : α → set α) :=
 { map_mul := λ x y, set.ext $ λ a, by simp [mem_singleton_iff, mem_pointwise_mul] }
 
 @[to_additive is_add_monoid_hom]
-def singleton.is_monoid_hom [monoid α] : is_monoid_hom (singleton : α → set α) :=
+lemma singleton.is_monoid_hom [monoid α] : is_monoid_hom (singleton : α → set α) :=
 { map_one := rfl, ..singleton.is_mul_hom }
 
 @[to_additive]
@@ -212,7 +212,7 @@ end is_mul_hom
 
 variables [monoid α] [monoid β] [is_monoid_hom f]
 
-def pointwise_mul_image_is_semiring_hom : is_semiring_hom (image f) :=
+lemma pointwise_mul_image_is_semiring_hom : is_semiring_hom (image f) :=
 { map_zero := image_empty _,
   map_one := by erw [image_singleton, is_monoid_hom.map_one f]; refl,
   map_add := image_union _,

src/category/monad/cont.lean

@@ -71,7 +71,7 @@ instance : is_lawful_monad (cont_t r m) :=
   pure_bind := by { intros, ext, refl },
   bind_assoc := by { intros, ext, refl } }
 
-def cont_t.monad_lift [monad m] {α} : m α → cont_t r m α :=
+def monad_lift [monad m] {α} : m α → cont_t r m α :=
 λ x f, x >>= f
 
 instance [monad m] : has_monad_lift m (cont_t r m) :=

src/category/traversable/equiv.lean

@@ -33,11 +33,11 @@ protected lemma comp_map {α β γ : Type u} (g : α → β) (h : β → γ) (x
   equiv.map (h ∘ g) x = equiv.map h (equiv.map g x) :=
 by simp [equiv.map]; apply comp_map
 
-protected def is_lawful_functor : @is_lawful_functor _ equiv.functor :=
+protected lemma is_lawful_functor : @is_lawful_functor _ equiv.functor :=
 { id_map := @equiv.id_map _ _,
   comp_map := @equiv.comp_map _ _ }
 
-protected def is_lawful_functor' [F : _root_.functor t']
+protected lemma is_lawful_functor' [F : _root_.functor t']
   (h₀ : ∀ {α β} (f : α → β), _root_.functor.map f = equiv.map f)
   (h₁ : ∀ {α β} (f : β), _root_.functor.map_const f = (equiv.map ∘ function.const α) f) :
   _root_.is_lawful_functor t' :=

src/category_theory/natural_isomorphism.lean

@@ -94,12 +94,12 @@ def of_components (app : ∀ X : C, (F.obj X) ≅ (G.obj X))
   F ≅ G :=
 as_iso { app := λ X, (app X).hom }
 
-@[simp] def of_components.app (app' : ∀ X : C, (F.obj X) ≅ (G.obj X)) (naturality) (X) :
+@[simp] lemma of_components.app (app' : ∀ X : C, (F.obj X) ≅ (G.obj X)) (naturality) (X) :
   (of_components app' naturality).app X = app' X :=
 by tidy
-@[simp] def of_components.hom_app (app : ∀ X : C, (F.obj X) ≅ (G.obj X)) (naturality) (X) :
+@[simp] lemma of_components.hom_app (app : ∀ X : C, (F.obj X) ≅ (G.obj X)) (naturality) (X) :
   (of_components app naturality).hom.app X = (app X).hom := rfl
-@[simp] def of_components.inv_app (app : ∀ X : C, (F.obj X) ≅ (G.obj X)) (naturality) (X) :
+@[simp] lemma of_components.inv_app (app : ∀ X : C, (F.obj X) ≅ (G.obj X)) (naturality) (X) :
   (of_components app naturality).inv.app X = (app X).inv := rfl
 
 include ℰ