simp only [image_subset_iff, Subtype.coe_preimage_self, subset_univ, basis_iff_mem_maximals,
  mem_maximals_iff, mem_setOf_eq, ← e.indep_image_iff, preimage_val_image_val_eq_self, and_imp,
  preimage_image, and_congr_right_iff]
α : Type u_1
β : Type u_2
M : Matroid α
N : Matroid β
e : M ≂ N
I X : Set ↑M.E
⊢ M.Basis ↑I ↑X ↔ N.Basis ↑(⇑e '' I) ↑(⇑e '' X)
α : Type u_1
β : Type u_2
M : Matroid α
N : Matroid β
e : M ≂ N
I X : Set ↑M.E
⊢ M.Indep ↑I →
    I ⊆ X →
      ((∀ ⦃y : Set α⦄, M.Indep y → y ⊆ ↑X → I ⊆ Subtype.val ⁻¹' y → ↑I = y) ↔
        ∀ ⦃y : Set β⦄, N.Indep y → y ⊆ ↑(⇑e '' X) → I ⊆ ⇑e ⁻¹' (Subtype.val ⁻¹' y) → ↑(⇑e '' I) = y)