-- Mathlib/SetTheory/Cardinal/Arithmetic.lean
theorem mul_eq_left_iff {a b : Cardinal} : a * b = a ↔ max ℵ₀ b ≤ a ∧ b ≠ 0 ∨ b = 1 ∨ a = 0

Proof state:
a b : Cardinal.{u_1}
⊢ a * b = a ↔ ℵ₀ ⊔ b ≤ a ∧ b ≠ 0 ∨ b = 1 ∨ a = 0

Tactic:
rw [max_le_iff]

Result:
a b : Cardinal.{u_1}
⊢ a * b = a ↔ (ℵ₀ ≤ a ∧ b ≤ a) ∧ b ≠ 0 ∨ b = 1 ∨ a = 0

Proof state:
n m : ℕ
h2a : 1 ≤ n
hb : 1 ≤ m
h : n * m = n
⊢ ¬1 < m

Tactic:
apply fun h2b => ne_of_gt _ h

Result:
n m : ℕ
h2a : 1 ≤ n
hb : 1 ≤ m
h : n * m = n
⊢ 1 < m → n < n * m

Proof state:
case refine_2.inr.inl
a : Cardinal.{u_1}
⊢ a * 1 = a

case refine_2.inr.inr
b : Cardinal.{u_1}
⊢ 0 * b = 0

Tactic:
all_goals simp

Result:
no goals

Proof state:
n m : ℕ
h2a : 1 ≤ n
hb : 1 ≤ m
h : n * m = n
⊢ 0 < n

Tactic:
apply Nat.lt_of_succ_le h2a

Result:
no goals

Proof state:
case neg.h
a b : Cardinal.{u_1}
h : a * b = a
ha : a < ℵ₀
h2a : ¬a = 0
hb : b ≠ 0
⊢ b = 1

Tactic:
rw [← h, mul_lt_aleph0_iff, lt_aleph0, lt_aleph0] at ha

Result:
case neg.h
a b : Cardinal.{u_1}
h : a * b = a
ha : a = 0 ∨ b = 0 ∨ (∃ n, a = ↑n) ∧ ∃ n, b = ↑n
h2a : ¬a = 0
hb : b ≠ 0
⊢ b = 1

Proof state:
case neg.h.inr.inr.intro.intro.intro
n : ℕ
h2a : 1 ≤ ↑n
m : ℕ
hb : 1 ≤ ↑m
h : ↑n * ↑m = ↑n
⊢ ↑m = 1

Tactic:
norm_cast at h2a hb h ⊢

Result:
case neg.h.inr.inr.intro.intro.intro
n m : ℕ
h2a : 1 ≤ n
hb : 1 ≤ m
h : n * m = n
⊢ m = 1

Proof state:
case refine_1.inr.h
a b : Cardinal.{u_1}
h : a * b = a
ha : a < ℵ₀
⊢ b = 1 ∨ a = 0

Tactic:
by_cases h2a : a = 0

Result:
case pos
a b : Cardinal.{u_1}
h : a * b = a
ha : a < ℵ₀
h2a : a = 0
⊢ b = 1 ∨ a = 0

case neg
a b : Cardinal.{u_1}
h : a * b = a
ha : a < ℵ₀
h2a : ¬a = 0
⊢ b = 1 ∨ a = 0

Proof state:
case refine_1.inl.h
a b : Cardinal.{u_1}
h : a * b = a
ha : ℵ₀ ≤ a
this : a ≠ 0
⊢ ℵ₀ ≤ a ∧ b ≤ a ∧ b ≠ 0

Tactic:
use ha

Result:
case right
a b : Cardinal.{u_1}
h : a * b = a
ha : ℵ₀ ≤ a
this : a ≠ 0
⊢ b ≤ a ∧ b ≠ 0

Proof state:
case neg.h
a b : Cardinal.{u_1}
h : a * b = a
ha : a = 0 ∨ b = 0 ∨ (∃ n, a = ↑n) ∧ ∃ n, b = ↑n
h2a : ¬a = 0
hb : b ≠ 0
⊢ b = 1

Tactic:
rcases ha with (rfl | rfl | ⟨⟨n, rfl⟩, ⟨m, rfl⟩⟩)

Result:
case neg.h.inl
b : Cardinal.{u_1}
hb : b ≠ 0
h : 0 * b = 0
h2a : ¬0 = 0
⊢ b = 1

case neg.h.inr.inl
a : Cardinal.{u_1}
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

Proof state:
a b : Cardinal.{u_1}
h : a * b = a
ha : ℵ₀ ≤ a
⊢ a ≠ 0

Tactic:
rintro rfl

Result:
b : Cardinal.{u_1}
h : 0 * b = 0
ha : ℵ₀ ≤ 0
⊢ False

Proof state:
case neg.h.inr.inr.intro.intro.intro
n : ℕ
h2a : ↑n ≠ 0
m : ℕ
hb : ↑m ≠ 0
h : ↑n * ↑m = ↑n
⊢ ↑m = 1

Tactic:
rw [← one_le_iff_ne_zero] at h2a hb

Result:
case neg.h.inr.inr.intro.intro.intro
n : ℕ
h2a : 1 ≤ ↑n
m : ℕ
hb : 1 ≤ ↑m
h : ↑n * ↑m = ↑n
⊢ ↑m = 1

Proof state:
case right.left
a b : Cardinal.{u_1}
h : a * b = a
ha : ℵ₀ ≤ a
this : a ≠ 0
⊢ b ≤ a

Tactic:
rw [← not_lt]

Result:
case right.left
a b : Cardinal.{u_1}
h : a * b = a
ha : ℵ₀ ≤ a
this : a ≠ 0
⊢ ¬a < b

Proof state:
case right.right
a : Cardinal.{u_1}
ha : ℵ₀ ≤ a
this : a ≠ 0
h : a * 0 = a
⊢ a = 0

Tactic:
rw [mul_zero] at h

Result:
case right.right
a : Cardinal.{u_1}
ha : ℵ₀ ≤ a
this : a ≠ 0
h : 0 = a
⊢ a = 0

Proof state:
case refine_2
a b : Cardinal.{u_1}
⊢ (ℵ₀ ≤ a ∧ b ≤ a) ∧ b ≠ 0 ∨ b = 1 ∨ a = 0 → a * b = a

Tactic:
rintro (⟨⟨ha, hab⟩, hb⟩ | rfl | rfl)

Result:
case refine_2.inl.intro.intro
a b : Cardinal.{u_1}
hb : b ≠ 0
ha : ℵ₀ ≤ a
hab : b ≤ a
⊢ a * b = a

case refine_2.inr.inl
a : Cardinal.{u_1}
⊢ a * 1 = a

case refine_2.inr.inr
b : Cardinal.{u_1}
⊢ 0 * b = 0

Proof state:
case neg
a b : Cardinal.{u_1}
h : a * b = a
ha : a < ℵ₀
h2a : ¬a = 0
⊢ b = 1 ∨ a = 0

Tactic:
have hb : b ≠ 0 := by
  rintro rfl
  apply h2a
  rw [mul_zero] at h
  exact h.symm

Result:
case neg
a b : Cardinal.{u_1}
h : a * b = a
ha : a < ℵ₀
h2a : ¬a = 0
hb : b ≠ 0
⊢ b = 1 ∨ a = 0

Proof state:
case refine_1.inl.h
a b : Cardinal.{u_1}
h : a * b = a
ha : ℵ₀ ≤ a
this : a ≠ 0
⊢ (ℵ₀ ≤ a ∧ b ≤ a) ∧ b ≠ 0

Tactic:
rw [and_assoc]

Result:
case refine_1.inl.h
a b : Cardinal.{u_1}
h : a * b = a
ha : ℵ₀ ≤ a
this : a ≠ 0
⊢ ℵ₀ ≤ a ∧ b ≤ a ∧ b ≠ 0

Proof state:
case neg.h.inl
b : Cardinal.{u_1}
hb : b ≠ 0
h : 0 * b = 0
h2a : ¬0 = 0
⊢ b = 1

Tactic:
contradiction

Result:
no goals

Proof state:
a : Cardinal.{u_1}
ha : a < ℵ₀
h2a : ¬a = 0
h : a * 0 = a
⊢ False

Tactic:
apply h2a

Result:
a : Cardinal.{u_1}
ha : a < ℵ₀
h2a : ¬a = 0
h : a * 0 = a
⊢ a = 0

Proof state:
case neg.h.inr.inl
a : Cardinal.{u_1}
h2a : ¬a = 0
h : a * 0 = a
hb : 0 ≠ 0
⊢ 0 = 1

Tactic:
contradiction

Result:
no goals

Proof state:
n m : ℕ
h2a : 1 ≤ n
hb : 1 ≤ m
h : n * m = n
⊢ 1 < m → n < n * m

Tactic:
conv_rhs => left; rw [← mul_one n]

Result:
n m : ℕ
h2a : 1 ≤ n
hb : 1 ≤ m
h : n * m = n
⊢ 1 < m → n * 1 < n * m

Proof state:
case pos
a b : Cardinal.{u_1}
h : a * b = a
ha : a < ℵ₀
h2a : a = 0
⊢ b = 1 ∨ a = 0

Tactic:
exact Or.inr h2a

Result:
no goals

Proof state:
case refine_1.inl
a b : Cardinal.{u_1}
h : a * b = a
ha : ℵ₀ ≤ a
⊢ (ℵ₀ ≤ a ∧ b ≤ a) ∧ b ≠ 0 ∨ b = 1 ∨ a = 0

Tactic:
have : a ≠ 0 := by
  rintro rfl
  exact ha.not_lt aleph0_pos

Result:
case refine_1.inl
a b : Cardinal.{u_1}
h : a * b = a
ha : ℵ₀ ≤ a
this : a ≠ 0
⊢ (ℵ₀ ≤ a ∧ b ≤ a) ∧ b ≠ 0 ∨ b = 1 ∨ a = 0

Proof state:
n m : ℕ
h2a : 1 ≤ n
hb : 1 ≤ m
h : n * m = n
⊢ 1 < m → 1 < m

Tactic:
exact id

Result:
no goals

Proof state:
n m : ℕ
h2a : 1 ≤ n
hb : 1 ≤ m
h : n * m = n
⊢ 1 < m → n * 1 < n * m

Tactic:
rw [Nat.mul_lt_mul_left]

Result:
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

Proof state:
case neg.h.inr.inr.intro.intro.intro
n m : ℕ
h2a : 1 ≤ n
hb : 1 ≤ m
h : n * m = n
⊢ m = 1

Tactic:
apply le_antisymm _ hb

Result:
n m : ℕ
h2a : 1 ≤ n
hb : 1 ≤ m
h : n * m = n
⊢ m ≤ 1

Proof state:
a b : Cardinal.{u_1}
h : a * b = a
ha : a < ℵ₀
h2a : ¬a = 0
⊢ b ≠ 0

Tactic:
rintro rfl

Result:
a : Cardinal.{u_1}
ha : a < ℵ₀
h2a : ¬a = 0
h : a * 0 = a
⊢ False

Proof state:
a : Cardinal.{u_1}
ha : a < ℵ₀
h2a : ¬a = 0
h : a * 0 = a
⊢ a = 0

Tactic:
rw [mul_zero] at h

Result:
a : Cardinal.{u_1}
ha : a < ℵ₀
h2a : ¬a = 0
h : 0 = a
⊢ a = 0

Proof state:
case right.right
a : Cardinal.{u_1}
ha : ℵ₀ ≤ a
this : a ≠ 0
h : a * 0 = a
⊢ False

Tactic:
apply this

Result:
case right.right
a : Cardinal.{u_1}
ha : ℵ₀ ≤ a
this : a ≠ 0
h : a * 0 = a
⊢ a = 0

Proof state:
a : Cardinal.{u_1}
ha : a < ℵ₀
h2a : ¬a = 0
h : 0 = a
⊢ a = 0

Tactic:
exact h.symm

Result:
no goals

Proof state:
case right.left
a b : Cardinal.{u_1}
h : a * b = a
ha : ℵ₀ ≤ a
this : a ≠ 0
⊢ ¬a < b

Tactic:
exact fun hb => ne_of_gt (hb.trans_le (le_mul_left this)) h

Result:
no goals

Proof state:
case neg
a b : Cardinal.{u_1}
h : a * b = a
ha : a < ℵ₀
h2a : ¬a = 0
hb : b ≠ 0
⊢ b = 1 ∨ a = 0

Tactic:
left

Result:
case neg.h
a b : Cardinal.{u_1}
h : a * b = a
ha : a < ℵ₀
h2a : ¬a = 0
hb : b ≠ 0
⊢ b = 1

Proof state:
case refine_2.inl.intro.intro
a b : Cardinal.{u_1}
hb : b ≠ 0
ha : ℵ₀ ≤ a
hab : b ≤ a
⊢ a * b = a

Tactic:
rw [mul_eq_max_of_aleph0_le_left ha hb, max_eq_left hab]

Result:
no goals

Proof state:
case refine_1
a b : Cardinal.{u_1}
h : a * b = a
⊢ (ℵ₀ ≤ a ∧ b ≤ a) ∧ b ≠ 0 ∨ b = 1 ∨ a = 0

Tactic:
rcases le_or_lt ℵ₀ a with ha | ha

Result:
case refine_1.inl
a b : Cardinal.{u_1}
h : a * b = a
ha : ℵ₀ ≤ a
⊢ (ℵ₀ ≤ a ∧ b ≤ a) ∧ b ≠ 0 ∨ b = 1 ∨ a = 0

case refine_1.inr
a b : Cardinal.{u_1}
h : a * b = a
ha : a < ℵ₀
⊢ (ℵ₀ ≤ a ∧ b ≤ a) ∧ b ≠ 0 ∨ b = 1 ∨ a = 0

Proof state:
case refine_2.inr.inr
b : Cardinal.{u_1}
⊢ 0 * b = 0

Tactic:
simp

Result:
no goals

Proof state:
case refine_1.inl
a b : Cardinal.{u_1}
h : a * b = a
ha : ℵ₀ ≤ a
this : a ≠ 0
⊢ (ℵ₀ ≤ a ∧ b ≤ a) ∧ b ≠ 0 ∨ b = 1 ∨ a = 0

Tactic:
left

Result:
case refine_1.inl.h
a b : Cardinal.{u_1}
h : a * b = a
ha : ℵ₀ ≤ a
this : a ≠ 0
⊢ (ℵ₀ ≤ a ∧ b ≤ a) ∧ b ≠ 0

Proof state:
b : Cardinal.{u_1}
h : 0 * b = 0
ha : ℵ₀ ≤ 0
⊢ False

Tactic:
exact ha.not_lt aleph0_pos

Result:
no goals