simp [hX.ne, hY.ne] at h_eq
case intro.inl
α : Type u_1
ι : Type u_2
M N : Matroid α
I B X X' Y Y' Z R : Set α
n : ℕ∞
e f : α
hX : M.rFin X
hY : M.rFin Y
h_eq : M.er X = ⊤ ∨ M.er Y = ⊤
⊢ M.r (X ∩ Y) + M.r (X ∪ Y) ≤ M.r X + M.r Y
no goals