awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
u_1 v_1 v w u : V
h : G.Adj v w
p : G.Walk w u
ihp :
  ∀ (hp : p.IsPath) ⦃n : ℕ⦄ (hn : Membership.mem (γ := Set ℕ) {i : ℕ | i ≤ p.length} n) ⦃m : ℕ⦄
    (hm : Membership.mem (γ := Set ℕ) {i : ℕ | i ≤ p.length} m) (hnm : p.getVert n = p.getVert m), n = m
hp : (cons h p).IsPath
n : ℕ
hn : n ≤ p.length + 1
m : ℕ
hm : m ≤ p.length + 1
hnm : (cons h p).getVert n = (cons h p).getVert m
hn0 : n = 0
pos : ∀ (hm0 : m = 0), n = m
neg : ∀ (hm0 : ¬m = 0), n = m
⊢ n = m

Tactic:
by_cases hm0 : m = 0
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
u_1 v_1 v w u : V
h : G.Adj v w
p : G.Walk w u
ihp :
  ∀ (hp : p.IsPath) ⦃n : ℕ⦄ (hn : Membership.mem (γ := Set ℕ) {i : ℕ | i ≤ p.length} n) ⦃m : ℕ⦄
    (hm : Membership.mem (γ := Set ℕ) {i : ℕ | i ≤ p.length} m) (hnm : p.getVert n = p.getVert m), n = m
hp : (cons h p).IsPath
n : ℕ
hn : n ≤ p.length + 1
m : ℕ
hm : m ≤ p.length + 1
hnm : (cons h p).getVert n = (cons h p).getVert m
hn0 : ¬n = 0
pos : ∀ (hm0 : m = 0), n = m
neg : ∀ (hm0 : ¬m = 0), n = m
⊢ n = m

Tactic:
by_cases hm0 : m = 0
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
u_1 v_1 v w u : V
h : G.Adj v w
p : G.Walk w u
ihp :
  ∀ (hp : p.IsPath) ⦃n : ℕ⦄ (hn : Membership.mem (γ := Set ℕ) {i : ℕ | i ≤ p.length} n) ⦃m : ℕ⦄
    (hm : Membership.mem (γ := Set ℕ) {i : ℕ | i ≤ p.length} m) (hnm : p.getVert n = p.getVert m), n = m
hp : (cons h p).IsPath
n : ℕ
hn : n ≤ p.length + 1
m : ℕ
hm : m ≤ p.length + 1
hnm : (cons h p).getVert n = (cons h p).getVert m
hn0 : n = 0
hm0 : m = 0
⊢ n = m

Tactic:
lia
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
u_1 v_1 v w u : V
h : G.Adj v w
p : G.Walk w u
ihp :
  ∀ (hp : p.IsPath) ⦃n : ℕ⦄ (hn : Membership.mem (γ := Set ℕ) {i : ℕ | i ≤ p.length} n) ⦃m : ℕ⦄
    (hm : Membership.mem (γ := Set ℕ) {i : ℕ | i ≤ p.length} m) (hnm : p.getVert n = p.getVert m), n = m
hp : (cons h p).IsPath
n : ℕ
hn : n ≤ p.length + 1
m : ℕ
hm : m ≤ p.length + 1
hnm : (cons h p).getVert n = (cons h p).getVert m
hn0 : n = 0
hm0 : ¬m = 0
⊢ v = p.getVert (m - 1)

Tactic:
simp only [hn0, getVert_zero, Walk.getVert_cons p h hm0] at hnm

Premises used: SimpleGraph.Walk.getVert_cons, SimpleGraph.Walk.getVert_zero
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
u_1 v_1 v w u : V
h : G.Adj v w
p : G.Walk w u
ihp :
  ∀ (hp : p.IsPath) ⦃n : ℕ⦄ (hn : Membership.mem (γ := Set ℕ) {i : ℕ | i ≤ p.length} n) ⦃m : ℕ⦄
    (hm : Membership.mem (γ := Set ℕ) {i : ℕ | i ≤ p.length} m) (hnm : p.getVert n = p.getVert m), n = m
hp : (cons h p).IsPath
n : ℕ
hn : n ≤ p.length + 1
m : ℕ
hm : m ≤ p.length + 1
hn0 : n = 0
hm0 : ¬m = 0
hnm : v = p.getVert (m - 1)
⊢ v ∉ p.support

Tactic:
aesop
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
u_1 v_1 v w u : V
h : G.Adj v w
p : G.Walk w u
ihp :
  ∀ (hp : p.IsPath) ⦃n : ℕ⦄ (hn : Membership.mem (γ := Set ℕ) {i : ℕ | i ≤ p.length} n) ⦃m : ℕ⦄
    (hm : Membership.mem (γ := Set ℕ) {i : ℕ | i ≤ p.length} m) (hnm : p.getVert n = p.getVert m), n = m
hp : (cons h p).IsPath
n : ℕ
hn : n ≤ p.length + 1
m : ℕ
hm : m ≤ p.length + 1
hn0 : n = 0
hm0 : ¬m = 0
hnm : v = p.getVert (m - 1)
⊢ v ∉ p.support

Tactic:
have hvp : v ∉ p.support := by aesop
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
u_1 v_1 v w u : V
h : G.Adj v w
p : G.Walk w u
ihp :
  ∀ (hp : p.IsPath) ⦃n : ℕ⦄ (hn : Membership.mem (γ := Set ℕ) {i : ℕ | i ≤ p.length} n) ⦃m : ℕ⦄
    (hm : Membership.mem (γ := Set ℕ) {i : ℕ | i ≤ p.length} m) (hnm : p.getVert n = p.getVert m), n = m
hp : (cons h p).IsPath
n : ℕ
hn : n ≤ p.length + 1
m : ℕ
hm : m ≤ p.length + 1
hn0 : n = 0
hm0 : ¬m = 0
hnm : v = p.getVert (m - 1)
hvp : v ∉ p.support
⊢ m - 1 ≤ p.length

Tactic:
lia
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
u_1 v_1 v w u : V
h : G.Adj v w
p : G.Walk w u
ihp :
  ∀ (hp : p.IsPath) ⦃n : ℕ⦄ (hn : Membership.mem (γ := Set ℕ) {i : ℕ | i ≤ p.length} n) ⦃m : ℕ⦄
    (hm : Membership.mem (γ := Set ℕ) {i : ℕ | i ≤ p.length} m) (hnm : p.getVert n = p.getVert m), n = m
hp : (cons h p).IsPath
n : ℕ
hn : n ≤ p.length + 1
m : ℕ
hm : m ≤ p.length + 1
hn0 : n = 0
hm0 : ¬m = 0
hnm : v = p.getVert (m - 1)
hvp : v ∉ p.support
⊢ n = m

Tactic:
exact (hvp (Walk.mem_support_iff_exists_getVert.mpr ⟨(m - 1), ⟨hnm.symm, by lia⟩⟩)).elim

Premises used: Iff.mpr, False.elim, HSub.hSub, And.intro, Exists.intro, OfNat.ofNat, Eq.symm, SimpleGraph.Walk.mem_support_iff_exists_getVert
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
u_1 v_1 v w u : V
h : G.Adj v w
p : G.Walk w u
ihp :
  ∀ (hp : p.IsPath) ⦃n : ℕ⦄ (hn : Membership.mem (γ := Set ℕ) {i : ℕ | i ≤ p.length} n) ⦃m : ℕ⦄
    (hm : Membership.mem (γ := Set ℕ) {i : ℕ | i ≤ p.length} m) (hnm : p.getVert n = p.getVert m), n = m
hp : (cons h p).IsPath
n : ℕ
hn : n ≤ p.length + 1
m : ℕ
hm : m ≤ p.length + 1
hnm : (cons h p).getVert n = (cons h p).getVert m
hn0 : ¬n = 0
hm0 : m = 0
⊢ p.getVert (n - 1) = (cons h p).getVert 0

Tactic:
simp only [hm0, Walk.getVert_cons p h hn0] at hnm

Premises used: SimpleGraph.Walk.getVert_cons
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
u_1 v_1 v w u : V
h : G.Adj v w
p : G.Walk w u
ihp :
  ∀ (hp : p.IsPath) ⦃n : ℕ⦄ (hn : Membership.mem (γ := Set ℕ) {i : ℕ | i ≤ p.length} n) ⦃m : ℕ⦄
    (hm : Membership.mem (γ := Set ℕ) {i : ℕ | i ≤ p.length} m) (hnm : p.getVert n = p.getVert m), n = m
hp : (cons h p).IsPath
n : ℕ
hn : n ≤ p.length + 1
m : ℕ
hm : m ≤ p.length + 1
hn0 : ¬n = 0
hm0 : m = 0
hnm : p.getVert (n - 1) = (cons h p).getVert 0
⊢ v ∉ p.support

Tactic:
simp_all
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
u_1 v_1 v w u : V
h : G.Adj v w
p : G.Walk w u
ihp :
  ∀ (hp : p.IsPath) ⦃n : ℕ⦄ (hn : Membership.mem (γ := Set ℕ) {i : ℕ | i ≤ p.length} n) ⦃m : ℕ⦄
    (hm : Membership.mem (γ := Set ℕ) {i : ℕ | i ≤ p.length} m) (hnm : p.getVert n = p.getVert m), n = m
hp : (cons h p).IsPath
n : ℕ
hn : n ≤ p.length + 1
m : ℕ
hm : m ≤ p.length + 1
hn0 : ¬n = 0
hm0 : m = 0
hnm : p.getVert (n - 1) = (cons h p).getVert 0
⊢ v ∉ p.support

Tactic:
have hvp : v ∉ p.support := by simp_all
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
u_1 v_1 v w u : V
h : G.Adj v w
p : G.Walk w u
ihp :
  ∀ (hp : p.IsPath) ⦃n : ℕ⦄ (hn : Membership.mem (γ := Set ℕ) {i : ℕ | i ≤ p.length} n) ⦃m : ℕ⦄
    (hm : Membership.mem (γ := Set ℕ) {i : ℕ | i ≤ p.length} m) (hnm : p.getVert n = p.getVert m), n = m
hp : (cons h p).IsPath
n : ℕ
hn : n ≤ p.length + 1
m : ℕ
hm : m ≤ p.length + 1
hn0 : ¬n = 0
hm0 : m = 0
hnm : p.getVert (n - 1) = (cons h p).getVert 0
hvp : v ∉ p.support
⊢ n - 1 ≤ p.length

Tactic:
lia
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
u_1 v_1 v w u : V
h : G.Adj v w
p : G.Walk w u
ihp :
  ∀ (hp : p.IsPath) ⦃n : ℕ⦄ (hn : Membership.mem (γ := Set ℕ) {i : ℕ | i ≤ p.length} n) ⦃m : ℕ⦄
    (hm : Membership.mem (γ := Set ℕ) {i : ℕ | i ≤ p.length} m) (hnm : p.getVert n = p.getVert m), n = m
hp : (cons h p).IsPath
n : ℕ
hn : n ≤ p.length + 1
m : ℕ
hm : m ≤ p.length + 1
hn0 : ¬n = 0
hm0 : m = 0
hnm : p.getVert (n - 1) = (cons h p).getVert 0
hvp : v ∉ p.support
⊢ n = m

Tactic:
exact (hvp (Walk.mem_support_iff_exists_getVert.mpr ⟨(n - 1), ⟨hnm, by lia⟩⟩)).elim

Premises used: Iff.mpr, False.elim, HSub.hSub, And.intro, Exists.intro, OfNat.ofNat, SimpleGraph.Walk.mem_support_iff_exists_getVert
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
u_1 v_1 v w u : V
h : G.Adj v w
p : G.Walk w u
ihp :
  ∀ (hp : p.IsPath) ⦃n : ℕ⦄ (hn : Membership.mem (γ := Set ℕ) {i : ℕ | i ≤ p.length} n) ⦃m : ℕ⦄
    (hm : Membership.mem (γ := Set ℕ) {i : ℕ | i ≤ p.length} m) (hnm : p.getVert n = p.getVert m), n = m
hp : (cons h p).IsPath
n : ℕ
hn : n ≤ p.length + 1
m : ℕ
hm : m ≤ p.length + 1
hnm : (cons h p).getVert n = (cons h p).getVert m
hn0 : ¬n = 0
hm0 : ¬m = 0
⊢ p.getVert (n - 1) = p.getVert (m - 1)

Tactic:
simp only [Walk.getVert_cons _ _ hn0, Walk.getVert_cons _ _ hm0] at hnm

Premises used: SimpleGraph.Walk.getVert_cons
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
u_1 v_1 v w u : V
h : G.Adj v w
p : G.Walk w u
ihp :
  ∀ (hp : p.IsPath) ⦃n : ℕ⦄ (hn : Membership.mem (γ := Set ℕ) {i : ℕ | i ≤ p.length} n) ⦃m : ℕ⦄
    (hm : Membership.mem (γ := Set ℕ) {i : ℕ | i ≤ p.length} m) (hnm : p.getVert n = p.getVert m), n = m
hp : (cons h p).IsPath
n : ℕ
hn : n ≤ p.length + 1
m : ℕ
hm : m ≤ p.length + 1
hn0 : ¬n = 0
hm0 : ¬m = 0
hnm : p.getVert (n - 1) = p.getVert (m - 1)
⊢ n - 1 ≤ p.length

Tactic:
lia
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
u_1 v_1 v w u : V
h : G.Adj v w
p : G.Walk w u
ihp :
  ∀ (hp : p.IsPath) ⦃n : ℕ⦄ (hn : Membership.mem (γ := Set ℕ) {i : ℕ | i ≤ p.length} n) ⦃m : ℕ⦄
    (hm : Membership.mem (γ := Set ℕ) {i : ℕ | i ≤ p.length} m) (hnm : p.getVert n = p.getVert m), n = m
hp : (cons h p).IsPath
n : ℕ
hn : n ≤ p.length + 1
m : ℕ
hm : m ≤ p.length + 1
hn0 : ¬n = 0
hm0 : ¬m = 0
hnm : p.getVert (n - 1) = p.getVert (m - 1)
⊢ m - 1 ≤ p.length

Tactic:
lia
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
u_1 v_1 v w u : V
h : G.Adj v w
p : G.Walk w u
ihp :
  ∀ (hp : p.IsPath) ⦃n : ℕ⦄ (hn : Membership.mem (γ := Set ℕ) {i : ℕ | i ≤ p.length} n) ⦃m : ℕ⦄
    (hm : Membership.mem (γ := Set ℕ) {i : ℕ | i ≤ p.length} m) (hnm : p.getVert n = p.getVert m), n = m
hp : (cons h p).IsPath
n : ℕ
hn : n ≤ p.length + 1
m : ℕ
hm : m ≤ p.length + 1
hn0 : ¬n = 0
hm0 : ¬m = 0
hnm : p.getVert (n - 1) = p.getVert (m - 1)
⊢ n - 1 = m - 1

Tactic:
have := ihp hp.of_cons (by lia : (n - 1) ≤ p.length)
        (by lia : (m - 1) ≤ p.length) hnm
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
u_1 v_1 v w u : V
h : G.Adj v w
p : G.Walk w u
ihp :
  ∀ (hp : p.IsPath) ⦃n : ℕ⦄ (hn : Membership.mem (γ := Set ℕ) {i : ℕ | i ≤ p.length} n) ⦃m : ℕ⦄
    (hm : Membership.mem (γ := Set ℕ) {i : ℕ | i ≤ p.length} m) (hnm : p.getVert n = p.getVert m), n = m
hp : (cons h p).IsPath
n : ℕ
hn : n ≤ p.length + 1
m : ℕ
hm : m ≤ p.length + 1
hn0 : ¬n = 0
hm0 : ¬m = 0
hnm : p.getVert (n - 1) = p.getVert (m - 1)
this : n - 1 = m - 1
⊢ n = m

Tactic:
lia
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
hp : p.IsPath
n : ℕ
hn : Membership.mem (γ := Set ℕ) {i : ℕ | i ≤ p.length} n
m : ℕ
hm : Membership.mem (γ := Set ℕ) {i : ℕ | i ≤ p.length} m
hnm : p.getVert n = p.getVert m
nil :
  ∀ {u : V} (hp : IsPath.{u} (V := V) (G := G) (u := u) Walk.nil) ⦃n : ℕ⦄
    (hn : Membership.mem (γ := Set ℕ) {i : ℕ | i ≤ length.{u} (V := V) (G := G) (u := u) Walk.nil} n) ⦃m : ℕ⦄
    (hm : Membership.mem (γ := Set ℕ) {i : ℕ | i ≤ length.{u} (V := V) (G := G) (u := u) Walk.nil} m)
    (hnm : Eq.{u + 1} (α := V) (getVert (G := G) (u := u) Walk.nil n) (getVert (G := G) (u := u) Walk.nil m)), n = m
cons :
  ∀ {v w u : V} (h : G.Adj v w) (p : G.Walk w u)
    (ihp :
      ∀ (hp : p.IsPath) ⦃n : ℕ⦄ (hn : Membership.mem (γ := Set ℕ) {i : ℕ | i ≤ p.length} n) ⦃m : ℕ⦄
        (hm : Membership.mem (γ := Set ℕ) {i : ℕ | i ≤ p.length} m) (hnm : p.getVert n = p.getVert m), n = m)
    (hp : (Walk.cons h p).IsPath) ⦃n : ℕ⦄ (hn : Membership.mem (γ := Set ℕ) {i : ℕ | i ≤ (Walk.cons h p).length} n)
    ⦃m : ℕ⦄ (hm : Membership.mem (γ := Set ℕ) {i : ℕ | i ≤ (Walk.cons h p).length} m)
    (hnm : (Walk.cons h p).getVert n = (Walk.cons h p).getVert m), n = m
⊢ n = m

Tactic:
induction p generalizing n m with
  | nil => simp_all
  | @cons v w u h p ihp =>
    simp only [length_cons, Set.mem_setOf_eq] at hn hm hnm
    by_cases hn0 : n = 0 <;> by_cases hm0 : m = 0
    · lia
    · simp only [hn0, getVert_zero, Walk.getVert_cons p h hm0] at hnm
      have hvp : v ∉ p.support := by aesop
      exact (hvp (Walk.mem_support_iff_exists_getVert.mpr ⟨(m - 1), ⟨hnm.symm, by lia⟩⟩)).elim
    · simp only [hm0, Walk.getVert_cons p h hn0] at hnm
      have hvp : v ∉ p.support := by simp_all
      exact (hvp (Walk.mem_support_iff_exists_getVert.mpr ⟨(n - 1), ⟨hnm, by lia⟩⟩)).elim
    · simp only [Walk.getVert_cons _ _ hn0, Walk.getVert_cons _ _ hm0] at hnm
      have := ihp hp.of_cons (by lia : (n - 1) ≤ p.length)
        (by lia : (m - 1) ≤ p.length) hnm
      lia

Premises used: SimpleGraph.Walk.getVert_zero, Set.mem_setOf_eq, SimpleGraph.Walk.cons, SimpleGraph.Walk.IsPath.nil, SimpleGraph.Walk.length_cons
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
u w : V
i : ℕ
p : G.Walk u w
hp : p.IsPath
h : ¬p.Nil
⊢ i = 0 → p.getVert i = u

Tactic:
simp_all
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
u w : V
i : ℕ
p : G.Walk u w
hp : p.IsPath
h : ¬p.Nil
refine : ∀ (h : p.getVert i = u), i = 0
⊢ p.getVert i = u ↔ i = 0

Tactic:
refine ⟨fun h ↦ ?_, by simp_all⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
u w : V
i : ℕ
p : G.Walk u w
hp : p.IsPath
h_1 : ¬p.Nil
h : p.getVert i = u
pos : ∀ (h' : i ≤ p.length), i = 0
neg : ∀ (h' : ¬i ≤ p.length), i = 0
⊢ i = 0

Tactic:
by_cases h' : i ≤ p.length

Premises used: SimpleGraph.Walk.length
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
u w : V
i : ℕ
p : G.Walk u w
hp : p.IsPath
h_1 : ¬p.Nil
h : p.getVert i = u
h' : i ≤ p.length
⊢ i ≤ p.length

Tactic:
lia
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
u w : V
i : ℕ
p : G.Walk u w
hp : p.IsPath
h_1 : ¬p.Nil
h : p.getVert i = u
h' : i ≤ p.length
⊢ 0 ≤ p.length

Tactic:
lia
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
u w : V
i : ℕ
p : G.Walk u w
hp : p.IsPath
h_1 : ¬p.Nil
h : p.getVert i = u
h' : i ≤ p.length
pos : p.getVert i = p.getVert 0
⊢ i = 0

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

Premises used: SimpleGraph.Walk.IsPath.getVert_injOn
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
u w : V
i : ℕ
p : G.Walk u w
hp : p.IsPath
h_1 : ¬p.Nil
h : p.getVert i = u
h' : i ≤ p.length
⊢ p.getVert i = p.getVert 0

Tactic:
simp [h]
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
u w : V
i : ℕ
p : G.Walk u w
hp : p.IsPath
h_1 : ¬p.Nil
h : p.getVert i = u
h' : ¬i ≤ p.length
⊢ w = u

Tactic:
rw [p.getVert_of_length_le (le_of_not_ge h')] at h

Premises used: SimpleGraph.Walk.getVert_of_length_le, le_of_not_ge
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
u w : V
i : ℕ
p : G.Walk u w
hp : p.IsPath
h_1 : ¬p.Nil
h : p.getVert i = u
h' : ¬i ≤ p.length
h₁ : w = u
⊢ ¬i ≤ p.length

Tactic:
rw [p.getVert_of_length_le (le_of_not_ge h')] at h

Premises used: SimpleGraph.Walk.getVert_of_length_le, le_of_not_ge
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
u w : V
i : ℕ
p : G.Walk u w
hp : p.IsPath
h_1 : ¬p.Nil
h : w = u
h' : ¬i ≤ p.length
neg : ∀ {p : G.Walk w w} (hp : p.IsPath) (h : ¬p.Nil) (h' : ¬i ≤ p.length), i = 0
⊢ i = 0

Tactic:
subst h
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
w : V
i : ℕ
p : G.Walk w w
hp : p.IsPath
h : ¬p.Nil
h' : ¬i ≤ p.length
⊢ i = 0

Tactic:
simp_all
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
u w : V
i : ℕ
p : G.Walk u w
hp : p.IsPath
hi : i ≤ p.length
nil :
  ∀ (hp : IsPath.{u} (V := V) (G := G) (u := u) Walk.nil) (hi : i ≤ length.{u} (V := V) (G := G) (u := u) Walk.nil),
    getVert (G := G) (u := u) Walk.nil i = u ↔ i = 0
cons :
  ∀ {v : V} (h : G.Adj u v) (p : G.Walk v w) (hp : (Walk.cons h p).IsPath) (hi : i ≤ (Walk.cons h p).length),
    (Walk.cons h p).getVert i = u ↔ i = 0
⊢ p.getVert i = u ↔ i = 0

Tactic:
cases p
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
u : V
i : ℕ
hp : IsPath.{u} (V := V) (G := G) (u := u) Walk.nil
hi : i ≤ length.{u} (V := V) (G := G) (u := u) Walk.nil
⊢ getVert (G := G) (u := u) Walk.nil i = u ↔ i = 0

Tactic:
simpa using hi
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
u w : V
i : ℕ
v : V
h : G.Adj u v
p : G.Walk v w
hp : (cons h p).IsPath
hi : i ≤ (cons h p).length
⊢ (cons h p).getVert i = u ↔ i = 0

Tactic:
hp.getVert_eq_start_iff_of_not_nil not_nil_cons

Premises used: SimpleGraph.Walk.not_nil_cons, SimpleGraph.Walk.IsPath.getVert_eq_start_iff_of_not_nil
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
u w : V
i : ℕ
v : V
h : G.Adj u v
p : G.Walk v w
hp : (cons h p).IsPath
hi : i ≤ (cons h p).length
⊢ (cons h p).getVert i = u ↔ i = 0

Tactic:
exact hp.getVert_eq_start_iff_of_not_nil not_nil_cons

Premises used: SimpleGraph.Walk.not_nil_cons, SimpleGraph.Walk.IsPath.getVert_eq_start_iff_of_not_nil
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
u w : V
i : ℕ
p : G.Walk u w
hp : p.IsPath
hi : i ≤ p.length
⊢ p.reverse.length - i ≤ p.reverse.length

Tactic:
lia
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
u w : V
i : ℕ
p : G.Walk u w
hp : p.IsPath
hi : i ≤ p.length
⊢ p.reverse.getVert (p.reverse.length - i) = w ↔ p.reverse.length - i = 0

Tactic:
have := hp.reverse.getVert_eq_start_iff (by lia : p.reverse.length - i ≤ p.reverse.length)
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
u w : V
i : ℕ
p : G.Walk u w
hp : p.IsPath
hi : i ≤ p.length
this : p.reverse.getVert (p.reverse.length - i) = w ↔ p.reverse.length - i = 0
⊢ p.length - (p.length - i) = i

Tactic:
lia
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
u w : V
i : ℕ
p : G.Walk u w
hp : p.IsPath
hi : i ≤ p.length
this : p.reverse.getVert (p.reverse.length - i) = w ↔ p.reverse.length - i = 0
⊢ p.getVert i = w ↔ p.length - i = 0

Tactic:
simp only [length_reverse, getVert_reverse, show p.length - (p.length - i) = i by lia] at this

Premises used: SimpleGraph.Walk.getVert_reverse, SimpleGraph.Walk.length_reverse
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
u w : V
i : ℕ
p : G.Walk u w
hp : p.IsPath
hi : i ≤ p.length
this : p.getVert i = w ↔ p.length - i = 0
rw : p.length - i = 0 ↔ i = p.length
⊢ p.getVert i = w ↔ i = p.length

Tactic:
rw [this]
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
u w : V
i : ℕ
p : G.Walk u w
hp : p.IsPath
hi : i ≤ p.length
this : p.getVert i = w ↔ p.length - i = 0
⊢ p.length - i = 0 ↔ i = p.length

Tactic:
lia
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
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:
⟨?_, fun a => a.getVert_injOn⟩

Premises used: SimpleGraph.Walk.IsPath.getVert_injOn, Iff.intro
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
refine : Set.InjOn p.getVert {i : ℕ | i ≤ p.length} → p.IsPath
⊢ Set.InjOn p.getVert {i : ℕ | i ≤ p.length} ↔ p.IsPath

Tactic:
refine ⟨?_, fun a => a.getVert_injOn⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
u v u_1 : V
⊢ Set.InjOn.{0, u} (β := V) (getVert (G := G) (u := u_1) Walk.nil)
      {i : ℕ | i ≤ length.{u} (V := V) (G := G) (u := u_1) Walk.nil} →
    IsPath.{u} (V := V) (G := G) (u := u_1) Walk.nil

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
u v u_1 v_1 w : V
h : G.Adj u_1 v_1
q : G.Walk v_1 w
ih : Set.InjOn q.getVert {i : ℕ | i ≤ q.length} → q.IsPath
hinj : Set.InjOn (Walk.cons h q).getVert {i : ℕ | i ≤ (Walk.cons h q).length}
cons : q.IsPath ∧ u_1 ∉ q.support
⊢ (Walk.cons h q).IsPath

Tactic:
rw [cons_isPath_iff]

Premises used: SimpleGraph.Walk.cons_isPath_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
u v u_1 v_1 w : V
h : G.Adj u_1 v_1
q : G.Walk v_1 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 + 1 ≤ q.length + 1

Tactic:
lia
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
u v u_1 v_1 w : V
h : G.Adj u_1 v_1
q : G.Walk v_1 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:
lia
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
u v u_1 v_1 w : V
h : G.Adj u_1 v_1
q : G.Walk v_1 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
⊢ (cons h q).getVert (n + 1) = (cons h q).getVert (m + 1)

Tactic:
simpa [getVert_cons] using hnm

Premises used: SimpleGraph.Walk.getVert_cons
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
u v u_1 v_1 w : V
h : G.Adj u_1 v_1
q : G.Walk v_1 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 + 1 = m + 1

Tactic:
have := hinj
        (by rw [length_cons]; lia : n + 1 ≤ (q.cons h).length)
        (by rw [length_cons]; lia : m + 1 ≤ (q.cons h).length)
        (by simpa [getVert_cons] using hnm)
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
u v u_1 v_1 w : V
h : G.Adj u_1 v_1
q : G.Walk v_1 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:
lia
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
u v u_1 v_1 w : V
h : G.Adj u_1 v_1
q : G.Walk v_1 w
ih : Set.InjOn q.getVert {i : ℕ | i ≤ q.length} → q.IsPath
hinj : Set.InjOn (Walk.cons h q).getVert {i : ℕ | i ≤ (Walk.cons h q).length}
cons : ∀ (h' : u_1 ∈ q.support), False
⊢ q.IsPath ∧ u_1 ∉ 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]; lia : n + 1 ≤ (q.cons h).length)
        (by rw [length_cons]; lia : m + 1 ≤ (q.cons h).length)
        (by simpa [getVert_cons] using hnm)
      lia), fun h' => ?_⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
u v u_1 v_1 w : V
h : G.Adj u_1 v_1
q : G.Walk v_1 w
ih : Set.InjOn q.getVert {i : ℕ | i ≤ q.length} → q.IsPath
hinj : Set.InjOn (Walk.cons h q).getVert {i : ℕ | i ≤ (Walk.cons h q).length}
h' : u_1 ∈ q.support
cons : ∀ (n : ℕ) (hn : q.getVert n = u_1) (hnl : n ≤ q.length), False
⊢ False

Tactic:
obtain ⟨n, ⟨hn, hnl⟩⟩ := mem_support_iff_exists_getVert.mp h'

Premises used: Iff.mp, SimpleGraph.Walk.mem_support_iff_exists_getVert
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
u v u_1 v_1 w : V
h : G.Adj u_1 v_1
q : G.Walk v_1 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_1 ∈ q.support
n : ℕ
hn : q.getVert n = u_1
hnl : n ≤ q.length
⊢ n + 1 ≤ q.length + 1

Tactic:
lia
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
u v u_1 v_1 w : V
h : G.Adj u_1 v_1
q : G.Walk v_1 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_1 ∈ q.support
n : ℕ
hn : q.getVert n = u_1
hnl : n ≤ q.length
⊢ 0 ≤ (cons h q).length

Tactic:
lia