awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Decomp (goal)
Goal:
V : Type u
G : SimpleGraph V
v w u : V
inst : DecidableEq V
x : V
p : G.Walk u v
q : G.Walk v w
hx : x ∈ p.support
⊢ (p.append q).takeUntil x ⋯ = p.takeUntil x hx
have nil : ∀ {u : V} (q : G.Walk u w) (hx : Membership.mem (γ := List V) (support (G := G) (u := u) nil) x),
  (append nil q).takeUntil x sorry = takeUntil nil x hx
Tactic: induction p with
  | nil => rw [mem_support_nil_iff] at hx; subst_vars; simp
  | cons => grind [cons_append, takeUntil]
Cleared hypotheses: p, q, hx
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Decomp (goal)
Goal:
V : Type u
G : SimpleGraph V
v w u : V
inst : DecidableEq V
x : V
p : G.Walk u v
q : G.Walk v w
hx : x ∈ p.support
nil :
  ∀ {u : V} (q : G.Walk u w) (hx : Membership.mem (γ := List V) (support (G := G) (u := u) Walk.nil) x),
    (append Walk.nil q).takeUntil x ⋯ = takeUntil Walk.nil x hx
⊢ (p.append q).takeUntil x ⋯ = p.takeUntil x hx
have cons : ∀ {u v w_1 : V} (h : G.Adj u v) (p : G.Walk v w_1),
  (∀ (q : G.Walk w_1 w) (hx : x ∈ p.support), (p.append q).takeUntil x sorry = p.takeUntil x hx) →
    ∀ (q : G.Walk w_1 w) (hx : x ∈ (cons h p).support), ((cons h p).append q).takeUntil x sorry = (cons h p).takeUntil x hx
Tactic: induction p with
  | nil => rw [mem_support_nil_iff] at hx; subst_vars; simp
  | cons => grind [cons_append, takeUntil]
Cleared hypotheses: p, q, hx
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Decomp (goal)
Goal:
V : Type u
G : SimpleGraph V
w : V
inst : DecidableEq V
u v : V
n : ℕ
p : G.Walk u v
hw : w ∈ p.support
hn : n ≤ (p.takeUntil w hw).length
| p.getVert n
have rw : if n < (p.takeUntil w hw).length then (p.takeUntil w hw).getVert n
else (p.dropUntil w hw).getVert (n - (p.takeUntil w hw).length)
Tactic: rw [← take_spec p hw, getVert_append]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Decomp (goal)
Goal:
V : Type u
G : SimpleGraph V
w : V
inst : DecidableEq V
u v : V
n : ℕ
p : G.Walk u v
hw : w ∈ p.support
hn : n ≤ (p.takeUntil w hw).length
⊢ (p.takeUntil w hw).getVert n = p.getVert n
have conv_rhs : (p.takeUntil w hw).getVert n =
  if n < (p.takeUntil w hw).length then (p.takeUntil w hw).getVert n
  else (p.dropUntil w hw).getVert (n - (p.takeUntil w hw).length)
Tactic: conv_rhs => rw [← take_spec p hw, getVert_append]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Decomp (goal)
Goal:
V : Type u
G : SimpleGraph V
w : V
inst : DecidableEq V
u v : V
n : ℕ
p : G.Walk u v
hw : w ∈ p.support
hn : n ≤ (p.takeUntil w hw).length
⊢ (p.takeUntil w hw).getVert n =
    if n < (p.takeUntil w hw).length then (p.takeUntil w hw).getVert n
    else (p.dropUntil w hw).getVert (n - (p.takeUntil w hw).length)
have inl : n < (p.takeUntil w hw).length →
  (p.takeUntil w hw).getVert n =
    if n < (p.takeUntil w hw).length then (p.takeUntil w hw).getVert n
    else (p.dropUntil w hw).getVert (n - (p.takeUntil w hw).length)
Tactic: cases hn.lt_or_eq
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Decomp (goal)
Goal:
V : Type u
G : SimpleGraph V
w : V
inst : DecidableEq V
u v : V
n : ℕ
p : G.Walk u v
hw : w ∈ p.support
hn : n ≤ (p.takeUntil w hw).length
inl :
  n < (p.takeUntil w hw).length →
    (p.takeUntil w hw).getVert n =
      if n < (p.takeUntil w hw).length then (p.takeUntil w hw).getVert n
      else (p.dropUntil w hw).getVert (n - (p.takeUntil w hw).length)
⊢ (p.takeUntil w hw).getVert n =
    if n < (p.takeUntil w hw).length then (p.takeUntil w hw).getVert n
    else (p.dropUntil w hw).getVert (n - (p.takeUntil w hw).length)
have inr : n = (p.takeUntil w hw).length →
  (p.takeUntil w hw).getVert n =
    if n < (p.takeUntil w hw).length then (p.takeUntil w hw).getVert n
    else (p.dropUntil w hw).getVert (n - (p.takeUntil w hw).length)
Tactic: cases hn.lt_or_eq
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Decomp (goal)
Goal:
V : Type u
G : SimpleGraph V
v w u : V
inst : DecidableEq V
hsu : w ≠ u
p : G.Walk u v
h : w ∈ p.support
⊢ (p.takeUntil w h).snd = p.snd
have apply : 1 ≤ (p.takeUntil w h).length
Tactic: apply p.getVert_takeUntil h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Decomp (goal)
Goal:
V : Type u
G : SimpleGraph V
v w u : V
inst : DecidableEq V
hsu : w ≠ u
p : G.Walk u v
h : w ∈ p.support
⊢ 1 ≤ (p.takeUntil w h).length
have contrapose : ∀ (hsu : ¬1 ≤ (p.takeUntil w h).length), w = u
Tactic: contrapose hsu
Cleared hypotheses: hsu
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Decomp (goal)
Goal:
V : Type u
G : SimpleGraph V
v w u : V
inst : DecidableEq V
p : G.Walk u v
h : w ∈ p.support
hsu : ¬1 ≤ (p.takeUntil w h).length
⊢ w = u
have symm : u = w
Tactic: symm
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Decomp (hypothesis)
Goal:
V : Type u
G : SimpleGraph V
v w u : V
inst : DecidableEq V
p : G.Walk v w
h : u ∈ p.support
⊢ p.getVert (p.takeUntil u h).length = u
have this : ((p.takeUntil u h).append (p.dropUntil u h)).getVert (p.takeUntil u h).length = p.getVert (p.takeUntil u h).length
Tactic: have := congr_arg₂ (y := (p.takeUntil _ h).length) getVert (p.take_spec h) rfl
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Decomp (hypothesis)
Goal:
V : Type u
G : SimpleGraph V
v w : V
inst : DecidableEq V
n : ℕ
p : G.Walk v w
h : p.getVert n ∈ p.support
hn : n < (p.takeUntil (p.getVert n) h).length
⊢ False
have h₁ : n < (p.takeUntil (p.getVert n) h).support.dropLast.length
Tactic: have h₁ : n < (p.takeUntil _ h).support.dropLast.length := by simpa
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Decomp (goal)
Goal:
V : Type u
G : SimpleGraph V
v w : V
inst : DecidableEq V
n : ℕ
p : G.Walk v w
h : p.getVert n ∈ p.support
hn : n < (p.takeUntil (p.getVert n) h).length
h₁ : n < (p.takeUntil (p.getVert n) h).support.dropLast.length
⊢ p.getVert n ∈ (p.takeUntil (p.getVert n) h).support.dropLast
have simp_rw : getElem (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) (p.takeUntil (p.getVert n) h).support n sorry ∈
  (p.takeUntil (p.getVert n) h).support.dropLast
Tactic: simp_rw [p.getVert_takeUntil h hn.le ▸ getVert_eq_support_getElem _ hn.le,
      ← List.getElem_dropLast h₁, List.getElem_mem h₁]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Decomp (goal)
Goal:
V : Type u
G : SimpleGraph V
v w : V
inst : DecidableEq V
n : ℕ
p : G.Walk v w
h : p.getVert n ∈ p.support
hn : n < (p.takeUntil (p.getVert n) h).length
h₁ : n < (p.takeUntil (p.getVert n) h).support.dropLast.length
simp_rw :
  getElem (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) (p.takeUntil (p.getVert n) h).support n ⋯ ∈
    (p.takeUntil (p.getVert n) h).support.dropLast
⊢ p.getVert n ∈ (p.takeUntil (p.getVert n) h).support.dropLast
have simp_rw₁ : getElem (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) (p.takeUntil (p.getVert n) h).support.dropLast n h₁ ∈
  (p.takeUntil (p.getVert n) h).support.dropLast
Tactic: simp_rw [p.getVert_takeUntil h hn.le ▸ getVert_eq_support_getElem _ hn.le,
      ← List.getElem_dropLast h₁, List.getElem_mem h₁]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Decomp (hypothesis)
Goal:
V : Type u
G : SimpleGraph V
v w : V
inst : DecidableEq V
n : ℕ
p : G.Walk v w
h : p.getVert n ∈ p.support
hn : n < (p.takeUntil (p.getVert n) h).length
h₁ : n < (p.takeUntil (p.getVert n) h).support.dropLast.length
⊢ False
have this : p.getVert n ∈ (p.takeUntil (p.getVert n) h).support.dropLast
Tactic: have : p.getVert n ∈ (p.takeUntil _ h).support.dropLast := by
    simp_rw [p.getVert_takeUntil h hn.le ▸ getVert_eq_support_getElem _ hn.le,
      ← List.getElem_dropLast h₁, List.getElem_mem h₁]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Decomp (hypothesis)
Goal:
V : Type u
G : SimpleGraph V
v w : V
inst : DecidableEq V
n : ℕ
p : G.Walk v w
h : p.getVert n ∈ p.support
hn : n < (p.takeUntil (p.getVert n) h).length
h₁ : n < (p.takeUntil (p.getVert n) h).support.dropLast.length
this : p.getVert n ∈ (p.takeUntil (p.getVert n) h).support.dropLast
⊢ False
have this₁ : List.count (p.getVert n) ((p.takeUntil (p.getVert n) h).support.dropLast ++ [p.getVert n]) = 1
Tactic: have := dropLast_support_concat _ ▸ p.count_support_takeUntil_eq_one h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Decomp (goal)
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
u v w : V
p : G.Walk v w
h : u ∈ p.support
huw : u ≠ w
⊢ (p.takeUntil u h).length < p.length
have rw : (p.takeUntil u h).length ≠ p.length
Tactic: rw [(p.length_takeUntil_le h).lt_iff_ne]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Decomp (goal)
Goal:
V : Type u
G : SimpleGraph V
v u : V
inst : DecidableEq V
w x : V
p : G.Walk u v
hw : w ∈ p.support
hx : x ∈ (p.takeUntil w hw).support
⊢ (p.takeUntil w hw).takeUntil x hx = p.takeUntil x ⋯
have simp_rw : ((p.takeUntil w hw).append (p.dropUntil w hw)).takeUntil x sorry = p.takeUntil x sorry
Tactic: simp_rw [← takeUntil_append_of_mem_left _ (p.dropUntil w hw) hx, take_spec]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Decomp (goal)
Goal:
V : Type u
G : SimpleGraph V
v u : V
inst : DecidableEq V
p : G.Walk u v
w x : V
h : x ≠ w
hw : w ∈ p.support
hx : x ∈ (p.takeUntil w hw).support
⊢ w ∉ (p.takeUntil x ⋯).support
have rw : w ∉ ((p.takeUntil w hw).takeUntil x hx).support
Tactic: rw [← takeUntil_takeUntil p hw hx]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Decomp (hypothesis)
Goal:
V : Type u
G : SimpleGraph V
v u : V
inst : DecidableEq V
p : G.Walk u v
w x : V
h : x ≠ w
hw : w ∈ p.support
hx : x ∈ (p.takeUntil w hw).support
hw' : w ∈ ((p.takeUntil w hw).takeUntil x hx).support
⊢ False
have h1 : (((p.takeUntil w hw).takeUntil x hx).takeUntil w hw').length < ((p.takeUntil w hw).takeUntil x hx).length
Tactic: have h1 : (((p.takeUntil w hw).takeUntil x hx).takeUntil w hw').length
      < ((p.takeUntil w hw).takeUntil x hx).length := by
    exact length_takeUntil_lt _ h.symm
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Decomp (hypothesis)
Goal:
V : Type u
G : SimpleGraph V
v u : V
inst : DecidableEq V
p : G.Walk u v
w x : V
h : x ≠ w
hw : w ∈ p.support
hx : x ∈ (p.takeUntil w hw).support
hw' : w ∈ ((p.takeUntil w hw).takeUntil x hx).support
h1 : (((p.takeUntil w hw).takeUntil x hx).takeUntil w hw').length < ((p.takeUntil w hw).takeUntil x hx).length
⊢ False
have h2 : ((p.takeUntil w hw).takeUntil x hx).length < (p.takeUntil w hw).length
Tactic: have h2 : ((p.takeUntil w hw).takeUntil x hx).length < (p.takeUntil w hw).length := by
    exact length_takeUntil_lt _ h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Decomp (hypothesis)
Goal:
V : Type u
G : SimpleGraph V
v u : V
inst : DecidableEq V
p : G.Walk u v
w x : V
h : x ≠ w
hw : w ∈ p.support
hx : x ∈ (p.takeUntil w hw).support
hw' : w ∈ ((p.takeUntil w hw).takeUntil x hx).support
h1 : (((p.takeUntil w hw).takeUntil x hx).takeUntil w hw').length < ((p.takeUntil w hw).takeUntil x hx).length
h2 : ((p.takeUntil w hw).takeUntil x hx).length < (p.takeUntil w hw).length
⊢ False
have h1₁ : (p.takeUntil w sorry).length < (p.takeUntil x sorry).length
Tactic: simp only [takeUntil_takeUntil] at h1 h2
Cleared hypotheses: h1, h2
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Decomp (hypothesis)
Goal:
V : Type u
G : SimpleGraph V
v u : V
inst : DecidableEq V
p : G.Walk u v
w x : V
h : x ≠ w
hw : w ∈ p.support
hx : x ∈ (p.takeUntil w hw).support
hw' : w ∈ ((p.takeUntil w hw).takeUntil x hx).support
h1 : (((p.takeUntil w hw).takeUntil x hx).takeUntil w hw').length < ((p.takeUntil w hw).takeUntil x hx).length
h2 : ((p.takeUntil w hw).takeUntil x hx).length < (p.takeUntil w hw).length
h1₁ : (p.takeUntil w ⋯).length < (p.takeUntil x ⋯).length
⊢ False
have h2₁ : (p.takeUntil x sorry).length < (p.takeUntil w hw).length
Tactic: simp only [takeUntil_takeUntil] at h1 h2
Cleared hypotheses: h1, h2
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Decomp (goal)
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).support.tail ~r c.support.tail
have simp : (c.dropUntil u h).support.tail ++ (c.takeUntil u h).support.tail ~r c.support.tail
Tactic: simp only [rotate, tail_support_append]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Decomp (goal)
Goal:
V : Type u
G : SimpleGraph V
v : V
inst : DecidableEq V
c : G.Walk v v
u : V
h : u ∈ c.support
⊢ (c.dropUntil u h).support.tail ++ (c.takeUntil u h).support.tail ~r c.support.tail
have apply : (c.takeUntil u h).support.tail ++ (c.dropUntil u h).support.tail ~r c.support.tail
Tactic: apply List.IsRotated.trans List.isRotated_append
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Decomp (goal)
Goal:
V : Type u
G : SimpleGraph V
v : V
inst : DecidableEq V
c : G.Walk v v
u : V
h : u ∈ c.support
⊢ (c.takeUntil u h).support.tail ++ (c.dropUntil u h).support.tail ~r c.support.tail
have rw : ((c.takeUntil u h).append (c.dropUntil u h)).support.tail ~r c.support.tail
Tactic: rw [← tail_support_append, take_spec]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Decomp (goal)
Goal:
V : Type u
G : SimpleGraph V
v : V
inst : DecidableEq V
c : G.Walk v v
u : V
h : u ∈ c.support
rw : ((c.takeUntil u h).append (c.dropUntil u h)).support.tail ~r c.support.tail
⊢ (c.takeUntil u h).support.tail ++ (c.dropUntil u h).support.tail ~r c.support.tail
have rw₁ : c.support.tail ~r c.support.tail
Tactic: rw [← tail_support_append, take_spec]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Decomp (goal)
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).darts ~r c.darts
have simp : (c.dropUntil u h).darts ++ (c.takeUntil u h).darts ~r c.darts
Tactic: simp only [rotate, darts_append]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Decomp (goal)
Goal:
V : Type u
G : SimpleGraph V
v : V
inst : DecidableEq V
c : G.Walk v v
u : V
h : u ∈ c.support
⊢ (c.dropUntil u h).darts ++ (c.takeUntil u h).darts ~r c.darts
have apply : (c.takeUntil u h).darts ++ (c.dropUntil u h).darts ~r c.darts
Tactic: apply List.IsRotated.trans List.isRotated_append
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Decomp (goal)
Goal:
V : Type u
G : SimpleGraph V
v : V
inst : DecidableEq V
c : G.Walk v v
u : V
h : u ∈ c.support
⊢ (c.takeUntil u h).darts ++ (c.dropUntil u h).darts ~r c.darts
have rw : ((c.takeUntil u h).append (c.dropUntil u h)).darts ~r c.darts
Tactic: rw [← darts_append, take_spec]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Decomp (goal)
Goal:
V : Type u
G : SimpleGraph V
v : V
inst : DecidableEq V
c : G.Walk v v
u : V
h : u ∈ c.support
rw : ((c.takeUntil u h).append (c.dropUntil u h)).darts ~r c.darts
⊢ (c.takeUntil u h).darts ++ (c.dropUntil u h).darts ~r c.darts
have rw₁ : c.darts ~r c.darts
Tactic: rw [← darts_append, take_spec]
-- 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 u' v' : V
p : G.Walk u v
hu : u = u'
hv : v = v'
⊢ Walk.map f (p.copy hu hv) = (Walk.map f p).copy ⋯ ⋯
have subst_vars : ∀ (p : G.Walk u' v'), Walk.map f (p.copy sorry sorry) = (Walk.map f p).copy sorry sorry
Tactic: subst_vars
Cleared hypotheses: u, v, p, hu, hv
-- 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
⊢ Walk.map Hom.id p = p
have nil : ∀ {u : V}, Eq.{u + 1} (α := G.Walk ((Hom.id : (a : V) → V) u) ((Hom.id : (a : V) → V) u)) (Walk.map Hom.id nil) nil
Tactic: induction p
Cleared hypotheses: 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.{u + 1} (α := G.Walk ((Hom.id : (a : V) → V) u) ((Hom.id : (a : V) → V) u)) (Walk.map Hom.id Walk.nil) Walk.nil
⊢ Walk.map Hom.id p = p
have 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 (cons h p) = cons h p
Tactic: induction p
Cleared hypotheses: p
-- 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 : V
p : G.Walk u v
⊢ Walk.map f' (Walk.map f p) = Walk.map (f'.comp f) p
have 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 nil)) (Walk.map (f'.comp f) nil)
Tactic: induction p
-- 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 : 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)
⊢ Walk.map f' (Walk.map f p) = Walk.map (f'.comp f) p
have 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 (cons h p)) = Walk.map (f'.comp f) (cons h p)
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'
u v : V
p : G.Walk u v
f f' : G →g G'
h : f = f'
⊢ Walk.map f p = (Walk.map f' p).copy ⋯ ⋯
have subst_vars : Walk.map f' p = (Walk.map f' p).copy sorry sorry
Tactic: subst_vars
Cleared hypotheses: f, 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'
u v : V
p : G.Walk u v
⊢ (Walk.map f p).Nil ↔ p.Nil
have nil : Nil (v := (f : (a : V) → V') u) (Walk.map f nil) ↔ Nil.{u} (V := V) (G := G) (v := u) nil
Tactic: cases p
Cleared hypotheses: v, 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 : Nil (v := (f : (a : V) → V') u) (Walk.map f Walk.nil) ↔ Nil.{u} (V := V) (G := G) (v := u) Walk.nil
⊢ (Walk.map f p).Nil ↔ p.Nil
have cons : ∀ {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: cases p
Cleared hypotheses: 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
p : G.Walk u u
⊢ Walk.map f p = nil ↔ p = nil
have nil : 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: cases p
Cleared hypotheses: 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
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
⊢ Walk.map f p = Walk.nil ↔ p = Walk.nil
have cons : ∀ {v : V} (h : G.Adj u v) (p : G.Walk v u), Walk.map f (cons h p) = Walk.nil ↔ cons h p = Walk.nil
Tactic: cases p
Cleared hypotheses: 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).length = p.length
have nil : ∀ {u : V}, length (u := (f : (a : V) → V') u) (Walk.map f nil) = length.{u} (V := V) (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}, length (u := (f : (a : V) → V') u) (Walk.map f Walk.nil) = length.{u} (V := V) (G := G) (u := u) Walk.nil
⊢ (Walk.map f p).length = p.length
have 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 (cons h p)).length = (cons h p).length
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 w : V
p : G.Walk u v
q : G.Walk v w
⊢ Walk.map f (p.append q) = (Walk.map f p).append (Walk.map f q)
have nil : ∀ {u : V} (q : G.Walk u w), Walk.map f (append nil q) = append (Walk.map f nil) (Walk.map f q)
Tactic: induction p
Cleared hypotheses: p, q
-- 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 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)
⊢ Walk.map f (p.append q) = (Walk.map f p).append (Walk.map f q)
have 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 ((cons h p).append q) = (Walk.map f (cons h p)).append (Walk.map f q)
Tactic: induction p
Cleared hypotheses: p, q
-- 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).reverse = Walk.map f p.reverse
have nil : ∀ {u : V},
  Eq (α := G'.Walk ((f : (a : V) → V') u) ((f : (a : V) → V') u)) (reverse (Walk.map f nil)) (Walk.map f (reverse 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},
    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))
⊢ (Walk.map f p).reverse = Walk.map f p.reverse
have 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 (cons h p)).reverse = Walk.map f (cons h p).reverse
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).support = List.map (⇑f : (a : V) → V') p.support
have nil : ∀ {u : V},
  support (u := (f : (a : V) → V') u) (Walk.map f nil) =
    List.map.{u, v} (α := V) (⇑f : (a : V) → V') (support (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},
    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)
⊢ (Walk.map f p).support = List.map (⇑f : (a : V) → V') p.support
have 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 (cons h p)).support = List.map (⇑f : (a : V) → V') (cons h p).support
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).darts = List.map f.mapDart p.darts
have nil : ∀ {u : V}, darts (u := (f : (a : V) → V') u) (Walk.map f nil) = List.map f.mapDart (darts (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}, darts (u := (f : (a : V) → V') u) (Walk.map f Walk.nil) = List.map f.mapDart (darts (u := u) Walk.nil)
⊢ (Walk.map f p).darts = List.map f.mapDart p.darts
have 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 (cons h p)).darts = List.map f.mapDart (cons h p).darts
Tactic: induction p