English
Prime (n.cast) in cardinal sense corresponds to Nat.Prime(n).
Русский
Простое в кардинальном смысле числа n равно Nat.Prime(n).
LaTeX
$$$\mathrm{Prime}(n.cast) \iff \mathrm{Nat.Prime}(n)$$$
Lean4
@[simp]
theorem nat_is_prime_iff : Prime (n : Cardinal) ↔ n.Prime :=
by
simp only [Prime, Nat.prime_iff]
refine and_congr (by simp) (and_congr ?_ ⟨fun h b c hbc => ?_, fun h b c hbc => ?_⟩)
· simp only [isUnit_iff, Nat.isUnit_iff]
exact mod_cast Iff.rfl
· exact mod_cast h b c (mod_cast hbc)
rcases lt_or_ge (b * c) ℵ₀ with h' | h'
· rcases mul_lt_aleph0_iff.mp h' with (rfl | rfl | ⟨hb, hc⟩)
· simp
· simp
lift b to ℕ using hb
lift c to ℕ using hc
exact mod_cast h b c (mod_cast hbc)
rcases aleph0_le_mul_iff.mp h' with ⟨hb, hc, hℵ₀⟩
have hn : (n : Cardinal) ≠ 0 := by
intro h
rw [h, zero_dvd_iff, mul_eq_zero] at hbc
cases hbc <;> contradiction
wlog hℵ₀b : ℵ₀ ≤ b
apply (this h c b _ _ hc hb hℵ₀.symm hn (hℵ₀.resolve_left hℵ₀b)).symm <;> try assumption
· rwa [mul_comm] at hbc
· rwa [mul_comm] at h'
· exact Or.inl (dvd_of_le_of_aleph0_le hn ((nat_lt_aleph0 n).le.trans hℵ₀b) hℵ₀b)
