Theorem: Matroid.indep_iff_forall_subset_not_circuit' (Matroid/Circuit.lean)

State before:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
⊢ M.Indep I ↔ (∀ C ⊆ I, ¬M.Circuit C) ∧ I ⊆ M.E
Tactic:
simp_rw [indep_iff_not_dep, dep_iff_superset_circuit', not_and, imp_not_comm (b := _ ⊆ _)]
State after:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
⊢ (I ⊆ M.E → ¬∃ C ⊆ I, M.Circuit C) ∧ I ⊆ M.E ↔ (∀ C ⊆ I, ¬M.Circuit C) ∧ I ⊆ M.E

State before:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
⊢ (I ⊆ M.E → ¬∃ C ⊆ I, M.Circuit C) ∧ I ⊆ M.E ↔ (∀ C ⊆ I, ¬M.Circuit C) ∧ I ⊆ M.E
Tactic:
aesop
State after:
no goals