Theorem: GraphTheory.ES1.q4 (LeanCamCombi/ExampleSheets/Graph/ES1.lean)

State before:
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝¹ : Finite α
inst✝ : Nontrivial α
G : SimpleGraph α
hG : G.Connected
⊢ ∃ a, (⊤.deleteVerts {a}).coe.Connected
Tactic:
cases nonempty_fintype α
State after:
case intro
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝¹ : Finite α
inst✝ : Nontrivial α
G : SimpleGraph α
hG : G.Connected
val✝ : Fintype α
⊢ ∃ a, (⊤.deleteVerts {a}).coe.Connected

State before:
case intro
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝¹ : Finite α
inst✝ : Nontrivial α
G : SimpleGraph α
hG : G.Connected
val✝ : Fintype α
⊢ ∃ a, (⊤.deleteVerts {a}).coe.Connected
Tactic:
sorry
State after:
no goals