Theorem: Matroid.restrict_indep_eq_freeOn (Matroid/Minor/Basic.lean)

State before:
α : Type u_1
M M' N : Matroid α
e f : α
I J R B X Y Z K E : Set α
hI : M.Indep I
⊢ M ↾ I = freeOn I
Tactic:
refine eq_of_indep_iff_indep_forall rfl (fun J _ ↦ ?_)
State after:
α : Type u_1
M M' N : Matroid α
e f : α
I J✝ R B X Y Z K E : Set α
hI : M.Indep I
J : Set α
x✝ : J ⊆ (M ↾ I).E
⊢ (M ↾ I).Indep J ↔ (freeOn I).Indep J

State before:
α : Type u_1
M M' N : Matroid α
e f : α
I J✝ R B X Y Z K E : Set α
hI : M.Indep I
J : Set α
x✝ : J ⊆ (M ↾ I).E
⊢ (M ↾ I).Indep J ↔ (freeOn I).Indep J
Tactic:
simp only [restrict_ground_eq, restrict_indep_iff, freeOn_indep_iff, and_iff_right_iff_imp]
State after:
α : Type u_1
M M' N : Matroid α
e f : α
I J✝ R B X Y Z K E : Set α
hI : M.Indep I
J : Set α
x✝ : J ⊆ (M ↾ I).E
⊢ J ⊆ I → M.Indep J

State before:
α : Type u_1
M M' N : Matroid α
e f : α
I J✝ R B X Y Z K E : Set α
hI : M.Indep I
J : Set α
x✝ : J ⊆ (M ↾ I).E
⊢ J ⊆ I → M.Indep J
Tactic:
exact hI.subset
State after:
no goals