refine eq_of_base_iff_base_forall (by simp) (fun B hB ↦ ?_)
α : Type u_1
β : Type u_2
f : α → β
E✝ I s : Set α
M : Matroid α
N : Matroid β
E : Set α
h : BijOn f E N.E
⊢ (N.comapOn E f)✶ = N✶.comapOn E f
α : Type u_1
β : Type u_2
f : α → β
E✝ I s : Set α
M : Matroid α
N : Matroid β
E : Set α
h : BijOn f E N.E
B : Set α
hB : B ⊆ (N.comapOn E f)✶.E
⊢ (N.comapOn E f)✶.Base B ↔ (N✶.comapOn E f).Base B