refine' eq_of_indep_iff_indep_forall hE fun I hI ↦ _
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
M₁ M₂ : Matroid α
hE : M₁.E = M₂.E
h : ∀ C ⊆ M₁.E, M₁.Circuit C ↔ M₂.Circuit C
h' : ∀ (C : Set α), M₁.Circuit C ↔ M₂.Circuit C
⊢ M₁ = M₂
α : Type u_1
M : Matroid α
C C' I✝ X K C₁ C₂ R : Set α
e f x y : α
M₁ M₂ : Matroid α
hE : M₁.E = M₂.E
h : ∀ C ⊆ M₁.E, M₁.Circuit C ↔ M₂.Circuit C
h' : ∀ (C : Set α), M₁.Circuit C ↔ M₂.Circuit C
I : Set α
hI : I ⊆ M₁.E
⊢ M₁.Indep I ↔ M₂.Indep I