refine' ⟨fun h ↦ _, fun ⟨I, hIX, hI, hIc⟩ ↦ _⟩
α : Type u_1
ι : Type u_2
M N : Matroid α
I B X X' Y Y' Z R : Set α
n : ℕ∞
e f : α
⊢ n ≤ M.er X ↔ ∃ I ⊆ X, M.Indep I ∧ I.encard = n
case refine'_1
α : Type u_1
ι : Type u_2
M N : Matroid α
I B X X' Y Y' Z R : Set α
n : ℕ∞
e f : α
h : n ≤ M.er X
⊢ ∃ I ⊆ X, M.Indep I ∧ I.encard = n

case refine'_2
α : Type u_1
ι : Type u_2
M N : Matroid α
I✝ B X X' Y Y' Z R : Set α
n : ℕ∞
e f : α
x✝ : ∃ I ⊆ X, M.Indep I ∧ I.encard = n
I : Set α
hIX : I ⊆ X
hI : M.Indep I
hIc : I.encard = n
⊢ n ≤ M.er X