no goals
α : Type u_1
β : Type ?u.123382
s t : Set α
a b x y : α
f : α → β
h : s ⊆ t
ht : autoParam (Set.Finite t) _auto✝
⊢ ncard (t \ s) + ncard s = ncard t
classical
rw [ncard_eq_toFinset_card _ ht, ncard_eq_toFinset_card _ (ht.subset h),
  ncard_eq_toFinset_card _ (ht.diff s), Finite.toFinset_diff]
refine' Finset.card_sdiff_add_card_eq_card _
rwa [Finite.toFinset_subset_toFinset]
α : Type u_1
β : Type ?u.123382
s t : Set α
a b x y : α
f : α → β
h : s ⊆ t
ht : autoParam (Set.Finite t) _auto✝
⊢ Finset.card (Finite.toFinset ?hs \ Finite.toFinset ?ht) + Finset.card (Finite.toFinset (_ : Set.Finite s)) =
    Finset.card (Finite.toFinset ht)

case hs
α : Type u_1
β : Type ?u.123382
s t : Set α
a b x y : α
f : α → β
h : s ⊆ t
ht : autoParam (Set.Finite t) _auto✝
⊢ Set.Finite t

case ht
α : Type u_1
β : Type ?u.123382
s t : Set α
a b x y : α
f : α → β
h : s ⊆ t
ht : autoParam (Set.Finite t) _auto✝
⊢ Set.Finite s
α : Type u_1
β : Type ?u.123382
s t : Set α
a b x y : α
f : α → β
h : s ⊆ t
ht : autoParam (Set.Finite t) _auto✝
⊢ ncard (t \ s) + ncard s = ncard t
rw [ncard_eq_toFinset_card _ ht, ncard_eq_toFinset_card _ (ht.subset h),
  ncard_eq_toFinset_card _ (ht.diff s), Finite.toFinset_diff]
α : Type u_1
β : Type ?u.123382
s t : Set α
a b x y : α
f : α → β
h : s ⊆ t
ht : autoParam (Set.Finite t) _auto✝
⊢ Finite.toFinset (_ : Set.Finite s) ⊆ Finite.toFinset ht
α : Type u_1
β : Type ?u.123382
s t : Set α
a b x y : α
f : α → β
h : s ⊆ t
ht : autoParam (Set.Finite t) _auto✝
⊢ Finset.card (Finite.toFinset ?hs \ Finite.toFinset ?ht) + Finset.card (Finite.toFinset (_ : Set.Finite s)) =
    Finset.card (Finite.toFinset ht)

case hs
α : Type u_1
β : Type ?u.123382
s t : Set α
a b x y : α
f : α → β
h : s ⊆ t
ht : autoParam (Set.Finite t) _auto✝
⊢ Set.Finite t

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