awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
hadj : G.Adj u_1 v_1
p : G.Walk v_1 w
hind : ∀ (hp : G.Adj p.penultimate w), p.dropLast.concat hp = p
hp : G.Adj (Walk.cons hadj p).penultimate w
cons :
  ∀ (hind : ∀ (hp : G.Adj (penultimate (G := G) (u := v_1) nil) v_1), concat (dropLast nil) hp = nil)
    (hp : G.Adj (Walk.cons hadj nil).penultimate v_1), (Walk.cons hadj nil).dropLast.concat hp = Walk.cons hadj nil
⊢ (Walk.cons hadj p).dropLast.concat hp = Walk.cons hadj p
have cons₁ : ∀ {v : V} (h : G.Adj v_1 v) (p : G.Walk v w)
  (hind : ∀ (hp : G.Adj (Walk.cons h p).penultimate w), (Walk.cons h p).dropLast.concat hp = Walk.cons h p)
  (hp : G.Adj (Walk.cons hadj (Walk.cons h p)).penultimate w),
  (Walk.cons hadj (Walk.cons h p)).dropLast.concat hp = Walk.cons hadj (Walk.cons h p)
Tactic: cases p with
    | nil => rfl
    | _ => simp [hind]
Cleared hypotheses: p, hind, hp
-- 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
hp : G.Adj p.penultimate v
⊢ p.dropLast.concat hp = p
have nil : ∀ {u : V} (hp : G.Adj (penultimate (G := G) (u := u) nil) u), concat (dropLast nil) hp = nil
Tactic: induction p with
  | nil => simp at hp
  | cons hadj p hind =>
    cases p with
    | nil => rfl
    | _ => simp [hind]
Cleared hypotheses: p, hp
-- 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
hp : G.Adj p.penultimate v
nil : ∀ {u : V} (hp : G.Adj (penultimate (G := G) (u := u) Walk.nil) u), concat (dropLast Walk.nil) hp = Walk.nil
⊢ p.dropLast.concat hp = p
have cons : ∀ {u v w : V} (hadj : G.Adj u v) (p : G.Walk v w) (hind : ∀ (hp : G.Adj p.penultimate w), p.dropLast.concat hp = p)
  (hp : G.Adj (cons hadj p).penultimate w), (cons hadj p).dropLast.concat hp = cons hadj p
Tactic: induction p with
  | nil => simp at hp
  | cons hadj p hind =>
    cases p with
    | nil => rfl
    | _ => simp [hind]
Cleared hypotheses: p, hp
-- 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
hp : ¬p.Nil
⊢ u :: p.tail.support = p.support
have rw : (cons sorry p.tail).support = p.support
Tactic: rw [← support_cons (p.adj_snd hp), cons_tail_eq _ hp]
-- 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
hp : ¬p.Nil
rw : (cons ⋯ p.tail).support = p.support
⊢ u :: p.tail.support = p.support
have rw₁ : p.support = p.support
Tactic: rw [← support_cons (p.adj_snd hp), cons_tail_eq _ hp]
-- 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
hp : ¬p.Nil
⊢ p.dropLast.support ++ [v] = p.support
have rw : (p.dropLast.concat sorry).support = p.support
Tactic: rw [← support_concat _ <| adj_penultimate hp, concat_dropLast]
-- 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
hp : ¬p.Nil
rw : (p.dropLast.concat ⋯).support = p.support
⊢ p.dropLast.support ++ [v] = p.support
have rw₁ : p.support = p.support
Tactic: rw [← support_concat _ <| adj_penultimate hp, concat_dropLast]
-- 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
hp : ¬p.Nil
⊢ p.tail.length + 1 = p.length
have rw : (cons sorry p.tail).length = p.length
Tactic: rw [← length_cons (p.adj_snd hp), cons_tail_eq _ hp]
-- 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
hp : ¬p.Nil
rw : (cons ⋯ p.tail).length = p.length
⊢ p.tail.length + 1 = p.length
have rw₁ : p.length = p.length
Tactic: rw [← length_cons (p.adj_snd hp), cons_tail_eq _ hp]
-- 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
hp : ¬p.Nil
⊢ p.dropLast.length + 1 = p.length
have rw : (p.dropLast.concat sorry).length = p.length
Tactic: rw [← length_concat _ <| p.adj_penultimate hp, concat_dropLast]
-- 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
hp : ¬p.Nil
rw : (p.dropLast.concat ⋯).length = p.length
⊢ p.dropLast.length + 1 = p.length
have rw₁ : p.length = p.length
Tactic: rw [← length_concat _ <| p.adj_penultimate hp, concat_dropLast]
-- 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.dropLast.length = p.length - 1
have nil : length.{u} (V := V) (G := G) (u := u) (v := penultimate (G := G) (u := u) nil) (dropLast nil) =
  length.{u} (V := V) (G := G) (u := u) nil - 1
Tactic: cases p
Cleared hypotheses: v, 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 :
  length.{u} (V := V) (G := G) (u := u) (v := penultimate (G := G) (u := u) Walk.nil) (dropLast Walk.nil) =
    length.{u} (V := V) (G := G) (u := u) Walk.nil - 1
⊢ p.dropLast.length = p.length - 1
have cons : ∀ {v_1 : V} (h : G.Adj u v_1) (p : G.Walk v_1 v), (cons h p).dropLast.length = (cons h p).length - 1
Tactic: cases p
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Operations (goal)
Goal:
V : Type u
G : SimpleGraph V
v w : V
p : G.Walk v w
hp : p.Nil
⊢ p.tail.Nil
have nil : ∀ (hp : Nil.{u} (V := V) (G := G) (v := v) Walk.nil),
  Nil.{u} (V := V) (G := G) (v := snd (G := G) (u := v) Walk.nil) (tail Walk.nil)
Tactic: cases p
Cleared hypotheses: w, p, hp
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Operations (goal)
Goal:
V : Type u
G : SimpleGraph V
v w : V
p : G.Walk v w
hp : p.Nil
nil :
  ∀ (hp : Nil.{u} (V := V) (G := G) (v := v) Walk.nil),
    Nil.{u} (V := V) (G := G) (v := snd (G := G) (u := v) Walk.nil) (tail Walk.nil)
⊢ p.tail.Nil
have cons : ∀ {v_1 : V} (h : G.Adj v v_1) (p : G.Walk v_1 w) (hp : (cons h p).Nil), (cons h p).tail.Nil
Tactic: cases p
Cleared hypotheses: p, hp
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Operations (goal)
Goal:
V : Type u
G : SimpleGraph V
v w : V
p : G.Walk v w
hp : p.Nil
⊢ p.dropLast.Nil
have nil : ∀ (hp : Nil.{u} (V := V) (G := G) (v := v) Walk.nil),
  Nil.{u} (V := V) (G := G) (v := v) (w := penultimate (G := G) (u := v) Walk.nil) (dropLast Walk.nil)
Tactic: cases p
Cleared hypotheses: w, p, hp
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Operations (goal)
Goal:
V : Type u
G : SimpleGraph V
v w : V
p : G.Walk v w
hp : p.Nil
nil :
  ∀ (hp : Nil.{u} (V := V) (G := G) (v := v) Walk.nil),
    Nil.{u} (V := V) (G := G) (v := v) (w := penultimate (G := G) (u := v) Walk.nil) (dropLast Walk.nil)
⊢ p.dropLast.Nil
have cons : ∀ {v_1 : V} (h : G.Adj v v_1) (p : G.Walk v_1 w) (hp : (cons h p).Nil), (cons h p).dropLast.Nil
Tactic: cases p
Cleared hypotheses: p, hp
-- 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).Nil = p.Nil
have subst_vars : ∀ {p : G.Walk u' v'}, (p.copy sorry sorry).Nil = p.Nil
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 : V
p : G.Walk u v
hp : ¬p.Nil
⊢ p.tail.support = p.support.tail
have rw : p.tail.support = (u :: p.tail.support).tail
Tactic: rw [← cons_support_tail hp, List.tail_cons]
-- 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
hp : ¬p.Nil
rw : p.tail.support = (u :: p.tail.support).tail
⊢ p.tail.support = p.support.tail
have rw₁ : p.tail.support = p.tail.support
Tactic: rw [← cons_support_tail hp, List.tail_cons]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Operations (goal)
Goal:
V : Type u
G : SimpleGraph V
u v w x : V
p : G.Walk u v
i : ℕ
h : u = w
h' : v = x
⊢ (p.copy h h').getVert i = p.getVert i
have subst_vars : ∀ (p : G.Walk w x), (p.copy sorry sorry).getVert i = p.getVert i
Tactic: subst_vars
Cleared hypotheses: u, v, p, h, h'
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Operations (goal)
Goal:
V : Type u
G : SimpleGraph V
u v : V
n : ℕ
p : G.Walk u v
⊢ p.tail.getVert n = p.getVert (n + 1)
have nil : Eq.{u + 1} (α := V) (getVert (G := G) (u := snd (G := G) (u := u) nil) (tail nil) n)
  (getVert (G := G) (u := u) nil (n + 1))
Tactic: cases p
Cleared hypotheses: v, p
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Operations (goal)
Goal:
V : Type u
G : SimpleGraph V
u v : V
n : ℕ
p : G.Walk u v
nil :
  Eq.{u + 1} (α := V) (getVert (G := G) (u := snd (G := G) (u := u) Walk.nil) (tail Walk.nil) n)
    (getVert (G := G) (u := u) Walk.nil (n + 1))
⊢ p.tail.getVert n = p.getVert (n + 1)
have cons : ∀ {v_1 : V} (h : G.Adj u v_1) (p : G.Walk v_1 v), (cons h p).tail.getVert n = (cons h p).getVert (n + 1)
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 v : V
p : G.Walk u v
hp : ¬p.Nil
i : ℕ
h : i + 1 ≠ 0
⊢ p.getVert (i + 1) ∈ p.support.tail
have rw : p.tail.getVert i ∈ p.tail.support
Tactic: rw [← getVert_tail, ← p.support_tail_of_not_nil hp]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Operations (goal)
Goal:
V : Type u
G : SimpleGraph V
u v : V
p q : G.Walk u v
hl : p.length = q.length
h : ∀ k ≤ p.length, p.getVert k = q.getVert k
⊢ p = q
have suffices : ∀ (k : ℕ),
  getElem? (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) p.support k =
    getElem? (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) q.support k
Tactic: suffices ∀ k : ℕ, p.support[k]? = q.support[k]? by
    exact ext_support <| List.ext_getElem?_iff.mpr this
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Operations (goal)
Goal:
V : Type u
G : SimpleGraph V
u v : V
p q : G.Walk u v
hl : p.length = q.length
h : ∀ k ≤ p.length, p.getVert k = q.getVert k
k : ℕ
hk : k ≤ p.length
⊢ getElem? (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) p.support k =
    getElem? (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) q.support k
have inl : some (p.getVert k) = some (q.getVert k)
Tactic: rw [← getVert_eq_support_getElem? p hk, ← getVert_eq_support_getElem? q (hl ▸ hk)]
-- 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
hl : p.length = q.length
h : ∀ k ≤ p.length, p.getVert k = q.getVert k
k : ℕ
hk : p.length < k
⊢ getElem? (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) p.support k =
    getElem? (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) q.support k
have hk₁ : p.length + 1 ≤ k
Tactic: replace hk : p.length + 1 ≤ k := hk
Cleared hypotheses: hk
-- 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
hl : p.length = q.length
h : ∀ k ≤ p.length, p.getVert k = q.getVert k
k : ℕ
hk : p.length + 1 ≤ k
⊢ getElem? (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) p.support k =
    getElem? (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) q.support k
have ht : q.length + 1 ≤ k
Tactic: have ht : q.length + 1 ≤ k := hl ▸ hk
-- 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
hl : p.length = q.length
h : ∀ k ≤ p.length, p.getVert k = q.getVert k
k : ℕ
hk : p.length + 1 ≤ k
ht : q.length + 1 ≤ k
⊢ getElem? (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) p.support k =
    getElem? (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) q.support k
have hk₁ : getElem? (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) p.support k = none
Tactic: rw [← length_support, ← List.getElem?_eq_none_iff] at hk ht
Cleared hypotheses: hk, ht
-- 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
hl : p.length = q.length
h : ∀ k ≤ p.length, p.getVert k = q.getVert k
k : ℕ
hk : p.length + 1 ≤ k
ht : q.length + 1 ≤ k
hk₁ : getElem? (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) p.support k = none
⊢ getElem? (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) p.support k =
    getElem? (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) q.support k
have ht₁ : getElem? (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) q.support k = none
Tactic: rw [← length_support, ← List.getElem?_eq_none_iff] at hk ht
Cleared hypotheses: hk, ht
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Operations (goal)
Goal:
V : Type u
G : SimpleGraph V
u v : V
p q : G.Walk u v
hl : p.length = q.length
h : ∀ k ≤ p.length, p.getVert k = q.getVert k
k : ℕ
hk : getElem? (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) p.support k = none
ht : getElem? (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) q.support k = none
⊢ getElem? (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) p.support k =
    getElem? (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) q.support k
have inr : none = getElem? (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) q.support k
Tactic: rw [hk, ht]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Operations (goal)
Goal:
V : Type u
G : SimpleGraph V
u v : V
p q : G.Walk u v
hl : p.length = q.length
h : ∀ k ≤ p.length, p.getVert k = q.getVert k
k : ℕ
hk : getElem? (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) p.support k = none
ht : getElem? (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) q.support k = none
inr : none = getElem? (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) q.support k
⊢ getElem? (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) p.support k =
    getElem? (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) q.support k
have inr₁ : Eq.{u + 1} (α := Option V) none none
Tactic: rw [hk, ht]
-- 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
hl : p.length = q.length
h : ∀ k ≤ p.length, p.getVert k = q.getVert k
k : ℕ
⊢ getElem? (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) p.support k =
    getElem? (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) q.support k
have x : k ≤ p.length ∨ p.length < k
Tactic: cases le_or_gt k p.length with
  | inl hk =>
    rw [← getVert_eq_support_getElem? p hk, ← getVert_eq_support_getElem? q (hl ▸ hk)]
    exact congrArg some (h k hk)
  | inr hk =>
    replace hk : p.length + 1 ≤ k := hk
    have ht : q.length + 1 ≤ k := hl ▸ hk
    rw [← length_support, ← List.getElem?_eq_none_iff] at hk ht
    rw [hk, ht]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Operations (goal)
Goal:
V : Type u
G : SimpleGraph V
u v : V
p q : G.Walk u v
h : ∀ (k : ℕ), p.getVert k = q.getVert k
⊢ p = q
have inr : ∀ (this : ∀ {p q : G.Walk u v} (h : ∀ (k : ℕ), p.getVert k = q.getVert k) (hpq : p.length ≤ q.length), p = q)
  (hpq : ¬p.length ≤ q.length), p = q
Tactic: wlog hpq : p.length ≤ q.length generalizing p q
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Operations (goal)
Goal:
V : Type u
G : SimpleGraph V
u v : V
p q : G.Walk u v
h : ∀ (k : ℕ), p.getVert k = q.getVert k
inr :
  ∀ (this : ∀ {p q : G.Walk u v} (h : ∀ (k : ℕ), p.getVert k = q.getVert k) (hpq : p.length ≤ q.length), p = q)
    (hpq : ¬p.length ≤ q.length), p = q
⊢ p = q
have wlog : ∀ {p q : G.Walk u v} (h : ∀ (k : ℕ), p.getVert k = q.getVert k) (hpq : p.length ≤ q.length), p = q
Tactic: wlog hpq : p.length ≤ q.length generalizing p q
Cleared hypotheses: p, q, h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Operations (goal)
Goal:
V : Type u
G : SimpleGraph V
u v : V
p q : G.Walk u v
h : ∀ (k : ℕ), p.getVert k = q.getVert k
hpq : p.length ≤ q.length
⊢ p = q
have refine : q.length ≤ p.length
Tactic: refine ext_getVert_le_length (hpq.antisymm ?_) fun k _ ↦ h k
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Operations (goal)
Goal:
V : Type u
G : SimpleGraph V
u v : V
p q : G.Walk u v
h : ∀ (k : ℕ), p.getVert k = q.getVert k
hpq : p.length ≤ q.length
⊢ q.length ≤ p.length
have by_contra! : ∀ (this : p.length < q.length), False
Tactic: by_contra!
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Subwalks (goal)
Goal:
V : Type u_1
G : SimpleGraph V
u v u' v' w : V
p : G.Walk u v
q : G.Walk u' v'
hpq : p.IsSubwalk q
h : G.Adj w u'
⊢ p.IsSubwalk (cons h q)
have obtain : ∀ (r1 : G.Walk u' u) (r2 : G.Walk v v'), p.IsSubwalk (cons h ((r1.append p).append r2))
Tactic: obtain ⟨r1, r2, rfl⟩ := hpq
Cleared hypotheses: q, hpq
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Subwalks (goal)
Goal:
V : Type u_1
G : SimpleGraph V
u v u' v' w : V
p : G.Walk u v
h : G.Adj w u'
r1 : G.Walk u' u
r2 : G.Walk v v'
⊢ p.IsSubwalk (cons h ((r1.append p).append r2))
have h₁ : cons h ((r1.append p).append r2) = ((cons h r1).append p).append r2
Tactic: use r1.cons h, r2
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Subwalks (goal)
Goal:
V : Type u_1
G : SimpleGraph V
u v u' v' w : V
p : G.Walk u v
q : G.Walk u' v'
hpq : p.IsSubwalk q
h : G.Adj v' w
⊢ p.IsSubwalk (q.concat h)
have obtain : ∀ (r₁ : G.Walk u' u) (r₂ : G.Walk v v'), p.IsSubwalk (((r₁.append p).append r₂).concat h)
Tactic: obtain ⟨r₁, r₂, rfl⟩ := hpq
Cleared hypotheses: q, hpq
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Subwalks (goal)
Goal:
V : Type u_1
G : SimpleGraph V
u v u' v' w : V
p : G.Walk u v
h : G.Adj v' w
r₁ : G.Walk u' u
r₂ : G.Walk v v'
⊢ ((r₁.append p).append r₂).concat h = (r₁.append p).append (r₂.concat h)
have rw : ((r₁.append p).append r₂).concat h = ((r₁.append p).append r₂).concat h
Tactic: rw [append_concat]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Subwalks (goal)
Goal:
V : Type u_1
G : SimpleGraph V
u₁ v₁ u₂ v₂ u₃ v₃ : V
p₁ : G.Walk u₁ v₁
p₂ : G.Walk u₂ v₂
p₃ : G.Walk u₃ v₃
h₁ : p₁.IsSubwalk p₂
h₂ : p₂.IsSubwalk p₃
⊢ p₁.IsSubwalk p₃
have obtain : ∀ (q₁ : G.Walk u₂ u₁) (r₁ : G.Walk v₁ v₂) (h₂ : ((q₁.append p₁).append r₁).IsSubwalk p₃), p₁.IsSubwalk p₃
Tactic: obtain ⟨q₁, r₁, rfl⟩ := h₁
Cleared hypotheses: p₂, h₁, h₂
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Subwalks (goal)
Goal:
V : Type u_1
G : SimpleGraph V
u₁ v₁ u₂ v₂ u₃ v₃ : V
p₁ : G.Walk u₁ v₁
p₃ : G.Walk u₃ v₃
q₁ : G.Walk u₂ u₁
r₁ : G.Walk v₁ v₂
h₂ : ((q₁.append p₁).append r₁).IsSubwalk p₃
⊢ p₁.IsSubwalk p₃
have obtain : ∀ (q₂ : G.Walk u₃ u₂) (r₂ : G.Walk v₂ v₃), p₁.IsSubwalk ((q₂.append ((q₁.append p₁).append r₁)).append r₂)
Tactic: obtain ⟨q₂, r₂, rfl⟩ := h₂
Cleared hypotheses: p₃, h₂
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Subwalks (goal)
Goal:
V : Type u_1
G : SimpleGraph V
u₁ v₁ u₂ v₂ u₃ v₃ : V
p₁ : G.Walk u₁ v₁
q₁ : G.Walk u₂ u₁
r₁ : G.Walk v₁ v₂
q₂ : G.Walk u₃ u₂
r₂ : G.Walk v₂ v₃
⊢ p₁.IsSubwalk ((q₂.append ((q₁.append p₁).append r₁)).append r₂)
have h : (q₂.append ((q₁.append p₁).append r₁)).append r₂ = ((q₂.append q₁).append p₁).append (r₁.append r₂)
Tactic: use q₂.append q₁, r₁.append r₂
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Subwalks (goal)
Goal:
V : Type u_1
G : SimpleGraph V
u u' : V
⊢ IsSubwalk.{u_1} (V := V) (G := G) (u₁ := u) (u₂ := u') nil nil ↔
    ∃ (hu : u' = u) (hv : u' = u), Eq (α := G.Walk u u) nil (Walk.copy nil hu hv)
have nil : IsSubwalk.{u_1} (V := V) (G := G) (u₁ := u) (u₂ := u') nil nil →
  ∃ (hu : u' = u) (hv : u' = u), Eq (α := G.Walk u u) nil (Walk.copy nil hu hv)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Subwalks (goal)
Goal:
V : Type u_1
G : SimpleGraph V
u u' : V
nil :
  IsSubwalk.{u_1} (V := V) (G := G) (u₁ := u) (u₂ := u') Walk.nil Walk.nil →
    ∃ (hu : u' = u) (hv : u' = u), Eq (α := G.Walk u u) Walk.nil (Walk.copy Walk.nil hu hv)
⊢ IsSubwalk.{u_1} (V := V) (G := G) (u₁ := u) (u₂ := u') Walk.nil Walk.nil ↔
    ∃ (hu : u' = u) (hv : u' = u), Eq (α := G.Walk u u) Walk.nil (Walk.copy Walk.nil hu hv)
have nil₁ : (∃ (hu : u' = u) (hv : u' = u), Eq (α := G.Walk u u) Walk.nil (Walk.copy Walk.nil hu hv)) →
  IsSubwalk.{u_1} (V := V) (G := G) (u₁ := u) (u₂ := u') Walk.nil Walk.nil
Tactic: constructor
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Subwalks (goal)
Goal:
V : Type u_1
G : SimpleGraph V
u v u' v_1 : V
h : G.Adj u v_1
p : G.Walk v_1 v
⊢ (cons h p).IsSubwalk (u₂ := u') nil ↔ ∃ (hu : u' = u) (hv : u' = v), cons h p = Walk.copy nil hu hv
have cons : (cons h p).IsSubwalk (u₂ := u') nil → ∃ (hu : u' = u) (hv : u' = v), cons h p = Walk.copy nil hu hv
Tactic: constructor
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Subwalks (goal)
Goal:
V : Type u_1
G : SimpleGraph V
u v u' v_1 : V
h : G.Adj u v_1
p : G.Walk v_1 v
cons : (Walk.cons h p).IsSubwalk (u₂ := u') nil → ∃ (hu : u' = u) (hv : u' = v), Walk.cons h p = Walk.copy nil hu hv
⊢ (Walk.cons h p).IsSubwalk (u₂ := u') nil ↔ ∃ (hu : u' = u) (hv : u' = v), Walk.cons h p = Walk.copy nil hu hv
have cons₁ : (∃ (hu : u' = u) (hv : u' = v), Walk.cons h p = Walk.copy nil hu hv) → (Walk.cons h p).IsSubwalk (u₂ := u') nil
Tactic: constructor
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Subwalks (goal)
Goal:
V : Type u_1
G : SimpleGraph V
u v u' : V
p : G.Walk u v
⊢ p.IsSubwalk (u₂ := u') nil ↔ ∃ (hu : u' = u) (hv : u' = v), p = Walk.copy nil hu hv
have nil : IsSubwalk.{u_1} (V := V) (G := G) (u₁ := u) (u₂ := u') nil nil ↔
  ∃ (hu : u' = u) (hv : u' = u), Eq (α := G.Walk u u) nil (Walk.copy nil hu hv)
Tactic: cases p with
  | nil =>
    constructor
    · rintro ⟨_ | _, _, ⟨⟩⟩
      simp
    · rintro ⟨rfl, _, _⟩
      simp
  | cons h p =>
    constructor
    · rintro ⟨_ | _, _, h⟩ <;> simp at h
    · rintro ⟨rfl, rfl, ⟨⟩⟩
Cleared hypotheses: v, p
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Subwalks (goal)
Goal:
V : Type u_1
G : SimpleGraph V
u v u' : V
p : G.Walk u v
nil :
  IsSubwalk.{u_1} (V := V) (G := G) (u₁ := u) (u₂ := u') Walk.nil Walk.nil ↔
    ∃ (hu : u' = u) (hv : u' = u), Eq (α := G.Walk u u) Walk.nil (Walk.copy Walk.nil hu hv)
⊢ p.IsSubwalk (u₂ := u') Walk.nil ↔ ∃ (hu : u' = u) (hv : u' = v), p = Walk.copy Walk.nil hu hv
have cons : ∀ {v_1 : V} (h : G.Adj u v_1) (p : G.Walk v_1 v),
  (cons h p).IsSubwalk (u₂ := u') Walk.nil ↔ ∃ (hu : u' = u) (hv : u' = v), cons h p = Walk.copy Walk.nil hu hv
Tactic: cases p with
  | nil =>
    constructor
    · rintro ⟨_ | _, _, ⟨⟩⟩
      simp
    · rintro ⟨rfl, _, _⟩
      simp
  | cons h p =>
    constructor
    · rintro ⟨_ | _, _, h⟩ <;> simp at h
    · rintro ⟨rfl, rfl, ⟨⟩⟩
Cleared hypotheses: p
-- 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'
⊢ p₁.IsSubwalk p₂ ↔ p₁.support <:+: p₂.support
have refine_1 : p₁.IsSubwalk p₂ →
  ∀ (ru : G.Walk v' v) (rv : G.Walk w w') (h : p₂ = (ru.append p₁).append rv), p₁.support <:+: p₂.support
Tactic: refine ⟨fun ⟨ru, rv, h⟩ ↦ ?_, fun ⟨s, t, h⟩ ↦ ?_⟩
-- 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'
refine_1 :
  p₁.IsSubwalk p₂ →
    ∀ (ru : G.Walk v' v) (rv : G.Walk w w') (h : p₂ = (ru.append p₁).append rv), p₁.support <:+: p₂.support
⊢ p₁.IsSubwalk p₂ ↔ p₁.support <:+: p₂.support
have refine_2 : p₁.support <:+: p₂.support → ∀ (s t : List V) (h : s ++ p₁.support ++ t = p₂.support), p₁.IsSubwalk p₂
Tactic: refine ⟨fun ⟨ru, rv, h⟩ ↦ ?_, fun ⟨s, t, h⟩ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Subwalks (hypothesis)
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
⊢ p₁.IsSubwalk p₂
have this : s.length + p₁.length ≤ p₂.length
Tactic: have : (s.length + p₁.length) ≤ p₂.length := by grind [_=_ length_support]