rw [← ground_eq_empty_iff, loopyOn_ground] at hLoopy
case refine_1.inl.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 β✝
β : Type u_7
E : Set β
hLoopy : loopyOn E = emptyOn β
h : emptyOn α ≂ loopyOn E
⊢ Nonempty (↑∅ ≃ ↑E)
case refine_1.inl.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 β✝
β : Type u_7
E : Set β
hLoopy : E = ∅
h : emptyOn α ≂ loopyOn E
⊢ Nonempty (↑∅ ≃ ↑E)