From 09c6c05e2669a3f08b131096ed25a27b2afca157 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 30 Oct 2014 18:44:05 -0700 Subject: [PATCH] chore(library/data/quotient): replace 'let' with 'have' and cleanup --- library/data/quotient/basic.lean | 10 ++++++---- 1 file changed, 6 insertions(+), 4 deletions(-) diff --git a/library/data/quotient/basic.lean b/library/data/quotient/basic.lean index 6aac166d8..611016a4a 100644 --- a/library/data/quotient/basic.lean +++ b/library/data/quotient/basic.lean @@ -121,12 +121,14 @@ theorem comp {A B : Type} {R : A → A → Prop} {abs : A → B} {rep : B → A} (Q : is_quotient R abs rep) {C : B → Type} {f : forall (a : A), C (abs a)} (H : forall (r s : A) (H' : R r s), eq.drec_on (eq_abs Q H') (f r) = f s) {a : A} (Ha : R a a) : rec Q f (abs a) = f a := -have H2 [visible] : R a (rep (abs a)), from R_rep_abs Q Ha, -let Heq : abs (rep (abs a)) = abs a := abs_rep Q (abs a) in +have H2 [visible] : R a (rep (abs a)), from + R_rep_abs Q Ha, +have Heq [visible] : abs (rep (abs a)) = abs a, from + abs_rep Q (abs a), calc rec Q f (abs a) = eq.drec_on Heq (f (rep (abs a))) : rfl - ... = eq.drec_on Heq (eq.drec_on (Heq⁻¹) (f a)) : {(H _ _ H2)⁻¹} - ... = f a : eq.rec_on_compose (eq_abs Q H2) _ _ + ... = eq.drec_on Heq (eq.drec_on (Heq⁻¹) (f a)) : {(H _ _ H2)⁻¹} + ... = f a : eq.rec_on_compose (eq_abs Q H2) _ _ definition rec_constant {A B : Type} {R : A → A → Prop} {abs : A → B} {rep : B → A} (Q : is_quotient R abs rep) {C : Type} (f : A → C) (b : B) : C :=