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

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

State before:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
he : e ∈ M.cl I
⊢ ⋂₀ {J | J ⊆ I ∧ e ∈ M.cl J} ⊆ I
Tactic:
exact sInter_subset_of_mem ⟨Subset.rfl, he⟩
State after:
no goals