exact hC.1.mem_connectedTo_mem heC hfC
case inr.intro.intro.intro
α : Type u_1
M : Matroid α
C✝ K : Set α
e f g : α
R : Set α
hR : R ⊆ M.E
hef : (M ↾ R).ConnectedTo e f
hne : e ≠ f
C : Set α
hC : M.Circuit C ∧ C ⊆ R
heC : e ∈ C
hfC : f ∈ C
⊢ M.ConnectedTo e f
no goals