obtain ⟨C, D, _, _, _, rfl⟩ := h
α : Type u_1
M M' N : Matroid α
e f : α
I J R B X Y Z K E : Set α
h : M ≤m loopyOn E
⊢ M = loopyOn M.E
case intro.intro.intro.intro.intro
α : Type u_1
M' N : Matroid α
e f : α
I J R B X Y Z K E C D : Set α
left✝² : C ⊆ (loopyOn E).E
left✝¹ : D ⊆ (loopyOn E).E
left✝ : Disjoint C D
⊢ loopyOn E ／ C ＼ D = loopyOn (loopyOn E ／ C ＼ D).E