Theorem: Matroid.indep_iff_restrict_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 α
⊢ M.Indep I ↔ M ↾ I = freeOn I
Tactic:
refine ⟨restrict_indep_eq_freeOn, fun h ↦ ?_⟩
State after:
α : Type u_1
M M' N : Matroid α
e f : α
I J R B X Y Z K E : Set α
h : M ↾ I = freeOn I
⊢ M.Indep I

State before:
α : Type u_1
M M' N : Matroid α
e f : α
I J R B X Y Z K E : Set α
h : M ↾ I = freeOn I
⊢ M.Indep I
Tactic:
have h' := restrict_indep_iff (M := M) (I := I) (R := I)
State after:
α : Type u_1
M M' N : Matroid α
e f : α
I J R B X Y Z K E : Set α
h : M ↾ I = freeOn I
h' : (M ↾ I).Indep I ↔ M.Indep I ∧ I ⊆ I
⊢ M.Indep I

State before:
α : Type u_1
M M' N : Matroid α
e f : α
I J R B X Y Z K E : Set α
h : M ↾ I = freeOn I
h' : (M ↾ I).Indep I ↔ M.Indep I ∧ I ⊆ I
⊢ M.Indep I
Tactic:
rwa [h, freeOn_indep_iff, iff_true_intro Subset.rfl, and_true, true_iff] at h'
State after:
no goals