Theorem: Matroid.eq_of_restrictSubtype_eq (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 α
hM : M.E = E
hN : N.E = E
h : M.restrictSubtype E = N.restrictSubtype E
⊢ M = N
Tactic:
subst hM
State after:
α : Type u_1
β : Type u_2
f : α → β
E I✝ s : Set α
M✝ : Matroid α
N✝ : Matroid β
X I : Set α
M N : Matroid α
hN : N.E = M.E
h : M.restrictSubtype M.E = N.restrictSubtype M.E
⊢ M = N

State before:
α : Type u_1
β : Type u_2
f : α → β
E I✝ s : Set α
M✝ : Matroid α
N✝ : Matroid β
X I : Set α
M N : Matroid α
hN : N.E = M.E
h : M.restrictSubtype M.E = N.restrictSubtype M.E
⊢ M = N
Tactic:
refine eq_of_indep_iff_indep_forall (by rw [hN]) (fun I hI ↦ ?_)
State after:
α : Type u_1
β : Type u_2
f : α → β
E I✝¹ s : Set α
M✝ : Matroid α
N✝ : Matroid β
X I✝ : Set α
M N : Matroid α
hN : N.E = M.E
h : M.restrictSubtype M.E = N.restrictSubtype M.E
I : Set α
hI : I ⊆ M.E
⊢ M.Indep I ↔ N.Indep I

State before:
α : Type u_1
β : Type u_2
f : α → β
E I✝¹ s : Set α
M✝ : Matroid α
N✝ : Matroid β
X I✝ : Set α
M N : Matroid α
hN : N.E = M.E
h : M.restrictSubtype M.E = N.restrictSubtype M.E
I : Set α
hI : I ⊆ M.E
⊢ M.Indep I ↔ N.Indep I
Tactic:
rwa [← restrictSubtype_indep_iff_of_subset hI, h, restrictSubtype_indep_iff_of_subset]
State after:
no goals

State before:
α : Type u_1
β : Type u_2
f : α → β
E I✝ s : Set α
M✝ : Matroid α
N✝ : Matroid β
X I : Set α
M N : Matroid α
hN : N.E = M.E
h : M.restrictSubtype M.E = N.restrictSubtype M.E
⊢ M.E = N.E
Tactic:
rw [hN]
State after:
no goals