ext e
case intro.intro.intro.intro.intro
α : Type u_1
ι : Type u_2
M✝ : Matroid α
F I✝ J X✝ Y B C R : Set α
e f✝ x y : α
β : Type u_3
M : Matroid α
f : α → β
hf : InjOn f M.E
I X : Set α
hI' : M.Basis I X
hX : f '' X ⊆ f '' M.E
hI : (M.map f hf).Basis (f '' I) (f '' X)
⊢ f '' M.cl I = (M.map f hf).cl (f '' I)
case intro.intro.intro.intro.intro.h
α : Type u_1
ι : Type u_2
M✝ : Matroid α
F I✝ J X✝ Y B C R : Set α
e✝ f✝ x y : α
β : Type u_3
M : Matroid α
f : α → β
hf : InjOn f M.E
I X : Set α
hI' : M.Basis I X
hX : f '' X ⊆ f '' M.E
hI : (M.map f hf).Basis (f '' I) (f '' X)
e : β
⊢ e ∈ f '' M.cl I ↔ e ∈ (M.map f hf).cl (f '' I)