Theorem: Matroid.fundCocct_inter_eq (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 α
M : Matroid α
B : Set α
he : e ∈ B
⊢ fundCocct e B ∩ B = {e}
Tactic:
refine subset_antisymm ?_ (singleton_subset_iff.2 ⟨M.mem_fundCocct _ _, he⟩)
State after:
α : Type u_1
M✝ : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
B✝ : Set α
M : Matroid α
B : Set α
he : e ∈ B
⊢ fundCocct e B ∩ B ⊆ {e}

State before:
α : Type u_1
M✝ : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
B✝ : Set α
M : Matroid α
B : Set α
he : e ∈ B
⊢ fundCocct e B ∩ B ⊆ {e}
Tactic:
refine (inter_subset_inter_left _ (M.fundCocct_subset_insert_compl _ _)).trans ?_
State after:
α : Type u_1
M✝ : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
B✝ : Set α
M : Matroid α
B : Set α
he : e ∈ B
⊢ insert e (M.E \ B) ∩ B ⊆ {e}

State before:
α : Type u_1
M✝ : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
B✝ : Set α
M : Matroid α
B : Set α
he : e ∈ B
⊢ insert e (M.E \ B) ∩ B ⊆ {e}
Tactic:
simp (config := {contextual := true})
State after:
no goals