Theorem: Matroid.Indep.exists_cocircuit_inter_eq_mem (Matroid/Circuit.lean)

State before:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
B : Set α
hI : M.Indep I
heI : e ∈ I
⊢ ∃ K, M.Cocircuit K ∧ K ∩ I = {e}
Tactic:
obtain ⟨B, hB, hIB⟩ := hI.exists_base_superset
State after:
case intro.intro
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
B✝ : Set α
hI : M.Indep I
heI : e ∈ I
B : Set α
hB : M.Base B
hIB : I ⊆ B
⊢ ∃ K, M.Cocircuit K ∧ K ∩ I = {e}

State before:
case intro.intro
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
B✝ : Set α
hI : M.Indep I
heI : e ∈ I
B : Set α
hB : M.Base B
hIB : I ⊆ B
⊢ ∃ K, M.Cocircuit K ∧ K ∩ I = {e}
Tactic:
refine ⟨M.fundCocct e B, fundCocct_cocircuit (hIB heI) hB, ?_⟩
State after:
case intro.intro
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
B✝ : Set α
hI : M.Indep I
heI : e ∈ I
B : Set α
hB : M.Base B
hIB : I ⊆ B
⊢ fundCocct e B ∩ I = {e}

State before:
case intro.intro
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
B✝ : Set α
hI : M.Indep I
heI : e ∈ I
B : Set α
hB : M.Base B
hIB : I ⊆ B
⊢ fundCocct e B ∩ I = {e}
Tactic:
rw [subset_antisymm_iff, subset_inter_iff, singleton_subset_iff, and_iff_right
  (mem_fundCocct _ _ _), singleton_subset_iff, and_iff_left heI, ← M.fundCocct_inter_eq (hIB heI)]
State after:
case intro.intro
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
B✝ : Set α
hI : M.Indep I
heI : e ∈ I
B : Set α
hB : M.Base B
hIB : I ⊆ B
⊢ fundCocct e B ∩ I ⊆ fundCocct e B ∩ B

State before:
case intro.intro
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
B✝ : Set α
hI : M.Indep I
heI : e ∈ I
B : Set α
hB : M.Base B
hIB : I ⊆ B
⊢ fundCocct e B ∩ I ⊆ fundCocct e B ∩ B
Tactic:
exact inter_subset_inter_right _ hIB
State after:
no goals