simp_rw [indep_iff_forall_subset_not_circuit hI, h',
  indep_iff_forall_subset_not_circuit (hI.trans_eq hE)]
α : 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
no goals