Theorem: Matroid.cl_inter_coloops_eq (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 α
M : Matroid α
X : Set α
⊢ M.cl X ∩ M✶.cl ∅ = X ∩ M✶.cl ∅
Tactic:
simp_rw [Set.ext_iff, mem_inter_iff, ← coloop_iff_mem_cl_empty, and_congr_left_iff]
State after:
α : Type u_1
β : Type u_2
M✝ N : Matroid α
e f : α
B L L' I X✝ Y Z F C K : Set α
M : Matroid α
X : Set α
⊢ ∀ (x : α), M.Coloop x → (x ∈ M.cl X ↔ x ∈ X)

State before:
α : Type u_1
β : Type u_2
M✝ N : Matroid α
e f : α
B L L' I X✝ Y Z F C K : Set α
M : Matroid α
X : Set α
⊢ ∀ (x : α), M.Coloop x → (x ∈ M.cl X ↔ x ∈ X)
Tactic:
intro e he
State after:
α : Type u_1
β : Type u_2
M✝ N : Matroid α
e✝ f : α
B L L' I X✝ Y Z F C K : Set α
M : Matroid α
X : Set α
e : α
he : M.Coloop e
⊢ e ∈ M.cl X ↔ e ∈ X

State before:
α : Type u_1
β : Type u_2
M✝ N : Matroid α
e✝ f : α
B L L' I X✝ Y Z F C K : Set α
M : Matroid α
X : Set α
e : α
he : M.Coloop e
⊢ e ∈ M.cl X ↔ e ∈ X
Tactic:
rw [he.mem_cl_iff_mem]
State after:
no goals