-- Mathlib/SetTheory/Cardinal/Divisibility.lean
theorem prime_of_aleph0_le (ha : ℵ₀ ≤ a) : Prime a

Proof state:
case refine_2.inr.inr
a : Cardinal.{u}
ha : ℵ₀ ≤ a
b c : Cardinal.{u}
hbc : a ∣ b * c
hz : b * c ≠ 0
this : ∀ {a : Cardinal.{u}}, ℵ₀ ≤ a → ∀ (b c : Cardinal.{u}), a ∣ b * c → b * c ≠ 0 → c ≤ b → a ∣ b ∨ a ∣ c
h : ¬c ≤ b
⊢ a ∣ b ∨ a ∣ c

Tactic:
cases le_total c b <;> [solve_by_elim; rw [or_comm]]

Result:
case refine_2.inr.inr.inr
a : Cardinal.{u}
ha : ℵ₀ ≤ a
b c : Cardinal.{u}
hbc : a ∣ b * c
hz : b * c ≠ 0
this : ∀ {a : Cardinal.{u}}, ℵ₀ ≤ a → ∀ (b c : Cardinal.{u}), a ∣ b * c → b * c ≠ 0 → c ≤ b → a ∣ b ∨ a ∣ c
h : ¬c ≤ b
h✝ : b ≤ c
⊢ a ∣ c ∨ a ∣ b

Proof state:
a : Cardinal.{u}
ha : ℵ₀ ≤ a
⊢ Prime a

Tactic:
refine ⟨(aleph0_pos.trans_le ha).ne', ?_, fun b c hbc => ?_⟩

Result:
case refine_1
a : Cardinal.{u}
ha : ℵ₀ ≤ a
⊢ ¬IsUnit a

case refine_2
a : Cardinal.{u}
ha : ℵ₀ ≤ a
b c : Cardinal.{u}
hbc : a ∣ b * c
⊢ a ∣ b ∨ a ∣ c

Proof state:
case refine_1
a : Cardinal.{u}
ha : ℵ₀ ≤ a
⊢ ¬a = 1

Tactic:
exact (one_lt_aleph0.trans_le ha).ne'

Result:
no goals

Proof state:
case refine_2.inr.inr.inr
a : Cardinal.{u}
ha : ℵ₀ ≤ a
b c : Cardinal.{u}
hbc : a ∣ b * c
hz : b * c ≠ 0
this : ∀ {a : Cardinal.{u}}, ℵ₀ ≤ a → ∀ (b c : Cardinal.{u}), a ∣ b * c → b * c ≠ 0 → c ≤ b → a ∣ b ∨ a ∣ c
h : ¬c ≤ b
h✝ : b ≤ c
⊢ a ∣ c ∨ a ∣ b

Tactic:
apply_assumption

Result:
case refine_2.inr.inr.inr.ha
a : Cardinal.{u}
ha : ℵ₀ ≤ a
b c : Cardinal.{u}
hbc : a ∣ b * c
hz : b * c ≠ 0
this : ∀ {a : Cardinal.{u}}, ℵ₀ ≤ a → ∀ (b c : Cardinal.{u}), a ∣ b * c → b * c ≠ 0 → c ≤ b → a ∣ b ∨ a ∣ c
h : ¬c ≤ b
h✝ : b ≤ c
⊢ ℵ₀ ≤ a

case refine_2.inr.inr.inr.hbc
a : Cardinal.{u}
ha : ℵ₀ ≤ a
b c : Cardinal.{u}
hbc : a ∣ b * c
hz : b * c ≠ 0
this : ∀ {a : Cardinal.{u}}, ℵ₀ ≤ a → ∀ (b c : Cardinal.{u}), a ∣ b * c → b * c ≠ 0 → c ≤ b → a ∣ b ∨ a ∣ c
h : ¬c ≤ b
h✝ : b ≤ c
⊢ a ∣ c * b

case refine_2.inr.inr.inr.hz
a : Cardinal.{u}
ha : ℵ₀ ≤ a
b c : Cardinal.{u}
hbc : a ∣ b * c
hz : b * c ≠ 0
this : ∀ {a : Cardinal.{u}}, ℵ₀ ≤ a → ∀ (b c : Cardinal.{u}), a ∣ b * c → b * c ≠ 0 → c ≤ b → a ∣ b ∨ a ∣ c
h : ¬c ≤ b
h✝ : b ≤ c
⊢ c * b ≠ 0

case refine_2.inr.inr.inr.h
a : Cardinal.{u}
ha : ℵ₀ ≤ a
b c : Cardinal.{u}
hbc : a ∣ b * c
hz : b * c ≠ 0
this : ∀ {a : Cardinal.{u}}, ℵ₀ ≤ a → ∀ (b c : Cardinal.{u}), a ∣ b * c → b * c ≠ 0 → c ≤ b → a ∣ b ∨ a ∣ c
h : ¬c ≤ b
h✝ : b ≤ c
⊢ b ≤ c

Proof state:
case refine_2.inr
a : Cardinal.{u}
ha : ℵ₀ ≤ a
b c : Cardinal.{u}
hbc : a ∣ b * c
hz : b * c ≠ 0
⊢ a ∣ b ∨ a ∣ c

Tactic:
wlog h : c ≤ b

Result:
case refine_2.inr.inr
a : Cardinal.{u}
ha : ℵ₀ ≤ a
b c : Cardinal.{u}
hbc : a ∣ b * c
hz : b * c ≠ 0
this : ∀ {a : Cardinal.{u}}, ℵ₀ ≤ a → ∀ (b c : Cardinal.{u}), a ∣ b * c → b * c ≠ 0 → c ≤ b → a ∣ b ∨ a ∣ c
h : ¬c ≤ b
⊢ a ∣ b ∨ a ∣ c

a✝ a : Cardinal.{u}
ha : ℵ₀ ≤ a
b c : Cardinal.{u}
hbc : a ∣ b * c
hz : b * c ≠ 0
h : c ≤ b
⊢ a ∣ b ∨ a ∣ c

Proof state:
case refine_2.inl
a : Cardinal.{u}
ha : ℵ₀ ≤ a
b c : Cardinal.{u}
hbc : a ∣ b * c
hz : b * c = 0
⊢ a ∣ b ∨ a ∣ c

Tactic:
rcases mul_eq_zero.mp hz with (rfl | rfl) <;> simp

Result:
no goals

Proof state:
case refine_2
a : Cardinal.{u}
ha : ℵ₀ ≤ a
b c : Cardinal.{u}
hbc : a ∣ b * c
⊢ a ∣ b ∨ a ∣ c

Tactic:
rcases eq_or_ne (b * c) 0 with hz | hz

Result:
case refine_2.inl
a : Cardinal.{u}
ha : ℵ₀ ≤ a
b c : Cardinal.{u}
hbc : a ∣ b * c
hz : b * c = 0
⊢ a ∣ b ∨ a ∣ c

case refine_2.inr
a : Cardinal.{u}
ha : ℵ₀ ≤ a
b c : Cardinal.{u}
hbc : a ∣ b * c
hz : b * c ≠ 0
⊢ a ∣ b ∨ a ∣ c

Proof state:
case refine_1
a : Cardinal.{u}
ha : ℵ₀ ≤ a
⊢ ¬IsUnit a

Tactic:
rw [isUnit_iff]

Result:
case refine_1
a : Cardinal.{u}
ha : ℵ₀ ≤ a
⊢ ¬a = 1

Proof state:
case refine_2.inr.inr.inr.ha
a : Cardinal.{u}
ha : ℵ₀ ≤ a
b c : Cardinal.{u}
hbc : a ∣ b * c
hz : b * c ≠ 0
this : ∀ {a : Cardinal.{u}}, ℵ₀ ≤ a → ∀ (b c : Cardinal.{u}), a ∣ b * c → b * c ≠ 0 → c ≤ b → a ∣ b ∨ a ∣ c
h : ¬c ≤ b
h✝ : b ≤ c
⊢ ℵ₀ ≤ a

case refine_2.inr.inr.inr.hbc
a : Cardinal.{u}
ha : ℵ₀ ≤ a
b c : Cardinal.{u}
hbc : a ∣ b * c
hz : b * c ≠ 0
this : ∀ {a : Cardinal.{u}}, ℵ₀ ≤ a → ∀ (b c : Cardinal.{u}), a ∣ b * c → b * c ≠ 0 → c ≤ b → a ∣ b ∨ a ∣ c
h : ¬c ≤ b
h✝ : b ≤ c
⊢ a ∣ c * b

case refine_2.inr.inr.inr.hz
a : Cardinal.{u}
ha : ℵ₀ ≤ a
b c : Cardinal.{u}
hbc : a ∣ b * c
hz : b * c ≠ 0
this : ∀ {a : Cardinal.{u}}, ℵ₀ ≤ a → ∀ (b c : Cardinal.{u}), a ∣ b * c → b * c ≠ 0 → c ≤ b → a ∣ b ∨ a ∣ c
h : ¬c ≤ b
h✝ : b ≤ c
⊢ c * b ≠ 0

case refine_2.inr.inr.inr.h
a : Cardinal.{u}
ha : ℵ₀ ≤ a
b c : Cardinal.{u}
hbc : a ∣ b * c
hz : b * c ≠ 0
this : ∀ {a : Cardinal.{u}}, ℵ₀ ≤ a → ∀ (b c : Cardinal.{u}), a ∣ b * c → b * c ≠ 0 → c ≤ b → a ∣ b ∨ a ∣ c
h : ¬c ≤ b
h✝ : b ≤ c
⊢ b ≤ c

Tactic:
assumption'

Result:
case refine_2.inr.inr.inr.hbc
a : Cardinal.{u}
ha : ℵ₀ ≤ a
b c : Cardinal.{u}
hbc : a ∣ b * c
hz : b * c ≠ 0
this : ∀ {a : Cardinal.{u}}, ℵ₀ ≤ a → ∀ (b c : Cardinal.{u}), a ∣ b * c → b * c ≠ 0 → c ≤ b → a ∣ b ∨ a ∣ c
h : ¬c ≤ b
h✝ : b ≤ c
⊢ a ∣ c * b

case refine_2.inr.inr.inr.hz
a : Cardinal.{u}
ha : ℵ₀ ≤ a
b c : Cardinal.{u}
hbc : a ∣ b * c
hz : b * c ≠ 0
this : ∀ {a : Cardinal.{u}}, ℵ₀ ≤ a → ∀ (b c : Cardinal.{u}), a ∣ b * c → b * c ≠ 0 → c ≤ b → a ∣ b ∨ a ∣ c
h : ¬c ≤ b
h✝ : b ≤ c
⊢ c * b ≠ 0

Proof state:
a✝ a : Cardinal.{u}
ha : ℵ₀ ≤ a
b c : Cardinal.{u}
hbc : a ∣ b * c
hz : b * c ≠ 0
h : c ≤ b
⊢ a ∣ b ∨ a ∣ c

Tactic:
left

Result:
case h
a✝ a : Cardinal.{u}
ha : ℵ₀ ≤ a
b c : Cardinal.{u}
hbc : a ∣ b * c
hz : b * c ≠ 0
h : c ≤ b
⊢ a ∣ b

Proof state:
case h
a✝ a : Cardinal.{u}
ha : ℵ₀ ≤ a
b c : Cardinal.{u}
hbc : a ∣ b * c
hz : b * c ≠ 0
h : c ≤ b
habc : a ≤ b * c
⊢ a ∣ b

Tactic:
rwa [mul_eq_max' <| ha.trans <| habc, max_def', if_pos h] at hbc

Result:
no goals

Proof state:
case h
a✝ a : Cardinal.{u}
ha : ℵ₀ ≤ a
b c : Cardinal.{u}
hbc : a ∣ b * c
hz : b * c ≠ 0
h : c ≤ b
⊢ a ∣ b

Tactic:
have habc := le_of_dvd hz hbc

Result:
case h
a✝ a : Cardinal.{u}
ha : ℵ₀ ≤ a
b c : Cardinal.{u}
hbc : a ∣ b * c
hz : b * c ≠ 0
h : c ≤ b
habc : a ≤ b * c
⊢ a ∣ b

Proof state:
case refine_2.inr.inr.inr.hbc
a : Cardinal.{u}
ha : ℵ₀ ≤ a
b c : Cardinal.{u}
hbc : a ∣ b * c
hz : b * c ≠ 0
this : ∀ {a : Cardinal.{u}}, ℵ₀ ≤ a → ∀ (b c : Cardinal.{u}), a ∣ b * c → b * c ≠ 0 → c ≤ b → a ∣ b ∨ a ∣ c
h : ¬c ≤ b
h✝ : b ≤ c
⊢ a ∣ c * b

case refine_2.inr.inr.inr.hz
a : Cardinal.{u}
ha : ℵ₀ ≤ a
b c : Cardinal.{u}
hbc : a ∣ b * c
hz : b * c ≠ 0
this : ∀ {a : Cardinal.{u}}, ℵ₀ ≤ a → ∀ (b c : Cardinal.{u}), a ∣ b * c → b * c ≠ 0 → c ≤ b → a ∣ b ∨ a ∣ c
h : ¬c ≤ b
h✝ : b ≤ c
⊢ c * b ≠ 0

Tactic:
all_goals rwa [mul_comm]

Result:
no goals

Proof state:
case refine_2.inr.inr.inr.hz
a : Cardinal.{u}
ha : ℵ₀ ≤ a
b c : Cardinal.{u}
hbc : a ∣ b * c
hz : b * c ≠ 0
this : ∀ {a : Cardinal.{u}}, ℵ₀ ≤ a → ∀ (b c : Cardinal.{u}), a ∣ b * c → b * c ≠ 0 → c ≤ b → a ∣ b ∨ a ∣ c
h : ¬c ≤ b
h✝ : b ≤ c
⊢ c * b ≠ 0

Tactic:
rwa [mul_comm]

Result:
no goals