Theorem: Matroid.Parallel.eq_of_indep (Matroid/Parallel.lean)

State before:
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
h : M.Parallel e f
hi : M.Indep {e, f}
⊢ e = f
Tactic:
by_contra hef
State after:
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
h : M.Parallel e f
hi : M.Indep {e, f}
hef : ¬e = f
⊢ False

State before:
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
h : M.Parallel e f
hi : M.Indep {e, f}
hef : ¬e = f
⊢ False
Tactic:
exact ((h.nonloop_left.parallel_iff_dep h.nonloop_right hef).1 h).not_indep hi
State after:
no goals