rw [← isIso_dual_iff, freeOn_dual_eq, isIso_loopyOn_iff, ← eq_dual_iff_dual_eq, dual_ground,
  loopyOn_dual_eq]
α : 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 ≂ freeOn E ↔ M = freeOn M.E ∧ Nonempty (↑M.E ≃ ↑E)
no goals