Theorem: Matroid.delete_circuit_iff (Matroid/Minor/Basic.lean)

State before:
α : Type u_1
M M' N : Matroid α
e f : α
I J R✝ B X Y Z K D D₁ D₂ R C : Set α
⊢ (M ＼ D).Circuit C ↔ M.Circuit C ∧ Disjoint C D
Tactic:
simp_rw [circuit_iff, delete_dep_iff, and_imp]
State after:
α : Type u_1
M M' N : Matroid α
e f : α
I J R✝ B X Y Z K D D₁ D₂ R C : Set α
⊢ ((M.Dep C ∧ Disjoint C D) ∧ ∀ ⦃I : Set α⦄, M.Dep I → Disjoint I D → I ⊆ C → I = C) ↔
    (M.Dep C ∧ ∀ ⦃I : Set α⦄, M.Dep I → I ⊆ C → I = C) ∧ Disjoint C D

State before:
α : Type u_1
M M' N : Matroid α
e f : α
I J R✝ B X Y Z K D D₁ D₂ R C : Set α
⊢ ((M.Dep C ∧ Disjoint C D) ∧ ∀ ⦃I : Set α⦄, M.Dep I → Disjoint I D → I ⊆ C → I = C) ↔
    (M.Dep C ∧ ∀ ⦃I : Set α⦄, M.Dep I → I ⊆ C → I = C) ∧ Disjoint C D
Tactic:
rw [and_comm, ← and_assoc, and_congr_left_iff, and_comm, and_congr_right_iff]
State after:
α : Type u_1
M M' N : Matroid α
e f : α
I J R✝ B X Y Z K D D₁ D₂ R C : Set α
⊢ Disjoint C D →
    M.Dep C → ((∀ ⦃I : Set α⦄, M.Dep I → Disjoint I D → I ⊆ C → I = C) ↔ ∀ ⦃I : Set α⦄, M.Dep I → I ⊆ C → I = C)

State before:
α : Type u_1
M M' N : Matroid α
e f : α
I J R✝ B X Y Z K D D₁ D₂ R C : Set α
⊢ Disjoint C D →
    M.Dep C → ((∀ ⦃I : Set α⦄, M.Dep I → Disjoint I D → I ⊆ C → I = C) ↔ ∀ ⦃I : Set α⦄, M.Dep I → I ⊆ C → I = C)
Tactic:
exact fun hdj _↦ ⟨fun h I hId hIC ↦ h hId (disjoint_of_subset_left hIC hdj) hIC,
  fun h I hI _ hIC ↦ h hI hIC⟩
State after:
no goals