Theorem: Matroid.flat_contract_iff (Matroid/Flat.lean)

State before:
α : Type u_1
M : Matroid α
I F X Y F' F₀ F₁ F₂ P L H H₁ H₂ H' B C K : Set α
e f : α
hC : autoParam (C ⊆ M.E) _auto✝
⊢ (M ／ C).Flat F ↔ M.Flat (F ∪ C) ∧ Disjoint F C
Tactic:
rw [flat_iff_cl_self, contract_cl_eq, subset_antisymm_iff, subset_diff, diff_subset_iff,
  union_comm C, ← and_assoc, and_congr_left_iff, flat_iff_cl_self, subset_antisymm_iff,
  and_congr_right_iff]
State after:
α : Type u_1
M : Matroid α
I F X Y F' F₀ F₁ F₂ P L H H₁ H₂ H' B C K : Set α
e f : α
hC : autoParam (C ⊆ M.E) _auto✝
⊢ Disjoint F C → M.cl (F ∪ C) ⊆ F ∪ C → (F ⊆ M.cl (F ∪ C) ↔ F ∪ C ⊆ M.cl (F ∪ C))

State before:
α : Type u_1
M : Matroid α
I F X Y F' F₀ F₁ F₂ P L H H₁ H₂ H' B C K : Set α
e f : α
hC : autoParam (C ⊆ M.E) _auto✝
⊢ Disjoint F C → M.cl (F ∪ C) ⊆ F ∪ C → (F ⊆ M.cl (F ∪ C) ↔ F ∪ C ⊆ M.cl (F ∪ C))
Tactic:
exact fun _ _ ↦ ⟨fun h ↦ M.subset_cl _ (union_subset (h.trans (M.cl_subset_ground _)) hC),
  fun h ↦ subset_union_left.trans h⟩
State after:
no goals