awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Basic
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
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
⊢ ∃ d ∈ (cons a p').darts, d.toProd.1 ∈ S ∧ d.toProd.2 ∉ S

Tactic:
obtain ⟨d, hd, hcd⟩ := ih h vS
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Basic
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 : 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:
⟨d, List.Mem.tail _ hd, hcd⟩

Premises used: List.Mem.tail, And.intro, Exists.intro
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Basic
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 : 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:
exact ⟨d, List.Mem.tail _ hd, hcd⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Basic
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

Tactic:
⟨⟨_, a⟩, List.Mem.head _, uS, h⟩

Premises used: And.intro, Exists.intro, List.Mem.head, SimpleGraph.Dart.mk
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Basic
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

Tactic:
exact ⟨⟨_, a⟩, List.Mem.head _, uS, h⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Basic
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
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 ∈ (Walk.cons a p').darts, d.toProd.1 ∈ S ∧ d.toProd.2 ∉ S
⊢ ∃ d ∈ 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⟩

Premises used: SimpleGraph.Walk.cons, SimpleGraph.Walk.nil
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Basic
Goal:
V : Type u
G : SimpleGraph V
v : V
⊢ Eq (α := G.Walk ([v].head ⋯) ([v].getLast ⋯)) (ofSupport [v] ⋯ ⋯) nil

Tactic:
rfl

Premises used: List.head, SimpleGraph.Walk.ofSupport, rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Basic
Goal:
V : Type u
G : SimpleGraph V
u v : V
l : List V
hchain : List.IsChain G.Adj (u :: v :: l)
⊢ ofSupport (u :: v :: l) ⋯ hchain = cons ⋯ (ofSupport (v :: l) ⋯ ⋯)

Tactic:
rfl

Premises used: SimpleGraph.Walk.ofSupport, rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Basic
Goal:
V : Type u
G : SimpleGraph V
l : List V
head : V
hne : [head] ≠ []
hchain : List.IsChain G.Adj [head]
⊢ (ofSupport [head] hne hchain).support = [head]

Tactic:
rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Basic
Goal:
V : Type u
G : SimpleGraph V
l_1 : List V
head v : V
l : List V
hne : head :: v :: l ≠ []
hchain : List.IsChain G.Adj (head :: v :: l)
⊢ (ofSupport (head :: v :: l) hne hchain).support = head :: v :: l

Tactic:
simpa using support_ofSupport (l.cons_ne_nil v) hchain.of_cons

Premises used: List.IsChain.of_cons, List.cons_ne_nil
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Basic
Goal:
V : Type u
G : SimpleGraph V
l : List V
hne : l ≠ []
hchain : List.IsChain G.Adj l
⊢ (ofSupport l hne hchain).support = l

Tactic:
match l with
  | [_] => rfl
  | _ :: v :: l =>
    simpa using support_ofSupport (l.cons_ne_nil v) hchain.of_cons
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Basic
Goal:
V : Type u
G : SimpleGraph V
l : List V
hne : l ≠ []
hchain : List.IsChain G.Adj l
⊢ (ofSupport l hne hchain).length = l.length - 1

Tactic:
grind [support_ofSupport]

Premises used: SimpleGraph.Walk.support_ofSupport
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Basic
Goal:
V : Type u
G : SimpleGraph V
d : G.Dart
⊢ ofDarts [d] ⋯ ⋯ = cons ⋯ nil

Tactic:
rfl

Premises used: SimpleGraph.Walk.ofDarts, rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Basic
Goal:
V : Type u
G : SimpleGraph V
d₁ d₂ : G.Dart
l : List G.Dart
hchain : List.IsChain G.DartAdj (d₁ :: d₂ :: l)
⊢ Eq (α := G.Walk ((d₁ :: d₂ :: l).head ⋯).toProd.1 ((d₁ :: d₂ :: l).getLast ⋯).toProd.2)
    (ofDarts (d₁ :: d₂ :: l) ⋯ hchain) (cons ⋯ (ofDarts (d₂ :: l) ⋯ ⋯))

Tactic:
rfl

Premises used: SimpleGraph.Walk.ofDarts, rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Basic
Goal:
V : Type u
G : SimpleGraph V
l : List G.Dart
head : G.Dart
hne : [head] ≠ []
hchain : List.IsChain G.DartAdj [head]
⊢ (ofDarts [head] hne hchain).darts = [head]

Tactic:
rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Basic
Goal:
V : Type u
G : SimpleGraph V
l_1 : List G.Dart
d₁ d₂ : G.Dart
l : List G.Dart
hne : d₁ :: d₂ :: l ≠ []
hchain : List.IsChain G.DartAdj (d₁ :: d₂ :: l)
⊢ (ofDarts (d₁ :: d₂ :: l) hne hchain).darts = d₁ :: d₂ :: l

Tactic:
simpa [hchain.rel.symm] using darts_ofDarts (l.cons_ne_nil d₂) hchain.of_cons

Premises used: List.IsChain.rel, List.IsChain.of_cons, List.cons_ne_nil, Eq.symm
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Basic
Goal:
V : Type u
G : SimpleGraph V
l : List G.Dart
hne : l ≠ []
hchain : List.IsChain G.DartAdj l
⊢ (ofDarts l hne hchain).darts = l

Tactic:
match l with
  | [_] => rfl
  | d₁ :: d₂ :: l =>
    simpa [hchain.rel.symm] using darts_ofDarts (l.cons_ne_nil d₂) hchain.of_cons
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Basic
Goal:
V : Type u
G : SimpleGraph V
l : List G.Dart
hne : l ≠ []
hchain : List.IsChain G.DartAdj l
⊢ (ofDarts l hne hchain).edges = List.map Dart.edge l

Tactic:
simp [edges]

Premises used: SimpleGraph.Walk.edges
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Basic
Goal:
V : Type u
G : SimpleGraph V
l : List G.Dart
hne : l ≠ []
hchain : List.IsChain G.DartAdj l
⊢ (ofDarts l hne hchain).length = l.length

Tactic:
grind [darts_ofDarts]

Premises used: SimpleGraph.Walk.darts_ofDarts
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Chord
Goal:
V : Type u_1
G : SimpleGraph V
u v w : V
p : G.Walk u v
e : Sym2 V
⊢ ∀ (a₁ a₂ : V),
    Eq (α := Prop) ((fun (v_1 w : V) ↦ v_1 ∈ p.support ∧ w ∈ p.support) a₁ a₂)
      ((fun (v_1 w : V) ↦ v_1 ∈ p.support ∧ w ∈ p.support) a₂ a₁)

Tactic:
grind
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Chord
Goal:
V : Type u_1
G : SimpleGraph V
u v : V
p : G.Walk u v
u' v' : V
⊢ p.IsChord s(u', v') ↔ G.Adj u' v' ∧ s(u', v') ∉ p.edges ∧ u' ∈ p.support ∧ v' ∈ p.support

Tactic:
.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Sym2.fromRel, SimpleGraph.Walk.IsChord
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Chord
Goal:
V : Type u_1
G : SimpleGraph V
u v : V
p : G.Walk u v
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
⊢ p.IsChordless ↔ ∀ ⦃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]

Premises used: Sym2.forall, SimpleGraph.Walk.isChord_sym2Mk, SimpleGraph.Walk.IsChordless
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Chord
Goal:
V : Type u_1
G : SimpleGraph V
u v : V
p : G.Walk u v
⊢ (∀ (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:
grind
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Chord
Goal:
V : Type u_1
G : SimpleGraph V
u v : V
p : G.Walk u v
h : p.IsChordless
u' v' : V
hu' : u' ∈ p.support
hv' : v' ∈ p.support
hadj : G.Adj u' v'
⊢ s(u', v') ∈ p.edges

Tactic:
isChordless_iff_forall_mem_edges.mp h hu' hv' hadj

Premises used: SimpleGraph.Walk.isChordless_iff_forall_mem_edges, Iff.mp
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Counting
Goal:
V : Type u
G : SimpleGraph V
u : V
⊢ Eq (α := Set (G.Walk u u)) {p : G.Walk u u | p.length = 0} {nil}

Tactic:
simp [Walk.length_eq_zero_iff, ← Walk.eq_nil_iff_nil]

Premises used: SimpleGraph.Walk.eq_nil_iff_nil, SimpleGraph.Walk.length_eq_zero_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Counting
Goal:
V : Type u
G : SimpleGraph V
u v : V
h : u ≠ v
⊢ Eq.{u + 1} (α := Set (G.Walk u v)) {p : G.Walk u v | p.length = 0} ∅

Tactic:
Set.eq_empty_of_forall_notMem (h <| ·.eq_of_length_eq_zero ·)

Premises used: SimpleGraph.Walk.eq_of_length_eq_zero, Set.eq_empty_of_forall_notMem
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Counting
Goal:
V : Type u
G : SimpleGraph V
u v : V
n : ℕ
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
⊢ 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})

Tactic:
ext p
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Counting
Goal:
V : Type u
G : SimpleGraph V
u : V
n : ℕ
⊢ 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:
simp [eq_comm]

Premises used: eq_comm
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Counting
Goal:
V : Type u
G : SimpleGraph V
u v : V
n : ℕ
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:
grind [length_cons, Set.mem_iUnion]

Premises used: Set.mem_iUnion, SimpleGraph.Walk.length_cons
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Counting
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
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)
⊢ 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:
cases p with
  | nil => simp [eq_comm]
  | cons huw pwv => grind [length_cons, Set.mem_iUnion]

Premises used: Set.mem_iUnion, eq_comm, SimpleGraph.Walk.cons, SimpleGraph.Walk.nil, SimpleGraph.Walk.length_cons
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Counting
Goal:
V : Type u
G : SimpleGraph V
u v v_1 : V
h : G.Adj u v_1
h_1 : G.Adj v_1 v
hp : (Walk.cons h (Walk.cons h_1 Walk.nil)).length = 2
⊢ Eq (α := { p : G.Walk u v // p.length = 2 })
    ((fun (w : (↑(G.commonNeighbors u v) : Type u)) ↦
        (Subtype.mk (p := fun (p : G.Walk u v) ↦ p.length = 2) ((Adj.toWalk ⋯).concat ⋯) ⋯ :
          { p : G.Walk u v // p.length = 2 }))
      ((fun (p : { p : G.Walk u v // p.length = 2 }) ↦
          (Subtype.mk (p := fun (x : V) ↦ x ∈ G.commonNeighbors u v) (↑p : G.Walk u v).snd ⋯ :
            { x : V // x ∈ G.commonNeighbors u v }))
        (Subtype.mk (p := fun (p : G.Walk u v) ↦ p.length = 2) (Walk.cons h (Walk.cons h_1 Walk.nil)) hp)))
    (Subtype.mk (p := fun (p : G.Walk u v) ↦ p.length = 2) (Walk.cons h (Walk.cons h_1 Walk.nil)) hp)

Tactic:
rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Counting
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
inst_1 : G.LocallyFinite
n : ℕ
u v : V
h : u = v
subst : Finset (G.Walk v v)
⊢ Finset (G.Walk u v)

Tactic:
subst u
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Counting
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
inst_1 : G.LocallyFinite
n : ℕ
v : V
⊢ Finset (G.Walk v v)

Tactic:
exact {Walk.nil}

Premises used: SimpleGraph.Walk.nil
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Counting
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
inst_1 : G.LocallyFinite
n_1 : ℕ
u v : V
n : ℕ
w : (↑(G.neighborSet u) : Type u)
x x_1 : G.Walk (↑w : V) v
⊢ Eq.{u + 1} (α := G.Walk u v) ((fun (p : G.Walk (↑w : V) v) ↦ Walk.cons ⋯ p) x)
      ((fun (p : G.Walk (↑w : V) v) ↦ Walk.cons ⋯ p) x_1) →
    x = x_1

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Counting
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
inst_1 : G.LocallyFinite
u v : V
⊢ (↑(G.finsetWalkLength 0 u v) : Set (G.Walk u v)) = {p : G.Walk u v | p.length = 0}

Tactic:
grind [finsetWalkLength, Walk.length_eq_zero_iff, Walk.eq_nil_iff_nil, Walk.Nil.eq]

Premises used: SimpleGraph.finsetWalkLength, SimpleGraph.Walk.eq_nil_iff_nil, SimpleGraph.Walk.Nil.eq, SimpleGraph.Walk.length_eq_zero_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Counting
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
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 ⋯ 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})
⊢ (↑(G.finsetWalkLength (n + 1) u v) : Set (G.Walk u v)) = {p : G.Walk u v | p.length = n + 1}

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]

Premises used: SimpleGraph.finsetWalkLength, Finset.mem_univ, Finset.coe_biUnion, Set.iUnion_coe_set, SimpleGraph.Walk.setOf_length_eq_add_one, Set.iUnion_true, Finset.coe_map, Finset.mem_coe
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Counting
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
succ :
  ∀ (x : V),
    (∀ {α : Type u} {p q : Prop} {f₁ : p → Set α} {f₂ : q → Set α} (pq : p ↔ q) (f : ∀ (x : q), f₁ ⋯ = 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}
⊢ 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})

Tactic:
congr!
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Counting
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 x : V
h_congr_thm :
  ∀ {α : Type u} {p q : Prop} {f₁ : p → Set α} {f₂ : q → Set α} (pq : p ↔ q) (f : ∀ (x : q), f₁ ⋯ = f₂ x),
    Set.iUnion f₁ = Set.iUnion f₂
h : G.Adj u x
⊢ (↑(G.finsetWalkLength n x v) : Set (G.Walk x v)) = {p' : G.Walk x v | p'.length = n}

Tactic:
grind
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Counting
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}
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}
⊢ (↑(G.finsetWalkLength n u v) : Set (G.Walk u v)) = {p : G.Walk u v | p.length = n}

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

Premises used: SimpleGraph.finsetWalkLength, Finset.mem_univ, Finset.coe_biUnion, SimpleGraph.Walk.eq_nil_iff_nil, Set.iUnion_coe_set, SimpleGraph.Walk.Nil.eq, SimpleGraph.Walk.setOf_length_eq_add_one, Set.iUnion_true, Finset.coe_map, Finset.mem_coe, SimpleGraph.Walk.length_eq_zero_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Counting
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
inst_1 : G.LocallyFinite
n : ℕ
u v : V
p : G.Walk u v
⊢ p ∈ G.finsetWalkLength n u v ↔ p.length = n

Tactic:
Set.ext_iff.mp (G.coe_finsetWalkLength_eq n u v) p

Premises used: Set.Mem, setOf, SimpleGraph.coe_finsetWalkLength_eq, Iff.mp, Set.ext_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Counting
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
inst_1 : G.LocallyFinite
n : ℕ
u v : V
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
⊢ (↑(G.finsetWalkLengthLT n u v) : Set (G.Walk u v)) = {p : G.Walk u v | p.length < n}

Tactic:
ext p
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Counting
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
inst_1 : G.LocallyFinite
n : ℕ
u v : V
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:
simp [finsetWalkLengthLT, mem_finsetWalkLength_iff]

Premises used: SimpleGraph.mem_finsetWalkLength_iff, SimpleGraph.finsetWalkLengthLT
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Counting
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
inst_1 : G.LocallyFinite
n : ℕ
u v : V
p : G.Walk u v
⊢ p ∈ G.finsetWalkLengthLT n u v ↔ p.length < n

Tactic:
Set.ext_iff.mp (G.coe_finsetWalkLengthLT_eq n u v) p

Premises used: Set.Mem, Iff.mp, Set.ext_iff, SimpleGraph.coe_finsetWalkLengthLT_eq, Nat.lt
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Counting
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
rw₁ 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
⊢ p ∈ G.finsetWalkLength n 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]

Premises used: SimpleGraph.coe_finsetWalkLength_eq, Finset.mem_coe
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Counting
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
inst_1 : G.LocallyFinite
n : ℕ
u v : V
⊢ Set.toFinset {p : G.Walk u v | p.length = n} = G.finsetWalkLength n u v

Tactic:
simp [← coe_finsetWalkLength_eq]

Premises used: SimpleGraph.coe_finsetWalkLength_eq
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Counting
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
rw₁ 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
⊢ p ∈ G.finsetWalkLengthLT n 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]

Premises used: SimpleGraph.coe_finsetWalkLengthLT_eq, Finset.mem_coe
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Counting
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
inst_1 : G.LocallyFinite
u v : V
n : ℕ
⊢ ∀ (x : G.Walk u v),
    x ∈ {w ∈ G.finsetWalkLength n u v | w.IsPath} ↔
      Membership.mem (γ := Set (G.Walk u v)) {p : G.Walk u v | p.IsPath ∧ p.length = n} x

Tactic:
simp [mem_finsetWalkLength_iff, and_comm]

Premises used: SimpleGraph.mem_finsetWalkLength_iff, and_comm
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Counting
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
inst_1 : G.LocallyFinite
u v : V
n : ℕ
⊢ ∀ (x : G.Walk u v),
    x ∈ {w ∈ G.finsetWalkLengthLT n u v | w.IsPath} ↔
      Membership.mem (γ := Set (G.Walk u v)) {p : G.Walk u v | p.IsPath ∧ p.length < n} x

Tactic:
simp [mem_finsetWalkLengthLT_iff, and_comm]

Premises used: and_comm, SimpleGraph.mem_finsetWalkLengthLT_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Decomp
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
rw rw₁ : G.Walk v v
⊢ G.Walk v u

Tactic:
rw [mem_support_nil_iff.mp h]

Premises used: SimpleGraph.Walk.mem_support_nil_iff, Iff.mp
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Decomp
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
tail : List.Mem u p.support → u ∈ p.support
⊢ u ∈ p.support

Tactic:
cases h
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Decomp
Goal:
V : Type u
G : SimpleGraph V
v_1 w_1 u : V
inst : DecidableEq V
v w_2 w v_2 : V
r : G.Adj v v_2
p : G.Walk v_2 w
hx : ¬v = v
⊢ v ∈ p.support

Tactic:
(hx rfl).elim

Premises used: False.elim, rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Decomp
Goal:
V : Type u
G : SimpleGraph V
v_1 w_1 u : V
inst : DecidableEq V
v w_2 w v_2 : V
r : G.Adj v v_2
p : G.Walk v_2 w
hx : ¬v = v
⊢ v ∈ p.support

Tactic:
exact (hx rfl).elim

Premises used: False.elim, rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Decomp
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
hx : ¬v = u
h : List.Mem u p.support
⊢ u ∈ p.support

Tactic:
assumption
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Decomp
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
u : V
h : Membership.mem (γ := List V) (support (G := G) (u := u) nil) u
⊢ takeUntil nil u h = nil

Tactic:
rfl

Premises used: Eq.mpr, SimpleGraph.Walk.takeUntil, rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Decomp
Goal:
V : Type u
G : SimpleGraph V
v w u : V
inst : DecidableEq V
v' : V
p : G.Walk v' v
hwp : w ∈ p.support
h : u ≠ w
hadj : G.Adj u v'
⊢ (cons hadj p).takeUntil w ⋯ = cons hadj (p.takeUntil w hwp)

Tactic:
simp [Walk.takeUntil, h]

Premises used: SimpleGraph.Walk.takeUntil