awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
u v u_1 v_1 w : V
h : G.Adj u_1 v_1
p : G.Walk v_1 w
ih : p.bypass.support ⊆ p.support
pos : ∀ (h : u_1 ∈ p.bypass.support), (p.bypass.dropUntil u_1 h).support ⊆ u_1 :: p.support
neg : u_1 ∉ p.bypass.support → (cons h p.bypass).support ⊆ u_1 :: p.support
⊢ support (G := G) (u := u_1) (v := w)
      (if hs : u_1 ∈ p.bypass.support then p.bypass.dropUntil u_1 hs else cons h p.bypass) ⊆
    u_1 :: p.support

Tactic:
split_ifs
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
u v u_1 v_1 w : V
h : G.Adj u_1 v_1
p : G.Walk v_1 w
ih : p.bypass.support ⊆ p.support
h_1 : u_1 ∈ p.bypass.support
pos : p.bypass.support ⊆ u_1 :: p.support
⊢ (p.bypass.dropUntil u_1 h_1).support ⊆ u_1 :: p.support

Tactic:
apply List.Subset.trans (support_dropUntil_subset _ _)

Premises used: SimpleGraph.Walk.support_dropUntil_subset, List.Subset.trans
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
u v u_1 v_1 w : V
h : G.Adj u_1 v_1
p : G.Walk v_1 w
ih : p.bypass.support ⊆ p.support
h_1 : u_1 ∈ p.bypass.support
pos : p.bypass.support ⊆ p.support
⊢ p.bypass.support ⊆ u_1 :: p.support

Tactic:
apply List.subset_cons_of_subset

Premises used: List.subset_cons_of_subset
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
u v u_1 v_1 w : V
h : G.Adj u_1 v_1
p : G.Walk v_1 w
ih : p.bypass.support ⊆ p.support
h_1 : u_1 ∈ p.bypass.support
⊢ p.bypass.support ⊆ p.support

Tactic:
assumption
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
u v u_1 v_1 w : V
h : G.Adj u_1 v_1
p : G.Walk v_1 w
ih : p.bypass.support ⊆ p.support
h_1 : u_1 ∉ p.bypass.support
neg : p.bypass.support ⊆ p.support
⊢ u_1 :: p.bypass.support ⊆ u_1 :: p.support

Tactic:
apply List.cons_subset_cons

Premises used: List.cons_subset_cons
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
u v u_1 v_1 w : V
h : G.Adj u_1 v_1
p : G.Walk v_1 w
ih : p.bypass.support ⊆ p.support
h_1 : u_1 ∉ p.bypass.support
⊢ p.bypass.support ⊆ p.support

Tactic:
assumption
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
u v : V
p : G.Walk u v
nil :
  ∀ {u : V}, Subset.{u} (α := List V) (support (G := G) (u := u) (bypass Walk.nil)) (support (G := G) (u := u) Walk.nil)
cons :
  ∀ {u v w : V} (h : G.Adj u v) (p : G.Walk v w) (ih : p.bypass.support ⊆ p.support),
    (Walk.cons h p).bypass.support ⊆ (Walk.cons h p).support
⊢ p.bypass.support ⊆ p.support

Tactic:
induction p with
  | nil => simp!
  | cons _ _ ih =>
    simp! only
    split_ifs
    · apply List.Subset.trans (support_dropUntil_subset _ _)
      apply List.subset_cons_of_subset
      assumption
    · rw [support_cons]
      apply List.cons_subset_cons
      assumption

Premises used: SimpleGraph.Walk.support_cons, List.cons_subset_cons, List.subset_cons_of_subset, SimpleGraph.Walk.support_dropUntil_subset, SimpleGraph.Walk.cons, SimpleGraph.Walk.nil, List.Subset.trans
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
u v : V
p : G.Walk u v
⊢ (↑p.toPath : G.Walk u v).support ⊆ p.support

Tactic:
support_bypass_subset _

Premises used: SimpleGraph.Walk.support_bypass_subset
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
u v u_1 : V
⊢ Subset.{u} (α := List G.Dart) (darts (u := u_1) (bypass nil)) (darts (u := u_1) nil)

Tactic:
simp!
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
u v u_1 v_1 w : V
h : G.Adj u_1 v_1
p : G.Walk v_1 w
ih : p.bypass.darts ⊆ p.darts
pos :
  ∀ (h_1 : u_1 ∈ p.bypass.support), (p.bypass.dropUntil u_1 h_1).darts ⊆ { fst := u_1, snd := v_1, adj := h } :: p.darts
neg : u_1 ∉ p.bypass.support → (cons h p.bypass).darts ⊆ { fst := u_1, snd := v_1, adj := h } :: p.darts
⊢ darts (u := u_1) (v := w) (if hs : u_1 ∈ p.bypass.support then p.bypass.dropUntil u_1 hs else cons h p.bypass) ⊆
    { fst := u_1, snd := v_1, adj := h : G.Dart } :: p.darts

Tactic:
split_ifs
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
u v u_1 v_1 w : V
h : G.Adj u_1 v_1
p : G.Walk v_1 w
ih : p.bypass.darts ⊆ p.darts
h_1 : u_1 ∈ p.bypass.support
pos : p.bypass.darts ⊆ { fst := u_1, snd := v_1, adj := h } :: p.darts
⊢ (p.bypass.dropUntil u_1 h_1).darts ⊆ { fst := u_1, snd := v_1, adj := h } :: p.darts

Tactic:
apply List.Subset.trans (darts_dropUntil_subset _ _)

Premises used: List.Subset.trans, SimpleGraph.Walk.darts_dropUntil_subset
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
u v u_1 v_1 w : V
h : G.Adj u_1 v_1
p : G.Walk v_1 w
ih : p.bypass.darts ⊆ p.darts
h_1 : u_1 ∈ p.bypass.support
⊢ p.bypass.darts ⊆ { fst := u_1, snd := v_1, adj := h } :: p.darts

Tactic:
apply List.subset_cons_of_subset _ ih

Premises used: List.subset_cons_of_subset
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
u v u_1 v_1 w : V
h : G.Adj u_1 v_1
p : G.Walk v_1 w
ih : p.bypass.darts ⊆ p.darts
h_1 : u_1 ∉ p.bypass.support
⊢ { fst := u_1, snd := v_1, adj := h : G.Dart } :: p.bypass.darts ⊆ { fst := u_1, snd := v_1, adj := h } :: p.darts

Tactic:
List.cons_subset_cons _ ih

Premises used: List.cons_subset_cons
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
u v u_1 v_1 w : V
h : G.Adj u_1 v_1
p : G.Walk v_1 w
ih : p.bypass.darts ⊆ p.darts
h_1 : u_1 ∉ p.bypass.support
⊢ { fst := u_1, snd := v_1, adj := h : G.Dart } :: p.bypass.darts ⊆ { fst := u_1, snd := v_1, adj := h } :: p.darts

Tactic:
exact List.cons_subset_cons _ ih

Premises used: List.cons_subset_cons
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
u v : V
p : G.Walk u v
nil : ∀ {u : V}, Subset.{u} (α := List G.Dart) (darts (u := u) (bypass Walk.nil)) (darts (u := u) Walk.nil)
cons :
  ∀ {u v w : V} (h : G.Adj u v) (p : G.Walk v w) (ih : p.bypass.darts ⊆ p.darts),
    (Walk.cons h p).bypass.darts ⊆ (Walk.cons h p).darts
⊢ p.bypass.darts ⊆ p.darts

Tactic:
induction p with
  | nil => simp!
  | cons _ _ ih =>
    simp! only
    split_ifs
    · apply List.Subset.trans (darts_dropUntil_subset _ _)
      apply List.subset_cons_of_subset _ ih
    · rw [darts_cons]
      exact List.cons_subset_cons _ ih

Premises used: SimpleGraph.Walk.cons, SimpleGraph.Walk.darts_cons, SimpleGraph.Walk.nil, List.Subset.trans, SimpleGraph.Walk.darts_dropUntil_subset
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
u v : V
p : G.Walk u v
⊢ p.bypass.edges ⊆ p.edges

Tactic:
List.map_subset _ p.darts_bypass_subset

Premises used: List.map_subset, SimpleGraph.Walk.darts_bypass_subset, SimpleGraph.Walk.edges
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
u v : V
p : G.Walk u v
⊢ (↑p.toPath : G.Walk u v).darts ⊆ p.darts

Tactic:
darts_bypass_subset _

Premises used: SimpleGraph.Walk.darts_bypass_subset
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
u v : V
p : G.Walk u v
⊢ (↑p.toPath : G.Walk u v).edges ⊆ p.edges

Tactic:
edges_bypass_subset _

Premises used: SimpleGraph.Walk.edges_bypass_subset
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
v : V
⊢ Eq.{u + 1} (α := G.Walk v v) (cycleBypass nil) nil

Tactic:
rfl

Premises used: SimpleGraph.Walk.cycleBypass, rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
v : V
⊢ Subset.{u} (α := List (Sym2 V)) (edges (G := G) (u := v) (cycleBypass nil)) (edges (G := G) (u := v) nil)

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
v v' : V
hvv' : G.Adj v v'
w : G.Walk v' v
dsimp : s(v, v') :: w.bypass.edges ⊆ s(v, v') :: w.edges
⊢ (cons hvv' w).cycleBypass.edges ⊆ (cons hvv' w).edges

Tactic:
dsimp only [cycleBypass, edges_cons]

Premises used: SimpleGraph.Walk.cycleBypass, SimpleGraph.Walk.edges_cons
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
v v' : V
hvv' : G.Adj v v'
w : G.Walk v' v
s : w.bypass.edges ⊆ w.edges
⊢ s(v, v') :: w.bypass.edges ⊆ s(v, v') :: w.edges

Tactic:
gcongr
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
v v' : V
hvv' : G.Adj v v'
w : G.Walk v' v
⊢ w.bypass.edges ⊆ w.edges

Tactic:
edges_bypass_subset _

Premises used: SimpleGraph.Walk.edges_bypass_subset
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
v v' : V
hvv' : G.Adj v v'
w : G.Walk v' v
⊢ w.bypass.edges ⊆ w.edges

Tactic:
exact edges_bypass_subset _

Premises used: SimpleGraph.Walk.edges_bypass_subset
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
v v' : V
hvv' : G.Adj v v'
w : G.Walk v' v
dsimp : s(v, v') :: w.bypass.edges ⊆ s(v, v') :: w.edges
s : w.bypass.edges ⊆ w.edges
⊢ (cons hvv' w).cycleBypass.edges ⊆ (cons hvv' w).edges

Tactic:
classical
    dsimp only [cycleBypass, edges_cons]
    gcongr
    exact edges_bypass_subset _

Premises used: SimpleGraph.Walk.cycleBypass, SimpleGraph.Walk.edges_cons, SimpleGraph.Walk.edges_bypass_subset
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
v v' : V
hvv' : G.Adj v v'
w : G.Walk v' v
hw : (cons hvv' w).IsCircuit
⊢ cons hvv' w.bypass ≠ nil

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
v v' : V
hvv' : G.Adj v v'
w : G.Walk v' v
hw : (cons hvv' w).IsCircuit
refine_1 : ∀ (hvv' : s(v, v') ∈ w.bypass.edges), False
refine_2 : (cons hvv' w.bypass).support.tail.Nodup
⊢ (cons hvv' w.bypass).IsCycle

Tactic:
refine ⟨⟨(bypass_isPath _).isTrail.cons _ fun hvv' ↦ ?_, by simp⟩, ?_⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
v v' : V
hvv'_1 : G.Adj v v'
w : G.Walk v' v
hw : (cons hvv'_1 w).IsCircuit
hvv' : s(v, v') ∈ w.bypass.edges
⊢ w.IsTrail ∧ s(v, v') ∉ w.edges

Tactic:
simp only [isCircuit_def, isTrail_cons, ne_eq, reduceCtorEq, not_false_eq_true,
        and_true] at hw

Premises used: reduceCtorEq, and_true, SimpleGraph.Walk.isCircuit_def, ne_eq, SimpleGraph.Walk.isTrail_cons, not_false_eq_true
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
v v' : V
hvv'_1 : G.Adj v v'
w : G.Walk v' v
hvv' : s(v, v') ∈ w.bypass.edges
hw : w.IsTrail ∧ s(v, v') ∉ w.edges
⊢ False

Tactic:
hw.2 <| edges_bypass_subset _ hvv'

Premises used: And.right, SimpleGraph.Walk.edges_bypass_subset
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
v v' : V
hvv'_1 : G.Adj v v'
w : G.Walk v' v
hvv' : s(v, v') ∈ w.bypass.edges
hw : w.IsTrail ∧ s(v, v') ∉ w.edges
⊢ False

Tactic:
exact hw.2 <| edges_bypass_subset _ hvv'

Premises used: And.right, SimpleGraph.Walk.edges_bypass_subset
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
v v' : V
hvv' : G.Adj v v'
w : G.Walk v' v
hw : (cons hvv' w).IsCircuit
⊢ (cons hvv' w.bypass).support.tail.Nodup

Tactic:
simpa using (bypass_isPath _).support_nodup

Premises used: SimpleGraph.Walk.bypass_isPath, SimpleGraph.Walk.IsPath.support_nodup
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
v : V
w : G.Walk v v
hw : w ≠ Walk.nil
hw' : w.IsTrail
⊢ w.cycleBypass.IsCycle

Tactic:
(w.isCircuit_def.mpr ⟨hw', hw⟩).isCycle_cycleBypass

Premises used: Iff.mpr, SimpleGraph.Walk.isCircuit_def, And.intro, SimpleGraph.Walk.IsCircuit.isCycle_cycleBypass
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
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
hinj : Injective.{u + 1, v + 1} (α := V) (β := V') (⇑f : (a : V) → V')
u_1 : V
hp : IsPath.{u} (V := V) (G := G) (u := u_1) nil
⊢ IsPath (u := (f : (a : V) → V') u_1) (Walk.map f nil)

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
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
hinj : Injective.{u + 1, v + 1} (α := V) (β := V') (⇑f : (a : V) → V')
u_1 v_1 w : V
h : G.Adj u_1 v_1
p_1 : G.Walk v_1 w
ih : ∀ (hp : p_1.IsPath), (Walk.map f p_1).IsPath
hp : (cons h p_1).IsPath
⊢ p_1.IsPath ∧ u_1 ∉ p_1.support

Tactic:
rw [Walk.cons_isPath_iff] at hp

Premises used: SimpleGraph.Walk.cons_isPath_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
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
hinj : Injective.{u + 1, v + 1} (α := V) (β := V') (⇑f : (a : V) → V')
u_1 v_1 w : V
h : G.Adj u_1 v_1
p_1 : G.Walk v_1 w
ih : ∀ (hp : p_1.IsPath), (Walk.map f p_1).IsPath
hp : p_1.IsPath ∧ u_1 ∉ p_1.support
cons : ∀ x ∈ p_1.support, ¬Eq.{v + 1} (α := V') ((f : (a : V) → V') x : V') ((f : (a : V) → V') u_1 : V')
⊢ (Walk.map f (Walk.cons h p_1)).IsPath

Tactic:
simp only [map_cons, cons_isPath_iff, ih hp.1, support_map, List.mem_map, not_exists, not_and,
      true_and]

Premises used: not_exists, And.left, SimpleGraph.Walk.map_cons, SimpleGraph.Walk.cons_isPath_iff, SimpleGraph.Walk.support_map, List.mem_map, not_and, true_and
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
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
hinj : Injective.{u + 1, v + 1} (α := V) (β := V') (⇑f : (a : V) → V')
u_1 v_1 w : V
h : G.Adj u_1 v_1
p_1 : G.Walk v_1 w
ih : ∀ (hp : p_1.IsPath), (Walk.map f p_1).IsPath
hp : p_1.IsPath ∧ u_1 ∉ p_1.support
x : V
hx : x ∈ p_1.support
hf : Eq.{v + 1} (α := V') ((f : (a : V) → V') x : V') ((f : (a : V) → V') u_1 : V')
⊢ u_1 ∈ p_1.support

Tactic:
cases hinj hf
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
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
hinj : Injective.{u + 1, v + 1} (α := V) (β := V') (⇑f : (a : V) → V')
u_1 v_1 w : V
h : G.Adj u_1 v_1
p_1 : G.Walk v_1 w
ih : ∀ (hp : p_1.IsPath), (Walk.map f p_1).IsPath
hp : p_1.IsPath ∧ u_1 ∉ p_1.support
x : V
hx : x ∈ p_1.support
hf : Eq.{v + 1} (α := V') ((f : (a : V) → V') x : V') ((f : (a : V) → V') u_1 : V')
hx₁ : u_1 ∈ p_1.support
⊢ Eq.{v + 1} (α := V') ((f : (a : V) → V') u_1 : V') ((f : (a : V) → V') u_1 : V')

Tactic:
cases hinj hf
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
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
hinj : Injective.{u + 1, v + 1} (α := V) (β := V') (⇑f : (a : V) → V')
u_1 v_1 w : V
h : G.Adj u_1 v_1
p_1 : G.Walk v_1 w
ih : ∀ (hp : p_1.IsPath), (Walk.map f p_1).IsPath
hp : p_1.IsPath ∧ u_1 ∉ p_1.support
hx : u_1 ∈ p_1.support
hf : Eq.{v + 1} (α := V') ((f : (a : V) → V') u_1 : V') ((f : (a : V) → V') u_1 : V')
⊢ False

Tactic:
hp.2 hx

Premises used: And.right
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
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
hinj : Injective.{u + 1, v + 1} (α := V) (β := V') (⇑f : (a : V) → V')
u_1 v_1 w : V
h : G.Adj u_1 v_1
p_1 : G.Walk v_1 w
ih : ∀ (hp : p_1.IsPath), (Walk.map f p_1).IsPath
hp : p_1.IsPath ∧ u_1 ∉ p_1.support
hx : u_1 ∈ p_1.support
hf : Eq.{v + 1} (α := V') ((f : (a : V) → V') u_1 : V') ((f : (a : V) → V') u_1 : V')
⊢ False

Tactic:
exact hp.2 hx

Premises used: And.right
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
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
hinj : Injective.{u + 1, v + 1} (α := V) (β := V') (⇑f : (a : V) → V')
hp : p.IsPath
nil :
  ∀ {u : V} (hp : IsPath.{u} (V := V) (G := G) (u := u) Walk.nil),
    IsPath (u := (f : (a : V) → V') u) (Walk.map f Walk.nil)
cons :
  ∀ {u v w : V} (h : G.Adj u v) (p : G.Walk v w) (ih : ∀ (hp : p.IsPath), (Walk.map f p).IsPath)
    (hp : (Walk.cons h p).IsPath), (Walk.map f (Walk.cons h p)).IsPath
⊢ (Walk.map f p).IsPath

Tactic:
induction p with
  | nil => simp
  | cons _ _ ih =>
    rw [Walk.cons_isPath_iff] at hp
    simp only [map_cons, cons_isPath_iff, ih hp.1, support_map, List.mem_map, not_exists, not_and,
      true_and]
    intro x hx hf
    cases hinj hf
    exact hp.2 hx

Premises used: not_exists, SimpleGraph.Walk.cons, SimpleGraph.Walk.nil, SimpleGraph.Walk.map_cons, SimpleGraph.Walk.cons_isPath_iff, SimpleGraph.Walk.support_map, List.mem_map, not_and, true_and
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
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'
u_1 : V
hp : IsPath (u := (f : (a : V) → V') u_1) (Walk.map f Walk.nil)
⊢ IsPath.{u} (V := V) (G := G) (u := u_1) Walk.nil

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
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'
u_1 v_1 w : V
h : G.Adj u_1 v_1
p_1 : G.Walk v_1 w
ih : ∀ (hp : (Walk.map f p_1).IsPath), p_1.IsPath
hp : (Walk.map f (cons h p_1)).IsPath
⊢ (cons h p_1).IsPath

Tactic:
grind [map_cons, Walk.cons_isPath_iff, support_map]

Premises used: SimpleGraph.Walk.map_cons, SimpleGraph.Walk.cons_isPath_iff, SimpleGraph.Walk.support_map
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
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'
hp : (Walk.map f p).IsPath
nil :
  ∀ {u : V} (hp : IsPath (u := (f : (a : V) → V') u) (Walk.map f Walk.nil)),
    IsPath.{u} (V := V) (G := G) (u := u) Walk.nil
cons :
  ∀ {u v w : V} (h : G.Adj u v) (p : G.Walk v w) (ih : ∀ (hp : (Walk.map f p).IsPath), p.IsPath)
    (hp : (Walk.map f (Walk.cons h p)).IsPath), (Walk.cons h p).IsPath
⊢ p.IsPath

Tactic:
induction p with
  | nil => simp
  | cons _ _ ih => grind [map_cons, Walk.cons_isPath_iff, support_map]

Premises used: SimpleGraph.Walk.cons, SimpleGraph.Walk.IsPath.nil, SimpleGraph.Walk.map_cons, SimpleGraph.Walk.cons_isPath_iff, SimpleGraph.Walk.support_map
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
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
hinj : Injective.{u + 1, v + 1} (α := V) (β := V') (⇑f : (a : V) → V')
⊢ (Walk.map f p).IsPath ↔ p.IsPath

Tactic:
⟨IsPath.of_map, map_isPath_of_injective hinj⟩

Premises used: SimpleGraph.Walk.IsPath.of_map, Iff.intro, SimpleGraph.Walk.map_isPath_of_injective
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
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
hinj : Injective.{u + 1, v + 1} (α := V) (β := V') (⇑f : (a : V) → V')
u_1 : V
⊢ IsTrail (u := (f : (a : V) → V') u_1) (Walk.map f nil) ↔ IsTrail.{u} (V := V) (G := G) (u := u_1) nil

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
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
hinj : Injective.{u + 1, v + 1} (α := V) (β := V') (⇑f : (a : V) → V')
u_1 v_1 w : V
h : G.Adj u_1 v_1
p_1 : G.Walk v_1 w
ih : (Walk.map f p_1).IsTrail ↔ p_1.IsTrail
cons :
  p_1.IsTrail ∧ (s((f : (a : V) → V') u_1, (f : (a : V) → V') v_1) : Sym2 V') ∉ (Walk.map f p_1).edges ↔
    p_1.IsTrail ∧ s(u_1, v_1) ∉ p_1.edges
⊢ (Walk.map f (Walk.cons h p_1)).IsTrail ↔ (Walk.cons h p_1).IsTrail

Tactic:
rw [map_cons, isTrail_cons, ih, isTrail_cons]

Premises used: SimpleGraph.Walk.map_cons, SimpleGraph.Walk.isTrail_cons
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
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
hinj : Injective.{u + 1, v + 1} (α := V) (β := V') (⇑f : (a : V) → V')
u_1 v_1 w : V
h : G.Adj u_1 v_1
p_1 : G.Walk v_1 w
ih : (Walk.map f p_1).IsTrail ↔ p_1.IsTrail
cons : (s((f : (a : V) → V') u_1, (f : (a : V) → V') v_1) : Sym2 V') ∉ (Walk.map f p_1).edges ↔ s(u_1, v_1) ∉ p_1.edges
⊢ p_1.IsTrail ∧ (s((f : (a : V) → V') u_1, (f : (a : V) → V') v_1) : Sym2 V') ∉ (Walk.map f p_1).edges ↔
    p_1.IsTrail ∧ s(u_1, v_1) ∉ p_1.edges

Tactic:
apply and_congr_right'

Premises used: and_congr_right'
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
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
hinj : Injective.{u + 1, v + 1} (α := V) (β := V') (⇑f : (a : V) → V')
u_1 v_1 w : V
h : G.Adj u_1 v_1
p_1 : G.Walk v_1 w
ih : (Walk.map f p_1).IsTrail ↔ p_1.IsTrail
cons : Sym2.map (⇑f : (a : V) → V') s(u_1, v_1) ∉ (Walk.map f p_1).edges ↔ s(u_1, v_1) ∉ p_1.edges
cons₁ :
  Sym2.map (⇑f : (a : V) → V') s(u_1, v_1) ∉ List.map (Sym2.map (⇑f : (a : V) → V')) p_1.edges ↔ s(u_1, v_1) ∉ p_1.edges
cons₂ cons₃ :
  Sym2.map (⇑f : (a : V) → V') s(u_1, v_1) ∉ List.map (Sym2.map (⇑f : (a : V) → V')) p_1.edges ↔
    Sym2.map (⇑f : (a : V) → V') s(u_1, v_1) ∉ List.map (Sym2.map (⇑f : (a : V) → V')) p_1.edges
⊢ (s((f : (a : V) → V') u_1, (f : (a : V) → V') v_1) : Sym2 V') ∉ (Walk.map f p_1).edges ↔ s(u_1, v_1) ∉ p_1.edges

Tactic:
rw [← Sym2.map_mk, edges_map, ← List.mem_map_of_injective (Sym2.map.injective hinj)]

Premises used: Sym2.map.injective, Sym2.map_mk, List.mem_map_of_injective, SimpleGraph.Walk.edges_map
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
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
hinj : Injective.{u + 1, v + 1} (α := V) (β := V') (⇑f : (a : V) → V')
nil :
  ∀ {u : V}, IsTrail (u := (f : (a : V) → V') u) (Walk.map f Walk.nil) ↔ IsTrail.{u} (V := V) (G := G) (u := u) Walk.nil
cons :
  ∀ {u v w : V} (h : G.Adj u v) (p : G.Walk v w) (ih : (Walk.map f p).IsTrail ↔ p.IsTrail),
    (Walk.map f (Walk.cons h p)).IsTrail ↔ (Walk.cons h p).IsTrail
⊢ (Walk.map f p).IsTrail ↔ p.IsTrail

Tactic:
induction p with
  | nil => simp
  | cons _ _ ih =>
    rw [map_cons, isTrail_cons, ih, isTrail_cons]
    apply and_congr_right'
    rw [← Sym2.map_mk, edges_map, ← List.mem_map_of_injective (Sym2.map.injective hinj)]

Premises used: Sym2.map.injective, and_congr_right', SimpleGraph.Walk.cons, Sym2.map_mk, List.mem_map_of_injective, SimpleGraph.Walk.nil, SimpleGraph.Walk.map_cons, SimpleGraph.Walk.isTrail_cons, SimpleGraph.Walk.edges_map