refine ⟨fun h ↦ ⟨by obtain ⟨C, D, _, _, _, rfl⟩ := h; simp, h.subset⟩, fun ⟨h, hss⟩ ↦ ?_⟩
α : Type u_1
M M' N : Matroid α
e f : α
I J R B X Y Z K E : Set α
⊢ M ≤m loopyOn E ↔ M = loopyOn M.E ∧ M.E ⊆ E
α : Type u_1
M M' N : Matroid α
e f : α
I J R B X Y Z K E : Set α
x✝ : M = loopyOn M.E ∧ M.E ⊆ E
h : M = loopyOn M.E
hss : M.E ⊆ E
⊢ M ≤m loopyOn E