Theorem: Matroid.restrict_subset_loops_eq (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 α
hX : X ⊆ M.cl ∅
⊢ M ↾ X = loopyOn X
Tactic:
refine eq_of_indep_iff_indep_forall rfl (fun I hI ↦ ?_)
State after:
α : Type u_1
M M' N : Matroid α
e f : α
I✝ J R B X Y Z K E : Set α
hX : X ⊆ M.cl ∅
I : Set α
hI : I ⊆ (M ↾ X).E
⊢ (M ↾ X).Indep I ↔ (loopyOn X).Indep I

State before:
α : Type u_1
M M' N : Matroid α
e f : α
I✝ J R B X Y Z K E : Set α
hX : X ⊆ M.cl ∅
I : Set α
hI : I ⊆ (M ↾ X).E
⊢ (M ↾ X).Indep I ↔ (loopyOn X).Indep I
Tactic:
simp only [restrict_indep_iff, loopyOn_indep_iff]
State after:
α : Type u_1
M M' N : Matroid α
e f : α
I✝ J R B X Y Z K E : Set α
hX : X ⊆ M.cl ∅
I : Set α
hI : I ⊆ (M ↾ X).E
⊢ M.Indep I ∧ I ⊆ X ↔ I = ∅

State before:
α : Type u_1
M M' N : Matroid α
e f : α
I✝ J R B X Y Z K E : Set α
hX : X ⊆ M.cl ∅
I : Set α
hI : I ⊆ (M ↾ X).E
⊢ M.Indep I ∧ I ⊆ X ↔ I = ∅
Tactic:
use fun h ↦ h.1.eq_empty_of_subset_loops (h.2.trans hX)
State after:
case mpr
α : Type u_1
M M' N : Matroid α
e f : α
I✝ J R B X Y Z K E : Set α
hX : X ⊆ M.cl ∅
I : Set α
hI : I ⊆ (M ↾ X).E
⊢ I = ∅ → M.Indep I ∧ I ⊆ X

State before:
case mpr
α : Type u_1
M M' N : Matroid α
e f : α
I✝ J R B X Y Z K E : Set α
hX : X ⊆ M.cl ∅
I : Set α
hI : I ⊆ (M ↾ X).E
⊢ I = ∅ → M.Indep I ∧ I ⊆ X
Tactic:
rintro rfl
State after:
case mpr
α : Type u_1
M M' N : Matroid α
e f : α
I J R B X Y Z K E : Set α
hX : X ⊆ M.cl ∅
hI : ∅ ⊆ (M ↾ X).E
⊢ M.Indep ∅ ∧ ∅ ⊆ X

State before:
case mpr
α : Type u_1
M M' N : Matroid α
e f : α
I J R B X Y Z K E : Set α
hX : X ⊆ M.cl ∅
hI : ∅ ⊆ (M ↾ X).E
⊢ M.Indep ∅ ∧ ∅ ⊆ X
Tactic:
simp
State after:
no goals