Theorem: Set.BijOn.exists_extend (Matroid/ForMathlib/Function.lean)

State before:
α : Type u_1
β : Type u_2
r s s₁ s₂ : Set α
t t' t₁ t₂ : Set β
f : α → β
h : BijOn f s t
htt' : t ⊆ t'
ht' : t' ⊆ range f
⊢ ∃ s', s ⊆ s' ∧ BijOn f s' t'
Tactic:
simpa using h.exists_extend_of_subset (subset_univ s) htt' (by simpa [SurjOn])
State after:
no goals

State before:
α : Type u_1
β : Type u_2
r s s₁ s₂ : Set α
t t' t₁ t₂ : Set β
f : α → β
h : BijOn f s t
htt' : t ⊆ t'
ht' : t' ⊆ range f
⊢ SurjOn f univ t'
Tactic:
simpa [SurjOn]
State after:
no goals