case refine'_1
α β : Type u
a b : Cardinal
h : a * b < ℵ₀
⊢ a = 0 ∨ b = 0 ∨ a < ℵ₀ ∧ b < ℵ₀

case refine'_2
α β : Type u
a b : Cardinal
⊢ a = 0 ∨ b = 0 ∨ a < ℵ₀ ∧ b < ℵ₀ → a * b < ℵ₀
α β : Type u
a b : Cardinal
⊢ a * b < ℵ₀ ↔ a = 0 ∨ b = 0 ∨ a < ℵ₀ ∧ b < ℵ₀
refine' ⟨fun h => _, _⟩
no goals
case refine'_2
α β : Type u
a b : Cardinal
⊢ a = 0 ∨ b = 0 ∨ a < ℵ₀ ∧ b < ℵ₀ → a * b < ℵ₀
rintro (rfl | rfl | ⟨ha, hb⟩) <;> simp only [*, mul_lt_aleph0, aleph0_pos, zero_mul, mul_zero]
case pos
α β : Type u
a b : Cardinal
h : a * b < ℵ₀
ha : a = 0
⊢ a = 0 ∨ b = 0 ∨ a < ℵ₀ ∧ b < ℵ₀

case neg
α β : Type u
a b : Cardinal
h : a * b < ℵ₀
ha : ¬a = 0
⊢ a = 0 ∨ b = 0 ∨ a < ℵ₀ ∧ b < ℵ₀
case refine'_1
α β : Type u
a b : Cardinal
h : a * b < ℵ₀
⊢ a = 0 ∨ b = 0 ∨ a < ℵ₀ ∧ b < ℵ₀
by_cases ha : a = 0
case neg.h
α β : Type u
a b : Cardinal
h : a * b < ℵ₀
ha : ¬a = 0
⊢ b = 0 ∨ a < ℵ₀ ∧ b < ℵ₀
case neg
α β : Type u
a b : Cardinal
h : a * b < ℵ₀
ha : ¬a = 0
⊢ a = 0 ∨ b = 0 ∨ a < ℵ₀ ∧ b < ℵ₀
right
case pos
α β : Type u
a b : Cardinal
h : a * b < ℵ₀
ha : ¬a = 0
hb : b = 0
⊢ b = 0 ∨ a < ℵ₀ ∧ b < ℵ₀

case neg
α β : Type u
a b : Cardinal
h : a * b < ℵ₀
ha : ¬a = 0
hb : ¬b = 0
⊢ b = 0 ∨ a < ℵ₀ ∧ b < ℵ₀
case neg.h
α β : Type u
a b : Cardinal
h : a * b < ℵ₀
ha : ¬a = 0
⊢ b = 0 ∨ a < ℵ₀ ∧ b < ℵ₀
by_cases hb : b = 0
case neg.h
α β : Type u
a b : Cardinal
h : a * b < ℵ₀
ha : ¬a = 0
hb : ¬b = 0
⊢ a < ℵ₀ ∧ b < ℵ₀
case neg
α β : Type u
a b : Cardinal
h : a * b < ℵ₀
ha : ¬a = 0
hb : ¬b = 0
⊢ b = 0 ∨ a < ℵ₀ ∧ b < ℵ₀
right
case neg.h
α β : Type u
a b : Cardinal
h : a * b < ℵ₀
ha : 1 ≤ a
hb : 1 ≤ b
⊢ a < ℵ₀ ∧ b < ℵ₀
case neg.h
α β : Type u
a b : Cardinal
h : a * b < ℵ₀
ha : ¬a = 0
hb : ¬b = 0
⊢ a < ℵ₀ ∧ b < ℵ₀
rw [← Ne, ← one_le_iff_ne_zero] at ha hb
case neg.h.left
α β : Type u
a b : Cardinal
h : a * b < ℵ₀
ha : 1 ≤ a
hb : 1 ≤ b
⊢ a < ℵ₀

case neg.h.right
α β : Type u
a b : Cardinal
h : a * b < ℵ₀
ha : 1 ≤ a
hb : 1 ≤ b
⊢ b < ℵ₀
case neg.h
α β : Type u
a b : Cardinal
h : a * b < ℵ₀
ha : 1 ≤ a
hb : 1 ≤ b
⊢ a < ℵ₀ ∧ b < ℵ₀
constructor
no goals
case pos
α β : Type u
a b : Cardinal
h : a * b < ℵ₀
ha : a = 0
⊢ a = 0 ∨ b = 0 ∨ a < ℵ₀ ∧ b < ℵ₀
exact Or.inl ha
no goals
case pos
α β : Type u
a b : Cardinal
h : a * b < ℵ₀
ha : ¬a = 0
hb : b = 0
⊢ b = 0 ∨ a < ℵ₀ ∧ b < ℵ₀
exact Or.inl hb
case neg.h.left
α β : Type u
a b : Cardinal
h : a * b < ℵ₀
ha : 1 ≤ a
hb : 1 ≤ b
⊢ a * 1 < ℵ₀
case neg.h.left
α β : Type u
a b : Cardinal
h : a * b < ℵ₀
ha : 1 ≤ a
hb : 1 ≤ b
⊢ a < ℵ₀
rw [← mul_one a]
no goals
case neg.h.left
α β : Type u
a b : Cardinal
h : a * b < ℵ₀
ha : 1 ≤ a
hb : 1 ≤ b
⊢ a * 1 < ℵ₀
refine' (mul_le_mul' le_rfl hb).trans_lt h
case neg.h.right
α β : Type u
a b : Cardinal
h : a * b < ℵ₀
ha : 1 ≤ a
hb : 1 ≤ b
⊢ 1 * b < ℵ₀
case neg.h.right
α β : Type u
a b : Cardinal
h : a * b < ℵ₀
ha : 1 ≤ a
hb : 1 ≤ b
⊢ b < ℵ₀
rw [← one_mul b]
no goals
case neg.h.right
α β : Type u
a b : Cardinal
h : a * b < ℵ₀
ha : 1 ≤ a
hb : 1 ≤ b
⊢ 1 * b < ℵ₀
refine' (mul_le_mul' ha le_rfl).trans_lt h