simp_rw [comapOn_base_iff, and_congr_left_iff, and_imp,
  basis'_iff_basis_inter_ground, inter_eq_self_of_subset_right h, basis_ground_iff, implies_true]
α : Type u_1
β : Type u_2
f : α → β
E✝ I s : Set α
M : Matroid α
N : Matroid β
E : Set α
h : SurjOn f E N.E
B : Set α
⊢ (N.comapOn E f).Base B ↔ N.Base (f '' B) ∧ B ⊆ E ∧ InjOn f B
no goals