Theorem: Matroid.contract_spanning_iff' (Matroid/Minor/Basic.lean)

State before:
α : Type u_1
M✝ M' N : Matroid α
e f : α
I J R B X✝ Y Z K C✝ C₁ C₂ : Set α
M : Matroid α
C X : Set α
⊢ (M ／ C).Spanning X ↔ M.Spanning (X ∪ C ∩ M.E) ∧ Disjoint X C
Tactic:
simp_rw [Spanning, contract_cl_eq, contract_ground, subset_diff, union_subset_iff,
  and_iff_left inter_subset_right, ← and_assoc, and_congr_left_iff,
  subset_antisymm_iff, subset_diff, diff_subset_iff, and_iff_left disjoint_sdiff_left,
  and_iff_right (M.cl_subset_ground _ ),
  and_iff_right (subset_union_of_subset_right (M.cl_subset_ground _) C)]
State after:
α : Type u_1
M✝ M' N : Matroid α
e f : α
I J R B X✝ Y Z K C✝ C₁ C₂ : Set α
M : Matroid α
C X : Set α
⊢ Disjoint X C → X ⊆ M.E → (M.E ⊆ C ∪ M.cl (X ∪ C) ↔ M.E ⊆ M.cl (X ∪ C ∩ M.E))

State before:
α : Type u_1
M✝ M' N : Matroid α
e f : α
I J R B X✝ Y Z K C✝ C₁ C₂ : Set α
M : Matroid α
C X : Set α
⊢ Disjoint X C → X ⊆ M.E → (M.E ⊆ C ∪ M.cl (X ∪ C) ↔ M.E ⊆ M.cl (X ∪ C ∩ M.E))
Tactic:
rw [← inter_eq_left (s := M.E), inter_union_distrib_left,
  inter_eq_self_of_subset_right (M.cl_subset_ground _), subset_antisymm_iff, union_subset_iff,
  and_iff_right inter_subset_left, union_eq_self_of_subset_left (s := M.E ∩ C),
  and_iff_right (M.cl_subset_ground _), Iff.comm, ← cl_union_cl_right_eq,cl_inter_ground,
  cl_union_cl_right_eq]
State after:
α : Type u_1
M✝ M' N : Matroid α
e f : α
I J R B X✝ Y Z K C✝ C₁ C₂ : Set α
M : Matroid α
C X : Set α
⊢ Disjoint X C → X ⊆ M.E → (M.E ⊆ M.cl (X ∪ C) ↔ M.E ⊆ M.cl (X ∪ C))

α : Type u_1
M✝ M' N : Matroid α
e f : α
I J R B X✝ Y Z K C✝ C₁ C₂ : Set α
M : Matroid α
C X : Set α
⊢ M.E ∩ C ⊆ M.cl (X ∪ C)

State before:
α : Type u_1
M✝ M' N : Matroid α
e f : α
I J R B X✝ Y Z K C✝ C₁ C₂ : Set α
M : Matroid α
C X : Set α
⊢ M.E ∩ C ⊆ M.cl (X ∪ C)
Tactic:
exact (M.subset_cl _).trans
  (M.cl_subset_cl (inter_subset_right.trans subset_union_right))
State after:
no goals

State before:
α : Type u_1
M✝ M' N : Matroid α
e f : α
I J R B X✝ Y Z K C✝ C₁ C₂ : Set α
M : Matroid α
C X : Set α
⊢ Disjoint X C → X ⊆ M.E → (M.E ⊆ M.cl (X ∪ C) ↔ M.E ⊆ M.cl (X ∪ C))
Tactic:
exact fun _ _ ↦ Iff.rfl
State after:
no goals