Theorem: Matroid.contract_loop_iff_mem_cl (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 ／ C).Loop e ↔ e ∈ M.cl C \ C
Tactic:
obtain ⟨I, D, hI, -, -, hM⟩ := M.exists_eq_contract_indep_delete C
State after:
case intro.intro.intro.intro.intro
α : Type u_1
M M' N : Matroid α
e f : α
I✝ J R B X Y Z K C C₁ C₂ I D : Set α
hI : M.Basis I (C ∩ M.E)
hM : M ／ C = M ／ I ＼ D
⊢ (M ／ C).Loop e ↔ e ∈ M.cl C \ C

State before:
case intro.intro.intro.intro.intro
α : Type u_1
M M' N : Matroid α
e f : α
I✝ J R B X Y Z K C C₁ C₂ I D : Set α
hI : M.Basis I (C ∩ M.E)
hM : M ／ C = M ／ I ＼ D
⊢ (M ／ C).Loop e ↔ e ∈ M.cl C \ C
Tactic:
rw [hM, delete_loop_iff, ← singleton_dep, hI.indep.contract_dep_iff, disjoint_singleton_left,
  singleton_union, hI.indep.insert_dep_iff, mem_diff, ← M.cl_inter_ground C, hI.cl_eq_cl,
  and_comm (a := e ∉ I), and_self_right, ← mem_diff, ← mem_diff, diff_diff]
State after:
case intro.intro.intro.intro.intro
α : Type u_1
M M' N : Matroid α
e f : α
I✝ J R B X Y Z K C C₁ C₂ I D : Set α
hI : M.Basis I (C ∩ M.E)
hM : M ／ C = M ／ I ＼ D
⊢ e ∈ M.cl (C ∩ M.E) \ (I ∪ D) ↔ e ∈ M.cl (C ∩ M.E) \ C

State before:
case intro.intro.intro.intro.intro
α : Type u_1
M M' N : Matroid α
e f : α
I✝ J R B X Y Z K C C₁ C₂ I D : Set α
hI : M.Basis I (C ∩ M.E)
hM : M ／ C = M ／ I ＼ D
⊢ e ∈ M.cl (C ∩ M.E) \ (I ∪ D) ↔ e ∈ M.cl (C ∩ M.E) \ C
Tactic:
apply_fun Matroid.E at hM
State after:
case intro.intro.intro.intro.intro
α : Type u_1
M M' N : Matroid α
e f : α
I✝ J R B X Y Z K C C₁ C₂ I D : Set α
hI : M.Basis I (C ∩ M.E)
hM : (M ／ C).E = (M ／ I ＼ D).E
⊢ e ∈ M.cl (C ∩ M.E) \ (I ∪ D) ↔ e ∈ M.cl (C ∩ M.E) \ C

State before:
case intro.intro.intro.intro.intro
α : Type u_1
M M' N : Matroid α
e f : α
I✝ J R B X Y Z K C C₁ C₂ I D : Set α
hI : M.Basis I (C ∩ M.E)
hM : (M ／ C).E = (M ／ I ＼ D).E
⊢ e ∈ M.cl (C ∩ M.E) \ (I ∪ D) ↔ e ∈ M.cl (C ∩ M.E) \ C
Tactic:
rw [delete_ground, contract_ground, contract_ground, diff_diff, diff_eq_diff_iff_inter_eq_inter,
  inter_comm, inter_comm M.E] at hM
State after:
case intro.intro.intro.intro.intro
α : Type u_1
M M' N : Matroid α
e f : α
I✝ J R B X Y Z K C C₁ C₂ I D : Set α
hI : M.Basis I (C ∩ M.E)
hM : C ∩ M.E = (I ∪ D) ∩ M.E
⊢ e ∈ M.cl (C ∩ M.E) \ (I ∪ D) ↔ e ∈ M.cl (C ∩ M.E) \ C

State before:
case intro.intro.intro.intro.intro
α : Type u_1
M M' N : Matroid α
e f : α
I✝ J R B X Y Z K C C₁ C₂ I D : Set α
hI : M.Basis I (C ∩ M.E)
hM : C ∩ M.E = (I ∪ D) ∩ M.E
⊢ e ∈ M.cl (C ∩ M.E) \ (I ∪ D) ↔ e ∈ M.cl (C ∩ M.E) \ C
Tactic:
exact
  ⟨fun h ↦ ⟨h.1, fun heC ↦ h.2 (hM.subset ⟨heC, M.cl_subset_ground _ h.1⟩).1⟩, fun h ↦
    ⟨h.1, fun h' ↦ h.2 (hM.symm.subset ⟨h', M.cl_subset_ground _ h.1⟩).1⟩⟩
State after:
no goals