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
motive : (u v : V) → G.Walk u v → Sort u_1
Hnil : {u : V} → motive u u nil
Hconcat : {u v w : V} → (p : G.Walk u v) → (h : G.Adj v w) → motive u v p → motive u w (p.concat h)
u v w : V
p : G.Walk u v
h : G.Adj v w
⊢ concatRecAux (motive := motive) (@Hnil) (@Hconcat) (p.concat h).reverse ≍
    concatRecAux (motive := motive) (@Hnil) (@Hconcat) (cons ⋯ p.reverse)
have e_8 : (p.concat h).reverse = cons sorry p.reverse
Tactic: congr
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Operations (goal)
Goal:
V : Type u
G : SimpleGraph V
motive : (u v : V) → G.Walk u v → Sort u_1
Hnil : {u : V} → motive u u nil
Hconcat : {u v w : V} → (p : G.Walk u v) → (h : G.Adj v w) → motive u v p → motive u w (p.concat h)
u v w : V
p : G.Walk u v
h : G.Adj v w
⊢ concatRecAux (motive := motive) (@Hnil) (@Hconcat) (cons ⋯ p.reverse) ≍
    Hconcat p h
      (Eq.rec (motive := fun (x : G.Walk u v) (h : p.reverse.reverse = x) ↦ motive u v x)
        (concatRecAux (motive := fun (x x_1 : V) (x_2 : G.Walk x x_1) ↦ motive x x_1 x_2) (@Hnil) (@Hconcat) p.reverse)
        ⋯)
have rw : Hconcat p.reverse.reverse sorry (concatRecAux (motive := motive) (@Hnil) (@Hconcat) p.reverse) ≍
  Hconcat p h
    (Eq.rec (motive := fun (x : G.Walk u v) (h : p.reverse.reverse = x) ↦ motive u v x)
      (concatRecAux (motive := fun (x x_1 : V) (x_2 : G.Walk x x_1) ↦ motive x x_1 x_2) (@Hnil) (@Hconcat) p.reverse) sorry)
Tactic: rw [concatRecAux, eqRec_heq_iff_heq]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Operations (goal)
Goal:
V : Type u
G : SimpleGraph V
motive : (u v : V) → G.Walk u v → Sort u_1
Hnil : {u : V} → motive u u nil
Hconcat : {u v w : V} → (p : G.Walk u v) → (h : G.Adj v w) → motive u v p → motive u w (p.concat h)
u v w : V
p : G.Walk u v
h : G.Adj v w
⊢ Hconcat p.reverse.reverse ⋯ (concatRecAux (motive := motive) (@Hnil) (@Hconcat) p.reverse) ≍
    Hconcat p h
      (Eq.rec (motive := fun (x : G.Walk u v) (h : p.reverse.reverse = x) ↦ motive u v x)
        (concatRecAux (motive := fun (x x_1 : V) (x_2 : G.Walk x x_1) ↦ motive x x_1 x_2) (@Hnil) (@Hconcat) p.reverse)
        ⋯)
have e_4 : p.reverse.reverse = p
Tactic: congr
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Operations (goal)
Goal:
V : Type u
G : SimpleGraph V
motive : (u v : V) → G.Walk u v → Sort u_1
Hnil : {u : V} → motive u u nil
Hconcat : {u v w : V} → (p : G.Walk u v) → (h : G.Adj v w) → motive u v p → motive u w (p.concat h)
u v w : V
p : G.Walk u v
h : G.Adj v w
e_4 : p.reverse.reverse = p
⊢ Hconcat p.reverse.reverse ⋯ (concatRecAux (motive := motive) (@Hnil) (@Hconcat) p.reverse) ≍
    Hconcat p h
      (Eq.rec (motive := fun (x : G.Walk u v) (h : p.reverse.reverse = x) ↦ motive u v x)
        (concatRecAux (motive := fun (x x_1 : V) (x_2 : G.Walk x x_1) ↦ motive x x_1 x_2) (@Hnil) (@Hconcat) p.reverse)
        ⋯)
have e_6 : HEq (concatRecAux (motive := motive) (@Hnil) (@Hconcat) p.reverse) (β := motive u v p)
  (Eq.rec (motive := fun (x : G.Walk u v) (h : p.reverse.reverse = x) ↦ motive u v x)
      (concatRecAux (motive := fun (x x_1 : V) (x_2 : G.Walk x x_1) ↦ motive x x_1 x_2) (@Hnil) (@Hconcat) p.reverse)
      sorry :
    motive u v p)
Tactic: congr
-- 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 : G.Adj v u
⊢ p.concat h ≠ nil
have nil : ∀ (h : G.Adj u u), concat nil h ≠ nil
Tactic: cases p
Cleared hypotheses: v, 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 : G.Adj v u
nil : ∀ (h : G.Adj u u), concat Walk.nil h ≠ Walk.nil
⊢ p.concat h ≠ Walk.nil
have cons : ∀ {v_1 : V} (h_1 : G.Adj u v_1) (p : G.Walk v_1 v), (cons h_1 p).concat h ≠ Walk.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 v v' w : V
h' : G.Adj v' w
u_1 : V
h : G.Adj u_1 w
p' : G.Walk u_1 v'
he : concat nil h = p'.concat h'
⊢ ∃ (hv : u_1 = v'), Walk.copy nil ⋯ hv = p'
have nil : ∀ {h : G.Adj v' w} (he : concat nil h = concat nil h'),
  ∃ (hv : v' = v'), Eq (α := G.Walk v' v') (Walk.copy nil sorry hv) nil
Tactic: cases p'
Cleared hypotheses: u_1, h, p', he
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Operations (goal)
Goal:
V : Type u
G : SimpleGraph V
u v v' w : V
h' : G.Adj v' w
u_1 : V
h : G.Adj u_1 w
p' : G.Walk u_1 v'
he : concat Walk.nil h = p'.concat h'
nil :
  ∀ {h : G.Adj v' w} (he : concat Walk.nil h = concat Walk.nil h'),
    ∃ (hv : v' = v'), Eq (α := G.Walk v' v') (Walk.copy Walk.nil ⋯ hv) Walk.nil
⊢ ∃ (hv : u_1 = v'), Walk.copy Walk.nil ⋯ hv = p'
have nil₁ : ∀ {v : V} (h_1 : G.Adj u_1 v) (p : G.Walk v v') (he : concat Walk.nil h = (cons h_1 p).concat h'),
  ∃ (hv : u_1 = v'), Walk.copy Walk.nil sorry hv = cons h_1 p
Tactic: cases p'
Cleared hypotheses: p', he
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Operations (hypothesis)
Goal:
V : Type u
G : SimpleGraph V
u v v' w : V
h' : G.Adj v' w
u_1 : V
h : G.Adj u_1 w
v_1 : V
h_1 : G.Adj u_1 v_1
p : G.Walk v_1 v'
he : concat nil h = (cons h_1 p).concat h'
⊢ ∃ (hv : u_1 = v'), Walk.copy nil ⋯ hv = cons h_1 p
have he₁ : w = v_1 ∧ HEq (α := G.Walk w w) nil (p.concat h')
Tactic: simp only [concat_nil, concat_cons, cons.injEq] at he
Cleared hypotheses: he
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Operations (goal)
Goal:
V : Type u
G : SimpleGraph V
u v v' w : V
h' : G.Adj v' w
u_1 : V
h : G.Adj u_1 w
v_1 : V
h_1 : G.Adj u_1 v_1
p : G.Walk v_1 v'
he : w = v_1 ∧ HEq (α := G.Walk w w) nil (p.concat h')
⊢ ∃ (hv : u_1 = v'), Walk.copy nil ⋯ hv = cons h_1 p
have nil : ∀ (h : G.Adj u_1 w) (p : G.Walk w v') (he : HEq (α := G.Walk w w) nil (p.concat h')),
  ∃ (hv : u_1 = v'), Walk.copy nil sorry hv = cons h p
Tactic: obtain ⟨rfl, he⟩ := he
Cleared hypotheses: v_1, h_1, p, he
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Operations (hypothesis)
Goal:
V : Type u
G : SimpleGraph V
u v v' w : V
h' : G.Adj v' w
u_1 v_1 w_1 : V
h_1 : G.Adj u_1 v_1
p : G.Walk v_1 w_1
ih : ∀ {h : G.Adj w_1 w} {p' : G.Walk v_1 v'} (he : p.concat h = p'.concat h'), ∃ (hv : w_1 = v'), p.copy ⋯ hv = p'
h : G.Adj w_1 w
p' : G.Walk u_1 v'
he : (cons h_1 p).concat h = p'.concat h'
⊢ ∃ (hv : w_1 = v'), (cons h_1 p).copy ⋯ hv = p'
have he₁ : cons h_1 (p.concat h) = p'.concat h'
Tactic: rw [concat_cons] at he
Cleared hypotheses: he
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Operations (goal)
Goal:
V : Type u
G : SimpleGraph V
u v v' w : V
h' : G.Adj v' w
u_1 v_1 w_1 : V
h_1 : G.Adj u_1 v_1
p : G.Walk v_1 w_1
ih : ∀ {h : G.Adj w_1 w} {p' : G.Walk v_1 v'} (he : p.concat h = p'.concat h'), ∃ (hv : w_1 = v'), p.copy ⋯ hv = p'
h : G.Adj w_1 w
p' : G.Walk u_1 v'
he : cons h_1 (p.concat h) = p'.concat h'
⊢ ∃ (hv : w_1 = v'), (cons h_1 p).copy ⋯ hv = p'
have cons : ∀ (h_2 : G.Adj v' v_1) (he : cons h_2 (p.concat h) = concat nil h'), ∃ (hv : w_1 = v'), (cons h_2 p).copy sorry hv = nil
Tactic: cases p'
Cleared hypotheses: u_1, h_1, p', he
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Operations (goal)
Goal:
V : Type u
G : SimpleGraph V
u v v' w : V
h' : G.Adj v' w
u_1 v_1 w_1 : V
h_1 : G.Adj u_1 v_1
p : G.Walk v_1 w_1
ih : ∀ {h : G.Adj w_1 w} {p' : G.Walk v_1 v'} (he : p.concat h = p'.concat h'), ∃ (hv : w_1 = v'), p.copy ⋯ hv = p'
h : G.Adj w_1 w
p' : G.Walk u_1 v'
he : Walk.cons h_1 (p.concat h) = p'.concat h'
cons :
  ∀ (h_2 : G.Adj v' v_1) (he : Walk.cons h_2 (p.concat h) = concat nil h'),
    ∃ (hv : w_1 = v'), (Walk.cons h_2 p).copy ⋯ hv = nil
⊢ ∃ (hv : w_1 = v'), (Walk.cons h_1 p).copy ⋯ hv = p'
have cons₁ : ∀ {v : V} (h_2 : G.Adj u_1 v) (p_1 : G.Walk v v') (he : Walk.cons h_1 (p.concat h) = (Walk.cons h_2 p_1).concat h'),
  ∃ (hv : w_1 = v'), (Walk.cons h_1 p).copy sorry hv = Walk.cons h_2 p_1
Tactic: cases p'
Cleared hypotheses: p', he
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Operations (hypothesis)
Goal:
V : Type u
G : SimpleGraph V
u v v' w : V
h' : G.Adj v' w
v_1 w_1 : V
p : G.Walk v_1 w_1
ih : ∀ {h : G.Adj w_1 w} {p' : G.Walk v_1 v'} (he : p.concat h = p'.concat h'), ∃ (hv : w_1 = v'), p.copy ⋯ hv = p'
h : G.Adj w_1 w
h_1 : G.Adj v' v_1
he : cons h_1 (p.concat h) = concat nil h'
⊢ ∃ (hv : w_1 = v'), (cons h_1 p).copy ⋯ hv = nil
have he₁ : v_1 = w ∧ HEq (p.concat h) (β := G.Walk w w) nil
Tactic: simp only [concat_nil, cons.injEq] at he
Cleared hypotheses: he
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Operations (hypothesis)
Goal:
V : Type u
G : SimpleGraph V
u v v' w : V
h' : G.Adj v' w
v_1 w_1 : V
p : G.Walk v_1 w_1
ih : ∀ {h : G.Adj w_1 w} {p' : G.Walk v_1 v'} (he : p.concat h = p'.concat h'), ∃ (hv : w_1 = v'), p.copy ⋯ hv = p'
h : G.Adj w_1 w
h_1 : G.Adj v' v_1
he : v_1 = w ∧ HEq (p.concat h) (β := G.Walk w w) nil
h'₁ : G.Adj v' v_1
⊢ ∃ (hv : w_1 = v'), (cons h_1 p).copy ⋯ hv = nil
have ih₁ : ∀ {h : G.Adj w_1 v_1} {p' : G.Walk v_1 v'} (he : p.concat h = p'.concat h'₁), ∃ (hv : w_1 = v'), p.copy sorry hv = p'
Tactic: obtain ⟨rfl, he⟩ := he
Cleared hypotheses: w, h', ih, h, he
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Operations (hypothesis)
Goal:
V : Type u
G : SimpleGraph V
u v v' w : V
h' : G.Adj v' w
v_1 w_1 : V
p : G.Walk v_1 w_1
ih : ∀ {h : G.Adj w_1 w} {p' : G.Walk v_1 v'} (he : p.concat h = p'.concat h'), ∃ (hv : w_1 = v'), p.copy ⋯ hv = p'
h : G.Adj w_1 w
h_1 : G.Adj v' v_1
he : v_1 = w ∧ HEq (p.concat h) (β := G.Walk w w) nil
h'₁ : G.Adj v' v_1
ih₁ : ∀ {h : G.Adj w_1 v_1} {p' : G.Walk v_1 v'} (he : p.concat h = p'.concat h'₁), ∃ (hv : w_1 = v'), p.copy ⋯ hv = p'
⊢ ∃ (hv : w_1 = v'), (cons h_1 p).copy ⋯ hv = nil
have h₁ : G.Adj w_1 v_1
Tactic: obtain ⟨rfl, he⟩ := he
Cleared hypotheses: w, h', ih, h, he
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Operations (hypothesis)
Goal:
V : Type u
G : SimpleGraph V
u v v' w : V
h' : G.Adj v' w
v_1 w_1 : V
p : G.Walk v_1 w_1
ih : ∀ {h : G.Adj w_1 w} {p' : G.Walk v_1 v'} (he : p.concat h = p'.concat h'), ∃ (hv : w_1 = v'), p.copy ⋯ hv = p'
h : G.Adj w_1 w
h_1 : G.Adj v' v_1
he : v_1 = w ∧ HEq (p.concat h) (β := G.Walk w w) nil
h'₁ : G.Adj v' v_1
ih₁ : ∀ {h : G.Adj w_1 v_1} {p' : G.Walk v_1 v'} (he : p.concat h = p'.concat h'₁), ∃ (hv : w_1 = v'), p.copy ⋯ hv = p'
h₁ : G.Adj w_1 v_1
⊢ ∃ (hv : w_1 = v'), (cons h_1 p).copy ⋯ hv = nil
have he₁ : HEq (p.concat h₁) (β := G.Walk v_1 v_1) nil
Tactic: obtain ⟨rfl, he⟩ := he
Cleared hypotheses: w, h', ih, h, he
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Operations (hypothesis)
Goal:
V : Type u
G : SimpleGraph V
u v v' w : V
h' : G.Adj v' w
u_1 v_1 w_1 : V
h_1 : G.Adj u_1 v_1
p : G.Walk v_1 w_1
ih : ∀ {h : G.Adj w_1 w} {p' : G.Walk v_1 v'} (he : p.concat h = p'.concat h'), ∃ (hv : w_1 = v'), p.copy ⋯ hv = p'
h : G.Adj w_1 w
v_2 : V
h_2 : G.Adj u_1 v_2
p_1 : G.Walk v_2 v'
he : cons h_1 (p.concat h) = (cons h_2 p_1).concat h'
⊢ ∃ (hv : w_1 = v'), (cons h_1 p).copy ⋯ hv = cons h_2 p_1
have he₁ : v_1 = v_2 ∧ p.concat h ≍ p_1.concat h'
Tactic: rw [concat_cons, cons.injEq] at he
Cleared hypotheses: he
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Operations (goal)
Goal:
V : Type u
G : SimpleGraph V
u v v' w : V
h' : G.Adj v' w
u_1 v_1 w_1 : V
h_1 : G.Adj u_1 v_1
p : G.Walk v_1 w_1
ih : ∀ {h : G.Adj w_1 w} {p' : G.Walk v_1 v'} (he : p.concat h = p'.concat h'), ∃ (hv : w_1 = v'), p.copy ⋯ hv = p'
h : G.Adj w_1 w
v_2 : V
h_2 : G.Adj u_1 v_2
p_1 : G.Walk v_2 v'
he : v_1 = v_2 ∧ p.concat h ≍ p_1.concat h'
⊢ ∃ (hv : w_1 = v'), (cons h_1 p).copy ⋯ hv = cons h_2 p_1
have cons : ∀ (h_3 : G.Adj u_1 v_1) (p_2 : G.Walk v_1 v') (he : p.concat h ≍ p_2.concat h'),
  ∃ (hv : w_1 = v'), (cons h_1 p).copy sorry hv = cons h_3 p_2
Tactic: obtain ⟨rfl, he⟩ := he
Cleared hypotheses: v_2, h_2, p_1, he
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Operations (goal)
Goal:
V : Type u
G : SimpleGraph V
u v v' w : V
h' : G.Adj v' w
u_1 v_1 w_1 : V
h_1 : G.Adj u_1 v_1
p : G.Walk v_1 w_1
ih : ∀ {h : G.Adj w_1 w} {p' : G.Walk v_1 v'} (he : p.concat h = p'.concat h'), ∃ (hv : w_1 = v'), p.copy ⋯ hv = p'
h : G.Adj w_1 w
h_2 : G.Adj u_1 v_1
p_1 : G.Walk v_1 v'
he : p.concat h ≍ p_1.concat h'
⊢ ∃ (hv : w_1 = v'), (cons h_1 p).copy ⋯ hv = cons h_2 p_1
have cons : ∀ {h' : G.Adj w_1 w}
  (ih :
    ∀ {h : G.Adj w_1 w} {p' : G.Walk v_1 w_1} (he : p.concat h = p'.concat h'), ∃ (hv : w_1 = w_1), p.copy sorry hv = p')
  (he : p.concat h ≍ (p.copy sorry sorry).concat h'), ∃ (hv : w_1 = w_1), (cons h_1 p).copy sorry hv = cons h_2 (p.copy sorry sorry)
Tactic: obtain ⟨rfl, rfl⟩ := ih (heq_iff_eq.mp he)
Cleared hypotheses: v', h', ih, p_1, he
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Operations (goal)
Goal:
V : Type u
G : SimpleGraph V
u v v' w : V
p : G.Walk u v
h : G.Adj v w
p' : G.Walk u v'
h' : G.Adj v' w
he : p.concat h = p'.concat h'
⊢ ∃ (hv : v = v'), p.copy ⋯ hv = p'
have nil : ∀ {u : V} {h : G.Adj u w} {p' : G.Walk u v'} (he : concat nil h = p'.concat h'),
  ∃ (hv : u = v'), Walk.copy nil sorry hv = p'
Tactic: induction p with
  | nil =>
    cases p'
    · exact ⟨rfl, rfl⟩
    · simp only [concat_nil, concat_cons, cons.injEq] at he
      obtain ⟨rfl, he⟩ := he
      exact (concat_ne_nil _ _ (heq_iff_eq.mp he).symm).elim
  | cons _ _ ih =>
    rw [concat_cons] at he
    cases p'
    · simp only [concat_nil, cons.injEq] at he
      obtain ⟨rfl, he⟩ := he
      exact (concat_ne_nil _ _ (heq_iff_eq.mp he)).elim
    · rw [concat_cons, cons.injEq] at he
      obtain ⟨rfl, he⟩ := he
      obtain ⟨rfl, rfl⟩ := ih (heq_iff_eq.mp he)
      exact ⟨rfl, rfl⟩
Cleared hypotheses: p, h, p', he
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Operations (goal)
Goal:
V : Type u
G : SimpleGraph V
u v v' w : V
p : G.Walk u v
h : G.Adj v w
p' : G.Walk u v'
h' : G.Adj v' w
he : p.concat h = p'.concat h'
nil :
  ∀ {u : V} {h : G.Adj u w} {p' : G.Walk u v'} (he : concat Walk.nil h = p'.concat h'),
    ∃ (hv : u = v'), Walk.copy Walk.nil ⋯ hv = p'
⊢ ∃ (hv : v = v'), p.copy ⋯ hv = p'
have cons : ∀ {u v w_1 : V} (h : G.Adj u v) (p : G.Walk v w_1)
  (ih : ∀ {h : G.Adj w_1 w} {p' : G.Walk v v'} (he : p.concat h = p'.concat h'), ∃ (hv : w_1 = v'), p.copy sorry hv = p')
  {h_1 : G.Adj w_1 w} {p' : G.Walk u v'} (he : (cons h p).concat h_1 = p'.concat h'),
  ∃ (hv : w_1 = v'), (cons h p).copy sorry hv = p'
Tactic: induction p with
  | nil =>
    cases p'
    · exact ⟨rfl, rfl⟩
    · simp only [concat_nil, concat_cons, cons.injEq] at he
      obtain ⟨rfl, he⟩ := he
      exact (concat_ne_nil _ _ (heq_iff_eq.mp he).symm).elim
  | cons _ _ ih =>
    rw [concat_cons] at he
    cases p'
    · simp only [concat_nil, cons.injEq] at he
      obtain ⟨rfl, he⟩ := he
      exact (concat_ne_nil _ _ (heq_iff_eq.mp he)).elim
    · rw [concat_cons, cons.injEq] at he
      obtain ⟨rfl, he⟩ := he
      obtain ⟨rfl, rfl⟩ := ih (heq_iff_eq.mp he)
      exact ⟨rfl, rfl⟩
Cleared hypotheses: p, h, p', he
-- 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).support = p.support ++ [w]
have nil : ∀ {u : V} (h : G.Adj u w), (concat nil h).support = support (G := G) (u := u) nil ++ [w]
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).support = support (G := G) (u := u) Walk.nil ++ [w]
⊢ (p.concat h).support = p.support ++ [w]
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).support = p.support ++ [w]) →
    ∀ (h_1 : G.Adj w_1 w), ((cons h p).concat h_1).support = (cons h p).support ++ [w]
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).support = p.support
have subst_vars : ∀ (p : G.Walk u' v'), (p.copy sorry sorry).support = p.support
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').support = p.support ++ p'.support.tail
have nil : ∀ {u : V} (p' : G.Walk u w), (append nil p').support = support (G := G) (u := u) nil ++ p'.support.tail
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').support = support (G := G) (u := u) Walk.nil ++ p'.support.tail
⊢ (p.append p').support = p.support ++ p'.support.tail
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').support = p.support ++ p'.support.tail) →
    ∀ (p' : G.Walk w_1 w), ((cons h p).append p').support = (cons h p).support ++ p'.support.tail
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 u_1 : V
p' : G.Walk u_1 w
⊢ (append nil p').support = support (G := G) (u := u_1) nil ++ p'.support.tail
have nil : support (G := G) (u := w) (append nil nil) =
  HAppend.hAppend (α := List V) (support (G := G) (u := w) nil) (List.tail (support (G := G) (u := w) nil))
Tactic: cases p'
Cleared hypotheses: u_1, p'
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Operations (goal)
Goal:
V : Type u
G : SimpleGraph V
u v w u_1 : V
p' : G.Walk u_1 w
nil :
  support (G := G) (u := w) (append Walk.nil Walk.nil) =
    HAppend.hAppend (α := List V) (support (G := G) (u := w) Walk.nil) (List.tail (support (G := G) (u := w) Walk.nil))
⊢ (append Walk.nil p').support = support (G := G) (u := u_1) Walk.nil ++ p'.support.tail
have nil₁ : ∀ {v : V} (h : G.Adj u_1 v) (p : G.Walk v w),
  (append Walk.nil (cons h p)).support = support (G := G) (u := u_1) Walk.nil ++ (cons h p).support.tail
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 w u_1 v_1 w_1 : V
h : G.Adj u_1 v_1
p : G.Walk v_1 w_1
p_ih : ∀ (p' : G.Walk w_1 w), (p.append p').support = p.support ++ p'.support.tail
p' : G.Walk w_1 w
⊢ ((cons h p).append p').support = (cons h p).support ++ p'.support.tail
have cons : ∀ (p : G.Walk v_1 w),
  (∀ (p' : G.Walk w w), (p.append p').support = p.support ++ p'.support.tail) →
    ((cons h p).append nil).support = (cons h p).support ++ List.tail (support (G := G) (u := w) nil)
Tactic: cases p'
Cleared hypotheses: w_1, p, p_ih, p'
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Operations (goal)
Goal:
V : Type u
G : SimpleGraph V
u v w u_1 v_1 w_1 : V
h : G.Adj u_1 v_1
p : G.Walk v_1 w_1
p_ih : ∀ (p' : G.Walk w_1 w), (p.append p').support = p.support ++ p'.support.tail
p' : G.Walk w_1 w
cons :
  ∀ (p : G.Walk v_1 w),
    (∀ (p' : G.Walk w w), (p.append p').support = p.support ++ p'.support.tail) →
      ((Walk.cons h p).append nil).support = (Walk.cons h p).support ++ List.tail (support (G := G) (u := w) nil)
⊢ ((Walk.cons h p).append p').support = (Walk.cons h p).support ++ p'.support.tail
have cons₁ : ∀ {v : V} (h_1 : G.Adj w_1 v) (p_1 : G.Walk v w),
  ((Walk.cons h p).append (Walk.cons h_1 p_1)).support = (Walk.cons h p).support ++ (Walk.cons h_1 p_1).support.tail
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
⊢ p.reverse.support = p.support.reverse
have nil : ∀ {u : V},
  Eq.{u + 1} (α := List V) (support (G := G) (u := u) (reverse nil)) (List.reverse (support (G := G) (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 V) (support (G := G) (u := u) (reverse Walk.nil))
      (List.reverse (support (G := G) (u := u) Walk.nil))
⊢ p.reverse.support = p.support.reverse
have cons : ∀ {u v w : V} (h : G.Adj u v) (p : G.Walk v w),
  p.reverse.support = p.support.reverse → (cons h p).reverse.support = (cons h p).support.reverse
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 w : V
p : G.Walk u v
p' : G.Walk v w
⊢ (p.append p').support = p.support.dropLast ++ p'.support
have nil : ∀ {u : V} (p' : G.Walk u w), (append nil p').support = List.dropLast (support (G := G) (u := u) nil) ++ p'.support
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').support = List.dropLast (support (G := G) (u := u) Walk.nil) ++ p'.support
⊢ (p.append p').support = p.support.dropLast ++ p'.support
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').support = p.support.dropLast ++ p'.support) →
    ∀ (p' : G.Walk w_1 w), ((cons h p).append p').support = (cons h p).support.dropLast ++ p'.support
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
⊢ (p.append p').support.tail = p.support.tail ++ p'.support.tail
have rw : (p.support ++ p'.support.tail).tail = p.support.tail ++ p'.support.tail
Tactic: rw [support_append, List.tail_append_of_ne_nil (support_ne_nil _)]
-- 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).tail = p.support.tail ++ p'.support.tail
⊢ (p.append p').support.tail = p.support.tail ++ p'.support.tail
have rw₁ : p.support.tail ++ p'.support.tail = p.support.tail ++ p'.support.tail
Tactic: rw [support_append, List.tail_append_of_ne_nil (support_ne_nil _)]
-- 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.support.dropLast ++ [v] = p.support
have cons : ∀ {v_1 : V} (h : G.Adj u v_1) (p : G.Walk v_1 v), (cons h p).support.dropLast ++ [v] = (cons h p).support
Tactic: cases p with | nil => rfl | cons h 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_1 : V
h : G.Adj u v_1
p : G.Walk v_1 v
⊢ (cons h p).support.dropLast ++ [v] = (cons h p).support
have cons : ∀ (w : V) (w_1 : G.Walk u w) (w_2 : G.Adj w v) (hp : cons h p = w_1.concat w_2),
  (cons h p).support.dropLast ++ [v] = (cons h p).support
Tactic: have ⟨_, _, _, hp⟩ := p.exists_cons_eq_concat 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 : p.support = q.support
⊢ p = q
have refine : (List.map Dart.toProd p.darts).unzip = (List.map Dart.toProd q.darts).unzip
Tactic: refine darts_injective (Dart.toProd_injective.list_map (List.rightInverse_unzip_zip.injective ?_))
-- 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
⊢ (List.map Dart.toProd p.darts).unzip = (List.map Dart.toProd q.darts).unzip
have this : Eq.{u + 1} (α := G.Dart → V) (Prod.fst ∘ Dart.toProd) fun (d : G.Dart) ↦ d.toProd.1
Tactic: have : Prod.fst ∘ Dart.toProd = fun d : G.Dart ↦ d.fst := rfl