case mp
α : Type u_1
β : Type u_2
γ : Type ?u.68088
ι : Sort ?u.68091
π : α → Type ?u.68096
s s₁ s₂ : Set α
t : Set β
f : α → β
⊢ SurjOn f s t → ∃ s' x, BijOn f s' t

case mpr
α : Type u_1
β : Type u_2
γ : Type ?u.68088
ι : Sort ?u.68091
π : α → Type ?u.68096
s s₁ s₂ : Set α
t : Set β
f : α → β
⊢ (∃ s' x, BijOn f s' t) → SurjOn f s t
α : Type u_1
β : Type u_2
γ : Type ?u.68088
ι : Sort ?u.68091
π : α → Type ?u.68096
s s₁ s₂ : Set α
t : Set β
f : α → β
⊢ SurjOn f s t ↔ ∃ s' x, BijOn f s' t
constructor
case mp.inl
α : Type u_1
β : Type u_2
γ : Type ?u.68088
ι : Sort ?u.68091
π : α → Type ?u.68096
s s₁ s₂ : Set α
f : α → β
⊢ SurjOn f s ∅ → ∃ s' x, BijOn f s' ∅

case mp.inr
α : Type u_1
β : Type u_2
γ : Type ?u.68088
ι : Sort ?u.68091
π : α → Type ?u.68096
s s₁ s₂ : Set α
t : Set β
f : α → β
ht : Set.Nonempty t
⊢ SurjOn f s t → ∃ s' x, BijOn f s' t
case mp
α : Type u_1
β : Type u_2
γ : Type ?u.68088
ι : Sort ?u.68091
π : α → Type ?u.68096
s s₁ s₂ : Set α
t : Set β
f : α → β
⊢ SurjOn f s t → ∃ s' x, BijOn f s' t
rcases eq_empty_or_nonempty t with (rfl | ht)
no goals
case mp.inl
α : Type u_1
β : Type u_2
γ : Type ?u.68088
ι : Sort ?u.68091
π : α → Type ?u.68096
s s₁ s₂ : Set α
f : α → β
⊢ SurjOn f s ∅ → ∃ s' x, BijOn f s' ∅
exact fun _ => ⟨∅, empty_subset _, bijOn_empty f⟩
case mp.inr
α : Type u_1
β : Type u_2
γ : Type ?u.68088
ι : Sort ?u.68091
π : α → Type ?u.68096
s s₁ s₂ : Set α
t : Set β
f : α → β
ht : Set.Nonempty t
h : SurjOn f s t
⊢ ∃ s' x, BijOn f s' t
case mp.inr
α : Type u_1
β : Type u_2
γ : Type ?u.68088
ι : Sort ?u.68091
π : α → Type ?u.68096
s s₁ s₂ : Set α
t : Set β
f : α → β
ht : Set.Nonempty t
⊢ SurjOn f s t → ∃ s' x, BijOn f s' t
intro h
case mp.inr
α : Type u_1
β : Type u_2
γ : Type ?u.68088
ι : Sort ?u.68091
π : α → Type ?u.68096
s s₁ s₂ : Set α
t : Set β
f : α → β
ht : Set.Nonempty t
h : SurjOn f s t
this : Nonempty α
⊢ ∃ s' x, BijOn f s' t
case mp.inr
α : Type u_1
β : Type u_2
γ : Type ?u.68088
ι : Sort ?u.68091
π : α → Type ?u.68096
s s₁ s₂ : Set α
t : Set β
f : α → β
ht : Set.Nonempty t
h : SurjOn f s t
⊢ ∃ s' x, BijOn f s' t
haveI : Nonempty α := ⟨Classical.choose (h.comap_nonempty ht)⟩
no goals
case mp.inr
α : Type u_1
β : Type u_2
γ : Type ?u.68088
ι : Sort ?u.68091
π : α → Type ?u.68096
s s₁ s₂ : Set α
t : Set β
f : α → β
ht : Set.Nonempty t
h : SurjOn f s t
this : Nonempty α
⊢ ∃ s' x, BijOn f s' t
exact ⟨_, h.mapsTo_invFunOn.image_subset, h.bijOn_subset⟩
case mpr.intro.intro
α : Type u_1
β : Type u_2
γ : Type ?u.68088
ι : Sort ?u.68091
π : α → Type ?u.68096
s s₁ s₂ : Set α
t : Set β
f : α → β
s' : Set α
hs' : s' ⊆ s
hfs' : BijOn f s' t
⊢ SurjOn f s t
case mpr
α : Type u_1
β : Type u_2
γ : Type ?u.68088
ι : Sort ?u.68091
π : α → Type ?u.68096
s s₁ s₂ : Set α
t : Set β
f : α → β
⊢ (∃ s' x, BijOn f s' t) → SurjOn f s t
rintro ⟨s', hs', hfs'⟩
no goals
case mpr.intro.intro
α : Type u_1
β : Type u_2
γ : Type ?u.68088
ι : Sort ?u.68091
π : α → Type ?u.68096
s s₁ s₂ : Set α
t : Set β
f : α → β
s' : Set α
hs' : s' ⊆ s
hfs' : BijOn f s' t
⊢ SurjOn f s t
exact hfs'.surjOn.mono hs' (Subset.refl _)