apply suggestion

LorenzoLuccioli · Aug 6, 2024 · c8050ed · c8050ed
1 parent 1b1f98c
commit c8050ed
Showing 1 changed file with 0 additions and 3 deletions.
diff --git 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