Theorem: Matroid.Base.fundCct_circuit (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 α
hB : M.Base B
hx : x ∈ M.E \ B
⊢ M.Circuit (M.fundCct x B)
Tactic:
apply hB.indep.fundCct_circuit
State after:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
B : Set α
hB : M.Base B
hx : x ∈ M.E \ B
⊢ x ∈ M.cl B \ B

State before:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
B : Set α
hB : M.Base B
hx : x ∈ M.E \ B
⊢ x ∈ M.cl B \ B
Tactic:
rwa [hB.cl_eq]
State after:
no goals