awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Subwalks (goal)
Goal:
V : Type u_1
G : SimpleGraph V
v w v' w' : V
p₁ : G.Walk v w
p₂ : G.Walk v' w'
h_1 : p₁.support <:+: p₂.support
s t : List V
h : s ++ p₁.support ++ t = p₂.support
this : s.length + p₁.length ≤ p₂.length
⊢ p₁.IsSubwalk p₂
have refine_2 : p₂.getVert s.length = v
Tactic: refine ⟨p₂.take s.length |>.copy rfl ?_, p₂.drop (s.length + p₁.length) |>.copy ?_ rfl, ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Subwalks (goal)
Goal:
V : Type u_1
G : SimpleGraph V
v w v' w' : V
p₁ : G.Walk v w
p₂ : G.Walk v' w'
h_1 : p₁.support <:+: p₂.support
s t : List V
h : s ++ p₁.support ++ t = p₂.support
this : s.length + p₁.length ≤ p₂.length
refine_2 : p₂.getVert s.length = v
⊢ p₁.IsSubwalk p₂
have refine_2₁ : p₂.getVert (s.length + p₁.length) = w
Tactic: refine ⟨p₂.take s.length |>.copy rfl ?_, p₂.drop (s.length + p₁.length) |>.copy ?_ rfl, ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Subwalks (goal)
Goal:
V : Type u_1
G : SimpleGraph V
v w v' w' : V
p₁ : G.Walk v w
p₂ : G.Walk v' w'
h_1 : p₁.support <:+: p₂.support
s t : List V
h : s ++ p₁.support ++ t = p₂.support
this : s.length + p₁.length ≤ p₂.length
refine_2 : p₂.getVert s.length = v
refine_2₁ : p₂.getVert (s.length + p₁.length) = w
⊢ p₁.IsSubwalk p₂
have refine_2₂ : p₂ = ((Walk.copy (p₂.take s.length) sorry sorry).append p₁).append (Walk.copy (p₂.drop (s.length + p₁.length)) sorry sorry)
Tactic: refine ⟨p₂.take s.length |>.copy rfl ?_, p₂.drop (s.length + p₁.length) |>.copy ?_ rfl, ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Subwalks (goal)
Goal:
V : Type u_1
G : SimpleGraph V
v w v' w' : V
p₁ : G.Walk v w
p₂ : G.Walk v' w'
h_1 : p₁.support <:+: p₂.support
s t : List V
h : s ++ p₁.support ++ t = p₂.support
this : s.length + p₁.length ≤ p₂.length
⊢ p₂ = ((Walk.copy (p₂.take s.length) ⋯ ⋯).append p₁).append (Walk.copy (p₂.drop (s.length + p₁.length)) ⋯ ⋯)
have refine_2 : p₂.support =
  (((Walk.copy (p₂.take s.length) sorry sorry).append p₁).append (Walk.copy (p₂.drop (s.length + p₁.length)) sorry sorry)).support
Tactic: apply ext_support
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Subwalks (goal)
Goal:
V : Type u_1
G : SimpleGraph V
v w v' w' : V
p₁ : G.Walk v w
p₂ : G.Walk v' w'
h_1 : p₁.support <:+: p₂.support
s t : List V
h : s ++ p₁.support ++ t = p₂.support
this : s.length + p₁.length ≤ p₂.length
⊢ p₂.support =
    (((Walk.copy (p₂.take s.length) ⋯ ⋯).append p₁).append (Walk.copy (p₂.drop (s.length + p₁.length)) ⋯ ⋯)).support
have refine_2 : s ++ p₁.support ++ t =
  List.take (s.length + 1) s ++ List.take (s.length + 1 - s.length) p₁.support ++
        List.take (s.length + 1 - (s ++ p₁.support).length) t ++
      p₁.support.tail ++
    List.drop (min (s.length + p₁.length) p₂.length + 1) (s ++ p₁.support ++ t)
Tactic: simp only [← h, support_append, support_copy, take_support_eq_support_take_succ,
      List.take_append, drop_support_eq_support_drop_min, List.tail_drop]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Subwalks (goal)
Goal:
V : Type u_1
G : SimpleGraph V
v w v' w' : V
p₁ : G.Walk v w
p₂ : G.Walk v' w'
h_1 : p₁.support <:+: p₂.support
s t : List V
h : s ++ p₁.support ++ t = p₂.support
this : s.length + p₁.length ≤ p₂.length
⊢ s ++ p₁.support ++ t =
    List.take (s.length + 1) s ++ List.take (s.length + 1 - s.length) p₁.support ++
          List.take (s.length + 1 - (s ++ p₁.support).length) t ++
        p₁.support.tail ++
      List.drop (min (s.length + p₁.length) p₂.length + 1) (s ++ p₁.support ++ t)
have refine_2 : s ++ v :: p₁.support.tail ++ t =
  List.take (s.length + 1) s ++ List.take (s.length + 1 - s.length) (v :: p₁.support.tail) ++
        List.take (s.length + 1 - (s ++ v :: p₁.support.tail).length) t ++
      (v :: p₁.support.tail).tail ++
    (HAppend.hAppend (α := List V) [] [] ++ List.drop (s.length + p₁.length + 1 - (s ++ v :: p₁.support.tail).length) t)
Tactic: rw [Nat.min_eq_left (by grind), List.drop_append, List.drop_append,
      List.drop_eq_nil_of_le (by lia), List.drop_eq_nil_of_le (by grind), ← p₁.cons_tail_support]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Subwalks (goal)
Goal:
V : Type u_1
G : SimpleGraph V
u v u' v' : V
p₁ : G.Walk u v
p₂ : G.Walk u' v'
hnil : ¬p₁.Nil
⊢ p₁.IsSubwalk p₂ ↔ p₁.darts <:+: p₂.darts
have rw : (∃ (k : ℕ),
    p₁.support.length + k ≤ p₂.support.length ∧
      ∀ (i : ℕ) (h : i < p₁.support.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) p₁.support i h)) ↔
  ∃ (k : ℕ),
    p₁.darts.length + k ≤ p₂.darts.length ∧
      ∀ (i : ℕ) (h : i < p₁.darts.length),
        getElem? (valid := fun (as : List G.Dart) (i : ℕ) ↦ i < as.length) p₂.darts (i + k) =
          some (getElem (valid := fun (as : List G.Dart) (i : ℕ) ↦ i < as.length) p₁.darts i h)
Tactic: rw [isSubwalk_iff_support_isInfix, List.infix_iff_getElem?, List.infix_iff_getElem?]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Subwalks (goal)
Goal:
V : Type u_1
G : SimpleGraph V
u v u' v' : V
p₁ : G.Walk u v
p₂ : G.Walk u' v'
hnil : ¬p₁.Nil
⊢ (∃ (k : ℕ),
      p₁.support.length + k ≤ p₂.support.length ∧
        ∀ (i : ℕ) (h : i < p₁.support.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) p₁.support i h)) ↔
    ∃ (k : ℕ),
      p₁.darts.length + k ≤ p₂.darts.length ∧
        ∀ (i : ℕ) (h : i < p₁.darts.length),
          getElem? (valid := fun (as : List G.Dart) (i : ℕ) ↦ i < as.length) p₂.darts (i + k) =
            some (getElem (valid := fun (as : List G.Dart) (i : ℕ) ↦ i < as.length) p₁.darts i h)
have refine_1 : (∃ (k : ℕ),
    p₁.support.length + k ≤ p₂.support.length ∧
      ∀ (i : ℕ) (h : i < p₁.support.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) p₁.support i h)) →
  ∀ (k : ℕ) (hk : p₁.support.length + k ≤ p₂.support.length)
    (h :
      ∀ (i : ℕ) (h : i < p₁.support.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) p₁.support i h))
    (i : ℕ) (hi : i < p₁.darts.length),
    getElem? (valid := fun (as : List G.Dart) (i : ℕ) ↦ i < as.length) p₂.darts (i + k) =
      some (getElem (valid := fun (as : List G.Dart) (i : ℕ) ↦ i < as.length) p₁.darts i hi)
Tactic: refine ⟨fun ⟨k, hk, h⟩ ↦ ⟨k, by grind, fun i hi ↦ ?_⟩,
    fun ⟨k, hk, h⟩ ↦ ⟨k, by grind, fun i hi ↦ ?_⟩⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Subwalks (goal)
Goal:
V : Type u_1
G : SimpleGraph V
u v u' v' : V
p₁ : G.Walk u v
p₂ : G.Walk u' v'
hnil : ¬p₁.Nil
refine_1 :
  (∃ (k : ℕ),
      p₁.support.length + k ≤ p₂.support.length ∧
        ∀ (i : ℕ) (h : i < p₁.support.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) p₁.support i h)) →
    ∀ (k : ℕ) (hk : p₁.support.length + k ≤ p₂.support.length)
      (h :
        ∀ (i : ℕ) (h : i < p₁.support.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) p₁.support i h))
      (i : ℕ) (hi : i < p₁.darts.length),
      getElem? (valid := fun (as : List G.Dart) (i : ℕ) ↦ i < as.length) p₂.darts (i + k) =
        some (getElem (valid := fun (as : List G.Dart) (i : ℕ) ↦ i < as.length) p₁.darts i hi)
⊢ (∃ (k : ℕ),
      p₁.support.length + k ≤ p₂.support.length ∧
        ∀ (i : ℕ) (h : i < p₁.support.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) p₁.support i h)) ↔
    ∃ (k : ℕ),
      p₁.darts.length + k ≤ p₂.darts.length ∧
        ∀ (i : ℕ) (h : i < p₁.darts.length),
          getElem? (valid := fun (as : List G.Dart) (i : ℕ) ↦ i < as.length) p₂.darts (i + k) =
            some (getElem (valid := fun (as : List G.Dart) (i : ℕ) ↦ i < as.length) p₁.darts i h)
have refine_2 : (∃ (k : ℕ),
    p₁.darts.length + k ≤ p₂.darts.length ∧
      ∀ (i : ℕ) (h : i < p₁.darts.length),
        getElem? (valid := fun (as : List G.Dart) (i : ℕ) ↦ i < as.length) p₂.darts (i + k) =
          some (getElem (valid := fun (as : List G.Dart) (i : ℕ) ↦ i < as.length) p₁.darts i h)) →
  ∀ (k : ℕ) (hk : p₁.darts.length + k ≤ p₂.darts.length)
    (h :
      ∀ (i : ℕ) (h : i < p₁.darts.length),
        getElem? (valid := fun (as : List G.Dart) (i : ℕ) ↦ i < as.length) p₂.darts (i + k) =
          some (getElem (valid := fun (as : List G.Dart) (i : ℕ) ↦ i < as.length) p₁.darts i h))
    (i : ℕ) (hi : i < p₁.support.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) p₁.support i hi)
Tactic: refine ⟨fun ⟨k, hk, h⟩ ↦ ⟨k, by grind, fun i hi ↦ ?_⟩,
    fun ⟨k, hk, h⟩ ↦ ⟨k, by grind, fun i hi ↦ ?_⟩⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Subwalks (goal)
Goal:
V : Type u_1
G : SimpleGraph V
u v u' v' : V
p₁ : G.Walk u v
p₂ : G.Walk u' v'
hnil : ¬p₁.Nil
h_1 :
  ∃ (k : ℕ),
    p₁.support.length + k ≤ p₂.support.length ∧
      ∀ (i : ℕ) (h : i < p₁.support.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) p₁.support i h)
k : ℕ
hk : p₁.support.length + k ≤ p₂.support.length
h :
  ∀ (i : ℕ) (h : i < p₁.support.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) p₁.support i h)
i : ℕ
hi : i < p₁.darts.length
⊢ getElem? (valid := fun (as : List G.Dart) (i : ℕ) ↦ i < as.length) p₂.darts (i + k) =
    some (getElem (valid := fun (as : List G.Dart) (i : ℕ) ↦ i < as.length) p₁.darts i hi)
have refine_1 : getElem (valid := fun (as : List G.Dart) (i : ℕ) ↦ i < as.length) p₂.darts (i + k) sorry =
  getElem (valid := fun (as : List G.Dart) (i : ℕ) ↦ i < as.length) p₁.darts i hi
Tactic: rw [getElem?_pos _ _ <| by grind, Option.some_inj]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Subwalks (goal)
Goal:
V : Type u_1
G : SimpleGraph V
u v u' v' : V
p₁ : G.Walk u v
p₂ : G.Walk u' v'
hnil : ¬p₁.Nil
h_1 :
  ∃ (k : ℕ),
    p₁.support.length + k ≤ p₂.support.length ∧
      ∀ (i : ℕ) (h : i < p₁.support.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) p₁.support i h)
k : ℕ
hk : p₁.support.length + k ≤ p₂.support.length
h :
  ∀ (i : ℕ) (h : i < p₁.support.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) p₁.support i h)
i : ℕ
hi : i < p₁.darts.length
⊢ getElem (valid := fun (as : List G.Dart) (i : ℕ) ↦ i < as.length) p₂.darts (i + k) ⋯ =
    getElem (valid := fun (as : List G.Dart) (i : ℕ) ↦ i < as.length) p₁.darts i hi
have refine_1 : (getElem (valid := fun (as : List G.Dart) (i : ℕ) ↦ i < as.length) p₂.darts (i + k) sorry).toProd.1 =
  (getElem (valid := fun (as : List G.Dart) (i : ℕ) ↦ i < as.length) p₁.darts i hi).toProd.1
Tactic: ext
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Subwalks (goal)
Goal:
V : Type u_1
G : SimpleGraph V
u v u' v' : V
p₁ : G.Walk u v
p₂ : G.Walk u' v'
hnil : ¬p₁.Nil
h_1 :
  ∃ (k : ℕ),
    p₁.support.length + k ≤ p₂.support.length ∧
      ∀ (i : ℕ) (h : i < p₁.support.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) p₁.support i h)
k : ℕ
hk : p₁.support.length + k ≤ p₂.support.length
h :
  ∀ (i : ℕ) (h : i < p₁.support.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) p₁.support i h)
i : ℕ
hi : i < p₁.darts.length
refine_1 :
  (getElem (valid := fun (as : List G.Dart) (i : ℕ) ↦ i < as.length) p₂.darts (i + k) ⋯).toProd.1 =
    (getElem (valid := fun (as : List G.Dart) (i : ℕ) ↦ i < as.length) p₁.darts i hi).toProd.1
⊢ getElem (valid := fun (as : List G.Dart) (i : ℕ) ↦ i < as.length) p₂.darts (i + k) ⋯ =
    getElem (valid := fun (as : List G.Dart) (i : ℕ) ↦ i < as.length) p₁.darts i hi
have refine_1₁ : (getElem (valid := fun (as : List G.Dart) (i : ℕ) ↦ i < as.length) p₂.darts (i + k) sorry).toProd.2 =
  (getElem (valid := fun (as : List G.Dart) (i : ℕ) ↦ i < as.length) p₁.darts i hi).toProd.2
Tactic: ext
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Subwalks (goal)
Goal:
V : Type u_1
G : SimpleGraph V
u v u' v' : V
p₁ : G.Walk u v
p₂ : G.Walk u' v'
hnil : ¬p₁.Nil
h_1 :
  ∃ (k : ℕ),
    p₁.darts.length + k ≤ p₂.darts.length ∧
      ∀ (i : ℕ) (h : i < p₁.darts.length),
        getElem? (valid := fun (as : List G.Dart) (i : ℕ) ↦ i < as.length) p₂.darts (i + k) =
          some (getElem (valid := fun (as : List G.Dart) (i : ℕ) ↦ i < as.length) p₁.darts i h)
k : ℕ
hk : p₁.darts.length + k ≤ p₂.darts.length
h :
  ∀ (i : ℕ) (h : i < p₁.darts.length),
    getElem? (valid := fun (as : List G.Dart) (i : ℕ) ↦ i < as.length) p₂.darts (i + k) =
      some (getElem (valid := fun (as : List G.Dart) (i : ℕ) ↦ i < as.length) p₁.darts i h)
i : ℕ
hi : i < p₁.support.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) p₁.support i hi)
have refine_2 : getElem (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) p₂.support (i + k) sorry =
  getElem (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) p₁.support i hi
Tactic: rw [getElem?_pos _ _ <| by grind, Option.some_inj]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Subwalks (goal)
Goal:
V : Type u_1
G : SimpleGraph V
u v u' v' : V
p₁ : G.Walk u v
p₂ : G.Walk u' v'
hnil : ¬p₁.Nil
h_1 :
  ∃ (k : ℕ),
    p₁.darts.length + k ≤ p₂.darts.length ∧
      ∀ (i : ℕ) (h : i < p₁.darts.length),
        getElem? (valid := fun (as : List G.Dart) (i : ℕ) ↦ i < as.length) p₂.darts (i + k) =
          some (getElem (valid := fun (as : List G.Dart) (i : ℕ) ↦ i < as.length) p₁.darts i h)
k : ℕ
hk : p₁.darts.length + k ≤ p₂.darts.length
h :
  ∀ (i : ℕ) (h : i < p₁.darts.length),
    getElem? (valid := fun (as : List G.Dart) (i : ℕ) ↦ i < as.length) p₂.darts (i + k) =
      some (getElem (valid := fun (as : List G.Dart) (i : ℕ) ↦ i < as.length) p₁.darts i h)
i : ℕ
hi : i < p₁.support.length
⊢ getElem (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) p₂.support (i + k) ⋯ =
    getElem (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) p₁.support i hi
have pos : ∀ (hi' : i = p₁.length),
  getElem (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) p₂.support (i + k) sorry =
    getElem (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) p₁.support i hi
Tactic: by_cases hi' : i = p₁.length
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Subwalks (goal)
Goal:
V : Type u_1
G : SimpleGraph V
u v u' v' : V
p₁ : G.Walk u v
p₂ : G.Walk u' v'
hnil : ¬p₁.Nil
h_1 :
  ∃ (k : ℕ),
    p₁.darts.length + k ≤ p₂.darts.length ∧
      ∀ (i : ℕ) (h : i < p₁.darts.length),
        getElem? (valid := fun (as : List G.Dart) (i : ℕ) ↦ i < as.length) p₂.darts (i + k) =
          some (getElem (valid := fun (as : List G.Dart) (i : ℕ) ↦ i < as.length) p₁.darts i h)
k : ℕ
hk : p₁.darts.length + k ≤ p₂.darts.length
h :
  ∀ (i : ℕ) (h : i < p₁.darts.length),
    getElem? (valid := fun (as : List G.Dart) (i : ℕ) ↦ i < as.length) p₂.darts (i + k) =
      some (getElem (valid := fun (as : List G.Dart) (i : ℕ) ↦ i < as.length) p₁.darts i h)
i : ℕ
hi : i < p₁.support.length
pos :
  ∀ (hi' : i = p₁.length),
    getElem (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) p₂.support (i + k) ⋯ =
      getElem (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) p₁.support i hi
⊢ getElem (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) p₂.support (i + k) ⋯ =
    getElem (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) p₁.support i hi
have neg : ∀ (hi' : ¬i = p₁.length),
  getElem (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) p₂.support (i + k) sorry =
    getElem (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) p₁.support i hi
Tactic: by_cases hi' : i = p₁.length
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Subwalks (hypothesis)
Goal:
V : Type u_1
G : SimpleGraph V
u v u' v' : V
p₁ : G.Walk u v
p₂ : G.Walk u' v'
hnil : ¬p₁.Nil
h_1 :
  ∃ (k : ℕ),
    p₁.darts.length + k ≤ p₂.darts.length ∧
      ∀ (i : ℕ) (h : i < p₁.darts.length),
        getElem? (valid := fun (as : List G.Dart) (i : ℕ) ↦ i < as.length) p₂.darts (i + k) =
          some (getElem (valid := fun (as : List G.Dart) (i : ℕ) ↦ i < as.length) p₁.darts i h)
k : ℕ
hk : p₁.darts.length + k ≤ p₂.darts.length
h :
  ∀ (i : ℕ) (h : i < p₁.darts.length),
    getElem? (valid := fun (as : List G.Dart) (i : ℕ) ↦ i < as.length) p₂.darts (i + k) =
      some (getElem (valid := fun (as : List G.Dart) (i : ℕ) ↦ i < as.length) p₁.darts i h)
i : ℕ
hi : i < p₁.support.length
hi' : i = p₁.length
⊢ getElem (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) p₂.support (i + k) ⋯ =
    getElem (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) p₁.support i hi
have this : ∀ (h : i - 1 < p₁.darts.length),
  getElem? (valid := fun (as : List G.Dart) (i : ℕ) ↦ i < as.length) p₂.darts (i - 1 + k) =
    some (getElem (valid := fun (as : List G.Dart) (i : ℕ) ↦ i < as.length) p₁.darts (i - 1) h)
Tactic: have := h <| i - 1
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Subwalks (hypothesis)
Goal:
V : Type u_1
G : SimpleGraph V
u v u' v' : V
p₁ : G.Walk u v
p₂ : G.Walk u' v'
hnil : ¬p₁.Nil
h_1 :
  ∃ (k : ℕ),
    p₁.darts.length + k ≤ p₂.darts.length ∧
      ∀ (i : ℕ) (h : i < p₁.darts.length),
        getElem? (valid := fun (as : List G.Dart) (i : ℕ) ↦ i < as.length) p₂.darts (i + k) =
          some (getElem (valid := fun (as : List G.Dart) (i : ℕ) ↦ i < as.length) p₁.darts i h)
k : ℕ
hk : p₁.darts.length + k ≤ p₂.darts.length
h :
  ∀ (i : ℕ) (h : i < p₁.darts.length),
    getElem? (valid := fun (as : List G.Dart) (i : ℕ) ↦ i < as.length) p₂.darts (i + k) =
      some (getElem (valid := fun (as : List G.Dart) (i : ℕ) ↦ i < as.length) p₁.darts i h)
i : ℕ
hi : i < p₁.support.length
hi' : ¬i = p₁.length
⊢ getElem (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) p₂.support (i + k) ⋯ =
    getElem (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) p₁.support i hi
have this : ∀ (h : i < p₁.darts.length),
  getElem? (valid := fun (as : List G.Dart) (i : ℕ) ↦ i < as.length) p₂.darts (i + k) =
    some (getElem (valid := fun (as : List G.Dart) (i : ℕ) ↦ i < as.length) p₁.darts i h)
Tactic: have := h i
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Subwalks (goal)
Goal:
V : Type u_1
G : SimpleGraph V
u v u' v' : V
p : G.Walk u v
h : G.Adj u' v'
⊢ h.toWalk.IsSubwalk p ∨ ⋯.toWalk.IsSubwalk p ↔ s(u', v') ∈ p.edges
have rw : { fst := u', snd := v', adj := h : G.Dart } ∈ p.darts ∨ { fst := v', snd := u', adj := sorry : G.Dart } ∈ p.darts ↔
  ∃ a ∈ p.darts, a.edge = s(u', v')
Tactic: rw [isSubwalk_toWalk_iff_mem_darts, isSubwalk_toWalk_iff_mem_darts, edges, List.mem_map]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Subwalks (goal)
Goal:
V : Type u_1
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 ∨ { fst := v', snd := u', adj := ⋯ : G.Dart } ∈ p.darts ↔
    ∃ a ∈ p.darts, a.edge = s(u', v')
have refine : ∀ (h_1 : ∃ a ∈ p.darts, a.edge = s(u', v')),
  { fst := u', snd := v', adj := h : G.Dart } ∈ p.darts ∨ { fst := v', snd := u', adj := sorry : G.Dart } ∈ p.darts
Tactic: refine ⟨fun h ↦ by grind [Dart.edge], fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Subwalks (goal)
Goal:
V : Type u_1
G : SimpleGraph V
u v u' v' : V
p : G.Walk u v
h_1 : G.Adj u' v'
h : ∃ a ∈ p.darts, a.edge = s(u', v')
⊢ { fst := u', snd := v', adj := h_1 : G.Dart } ∈ p.darts ∨ { fst := v', snd := u', adj := ⋯ : G.Dart } ∈ p.darts
have have : ∀ (d : G.Dart) (hd : d ∈ p.darts) (h : d.edge = s(u', v')),
  { fst := u', snd := v', adj := h_1 : G.Dart } ∈ p.darts ∨ { fst := v', snd := u', adj := sorry : G.Dart } ∈ p.darts
Tactic: have ⟨d, hd, h⟩ := h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Subwalks (hypothesis)
Goal:
V : Type u_1
G : SimpleGraph V
u v u' v' : V
p : G.Walk u v
h_1 : G.Adj u' v'
h_2 : ∃ a ∈ p.darts, a.edge = s(u', v')
d : G.Dart
hd : d ∈ p.darts
h : d.edge = s(u', v')
⊢ { fst := u', snd := v', adj := h_1 : G.Dart } ∈ p.darts ∨ { fst := v', snd := u', adj := ⋯ : G.Dart } ∈ p.darts
have h₁ : (d.toProd.1, d.toProd.2) = (u', v') ∨ (d.toProd.1, d.toProd.2) = (u', v').swap
Tactic: rw [Dart.edge, Sym2.eq, Sym2.rel_iff'] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Subwalks (goal)
Goal:
V : Type u_1
G : SimpleGraph V
u v u' v' : V
p : G.Walk u v
h_1 : G.Adj u' v'
h_2 : ∃ a ∈ p.darts, a.edge = s(u', v')
d : G.Dart
hd : d ∈ p.darts
h : (d.toProd.1, d.toProd.2) = (u', v') ∨ (d.toProd.1, d.toProd.2) = (u', v').swap
⊢ { fst := u', snd := v', adj := h_1 : G.Dart } ∈ p.darts ∨ { fst := v', snd := u', adj := ⋯ : G.Dart } ∈ p.darts
have refine_1 : ∀ (h : (d.toProd.1, d.toProd.2) = (u', v')), { fst := u', snd := v', adj := h_1 : G.Dart } ∈ p.darts
Tactic: refine h.imp (fun h ↦ ?_) (fun h ↦ ?_)
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Subwalks (goal)
Goal:
V : Type u_1
G : SimpleGraph V
u v u' v' : V
p : G.Walk u v
h_1 : G.Adj u' v'
h_2 : ∃ a ∈ p.darts, a.edge = s(u', v')
d : G.Dart
hd : d ∈ p.darts
h : (d.toProd.1, d.toProd.2) = (u', v') ∨ (d.toProd.1, d.toProd.2) = (u', v').swap
refine_1 : ∀ (h : (d.toProd.1, d.toProd.2) = (u', v')), { fst := u', snd := v', adj := h_1 : G.Dart } ∈ p.darts
⊢ { fst := u', snd := v', adj := h_1 : G.Dart } ∈ p.darts ∨ { fst := v', snd := u', adj := ⋯ : G.Dart } ∈ p.darts
have refine_2 : ∀ (h : (d.toProd.1, d.toProd.2) = (u', v').swap), { fst := v', snd := u', adj := sorry : G.Dart } ∈ p.darts
Tactic: refine h.imp (fun h ↦ ?_) (fun h ↦ ?_)
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Subwalks (goal)
Goal:
V : Type u_1
G : SimpleGraph V
u v u' v' : V
p : G.Walk u v
h_1 : G.Adj u' v'
h_2 : ∃ a ∈ p.darts, a.edge = s(u', v')
d : G.Dart
hd : d ∈ p.darts
h_3 : (d.toProd.1, d.toProd.2) = (u', v') ∨ (d.toProd.1, d.toProd.2) = (u', v').swap
h : (d.toProd.1, d.toProd.2) = (u', v')
⊢ { fst := u', snd := v', adj := h_1 : G.Dart } ∈ p.darts
have h₁ : (u', v') = d.toProd
Tactic: convert! hd using 2
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Subwalks (goal)
Goal:
V : Type u_1
G : SimpleGraph V
u v u' v' : V
p : G.Walk u v
h_1 : G.Adj u' v'
h_2 : ∃ a ∈ p.darts, a.edge = s(u', v')
d : G.Dart
hd : d ∈ p.darts
h_3 : (d.toProd.1, d.toProd.2) = (u', v') ∨ (d.toProd.1, d.toProd.2) = (u', v').swap
h : (d.toProd.1, d.toProd.2) = (u', v').swap
⊢ { fst := v', snd := u', adj := ⋯ : G.Dart } ∈ p.darts
have h₁ : (v', u') = d.toProd
Tactic: convert! hd using 2
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Subwalks (goal)
Goal:
V : Type u_1
G : SimpleGraph V
u v u' v' : V
p : G.Walk u v
⊢ [u', v'] <:+: p.support ∨ [v', u'] <:+: p.support ↔ s(u', v') ∈ p.edges
have refine_1 : ∀ (h : [u', v'] <:+: p.support ∨ [v', u'] <:+: p.support), s(u', v') ∈ p.edges
Tactic: refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩