From 64cc710ff70dd1f26514ae96dc38d459a128e3a7 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 6 May 2015 10:34:43 -0700 Subject: [PATCH] refactor(ordered_group): replace 'match' with 'obtain' --- library/algebra/ordered_group.lean | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/library/algebra/ordered_group.lean b/library/algebra/ordered_group.lean index b5298e20d..447d014fd 100644 --- a/library/algebra/ordered_group.lean +++ b/library/algebra/ordered_group.lean @@ -152,9 +152,8 @@ section have Hbz : b = 0, from le.antisymm Hb' Hb, and.intro Haz Hbz) (assume Hab : a = 0 ∧ b = 0, - match Hab with - | and.intro Ha' Hb' := by rewrite [Ha', Hb', add_zero] - end) + obtain Ha' Hb', from Hab, + by rewrite [Ha', Hb', add_zero]) theorem le_add_of_nonneg_of_le (Ha : 0 ≤ a) (Hbc : b ≤ c) : b ≤ a + c := !zero_add ▸ add_le_add Ha Hbc