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

State before:
α : Type u_1
β : Type u_2
f : α → β
E✝ I✝ s : Set α
M✝ : Matroid α
N✝ : Matroid β
E X I : Set α
M N : Matroid α
hIX : I ⊆ X
⊢ (M.restrictSubtype X).Indep (X ↓∩ I) ↔ M.Indep I
Tactic:
rw [restrictSubtype_indep_iff, image_preimage_eq_iff.2]
State after:
α : Type u_1
β : Type u_2
f : α → β
E✝ I✝ s : Set α
M✝ : Matroid α
N✝ : Matroid β
E X I : Set α
M N : Matroid α
hIX : I ⊆ X
⊢ I ⊆ range Subtype.val

State before:
α : Type u_1
β : Type u_2
f : α → β
E✝ I✝ s : Set α
M✝ : Matroid α
N✝ : Matroid β
E X I : Set α
M N : Matroid α
hIX : I ⊆ X
⊢ I ⊆ range Subtype.val
Tactic:
simpa
State after:
no goals