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

Goal state before:
pp: case pos
V : Type u_1
G : SimpleGraph V
s t : V
inst✝ : DecidableEq V
hn : ¬G.Adj s t
e : Sym2 V
x✝ y✝ : V
h✝¹ : x✝ = t
h✝ : y✝ = t
⊢ False ↔ G.Adj x✝ y✝ ∧ ¬(G.Adj x✝ y✝ ∧ (t = x✝ ∨ t = y✝)) ∨ s(x✝, y✝) ∈ (fun x ↦ s(x, t)) '' G.neighborSet s

pp: case neg
V : Type u_1
G : SimpleGraph V
s t : V
inst✝ : DecidableEq V
hn : ¬G.Adj s t
e : Sym2 V
x✝ y✝ : V
h✝¹ : x✝ = t
h✝ : ¬y✝ = t
⊢ G.Adj s y✝ ↔ G.Adj x✝ y✝ ∧ ¬(G.Adj x✝ y✝ ∧ (t = x✝ ∨ t = y✝)) ∨ s(x✝, y✝) ∈ (fun x ↦ s(x, t)) '' G.neighborSet s

pp: case pos
V : Type u_1
G : SimpleGraph V
s t : V
inst✝ : DecidableEq V
hn : ¬G.Adj s t
e : Sym2 V
x✝ y✝ : V
h✝¹ : ¬x✝ = t
h✝ : y✝ = t
⊢ G.Adj x✝ s ↔ G.Adj x✝ y✝ ∧ ¬(G.Adj x✝ y✝ ∧ (t = x✝ ∨ t = y✝)) ∨ s(x✝, y✝) ∈ (fun x ↦ s(x, t)) '' G.neighborSet s

pp: case neg
V : Type u_1
G : SimpleGraph V
s t : V
inst✝ : DecidableEq V
hn : ¬G.Adj s t
e : Sym2 V
x✝ y✝ : V
h✝¹ : ¬x✝ = t
h✝ : ¬y✝ = t
⊢ G.Adj x✝ y✝ ↔ G.Adj x✝ y✝ ∧ ¬(G.Adj x✝ y✝ ∧ (t = x✝ ∨ t = y✝)) ∨ s(x✝, y✝) ∈ (fun x ↦ s(x, t)) '' G.neighborSet s

Tactic:
;

Goal state after:
case pos
V : Type u_1
G : SimpleGraph V
s t : V
inst✝ : DecidableEq V
hn : ¬G.Adj s t
e : Sym2 V
x✝ y✝ : V
h✝¹ : x✝ = t
h✝ : y✝ = t
⊢ False ↔ G.Adj x✝ y✝ ∧ ¬(G.Adj x✝ y✝ ∧ (t = x✝ ∨ t = y✝)) ∨ s(x✝, y✝) ∈ (fun x ↦ s(x, t)) '' G.neighborSet s

case neg
V : Type u_1
G : SimpleGraph V
s t : V
inst✝ : DecidableEq V
hn : ¬G.Adj s t
e : Sym2 V
x✝ y✝ : V
h✝¹ : x✝ = t
h✝ : ¬y✝ = t
⊢ G.Adj s y✝ ↔ G.Adj x✝ y✝ ∧ ¬(G.Adj x✝ y✝ ∧ (t = x✝ ∨ t = y✝)) ∨ s(x✝, y✝) ∈ (fun x ↦ s(x, t)) '' G.neighborSet s

case pos
V : Type u_1
G : SimpleGraph V
s t : V
inst✝ : DecidableEq V
hn : ¬G.Adj s t
e : Sym2 V
x✝ y✝ : V
h✝¹ : ¬x✝ = t
h✝ : y✝ = t
⊢ G.Adj x✝ s ↔ G.Adj x✝ y✝ ∧ ¬(G.Adj x✝ y✝ ∧ (t = x✝ ∨ t = y✝)) ∨ s(x✝, y✝) ∈ (fun x ↦ s(x, t)) '' G.neighborSet s

case neg
V : Type u_1
G : SimpleGraph V
s t : V
inst✝ : DecidableEq V
hn : ¬G.Adj s t
e : Sym2 V
x✝ y✝ : V
h✝¹ : ¬x✝ = t
h✝ : ¬y✝ = t
⊢ G.Adj x✝ y✝ ↔ G.Adj x✝ y✝ ∧ ¬(G.Adj x✝ y✝ ∧ (t = x✝ ∨ t = y✝)) ∨ s(x✝, y✝) ∈ (fun x ↦ s(x, t)) '' G.neighborSet s
Module: Mathlib.Combinatorics.SimpleGraph.Operations

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
s t : V
inst✝ : DecidableEq V
hn : ¬G.Adj s t
e : Sym2 V
x✝ y✝ : V
h✝¹ : ¬x✝ = t
h✝ : y✝ = t
⊢ G.Adj s x✝ ↔ G.Adj x✝ y✝ ∧ ¬(G.Adj x✝ y✝ ∧ (t = x✝ ∨ t = y✝)) ∨ s(x✝, y✝) ∈ (fun x ↦ s(x, t)) '' G.neighborSet s

Tactic:
;

Goal state after:
V : Type u_1
G : SimpleGraph V
s t : V
inst✝ : DecidableEq V
hn : ¬G.Adj s t
e : Sym2 V
x✝ y✝ : V
h✝¹ : ¬x✝ = t
h✝ : y✝ = t
⊢ G.Adj s x✝ ↔ G.Adj x✝ y✝ ∧ ¬(G.Adj x✝ y✝ ∧ (t = x✝ ∨ t = y✝)) ∨ s(x✝, y✝) ∈ (fun x ↦ s(x, t)) '' G.neighborSet s
Module: Mathlib.Combinatorics.SimpleGraph.Operations

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
s t : V
inst✝ : DecidableEq V
ha : G.Adj s t
e : Sym2 V
⊢ e ∈ (G.replaceVertex s t).edgeSet ↔
    e ∈ (G.edgeSet \ G.incidenceSet t ∪ (fun x ↦ s(x, t)) '' G.neighborSet s) \ {s(t, t)}

Tactic:
;

Goal state after:
V : Type u_1
G : SimpleGraph V
s t : V
inst✝ : DecidableEq V
ha : G.Adj s t
e : Sym2 V
⊢ e ∈ (G.replaceVertex s t).edgeSet ↔
    e ∈ (G.edgeSet \ G.incidenceSet t ∪ (fun x ↦ s(x, t)) '' G.neighborSet s) \ {s(t, t)}
Module: Mathlib.Combinatorics.SimpleGraph.Operations

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
s t : V
inst✝ : DecidableEq V
ha : G.Adj s t
e : Sym2 V
x✝ y✝ : V
⊢ (if x✝ = t then if y✝ = t then False else G.Adj s y✝ else if y✝ = t then G.Adj x✝ s else G.Adj x✝ y✝) ↔
    (G.Adj x✝ y✝ ∧ ¬(G.Adj x✝ y✝ ∧ (t = x✝ ∨ t = y✝)) ∨ s(x✝, y✝) ∈ (fun x ↦ s(x, t)) '' G.neighborSet s) ∧
      s(x✝, y✝) ∉ {s(t, t)}

Tactic:
;

Goal state after:
V : Type u_1
G : SimpleGraph V
s t : V
inst✝ : DecidableEq V
ha : G.Adj s t
e : Sym2 V
x✝ y✝ : V
⊢ (if x✝ = t then if y✝ = t then False else G.Adj s y✝ else if y✝ = t then G.Adj x✝ s else G.Adj x✝ y✝) ↔
    (G.Adj x✝ y✝ ∧ ¬(G.Adj x✝ y✝ ∧ (t = x✝ ∨ t = y✝)) ∨ s(x✝, y✝) ∈ (fun x ↦ s(x, t)) '' G.neighborSet s) ∧
      s(x✝, y✝) ∉ {s(t, t)}
Module: Mathlib.Combinatorics.SimpleGraph.Operations

Goal state before:
pp: case pos
V : Type u_1
G : SimpleGraph V
s t : V
inst✝ : DecidableEq V
ha : G.Adj s t
e : Sym2 V
x✝ y✝ : V
h✝¹ : x✝ = t
h✝ : y✝ = t
⊢ False ↔
    (G.Adj x✝ y✝ ∧ ¬(G.Adj x✝ y✝ ∧ (t = x✝ ∨ t = y✝)) ∨ s(x✝, y✝) ∈ (fun x ↦ s(x, t)) '' G.neighborSet s) ∧
      s(x✝, y✝) ∉ {s(t, t)}

pp: case neg
V : Type u_1
G : SimpleGraph V
s t : V
inst✝ : DecidableEq V
ha : G.Adj s t
e : Sym2 V
x✝ y✝ : V
h✝¹ : x✝ = t
h✝ : ¬y✝ = t
⊢ G.Adj s y✝ ↔
    (G.Adj x✝ y✝ ∧ ¬(G.Adj x✝ y✝ ∧ (t = x✝ ∨ t = y✝)) ∨ s(x✝, y✝) ∈ (fun x ↦ s(x, t)) '' G.neighborSet s) ∧
      s(x✝, y✝) ∉ {s(t, t)}

pp: case pos
V : Type u_1
G : SimpleGraph V
s t : V
inst✝ : DecidableEq V
ha : G.Adj s t
e : Sym2 V
x✝ y✝ : V
h✝¹ : ¬x✝ = t
h✝ : y✝ = t
⊢ G.Adj x✝ s ↔
    (G.Adj x✝ y✝ ∧ ¬(G.Adj x✝ y✝ ∧ (t = x✝ ∨ t = y✝)) ∨ s(x✝, y✝) ∈ (fun x ↦ s(x, t)) '' G.neighborSet s) ∧
      s(x✝, y✝) ∉ {s(t, t)}

pp: case neg
V : Type u_1
G : SimpleGraph V
s t : V
inst✝ : DecidableEq V
ha : G.Adj s t
e : Sym2 V
x✝ y✝ : V
h✝¹ : ¬x✝ = t
h✝ : ¬y✝ = t
⊢ G.Adj x✝ y✝ ↔
    (G.Adj x✝ y✝ ∧ ¬(G.Adj x✝ y✝ ∧ (t = x✝ ∨ t = y✝)) ∨ s(x✝, y✝) ∈ (fun x ↦ s(x, t)) '' G.neighborSet s) ∧
      s(x✝, y✝) ∉ {s(t, t)}

Tactic:
;

Goal state after:
case pos
V : Type u_1
G : SimpleGraph V
s t : V
inst✝ : DecidableEq V
ha : G.Adj s t
e : Sym2 V
x✝ y✝ : V
h✝¹ : x✝ = t
h✝ : y✝ = t
⊢ False ↔
    (G.Adj x✝ y✝ ∧ ¬(G.Adj x✝ y✝ ∧ (t = x✝ ∨ t = y✝)) ∨ s(x✝, y✝) ∈ (fun x ↦ s(x, t)) '' G.neighborSet s) ∧
      s(x✝, y✝) ∉ {s(t, t)}

case neg
V : Type u_1
G : SimpleGraph V
s t : V
inst✝ : DecidableEq V
ha : G.Adj s t
e : Sym2 V
x✝ y✝ : V
h✝¹ : x✝ = t
h✝ : ¬y✝ = t
⊢ G.Adj s y✝ ↔
    (G.Adj x✝ y✝ ∧ ¬(G.Adj x✝ y✝ ∧ (t = x✝ ∨ t = y✝)) ∨ s(x✝, y✝) ∈ (fun x ↦ s(x, t)) '' G.neighborSet s) ∧
      s(x✝, y✝) ∉ {s(t, t)}

case pos
V : Type u_1
G : SimpleGraph V
s t : V
inst✝ : DecidableEq V
ha : G.Adj s t
e : Sym2 V
x✝ y✝ : V
h✝¹ : ¬x✝ = t
h✝ : y✝ = t
⊢ G.Adj x✝ s ↔
    (G.Adj x✝ y✝ ∧ ¬(G.Adj x✝ y✝ ∧ (t = x✝ ∨ t = y✝)) ∨ s(x✝, y✝) ∈ (fun x ↦ s(x, t)) '' G.neighborSet s) ∧
      s(x✝, y✝) ∉ {s(t, t)}

case neg
V : Type u_1
G : SimpleGraph V
s t : V
inst✝ : DecidableEq V
ha : G.Adj s t
e : Sym2 V
x✝ y✝ : V
h✝¹ : ¬x✝ = t
h✝ : ¬y✝ = t
⊢ G.Adj x✝ y✝ ↔
    (G.Adj x✝ y✝ ∧ ¬(G.Adj x✝ y✝ ∧ (t = x✝ ∨ t = y✝)) ∨ s(x✝, y✝) ∈ (fun x ↦ s(x, t)) '' G.neighborSet s) ∧
      s(x✝, y✝) ∉ {s(t, t)}
Module: Mathlib.Combinatorics.SimpleGraph.Operations

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
s t : V
inst✝ : DecidableEq V
ha : G.Adj s t
e : Sym2 V
x✝ y✝ : V
h✝¹ : ¬x✝ = t
h✝ : y✝ = t
⊢ G.Adj s x✝ ↔
    (G.Adj x✝ y✝ ∧ ¬(G.Adj x✝ y✝ ∧ (t = x✝ ∨ t = y✝)) ∨ s(x✝, y✝) ∈ (fun x ↦ s(x, t)) '' G.neighborSet s) ∧
      s(x✝, y✝) ∉ {s(t, t)}

Tactic:
;

Goal state after:
V : Type u_1
G : SimpleGraph V
s t : V
inst✝ : DecidableEq V
ha : G.Adj s t
e : Sym2 V
x✝ y✝ : V
h✝¹ : ¬x✝ = t
h✝ : y✝ = t
⊢ G.Adj s x✝ ↔
    (G.Adj x✝ y✝ ∧ ¬(G.Adj x✝ y✝ ∧ (t = x✝ ∨ t = y✝)) ∨ s(x✝, y✝) ∈ (fun x ↦ s(x, t)) '' G.neighborSet s) ∧
      s(x✝, y✝) ∉ {s(t, t)}
Module: Mathlib.Combinatorics.SimpleGraph.Operations

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
s t : V
inst✝ : DecidableEq V
x✝¹ x✝ : V
⊢ Decidable ((x✝¹ = s ∧ x✝ = t ∨ x✝¹ = t ∧ x✝ = s) ∧ x✝¹ ≠ x✝)

Tactic:
;

Goal state after:
V : Type u_1
G : SimpleGraph V
s t : V
inst✝ : DecidableEq V
x✝¹ x✝ : V
⊢ Decidable ((x✝¹ = s ∧ x✝ = t ∨ x✝¹ = t ∧ x✝ = s) ∧ x✝¹ ≠ x✝)
Module: Mathlib.Combinatorics.SimpleGraph.Operations

Goal state before:
pp: V : Type u_1
s x✝¹ x✝ : V
⊢ (edge s s).Adj x✝¹ x✝ ↔ ⊥.Adj x✝¹ x✝

Tactic:
;

Goal state after:
V : Type u_1
s x✝¹ x✝ : V
⊢ (edge s s).Adj x✝¹ x✝ ↔ ⊥.Adj x✝¹ x✝
Module: Mathlib.Combinatorics.SimpleGraph.Operations

Goal state before:
pp: V : Type u_1
s x✝¹ x✝ : V
⊢ (x✝¹ = s ∧ x✝ = s ∨ x✝¹ = s ∧ x✝ = s) ∧ x✝¹ ≠ x✝ ↔ ⊥.Adj x✝¹ x✝

Tactic:
;

Goal state after:
V : Type u_1
s x✝¹ x✝ : V
⊢ (x✝¹ = s ∧ x✝ = s ∨ x✝¹ = s ∧ x✝ = s) ∧ x✝¹ ≠ x✝ ↔ ⊥.Adj x✝¹ x✝
Module: Mathlib.Combinatorics.SimpleGraph.Operations

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
s t : V
inst✝² : Fintype V
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableEq V
⊢ Fintype ↑(fromEdgeSet {s(s, t)}).edgeSet

Tactic:
;

Goal state after:
V : Type u_1
G : SimpleGraph V
s t : V
inst✝² : Fintype V
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableEq V
⊢ Fintype ↑(fromEdgeSet {s(s, t)}).edgeSet
Module: Mathlib.Combinatorics.SimpleGraph.Subgraph

Goal state before:
pp: ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G' G'' : G.Subgraph
s✝ s' s : Set V
h : s ⊆ G'.verts
x✝ : ↑(G'.induce s).verts
v : V
hv✝ : v ∈ (G'.induce s).verts
hv : v ∈ s
⊢ ⟨v, ⋯⟩ ∈ {v | ↑v ∈ s}

Tactic:
;

Goal state after:
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G' G'' : G.Subgraph
s✝ s' s : Set V
h : s ⊆ G'.verts
x✝ : ↑(G'.induce s).verts
v : V
hv✝ : v ∈ (G'.induce s).verts
hv : v ∈ s
⊢ ⟨v, ⋯⟩ ∈ {v | ↑v ∈ s}
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Basic

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v u' v' : V
p : G.Walk u v
h : G.Adj u' v'
⊢ { fst := u', snd := v', adj := h } ∈ p.darts ↔ [u', v'] <:+: p.support

Tactic:
by
  refine .trans ⟨fun h ↦ ?_, fun ⟨i, hi, h⟩ ↦ ?_⟩ List.infix_iff_getElem?.symm
  · have ⟨i, hi, h⟩ := List.getElem_of_mem h
    exact ⟨i, by grind, fun j hj ↦ by grind [fst_darts_getElem, snd_darts_getElem]⟩
  · have := h 0
    have := h 1
    convert! p.darts.getElem_mem (n := i) (by grind)
      <;> grind [fst_darts_getElem, snd_darts_getElem]

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u : V
x✝ : Sym2 V
⊢ x✝ ∈ nil.edgeSet ↔ x✝ ∈ ∅

Tactic:
;

Goal state after:
V : Type u
G : SimpleGraph V
u : V
x✝ : Sym2 V
⊢ x✝ ∈ nil.edgeSet ↔ x✝ ∈ ∅
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Basic

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v w : V
h : G.Adj u v
p : G.Walk v w
x✝ : Sym2 V
⊢ x✝ ∈ (cons h p).edgeSet ↔ x✝ ∈ insert s(u, v) p.edgeSet

Tactic:
;

Goal state after:
V : Type u
G : SimpleGraph V
u v w : V
h : G.Adj u v
p : G.Walk v w
x✝ : Sym2 V
⊢ x✝ ∈ (cons h p).edgeSet ↔ x✝ ∈ insert s(u, v) p.edgeSet
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
x✝ : Sym2 V'
⊢ x✝ ∈ (Walk.map f p).edgeSet ↔ x✝ ∈ Sym2.map ⇑f '' p.edgeSet

Tactic:
;

Goal state after:
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
f : G →g G'
u v : V
p : G.Walk u v
x✝ : Sym2 V'
⊢ x✝ ∈ (Walk.map f p).edgeSet ↔ x✝ ∈ Sym2.map ⇑f '' p.edgeSet
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Basic

Goal state before:
pp: case cons
V : Type u
G : SimpleGraph V
u v w u✝ v✝ w✝ : V
h : G.Adj u✝ v✝
p : G.Walk v✝ w✝
ih : ¬p.Nil → (w ∈ p.support ↔ ∃ e ∈ p.edges, w ∈ e)
hnil : ¬(cons h p).Nil
⊢ w ∈ (cons h p).support ↔ ∃ e ∈ (cons h p).edges, w ∈ e

Tactic:
cases p <;> aesop

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
x✝ : Sym2 V
⊢ x✝ ∈ (p.transfer H hp).edgeSet ↔ x✝ ∈ p.edgeSet

Tactic:
;

Goal state after:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
H : SimpleGraph V
hp : ∀ e ∈ p.edges, e ∈ H.edgeSet
x✝ : Sym2 V
⊢ x✝ ∈ (p.transfer H hp).edgeSet ↔ x✝ ∈ p.edgeSet
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Basic

Goal state before:
pp: case pos
V : Type u
G : SimpleGraph V
u v : V
S : Set V
u✝ x w✝ : V
a : G.Adj u✝ x
p' : G.Walk x w✝
ih : x ∈ S → w✝ ∉ S → ∃ d ∈ p'.darts, d.toProd.1 ∈ S ∧ d.toProd.2 ∉ S
uS : u✝ ∈ S
vS : w✝ ∉ S
h : x ∈ S
⊢ ∃ d ∈ (cons a p').darts, d.toProd.1 ∈ S ∧ d.toProd.2 ∉ S

Tactic:
obtain ⟨d, hd, hcd⟩ := ih h vS

Goal state after:
case pos
V : Type u
G : SimpleGraph V
u v : V
S : Set V
u✝ x w✝ : V
a : G.Adj u✝ x
p' : G.Walk x w✝
ih : x ∈ S → w✝ ∉ S → ∃ d ∈ p'.darts, d.toProd.1 ∈ S ∧ d.toProd.2 ∉ S
uS : u✝ ∈ S
vS : w✝ ∉ S
h : x ∈ S
d : G.Dart
hd : d ∈ p'.darts
hcd : d.toProd.1 ∈ S ∧ d.toProd.2 ∉ S
⊢ ∃ d ∈ (cons a p').darts, d.toProd.1 ∈ S ∧ d.toProd.2 ∉ S
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Maps

Goal state before:
pp: V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
f : G →g G'
f' : G' →g G''
u v u' v' w : V
p : G.Walk u v
H : SimpleGraph V
hp : ∀ e ∈ p.edges, e ∈ H.edgeSet
⊢ ∀ e ∈ p.edges, e ∈ H.edgeSet

Tactic:
;

Goal state after:
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
f : G →g G'
f' : G' →g G''
u v u' v' w : V
p : G.Walk u v
H : SimpleGraph V
hp : ∀ e ∈ p.edges, e ∈ H.edgeSet
⊢ ∀ e ∈ p.edges, e ∈ H.edgeSet
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Maps

Goal state before:
pp: V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
f : G →g G'
f' : G' →g G''
u v u' v' w : V
p✝ : G.Walk u v
H : SimpleGraph V
s s' : Set V
e : Sym2 V
p : G.Walk v w
hp : e ∉ p.edges
x✝ : Sym2 V
⊢ x✝ ∈ {e} → x✝ ∉ p.edges

Tactic:
;

Goal state after:
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
f : G →g G'
f' : G' →g G''
u v u' v' w : V
p✝ : G.Walk u v
H : SimpleGraph V
s s' : Set V
e : Sym2 V
p : G.Walk v w
hp : e ∉ p.edges
x✝ : Sym2 V
⊢ x✝ ∈ {e} → x✝ ∉ p.edges
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Maps

Goal state before:
pp: V : Type u
G : SimpleGraph V
v w : V
s : Set (Sym2 V)
p : G.Walk v w
hp : ∀ e ∈ p.edges, e ∉ s
⊢ p.transfer G ⋯ = p

pp: case hp
V : Type u
G : SimpleGraph V
v w : V
s : Set (Sym2 V)
p : G.Walk v w
hp : ∀ e ∈ p.edges, e ∉ s
⊢ ∀ e ∈ (toDeleteEdges s p hp).edges, e ∈ G.edgeSet

Tactic:
transfer_self

Goal state after:
V : Type u
G : SimpleGraph V
v w : V
s : Set (Sym2 V)
p : G.Walk v w
hp : ∀ e ∈ p.edges, e ∉ s
⊢ p = p

case hp
V : Type u
G : SimpleGraph V
v w : V
s : Set (Sym2 V)
p : G.Walk v w
hp : ∀ e ∈ p.edges, e ∉ s
⊢ ∀ e ∈ (toDeleteEdges s p hp).edges, e ∈ G.edgeSet
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk

Goal state before:
pp: case hbc
α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
P : Finpartition univ
ε : ℝ
inst✝ : Nonempty α
hPα : #P.parts * 16 ^ #P.parts ≤ Fintype.card α
hPε : 100 ≤ 4 ^ #P.parts * ε ^ 5
hε₁ : ε ≤ 1
this : 0 ≤ ε
⊢ 50⁻¹ + 1 ^ 5 / 10000 ≤ 49⁻¹

Tactic:
;

Goal state after:
case hbc
α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
P : Finpartition univ
ε : ℝ
inst✝ : Nonempty α
hPα : #P.parts * 16 ^ #P.parts ≤ Fintype.card α
hPε : 100 ≤ 4 ^ #P.parts * ε ^ 5
hε₁ : ε ≤ 1
this : 0 ≤ ε
⊢ 50⁻¹ + 1 ^ 5 / 10000 ≤ 49⁻¹
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Decomp

Goal state before:
pp: case refl
V : Type u
G : SimpleGraph V
v w : V
inst✝ : DecidableEq V
p : G.Walk w v
hwp : w ∈ p.support
⊢ (p.takeUntil w hwp).Nil

Tactic:
;

Goal state after:
case refl
V : Type u
G : SimpleGraph V
v w : V
inst✝ : DecidableEq V
p : G.Walk w v
hwp : w ∈ p.support
⊢ (p.takeUntil w hwp).Nil
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Decomp

Goal state before:
pp: V : Type u
G : SimpleGraph V
v w u✝ : V
inst✝ : DecidableEq V
u v' w' : V
p : G.Walk v' w'
h : u ∈ (p.copy ⋯ ⋯).support
⊢ u ∈ p.support

Tactic:
;

Goal state after:
V : Type u
G : SimpleGraph V
v w u✝ : V
inst✝ : DecidableEq V
u v' w' : V
p : G.Walk v' w'
h : u ∈ (p.copy ⋯ ⋯).support
⊢ u ∈ p.support
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 v w
h : u ∈ p.support
⊢ List.drop (min (List.idxOf u p.support) p.length) p.support <:+ p.support

Tactic:
List.drop_suffix

Goal state after:
V : Type u
G : SimpleGraph V
v w u : V
inst✝ : DecidableEq V
p : G.Walk v w
h : u ∈ p.support
⊢ p.support <:+ p.support
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 v w
h : u ∈ p.support
⊢ List.drop (List.idxOf u p.support) p.darts <:+ p.darts

Tactic:
List.drop_suffix

Goal state after:
V : Type u
G : SimpleGraph V
v w u : V
inst✝ : DecidableEq V
p : G.Walk v w
h : u ∈ p.support
⊢ p.darts <:+ p.darts
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Decomp

Goal state before:
pp: case nil
V : Type u
G : SimpleGraph V
v w u : V
inst✝ : DecidableEq V
x u✝ : V
q : G.Walk u✝ w
hx✝ : x ∈ nil.support
hx : x = u✝
⊢ (nil.append q).takeUntil x ⋯ = nil.takeUntil x hx✝

Tactic:
;

Goal state after:
case nil
V : Type u
G : SimpleGraph V
v w u : V
inst✝ : DecidableEq V
x u✝ : V
q : G.Walk u✝ w
hx✝ : x ∈ nil.support
hx : x = u✝
⊢ (nil.append q).takeUntil x ⋯ = nil.takeUntil x hx✝
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Decomp

Goal state before:
pp: case nil
V : Type u
G : SimpleGraph V
v w u : V
inst✝ : DecidableEq V
u✝ : V
q : G.Walk u✝ w
hx : u✝ ∈ nil.support
⊢ (nil.append q).takeUntil u✝ ⋯ = nil.takeUntil u✝ hx

Tactic:
;

Goal state after:
case nil
V : Type u
G : SimpleGraph V
v w u : V
inst✝ : DecidableEq V
u✝ : V
q : G.Walk u✝ w
hx : u✝ ∈ nil.support
⊢ (nil.append q).takeUntil u✝ ⋯ = nil.takeUntil u✝ hx
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Subwalks

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
u v : V
p₁ p₂ : G.Walk u v
h₁ : p₁.IsSubwalk p₂
h₂ : p₂.IsSubwalk p₁
⊢ p₁ = p₂

Tactic:
isSubwalk_iff_support_isInfix

Goal state after:
V : Type u_1
G : SimpleGraph V
u v : V
p₁ p₂ : G.Walk u v
h₁ : p₁.support <:+: p₂.support
h₂ : p₂.support <:+: p₁.support
⊢ p₁ = p₂
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:
;

Goal state after:
V : Type u
G : SimpleGraph V
u : V
p : G.Walk u u
⊢ p.length + 1 - 1 ≤ p.length
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
x✝ : Sym2 V
⊢ x✝ ∈ p.reverse.edgeSet ↔ x✝ ∈ p.edgeSet

Tactic:
;

Goal state after:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
x✝ : Sym2 V
⊢ x✝ ∈ p.reverse.edgeSet ↔ x✝ ∈ p.edgeSet
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
h : G.Adj v w
x✝ : Sym2 V
⊢ x✝ ∈ (p.concat h).edgeSet ↔ x✝ ∈ insert s(v, w) p.edgeSet

Tactic:
;

Goal state after:
V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk u v
h : G.Adj v w
x✝ : Sym2 V
⊢ x✝ ∈ (p.concat h).edgeSet ↔ x✝ ∈ insert s(v, w) p.edgeSet
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
q : G.Walk v w
x✝ : Sym2 V
⊢ x✝ ∈ (p.append q).edgeSet ↔ x✝ ∈ p.edgeSet ∪ q.edgeSet

Tactic:
;

Goal state after:
V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk u v
q : G.Walk v w
x✝ : Sym2 V
⊢ x✝ ∈ (p.append q).edgeSet ↔ x✝ ∈ p.edgeSet ∪ q.edgeSet
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v u' v' : V
p : G.Walk u v
hu : u = u'
hv : v = v'
x✝ : Sym2 V
⊢ x✝ ∈ (p.copy hu hv).edgeSet ↔ x✝ ∈ p.edgeSet

Tactic:
;

Goal state after:
V : Type u
G : SimpleGraph V
u v u' v' : V
p : G.Walk u v
hu : u = u'
hv : v = v'
x✝ : Sym2 V
⊢ x✝ ∈ (p.copy hu hv).edgeSet ↔ x✝ ∈ p.edgeSet
Module: Mathlib.Combinatorics.SimpleGraph.Paths

Goal state before:
pp: V : Type u
G : SimpleGraph V
inst✝ : Fintype ↑G.edgeSet
u v : V
w : G.Walk u v
h : w.IsTrail
⊢ w.length ≤ G.edgeFinset.card

Tactic:
let edges := w.edges.toFinset

Goal state after:
V : Type u
G : SimpleGraph V
inst✝ : Fintype ↑G.edgeSet
u v : V
w : G.Walk u v
h : w.IsTrail
edges : Finset (Sym2 V) := w.edges.toFinset
⊢ w.length ≤ G.edgeFinset.card
Module: Mathlib.Combinatorics.SimpleGraph.Paths

Goal state before:
pp: V : Type u
G : SimpleGraph V
inst✝ : Fintype ↑G.edgeSet
u v : V
w : G.Walk u v
h : w.IsTrail
edges : Finset (Sym2 V) := w.edges.toFinset
⊢ w.length ≤ G.edgeFinset.card

Tactic:
have : edges.card = w.length := length_edges _ ▸ List.toFinset_card_of_nodup h.edges_nodup

Goal state after:
V : Type u
G : SimpleGraph V
inst✝ : Fintype ↑G.edgeSet
u v : V
w : G.Walk u v
h : w.IsTrail
edges : Finset (Sym2 V) := w.edges.toFinset
this : edges.card = w.length
⊢ w.length ≤ G.edgeFinset.card
Module: Mathlib.Combinatorics.SimpleGraph.Paths

Goal state before:
pp: case nil
V : Type u
G : SimpleGraph V
u : V
⊢ nil.IsPath ↔ nil.Nil

Tactic:
simp [IsPath.nil]

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

Goal state before:
pp: case cons
V : Type u
G : SimpleGraph V
u v✝ : V
h✝ : G.Adj u v✝
p✝ : G.Walk v✝ u
⊢ (cons h✝ p✝).IsPath ↔ (cons h✝ p✝).Nil

Tactic:
simp [IsPath.nil]

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
h : p.reverse.IsPath
⊢ p = p.reverse.reverse

Tactic:
;

Goal state after:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
h : p.reverse.IsPath
⊢ p = p.reverse.reverse
Module: Mathlib.Combinatorics.SimpleGraph.Paths

Goal state before:
pp: V : Type u
u v✝ : V
h : ⊥.Adj u v✝
p✝ : ⊥.Walk v✝ u
hp : (cons h p✝).IsCircuit
⊢ False

Tactic:
;

Goal state after:
V : Type u
u v✝ : V
h : ⊥.Adj u v✝
p✝ : ⊥.Walk v✝ u
hp : (cons h p✝).IsCircuit
⊢ False
Module: Mathlib.Combinatorics.SimpleGraph.Paths

Goal state before:
pp: V : Type u
G : SimpleGraph V
N : Nonempty V
inst✝ : Finite ↑G.edgeSet
this : Fintype ↑G.edgeSet
s : Set ℕ := {n | ∃ u v p, p.IsTrail ∧ p.length = n}
⊢ ∃ u v p, ∃ (_ : p.IsTrail), ∀ (u' v' : V) (p' : G.Walk u' v'), p'.IsTrail → p'.length ≤ p.length

Tactic:
have : s.Finite := Set.Finite.subset (Set.finite_le_nat G.edgeFinset.card)
    fun n ⟨_, _, _, hp, hn⟩ ↦ hn ▸ hp.length_le_card_edgeFinset

Goal state after:
V : Type u
G : SimpleGraph V
N : Nonempty V
inst✝ : Finite ↑G.edgeSet
this✝ : Fintype ↑G.edgeSet
s : Set ℕ := {n | ∃ u v p, p.IsTrail ∧ p.length = n}
this : s.Finite
⊢ ∃ u v p, ∃ (_ : p.IsTrail), ∀ (u' v' : V) (p' : G.Walk u' v'), p'.IsTrail → p'.length ≤ p.length
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
hp : ¬p.Nil
⊢ p.tail.support = p.support.tail

Tactic:
simp [← p.cons_tail_eq hp]

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
⊢ i ≤ p.length

Tactic:
;

Goal state after:
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
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:
;

Goal state after:
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
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.getVert i = w ↔ i = p.length

Tactic:
have := hp.reverse.getVert_eq_start_iff (by lia : p.reverse.length - i ≤ p.reverse.length)
  simp only [length_reverse, getVert_reverse, show p.length - (p.length - i) = i by lia] at this
  rw [this]
  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}
⊢ (cons h q).IsPath

Tactic:
rw [cons_isPath_iff]

Goal state after:
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}
⊢ q.IsPath ∧ u✝ ∉ q.support
Module: Mathlib.Combinatorics.SimpleGraph.Clique

Goal state before:
pp: α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
x : Set α
hs : G.IsClique x
ht : (⇑f '' x).Nontrivial
⊢ (SimpleGraph.map (⇑f) G).IsClique (⇑f '' x)

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
x : Set α
hs : G.IsClique x
ht : (⇑f '' x).Nontrivial
⊢ (SimpleGraph.map (⇑f) G).IsClique (⇑f '' x)