α β γ : Cardinal
γ₀ : γ < ℵ₀
h : α + γ ≤ β + γ
⊢ α ≤ β
α β γ : Cardinal
γ₀ : γ < ℵ₀
⊢ α + γ ≤ β + γ ↔ α ≤ β
refine' ⟨fun h => _, fun h => add_le_add_right h γ⟩
α β γ : Cardinal
γ₀ : γ < ℵ₀
h : ¬α ≤ β
⊢ ¬α + γ ≤ β + γ
α β γ : Cardinal
γ₀ : γ < ℵ₀
h : α + γ ≤ β + γ
⊢ α ≤ β
contrapose h
α β γ : Cardinal
γ₀ : γ < ℵ₀
h : β ≤ α ∧ ¬β = α
⊢ β + γ ≤ α + γ ∧ ¬β + γ = α + γ
α β γ : Cardinal
γ₀ : γ < ℵ₀
h : ¬α ≤ β
⊢ ¬α + γ ≤ β + γ
rw [not_le, lt_iff_le_and_ne, Ne] at h⊢
no goals
α β γ : Cardinal
γ₀ : γ < ℵ₀
h : β ≤ α ∧ ¬β = α
⊢ β + γ ≤ α + γ ∧ ¬β + γ = α + γ
exact ⟨add_le_add_right h.1 γ, mt (add_right_inj_of_lt_aleph0 γ₀).1 h.2⟩