obtain ⟨I, X, hI₁, hI₂, h⟩ := exists_common_ind M₁ M₂
case refine_2
α : Type u_1
M M₁✝ M₂✝ : Matroid α
A I X E : Set α
M₁ M₂ : Matroid α
inst✝¹ : M₁.Finite
inst✝ : M₂.FiniteRk
⊢ ⨅ X, M₁.r X + M₂.r (M₂.E \ X) ≤ M₁.maxCommonInd M₂
case refine_2.intro.intro.intro.intro
α : Type u_1
M M₁✝ M₂✝ : Matroid α
A I✝ X✝ E : Set α
M₁ M₂ : Matroid α
inst✝¹ : M₁.Finite
inst✝ : M₂.FiniteRk
I X : Set α
hI₁ : M₁.Indep I
hI₂ : M₂.Indep I
h : I.ncard = M₁.r X + M₂.r (M₂.E \ X)
⊢ ⨅ X, M₁.r X + M₂.r (M₂.E \ X) ≤ M₁.maxCommonInd M₂