simp at hY
case intro.intro
α : Type u_1
ι : Type u_2
M N : Matroid α
I B X X' Y Y' Z R : Set α
n : ℕ∞
e✝ f : α
hXY : X ⊆ Y
hlt : M.er X < M.er Y
e : α
he : e ∈ Y \ X
hins : M.er (insert e X) = M.er X + 1
hY : 1 ≤ 0
⊢ False
no goals