rintro _ _ x hx rfl y hy rfl
α : Type u_1
M N : Matroid α
e f✝ g : α
I X P D : Set α
β : Type u_2
hM : M.Simple
f : α → β
hf : InjOn f M.E
⊢ ∀ ⦃e f_1 : β⦄, ∀ x ∈ M.E, f x = e → ∀ x ∈ M.E, f x = f_1 → ∃ I₀, M.Indep I₀ ∧ {e, f_1} = f '' I₀
α : Type u_1
M N : Matroid α
e f✝ g : α
I X P D : Set α
β : Type u_2
hM : M.Simple
f : α → β
hf : InjOn f M.E
x : α
hx : x ∈ M.E
y : α
hy : y ∈ M.E
⊢ ∃ I₀, M.Indep I₀ ∧ {f x, f y} = f '' I₀