exact .inr ⟨ht' hyt', hyt'⟩
case intro.intro.refine_4
α : Type u_1
β : Type u_2
r✝ s s₁ s₂ : Set α
t t' t₁ t₂ : Set β
f : α → β
h : BijOn f s t
hss₁ : s ⊆ s₁
htt' : t ⊆ t'
ht' : SurjOn f s₁ t'
r : Set α
hrss : r ⊆ (s₁ ∩ f ⁻¹' t') \ f ⁻¹' t
hbij : BijOn f r ((f '' s₁ ∩ t') \ t)
y : β
hyt' : y ∈ t'
⊢ y ∈ t ∪ f '' s₁ ∩ t'
no goals