-- Mathlib/Combinatorics/SimpleGraph/Connectivity/WalkDecomp.lean
theorem mem_support_iff_exists_getVert {u v w : V} {p : G.Walk v w} :
    u ∈ p.support ↔ ∃ n, p.getVert n = u ∧ n ≤ p.length

Proof state:
case h
V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk v w
n : ℕ
hn : p.getVert (n + 1) = u ∧ n + 1 ≤ p.length
hnp : ¬p.Nil
⊢ p.tail.getVert n = u ∧ n ≤ p.tail.length

Tactic:
rwa [getVert_tail, ← Nat.add_one_le_add_one_iff, length_tail_add_one hnp]

Result:
no goals

Proof state:
V : Type u
G : SimpleGraph V
u : V
x✝ : (v : V) ×' (w : V) ×' G.Walk v w
a✝³ :
  ∀ (y : (v : V) ×' (w : V) ×' G.Walk v w),
    (invImage (fun x => PSigma.casesOn x fun v w => PSigma.casesOn w fun w p => p.length)
            instWellFoundedRelationOfSizeOf).1
        y x✝ →
      (u ∈ y.2.2.support ↔ ∃ n, y.2.2.getVert n = u ∧ n ≤ y.2.2.length)
v : V
w✝ : (w : V) ×' G.Walk v w
a✝² :
  ∀ (y : (v : V) ×' (w : V) ×' G.Walk v w),
    (invImage (fun x => PSigma.casesOn x fun v w => PSigma.casesOn w fun w p => p.length)
            instWellFoundedRelationOfSizeOf).1
        y ⟨v, w✝⟩ →
      (u ∈ y.2.2.support ↔ ∃ n, y.2.2.getVert n = u ∧ n ≤ y.2.2.length)
w : V
p : G.Walk v w
a✝¹ :
  ∀ (y : (v : V) ×' (w : V) ×' G.Walk v w),
    (invImage (fun x => PSigma.casesOn x fun v w => PSigma.casesOn w fun w p => p.length)
            instWellFoundedRelationOfSizeOf).1
        y ⟨v, ⟨w, p⟩⟩ →
      (u ∈ y.2.2.support ↔ ∃ n, y.2.2.getVert n = u ∧ n ≤ y.2.2.length)
a✝ : ∃ n, p.getVert n = u ∧ n ≤ p.length
n✝ : ℕ
hn✝ : p.getVert n✝ = u ∧ n✝ ≤ p.length
n : ℕ
h✝ : n✝ = n + 1
hn : p.getVert (n + 1) = u ∧ n + 1 ≤ p.length
hnp : ¬p.Nil
⊢ p.tail.length < p.length

Tactic:
rw [Nat.lt_iff_add_one_le, length_tail_add_one hnp]

Result:
no goals

Proof state:
case mpr.intro.zero
V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk v w
hn : p.getVert 0 = u ∧ 0 ≤ p.length
⊢ u = v ∨ u ∈ p.support.tail

Tactic:
aesop

Result:
no goals

Proof state:
case mp.intro.intro
V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk v w
h : u ∈ p.support
q : G.Walk v u
r : G.Walk u w
hqr : p = q.append r
⊢ ∃ n, p.getVert n = u ∧ n ≤ p.length

Tactic:
use q.length

Result:
case h
V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk v w
h : u ∈ p.support
q : G.Walk v u
r : G.Walk u w
hqr : p = q.append r
⊢ p.getVert q.length = u ∧ q.length ≤ p.length

Proof state:
case mp
V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk v w
h : u ∈ p.support
⊢ ∃ n, p.getVert n = u ∧ n ≤ p.length

Tactic:
obtain ⟨q, r, hqr⟩ := SimpleGraph.Walk.mem_support_iff_exists_append.mp h

Result:
case mp.intro.intro
V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk v w
h : u ∈ p.support
q : G.Walk v u
r : G.Walk u w
hqr : p = q.append r
⊢ ∃ n, p.getVert n = u ∧ n ≤ p.length

Proof state:
case mpr.intro
V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk v w
n : ℕ
hn : p.getVert n = u ∧ n ≤ p.length
⊢ u ∈ p.support

Tactic:
rw [mem_support_iff]

Result:
case mpr.intro
V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk v w
n : ℕ
hn : p.getVert n = u ∧ n ≤ p.length
⊢ u = v ∨ u ∈ p.support.tail

Proof state:
case mpr.intro.succ.h
V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk v w
n : ℕ
hn : p.getVert (n + 1) = u ∧ n + 1 ≤ p.length
hnp : ¬p.Nil
⊢ u ∈ p.support.tail

Tactic:
rw [← support_tail_of_not_nil _ hnp, mem_support_iff_exists_getVert]

Result:
case mpr.intro.succ.h
V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk v w
n : ℕ
hn : p.getVert (n + 1) = u ∧ n + 1 ≤ p.length
hnp : ¬p.Nil
⊢ ∃ n, p.tail.getVert n = u ∧ n ≤ p.tail.length

Proof state:
V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk v w
n : ℕ
hn : p.getVert (n + 1) = u ∧ n + 1 ≤ p.length
⊢ ¬p.length = 0

Tactic:
omega

Result:
no goals

Proof state:
V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk v w
n : ℕ
hn : p.getVert (n + 1) = u ∧ n + 1 ≤ p.length
⊢ ¬p.Nil

Tactic:
rw [nil_iff_length_eq]

Result:
V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk v w
n : ℕ
hn : p.getVert (n + 1) = u ∧ n + 1 ≤ p.length
⊢ ¬p.length = 0

Proof state:
V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk v w
⊢ u ∈ p.support ↔ ∃ n, p.getVert n = u ∧ n ≤ p.length

Tactic:
constructor

Result:
case mp
V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk v w
⊢ u ∈ p.support → ∃ n, p.getVert n = u ∧ n ≤ p.length

case mpr
V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk v w
⊢ (∃ n, p.getVert n = u ∧ n ≤ p.length) → u ∈ p.support

Proof state:
case h
V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk v w
h : u ∈ p.support
q : G.Walk v u
r : G.Walk u w
hqr : p = q.append r
⊢ (if q.length < q.length then q.getVert q.length else r.getVert (q.length - q.length)) = u ∧
    q.length ≤ (q.append r).length

Tactic:
simp only [lt_self_iff_false, ↓reduceIte, Nat.sub_self, getVert_zero, length_append,
  Nat.le_add_right, and_self]

Result:
no goals

Proof state:
case h
V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk v w
h : u ∈ p.support
q : G.Walk v u
r : G.Walk u w
hqr : p = q.append r
⊢ p.getVert q.length = u ∧ q.length ≤ p.length

Tactic:
rw [hqr, Walk.getVert_append]

Result:
case h
V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk v w
h : u ∈ p.support
q : G.Walk v u
r : G.Walk u w
hqr : p = q.append r
⊢ (if q.length < q.length then q.getVert q.length else r.getVert (q.length - q.length)) = u ∧
    q.length ≤ (q.append r).length

Proof state:
case mpr
V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk v w
⊢ (∃ n, p.getVert n = u ∧ n ≤ p.length) → u ∈ p.support

Tactic:
rintro ⟨n, hn⟩

Result:
case mpr.intro
V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk v w
n : ℕ
hn : p.getVert n = u ∧ n ≤ p.length
⊢ u ∈ p.support

Proof state:
case mpr.intro
V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk v w
n : ℕ
hn : p.getVert n = u ∧ n ≤ p.length
⊢ u = v ∨ u ∈ p.support.tail

Tactic:
cases n with
| zero => aesop
| succ n =>
  right
  have hnp : ¬ p.Nil := by
    rw [nil_iff_length_eq]
    omega
  rw [← support_tail_of_not_nil _ hnp, mem_support_iff_exists_getVert]
  use n
  rwa [getVert_tail, ← Nat.add_one_le_add_one_iff, length_tail_add_one hnp]

Result:
no goals

Proof state:
case mpr.intro.succ.h
V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk v w
n : ℕ
hn : p.getVert (n + 1) = u ∧ n + 1 ≤ p.length
⊢ u ∈ p.support.tail

Tactic:
have hnp : ¬ p.Nil := by
  rw [nil_iff_length_eq]
  omega

Result:
case mpr.intro.succ.h
V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk v w
n : ℕ
hn : p.getVert (n + 1) = u ∧ n + 1 ≤ p.length
hnp : ¬p.Nil
⊢ u ∈ p.support.tail

Proof state:
case mpr.intro.succ
V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk v w
n : ℕ
hn : p.getVert (n + 1) = u ∧ n + 1 ≤ p.length
⊢ u = v ∨ u ∈ p.support.tail

Tactic:
right

Result:
case mpr.intro.succ.h
V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk v w
n : ℕ
hn : p.getVert (n + 1) = u ∧ n + 1 ≤ p.length
⊢ u ∈ p.support.tail

Proof state:
case mpr.intro.succ.h
V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk v w
n : ℕ
hn : p.getVert (n + 1) = u ∧ n + 1 ≤ p.length
hnp : ¬p.Nil
⊢ ∃ n, p.tail.getVert n = u ∧ n ≤ p.tail.length

Tactic:
use n

Result:
case h
V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk v w
n : ℕ
hn : p.getVert (n + 1) = u ∧ n + 1 ≤ p.length
hnp : ¬p.Nil
⊢ p.tail.getVert n = u ∧ n ≤ p.tail.length

Proof state:
case mp
V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk v w
⊢ u ∈ p.support → ∃ n, p.getVert n = u ∧ n ≤ p.length

Tactic:
intro h

Result:
case mp
V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk v w
h : u ∈ p.support
⊢ ∃ n, p.getVert n = u ∧ n ≤ p.length