exact ⟨hi.ne, hu.ne⟩
α : 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
c : ℕ∞
h_eq : M.er X + M.er Y = M.er (X ∩ Y) + M.er (X ∪ Y) + c
hc : c ≠ ⊤
hi : M.rFin (X ∩ Y)
hu : M.rFin (X ∪ Y)
⊢ ¬M.er (X ∩ Y) = ⊤ ∧ ¬M.er (X ∪ Y) = ⊤
no goals