Theorem: Matroid.ConnectedTo.exists_circuit_of_ne (Matroid/Connectivity.lean)

State before:
α : Type u_1
M : Matroid α
C K : Set α
e f g : α
h : M.ConnectedTo e f
hne : e ≠ f
⊢ ∃ C, M.Circuit C ∧ e ∈ C ∧ f ∈ C
Tactic:
simpa [ConnectedTo, hne] using h
State after:
no goals