Theorem: Matroid.circuit_iff_forall_ssubset (Matroid/Circuit.lean)

State before:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
⊢ M.Circuit C ↔ M.Dep C ∧ ∀ ⦃I : Set α⦄, I ⊂ C → M.Indep I
Tactic:
simp_rw [circuit_iff, dep_iff, and_congr_right_iff, ssubset_iff_subset_ne, and_imp]
State after:
α : 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)

State before:
α : 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)
Tactic:
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)⟩
State after:
no goals