Theorem: Matroid.Coloop.not_connected (Matroid/Connectivity.lean)

State before:
α : Type u_1
M : Matroid α
C K : Set α
e f g : α
he : M.Coloop e
hE : M.E.Nontrivial
⊢ ¬M.Connected
Tactic:
obtain ⟨f, hfE, hfe⟩ := hE.exists_ne e
State after:
case intro.intro
α : Type u_1
M : Matroid α
C K : Set α
e f✝ g : α
he : M.Coloop e
hE : M.E.Nontrivial
f : α
hfE : f ∈ M.E
hfe : f ≠ e
⊢ ¬M.Connected

State before:
case intro.intro
α : Type u_1
M : Matroid α
C K : Set α
e f✝ g : α
he : M.Coloop e
hE : M.E.Nontrivial
f : α
hfE : f ∈ M.E
hfe : f ≠ e
⊢ ¬M.Connected
Tactic:
rintro ⟨-, hconn⟩
State after:
case intro.intro.intro
α : Type u_1
M : Matroid α
C K : Set α
e f✝ g : α
he : M.Coloop e
hE : M.E.Nontrivial
f : α
hfE : f ∈ M.E
hfe : f ≠ e
hconn : ∀ ⦃e f : α⦄, e ∈ M.E → f ∈ M.E → M.ConnectedTo e f
⊢ False

State before:
case intro.intro.intro
α : Type u_1
M : Matroid α
C K : Set α
e f✝ g : α
he : M.Coloop e
hE : M.E.Nontrivial
f : α
hfE : f ∈ M.E
hfe : f ≠ e
hconn : ∀ ⦃e f : α⦄, e ∈ M.E → f ∈ M.E → M.ConnectedTo e f
⊢ False
Tactic:
obtain ⟨K, hK, heK, -⟩ := (hconn he.mem_ground hfE).exists_circuit_of_ne hfe.symm
State after:
case intro.intro.intro.intro.intro.intro
α : Type u_1
M : Matroid α
C K✝ : Set α
e f✝ g : α
he : M.Coloop e
hE : M.E.Nontrivial
f : α
hfE : f ∈ M.E
hfe : f ≠ e
hconn : ∀ ⦃e f : α⦄, e ∈ M.E → f ∈ M.E → M.ConnectedTo e f
K : Set α
hK : M.Circuit K
heK : e ∈ K
⊢ False

State before:
case intro.intro.intro.intro.intro.intro
α : Type u_1
M : Matroid α
C K✝ : Set α
e f✝ g : α
he : M.Coloop e
hE : M.E.Nontrivial
f : α
hfE : f ∈ M.E
hfe : f ≠ e
hconn : ∀ ⦃e f : α⦄, e ∈ M.E → f ∈ M.E → M.ConnectedTo e f
K : Set α
hK : M.Circuit K
heK : e ∈ K
⊢ False
Tactic:
exact he.not_mem_circuit hK heK
State after:
no goals