-- Mathlib/Combinatorics/SimpleGraph/Path.lean
lemma IsPath.getVert_injOn_iff (p : G.Walk u v) : Set.InjOn p.getVert {i | i ≤ p.length} ↔
    p.IsPath

Proof state:
V : Type u
G : SimpleGraph V
u v u✝ v✝ w✝ : V
h : G.Adj u✝ v✝
q : G.Walk v✝ w✝
ih : Set.InjOn q.getVert {i | i ≤ q.length} → q.IsPath
hinj : Set.InjOn (cons h q).getVert {i | i ≤ (cons h q).length}
h' : u✝ ∈ q.support
n : ℕ
hn : q.getVert n = u✝
hnl : n ≤ q.length
⊢ n + 1 ≤ q.length + 1

Tactic:
omega

Result:
no goals

Proof state:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
⊢ Set.InjOn p.getVert {i | i ≤ p.length} ↔ p.IsPath

Tactic:
refine ⟨?_, fun a => a.getVert_injOn⟩

Result:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
⊢ Set.InjOn p.getVert {i | i ≤ p.length} → p.IsPath

Proof state:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
⊢ Set.InjOn p.getVert {i | i ≤ p.length} → p.IsPath

Tactic:
induction p with
| nil => simp
| cons h q ih =>
  intro hinj
  rw [cons_isPath_iff]
  refine ⟨ih (by
    intro n hn m hm hnm
    simp only [Set.mem_setOf_eq] at hn hm
    have := hinj (by rw [length_cons]; omega : n + 1 ≤ (q.cons h).length)
        (by rw [length_cons]; omega : m + 1 ≤ (q.cons h).length)
        (by simpa [getVert_cons] using hnm)
    omega), fun h' => ?_⟩
  obtain ⟨n, ⟨hn, hnl⟩⟩ := mem_support_iff_exists_getVert.mp h'
  have := hinj (by rw [length_cons]; omega : (n + 1) ≤ (q.cons h).length)
    (by omega : 0 ≤ (q.cons h).length) (show (q.cons h).getVert (n + 1) = (q.cons h).getVert 0
      from by rwa [getVert_cons _ _ (by omega : n + 1 ≠ 0), getVert_zero])
  omega

Result:
no goals

Proof state:
V : Type u
G : SimpleGraph V
u v u✝ v✝ w✝ : V
h : G.Adj u✝ v✝
q : G.Walk v✝ w✝
ih : Set.InjOn q.getVert {i | i ≤ q.length} → q.IsPath
hinj : Set.InjOn (cons h q).getVert {i | i ≤ (cons h q).length}
h' : u✝ ∈ q.support
n : ℕ
hn : q.getVert n = u✝
hnl : n ≤ q.length
⊢ 0 ≤ (cons h q).length

Tactic:
omega

Result:
no goals

Proof state:
V : Type u
G : SimpleGraph V
u v u✝ v✝ w✝ : V
h : G.Adj u✝ v✝
q : G.Walk v✝ w✝
ih : Set.InjOn q.getVert {i | i ≤ q.length} → q.IsPath
hinj : Set.InjOn (cons h q).getVert {i | i ≤ (cons h q).length}
n : ℕ
hn : n ∈ {i | i ≤ q.length}
m : ℕ
hm : m ∈ {i | i ≤ q.length}
hnm : q.getVert n = q.getVert m
⊢ n = m

Tactic:
simp only [Set.mem_setOf_eq] at hn hm

Result:
V : Type u
G : SimpleGraph V
u v u✝ v✝ w✝ : V
h : G.Adj u✝ v✝
q : G.Walk v✝ w✝
ih : Set.InjOn q.getVert {i | i ≤ q.length} → q.IsPath
hinj : Set.InjOn (cons h q).getVert {i | i ≤ (cons h q).length}
n : ℕ
hn : n ≤ q.length
m : ℕ
hm : m ≤ q.length
hnm : q.getVert n = q.getVert m
⊢ n = m

Proof state:
V : Type u
G : SimpleGraph V
u v u✝ v✝ w✝ : V
h : G.Adj u✝ v✝
q : G.Walk v✝ w✝
ih : Set.InjOn q.getVert {i | i ≤ q.length} → q.IsPath
hinj : Set.InjOn (cons h q).getVert {i | i ≤ (cons h q).length}
h' : u✝ ∈ q.support
n : ℕ
hn : q.getVert n = u✝
hnl : n ≤ q.length
⊢ (cons h q).getVert (n + 1) = (cons h q).getVert 0

Tactic:
rwa [getVert_cons _ _ (by omega : n + 1 ≠ 0), getVert_zero]

Result:
no goals

Proof state:
V : Type u
G : SimpleGraph V
u v u✝ v✝ w✝ : V
h : G.Adj u✝ v✝
q : G.Walk v✝ w✝
ih : Set.InjOn q.getVert {i | i ≤ q.length} → q.IsPath
hinj : Set.InjOn (cons h q).getVert {i | i ≤ (cons h q).length}
⊢ Set.InjOn q.getVert {i | i ≤ q.length}

Tactic:
intro n hn m hm hnm

Result:
V : Type u
G : SimpleGraph V
u v u✝ v✝ w✝ : V
h : G.Adj u✝ v✝
q : G.Walk v✝ w✝
ih : Set.InjOn q.getVert {i | i ≤ q.length} → q.IsPath
hinj : Set.InjOn (cons h q).getVert {i | i ≤ (cons h q).length}
n : ℕ
hn : n ∈ {i | i ≤ q.length}
m : ℕ
hm : m ∈ {i | i ≤ q.length}
hnm : q.getVert n = q.getVert m
⊢ n = m

Proof state:
case cons
V : Type u
G : SimpleGraph V
u v u✝ v✝ w✝ : V
h : G.Adj u✝ v✝
q : G.Walk v✝ w✝
ih : Set.InjOn q.getVert {i | i ≤ q.length} → q.IsPath
hinj : Set.InjOn (cons h q).getVert {i | i ≤ (cons h q).length}
⊢ (cons h q).IsPath

Tactic:
rw [cons_isPath_iff]

Result:
case cons
V : Type u
G : SimpleGraph V
u v u✝ v✝ w✝ : V
h : G.Adj u✝ v✝
q : G.Walk v✝ w✝
ih : Set.InjOn q.getVert {i | i ≤ q.length} → q.IsPath
hinj : Set.InjOn (cons h q).getVert {i | i ≤ (cons h q).length}
⊢ q.IsPath ∧ u✝ ∉ q.support

Proof state:
case nil
V : Type u
G : SimpleGraph V
u v u✝ : V
⊢ Set.InjOn Walk.nil.getVert {i | i ≤ Walk.nil.length} → Walk.nil.IsPath

Tactic:
simp

Result:
no goals

Proof state:
V : Type u
G : SimpleGraph V
u v u✝ v✝ w✝ : V
h : G.Adj u✝ v✝
q : G.Walk v✝ w✝
ih : Set.InjOn q.getVert {i | i ≤ q.length} → q.IsPath
hinj : Set.InjOn (cons h q).getVert {i | i ≤ (cons h q).length}
n : ℕ
hn : n ≤ q.length
m : ℕ
hm : m ≤ q.length
hnm : q.getVert n = q.getVert m
⊢ m + 1 ≤ q.length + 1

Tactic:
omega

Result:
no goals

Proof state:
case cons.intro.intro
V : Type u
G : SimpleGraph V
u v u✝ v✝ w✝ : V
h : G.Adj u✝ v✝
q : G.Walk v✝ w✝
ih : Set.InjOn q.getVert {i | i ≤ q.length} → q.IsPath
hinj : Set.InjOn (cons h q).getVert {i | i ≤ (cons h q).length}
h' : u✝ ∈ q.support
n : ℕ
hn : q.getVert n = u✝
hnl : n ≤ q.length
⊢ False

Tactic:
have := hinj (by rw [length_cons]; omega : (n + 1) ≤ (q.cons h).length)
  (by omega : 0 ≤ (q.cons h).length) (show (q.cons h).getVert (n + 1) = (q.cons h).getVert 0
    from by rwa [getVert_cons _ _ (by omega : n + 1 ≠ 0), getVert_zero])

Result:
case cons.intro.intro
V : Type u
G : SimpleGraph V
u v u✝ v✝ w✝ : V
h : G.Adj u✝ v✝
q : G.Walk v✝ w✝
ih : Set.InjOn q.getVert {i | i ≤ q.length} → q.IsPath
hinj : Set.InjOn (cons h q).getVert {i | i ≤ (cons h q).length}
h' : u✝ ∈ q.support
n : ℕ
hn : q.getVert n = u✝
hnl : n ≤ q.length
this : n + 1 = 0
⊢ False

Proof state:
V : Type u
G : SimpleGraph V
u v u✝ v✝ w✝ : V
h : G.Adj u✝ v✝
q : G.Walk v✝ w✝
ih : Set.InjOn q.getVert {i | i ≤ q.length} → q.IsPath
hinj : Set.InjOn (cons h q).getVert {i | i ≤ (cons h q).length}
h' : u✝ ∈ q.support
n : ℕ
hn : q.getVert n = u✝
hnl : n ≤ q.length
⊢ n + 1 ≤ (cons h q).length

Tactic:
rw [length_cons]

Result:
V : Type u
G : SimpleGraph V
u v u✝ v✝ w✝ : V
h : G.Adj u✝ v✝
q : G.Walk v✝ w✝
ih : Set.InjOn q.getVert {i | i ≤ q.length} → q.IsPath
hinj : Set.InjOn (cons h q).getVert {i | i ≤ (cons h q).length}
h' : u✝ ∈ q.support
n : ℕ
hn : q.getVert n = u✝
hnl : n ≤ q.length
⊢ n + 1 ≤ q.length + 1

Proof state:
case cons
V : Type u
G : SimpleGraph V
u v u✝ v✝ w✝ : V
h : G.Adj u✝ v✝
q : G.Walk v✝ w✝
ih : Set.InjOn q.getVert {i | i ≤ q.length} → q.IsPath
hinj : Set.InjOn (cons h q).getVert {i | i ≤ (cons h q).length}
⊢ q.IsPath ∧ u✝ ∉ q.support

Tactic:
refine ⟨ih (by
  intro n hn m hm hnm
  simp only [Set.mem_setOf_eq] at hn hm
  have := hinj (by rw [length_cons]; omega : n + 1 ≤ (q.cons h).length)
      (by rw [length_cons]; omega : m + 1 ≤ (q.cons h).length)
      (by simpa [getVert_cons] using hnm)
  omega), fun h' => ?_⟩

Result:
case cons
V : Type u
G : SimpleGraph V
u v u✝ v✝ w✝ : V
h : G.Adj u✝ v✝
q : G.Walk v✝ w✝
ih : Set.InjOn q.getVert {i | i ≤ q.length} → q.IsPath
hinj : Set.InjOn (cons h q).getVert {i | i ≤ (cons h q).length}
h' : u✝ ∈ q.support
⊢ False

Proof state:
case cons
V : Type u
G : SimpleGraph V
u v u✝ v✝ w✝ : V
h : G.Adj u✝ v✝
q : G.Walk v✝ w✝
ih : Set.InjOn q.getVert {i | i ≤ q.length} → q.IsPath
⊢ Set.InjOn (cons h q).getVert {i | i ≤ (cons h q).length} → (cons h q).IsPath

Tactic:
intro hinj

Result:
case cons
V : Type u
G : SimpleGraph V
u v u✝ v✝ w✝ : V
h : G.Adj u✝ v✝
q : G.Walk v✝ w✝
ih : Set.InjOn q.getVert {i | i ≤ q.length} → q.IsPath
hinj : Set.InjOn (cons h q).getVert {i | i ≤ (cons h q).length}
⊢ (cons h q).IsPath

Proof state:
V : Type u
G : SimpleGraph V
u v u✝ v✝ w✝ : V
h : G.Adj u✝ v✝
q : G.Walk v✝ w✝
ih : Set.InjOn q.getVert {i | i ≤ q.length} → q.IsPath
hinj : Set.InjOn (cons h q).getVert {i | i ≤ (cons h q).length}
n : ℕ
hn : n ≤ q.length
m : ℕ
hm : m ≤ q.length
hnm : q.getVert n = q.getVert m
this : n + 1 = m + 1
⊢ n = m

Tactic:
omega

Result:
no goals