rw [eq_comm, r_eq_zero_iff diff_subset, diff_subset_iff, ← hE]
case pos
α : 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
⊢ 0 = M₂.r (M₂.E \ M₁.cl ∅)
case pos
α : 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
⊢ M₁.E ⊆ M₁.cl ∅ ∪ M₂.cl ∅