rw [simple_iff_loopless_eq_of_parallel_forall] at h hC ⊢
α : Type u_1
M N : Matroid α
e f g : α
I X P D C : Set α
hC : (M ↾ C).Simple
h : (M ／ C).Simple
⊢ M.Simple
α : Type u_1
M N : Matroid α
e f g : α
I X P D C : Set α
hC : (M ↾ C).Loopless ∧ ∀ (e f : α), (M ↾ C).Parallel e f → e = f
h : (M ／ C).Loopless ∧ ∀ (e f : α), (M ／ C).Parallel e f → e = f
⊢ M.Loopless ∧ ∀ (e f : α), M.Parallel e f → e = f