Theorem: Matroid.Simple.eq_of_parallel_of_mem (Matroid/Simple.lean)

State before:
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
h : (M ↾ X).Simple
he : e ∈ X
hf : f ∈ X
hef : M.Parallel e f
⊢ ↑⟨e, he⟩ ∈ (M ↾ X).E
Tactic:
simpa
State after:
no goals

State before:
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
h : (M ↾ X).Simple
he : e ∈ X
hf : f ∈ X
hef : M.Parallel e f
⊢ (M ↾ X).Parallel ↑⟨e, he⟩ ↑⟨f, hf⟩
Tactic:
simp [restrict_parallel_iff, hef, he, hf]
State after:
no goals