a b : Cardinal
⊢ a * b = a ↔ (ℵ₀ ≤ a ∧ b ≤ a) ∧ b ≠ 0 ∨ b = 1 ∨ a = 0
a b : Cardinal
⊢ a * b = a ↔ max ℵ₀ b ≤ a ∧ b ≠ 0 ∨ b = 1 ∨ a = 0
rw [max_le_iff]
case refine'_1
a b : Cardinal
h : a * b = a
⊢ (ℵ₀ ≤ a ∧ b ≤ a) ∧ b ≠ 0 ∨ b = 1 ∨ a = 0

case refine'_2
a b : Cardinal
⊢ (ℵ₀ ≤ a ∧ b ≤ a) ∧ b ≠ 0 ∨ b = 1 ∨ a = 0 → a * b = a
a b : Cardinal
⊢ a * b = a ↔ (ℵ₀ ≤ a ∧ b ≤ a) ∧ b ≠ 0 ∨ b = 1 ∨ a = 0
refine' ⟨fun h => _, _⟩
case refine'_1.inl
a b : Cardinal
h : a * b = a
ha : ℵ₀ ≤ a
⊢ (ℵ₀ ≤ a ∧ b ≤ a) ∧ b ≠ 0 ∨ b = 1 ∨ a = 0

case refine'_1.inr
a b : Cardinal
h : a * b = a
ha : a < ℵ₀
⊢ (ℵ₀ ≤ a ∧ b ≤ a) ∧ b ≠ 0 ∨ b = 1 ∨ a = 0
case refine'_1
a b : Cardinal
h : a * b = a
⊢ (ℵ₀ ≤ a ∧ b ≤ a) ∧ b ≠ 0 ∨ b = 1 ∨ a = 0
cases' le_or_lt ℵ₀ a with ha ha
case refine'_1.inr.h
a b : Cardinal
h : a * b = a
ha : a < ℵ₀
⊢ b = 1 ∨ a = 0
case refine'_1.inr
a b : Cardinal
h : a * b = a
ha : a < ℵ₀
⊢ (ℵ₀ ≤ a ∧ b ≤ a) ∧ b ≠ 0 ∨ b = 1 ∨ a = 0
right
case pos
a b : Cardinal
h : a * b = a
ha : a < ℵ₀
h2a : a = 0
⊢ b = 1 ∨ a = 0

case neg
a b : Cardinal
h : a * b = a
ha : a < ℵ₀
h2a : ¬a = 0
⊢ b = 1 ∨ a = 0
case refine'_1.inr.h
a b : Cardinal
h : a * b = a
ha : a < ℵ₀
⊢ b = 1 ∨ a = 0
by_cases h2a : a = 0
case neg
a b : Cardinal
h : a * b = a
ha : a < ℵ₀
h2a : ¬a = 0
hb : b ≠ 0
⊢ b = 1 ∨ a = 0
case neg
a b : Cardinal
h : a * b = a
ha : a < ℵ₀
h2a : ¬a = 0
⊢ b = 1 ∨ a = 0
have hb : b ≠ 0 := by
  rintro rfl
  apply h2a
  rw [mul_zero] at h
  exact h.symm
case neg.h
a b : Cardinal
h : a * b = a
ha : a < ℵ₀
h2a : ¬a = 0
hb : b ≠ 0
⊢ b = 1
case neg
a b : Cardinal
h : a * b = a
ha : a < ℵ₀
h2a : ¬a = 0
hb : b ≠ 0
⊢ b = 1 ∨ a = 0
left
case neg.h
a b : Cardinal
h : a * b = a
ha : a = 0 ∨ b = 0 ∨ (∃ n, a = ↑n) ∧ ∃ n, b = ↑n
h2a : ¬a = 0
hb : b ≠ 0
⊢ b = 1
case neg.h
a b : Cardinal
h : a * b = a
ha : a < ℵ₀
h2a : ¬a = 0
hb : b ≠ 0
⊢ b = 1
rw [← h, mul_lt_aleph0_iff, lt_aleph0, lt_aleph0] at ha
case neg.h.inl
b : Cardinal
hb : b ≠ 0
h : 0 * b = 0
h2a : ¬0 = 0
⊢ b = 1

case neg.h.inr.inl
a : Cardinal
h2a : ¬a = 0
h : a * 0 = a
hb : 0 ≠ 0
⊢ 0 = 1

case neg.h.inr.inr.intro.intro.intro
n : ℕ
h2a : ¬↑n = 0
m : ℕ
hb : ↑m ≠ 0
h : ↑n * ↑m = ↑n
⊢ ↑m = 1
case neg.h
a b : Cardinal
h : a * b = a
ha : a = 0 ∨ b = 0 ∨ (∃ n, a = ↑n) ∧ ∃ n, b = ↑n
h2a : ¬a = 0
hb : b ≠ 0
⊢ b = 1
rcases ha with (rfl | rfl | ⟨⟨n, rfl⟩, ⟨m, rfl⟩⟩)
case neg.h.inr.inl
a : Cardinal
h2a : ¬a = 0
h : a * 0 = a
hb : 0 ≠ 0
⊢ 0 = 1

case neg.h.inr.inr.intro.intro.intro
n : ℕ
h2a : ¬↑n = 0
m : ℕ
hb : ↑m ≠ 0
h : ↑n * ↑m = ↑n
⊢ ↑m = 1
case neg.h.inl
b : Cardinal
hb : b ≠ 0
h : 0 * b = 0
h2a : ¬0 = 0
⊢ b = 1

case neg.h.inr.inl
a : Cardinal
h2a : ¬a = 0
h : a * 0 = a
hb : 0 ≠ 0
⊢ 0 = 1

case neg.h.inr.inr.intro.intro.intro
n : ℕ
h2a : ¬↑n = 0
m : ℕ
hb : ↑m ≠ 0
h : ↑n * ↑m = ↑n
⊢ ↑m = 1
contradiction
case neg.h.inr.inr.intro.intro.intro
n : ℕ
h2a : ¬↑n = 0
m : ℕ
hb : ↑m ≠ 0
h : ↑n * ↑m = ↑n
⊢ ↑m = 1
case neg.h.inr.inl
a : Cardinal
h2a : ¬a = 0
h : a * 0 = a
hb : 0 ≠ 0
⊢ 0 = 1

case neg.h.inr.inr.intro.intro.intro
n : ℕ
h2a : ¬↑n = 0
m : ℕ
hb : ↑m ≠ 0
h : ↑n * ↑m = ↑n
⊢ ↑m = 1
contradiction
case neg.h.inr.inr.intro.intro.intro
n : ℕ
h2a : ↑n ≠ 0
m : ℕ
hb : ↑m ≠ 0
h : ↑n * ↑m = ↑n
⊢ ↑m = 1
case neg.h.inr.inr.intro.intro.intro
n : ℕ
h2a : ¬↑n = 0
m : ℕ
hb : ↑m ≠ 0
h : ↑n * ↑m = ↑n
⊢ ↑m = 1
rw [← Ne] at h2a
case neg.h.inr.inr.intro.intro.intro
n : ℕ
h2a : 1 ≤ ↑n
m : ℕ
hb : 1 ≤ ↑m
h : ↑n * ↑m = ↑n
⊢ ↑m = 1
case neg.h.inr.inr.intro.intro.intro
n : ℕ
h2a : ↑n ≠ 0
m : ℕ
hb : ↑m ≠ 0
h : ↑n * ↑m = ↑n
⊢ ↑m = 1
rw [← one_le_iff_ne_zero] at h2a hb
case neg.h.inr.inr.intro.intro.intro
n m : ℕ
h2a : 1 ≤ n
hb : 1 ≤ m
h : n * m = n
⊢ m = 1
case neg.h.inr.inr.intro.intro.intro
n : ℕ
h2a : 1 ≤ ↑n
m : ℕ
hb : 1 ≤ ↑m
h : ↑n * ↑m = ↑n
⊢ ↑m = 1
norm_cast  at h2a hb h⊢
n m : ℕ
h2a : 1 ≤ n
hb : 1 ≤ m
h : n * m = n
⊢ m ≤ 1
case neg.h.inr.inr.intro.intro.intro
n m : ℕ
h2a : 1 ≤ n
hb : 1 ≤ m
h : n * m = n
⊢ m = 1
apply le_antisymm _ hb
n m : ℕ
h2a : 1 ≤ n
hb : 1 ≤ m
h : n * m = n
⊢ ¬1 < m
n m : ℕ
h2a : 1 ≤ n
hb : 1 ≤ m
h : n * m = n
⊢ m ≤ 1
rw [← not_lt]
n m : ℕ
h2a : 1 ≤ n
hb : 1 ≤ m
h : n * m = n
⊢ 1 < m → n < n * m
n m : ℕ
h2a : 1 ≤ n
hb : 1 ≤ m
h : n * m = n
⊢ ¬1 < m
apply fun h2b => ne_of_gt _ h
n m : ℕ
h2a : 1 ≤ n
hb : 1 ≤ m
h : n * m = n
⊢ 1 < m → n * 1 < n * m
n m : ℕ
h2a : 1 ≤ n
hb : 1 ≤ m
h : n * m = n
⊢ 1 < m → n < n * m
conv_rhs => left; rw [← mul_one n]
n m : ℕ
h2a : 1 ≤ n
hb : 1 ≤ m
h : n * m = n
⊢ 1 < m → 1 < m

n m : ℕ
h2a : 1 ≤ n
hb : 1 ≤ m
h : n * m = n
⊢ 0 < n
n m : ℕ
h2a : 1 ≤ n
hb : 1 ≤ m
h : n * m = n
⊢ 1 < m → n * 1 < n * m
rw [mul_lt_mul_left]
n m : ℕ
h2a : 1 ≤ n
hb : 1 ≤ m
h : n * m = n
⊢ 0 < n
n m : ℕ
h2a : 1 ≤ n
hb : 1 ≤ m
h : n * m = n
⊢ 1 < m → 1 < m

n m : ℕ
h2a : 1 ≤ n
hb : 1 ≤ m
h : n * m = n
⊢ 0 < n
exact id
no goals
n m : ℕ
h2a : 1 ≤ n
hb : 1 ≤ m
h : n * m = n
⊢ 0 < n
apply Nat.lt_of_succ_le h2a
case refine'_1.inl
a b : Cardinal
h : a * b = a
ha : ℵ₀ ≤ a
this : a ≠ 0
⊢ (ℵ₀ ≤ a ∧ b ≤ a) ∧ b ≠ 0 ∨ b = 1 ∨ a = 0
case refine'_1.inl
a b : Cardinal
h : a * b = a
ha : ℵ₀ ≤ a
⊢ (ℵ₀ ≤ a ∧ b ≤ a) ∧ b ≠ 0 ∨ b = 1 ∨ a = 0
have : a ≠ 0 := by
  rintro rfl
  exact ha.not_lt aleph0_pos
case refine'_1.inl.h
a b : Cardinal
h : a * b = a
ha : ℵ₀ ≤ a
this : a ≠ 0
⊢ (ℵ₀ ≤ a ∧ b ≤ a) ∧ b ≠ 0
case refine'_1.inl
a b : Cardinal
h : a * b = a
ha : ℵ₀ ≤ a
this : a ≠ 0
⊢ (ℵ₀ ≤ a ∧ b ≤ a) ∧ b ≠ 0 ∨ b = 1 ∨ a = 0
left
case refine'_1.inl.h
a b : Cardinal
h : a * b = a
ha : ℵ₀ ≤ a
this : a ≠ 0
⊢ ℵ₀ ≤ a ∧ b ≤ a ∧ b ≠ 0
case refine'_1.inl.h
a b : Cardinal
h : a * b = a
ha : ℵ₀ ≤ a
this : a ≠ 0
⊢ (ℵ₀ ≤ a ∧ b ≤ a) ∧ b ≠ 0
rw [and_assoc]
case refine'_1.inl.h
a b : Cardinal
h : a * b = a
ha : ℵ₀ ≤ a
this : a ≠ 0
⊢ b ≤ a ∧ b ≠ 0
case refine'_1.inl.h
a b : Cardinal
h : a * b = a
ha : ℵ₀ ≤ a
this : a ≠ 0
⊢ ℵ₀ ≤ a ∧ b ≤ a ∧ b ≠ 0
use ha
case refine'_1.inl.h.left
a b : Cardinal
h : a * b = a
ha : ℵ₀ ≤ a
this : a ≠ 0
⊢ b ≤ a

case refine'_1.inl.h.right
a b : Cardinal
h : a * b = a
ha : ℵ₀ ≤ a
this : a ≠ 0
⊢ b ≠ 0
case refine'_1.inl.h
a b : Cardinal
h : a * b = a
ha : ℵ₀ ≤ a
this : a ≠ 0
⊢ b ≤ a ∧ b ≠ 0
constructor
b : Cardinal
h : 0 * b = 0
ha : ℵ₀ ≤ 0
⊢ False
a b : Cardinal
h : a * b = a
ha : ℵ₀ ≤ a
⊢ a ≠ 0
rintro rfl
no goals
b : Cardinal
h : 0 * b = 0
ha : ℵ₀ ≤ 0
⊢ False
exact ha.not_lt aleph0_pos
case refine'_1.inl.h.left
a b : Cardinal
h : a * b = a
ha : ℵ₀ ≤ a
this : a ≠ 0
⊢ ¬a < b
case refine'_1.inl.h.left
a b : Cardinal
h : a * b = a
ha : ℵ₀ ≤ a
this : a ≠ 0
⊢ b ≤ a
rw [← not_lt]
no goals
case refine'_1.inl.h.left
a b : Cardinal
h : a * b = a
ha : ℵ₀ ≤ a
this : a ≠ 0
⊢ ¬a < b
exact fun hb => ne_of_gt (hb.trans_le (le_mul_left this)) h
case refine'_1.inl.h.right
a : Cardinal
ha : ℵ₀ ≤ a
this : a ≠ 0
h : a * 0 = a
⊢ False
case refine'_1.inl.h.right
a b : Cardinal
h : a * b = a
ha : ℵ₀ ≤ a
this : a ≠ 0
⊢ b ≠ 0
rintro rfl
case refine'_1.inl.h.right
a : Cardinal
ha : ℵ₀ ≤ a
this : a ≠ 0
h : a * 0 = a
⊢ a = 0
case refine'_1.inl.h.right
a : Cardinal
ha : ℵ₀ ≤ a
this : a ≠ 0
h : a * 0 = a
⊢ False
apply this
case refine'_1.inl.h.right
a : Cardinal
ha : ℵ₀ ≤ a
this : a ≠ 0
h : 0 = a
⊢ a = 0
case refine'_1.inl.h.right
a : Cardinal
ha : ℵ₀ ≤ a
this : a ≠ 0
h : a * 0 = a
⊢ a = 0
rw [mul_zero] at h
no goals
case refine'_1.inl.h.right
a : Cardinal
ha : ℵ₀ ≤ a
this : a ≠ 0
h : 0 = a
⊢ a = 0
exact h.symm
no goals
case pos
a b : Cardinal
h : a * b = a
ha : a < ℵ₀
h2a : a = 0
⊢ b = 1 ∨ a = 0
exact Or.inr h2a
a : Cardinal
ha : a < ℵ₀
h2a : ¬a = 0
h : a * 0 = a
⊢ False
a b : Cardinal
h : a * b = a
ha : a < ℵ₀
h2a : ¬a = 0
⊢ b ≠ 0
rintro rfl
a : Cardinal
ha : a < ℵ₀
h2a : ¬a = 0
h : a * 0 = a
⊢ a = 0
a : Cardinal
ha : a < ℵ₀
h2a : ¬a = 0
h : a * 0 = a
⊢ False
apply h2a
a : Cardinal
ha : a < ℵ₀
h2a : ¬a = 0
h : 0 = a
⊢ a = 0
a : Cardinal
ha : a < ℵ₀
h2a : ¬a = 0
h : a * 0 = a
⊢ a = 0
rw [mul_zero] at h
no goals
a : Cardinal
ha : a < ℵ₀
h2a : ¬a = 0
h : 0 = a
⊢ a = 0
exact h.symm
case refine'_2.inl.intro.intro
a b : Cardinal
hb : b ≠ 0
ha : ℵ₀ ≤ a
hab : b ≤ a
⊢ a * b = a

case refine'_2.inr.inl
a : Cardinal
⊢ a * 1 = a

case refine'_2.inr.inr
b : Cardinal
⊢ 0 * b = 0
case refine'_2
a b : Cardinal
⊢ (ℵ₀ ≤ a ∧ b ≤ a) ∧ b ≠ 0 ∨ b = 1 ∨ a = 0 → a * b = a
rintro (⟨⟨ha, hab⟩, hb⟩ | rfl | rfl)
no goals
case refine'_2.inr.inl
a : Cardinal
⊢ a * 1 = a

case refine'_2.inr.inr
b : Cardinal
⊢ 0 * b = 0
all_goals simp
no goals
case refine'_2.inl.intro.intro
a b : Cardinal
hb : b ≠ 0
ha : ℵ₀ ≤ a
hab : b ≤ a
⊢ a * b = a
rw [mul_eq_max_of_aleph0_le_left ha hb, max_eq_left hab]
no goals
case refine'_2.inr.inr
b : Cardinal
⊢ 0 * b = 0
simp