Theorem: Matroid.contract_nonloop_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 ／ C).Nonloop e ↔ e ∈ M.E \ M.cl C
Tactic:
rw [nonloop_iff_mem_compl_loops, contract_ground, contract_loops_eq]
State after:
α : Type u_1
M M' N : Matroid α
e f : α
I J R B X Y Z K C C₁ C₂ : Set α
⊢ e ∈ (M.E \ C) \ (M.cl C \ C) ↔ e ∈ M.E \ M.cl C

State before:
α : Type u_1
M M' N : Matroid α
e f : α
I J R B X Y Z K C C₁ C₂ : Set α
⊢ e ∈ (M.E \ C) \ (M.cl C \ C) ↔ e ∈ M.E \ M.cl C
Tactic:
refine ⟨fun ⟨he,heC⟩ ↦ ⟨he.1, fun h ↦ heC ⟨h, he.2⟩⟩,
  fun h ↦ ⟨⟨h.1, fun heC ↦ h.2 ?_⟩, fun h' ↦ h.2 h'.1⟩⟩
State after:
α : Type u_1
M M' N : Matroid α
e f : α
I J R B X Y Z K C C₁ C₂ : Set α
h : e ∈ M.E \ M.cl C
heC : e ∈ C
⊢ e ∈ M.cl C

State before:
α : Type u_1
M M' N : Matroid α
e f : α
I J R B X Y Z K C C₁ C₂ : Set α
h : e ∈ M.E \ M.cl C
heC : e ∈ C
⊢ e ∈ M.cl C
Tactic:
rw [← cl_inter_ground]
State after:
α : Type u_1
M M' N : Matroid α
e f : α
I J R B X Y Z K C C₁ C₂ : Set α
h : e ∈ M.E \ M.cl C
heC : e ∈ C
⊢ e ∈ M.cl (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 α
h : e ∈ M.E \ M.cl C
heC : e ∈ C
⊢ e ∈ M.cl (C ∩ M.E)
Tactic:
exact (M.subset_cl (C ∩ M.E)) ⟨heC, h.1⟩
State after:
no goals