From 42eda36225c9d0958ae7e675896d301bcb16bc5c Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 15 Dec 2015 09:33:57 -0800 Subject: [PATCH] chore(library/algebra/ordered_ring): use 'note' --- library/algebra/ordered_ring.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/library/algebra/ordered_ring.lean b/library/algebra/ordered_ring.lean index 31cb32f1a2..1379dde857 100644 --- a/library/algebra/ordered_ring.lean +++ b/library/algebra/ordered_ring.lean @@ -440,8 +440,8 @@ section begin apply le_of_not_gt, intro Hab, - let Hposa := lt_of_le_of_lt Hb Hab, - let H' := calc + note Hposa := lt_of_le_of_lt Hb Hab, + note H' := calc b * b ≤ a * b : mul_le_mul_of_nonneg_right (le_of_lt Hab) Hb ... < a * a : mul_lt_mul_of_pos_left Hab Hposa, apply (not_le_of_gt H') H