simp only [mem_setOf_eq, forall_exists_index, and_imp]
case h
α : Type u_1
M M₁ M₂ : Matroid α
A I X E : Set α
inst✝ : M₁.Finite
hI₁ : M₁.Indep I
hI₂ : M₂.Indep I
⊢ ∀ a ∈ {n | ∃ I, M₁.Indep I ∧ M₂.Indep I ∧ I.ncard = n}, a ≤ M₁.E.ncard
case h
α : Type u_1
M M₁ M₂ : Matroid α
A I X E : Set α
inst✝ : M₁.Finite
hI₁ : M₁.Indep I
hI₂ : M₂.Indep I
⊢ ∀ (a : ℕ) (x : Set α), M₁.Indep x → M₂.Indep x → x.ncard = a → a ≤ M₁.E.ncard