awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Maps (goal)
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).edges = List.map (Sym2.map (⇑f : (a : V) → V')) p.edges
have nil : ∀ {u : V},
  edges (u := (f : (a : V) → V') u) (Walk.map f nil) =
    List.map.{u, v} (α := Sym2 V) (Sym2.map (⇑f : (a : V) → V')) (edges (G := G) (u := u) nil)
Tactic: induction p
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Maps (goal)
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)
⊢ (Walk.map f p).edges = List.map (Sym2.map (⇑f : (a : V) → V')) p.edges
have 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 (cons h p)).edges = List.map (Sym2.map (⇑f : (a : V) → V')) (cons h p).edges
Tactic: induction p
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Maps (goal)
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).edgeSet = Sym2.map (⇑f : (a : V) → V') '' p.edgeSet
have h : ∀ (x : Sym2 V'),
  x ∈ (Walk.map f p).edgeSet ↔ Membership.mem (γ := Set (Sym2 V')) (Sym2.map (⇑f : (a : V) → V') '' p.edgeSet) x
Tactic: ext
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Maps (goal)
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 : ℕ
⊢ (Walk.map f p).getVert n = (f : (a : V) → V') (p.getVert n)
have nil : ∀ {u : V} (n : ℕ),
  getVert (u := (f : (a : V) → V') u) (Walk.map f nil) n = (f : (a : V) → V') (getVert (G := G) (u := u) nil n)
Tactic: induction p generalizing n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Maps (goal)
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)
⊢ (Walk.map f p).getVert n = (f : (a : V) → V') (p.getVert n)
have 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 (cons h p)).getVert n = (f : (a : V) → V') ((cons h p).getVert n)
Tactic: induction p generalizing n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Maps (goal)
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 = (f : (a : V) → V') (getVert (G := G) (u := u_1) nil n)
have nil : 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: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Maps (goal)
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)
⊢ 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)
have 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))
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Maps (goal)
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 = (f : (a : V) → V') ((cons h p_1).getVert n)
have cons : (Walk.map f (cons h p_1)).getVert 0 = (f : (a : V) → V') ((cons h p_1).getVert 0)
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Maps (goal)
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)
⊢ (Walk.map f (Walk.cons h p_1)).getVert n = (f : (a : V) → V') ((Walk.cons h p_1).getVert n)
have 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))
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Maps (goal)
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 nil = Walk.map f p'
⊢ nil = p'
have nil : ∀ (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: cases p'
Cleared hypotheses: p', h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Maps (goal)
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
⊢ Walk.nil = p'
have 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
Tactic: cases p'
Cleared hypotheses: p', h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Maps (hypothesis)
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)
⊢ cons h_1 p = cons h_2 p_1
have 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
Tactic: simp only [map_cons, cons.injEq] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Maps (goal)
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 (cons h_1 p) = Walk.map f p'
⊢ cons h_1 p = p'
have 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 (cons h_1 p) = Walk.map f nil), cons h_1 p = nil
Tactic: cases p' with
    | nil => simp at h
    | cons _ _ =>
      simp only [map_cons, cons.injEq] at h
      grind
Cleared hypotheses: w, p, ih, p', h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Maps (goal)
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
⊢ Walk.cons h_1 p = p'
have 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
Tactic: cases p' with
    | nil => simp at h
    | cons _ _ =>
      simp only [map_cons, cons.injEq] at h
      grind
Cleared hypotheses: p', h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Maps (goal)
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'
⊢ p = p'
have nil : ∀ {u : V} ⦃p' : G.Walk u u⦄ (h : Walk.map f nil = Walk.map f p'), nil = 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
Cleared hypotheses: p, p', h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Maps (goal)
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'
⊢ p = p'
have 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 (cons h p) = Walk.map f p'), cons h 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
Cleared hypotheses: p, p', h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Maps (goal)
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
⊢ p.transfer G ⋯ = p
have nil : ∀ {u : V}, Eq (α := G.Walk u u) (Walk.transfer nil G sorry) nil
Tactic: induction p
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Maps (goal)
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
⊢ p.transfer G ⋯ = p
have cons : ∀ {u v w : V} (h : G.Adj u v) (p : G.Walk v w), p.transfer G sorry = p → (cons h p).transfer G sorry = cons h p
Tactic: induction p
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Maps (goal)
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
⊢ p.transfer H hp = Walk.map (Hom.ofLE GH) p
have nil : ∀ {u : V} (hp : ∀ (e : Sym2 V), Membership.mem (γ := List (Sym2 V)) (edges (G := G) (u := u) nil) e → e ∈ H.edgeSet),
  Walk.transfer nil H hp = Walk.map (Hom.ofLE GH) nil
Tactic: induction p
Cleared hypotheses: hp
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Maps (goal)
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
⊢ p.transfer H hp = Walk.map (Hom.ofLE GH) p
have 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 ∈ (cons h p).edges, e ∈ H.edgeSet), (cons h p).transfer H hp = Walk.map (Hom.ofLE GH) (cons h p)
Tactic: induction p
Cleared hypotheses: hp
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Maps (goal)
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
⊢ (p.transfer H hp).edges = p.edges
have nil : ∀ {u : V} (hp : ∀ (e : Sym2 V), Membership.mem (γ := List (Sym2 V)) (edges (G := G) (u := u) nil) e → e ∈ H.edgeSet),
  (Walk.transfer nil H hp).edges = edges (G := G) (u := u) nil
Tactic: induction p
Cleared hypotheses: hp
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Maps (goal)
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
⊢ (p.transfer H hp).edges = p.edges
have 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 ∈ (cons h p).edges, e ∈ H.edgeSet), ((cons h p).transfer H hp).edges = (cons h p).edges
Tactic: induction p
Cleared hypotheses: hp
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Maps (goal)
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
⊢ (p.transfer H hp).edgeSet = p.edgeSet
have h : ∀ (x : Sym2 V), x ∈ (p.transfer H hp).edgeSet ↔ x ∈ p.edgeSet
Tactic: ext
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Maps (goal)
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
⊢ (p.transfer H hp).support = p.support
have nil : ∀ {u : V} (hp : ∀ (e : Sym2 V), Membership.mem (γ := List (Sym2 V)) (edges (G := G) (u := u) nil) e → e ∈ H.edgeSet),
  (Walk.transfer nil H hp).support = support (G := G) (u := u) nil
Tactic: induction p
Cleared hypotheses: hp
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Maps (goal)
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
⊢ (p.transfer H hp).support = p.support
have 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 ∈ (cons h p).edges, e ∈ H.edgeSet), ((cons h p).transfer H hp).support = (cons h p).support
Tactic: induction p
Cleared hypotheses: hp
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Maps (goal)
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
⊢ (p.transfer H hp).length = p.length
have nil : ∀ {u : V} (hp : ∀ (e : Sym2 V), Membership.mem (γ := List (Sym2 V)) (edges (G := G) (u := u) nil) e → e ∈ H.edgeSet),
  (Walk.transfer nil H hp).length = length.{u} (V := V) (G := G) (u := u) nil
Tactic: induction p
Cleared hypotheses: hp
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Maps (goal)
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
⊢ (p.transfer H hp).length = p.length
have 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 ∈ (cons h p).edges, e ∈ H.edgeSet), ((cons h p).transfer H hp).length = (cons h p).length
Tactic: induction p
Cleared hypotheses: hp
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Maps (goal)
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
⊢ (p.transfer H hp).transfer K hp' = p.transfer K ⋯
have nil : ∀ {u : V} (hp : ∀ (e : Sym2 V), Membership.mem (γ := List (Sym2 V)) (edges (G := G) (u := u) 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 sorry
Tactic: induction p
Cleared hypotheses: hp, hp'
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Maps (goal)
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 ⋯
⊢ (p.transfer H hp).transfer K hp' = p.transfer K ⋯
have 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 sorry) →
    ∀ (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 sorry
Tactic: induction p
Cleared hypotheses: hp, hp'
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Maps (goal)
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
⊢ (p.append q).transfer H hpq = (p.transfer H ⋯).append (q.transfer H ⋯)
have nil : ∀ {u : V} (q : G.Walk u w) (hpq : ∀ e ∈ (append nil q).edges, e ∈ H.edgeSet),
  (append nil q).transfer H hpq = append (Walk.transfer (G := G) nil H sorry) (q.transfer H sorry)
Tactic: induction p
Cleared hypotheses: q, hpq
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Maps (goal)
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 ⋯)
⊢ (p.append q).transfer H hpq = (p.transfer H ⋯).append (q.transfer H ⋯)
have 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 sorry).append (q.transfer H sorry)) →
    ∀ (q : G.Walk w_1 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 sorry).append (q.transfer H sorry)
Tactic: induction p
Cleared hypotheses: q, hpq
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Maps (goal)
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
⊢ (p.transfer H hp).reverse = p.reverse.transfer H ⋯
have nil : ∀ {u : V} (hp : ∀ (e : Sym2 V), Membership.mem (γ := List (Sym2 V)) (edges (G := G) (u := u) nil) e → e ∈ H.edgeSet),
  (Walk.transfer nil H hp).reverse = Walk.transfer (reverse nil) H sorry
Tactic: induction p
Cleared hypotheses: hp
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Maps (goal)
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 ⋯
⊢ (p.transfer H hp).reverse = p.reverse.transfer H ⋯
have 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 sorry) →
    ∀ (hp : ∀ e ∈ (cons h p).edges, e ∈ H.edgeSet), ((cons h p).transfer H hp).reverse = (cons h p).reverse.transfer H sorry
Tactic: induction p
Cleared hypotheses: hp
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Maps (goal)
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.deleteEdges s).edgeSet
have simp : ∀ e ∈ p.edges, e ∈ G.edgeSet ∧ e ∉ s
Tactic: simp only [edgeSet_deleteEdges, Set.mem_diff]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Maps (goal)
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
⊢ x ∈ p.edges → x ∉ {e}
have contrapose : Membership.mem (γ := Set (Sym2 V)) {e} x → x ∉ p.edges
Tactic: contrapose
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Maps (goal)
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
⊢ Walk.map (Hom.ofLE ⋯) (toDeleteEdges s p hp) = p
have hp₁ : ∀ e ∈ (toDeleteEdges s p hp).edges, e ∈ G.edgeSet
Tactic: rw [← transfer_eq_map_ofLE, transfer_transfer, transfer_self]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Operations (goal)
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''
⊢ (p.copy hu hv).copy hu' hv' = p.copy ⋯ ⋯
have subst_vars : ∀ (p : G.Walk u'' v''), (p.copy sorry sorry).copy sorry sorry = p.copy sorry sorry
Tactic: subst_vars
Cleared hypotheses: u, v, u', v', p, hu, hv, hu', hv'
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Operations (goal)
Goal:
V : Type u
G : SimpleGraph V
u u' : V
hu : u = u'
⊢ Eq (α := G.Walk u' u') (Walk.copy nil hu hu) nil
have subst_vars : Eq (α := G.Walk u' u') (Walk.copy nil sorry sorry) nil
Tactic: subst_vars
Cleared hypotheses: u, hu
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Operations (goal)
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'
⊢ (cons h p).copy hu hw = cons ⋯ (p.copy ⋯ hw)
have subst_vars : ∀ (h : G.Adj u' v) (p : G.Walk v w'), (cons h p).copy sorry sorry = cons sorry (p.copy sorry sorry)
Tactic: subst_vars
Cleared hypotheses: u, w, h, p, hu, hw
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Operations (goal)
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
⊢ cons h (p.copy hv hw) = Walk.copy (cons ⋯ p) ⋯ hw
have subst_vars : ∀ (h : G.Adj u v'), cons h (p.copy sorry sorry) = Walk.copy (cons sorry p) sorry sorry
Tactic: subst_vars
Cleared hypotheses: v, w, h, hv, hw
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Operations (goal)
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
⊢ p.append nil = p
have nil : ∀ {u : V}, Eq.{u + 1} (α := G.Walk u u) (append nil nil) nil
Tactic: induction p
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Operations (goal)
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
nil : ∀ {u : V}, Eq.{u + 1} (α := G.Walk u u) (append Walk.nil Walk.nil) Walk.nil
⊢ p.append Walk.nil = p
have cons : ∀ {u v w : V} (h : G.Adj u v) (p : G.Walk v w), p.append Walk.nil = p → (cons h p).append Walk.nil = cons h p
Tactic: induction p
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Operations (goal)
Goal:
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
have nil : ∀ {u : V} (q : G.Walk u w), append nil (q.append r) = (append nil q).append r
Tactic: induction p
Cleared hypotheses: p, q