refine le_antisymm (le_ciInf fun X ↦ ?_) ?_
α : Type u_1
M M₁✝ M₂✝ : Matroid α
A I X E : Set α
M₁ M₂ : Matroid α
inst✝¹ : M₁.Finite
inst✝ : M₂.FiniteRk
⊢ M₁.maxCommonInd M₂ = ⨅ X, M₁.r X + M₂.r (M₂.E \ X)
case refine_1
α : Type u_1
M M₁✝ M₂✝ : Matroid α
A I X✝ E : Set α
M₁ M₂ : Matroid α
inst✝¹ : M₁.Finite
inst✝ : M₂.FiniteRk
X : Set α
⊢ M₁.maxCommonInd M₂ ≤ M₁.r X + M₂.r (M₂.E \ X)

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₂