-- Mathlib/Combinatorics/SimpleGraph/Hamiltonian.lean
lemma IsHamiltonian.connected (hG : G.IsHamiltonian) : G.Connected where
  preconnected a b

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
G : SimpleGraph α
inst✝ : Fintype α
hG : G.IsHamiltonian
x✝ : IsEmpty α
⊢ False

Tactic:
simpa using hG <| by simp [@Fintype.card_eq_zero]

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
G : SimpleGraph α
inst✝ : Fintype α
hG : G.IsHamiltonian
x✝ : IsEmpty α
⊢ Fintype.card α ≠ 1

Tactic:
simp [@Fintype.card_eq_zero]

Result:
no goals

Proof state:
case inr.intro.intro
α : Type u_1
inst✝¹ : DecidableEq α
G : SimpleGraph α
inst✝ : Fintype α
hG : G.IsHamiltonian
a b : α
hab : a ≠ b
this : Nontrivial α
w✝ : α
p : G.Walk w✝ w✝
hp : p.IsHamiltonianCycle
a_mem : a ∈ p.support
b_mem : b ∈ p.support
⊢ G.Reachable a b

Tactic:
exact ((p.takeUntil a a_mem).reverse.append <| p.takeUntil b b_mem).reachable

Result:
no goals

Proof state:
case inr.intro.intro
α : Type u_1
inst✝¹ : DecidableEq α
G : SimpleGraph α
inst✝ : Fintype α
hG : G.IsHamiltonian
a b : α
hab : a ≠ b
this : Nontrivial α
w✝ : α
p : G.Walk w✝ w✝
hp : p.IsHamiltonianCycle
⊢ G.Reachable a b

Tactic:
have a_mem := hp.mem_support a

Result:
case inr.intro.intro
α : Type u_1
inst✝¹ : DecidableEq α
G : SimpleGraph α
inst✝ : Fintype α
hG : G.IsHamiltonian
a b : α
hab : a ≠ b
this : Nontrivial α
w✝ : α
p : G.Walk w✝ w✝
hp : p.IsHamiltonianCycle
a_mem : a ∈ p.support
⊢ G.Reachable a b

Proof state:
case inr
α : Type u_1
inst✝¹ : DecidableEq α
G : SimpleGraph α
inst✝ : Fintype α
hG : G.IsHamiltonian
a b : α
hab : a ≠ b
this : Nontrivial α
⊢ G.Reachable a b

Tactic:
obtain ⟨_, p, hp⟩ := hG Fintype.one_lt_card.ne'

Result:
case inr.intro.intro
α : Type u_1
inst✝¹ : DecidableEq α
G : SimpleGraph α
inst✝ : Fintype α
hG : G.IsHamiltonian
a b : α
hab : a ≠ b
this : Nontrivial α
w✝ : α
p : G.Walk w✝ w✝
hp : p.IsHamiltonianCycle
⊢ G.Reachable a b

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
G : SimpleGraph α
inst✝ : Fintype α
hG : G.IsHamiltonian
a b : α
⊢ G.Reachable a b

Tactic:
obtain rfl | hab := eq_or_ne a b

Result:
case inl
α : Type u_1
inst✝¹ : DecidableEq α
G : SimpleGraph α
inst✝ : Fintype α
hG : G.IsHamiltonian
a : α
⊢ G.Reachable a a

case inr
α : Type u_1
inst✝¹ : DecidableEq α
G : SimpleGraph α
inst✝ : Fintype α
hG : G.IsHamiltonian
a b : α
hab : a ≠ b
⊢ G.Reachable a b

Proof state:
case inr
α : Type u_1
inst✝¹ : DecidableEq α
G : SimpleGraph α
inst✝ : Fintype α
hG : G.IsHamiltonian
a b : α
hab : a ≠ b
⊢ G.Reachable a b

Tactic:
have : Nontrivial α := ⟨a, b, hab⟩

Result:
case inr
α : Type u_1
inst✝¹ : DecidableEq α
G : SimpleGraph α
inst✝ : Fintype α
hG : G.IsHamiltonian
a b : α
hab : a ≠ b
this : Nontrivial α
⊢ G.Reachable a b

Proof state:
case inr.intro.intro
α : Type u_1
inst✝¹ : DecidableEq α
G : SimpleGraph α
inst✝ : Fintype α
hG : G.IsHamiltonian
a b : α
hab : a ≠ b
this : Nontrivial α
w✝ : α
p : G.Walk w✝ w✝
hp : p.IsHamiltonianCycle
a_mem : a ∈ p.support
⊢ G.Reachable a b

Tactic:
have b_mem := hp.mem_support b

Result:
case inr.intro.intro
α : Type u_1
inst✝¹ : DecidableEq α
G : SimpleGraph α
inst✝ : Fintype α
hG : G.IsHamiltonian
a b : α
hab : a ≠ b
this : Nontrivial α
w✝ : α
p : G.Walk w✝ w✝
hp : p.IsHamiltonianCycle
a_mem : a ∈ p.support
b_mem : b ∈ p.support
⊢ G.Reachable a b

Proof state:
case inl
α : Type u_1
inst✝¹ : DecidableEq α
G : SimpleGraph α
inst✝ : Fintype α
hG : G.IsHamiltonian
a : α
⊢ G.Reachable a a

Tactic:
rfl

Result:
no goals