lint

leanprover-community · Oct 22, 2023 · 8f501cb · 8f501cb
1 parent b0bc32e
commit 8f501cb
Showing 1 changed file with 3 additions and 4 deletions.
diff --git a/Mathlib/Data/Real/ENNReal.lean b/Mathlib/Data/Real/ENNReal.lean
@@ -633,11 +633,10 @@ 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)
+  · rintro (⟨ha, hb⟩ | rfl | rfl)
     · exact mul_lt_top ha.ne hb.ne
-    · simp [this]
-    · simp [this]
+    · 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