obtain ⟨I, X, -, hI₁, hI₂, hcard⟩ := exists_common_ind_aux M₁ (M₂ ↾ M₁.E) rfl
α : Type u_1
M M₁✝ M₂✝ : Matroid α
A I X E : Set α
M₁ M₂ : Matroid α
inst✝ : M₁.Finite
⊢ ∃ I X, M₁.Indep I ∧ M₂.Indep I ∧ I.ncard = M₁.r X + M₂.r (M₂.E \ X)
case intro.intro.intro.intro.intro
α : Type u_1
M M₁✝ M₂✝ : Matroid α
A I✝ X✝ E : Set α
M₁ M₂ : Matroid α
inst✝ : M₁.Finite
I X : Set α
hI₁ : M₁.Indep I
hI₂ : (M₂ ↾ M₁.E).Indep I
hcard : I.ncard = M₁.r X + (M₂ ↾ M₁.E).r ((M₂ ↾ M₁.E).E \ X)
⊢ ∃ I X, M₁.Indep I ∧ M₂.Indep I ∧ I.ncard = M₁.r X + M₂.r (M₂.E \ X)