Theorem: Matroid.relRank_eq_one_iff (Matroid/Minor/Rank.lean)

State before:
α : Type u_1
M N : Matroid α
I J C D X Y Z : Set α
e f : α
hY : autoParam (Y ⊆ M.E) _auto✝
⊢ M.relRank X Y = 1 ↔ ∃ e ∈ Y \ M.cl X, Y ⊆ M.cl (insert e X)
Tactic:
rw [← relRank_cl_left, relRank_eq_er_diff_contract, er_eq_one_iff
  (show Y \ (M.cl X) ⊆ (M ／ (M.cl X)).E from diff_subset_diff_left hY)]
State after:
α : Type u_1
M N : Matroid α
I J C D X Y Z : Set α
e f : α
hY : autoParam (Y ⊆ M.E) _auto✝
⊢ (∃ e ∈ Y \ M.cl X, (M ／ M.cl X).Nonloop e ∧ Y \ M.cl X ⊆ (M ／ M.cl X).cl {e}) ↔
    ∃ e ∈ Y \ M.cl X, Y ⊆ M.cl (insert e X)

State before:
α : Type u_1
M N : Matroid α
I J C D X Y Z : Set α
e f : α
hY : autoParam (Y ⊆ M.E) _auto✝
⊢ (∃ e ∈ Y \ M.cl X, (M ／ M.cl X).Nonloop e ∧ Y \ M.cl X ⊆ (M ／ M.cl X).cl {e}) ↔
    ∃ e ∈ Y \ M.cl X, Y ⊆ M.cl (insert e X)
Tactic:
simp only [contract_cl_eq, singleton_union, diff_subset_iff, diff_union_self,
  cl_insert_cl_eq_cl_insert, union_diff_self, contract_nonloop_iff, cl_cl,
  union_eq_self_of_subset_left (M.cl_subset_cl (subset_insert _ X))]
State after:
α : Type u_1
M N : Matroid α
I J C D X Y Z : Set α
e f : α
hY : autoParam (Y ⊆ M.E) _auto✝
⊢ (∃ e ∈ Y \ M.cl X, e ∈ M.E \ M.cl X ∧ Y ⊆ M.cl (insert e X)) ↔ ∃ e ∈ Y \ M.cl X, Y ⊆ M.cl (insert e X)

State before:
α : Type u_1
M N : Matroid α
I J C D X Y Z : Set α
e f : α
hY : autoParam (Y ⊆ M.E) _auto✝
⊢ (∃ e ∈ Y \ M.cl X, e ∈ M.E \ M.cl X ∧ Y ⊆ M.cl (insert e X)) ↔ ∃ e ∈ Y \ M.cl X, Y ⊆ M.cl (insert e X)
Tactic:
exact ⟨fun ⟨e,he,_,hY'⟩ ↦ ⟨e,he,hY'⟩, fun ⟨e, he, hY'⟩ ↦ ⟨e, he, ⟨hY he.1, he.2⟩, hY'⟩⟩
State after:
no goals