simp only [Partition.RepFun.mk_apply, mem_image, mem_setOf_eq]
case h.e'_3.h.e'_3.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
x : α
h : x ∈ N.E
hx : M.Nonloop x
⊢ x ∈
    ⇑{ toFun := fun x => if hx : M.Nonloop x then f hx else x, apply_eq_self_of_not_mem := ⋯, rel_apply_of_mem := ⋯,
          apply_eq_of_rel := ⋯ } ''
      {e | M.Nonloop e}
case h.e'_3.h.e'_3.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
x : α
h : x ∈ N.E
hx : M.Nonloop x
⊢ ∃ x_1, M.Nonloop x_1 ∧ (if hx : M.Nonloop x_1 then f hx else x_1) = x