Theorem: Matroid.restrict_loop_iff (Matroid/Loop.lean)

State before:
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I X Y Z F C K R : Set α
⊢ (M ↾ R).Loop e ↔ e ∈ R ∧ (M.Loop e ∨ e ∉ M.E)
Tactic:
rw [← singleton_dep, restrict_dep_iff, singleton_subset_iff, ← singleton_dep, and_comm,
  and_congr_right_iff, Dep, and_or_right, singleton_subset_iff, and_iff_left or_not,
  or_iff_left_of_imp (fun he hi ↦ he (singleton_subset_iff.1 hi.subset_ground))]
State after:
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I X Y Z F C K R : Set α
⊢ e ∈ R → (¬M.Indep {e} ↔ ¬M.Indep {e})

State before:
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I X Y Z F C K R : Set α
⊢ e ∈ R → (¬M.Indep {e} ↔ ¬M.Indep {e})
Tactic:
simp only [singleton_subset_iff, implies_true]
State after:
no goals