simpa using IsoMinor.rk_le e.dual
α : Type u_1
M : Matroid α
E I B X C : Set α
k : ℕ∞
a b a' b' a₁ a₂ d₁ d₂ : ℕ
x✝ : Nonempty (unif a₁ (a₁ + d₁) ≤i unif a₂ (a₂ + d₂))
e : unif a₁ (a₁ + d₁) ≤i unif a₂ (a₂ + d₂)
⊢ d₁ ≤ d₂
no goals