case inl
o₁ o₂ : Ordinal
h : aleph o₁ ≤ aleph o₂
⊢ max (aleph o₁) (aleph o₂) = aleph (max o₁ o₂)

case inr
o₁ o₂ : Ordinal
h : aleph o₂ ≤ aleph o₁
⊢ max (aleph o₁) (aleph o₂) = aleph (max o₁ o₂)
o₁ o₂ : Ordinal
⊢ max (aleph o₁) (aleph o₂) = aleph (max o₁ o₂)
cases' le_total (aleph o₁) (aleph o₂) with h h
no goals
case inl
o₁ o₂ : Ordinal
h : aleph o₁ ≤ aleph o₂
⊢ max (aleph o₁) (aleph o₂) = aleph (max o₁ o₂)
rw [max_eq_right h, max_eq_right (aleph_le.1 h)]
no goals
case inr
o₁ o₂ : Ordinal
h : aleph o₂ ≤ aleph o₁
⊢ max (aleph o₁) (aleph o₂) = aleph (max o₁ o₂)
rw [max_eq_left h, max_eq_left (aleph_le.1 h)]