awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
u : V
i : ℕ
p : G.Walk u u
hpc : p.IsCycle
h : i ≤ p.length
h' : p.getVert (i - 1) = p.getVert (i + 1)
hl : 3 ≤ p.length
hi' : i ≥ p.length - 1
h'₁ : i - 1 = 0 ∨ i - 1 = p.length
⊢ 3 ≤ p.length

Tactic:
rw [p.getVert_of_length_le (by lia : p.length ≤ i + 1),
      hpc.getVert_endpoint_iff (by lia)] at h'

Premises used: SimpleGraph.Walk.getVert_of_length_le, SimpleGraph.Walk.IsCycle.getVert_endpoint_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
u : V
i : ℕ
p : G.Walk u u
hpc : p.IsCycle
h : i ≤ p.length
h' : p.getVert (i - 1) = p.getVert (i + 1)
hl : 3 ≤ p.length
hi' : i ≥ p.length - 1
h'₁ : i - 1 = 0 ∨ i - 1 = p.length
hl₁ : 3 ≤ p.length
⊢ i ≥ p.length - 1

Tactic:
rw [p.getVert_of_length_le (by lia : p.length ≤ i + 1),
      hpc.getVert_endpoint_iff (by lia)] at h'

Premises used: SimpleGraph.Walk.getVert_of_length_le, SimpleGraph.Walk.IsCycle.getVert_endpoint_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
u : V
i : ℕ
p : G.Walk u u
hpc : p.IsCycle
h : i ≤ p.length
h' : i - 1 = 0 ∨ i - 1 = p.length
hl : 3 ≤ p.length
hi' : i ≥ p.length - 1
⊢ False

Tactic:
lia
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
u : V
i : ℕ
p : G.Walk u u
hpc : p.IsCycle
h : i ≤ p.length
h' : p.getVert (i - 1) = p.getVert (i + 1)
hl : 3 ≤ p.length
hi' : ¬i ≥ p.length - 1
simp : i ≤ p.length - 1 + 1
⊢ Membership.mem (γ := Set ℕ) {i : ℕ | i ≤ p.length - 1} (i - 1)

Tactic:
simp only [Set.mem_setOf_eq, Nat.sub_le_iff_le_add]

Premises used: Nat.sub_le_iff_le_add, Set.mem_setOf_eq
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
u : V
i : ℕ
p : G.Walk u u
hpc : p.IsCycle
h : i ≤ p.length
h' : p.getVert (i - 1) = p.getVert (i + 1)
hl : 3 ≤ p.length
hi' : ¬i ≥ p.length - 1
⊢ i ≤ p.length - 1 + 1

Tactic:
lia
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
u : V
i : ℕ
p : G.Walk u u
hpc : p.IsCycle
h : i ≤ p.length
h' : p.getVert (i - 1) = p.getVert (i + 1)
hl : 3 ≤ p.length
hi' : ¬i ≥ p.length - 1
⊢ i + 1 ≤ p.length - 1

Tactic:
lia
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
u : V
i : ℕ
p : G.Walk u u
hpc : p.IsCycle
h : i ≤ p.length
h' : p.getVert (i - 1) = p.getVert (i + 1)
hl : 3 ≤ p.length
hi' : ¬i ≥ p.length - 1
⊢ i - 1 = i + 1

Tactic:
have := hpc.getVert_injOn' (by simp only [Set.mem_setOf_eq, Nat.sub_le_iff_le_add]; lia)
    (by simp only [Set.mem_setOf_eq]; lia) h'
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
u : V
i : ℕ
p : G.Walk u u
hpc : p.IsCycle
h : i ≤ p.length
h' : p.getVert (i - 1) = p.getVert (i + 1)
hl : 3 ≤ p.length
hi' : ¬i ≥ p.length - 1
this : i - 1 = i + 1
⊢ False

Tactic:
lia
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
u : V
p : G.Walk u u
⊢ p.IsCycle ↔ p.tail.IsPath ∧ 3 ≤ p.length

Tactic:
⟨fun h ↦ ⟨h.isPath_tail, h.three_le_length⟩, fun ⟨h₁, h₂⟩ ↦ ?_⟩

Premises used: SimpleGraph.Walk.IsCycle, _private.0.SimpleGraph.Walk.isCycle_iff_isPath_tail_and_le_length.match_1, And.intro, Iff.intro, SimpleGraph.Walk.IsCycle.three_le_length, SimpleGraph.Walk.IsCycle.isPath_tail
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
u : V
p : G.Walk u u
refine : p.tail.IsPath ∧ 3 ≤ p.length → ∀ (h₁ : p.tail.IsPath) (h₂ : 3 ≤ p.length), p.IsCycle
⊢ p.IsCycle ↔ p.tail.IsPath ∧ 3 ≤ p.length

Tactic:
refine ⟨fun h ↦ ⟨h.isPath_tail, h.three_le_length⟩, fun ⟨h₁, h₂⟩ ↦ ?_⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
u : V
h :
  IsPath.{u} (V := V) (G := G) (u := snd (G := G) (u := u) nil) (tail nil) ∧
    3 ≤ length.{u} (V := V) (G := G) (u := u) nil
h₁ : IsPath.{u} (V := V) (G := G) (u := snd (G := G) (u := u) nil) (tail nil)
h₂ : 3 ≤ length.{u} (V := V) (G := G) (u := u) nil
⊢ IsCycle.{u} (V := V) (G := G) (u := u) nil

Tactic:
simp_all
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
u v : V
h' : G.Adj u v
p : G.Walk v u
h : (cons h' p).tail.IsPath ∧ 3 ≤ (cons h' p).length
h₁ : (cons h' p).tail.IsPath
h₂ : 3 ≤ (cons h' p).length
⊢ p.IsPath

Tactic:
simp only [getVert_cons_succ, tail_cons, isPath_copy, length_cons] at h₁ h₂

Premises used: SimpleGraph.Walk.tail_cons, SimpleGraph.Walk.getVert_cons_succ, SimpleGraph.Walk.isPath_copy, SimpleGraph.Walk.length_cons
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
u v : V
h' : G.Adj u v
p : G.Walk v u
h : (cons h' p).tail.IsPath ∧ 3 ≤ (cons h' p).length
h₂ : 3 ≤ p.length + 1
h₁ : p.IsPath
⊢ (cons h' p).IsCycle

Tactic:
p.cons_isCycle_iff h' |>.mpr ⟨h₁, fun hh ↦ ?_⟩

Premises used: Iff.mpr, SimpleGraph.Walk.cons_isCycle_iff, And.intro
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
u v : V
h' : G.Adj u v
p : G.Walk v u
h : (Walk.cons h' p).tail.IsPath ∧ 3 ≤ (Walk.cons h' p).length
h₂ : 3 ≤ p.length + 1
h₁ : p.IsPath
cons : ∀ (hh : s(u, v) ∈ p.edges), False
⊢ (Walk.cons h' p).IsCycle

Tactic:
refine p.cons_isCycle_iff h' |>.mpr ⟨h₁, fun hh ↦ ?_⟩

Premises used: Iff.mpr, SimpleGraph.Walk.cons_isCycle_iff, And.intro
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
u v : V
h' : G.Adj u v
p : G.Walk v u
h : (cons h' p).tail.IsPath ∧ 3 ≤ (cons h' p).length
h₂ : 3 ≤ p.length + 1
h₁ : p.IsPath
hh : s(u, v) ∈ p.edges
⊢ getElem (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) p.support 0 ⋯ =
    getElem (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) p.support (p.length - 1) ⋯

Tactic:
simp [← List.head_eq_getElem_zero, h₁.eq_penultimate_of_mem_edges hh]

Premises used: List.head_eq_getElem_zero, SimpleGraph.Walk.IsPath.eq_penultimate_of_mem_edges
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
u v : V
h' : G.Adj u v
p : G.Walk v u
h : (cons h' p).tail.IsPath ∧ 3 ≤ (cons h' p).length
h₂ : 3 ≤ p.length + 1
h₁ : p.IsPath
hh : s(u, v) ∈ p.edges
⊢ getElem (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) p.support 0 ⋯ =
    getElem (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) p.support (p.length - 1) ⋯

Tactic:
have : p.support[0] = p.support[p.length - 1] := by
      simp [← List.head_eq_getElem_zero, h₁.eq_penultimate_of_mem_edges hh]
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
u v : V
h' : G.Adj u v
p : G.Walk v u
h : (cons h' p).tail.IsPath ∧ 3 ≤ (cons h' p).length
h₂ : 3 ≤ p.length + 1
h₁ : p.IsPath
hh : s(u, v) ∈ p.edges
this :
  getElem (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) p.support 0 ⋯ =
    getElem (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) p.support (p.length - 1) ⋯
⊢ (⟨0, ⋯⟩ : Fin p.support.length) = ⟨p.length - 1, ⋯⟩

Tactic:
have := p.isPath_iff_injective_get_support.mp h₁ this
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
u v : V
h' : G.Adj u v
p : G.Walk v u
h : (cons h' p).tail.IsPath ∧ 3 ≤ (cons h' p).length
h₂ : 3 ≤ p.length + 1
h₁ : p.IsPath
hh : s(u, v) ∈ p.edges
this_1 :
  getElem (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) p.support 0 ⋯ =
    getElem (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) p.support (p.length - 1) ⋯
this : (⟨0, ⋯⟩ : Fin p.support.length) = ⟨p.length - 1, ⋯⟩
⊢ False

Tactic:
lia
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
u : V
p : G.Walk u u
h : p.tail.IsPath ∧ 3 ≤ p.length
h₁ : p.tail.IsPath
h₂ : 3 ≤ p.length
nil :
  IsPath.{u} (V := V) (G := G) (u := snd (G := G) (u := u) Walk.nil) (tail Walk.nil) ∧
      3 ≤ length.{u} (V := V) (G := G) (u := u) Walk.nil →
    ∀ (h₁ : IsPath.{u} (V := V) (G := G) (u := snd (G := G) (u := u) Walk.nil) (tail Walk.nil))
      (h₂ : 3 ≤ length.{u} (V := V) (G := G) (u := u) Walk.nil), IsCycle.{u} (V := V) (G := G) (u := u) Walk.nil
cons :
  ∀ {v : V} (h' : G.Adj u v) (p : G.Walk v u),
    (Walk.cons h' p).tail.IsPath ∧ 3 ≤ (Walk.cons h' p).length →
      ∀ (h₁ : (Walk.cons h' p).tail.IsPath) (h₂ : 3 ≤ (Walk.cons h' p).length), (Walk.cons h' p).IsCycle
⊢ p.IsCycle

Tactic:
cases p with
  | nil => simp_all
  | cons h' p =>
    simp only [getVert_cons_succ, tail_cons, isPath_copy, length_cons] at h₁ h₂
    refine p.cons_isCycle_iff h' |>.mpr ⟨h₁, fun hh ↦ ?_⟩
    have : p.support[0] = p.support[p.length - 1] := by
      simp [← List.head_eq_getElem_zero, h₁.eq_penultimate_of_mem_edges hh]
    have := p.isPath_iff_injective_get_support.mp h₁ this
    lia

Premises used: SimpleGraph.Walk.tail_cons, SimpleGraph.Walk.getVert_cons_succ, SimpleGraph.Walk.cons, SimpleGraph.Walk.isPath_copy, SimpleGraph.Walk.nil, SimpleGraph.Walk.length_cons
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
u v w : V
p : G.Walk v w
hc : p.IsTrail
h : u ∈ p.support
rwa rwa₁ rwa₂ rwa₃ :
  ∀ (hc : ((p.takeUntil u h).append (p.dropUntil u h)).IsTrail), ((p.takeUntil u h).append (p.dropUntil u h)).IsTrail
⊢ ((p.takeUntil u h).append (p.dropUntil u h)).IsTrail

Tactic:
rwa [← take_spec _ h] at hc

Premises used: SimpleGraph.Walk.take_spec
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
u v w : V
p : G.Walk v w
hc : p.IsPath
h : u ∈ p.support
rwa rwa₁ rwa₂ rwa₃ :
  ∀ (hc : ((p.takeUntil u h).append (p.dropUntil u h)).IsPath), ((p.takeUntil u h).append (p.dropUntil u h)).IsPath
⊢ ((p.takeUntil u h).append (p.dropUntil u h)).IsPath

Tactic:
rwa [← take_spec _ h] at hc

Premises used: SimpleGraph.Walk.take_spec
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
u v : V
inst : DecidableEq V
x : V
w : G.Walk u v
hw : w.IsTrail
hx : x ∈ w.support
⊢ ((w.takeUntil x hx).edges ++ (w.dropUntil x hx).edges).Nodup

Tactic:
simpa [← edges_append] using hw.edges_nodup

Premises used: SimpleGraph.Walk.IsTrail.edges_nodup, SimpleGraph.Walk.edges_append
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
u v : V
inst : DecidableEq V
c : G.Walk v v
hu : u ∈ c.support
rw : (c.rotate u hu).edges.Nodup ↔ c.IsTrail
rw₁ : (c.rotate u hu).edges.Nodup ↔ c.edges.Nodup
rw₂ rw₃ : c.edges.Nodup ↔ c.edges.Nodup
⊢ (c.rotate u hu).IsTrail ↔ c.IsTrail

Tactic:
rw [isTrail_def, isTrail_def, (c.rotate_edges u hu).perm.nodup_iff]

Premises used: SimpleGraph.Walk.rotate_edges, SimpleGraph.Walk.isTrail_def, List.Perm.nodup_iff, List.IsRotated.perm
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
u v : V
inst : DecidableEq V
c : G.Walk v v
hu : u ∈ c.support
⊢ (c.rotate u hu).IsCircuit ↔ c.IsCircuit

Tactic:
simp [isCircuit_def]

Premises used: SimpleGraph.Walk.isCircuit_def
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
u v : V
inst : DecidableEq V
c : G.Walk v v
hu : u ∈ c.support
⊢ (c.rotate u hu).IsCycle ↔ c.IsCycle

Tactic:
simp [isCycle_def, (support_rotate ..).perm.nodup_iff]

Premises used: SimpleGraph.Walk.isCycle_def, List.Perm.nodup_iff, SimpleGraph.Walk.support_rotate, List.IsRotated.perm
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
v w : V
inst : DecidableEq V
c : G.Walk v v
hc : c.IsCycle
h : w ∈ c.support
pos : ∀ (hvw : v = w), (c.takeUntil w h).IsPath
neg : ∀ (hvw : ¬v = w), (c.takeUntil w h).IsPath
⊢ (c.takeUntil w h).IsPath

Tactic:
by_cases hvw : v = w
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
v w : V
inst : DecidableEq V
c : G.Walk v v
hc : c.IsCycle
h : w ∈ c.support
hvw : v = w
pos : ∀ (h : v ∈ c.support), (c.takeUntil v h).IsPath
⊢ (c.takeUntil w h).IsPath

Tactic:
subst hvw
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
v : V
inst : DecidableEq V
c : G.Walk v v
hc : c.IsCycle
h : v ∈ c.support
⊢ (c.takeUntil v h).IsPath

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
v w : V
inst : DecidableEq V
c : G.Walk v v
hc : c.IsCycle
h : w ∈ c.support
hvw : ¬v = w
⊢ w ∈ c.support

Tactic:
rw [← isCycle_reverse, ← take_spec c h, reverse_append] at hc

Premises used: SimpleGraph.Walk.reverse_append, SimpleGraph.Walk.take_spec, SimpleGraph.Walk.isCycle_reverse
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
v w : V
inst : DecidableEq V
c : G.Walk v v
hc : c.IsCycle
h : w ∈ c.support
hvw : ¬v = w
h₁ : w ∈ c.support
⊢ ((c.dropUntil w h₁).reverse.append (c.takeUntil w h₁).reverse).IsCycle

Tactic:
rw [← isCycle_reverse, ← take_spec c h, reverse_append] at hc

Premises used: SimpleGraph.Walk.reverse_append, SimpleGraph.Walk.take_spec, SimpleGraph.Walk.isCycle_reverse
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
v w : V
inst : DecidableEq V
c : G.Walk v v
hc : c.IsCycle
h : w ∈ c.support
hvw : ¬v = w
h₁ : w ∈ c.support
hc₁ : ((c.dropUntil w h₁).reverse.append (c.takeUntil w h₁).reverse).IsCycle
⊢ ¬v = w

Tactic:
rw [← isCycle_reverse, ← take_spec c h, reverse_append] at hc

Premises used: SimpleGraph.Walk.reverse_append, SimpleGraph.Walk.take_spec, SimpleGraph.Walk.isCycle_reverse
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
v w : V
inst : DecidableEq V
c : G.Walk v v
h : w ∈ c.support
hc : ((c.dropUntil w h).reverse.append (c.takeUntil w h).reverse).IsCycle
hvw : ¬v = w
⊢ (c.takeUntil w h).IsPath

Tactic:
(c.takeUntil w h).isPath_reverse_iff.mp (hc.isPath_of_append_right (not_nil_of_ne hvw))

Premises used: SimpleGraph.Walk.isPath_reverse_iff, SimpleGraph.Walk.IsCycle.isPath_of_append_right, Iff.mp, SimpleGraph.Walk.not_nil_of_ne, SimpleGraph.Walk.takeUntil
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
v w : V
inst : DecidableEq V
c : G.Walk v v
h : w ∈ c.support
hc : ((c.dropUntil w h).reverse.append (c.takeUntil w h).reverse).IsCycle
hvw : ¬v = w
⊢ (c.takeUntil w h).IsPath

Tactic:
exact (c.takeUntil w h).isPath_reverse_iff.mp (hc.isPath_of_append_right (not_nil_of_ne hvw))

Premises used: SimpleGraph.Walk.isPath_reverse_iff, SimpleGraph.Walk.IsCycle.isPath_of_append_right, Iff.mp, SimpleGraph.Walk.not_nil_of_ne, SimpleGraph.Walk.takeUntil
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
v : V
inst : DecidableEq V
c : G.Walk v v
hc : c.IsCycle
⊢ List.count v c.support.tail = 1

Tactic:
have := List.count_eq_one_of_mem hc.support_nodup <| c.end_mem_tail_support hc.not_nil
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
v : V
inst : DecidableEq V
c : G.Walk v v
hc : c.IsCycle
this : List.count v c.support.tail = 1
⊢ c.support.head? = some v

Tactic:
have := c.head_support ▸ List.head?_eq_some_head c.support_ne_nil
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
v : V
inst : DecidableEq V
c : G.Walk v v
hc : c.IsCycle
this_1 : List.count v c.support.tail = 1
this : c.support.head? = some v
⊢ List.count v c.support = 2

Tactic:
grind
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
u v : V
inst : DecidableEq V
c : G.Walk v v
hc : c.IsCycle
hu : u ∈ c.support
hv : u ≠ v
⊢ u = c.support.head ⋯ ∨ u ∈ c.support.tail

Tactic:
have := List.eq_or_mem_of_mem_cons <| List.cons_head_tail c.support_ne_nil ▸ hu
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
u v : V
inst : DecidableEq V
c : G.Walk v v
hc : c.IsCycle
hu : u ∈ c.support
hv : u ≠ v
this : u = c.support.head ⋯ ∨ u ∈ c.support.tail
⊢ List.count u c.support.tail = 1

Tactic:
have := List.count_eq_one_of_mem hc.support_nodup <| this.resolve_left <| head_support _ ▸ hv
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
u v : V
inst : DecidableEq V
c : G.Walk v v
hc : c.IsCycle
hu : u ∈ c.support
hv : u ≠ v
this_1 : u = c.support.head ⋯ ∨ u ∈ c.support.tail
this : List.count u c.support.tail = 1
⊢ c.support.head? = some v

Tactic:
have := c.head_support ▸ List.head?_eq_some_head c.support_ne_nil
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
u v : V
inst : DecidableEq V
c : G.Walk v v
hc : c.IsCycle
hu : u ∈ c.support
hv : u ≠ v
this_1 : u = c.support.head ⋯ ∨ u ∈ c.support.tail
this_2 : List.count u c.support.tail = 1
this : c.support.head? = some v
⊢ List.count u c.support = 1

Tactic:
grind
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
u v w : V
inst : DecidableEq V
p : G.Walk u v
hp : p.IsPath
hw : w ∈ p.support
h : v ≠ w
hv : v ∈ (p.takeUntil w hw).support
⊢ ∃ (n : ℕ), (p.takeUntil w hw).getVert n = v ∧ n ≤ (p.takeUntil w hw).length

Tactic:
rw [Walk.mem_support_iff_exists_getVert] at hv

Premises used: SimpleGraph.Walk.mem_support_iff_exists_getVert
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
u v w : V
inst : DecidableEq V
p : G.Walk u v
hp : p.IsPath
hw : w ∈ p.support
h : v ≠ w
hv : ∃ (n : ℕ), (p.takeUntil w hw).getVert n = v ∧ n ≤ (p.takeUntil w hw).length
obtain : ∀ (n : ℕ) (hn : (p.takeUntil w hw).getVert n = v) (hnl : n ≤ (p.takeUntil w hw).length), False
⊢ False

Tactic:
obtain ⟨n, ⟨hn, hnl⟩⟩ := hv
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
u v w : V
inst : DecidableEq V
p : G.Walk u v
hp : p.IsPath
hw : w ∈ p.support
h : v ≠ w
n : ℕ
hn : (p.takeUntil w hw).getVert n = v
hnl : n ≤ (p.takeUntil w hw).length
⊢ p.getVert n = v

Tactic:
rw [getVert_takeUntil hw hnl] at hn

Premises used: SimpleGraph.Walk.getVert_takeUntil
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
u v w : V
inst : DecidableEq V
p : G.Walk u v
hp : p.IsPath
hw : w ∈ p.support
h : v ≠ w
n : ℕ
hn : (p.takeUntil w hw).getVert n = v
hnl : n ≤ (p.takeUntil w hw).length
hn₁ : p.getVert n = v
⊢ n ≤ (p.takeUntil w hw).length

Tactic:
rw [getVert_takeUntil hw hnl] at hn

Premises used: SimpleGraph.Walk.getVert_takeUntil
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
u v w : V
inst : DecidableEq V
p : G.Walk u v
hp : p.IsPath
hw : w ∈ p.support
h : v ≠ w
n : ℕ
hn : p.getVert n = v
hnl : n ≤ (p.takeUntil w hw).length
⊢ (p.takeUntil w hw).length < p.length

Tactic:
have := p.length_takeUntil_lt hw h.symm
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
u v w : V
inst : DecidableEq V
p : G.Walk u v
hp : p.IsPath
hw : w ∈ p.support
h : v ≠ w
n : ℕ
hn : p.getVert n = v
hnl : n ≤ (p.takeUntil w hw).length
this : (p.takeUntil w hw).length < p.length
⊢ n ≤ p.length

Tactic:
lia
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
u v w : V
inst : DecidableEq V
p : G.Walk u v
hp : p.IsPath
hw : w ∈ p.support
h : v ≠ w
n : ℕ
hn : p.getVert n = v
hnl : n ≤ (p.takeUntil w hw).length
this : (p.takeUntil w hw).length < p.length
⊢ Membership.mem (γ := Set ℕ) {i : ℕ | i ≤ p.length} p.length

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
u v w : V
inst : DecidableEq V
p : G.Walk u v
hp : p.IsPath
hw : w ∈ p.support
h : v ≠ w
n : ℕ
hn : p.getVert n = v
hnl : n ≤ (p.takeUntil w hw).length
this : (p.takeUntil w hw).length < p.length
⊢ n = p.length

Tactic:
have : n = p.length := hp.getVert_injOn (by rw [Set.mem_setOf]; lia) (by simp)
    (hn.symm ▸ p.getVert_length.symm)
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
u v w : V
inst : DecidableEq V
p : G.Walk u v
hp : p.IsPath
hw : w ∈ p.support
h : v ≠ w
n : ℕ
hn : p.getVert n = v
hnl : n ≤ (p.takeUntil w hw).length
this_1 : (p.takeUntil w hw).length < p.length
this : n = p.length
⊢ False

Tactic:
lia
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
⊢ p.IsPath ↔ ∀ (v_1 : V) (w : G.Walk v_1 v_1), w.IsSubwalk p → w.Nil

Tactic:
⟨fun hp v w hwp ↦ ?_, fun h ↦ .mk' ?_⟩

Premises used: Iff.intro, SimpleGraph.Walk.IsPath.mk'
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
refine_1 : ∀ (hp : p.IsPath) (v_1 : V) (w : G.Walk v_1 v_1) (hwp : w.IsSubwalk p), w.Nil
refine_2 : ∀ (h : ∀ (v_1 : V) (w : G.Walk v_1 v_1), w.IsSubwalk p → w.Nil), p.support.Nodup
⊢ p.IsPath ↔ ∀ (v_1 : V) (w : G.Walk v_1 v_1), w.IsSubwalk p → w.Nil

Tactic:
refine ⟨fun hp v w hwp ↦ ?_, fun h ↦ .mk' ?_⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
u v_1 : V
p : G.Walk u v_1
hp : p.IsPath
v : V
w : G.Walk v v
hwp : w.IsSubwalk p
⊢ w.Nil

Tactic:
simp [w.isPath_iff_eq_nil.mp <| isPath_of_isSubwalk hwp hp]

Premises used: SimpleGraph.Walk.isPath_of_isSubwalk, Iff.mp, SimpleGraph.Walk.isPath_iff_eq_nil
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
h : ∀ (v_1 : V) (w : G.Walk v_1 v_1), w.IsSubwalk p → w.Nil
⊢ p.support.Nodup

Tactic:
List.pairwise_iff_getElem.mpr fun i j _ _ _ _ ↦ ?_

Premises used: Iff.mpr, List.pairwise_iff_getElem, List.Nodup
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
h : ∀ (v_1 : V) (w : G.Walk v_1 v_1), w.IsSubwalk p → w.Nil
refine_2 :
  ∀ (i j : ℕ) (x : i < p.support.length) (x_1 : j < p.support.length),
    i < j →
      getElem (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) p.support i x =
          getElem (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) p.support j x_1 →
        False
⊢ p.support.Nodup

Tactic:
refine List.pairwise_iff_getElem.mpr fun i j _ _ _ _ ↦ ?_

Premises used: Iff.mpr, List.pairwise_iff_getElem
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
h : ∀ (v_1 : V) (w : G.Walk v_1 v_1), w.IsSubwalk p → w.Nil
i j : ℕ
h_1 : i < p.support.length
h_2 : j < p.support.length
h_3 : i < j
h_4 :
  getElem (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) p.support i h_1 =
    getElem (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) p.support j h_2
p' : G.Walk ((p.take j).getVert i) (p.getVert j) := (p.take j).drop i
⊢ ¬p'.Nil

Tactic:
grind [nil_drop_iff, take_length]

Premises used: SimpleGraph.Walk.nil_drop_iff, SimpleGraph.Walk.take_length
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
h : ∀ (v_1 : V) (w : G.Walk v_1 v_1), w.IsSubwalk p → w.Nil
i j : ℕ
h_1 : i < p.support.length
h_2 : j < p.support.length
h_3 : i < j
h_4 :
  getElem (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) p.support i h_1 =
    getElem (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) p.support j h_2
p' : G.Walk ((p.take j).getVert i) (p.getVert j) := (p.take j).drop i
⊢ ¬p'.Nil

Tactic:
have : ¬p'.Nil := by grind [nil_drop_iff, take_length]
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
h : ∀ (v_1 : V) (w : G.Walk v_1 v_1), w.IsSubwalk p → w.Nil
i j : ℕ
h_1 : i < p.support.length
h_2 : j < p.support.length
h_3 : i < j
h_4 :
  getElem (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) p.support i h_1 =
    getElem (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) p.support j h_2
p' : G.Walk ((p.take j).getVert i) (p.getVert j) := (p.take j).drop i
this : ¬p'.Nil
⊢ p'.IsSubwalk p

Tactic:
have : p'.IsSubwalk p := isSubwalk_drop _ i |>.trans <| p.isSubwalk_take j
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
h : ∀ (v_1 : V) (w : G.Walk v_1 v_1), w.IsSubwalk p → w.Nil
i j : ℕ
h_1 : i < p.support.length
h_2 : j < p.support.length
h_3 : i < j
h_4 :
  getElem (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) p.support i h_1 =
    getElem (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) p.support j h_2
p' : G.Walk ((p.take j).getVert i) (p.getVert j) := (p.take j).drop i
this_1 : ¬p'.Nil
this : p'.IsSubwalk p
⊢ False

Tactic:
grind [take_getVert, getVert_eq_support_getElem]

Premises used: SimpleGraph.Walk.getVert_eq_support_getElem, SimpleGraph.Walk.take_getVert