simp [f.apply_eq_apply hey]
case refine_1.intro.intro.intro.intro
α : Type u_1
M : Matroid α
e✝ f✝ g : α
I X P D : Set α
x y✝ e : α
he : M.Nonloop e
f : M.parallelClasses.RepFun
y : α
hey : M.Parallel e (f y)
⊢ f y = f e
no goals