Theorem: Matroid.circuit_iff_dep_forall_diff_singleton_indep (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 ∧ ∀ e ∈ C, M.Indep (C \ {e})
Tactic:
rw [circuit_iff_forall_ssubset, and_congr_right_iff]
State after:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
⊢ M.Dep C → ((∀ ⦃I : Set α⦄, I ⊂ C → M.Indep I) ↔ ∀ e ∈ C, M.Indep (C \ {e}))

State before:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
⊢ M.Dep C → ((∀ ⦃I : Set α⦄, I ⊂ C → M.Indep I) ↔ ∀ e ∈ C, M.Indep (C \ {e}))
Tactic:
refine' fun _ ↦ ⟨fun h e heC ↦ h (Iff.mpr diff_singleton_sSubset heC),
  fun h I hIC ↦ _⟩
State after:
α : Type u_1
M : Matroid α
C C' I✝ X K C₁ C₂ R : Set α
e f x y : α
x✝ : M.Dep C
h : ∀ e ∈ C, M.Indep (C \ {e})
I : Set α
hIC : 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 : α
x✝ : M.Dep C
h : ∀ e ∈ C, M.Indep (C \ {e})
I : Set α
hIC : I ⊂ C
⊢ M.Indep I
Tactic:
obtain ⟨e, he⟩ := exists_of_ssubset hIC
State after:
case intro
α : Type u_1
M : Matroid α
C C' I✝ X K C₁ C₂ R : Set α
e✝ f x y : α
x✝ : M.Dep C
h : ∀ e ∈ C, M.Indep (C \ {e})
I : Set α
hIC : I ⊂ C
e : α
he : e ∈ C ∧ e ∉ I
⊢ M.Indep I

State before:
case intro
α : Type u_1
M : Matroid α
C C' I✝ X K C₁ C₂ R : Set α
e✝ f x y : α
x✝ : M.Dep C
h : ∀ e ∈ C, M.Indep (C \ {e})
I : Set α
hIC : I ⊂ C
e : α
he : e ∈ C ∧ e ∉ I
⊢ M.Indep I
Tactic:
exact (h e he.1).subset (subset_diff_singleton hIC.subset he.2)
State after:
no goals