English
The statement a · b = a is characterized by a condition: either max(ℵ₀, b) ≤ a and b ≠ 0, or b = 1, or a = 0.
Русский
Уравнение a · b = a эквивалентно условию: либо max(ℵ₀, b) ≤ a и b ≠ 0, либо b = 1, либо a = 0.
LaTeX
$$$$ a \cdot b = a \iff \Big( \max(\aleph_0, b) \le a \land b \neq 0 \Big) \lor (b = 1) \lor (a = 0) $$$$
Lean4
theorem mul_eq_left_iff {a b : Cardinal} : a * b = a ↔ max ℵ₀ b ≤ a ∧ b ≠ 0 ∨ b = 1 ∨ a = 0 :=
by
rw [max_le_iff]
refine ⟨fun h => ?_, ?_⟩
· rcases le_or_gt ℵ₀ a with ha | ha
· have : a ≠ 0 := by
rintro rfl
exact ha.not_gt aleph0_pos
left
rw [and_assoc]
use ha
constructor
· rw [← not_lt]
exact fun hb => ne_of_gt (hb.trans_le (le_mul_left this)) h
· rintro rfl
apply this
rw [mul_zero] at h
exact h.symm
right
by_cases h2a : a = 0
· exact Or.inr h2a
have hb : b ≠ 0 := by
rintro rfl
apply h2a
rw [mul_zero] at h
exact h.symm
left
rw [← h, mul_lt_aleph0_iff, lt_aleph0, lt_aleph0] at ha
rcases ha with (rfl | rfl | ⟨⟨n, rfl⟩, ⟨m, rfl⟩⟩)
· contradiction
· contradiction
rw [← Ne] at h2a
rw [← one_le_iff_ne_zero] at h2a hb
norm_cast at h2a hb h ⊢
apply le_antisymm _ hb
rw [← not_lt]
apply fun h2b => ne_of_gt _ h
conv_rhs => left; rw [← mul_one n]
rw [Nat.mul_lt_mul_left]
· exact id
apply Nat.lt_of_succ_le h2a
· rintro (⟨⟨ha, hab⟩, hb⟩ | rfl | rfl)
· rw [mul_eq_max_of_aleph0_le_left ha hb, max_eq_left hab]
all_goals simp
