exact ⟨(unif_isoMinor_contr a₁ (a₁ + d₁) j).trans (unif_isoRestr_unif _ (by linarith)).isoMinor⟩
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₂))
no goals