rw [add_tsub_cancel_left, add_tsub_cancel_left, unif_isoMinor_unif_iff]
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₂
no goals