Theorem: Matroid.comap_basis'_iff (Matroid/Map.lean)

State before:
α : Type u_1
β : Type u_2
f : α → β
E I✝ s : Set α
M : Matroid α
N : Matroid β
I X : Set α
⊢ (N.comap f).Basis' I X ↔ N.Basis' (f '' I) (f '' X) ∧ I ⊆ X ∧ InjOn f I
Tactic:
simp only [basis'_iff_basis_inter_ground, comap_ground_eq, comap_basis_iff, image_inter_preimage,
  subset_inter_iff, ← and_assoc, and_congr_left_iff, and_iff_left_iff_imp, and_imp]
State after:
α : Type u_1
β : Type u_2
f : α → β
E I✝ s : Set α
M : Matroid α
N : Matroid β
I X : Set α
⊢ InjOn f I → N.Basis (f '' I) (f '' X ∩ N.E) → I ⊆ X → I ⊆ f ⁻¹' N.E

State before:
α : Type u_1
β : Type u_2
f : α → β
E I✝ s : Set α
M : Matroid α
N : Matroid β
I X : Set α
⊢ InjOn f I → N.Basis (f '' I) (f '' X ∩ N.E) → I ⊆ X → I ⊆ f ⁻¹' N.E
Tactic:
exact fun _ h _ ↦ (image_subset_iff.1 h.indep.subset_ground)
State after:
no goals