refine ⟨fun h ↦ ⟨h.simple.loopless, h.restriction, fun e he ↦ ?_⟩, fun ⟨h, hr, h'⟩ ↦ ?_⟩
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
x y : α
⊢ N.IsSimplification M ↔ N.Loopless ∧ N ≤r M ∧ ∀ ⦃e : α⦄, M.Nonloop e → ∃! f, f ∈ N.E ∧ M.Parallel e f
case refine_1
α : Type u_1
M N : Matroid α
e✝ f g : α
I X P D : Set α
x y : α
h : N.IsSimplification M
e : α
he : M.Nonloop e
⊢ ∃! f, f ∈ N.E ∧ M.Parallel e f

case 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
h' : ∀ ⦃e : α⦄, M.Nonloop e → ∃! f, f ∈ N.E ∧ M.Parallel e f
⊢ N.IsSimplification M