Theorem: Matroid.Cocircuit.nonloop_of_mem (Matroid/Loop.lean)

State before:
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I X Y Z F C K : Set α
hK : M.Cocircuit K
he : e ∈ K
⊢ M.Nonloop e
Tactic:
rw [← not_loop_iff (hK.subset_ground he), ← singleton_circuit]
State after:
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I X Y Z F C K : Set α
hK : M.Cocircuit K
he : e ∈ K
⊢ ¬M.Circuit {e}

State before:
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I X Y Z F C K : Set α
hK : M.Cocircuit K
he : e ∈ K
⊢ ¬M.Circuit {e}
Tactic:
intro he'
State after:
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I X Y Z F C K : Set α
hK : M.Cocircuit K
he : e ∈ K
he' : M.Circuit {e}
⊢ False

State before:
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I X Y Z F C K : Set α
hK : M.Cocircuit K
he : e ∈ K
he' : M.Circuit {e}
⊢ False
Tactic:
obtain ⟨f, ⟨rfl, -⟩, hfe⟩ := (he'.cocircuit_inter_nontrivial hK ⟨e, by simp [he]⟩).exists_ne e
State after:
case intro.intro.intro
α : Type u_1
β : Type u_2
M N : Matroid α
f✝ : α
B L L' I X Y Z F C K : Set α
hK : M.Cocircuit K
f : α
he : f ∈ K
he' : M.Circuit {f}
hfe : f ≠ f
⊢ False

State before:
case intro.intro.intro
α : Type u_1
β : Type u_2
M N : Matroid α
f✝ : α
B L L' I X Y Z F C K : Set α
hK : M.Cocircuit K
f : α
he : f ∈ K
he' : M.Circuit {f}
hfe : f ≠ f
⊢ False
Tactic:
exact hfe rfl
State after:
no goals

State before:
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I X Y Z F C K : Set α
hK : M.Cocircuit K
he : e ∈ K
he' : M.Circuit {e}
⊢ e ∈ {e} ∩ K
Tactic:
simp [he]
State after:
no goals