-- Mathlib/Combinatorics/SimpleGraph/Path.lean
lemma IsCycle.getVert_sub_one_neq_getVert_add_one {i : ℕ} {p : G.Walk u u} (hpc : p.IsCycle)
    (h : i ≤ p.length) : p.getVert (i - 1) ≠ p.getVert (i + 1)

Proof state:
case neg
V : Type u
G : SimpleGraph V
u : V
i : ℕ
p : G.Walk u u
hpc : p.IsCycle
h : i ≤ p.length
hl : 3 ≤ p.length
hi' : ¬i ≥ p.length - 1
⊢ p.getVert (i - 1) ≠ p.getVert (i + 1)

Tactic:
intro h'

Result:
case neg
V : Type u
G : SimpleGraph V
u : V
i : ℕ
p : G.Walk u u
hpc : p.IsCycle
h : i ≤ p.length
hl : 3 ≤ p.length
hi' : ¬i ≥ p.length - 1
h' : p.getVert (i - 1) = p.getVert (i + 1)
⊢ False

Proof state:
V : Type u
G : SimpleGraph V
u : V
i : ℕ
p : G.Walk u u
hpc : p.IsCycle
h : i ≤ p.length
hl : 3 ≤ p.length
hi' : ¬i ≥ p.length - 1
h' : p.getVert (i - 1) = p.getVert (i + 1)
⊢ i + 1 ≤ p.length - 1

Tactic:
omega

Result:
no goals

Proof state:
V : Type u
G : SimpleGraph V
u : V
i : ℕ
p : G.Walk u u
hpc : p.IsCycle
h : i ≤ p.length
hl : 3 ≤ p.length
hi' : i ≥ p.length - 1
h' : p.getVert (i - 1) = p.getVert (i + 1)
⊢ p.length ≤ i + 1

Tactic:
omega

Result:
no goals

Proof state:
case pos
V : Type u
G : SimpleGraph V
u : V
i : ℕ
p : G.Walk u u
hpc : p.IsCycle
h : i ≤ p.length
hl : 3 ≤ p.length
hi' : i ≥ p.length - 1
h' : p.getVert (i - 1) = p.getVert (i + 1)
⊢ False

Tactic:
rw [p.getVert_of_length_le (by omega : p.length ≤ i + 1),
  hpc.getVert_endpoint_iff (by omega)] at h'

Result:
case pos
V : Type u
G : SimpleGraph V
u : V
i : ℕ
p : G.Walk u u
hpc : p.IsCycle
h : i ≤ p.length
hl : 3 ≤ p.length
hi' : i ≥ p.length - 1
h' : i - 1 = 0 ∨ i - 1 = p.length
⊢ False

Proof state:
case neg
V : Type u
G : SimpleGraph V
u : V
i : ℕ
p : G.Walk u u
hpc : p.IsCycle
h : i ≤ p.length
hl : 3 ≤ p.length
hi' : ¬i ≥ p.length - 1
h' : p.getVert (i - 1) = p.getVert (i + 1)
⊢ False

Tactic:
have := hpc.getVert_injOn' (by simp only [Set.mem_setOf_eq, Nat.sub_le_iff_le_add]; omega)
  (by simp only [Set.mem_setOf_eq]; omega) h'

Result:
case neg
V : Type u
G : SimpleGraph V
u : V
i : ℕ
p : G.Walk u u
hpc : p.IsCycle
h : i ≤ p.length
hl : 3 ≤ p.length
hi' : ¬i ≥ p.length - 1
h' : p.getVert (i - 1) = p.getVert (i + 1)
this : i - 1 = i + 1
⊢ False

Proof state:
V : Type u
G : SimpleGraph V
u : V
i : ℕ
p : G.Walk u u
hpc : p.IsCycle
h : i ≤ p.length
hl : 3 ≤ p.length
hi' : ¬i ≥ p.length - 1
h' : p.getVert (i - 1) = p.getVert (i + 1)
⊢ i - 1 ∈ {i | i ≤ p.length - 1}

Tactic:
simp only [Set.mem_setOf_eq, Nat.sub_le_iff_le_add]

Result:
V : Type u
G : SimpleGraph V
u : V
i : ℕ
p : G.Walk u u
hpc : p.IsCycle
h : i ≤ p.length
hl : 3 ≤ p.length
hi' : ¬i ≥ p.length - 1
h' : p.getVert (i - 1) = p.getVert (i + 1)
⊢ i ≤ p.length - 1 + 1

Proof state:
V : Type u
G : SimpleGraph V
u : V
i : ℕ
p : G.Walk u u
hpc : p.IsCycle
h : i ≤ p.length
hl : 3 ≤ p.length
hi' : ¬i ≥ p.length - 1
h' : p.getVert (i - 1) = p.getVert (i + 1)
⊢ i ≤ p.length - 1 + 1

Tactic:
omega

Result:
no goals

Proof state:
case pos
V : Type u
G : SimpleGraph V
u : V
i : ℕ
p : G.Walk u u
hpc : p.IsCycle
h : i ≤ p.length
hl : 3 ≤ p.length
hi' : i ≥ p.length - 1
h' : i - 1 = 0 ∨ i - 1 = p.length
⊢ False

Tactic:
omega

Result:
no goals

Proof state:
V : Type u
G : SimpleGraph V
u : V
i : ℕ
p : G.Walk u u
hpc : p.IsCycle
h : i ≤ p.length
hl : 3 ≤ p.length
hi' : i ≥ p.length - 1
h' : p.getVert (i - 1) = u
⊢ i - 1 ≤ p.length

Tactic:
omega

Result:
no goals

Proof state:
V : Type u
G : SimpleGraph V
u : V
i : ℕ
p : G.Walk u u
hpc : p.IsCycle
h : i ≤ p.length
hl : 3 ≤ p.length
hi' : ¬i ≥ p.length - 1
h' : p.getVert (i - 1) = p.getVert (i + 1)
⊢ i + 1 ∈ {i | i ≤ p.length - 1}

Tactic:
simp only [Set.mem_setOf_eq]

Result:
V : Type u
G : SimpleGraph V
u : V
i : ℕ
p : G.Walk u u
hpc : p.IsCycle
h : i ≤ p.length
hl : 3 ≤ p.length
hi' : ¬i ≥ p.length - 1
h' : p.getVert (i - 1) = p.getVert (i + 1)
⊢ i + 1 ≤ p.length - 1

Proof state:
V : Type u
G : SimpleGraph V
u : V
i : ℕ
p : G.Walk u u
hpc : p.IsCycle
h : i ≤ p.length
hl : 3 ≤ p.length
⊢ p.getVert (i - 1) ≠ p.getVert (i + 1)

Tactic:
by_cases hi' : i ≥ p.length - 1

Result:
case pos
V : Type u
G : SimpleGraph V
u : V
i : ℕ
p : G.Walk u u
hpc : p.IsCycle
h : i ≤ p.length
hl : 3 ≤ p.length
hi' : i ≥ p.length - 1
⊢ p.getVert (i - 1) ≠ p.getVert (i + 1)

case neg
V : Type u
G : SimpleGraph V
u : V
i : ℕ
p : G.Walk u u
hpc : p.IsCycle
h : i ≤ p.length
hl : 3 ≤ p.length
hi' : ¬i ≥ p.length - 1
⊢ p.getVert (i - 1) ≠ p.getVert (i + 1)

Proof state:
case pos
V : Type u
G : SimpleGraph V
u : V
i : ℕ
p : G.Walk u u
hpc : p.IsCycle
h : i ≤ p.length
hl : 3 ≤ p.length
hi' : i ≥ p.length - 1
⊢ p.getVert (i - 1) ≠ p.getVert (i + 1)

Tactic:
intro h'

Result:
case pos
V : Type u
G : SimpleGraph V
u : V
i : ℕ
p : G.Walk u u
hpc : p.IsCycle
h : i ≤ p.length
hl : 3 ≤ p.length
hi' : i ≥ p.length - 1
h' : p.getVert (i - 1) = p.getVert (i + 1)
⊢ False

Proof state:
V : Type u
G : SimpleGraph V
u : V
i : ℕ
p : G.Walk u u
hpc : p.IsCycle
h : i ≤ p.length
⊢ p.getVert (i - 1) ≠ p.getVert (i + 1)

Tactic:
have hl := hpc.three_le_length

Result:
V : Type u
G : SimpleGraph V
u : V
i : ℕ
p : G.Walk u u
hpc : p.IsCycle
h : i ≤ p.length
hl : 3 ≤ p.length
⊢ p.getVert (i - 1) ≠ p.getVert (i + 1)

Proof state:
case neg
V : Type u
G : SimpleGraph V
u : V
i : ℕ
p : G.Walk u u
hpc : p.IsCycle
h : i ≤ p.length
hl : 3 ≤ p.length
hi' : ¬i ≥ p.length - 1
h' : p.getVert (i - 1) = p.getVert (i + 1)
this : i - 1 = i + 1
⊢ False

Tactic:
omega

Result:
no goals