awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Basic (hypothesis)
Goal:
V : Type u
G : SimpleGraph V
u_1 v_1 u c v : V
h₁ : G.Adj u v
w₁ : G.Walk v c
v' : V
h₂ : G.Adj u v'
w₂ : G.Walk v' c
h : (cons' u v c h₁ w₁).edges = (cons' u v' c h₂ w₂).edges
⊢ cons' u v c h₁ w₁ = cons' u v' c h₂ w₂
have h₃ : u ≠ v'
Tactic: have h₃ : u ≠ v' := by rintro rfl; exact G.loopless.irrefl _ h₂
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Basic (goal)
Goal:
V : Type u
G : SimpleGraph V
u_1 v_1 u c v : V
h₁ : G.Adj u v
w₁ : G.Walk v c
v' : V
h₂ : G.Adj u v'
w₂ : G.Walk v' c
h : (cons' u v c h₁ w₁).edges = (cons' u v' c h₂ w₂).edges
h₃ : u ≠ v'
⊢ cons' u v c h₁ w₁ = cons' u v' c h₂ w₂
have obtain : ∀ (h₂ : G.Adj u v) (w₂ : G.Walk v c) (h : (cons' u v c h₁ w₁).edges = (cons' u v c h₂ w₂).edges) (h₃ : u ≠ v)
  (h₃ : w₁.edges = w₂.edges), cons' u v c h₁ w₁ = cons' u v c h₂ w₂
Tactic: obtain ⟨rfl, h₃⟩ : v = v' ∧ w₁.edges = w₂.edges := by simpa [h₁, h₃] using h
Cleared hypotheses: v', h₂, w₂, h, h₃
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Basic (goal)
Goal:
V : Type u
G : SimpleGraph V
u_1 v_1 u c v : V
h₁ : G.Adj u v
w₁ : G.Walk v c
h₂ : G.Adj u v
w₂ : G.Walk v c
h : (cons' u v c h₁ w₁).edges = (cons' u v c h₂ w₂).edges
h₃_1 : u ≠ v
h₃ : w₁.edges = w₂.edges
⊢ cons' u v c h₁ w₁ = cons' u v c h₂ w₂
have rw : cons' u v c h₁ w₂ = cons' u v c h₂ w₂
Tactic: rw [edges_injective h₃]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Basic (goal)
Goal:
V : Type u
G : SimpleGraph V
u : V
⊢ Eq.{u + 1} (α := Set (Sym2 V)) (edgeSet (G := G) (u := u) nil) ∅
have h : ∀ (x : Sym2 V),
  Membership.mem (γ := Set (Sym2 V)) (edgeSet (G := G) (u := u) nil) x ↔ Membership.mem (γ := Set (Sym2 V)) ∅ x
Tactic: ext
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Basic (goal)
Goal:
V : Type u
G : SimpleGraph V
u v w : V
h : G.Adj u v
p : G.Walk v w
⊢ (cons h p).edgeSet = insert s(u, v) p.edgeSet
have h₁ : ∀ (x : Sym2 V), x ∈ (cons h p).edgeSet ↔ x ∈ insert s(u, v) p.edgeSet
Tactic: ext
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Basic (goal)
Goal:
V : Type u
G : SimpleGraph V
v w : V
p : G.Walk v w
⊢ p.Nil ↔ p.support = [v]
have nil : Nil.{u} (V := V) (G := G) (v := v) nil ↔ support (G := G) (u := v) nil = [v]
Tactic: cases p
Cleared hypotheses: w, p
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Basic (goal)
Goal:
V : Type u
G : SimpleGraph V
v w : V
p : G.Walk v w
nil : Nil.{u} (V := V) (G := G) (v := v) Walk.nil ↔ support (G := G) (u := v) Walk.nil = [v]
⊢ p.Nil ↔ p.support = [v]
have cons : ∀ {v_1 : V} (h : G.Adj v v_1) (p : G.Walk v_1 w), (cons h p).Nil ↔ (cons h p).support = [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
v w : V
p : G.Walk v w
⊢ p.darts = [] ↔ p.Nil
have nil : Eq.{u + 1} (α := List G.Dart) (darts (u := v) nil) [] ↔ Nil.{u} (V := V) (G := G) (v := v) nil
Tactic: cases p
Cleared hypotheses: w, p
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Basic (goal)
Goal:
V : Type u
G : SimpleGraph V
v w : V
p : G.Walk v w
nil : Eq.{u + 1} (α := List G.Dart) (darts (u := v) Walk.nil) [] ↔ Nil.{u} (V := V) (G := G) (v := v) Walk.nil
⊢ p.darts = [] ↔ p.Nil
have cons : ∀ {v_1 : V} (h : G.Adj v v_1) (p : G.Walk v_1 w), (cons h p).darts = [] ↔ (cons h p).Nil
Tactic: cases p
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Basic (goal)
Goal:
V : Type u
G : SimpleGraph V
v w : V
p : G.Walk v w
⊢ p.edges = [] ↔ p.Nil
have nil : Eq.{u + 1} (α := List (Sym2 V)) (edges (G := G) (u := v) nil) [] ↔ Nil.{u} (V := V) (G := G) (v := v) nil
Tactic: cases p
Cleared hypotheses: w, p
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Basic (goal)
Goal:
V : Type u
G : SimpleGraph V
v w : V
p : G.Walk v w
nil :
  Eq.{u + 1} (α := List (Sym2 V)) (edges (G := G) (u := v) Walk.nil) [] ↔ Nil.{u} (V := V) (G := G) (v := v) Walk.nil
⊢ p.edges = [] ↔ p.Nil
have cons : ∀ {v_1 : V} (h : G.Adj v v_1) (p : G.Walk v_1 w), (cons h p).edges = [] ↔ (cons h p).Nil
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
⊢ p.length = 0 ↔ p.Nil
have nil : length.{u} (V := V) (G := G) (u := u) nil = 0 ↔ Nil.{u} (V := V) (G := G) (v := u) nil
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 : length.{u} (V := V) (G := G) (u := u) Walk.nil = 0 ↔ Nil.{u} (V := V) (G := G) (v := u) Walk.nil
⊢ p.length = 0 ↔ p.Nil
have cons : ∀ {v_1 : V} (h : G.Adj u v_1) (p : G.Walk v_1 v), (cons h p).length = 0 ↔ (cons h p).Nil
Tactic: cases p
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Basic (goal)
Goal:
V : Type u
G : SimpleGraph V
v w : V
p : G.Walk v w
⊢ ¬p.Nil ↔ 0 < p.length
have nil : ¬Nil.{u} (V := V) (G := G) (v := v) nil ↔ 0 < length.{u} (V := V) (G := G) (u := v) nil
Tactic: cases p
Cleared hypotheses: w, p
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Basic (goal)
Goal:
V : Type u
G : SimpleGraph V
v w : V
p : G.Walk v w
nil : ¬Nil.{u} (V := V) (G := G) (v := v) Walk.nil ↔ 0 < length.{u} (V := V) (G := G) (u := v) Walk.nil
⊢ ¬p.Nil ↔ 0 < p.length
have cons : ∀ {v_1 : V} (h : G.Adj v v_1) (p : G.Walk v_1 w), ¬(cons h p).Nil ↔ 0 < (cons h p).length
Tactic: cases p
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Basic (goal)
Goal:
V : Type u
G : SimpleGraph V
v w : V
p : G.Walk v w
⊢ ¬p.Nil ↔ ∃ (u : V) (h : G.Adj v u) (q : G.Walk u w), p = cons h q
have nil : ¬Nil.{u} (V := V) (G := G) (v := v) nil ↔ ∃ (u : V) (h : G.Adj v u) (q : G.Walk u v), nil = cons h q
Tactic: cases p
Cleared hypotheses: w, p
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Basic (goal)
Goal:
V : Type u
G : SimpleGraph V
v w : V
p : G.Walk v w
nil : ¬Nil.{u} (V := V) (G := G) (v := v) Walk.nil ↔ ∃ (u : V) (h : G.Adj v u) (q : G.Walk u v), Walk.nil = cons h q
⊢ ¬p.Nil ↔ ∃ (u : V) (h : G.Adj v u) (q : G.Walk u w), p = cons h q
have cons : ∀ {v_1 : V} (h : G.Adj v v_1) (p : G.Walk v_1 w),
  ¬(cons h p).Nil ↔ ∃ (u : V) (h_1 : G.Adj v u) (q : G.Walk u w), cons h p = cons h_1 q
Tactic: cases p
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Basic (goal)
Goal:
V : Type u
G : SimpleGraph V
v : V
p : G.Walk v v
⊢ p = nil ↔ p.Nil
have nil : Eq.{u + 1} (α := G.Walk v v) nil nil ↔ Nil.{u} (V := V) (G := G) (v := v) nil
Tactic: cases p
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Basic (goal)
Goal:
V : Type u
G : SimpleGraph V
v : V
p : G.Walk v v
nil : Eq.{u + 1} (α := G.Walk v v) Walk.nil Walk.nil ↔ Nil.{u} (V := V) (G := G) (v := v) Walk.nil
⊢ p = Walk.nil ↔ p.Nil
have cons : ∀ {v_1 : V} (h : G.Adj v v_1) (p : G.Walk v_1 v), cons h p = Walk.nil ↔ (cons h p).Nil
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 w u_1 v_1 w_1 : V
h : G.Adj u_1 v_1
p : G.Walk v_1 w_1
ih : ∀ (hnil : ¬p.Nil), w ∈ p.support ↔ ∃ e ∈ p.edges, w ∈ e
hnil : ¬(cons h p).Nil
⊢ w ∈ (cons h p).support ↔ ∃ e ∈ (cons h p).edges, w ∈ e
have cons : ∀
  (ih :
    ∀ (hnil : ¬Nil.{u} (V := V) (G := G) (v := v_1) nil),
      Membership.mem (γ := List V) (support (G := G) (u := v_1) nil) w ↔
        ∃ (e : Sym2 V), Membership.mem (γ := List (Sym2 V)) (edges (G := G) (u := v_1) nil) e ∧ w ∈ e)
  (hnil : ¬(cons h nil).Nil), w ∈ (cons h nil).support ↔ ∃ e ∈ (cons h nil).edges, w ∈ e
Tactic: cases p
Cleared hypotheses: w_1, p, ih, hnil
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Basic (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
ih : ∀ (hnil : ¬p.Nil), w ∈ p.support ↔ ∃ e ∈ p.edges, w ∈ e
hnil : ¬(Walk.cons h p).Nil
cons :
  ∀
    (ih :
      ∀ (hnil : ¬Nil.{u} (V := V) (G := G) (v := v_1) nil),
        Membership.mem (γ := List V) (support (G := G) (u := v_1) nil) w ↔
          ∃ (e : Sym2 V), Membership.mem (γ := List (Sym2 V)) (edges (G := G) (u := v_1) nil) e ∧ w ∈ e)
    (hnil : ¬(Walk.cons h nil).Nil), w ∈ (Walk.cons h nil).support ↔ ∃ e ∈ (Walk.cons h nil).edges, w ∈ e
⊢ w ∈ (Walk.cons h p).support ↔ ∃ e ∈ (Walk.cons h p).edges, w ∈ e
have cons₁ : ∀ {v : V} (h_1 : G.Adj v_1 v) (p : G.Walk v w_1)
  (ih : ∀ (hnil : ¬(Walk.cons h_1 p).Nil), w ∈ (Walk.cons h_1 p).support ↔ ∃ e ∈ (Walk.cons h_1 p).edges, w ∈ e)
  (hnil : ¬(Walk.cons h (Walk.cons h_1 p)).Nil),
  w ∈ (Walk.cons h (Walk.cons h_1 p)).support ↔ ∃ e ∈ (Walk.cons h (Walk.cons h_1 p)).edges, w ∈ e
Tactic: cases p
Cleared hypotheses: p, ih, hnil
-- 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
hnil : ¬p.Nil
⊢ w ∈ p.support ↔ ∃ e ∈ p.edges, w ∈ e
have nil : ∀ {u : V} (hnil : ¬Nil.{u} (V := V) (G := G) (v := u) nil),
  Membership.mem (γ := List V) (support (G := G) (u := u) nil) w ↔
    ∃ (e : Sym2 V), Membership.mem (γ := List (Sym2 V)) (edges (G := G) (u := u) nil) e ∧ w ∈ e
Tactic: induction p with
  | nil => simp at hnil
  | cons h p ih => cases p <;> aesop
Cleared hypotheses: p, hnil
-- 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
hnil : ¬p.Nil
nil :
  ∀ {u : V} (hnil : ¬Nil.{u} (V := V) (G := G) (v := u) Walk.nil),
    Membership.mem (γ := List V) (support (G := G) (u := u) Walk.nil) w ↔
      ∃ (e : Sym2 V), Membership.mem (γ := List (Sym2 V)) (edges (G := G) (u := u) Walk.nil) e ∧ w ∈ e
⊢ w ∈ p.support ↔ ∃ e ∈ p.edges, w ∈ e
have cons : ∀ {u v w_1 : V} (h : G.Adj u v) (p : G.Walk v w_1) (ih : ∀ (hnil : ¬p.Nil), w ∈ p.support ↔ ∃ e ∈ p.edges, w ∈ e)
  (hnil : ¬(cons h p).Nil), w ∈ (cons h p).support ↔ ∃ e ∈ (cons h p).edges, w ∈ e
Tactic: induction p with
  | nil => simp at hnil
  | cons h p ih => cases p <;> aesop
Cleared hypotheses: p, hnil
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Basic (goal)
Goal:
V : Type u
G : SimpleGraph V
u v : V
S : Set V
u_1 x w : V
a : G.Adj u_1 x
p' : G.Walk x w
ih : ∀ (uS : x ∈ S) (vS : w ∉ S), ∃ d ∈ p'.darts, d.toProd.1 ∈ S ∧ d.toProd.2 ∉ S
uS : u_1 ∈ S
vS : w ∉ S
⊢ ∃ d ∈ (cons a p').darts, d.toProd.1 ∈ S ∧ d.toProd.2 ∉ S
have pos : ∀ (h : x ∈ S), ∃ d ∈ (cons a p').darts, d.toProd.1 ∈ S ∧ d.toProd.2 ∉ S
Tactic: by_cases h : x ∈ S
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Basic (goal)
Goal:
V : Type u
G : SimpleGraph V
u v : V
S : Set V
u_1 x w : V
a : G.Adj u_1 x
p' : G.Walk x w
ih : ∀ (uS : x ∈ S) (vS : w ∉ S), ∃ d ∈ p'.darts, d.toProd.1 ∈ S ∧ d.toProd.2 ∉ S
uS : u_1 ∈ S
vS : w ∉ S
pos : ∀ (h : x ∈ S), ∃ d ∈ (cons a p').darts, d.toProd.1 ∈ S ∧ d.toProd.2 ∉ S
⊢ ∃ d ∈ (cons a p').darts, d.toProd.1 ∈ S ∧ d.toProd.2 ∉ S
have neg : ∀ (h : x ∉ S), ∃ d ∈ (cons a p').darts, d.toProd.1 ∈ S ∧ d.toProd.2 ∉ S
Tactic: by_cases h : x ∈ S
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Basic (goal)
Goal:
V : Type u
G : SimpleGraph V
u v : V
S : Set V
u_1 x w : V
a : G.Adj u_1 x
p' : G.Walk x w
ih : ∀ (uS : x ∈ S) (vS : w ∉ S), ∃ d ∈ p'.darts, d.toProd.1 ∈ S ∧ d.toProd.2 ∉ S
uS : u_1 ∈ S
vS : w ∉ S
h : x ∈ S
⊢ ∃ d ∈ (cons a p').darts, d.toProd.1 ∈ S ∧ d.toProd.2 ∉ S
have pos : ∀ (d : G.Dart) (hd : d ∈ p'.darts) (hcd : d.toProd.1 ∈ S ∧ d.toProd.2 ∉ S),
  ∃ d ∈ (cons a p').darts, d.toProd.1 ∈ S ∧ d.toProd.2 ∉ S
Tactic: obtain ⟨d, hd, hcd⟩ := ih h vS
-- 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
S : Set V
uS : u ∈ S
vS : v ∉ S
⊢ ∃ d ∈ p.darts, d.toProd.1 ∈ S ∧ d.toProd.2 ∉ S
have nil : ∀ {u : V} (uS : u ∈ S) (vS : u ∉ S),
  ∃ (d : G.Dart), Membership.mem (γ := List G.Dart) (darts (u := u) nil) d ∧ d.toProd.1 ∈ S ∧ d.toProd.2 ∉ S
Tactic: induction p with
  | nil => cases vS uS
  | cons a p' ih =>
    rename_i x _
    by_cases h : x ∈ S
    · obtain ⟨d, hd, hcd⟩ := ih h vS
      exact ⟨d, List.Mem.tail _ hd, hcd⟩
    · exact ⟨⟨_, a⟩, List.Mem.head _, uS, h⟩
Cleared hypotheses: p, uS, vS
-- 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
S : Set V
uS : u ∈ S
vS : v ∉ S
nil :
  ∀ {u : V} (uS : u ∈ S) (vS : u ∉ S),
    ∃ (d : G.Dart), Membership.mem (γ := List G.Dart) (darts (u := u) Walk.nil) d ∧ d.toProd.1 ∈ S ∧ d.toProd.2 ∉ S
⊢ ∃ d ∈ p.darts, d.toProd.1 ∈ S ∧ d.toProd.2 ∉ S
have cons : ∀ {u v w : V} (a : G.Adj u v) (p' : G.Walk v w)
  (ih : ∀ (uS : v ∈ S) (vS : w ∉ S), ∃ d ∈ p'.darts, d.toProd.1 ∈ S ∧ d.toProd.2 ∉ S) (uS : u ∈ S) (vS : w ∉ S),
  ∃ d ∈ (cons a p').darts, d.toProd.1 ∈ S ∧ d.toProd.2 ∉ S
Tactic: induction p with
  | nil => cases vS uS
  | cons a p' ih =>
    rename_i x _
    by_cases h : x ∈ S
    · obtain ⟨d, hd, hcd⟩ := ih h vS
      exact ⟨d, List.Mem.tail _ hd, hcd⟩
    · exact ⟨⟨_, a⟩, List.Mem.head _, uS, h⟩
Cleared hypotheses: p, uS, vS
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Chord (goal)
Goal:
V : Type u_1
G : SimpleGraph V
u v : V
p : G.Walk u v
⊢ p.IsChordless ↔ ∀ ⦃u' v' : V⦄, u' ∈ p.support → v' ∈ p.support → G.Adj u' v' → s(u', v') ∈ p.edges
have simp : (∀ (x y : V), G.Adj x y → s(x, y) ∉ p.edges → x ∈ p.support → y ∉ p.support) ↔
  ∀ ⦃u' v' : V⦄, u' ∈ p.support → v' ∈ p.support → G.Adj u' v' → s(u', v') ∈ p.edges
Tactic: simp [IsChordless, Sym2.forall, isChord_sym2Mk]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Counting (goal)
Goal:
V : Type u
G : SimpleGraph V
u v : V
n : ℕ
⊢ Eq.{u + 1} (α := Set (G.Walk u v)) {p : G.Walk u v | p.length = n + 1}
    (⋃ (w : V), ⋃ (h : G.Adj u w), cons h '' {p' : G.Walk w v | p'.length = n})
have h : ∀ (p : G.Walk u v),
  Membership.mem (γ := Set (G.Walk u v)) {p : G.Walk u v | p.length = n + 1} p ↔
    Membership.mem (γ := Set (G.Walk u v)) (⋃ (w : V), ⋃ (h : G.Adj u w), cons h '' {p' : G.Walk w v | p'.length = n}) p
Tactic: ext p
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Counting (goal)
Goal:
V : Type u
G : SimpleGraph V
u v : V
n : ℕ
p : G.Walk u v
⊢ Membership.mem (γ := Set (G.Walk u v)) {p : G.Walk u v | p.length = n + 1} p ↔
    Membership.mem (γ := Set (G.Walk u v)) (⋃ (w : V), ⋃ (h : G.Adj u w), cons h '' {p' : G.Walk w v | p'.length = n}) p
have h : Membership.mem (γ := Set (G.Walk u u)) {p : G.Walk u u | p.length = n + 1} nil ↔
  Membership.mem (γ := Set (G.Walk u u)) (⋃ (w : V), ⋃ (h : G.Adj u w), cons h '' {p' : G.Walk w u | p'.length = n}) nil
Tactic: cases p with
  | nil => simp [eq_comm]
  | cons huw pwv => grind [length_cons, Set.mem_iUnion]
Cleared hypotheses: v, p
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Counting (goal)
Goal:
V : Type u
G : SimpleGraph V
u v : V
n : ℕ
p : G.Walk u v
h :
  Membership.mem (γ := Set (G.Walk u u)) {p : G.Walk u u | p.length = n + 1} nil ↔
    Membership.mem (γ := Set (G.Walk u u)) (⋃ (w : V), ⋃ (h : G.Adj u w), cons h '' {p' : G.Walk w u | p'.length = n})
      nil
⊢ Membership.mem (γ := Set (G.Walk u v)) {p : G.Walk u v | p.length = n + 1} p ↔
    Membership.mem (γ := Set (G.Walk u v)) (⋃ (w : V), ⋃ (h : G.Adj u w), cons h '' {p' : G.Walk w v | p'.length = n}) p
have h₁ : ∀ {v_1 : V} (huw : G.Adj u v_1) (pwv : G.Walk v_1 v),
  Membership.mem (γ := Set (G.Walk u v)) {p : G.Walk u v | p.length = n + 1} (cons huw pwv) ↔
    Membership.mem (γ := Set (G.Walk u v)) (⋃ (w : V), ⋃ (h : G.Adj u w), cons h '' {p' : G.Walk w v | p'.length = n})
      (cons huw pwv)
Tactic: cases p with
  | nil => simp [eq_comm]
  | cons huw pwv => grind [length_cons, Set.mem_iUnion]
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Counting (goal)
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
inst_1 : G.LocallyFinite
n : ℕ
u v : V
h : u = v
⊢ Finset (G.Walk u v)
have subst : Finset (G.Walk v v)
Tactic: subst u
Cleared hypotheses: u, h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Counting (goal)
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
inst_1 : G.LocallyFinite
n : ℕ
ih : ∀ (u v : V), (↑(G.finsetWalkLength n u v) : Set (G.Walk u v)) = {p : G.Walk u v | p.length = n}
u v : V
⊢ (↑(G.finsetWalkLength (n + 1) u v) : Set (G.Walk u v)) = {p : G.Walk u v | p.length = n + 1}
have succ : Eq.{u + 1} (α := Set (G.Walk u v))
  (⋃ (i : V),
    ⋃ (x : i ∈ G.neighborSet u),
      (fun (a : G.Walk i v) ↦
          ({ toFun := fun (p : G.Walk i v) ↦ Walk.cons sorry p, inj' := sorry } : (a : G.Walk i v) → G.Walk u v) a) ''
        (↑(G.finsetWalkLength n i v) : Set (G.Walk i v)))
  (⋃ (w : V), ⋃ (h : G.Adj u w), Walk.cons h '' {p' : G.Walk w v | p'.length = n})
Tactic: simp only [finsetWalkLength, Walk.setOf_length_eq_add_one, Finset.coe_biUnion, Finset.mem_coe,
      Finset.mem_univ, Set.iUnion_true, Finset.coe_map, Set.iUnion_coe_set]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Counting (goal)
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
inst_1 : G.LocallyFinite
n : ℕ
ih : ∀ (u v : V), (↑(G.finsetWalkLength n u v) : Set (G.Walk u v)) = {p : G.Walk u v | p.length = n}
u v : V
⊢ Eq.{u + 1} (α := Set (G.Walk u v))
    (⋃ (i : V),
      ⋃ (x : i ∈ G.neighborSet u),
        (fun (a : G.Walk i v) ↦
            ({ toFun := fun (p : G.Walk i v) ↦ Walk.cons ⋯ p, inj' := ⋯ } : (a : G.Walk i v) → G.Walk u v) a) ''
          (↑(G.finsetWalkLength n i v) : Set (G.Walk i v)))
    (⋃ (w : V), ⋃ (h : G.Adj u w), Walk.cons h '' {p' : G.Walk w v | p'.length = n})
have succ : ∀ (x : V),
  (∀ {α : Type u} {p q : Prop} {f₁ : p → Set α} {f₂ : q → Set α} (pq : p ↔ q) (f : ∀ (x : q), f₁ sorry = f₂ x),
      Set.iUnion f₁ = Set.iUnion f₂) →
    ∀ (x_1 : G.Adj u x), (↑(G.finsetWalkLength n x v) : Set (G.Walk x v)) = {p' : G.Walk x v | p'.length = n}
Tactic: congr!
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Counting (goal)
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
inst_1 : G.LocallyFinite
n : ℕ
u v : V
⊢ (↑(G.finsetWalkLength n u v) : Set (G.Walk u v)) = {p : G.Walk u v | p.length = n}
have zero : ∀ (u v : V), (↑(G.finsetWalkLength 0 u v) : Set (G.Walk u v)) = {p : G.Walk u v | p.length = 0}
Tactic: induction n generalizing u v with
  | zero => grind [finsetWalkLength, Walk.length_eq_zero_iff, Walk.eq_nil_iff_nil, Walk.Nil.eq]
  | succ n ih =>
    simp only [finsetWalkLength, Walk.setOf_length_eq_add_one, Finset.coe_biUnion, Finset.mem_coe,
      Finset.mem_univ, Set.iUnion_true, Finset.coe_map, Set.iUnion_coe_set]
    congr!
    grind
Cleared hypotheses: n, u, v
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Counting (goal)
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
inst_1 : G.LocallyFinite
n : ℕ
u v : V
zero : ∀ (u v : V), (↑(G.finsetWalkLength 0 u v) : Set (G.Walk u v)) = {p : G.Walk u v | p.length = 0}
⊢ (↑(G.finsetWalkLength n u v) : Set (G.Walk u v)) = {p : G.Walk u v | p.length = n}
have succ : ∀ (n : ℕ) (ih : ∀ (u v : V), (↑(G.finsetWalkLength n u v) : Set (G.Walk u v)) = {p : G.Walk u v | p.length = n})
  (u v : V), (↑(G.finsetWalkLength (n + 1) u v) : Set (G.Walk u v)) = {p : G.Walk u v | p.length = n + 1}
Tactic: induction n generalizing u v with
  | zero => grind [finsetWalkLength, Walk.length_eq_zero_iff, Walk.eq_nil_iff_nil, Walk.Nil.eq]
  | succ n ih =>
    simp only [finsetWalkLength, Walk.setOf_length_eq_add_one, Finset.coe_biUnion, Finset.mem_coe,
      Finset.mem_univ, Set.iUnion_true, Finset.coe_map, Set.iUnion_coe_set]
    congr!
    grind
Cleared hypotheses: n, u, v
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Counting (goal)
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
inst_1 : G.LocallyFinite
n : ℕ
u v : V
⊢ (↑(G.finsetWalkLengthLT n u v) : Set (G.Walk u v)) = {p : G.Walk u v | p.length < n}
have h : ∀ (p : G.Walk u v),
  p ∈ (↑(G.finsetWalkLengthLT n u v) : Set (G.Walk u v)) ↔
    Membership.mem (γ := Set (G.Walk u v)) {p : G.Walk u v | p.length < n} p
Tactic: ext p
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Counting (goal)
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
inst_1 : G.LocallyFinite
u v : V
n : ℕ
p : G.Walk u v
⊢ p ∈ G.finsetWalkLength n u v ↔ Membership.mem (γ := Set (G.Walk u v)) {p : G.Walk u v | p.length = n} p
have rw : p ∈ (↑(G.finsetWalkLength n u v) : Set (G.Walk u v)) ↔
  Membership.mem (γ := Set (G.Walk u v)) {p : G.Walk u v | p.length = n} p
Tactic: rw [← Finset.mem_coe, coe_finsetWalkLength_eq]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Counting (goal)
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
inst_1 : G.LocallyFinite
u v : V
n : ℕ
p : G.Walk u v
rw :
  p ∈ (↑(G.finsetWalkLength n u v) : Set (G.Walk u v)) ↔
    Membership.mem (γ := Set (G.Walk u v)) {p : G.Walk u v | p.length = n} p
⊢ p ∈ G.finsetWalkLength n u v ↔ Membership.mem (γ := Set (G.Walk u v)) {p : G.Walk u v | p.length = n} p
have rw₁ : Membership.mem (γ := Set (G.Walk u v)) {p : G.Walk u v | p.length = n} p ↔
  Membership.mem (γ := Set (G.Walk u v)) {p : G.Walk u v | p.length = n} p
Tactic: rw [← Finset.mem_coe, coe_finsetWalkLength_eq]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Counting (goal)
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
inst_1 : G.LocallyFinite
u v : V
n : ℕ
p : G.Walk u v
⊢ p ∈ G.finsetWalkLengthLT n u v ↔ Membership.mem (γ := Set (G.Walk u v)) {p : G.Walk u v | p.length < n} p
have rw : p ∈ (↑(G.finsetWalkLengthLT n u v) : Set (G.Walk u v)) ↔
  Membership.mem (γ := Set (G.Walk u v)) {p : G.Walk u v | p.length < n} p
Tactic: rw [← Finset.mem_coe, coe_finsetWalkLengthLT_eq]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Counting (goal)
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
inst_1 : G.LocallyFinite
u v : V
n : ℕ
p : G.Walk u v
rw :
  p ∈ (↑(G.finsetWalkLengthLT n u v) : Set (G.Walk u v)) ↔
    Membership.mem (γ := Set (G.Walk u v)) {p : G.Walk u v | p.length < n} p
⊢ p ∈ G.finsetWalkLengthLT n u v ↔ Membership.mem (γ := Set (G.Walk u v)) {p : G.Walk u v | p.length < n} p
have rw₁ : Membership.mem (γ := Set (G.Walk u v)) {p : G.Walk u v | p.length < n} p ↔
  Membership.mem (γ := Set (G.Walk u v)) {p : G.Walk u v | p.length < n} p
Tactic: rw [← Finset.mem_coe, coe_finsetWalkLengthLT_eq]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Decomp (goal)
Goal:
V : Type u
G : SimpleGraph V
v_1 w_1 u_1 : V
inst : DecidableEq V
v w u : V
h : Membership.mem (γ := List V) (support (G := G) (u := v) nil) u
⊢ G.Walk v u
have rw : G.Walk v v
Tactic: rw [mem_support_nil_iff.mp h]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Decomp (goal)
Goal:
V : Type u
G : SimpleGraph V
v_1 w_1 u_1 : V
inst : DecidableEq V
v w_2 w v_2 : V
r : G.Adj v v_2
p : G.Walk v_2 w
u : V
h : u ∈ (cons r p).support
hx : ¬v = u
⊢ u ∈ p.support
have head : ∀ (hx : ¬v = v), v ∈ p.support
Tactic: cases h
Cleared hypotheses: u, h, hx
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Decomp (goal)
Goal:
V : Type u
G : SimpleGraph V
v_1 w_1 u_1 : V
inst : DecidableEq V
v w_2 w v_2 : V
r : G.Adj v v_2
p : G.Walk v_2 w
u : V
h : u ∈ (cons r p).support
hx : ¬v = u
head : ∀ (hx : ¬v = v), v ∈ p.support
⊢ u ∈ p.support
have tail : List.Mem u p.support → u ∈ p.support
Tactic: cases h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Decomp (goal)
Goal:
V : Type u
G : SimpleGraph V
v u : V
inst : DecidableEq V
p : G.Walk u v
⊢ p.takeUntil u ⋯ = nil
have nil : Eq (α := G.Walk v v) (takeUntil nil v sorry) nil
Tactic: cases p
Cleared hypotheses: u, p
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Decomp (goal)
Goal:
V : Type u
G : SimpleGraph V
v u : V
inst : DecidableEq V
p : G.Walk u v
nil : Eq (α := G.Walk v v) (takeUntil Walk.nil v ⋯) Walk.nil
⊢ p.takeUntil u ⋯ = Walk.nil
have cons : ∀ {v_1 : V} (h : G.Adj u v_1) (p : G.Walk v_1 v), (cons h p).takeUntil u sorry = Walk.nil
Tactic: cases p
Cleared hypotheses: p