From 9ac5f28b03a26cd19bb43ec13eaa34682b595081 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 9 Sep 2014 19:15:11 -0700
Subject: [PATCH] refactor(library/logic/core/eq): cleanup

---
 library/logic/core/eq.lean | 68 +++++++++++++++++++-------------------
 1 file changed, 34 insertions(+), 34 deletions(-)

diff --git a/library/logic/core/eq.lean b/library/logic/core/eq.lean
index 09c01ac7b..9cfcc73e8 100644
--- a/library/logic/core/eq.lean
+++ b/library/logic/core/eq.lean
@@ -19,20 +19,20 @@ infix `=` := eq
 abbreviation rfl {A : Type} {a : A} := eq.refl a
 
 namespace eq
-theorem id_refl {A : Type} {a : A} (H1 : a = a) : H1 = (eq.refl a) :=
-rfl
+  theorem id_refl {A : Type} {a : A} (H1 : a = a) : H1 = (eq.refl a) :=
+  rfl
 
-theorem irrel {A : Type} {a b : A} (H1 H2 : a = b) : H1 = H2 :=
-rfl
+  theorem irrel {A : Type} {a b : A} (H1 H2 : a = b) : H1 = H2 :=
+  rfl
 
-theorem subst {A : Type} {a b : A} {P : A → Prop} (H1 : a = b) (H2 : P a) : P b :=
-rec H2 H1
+  theorem subst {A : Type} {a b : A} {P : A → Prop} (H1 : a = b) (H2 : P a) : P b :=
+  rec H2 H1
 
-theorem trans {A : Type} {a b c : A} (H1 : a = b) (H2 : b = c) : a = c :=
-subst H2 H1
+  theorem trans {A : Type} {a b c : A} (H1 : a = b) (H2 : b = c) : a = c :=
+  subst H2 H1
 
-theorem symm {A : Type} {a b : A} (H : a = b) : b = a :=
-subst H (refl a)
+  theorem symm {A : Type} {a b : A} (H : a = b) : b = a :=
+  subst H (refl a)
 end eq
 
 calc_subst eq.subst
@@ -47,33 +47,33 @@ end eq_ops
 open eq_ops
 
 namespace eq
--- eq_rec with arguments swapped, for transporting an element of a dependent type
-definition rec_on {A : Type} {a1 a2 : A} {B : A → Type} (H1 : a1 = a2) (H2 : B a1) : B a2 :=
-eq.rec H2 H1
+  -- eq_rec with arguments swapped, for transporting an element of a dependent type
+  definition rec_on {A : Type} {a1 a2 : A} {B : A → Type} (H1 : a1 = a2) (H2 : B a1) : B a2 :=
+  eq.rec H2 H1
 
-theorem rec_on_id {A : Type} {a : A} {B : A → Type} (H : a = a) (b : B a) : rec_on H b = b :=
-refl (rec_on rfl b)
+  theorem rec_on_id {A : Type} {a : A} {B : A → Type} (H : a = a) (b : B a) : rec_on H b = b :=
+  refl (rec_on rfl b)
 
-theorem rec_id {A : Type} {a : A} {B : A → Type} (H : a = a) (b : B a) : rec b H = b :=
-rec_on_id H b
+  theorem rec_id {A : Type} {a : A} {B : A → Type} (H : a = a) (b : B a) : rec b H = b :=
+  rec_on_id H b
 
-theorem rec_on_compose {A : Type} {a b c : A} {P : A → Type} (H1 : a = b) (H2 : b = c)
-    (u : P a) :
-  rec_on H2 (rec_on H1 u) = rec_on (trans H1 H2) u :=
-(show ∀(H2 : b = c), rec_on H2 (rec_on H1 u) = rec_on (trans H1 H2) u,
-  from rec_on H2 (take (H2 : b = b), rec_on_id H2 _))
-H2
+  theorem rec_on_compose {A : Type} {a b c : A} {P : A → Type} (H1 : a = b) (H2 : b = c)
+          (u : P a) :
+    rec_on H2 (rec_on H1 u) = rec_on (trans H1 H2) u :=
+    (show ∀(H2 : b = c), rec_on H2 (rec_on H1 u) = rec_on (trans H1 H2) u,
+      from rec_on H2 (take (H2 : b = b), rec_on_id H2 _))
+    H2
 end eq
 
 theorem congr_fun {A : Type} {B : A → Type} {f g : Π x, B x} (H : f = g) (a : A) : f a = g a :=
-H ▸ eq.refl (f a)
+H ▸ rfl
 
 theorem congr_arg {A : Type} {B : Type} {a b : A} (f : A → B) (H : a = b) : f a = f b :=
-H ▸ eq.refl (f a)
+H ▸ rfl
 
 theorem congr {A : Type} {B : Type} {f g : A → B} {a b : A} (H1 : f = g) (H2 : a = b) :
   f a = g b :=
-H1 ▸ H2 ▸ eq.refl (f a)
+H1 ▸ H2 ▸ rfl
 
 theorem equal_f {A : Type} {B : A → Type} {f g : Π x, B x} (H : f = g) : ∀x, f x = g x :=
 take x, congr_fun H x
@@ -106,17 +106,17 @@ definition ne [inline] {A : Type} (a b : A) := ¬(a = b)
 infix `≠` := ne
 
 namespace ne
-theorem intro {A : Type} {a b : A} (H : a = b → false) : a ≠ b :=
-H
+  theorem intro {A : Type} {a b : A} (H : a = b → false) : a ≠ b :=
+  H
 
-theorem elim {A : Type} {a b : A} (H1 : a ≠ b) (H2 : a = b) : false :=
-H1 H2
+  theorem elim {A : Type} {a b : A} (H1 : a ≠ b) (H2 : a = b) : false :=
+  H1 H2
 
-theorem irrefl {A : Type} {a : A} (H : a ≠ a) : false :=
-H rfl
+  theorem irrefl {A : Type} {a : A} (H : a ≠ a) : false :=
+  H rfl
 
-theorem symm {A : Type} {a b : A} (H : a ≠ b) : b ≠ a :=
-assume H1 : b = a, H (H1⁻¹)
+  theorem symm {A : Type} {a b : A} (H : a ≠ b) : b ≠ a :=
+  assume H1 : b = a, H (H1⁻¹)
 end ne
 
 theorem a_neq_a_elim {A : Type} {a : A} (H : a ≠ a) : false :=