case mp
α : Type ?u.92811
β : Type ?u.92814
a✝ b✝ c d : ℝ≥0∞
r p q : ℝ≥0
a b : ℝ≥0∞
⊢ a * b < ⊤ → a < ⊤ ∧ b < ⊤ ∨ a = 0 ∨ b = 0

case mpr
α : Type ?u.92811
β : Type ?u.92814
a✝ b✝ c d : ℝ≥0∞
r p q : ℝ≥0
a b : ℝ≥0∞
⊢ a < ⊤ ∧ b < ⊤ ∨ a = 0 ∨ b = 0 → a * b < ⊤
α : Type ?u.92811
β : Type ?u.92814
a✝ b✝ c d : ℝ≥0∞
r p q : ℝ≥0
a b : ℝ≥0∞
⊢ a * b < ⊤ ↔ a < ⊤ ∧ b < ⊤ ∨ a = 0 ∨ b = 0
constructor
case mp
α : Type ?u.92811
β : Type ?u.92814
a✝ b✝ c d : ℝ≥0∞
r p q : ℝ≥0
a b : ℝ≥0∞
h : a * b < ⊤
⊢ a < ⊤ ∧ b < ⊤ ∨ a = 0 ∨ b = 0
case mp
α : Type ?u.92811
β : Type ?u.92814
a✝ b✝ c d : ℝ≥0∞
r p q : ℝ≥0
a b : ℝ≥0∞
⊢ a * b < ⊤ → a < ⊤ ∧ b < ⊤ ∨ a = 0 ∨ b = 0
intro h
case mp
α : Type ?u.92811
β : Type ?u.92814
a✝ b✝ c d : ℝ≥0∞
r p q : ℝ≥0
a b : ℝ≥0∞
h : a * b < ⊤
⊢ ¬b = 0 → ¬a = 0 → a < ⊤ ∧ b < ⊤
case mp
α : Type ?u.92811
β : Type ?u.92814
a✝ b✝ c d : ℝ≥0∞
r p q : ℝ≥0
a b : ℝ≥0∞
h : a * b < ⊤
⊢ a < ⊤ ∧ b < ⊤ ∨ a = 0 ∨ b = 0
rw [← or_assoc, or_iff_not_imp_right, or_iff_not_imp_right]
case mp
α : Type ?u.92811
β : Type ?u.92814
a✝ b✝ c d : ℝ≥0∞
r p q : ℝ≥0
a b : ℝ≥0∞
h : a * b < ⊤
hb : ¬b = 0
ha : ¬a = 0
⊢ a < ⊤ ∧ b < ⊤
case mp
α : Type ?u.92811
β : Type ?u.92814
a✝ b✝ c d : ℝ≥0∞
r p q : ℝ≥0
a b : ℝ≥0∞
h : a * b < ⊤
⊢ ¬b = 0 → ¬a = 0 → a < ⊤ ∧ b < ⊤
intro hb ha
no goals
case mp
α : Type ?u.92811
β : Type ?u.92814
a✝ b✝ c d : ℝ≥0∞
r p q : ℝ≥0
a b : ℝ≥0∞
h : a * b < ⊤
hb : ¬b = 0
ha : ¬a = 0
⊢ a < ⊤ ∧ b < ⊤
exact ⟨lt_top_of_mul_ne_top_left h.ne hb, lt_top_of_mul_ne_top_right h.ne ha⟩
no goals
case mpr
α : Type ?u.92811
β : Type ?u.92814
a✝ b✝ c d : ℝ≥0∞
r p q : ℝ≥0
a b : ℝ≥0∞
⊢ a < ⊤ ∧ b < ⊤ ∨ a = 0 ∨ b = 0 → a * b < ⊤
rintro (⟨ha, hb⟩ | rfl | rfl) <;> [exact mul_lt_top ha.ne hb.ne; simp; simp]