α : Type ?u.93966
β : Type ?u.93969
a✝ b c d : ℝ≥0∞
r p q : ℝ≥0
a : ℝ≥0∞
⊢ a = 0 → a < ⊤
α : Type ?u.93966
β : Type ?u.93969
a✝ b c d : ℝ≥0∞
r p q : ℝ≥0
a : ℝ≥0∞
⊢ a * a < ⊤ ↔ a < ⊤
rw [ENNReal.mul_lt_top_iff, and_self, or_self, or_iff_left_iff_imp]
α : Type ?u.93966
β : Type ?u.93969
a b c d : ℝ≥0∞
r p q : ℝ≥0
⊢ 0 < ⊤
α : Type ?u.93966
β : Type ?u.93969
a✝ b c d : ℝ≥0∞
r p q : ℝ≥0
a : ℝ≥0∞
⊢ a = 0 → a < ⊤
rintro rfl
no goals
α : Type ?u.93966
β : Type ?u.93969
a b c d : ℝ≥0∞
r p q : ℝ≥0
⊢ 0 < ⊤
norm_num