case inl
α : Type u_1
β : Type ?u.6896
γ : Type ?u.6899
s t : Set α
h : Finite ↑(s ∪ t)
⊢ Nat.card ↑(s ∪ t) ≤ Nat.card ↑s + Nat.card ↑t

case inr
α : Type u_1
β : Type ?u.6896
γ : Type ?u.6899
s t : Set α
h : Infinite ↑(s ∪ t)
⊢ Nat.card ↑(s ∪ t) ≤ Nat.card ↑s + Nat.card ↑t
α : Type u_1
β : Type ?u.6896
γ : Type ?u.6899
s t : Set α
⊢ Nat.card ↑(s ∪ t) ≤ Nat.card ↑s + Nat.card ↑t
cases' _root_.finite_or_infinite (↥(s ∪ t)) with h h
case inl
α : Type u_1
β : Type ?u.6896
γ : Type ?u.6899
s t : Set α
h : Finite ↑s ∧ Finite ↑t
⊢ Nat.card ↑(s ∪ t) ≤ Nat.card ↑s + Nat.card ↑t
case inl
α : Type u_1
β : Type ?u.6896
γ : Type ?u.6899
s t : Set α
h : Finite ↑(s ∪ t)
⊢ Nat.card ↑(s ∪ t) ≤ Nat.card ↑s + Nat.card ↑t
rw [finite_coe_iff, finite_union, ← finite_coe_iff, ← finite_coe_iff] at h
case inl.intro
α : Type u_1
β : Type ?u.6896
γ : Type ?u.6899
s t : Set α
left✝ : Finite ↑s
right✝ : Finite ↑t
⊢ Nat.card ↑(s ∪ t) ≤ Nat.card ↑s + Nat.card ↑t
case inl
α : Type u_1
β : Type ?u.6896
γ : Type ?u.6899
s t : Set α
h : Finite ↑s ∧ Finite ↑t
⊢ Nat.card ↑(s ∪ t) ≤ Nat.card ↑s + Nat.card ↑t
cases h
case inl.intro
α : Type u_1
β : Type ?u.6896
γ : Type ?u.6899
s t : Set α
left✝ : Finite ↑s
right✝ : Finite ↑t
⊢ Cardinal.mk ↑(s ∪ t) ≤ Cardinal.mk ↑s + Cardinal.mk ↑t
case inl.intro
α : Type u_1
β : Type ?u.6896
γ : Type ?u.6899
s t : Set α
left✝ : Finite ↑s
right✝ : Finite ↑t
⊢ Nat.card ↑(s ∪ t) ≤ Nat.card ↑s + Nat.card ↑t
rw [← Cardinal.natCast_le, Nat.cast_add, Finite.cast_card_eq_mk, Finite.cast_card_eq_mk,
  Finite.cast_card_eq_mk]
no goals
case inl.intro
α : Type u_1
β : Type ?u.6896
γ : Type ?u.6899
s t : Set α
left✝ : Finite ↑s
right✝ : Finite ↑t
⊢ Cardinal.mk ↑(s ∪ t) ≤ Cardinal.mk ↑s + Cardinal.mk ↑t
exact Cardinal.mk_union_le s t
no goals
case inr
α : Type u_1
β : Type ?u.6896
γ : Type ?u.6899
s t : Set α
h : Infinite ↑(s ∪ t)
⊢ Nat.card ↑(s ∪ t) ≤ Nat.card ↑s + Nat.card ↑t
exact Nat.card_eq_zero_of_infinite.trans_le (zero_le _)