awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Basic (goal)
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
⊢ (↑p.support : Multiset V) = {u} + (↑p.support.tail : Multiset V)
have nil : (↑(support (G := G) (u := u) nil) : Multiset V) =
  HAdd.hAdd (α := Multiset V) {u} (↑(List.tail (support (G := G) (u := u) nil)) : Multiset V)
Tactic: cases p
Cleared hypotheses: v, p
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Basic (goal)
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
nil :
  (↑(support (G := G) (u := u) Walk.nil) : Multiset V) =
    HAdd.hAdd (α := Multiset V) {u} (↑(List.tail (support (G := G) (u := u) Walk.nil)) : Multiset V)
⊢ (↑p.support : Multiset V) = {u} + (↑p.support.tail : Multiset V)
have cons : ∀ {v_1 : V} (h : G.Adj u v_1) (p : G.Walk v_1 v),
  (↑(cons h p).support : Multiset V) = {u} + (↑(cons h p).support.tail : Multiset V)
Tactic: cases p
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Basic (goal)
Goal:
V : Type u
G : SimpleGraph V
d : G.Dart
v w : V
h : d.toProd.2 = v
p : G.Walk v w
⊢ List.IsChain G.DartAdj (d :: p.darts)
have nil : ∀ {u : V} {d : G.Dart} (h : d.toProd.2 = u), List.IsChain G.DartAdj (d :: darts (u := u) nil)
Tactic: induction p generalizing d with
  | nil => exact .singleton _
  | cons h' p ih => exact .cons_cons h (ih rfl)
Cleared hypotheses: d, h, p
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Basic (goal)
Goal:
V : Type u
G : SimpleGraph V
d : G.Dart
v w : V
h : d.toProd.2 = v
p : G.Walk v w
nil : ∀ {u : V} {d : G.Dart} (h : d.toProd.2 = u), List.IsChain G.DartAdj (d :: darts (u := u) Walk.nil)
⊢ List.IsChain G.DartAdj (d :: p.darts)
have cons : ∀ {u v w : V} (h' : G.Adj u v) (p : G.Walk v w)
  (ih : ∀ {d : G.Dart} (h : d.toProd.2 = v), List.IsChain G.DartAdj (d :: p.darts)) {d : G.Dart} (h : d.toProd.2 = u),
  List.IsChain G.DartAdj (d :: (cons h' p).darts)
Tactic: induction p generalizing d with
  | nil => exact .singleton _
  | cons h' p ih => exact .cons_cons h (ih rfl)
Cleared hypotheses: d, h, p
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Basic (goal)
Goal:
V : Type u
G : SimpleGraph V
u v v_1 : V
h' : G.Adj u v_1
p' : G.Walk v_1 v
e : Sym2 V
h : e ∈ (cons h' p').edges
⊢ e ∈ G.edgeSet
have head : { fst := u, snd := v_1, adj := h' : G.Dart }.edge ∈ G.edgeSet
Tactic: cases h
Cleared hypotheses: e, h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Basic (goal)
Goal:
V : Type u
G : SimpleGraph V
u v v_1 : V
h' : G.Adj u v_1
p' : G.Walk v_1 v
e : Sym2 V
h : e ∈ (cons h' p').edges
head : { fst := u, snd := v_1, adj := h' : G.Dart }.edge ∈ G.edgeSet
⊢ e ∈ G.edgeSet
have tail : List.Mem e (List.map Dart.edge p'.darts) → e ∈ G.edgeSet
Tactic: cases h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Basic (goal)
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
⊢ u :: List.map (fun (x : G.Dart) ↦ x.toProd.2) p.darts = p.support
have nil : ∀ {u : V}, u :: List.map (fun (x : G.Dart) ↦ x.toProd.2) (darts (u := u) nil) = support (G := G) (u := u) nil
Tactic: induction p
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Basic (goal)
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
nil :
  ∀ {u : V},
    u :: List.map (fun (x : G.Dart) ↦ x.toProd.2) (darts (u := u) Walk.nil) = support (G := G) (u := u) Walk.nil
⊢ u :: List.map (fun (x : G.Dart) ↦ x.toProd.2) p.darts = p.support
have cons : ∀ {u v w : V} (h : G.Adj u v) (p : G.Walk v w),
  v :: List.map (fun (x : G.Dart) ↦ x.toProd.2) p.darts = p.support →
    u :: List.map (fun (x : G.Dart) ↦ x.toProd.2) (cons h p).darts = (cons h p).support
Tactic: induction p
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Basic (goal)
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
⊢ List.map (fun (x : G.Dart) ↦ x.toProd.1) p.darts ++ [v] = p.support
have nil : ∀ {u : V}, List.map (fun (x : G.Dart) ↦ x.toProd.1) (darts (u := u) nil) ++ [u] = support (G := G) (u := u) nil
Tactic: induction p
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Basic (goal)
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
nil :
  ∀ {u : V},
    List.map (fun (x : G.Dart) ↦ x.toProd.1) (darts (u := u) Walk.nil) ++ [u] = support (G := G) (u := u) Walk.nil
⊢ List.map (fun (x : G.Dart) ↦ x.toProd.1) p.darts ++ [v] = p.support
have cons : ∀ {u v w : V} (h : G.Adj u v) (p : G.Walk v w),
  List.map (fun (x : G.Dart) ↦ x.toProd.1) p.darts ++ [w] = p.support →
    List.map (fun (x : G.Dart) ↦ x.toProd.1) (cons h p).darts ++ [w] = (cons h p).support
Tactic: induction p
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Basic (goal)
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
⊢ p.support.length = p.length + 1
have nil : ∀ {u : V}, List.length.{u} (α := V) (support (G := G) (u := u) nil) = length.{u} (V := V) (G := G) (u := u) nil + 1
Tactic: induction p
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Basic (goal)
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
nil :
  ∀ {u : V},
    List.length.{u} (α := V) (support (G := G) (u := u) Walk.nil) = length.{u} (V := V) (G := G) (u := u) Walk.nil + 1
⊢ p.support.length = p.length + 1
have cons : ∀ {u v w : V} (h : G.Adj u v) (p : G.Walk v w),
  p.support.length = p.length + 1 → (cons h p).support.length = (cons h p).length + 1
Tactic: induction p
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Basic (goal)
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
⊢ p.darts.length = p.length
have nil : ∀ {u : V}, List.length.{u} (α := G.Dart) (darts (u := u) nil) = length.{u} (V := V) (G := G) (u := u) nil
Tactic: induction p
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Basic (goal)
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
nil :
  ∀ {u : V}, List.length.{u} (α := G.Dart) (darts (u := u) Walk.nil) = length.{u} (V := V) (G := G) (u := u) Walk.nil
⊢ p.darts.length = p.length
have cons : ∀ {u v w : V} (h : G.Adj u v) (p : G.Walk v w), p.darts.length = p.length → (cons h p).darts.length = (cons h p).length
Tactic: induction p
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Basic (goal)
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
⊢ getElem (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) p.support 0 ⋯ = u
have nil : getElem (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) (support (G := G) (u := u) nil) 0 sorry = u
Tactic: cases p
Cleared hypotheses: v, p
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Basic (goal)
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
nil : getElem (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) (support (G := G) (u := u) Walk.nil) 0 ⋯ = u
⊢ getElem (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) p.support 0 ⋯ = u
have cons : ∀ {v_1 : V} (h : G.Adj u v_1) (p : G.Walk v_1 v),
  getElem (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) (cons h p).support 0 sorry = u
Tactic: cases p
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Basic (goal)
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
⊢ getElem (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) p.support p.length ⋯ = v
have nil : ∀ {u : V},
  getElem (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) (support (G := G) (u := u) nil)
      (length.{u} (V := V) (G := G) (u := u) nil) sorry =
    u
Tactic: induction p
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Basic (goal)
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
nil :
  ∀ {u : V},
    getElem (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) (support (G := G) (u := u) Walk.nil)
        (length.{u} (V := V) (G := G) (u := u) Walk.nil) ⋯ =
      u
⊢ getElem (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) p.support p.length ⋯ = v
have cons : ∀ {u v w : V} (h : G.Adj u v) (p : G.Walk v w),
  getElem (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) p.support p.length sorry = w →
    getElem (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) (cons h p).support (cons h p).length sorry = w
Tactic: induction p
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Basic (goal)
Goal:
V : Type u
G : SimpleGraph V
u v u' v' : V
p : G.Walk u v
h : G.Adj u' v'
⊢ { fst := u', snd := v', adj := h : G.Dart } ∈ p.darts ↔ [u', v'] <:+: p.support
have refine_1 : ∀ (h : { fst := u', snd := v', adj := h : G.Dart } ∈ p.darts),
  ∃ (k : ℕ),
    [u', v'].length + k ≤ p.support.length ∧
      ∀ (i : ℕ) (h : i < [u', v'].length),
        getElem? (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) p.support (i + k) =
          some (getElem (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) [u', v'] i h)
Tactic: refine .trans ⟨fun h ↦ ?_, fun ⟨i, hi, h⟩ ↦ ?_⟩ List.infix_iff_getElem?.symm
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Basic (goal)
Goal:
V : Type u
G : SimpleGraph V
u v u' v' : V
p : G.Walk u v
h : G.Adj u' v'
refine_1 :
  ∀ (h : { fst := u', snd := v', adj := h : G.Dart } ∈ p.darts),
    ∃ (k : ℕ),
      [u', v'].length + k ≤ p.support.length ∧
        ∀ (i : ℕ) (h : i < [u', v'].length),
          getElem? (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) p.support (i + k) =
            some (getElem (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) [u', v'] i h)
⊢ { fst := u', snd := v', adj := h : G.Dart } ∈ p.darts ↔ [u', v'] <:+: p.support
have refine_2 : (∃ (k : ℕ),
    [u', v'].length + k ≤ p.support.length ∧
      ∀ (i : ℕ) (h : i < [u', v'].length),
        getElem? (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) p.support (i + k) =
          some (getElem (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) [u', v'] i h)) →
  ∀ (i : ℕ) (hi : [u', v'].length + i ≤ p.support.length)
    (h_1 :
      ∀ (i_1 : ℕ) (h : i_1 < [u', v'].length),
        getElem? (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) p.support (i_1 + i) =
          some (getElem (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) [u', v'] i_1 h)),
    { fst := u', snd := v', adj := h : G.Dart } ∈ p.darts
Tactic: refine .trans ⟨fun h ↦ ?_, fun ⟨i, hi, h⟩ ↦ ?_⟩ List.infix_iff_getElem?.symm
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Basic (goal)
Goal:
V : Type u
G : SimpleGraph V
u v u' v' : V
p : G.Walk u v
h_1 : G.Adj u' v'
h : { fst := u', snd := v', adj := h_1 : G.Dart } ∈ p.darts
⊢ ∃ (k : ℕ),
    [u', v'].length + k ≤ p.support.length ∧
      ∀ (i : ℕ) (h : i < [u', v'].length),
        getElem? (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) p.support (i + k) =
          some (getElem (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) [u', v'] i h)
have refine_1 : ∀ (i : ℕ) (hi : i < p.darts.length)
  (h :
    getElem (valid := fun (as : List G.Dart) (i : ℕ) ↦ i < as.length) p.darts i hi =
      { fst := u', snd := v', adj := h_1 }),
  ∃ (k : ℕ),
    [u', v'].length + k ≤ p.support.length ∧
      ∀ (i : ℕ) (h : i < [u', v'].length),
        getElem? (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) p.support (i + k) =
          some (getElem (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) [u', v'] i h)
Tactic: have ⟨i, hi, h⟩ := List.getElem_of_mem h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Basic (hypothesis)
Goal:
V : Type u
G : SimpleGraph V
u v u' v' : V
p : G.Walk u v
h_1 : G.Adj u' v'
h_2 :
  ∃ (k : ℕ),
    [u', v'].length + k ≤ p.support.length ∧
      ∀ (i : ℕ) (h : i < [u', v'].length),
        getElem? (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) p.support (i + k) =
          some (getElem (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) [u', v'] i h)
i : ℕ
hi : [u', v'].length + i ≤ p.support.length
h :
  ∀ (i_1 : ℕ) (h : i_1 < [u', v'].length),
    getElem? (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) p.support (i_1 + i) =
      some (getElem (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) [u', v'] i_1 h)
⊢ { fst := u', snd := v', adj := h_1 : G.Dart } ∈ p.darts
have this : ∀ (h : 0 < [u', v'].length),
  getElem? (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) p.support (0 + i) =
    some (getElem (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) [u', v'] 0 h)
Tactic: have := h 0
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Basic (hypothesis)
Goal:
V : Type u
G : SimpleGraph V
u v u' v' : V
p : G.Walk u v
h_1 : G.Adj u' v'
h_2 :
  ∃ (k : ℕ),
    [u', v'].length + k ≤ p.support.length ∧
      ∀ (i : ℕ) (h : i < [u', v'].length),
        getElem? (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) p.support (i + k) =
          some (getElem (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) [u', v'] i h)
i : ℕ
hi : [u', v'].length + i ≤ p.support.length
h :
  ∀ (i_1 : ℕ) (h : i_1 < [u', v'].length),
    getElem? (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) p.support (i_1 + i) =
      some (getElem (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) [u', v'] i_1 h)
this :
  ∀ (h : 0 < [u', v'].length),
    getElem? (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) p.support (0 + i) =
      some (getElem (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) [u', v'] 0 h)
⊢ { fst := u', snd := v', adj := h_1 : G.Dart } ∈ p.darts
have this₁ : ∀ (h : 1 < [u', v'].length),
  getElem? (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) p.support (1 + i) =
    some (getElem (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) [u', v'] 1 h)
Tactic: have := h 1
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Basic (goal)
Goal:
V : Type u
G : SimpleGraph V
u v u' v' : V
p : G.Walk u v
h_1 : G.Adj u' v'
h_2 :
  ∃ (k : ℕ),
    [u', v'].length + k ≤ p.support.length ∧
      ∀ (i : ℕ) (h : i < [u', v'].length),
        getElem? (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) p.support (i + k) =
          some (getElem (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) [u', v'] i h)
i : ℕ
hi : [u', v'].length + i ≤ p.support.length
h :
  ∀ (i_1 : ℕ) (h : i_1 < [u', v'].length),
    getElem? (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) p.support (i_1 + i) =
      some (getElem (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) [u', v'] i_1 h)
this_1 :
  ∀ (h : 0 < [u', v'].length),
    getElem? (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) p.support (0 + i) =
      some (getElem (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) [u', v'] 0 h)
this :
  ∀ (h : 1 < [u', v'].length),
    getElem? (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) p.support (1 + i) =
      some (getElem (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) [u', v'] 1 h)
⊢ { fst := u', snd := v', adj := h_1 : G.Dart } ∈ p.darts
have h₁ : u' = (getElem (valid := fun (as : List G.Dart) (i : ℕ) ↦ i < as.length) p.darts i sorry).1.1
Tactic: convert! p.darts.getElem_mem (n := i) (by grind)
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Basic (goal)
Goal:
V : Type u
G : SimpleGraph V
u v u' v' : V
p : G.Walk u v
h_1 : G.Adj u' v'
h_2 :
  ∃ (k : ℕ),
    [u', v'].length + k ≤ p.support.length ∧
      ∀ (i : ℕ) (h : i < [u', v'].length),
        getElem? (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) p.support (i + k) =
          some (getElem (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) [u', v'] i h)
i : ℕ
hi : [u', v'].length + i ≤ p.support.length
h :
  ∀ (i_1 : ℕ) (h : i_1 < [u', v'].length),
    getElem? (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) p.support (i_1 + i) =
      some (getElem (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) [u', v'] i_1 h)
this_1 :
  ∀ (h : 0 < [u', v'].length),
    getElem? (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) p.support (0 + i) =
      some (getElem (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) [u', v'] 0 h)
this :
  ∀ (h : 1 < [u', v'].length),
    getElem? (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) p.support (1 + i) =
      some (getElem (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) [u', v'] 1 h)
h₁ : u' = (getElem (valid := fun (as : List G.Dart) (i : ℕ) ↦ i < as.length) p.darts i ⋯).1.1
⊢ { fst := u', snd := v', adj := h_1 : G.Dart } ∈ p.darts
have h₂ : v' = (getElem (valid := fun (as : List G.Dart) (i : ℕ) ↦ i < as.length) p.darts i sorry).1.2
Tactic: convert! p.darts.getElem_mem (n := i) (by grind)
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Basic (goal)
Goal:
V : Type u
G : SimpleGraph V
u v v_1 : V
h : G.Adj u v_1
p' : G.Walk v_1 v
d : G.Dart
hd : d ∈ (cons h p').darts
⊢ d.toProd.1 ∈ (cons h p').support
have simp : ∀ (hd : d = { fst := u, snd := v_1, adj := h } ∨ d ∈ p'.darts), d.toProd.1 = u ∨ d.toProd.1 ∈ p'.support
Tactic: simp only [support_cons, darts_cons, List.mem_cons] at hd ⊢
Cleared hypotheses: hd
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Basic (goal)
Goal:
V : Type u
G : SimpleGraph V
u v v_1 : V
h : G.Adj u v_1
p' : G.Walk v_1 v
d : G.Dart
hd : d = { fst := u, snd := v_1, adj := h } ∨ d ∈ p'.darts
⊢ d.toProd.1 = u ∨ d.toProd.1 ∈ p'.support
have inl : { fst := u, snd := v_1, adj := h : G.Dart }.toProd.1 = u ∨
  { fst := u, snd := v_1, adj := h : G.Dart }.toProd.1 ∈ p'.support
Tactic: rcases hd with rfl | hd
Cleared hypotheses: d, hd
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Basic (goal)
Goal:
V : Type u
G : SimpleGraph V
u v v_1 : V
h : G.Adj u v_1
p' : G.Walk v_1 v
d : G.Dart
hd : d = { fst := u, snd := v_1, adj := h } ∨ d ∈ p'.darts
inl :
  { fst := u, snd := v_1, adj := h : G.Dart }.toProd.1 = u ∨
    { fst := u, snd := v_1, adj := h : G.Dart }.toProd.1 ∈ p'.support
⊢ d.toProd.1 = u ∨ d.toProd.1 ∈ p'.support
have inr : ∀ (hd : d ∈ p'.darts), d.toProd.1 = u ∨ d.toProd.1 ∈ p'.support
Tactic: rcases hd with rfl | hd
Cleared hypotheses: hd
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Basic (goal)
Goal:
V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk u v
⊢ w ∈ p.support ↔ w = v ∨ ∃ e ∈ p.edges, w ∈ e
have nil : ∀ {u : V},
  Membership.mem (γ := List V) (support (G := G) (u := u) nil) w ↔
    w = u ∨ ∃ (e : Sym2 V), Membership.mem (γ := List (Sym2 V)) (edges (G := G) (u := u) nil) e ∧ w ∈ e
Tactic: induction p
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Basic (goal)
Goal:
V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk u v
nil :
  ∀ {u : V},
    Membership.mem (γ := List V) (support (G := G) (u := u) Walk.nil) w ↔
      w = u ∨ ∃ (e : Sym2 V), Membership.mem (γ := List (Sym2 V)) (edges (G := G) (u := u) Walk.nil) e ∧ w ∈ e
⊢ w ∈ p.support ↔ w = v ∨ ∃ e ∈ p.edges, w ∈ e
have cons : ∀ {u v w_1 : V} (h : G.Adj u v) (p : G.Walk v w_1),
  (w ∈ p.support ↔ w = w_1 ∨ ∃ e ∈ p.edges, w ∈ e) → (w ∈ (cons h p).support ↔ w = w_1 ∨ ∃ e ∈ (cons h p).edges, w ∈ e)
Tactic: induction p
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Basic (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'.darts.Nodup
h : (cons h_1 p').support.Nodup
⊢ (cons h_1 p').darts.Nodup
have cons : ∀ (h : u_1 ∉ p'.support ∧ p'.support.Nodup), { fst := u_1, snd := v_1, adj := h_1 : G.Dart } ∉ p'.darts ∧ p'.darts.Nodup
Tactic: simp only [darts_cons, support_cons, List.nodup_cons] at h ⊢
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Basic (goal)
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
h : p.support.Nodup
⊢ p.darts.Nodup
have nil : ∀ {u : V} (h : List.Nodup.{u} (α := V) (support (G := G) (u := u) nil)),
  List.Nodup.{u} (α := G.Dart) (darts (u := u) nil)
Tactic: induction p with
  | nil => simp
  | cons _ p' ih =>
    simp only [darts_cons, support_cons, List.nodup_cons] at h ⊢
    exact ⟨(h.1 <| dart_fst_mem_support_of_mem_darts p' ·), ih h.2⟩
Cleared hypotheses: p, h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Basic (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} (α := G.Dart) (darts (u := u) Walk.nil)
⊢ p.darts.Nodup
have cons : ∀ {u v w : V} (h : G.Adj u v) (p' : G.Walk v w) (ih : ∀ (h : p'.support.Nodup), p'.darts.Nodup)
  (h_1 : (cons h p').support.Nodup), (cons h p').darts.Nodup
Tactic: induction p with
  | nil => simp
  | cons _ p' ih =>
    simp only [darts_cons, support_cons, List.nodup_cons] at h ⊢
    exact ⟨(h.1 <| dart_fst_mem_support_of_mem_darts p' ·), ih h.2⟩
Cleared hypotheses: p, h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Basic (goal)
Goal:
V : Type u
G : SimpleGraph V
u v u_1 v_1 w : V
h : G.Adj u_1 v_1
p' : G.Walk v_1 w
ih : p'.edges = List.zipWith (fun (x1 x2 : V) ↦ s(x1, x2)) p'.support p'.support.tail
⊢ (cons h p').edges = List.zipWith (fun (x1 x2 : V) ↦ s(x1, x2)) (cons h p').support (cons h p').support.tail
have cons : ∀
  (ih :
    Eq.{u + 1} (α := List (Sym2 V)) (edges (G := G) (u := v_1) nil)
      (List.zipWith (fun (x1 x2 : V) ↦ s(x1, x2)) (support (G := G) (u := v_1) nil)
        (List.tail (support (G := G) (u := v_1) nil)))),
  (cons h nil).edges = List.zipWith (fun (x1 x2 : V) ↦ s(x1, x2)) (cons h nil).support (cons h nil).support.tail
Tactic: cases p'
Cleared hypotheses: w, p', ih
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Basic (goal)
Goal:
V : Type u
G : SimpleGraph V
u v u_1 v_1 w : V
h : G.Adj u_1 v_1
p' : G.Walk v_1 w
ih : p'.edges = List.zipWith (fun (x1 x2 : V) ↦ s(x1, x2)) p'.support p'.support.tail
cons :
  ∀
    (ih :
      Eq.{u + 1} (α := List (Sym2 V)) (edges (G := G) (u := v_1) nil)
        (List.zipWith (fun (x1 x2 : V) ↦ s(x1, x2)) (support (G := G) (u := v_1) nil)
          (List.tail (support (G := G) (u := v_1) nil)))),
    (Walk.cons h nil).edges =
      List.zipWith (fun (x1 x2 : V) ↦ s(x1, x2)) (Walk.cons h nil).support (Walk.cons h nil).support.tail
⊢ (Walk.cons h p').edges =
    List.zipWith (fun (x1 x2 : V) ↦ s(x1, x2)) (Walk.cons h p').support (Walk.cons h p').support.tail
have cons₁ : ∀ {v : V} (h_1 : G.Adj v_1 v) (p : G.Walk v w)
  (ih :
    (Walk.cons h_1 p).edges =
      List.zipWith (fun (x1 x2 : V) ↦ s(x1, x2)) (Walk.cons h_1 p).support (Walk.cons h_1 p).support.tail),
  (Walk.cons h (Walk.cons h_1 p)).edges =
    List.zipWith (fun (x1 x2 : V) ↦ s(x1, x2)) (Walk.cons h (Walk.cons h_1 p)).support
      (Walk.cons h (Walk.cons h_1 p)).support.tail
Tactic: cases p'
Cleared hypotheses: p', ih
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Basic (goal)
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
⊢ p.edges = List.zipWith (fun (x1 x2 : V) ↦ s(x1, x2)) p.support p.support.tail
have nil : ∀ {u : V},
  Eq.{u + 1} (α := List (Sym2 V)) (edges (G := G) (u := u) nil)
    (List.zipWith (fun (x1 x2 : V) ↦ s(x1, x2)) (support (G := G) (u := u) nil)
      (List.tail (support (G := G) (u := u) nil)))
Tactic: induction p with
  | nil => simp
  | cons _ p' ih => cases p' <;> simp [edges_cons, ih]
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Basic (goal)
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
nil :
  ∀ {u : V},
    Eq.{u + 1} (α := List (Sym2 V)) (edges (G := G) (u := u) Walk.nil)
      (List.zipWith (fun (x1 x2 : V) ↦ s(x1, x2)) (support (G := G) (u := u) Walk.nil)
        (List.tail (support (G := G) (u := u) Walk.nil)))
⊢ p.edges = List.zipWith (fun (x1 x2 : V) ↦ s(x1, x2)) p.support p.support.tail
have cons : ∀ {u v w : V} (h : G.Adj u v) (p' : G.Walk v w)
  (ih : p'.edges = List.zipWith (fun (x1 x2 : V) ↦ s(x1, x2)) p'.support p'.support.tail),
  (cons h p').edges = List.zipWith (fun (x1 x2 : V) ↦ s(x1, x2)) (cons h p').support (cons h p').support.tail
Tactic: induction p with
  | nil => simp
  | cons _ p' ih => cases p' <;> simp [edges_cons, ih]
Cleared hypotheses: p