Theorem: Matroid.fundCocct_cocircuit (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 α
he : e ∈ B
hB : M.Base B
⊢ M.Cocircuit (fundCocct e B)
Tactic:
apply hB.compl_base_dual.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 α
he : e ∈ B
hB : M.Base B
⊢ e ∈ M✶.cl (M.E \ B) \ (M.E \ B)

State before:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
B : Set α
he : e ∈ B
hB : M.Base B
⊢ e ∈ M✶.cl (M.E \ B) \ (M.E \ B)
Tactic:
simp only [mem_diff, he, not_true_eq_false, and_false, not_false_eq_true, and_true]
State after:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
B : Set α
he : e ∈ B
hB : M.Base B
⊢ e ∈ M✶.cl (M.E \ B)

State before:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
B : Set α
he : e ∈ B
hB : M.Base B
⊢ e ∈ M✶.cl (M.E \ B)
Tactic:
rw [hB.compl_base_dual.cl_eq, dual_ground]
State after:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
B : Set α
he : e ∈ B
hB : M.Base B
⊢ e ∈ M.E

State before:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
B : Set α
he : e ∈ B
hB : M.Base B
⊢ e ∈ M.E
Tactic:
exact hB.subset_ground he
State after:
no goals