awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Operations (hypothesis)
Goal:
V : Type u
G : SimpleGraph V
u v : V
p q : G.Walk u v
h : p.support = q.support
this : Eq.{u + 1} (α := G.Dart → V) (Prod.fst ∘ Dart.toProd) fun (d : G.Dart) ↦ d.toProd.1
⊢ (List.map Dart.toProd p.darts).unzip = (List.map Dart.toProd q.darts).unzip
have this₁ : Eq.{u + 1} (α := G.Dart → V) (Prod.snd ∘ Dart.toProd) fun (d : G.Dart) ↦ d.toProd.2
Tactic: have : Prod.snd ∘ Dart.toProd = fun d : G.Dart ↦ d.snd := rfl
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Operations (goal)
Goal:
V : Type u
G : SimpleGraph V
t u v w : V
p : G.Walk u v
p' : G.Walk v w
⊢ t ∈ (p.append p').support.tail ↔ t ∈ p.support.tail ∨ t ∈ p'.support.tail
have rw : t ∈ p.support.tail ++ p'.support.tail ↔ t ∈ p.support.tail ∨ t ∈ p'.support.tail
Tactic: rw [tail_support_append, List.mem_append]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Operations (goal)
Goal:
V : Type u
G : SimpleGraph V
t u v w : V
p : G.Walk u v
p' : G.Walk v w
rw : t ∈ p.support.tail ++ p'.support.tail ↔ t ∈ p.support.tail ∨ t ∈ p'.support.tail
⊢ t ∈ (p.append p').support.tail ↔ t ∈ p.support.tail ∨ t ∈ p'.support.tail
have rw₁ : t ∈ p.support.tail ∨ t ∈ p'.support.tail ↔ t ∈ p.support.tail ∨ t ∈ p'.support.tail
Tactic: rw [tail_support_append, List.mem_append]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Operations (goal)
Goal:
V : Type u
G : SimpleGraph V
t u v w : V
p : G.Walk u v
p' : G.Walk v w
⊢ t ∈ (p.append p').support ↔ t ∈ p.support ∨ t ∈ p'.support
have simp : t = u ∨ t ∈ p.support.tail ∨ t ∈ p'.support.tail ↔ (t = u ∨ t ∈ p.support.tail) ∨ t = v ∨ t ∈ p'.support.tail
Tactic: simp only [mem_support_iff, mem_tail_support_append_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Operations (goal)
Goal:
V : Type u
G : SimpleGraph V
t u v w : V
p : G.Walk u v
p' : G.Walk v w
⊢ t = u ∨ t ∈ p.support.tail ∨ t ∈ p'.support.tail ↔ (t = u ∨ t ∈ p.support.tail) ∨ t = v ∨ t ∈ p'.support.tail
have inl : ∀ (p : G.Walk u t) (p' : G.Walk t w),
  t = u ∨ t ∈ p.support.tail ∨ t ∈ p'.support.tail ↔ (t = u ∨ t ∈ p.support.tail) ∨ t = t ∨ t ∈ p'.support.tail
Tactic: obtain rfl | h := eq_or_ne t v
Cleared hypotheses: v, p, p'
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Operations (goal)
Goal:
V : Type u
G : SimpleGraph V
t u v w : V
p : G.Walk u v
p' : G.Walk v w
inl :
  ∀ (p : G.Walk u t) (p' : G.Walk t w),
    t = u ∨ t ∈ p.support.tail ∨ t ∈ p'.support.tail ↔ (t = u ∨ t ∈ p.support.tail) ∨ t = t ∨ t ∈ p'.support.tail
⊢ t = u ∨ t ∈ p.support.tail ∨ t ∈ p'.support.tail ↔ (t = u ∨ t ∈ p.support.tail) ∨ t = v ∨ t ∈ p'.support.tail
have inr : ∀ (h : t ≠ v),
  t = u ∨ t ∈ p.support.tail ∨ t ∈ p'.support.tail ↔ (t = u ∨ t ∈ p.support.tail) ∨ t = v ∨ t ∈ p'.support.tail
Tactic: obtain rfl | h := eq_or_ne t v
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Operations (goal)
Goal:
V : Type u
G : SimpleGraph V
t u w : V
p : G.Walk u t
p' : G.Walk t w
⊢ t = u ∨ t ∈ p.support.tail ∨ t ∈ p'.support.tail ↔ (t = u ∨ t ∈ p.support.tail) ∨ t = t ∨ t ∈ p'.support.tail
have inl : ∀ (p : G.Walk t t),
  t = t ∨ t ∈ p.support.tail ∨ t ∈ p'.support.tail ↔ (t = t ∨ t ∈ p.support.tail) ∨ t = t ∨ t ∈ p'.support.tail
Tactic: obtain rfl | h' := eq_or_ne t u
Cleared hypotheses: u, p
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Operations (goal)
Goal:
V : Type u
G : SimpleGraph V
t u w : V
p : G.Walk u t
p' : G.Walk t w
inl :
  ∀ (p : G.Walk t t),
    t = t ∨ t ∈ p.support.tail ∨ t ∈ p'.support.tail ↔ (t = t ∨ t ∈ p.support.tail) ∨ t = t ∨ t ∈ p'.support.tail
⊢ t = u ∨ t ∈ p.support.tail ∨ t ∈ p'.support.tail ↔ (t = u ∨ t ∈ p.support.tail) ∨ t = t ∨ t ∈ p'.support.tail
have inl₁ : ∀ (h' : t ≠ u),
  t = u ∨ t ∈ p.support.tail ∨ t ∈ p'.support.tail ↔ (t = u ∨ t ∈ p.support.tail) ∨ t = t ∨ t ∈ p'.support.tail
Tactic: obtain rfl | h' := eq_or_ne t u
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Operations (goal)
Goal:
V : Type u
G : SimpleGraph V
t u v w : V
p : G.Walk u v
p' : G.Walk v w
h : t ≠ v
⊢ t = u ∨ t ∈ p.support.tail ∨ t ∈ p'.support.tail ↔ (t = u ∨ t ∈ p.support.tail) ∨ t = v ∨ t ∈ p'.support.tail
have inr : ∀ (p : G.Walk t v),
  t = t ∨ t ∈ p.support.tail ∨ t ∈ p'.support.tail ↔ (t = t ∨ t ∈ p.support.tail) ∨ t = v ∨ t ∈ p'.support.tail
Tactic: obtain rfl | h' := eq_or_ne t u
Cleared hypotheses: u, p
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Operations (goal)
Goal:
V : Type u
G : SimpleGraph V
t u v w : V
p : G.Walk u v
p' : G.Walk v w
h : t ≠ v
inr :
  ∀ (p : G.Walk t v),
    t = t ∨ t ∈ p.support.tail ∨ t ∈ p'.support.tail ↔ (t = t ∨ t ∈ p.support.tail) ∨ t = v ∨ t ∈ p'.support.tail
⊢ t = u ∨ t ∈ p.support.tail ∨ t ∈ p'.support.tail ↔ (t = u ∨ t ∈ p.support.tail) ∨ t = v ∨ t ∈ p'.support.tail
have inr₁ : ∀ (h' : t ≠ u),
  t = u ∨ t ∈ p.support.tail ∨ t ∈ p'.support.tail ↔ (t = u ∨ t ∈ p.support.tail) ∨ t = v ∨ t ∈ p'.support.tail
Tactic: obtain rfl | h' := eq_or_ne t u
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Operations (hypothesis)
Goal:
V : Type u
G : SimpleGraph V
t u w : V
p : G.Walk u t
p' : G.Walk t w
h' : t ≠ u
⊢ t = u ∨ t ∈ p.support.tail ∨ t ∈ p'.support.tail ↔ (t = u ∨ t ∈ p.support.tail) ∨ t = t ∨ t ∈ p'.support.tail
have this : u ≠ t
Tactic: have := h'.symm
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Operations (hypothesis)
Goal:
V : Type u
G : SimpleGraph V
t u w : V
p : G.Walk u t
p' : G.Walk t w
h' : t ≠ u
⊢ t = u ∨ t ∈ p.support.tail ∨ t ∈ p'.support.tail ↔ (t = u ∨ t ∈ p.support.tail) ∨ t = t ∨ t ∈ p'.support.tail
have this : u ≠ t
Tactic: try have := h'.symm
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Operations (hypothesis)
Goal:
V : Type u
G : SimpleGraph V
t u v w : V
p : G.Walk u v
p' : G.Walk v w
h : t ≠ v
h' : t ≠ u
⊢ t = u ∨ t ∈ p.support.tail ∨ t ∈ p'.support.tail ↔ (t = u ∨ t ∈ p.support.tail) ∨ t = v ∨ t ∈ p'.support.tail
have this : u ≠ t
Tactic: have := h'.symm
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Operations (hypothesis)
Goal:
V : Type u
G : SimpleGraph V
t u v w : V
p : G.Walk u v
p' : G.Walk v w
h : t ≠ v
h' : t ≠ u
⊢ t = u ∨ t ∈ p.support.tail ∨ t ∈ p'.support.tail ↔ (t = u ∨ t ∈ p.support.tail) ∨ t = v ∨ t ∈ p'.support.tail
have this : u ≠ t
Tactic: try have := h'.symm
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Operations (goal)
Goal:
V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk u v
p' : G.Walk v w
⊢ (↑(p.append p').support : Multiset V) = {u} + (↑p.support.tail : Multiset V) + (↑p'.support.tail : Multiset V)
have rw : (↑(p.support ++ p'.support.tail) : Multiset V) = {u} + (↑p.support.tail : Multiset V) + (↑p'.support.tail : Multiset V)
Tactic: rw [support_append, ← Multiset.coe_add, coe_support]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Operations (goal)
Goal:
V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk u v
p' : G.Walk v w
rw :
  (↑(p.support ++ p'.support.tail) : Multiset V) =
    {u} + (↑p.support.tail : Multiset V) + (↑p'.support.tail : Multiset V)
⊢ (↑(p.append p').support : Multiset V) = {u} + (↑p.support.tail : Multiset V) + (↑p'.support.tail : Multiset V)
have rw₁ : (↑p.support : Multiset V) + (↑p'.support.tail : Multiset V) =
  {u} + (↑p.support.tail : Multiset V) + (↑p'.support.tail : Multiset V)
Tactic: rw [support_append, ← Multiset.coe_add, coe_support]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Operations (goal)
Goal:
V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk u v
p' : G.Walk v w
rw :
  (↑(p.support ++ p'.support.tail) : Multiset V) =
    {u} + (↑p.support.tail : Multiset V) + (↑p'.support.tail : Multiset V)
rw₁ :
  (↑p.support : Multiset V) + (↑p'.support.tail : Multiset V) =
    {u} + (↑p.support.tail : Multiset V) + (↑p'.support.tail : Multiset V)
⊢ (↑(p.append p').support : Multiset V) = {u} + (↑p.support.tail : Multiset V) + (↑p'.support.tail : Multiset V)
have rw₂ : {u} + (↑p.support.tail : Multiset V) + (↑p'.support.tail : Multiset V) =
  {u} + (↑p.support.tail : Multiset V) + (↑p'.support.tail : Multiset V)
Tactic: rw [support_append, ← Multiset.coe_add, coe_support]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Operations (goal)
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
u v w : V
p : G.Walk u v
p' : G.Walk v w
⊢ (↑(p.append p').support : Multiset V) = (↑p.support : Multiset V) + (↑p'.support : Multiset V) - {v}
have simp_rw : (↑(p.support ++ p'.support.tail) : Multiset V) = (↑p.support : Multiset V) + (↑p'.support : Multiset V) - {v}
Tactic: simp_rw [support_append, ← Multiset.coe_add, coe_support, add_comm ({v} : Multiset V),
    ← add_assoc, add_tsub_cancel_right]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Operations (goal)
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
u v w : V
p : G.Walk u v
p' : G.Walk v w
simp_rw : (↑(p.support ++ p'.support.tail) : Multiset V) = (↑p.support : Multiset V) + (↑p'.support : Multiset V) - {v}
⊢ (↑(p.append p').support : Multiset V) = (↑p.support : Multiset V) + (↑p'.support : Multiset V) - {v}
have simp_rw₁ : (↑p.support : Multiset V) + (↑p'.support.tail : Multiset V) =
  (↑p.support : Multiset V) + (↑p'.support : Multiset V) - {v}
Tactic: simp_rw [support_append, ← Multiset.coe_add, coe_support, add_comm ({v} : Multiset V),
    ← add_assoc, add_tsub_cancel_right]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Operations (goal)
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
u v w : V
p : G.Walk u v
p' : G.Walk v w
simp_rw : (↑(p.support ++ p'.support.tail) : Multiset V) = (↑p.support : Multiset V) + (↑p'.support : Multiset V) - {v}
simp_rw₁ :
  (↑p.support : Multiset V) + (↑p'.support.tail : Multiset V) =
    (↑p.support : Multiset V) + (↑p'.support : Multiset V) - {v}
⊢ (↑(p.append p').support : Multiset V) = (↑p.support : Multiset V) + (↑p'.support : Multiset V) - {v}
have simp_rw₂ : {u} + (↑p.support.tail : Multiset V) + (↑p'.support.tail : Multiset V) =
  {u} + (↑p.support.tail : Multiset V) + ({v} + (↑p'.support.tail : Multiset V)) - {v}
Tactic: simp_rw [support_append, ← Multiset.coe_add, coe_support, add_comm ({v} : Multiset V),
    ← add_assoc, add_tsub_cancel_right]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Operations (goal)
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
u v w : V
p : G.Walk u v
p' : G.Walk v w
simp_rw : (↑(p.support ++ p'.support.tail) : Multiset V) = (↑p.support : Multiset V) + (↑p'.support : Multiset V) - {v}
simp_rw₁ :
  (↑p.support : Multiset V) + (↑p'.support.tail : Multiset V) =
    (↑p.support : Multiset V) + (↑p'.support : Multiset V) - {v}
simp_rw₂ :
  {u} + (↑p.support.tail : Multiset V) + (↑p'.support.tail : Multiset V) =
    {u} + (↑p.support.tail : Multiset V) + ({v} + (↑p'.support.tail : Multiset V)) - {v}
⊢ (↑(p.append p').support : Multiset V) = (↑p.support : Multiset V) + (↑p'.support : Multiset V) - {v}
have simp_rw₃ : {u} + (↑p.support.tail : Multiset V) + (↑p'.support.tail : Multiset V) =
  {u} + (↑p.support.tail : Multiset V) + ((↑p'.support.tail : Multiset V) + {v}) - {v}
Tactic: simp_rw [support_append, ← Multiset.coe_add, coe_support, add_comm ({v} : Multiset V),
    ← add_assoc, add_tsub_cancel_right]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Operations (goal)
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
u v w : V
p : G.Walk u v
p' : G.Walk v w
simp_rw : (↑(p.support ++ p'.support.tail) : Multiset V) = (↑p.support : Multiset V) + (↑p'.support : Multiset V) - {v}
simp_rw₁ :
  (↑p.support : Multiset V) + (↑p'.support.tail : Multiset V) =
    (↑p.support : Multiset V) + (↑p'.support : Multiset V) - {v}
simp_rw₂ :
  {u} + (↑p.support.tail : Multiset V) + (↑p'.support.tail : Multiset V) =
    {u} + (↑p.support.tail : Multiset V) + ({v} + (↑p'.support.tail : Multiset V)) - {v}
simp_rw₃ :
  {u} + (↑p.support.tail : Multiset V) + (↑p'.support.tail : Multiset V) =
    {u} + (↑p.support.tail : Multiset V) + ((↑p'.support.tail : Multiset V) + {v}) - {v}
⊢ (↑(p.append p').support : Multiset V) = (↑p.support : Multiset V) + (↑p'.support : Multiset V) - {v}
have simp_rw₄ : {u} + (↑p.support.tail : Multiset V) + (↑p'.support.tail : Multiset V) =
  {u} + (↑p.support.tail : Multiset V) + (↑p'.support.tail : Multiset V) + {v} - {v}
Tactic: simp_rw [support_append, ← Multiset.coe_add, coe_support, add_comm ({v} : Multiset V),
    ← add_assoc, add_tsub_cancel_right]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Operations (hypothesis)
Goal:
V : Type u
G : SimpleGraph V
u v_1 : V
p_1 : G.Walk u v_1
v u' : V
h₁ : G.Adj u u'
v' : V
h₂ : G.Adj u' v'
p : G.Walk v' v
⊢ ofSupport (cons h₁ (cons h₂ p)).support ⋯ ⋯ = (cons h₁ (cons h₂ p)).copy ⋯ ⋯
have this : ofSupport (cons h₂ p).support sorry sorry = (cons h₂ p).copy sorry sorry
Tactic: have := p.cons h₂ |>.ofSupport_support
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Operations (goal)
Goal:
V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk u v
h : G.Adj v w
⊢ (p.concat h).darts = p.darts.concat { fst := v, snd := w, adj := h }
have nil : ∀ {u : V} (h : G.Adj u w), (concat nil h).darts = List.concat (darts (u := u) nil) { fst := u, snd := w, adj := h }
Tactic: induction p
Cleared hypotheses: p, h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Operations (goal)
Goal:
V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk u v
h : G.Adj v w
nil :
  ∀ {u : V} (h : G.Adj u w),
    (concat Walk.nil h).darts = List.concat (darts (u := u) Walk.nil) { fst := u, snd := w, adj := h }
⊢ (p.concat h).darts = p.darts.concat { fst := v, snd := w, adj := h }
have cons : ∀ {u v w_1 : V} (h : G.Adj u v) (p : G.Walk v w_1),
  (∀ (h : G.Adj w_1 w), (p.concat h).darts = p.darts.concat { fst := w_1, snd := w, adj := h }) →
    ∀ (h_1 : G.Adj w_1 w), ((cons h p).concat h_1).darts = (cons h p).darts.concat { fst := w_1, snd := w, adj := h_1 }
Tactic: induction p
Cleared hypotheses: p, h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Operations (goal)
Goal:
V : Type u
G : SimpleGraph V
u v u' v' : V
p : G.Walk u v
hu : u = u'
hv : v = v'
⊢ (p.copy hu hv).darts = p.darts
have subst_vars : ∀ (p : G.Walk u' v'), (p.copy sorry sorry).darts = p.darts
Tactic: subst_vars
Cleared hypotheses: u, v, p, hu, hv
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Operations (goal)
Goal:
V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk u v
p' : G.Walk v w
⊢ (p.append p').darts = p.darts ++ p'.darts
have nil : ∀ {u : V} (p' : G.Walk u w), (append nil p').darts = darts (u := u) nil ++ p'.darts
Tactic: induction p
Cleared hypotheses: p, p'
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Operations (goal)
Goal:
V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk u v
p' : G.Walk v w
nil : ∀ {u : V} (p' : G.Walk u w), (append Walk.nil p').darts = darts (u := u) Walk.nil ++ p'.darts
⊢ (p.append p').darts = p.darts ++ p'.darts
have cons : ∀ {u v w_1 : V} (h : G.Adj u v) (p : G.Walk v w_1),
  (∀ (p' : G.Walk w_1 w), (p.append p').darts = p.darts ++ p'.darts) →
    ∀ (p' : G.Walk w_1 w), ((cons h p).append p').darts = (cons h p).darts ++ p'.darts
Tactic: induction p
Cleared hypotheses: p, 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
⊢ p.reverse.darts = (List.map Dart.symm p.darts).reverse
have nil : ∀ {u : V},
  Eq.{u + 1} (α := List G.Dart) (darts (u := u) (reverse nil)) (List.reverse (List.map Dart.symm (darts (u := u) 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} (α := List G.Dart) (darts (u := u) (reverse Walk.nil))
      (List.reverse (List.map Dart.symm (darts (u := u) Walk.nil)))
⊢ p.reverse.darts = (List.map Dart.symm p.darts).reverse
have cons : ∀ {u v w : V} (h : G.Adj u v) (p : G.Walk v w),
  p.reverse.darts = (List.map Dart.symm p.darts).reverse →
    (cons h p).reverse.darts = (List.map Dart.symm (cons h p).darts).reverse
Tactic: induction p
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Operations (hypothesis)
Goal:
V : Type u
G : SimpleGraph V
u v_1 : V
p_1 : G.Walk u v_1
hp : ¬p_1.Nil
v u' : V
h₁ : G.Adj u u'
v' : V
h₂ : G.Adj u' v'
p : G.Walk v' v
h : ¬(cons h₁ (cons h₂ p)).Nil
⊢ ofDarts (cons h₁ (cons h₂ p)).darts ⋯ ⋯ = (cons h₁ (cons h₂ p)).copy ⋯ ⋯
have this : Eq (α := G.Walk ((cons h₂ p).darts.head sorry).toProd.1 ((cons h₂ p).darts.getLast sorry).toProd.2)
  (ofDarts (cons h₂ p).darts sorry sorry : G.Walk ((cons h₂ p).darts.head sorry).toProd.1 ((cons h₂ p).darts.getLast sorry).toProd.2)
  ((cons h₂ p).copy sorry sorry : G.Walk ((cons h₂ p).darts.head sorry).toProd.1 ((cons h₂ p).darts.getLast sorry).toProd.2)
Tactic: have := p.cons h₂ |>.ofDarts_darts not_nil_cons
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Operations (goal)
Goal:
V : Type u
G : SimpleGraph V
u v u' v' : V
p : G.Walk u v
hu : u = u'
hv : v = v'
⊢ (p.copy hu hv).edges = p.edges
have subst_vars : ∀ (p : G.Walk u' v'), (p.copy sorry sorry).edges = p.edges
Tactic: subst_vars
Cleared hypotheses: u, v, p, hu, hv
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Operations (goal)
Goal:
V : Type u
G : SimpleGraph V
t u v w : V
p : G.Walk v w
he : s(t, u) ∈ p.edges
⊢ t ∈ p.support
have obtain : ∀ (d : G.Dart) (hd : d ∈ p.darts) (he : d.edge = s(t, u)), t ∈ p.support
Tactic: obtain ⟨d, hd, he⟩ := List.mem_map.mp he
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Operations (hypothesis)
Goal:
V : Type u
G : SimpleGraph V
t u v w : V
p : G.Walk v w
he_1 : s(t, u) ∈ p.edges
d : G.Dart
hd : d ∈ p.darts
he : d.edge = s(t, u)
⊢ t ∈ p.support
have he₁ : d.toProd.1 = t ∧ d.toProd.2 = u ∨ d.toProd.1 = u ∧ d.toProd.2 = t
Tactic: rw [dart_edge_eq_mk'_iff'] at he
Cleared hypotheses: he
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Operations (goal)
Goal:
V : Type u
G : SimpleGraph V
t u v w : V
p : G.Walk v w
he_1 : s(t, u) ∈ p.edges
d : G.Dart
hd : d ∈ p.darts
he : d.toProd.1 = t ∧ d.toProd.2 = u ∨ d.toProd.1 = u ∧ d.toProd.2 = t
⊢ t ∈ p.support
have inl : ∀ (he : s(d.toProd.1, d.toProd.2) ∈ p.edges), d.toProd.1 ∈ p.support
Tactic: rcases he with ⟨rfl, rfl⟩ | ⟨rfl, rfl⟩
Cleared hypotheses: t, u, he_1, he
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Operations (goal)
Goal:
V : Type u
G : SimpleGraph V
t u v w : V
p : G.Walk v w
he_1 : s(t, u) ∈ p.edges
d : G.Dart
hd : d ∈ p.darts
he : d.toProd.1 = t ∧ d.toProd.2 = u ∨ d.toProd.1 = u ∧ d.toProd.2 = t
inl : ∀ (he : s(d.toProd.1, d.toProd.2) ∈ p.edges), d.toProd.1 ∈ p.support
⊢ t ∈ p.support
have inr : ∀ (he : s(d.toProd.2, d.toProd.1) ∈ p.edges), d.toProd.2 ∈ p.support
Tactic: rcases he with ⟨rfl, rfl⟩ | ⟨rfl, rfl⟩
Cleared hypotheses: t, u, he_1, he
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Operations (goal)
Goal:
V : Type u
G : SimpleGraph V
u v u_1 v_1 w : V
h_1 : G.Adj u_1 v_1
p' : G.Walk v_1 w
ih : ∀ (h : p'.support.Nodup), p'.edges.Nodup
h : (cons h_1 p').support.Nodup
⊢ (cons h_1 p').edges.Nodup
have cons : ∀ (h : u_1 ∉ p'.support ∧ p'.support.Nodup), s(u_1, v_1) ∉ p'.edges ∧ p'.edges.Nodup
Tactic: simp only [support_cons, List.nodup_cons, edges_cons] at h ⊢
Cleared hypotheses: h
-- 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
h : p.support.Nodup
⊢ p.edges.Nodup
have nil : ∀ {u : V} (h : List.Nodup.{u} (α := V) (support (G := G) (u := u) nil)),
  List.Nodup.{u} (α := Sym2 V) (edges (G := G) (u := u) nil)
Tactic: induction p with
  | nil => simp
  | cons _ p' ih =>
    simp only [support_cons, List.nodup_cons, edges_cons] at h ⊢
    exact ⟨(h.1 <| fst_mem_support_of_mem_edges p' ·), ih h.2⟩
Cleared hypotheses: p, h
-- 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
h : p.support.Nodup
nil :
  ∀ {u : V} (h : List.Nodup.{u} (α := V) (support (G := G) (u := u) Walk.nil)),
    List.Nodup.{u} (α := Sym2 V) (edges (G := G) (u := u) Walk.nil)
⊢ p.edges.Nodup
have cons : ∀ {u v w : V} (h : G.Adj u v) (p' : G.Walk v w) (ih : ∀ (h : p'.support.Nodup), p'.edges.Nodup)
  (h_1 : (cons h p').support.Nodup), (cons h p').edges.Nodup
Tactic: induction p with
  | nil => simp
  | cons _ p' ih =>
    simp only [support_cons, List.nodup_cons, edges_cons] at h ⊢
    exact ⟨(h.1 <| fst_mem_support_of_mem_edges p' ·), ih h.2⟩
Cleared hypotheses: p, h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Operations (goal)
Goal:
V : Type u
G : SimpleGraph V
u : V
p : G.Walk u u
⊢ p.reverse.support.tail.Nodup ↔ p.support.tail.Nodup
have refine : getElem? (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) p.support 0 = p.support.getLast?
Tactic: refine p.support_reverse ▸ p.support.nodup_tail_reverse ?_
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Operations (goal)
Goal:
V : Type u
G : SimpleGraph V
u : V
p : G.Walk u u
⊢ p.support.length - 1 ≤ p.length
have rw : p.length + 1 - 1 ≤ p.length
Tactic: rw [Walk.length_support]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Operations (goal)
Goal:
V : Type u
G : SimpleGraph V
u : V
p : G.Walk u u
⊢ getElem? (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) p.support 0 = p.support.getLast?
have rw : some (p.getVert 0) = some (p.getVert (p.support.length - 1))
Tactic: rw [← getVert_eq_support_getElem? _ (by lia), List.getLast?_eq_getElem?,
    ← getVert_eq_support_getElem? _ (by rw [Walk.length_support]; lia)]
-- 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.reverse.edgeSet = p.edgeSet
have h : ∀ (x : Sym2 V), x ∈ p.reverse.edgeSet ↔ x ∈ p.edgeSet
Tactic: ext
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Operations (goal)
Goal:
V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk u v
h : G.Adj v w
⊢ (p.concat h).edgeSet = insert s(v, w) p.edgeSet
have h₁ : ∀ (x : Sym2 V), x ∈ (p.concat h).edgeSet ↔ x ∈ insert s(v, w) p.edgeSet
Tactic: ext
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Operations (goal)
Goal:
V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk u v
q : G.Walk v w
⊢ (p.append q).edgeSet = p.edgeSet ∪ q.edgeSet
have h : ∀ (x : Sym2 V), x ∈ (p.append q).edgeSet ↔ x ∈ p.edgeSet ∪ q.edgeSet
Tactic: ext
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Operations (goal)
Goal:
V : Type u
G : SimpleGraph V
u v u' v' : V
p : G.Walk u v
hu : u = u'
hv : v = v'
⊢ (p.copy hu hv).edgeSet = p.edgeSet
have h : ∀ (x : Sym2 V), x ∈ (p.copy hu hv).edgeSet ↔ x ∈ p.edgeSet
Tactic: ext
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Operations (goal)
Goal:
V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk u v
q : G.Walk v w
⊢ (p.append q).Nil ↔ p.Nil ∧ q.Nil
have nil : ∀ {q : G.Walk u w}, (append nil q).Nil ↔ Nil.{u} (V := V) (G := G) (v := u) nil ∧ q.Nil
Tactic: cases p
Cleared hypotheses: v, p, q
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Operations (goal)
Goal:
V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk u v
q : G.Walk v w
nil : ∀ {q : G.Walk u w}, (append Walk.nil q).Nil ↔ Nil.{u} (V := V) (G := G) (v := u) Walk.nil ∧ q.Nil
⊢ (p.append q).Nil ↔ p.Nil ∧ q.Nil
have cons : ∀ {v_1 : V} (h : G.Adj u v_1) (p : G.Walk v_1 v), ((cons h p).append q).Nil ↔ (cons h p).Nil ∧ q.Nil
Tactic: cases p
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Operations (goal)
Goal:
V : Type u
G : SimpleGraph V
u w : V
q : G.Walk u w
⊢ (append nil q).Nil ↔ Nil.{u} (V := V) (G := G) (v := u) nil ∧ q.Nil
have nil : Nil.{u} (V := V) (G := G) (v := u) (append nil nil) ↔
  Nil.{u} (V := V) (G := G) (v := u) nil ∧ Nil.{u} (V := V) (G := G) (v := u) nil
Tactic: cases q
Cleared hypotheses: w, q