chore(*): rfl-lemmas on same line

algebra/group.lean

@@ -148,11 +148,9 @@ sorry -- by simp
 theorem one_add_bit0 [add_comm_semigroup A] [has_one A] (a : A) : one + bit0 a = bit1 a :=
 sorry -- by simp
 
-theorem bit0_add_one [has_add A] [has_one A] (a : A) : bit0 a + one = bit1 a :=
-rfl
+theorem bit0_add_one [has_add A] [has_one A] (a : A) : bit0 a + one = bit1 a := rfl
 
-theorem bit1_add_one [has_add A] [has_one A] (a : A) : bit1 a + one = add1 (bit1 a) :=
-rfl
+theorem bit1_add_one [has_add A] [has_one A] (a : A) : bit1 a + one = add1 (bit1 a) := rfl
 
 theorem bit1_add_one_helper [has_add A] [has_one A] (a t : A) (H : add1 (bit1 a) = t) :
         bit1 a + one = t :=
@@ -165,8 +163,7 @@ theorem one_add_bit1_helper [add_comm_semigroup A] [has_one A] (a t : A)
         (H : add1 (bit1 a) = t) : one + bit1 a = t :=
 sorry -- by inst_simp
 
-theorem add1_bit0 [has_add A] [has_one A] (a : A) : add1 (bit0 a) = bit1 a :=
-rfl
+theorem add1_bit0 [has_add A] [has_one A] (a : A) : add1 (bit0 a) = bit1 a := rfl
 
 theorem add1_bit1 [add_comm_semigroup A] [has_one A] (a : A) :
         add1 (bit1 a) = bit0 (add1 a) :=
@@ -176,14 +173,12 @@ theorem add1_bit1_helper [add_comm_semigroup A] [has_one A] (a t : A) (H : add1
         add1 (bit1 a) = bit0 t :=
 sorry -- by inst_simp
 
-theorem add1_one [has_add A] [has_one A] : add1 (one : A) = bit0 one :=
-rfl
+theorem add1_one [has_add A] [has_one A] : add1 (one : A) = bit0 one := rfl
 
 theorem add1_zero [add_monoid A] [has_one A] : add1 (zero : A) = one :=
 sorry -- by simp
 
-theorem one_add_one [has_add A] [has_one A] : (one : A) + one = bit0 one :=
-rfl
+theorem one_add_one [has_add A] [has_one A] : (one : A) + one = bit0 one := rfl
 
 theorem subst_into_sum [has_add A] (l r tl tr t : A) (prl : l = tl) (prr : r = tr)
         (prt : tl + tr = t) : l + r = t :=

algebra/lattice/filter.lean

@@ -96,8 +96,7 @@ variables {α β : Type u}
 theorem ne_empty_iff_exists_mem {s : set α} : s ≠ ∅ ↔ ∃ x, x ∈ s :=
 ⟨exists_mem_of_ne_empty, assume ⟨x, (hx : x ∈ s)⟩ h, by rw [h] at hx; assumption⟩
 
-theorem fmap_eq_image {f : α → β} {s : set α} : f <$> s = f '' s :=
-rfl
+theorem fmap_eq_image {f : α → β} {s : set α} : f <$> s = f '' s := rfl
 
 theorem mem_seq_iff {f : set (α → β)} {s : set α} {b : β} :
   b ∈ (f <*> s) ↔ (∃(f' : α → β), ∃a ∈ s, f' ∈ f ∧ b = f' a) :=
@@ -117,12 +116,10 @@ protected def prod (s : set α) (t : set β) : set (α × β) :=
 {p | p.1 ∈ s ∧ p.2 ∈ t}
 
 theorem mem_prod_eq {s : set α} {t : set β} {p : α × β} :
-  p ∈ set.prod s t = (p.1 ∈ s ∧ p.2 ∈ t) :=
-rfl
+  p ∈ set.prod s t = (p.1 ∈ s ∧ p.2 ∈ t) := rfl
 
 theorem prod_vimage_eq {s : set α} {t : set β} {f : γ → α} {g : δ → β} :
-  set.prod (vimage f s) (vimage g t) = vimage (λp, (f p.1, g p.2)) (set.prod s t) :=
-rfl
+  set.prod (vimage f s) (vimage g t) = vimage (λp, (f p.1, g p.2)) (set.prod s t) := rfl
 
 theorem prod_mono {s₁ s₂ : set α} {t₁ t₂ : set β} (hs : s₁ ⊆ s₂) (ht : t₁ ⊆ t₂) :
   set.prod s₁ t₁ ⊆ set.prod s₂ t₂ :=
@@ -170,19 +167,16 @@ begin
 end
 
 @[simp] theorem prod_mk_mem_set_prod_eq {a : α} {b : β} {s : set α} {t : set β} :
-  (a, b) ∈ set.prod s t = (a ∈ s ∧ b ∈ t) :=
-rfl
+  (a, b) ∈ set.prod s t = (a ∈ s ∧ b ∈ t) := rfl
 
 theorem monotone_inter [weak_order β] {f g : β → set α}
   (hf : monotone f) (hg : monotone g) : monotone (λx, (f x) ∩ (g x)) :=
 assume a b h x ⟨h₁, h₂⟩, ⟨hf h h₁, hg h h₂⟩
 
 @[simp] theorem vimage_set_of_eq {p : α → Prop} {f : β → α} :
-  vimage f {a | p a} = {a | p (f a)} :=
-rfl
+  vimage f {a | p a} = {a | p (f a)} := rfl
 
-@[simp] theorem set_of_mem_eq {s : set α} : {x | x ∈ s} = s :=
-rfl
+@[simp] theorem set_of_mem_eq {s : set α} : {x | x ∈ s} = s := rfl
 
 theorem mem_image_iff_of_inverse (f : α → β) (g : β → α) {b : β} {s : set α}
   (h₁ : ∀a, g (f a) = a ) (h₂ : ∀b, f (g b) = b ) : b ∈ f '' s ↔ g b ∈ s :=
@@ -445,11 +439,9 @@ assume f_in_s t' h, h f_in_s
 protected theorem Sup_le {s : set (filter α)} {f : filter α} : (∀g∈s, g ≤ f) → Sup s ≤ f :=
 assume h a ha g hg, h g hg ha
 
-@[simp] theorem mem_join_sets {s : set α} {f : filter (filter α)} : s ∈ (join f).sets = ({t | s ∈ filter.sets t} ∈ f.sets) :=
-rfl
+@[simp] theorem mem_join_sets {s : set α} {f : filter (filter α)} : s ∈ (join f).sets = ({t | s ∈ filter.sets t} ∈ f.sets) := rfl
 
-@[simp] theorem mem_principal_sets {s t : set α} : s ∈ (principal t).sets = (t ⊆ s) :=
-rfl
+@[simp] theorem mem_principal_sets {s t : set α} : s ∈ (principal t).sets = (t ⊆ s) := rfl
 
 @[simp] theorem le_principal_iff {s : set α} {f : filter α} : f ≤ principal s ↔ s ∈ f.sets :=
 show (∀{t}, s ⊆ t → t ∈ f.sets) ↔ s ∈ f.sets,
@@ -490,8 +482,7 @@ instance complete_lattice_filter : complete_lattice (filter α) :=
   map f (principal s) = principal (set.image f s) :=
 filter_eq $ set.ext $ assume a, image_subset_iff_subset_vimage.symm
 
-@[simp] theorem join_principal_eq_Sup {s : set (filter α)} : join (principal s) = Sup s :=
-rfl
+@[simp] theorem join_principal_eq_Sup {s : set (filter α)} : join (principal s) = Sup s := rfl
 
 instance monad_filter : monad filter :=
 { monad .
@@ -672,11 +663,9 @@ filter_eq $ set.ext $ by simp [union_subset_iff]
 @[simp] theorem supr_principal {ι : Sort w} {s : ι → set α} : (⨆x, principal (s x)) = principal (⋃i, s i) :=
 filter_eq $ set.ext $ assume x, by simp [supr_sets_eq]; exact (@supr_le_iff (set α) _ _ _ _).symm
 
-theorem principal_univ : principal (univ : set α) = ⊤ :=
-rfl
+theorem principal_univ : principal (univ : set α) = ⊤ := rfl
 
-theorem principal_empty : principal (∅ : set α) = ⊥ :=
-rfl
+theorem principal_empty : principal (∅ : set α) = ⊥ := rfl
 
 @[simp] theorem principal_eq_bot_iff {s : set α} : principal s = ⊥ ↔ s = ∅ :=
 ⟨assume h, principal_eq_iff_eq.mp $ by simp [principal_empty, h], assume h, by simp [*, principal_empty]⟩
@@ -687,8 +676,7 @@ by simp; exact id
 /- map equations -/
 
 @[simp] theorem mem_map {f : filter α} {s : set β} {m : α → β} :
-  (s ∈ (map m f).sets) = ({x | m x ∈ s} ∈ f.sets) :=
-rfl
+  (s ∈ (map m f).sets) = ({x | m x ∈ s} ∈ f.sets) := rfl
 
 theorem image_mem_map {f : filter α} {m : α → β} {s : set α} (hs : s ∈ f.sets):
   m '' s ∈ (map m f).sets :=

algebra/order.lean

@@ -63,8 +63,7 @@ def weak_order_dual (wo : weak_order α) : weak_order α :=
 
 theorem le_dual_eq_le {α : Type} (wo : weak_order α) (a b : α) :
   @has_le.le _ (@weak_order.to_has_le _ (weak_order_dual wo)) a b =
-  @has_le.le _ (@weak_order.to_has_le _ wo) b a :=
-rfl
+  @has_le.le _ (@weak_order.to_has_le _ wo) b a := rfl
 
 theorem comp_le_comp_left_of_monotone [weak_order α] [weak_order β] [weak_order γ]
   {f : β → α} {g h : γ → β} (m_f : monotone f) (le_gh : g ≤ h) : has_le.le.{max w u} (f ∘ g) (f ∘ h) :=

data/bool.lean

@@ -45,11 +45,9 @@ by cases a; cases b; simp
 theorem dichotomy (b : bool) : b = ff ∨ b = tt :=
 by cases b; simp
 
-@[simp] theorem cond_ff {A : Type} (t e : A) : cond ff t e = e :=
-rfl
+@[simp] theorem cond_ff {A : Type} (t e : A) : cond ff t e = e := rfl
 
-@[simp] theorem cond_tt {A : Type} (t e : A) : cond tt t e = t :=
-rfl
+@[simp] theorem cond_tt {A : Type} (t e : A) : cond tt t e = t := rfl
 
 theorem eq_tt_of_ne_ff {a : bool} : a ≠ ff → a = tt :=
 by cases a; simp
@@ -99,11 +97,9 @@ begin cases a, simp [H₁, H₂], simp [H₂] end
 theorem band_elim_right {a b : bool} (H : a && b = tt) : b = tt :=
 begin cases a, contradiction, simp at H, exact H end
 
-@[simp] theorem bnot_false : bnot ff = tt :=
-rfl
+@[simp] theorem bnot_false : bnot ff = tt := rfl
 
-@[simp] theorem bnot_true : bnot tt = ff :=
-rfl
+@[simp] theorem bnot_true : bnot tt = ff := rfl
 
 @[simp] theorem bnot_bnot (a : bool) : bnot (bnot a) = a :=
 by cases a; simp

data/list/basic.lean

@@ -63,27 +63,22 @@ by induction l₂ with b l₂ ih; simp
 
 /- last -/
 
-@[simp] theorem last_singleton (a : α) (h : [a] ≠ []) : last [a] h = a :=
-rfl
+@[simp] theorem last_singleton (a : α) (h : [a] ≠ []) : last [a] h = a := rfl
 
 @[simp] theorem last_cons_cons (a₁ a₂ : α) (l : list α) (h : a₁::a₂::l ≠ []) :
-  last (a₁::a₂::l) h = last (a₂::l) (cons_ne_nil a₂ l) :=
-rfl
+  last (a₁::a₂::l) h = last (a₂::l) (cons_ne_nil a₂ l) := rfl
 
 theorem last_congr {l₁ l₂ : list α} (h₁ : l₁ ≠ []) (h₂ : l₂ ≠ []) (h₃ : l₁ = l₂) :
   last l₁ h₁ = last l₂ h₂ :=
 by subst l₁
 
 /- head and tail -/
 
-@[simp] theorem head_cons [h : inhabited α] (a : α) (l : list α) : head (a::l) = a :=
-rfl
+@[simp] theorem head_cons [h : inhabited α] (a : α) (l : list α) : head (a::l) = a := rfl
 
-@[simp] theorem tail_nil : tail (@nil α) = [] :=
-rfl
+@[simp] theorem tail_nil : tail (@nil α) = [] := rfl
 
-@[simp] theorem tail_cons (a : α) (l : list α) : tail (a::l) = l :=
-rfl
+@[simp] theorem tail_cons (a : α) (l : list α) : tail (a::l) = l := rfl
 
 /- list membership -/
 
@@ -95,11 +90,9 @@ attribute [simp] mem_nil_iff mem_cons_self mem_cons_iff
 section index_of
 variable [decidable_eq α]
 
-@[simp] theorem index_of_nil (a : α) : index_of a [] = 0 :=
-rfl
+@[simp] theorem index_of_nil (a : α) : index_of a [] = 0 := rfl
 
-theorem index_of_cons (a b : α) (l : list α) : index_of a (b::l) = if a = b then 0 else succ (index_of a l) :=
-rfl
+theorem index_of_cons (a b : α) (l : list α) : index_of a (b::l) = if a = b then 0 else succ (index_of a l) := rfl
 
 @[simp] theorem index_of_cons_of_eq {a b : α} (l : list α) : a = b → index_of a (b::l) = 0 :=
 assume e, if_pos e
@@ -178,11 +171,9 @@ match (nth l n) with
 | none     := arbitrary α
 end
 
-theorem inth_zero [inhabited α] (a : α) (l : list α) : inth (a :: l) 0 = a :=
-rfl
+theorem inth_zero [inhabited α] (a : α) (l : list α) : inth (a :: l) 0 = a := rfl
 
-theorem inth_succ [inhabited α] (a : α) (l : list α) (n : nat) : inth (a::l) (n+1) = inth l n :=
-rfl
+theorem inth_succ [inhabited α] (a : α) (l : list α) (n : nat) : inth (a::l) (n+1) = inth l n := rfl
 
 end nth
 
@@ -193,12 +184,10 @@ def ith : Π (l : list α) (i : nat), i < length l → α
 | (a::ains) 0        h := a
 | (a::ains) (succ i) h := ith ains i (lt_of_succ_lt_succ h)
 
-@[simp] theorem ith_zero (a : α) (l : list α) (h : 0 < length (a::l)) : ith (a::l) 0 h = a :=
-rfl
+@[simp] theorem ith_zero (a : α) (l : list α) (h : 0 < length (a::l)) : ith (a::l) 0 h = a := rfl
 
 @[simp] theorem ith_succ (a : α) (l : list α) (i : nat) (h : succ i < length (a::l))
-                      : ith (a::l) (succ i) h = ith l i (lt_of_succ_lt_succ h) :=
-rfl
+                      : ith (a::l) (succ i) h = ith l i (lt_of_succ_lt_succ h) := rfl
 end ith
 
 section take
@@ -279,12 +268,10 @@ def count (a : α) : list α → nat
 | []      := 0
 | (x::xs) := if a = x then succ (count xs) else count xs
 
-@[simp] theorem count_nil (a : α) : count a [] = 0 :=
-rfl
+@[simp] theorem count_nil (a : α) : count a [] = 0 := rfl
 
 theorem count_cons (a b : α) (l : list α) :
-  count a (b :: l) = if a = b then succ (count a l) else count a l :=
-rfl
+  count a (b :: l) = if a = b then succ (count a l) else count a l := rfl
 
 theorem count_cons' (a b : α) (l : list α) :
   count a (b :: l) = count a l + (if a = b then 1 else 0) :=