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