intro a (ha : M.Nonloop a)
case refine_2.refine_2
α : 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 ∈ {e | M.Nonloop e}, M.parallelClasses.Rel a ((fun x => if hx : M.Nonloop x then f hx else x) a)
case refine_2.refine_2
α : 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 : α
ha : M.Nonloop a
⊢ M.parallelClasses.Rel a ((fun x => if hx : M.Nonloop x then f hx else x) a)