refine eq_of_indep_iff_indep_forall (by simp [h.sdiff_eq_right]) (fun I _ ↦ ?_)
α : Type u_1
M✝ M' N : Matroid α
e f : α
I J R✝ B X Y Z K : Set α
M₀ M₁ M₂ M : Matroid α
C R : Set α
h : Disjoint C R
⊢ M ／ C ↾ R = (M ↾ (R ∪ C)) ／ C
α : Type u_1
M✝ M' N : Matroid α
e f : α
I✝ J R✝ B X Y Z K : Set α
M₀ M₁ M₂ M : Matroid α
C R : Set α
h : Disjoint C R
I : Set α
x✝ : I ⊆ (M ／ C ↾ R).E
⊢ (M ／ C ↾ R).Indep I ↔ ((M ↾ (R ∪ C)) ／ C).Indep I