rw [simple_iff_loopless_eq_of_parallel_forall, loopless_iff_forall_circuit, and_iff_left]
case refine_2
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
h : ∀ (C : Set α), M.Circuit C → 3 ≤ C.encard
⊢ M.Simple
case refine_2
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
h : ∀ (C : Set α), M.Circuit C → 3 ≤ C.encard
⊢ ∀ (C : Set α), M.Circuit C → 1 < C.encard

case refine_2
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
h : ∀ (C : Set α), M.Circuit C → 3 ≤ C.encard
⊢ ∀ (e f : α), M.Parallel e f → e = f