intro hI hIX
α : 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)
α : Type u_1
β : Type u_2
M : Matroid α
N : Matroid β
e : M ≂ N
I X : Set ↑M.E
hI : M.Indep ↑I
hIX : 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