Theorem: Matroid.cl_inter_eq_of_subset_coloops (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 X : Set α
hK : K ⊆ M✶.cl ∅
⊢ M.cl X ∩ K = X ∩ K
Tactic:
have hKE : K ∩ M.E = K := by
  rw [inter_eq_left, ← dual_ground]; exact hK.trans (cl_subset_ground _ _)
State after:
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I X✝ Y Z F C K X : Set α
hK : K ⊆ M✶.cl ∅
hKE : K ∩ M.E = K
⊢ M.cl X ∩ K = X ∩ K

State before:
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I X✝ Y Z F C K X : Set α
hK : K ⊆ M✶.cl ∅
hKE : K ∩ M.E = K
⊢ M.cl X ∩ K = X ∩ K
Tactic:
rw [← hKE, ← inter_assoc X, inter_right_comm, hKE, ← cl_inter_ground,
  subset_antisymm_iff, and_iff_left (inter_subset_inter_left K (M.subset_cl _)),
  ← inter_eq_self_of_subset_right hK, ← inter_assoc, cl_inter_coloops_eq,
  inter_assoc]
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 X : Set α
hK : K ⊆ M✶.cl ∅
⊢ K ∩ M.E = K
Tactic:
rw [inter_eq_left, ← dual_ground]
State after:
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I X✝ Y Z F C K X : Set α
hK : K ⊆ M✶.cl ∅
⊢ K ⊆ M✶.E

State before:
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I X✝ Y Z F C K X : Set α
hK : K ⊆ M✶.cl ∅
⊢ K ⊆ M✶.E
Tactic:
exact hK.trans (cl_subset_ground _ _)
State after:
no goals