rw [eq_loopyOn_iff]
α : Type u_1
β : Type u_2
f✝ : α → β
E✝ I s : Set α
M : Matroid α
N : Matroid β
f : α → β
E : Set β
⊢ (loopyOn E).comap f = loopyOn (f ⁻¹' E)
α : Type u_1
β : Type u_2
f✝ : α → β
E✝ I s : Set α
M : Matroid α
N : Matroid β
f : α → β
E : Set β
⊢ ((loopyOn E).comap f).E = f ⁻¹' E ∧ ∀ X ⊆ ((loopyOn E).comap f).E, ((loopyOn E).comap f).Indep X → X = ∅