α : Type u_1
β : Type ?u.119105
s✝ t✝ : Set α
a b x y : α
f : α → β
s t : Set α
hs : autoParam (Set.Finite s) _auto✝
ht : autoParam (Set.Finite t) _auto✝
hu : Set.Finite (s ∪ t)
⊢ ncard (s ∪ t) + ncard (s ∩ t) = ncard s + ncard t
α : Type u_1
β : Type ?u.119105
s✝ t✝ : Set α
a b x y : α
f : α → β
s t : Set α
hs : autoParam (Set.Finite s) _auto✝
ht : autoParam (Set.Finite t) _auto✝
⊢ ncard (s ∪ t) + ncard (s ∩ t) = ncard s + ncard t
have hu := hs.union ht
α : Type u_1
β : Type ?u.119105
s✝ t✝ : Set α
a b x y : α
f : α → β
s t : Set α
hs : autoParam (Set.Finite s) _auto✝
ht : autoParam (Set.Finite t) _auto✝
hu : Set.Finite (s ∪ t)
hi : Set.Finite (s ∩ t)
⊢ ncard (s ∪ t) + ncard (s ∩ t) = ncard s + ncard t
α : Type u_1
β : Type ?u.119105
s✝ t✝ : Set α
a b x y : α
f : α → β
s t : Set α
hs : autoParam (Set.Finite s) _auto✝
ht : autoParam (Set.Finite t) _auto✝
hu : Set.Finite (s ∪ t)
⊢ ncard (s ∪ t) + ncard (s ∩ t) = ncard s + ncard t
have hi := hs.subset (inter_subset_left s t)
α : Type u_1
β : Type ?u.119105
s✝ t✝ : Set α
a b x y : α
f : α → β
s t : Set α
hs : autoParam (Set.Finite s) _auto✝
ht : autoParam (Set.Finite t) _auto✝
hu : Set.Finite (s ∪ t)
hi : Set.Finite (s ∩ t)
⊢ Finset.card (Finite.toFinset ?hs ∪ Finite.toFinset ?ht) + Finset.card (Finite.toFinset ?hs ∩ Finite.toFinset ?ht) =
    Finset.card (Finite.toFinset hs) + Finset.card (Finite.toFinset ht)

case hs
α : Type u_1
β : Type ?u.119105
s✝ t✝ : Set α
a b x y : α
f : α → β
s t : Set α
hs : autoParam (Set.Finite s) _auto✝
ht : autoParam (Set.Finite t) _auto✝
hu : Set.Finite (s ∪ t)
hi : Set.Finite (s ∩ t)
⊢ Set.Finite s

case ht
α : Type u_1
β : Type ?u.119105
s✝ t✝ : Set α
a b x y : α
f : α → β
s t : Set α
hs : autoParam (Set.Finite s) _auto✝
ht : autoParam (Set.Finite t) _auto✝
hu : Set.Finite (s ∪ t)
hi : Set.Finite (s ∩ t)
⊢ Set.Finite t

case hs
α : Type u_1
β : Type ?u.119105
s✝ t✝ : Set α
a b x y : α
f : α → β
s t : Set α
hs : autoParam (Set.Finite s) _auto✝
ht : autoParam (Set.Finite t) _auto✝
hu : Set.Finite (s ∪ t)
hi : Set.Finite (s ∩ t)
⊢ Set.Finite s

case ht
α : Type u_1
β : Type ?u.119105
s✝ t✝ : Set α
a b x y : α
f : α → β
s t : Set α
hs : autoParam (Set.Finite s) _auto✝
ht : autoParam (Set.Finite t) _auto✝
hu : Set.Finite (s ∪ t)
hi : Set.Finite (s ∩ t)
⊢ Set.Finite t

case hs
α : Type u_1
β : Type ?u.119105
s✝ t✝ : Set α
a b x y : α
f : α → β
s t : Set α
hs : autoParam (Set.Finite s) _auto✝
ht : autoParam (Set.Finite t) _auto✝
hu : Set.Finite (s ∪ t)
hi : Set.Finite (s ∩ t)
⊢ Set.Finite s

case ht
α : Type u_1
β : Type ?u.119105
s✝ t✝ : Set α
a b x y : α
f : α → β
s t : Set α
hs : autoParam (Set.Finite s) _auto✝
ht : autoParam (Set.Finite t) _auto✝
hu : Set.Finite (s ∪ t)
hi : Set.Finite (s ∩ t)
⊢ Set.Finite t
α : Type u_1
β : Type ?u.119105
s✝ t✝ : Set α
a b x y : α
f : α → β
s t : Set α
hs : autoParam (Set.Finite s) _auto✝
ht : autoParam (Set.Finite t) _auto✝
hu : Set.Finite (s ∪ t)
hi : Set.Finite (s ∩ t)
⊢ ncard (s ∪ t) + ncard (s ∩ t) = ncard s + ncard t
rw [ncard_eq_toFinset_card _ hs, ncard_eq_toFinset_card _ ht, ncard_eq_toFinset_card _ hu,
  ncard_eq_toFinset_card _ hi, Finite.toFinset_union, Finite.toFinset_inter]
no goals
α : Type u_1
β : Type ?u.119105
s✝ t✝ : Set α
a b x y : α
f : α → β
s t : Set α
hs : autoParam (Set.Finite s) _auto✝
ht : autoParam (Set.Finite t) _auto✝
hu : Set.Finite (s ∪ t)
hi : Set.Finite (s ∩ t)
⊢ Finset.card (Finite.toFinset ?hs ∪ Finite.toFinset ?ht) + Finset.card (Finite.toFinset ?hs ∩ Finite.toFinset ?ht) =
    Finset.card (Finite.toFinset hs) + Finset.card (Finite.toFinset ht)
exact Finset.card_union_add_card_inter _ _