case inl
α β : Type u
y : Cardinal
⊢ ↑toNat (0 * y) = ↑toNat 0 * ↑toNat y

case inr
α β : Type u
x y : Cardinal
hx1 : x ≠ 0
⊢ ↑toNat (x * y) = ↑toNat x * ↑toNat y
α β : Type u
x y : Cardinal
⊢ ↑toNat (x * y) = ↑toNat x * ↑toNat y
rcases eq_or_ne x 0 with (rfl | hx1)
case inr.inl
α β : Type u
x : Cardinal
hx1 : x ≠ 0
⊢ ↑toNat (x * 0) = ↑toNat x * ↑toNat 0

case inr.inr
α β : Type u
x y : Cardinal
hx1 : x ≠ 0
hy1 : y ≠ 0
⊢ ↑toNat (x * y) = ↑toNat x * ↑toNat y
case inr
α β : Type u
x y : Cardinal
hx1 : x ≠ 0
⊢ ↑toNat (x * y) = ↑toNat x * ↑toNat y
rcases eq_or_ne y 0 with (rfl | hy1)
case inr.inr.inl
α β : Type u
x y : Cardinal
hx1 : x ≠ 0
hy1 : y ≠ 0
hx2 : x < ℵ₀
⊢ ↑toNat (x * y) = ↑toNat x * ↑toNat y

case inr.inr.inr
α β : Type u
x y : Cardinal
hx1 : x ≠ 0
hy1 : y ≠ 0
hx2 : ℵ₀ ≤ x
⊢ ↑toNat (x * y) = ↑toNat x * ↑toNat y
case inr.inr
α β : Type u
x y : Cardinal
hx1 : x ≠ 0
hy1 : y ≠ 0
⊢ ↑toNat (x * y) = ↑toNat x * ↑toNat y
cases' lt_or_le x ℵ₀ with hx2 hx2
no goals
case inl
α β : Type u
y : Cardinal
⊢ ↑toNat (0 * y) = ↑toNat 0 * ↑toNat y
rw [zero_mul, zero_toNat, zero_mul]
no goals
case inr.inl
α β : Type u
x : Cardinal
hx1 : x ≠ 0
⊢ ↑toNat (x * 0) = ↑toNat x * ↑toNat 0
rw [mul_zero, zero_toNat, mul_zero]
case inr.inr.inl.inl
α β : Type u
x y : Cardinal
hx1 : x ≠ 0
hy1 : y ≠ 0
hx2 : x < ℵ₀
hy2 : y < ℵ₀
⊢ ↑toNat (x * y) = ↑toNat x * ↑toNat y

case inr.inr.inl.inr
α β : Type u
x y : Cardinal
hx1 : x ≠ 0
hy1 : y ≠ 0
hx2 : x < ℵ₀
hy2 : ℵ₀ ≤ y
⊢ ↑toNat (x * y) = ↑toNat x * ↑toNat y
case inr.inr.inl
α β : Type u
x y : Cardinal
hx1 : x ≠ 0
hy1 : y ≠ 0
hx2 : x < ℵ₀
⊢ ↑toNat (x * y) = ↑toNat x * ↑toNat y
cases' lt_or_le y ℵ₀ with hy2 hy2
case inr.inr.inl.inl.intro
α β : Type u
y : Cardinal
hy1 : y ≠ 0
hy2 : y < ℵ₀
x : ℕ
hx1 : ↑x ≠ 0
⊢ ↑toNat (↑x * y) = ↑toNat ↑x * ↑toNat y
case inr.inr.inl.inl
α β : Type u
x y : Cardinal
hx1 : x ≠ 0
hy1 : y ≠ 0
hx2 : x < ℵ₀
hy2 : y < ℵ₀
⊢ ↑toNat (x * y) = ↑toNat x * ↑toNat y
lift x to ℕ using hx2
case inr.inr.inl.inl.intro.intro
α β : Type u
x : ℕ
hx1 : ↑x ≠ 0
y : ℕ
hy1 : ↑y ≠ 0
⊢ ↑toNat (↑x * ↑y) = ↑toNat ↑x * ↑toNat ↑y
case inr.inr.inl.inl.intro
α β : Type u
y : Cardinal
hy1 : y ≠ 0
hy2 : y < ℵ₀
x : ℕ
hx1 : ↑x ≠ 0
⊢ ↑toNat (↑x * y) = ↑toNat ↑x * ↑toNat y
lift y to ℕ using hy2
no goals
case inr.inr.inl.inl.intro.intro
α β : Type u
x : ℕ
hx1 : ↑x ≠ 0
y : ℕ
hy1 : ↑y ≠ 0
⊢ ↑toNat (↑x * ↑y) = ↑toNat ↑x * ↑toNat ↑y
rw [← Nat.cast_mul, toNat_cast, toNat_cast, toNat_cast]
case inr.inr.inl.inr
α β : Type u
x y : Cardinal
hx1 : x ≠ 0
hy1 : y ≠ 0
hx2 : x < ℵ₀
hy2 : ℵ₀ ≤ y
⊢ ℵ₀ ≤ x * y
case inr.inr.inl.inr
α β : Type u
x y : Cardinal
hx1 : x ≠ 0
hy1 : y ≠ 0
hx2 : x < ℵ₀
hy2 : ℵ₀ ≤ y
⊢ ↑toNat (x * y) = ↑toNat x * ↑toNat y
rw [toNat_apply_of_aleph0_le hy2, mul_zero, toNat_apply_of_aleph0_le]
no goals
case inr.inr.inl.inr
α β : Type u
x y : Cardinal
hx1 : x ≠ 0
hy1 : y ≠ 0
hx2 : x < ℵ₀
hy2 : ℵ₀ ≤ y
⊢ ℵ₀ ≤ x * y
exact aleph0_le_mul_iff'.2 (Or.inl ⟨hx1, hy2⟩)
case inr.inr.inr
α β : Type u
x y : Cardinal
hx1 : x ≠ 0
hy1 : y ≠ 0
hx2 : ℵ₀ ≤ x
⊢ ℵ₀ ≤ x * y
case inr.inr.inr
α β : Type u
x y : Cardinal
hx1 : x ≠ 0
hy1 : y ≠ 0
hx2 : ℵ₀ ≤ x
⊢ ↑toNat (x * y) = ↑toNat x * ↑toNat y
rw [toNat_apply_of_aleph0_le hx2, zero_mul, toNat_apply_of_aleph0_le]
no goals
case inr.inr.inr
α β : Type u
x y : Cardinal
hx1 : x ≠ 0
hy1 : y ≠ 0
hx2 : ℵ₀ ≤ x
⊢ ℵ₀ ≤ x * y
exact aleph0_le_mul_iff'.2 (Or.inr ⟨hx2, hy1⟩)