case mk.mk.mk.mk.intro.intro
α✝ β✝ : Type u
a✝ : Cardinal
α : Type u_1
b✝ : Cardinal
β : Type u_1
c✝ : Cardinal
γ : Type u_1
d✝ : Cardinal
δ : Type u_1
e₁ : α ↪ β
e₂ : γ ↪ δ
⊢ Quot.mk Setoid.r α + Quot.mk Setoid.r γ ≤ Quot.mk Setoid.r β + Quot.mk Setoid.r δ
α β : Type u
⊢ ∀ {a b c d : Cardinal}, a ≤ b → c ≤ d → a + c ≤ b + d
rintro ⟨α⟩ ⟨β⟩ ⟨γ⟩ ⟨δ⟩ ⟨e₁⟩ ⟨e₂⟩
no goals
case mk.mk.mk.mk.intro.intro
α✝ β✝ : Type u
a✝ : Cardinal
α : Type u_1
b✝ : Cardinal
β : Type u_1
c✝ : Cardinal
γ : Type u_1
d✝ : Cardinal
δ : Type u_1
e₁ : α ↪ β
e₂ : γ ↪ δ
⊢ Quot.mk Setoid.r α + Quot.mk Setoid.r γ ≤ Quot.mk Setoid.r β + Quot.mk Setoid.r δ
exact ⟨e₁.sumMap e₂⟩