Theorem: Matroid.basis_iff_empty_of_subset_loops (Matroid/Loop.lean)

State before:
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I X Y Z F C K : Set α
hX : X ⊆ M.cl ∅
⊢ M.Basis I X ↔ I = ∅
Tactic:
refine ⟨fun h ↦ ?_, by rintro rfl; simpa⟩
State after:
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I X Y Z F C K : Set α
hX : X ⊆ M.cl ∅
h : M.Basis I X
⊢ I = ∅

State before:
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I X Y Z F C K : Set α
hX : X ⊆ M.cl ∅
h : M.Basis I X
⊢ I = ∅
Tactic:
replace h := (cl_eq_loops_of_subset hX) ▸ h.basis_cl_right
State after:
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I X Y Z F C K : Set α
hX : X ⊆ M.cl ∅
h : M.Basis I (M.cl ∅)
⊢ I = ∅

State before:
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I X Y Z F C K : Set α
hX : X ⊆ M.cl ∅
h : M.Basis I (M.cl ∅)
⊢ I = ∅
Tactic:
simpa using h
State after:
no goals

State before:
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I X Y Z F C K : Set α
hX : X ⊆ M.cl ∅
⊢ I = ∅ → M.Basis I X
Tactic:
rintro rfl
State after:
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' X Y Z F C K : Set α
hX : X ⊆ M.cl ∅
⊢ M.Basis ∅ X

State before:
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' X Y Z F C K : Set α
hX : X ⊆ M.cl ∅
⊢ M.Basis ∅ X
Tactic:
simpa
State after:
no goals