intro I hI hIC
α : Type u_1
M : Matroid α
C✝ C' I X K C₁ C₂ R : Set α
e✝ f x y : α
β : Type u_2
N : Matroid β
e : M ≂ N
C : Set ↑M.E
hC : M.Circuit ↑C
⊢ ∀ ⦃I : Set β⦄, N.Dep I → I ⊆ ↑(⇑e '' C) → I = ↑(⇑e '' C)
α : Type u_1
M : Matroid α
C✝ C' I✝ X K C₁ C₂ R : Set α
e✝ f x y : α
β : Type u_2
N : Matroid β
e : M ≂ N
C : Set ↑M.E
hC : M.Circuit ↑C
I : Set β
hI : N.Dep I
hIC : I ⊆ ↑(⇑e '' C)
⊢ I = ↑(⇑e '' C)