push_neg at hloop
case neg
α : Type u_1
M M₁✝ M₂✝ : Matroid α
A I X E : Set α
M₁ M₂ : Matroid α
inst✝ : M₁.Finite
hE : M₁.E = M₂.E
x✝ : M₂.Finite
hloop : ¬∀ e ∈ M₁.E, M₁.Loop e ∨ M₂.Loop e
⊢ ∃ I, ∃ X ⊆ M₁.E, M₁.Indep I ∧ M₂.Indep I ∧ I.ncard = M₁.r X + M₂.r (M₂.E \ X)
case neg
α : Type u_1
M M₁✝ M₂✝ : Matroid α
A I X E : Set α
M₁ M₂ : Matroid α
inst✝ : M₁.Finite
hE : M₁.E = M₂.E
x✝ : M₂.Finite
hloop : ∃ e ∈ M₁.E, ¬M₁.Loop e ∧ ¬M₂.Loop e
⊢ ∃ I, ∃ X ⊆ M₁.E, M₁.Indep I ∧ M₂.Indep I ∧ I.ncard = M₁.r X + M₂.r (M₂.E \ X)