From b04fb529c8c77e979e32587a8c53c900c8d1d94a Mon Sep 17 00:00:00 2001
From: Mauricio Collares <mauricio@collares.org>
Date: Sun, 22 Oct 2023 18:11:23 +0200
Subject: [PATCH] lint

---
 Mathlib/Data/Real/ENNReal.lean | 6 +-----
 1 file changed, 1 insertion(+), 5 deletions(-)

diff --git a/Mathlib/Data/Real/ENNReal.lean b/Mathlib/Data/Real/ENNReal.lean
index ada7acdfb470f2..185db4b78ccbc1 100644
--- a/Mathlib/Data/Real/ENNReal.lean
+++ b/Mathlib/Data/Real/ENNReal.lean
@@ -633,11 +633,7 @@ theorem mul_lt_top_iff {a b : ℝ≥0∞} : a * b < ∞ ↔ a < ∞ ∧ b < ∞
     rw [← or_assoc, or_iff_not_imp_right, or_iff_not_imp_right]
     intro hb ha
     exact ⟨lt_top_of_mul_ne_top_left h.ne hb, lt_top_of_mul_ne_top_right h.ne ha⟩
-  · have : 0 < (⊤ : ℝ≥0∞) := by decide
-    rintro (⟨ha, hb⟩ | rfl | rfl)
-    · exact mul_lt_top ha.ne hb.ne
-    · simp [this]
-    · simp [this]
+  · rintro (⟨ha, hb⟩ | rfl | rfl) <;> [exact mul_lt_top ha.ne hb.ne; simp; simp]
 #align ennreal.mul_lt_top_iff ENNReal.mul_lt_top_iff
 
 theorem mul_self_lt_top_iff {a : ℝ≥0∞} : a * a < ⊤ ↔ a < ⊤ := by