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

State before:
α : Type u_1
M : Matroid α
C K : Set α
e f g : α
h : M.ConnectedTo e f
hef : e ≠ f
⊢ M.Nonloop e
Tactic:
obtain ⟨C, hC, heC, hfC⟩ := h.exists_circuit_of_ne hef
State after:
case intro.intro.intro
α : Type u_1
M : Matroid α
C✝ K : Set α
e f g : α
h : M.ConnectedTo e f
hef : e ≠ f
C : Set α
hC : M.Circuit C
heC : e ∈ C
hfC : f ∈ C
⊢ M.Nonloop e

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