a b : Cardinal
n m : ℕ
ha : ℵ₀ ≤ a
⊢ ¬¬IsUnit a ∨ ¬∀ (a_1 b : Cardinal), a = a_1 * b → IsUnit a_1 ∨ IsUnit b
a b : Cardinal
n m : ℕ
ha : ℵ₀ ≤ a
⊢ ¬Irreducible a
rw [irreducible_iff, not_and_or]
a b : Cardinal
n m : ℕ
ha : ℵ₀ ≤ a
h : ∀ (a_1 b : Cardinal), a = a_1 * b → IsUnit a_1 ∨ IsUnit b
⊢ False
a b : Cardinal
n m : ℕ
ha : ℵ₀ ≤ a
⊢ ¬¬IsUnit a ∨ ¬∀ (a_1 b : Cardinal), a = a_1 * b → IsUnit a_1 ∨ IsUnit b
refine' Or.inr fun h => _
no goals
a b : Cardinal
n m : ℕ
ha : ℵ₀ ≤ a
h : ∀ (a_1 b : Cardinal), a = a_1 * b → IsUnit a_1 ∨ IsUnit b
⊢ False
simpa [mul_aleph0_eq ha, isUnit_iff, (one_lt_aleph0.trans_le ha).ne', one_lt_aleph0.ne'] using
  h a ℵ₀