Theorem: Matroid.Parallel.mem_cocircuit_of_mem (Matroid/Parallel.lean)

State before:
α : Type u_1
M N : Matroid α
e f g : α
I X P D K : Set α
hef : M.Parallel e f
hK : M.Cocircuit K
he : e ∈ K
⊢ f ∈ K
Tactic:
by_contra hf
State after:
α : Type u_1
M N : Matroid α
e f g : α
I X P D K : Set α
hef : M.Parallel e f
hK : M.Cocircuit K
he : e ∈ K
hf : f ∉ K
⊢ False

State before:
α : Type u_1
M N : Matroid α
e f g : α
I X P D K : Set α
hef : M.Parallel e f
hK : M.Cocircuit K
he : e ∈ K
hf : f ∉ K
⊢ False
Tactic:
have hK' := (hK.compl_hyperplane).flat.cl
State after:
α : Type u_1
M N : Matroid α
e f g : α
I X P D K : Set α
hef : M.Parallel e f
hK : M.Cocircuit K
he : e ∈ K
hf : f ∉ K
hK' : M.cl (M.E \ K) = M.E \ K
⊢ False

State before:
α : Type u_1
M N : Matroid α
e f g : α
I X P D K : Set α
hef : M.Parallel e f
hK : M.Cocircuit K
he : e ∈ K
hf : f ∉ K
hK' : M.cl (M.E \ K) = M.E \ K
⊢ False
Tactic:
have hfK := hK'.symm.subset ⟨hef.mem_ground_right, hf⟩
State after:
α : Type u_1
M N : Matroid α
e f g : α
I X P D K : Set α
hef : M.Parallel e f
hK : M.Cocircuit K
he : e ∈ K
hf : f ∉ K
hK' : M.cl (M.E \ K) = M.E \ K
hfK : f ∈ M.cl (M.E \ K)
⊢ False

State before:
α : Type u_1
M N : Matroid α
e f g : α
I X P D K : Set α
hef : M.Parallel e f
hK : M.Cocircuit K
he : e ∈ K
hf : f ∉ K
hK' : M.cl (M.E \ K) = M.E \ K
hfK : f ∈ M.cl (M.E \ K)
⊢ False
Tactic:
rw [← hef.mem_cl_iff_mem_cl, hK'] at hfK
State after:
α : Type u_1
M N : Matroid α
e f g : α
I X P D K : Set α
hef : M.Parallel e f
hK : M.Cocircuit K
he : e ∈ K
hf : f ∉ K
hK' : M.cl (M.E \ K) = M.E \ K
hfK : e ∈ M.E \ K
⊢ False

State before:
α : Type u_1
M N : Matroid α
e f g : α
I X P D K : Set α
hef : M.Parallel e f
hK : M.Cocircuit K
he : e ∈ K
hf : f ∉ K
hK' : M.cl (M.E \ K) = M.E \ K
hfK : e ∈ M.E \ K
⊢ False
Tactic:
exact hfK.2 he
State after:
no goals