case intro.intro.intro
α : Type u_1
β : Type ?u.132165
s t : Set α
a b x y : α
f : α → β
m : ℕ
hs : ncard s ≤ m
ht : m ≤ ncard t
h : s ⊆ t
r : Set α
hsr : s ⊆ r
hrt : r ⊆ t
hc : ncard r = m - ncard s + ncard s
⊢ ∃ r, s ⊆ r ∧ r ⊆ t ∧ ncard r = m
α : Type u_1
β : Type ?u.132165
s t : Set α
a b x y : α
f : α → β
m : ℕ
hs : ncard s ≤ m
ht : m ≤ ncard t
h : s ⊆ t
⊢ ∃ r, s ⊆ r ∧ r ⊆ t ∧ ncard r = m
obtain ⟨r, hsr, hrt, hc⟩ :=
  exists_intermediate_Set (m - s.ncard) (by rwa [tsub_add_cancel_of_le hs]) h
case intro.intro.intro
α : Type u_1
β : Type ?u.132165
s t : Set α
a b x y : α
f : α → β
m : ℕ
hs : ncard s ≤ m
ht : m ≤ ncard t
h : s ⊆ t
r : Set α
hsr : s ⊆ r
hrt : r ⊆ t
hc : ncard r = m
⊢ ∃ r, s ⊆ r ∧ r ⊆ t ∧ ncard r = m
case intro.intro.intro
α : Type u_1
β : Type ?u.132165
s t : Set α
a b x y : α
f : α → β
m : ℕ
hs : ncard s ≤ m
ht : m ≤ ncard t
h : s ⊆ t
r : Set α
hsr : s ⊆ r
hrt : r ⊆ t
hc : ncard r = m - ncard s + ncard s
⊢ ∃ r, s ⊆ r ∧ r ⊆ t ∧ ncard r = m
rw [tsub_add_cancel_of_le hs] at hc
no goals
case intro.intro.intro
α : Type u_1
β : Type ?u.132165
s t : Set α
a b x y : α
f : α → β
m : ℕ
hs : ncard s ≤ m
ht : m ≤ ncard t
h : s ⊆ t
r : Set α
hsr : s ⊆ r
hrt : r ⊆ t
hc : ncard r = m
⊢ ∃ r, s ⊆ r ∧ r ⊆ t ∧ ncard r = m
exact ⟨r, hsr, hrt, hc⟩
no goals
α : Type u_1
β : Type ?u.132165
s t : Set α
a b x y : α
f : α → β
m : ℕ
hs : ncard s ≤ m
ht : m ≤ ncard t
h : s ⊆ t
⊢ m - ncard s + ncard s ≤ ncard t
rwa [tsub_add_cancel_of_le hs]