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

State before:
α : Type u_1
M : Matroid α
C K : Set α
e f g : α
h : M.ConnectedTo e f
⊢ M.ConnectedTo f e
Tactic:
obtain (⟨rfl, hef⟩ | ⟨C, hC, heC, hfC⟩) := h
State after:
case inl.intro
α : Type u_1
M : Matroid α
C K : Set α
e g : α
hef : e ∈ M.E
⊢ M.ConnectedTo e e

case inr.intro.intro.intro
α : Type u_1
M : Matroid α
C✝ K : Set α
e f g : α
C : Set α
hC : M.Circuit C
heC : e ∈ C
hfC : f ∈ C
⊢ M.ConnectedTo f e

State before:
case inr.intro.intro.intro
α : Type u_1
M : Matroid α
C✝ K : Set α
e f g : α
C : Set α
hC : M.Circuit C
heC : e ∈ C
hfC : f ∈ C
⊢ M.ConnectedTo f e
Tactic:
exact .inr ⟨C, hC, hfC, heC⟩
State after:
no goals

State before:
case inl.intro
α : Type u_1
M : Matroid α
C K : Set α
e g : α
hef : e ∈ M.E
⊢ M.ConnectedTo e e
Tactic:
exact connectedTo_self hef
State after:
no goals