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

Goal state before:
pp: case cons.zero
V : Type u
G : SimpleGraph V
u v u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
ih : ∀ {i : ℕ}, p✝.length ≤ i → p✝.getVert i = w✝
hi : (cons h✝ p✝).length ≤ 0
⊢ (cons h✝ p✝).getVert 0 = w✝

pp: case cons.succ
V : Type u
G : SimpleGraph V
u v u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
ih : ∀ {i : ℕ}, p✝.length ≤ i → p✝.getVert i = w✝
n✝ : ℕ
hi : (cons h✝ p✝).length ≤ n✝ + 1
⊢ (cons h✝ p✝).getVert (n✝ + 1) = w✝

Tactic:
·

Goal state after:
case cons.zero
V : Type u
G : SimpleGraph V
u v u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
ih : ∀ {i : ℕ}, p✝.length ≤ i → p✝.getVert i = w✝
hi : (cons h✝ p✝).length ≤ 0
⊢ (cons h✝ p✝).getVert 0 = w✝
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Traversal

Goal state before:
pp: case cons.succ
V : Type u
G : SimpleGraph V
u v u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
ih : ∀ {i : ℕ}, p✝.length ≤ i → p✝.getVert i = w✝
n✝ : ℕ
hi : (cons h✝ p✝).length ≤ n✝ + 1
⊢ (cons h✝ p✝).getVert (n✝ + 1) = w✝

Tactic:
·

Goal state after:
case cons.succ
V : Type u
G : SimpleGraph V
u v u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
ih : ∀ {i : ℕ}, p✝.length ≤ i → p✝.getVert i = w✝
n✝ : ℕ
hi : (cons h✝ p✝).length ≤ n✝ + 1
⊢ (cons h✝ p✝).getVert (n✝ + 1) = w✝
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Traversal

Goal state before:
pp: case cons.zero
V : Type u
G : SimpleGraph V
u v u✝ v✝ w✝ : V
hxy : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
ih : ∀ {i : ℕ}, i < p✝.length → G.Adj (p✝.getVert i) (p✝.getVert (i + 1))
hi : 0 < (cons hxy p✝).length
⊢ G.Adj ((cons hxy p✝).getVert 0) ((cons hxy p✝).getVert (0 + 1))

pp: case cons.succ
V : Type u
G : SimpleGraph V
u v u✝ v✝ w✝ : V
hxy : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
ih : ∀ {i : ℕ}, i < p✝.length → G.Adj (p✝.getVert i) (p✝.getVert (i + 1))
n✝ : ℕ
hi : n✝ + 1 < (cons hxy p✝).length
⊢ G.Adj ((cons hxy p✝).getVert (n✝ + 1)) ((cons hxy p✝).getVert (n✝ + 1 + 1))

Tactic:
·

Goal state after:
case cons.zero
V : Type u
G : SimpleGraph V
u v u✝ v✝ w✝ : V
hxy : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
ih : ∀ {i : ℕ}, i < p✝.length → G.Adj (p✝.getVert i) (p✝.getVert (i + 1))
hi : 0 < (cons hxy p✝).length
⊢ G.Adj ((cons hxy p✝).getVert 0) ((cons hxy p✝).getVert (0 + 1))
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Traversal

Goal state before:
pp: case cons.succ
V : Type u
G : SimpleGraph V
u v u✝ v✝ w✝ : V
hxy : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
ih : ∀ {i : ℕ}, i < p✝.length → G.Adj (p✝.getVert i) (p✝.getVert (i + 1))
n✝ : ℕ
hi : n✝ + 1 < (cons hxy p✝).length
⊢ G.Adj ((cons hxy p✝).getVert (n✝ + 1)) ((cons hxy p✝).getVert (n✝ + 1 + 1))

Tactic:
·

Goal state after:
case cons.succ
V : Type u
G : SimpleGraph V
u v u✝ v✝ w✝ : V
hxy : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
ih : ∀ {i : ℕ}, i < p✝.length → G.Adj (p✝.getVert i) (p✝.getVert (i + 1))
n✝ : ℕ
hi : n✝ + 1 < (cons hxy p✝).length
⊢ G.Adj ((cons hxy p✝).getVert (n✝ + 1)) ((cons hxy p✝).getVert (n✝ + 1 + 1))
Module: Mathlib.Combinatorics.SimpleGraph.Subgraph

Goal state before:
pp: case verts
V : Type u
G : SimpleGraph V
v w : V
hvw : G.Adj v w
x✝ : V
⊢ x✝ ∈ (G.subgraphOfAdj hvw).verts ↔ x✝ ∈ (⊤.induce {v, w}).verts

pp: case Adj
V : Type u
G : SimpleGraph V
v w : V
hvw : G.Adj v w
x✝¹ x✝ : V
⊢ (G.subgraphOfAdj hvw).Adj x✝¹ x✝ ↔ (⊤.induce {v, w}).Adj x✝¹ x✝

Tactic:
·

Goal state after:
case verts
V : Type u
G : SimpleGraph V
v w : V
hvw : G.Adj v w
x✝ : V
⊢ x✝ ∈ (G.subgraphOfAdj hvw).verts ↔ x✝ ∈ (⊤.induce {v, w}).verts
Module: Mathlib.Combinatorics.SimpleGraph.Subgraph

Goal state before:
pp: case Adj
V : Type u
G : SimpleGraph V
v w : V
hvw : G.Adj v w
x✝¹ x✝ : V
⊢ (G.subgraphOfAdj hvw).Adj x✝¹ x✝ ↔ (⊤.induce {v, w}).Adj x✝¹ x✝

Tactic:
·

Goal state after:
case Adj
V : Type u
G : SimpleGraph V
v w : V
hvw : G.Adj v w
x✝¹ x✝ : V
⊢ (G.subgraphOfAdj hvw).Adj x✝¹ x✝ ↔ (⊤.induce {v, w}).Adj x✝¹ x✝
Module: Mathlib.Combinatorics.SimpleGraph.Subgraph

Goal state before:
pp: case Adj.mp
V : Type u
G : SimpleGraph V
v w : V
hvw : G.Adj v w
x✝¹ x✝ : V
⊢ (G.subgraphOfAdj hvw).Adj x✝¹ x✝ → (⊤.induce {v, w}).Adj x✝¹ x✝

pp: case Adj.mpr
V : Type u
G : SimpleGraph V
v w : V
hvw : G.Adj v w
x✝¹ x✝ : V
⊢ (⊤.induce {v, w}).Adj x✝¹ x✝ → (G.subgraphOfAdj hvw).Adj x✝¹ x✝

Tactic:
·

Goal state after:
case Adj.mp
V : Type u
G : SimpleGraph V
v w : V
hvw : G.Adj v w
x✝¹ x✝ : V
⊢ (G.subgraphOfAdj hvw).Adj x✝¹ x✝ → (⊤.induce {v, w}).Adj x✝¹ x✝
Module: Mathlib.Combinatorics.SimpleGraph.Subgraph

Goal state before:
pp: case Adj.mpr
V : Type u
G : SimpleGraph V
v w : V
hvw : G.Adj v w
x✝¹ x✝ : V
⊢ (⊤.induce {v, w}).Adj x✝¹ x✝ → (G.subgraphOfAdj hvw).Adj x✝¹ x✝

Tactic:
·

Goal state after:
case Adj.mpr
V : Type u
G : SimpleGraph V
v w : V
hvw : G.Adj v w
x✝¹ x✝ : V
⊢ (⊤.induce {v, w}).Adj x✝¹ x✝ → (G.subgraphOfAdj hvw).Adj x✝¹ x✝
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Traversal

Goal state before:
pp: case pos
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
n : ℕ
h : n ≤ p.length
⊢ p.getVert n = p.support.getD n v

pp: case neg
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
n : ℕ
h : ¬n ≤ p.length
⊢ p.getVert n = p.support.getD n v

Tactic:
·

Goal state after:
case pos
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
n : ℕ
h : n ≤ p.length
⊢ p.getVert n = p.support.getD n v
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Traversal

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v u' v' : V
p : G.Walk u v
h : [u', v'] <:+: p.support
⊢ G.Adj u' v'

Tactic:
have ⟨k, hk, h⟩ := List.infix_iff_getElem?.mp h

Goal state after:
V : Type u
G : SimpleGraph V
u v u' v' : V
p : G.Walk u v
h✝ : [u', v'] <:+: p.support
k : ℕ
hk : [u', v'].length + k ≤ p.support.length
h : ∀ (i : ℕ) (h : i < [u', v'].length), p.support[i + k]? = some [u', v'][i]
⊢ G.Adj u' v'
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk

Goal state before:
pp: case pos
α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
P : Finpartition univ
hP : P.IsEquipartition
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
U : Finset α
hU : U ∈ P.parts
hm : m ≠ 0
h✝ : #U = m * 4 ^ #P.parts + (Fintype.card α / #P.parts - m * 4 ^ #P.parts)
⊢ #(equitabilise ⋯).parts = 4 ^ #P.parts

pp: case neg
α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
P : Finpartition univ
hP : P.IsEquipartition
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
U : Finset α
hU : U ∈ P.parts
hm : m ≠ 0
h✝ : ¬#U = m * 4 ^ #P.parts + (Fintype.card α / #P.parts - m * 4 ^ #P.parts)
⊢ #(equitabilise ⋯).parts = 4 ^ #P.parts

Tactic:
·

Goal state after:
case pos
α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
P : Finpartition univ
hP : P.IsEquipartition
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
U : Finset α
hU : U ∈ P.parts
hm : m ≠ 0
h✝ : #U = m * 4 ^ #P.parts + (Fintype.card α / #P.parts - m * 4 ^ #P.parts)
⊢ #(equitabilise ⋯).parts = 4 ^ #P.parts
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk

Goal state before:
pp: case neg
α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
P : Finpartition univ
hP : P.IsEquipartition
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
U : Finset α
hU : U ∈ P.parts
hm : m ≠ 0
h✝ : ¬#U = m * 4 ^ #P.parts + (Fintype.card α / #P.parts - m * 4 ^ #P.parts)
⊢ #(equitabilise ⋯).parts = 4 ^ #P.parts

Tactic:
·

Goal state after:
case neg
α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
P : Finpartition univ
hP : P.IsEquipartition
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
U : Finset α
hU : U ∈ P.parts
hm : m ≠ 0
h✝ : ¬#U = m * 4 ^ #P.parts + (Fintype.card α / #P.parts - m * 4 ^ #P.parts)
⊢ #(equitabilise ⋯).parts = 4 ^ #P.parts
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Basic

Goal state before:
pp: case head
V : Type u
G : SimpleGraph V
u v v✝ : V
h' : G.Adj u v✝
p' : G.Walk v✝ v
⊢ { fst := u, snd := v✝, adj := h' }.edge ∈ G.edgeSet

pp: case tail
V : Type u
G : SimpleGraph V
u v v✝ : V
h' : G.Adj u v✝
p' : G.Walk v✝ v
e : Sym2 V
a✝ : List.Mem e (List.map Dart.edge p'.darts)
⊢ e ∈ G.edgeSet

Tactic:
·

Goal state after:
case head
V : Type u
G : SimpleGraph V
u v v✝ : V
h' : G.Adj u v✝
p' : G.Walk v✝ v
⊢ { fst := u, snd := v✝, adj := h' }.edge ∈ G.edgeSet
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Basic

Goal state before:
pp: case refine_1
V : Type u
G : SimpleGraph V
u v u' v' : V
p : G.Walk u v
h✝ : G.Adj u' v'
h : { fst := u', snd := v', adj := h✝ } ∈ p.darts
⊢ ∃ k,
    [u', v'].length + k ≤ p.support.length ∧ ∀ (i : ℕ) (h : i < [u', v'].length), p.support[i + k]? = some [u', v'][i]

pp: case refine_2
V : Type u
G : SimpleGraph V
u v u' v' : V
p : G.Walk u v
h✝ : G.Adj u' v'
x✝ :
  ∃ k,
    [u', v'].length + k ≤ p.support.length ∧ ∀ (i : ℕ) (h : i < [u', v'].length), p.support[i + k]? = some [u', v'][i]
i : ℕ
hi : [u', v'].length + i ≤ p.support.length
h : ∀ (i_1 : ℕ) (h : i_1 < [u', v'].length), p.support[i_1 + i]? = some [u', v'][i_1]
⊢ { fst := u', snd := v', adj := h✝ } ∈ p.darts

Tactic:
·

Goal state after:
case refine_1
V : Type u
G : SimpleGraph V
u v u' v' : V
p : G.Walk u v
h✝ : G.Adj u' v'
h : { fst := u', snd := v', adj := h✝ } ∈ p.darts
⊢ ∃ k,
    [u', v'].length + k ≤ p.support.length ∧ ∀ (i : ℕ) (h : i < [u', v'].length), p.support[i + k]? = some [u', v'][i]
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'
h✝ : { fst := u', snd := v', adj := h✝¹ } ∈ p.darts
i : ℕ
hi : i < p.darts.length
h : p.darts[i] = { fst := u', snd := v', adj := h✝¹ }
j : ℕ
hj : j < [u', v'].length
⊢ p.support[j + i]? = some [u', v'][j]

Tactic:
by grind [fst_darts_getElem, snd_darts_getElem]

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

Goal state before:
pp: case refine_2
V : Type u
G : SimpleGraph V
u v u' v' : V
p : G.Walk u v
h✝ : G.Adj u' v'
x✝ :
  ∃ k,
    [u', v'].length + k ≤ p.support.length ∧ ∀ (i : ℕ) (h : i < [u', v'].length), p.support[i + k]? = some [u', v'][i]
i : ℕ
hi : [u', v'].length + i ≤ p.support.length
h : ∀ (i_1 : ℕ) (h : i_1 < [u', v'].length), p.support[i_1 + i]? = some [u', v'][i_1]
⊢ { fst := u', snd := v', adj := h✝ } ∈ p.darts

Tactic:
·

Goal state after:
case refine_2
V : Type u
G : SimpleGraph V
u v u' v' : V
p : G.Walk u v
h✝ : G.Adj u' v'
x✝ :
  ∃ k,
    [u', v'].length + k ≤ p.support.length ∧ ∀ (i : ℕ) (h : i < [u', v'].length), p.support[i + k]? = some [u', v'][i]
i : ℕ
hi : [u', v'].length + i ≤ p.support.length
h : ∀ (i_1 : ℕ) (h : i_1 < [u', v'].length), p.support[i_1 + i]? = some [u', v'][i_1]
⊢ { fst := u', snd := v', adj := h✝ } ∈ p.darts
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk

Goal state before:
pp: case h₁
α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
P : Finpartition univ
hP : P.IsEquipartition
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
U : Finset α
hU : U ∈ P.parts
𝒜 : Finset (Finset α)
s : Finset α
h𝒜 : 𝒜 ⊆ (chunk hP G ε hU).parts
hs : s ∈ 𝒜
⊢ ↑(#𝒜) * ↑m ≤ ↑(#(𝒜.sup id))

pp: case h₂
α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
P : Finpartition univ
hP : P.IsEquipartition
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
U : Finset α
hU : U ∈ P.parts
𝒜 : Finset (Finset α)
s : Finset α
h𝒜 : 𝒜 ⊆ (chunk hP G ε hU).parts
hs : s ∈ 𝒜
⊢ ↑(#s) ≤ ↑m + 1

Tactic:
·

Goal state after:
case h₁
α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
P : Finpartition univ
hP : P.IsEquipartition
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
U : Finset α
hU : U ∈ P.parts
𝒜 : Finset (Finset α)
s : Finset α
h𝒜 : 𝒜 ⊆ (chunk hP G ε hU).parts
hs : s ∈ 𝒜
⊢ ↑(#𝒜) * ↑m ≤ ↑(#(𝒜.sup id))
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Basic

Goal state before:
pp: case inl
V : Type u
G : SimpleGraph V
u v v✝ : V
h : G.Adj u v✝
p' : G.Walk v✝ v
⊢ { fst := u, snd := v✝, adj := h }.toProd.1 = u ∨ { fst := u, snd := v✝, adj := h }.toProd.1 ∈ p'.support

pp: case inr
V : Type u
G : SimpleGraph V
u v v✝ : V
h : G.Adj u v✝
p' : G.Walk v✝ v
d : G.Dart
hd : d ∈ p'.darts
⊢ d.toProd.1 = u ∨ d.toProd.1 ∈ p'.support

Tactic:
·

Goal state after:
case inl
V : Type u
G : SimpleGraph V
u v v✝ : V
h : G.Adj u v✝
p' : G.Walk v✝ v
⊢ { fst := u, snd := v✝, adj := h }.toProd.1 = u ∨ { fst := u, snd := v✝, adj := h }.toProd.1 ∈ p'.support
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Basic

Goal state before:
pp: case inr
V : Type u
G : SimpleGraph V
u v v✝ : V
h : G.Adj u v✝
p' : G.Walk v✝ v
d : G.Dart
hd : d ∈ p'.darts
⊢ d.toProd.1 = u ∨ d.toProd.1 ∈ p'.support

Tactic:
·

Goal state after:
case inr
V : Type u
G : SimpleGraph V
u v v✝ : V
h : G.Adj u v✝
p' : G.Walk v✝ v
d : G.Dart
hd : d ∈ p'.darts
⊢ d.toProd.1 = u ∨ d.toProd.1 ∈ p'.support
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk

Goal state before:
pp: case h₂
α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
P : Finpartition univ
hP : P.IsEquipartition
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
U : Finset α
hU : U ∈ P.parts
𝒜 : Finset (Finset α)
s : Finset α
h𝒜 : 𝒜 ⊆ (chunk hP G ε hU).parts
hs : s ∈ 𝒜
⊢ ↑(#s) ≤ ↑m + 1

Tactic:
·

Goal state after:
case h₂
α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
P : Finpartition univ
hP : P.IsEquipartition
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
U : Finset α
hU : U ∈ P.parts
𝒜 : Finset (Finset α)
s : Finset α
h𝒜 : 𝒜 ⊆ (chunk hP G ε hU).parts
hs : s ∈ 𝒜
⊢ ↑(#s) ≤ ↑m + 1
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk

Goal state before:
pp: case h₁
α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
P : Finpartition univ
hP : P.IsEquipartition
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
U : Finset α
hU : U ∈ P.parts
𝒜 : Finset (Finset α)
s : Finset α
m_pos : 0 < ↑m
h𝒜 : 𝒜 ⊆ (chunk hP G ε hU).parts
hs : s ∈ 𝒜
⊢ ↑(#(𝒜.biUnion id)) ≤ ↑(#𝒜) * (↑m + 1)

pp: case a
α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
P : Finpartition univ
hP : P.IsEquipartition
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
U : Finset α
hU : U ∈ P.parts
𝒜 : Finset (Finset α)
s : Finset α
m_pos : 0 < ↑m
h𝒜 : 𝒜 ⊆ (chunk hP G ε hU).parts
hs : s ∈ 𝒜
⊢ m ≤ #s

Tactic:
·

Goal state after:
case h₁
α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
P : Finpartition univ
hP : P.IsEquipartition
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
U : Finset α
hU : U ∈ P.parts
𝒜 : Finset (Finset α)
s : Finset α
m_pos : 0 < ↑m
h𝒜 : 𝒜 ⊆ (chunk hP G ε hU).parts
hs : s ∈ 𝒜
⊢ ↑(#(𝒜.biUnion id)) ≤ ↑(#𝒜) * (↑m + 1)
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk

Goal state before:
pp: case a
α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
P : Finpartition univ
hP : P.IsEquipartition
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
U : Finset α
hU : U ∈ P.parts
𝒜 : Finset (Finset α)
s : Finset α
m_pos : 0 < ↑m
h𝒜 : 𝒜 ⊆ (chunk hP G ε hU).parts
hs : s ∈ 𝒜
⊢ m ≤ #s

Tactic:
·

Goal state after:
case a
α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
P : Finpartition univ
hP : P.IsEquipartition
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
U : Finset α
hU : U ∈ P.parts
𝒜 : Finset (Finset α)
s : Finset α
m_pos : 0 < ↑m
h𝒜 : 𝒜 ⊆ (chunk hP G ε hU).parts
hs : s ∈ 𝒜
⊢ m ≤ #s
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

pp: case neg
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:
·

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 ∈ (cons a p').darts, d.toProd.1 ∈ S ∧ d.toProd.2 ∉ S
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Basic

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

Goal state after:
case neg
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
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Maps

Goal state before:
pp: V : Type u
G : SimpleGraph V
s : Set V
u v✝ v u' : V
hu : G.Adj u u'
w : G.Walk u' v
hw : ∀ x ∈ (cons hu w).support, x ∈ s
⊢ (Walk.induce s (cons hu w) hw).support = (cons hu w).support.attachWith (Membership.mem s) hw

Tactic:
by simp [support_induce]

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

Goal state before:
pp: case nil.mp
V : Type u_1
G : SimpleGraph V
u u' : V
⊢ nil.IsSubwalk nil → ∃ (hu : u' = u) (hv : u' = u), nil = nil.copy hu hv

pp: case nil.mpr
V : Type u_1
G : SimpleGraph V
u u' : V
⊢ (∃ (hu : u' = u) (hv : u' = u), nil = nil.copy hu hv) → nil.IsSubwalk nil

Tactic:
·

Goal state after:
case nil.mp
V : Type u_1
G : SimpleGraph V
u u' : V
⊢ nil.IsSubwalk nil → ∃ (hu : u' = u) (hv : u' = u), nil = nil.copy hu hv
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Subwalks

Goal state before:
pp: case nil.mpr
V : Type u_1
G : SimpleGraph V
u u' : V
⊢ (∃ (hu : u' = u) (hv : u' = u), nil = nil.copy hu hv) → nil.IsSubwalk nil

Tactic:
·

Goal state after:
case nil.mpr
V : Type u_1
G : SimpleGraph V
u u' : V
⊢ (∃ (hu : u' = u) (hv : u' = u), nil = nil.copy hu hv) → nil.IsSubwalk nil
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Subwalks

Goal state before:
pp: case nil.mpr
V : Type u_1
G : SimpleGraph V
u u' : V
⊢ (∃ (hu : u' = u) (hv : u' = u), nil = nil.copy hu hv) → nil.IsSubwalk nil

Tactic:
rintro ⟨rfl, _, _⟩

Goal state after:
case nil.mpr
V : Type u_1
G : SimpleGraph V
u' : V
w✝ : u' = u'
h✝ : nil = nil.copy ⋯ w✝
⊢ nil.IsSubwalk nil
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Subwalks

Goal state before:
pp: case cons.mp
V : Type u_1
G : SimpleGraph V
u v u' v✝ : V
h : G.Adj u v✝
p : G.Walk v✝ v
⊢ (cons h p).IsSubwalk nil → ∃ (hu : u' = u) (hv : u' = v), cons h p = nil.copy hu hv

pp: case cons.mpr
V : Type u_1
G : SimpleGraph V
u v u' v✝ : V
h : G.Adj u v✝
p : G.Walk v✝ v
⊢ (∃ (hu : u' = u) (hv : u' = v), cons h p = nil.copy hu hv) → (cons h p).IsSubwalk nil

Tactic:
·

Goal state after:
case cons.mp
V : Type u_1
G : SimpleGraph V
u v u' v✝ : V
h : G.Adj u v✝
p : G.Walk v✝ v
⊢ (cons h p).IsSubwalk nil → ∃ (hu : u' = u) (hv : u' = v), cons h p = nil.copy hu hv
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk

Goal state before:
pp: α : 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
this : ↑m / (↑m + 1) = 1 - 1 / (↑m + 1)
⊢ 50 * 2 / ε ^ 5 ≤ ↑m + 1

pp: α : 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
this : ↑m / (↑m + 1) = 1 - 1 / (↑m + 1)
⊢ 0 < ε ^ 5 / (50 * 2)

Tactic:
·

Goal state after:
α : 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
this : ↑m / (↑m + 1) = 1 - 1 / (↑m + 1)
⊢ 50 * 2 / ε ^ 5 ≤ ↑m + 1
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Subwalks

Goal state before:
pp: case cons.mpr
V : Type u_1
G : SimpleGraph V
u v u' v✝ : V
h : G.Adj u v✝
p : G.Walk v✝ v
⊢ (∃ (hu : u' = u) (hv : u' = v), cons h p = nil.copy hu hv) → (cons h p).IsSubwalk nil

Tactic:
·

Goal state after:
case cons.mpr
V : Type u_1
G : SimpleGraph V
u v u' v✝ : V
h : G.Adj u v✝
p : G.Walk v✝ v
⊢ (∃ (hu : u' = u) (hv : u' = v), cons h p = nil.copy hu hv) → (cons h p).IsSubwalk nil
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Subwalks

Goal state before:
pp: case refine_1
V : Type u_1
G : SimpleGraph V
v w v' w' : V
p₁ : G.Walk v w
p₂ : G.Walk v' w'
x✝ : p₁.IsSubwalk p₂
ru : G.Walk v' v
rv : G.Walk w w'
h : p₂ = (ru.append p₁).append rv
⊢ p₁.support <:+: p₂.support

pp: case refine_2
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
⊢ p₁.IsSubwalk p₂

Tactic:
·

Goal state after:
case refine_1
V : Type u_1
G : SimpleGraph V
v w v' w' : V
p₁ : G.Walk v w
p₂ : G.Walk v' w'
x✝ : p₁.IsSubwalk p₂
ru : G.Walk v' v
rv : G.Walk w w'
h : p₂ = (ru.append p₁).append rv
⊢ p₁.support <:+: p₂.support
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Subwalks

Goal state before:
pp: case refine_2
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
⊢ p₁.IsSubwalk p₂

Tactic:
·

Goal state after:
case refine_2
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
⊢ p₁.IsSubwalk p₂
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations

Goal state before:
pp: case inl
V : Type u
G : SimpleGraph V
u v u✝ v✝ w✝ : V
h : G.Adj u✝ v✝
p : G.Walk v✝ w✝
ih : p.reverse.getVert p.length = p.getVert (p.length - p.length)
hi : ¬p.length < p.length
⊢ (cons ⋯ nil).getVert (p.length - p.length) = (cons h p).getVert (p.length + 1 - p.length)

pp: case inr
V : Type u
G : SimpleGraph V
u v : V
i : ℕ
u✝ v✝ w✝ : V
h : G.Adj u✝ v✝
p : G.Walk v✝ w✝
ih : p.reverse.getVert i = p.getVert (p.length - i)
hi : ¬i < p.length
hi' : p.length < i
⊢ (cons ⋯ nil).getVert (i - p.length) = (cons h p).getVert (p.length + 1 - i)

Tactic:
·

Goal state after:
case inl
V : Type u
G : SimpleGraph V
u v u✝ v✝ w✝ : V
h : G.Adj u✝ v✝
p : G.Walk v✝ w✝
ih : p.reverse.getVert p.length = p.getVert (p.length - p.length)
hi : ¬p.length < p.length
⊢ (cons ⋯ nil).getVert (p.length - p.length) = (cons h p).getVert (p.length + 1 - p.length)
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Subwalks

Goal state before:
pp: case refine_2.refine_1
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
⊢ p₂.getVert s.length = v

pp: case refine_2.refine_2
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
⊢ p₂.getVert (s.length + p₁.length) = w

pp: case refine_2.refine_3
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
⊢ p₂ =
    (((p₂.take s.length).copy ⋯ ?refine_2.refine_1).append p₁).append
      ((p₂.drop (s.length + p₁.length)).copy ?refine_2.refine_2 ⋯)

Tactic:
·

Goal state after:
case refine_2.refine_1
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
⊢ p₂.getVert s.length = v
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:
by lia

Goal state after: