-- Mathlib/SetTheory/Cardinal/Arithmetic.lean
theorem add_eq_left_iff {a b : Cardinal} : a + b = a ↔ max ℵ₀ b ≤ a ∨ b = 0

Proof state:
a b : Cardinal.{u_1}
h : a + b = a
ha : ℵ₀ ≤ a
⊢ a < b → a < a + b

Tactic:
intro hb

Result:
a b : Cardinal.{u_1}
h : a + b = a
ha : ℵ₀ ≤ a
hb : a < b
⊢ a < a + b

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

Tactic:
left

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

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

Tactic:
right

Result:
case refine_1.inr.h
a b : Cardinal.{u_1}
h : a + b = a
ha : a < ℵ₀
⊢ b = 0

Proof state:
case refine_1.inr.h.intro.intro.intro
n m : ℕ
h : ↑n + ↑m = ↑n
⊢ ↑m = 0

Tactic:
norm_cast at h ⊢

Result:
case refine_1.inr.h.intro.intro.intro
n m : ℕ
h : n + m = n
⊢ m = 0

Proof state:
a b : Cardinal.{u_1}
⊢ a + b = a ↔ ℵ₀ ⊔ b ≤ a ∨ b = 0

Tactic:
rw [max_le_iff]

Result:
a b : Cardinal.{u_1}
⊢ a + b = a ↔ ℵ₀ ≤ a ∧ b ≤ a ∨ b = 0

Proof state:
case refine_2.inr
a b : Cardinal.{u_1}
h3 : b = 0
⊢ a + b = a

Tactic:
rw [h3, add_zero]

Result:
no goals

Proof state:
a b : Cardinal.{u_1}
⊢ a + b = a ↔ ℵ₀ ≤ a ∧ b ≤ a ∨ b = 0

Tactic:
refine ⟨fun h => ?_, ?_⟩

Result:
case refine_1
a b : Cardinal.{u_1}
h : a + b = a
⊢ ℵ₀ ≤ a ∧ b ≤ a ∨ b = 0

case refine_2
a b : Cardinal.{u_1}
⊢ ℵ₀ ≤ a ∧ b ≤ a ∨ b = 0 → a + b = a

Proof state:
case refine_1.inr.h
a b : Cardinal.{u_1}
h : a + b = a
ha : (∃ n, a = ↑n) ∧ ∃ n, b = ↑n
⊢ b = 0

Tactic:
rcases ha with ⟨⟨n, rfl⟩, ⟨m, rfl⟩⟩

Result:
case refine_1.inr.h.intro.intro.intro
n m : ℕ
h : ↑n + ↑m = ↑n
⊢ ↑m = 0

Proof state:
case refine_1
a b : Cardinal.{u_1}
h : a + b = a
⊢ ℵ₀ ≤ a ∧ b ≤ a ∨ b = 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

case refine_1.inr
a b : Cardinal.{u_1}
h : a + b = a
ha : a < ℵ₀
⊢ ℵ₀ ≤ a ∧ b ≤ a ∨ b = 0

Proof state:
case right
a b : Cardinal.{u_1}
h : a + b = a
ha : ℵ₀ ≤ a
⊢ b ≤ a

Tactic:
rw [← not_lt]

Result:
case right
a b : Cardinal.{u_1}
h : a + b = a
ha : ℵ₀ ≤ a
⊢ ¬a < b

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

Tactic:
use ha

Result:
case right
a b : Cardinal.{u_1}
h : a + b = a
ha : ℵ₀ ≤ a
⊢ b ≤ a

Proof state:
case right
a b : Cardinal.{u_1}
h : a + b = a
ha : ℵ₀ ≤ a
⊢ ¬a < b

Tactic:
apply fun hb => ne_of_gt _ h

Result:
a b : Cardinal.{u_1}
h : a + b = a
ha : ℵ₀ ≤ a
⊢ a < b → a < a + b

Proof state:
a b : Cardinal.{u_1}
h : a + b = a
ha : ℵ₀ ≤ a
hb : a < b
⊢ a < a + b

Tactic:
exact hb.trans_le (self_le_add_left b a)

Result:
no goals

Proof state:
case refine_1.inr.h.intro.intro.intro
n m : ℕ
h : n + m = n
⊢ m = 0

Tactic:
rw [← add_right_inj, h, add_zero]

Result:
no goals

Proof state:
case refine_2
a b : Cardinal.{u_1}
⊢ ℵ₀ ≤ a ∧ b ≤ a ∨ b = 0 → a + b = a

Tactic:
rintro (⟨h1, h2⟩ | h3)

Result:
case refine_2.inl.intro
a b : Cardinal.{u_1}
h1 : ℵ₀ ≤ a
h2 : b ≤ a
⊢ a + b = a

case refine_2.inr
a b : Cardinal.{u_1}
h3 : b = 0
⊢ a + b = a

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

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

Result:
case refine_1.inr.h
a b : Cardinal.{u_1}
h : a + b = a
ha : (∃ n, a = ↑n) ∧ ∃ n, b = ↑n
⊢ b = 0

Proof state:
case refine_2.inl.intro
a b : Cardinal.{u_1}
h1 : ℵ₀ ≤ a
h2 : b ≤ a
⊢ a + b = a

Tactic:
rw [add_eq_max h1, max_eq_left h2]

Result:
no goals