α β : Type u
S T : Set α
h : T ⊆ S
⊢ Disjoint (S \ T) T
α β : Type u
S T : Set α
h : T ⊆ S
⊢ (#↑(S \ T)) + (#↑T) = (#↑S)
refine (mk_union_of_disjoint <| ?_).symm.trans <| by rw [diff_union_of_subset h]
no goals
α β : Type u
S T : Set α
h : T ⊆ S
⊢ Disjoint (S \ T) T
exact disjoint_sdiff_self_left
no goals
α β : Type u
S T : Set α
h : T ⊆ S
⊢ (#↑(S \ T ∪ T)) = (#↑S)
rw [diff_union_of_subset h]