awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
v : V
p : G.Walk v v
hp : p.IsCycle
⊢ p.IsTrail

Tactic:
have ⟨⟨hp, hp'⟩, _⟩ := hp
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
v : V
p : G.Walk v v
hp : p.IsCycle
hp₁ : p.IsTrail
⊢ p ≠ nil

Tactic:
have ⟨⟨hp, hp'⟩, _⟩ := hp
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
v : V
p : G.Walk v v
hp : p.IsCycle
hp₁ : p.IsTrail
hp' : p ≠ nil
⊢ p.support.tail.Nodup

Tactic:
have ⟨⟨hp, hp'⟩, _⟩ := hp
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
v : V
p : G.Walk v v
hp_1 : IsCycle.{u} (V := V) (G := G) (u := v) nil
hp : IsTrail.{u} (V := V) (G := G) (u := v) nil
hp' : Ne.{u + 1} (α := G.Walk v v) nil nil
support_nodup : List.Nodup.{u} (α := V) (List.tail (support (G := G) (u := v) nil))
⊢ 3 ≤ length.{u} (V := V) (G := G) (u := v) nil

Tactic:
simp at hp'
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
v : V
p : G.Walk v v
h : G.Adj v v
hp_1 : (cons h nil).IsCycle
hp : (cons h nil).IsTrail
hp' : cons h nil ≠ nil
support_nodup : (cons h nil).support.tail.Nodup
⊢ 3 ≤ (cons h nil).length

Tactic:
simp at h
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
v : V
p : G.Walk v v
v_1 : V
h : G.Adj v v_1
h_1 : G.Adj v_1 v
hp_1 : (cons h (cons h_1 nil)).IsCycle
hp : (cons h (cons h_1 nil)).IsTrail
hp' : cons h (cons h_1 nil) ≠ nil
support_nodup : (cons h (cons h_1 nil)).support.tail.Nodup
⊢ 3 ≤ (cons h (cons h_1 nil)).length

Tactic:
simp at hp
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
v : V
p : G.Walk v v
v_1 : V
h : G.Adj v v_1
v_2 : V
h_1 : G.Adj v_1 v_2
v_3 : V
h_2 : G.Adj v_2 v_3
p_1 : G.Walk v_3 v
hp_1 : (cons h (cons h_1 (cons h_2 p_1))).IsCycle
hp : (cons h (cons h_1 (cons h_2 p_1))).IsTrail
hp' : cons h (cons h_1 (cons h_2 p_1)) ≠ nil
support_nodup : (cons h (cons h_1 (cons h_2 p_1))).support.tail.Nodup
⊢ 3 ≤ p_1.length + 1 + 1 + 1

Tactic:
lia
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
v : V
p : G.Walk v v
hp_1 : p.IsCycle
hp : p.IsTrail
hp' : p ≠ nil
support_nodup : p.support.tail.Nodup
⊢ 3 ≤ p.length

Tactic:
match p with
  | .nil => simp at hp'
  | .cons h .nil => simp at h
  | .cons _ (.cons _ .nil) => simp at hp
  | .cons _ (.cons _ (.cons _ _)) => simp_rw [SimpleGraph.Walk.length_cons]; lia
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
h : G.Adj v u
hc : (cons h p).IsCycle
⊢ 3 ≤ p.length + 1

Tactic:
have := Walk.length_cons _ _ ▸ Walk.IsCycle.three_le_length hc
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
h : G.Adj v u
hc : (cons h p).IsCycle
this : 3 ≤ p.length + 1
rw : 0 < p.length
⊢ ¬p.Nil

Tactic:
rw [Walk.not_nil_iff_lt_length]

Premises used: SimpleGraph.Walk.not_nil_iff_lt_length
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
h : G.Adj v u
hc : (cons h p).IsCycle
this : 3 ≤ p.length + 1
⊢ 0 < p.length

Tactic:
lia
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk v u
h : G.Adj u v
simp : (s(u, v) ∉ p.edges ∧ p.edges.Nodup) ∧ cons h p ≠ nil ∧ p.support.Nodup ↔ p.support.Nodup ∧ s(u, v) ∉ p.edges
⊢ (cons h p).IsCycle ↔ p.IsPath ∧ s(u, v) ∉ p.edges

Tactic:
simp only [Walk.isCycle_def, Walk.isPath_def, Walk.isTrail_def, edges_cons, List.nodup_cons,
    support_cons, List.tail_cons]

Premises used: SimpleGraph.Walk.isCycle_def, SimpleGraph.Walk.support_cons, SimpleGraph.Walk.isPath_def, SimpleGraph.Walk.isTrail_def, List.tail_cons, List.nodup_cons, SimpleGraph.Walk.edges_cons
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk v u
h : G.Adj u v
⊢ p.support.Nodup → p.edges.Nodup

Tactic:
have : p.support.Nodup → p.edges.Nodup := edges_nodup_of_support_nodup
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk v u
h : G.Adj u v
this : p.support.Nodup → p.edges.Nodup
inl :
  ∀ (this : ¬p.support.Nodup),
    (s(u, v) ∉ p.edges ∧ p.edges.Nodup) ∧ cons h p ≠ nil ∧ p.support.Nodup ↔ p.support.Nodup ∧ s(u, v) ∉ p.edges
inr :
  ∀ (this : p.edges.Nodup),
    (s(u, v) ∉ p.edges ∧ p.edges.Nodup) ∧ cons h p ≠ nil ∧ p.support.Nodup ↔ p.support.Nodup ∧ s(u, v) ∉ p.edges
inl₁ :
  ∀ (this : ¬p.support.Nodup),
    (s(u, v) ∉ p.edges ∧ p.edges.Nodup) ∧ cons h p ≠ nil ∧ p.support.Nodup ↔ p.support.Nodup ∧ s(u, v) ∉ p.edges
inr₁ :
  ∀ (this : p.edges.Nodup),
    (s(u, v) ∉ p.edges ∧ p.edges.Nodup) ∧ cons h p ≠ nil ∧ p.support.Nodup ↔ p.support.Nodup ∧ s(u, v) ∉ p.edges
inl₂ :
  ∀ (this : ¬p.support.Nodup),
    (s(u, v) ∉ p.edges ∧ p.edges.Nodup) ∧ cons h p ≠ nil ∧ p.support.Nodup → p.support.Nodup ∧ s(u, v) ∉ p.edges
inl₃ :
  ∀ (this : ¬p.support.Nodup),
    p.support.Nodup ∧ s(u, v) ∉ p.edges → (s(u, v) ∉ p.edges ∧ p.edges.Nodup) ∧ cons h p ≠ nil ∧ p.support.Nodup
inr₂ :
  ∀ (this : p.edges.Nodup),
    (s(u, v) ∉ p.edges ∧ p.edges.Nodup) ∧ cons h p ≠ nil ∧ p.support.Nodup → p.support.Nodup ∧ s(u, v) ∉ p.edges
inr₃ :
  ∀ (this : p.edges.Nodup),
    p.support.Nodup ∧ s(u, v) ∉ p.edges → (s(u, v) ∉ p.edges ∧ p.edges.Nodup) ∧ cons h p ≠ nil ∧ p.support.Nodup
inl₄ :
  ∀ (this : ¬p.support.Nodup),
    s(u, v) ∉ p.edges → p.edges.Nodup → cons h p ≠ nil → p.support.Nodup → p.support.Nodup ∧ s(u, v) ∉ p.edges
inl₅ :
  ∀ (this : ¬p.support.Nodup),
    p.support.Nodup → s(u, v) ∉ p.edges → (s(u, v) ∉ p.edges ∧ p.edges.Nodup) ∧ cons h p ≠ nil ∧ p.support.Nodup
inr₄ inr₅ :
  ∀ (this : p.edges.Nodup),
    s(u, v) ∉ p.edges → p.edges.Nodup → cons h p ≠ nil → p.support.Nodup → p.support.Nodup ∧ s(u, v) ∉ p.edges
inr₆ : ∀ (this : p.edges.Nodup), s(u, v) ∉ p.edges → p.edges.Nodup → cons h p ≠ nil → p.support.Nodup → p.support.Nodup
inr₇ :
  ∀ (this : p.edges.Nodup), s(u, v) ∉ p.edges → p.edges.Nodup → cons h p ≠ nil → p.support.Nodup → s(u, v) ∉ p.edges
inr₈ inr₉ :
  ∀ (this : p.edges.Nodup),
    p.support.Nodup → s(u, v) ∉ p.edges → (s(u, v) ∉ p.edges ∧ p.edges.Nodup) ∧ cons h p ≠ nil ∧ p.support.Nodup
inr₁₀ : ∀ (this : p.edges.Nodup), p.support.Nodup → s(u, v) ∉ p.edges → s(u, v) ∉ p.edges
inr₁₁ : ∀ (this : p.edges.Nodup), p.support.Nodup → s(u, v) ∉ p.edges → p.edges.Nodup
inr₁₂ : ∀ (this : p.edges.Nodup), p.support.Nodup → s(u, v) ∉ p.edges → cons h p ≠ nil
inr₁₃ : ∀ (this : p.edges.Nodup), p.support.Nodup → s(u, v) ∉ p.edges → p.support.Nodup
inr₁₄ : ∀ (this : p.edges.Nodup), p.support.Nodup → s(u, v) ∉ p.edges → cons h p = nil → False
⊢ (s(u, v) ∉ p.edges ∧ p.edges.Nodup) ∧ cons h p ≠ nil ∧ p.support.Nodup ↔ p.support.Nodup ∧ s(u, v) ∉ p.edges

Tactic:
tauto
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
u : V
p : G.Walk u u
h : p.IsCycle
simp : ∀ (h : p.IsTrail ∧ p ≠ nil ∧ p.support.tail.Nodup), p.reverse.IsTrail ∧ p.reverse ≠ nil ∧ p.support.tail.Nodup
⊢ p.reverse.IsCycle

Tactic:
simp only [Walk.isCycle_def, nodup_tail_support_reverse] at h ⊢

Premises used: SimpleGraph.Walk.isCycle_def, SimpleGraph.Walk.nodup_tail_support_reverse
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
u : V
p : G.Walk u u
h : p.IsTrail ∧ p ≠ nil ∧ p.support.tail.Nodup
h' : p.reverse = nil
⊢ p = nil

Tactic:
simp_all [← Walk.length_eq_zero_iff]

Premises used: SimpleGraph.Walk.length_eq_zero_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
u : V
p : G.Walk u u
h : p.IsTrail ∧ p ≠ nil ∧ p.support.tail.Nodup
⊢ p.reverse.IsTrail ∧ p.reverse ≠ nil ∧ p.support.tail.Nodup

Tactic:
exact ⟨h.1.reverse, fun h' ↦ h.2.1 (by simp_all [← Walk.length_eq_zero_iff]), h.2.2⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
u : V
p : G.Walk u u
h : p.reverse.IsCycle
⊢ p.IsCycle

Tactic:
simpa using h.reverse

Premises used: SimpleGraph.Walk.IsCycle.reverse
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
q : G.Walk v u
h : ¬p.Nil
hcyc : (p.append q).IsCycle
⊢ (p.append q).support.tail.Nodup

Tactic:
have := hcyc.2
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
q : G.Walk v u
h : ¬p.Nil
hcyc : (p.append q).IsCycle
this : (p.append q).support.tail.Nodup
⊢ p.support.tail.Nodup ∧ q.support.tail.Nodup ∧ p.support.tail.Disjoint q.support.tail

Tactic:
rw [tail_support_append, List.nodup_append'] at this

Premises used: List.nodup_append', SimpleGraph.Walk.tail_support_append
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
q : G.Walk v u
h : ¬p.Nil
hcyc : (p.append q).IsCycle
this : p.support.tail.Nodup ∧ q.support.tail.Nodup ∧ p.support.tail.Disjoint q.support.tail
rw : v ∉ q.support.tail ∧ q.support.tail.Nodup
⊢ q.IsPath

Tactic:
rw [isPath_def, ← cons_tail_support, List.nodup_cons]

Premises used: SimpleGraph.Walk.isPath_def, SimpleGraph.Walk.cons_tail_support, List.nodup_cons
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
q : G.Walk v u
h : ¬p.Nil
hcyc : (p.append q).IsCycle
this : p.support.tail.Nodup ∧ q.support.tail.Nodup ∧ p.support.tail.Disjoint q.support.tail
⊢ v ∉ q.support.tail ∧ q.support.tail.Nodup

Tactic:
⟨this.2.2 (p.end_mem_tail_support h), this.2.1⟩

Premises used: SimpleGraph.Walk.end_mem_tail_support, And.right, And.left, And.intro
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
q : G.Walk v u
h : ¬p.Nil
hcyc : (p.append q).IsCycle
this : p.support.tail.Nodup ∧ q.support.tail.Nodup ∧ p.support.tail.Disjoint q.support.tail
⊢ v ∉ q.support.tail ∧ q.support.tail.Nodup

Tactic:
exact ⟨this.2.2 (p.end_mem_tail_support h), this.2.1⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
q : G.Walk v u
h : ¬q.Nil
hcyc : (p.append q).IsCycle
⊢ ¬q.reverse.Nil

Tactic:
simpa
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
u : V
p : G.Walk u u
h : p.IsCycle
⊢ p.tail.IsPath

Tactic:
IsPath.mk' <| p.support_tail_of_not_nil h.not_nil ▸ h.support_nodup

Premises used: Eq.rec, SimpleGraph.Walk.support_tail_of_not_nil, SimpleGraph.Walk.IsCycle.support_nodup, Eq.symm, SimpleGraph.Walk.IsPath.mk', SimpleGraph.Walk.IsCycle.not_nil
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
u : V
hp : IsPath.{u} (V := V) (G := G) (u := u) Walk.nil
⊢ IsPath.{u} (V := V) (G := G) (u := snd (G := G) (u := u) Walk.nil) (Walk.tail Walk.nil)

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
u v v_1 : V
hadj : G.Adj u v_1
p : G.Walk v_1 v
hp : (cons hadj p).IsPath
⊢ (cons hadj p).tail.IsPath

Tactic:
simp_all [Walk.isPath_def]

Premises used: SimpleGraph.Walk.isPath_def
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
hp : p.IsPath
nil :
  ∀ (hp : IsPath.{u} (V := V) (G := G) (u := u) Walk.nil),
    IsPath.{u} (V := V) (G := G) (u := snd (G := G) (u := u) Walk.nil) (Walk.tail Walk.nil)
cons :
  ∀ {v_1 : V} (hadj : G.Adj u v_1) (p : G.Walk v_1 v) (hp : (Walk.cons hadj p).IsPath), (Walk.cons hadj p).tail.IsPath
⊢ p.tail.IsPath

Tactic:
cases p with
  | nil => simp
  | cons hadj p =>
    simp_all [Walk.isPath_def]

Premises used: SimpleGraph.Walk.isPath_def, SimpleGraph.Walk.cons, SimpleGraph.Walk.IsPath.nil
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
N : Nonempty V
inst : Finite.{u + 1} (↑G.edgeSet : Type u)
have :
  ∀ (this : Fintype (↑G.edgeSet : Type u)),
    ∃ (u : V) (v : V) (p : G.Walk u v) (_ : p.IsTrail),
      ∀ (u' v' : V) (p' : G.Walk u' v'), p'.IsTrail → p'.length ≤ p.length
⊢ ∃ (u : V) (v : V) (p : G.Walk u v) (_ : p.IsTrail),
    ∀ (u' v' : V) (p' : G.Walk u' v'), p'.IsTrail → p'.length ≤ p.length

Tactic:
have := Fintype.ofFinite G.edgeSet
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
N : Nonempty V
inst : Finite.{u + 1} (↑G.edgeSet : Type u)
this : Fintype (↑G.edgeSet : Type u)
s : Set ℕ := {n : ℕ | ∃ (u : V) (v : V) (p : G.Walk u v), p.IsTrail ∧ p.length = n}
⊢ s.Finite

Tactic:
have : s.Finite := Set.Finite.subset (Set.finite_le_nat G.edgeFinset.card)
    fun n ⟨_, _, _, hp, hn⟩ ↦ hn ▸ hp.length_le_card_edgeFinset
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
N : Nonempty V
inst : Finite.{u + 1} (↑G.edgeSet : Type u)
this_1 : Fintype (↑G.edgeSet : Type u)
s : Set ℕ := {n : ℕ | ∃ (u : V) (v : V) (p : G.Walk u v), p.IsTrail ∧ p.length = n}
this : s.Finite
obtain :
  ∀ (x : V),
    ∃ (u : V) (v : V) (p : G.Walk u v) (_ : p.IsTrail),
      ∀ (u' v' : V) (p' : G.Walk u' v'), p'.IsTrail → p'.length ≤ p.length
⊢ ∃ (u : V) (v : V) (p : G.Walk u v) (_ : p.IsTrail),
    ∀ (u' v' : V) (p' : G.Walk u' v'), p'.IsTrail → p'.length ≤ p.length

Tactic:
obtain ⟨x⟩ := N
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
inst : Finite.{u + 1} (↑G.edgeSet : Type u)
this_1 : Fintype (↑G.edgeSet : Type u)
s : Set ℕ := {n : ℕ | ∃ (u : V) (v : V) (p : G.Walk u v), p.IsTrail ∧ p.length = n}
this : s.Finite
x : V
⊢ IsTrail.{u} (V := V) (G := G) (u := x) nil ∧ length.{u} (V := V) (G := G) (u := x) nil = 0

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
inst : Finite.{u + 1} (↑G.edgeSet : Type u)
this_1 : Fintype (↑G.edgeSet : Type u)
s : Set ℕ := {n : ℕ | ∃ (u : V) (v : V) (p : G.Walk u v), p.IsTrail ∧ p.length = n}
this : s.Finite
x : V
obtain :
  ∀ (w : ℕ) (hn : ∀ ⦃y : ℕ⦄, (fun (x : ℕ) ↦ x ∈ s) y → w ≤ y → y ≤ w) (u v : V) (p : G.Walk u v) (hp : p.IsTrail),
    p.length = w →
      ∃ (u : V) (v : V) (p : G.Walk u v) (_ : p.IsTrail),
        ∀ (u' v' : V) (p' : G.Walk u' v'), p'.IsTrail → p'.length ≤ p.length
⊢ ∃ (u : V) (v : V) (p : G.Walk u v) (_ : p.IsTrail),
    ∀ (u' v' : V) (p' : G.Walk u' v'), p'.IsTrail → p'.length ≤ p.length

Tactic:
obtain ⟨_, ⟨⟨u, v, p, hp, _⟩, hn⟩⟩ := this.exists_maximal ⟨0, ⟨x, x, Walk.nil, by simp⟩⟩

Premises used: SimpleGraph.Walk.nil, Set.Finite.exists_maximal, Exists.intro, OfNat.ofNat
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
inst : Finite.{u + 1} (↑G.edgeSet : Type u)
this_1 : Fintype (↑G.edgeSet : Type u)
s : Set ℕ := {n : ℕ | ∃ (u : V) (v : V) (p : G.Walk u v), p.IsTrail ∧ p.length = n}
this : s.Finite
x : V
w : ℕ
hn : ∀ ⦃y : ℕ⦄, (fun (x : ℕ) ↦ x ∈ s) y → w ≤ y → y ≤ w
u v : V
p : G.Walk u v
hp : p.IsTrail
right : p.length = w
⊢ ∃ (u : V) (v : V) (p : G.Walk u v) (_ : p.IsTrail),
    ∀ (u' v' : V) (p' : G.Walk u' v'), p'.IsTrail → p'.length ≤ p.length

Tactic:
⟨u, v, p, hp, fun u' v' p' hp' ↦ ?_⟩

Premises used: Exists.intro
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
inst : Finite.{u + 1} (↑G.edgeSet : Type u)
this_1 : Fintype (↑G.edgeSet : Type u)
s : Set ℕ := {n : ℕ | ∃ (u : V) (v : V) (p : G.Walk u v), p.IsTrail ∧ p.length = n}
this : s.Finite
x : V
w : ℕ
hn : ∀ ⦃y : ℕ⦄, (fun (x : ℕ) ↦ x ∈ s) y → w ≤ y → y ≤ w
u v : V
p : G.Walk u v
hp : p.IsTrail
right : p.length = w
refine : ∀ (u' v' : V) (p' : G.Walk u' v') (hp' : p'.IsTrail), p'.length ≤ p.length
⊢ ∃ (u : V) (v : V) (p : G.Walk u v) (_ : p.IsTrail),
    ∀ (u' v' : V) (p' : G.Walk u' v'), p'.IsTrail → p'.length ≤ p.length

Tactic:
refine ⟨u, v, p, hp, fun u' v' p' hp' ↦ ?_⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
inst : Finite.{u + 1} (↑G.edgeSet : Type u)
this_1 : Fintype (↑G.edgeSet : Type u)
s : Set ℕ := {n : ℕ | ∃ (u : V) (v : V) (p : G.Walk u v), p.IsTrail ∧ p.length = n}
this : s.Finite
x : V
w : ℕ
hn : ∀ ⦃y : ℕ⦄, (fun (x : ℕ) ↦ x ∈ s) y → w ≤ y → y ≤ w
u v : V
p : G.Walk u v
hp : p.IsTrail
right : p.length = w
u' v' : V
p' : G.Walk u' v'
hp' : p'.IsTrail
⊢ w ≤ p'.length → p'.length ≤ w

Tactic:
have := hn ⟨u', v', p', hp', Eq.refl p'.length⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
inst : Finite.{u + 1} (↑G.edgeSet : Type u)
this_1 : Fintype (↑G.edgeSet : Type u)
s : Set ℕ := {n : ℕ | ∃ (u : V) (v : V) (p : G.Walk u v), p.IsTrail ∧ p.length = n}
this_2 : s.Finite
x : V
w : ℕ
hn : ∀ ⦃y : ℕ⦄, (fun (x : ℕ) ↦ x ∈ s) y → w ≤ y → y ≤ w
u v : V
p : G.Walk u v
hp : p.IsTrail
right : p.length = w
u' v' : V
p' : G.Walk u' v'
hp' : p'.IsTrail
this : w ≤ p'.length → p'.length ≤ w
⊢ p'.length ≤ p.length

Tactic:
lia
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
N : Nonempty V
inst : Finite.{u + 1} (↑G.edgeSet : Type u)
have :
  ∀ (this : Fintype (↑G.edgeSet : Type u)),
    ∃ (u : V) (v : V) (p : G.Walk u v) (_ : p.IsPath),
      ∀ (u' v' : V) (p' : G.Walk u' v'), p'.IsPath → p'.length ≤ p.length
⊢ ∃ (u : V) (v : V) (p : G.Walk u v) (_ : p.IsPath), ∀ (u' v' : V) (p' : G.Walk u' v'), p'.IsPath → p'.length ≤ p.length

Tactic:
have := Fintype.ofFinite G.edgeSet
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
N : Nonempty V
inst : Finite.{u + 1} (↑G.edgeSet : Type u)
this : Fintype (↑G.edgeSet : Type u)
s : Set ℕ := {n : ℕ | ∃ (u : V) (v : V) (p : G.Walk u v), p.IsPath ∧ p.length = n}
⊢ s.Finite

Tactic:
have : s.Finite := Set.Finite.subset (Set.finite_le_nat G.edgeFinset.card)
    fun n ⟨_, _, _, hp, hn⟩ ↦ hn ▸ hp.isTrail.length_le_card_edgeFinset
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
N : Nonempty V
inst : Finite.{u + 1} (↑G.edgeSet : Type u)
this_1 : Fintype (↑G.edgeSet : Type u)
s : Set ℕ := {n : ℕ | ∃ (u : V) (v : V) (p : G.Walk u v), p.IsPath ∧ p.length = n}
this : s.Finite
obtain :
  ∀ (x : V),
    ∃ (u : V) (v : V) (p : G.Walk u v) (_ : p.IsPath),
      ∀ (u' v' : V) (p' : G.Walk u' v'), p'.IsPath → p'.length ≤ p.length
⊢ ∃ (u : V) (v : V) (p : G.Walk u v) (_ : p.IsPath), ∀ (u' v' : V) (p' : G.Walk u' v'), p'.IsPath → p'.length ≤ p.length

Tactic:
obtain ⟨x⟩ := N
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
inst : Finite.{u + 1} (↑G.edgeSet : Type u)
this_1 : Fintype (↑G.edgeSet : Type u)
s : Set ℕ := {n : ℕ | ∃ (u : V) (v : V) (p : G.Walk u v), p.IsPath ∧ p.length = n}
this : s.Finite
x : V
⊢ IsPath.{u} (V := V) (G := G) (u := x) nil ∧ length.{u} (V := V) (G := G) (u := x) nil = 0

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
inst : Finite.{u + 1} (↑G.edgeSet : Type u)
this_1 : Fintype (↑G.edgeSet : Type u)
s : Set ℕ := {n : ℕ | ∃ (u : V) (v : V) (p : G.Walk u v), p.IsPath ∧ p.length = n}
this : s.Finite
x : V
obtain :
  ∀ (w : ℕ) (hn : ∀ ⦃y : ℕ⦄, (fun (x : ℕ) ↦ x ∈ s) y → w ≤ y → y ≤ w) (u v : V) (p : G.Walk u v) (hp : p.IsPath),
    p.length = w →
      ∃ (u : V) (v : V) (p : G.Walk u v) (_ : p.IsPath),
        ∀ (u' v' : V) (p' : G.Walk u' v'), p'.IsPath → p'.length ≤ p.length
⊢ ∃ (u : V) (v : V) (p : G.Walk u v) (_ : p.IsPath), ∀ (u' v' : V) (p' : G.Walk u' v'), p'.IsPath → p'.length ≤ p.length

Tactic:
obtain ⟨_, ⟨⟨u, v, p, hp, _⟩, hn⟩⟩ := this.exists_maximal ⟨0, ⟨x, x, Walk.nil, by simp⟩⟩

Premises used: SimpleGraph.Walk.nil, Set.Finite.exists_maximal, Exists.intro, OfNat.ofNat
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
inst : Finite.{u + 1} (↑G.edgeSet : Type u)
this_1 : Fintype (↑G.edgeSet : Type u)
s : Set ℕ := {n : ℕ | ∃ (u : V) (v : V) (p : G.Walk u v), p.IsPath ∧ p.length = n}
this : s.Finite
x : V
w : ℕ
hn : ∀ ⦃y : ℕ⦄, (fun (x : ℕ) ↦ x ∈ s) y → w ≤ y → y ≤ w
u v : V
p : G.Walk u v
hp : p.IsPath
right : p.length = w
⊢ ∃ (u : V) (v : V) (p : G.Walk u v) (_ : p.IsPath), ∀ (u' v' : V) (p' : G.Walk u' v'), p'.IsPath → p'.length ≤ p.length

Tactic:
⟨u, v, p, hp, fun u' v' p' hp' ↦ ?_⟩

Premises used: Exists.intro
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
inst : Finite.{u + 1} (↑G.edgeSet : Type u)
this_1 : Fintype (↑G.edgeSet : Type u)
s : Set ℕ := {n : ℕ | ∃ (u : V) (v : V) (p : G.Walk u v), p.IsPath ∧ p.length = n}
this : s.Finite
x : V
w : ℕ
hn : ∀ ⦃y : ℕ⦄, (fun (x : ℕ) ↦ x ∈ s) y → w ≤ y → y ≤ w
u v : V
p : G.Walk u v
hp : p.IsPath
right : p.length = w
refine : ∀ (u' v' : V) (p' : G.Walk u' v') (hp' : p'.IsPath), p'.length ≤ p.length
⊢ ∃ (u : V) (v : V) (p : G.Walk u v) (_ : p.IsPath), ∀ (u' v' : V) (p' : G.Walk u' v'), p'.IsPath → p'.length ≤ p.length

Tactic:
refine ⟨u, v, p, hp, fun u' v' p' hp' ↦ ?_⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
inst : Finite.{u + 1} (↑G.edgeSet : Type u)
this_1 : Fintype (↑G.edgeSet : Type u)
s : Set ℕ := {n : ℕ | ∃ (u : V) (v : V) (p : G.Walk u v), p.IsPath ∧ p.length = n}
this : s.Finite
x : V
w : ℕ
hn : ∀ ⦃y : ℕ⦄, (fun (x : ℕ) ↦ x ∈ s) y → w ≤ y → y ≤ w
u v : V
p : G.Walk u v
hp : p.IsPath
right : p.length = w
u' v' : V
p' : G.Walk u' v'
hp' : p'.IsPath
⊢ w ≤ p'.length → p'.length ≤ w

Tactic:
have := hn ⟨u', v', p', hp', Eq.refl p'.length⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
inst : Finite.{u + 1} (↑G.edgeSet : Type u)
this_1 : Fintype (↑G.edgeSet : Type u)
s : Set ℕ := {n : ℕ | ∃ (u : V) (v : V) (p : G.Walk u v), p.IsPath ∧ p.length = n}
this_2 : s.Finite
x : V
w : ℕ
hn : ∀ ⦃y : ℕ⦄, (fun (x : ℕ) ↦ x ∈ s) y → w ≤ y → y ≤ w
u v : V
p : G.Walk u v
hp : p.IsPath
right : p.length = w
u' v' : V
p' : G.Walk u' v'
hp' : p'.IsPath
this : w ≤ p'.length → p'.length ≤ w
⊢ p'.length ≤ p.length

Tactic:
lia
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
u_1 u' v_1 w : V
p_1 : G.Walk u_1 v_1
f : G →g G'
inst : DecidableEq V
u v : V
p : G.Walk u v
rw : Decidable p.support.Nodup
⊢ Decidable p.IsPath

Tactic:
rw [isPath_def]

Premises used: SimpleGraph.Walk.isPath_def
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
u_1 u' v_1 w : V
p_1 : G.Walk u_1 v_1
f : G →g G'
inst : DecidableEq V
u v : V
p : G.Walk u v
⊢ Decidable p.support.Nodup

Tactic:
infer_instance
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
inst : Fintype V
u v : V
p : G.Walk u v
hp : p.IsPath
rw : p.support.length ≤ Fintype.card V
⊢ p.length < Fintype.card V

Tactic:
rw [Nat.lt_iff_add_one_le, ← length_support]

Premises used: SimpleGraph.Walk.length_support, Nat.lt_iff_add_one_le
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
inst : Fintype V
u v : V
p : G.Walk u v
hp : p.IsPath
⊢ p.support.length ≤ Fintype.card V

Tactic:
hp.support_nodup.length_le_card

Premises used: List.Nodup.length_le_card, SimpleGraph.Walk.IsPath.support_nodup
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
inst : Fintype V
u v : V
p : G.Walk u v
hp : p.IsPath
⊢ p.support.length ≤ Fintype.card V

Tactic:
exact hp.support_nodup.length_le_card

Premises used: List.Nodup.length_le_card, SimpleGraph.Walk.IsPath.support_nodup
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
u v u_1 : V
hp : IsPath.{u} (V := V) (G := G) (u := u_1) Walk.nil
n : ℕ
hn : Membership.mem (γ := Set ℕ) {i : ℕ | i ≤ length.{u} (V := V) (G := G) (u := u_1) Walk.nil} n
m : ℕ
hm : Membership.mem (γ := Set ℕ) {i : ℕ | i ≤ length.{u} (V := V) (G := G) (u := u_1) Walk.nil} m
hnm : Eq.{u + 1} (α := V) (getVert (G := G) (u := u_1) Walk.nil n) (getVert (G := G) (u := u_1) Walk.nil m)
⊢ n = m

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
hnm : (cons h p).getVert n = (cons h p).getVert m
pos : ∀ (hn0 : n = 0), n = m
neg : ∀ (hn0 : ¬n = 0), n = m
⊢ n = m

Tactic:
by_cases hn0 : n = 0