rw [maxCommonInd, Nat.sSup_def, Nat.le_find_iff]
α : Type u_1
M M₁ M₂ : Matroid α
A I X E : Set α
inst✝ : M₁.Finite
hI₁ : M₁.Indep I
hI₂ : M₂.Indep I
⊢ I.ncard ≤ M₁.maxCommonInd M₂
α : Type u_1
M M₁ M₂ : Matroid α
A I X E : Set α
inst✝ : M₁.Finite
hI₁ : M₁.Indep I
hI₂ : M₂.Indep I
⊢ ∀ m < I.ncard, ¬∀ a ∈ {n | ∃ I, M₁.Indep I ∧ M₂.Indep I ∧ I.ncard = n}, a ≤ m

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
⊢ ∃ n, ∀ a ∈ {n | ∃ I, M₁.Indep I ∧ M₂.Indep I ∧ I.ncard = n}, a ≤ n