exact fun _ hC ↦ ⟨fun h I hIC hne ↦ by_contra fun hi ↦ hne (h hi (hIC.trans hC) hIC),
  fun h I hi _ hIC ↦ by_contra fun hne ↦ hi (h hIC hne)⟩
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
⊢ ¬M.Indep C →
    C ⊆ M.E → ((∀ ⦃I : Set α⦄, ¬M.Indep I → I ⊆ M.E → I ⊆ C → I = C) ↔ ∀ ⦃I : Set α⦄, I ⊆ C → I ≠ C → M.Indep I)
no goals