exact fun m hm ↦ ⟨_, I, hI₁, hI₂, rfl, hm⟩
α : Type u_1
M M₁ M₂ : Matroid α
A I X E : Set α
inst✝ : M₁.Finite
hI₁ : M₁.Indep I
hI₂ : M₂.Indep I
⊢ ∀ m < I.ncard, ∃ x x_1, ∃ (_ : M₁.Indep x_1) (_ : M₂.Indep x_1) (_ : x_1.ncard = x), m < x
no goals