obtain ⟨j, rfl⟩ := Nat.exists_eq_add_of_le h.1
α : Type u_1
M : Matroid α
E I B X C : Set α
k : ℕ∞
a b a' b' a₁ a₂ d₁ d₂ : ℕ
h : a₁ ≤ a₂ ∧ d₁ ≤ d₂
⊢ Nonempty (unif a₁ (a₁ + d₁) ≤i unif a₂ (a₂ + d₂))
case intro
α : Type u_1
M : Matroid α
E I B X C : Set α
k : ℕ∞
a b a' b' a₁ d₁ d₂ j : ℕ
h : a₁ ≤ a₁ + j ∧ d₁ ≤ d₂
⊢ Nonempty (unif a₁ (a₁ + d₁) ≤i unif (a₁ + j) (a₁ + j + d₂))