Theorem: Matroid.restrictSubtype_dual (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 α
⊢ (M.restrictSubtype M.E)✶ = M✶.restrictSubtype M.E
Tactic:
rw [restrictSubtype, ← comapOn_preimage_eq, comapOn_dual_eq_of_bijOn, restrict_ground_eq_self,
  ← dual_ground, comapOn_preimage_eq, restrictSubtype, restrict_ground_eq_self]
State after:
α : Type u_1
β : Type u_2
f : α → β
E✝ I✝ s : Set α
M✝ : Matroid α
N✝ : Matroid β
E X I : Set α
M N : Matroid α
⊢ BijOn Subtype.val (M.E ↓∩ (M ↾ M.E).E) (M ↾ M.E).E

State before:
α : Type u_1
β : Type u_2
f : α → β
E✝ I✝ s : Set α
M✝ : Matroid α
N✝ : Matroid β
E X I : Set α
M N : Matroid α
⊢ BijOn Subtype.val (M.E ↓∩ (M ↾ M.E).E) (M ↾ M.E).E
Tactic:
exact ⟨by simp [MapsTo], Subtype.val_injective.injOn, by simp [SurjOn, Subset.rfl]⟩
State after:
no goals

State before:
α : Type u_1
β : Type u_2
f : α → β
E✝ I✝ s : Set α
M✝ : Matroid α
N✝ : Matroid β
E X I : Set α
M N : Matroid α
⊢ MapsTo Subtype.val (M.E ↓∩ (M ↾ M.E).E) (M ↾ M.E).E
Tactic:
simp [MapsTo]
State after:
no goals

State before:
α : Type u_1
β : Type u_2
f : α → β
E✝ I✝ s : Set α
M✝ : Matroid α
N✝ : Matroid β
E X I : Set α
M N : Matroid α
⊢ SurjOn Subtype.val (M.E ↓∩ (M ↾ M.E).E) (M ↾ M.E).E
Tactic:
simp [SurjOn, Subset.rfl]
State after:
no goals