From c8050ed7be37e6ae921f8c2bd926f323e7766307 Mon Sep 17 00:00:00 2001 From: Lorenzo Luccioli Date: Tue, 6 Aug 2024 17:20:57 +0200 Subject: [PATCH] apply suggestion --- TestingLowerBounds/ForMathlib/EReal.lean | 3 --- 1 file changed, 3 deletions(-) diff --git a/TestingLowerBounds/ForMathlib/EReal.lean b/TestingLowerBounds/ForMathlib/EReal.lean index 2fc32964..34e34de1 100644 --- a/TestingLowerBounds/ForMathlib/EReal.lean +++ b/TestingLowerBounds/ForMathlib/EReal.lean @@ -9,9 +9,6 @@ namespace EReal instance : CharZero EReal := inferInstanceAs (CharZero (WithBot (WithTop ℝ))) -lemma eq_coe_of_ne_top_of_ne_bot {x : EReal} (hx : x ≠ ⊤) (hx' : x ≠ ⊥) : ∃ r : ℝ, x = r := by - induction x <;> tauto - lemma coe_ennreal_toReal {x : ℝ≥0∞} (hx : x ≠ ∞) : (x.toReal : EReal) = x := by lift x to ℝ≥0 using hx rfl