-- Mathlib/Data/Set/Card.lean
theorem exists_superset_subset_encard_eq {k : ℕ∞}
    (hst : s ⊆ t) (hsk : s.encard ≤ k) (hkt : k ≤ t.encard) :
    ∃ r, s ⊆ r ∧ r ⊆ t ∧ r.encard = k

Proof state:
α : Type u_1
s t : Set α
hst : s ⊆ t
hs : s.encard ≠ ⊤
k : ℕ∞
hsk : s.encard ≤ s.encard + k
hkt : s.encard + k ≤ t.encard
k' : ℕ∞
hk' : t.encard = s.encard + k + k'
⊢ k ≤ (t \ s).encard

Tactic:
rw [← encard_diff_add_encard_of_subset hst, add_comm] at hkt

Result:
α : Type u_1
s t : Set α
hst : s ⊆ t
hs : s.encard ≠ ⊤
k : ℕ∞
hsk : s.encard ≤ s.encard + k
hkt : k + s.encard ≤ (t \ s).encard + s.encard
k' : ℕ∞
hk' : t.encard = s.encard + k + k'
⊢ k ≤ (t \ s).encard

Proof state:
case inr
α : Type u_1
s t : Set α
k : ℕ∞
hst : s ⊆ t
hsk : s.encard ≤ k
hkt : k ≤ t.encard
hs : s.encard ≠ ⊤
⊢ ∃ r, s ⊆ r ∧ r ⊆ t ∧ r.encard = k

Tactic:
obtain ⟨k, rfl⟩ := exists_add_of_le hsk

Result:
case inr.intro
α : Type u_1
s t : Set α
hst : s ⊆ t
hs : s.encard ≠ ⊤
k : ℕ∞
hsk : s.encard ≤ s.encard + k
hkt : s.encard + k ≤ t.encard
⊢ ∃ r, s ⊆ r ∧ r ⊆ t ∧ r.encard = s.encard + k

Proof state:
case inr.intro.intro
α : Type u_1
s t : Set α
hst : s ⊆ t
hs : s.encard ≠ ⊤
k : ℕ∞
hsk : s.encard ≤ s.encard + k
hkt : s.encard + k ≤ t.encard
k' : ℕ∞
hk' : t.encard = s.encard + k + k'
⊢ ∃ r, s ⊆ r ∧ r ⊆ t ∧ r.encard = s.encard + k

Tactic:
have hk : k ≤ encard (t \ s) := by
  rw [← encard_diff_add_encard_of_subset hst, add_comm] at hkt
  exact WithTop.le_of_add_le_add_right hs hkt

Result:
case inr.intro.intro
α : Type u_1
s t : Set α
hst : s ⊆ t
hs : s.encard ≠ ⊤
k : ℕ∞
hsk : s.encard ≤ s.encard + k
hkt : s.encard + k ≤ t.encard
k' : ℕ∞
hk' : t.encard = s.encard + k + k'
hk : k ≤ (t \ s).encard
⊢ ∃ r, s ⊆ r ∧ r ⊆ t ∧ r.encard = s.encard + k

Proof state:
case inl
α : Type u_1
s t : Set α
k : ℕ∞
hst : s ⊆ t
hsk : s.encard ≤ k
hkt : k ≤ t.encard
hs : s.encard = ⊤
⊢ ∃ r, s ⊆ r ∧ r ⊆ t ∧ r.encard = k

Tactic:
rw [hs, top_le_iff] at hsk

Result:
case inl
α : Type u_1
s t : Set α
k : ℕ∞
hst : s ⊆ t
hsk : k = ⊤
hkt : k ≤ t.encard
hs : s.encard = ⊤
⊢ ∃ r, s ⊆ r ∧ r ⊆ t ∧ r.encard = k

Proof state:
α : Type u_1
s t : Set α
k : ℕ∞
hst : s ⊆ t
hsk : s.encard ≤ k
hkt : k ≤ t.encard
⊢ ∃ r, s ⊆ r ∧ r ⊆ t ∧ r.encard = k

Tactic:
obtain (hs | hs) := eq_or_ne s.encard ⊤

Result:
case inl
α : Type u_1
s t : Set α
k : ℕ∞
hst : s ⊆ t
hsk : s.encard ≤ k
hkt : k ≤ t.encard
hs : s.encard = ⊤
⊢ ∃ r, s ⊆ r ∧ r ⊆ t ∧ r.encard = k

case inr
α : Type u_1
s t : Set α
k : ℕ∞
hst : s ⊆ t
hsk : s.encard ≤ k
hkt : k ≤ t.encard
hs : s.encard ≠ ⊤
⊢ ∃ r, s ⊆ r ∧ r ⊆ t ∧ r.encard = k

Proof state:
α : Type u_1
s t : Set α
hst : s ⊆ t
hs : s.encard ≠ ⊤
k : ℕ∞
hsk : s.encard ≤ s.encard + k
hkt : k + s.encard ≤ (t \ s).encard + s.encard
k' : ℕ∞
hk' : t.encard = s.encard + k + k'
⊢ k ≤ (t \ s).encard

Tactic:
exact WithTop.le_of_add_le_add_right hs hkt

Result:
no goals

Proof state:
case inr.intro
α : Type u_1
s t : Set α
hst : s ⊆ t
hs : s.encard ≠ ⊤
k : ℕ∞
hsk : s.encard ≤ s.encard + k
hkt : s.encard + k ≤ t.encard
⊢ ∃ r, s ⊆ r ∧ r ⊆ t ∧ r.encard = s.encard + k

Tactic:
obtain ⟨k', hk'⟩ := exists_add_of_le hkt

Result:
case inr.intro.intro
α : Type u_1
s t : Set α
hst : s ⊆ t
hs : s.encard ≠ ⊤
k : ℕ∞
hsk : s.encard ≤ s.encard + k
hkt : s.encard + k ≤ t.encard
k' : ℕ∞
hk' : t.encard = s.encard + k + k'
⊢ ∃ r, s ⊆ r ∧ r ⊆ t ∧ r.encard = s.encard + k

Proof state:
case inl
α : Type u_1
s t : Set α
k : ℕ∞
hst : s ⊆ t
hsk : k = ⊤
hkt : k ≤ t.encard
hs : s.encard = ⊤
⊢ ∃ r, s ⊆ r ∧ r ⊆ t ∧ r.encard = k

Tactic:
subst hsk

Result:
case inl
α : Type u_1
s t : Set α
hst : s ⊆ t
hs : s.encard = ⊤
hkt : ⊤ ≤ t.encard
⊢ ∃ r, s ⊆ r ∧ r ⊆ t ∧ r.encard = ⊤

Proof state:
case inr.intro.intro
α : Type u_1
s t : Set α
hst : s ⊆ t
hs : s.encard ≠ ⊤
k : ℕ∞
hsk : s.encard ≤ s.encard + k
hkt : s.encard + k ≤ t.encard
k' : ℕ∞
hk' : t.encard = s.encard + k + k'
hk : k ≤ (t \ s).encard
⊢ ∃ r, s ⊆ r ∧ r ⊆ t ∧ r.encard = s.encard + k

Tactic:
obtain ⟨r', hr', rfl⟩ := exists_subset_encard_eq hk

Result:
case inr.intro.intro.intro.intro
α : Type u_1
s t : Set α
hst : s ⊆ t
hs : s.encard ≠ ⊤
k' : ℕ∞
r' : Set α
hr' : r' ⊆ t \ s
hsk : s.encard ≤ s.encard + r'.encard
hkt : s.encard + r'.encard ≤ t.encard
hk' : t.encard = s.encard + r'.encard + k'
hk : r'.encard ≤ (t \ s).encard
⊢ ∃ r, s ⊆ r ∧ r ⊆ t ∧ r.encard = s.encard + r'.encard

Proof state:
case inl
α : Type u_1
s t : Set α
hst : s ⊆ t
hs : s.encard = ⊤
hkt : ⊤ ≤ t.encard
⊢ ∃ r, s ⊆ r ∧ r ⊆ t ∧ r.encard = ⊤

Tactic:
exact ⟨s, Subset.rfl, hst, hs⟩

Result:
no goals

Proof state:
case inr.intro.intro.intro.intro
α : Type u_1
s t : Set α
hst : s ⊆ t
hs : s.encard ≠ ⊤
k' : ℕ∞
r' : Set α
hr' : r' ⊆ t \ s
hsk : s.encard ≤ s.encard + r'.encard
hkt : s.encard + r'.encard ≤ t.encard
hk' : t.encard = s.encard + r'.encard + k'
hk : r'.encard ≤ (t \ s).encard
⊢ (s ∪ r').encard = s.encard + r'.encard

Tactic:
rw [encard_union_eq (disjoint_of_subset_right hr' disjoint_sdiff_right)]

Result:
no goals

Proof state:
case inr.intro.intro.intro.intro
α : Type u_1
s t : Set α
hst : s ⊆ t
hs : s.encard ≠ ⊤
k' : ℕ∞
r' : Set α
hr' : r' ⊆ t \ s
hsk : s.encard ≤ s.encard + r'.encard
hkt : s.encard + r'.encard ≤ t.encard
hk' : t.encard = s.encard + r'.encard + k'
hk : r'.encard ≤ (t \ s).encard
⊢ ∃ r, s ⊆ r ∧ r ⊆ t ∧ r.encard = s.encard + r'.encard

Tactic:
refine ⟨s ∪ r', subset_union_left, union_subset hst (hr'.trans diff_subset), ?_⟩

Result:
case inr.intro.intro.intro.intro
α : Type u_1
s t : Set α
hst : s ⊆ t
hs : s.encard ≠ ⊤
k' : ℕ∞
r' : Set α
hr' : r' ⊆ t \ s
hsk : s.encard ≤ s.encard + r'.encard
hkt : s.encard + r'.encard ≤ t.encard
hk' : t.encard = s.encard + r'.encard + k'
hk : r'.encard ≤ (t \ s).encard
⊢ (s ∪ r').encard = s.encard + r'.encard