Theorem: Matroid.Connected.exists_circuit (Matroid/Connectivity.lean)

State before:
α : Type u_1
M : Matroid α
C K : Set α
e f g : α
h : M.Connected
hM : M.E.Nontrivial
he : e ∈ M.E
hf : f ∈ M.E
⊢ ∃ C, M.Circuit C ∧ e ∈ C ∧ f ∈ C
Tactic:
obtain (rfl | hne) := eq_or_ne e f
State after:
case inl
α : Type u_1
M : Matroid α
C K : Set α
e g : α
h : M.Connected
hM : M.E.Nontrivial
he hf : e ∈ M.E
⊢ ∃ C, M.Circuit C ∧ e ∈ C ∧ e ∈ C

case inr
α : Type u_1
M : Matroid α
C K : Set α
e f g : α
h : M.Connected
hM : M.E.Nontrivial
he : e ∈ M.E
hf : f ∈ M.E
hne : e ≠ f
⊢ ∃ C, M.Circuit C ∧ e ∈ C ∧ f ∈ C

State before:
case inr
α : Type u_1
M : Matroid α
C K : Set α
e f g : α
h : M.Connected
hM : M.E.Nontrivial
he : e ∈ M.E
hf : f ∈ M.E
hne : e ≠ f
⊢ ∃ C, M.Circuit C ∧ e ∈ C ∧ f ∈ C
Tactic:
exact (h.2 he hf).exists_circuit_of_ne hne
State after:
no goals

State before:
case inl
α : Type u_1
M : Matroid α
C K : Set α
e g : α
h : M.Connected
hM : M.E.Nontrivial
he hf : e ∈ M.E
⊢ ∃ C, M.Circuit C ∧ e ∈ C ∧ e ∈ C
Tactic:
obtain (he' | he') := em (M.Coloop e)
State after:
case inl.inl
α : Type u_1
M : Matroid α
C K : Set α
e g : α
h : M.Connected
hM : M.E.Nontrivial
he hf : e ∈ M.E
he' : M.Coloop e
⊢ ∃ C, M.Circuit C ∧ e ∈ C ∧ e ∈ C

case inl.inr
α : Type u_1
M : Matroid α
C K : Set α
e g : α
h : M.Connected
hM : M.E.Nontrivial
he hf : e ∈ M.E
he' : ¬M.Coloop e
⊢ ∃ C, M.Circuit C ∧ e ∈ C ∧ e ∈ C

State before:
case inl.inr
α : Type u_1
M : Matroid α
C K : Set α
e g : α
h : M.Connected
hM : M.E.Nontrivial
he hf : e ∈ M.E
he' : ¬M.Coloop e
⊢ ∃ C, M.Circuit C ∧ e ∈ C ∧ e ∈ C
Tactic:
obtain ⟨C, hC, heC⟩ := exists_mem_circuit_of_not_coloop he he'
State after:
case inl.inr.intro.intro
α : Type u_1
M : Matroid α
C✝ K : Set α
e g : α
h : M.Connected
hM : M.E.Nontrivial
he hf : e ∈ M.E
he' : ¬M.Coloop e
C : Set α
hC : M.Circuit C
heC : e ∈ C
⊢ ∃ C, M.Circuit C ∧ e ∈ C ∧ e ∈ C

State before:
case inl.inr.intro.intro
α : Type u_1
M : Matroid α
C✝ K : Set α
e g : α
h : M.Connected
hM : M.E.Nontrivial
he hf : e ∈ M.E
he' : ¬M.Coloop e
C : Set α
hC : M.Circuit C
heC : e ∈ C
⊢ ∃ C, M.Circuit C ∧ e ∈ C ∧ e ∈ C
Tactic:
exact ⟨C, hC, heC, heC⟩
State after:
no goals

State before:
case inl.inl
α : Type u_1
M : Matroid α
C K : Set α
e g : α
h : M.Connected
hM : M.E.Nontrivial
he hf : e ∈ M.E
he' : M.Coloop e
⊢ ∃ C, M.Circuit C ∧ e ∈ C ∧ e ∈ C
Tactic:
exact False.elim <| he'.not_connected hM h
State after:
no goals