awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Maps
Goal:
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
f : G →g G'
hinj : Function.Injective.{u + 1, v + 1} (α := V) (β := V') (⇑f : (a : V) → V')
u v : V
p p' : G.Walk u v
h : Walk.map f p = Walk.map f p'
nil : ∀ {u : V} ⦃p' : G.Walk u u⦄ (h : Walk.map f Walk.nil = Walk.map f p'), Walk.nil = p'
cons :
  ∀ {u v w : V} (h : G.Adj u v) (p : G.Walk v w) (ih : ∀ ⦃p' : G.Walk v w⦄ (h : Walk.map f p = Walk.map f p'), p = p')
    ⦃p' : G.Walk u w⦄ (h_1 : Walk.map f (Walk.cons h p) = Walk.map f p'), Walk.cons h p = p'
⊢ p = p'

Tactic:
induction p with
  | nil => cases p' <;> simp at h ⊢
  | cons _ _ ih =>
    cases p' with
    | nil => simp at h
    | cons _ _ =>
      simp only [map_cons, cons.injEq] at h
      grind

Premises used: SimpleGraph.Walk.cons.injEq, SimpleGraph.Walk.cons, SimpleGraph.Walk.nil, SimpleGraph.Walk.map_cons
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Maps
Goal:
V : Type u
G G' : SimpleGraph V
h : G ≤ G'
u v : V
p : G.Walk u v
⊢ (mapLe h p).support = p.support

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Maps
Goal:
V : Type u
G G' : SimpleGraph V
h : G ≤ G'
u v : V
p : G.Walk u v
⊢ (mapLe h p).edges = p.edges

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Maps
Goal:
V : Type u
G G' : SimpleGraph V
h : G ≤ G'
u v : V
p : G.Walk u v
⊢ (mapLe h p).edgeSet = p.edgeSet

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Maps
Goal:
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_1 v_1 u' v' w_1 : V
p_1 : G.Walk u_1 v_1
u_2 v_2 : V
p_2 : G.Walk u_2 v_2
H : SimpleGraph V
u w v : V
h_1 : G.Adj u v
p : G.Walk v w
h : ∀ e ∈ (cons' u v w h_1 p).edges, e ∈ H.edgeSet
⊢ s(u, v) ∈ (cons' u v w h_1 p).edges

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Maps
Goal:
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_1 v_1 u' v' w_1 : V
p_1 : G.Walk u_1 v_1
u_2 v_2 : V
p_2 : G.Walk u_2 v_2
H : SimpleGraph V
u w v : V
h_1 : G.Adj u v
p : G.Walk v w
h : ∀ e ∈ (cons' u v w h_1 p).edges, e ∈ H.edgeSet
e : Sym2 V
he : e ∈ p.edges
⊢ e ∈ (cons' u v w h_1 p).edges

Tactic:
simp [he]
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Maps
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
nil : ∀ {u : V}, Eq (α := G.Walk u u) (Walk.transfer Walk.nil G ⋯) Walk.nil
cons : ∀ {u v w : V} (h : G.Adj u v) (p : G.Walk v w), p.transfer G ⋯ = p → (Walk.cons h p).transfer G ⋯ = Walk.cons h p
⊢ p.transfer G ⋯ = p

Tactic:
induction p
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Maps
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
u_1 : V
⊢ Eq (α := G.Walk u_1 u_1) (Walk.transfer nil G ⋯) nil

Tactic:
simp [*]
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Maps
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
u_1 v_1 w : V
h : G.Adj u_1 v_1
p_1 : G.Walk v_1 w
p_ih : p_1.transfer G ⋯ = p_1
⊢ (cons h p_1).transfer G ⋯ = cons h p_1

Tactic:
simp [*]
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Maps
Goal:
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
nil :
  ∀ {u : V}
    (hp : ∀ (e : Sym2 V), Membership.mem (γ := List (Sym2 V)) (edges (G := G) (u := u) Walk.nil) e → e ∈ H.edgeSet),
    Walk.transfer Walk.nil H hp = Walk.map (Hom.ofLE GH) Walk.nil
cons :
  ∀ {u v w : V} (h : G.Adj u v) (p : G.Walk v w),
    (∀ (hp : ∀ e ∈ p.edges, e ∈ H.edgeSet), p.transfer H hp = Walk.map (Hom.ofLE GH) p) →
      ∀ (hp : ∀ e ∈ (Walk.cons h p).edges, e ∈ H.edgeSet),
        (Walk.cons h p).transfer H hp = Walk.map (Hom.ofLE GH) (Walk.cons h p)
⊢ p.transfer H hp = Walk.map (Hom.ofLE GH) p

Tactic:
induction p
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Maps
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
H : SimpleGraph V
GH : G ≤ H
u_1 : V
hp : ∀ (e : Sym2 V), Membership.mem (γ := List (Sym2 V)) (edges (G := G) (u := u_1) nil) e → e ∈ H.edgeSet
⊢ Walk.transfer nil H hp = Walk.map (Hom.ofLE GH) nil

Tactic:
simp [*]
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Maps
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
H : SimpleGraph V
GH : G ≤ H
u_1 v_1 w : V
h : G.Adj u_1 v_1
p_1 : G.Walk v_1 w
p_ih : ∀ (hp : ∀ e ∈ p_1.edges, e ∈ H.edgeSet), p_1.transfer H hp = Walk.map (Hom.ofLE GH) p_1
hp : ∀ e ∈ (cons h p_1).edges, e ∈ H.edgeSet
⊢ (cons h p_1).transfer H hp = Walk.map (Hom.ofLE GH) (cons h p_1)

Tactic:
simp [*]
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Maps
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
H : SimpleGraph V
hp : ∀ e ∈ p.edges, e ∈ H.edgeSet
nil :
  ∀ {u : V}
    (hp : ∀ (e : Sym2 V), Membership.mem (γ := List (Sym2 V)) (edges (G := G) (u := u) Walk.nil) e → e ∈ H.edgeSet),
    (Walk.transfer Walk.nil H hp).edges = edges (G := G) (u := u) Walk.nil
cons :
  ∀ {u v w : V} (h : G.Adj u v) (p : G.Walk v w),
    (∀ (hp : ∀ e ∈ p.edges, e ∈ H.edgeSet), (p.transfer H hp).edges = p.edges) →
      ∀ (hp : ∀ e ∈ (Walk.cons h p).edges, e ∈ H.edgeSet), ((Walk.cons h p).transfer H hp).edges = (Walk.cons h p).edges
⊢ (p.transfer H hp).edges = p.edges

Tactic:
induction p
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Maps
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
H : SimpleGraph V
u_1 : V
hp : ∀ (e : Sym2 V), Membership.mem (γ := List (Sym2 V)) (edges (G := G) (u := u_1) nil) e → e ∈ H.edgeSet
⊢ (Walk.transfer nil H hp).edges = edges (G := G) (u := u_1) nil

Tactic:
simp [*]
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Maps
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
H : SimpleGraph V
u_1 v_1 w : V
h : G.Adj u_1 v_1
p_1 : G.Walk v_1 w
p_ih : ∀ (hp : ∀ e ∈ p_1.edges, e ∈ H.edgeSet), (p_1.transfer H hp).edges = p_1.edges
hp : ∀ e ∈ (cons h p_1).edges, e ∈ H.edgeSet
⊢ ((cons h p_1).transfer H hp).edges = (cons h p_1).edges

Tactic:
simp [*]
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Maps
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
H : SimpleGraph V
hp : ∀ e ∈ p.edges, e ∈ H.edgeSet
h : ∀ (x : Sym2 V), x ∈ (p.transfer H hp).edgeSet ↔ x ∈ p.edgeSet
⊢ (p.transfer H hp).edgeSet = p.edgeSet

Tactic:
ext
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Maps
Goal:
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:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Maps
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
H : SimpleGraph V
hp : ∀ e ∈ p.edges, e ∈ H.edgeSet
nil :
  ∀ {u : V}
    (hp : ∀ (e : Sym2 V), Membership.mem (γ := List (Sym2 V)) (edges (G := G) (u := u) Walk.nil) e → e ∈ H.edgeSet),
    (Walk.transfer Walk.nil H hp).support = support (G := G) (u := u) Walk.nil
cons :
  ∀ {u v w : V} (h : G.Adj u v) (p : G.Walk v w),
    (∀ (hp : ∀ e ∈ p.edges, e ∈ H.edgeSet), (p.transfer H hp).support = p.support) →
      ∀ (hp : ∀ e ∈ (Walk.cons h p).edges, e ∈ H.edgeSet),
        ((Walk.cons h p).transfer H hp).support = (Walk.cons h p).support
⊢ (p.transfer H hp).support = p.support

Tactic:
induction p
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Maps
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
H : SimpleGraph V
u_1 : V
hp : ∀ (e : Sym2 V), Membership.mem (γ := List (Sym2 V)) (edges (G := G) (u := u_1) nil) e → e ∈ H.edgeSet
⊢ (Walk.transfer nil H hp).support = support (G := G) (u := u_1) nil

Tactic:
simp [*]
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Maps
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
H : SimpleGraph V
u_1 v_1 w : V
h : G.Adj u_1 v_1
p_1 : G.Walk v_1 w
p_ih : ∀ (hp : ∀ e ∈ p_1.edges, e ∈ H.edgeSet), (p_1.transfer H hp).support = p_1.support
hp : ∀ e ∈ (cons h p_1).edges, e ∈ H.edgeSet
⊢ ((cons h p_1).transfer H hp).support = (cons h p_1).support

Tactic:
simp [*]
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Maps
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
H : SimpleGraph V
hp : ∀ e ∈ p.edges, e ∈ H.edgeSet
nil :
  ∀ {u : V}
    (hp : ∀ (e : Sym2 V), Membership.mem (γ := List (Sym2 V)) (edges (G := G) (u := u) Walk.nil) e → e ∈ H.edgeSet),
    (Walk.transfer Walk.nil H hp).length = length.{u} (V := V) (G := G) (u := u) Walk.nil
cons :
  ∀ {u v w : V} (h : G.Adj u v) (p : G.Walk v w),
    (∀ (hp : ∀ e ∈ p.edges, e ∈ H.edgeSet), (p.transfer H hp).length = p.length) →
      ∀ (hp : ∀ e ∈ (Walk.cons h p).edges, e ∈ H.edgeSet),
        ((Walk.cons h p).transfer H hp).length = (Walk.cons h p).length
⊢ (p.transfer H hp).length = p.length

Tactic:
induction p
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Maps
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
H : SimpleGraph V
u_1 : V
hp : ∀ (e : Sym2 V), Membership.mem (γ := List (Sym2 V)) (edges (G := G) (u := u_1) nil) e → e ∈ H.edgeSet
⊢ (Walk.transfer nil H hp).length = length.{u} (V := V) (G := G) (u := u_1) nil

Tactic:
simp [*]
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Maps
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
H : SimpleGraph V
u_1 v_1 w : V
h : G.Adj u_1 v_1
p_1 : G.Walk v_1 w
p_ih : ∀ (hp : ∀ e ∈ p_1.edges, e ∈ H.edgeSet), (p_1.transfer H hp).length = p_1.length
hp : ∀ e ∈ (cons h p_1).edges, e ∈ H.edgeSet
⊢ ((cons h p_1).transfer H hp).length = (cons h p_1).length

Tactic:
simp [*]
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Maps
Goal:
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
nil :
  ∀ {u : V}
    (hp : ∀ (e : Sym2 V), Membership.mem (γ := List (Sym2 V)) (edges (G := G) (u := u) Walk.nil) e → e ∈ H.edgeSet)
    (hp' : ∀ e ∈ (Walk.transfer Walk.nil H hp).edges, e ∈ K.edgeSet),
    (Walk.transfer Walk.nil H hp).transfer K hp' = Walk.transfer (G := G) Walk.nil K ⋯
cons :
  ∀ {u v w : V} (h : G.Adj u v) (p : G.Walk v w),
    (∀ (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 ∈ (Walk.cons h p).edges, e ∈ H.edgeSet)
        (hp' : ∀ e ∈ ((Walk.cons h p).transfer H hp).edges, e ∈ K.edgeSet),
        ((Walk.cons h p).transfer H hp).transfer K hp' = (Walk.cons h p).transfer K ⋯
⊢ (p.transfer H hp).transfer K hp' = p.transfer K ⋯

Tactic:
induction p
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Maps
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
H K : SimpleGraph V
u_1 : V
hp : ∀ (e : Sym2 V), Membership.mem (γ := List (Sym2 V)) (edges (G := G) (u := u_1) nil) e → e ∈ H.edgeSet
hp' : ∀ e ∈ (Walk.transfer nil H hp).edges, e ∈ K.edgeSet
⊢ (Walk.transfer nil H hp).transfer K hp' = Walk.transfer (G := G) nil K ⋯

Tactic:
simp [*]
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Maps
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
H K : SimpleGraph V
u_1 v_1 w : V
h : G.Adj u_1 v_1
p_1 : G.Walk v_1 w
p_ih :
  ∀ (hp : ∀ e ∈ p_1.edges, e ∈ H.edgeSet) (hp' : ∀ e ∈ (p_1.transfer H hp).edges, e ∈ K.edgeSet),
    (p_1.transfer H hp).transfer K hp' = p_1.transfer K ⋯
hp : ∀ e ∈ (cons h p_1).edges, e ∈ H.edgeSet
hp' : ∀ e ∈ ((cons h p_1).transfer H hp).edges, e ∈ K.edgeSet
⊢ ((cons h p_1).transfer H hp).transfer K hp' = (cons h p_1).transfer K ⋯

Tactic:
simp [*]
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Maps
Goal:
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_1 : 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
e : Sym2 V
he : e ∈ p.edges
⊢ e ∈ (p.append q).edges

Tactic:
simp [he]
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Maps
Goal:
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_1 : 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
e : Sym2 V
he : e ∈ q.edges
⊢ e ∈ (p.append q).edges

Tactic:
simp [he]
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Maps
Goal:
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
nil :
  ∀ {u : V} (q : G.Walk u w) (hpq : ∀ e ∈ (append Walk.nil q).edges, e ∈ H.edgeSet),
    (append Walk.nil q).transfer H hpq = append (Walk.transfer (G := G) Walk.nil H ⋯) (q.transfer H ⋯)
cons :
  ∀ {u v w_1 : V} (h : G.Adj u v) (p : G.Walk v w_1),
    (∀ (q : G.Walk w_1 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_1 w) (hpq : ∀ e ∈ ((Walk.cons h p).append q).edges, e ∈ H.edgeSet),
        ((Walk.cons h p).append q).transfer H hpq = ((Walk.cons h p).transfer H ⋯).append (q.transfer H ⋯)
⊢ (p.append q).transfer H hpq = (p.transfer H ⋯).append (q.transfer H ⋯)

Tactic:
induction p
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Maps
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
H : SimpleGraph V
w u_1 : V
q : G.Walk u_1 w
hpq : ∀ e ∈ (append nil q).edges, e ∈ H.edgeSet
⊢ (append nil q).transfer H hpq = append (Walk.transfer (G := G) nil H ⋯) (q.transfer H ⋯)

Tactic:
simp [*]
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Maps
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
H : SimpleGraph V
w u_1 v_1 w_1 : V
h : G.Adj u_1 v_1
p_1 : G.Walk v_1 w_1
p_ih :
  ∀ (q : G.Walk w_1 w) (hpq : ∀ e ∈ (p_1.append q).edges, e ∈ H.edgeSet),
    (p_1.append q).transfer H hpq = (p_1.transfer H ⋯).append (q.transfer H ⋯)
q : G.Walk w_1 w
hpq : ∀ e ∈ ((cons h p_1).append q).edges, e ∈ H.edgeSet
⊢ ((cons h p_1).append q).transfer H hpq = ((cons h p_1).transfer H ⋯).append (q.transfer H ⋯)

Tactic:
simp [*]
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Maps
Goal:
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 simp : ∀ e ∈ p.edges, e ∈ H.edgeSet
⊢ ∀ e ∈ p.reverse.edges, e ∈ H.edgeSet

Tactic:
simp only [edges_reverse, List.mem_reverse]

Premises used: List.mem_reverse, SimpleGraph.Walk.edges_reverse
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Maps
Goal:
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:
hp
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Maps
Goal:
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:
exact hp
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Maps
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
H : SimpleGraph V
hp : ∀ e ∈ p.edges, e ∈ H.edgeSet
nil :
  ∀ {u : V}
    (hp : ∀ (e : Sym2 V), Membership.mem (γ := List (Sym2 V)) (edges (G := G) (u := u) Walk.nil) e → e ∈ H.edgeSet),
    (Walk.transfer Walk.nil H hp).reverse = Walk.transfer (reverse Walk.nil) H ⋯
cons :
  ∀ {u v w : V} (h : G.Adj u v) (p : G.Walk v w),
    (∀ (hp : ∀ e ∈ p.edges, e ∈ H.edgeSet), (p.transfer H hp).reverse = p.reverse.transfer H ⋯) →
      ∀ (hp : ∀ e ∈ (Walk.cons h p).edges, e ∈ H.edgeSet),
        ((Walk.cons h p).transfer H hp).reverse = (Walk.cons h p).reverse.transfer H ⋯
⊢ (p.transfer H hp).reverse = p.reverse.transfer H ⋯

Tactic:
induction p
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Maps
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
H : SimpleGraph V
u_1 : V
hp : ∀ (e : Sym2 V), Membership.mem (γ := List (Sym2 V)) (edges (G := G) (u := u_1) nil) e → e ∈ H.edgeSet
⊢ (Walk.transfer nil H hp).reverse = Walk.transfer (reverse nil) H ⋯

Tactic:
simp [*]
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Maps
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
H : SimpleGraph V
u_1 v_1 w : V
h : G.Adj u_1 v_1
p_1 : G.Walk v_1 w
p_ih : ∀ (hp : ∀ e ∈ p_1.edges, e ∈ H.edgeSet), (p_1.transfer H hp).reverse = p_1.reverse.transfer H ⋯
hp : ∀ e ∈ (cons h p_1).edges, e ∈ H.edgeSet
⊢ ((cons h p_1).transfer H hp).reverse = (cons h p_1).reverse.transfer H ⋯

Tactic:
simp [*]
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Maps
Goal:
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_1 v_1 u'_1 v' w_1 : V
p : G.Walk u_1 v_1
H : SimpleGraph V
s s' : Set V
u v_2 v u' : V
huu' : G.Adj u u'
w : G.Walk u' v
hw : ∀ x ∈ (cons huu' w).support, x ∈ s
⊢ ∀ x ∈ w.support, x ∈ s

Tactic:
simp_all
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Maps
Goal:
V : Type u
G : SimpleGraph V
u : V
s : Set V
hw : ∀ (x : V), Membership.mem (γ := List V) (support (G := G) (u := u) nil) x → x ∈ s
⊢ Walk.induce s nil hw = nil

Tactic:
rfl

Premises used: SimpleGraph.Walk.induce, rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Maps
Goal:
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_1 : V
p : G.Walk u v
H : SimpleGraph V
s s' : Set V
huu' : G.Adj u u'
w : G.Walk u' v
hw : ∀ x ∈ (cons huu' w).support, x ∈ s
⊢ ∀ x ∈ w.support, x ∈ s

Tactic:
simp_all
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Maps
Goal:
V : Type u
G : SimpleGraph V
u v u' : V
s : Set V
huu' : G.Adj u u'
w : G.Walk u' v
hw : ∀ x ∈ (cons huu' w).support, x ∈ s
⊢ Walk.induce s (cons huu' w) hw = cons (v := Subtype.mk (p := fun (x : V) ↦ x ∈ s) u' ⋯) ⋯ (Walk.induce s w ⋯)

Tactic:
rfl

Premises used: SimpleGraph.Walk.induce, rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Maps
Goal:
V : Type u
G : SimpleGraph V
s : Set V
u v_1 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:
simp [support_induce]
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Maps
Goal:
V : Type u
G : SimpleGraph V
s : Set V
u v_1 v u' : V
huu' : G.Adj u u'
w : G.Walk u' v
hw : ∀ x ∈ (cons huu' w).support, x ∈ s
⊢ Walk.map (Embedding.toHom (Embedding.induce s)) (Walk.induce s (cons huu' w) hw) = cons huu' w

Tactic:
simp [map_induce]
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Maps
Goal:
V : Type u
G : SimpleGraph V
s s' : Set V
hs : s ⊆ s'
u v_1 v u' : V
huu' : G.Adj u u'
w : G.Walk u' v
hw : ∀ x ∈ (cons huu' w).support, x ∈ s
⊢ Walk.map (G.induceHomOfLE (s := s) (s' := s') hs).toHom (Walk.induce s (cons huu' w) hw) =
    Walk.induce s' (cons huu' w) ⋯

Tactic:
simp [map_induce_induceHomOfLE]
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Maps
Goal:
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_1 u' v' w_1 : V
p_1 : G.Walk u v_1
H : SimpleGraph V
s_1 s' : Set V
s : Set (Sym2 V)
v w : V
p : G.Walk v w
hp : ∀ e ∈ p.edges, e ∉ s
simp : ∀ e ∈ p.edges, e ∈ G.edgeSet ∧ e ∉ s
⊢ ∀ e ∈ p.edges, e ∈ (G.deleteEdges s).edgeSet

Tactic:
simp only [edgeSet_deleteEdges, Set.mem_diff]

Premises used: Set.mem_diff, SimpleGraph.edgeSet_deleteEdges
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Maps
Goal:
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_1 u' v' w_1 : V
p_1 : G.Walk u v_1
H : SimpleGraph V
s_1 s' : Set V
s : Set (Sym2 V)
v w : V
p : G.Walk v w
hp : ∀ e ∈ p.edges, e ∉ s
⊢ ∀ e ∈ p.edges, e ∈ G.edgeSet ∧ e ∉ s

Tactic:
fun e ep => ⟨edges_subset_edgeSet p ep, hp e ep⟩

Premises used: And.intro, SimpleGraph.Walk.edges_subset_edgeSet
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Maps
Goal:
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_1 u' v' w_1 : V
p_1 : G.Walk u v_1
H : SimpleGraph V
s_1 s' : Set V
s : Set (Sym2 V)
v w : V
p : G.Walk v w
hp : ∀ e ∈ p.edges, e ∉ s
⊢ ∀ e ∈ p.edges, e ∈ G.edgeSet ∧ e ∉ s

Tactic:
exact fun e ep => ⟨edges_subset_edgeSet p ep, hp e ep⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Maps
Goal:
V : Type u
G : SimpleGraph V
s : Set (Sym2 V)
v : V
hp : ∀ (e : Sym2 V), Membership.mem (γ := List (Sym2 V)) (edges (G := G) (u := v) nil) e → e ∉ s
⊢ toDeleteEdges s nil hp = nil

Tactic:
rfl

Premises used: SimpleGraph.Walk.transfer, rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Maps
Goal:
V : Type u
G : SimpleGraph V
s : Set (Sym2 V)
u v w : V
h : G.Adj u v
p : G.Walk v w
hp : ∀ e ∈ (cons h p).edges, e ∉ s
⊢ toDeleteEdges s (cons h p) hp = cons ⋯ (toDeleteEdges s p ⋯)

Tactic:
rfl

Premises used: SimpleGraph.Walk.transfer, rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Maps
Goal:
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_1 : 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
contrapose : Membership.mem (γ := Set (Sym2 V)) {e} x → x ∉ p.edges
⊢ x ∈ p.edges → x ∉ {e}

Tactic:
contrapose
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Maps
Goal:
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_1 : 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
⊢ Membership.mem (γ := Set (Sym2 V)) {e} x → x ∉ p.edges

Tactic:
simp +contextual [hp]
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Maps
Goal:
V : Type u
G : SimpleGraph V
v w : V
s : Set (Sym2 V)
p : G.Walk v w
hp : ∀ e ∈ p.edges, e ∉ s
hp₁ : ∀ e ∈ (toDeleteEdges s p hp).edges, e ∈ G.edgeSet
⊢ Walk.map (Hom.ofLE ⋯) (toDeleteEdges s p hp) = p

Tactic:
rw [← transfer_eq_map_ofLE, transfer_transfer, transfer_self]

Premises used: SimpleGraph.Walk.transfer_eq_map_ofLE, SimpleGraph.Walk.transfer_transfer, SimpleGraph.Walk.transfer_self
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Maps
Goal:
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:
apply edges_transfer _ _ ▸ p.edges_subset_edgeSet
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
⊢ p.copy ⋯ ⋯ = p

Tactic:
rfl

Premises used: SimpleGraph.Walk.copy, rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
u v u' v' u'' v'' : V
p : G.Walk u v
hu : u = u'
hv : v = v'
hu' : u' = u''
hv' : v' = v''
subst_vars : ∀ (p : G.Walk u'' v''), (p.copy ⋯ ⋯).copy ⋯ ⋯ = p.copy ⋯ ⋯
⊢ (p.copy hu hv).copy hu' hv' = p.copy ⋯ ⋯

Tactic:
subst_vars
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
u'' v'' : V
p : G.Walk u'' v''
⊢ (p.copy ⋯ ⋯).copy ⋯ ⋯ = p.copy ⋯ ⋯

Tactic:
rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
u u' : V
hu : u = u'
subst_vars : Eq (α := G.Walk u' u') (Walk.copy nil ⋯ ⋯) nil
⊢ Eq (α := G.Walk u' u') (Walk.copy nil hu hu) nil

Tactic:
subst_vars
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
u' : V
⊢ Eq (α := G.Walk u' u') (Walk.copy nil ⋯ ⋯) nil

Tactic:
rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
u v w u' w' : V
h : G.Adj u v
p : G.Walk v w
hu : u = u'
hw : w = w'
subst_vars : ∀ (h : G.Adj u' v) (p : G.Walk v w'), (cons h p).copy ⋯ ⋯ = cons ⋯ (p.copy ⋯ ⋯)
⊢ (cons h p).copy hu hw = cons ⋯ (p.copy ⋯ hw)

Tactic:
subst_vars
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
v u' w' : V
h : G.Adj u' v
p : G.Walk v w'
⊢ (cons h p).copy ⋯ ⋯ = cons ⋯ (p.copy ⋯ ⋯)

Tactic:
rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
u v w v' w' : V
h : G.Adj u v
p : G.Walk v' w'
hv : v' = v
hw : w' = w
subst_vars : ∀ (h : G.Adj u v'), cons h (p.copy ⋯ ⋯) = Walk.copy (cons ⋯ p) ⋯ ⋯
⊢ cons h (p.copy hv hw) = Walk.copy (cons ⋯ p) ⋯ hw

Tactic:
subst_vars