case inl
α : Type u_1
β : Type ?u.120485
s✝ t✝ : Set α
a b x y : α
f : α → β
s t : Set α
h : Set.Finite (s ∪ t)
⊢ ncard (s ∪ t) ≤ ncard s + ncard t

case inr
α : Type u_1
β : Type ?u.120485
s✝ t✝ : Set α
a b x y : α
f : α → β
s t : Set α
h : Set.Infinite (s ∪ t)
⊢ ncard (s ∪ t) ≤ ncard s + ncard t
α : Type u_1
β : Type ?u.120485
s✝ t✝ : Set α
a b x y : α
f : α → β
s t : Set α
⊢ ncard (s ∪ t) ≤ ncard s + ncard t
cases' (s ∪ t).finite_or_infinite with h h
case h.e'_3
α : Type u_1
β : Type ?u.120485
s✝ t✝ : Set α
a b x y : α
f : α → β
s t : Set α
h : Set.Infinite (s ∪ t)
⊢ ncard (s ∪ t) = 0
case inr
α : Type u_1
β : Type ?u.120485
s✝ t✝ : Set α
a b x y : α
f : α → β
s t : Set α
h : Set.Infinite (s ∪ t)
⊢ ncard (s ∪ t) ≤ ncard s + ncard t
convert Nat.zero_le _
no goals
case h.e'_3
α : Type u_1
β : Type ?u.120485
s✝ t✝ : Set α
a b x y : α
f : α → β
s t : Set α
h : Set.Infinite (s ∪ t)
⊢ ncard (s ∪ t) = 0
rw [h.ncard]
case inl
α : Type u_1
β : Type ?u.120485
s✝ t✝ : Set α
a b x y : α
f : α → β
s t : Set α
h : Set.Finite (s ∪ t)
hs : Set.Finite s
⊢ ncard (s ∪ t) ≤ ncard s + ncard t
case inl
α : Type u_1
β : Type ?u.120485
s✝ t✝ : Set α
a b x y : α
f : α → β
s t : Set α
h : Set.Finite (s ∪ t)
⊢ ncard (s ∪ t) ≤ ncard s + ncard t
have hs := h.subset (subset_union_left s t)
case inl
α : Type u_1
β : Type ?u.120485
s✝ t✝ : Set α
a b x y : α
f : α → β
s t : Set α
h : Set.Finite (s ∪ t)
hs : Set.Finite s
ht : Set.Finite t
⊢ ncard (s ∪ t) ≤ ncard s + ncard t
case inl
α : Type u_1
β : Type ?u.120485
s✝ t✝ : Set α
a b x y : α
f : α → β
s t : Set α
h : Set.Finite (s ∪ t)
hs : Set.Finite s
⊢ ncard (s ∪ t) ≤ ncard s + ncard t
have ht := h.subset (subset_union_right s t)
case inl
α : Type u_1
β : Type ?u.120485
s✝ t✝ : Set α
a b x y : α
f : α → β
s t : Set α
h : Set.Finite (s ∪ t)
hs : Set.Finite s
ht : Set.Finite t
⊢ Finset.card (Finite.toFinset ?inl.hs ∪ Finite.toFinset ?inl.ht) ≤
    Finset.card (Finite.toFinset hs) + Finset.card (Finite.toFinset ht)

case inl.hs
α : Type u_1
β : Type ?u.120485
s✝ t✝ : Set α
a b x y : α
f : α → β
s t : Set α
h : Set.Finite (s ∪ t)
hs : Set.Finite s
ht : Set.Finite t
⊢ Set.Finite s

case inl.ht
α : Type u_1
β : Type ?u.120485
s✝ t✝ : Set α
a b x y : α
f : α → β
s t : Set α
h : Set.Finite (s ∪ t)
hs : Set.Finite s
ht : Set.Finite t
⊢ Set.Finite t
case inl
α : Type u_1
β : Type ?u.120485
s✝ t✝ : Set α
a b x y : α
f : α → β
s t : Set α
h : Set.Finite (s ∪ t)
hs : Set.Finite s
ht : Set.Finite t
⊢ ncard (s ∪ t) ≤ ncard s + ncard t
rw [ncard_eq_toFinset_card _ hs, ncard_eq_toFinset_card _ ht, ncard_eq_toFinset_card _ h,
  Finite.toFinset_union]
no goals
case inl
α : Type u_1
β : Type ?u.120485
s✝ t✝ : Set α
a b x y : α
f : α → β
s t : Set α
h : Set.Finite (s ∪ t)
hs : Set.Finite s
ht : Set.Finite t
⊢ Finset.card (Finite.toFinset ?inl.hs ∪ Finite.toFinset ?inl.ht) ≤
    Finset.card (Finite.toFinset hs) + Finset.card (Finite.toFinset ht)

case inl.hs
α : Type u_1
β : Type ?u.120485
s✝ t✝ : Set α
a b x y : α
f : α → β
s t : Set α
h : Set.Finite (s ∪ t)
hs : Set.Finite s
ht : Set.Finite t
⊢ Set.Finite s

case inl.ht
α : Type u_1
β : Type ?u.120485
s✝ t✝ : Set α
a b x y : α
f : α → β
s t : Set α
h : Set.Finite (s ∪ t)
hs : Set.Finite s
ht : Set.Finite t
⊢ Set.Finite t
exact Finset.card_union_le _ _