case intro.intro.intro
α : Type u_1
β : Type ?u.135186
s✝ t✝ : Set α
a b x y : α
f : α → β
s t : Set α
ht : Set.Infinite t
hst : s ⊆ t
hs : Set.Finite s
k : ℕ
hsk : Set.ncard s ≤ k
s₁ : Set α
hs₁ : s₁ ⊆ t \ s
hs₁fin : Set.Finite s₁
hs₁card : Set.ncard s₁ = k - Set.ncard s
⊢ ∃ s', s ⊆ s' ∧ s' ⊆ t ∧ Set.ncard s' = k
α : Type u_1
β : Type ?u.135186
s✝ t✝ : Set α
a b x y : α
f : α → β
s t : Set α
ht : Set.Infinite t
hst : s ⊆ t
hs : Set.Finite s
k : ℕ
hsk : Set.ncard s ≤ k
⊢ ∃ s', s ⊆ s' ∧ s' ⊆ t ∧ Set.ncard s' = k
obtain ⟨s₁, hs₁, hs₁fin, hs₁card⟩ := (ht.diff hs).exists_subset_ncard_eq (k - s.ncard)
case intro.intro.intro
α : Type u_1
β : Type ?u.135186
s✝ t✝ : Set α
a b x y : α
f : α → β
s t : Set α
ht : Set.Infinite t
hst : s ⊆ t
hs : Set.Finite s
k : ℕ
hsk : Set.ncard s ≤ k
s₁ : Set α
hs₁ : s₁ ⊆ t \ s
hs₁fin : Set.Finite s₁
hs₁card : Set.ncard s₁ = k - Set.ncard s
⊢ Set.ncard (s ∪ s₁) = k
case intro.intro.intro
α : Type u_1
β : Type ?u.135186
s✝ t✝ : Set α
a b x y : α
f : α → β
s t : Set α
ht : Set.Infinite t
hst : s ⊆ t
hs : Set.Finite s
k : ℕ
hsk : Set.ncard s ≤ k
s₁ : Set α
hs₁ : s₁ ⊆ t \ s
hs₁fin : Set.Finite s₁
hs₁card : Set.ncard s₁ = k - Set.ncard s
⊢ ∃ s', s ⊆ s' ∧ s' ⊆ t ∧ Set.ncard s' = k
refine' ⟨s ∪ s₁, subset_union_left _ _, union_subset hst (hs₁.trans (diff_subset _ _)), _⟩
no goals
case intro.intro.intro
α : Type u_1
β : Type ?u.135186
s✝ t✝ : Set α
a b x y : α
f : α → β
s t : Set α
ht : Set.Infinite t
hst : s ⊆ t
hs : Set.Finite s
k : ℕ
hsk : Set.ncard s ≤ k
s₁ : Set α
hs₁ : s₁ ⊆ t \ s
hs₁fin : Set.Finite s₁
hs₁card : Set.ncard s₁ = k - Set.ncard s
⊢ Set.ncard (s ∪ s₁) = k
rwa [ncard_union_eq (disjoint_of_subset_right hs₁ disjoint_sdiff_right) hs hs₁fin, hs₁card,
  add_tsub_cancel_of_le]