simp_rw [he.cl_eq_cl_iff_circuit_of_ne hne, or_iff_right hne,
  circuit_iff_dep_forall_diff_singleton_indep, dep_iff, insert_subset_iff, singleton_subset_iff,
  and_iff_left hf.mem_ground, and_iff_left he.mem_ground, and_iff_left_iff_imp]
case inr
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I X Y Z F C K : Set α
he : M.Nonloop e
hf : M.Nonloop f
hne : e ≠ f
⊢ M.cl {e} = M.cl {f} ↔ e = f ∨ ¬M.Indep {e, f}
case inr
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I X Y Z F C K : Set α
he : M.Nonloop e
hf : M.Nonloop f
hne : e ≠ f
⊢ ¬M.Indep {e, f} → ∀ e_1 ∈ {e, f}, M.Indep ({e, f} \ {e_1})