Theorem: Matroid.point_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).Point P ↔ (M.cl C ⋖[M] (C ∪ P)) ∧ Disjoint P C
Tactic:
rw [Point, flat_contract_iff, covBy_iff_relRank_eq_one, relRank_cl_left,
  union_comm C, ← relRank_eq_relRank_union, and_iff_right (cl_flat _ _),
  ← relRank_eq_er_contract, and_assoc, and_assoc, and_congr_right_iff, and_comm,
  and_congr_left_iff, iff_and_self]
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✝
⊢ M.Flat (P ∪ C) → Disjoint P C → M.relRank C P = 1 → M.cl C ⊆ P ∪ 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✝
⊢ M.Flat (P ∪ C) → Disjoint P C → M.relRank C P = 1 → M.cl C ⊆ P ∪ C
Tactic:
rintro h - -
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✝
h : M.Flat (P ∪ C)
⊢ M.cl C ⊆ P ∪ 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✝
h : M.Flat (P ∪ C)
⊢ M.cl C ⊆ P ∪ C
Tactic:
rw [← h.cl]
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✝
h : M.Flat (P ∪ C)
⊢ M.cl C ⊆ M.cl (P ∪ 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✝
h : M.Flat (P ∪ C)
⊢ M.cl C ⊆ M.cl (P ∪ C)
Tactic:
exact M.cl_subset_cl subset_union_right
State after:
no goals