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