exact ⟨fun e he hl ↦ hl.dep.not_indep <| by simpa using h he he,
  fun e f hef ↦ hef.eq_of_indep (h hef.mem_ground_left hef.mem_ground_right) ⟩
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
h : ∀ ⦃e f : α⦄, e ∈ M.E → f ∈ M.E → M.Indep {e, f}
⊢ (∀ e ∈ M.E, ¬M.Loop e) ∧ ∀ (e f : α), M.Parallel e f → e = f
no goals