exact ⟨fun h C _ ↦ h C, fun h C hC ↦ h C hC.subset_ground hC⟩
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
B : Set α
⊢ (∀ (x : Set α), ¬M.Circuit x) ↔ ∀ C ⊆ M.E, ¬M.Circuit C
no goals