exact Eq.symm <| (hf hab.nonloop_left).2 (f hab.nonloop_right)
  ⟨(hf hab.nonloop_right).1.1, hab.trans (hf hab.nonloop_right).1.2⟩
case refine_2.refine_3
α : Type u_1
M N : Matroid α
e f✝ g : α
I X P D : Set α
x y : α
x✝ : N.Loopless ∧ N ≤r M ∧ ∀ ⦃e : α⦄, M.Nonloop e → ∃! f, f ∈ N.E ∧ M.Parallel e f
h : N.Loopless
hr : N ≤r M
f : ⦃e : α⦄ → M.Nonloop e → α
hf :
  ∀ ⦃e : α⦄ (a : M.Nonloop e),
    (fun f => f ∈ N.E ∧ M.Parallel e f) (f a) ∧ ∀ (y : α), (fun f => f ∈ N.E ∧ M.Parallel e f) y → y = f a
a b : α
hab : M.Parallel a b
⊢ f ⋯ = f ⋯
no goals