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

State before:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
hX : autoParam (X ⊆ M.E) _auto✝
⊢ e ∈ M.cl X ↔ e ∈ X ∨ ∃ C, M.Circuit C ∧ e ∈ C ∧ C ⊆ insert e X
Tactic:
refine' (em (e ∈ X)).elim (fun he ↦ iff_of_true (M.mem_cl_of_mem he) (Or.inl he)) (fun he ↦ _)
State after:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
hX : autoParam (X ⊆ M.E) _auto✝
he : e ∉ X
⊢ e ∈ M.cl X ↔ e ∈ X ∨ ∃ C, M.Circuit C ∧ e ∈ C ∧ C ⊆ insert e X

State before:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
hX : autoParam (X ⊆ M.E) _auto✝
he : e ∉ X
⊢ e ∈ M.cl X ↔ e ∈ X ∨ ∃ C, M.Circuit C ∧ e ∈ C ∧ C ⊆ insert e X
Tactic:
rw [or_iff_right he]
State after:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
hX : autoParam (X ⊆ M.E) _auto✝
he : e ∉ X
⊢ e ∈ M.cl X ↔ ∃ C, M.Circuit C ∧ e ∈ C ∧ C ⊆ insert e X

State before:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
hX : autoParam (X ⊆ M.E) _auto✝
he : e ∉ X
⊢ e ∈ M.cl X ↔ ∃ C, M.Circuit C ∧ e ∈ C ∧ C ⊆ insert e X
Tactic:
refine' ⟨fun h ↦ _, fun ⟨C, hC, heC, hCX⟩ ↦ _⟩
State after:
case refine'_1
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
hX : autoParam (X ⊆ M.E) _auto✝
he : e ∉ X
h : e ∈ M.cl X
⊢ ∃ C, M.Circuit C ∧ e ∈ C ∧ C ⊆ insert e X

case refine'_2
α : Type u_1
M : Matroid α
C✝ C' I X K C₁ C₂ R : Set α
e f x y : α
hX : autoParam (X ⊆ M.E) _auto✝
he : e ∉ X
x✝ : ∃ C, M.Circuit C ∧ e ∈ C ∧ C ⊆ insert e X
C : Set α
hC : M.Circuit C
heC : e ∈ C
hCX : C ⊆ insert e X
⊢ e ∈ M.cl X

State before:
case refine'_2
α : Type u_1
M : Matroid α
C✝ C' I X K C₁ C₂ R : Set α
e f x y : α
hX : autoParam (X ⊆ M.E) _auto✝
he : e ∉ X
x✝ : ∃ C, M.Circuit C ∧ e ∈ C ∧ C ⊆ insert e X
C : Set α
hC : M.Circuit C
heC : e ∈ C
hCX : C ⊆ insert e X
⊢ e ∈ M.cl X
Tactic:
refine' ((hC.subset_cl_diff_singleton e).trans (M.cl_subset_cl _)) heC
State after:
case refine'_2
α : Type u_1
M : Matroid α
C✝ C' I X K C₁ C₂ R : Set α
e f x y : α
hX : autoParam (X ⊆ M.E) _auto✝
he : e ∉ X
x✝ : ∃ C, M.Circuit C ∧ e ∈ C ∧ C ⊆ insert e X
C : Set α
hC : M.Circuit C
heC : e ∈ C
hCX : C ⊆ insert e X
⊢ C \ {e} ⊆ X

State before:
case refine'_2
α : Type u_1
M : Matroid α
C✝ C' I X K C₁ C₂ R : Set α
e f x y : α
hX : autoParam (X ⊆ M.E) _auto✝
he : e ∉ X
x✝ : ∃ C, M.Circuit C ∧ e ∈ C ∧ C ⊆ insert e X
C : Set α
hC : M.Circuit C
heC : e ∈ C
hCX : C ⊆ insert e X
⊢ C \ {e} ⊆ X
Tactic:
rwa [diff_subset_iff, singleton_union]
State after:
no goals

State before:
case refine'_1
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
hX : autoParam (X ⊆ M.E) _auto✝
he : e ∉ X
h : e ∈ M.cl X
⊢ ∃ C, M.Circuit C ∧ e ∈ C ∧ C ⊆ insert e X
Tactic:
obtain ⟨I, hI⟩ := M.exists_basis X
State after:
case refine'_1.intro
α : Type u_1
M : Matroid α
C C' I✝ X K C₁ C₂ R : Set α
e f x y : α
hX : autoParam (X ⊆ M.E) _auto✝
he : e ∉ X
h : e ∈ M.cl X
I : Set α
hI : M.Basis I X
⊢ ∃ C, M.Circuit C ∧ e ∈ C ∧ C ⊆ insert e X

State before:
case refine'_1.intro
α : Type u_1
M : Matroid α
C C' I✝ X K C₁ C₂ R : Set α
e f x y : α
hX : autoParam (X ⊆ M.E) _auto✝
he : e ∉ X
h : e ∈ M.cl X
I : Set α
hI : M.Basis I X
⊢ ∃ C, M.Circuit C ∧ e ∈ C ∧ C ⊆ insert e X
Tactic:
rw [← hI.cl_eq_cl] at h
State after:
case refine'_1.intro
α : Type u_1
M : Matroid α
C C' I✝ X K C₁ C₂ R : Set α
e f x y : α
hX : autoParam (X ⊆ M.E) _auto✝
he : e ∉ X
I : Set α
h : e ∈ M.cl I
hI : M.Basis I X
⊢ ∃ C, M.Circuit C ∧ e ∈ C ∧ C ⊆ insert e X

State before:
case refine'_1.intro
α : Type u_1
M : Matroid α
C C' I✝ X K C₁ C₂ R : Set α
e f x y : α
hX : autoParam (X ⊆ M.E) _auto✝
he : e ∉ X
I : Set α
h : e ∈ M.cl I
hI : M.Basis I X
⊢ ∃ C, M.Circuit C ∧ e ∈ C ∧ C ⊆ insert e X
Tactic:
exact ⟨M.fundCct e I, hI.indep.fundCct_circuit ⟨h, not_mem_subset hI.subset he⟩,
  M.mem_fundCct e I, (fundCct_subset_insert _ _).trans (insert_subset_insert hI.subset)⟩
State after:
no goals