From 99a1966fd6d589a6fdd6f90af443a88fe2482593 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 27 Jul 2014 13:32:59 -0700 Subject: [PATCH] refactor(library/standard/set): use the same style for mem_inter and mem_union Signed-off-by: Leonardo de Moura --- library/standard/set.lean | 4 +--- 1 file changed, 1 insertion(+), 3 deletions(-) diff --git a/library/standard/set.lean b/library/standard/set.lean index dbf880530..0cc819a17 100644 --- a/library/standard/set.lean +++ b/library/standard/set.lean @@ -32,9 +32,7 @@ theorem mem_inter (x : T) (A B : set T) : x ∈ A ∩ B ↔ (x ∈ A ∧ x ∈ B (assume H, have e1 : A x = '1, from and_elim_left H, have e2 : B x = '1, from and_elim_right H, - calc A x && B x = '1 && B x : {e1} - ... = '1 && '1 : {e2} - ... = '1 : band_b1_left '1) + show A x && B x = '1, from e1⁻¹ ▸ e2⁻¹ ▸ band_b1_left '1) theorem inter_comm (A B : set T) : A ∩ B = B ∩ A := funext (λx, band_comm (A x) (B x))