case hb0
α : Type ?u.294363
β : Type ?u.294366
a b c d : ℝ≥0∞
r p q : ℝ≥0
h₁ : b = ⊤ → a ≠ 0
h₂ : a = ⊤ → b ≠ 0
⊢ a ≠ 0 ∨ b ≠ ⊤

case hbt
α : Type ?u.294363
β : Type ?u.294366
a b c d : ℝ≥0∞
r p q : ℝ≥0
h₁ : b = ⊤ → a ≠ 0
h₂ : a = ⊤ → b ≠ 0
⊢ a ≠ ⊤ ∨ b ≠ 0
α : Type ?u.294363
β : Type ?u.294366
a b c d : ℝ≥0∞
r p q : ℝ≥0
h₁ : b = ⊤ → a ≠ 0
h₂ : a = ⊤ → b ≠ 0
⊢ a⁻¹ ≤ b ↔ 1 ≤ a * b
rw [← one_div, ENNReal.div_le_iff_le_mul, mul_comm]
no goals
case hb0
α : Type ?u.294363
β : Type ?u.294366
a b c d : ℝ≥0∞
r p q : ℝ≥0
h₁ : b = ⊤ → a ≠ 0
h₂ : a = ⊤ → b ≠ 0
⊢ a ≠ 0 ∨ b ≠ ⊤

case hbt
α : Type ?u.294363
β : Type ?u.294366
a b c d : ℝ≥0∞
r p q : ℝ≥0
h₁ : b = ⊤ → a ≠ 0
h₂ : a = ⊤ → b ≠ 0
⊢ a ≠ ⊤ ∨ b ≠ 0
exacts [or_not_of_imp h₁, not_or_of_imp h₂]