Theorem: Set.InjOn.exists_subset_injOn_subset_range_eq (Matroid/ForMathlib/Function.lean)

State before:
α : Type u_1
β : Type u_2
r s s₁ s₂ : Set α
t t' t₁ t₂ : Set β
f : α → β
hinj : InjOn f r
hrs : r ⊆ s
⊢ ∃ u, r ⊆ u ∧ u ⊆ s ∧ f '' u = f '' s ∧ InjOn f u
Tactic:
obtain ⟨u, hru, hus, h⟩ := hinj.bijOn_image.exists_extend_of_subset hrs
  (image_subset f hrs) Subset.rfl
State after:
case intro.intro.intro
α : Type u_1
β : Type u_2
r s s₁ s₂ : Set α
t t' t₁ t₂ : Set β
f : α → β
hinj : InjOn f r
hrs : r ⊆ s
u : Set α
hru : r ⊆ u
hus : u ⊆ s
h : BijOn f u (f '' s)
⊢ ∃ u, r ⊆ u ∧ u ⊆ s ∧ f '' u = f '' s ∧ InjOn f u

State before:
case intro.intro.intro
α : Type u_1
β : Type u_2
r s s₁ s₂ : Set α
t t' t₁ t₂ : Set β
f : α → β
hinj : InjOn f r
hrs : r ⊆ s
u : Set α
hru : r ⊆ u
hus : u ⊆ s
h : BijOn f u (f '' s)
⊢ ∃ u, r ⊆ u ∧ u ⊆ s ∧ f '' u = f '' s ∧ InjOn f u
Tactic:
exact ⟨u, hru, hus, h.image_eq, h.injOn⟩
State after:
no goals