-- Mathlib/Combinatorics/SimpleGraph/Hamiltonian.lean
lemma IsHamiltonianCycle.map {H : SimpleGraph β} (f : G →g H) (hf : Bijective f)
    (hp : p.IsHamiltonianCycle) : (p.map f).IsHamiltonianCycle where
  toIsCycle := hp.isCycle.map hf.injective
  isHamiltonian_tail

Proof state:
case nil
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
G : SimpleGraph α
a : α
H : SimpleGraph β
f : G →g H
hf : Bijective ⇑f
x : α
hp : nil.IsHamiltonianCycle
⊢ List.count (f x) (Walk.map f nil).tail.support = 1

Tactic:
cases hp.ne_nil rfl

Result:
no goals

Proof state:
case cons
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
G : SimpleGraph α
a : α
H : SimpleGraph β
f : G →g H
hf : Bijective ⇑f
x v✝ : α
y : G.Adj a v✝
p : G.Walk v✝ a
hp : (cons y p).IsHamiltonianCycle
⊢ List.count x (cons ?cons.h p).tail.support = 1

case cons.h
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
G : SimpleGraph α
a : α
H : SimpleGraph β
f : G →g H
hf : Bijective ⇑f
x v✝ : α
y : G.Adj a v✝
p : G.Walk v✝ a
hp : (cons y p).IsHamiltonianCycle
⊢ G.Adj ?m.8603 v✝

α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
G : SimpleGraph α
a : α
H : SimpleGraph β
f : G →g H
hf : Bijective ⇑f
x v✝ : α
y : G.Adj a v✝
p : G.Walk v✝ a
hp : (cons y p).IsHamiltonianCycle
⊢ α

Tactic:
exact hp.isHamiltonian_tail _

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
G : SimpleGraph α
a : α
p : G.Walk a a
H : SimpleGraph β
f : G →g H
hf : Bijective ⇑f
hp : p.IsHamiltonianCycle
⊢ (Walk.map f p).tail.IsHamiltonian

Tactic:
simp only [IsHamiltonian, hf.surjective.forall]

Result:
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
G : SimpleGraph α
a : α
p : G.Walk a a
H : SimpleGraph β
f : G →g H
hf : Bijective ⇑f
hp : p.IsHamiltonianCycle
⊢ ∀ (x : α), List.count (f x) (Walk.map f p).tail.support = 1

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
G : SimpleGraph α
a : α
p : G.Walk a a
H : SimpleGraph β
f : G →g H
hf : Bijective ⇑f
hp : p.IsHamiltonianCycle
x : α
⊢ List.count (f x) (Walk.map f p).tail.support = 1

Tactic:
rcases p with (_ | ⟨y, p⟩)

Result:
case nil
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
G : SimpleGraph α
a : α
H : SimpleGraph β
f : G →g H
hf : Bijective ⇑f
x : α
hp : nil.IsHamiltonianCycle
⊢ List.count (f x) (Walk.map f nil).tail.support = 1

case cons
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
G : SimpleGraph α
a : α
H : SimpleGraph β
f : G →g H
hf : Bijective ⇑f
x v✝ : α
y : G.Adj a v✝
p : G.Walk v✝ a
hp : (cons y p).IsHamiltonianCycle
⊢ List.count (f x) (Walk.map f (cons y p)).tail.support = 1

Proof state:
case cons
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
G : SimpleGraph α
a : α
H : SimpleGraph β
f : G →g H
hf : Bijective ⇑f
x v✝ : α
y : G.Adj a v✝
p : G.Walk v✝ a
hp : (cons y p).IsHamiltonianCycle
⊢ List.count (f x) (List.map (⇑f) p.support) = 1

Tactic:
rw [List.count_map_of_injective _ _ hf.injective, ← support_copy, ← tail_cons_eq]

Result:
case cons
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
G : SimpleGraph α
a : α
H : SimpleGraph β
f : G →g H
hf : Bijective ⇑f
x v✝ : α
y : G.Adj a v✝
p : G.Walk v✝ a
hp : (cons y p).IsHamiltonianCycle
⊢ List.count x (cons ?cons.h p).tail.support = 1

case cons.h
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
G : SimpleGraph α
a : α
H : SimpleGraph β
f : G →g H
hf : Bijective ⇑f
x v✝ : α
y : G.Adj a v✝
p : G.Walk v✝ a
hp : (cons y p).IsHamiltonianCycle
⊢ G.Adj ?m.8603 v✝

α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
G : SimpleGraph α
a : α
H : SimpleGraph β
f : G →g H
hf : Bijective ⇑f
x v✝ : α
y : G.Adj a v✝
p : G.Walk v✝ a
hp : (cons y p).IsHamiltonianCycle
⊢ α

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
G : SimpleGraph α
a : α
p : G.Walk a a
H : SimpleGraph β
f : G →g H
hf : Bijective ⇑f
hp : p.IsHamiltonianCycle
⊢ ∀ (x : α), List.count (f x) (Walk.map f p).tail.support = 1

Tactic:
intro x

Result:
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
G : SimpleGraph α
a : α
p : G.Walk a a
H : SimpleGraph β
f : G →g H
hf : Bijective ⇑f
hp : p.IsHamiltonianCycle
x : α
⊢ List.count (f x) (Walk.map f p).tail.support = 1

Proof state:
case cons
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
G : SimpleGraph α
a : α
H : SimpleGraph β
f : G →g H
hf : Bijective ⇑f
x v✝ : α
y : G.Adj a v✝
p : G.Walk v✝ a
hp : (cons y p).IsHamiltonianCycle
⊢ List.count (f x) (Walk.map f (cons y p)).tail.support = 1

Tactic:
simp only [map_cons, getVert_cons_succ, tail_cons_eq, support_copy,support_map]

Result:
case cons
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
G : SimpleGraph α
a : α
H : SimpleGraph β
f : G →g H
hf : Bijective ⇑f
x v✝ : α
y : G.Adj a v✝
p : G.Walk v✝ a
hp : (cons y p).IsHamiltonianCycle
⊢ List.count (f x) (List.map (⇑f) p.support) = 1