-- Mathlib/Combinatorics/SimpleGraph/Path.lean
lemma IsPath.getVert_eq_start_iff {i : ℕ} {p : G.Walk u w} (hp : p.IsPath) (hi : i ≤ p.length) :
    p.getVert i = u ↔ i = 0

Proof state:
V : Type u
G : SimpleGraph V
u w : V
i : ℕ
p : G.Walk u w
hp : p.IsPath
hi✝ : i ≤ p.length
h : p.getVert i = u
hi : ¬i = 0
⊢ i ≤ p.length

Tactic:
omega

Result:
no goals

Proof state:
V : Type u
G : SimpleGraph V
u w : V
i : ℕ
p : G.Walk u w
hp : p.IsPath
hi✝ : i ≤ p.length
h : p.getVert i = u
hi : ¬i = 0
⊢ 0 ∈ {i | i ≤ p.length}

Tactic:
rw [Set.mem_setOf]

Result:
V : Type u
G : SimpleGraph V
u w : V
i : ℕ
p : G.Walk u w
hp : p.IsPath
hi✝ : i ≤ p.length
h : p.getVert i = u
hi : ¬i = 0
⊢ 0 ≤ p.length

Proof state:
case pos
V : Type u
G : SimpleGraph V
u w : V
i : ℕ
p : G.Walk u w
hp : p.IsPath
hi✝ : i ≤ p.length
h : p.getVert i = u
hi : i = 0
⊢ i = 0

Tactic:
exact hi

Result:
no goals

Proof state:
V : Type u
G : SimpleGraph V
u w : V
i : ℕ
p : G.Walk u w
hp : p.IsPath
hi✝ : i ≤ p.length
h : p.getVert i = u
hi : ¬i = 0
⊢ i ∈ {i | i ≤ p.length}

Tactic:
rw [Set.mem_setOf]

Result:
V : Type u
G : SimpleGraph V
u w : V
i : ℕ
p : G.Walk u w
hp : p.IsPath
hi✝ : i ≤ p.length
h : p.getVert i = u
hi : ¬i = 0
⊢ i ≤ p.length

Proof state:
V : Type u
G : SimpleGraph V
u w : V
i : ℕ
p : G.Walk u w
hp : p.IsPath
hi : i ≤ p.length
⊢ i = 0 → p.getVert i = u

Tactic:
aesop

Result:
no goals

Proof state:
V : Type u
G : SimpleGraph V
u w : V
i : ℕ
p : G.Walk u w
hp : p.IsPath
hi : i ≤ p.length
⊢ p.getVert i = u ↔ i = 0

Tactic:
refine ⟨?_, by aesop⟩

Result:
V : Type u
G : SimpleGraph V
u w : V
i : ℕ
p : G.Walk u w
hp : p.IsPath
hi : i ≤ p.length
⊢ p.getVert i = u → i = 0

Proof state:
case neg
V : Type u
G : SimpleGraph V
u w : V
i : ℕ
p : G.Walk u w
hp : p.IsPath
hi✝ : i ≤ p.length
h : p.getVert i = u
hi : ¬i = 0
⊢ i = 0

Tactic:
apply hp.getVert_injOn (by rw [Set.mem_setOf]; omega) (by rw [Set.mem_setOf]; omega)

Result:
case neg
V : Type u
G : SimpleGraph V
u w : V
i : ℕ
p : G.Walk u w
hp : p.IsPath
hi✝ : i ≤ p.length
h : p.getVert i = u
hi : ¬i = 0
⊢ p.getVert i = p.getVert 0

Proof state:
V : Type u
G : SimpleGraph V
u w : V
i : ℕ
p : G.Walk u w
hp : p.IsPath
hi : i ≤ p.length
⊢ p.getVert i = u → i = 0

Tactic:
intro h

Result:
V : Type u
G : SimpleGraph V
u w : V
i : ℕ
p : G.Walk u w
hp : p.IsPath
hi : i ≤ p.length
h : p.getVert i = u
⊢ i = 0

Proof state:
case neg
V : Type u
G : SimpleGraph V
u w : V
i : ℕ
p : G.Walk u w
hp : p.IsPath
hi✝ : i ≤ p.length
h : p.getVert i = u
hi : ¬i = 0
⊢ p.getVert i = p.getVert 0

Tactic:
simp [h]

Result:
no goals

Proof state:
V : Type u
G : SimpleGraph V
u w : V
i : ℕ
p : G.Walk u w
hp : p.IsPath
hi : i ≤ p.length
h : p.getVert i = u
⊢ i = 0

Tactic:
by_cases hi : i = 0

Result:
case pos
V : Type u
G : SimpleGraph V
u w : V
i : ℕ
p : G.Walk u w
hp : p.IsPath
hi✝ : i ≤ p.length
h : p.getVert i = u
hi : i = 0
⊢ i = 0

case neg
V : Type u
G : SimpleGraph V
u w : V
i : ℕ
p : G.Walk u w
hp : p.IsPath
hi✝ : i ≤ p.length
h : p.getVert i = u
hi : ¬i = 0
⊢ i = 0

Proof state:
V : Type u
G : SimpleGraph V
u w : V
i : ℕ
p : G.Walk u w
hp : p.IsPath
hi✝ : i ≤ p.length
h : p.getVert i = u
hi : ¬i = 0
⊢ 0 ≤ p.length

Tactic:
omega

Result:
no goals