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

State before:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
hI : M.Indep I
he : e ∈ I
⊢ M.fundCct e I = {e}
Tactic:
rw [fundCct, ← union_singleton, union_eq_right]
State after:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
hI : M.Indep I
he : e ∈ I
⊢ I ∩ ⋂₀ {J | J ⊆ I ∧ e ∈ M.cl J} ⊆ {e}

State before:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
hI : M.Indep I
he : e ∈ I
⊢ I ∩ ⋂₀ {J | J ⊆ I ∧ e ∈ M.cl J} ⊆ {e}
Tactic:
refine inter_subset_right.trans (sInter_subset_of_mem ?_)
State after:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
hI : M.Indep I
he : e ∈ I
⊢ {e} ∈ {J | J ⊆ I ∧ e ∈ M.cl J}

State before:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
hI : M.Indep I
he : e ∈ I
⊢ {e} ∈ {J | J ⊆ I ∧ e ∈ M.cl J}
Tactic:
simp only [mem_setOf, singleton_subset_iff, and_iff_right he]
State after:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
hI : M.Indep I
he : e ∈ I
⊢ e ∈ M.cl {e}

State before:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
hI : M.Indep I
he : e ∈ I
⊢ e ∈ M.cl {e}
Tactic:
exact M.mem_cl_self _ (hI.subset_ground he)
State after:
no goals