awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
rwa : q.getVert (n + 1 - 1) = (cons h q).getVert 0
rwa₁ rwa₂ rwa₃ rwa₄ : q.getVert (n + 1 - 1) = u_1
⊢ (cons h q).getVert (n + 1) = (cons h q).getVert 0

Tactic:
rwa [getVert_cons _ _ n.add_one_ne_zero, getVert_zero]

Premises used: SimpleGraph.Walk.getVert_cons, SimpleGraph.Walk.getVert_zero, Nat.add_one_ne_zero
-- 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 = 0

Tactic:
have := hinj
      (by rw [length_cons]; lia : (n + 1) ≤ (q.cons h).length)
      (by lia : 0 ≤ (q.cons h).length)
      (by rwa [getVert_cons _ _ n.add_one_ne_zero, getVert_zero])
-- 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
this : n + 1 = 0
⊢ False

Tactic:
lia
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
nil :
  ∀ {u : V},
    Set.InjOn.{0, u} (β := V) (getVert (G := G) (u := u) Walk.nil)
        {i : ℕ | i ≤ length.{u} (V := V) (G := G) (u := u) Walk.nil} →
      IsPath.{u} (V := V) (G := G) (u := u) Walk.nil
cons :
  ∀ {u v w : V} (h : G.Adj u v) (q : G.Walk v w) (ih : Set.InjOn q.getVert {i : ℕ | i ≤ q.length} → q.IsPath),
    Set.InjOn (Walk.cons h q).getVert {i : ℕ | i ≤ (Walk.cons h q).length} → (Walk.cons h q).IsPath
⊢ Set.InjOn p.getVert {i : ℕ | i ≤ p.length} → p.IsPath

Tactic:
induction p with
  | nil => simp
  | cons h q ih =>
    intro hinj
    rw [cons_isPath_iff]
    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' => ?_⟩
    obtain ⟨n, ⟨hn, hnl⟩⟩ := mem_support_iff_exists_getVert.mp h'
    have := hinj
      (by rw [length_cons]; lia : (n + 1) ≤ (q.cons h).length)
      (by lia : 0 ≤ (q.cons h).length)
      (by rwa [getVert_cons _ _ n.add_one_ne_zero, getVert_zero])
    lia

Premises used: SimpleGraph.Walk.cons, SimpleGraph.Walk.IsPath.nil, SimpleGraph.Walk.cons_isPath_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk u v
hp : p.IsPath
hmem : s(u, w) ∈ p.edges
⊢ ¬p.Nil

Tactic:
have hnil := edges_eq_nil.not.mp <| List.ne_nil_of_mem hmem
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk u v
hp : p.IsPath
hmem : s(u, w) ∈ p.edges
hnil : ¬p.Nil
⊢ ((u, w) = (u, p.snd) ∨ (u, w) = (u, p.snd).swap) ∨ s(u, w) ∈ p.tail.edges

Tactic:
rw [← cons_tail_eq _ hnil, edges_cons, List.mem_cons, Sym2.eq, Sym2.rel_iff'] at hmem

Premises used: Sym2.eq, Sym2.rel_iff', SimpleGraph.Walk.edges_cons, List.mem_cons, SimpleGraph.Walk.cons_tail_eq
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk u v
hp : p.IsPath
hnil : ¬p.Nil
hmem : ((u, w) = (u, p.snd) ∨ (u, w) = (u, p.snd).swap) ∨ s(u, w) ∈ p.tail.edges
nil :
  ∀ {u : V} (hp : IsPath.{u} (V := V) (G := G) (u := u) Walk.nil) (hnil : ¬Nil.{u} (V := V) (G := G) (v := u) Walk.nil)
    (hmem :
      ((u, w) = (u, snd (G := G) (u := u) Walk.nil) ∨ (u, w) = Prod.swap (u, snd (G := G) (u := u) Walk.nil)) ∨
        Membership.mem (γ := List (Sym2 V)) (edges (G := G) (u := snd (G := G) (u := u) Walk.nil) (Walk.tail Walk.nil))
          s(u, w)),
    u ∉ support (G := G) (u := snd (G := G) (u := u) Walk.nil) (Walk.tail Walk.nil)
cons :
  ∀ {u v w_1 : V} (h : G.Adj u v) (p : G.Walk v w_1),
    (∀ (hp : p.IsPath) (hnil : ¬p.Nil)
        (hmem : ((v, w) = (v, p.snd) ∨ (v, w) = (v, p.snd).swap) ∨ s(v, w) ∈ p.tail.edges), v ∉ p.tail.support) →
      ∀ (hp : (Walk.cons h p).IsPath) (hnil : ¬(Walk.cons h p).Nil)
        (hmem :
          ((u, w) = (u, (Walk.cons h p).snd) ∨ (u, w) = (u, (Walk.cons h p).snd).swap) ∨
            s(u, w) ∈ (Walk.cons h p).tail.edges),
        u ∉ (Walk.cons h p).tail.support
⊢ u ∉ p.tail.support

Tactic:
induction p
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
u v w u_1 : V
hp : IsPath.{u} (V := V) (G := G) (u := u_1) Walk.nil
hnil : ¬Nil.{u} (V := V) (G := G) (v := u_1) Walk.nil
hmem :
  ((u_1, w) = (u_1, snd (G := G) (u := u_1) Walk.nil) ∨ (u_1, w) = Prod.swap (u_1, snd (G := G) (u := u_1) Walk.nil)) ∨
    Membership.mem (γ := List (Sym2 V)) (edges (G := G) (u := snd (G := G) (u := u_1) Walk.nil) (Walk.tail Walk.nil))
      s(u_1, w)
⊢ u_1 ∉ support (G := G) (u := snd (G := G) (u := u_1) Walk.nil) (Walk.tail Walk.nil)

Tactic:
simp_all
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
u v w u_1 v_1 w_1 : V
h : G.Adj u_1 v_1
p : G.Walk v_1 w_1
p_ih :
  ∀ (hp : p.IsPath) (hnil : ¬p.Nil)
    (hmem : ((v_1, w) = (v_1, p.snd) ∨ (v_1, w) = (v_1, p.snd).swap) ∨ s(v_1, w) ∈ p.tail.edges), v_1 ∉ p.tail.support
hp : (cons h p).IsPath
hnil : ¬(cons h p).Nil
hmem : ((u_1, w) = (u_1, (cons h p).snd) ∨ (u_1, w) = (u_1, (cons h p).snd).swap) ∨ s(u_1, w) ∈ (cons h p).tail.edges
⊢ u_1 ∉ (cons h p).tail.support

Tactic:
simp_all
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk u v
hp : p.IsPath
hnil : ¬p.Nil
hmem : ((u, w) = (u, p.snd) ∨ (u, w) = (u, p.snd).swap) ∨ s(u, w) ∈ p.tail.edges
⊢ u ∉ p.tail.support

Tactic:
have : u ∉ p.tail.support := by induction p <;> simp_all
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk u v
hp : p.IsPath
hnil : ¬p.Nil
hmem : ((u, w) = (u, p.snd) ∨ (u, w) = (u, p.snd).swap) ∨ s(u, w) ∈ p.tail.edges
this : u ∉ p.tail.support
⊢ w = p.snd

Tactic:
grind [fst_mem_support_of_mem_edges]

Premises used: SimpleGraph.Walk.fst_mem_support_of_mem_edges
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk u v
hp : p.IsPath
hmem : s(v, w) ∈ p.edges
⊢ w = p.penultimate

Tactic:
simpa [hmem] using isPath_reverse_iff p |>.mpr hp |>.eq_snd_of_mem_edges (w := w)

Premises used: Iff.mpr, SimpleGraph.Walk.IsPath.eq_snd_of_mem_edges, SimpleGraph.Walk.isPath_reverse_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
u_1 v_1 : V
p : G.Walk u_1 v_1
f : G →g G'
h : (Walk.map f p).IsPath
u : V
hu : Membership.mem (γ := Set V) {w : V | w ∈ p.support} u
v : V
hv : Membership.mem (γ := Set V) {w : V | w ∈ p.support} v
hf : Eq.{v + 1} (α := V') ((f : (a : V) → V') u : V') ((f : (a : V) → V') v : V')
obtain :
  ∀ (u : Fin p.support.length) (hu : Membership.mem (γ := Set V) {w : V | w ∈ p.support} (p.support.get u))
    (hf : Eq.{v + 1} (α := V') ((f : (a : V) → V') (p.support.get u) : V') ((f : (a : V) → V') v : V')),
    p.support.get u = v
⊢ u = v

Tactic:
obtain ⟨u, rfl⟩ := List.get_of_mem hu

Premises used: List.get_of_mem, rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
u_1 v_1 : V
p : G.Walk u_1 v_1
f : G →g G'
h : (Walk.map f p).IsPath
v : V
hv : Membership.mem (γ := Set V) {w : V | w ∈ p.support} v
u : Fin p.support.length
hu : Membership.mem (γ := Set V) {w : V | w ∈ p.support} (p.support.get u)
hf : Eq.{v + 1} (α := V') ((f : (a : V) → V') (p.support.get u) : V') ((f : (a : V) → V') v : V')
obtain :
  ∀ (v : Fin p.support.length) (hv : Membership.mem (γ := Set V) {w : V | w ∈ p.support} (p.support.get v))
    (hf : Eq.{v + 1} (α := V') ((f : (a : V) → V') (p.support.get u) : V') ((f : (a : V) → V') (p.support.get v) : V')),
    p.support.get u = p.support.get v
⊢ p.support.get u = v

Tactic:
obtain ⟨v, rfl⟩ := List.get_of_mem hv

Premises used: List.get_of_mem, rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
u_1 v_1 : V
p : G.Walk u_1 v_1
f : G →g G'
h : (Walk.map f p).IsPath
u : Fin p.support.length
hu : Membership.mem (γ := Set V) {w : V | w ∈ p.support} (p.support.get u)
v : Fin p.support.length
hv : Membership.mem (γ := Set V) {w : V | w ∈ p.support} (p.support.get v)
hf : Eq.{v + 1} (α := V') ((f : (a : V) → V') (p.support.get u) : V') ((f : (a : V) → V') (p.support.get v) : V')
e_a : u = v
⊢ p.support.get u = p.support.get v

Tactic:
congr
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
u_1 v_1 : V
p : G.Walk u_1 v_1
f : G →g G'
h : (Walk.map f p).IsPath
u : Fin p.support.length
hu : Membership.mem (γ := Set V) {w : V | w ∈ p.support} (p.support.get u)
v : Fin p.support.length
hv : Membership.mem (γ := Set V) {w : V | w ∈ p.support} (p.support.get v)
hf : Eq.{v + 1} (α := V') ((f : (a : V) → V') (p.support.get u) : V') ((f : (a : V) → V') (p.support.get v) : V')
⊢ Injective.{1, v + 1} (β := V') fun (i : Fin (Walk.map f p).support.length) ↦
    getElem (valid := fun (as : List V') (i : ℕ) ↦ i < as.length) (Walk.map f p).support (↑i : ℕ) ⋯

Tactic:
have := List.nodup_iff_injective_getElem.mp h.support_nodup
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
u_1 v_1 : V
p : G.Walk u_1 v_1
f : G →g G'
h : (Walk.map f p).IsPath
u : Fin p.support.length
hu : Membership.mem (γ := Set V) {w : V | w ∈ p.support} (p.support.get u)
v : Fin p.support.length
hv : Membership.mem (γ := Set V) {w : V | w ∈ p.support} (p.support.get v)
hf : Eq.{v + 1} (α := V') ((f : (a : V) → V') (p.support.get u) : V') ((f : (a : V) → V') (p.support.get v) : V')
this :
  Injective.{1, v + 1} (β := V') fun (i : Fin (Walk.map f p).support.length) ↦
    getElem (valid := fun (as : List V') (i : ℕ) ↦ i < as.length) (Walk.map f p).support (↑i : ℕ) ⋯
⊢ Injective.{1, v + 1} (β := V') fun (i : Fin p.support.length) ↦
    getElem (valid := fun (as : List V') (i : ℕ) ↦ i < as.length) (List.map (⇑f : (a : V) → V') p.support) (↑i : ℕ) ⋯

Tactic:
rw! (castMode := .all) [support_map, List.length_map] at this

Premises used: List.length_map, SimpleGraph.Walk.support_map
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
u_1 v_1 : V
p : G.Walk u_1 v_1
f : G →g G'
h : (Walk.map f p).IsPath
u : Fin p.support.length
hu : Membership.mem (γ := Set V) {w : V | w ∈ p.support} (p.support.get u)
v : Fin p.support.length
hv : Membership.mem (γ := Set V) {w : V | w ∈ p.support} (p.support.get v)
hf : Eq.{v + 1} (α := V') ((f : (a : V) → V') (p.support.get u) : V') ((f : (a : V) → V') (p.support.get v) : V')
this :
  Injective.{1, v + 1} (β := V') fun (i : Fin p.support.length) ↦
    getElem (valid := fun (as : List V') (i : ℕ) ↦ i < as.length) (List.map (⇑f : (a : V) → V') p.support) (↑i : ℕ) ⋯
e_a :
  Eq.{v + 1} (α := V')
    ((fun (i : Fin p.support.length) ↦
        getElem (valid := fun (as : List V') (i : ℕ) ↦ i < as.length) (List.map (⇑f : (a : V) → V') p.support) (↑i : ℕ)
          ⋯)
      u)
    ((fun (i : Fin p.support.length) ↦
        getElem (valid := fun (as : List V') (i : ℕ) ↦ i < as.length) (List.map (⇑f : (a : V) → V') p.support) (↑i : ℕ)
          ⋯)
      v)
⊢ u = v

Tactic:
apply this
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
u_1 v_1 : V
p : G.Walk u_1 v_1
f : G →g G'
h : (Walk.map f p).IsPath
u : Fin p.support.length
hu : Membership.mem (γ := Set V) {w : V | w ∈ p.support} (p.support.get u)
v : Fin p.support.length
hv : Membership.mem (γ := Set V) {w : V | w ∈ p.support} (p.support.get v)
hf : Eq.{v + 1} (α := V') ((f : (a : V) → V') (p.support.get u) : V') ((f : (a : V) → V') (p.support.get v) : V')
this :
  Injective.{1, v + 1} (β := V') fun (i : Fin p.support.length) ↦
    getElem (valid := fun (as : List V') (i : ℕ) ↦ i < as.length) (List.map (⇑f : (a : V) → V') p.support) (↑i : ℕ) ⋯
⊢ Eq.{v + 1} (α := V')
    ((fun (i : Fin p.support.length) ↦
        getElem (valid := fun (as : List V') (i : ℕ) ↦ i < as.length) (List.map (⇑f : (a : V) → V') p.support) (↑i : ℕ)
          ⋯)
      u)
    ((fun (i : Fin p.support.length) ↦
        getElem (valid := fun (as : List V') (i : ℕ) ↦ i < as.length) (List.map (⇑f : (a : V) → V') p.support) (↑i : ℕ)
          ⋯)
      v)

Tactic:
simpa
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
u : V
p : G.Walk u u
hpc : p.IsCycle
⊢ (cons ⋯ p.tail).IsCycle

Tactic:
rw [← p.cons_tail_eq hpc.not_nil] at hpc

Premises used: SimpleGraph.Walk.IsCycle.not_nil, SimpleGraph.Walk.cons_tail_eq
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
u : V
p : G.Walk u u
hpc_1 : p.IsCycle
hpc : (cons ⋯ p.tail).IsCycle
n : ℕ
hn : Membership.mem (γ := Set ℕ) {i : ℕ | 1 ≤ i ∧ i ≤ p.length} n
m : ℕ
hm : Membership.mem (γ := Set ℕ) {i : ℕ | 1 ≤ i ∧ i ≤ p.length} m
hnm : p.getVert n = p.getVert m
rw :
  ∀ (hn : 1 ≤ n ∧ n ≤ p.tail.length + 1) ⦃m : ℕ⦄ (hm : 1 ≤ m ∧ m ≤ p.tail.length + 1) (hnm : p.getVert n = p.getVert m),
    n = m
⊢ n = m

Tactic:
rw [← SimpleGraph.Walk.length_tail_add_one
    (p.not_nil_of_tail_not_nil (not_nil_of_isCycle_cons hpc)), Set.mem_setOf] at hn hm

Premises used: SimpleGraph.Walk.length_tail_add_one, Set.mem_setOf, SimpleGraph.Walk.not_nil_of_isCycle_cons, SimpleGraph.Walk.not_nil_of_tail_not_nil
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
u : V
p : G.Walk u u
hpc_1 : p.IsCycle
hpc : (cons ⋯ p.tail).IsCycle
n : ℕ
hn : 1 ≤ n ∧ n ≤ p.tail.length + 1
m : ℕ
hm : 1 ≤ m ∧ m ≤ p.tail.length + 1
hnm : p.getVert n = p.getVert m
⊢ n - 1 ≤ p.tail.length

Tactic:
lia
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
u : V
p : G.Walk u u
hpc_1 : p.IsCycle
hpc : (cons ⋯ p.tail).IsCycle
n : ℕ
hn : 1 ≤ n ∧ n ≤ p.tail.length + 1
m : ℕ
hm : 1 ≤ m ∧ m ≤ p.tail.length + 1
hnm : p.getVert n = p.getVert m
⊢ m - 1 ≤ p.tail.length

Tactic:
lia
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
u : V
p : G.Walk u u
hpc_1 : p.IsCycle
hpc : (cons ⋯ p.tail).IsCycle
n : ℕ
hn : 1 ≤ n ∧ n ≤ p.tail.length + 1
m : ℕ
hm : 1 ≤ m ∧ m ≤ p.tail.length + 1
hnm : p.getVert n = p.getVert m
⊢ p.tail.getVert (n - 1) = p.tail.getVert (m - 1)

Tactic:
simp_all
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
u : V
p : G.Walk u u
hpc_1 : p.IsCycle
hpc : (cons ⋯ p.tail).IsCycle
n : ℕ
hn : 1 ≤ n ∧ n ≤ p.tail.length + 1
m : ℕ
hm : 1 ≤ m ∧ m ≤ p.tail.length + 1
hnm : p.getVert n = p.getVert m
⊢ n - 1 = m - 1

Tactic:
have := ((Walk.cons_isCycle_iff _ _).mp hpc).1.getVert_injOn
    (by lia : n - 1 ≤ p.tail.length) (by lia : m - 1 ≤ p.tail.length)
    (by simp_all)
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
u : V
p : G.Walk u u
hpc_1 : p.IsCycle
hpc : (cons ⋯ p.tail).IsCycle
n : ℕ
hn : 1 ≤ n ∧ n ≤ p.tail.length + 1
m : ℕ
hm : 1 ≤ m ∧ m ≤ p.tail.length + 1
hnm : p.getVert n = p.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
p : G.Walk u u
hpc : p.IsCycle
n : ℕ
hn : n ≤ p.length - 1
m : ℕ
hm : m ≤ p.length - 1
hnm : p.getVert n = p.getVert m
⊢ 3 ≤ p.length

Tactic:
have := hpc.three_le_length
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
u : V
p : G.Walk u u
hpc : p.IsCycle
n : ℕ
hn : n ≤ p.length - 1
m : ℕ
hm : m ≤ p.length - 1
hnm : p.getVert n = p.getVert m
this : 3 ≤ p.length
simp : 1 ≤ p.length - n ∧ p.length - n ≤ p.length
⊢ Membership.mem (γ := Set ℕ) {i : ℕ | 1 ≤ i ∧ i ≤ p.reverse.length} (p.reverse.length - n)

Tactic:
simp only [Walk.length_reverse, Set.mem_setOf_eq]

Premises used: Set.mem_setOf_eq, SimpleGraph.Walk.length_reverse
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
u : V
p : G.Walk u u
hpc : p.IsCycle
n : ℕ
hn : n ≤ p.length - 1
m : ℕ
hm : m ≤ p.length - 1
hnm : p.getVert n = p.getVert m
this : 3 ≤ p.length
⊢ 1 ≤ p.length - n ∧ p.length - n ≤ p.length

Tactic:
lia
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
u : V
p : G.Walk u u
hpc : p.IsCycle
n : ℕ
hn : n ≤ p.length - 1
m : ℕ
hm : m ≤ p.length - 1
hnm : p.getVert n = p.getVert m
this : 3 ≤ p.length
simp : 1 ≤ p.length - m ∧ p.length - m ≤ p.length
⊢ Membership.mem (γ := Set ℕ) {i : ℕ | 1 ≤ i ∧ i ≤ p.reverse.length} (p.reverse.length - m)

Tactic:
simp only [Walk.length_reverse, Set.mem_setOf_eq]

Premises used: Set.mem_setOf_eq, SimpleGraph.Walk.length_reverse
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
u : V
p : G.Walk u u
hpc : p.IsCycle
n : ℕ
hn : n ≤ p.length - 1
m : ℕ
hm : m ≤ p.length - 1
hnm : p.getVert n = p.getVert m
this : 3 ≤ p.length
⊢ 1 ≤ p.length - m ∧ p.length - m ≤ p.length

Tactic:
lia
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
u : V
p : G.Walk u u
hpc : p.IsCycle
n : ℕ
hn : n ≤ p.length - 1
m : ℕ
hm : m ≤ p.length - 1
hnm : p.getVert n = p.getVert m
this : 3 ≤ p.length
⊢ p.length - (p.length - n) = n

Tactic:
lia
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
u : V
p : G.Walk u u
hpc : p.IsCycle
n : ℕ
hn : n ≤ p.length - 1
m : ℕ
hm : m ≤ p.length - 1
hnm : p.getVert n = p.getVert m
this : 3 ≤ p.length
⊢ p.length - (p.length - m) = m

Tactic:
lia
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
u : V
p : G.Walk u u
hpc : p.IsCycle
n : ℕ
hn : n ≤ p.length - 1
m : ℕ
hm : m ≤ p.length - 1
hnm : p.getVert n = p.getVert m
this : 3 ≤ p.length
⊢ p.reverse.getVert (p.reverse.length - n) = p.reverse.getVert (p.reverse.length - m)

Tactic:
simp [Walk.getVert_reverse, show p.length - (p.length - n) = n by lia, hnm,
      show p.length - (p.length - m) = m by lia]

Premises used: SimpleGraph.Walk.getVert_reverse
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
u : V
p : G.Walk u u
hpc : p.IsCycle
n : ℕ
hn : n ≤ p.length - 1
m : ℕ
hm : m ≤ p.length - 1
hnm : p.getVert n = p.getVert m
this : 3 ≤ p.length
⊢ p.length - n = p.length - m

Tactic:
have : p.length - n = p.length - m := Walk.length_reverse _ ▸ hpc.reverse.getVert_injOn
    (by simp only [Walk.length_reverse, Set.mem_setOf_eq]; lia)
    (by simp only [Walk.length_reverse, Set.mem_setOf_eq]; lia)
    (by simp [Walk.getVert_reverse, show p.length - (p.length - n) = n by lia, hnm,
      show p.length - (p.length - m) = m by lia])
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
u : V
p : G.Walk u u
hpc : p.IsCycle
n : ℕ
hn : n ≤ p.length - 1
m : ℕ
hm : m ≤ p.length - 1
hnm : p.getVert n = p.getVert m
this_1 : 3 ≤ p.length
this : p.length - n = p.length - m
⊢ n = m

Tactic:
lia
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
u : V
p : G.Walk u u
hp : p.IsCycle
h : p.snd = p.penultimate
⊢ 3 ≤ p.length

Tactic:
have := hp.three_le_length
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
u : V
p : G.Walk u u
hp : p.IsCycle
h : p.snd = p.penultimate
this : 3 ≤ p.length
simp : 1 ≤ p.length
⊢ Membership.mem (γ := Set ℕ) {i : ℕ | 1 ≤ i ∧ i ≤ p.length} 1

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
u : V
p : G.Walk u u
hp : p.IsCycle
h : p.snd = p.penultimate
this : 3 ≤ p.length
⊢ 1 ≤ p.length

Tactic:
lia
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
u : V
p : G.Walk u u
hp : p.IsCycle
h : p.snd = p.penultimate
this : 3 ≤ p.length
simp : 1 ≤ p.length - 1
⊢ Membership.mem (γ := Set ℕ) {i : ℕ | 1 ≤ i ∧ i ≤ p.length} (p.length - 1)

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
u : V
p : G.Walk u u
hp : p.IsCycle
h : p.snd = p.penultimate
this : 3 ≤ p.length
⊢ 1 ≤ p.length - 1

Tactic:
lia
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
u : V
p : G.Walk u u
hp : p.IsCycle
h : p.snd = p.penultimate
this : 3 ≤ p.length
⊢ 1 = p.length - 1

Tactic:
apply hp.getVert_injOn (by simp; lia) (by simp; lia) at h

Premises used: SimpleGraph.Walk.IsCycle.getVert_injOn
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
u : V
p : G.Walk u u
hp : p.IsCycle
this : 3 ≤ p.length
h : 1 = 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
hl : i ≤ p.length
⊢ i = 0 ∨ i = p.length → p.getVert i = u

Tactic:
aesop
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
u : V
i : ℕ
p : G.Walk u u
hpc : p.IsCycle
hl : i ≤ p.length
refine : p.getVert i = u → i = 0 ∨ i = p.length
⊢ p.getVert i = u ↔ i = 0 ∨ i = p.length

Tactic:
refine ⟨?_, by aesop⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
u : V
i : ℕ
p : G.Walk u u
hpc : p.IsCycle
hl : i ≤ p.length
rw : p.getVert i = u → ¬i = 0 → i = p.length
⊢ p.getVert i = u → i = 0 ∨ i = p.length

Tactic:
rw [or_iff_not_imp_left]

Premises used: Classical.or_iff_not_imp_left
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
u : V
i : ℕ
p : G.Walk u u
hpc : p.IsCycle
hl : i ≤ p.length
h : p.getVert i = u
hi : ¬i = 0
⊢ 1 ≤ i ∧ i ≤ p.length

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
hl : i ≤ p.length
h : p.getVert i = u
hi : ¬i = 0
⊢ 1 ≤ p.length ∧ p.length ≤ p.length

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
hl : i ≤ p.length
h : p.getVert i = u
hi : ¬i = 0
⊢ i = p.length

Tactic:
exact hpc.getVert_injOn (by simp only [Set.mem_setOf_eq]; lia)
    (by simp only [Set.mem_setOf_eq]; lia) (h.symm ▸ (Walk.getVert_length p).symm)

Premises used: SimpleGraph.Walk.IsCycle.getVert_injOn
-- 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)
⊢ 3 ≤ p.length

Tactic:
have hl := hpc.three_le_length
-- 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
pos : ∀ (hi' : i ≥ p.length - 1), False
neg : ∀ (hi' : ¬i ≥ p.length - 1), False
⊢ False

Tactic:
by_cases hi' : i ≥ p.length - 1

Premises used: SimpleGraph.Walk.length
-- 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
⊢ p.length ≤ i + 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) = u
hl : 3 ≤ p.length
hi' : i ≥ p.length - 1
⊢ i - 1 ≤ p.length

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 = 0 ∨ i - 1 = 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