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

Goal state before:
pp: α : 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
V : Finset α
hV : V ∈ P.parts
hUV : U ≠ V
hunif : ¬G.IsUniform ε U V
hPε : 100 ≤ 4 ^ #P.parts * ε ^ 5
hε₁ : ε ≤ 1
hP₁ : 0 < #P.parts
this : 2 ^ #P.parts * ↑m / (↑(#U) * ε) ≤ ε / 10
⊢ (1 - 2 ^ #P.parts * ↑m / (↑(#U) * ε)) * ↑(#(G.nonuniformWitness ε U V)) =
    ↑(#(G.nonuniformWitness ε U V)) - 2 ^ #P.parts * ↑m / (↑(#U) * ε) * ↑(#(G.nonuniformWitness ε U V))

Tactic:
by
      rw [sub_mul, one_mul]

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

Goal state before:
pp: case right
V : Type u
G : SimpleGraph V
G' G'' : G.Subgraph
s s' : Set V
hg : G' ≤ G''
hs : s ⊆ s'
v w : V
hv : v ∈ s
hw : w ∈ s
⊢ G'.Adj v w → v ∈ s' ∧ w ∈ s' ∧ G''.Adj v w

Tactic:
ha

Goal state after:
case right
V : Type u
G : SimpleGraph V
G' G'' : G.Subgraph
s s' : Set V
hg : G' ≤ G''
hs : s ⊆ s'
v w : V
hv : v ∈ s
hw : w ∈ s
ha : G'.Adj v w
⊢ v ∈ s' ∧ w ∈ s' ∧ G''.Adj v w
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Traversal

Goal state before:
pp: case cons.succ
V : Type u
G : SimpleGraph V
u v v✝ : V
h✝ : G.Adj u v✝
p✝ : G.Walk v✝ v
n : ℕ
h : n + 1 ≤ (cons h✝ p✝).length
⊢ (cons h✝ p✝).getVert (n + 1) = (cons h✝ p✝).support[n + 1]

Tactic:
simp_rw [support_cons, getVert_cons _ _ n.zero_ne_add_one.symm, List.getElem_cons]
      exact getVert_eq_support_getElem _ (Nat.sub_le_of_le_add h)

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

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

Tactic:
by_cases h : n ≤ p.length

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

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
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Basic

Goal state before:
pp: V : Type u
G : SimpleGraph V
a b : V
p : G.Walk a b
⊢ p.support.getLast ⋯ = b

Tactic:
induction p

Goal state after:
case nil
V : Type u
G : SimpleGraph V
a b u✝ : V
⊢ nil.support.getLast ⋯ = u✝

case cons
V : Type u
G : SimpleGraph V
a b u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ : p✝.support.getLast ⋯ = w✝
⊢ (cons h✝ p✝).support.getLast ⋯ = w✝
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Basic

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
⊢ v ∈ p.support

Tactic:
induction p

Goal state after:
case nil
V : Type u
G : SimpleGraph V
u v u✝ : V
⊢ u✝ ∈ nil.support

case cons
V : Type u
G : SimpleGraph V
u v u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ : w✝ ∈ p✝.support
⊢ w✝ ∈ (cons h✝ p✝).support
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Basic

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
⊢ u :: List.map (fun x ↦ x.toProd.2) p.darts = p.support

Tactic:
induction p

Goal state after:
case nil
V : Type u
G : SimpleGraph V
u v u✝ : V
⊢ u✝ :: List.map (fun x ↦ x.toProd.2) nil.darts = nil.support

case cons
V : Type u
G : SimpleGraph V
u v u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ : v✝ :: List.map (fun x ↦ x.toProd.2) p✝.darts = p✝.support
⊢ u✝ :: List.map (fun x ↦ x.toProd.2) (cons h✝ p✝).darts = (cons h✝ p✝).support
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Basic

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
⊢ List.map (fun x ↦ x.toProd.1) p.darts ++ [v] = p.support

Tactic:
induction p

Goal state after:
case nil
V : Type u
G : SimpleGraph V
u v u✝ : V
⊢ List.map (fun x ↦ x.toProd.1) nil.darts ++ [u✝] = nil.support

case cons
V : Type u
G : SimpleGraph V
u v u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ : List.map (fun x ↦ x.toProd.1) p✝.darts ++ [w✝] = p✝.support
⊢ List.map (fun x ↦ x.toProd.1) (cons h✝ p✝).darts ++ [w✝] = (cons h✝ p✝).support
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Basic

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
⊢ p.support.length = p.length + 1

Tactic:
induction p

Goal state after:
case nil
V : Type u
G : SimpleGraph V
u v u✝ : V
⊢ nil.support.length = nil.length + 1

case cons
V : Type u
G : SimpleGraph V
u v u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ : p✝.support.length = p✝.length + 1
⊢ (cons h✝ p✝).support.length = (cons h✝ p✝).length + 1
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Basic

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

Tactic:
induction p

Goal state after:
case nil
V : Type u
G : SimpleGraph V
u v u✝ : V
⊢ nil.darts.length = nil.length

case cons
V : Type u
G : SimpleGraph V
u v u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ : p✝.darts.length = p✝.length
⊢ (cons h✝ p✝).darts.length = (cons h✝ p✝).length
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:
rw [card_parts_equitabilise _ _ hm, tsub_add_cancel_of_le a_add_one_le_four_pow_parts_card]

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
⊢ p.support[p.length] = v

Tactic:
induction p

Goal state after:
case nil
V : Type u
G : SimpleGraph V
u v u✝ : V
⊢ nil.support[nil.length] = u✝

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

Tactic:
exact ⟨i, by grind, fun j hj ↦ by grind [fst_darts_getElem, snd_darts_getElem]⟩

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
⊢ Walk.map Hom.id p = p

Tactic:
induction p

Goal state after:
case nil
V : Type u
G : SimpleGraph V
u v u✝ : V
⊢ Walk.map Hom.id nil = nil

case cons
V : Type u
G : SimpleGraph V
u v u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ : Walk.map Hom.id p✝ = p✝
⊢ Walk.map Hom.id (cons h✝ p✝) = cons h✝ p✝
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 : V
p : G.Walk u v
⊢ Walk.map f' (Walk.map f p) = Walk.map (f'.comp f) p

Tactic:
induction p

Goal state after:
case nil
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 : V
p : G.Walk u v
u✝ : V
⊢ Walk.map f' (Walk.map f nil) = Walk.map (f'.comp f) nil

case cons
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 : V
p : G.Walk u v
u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ : Walk.map f' (Walk.map f p✝) = Walk.map (f'.comp f) p✝
⊢ Walk.map f' (Walk.map f (cons h✝ p✝)) = Walk.map (f'.comp f) (cons h✝ p✝)
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Basic

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk u v
⊢ w ∈ p.support ↔ w = v ∨ ∃ e ∈ p.edges, w ∈ e

Tactic:
induction p

Goal state after:
case nil
V : Type u
G : SimpleGraph V
u v w u✝ : V
⊢ w ∈ nil.support ↔ w = u✝ ∨ ∃ e ∈ nil.edges, w ∈ e

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✝
p_ih✝ : w ∈ p✝.support ↔ w = w✝ ∨ ∃ e ∈ p✝.edges, w ∈ e
⊢ w ∈ (cons h✝ p✝).support ↔ w = w✝ ∨ ∃ e ∈ (cons h✝ p✝).edges, w ∈ e
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).length = p.length

Tactic:
induction p

Goal state after:
case nil
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
f : G →g G'
u v : V
p : G.Walk u v
u✝ : V
⊢ (Walk.map f nil).length = nil.length

case cons
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
f : G →g G'
u v : V
p : G.Walk u v
u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ : (Walk.map f p✝).length = p✝.length
⊢ (Walk.map f (cons h✝ p✝)).length = (cons h✝ p✝).length
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 w : V
p : G.Walk u v
q : G.Walk v w
⊢ Walk.map f (p.append q) = (Walk.map f p).append (Walk.map f q)

Tactic:
induction p

Goal state after:
case nil
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
f : G →g G'
u v w u✝ : V
q : G.Walk u✝ w
⊢ Walk.map f (nil.append q) = (Walk.map f nil).append (Walk.map f q)

case cons
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
f : G →g G'
u v w u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ : ∀ (q : G.Walk w✝ w), Walk.map f (p✝.append q) = (Walk.map f p✝).append (Walk.map f q)
q : G.Walk w✝ w
⊢ Walk.map f ((cons h✝ p✝).append q) = (Walk.map f (cons h✝ p✝)).append (Walk.map f q)
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).reverse = Walk.map f p.reverse

Tactic:
induction p

Goal state after:
case nil
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
f : G →g G'
u v : V
p : G.Walk u v
u✝ : V
⊢ (Walk.map f nil).reverse = Walk.map f nil.reverse

case cons
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
f : G →g G'
u v : V
p : G.Walk u v
u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ : (Walk.map f p✝).reverse = Walk.map f p✝.reverse
⊢ (Walk.map f (cons h✝ p✝)).reverse = Walk.map f (cons h✝ p✝).reverse
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).support = List.map (⇑f) p.support

Tactic:
induction p

Goal state after:
case nil
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
f : G →g G'
u v : V
p : G.Walk u v
u✝ : V
⊢ (Walk.map f nil).support = List.map (⇑f) nil.support

case cons
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
f : G →g G'
u v : V
p : G.Walk u v
u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ : (Walk.map f p✝).support = List.map (⇑f) p✝.support
⊢ (Walk.map f (cons h✝ p✝)).support = List.map (⇑f) (cons h✝ p✝).support
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

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

case cons
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
f : G →g G'
u v : V
p : G.Walk u v
u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ : (Walk.map f p✝).darts = List.map f.mapDart p✝.darts
⊢ (Walk.map f (cons h✝ p✝)).darts = List.map f.mapDart (cons h✝ p✝).darts
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

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

case cons
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
f : G →g G'
u v : V
p : G.Walk u v
u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ : (Walk.map f p✝).edges = List.map (Sym2.map ⇑f) p✝.edges
⊢ (Walk.map f (cons h✝ p✝)).edges = List.map (Sym2.map ⇑f) (cons h✝ p✝).edges
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

Goal state after:
case nil
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
u✝ : V
⊢ nil.transfer G ⋯ = nil

case cons
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ : p✝.transfer G ⋯ = p✝
⊢ (cons h✝ p✝).transfer G ⋯ = cons h✝ p✝
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

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

case cons
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
H : SimpleGraph V
GH : G ≤ H
u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ : ∀ (hp : ∀ e ∈ p✝.edges, e ∈ H.edgeSet), p✝.transfer H hp = Walk.map (Hom.ofLE GH) p✝
hp : ∀ e ∈ (cons h✝ p✝).edges, e ∈ H.edgeSet
⊢ (cons h✝ p✝).transfer H hp = Walk.map (Hom.ofLE GH) (cons h✝ p✝)
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

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

case cons
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
H : SimpleGraph V
u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ : ∀ (hp : ∀ e ∈ p✝.edges, e ∈ H.edgeSet), (p✝.transfer H hp).edges = p✝.edges
hp : ∀ e ∈ (cons h✝ p✝).edges, e ∈ H.edgeSet
⊢ ((cons h✝ p✝).transfer H hp).edges = (cons h✝ p✝).edges
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

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

case cons
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
H : SimpleGraph V
u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ : ∀ (hp : ∀ e ∈ p✝.edges, e ∈ H.edgeSet), (p✝.transfer H hp).support = p✝.support
hp : ∀ e ∈ (cons h✝ p✝).edges, e ∈ H.edgeSet
⊢ ((cons h✝ p✝).transfer H hp).support = (cons h✝ p✝).support
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

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

case cons
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
H : SimpleGraph V
u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ : ∀ (hp : ∀ e ∈ p✝.edges, e ∈ H.edgeSet), (p✝.transfer H hp).length = p✝.length
hp : ∀ e ∈ (cons h✝ p✝).edges, e ∈ H.edgeSet
⊢ ((cons h✝ p✝).transfer H hp).length = (cons h✝ p✝).length
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

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

case cons
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
H K : SimpleGraph V
u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ :
  ∀ (hp : ∀ e ∈ p✝.edges, e ∈ H.edgeSet) (hp' : ∀ e ∈ (p✝.transfer H hp).edges, e ∈ K.edgeSet),
    (p✝.transfer H hp).transfer K hp' = p✝.transfer K ⋯
hp : ∀ e ∈ (cons h✝ p✝).edges, e ∈ H.edgeSet
hp' : ∀ e ∈ ((cons h✝ p✝).transfer H hp).edges, e ∈ K.edgeSet
⊢ ((cons h✝ p✝).transfer H hp).transfer K hp' = (cons h✝ p✝).transfer K ⋯
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

Goal state after:
case nil
V : Type u
G : SimpleGraph V
u v u✝ : V
⊢ nil.append nil = nil

case cons
V : Type u
G : SimpleGraph V
u v u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ : p✝.append nil = p✝
⊢ (cons h✝ p✝).append nil = cons h✝ p✝
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

Goal state after:
case nil
V : Type u
G : SimpleGraph V
u v w x : V
r : G.Walk w x
u✝ : V
q : G.Walk u✝ w
⊢ nil.append (q.append r) = (nil.append q).append r

case cons
V : Type u
G : SimpleGraph V
u v w x : V
r : G.Walk w x
u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ : ∀ (q : G.Walk w✝ w), p✝.append (q.append r) = (p✝.append q).append r
q : G.Walk w✝ w
⊢ (cons h✝ p✝).append (q.append r) = ((cons h✝ p✝).append q).append r
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

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

case cons
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
H : SimpleGraph V
w u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ :
  ∀ (q : G.Walk w✝ w) (hpq : ∀ e ∈ (p✝.append q).edges, e ∈ H.edgeSet),
    (p✝.append q).transfer H hpq = (p✝.transfer H ⋯).append (q.transfer H ⋯)
q : G.Walk w✝ w
hpq : ∀ e ∈ ((cons h✝ p✝).append q).edges, e ∈ H.edgeSet
⊢ ((cons h✝ p✝).append q).transfer H hpq = ((cons h✝ p✝).transfer H ⋯).append (q.transfer H ⋯)
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

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

case cons
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
H : SimpleGraph V
u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ : ∀ (hp : ∀ e ∈ p✝.edges, e ∈ H.edgeSet), (p✝.transfer H hp).reverse = p✝.reverse.transfer H ⋯
hp : ∀ e ∈ (cons h✝ p✝).edges, e ∈ H.edgeSet
⊢ ((cons h✝ p✝).transfer H hp).reverse = (cons h✝ p✝).reverse.transfer H ⋯
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
⊢ (p.append q).length = p.length + q.length

Tactic:
induction p

Goal state after:
case nil
V : Type u
G : SimpleGraph V
u v w u✝ : V
q : G.Walk u✝ w
⊢ (nil.append q).length = nil.length + q.length

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✝
p_ih✝ : ∀ (q : G.Walk w✝ w), (p✝.append q).length = p✝.length + q.length
q : G.Walk w✝ w
⊢ ((cons h✝ p✝).append q).length = (cons h✝ p✝).length + q.length
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Decomp

Goal state before:
pp: V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v w : V
p : G.Walk v w
h : u ∈ p.support
⊢ (p.takeUntil u h).append (p.dropUntil u h) = p

Tactic:
induction p

Goal state after:
case nil
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v w u✝ : V
h : u ∈ nil.support
⊢ (nil.takeUntil u h).append (nil.dropUntil u h) = nil

case cons
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v w u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ : ∀ (h : u ∈ p✝.support), (p✝.takeUntil u h).append (p✝.dropUntil u h) = p✝
h : u ∈ (cons h✝ p✝).support
⊢ ((cons h✝ p✝).takeUntil u h).append ((cons h✝ p✝).dropUntil u h) = cons h✝ p✝
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
⊢ (p.concat h).support = p.support ++ [w]

Tactic:
induction p

Goal state after:
case nil
V : Type u
G : SimpleGraph V
u v w u✝ : V
h : G.Adj u✝ w
⊢ (nil.concat h).support = nil.support ++ [w]

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✝
p_ih✝ : ∀ (h : G.Adj w✝ w), (p✝.concat h).support = p✝.support ++ [w]
h : G.Adj w✝ w
⊢ ((cons h✝ p✝).concat h).support = (cons h✝ p✝).support ++ [w]
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Decomp

Goal state before:
pp: V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v w : V
p : G.Walk v w
h : u ∈ p.support
⊢ List.count u (p.takeUntil u h).support = 1

Tactic:
induction p

Goal state after:
case nil
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v w u✝ : V
h : u ∈ nil.support
⊢ List.count u (nil.takeUntil u h).support = 1

case cons
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v w u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ : ∀ (h : u ∈ p✝.support), List.count u (p✝.takeUntil u h).support = 1
h : u ∈ (cons h✝ p✝).support
⊢ List.count u ((cons h✝ p✝).takeUntil u h).support = 1
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').support = p.support ++ p'.support.tail

Tactic:
induction p

Goal state after:
case nil
V : Type u
G : SimpleGraph V
u v w u✝ : V
p' : G.Walk u✝ w
⊢ (nil.append p').support = nil.support ++ p'.support.tail

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✝
p_ih✝ : ∀ (p' : G.Walk w✝ w), (p✝.append p').support = p✝.support ++ p'.support.tail
p' : G.Walk w✝ w
⊢ ((cons h✝ p✝).append p').support = (cons h✝ p✝).support ++ p'.support.tail
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.support = p.support.reverse

Tactic:
induction p

Goal state after:
case nil
V : Type u
G : SimpleGraph V
u v u✝ : V
⊢ nil.reverse.support = nil.support.reverse

case cons
V : Type u
G : SimpleGraph V
u v u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ : p✝.reverse.support = p✝.support.reverse
⊢ (cons h✝ p✝).reverse.support = (cons h✝ p✝).support.reverse