michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

chore(library/data/quotient): replace 'let' with 'have' and cleanup

Browse source
This commit is contained in:
Leonardo de Moura 2014-10-30 18:44:05 -07:00
parent 407e35692b
commit 09c6c05e26
1 changed files with 6 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

10
library/data/quotient/basic.lean
View file

@ -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 :=