rw [Set.union_diff_cancel hsub] at hcntB
case intro.left
α : Type
A B : Set α
hsub : A ⊆ B
hucnt : Uncountable B
hcntA : Set.Countable A
right✝ : Set.Infinite A
hcntmin : Set.Countable (B \ A)
hcntB : Set.Countable (A ∪ B \ A)
⊢ False
case intro.left
α : Type
A B : Set α
hsub : A ⊆ B
hucnt : Uncountable B
hcntA : Set.Countable A
right✝ : Set.Infinite A
hcntmin : Set.Countable (B \ A)
hcntB : Set.Countable B
⊢ False