Theorem: Matroid.Loopless.of_restrict_contract (Matroid/Simple.lean)

State before:
α : Type u_1
M N : Matroid α
e f g : α
I X P D C : Set α
hC : (M ↾ C).Loopless
h : (M ／ C).Loopless
⊢ M.Loopless
Tactic:
rw [loopless_iff_cl_empty] at *
State after:
α : Type u_1
M N : Matroid α
e f g : α
I X P D C : Set α
hC : (M ↾ C).cl ∅ = ∅
h : (M ／ C).cl ∅ = ∅
⊢ M.cl ∅ = ∅

State before:
α : Type u_1
M N : Matroid α
e f g : α
I X P D C : Set α
hC : (M ↾ C).cl ∅ = ∅
h : (M ／ C).cl ∅ = ∅
⊢ M.cl ∅ = ∅
Tactic:
rw [contract_loops_eq, diff_eq_empty] at h
State after:
α : Type u_1
M N : Matroid α
e f g : α
I X P D C : Set α
hC : (M ↾ C).cl ∅ = ∅
h : M.cl C ⊆ C
⊢ M.cl ∅ = ∅

State before:
α : Type u_1
M N : Matroid α
e f g : α
I X P D C : Set α
hC : (M ↾ C).cl ∅ = ∅
h : M.cl C ⊆ C
⊢ M.cl ∅ = ∅
Tactic:
rw [restrict_cl_eq', empty_inter, union_empty_iff] at hC
State after:
α : Type u_1
M N : Matroid α
e f g : α
I X P D C : Set α
hC : M.cl ∅ ∩ C = ∅ ∧ C \ M.E = ∅
h : M.cl C ⊆ C
⊢ M.cl ∅ = ∅

State before:
α : Type u_1
M N : Matroid α
e f g : α
I X P D C : Set α
hC : M.cl ∅ ∩ C = ∅ ∧ C \ M.E = ∅
h : M.cl C ⊆ C
⊢ M.cl ∅ = ∅
Tactic:
rw [← inter_union_diff (s := M.cl ∅) (t := C), hC.1, empty_union, diff_eq_empty]
State after:
α : Type u_1
M N : Matroid α
e f g : α
I X P D C : Set α
hC : M.cl ∅ ∩ C = ∅ ∧ C \ M.E = ∅
h : M.cl C ⊆ C
⊢ M.cl ∅ ⊆ C

State before:
α : Type u_1
M N : Matroid α
e f g : α
I X P D C : Set α
hC : M.cl ∅ ∩ C = ∅ ∧ C \ M.E = ∅
h : M.cl C ⊆ C
⊢ M.cl ∅ ⊆ C
Tactic:
exact (M.cl_subset_cl <| empty_subset C).trans h
State after:
no goals