From 79ba2638b7cc1def92245c4f56336be0de5774af Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 29 Feb 2016 13:29:03 -0800 Subject: [PATCH] fix(library/data/set/equinumerosity): add missing 'using' --- library/data/set/equinumerosity.lean | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/library/data/set/equinumerosity.lean b/library/data/set/equinumerosity.lean index 65738dcca1..b708c6c7c5 100644 --- a/library/data/set/equinumerosity.lean +++ b/library/data/set/equinumerosity.lean @@ -111,14 +111,15 @@ open set noncomputable definition h x := if x ∈ Union U then f x else ginv x lemma h_maps_to : maps_to h A B := + using f_maps_to dfltB, take a, suppose a ∈ A, show h a ∈ B, from by_cases (suppose a ∈ Union U, - by rewrite [↑h, if_pos this]; exact f_maps_to `a ∈ A`) + begin rewrite [↑h, if_pos this], exact f_maps_to `a ∈ A` end) (suppose a ∉ Union U, - by rewrite [↑h, if_neg this]; exact ginv_maps_to `a ∈ A`) + begin rewrite [↑h, if_neg this], exact ginv_maps_to `a ∈ A` end) /- h is injective -/