awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Decomp
Goal:
V : Type u
G : SimpleGraph V
v : V
inst : DecidableEq V
c : G.Walk v v
u : V
h : u ∈ c.support
⊢ (c.rotate u h).edges ~r c.edges

Tactic:
(rotate_darts c u h).map _

Premises used: List.IsRotated.map, SimpleGraph.Walk.edges, SimpleGraph.Walk.rotate_darts
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Decomp
Goal:
V : Type u
G : SimpleGraph V
v : V
inst : DecidableEq V
c : G.Walk v v
u : V
h : u ∈ c.support
⊢ (c.rotate u h).length = c.length

Tactic:
simpa using (rotate_edges c u h).perm.length_eq

Premises used: SimpleGraph.Walk.rotate_edges, List.Perm.length_eq, List.IsRotated.perm
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Decomp
Goal:
V : Type u
G : SimpleGraph V
v u : V
inst : DecidableEq V
c : G.Walk v v
h : u ∈ c.support
⊢ (c.rotate u h).Nil ↔ c.Nil

Tactic:
simp [← length_eq_zero_iff]

Premises used: SimpleGraph.Walk.length_eq_zero_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Decomp
Goal:
V : Type u
G : SimpleGraph V
v u : V
inst : DecidableEq V
c : G.Walk v v
h : u ∈ c.support
⊢ c.rotate u h = nil ↔ c = nil

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Decomp
Goal:
V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk v w
⊢ u ∈ p.support ↔ ∃ (n : ℕ), p.getVert n = u ∧ n ≤ p.length

Tactic:
Iff.intro
    (fun h ↦ ⟨_, p.getVert_length_takeUntil h, p.length_takeUntil_le h⟩)
    (fun ⟨_, h, _⟩ ↦ h ▸ getVert_mem_support _ _)

Premises used: SimpleGraph.Walk.length, SimpleGraph.Walk.length_takeUntil_le, SimpleGraph.Walk.support, Membership.mem, Eq.rec, SimpleGraph.Walk.getVert_mem_support, And.intro, Iff.intro, Exists.intro, SimpleGraph.Walk.takeUntil, _private.0.SimpleGraph.Walk.mem_support_iff_exists_getVert.match_1, SimpleGraph.Walk.getVert_length_takeUntil
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Decomp
Goal:
V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk v w
⊢ u ∈ p.support ↔ ∃ (n : ℕ), p.getVert n = u ∧ n ≤ p.length

Tactic:
exact Iff.intro
    (fun h ↦ ⟨_, p.getVert_length_takeUntil h, p.length_takeUntil_le h⟩)
    (fun ⟨_, h, _⟩ ↦ h ▸ getVert_mem_support _ _)

Premises used: Iff.intro
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Decomp
Goal:
V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk v w
⊢ u ∈ p.support ↔ ∃ (n : ℕ), p.getVert n = u ∧ n ≤ p.length

Tactic:
classical
  exact Iff.intro
    (fun h ↦ ⟨_, p.getVert_length_takeUntil h, p.length_takeUntil_le h⟩)
    (fun ⟨_, h, _⟩ ↦ h ▸ getVert_mem_support _ _)

Premises used: Iff.intro
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Maps
Goal:
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
f : G →g G'
u : V
⊢ Eq (α := G'.Walk ((f : (a : V) → V') u) ((f : (a : V) → V') u)) (Walk.map f nil) nil

Tactic:
rfl

Premises used: SimpleGraph.Walk.map, rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Maps
Goal:
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
f : G →g G'
u v : V
p : G.Walk u v
w : V
h : G.Adj w u
⊢ Walk.map f (cons h p) = cons ⋯ (Walk.map f p)

Tactic:
rfl

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

Tactic:
subst_vars
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Maps
Goal:
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.copy ⋯ ⋯) = (Walk.map f p).copy ⋯ ⋯

Tactic:
rfl
-- 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.{u + 1} (α := G.Walk ((Hom.id : (a : V) → V) u) ((Hom.id : (a : V) → V) u)) (Walk.map Hom.id Walk.nil) Walk.nil
cons :
  ∀ {u v w : V} (h : G.Adj u v) (p : G.Walk v w),
    Walk.map Hom.id p = p → Walk.map Hom.id (Walk.cons h p) = Walk.cons h p
⊢ Walk.map Hom.id p = p

Tactic:
induction p
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Maps
Goal:
V : Type u
G : SimpleGraph V
u v u_1 : V
⊢ Eq.{u + 1} (α := G.Walk ((Hom.id : (a : V) → V) u_1) ((Hom.id : (a : V) → V) u_1)) (Walk.map Hom.id nil) nil

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

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 : V
p : G.Walk u v
nil :
  ∀ {u : V},
    Eq (α :=
      G''.Walk ((f' : (a : V') → V'') ((f : (a : V) → V') u : V')) ((f' : (a : V') → V'') ((f : (a : V) → V') u : V')))
      (Walk.map f' (Walk.map f Walk.nil)) (Walk.map (f'.comp f) Walk.nil)
cons :
  ∀ {u v w : V} (h : G.Adj u v) (p : G.Walk v w),
    Walk.map f' (Walk.map f p) = Walk.map (f'.comp f) p →
      Walk.map f' (Walk.map f (Walk.cons h p)) = Walk.map (f'.comp f) (Walk.cons h p)
⊢ Walk.map f' (Walk.map f p) = Walk.map (f'.comp f) p

Tactic:
induction p
-- 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 : V
p : G.Walk u v
u_1 : V
⊢ Eq (α :=
    G''.Walk ((f' : (a : V') → V'') ((f : (a : V) → V') u_1 : V'))
      ((f' : (a : V') → V'') ((f : (a : V) → V') u_1 : V')))
    (Walk.map f' (Walk.map f nil)) (Walk.map (f'.comp f) nil)

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 : 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 : Walk.map f' (Walk.map f p_1) = Walk.map (f'.comp f) p_1
⊢ Walk.map f' (Walk.map f (cons h p_1)) = Walk.map (f'.comp f) (cons h p_1)

Tactic:
simp [*]
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Maps
Goal:
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
u v : V
p : G.Walk u v
f f' : G →g G'
h : f = f'
subst_vars : Walk.map f' p = (Walk.map f' p).copy ⋯ ⋯
⊢ Walk.map f p = (Walk.map f' p).copy ⋯ ⋯

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

Tactic:
rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Maps
Goal:
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
f : G →g G'
u v : V
p : G.Walk u v
nil : Nil (v := (f : (a : V) → V') u) (Walk.map f Walk.nil) ↔ Nil.{u} (V := V) (G := G) (v := u) Walk.nil
cons : ∀ {v_1 : V} (h : G.Adj u v_1) (p : G.Walk v_1 v), (Walk.map f (Walk.cons h p)).Nil ↔ (Walk.cons h p).Nil
⊢ (Walk.map f p).Nil ↔ p.Nil

Tactic:
cases p
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Maps
Goal:
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
f : G →g G'
u : V
⊢ Nil (v := (f : (a : V) → V') u) (Walk.map f nil) ↔ Nil.{u} (V := V) (G := G) (v := u) nil

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Maps
Goal:
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
f : G →g G'
u v v_1 : V
h : G.Adj u v_1
p : G.Walk v_1 v
⊢ (Walk.map f (cons h p)).Nil ↔ (cons h p).Nil

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Maps
Goal:
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
f : G →g G'
u : V
p : G.Walk u u
nil :
  Eq (α := G'.Walk ((f : (a : V) → V') u) ((f : (a : V) → V') u)) (Walk.map f Walk.nil) Walk.nil ↔
    Eq.{u + 1} (α := G.Walk u u) Walk.nil Walk.nil
cons : ∀ {v : V} (h : G.Adj u v) (p : G.Walk v u), Walk.map f (Walk.cons h p) = Walk.nil ↔ Walk.cons h p = Walk.nil
⊢ Walk.map f p = Walk.nil ↔ p = Walk.nil

Tactic:
cases p
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Maps
Goal:
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
f : G →g G'
u : V
⊢ Eq (α := G'.Walk ((f : (a : V) → V') u) ((f : (a : V) → V') u)) (Walk.map f nil) nil ↔
    Eq.{u + 1} (α := G.Walk u u) nil nil

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Maps
Goal:
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
f : G →g G'
u v : V
h : G.Adj u v
p : G.Walk v u
⊢ Walk.map f (cons h p) = nil ↔ cons h p = nil

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Maps
Goal:
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
f : G →g G'
u v : V
p : G.Walk u v
nil :
  ∀ {u : V}, length (u := (f : (a : V) → V') u) (Walk.map f Walk.nil) = 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),
    (Walk.map f p).length = p.length → (Walk.map f (Walk.cons h p)).length = (Walk.cons h p).length
⊢ (Walk.map f p).length = p.length

Tactic:
induction p
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Maps
Goal:
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_1 : V
⊢ length (u := (f : (a : V) → V') u_1) (Walk.map f nil) = length.{u} (V := V) (G := G) (u := u_1) nil

Tactic:
simp [*]
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Maps
Goal:
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_1 v_1 w : V
h : G.Adj u_1 v_1
p_1 : G.Walk v_1 w
p_ih : (Walk.map f p_1).length = p_1.length
⊢ (Walk.map f (cons h p_1)).length = (cons h p_1).length

Tactic:
simp [*]
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Maps
Goal:
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
nil : ∀ {u : V} (q : G.Walk u w), Walk.map f (append Walk.nil q) = append (Walk.map f Walk.nil) (Walk.map f q)
cons :
  ∀ {u v w_1 : V} (h : G.Adj u v) (p : G.Walk v w_1),
    (∀ (q : G.Walk w_1 w), Walk.map f (p.append q) = (Walk.map f p).append (Walk.map f q)) →
      ∀ (q : G.Walk w_1 w), Walk.map f ((Walk.cons h p).append q) = (Walk.map f (Walk.cons h p)).append (Walk.map f q)
⊢ Walk.map f (p.append q) = (Walk.map f p).append (Walk.map f q)

Tactic:
induction p
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Maps
Goal:
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
f : G →g G'
u v w u_1 : V
q : G.Walk u_1 w
⊢ Walk.map f (append nil q) = append (Walk.map f nil) (Walk.map f q)

Tactic:
simp [*]
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Maps
Goal:
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
f : G →g G'
u v w u_1 v_1 w_1 : V
h : G.Adj u_1 v_1
p : G.Walk v_1 w_1
p_ih : ∀ (q : G.Walk w_1 w), Walk.map f (p.append q) = (Walk.map f p).append (Walk.map f q)
q : G.Walk w_1 w
⊢ Walk.map f ((cons h p).append q) = (Walk.map f (cons h p)).append (Walk.map f q)

Tactic:
simp [*]
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Maps
Goal:
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
f : G →g G'
u v : V
p : G.Walk u v
nil :
  ∀ {u : V},
    Eq (α := G'.Walk ((f : (a : V) → V') u) ((f : (a : V) → V') u)) (reverse (Walk.map f Walk.nil))
      (Walk.map f (reverse Walk.nil))
cons :
  ∀ {u v w : V} (h : G.Adj u v) (p : G.Walk v w),
    (Walk.map f p).reverse = Walk.map f p.reverse →
      (Walk.map f (Walk.cons h p)).reverse = Walk.map f (Walk.cons h p).reverse
⊢ (Walk.map f p).reverse = Walk.map f p.reverse

Tactic:
induction p
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Maps
Goal:
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_1 : V
⊢ Eq (α := G'.Walk ((f : (a : V) → V') u_1) ((f : (a : V) → V') u_1)) (reverse (Walk.map f nil))
    (Walk.map f (reverse nil))

Tactic:
simp [map_append, *]

Premises used: SimpleGraph.Walk.map_append
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Maps
Goal:
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_1 v_1 w : V
h : G.Adj u_1 v_1
p_1 : G.Walk v_1 w
p_ih : (Walk.map f p_1).reverse = Walk.map f p_1.reverse
⊢ (Walk.map f (cons h p_1)).reverse = Walk.map f (cons h p_1).reverse

Tactic:
simp [map_append, *]

Premises used: SimpleGraph.Walk.map_append
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Maps
Goal:
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
f : G →g G'
u v : V
p : G.Walk u v
nil :
  ∀ {u : V},
    support (u := (f : (a : V) → V') u) (Walk.map f Walk.nil) =
      List.map.{u, v} (α := V) (⇑f : (a : V) → V') (support (G := G) (u := u) Walk.nil)
cons :
  ∀ {u v w : V} (h : G.Adj u v) (p : G.Walk v w),
    (Walk.map f p).support = List.map (⇑f : (a : V) → V') p.support →
      (Walk.map f (Walk.cons h p)).support = List.map (⇑f : (a : V) → V') (Walk.cons h p).support
⊢ (Walk.map f p).support = List.map (⇑f : (a : V) → V') p.support

Tactic:
induction p
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Maps
Goal:
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_1 : V
⊢ support (u := (f : (a : V) → V') u_1) (Walk.map f nil) =
    List.map.{u, v} (α := V) (⇑f : (a : V) → V') (support (G := G) (u := u_1) nil)

Tactic:
simp [*]
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Maps
Goal:
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_1 v_1 w : V
h : G.Adj u_1 v_1
p_1 : G.Walk v_1 w
p_ih : (Walk.map f p_1).support = List.map (⇑f : (a : V) → V') p_1.support
⊢ (Walk.map f (cons h p_1)).support = List.map (⇑f : (a : V) → V') (cons h p_1).support

Tactic:
simp [*]
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Maps
Goal:
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
f : G →g G'
u v : V
p : G.Walk u v
nil : ∀ {u : V}, darts (u := (f : (a : V) → V') u) (Walk.map f Walk.nil) = List.map f.mapDart (darts (u := u) Walk.nil)
cons :
  ∀ {u v w : V} (h : G.Adj u v) (p : G.Walk v w),
    (Walk.map f p).darts = List.map f.mapDart p.darts →
      (Walk.map f (Walk.cons h p)).darts = List.map f.mapDart (Walk.cons h p).darts
⊢ (Walk.map f p).darts = List.map f.mapDart p.darts

Tactic:
induction p
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Maps
Goal:
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_1 : V
⊢ darts (u := (f : (a : V) → V') u_1) (Walk.map f nil) = List.map f.mapDart (darts (u := u_1) nil)

Tactic:
simp [*]
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Maps
Goal:
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_1 v_1 w : V
h : G.Adj u_1 v_1
p_1 : G.Walk v_1 w
p_ih : (Walk.map f p_1).darts = List.map f.mapDart p_1.darts
⊢ (Walk.map f (cons h p_1)).darts = List.map f.mapDart (cons h p_1).darts

Tactic:
simp [*]
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Maps
Goal:
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
f : G →g G'
u v : V
p : G.Walk u v
nil :
  ∀ {u : V},
    edges (u := (f : (a : V) → V') u) (Walk.map f Walk.nil) =
      List.map.{u, v} (α := Sym2 V) (Sym2.map (⇑f : (a : V) → V')) (edges (G := G) (u := u) Walk.nil)
cons :
  ∀ {u v w : V} (h : G.Adj u v) (p : G.Walk v w),
    (Walk.map f p).edges = List.map (Sym2.map (⇑f : (a : V) → V')) p.edges →
      (Walk.map f (Walk.cons h p)).edges = List.map (Sym2.map (⇑f : (a : V) → V')) (Walk.cons h p).edges
⊢ (Walk.map f p).edges = List.map (Sym2.map (⇑f : (a : V) → V')) p.edges

Tactic:
induction p
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Maps
Goal:
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_1 : V
⊢ edges (u := (f : (a : V) → V') u_1) (Walk.map f nil) =
    List.map.{u, v} (α := Sym2 V) (Sym2.map (⇑f : (a : V) → V')) (edges (G := G) (u := u_1) nil)

Tactic:
simp [*]
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Maps
Goal:
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_1 v_1 w : V
h : G.Adj u_1 v_1
p_1 : G.Walk v_1 w
p_ih : (Walk.map f p_1).edges = List.map (Sym2.map (⇑f : (a : V) → V')) p_1.edges
⊢ (Walk.map f (cons h p_1)).edges = List.map (Sym2.map (⇑f : (a : V) → V')) (cons h p_1).edges

Tactic:
simp [*]
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Maps
Goal:
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
f : G →g G'
u v : V
p : G.Walk u v
h :
  ∀ (x : Sym2 V'),
    x ∈ (Walk.map f p).edgeSet ↔ Membership.mem (γ := Set (Sym2 V')) (Sym2.map (⇑f : (a : V) → V') '' p.edgeSet) x
⊢ (Walk.map f p).edgeSet = Sym2.map (⇑f : (a : V) → V') '' p.edgeSet

Tactic:
ext
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Maps
Goal:
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 ↔ Membership.mem (γ := Set (Sym2 V')) (Sym2.map (⇑f : (a : V) → V') '' p.edgeSet) x

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Maps
Goal:
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
f : G →g G'
u v : V
p : G.Walk u v
n : ℕ
nil :
  ∀ {u : V} (n : ℕ),
    getVert (u := (f : (a : V) → V') u) (Walk.map f Walk.nil) n =
      (f : (a : V) → V') (getVert (G := G) (u := u) Walk.nil n)
cons :
  ∀ {u v w : V} (h : G.Adj u v) (p : G.Walk v w),
    (∀ (n : ℕ), (Walk.map f p).getVert n = (f : (a : V) → V') (p.getVert n)) →
      ∀ (n : ℕ), (Walk.map f (Walk.cons h p)).getVert n = (f : (a : V) → V') ((Walk.cons h p).getVert n)
⊢ (Walk.map f p).getVert n = (f : (a : V) → V') (p.getVert n)

Tactic:
induction p generalizing n
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Maps
Goal:
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_1 : V
n : ℕ
nil :
  getVert (u := (f : (a : V) → V') u_1) (Walk.map f Walk.nil) 0 =
    (f : (a : V) → V') (getVert (G := G) (u := u_1) Walk.nil 0)
nil₁ :
  ∀ (n : ℕ),
    getVert (u := (f : (a : V) → V') u_1) (Walk.map f Walk.nil) (n + 1) =
      (f : (a : V) → V') (getVert (G := G) (u := u_1) Walk.nil (n + 1))
⊢ getVert (u := (f : (a : V) → V') u_1) (Walk.map f Walk.nil) n =
    (f : (a : V) → V') (getVert (G := G) (u := u_1) Walk.nil n)

Tactic:
cases n
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Maps
Goal:
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_1 v_1 w : V
h : G.Adj u_1 v_1
p_1 : G.Walk v_1 w
p_ih : ∀ (n : ℕ), (Walk.map f p_1).getVert n = (f : (a : V) → V') (p_1.getVert n)
n : ℕ
cons : (Walk.map f (Walk.cons h p_1)).getVert 0 = (f : (a : V) → V') ((Walk.cons h p_1).getVert 0)
cons₁ :
  ∀ (n : ℕ), (Walk.map f (Walk.cons h p_1)).getVert (n + 1) = (f : (a : V) → V') ((Walk.cons h p_1).getVert (n + 1))
⊢ (Walk.map f (Walk.cons h p_1)).getVert n = (f : (a : V) → V') ((Walk.cons h p_1).getVert n)

Tactic:
cases n
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Maps
Goal:
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_1 : V
⊢ getVert (u := (f : (a : V) → V') u_1) (Walk.map f nil) 0 = (f : (a : V) → V') (getVert (G := G) (u := u_1) nil 0)

Tactic:
simp [*]
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Maps
Goal:
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_1 : V
n : ℕ
⊢ getVert (u := (f : (a : V) → V') u_1) (Walk.map f nil) (n + 1) =
    (f : (a : V) → V') (getVert (G := G) (u := u_1) nil (n + 1))

Tactic:
simp [*]
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Maps
Goal:
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_1 v_1 w : V
h : G.Adj u_1 v_1
p_1 : G.Walk v_1 w
p_ih : ∀ (n : ℕ), (Walk.map f p_1).getVert n = (f : (a : V) → V') (p_1.getVert n)
⊢ (Walk.map f (cons h p_1)).getVert 0 = (f : (a : V) → V') ((cons h p_1).getVert 0)

Tactic:
simp [*]
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Maps
Goal:
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_1 v_1 w : V
h : G.Adj u_1 v_1
p_1 : G.Walk v_1 w
p_ih : ∀ (n : ℕ), (Walk.map f p_1).getVert n = (f : (a : V) → V') (p_1.getVert n)
n : ℕ
⊢ (Walk.map f (cons h p_1)).getVert (n + 1) = (f : (a : V) → V') ((cons h p_1).getVert (n + 1))

Tactic:
simp [*]
-- 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 u_1 : V
p' : G.Walk u_1 u_1
h : Walk.map f Walk.nil = Walk.map f p'
nil :
  ∀
    (h :
      Eq (α := G'.Walk ((f : (a : V) → V') u_1) ((f : (a : V) → V') u_1)) (Walk.map f Walk.nil) (Walk.map f Walk.nil)),
    Eq.{u + 1} (α := G.Walk u_1 u_1) Walk.nil Walk.nil
nil₁ :
  ∀ {v : V} (h : G.Adj u_1 v) (p : G.Walk v u_1) (h_1 : Walk.map f Walk.nil = Walk.map f (cons h p)),
    Walk.nil = cons h p
⊢ Walk.nil = p'

Tactic:
cases p'
-- 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 u_1 : V
h : Eq (α := G'.Walk ((f : (a : V) → V') u_1) ((f : (a : V) → V') u_1)) (Walk.map f nil) (Walk.map f nil)
⊢ Eq.{u + 1} (α := G.Walk u_1 u_1) nil nil

Tactic:
simp at h ⊢
-- 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 u_1 v_1 : V
h_1 : G.Adj u_1 v_1
p : G.Walk v_1 u_1
h : Walk.map f nil = Walk.map f (cons h_1 p)
⊢ nil = cons h_1 p

Tactic:
simp at h ⊢
-- 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 u_1 v_1 : V
h_1 : G.Adj u_1 v_1
p : G.Walk v_1 u_1
ih : ∀ ⦃p' : G.Walk v_1 u_1⦄ (h : Walk.map f p = Walk.map f p'), p = p'
h : Walk.map f (cons h_1 p) = Walk.map f nil
⊢ cons h_1 p = nil

Tactic:
simp at h
-- 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 u_1 v_1 w : V
h_1 : G.Adj u_1 v_1
p : G.Walk v_1 w
ih : ∀ ⦃p' : G.Walk v_1 w⦄ (h : Walk.map f p = Walk.map f p'), p = p'
v_2 : V
h_2 : G.Adj u_1 v_2
p_1 : G.Walk v_2 w
h : Walk.map f (cons h_1 p) = Walk.map f (cons h_2 p_1)
⊢ Eq.{v + 1} (α := V') ((f : (a : V) → V') v_1 : V') ((f : (a : V) → V') v_2 : V') ∧ Walk.map f p ≍ Walk.map f p_1

Tactic:
simp only [map_cons, cons.injEq] at h

Premises used: SimpleGraph.Walk.cons.injEq, SimpleGraph.Walk.map_cons
-- 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 u_1 v_1 w : V
h_1 : G.Adj u_1 v_1
p : G.Walk v_1 w
ih : ∀ ⦃p' : G.Walk v_1 w⦄ (h : Walk.map f p = Walk.map f p'), p = p'
v_2 : V
h_2 : G.Adj u_1 v_2
p_1 : G.Walk v_2 w
h : Eq.{v + 1} (α := V') ((f : (a : V) → V') v_1 : V') ((f : (a : V) → V') v_2 : V') ∧ Walk.map f p ≍ Walk.map f p_1
⊢ cons h_1 p = cons h_2 p_1

Tactic:
grind
-- 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 u_1 v_1 w : V
h_1 : G.Adj u_1 v_1
p : G.Walk v_1 w
ih : ∀ ⦃p' : G.Walk v_1 w⦄ (h : Walk.map f p = Walk.map f p'), p = p'
p' : G.Walk u_1 w
h : Walk.map f (Walk.cons h_1 p) = Walk.map f p'
cons :
  ∀ (p : G.Walk v_1 u_1) (ih : ∀ ⦃p' : G.Walk v_1 u_1⦄ (h : Walk.map f p = Walk.map f p'), p = p')
    (h : Walk.map f (Walk.cons h_1 p) = Walk.map f nil), Walk.cons h_1 p = nil
cons₁ :
  ∀ {v : V} (h : G.Adj u_1 v) (p_1 : G.Walk v w) (h_2 : Walk.map f (Walk.cons h_1 p) = Walk.map f (Walk.cons h p_1)),
    Walk.cons h_1 p = Walk.cons h p_1
⊢ Walk.cons h_1 p = p'

Tactic:
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