Theorem: Matroid.Dep.exists_circuit_subset (Matroid/Circuit.lean)

State before:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
hX : M.Dep X
⊢ ∃ C ⊆ X, M.Circuit C
Tactic:
rw [dep_iff, indep_iff_not_mem_cl_diff_forall] at hX
State after:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
hX : (¬∀ e ∈ X, e ∉ M.cl (X \ {e})) ∧ X ⊆ M.E
⊢ ∃ C ⊆ X, M.Circuit C

State before:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
hX : (¬∀ e ∈ X, e ∉ M.cl (X \ {e})) ∧ X ⊆ M.E
⊢ ∃ C ⊆ X, M.Circuit C
Tactic:
push_neg at hX
State after:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
hX : (∃ e ∈ X, e ∈ M.cl (X \ {e})) ∧ X ⊆ M.E
⊢ ∃ C ⊆ X, M.Circuit C

State before:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
hX : (∃ e ∈ X, e ∈ M.cl (X \ {e})) ∧ X ⊆ M.E
⊢ ∃ C ⊆ X, M.Circuit C
Tactic:
obtain ⟨⟨e, he, heX⟩, hXE⟩ := hX
State after:
case intro.intro.intro
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e✝ f x y : α
hXE : X ⊆ M.E
e : α
he : e ∈ X
heX : e ∈ M.cl (X \ {e})
⊢ ∃ C ⊆ X, M.Circuit C

State before:
case intro.intro.intro
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e✝ f x y : α
hXE : X ⊆ M.E
e : α
he : e ∈ X
heX : e ∈ M.cl (X \ {e})
⊢ ∃ C ⊆ X, M.Circuit C
Tactic:
obtain ⟨I, hI⟩ := M.exists_basis (X \ {e}) (diff_subset.trans hXE)
State after:
case intro.intro.intro.intro
α : Type u_1
M : Matroid α
C C' I✝ X K C₁ C₂ R : Set α
e✝ f x y : α
hXE : X ⊆ M.E
e : α
he : e ∈ X
heX : e ∈ M.cl (X \ {e})
I : Set α
hI : M.Basis I (X \ {e})
⊢ ∃ C ⊆ X, M.Circuit C

State before:
case intro.intro.intro.intro
α : Type u_1
M : Matroid α
C C' I✝ X K C₁ C₂ R : Set α
e✝ f x y : α
hXE : X ⊆ M.E
e : α
he : e ∈ X
heX : e ∈ M.cl (X \ {e})
I : Set α
hI : M.Basis I (X \ {e})
⊢ ∃ C ⊆ X, M.Circuit C
Tactic:
rw [← hI.cl_eq_cl] at heX
State after:
case intro.intro.intro.intro
α : Type u_1
M : Matroid α
C C' I✝ X K C₁ C₂ R : Set α
e✝ f x y : α
hXE : X ⊆ M.E
e : α
he : e ∈ X
I : Set α
heX : e ∈ M.cl I
hI : M.Basis I (X \ {e})
⊢ ∃ C ⊆ X, M.Circuit C

State before:
case intro.intro.intro.intro
α : Type u_1
M : Matroid α
C C' I✝ X K C₁ C₂ R : Set α
e✝ f x y : α
hXE : X ⊆ M.E
e : α
he : e ∈ X
I : Set α
heX : e ∈ M.cl I
hI : M.Basis I (X \ {e})
⊢ ∃ C ⊆ X, M.Circuit C
Tactic:
exact ⟨_, (fundCct_subset_insert e I).trans
  (insert_subset he (hI.subset.trans diff_subset)),
  hI.indep.fundCct_circuit ⟨heX, not_mem_subset hI.subset (not_mem_diff_of_mem rfl)⟩⟩
State after:
no goals