mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Maps

Goal state before:
pp: V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
f : G →g G'
u v : V
p : G.Walk u v
⊢ (Walk.map f p).darts = List.map f.mapDart p.darts

Tactic:
induction p <;> simp [*]

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Maps

Goal state before:
pp: V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
f : G →g G'
u v : V
p : G.Walk u v
⊢ (Walk.map f p).edges = List.map (Sym2.map ⇑f) p.edges

Tactic:
induction p <;> simp [*]

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Maps

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
⊢ p.transfer G ⋯ = p

Tactic:
induction p <;> simp [*]

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Maps

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
H : SimpleGraph V
hp : ∀ e ∈ p.edges, e ∈ H.edgeSet
GH : G ≤ H
⊢ p.transfer H hp = Walk.map (Hom.ofLE GH) p

Tactic:
induction p <;> simp [*]

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Maps

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
H : SimpleGraph V
hp : ∀ e ∈ p.edges, e ∈ H.edgeSet
⊢ (p.transfer H hp).edges = p.edges

Tactic:
induction p <;> simp [*]

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Maps

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
H : SimpleGraph V
hp : ∀ e ∈ p.edges, e ∈ H.edgeSet
⊢ (p.transfer H hp).support = p.support

Tactic:
induction p <;> simp [*]

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Maps

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
H : SimpleGraph V
hp : ∀ e ∈ p.edges, e ∈ H.edgeSet
⊢ (p.transfer H hp).length = p.length

Tactic:
induction p <;> simp [*]

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
⊢ p.append nil = p

Tactic:
induction p <;> simp [*]

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Maps

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
H : SimpleGraph V
hp : ∀ e ∈ p.edges, e ∈ H.edgeSet
K : SimpleGraph V
hp' : ∀ e ∈ (p.transfer H hp).edges, e ∈ K.edgeSet
⊢ (p.transfer H hp).transfer K hp' = p.transfer K ⋯

Tactic:
induction p <;> simp [*]

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v w x : V
p : G.Walk u v
q : G.Walk v w
r : G.Walk w x
⊢ p.append (q.append r) = (p.append q).append r

Tactic:
induction p <;> simp [*]

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Maps

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
H : SimpleGraph V
w : V
q : G.Walk v w
hpq : ∀ e ∈ (p.append q).edges, e ∈ H.edgeSet
⊢ (p.append q).transfer H hpq = (p.transfer H ⋯).append (q.transfer H ⋯)

Tactic:
induction p <;> simp [*]

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Maps

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
H : SimpleGraph V
hp : ∀ e ∈ p.edges, e ∈ H.edgeSet
⊢ (p.transfer H hp).reverse = p.reverse.transfer H ⋯

Tactic:
induction p <;> simp [*]

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Subwalks

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
u₁ v₁ u₂ v₂ u₃ v₃ : V
p₁ : G.Walk u₁ v₁
p₃ : G.Walk u₃ v₃
q₁ : G.Walk u₂ u₁
r₁ : G.Walk v₁ v₂
h₂ : ((q₁.append p₁).append r₁).IsSubwalk p₃
⊢ p₁.IsSubwalk p₃

Tactic:
obtain ⟨q₂, r₂, rfl⟩ := h₂

Goal state after:
V : Type u_1
G : SimpleGraph V
u₁ v₁ u₂ v₂ u₃ v₃ : V
p₁ : G.Walk u₁ v₁
q₁ : G.Walk u₂ u₁
r₁ : G.Walk v₁ v₂
q₂ : G.Walk u₃ u₂
r₂ : G.Walk v₂ v₃
⊢ p₁.IsSubwalk ((q₂.append ((q₁.append p₁).append r₁)).append r₂)
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Subwalks

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
v w v' w' : V
p₁ : G.Walk v w
p₂ : G.Walk v' w'
x✝ : p₁.support <:+: p₂.support
s t : List V
h : s ++ p₁.support ++ t = p₂.support
this : s.length + p₁.length ≤ p₂.length
⊢ s.length ≤ p₂.length

Tactic:
lia

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Subwalks

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
v w v' w' : V
p₁ : G.Walk v w
p₂ : G.Walk v' w'
x✝ : p₁.support <:+: p₂.support
s t : List V
h : s ++ p₁.support ++ t = p₂.support
this : s.length + p₁.length ≤ p₂.length
⊢ s.length ≤ s.length + p₁.length + 1

Tactic:
lia

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Decomp

Goal state before:
pp: V : Type u
G : SimpleGraph V
v u : V
inst✝ : DecidableEq V
p : G.Walk u v
⊢ p.takeUntil u ⋯ = nil

Tactic:
by cases p <;> simp [Walk.takeUntil]

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations

Goal state before:
pp: V : Type u
G : SimpleGraph V
motive : (u v : V) → G.Walk u v → Sort u_1
Hnil : {u : V} → motive u u nil
Hconcat : {u v w : V} → (p : G.Walk u v) → (h : G.Adj v w) → motive u v p → motive u w (p.concat h)
u v w : V
p : G.Walk u v
h : G.Adj v w
⊢ concatRecAux Hnil Hconcat (p.concat h).reverse ≍ concatRecAux Hnil Hconcat (cons ⋯ p.reverse)

Tactic:
congr
    simp

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Subwalks

Goal state before:
pp: case refine_1
V : Type u_1
G : SimpleGraph V
u v u' v' : V
p₁ : G.Walk u v
p₂ : G.Walk u' v'
hnil : ¬p₁.Nil
x✝ :
  ∃ k,
    p₁.support.length + k ≤ p₂.support.length ∧
      ∀ (i : ℕ) (h : i < p₁.support.length), p₂.support[i + k]? = some p₁.support[i]
k : ℕ
hk : p₁.support.length + k ≤ p₂.support.length
h : ∀ (i : ℕ) (h : i < p₁.support.length), p₂.support[i + k]? = some p₁.support[i]
i : ℕ
hi : i < p₁.darts.length
⊢ p₂.darts[i + k]? = some p₁.darts[i]

Tactic:
getElem?_pos _ _ <| by grind,

Goal state after:
case refine_1
V : Type u_1
G : SimpleGraph V
u v u' v' : V
p₁ : G.Walk u v
p₂ : G.Walk u' v'
hnil : ¬p₁.Nil
x✝ :
  ∃ k,
    p₁.support.length + k ≤ p₂.support.length ∧
      ∀ (i : ℕ) (h : i < p₁.support.length), p₂.support[i + k]? = some p₁.support[i]
k : ℕ
hk : p₁.support.length + k ≤ p₂.support.length
h : ∀ (i : ℕ) (h : i < p₁.support.length), p₂.support[i + k]? = some p₁.support[i]
i : ℕ
hi : i < p₁.darts.length
⊢ some p₂.darts[i + k] = some p₁.darts[i]
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Subwalks

Goal state before:
pp: case refine_2
V : Type u_1
G : SimpleGraph V
u v u' v' : V
p₁ : G.Walk u v
p₂ : G.Walk u' v'
hnil : ¬p₁.Nil
x✝ :
  ∃ k, p₁.darts.length + k ≤ p₂.darts.length ∧ ∀ (i : ℕ) (h : i < p₁.darts.length), p₂.darts[i + k]? = some p₁.darts[i]
k : ℕ
hk : p₁.darts.length + k ≤ p₂.darts.length
h : ∀ (i : ℕ) (h : i < p₁.darts.length), p₂.darts[i + k]? = some p₁.darts[i]
i : ℕ
hi : i < p₁.support.length
⊢ p₂.support[i + k]? = some p₁.support[i]

Tactic:
getElem?_pos _ _ <| by grind,

Goal state after:
case refine_2
V : Type u_1
G : SimpleGraph V
u v u' v' : V
p₁ : G.Walk u v
p₂ : G.Walk u' v'
hnil : ¬p₁.Nil
x✝ :
  ∃ k, p₁.darts.length + k ≤ p₂.darts.length ∧ ∀ (i : ℕ) (h : i < p₁.darts.length), p₂.darts[i + k]? = some p₁.darts[i]
k : ℕ
hk : p₁.darts.length + k ≤ p₂.darts.length
h : ∀ (i : ℕ) (h : i < p₁.darts.length), p₂.darts[i + k]? = some p₁.darts[i]
i : ℕ
hi : i < p₁.support.length
⊢ some p₂.support[i + k] = some p₁.support[i]
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk u v
p' : G.Walk v w
⊢ (p.append p').darts = p.darts ++ p'.darts

Tactic:
induction p <;> simp [*]

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
⊢ p.reverse.darts = (List.map Dart.symm p.darts).reverse

Tactic:
induction p <;> simp [*]

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Subwalks

Goal state before:
pp: case refine_1
V : Type u_1
G : SimpleGraph V
u v u' v' : V
p : G.Walk u v
h✝² : G.Adj u' v'
h✝¹ : ∃ a ∈ p.darts, a.edge = s(u', v')
d : G.Dart
hd : d ∈ p.darts
h✝ : (d.toProd.1, d.toProd.2) = (u', v') ∨ (d.toProd.1, d.toProd.2) = (u', v').swap
h : (d.toProd.1, d.toProd.2) = (u', v')
⊢ { fst := u', snd := v', adj := h✝² } ∈ p.darts

Tactic:
convert! hd using 2

Goal state after:
case e'_3
V : Type u_1
G : SimpleGraph V
u v u' v' : V
p : G.Walk u v
h✝² : G.Adj u' v'
h✝¹ : ∃ a ∈ p.darts, a.edge = s(u', v')
d : G.Dart
hd : d ∈ p.darts
h✝ : (d.toProd.1, d.toProd.2) = (u', v') ∨ (d.toProd.1, d.toProd.2) = (u', v').swap
h : (d.toProd.1, d.toProd.2) = (u', v')
⊢ (u', v') = d.toProd
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Subwalks

Goal state before:
pp: case refine_2
V : Type u_1
G : SimpleGraph V
u v u' v' : V
p : G.Walk u v
h✝² : G.Adj u' v'
h✝¹ : ∃ a ∈ p.darts, a.edge = s(u', v')
d : G.Dart
hd : d ∈ p.darts
h✝ : (d.toProd.1, d.toProd.2) = (u', v') ∨ (d.toProd.1, d.toProd.2) = (u', v').swap
h : (d.toProd.1, d.toProd.2) = (u', v').swap
⊢ { fst := v', snd := u', adj := ⋯ } ∈ p.darts

Tactic:
convert! hd using 2

Goal state after:
case e'_3
V : Type u_1
G : SimpleGraph V
u v u' v' : V
p : G.Walk u v
h✝² : G.Adj u' v'
h✝¹ : ∃ a ∈ p.darts, a.edge = s(u', v')
d : G.Dart
hd : d ∈ p.darts
h✝ : (d.toProd.1, d.toProd.2) = (u', v') ∨ (d.toProd.1, d.toProd.2) = (u', v').swap
h : (d.toProd.1, d.toProd.2) = (u', v').swap
⊢ (v', u') = d.toProd
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations

Goal state before:
pp: V : Type u
G : SimpleGraph V
u : V
p : G.Walk u u
⊢ 0 ≤ p.length

Tactic:
lia

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Decomp

Goal state before:
pp: V : Type u
G : SimpleGraph V
v w u : V
inst✝ : DecidableEq V
p : G.Walk u v
x : V
h : x ≠ w
hw : w ∈ p.support
hx : x ∈ (p.takeUntil w hw).support
hw' : w ∈ ((p.takeUntil w hw).takeUntil x hx).support
h1 : (p.takeUntil w ⋯).length < (p.takeUntil x ⋯).length
h2 : (p.takeUntil x ⋯).length < (p.takeUntil w hw).length
⊢ False

Tactic:
lia

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations

Goal state before:
pp: V : Type u
G : SimpleGraph V
u : V
p : G.Walk u u
⊢ p.length + 1 - 1 ≤ p.length

Tactic:
lia

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Paths

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk u v
hp : p.IsPath
hw : w ∈ p.support
⊢ ∃ q r, q.IsPath ∧ r.IsPath ∧ p = q.append r

Tactic:
obtain ⟨q, r, hqr⟩ := p.mem_support_iff_exists_append.mp hw

Goal state after:
V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk u v
hp : p.IsPath
hw : w ∈ p.support
q : G.Walk u w
r : G.Walk w v
hqr : p = q.append r
⊢ ∃ q r, q.IsPath ∧ r.IsPath ∧ p = q.append r
Module: Mathlib.Combinatorics.SimpleGraph.Paths

Goal state before:
pp: V : Type u
G : SimpleGraph V
inst✝ : Finite ↑G.edgeSet
this✝¹ : Fintype ↑G.edgeSet
s : Set ℕ := {n | ∃ u v p, 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
this : w✝ ≤ p'.length → p'.length ≤ w✝
⊢ p'.length ≤ p.length

Tactic:
lia

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Paths

Goal state before:
pp: V : Type u
G : SimpleGraph V
inst✝ : Finite ↑G.edgeSet
this✝¹ : Fintype ↑G.edgeSet
s : Set ℕ := {n | ∃ u v p, 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
this : w✝ ≤ p'.length → p'.length ≤ w✝
⊢ p'.length ≤ p.length

Tactic:
lia

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Paths

Goal state before:
pp: case pos
V : Type u
G : SimpleGraph V
u✝ v✝ v w u : V
h : G.Adj v w
p : G.Walk w u
ihp :
  p.IsPath → ∀ ⦃n : ℕ⦄, n ∈ {i | i ≤ p.length} → ∀ ⦃m : ℕ⦄, m ∈ {i | i ≤ p.length} → 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

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Paths

Goal state before:
pp: V : Type u
G : SimpleGraph V
u✝ v✝ v w u : V
h : G.Adj v w
p : G.Walk w u
ihp :
  p.IsPath → ∀ ⦃n : ℕ⦄, n ∈ {i | i ≤ p.length} → ∀ ⦃m : ℕ⦄, m ∈ {i | i ≤ p.length} → 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

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Paths

Goal state before:
pp: V : Type u
G : SimpleGraph V
u✝ v✝ v w u : V
h : G.Adj v w
p : G.Walk w u
ihp :
  p.IsPath → ∀ ⦃n : ℕ⦄, n ∈ {i | i ≤ p.length} → ∀ ⦃m : ℕ⦄, m ∈ {i | i ≤ p.length} → 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

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Paths

Goal state before:
pp: V : Type u
G : SimpleGraph V
u✝ v✝ v w u : V
h : G.Adj v w
p : G.Walk w u
ihp :
  p.IsPath → ∀ ⦃n : ℕ⦄, n ∈ {i | i ≤ p.length} → ∀ ⦃m : ℕ⦄, m ∈ {i | i ≤ p.length} → 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

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Paths

Goal state before:
pp: V : Type u
G : SimpleGraph V
u✝ v✝ v w u : V
h : G.Adj v w
p : G.Walk w u
ihp :
  p.IsPath → ∀ ⦃n : ℕ⦄, n ∈ {i | i ≤ p.length} → ∀ ⦃m : ℕ⦄, m ∈ {i | i ≤ p.length} → 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

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Paths

Goal state before:
pp: case neg
V : Type u
G : SimpleGraph V
u✝ v✝ v w u : V
h : G.Adj v w
p : G.Walk w u
ihp :
  p.IsPath → ∀ ⦃n : ℕ⦄, n ∈ {i | i ≤ p.length} → ∀ ⦃m : ℕ⦄, m ∈ {i | i ≤ p.length} → 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

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v✝¹ : V
p✝ : G.Walk u v✝¹
v v✝ : V
hadj : G.Adj u v✝
p : G.Walk v✝ v
⊢ (cons hadj p).tail.reverse.support = ((cons hadj p).reverse.dropLast.copy ⋯ ⋯).support

Tactic:
support_copy

Goal state after:
V : Type u
G : SimpleGraph V
u v✝¹ : V
p✝ : G.Walk u v✝¹
v v✝ : V
hadj : G.Adj u v✝
p : G.Walk v✝ v
⊢ (cons hadj p).tail.reverse.support = (cons hadj p).reverse.dropLast.support
Module: Mathlib.Combinatorics.SimpleGraph.Paths

Goal state before:
pp: V : Type u
G : SimpleGraph V
u w : V
i : ℕ
p : G.Walk u w
hp : p.IsPath
h✝ : ¬p.Nil
h : p.getVert i = u
h' : i ≤ p.length
⊢ i ≤ p.length

Tactic:
lia

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Paths

Goal state before:
pp: V : Type u
G : SimpleGraph V
u w : V
i : ℕ
p : G.Walk u w
hp : p.IsPath
h✝ : ¬p.Nil
h : p.getVert i = u
h' : i ≤ p.length
⊢ 0 ≤ p.length

Tactic:
lia

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Paths

Goal state before:
pp: 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

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Paths

Goal state before:
pp: 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

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Paths

Goal state before:
pp: 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

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Paths

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v 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
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

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Paths

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v 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
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

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Paths

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v 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
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

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Paths

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v 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
hinj : Set.InjOn (cons h q).getVert {i | i ≤ (cons h q).length}
h' : u✝ ∈ q.support
n : ℕ
hn : q.getVert n = u✝
hnl : n ≤ q.length
⊢ n + 1 ≤ q.length + 1

Tactic:
lia

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Paths

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v 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
hinj : Set.InjOn (cons h q).getVert {i | i ≤ (cons h q).length}
h' : u✝ ∈ q.support
n : ℕ
hn : q.getVert n = u✝
hnl : n ≤ q.length
⊢ 0 ≤ (cons h q).length

Tactic:
lia

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Paths

Goal state before:
pp: case cons
V : Type u
G : SimpleGraph V
u v 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
hinj : Set.InjOn (cons h q).getVert {i | i ≤ (cons h q).length}
h' : u✝ ∈ q.support
n : ℕ
hn : q.getVert n = u✝
hnl : n ≤ q.length
this : n + 1 = 0
⊢ False

Tactic:
lia

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Paths

Goal state before:
pp: V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
u✝ v✝ : V
p : G.Walk u✝ v✝
f : G →g G'
h : (Walk.map f p).IsPath
u : Fin p.support.length
hu : p.support.get u ∈ {w | w ∈ p.support}
v : Fin p.support.length
hv : p.support.get v ∈ {w | w ∈ p.support}
hf : f (p.support.get u) = f (p.support.get v)
this : Injective fun i ↦ (Walk.map f p).support[↑i]
⊢ u = v

Tactic:
support_map,

Goal state after:
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
u✝ v✝ : V
p : G.Walk u✝ v✝
f : G →g G'
h : (Walk.map f p).IsPath
u : Fin p.support.length
hu : p.support.get u ∈ {w | w ∈ p.support}
v : Fin p.support.length
hv : p.support.get v ∈ {w | w ∈ p.support}
hf : f (p.support.get u) = f (p.support.get v)
this : Injective fun i ↦ (List.map (⇑f) p.support)[↑i]
⊢ u = v
Module: Mathlib.Combinatorics.SimpleGraph.Paths

Goal state before:
pp: V : Type u
G : SimpleGraph V
u : V
p : G.Walk u u
hpc✝ : 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

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Paths

Goal state before:
pp: V : Type u
G : SimpleGraph V
u : V
p : G.Walk u u
hpc✝ : 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

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Paths

Goal state before:
pp: V : Type u
G : SimpleGraph V
u : V
p : G.Walk u u
hpc✝ : 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

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Paths

Goal state before:
pp: 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

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Paths

Goal state before:
pp: 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

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Paths

Goal state before:
pp: 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

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Paths

Goal state before:
pp: 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

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Paths

Goal state before:
pp: 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
this : p.length - n = p.length - m
⊢ n = m

Tactic:
lia

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Paths

Goal state before:
pp: 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

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Paths

Goal state before:
pp: 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

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Paths

Goal state before:
pp: 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

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Paths

Goal state before:
pp: 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

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Paths

Goal state before:
pp: 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

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Paths

Goal state before:
pp: 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

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Paths

Goal state before:
pp: 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

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Paths

Goal state before:
pp: case pos
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

Goal state after: