refine Circuit.mem_connectedTo_mem hK.of_contract.circuit (mem_fundCocct _ _ _) ?_
case inr.intro.intro.intro.intro.intro
α : Type u_1
M : Matroid α
C✝ K : Set α
e f g : α
h : M.ConnectedTo e f
hne : e ≠ f
C : Set α
hC : M.Circuit C
heC : e ∈ C
hfC : f ∈ C
hpara : (M ／ (C \ {e, f})).Parallel e f
B : Set α
hB : (M ／ (C \ {e, f})).Base B
heB : e ∈ B
hK : (M ／ (C \ {e, f})).Cocircuit (fundCocct e B)
⊢ M✶.ConnectedTo e f
case inr.intro.intro.intro.intro.intro
α : Type u_1
M : Matroid α
C✝ K : Set α
e f g : α
h : M.ConnectedTo e f
hne : e ≠ f
C : Set α
hC : M.Circuit C
heC : e ∈ C
hfC : f ∈ C
hpara : (M ／ (C \ {e, f})).Parallel e f
B : Set α
hB : (M ／ (C \ {e, f})).Base B
heB : e ∈ B
hK : (M ／ (C \ {e, f})).Cocircuit (fundCocct e B)
⊢ f ∈ fundCocct e B