simp_rw [circuit_iff, restrict_dep_iff, dep_iff, and_imp] at *
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
hC : M.Circuit C
hCR : C ⊆ R
⊢ (M ↾ R).Circuit C
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
hCR : C ⊆ R
hC : (¬M.Indep C ∧ C ⊆ M.E) ∧ ∀ ⦃I : Set α⦄, ¬M.Indep I → I ⊆ M.E → I ⊆ C → I = C
⊢ (¬M.Indep C ∧ C ⊆ R) ∧ ∀ ⦃I : Set α⦄, ¬M.Indep I → I ⊆ R → I ⊆ C → I = C