Theorem: Matroid.comap_indep_iff_of_injOn (Matroid/Map.lean)

State before:
α : Type u_1
β : Type u_2
f : α → β
E I s : Set α
M : Matroid α
N : Matroid β
hf : InjOn f (f ⁻¹' N.E)
⊢ (N.comap f).Indep I ↔ N.Indep (f '' I)
Tactic:
rw [comap_indep_iff, and_iff_left_iff_imp]
State after:
α : Type u_1
β : Type u_2
f : α → β
E I s : Set α
M : Matroid α
N : Matroid β
hf : InjOn f (f ⁻¹' N.E)
⊢ N.Indep (f '' I) → InjOn f I

State before:
α : Type u_1
β : Type u_2
f : α → β
E I s : Set α
M : Matroid α
N : Matroid β
hf : InjOn f (f ⁻¹' N.E)
⊢ N.Indep (f '' I) → InjOn f I
Tactic:
refine fun hi ↦ hf.mono <| subset_trans ?_ (preimage_mono hi.subset_ground)
State after:
α : Type u_1
β : Type u_2
f : α → β
E I s : Set α
M : Matroid α
N : Matroid β
hf : InjOn f (f ⁻¹' N.E)
hi : N.Indep (f '' I)
⊢ I ⊆ f ⁻¹' (f '' I)

State before:
α : Type u_1
β : Type u_2
f : α → β
E I s : Set α
M : Matroid α
N : Matroid β
hf : InjOn f (f ⁻¹' N.E)
hi : N.Indep (f '' I)
⊢ I ⊆ f ⁻¹' (f '' I)
Tactic:
apply subset_preimage_image
State after:
no goals