no goals
α : Type u_1
β : Type ?u.122422
s t : Set α
a b x y : α
f : α → β
h : Disjoint s t
hs : autoParam (Set.Finite s) _auto✝
ht : autoParam (Set.Finite t) _auto✝
⊢ ncard (s ∪ t) = ncard s + ncard t
classical
rw [ncard_eq_toFinset_card _ hs, ncard_eq_toFinset_card _ ht,
  ncard_eq_toFinset_card _ (hs.union ht), Finite.toFinset_union]
refine' Finset.card_union_eq _
rwa [Finite.disjoint_toFinset]
α : Type u_1
β : Type ?u.122422
s t : Set α
a b x y : α
f : α → β
h : Disjoint s t
hs : autoParam (Set.Finite s) _auto✝
ht : autoParam (Set.Finite t) _auto✝
⊢ 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.122422
s t : Set α
a b x y : α
f : α → β
h : Disjoint s t
hs : autoParam (Set.Finite s) _auto✝
ht : autoParam (Set.Finite t) _auto✝
⊢ Set.Finite s

case ht
α : Type u_1
β : Type ?u.122422
s t : Set α
a b x y : α
f : α → β
h : Disjoint s t
hs : autoParam (Set.Finite s) _auto✝
ht : autoParam (Set.Finite t) _auto✝
⊢ Set.Finite t
α : Type u_1
β : Type ?u.122422
s t : Set α
a b x y : α
f : α → β
h : Disjoint s t
hs : autoParam (Set.Finite s) _auto✝
ht : autoParam (Set.Finite t) _auto✝
⊢ ncard (s ∪ t) = ncard s + ncard t
rw [ncard_eq_toFinset_card _ hs, ncard_eq_toFinset_card _ ht,
  ncard_eq_toFinset_card _ (hs.union ht), Finite.toFinset_union]
α : Type u_1
β : Type ?u.122422
s t : Set α
a b x y : α
f : α → β
h : Disjoint s t
hs : autoParam (Set.Finite s) _auto✝
ht : autoParam (Set.Finite t) _auto✝
⊢ Disjoint (Finite.toFinset hs) (Finite.toFinset ht)
α : Type u_1
β : Type ?u.122422
s t : Set α
a b x y : α
f : α → β
h : Disjoint s t
hs : autoParam (Set.Finite s) _auto✝
ht : autoParam (Set.Finite t) _auto✝
⊢ 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.122422
s t : Set α
a b x y : α
f : α → β
h : Disjoint s t
hs : autoParam (Set.Finite s) _auto✝
ht : autoParam (Set.Finite t) _auto✝
⊢ Set.Finite s

case ht
α : Type u_1
β : Type ?u.122422
s t : Set α
a b x y : α
f : α → β
h : Disjoint s t
hs : autoParam (Set.Finite s) _auto✝
ht : autoParam (Set.Finite t) _auto✝
⊢ Set.Finite t
refine' Finset.card_union_eq _
no goals
α : Type u_1
β : Type ?u.122422
s t : Set α
a b x y : α
f : α → β
h : Disjoint s t
hs : autoParam (Set.Finite s) _auto✝
ht : autoParam (Set.Finite t) _auto✝
⊢ Disjoint (Finite.toFinset hs) (Finite.toFinset ht)
rwa [Finite.disjoint_toFinset]