rintro ⟨hM, ⟨e⟩⟩
case refine_2
α : Type u_1
β✝ : Type u_2
γ : Type u_3
α₁ : Type u_4
α₂ : Type u_5
α₃ : Type u_6
M✝¹ : Matroid α
N✝ : Matroid β✝
B I D X Y : Set α
M✝ : Matroid α
N : Matroid β✝
M : Matroid α
β : Type u_7
E : Set β
⊢ M = loopyOn M.E ∧ Nonempty (↑M.E ≃ ↑E) → M ≂ loopyOn E
case refine_2.intro.intro
α : Type u_1
β✝ : Type u_2
γ : Type u_3
α₁ : Type u_4
α₂ : Type u_5
α₃ : Type u_6
M✝¹ : Matroid α
N✝ : Matroid β✝
B I D X Y : Set α
M✝ : Matroid α
N : Matroid β✝
M : Matroid α
β : Type u_7
E : Set β
hM : M = loopyOn M.E
e : ↑M.E ≃ ↑E
⊢ M ≂ loopyOn E