ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>a : Ordinal.{u}<VAR>n : ℕ<GOAL>↑n ♯ a = a + ↑n
<VAR>a b : Ordinal.{u}<GOAL>a + b ≤ a ♯ b
<VAR>a : NatOrdinal<GOAL>a + 1 = Order.succ a
<VAR>n : ℕ<GOAL>NatOrdinal.toOrdinal ↑n = ↑n
<VAR>a b : Ordinal.{u_1}<GOAL>a ♯ b = NatOrdinal.toOrdinal (Ordinal.toNatOrdinal a + Ordinal.toNatOrdinal b)
<VAR>n : ℕ<GOAL>Ordinal.toNatOrdinal ↑n = ↑n
<VAR>a b c : Ordinal.{u_1}<GOAL>a ♯ b < a ♯ c → b < c
<VAR>a b c : Ordinal.{u_1}<GOAL>b ♯ a < c ♯ a → b < c
<VAR>a b c : Ordinal.{u_1}<GOAL>a ♯ b ≤ a ♯ c → b ≤ c
<VAR>a b c : Ordinal.{u_1}<GOAL>b ♯ a ≤ c ♯ a → b ≤ c
<VAR>a : Ordinal.{u_1}<VAR>b c : Ordinal.{u_1}<GOAL>a ♯ b < a ♯ c ↔ b < c
<VAR>a : Ordinal.{u_1}<VAR>b c : Ordinal.{u_1}<GOAL>b ♯ a < c ♯ a ↔ b < c
<VAR>a : Ordinal.{u_1}<VAR>b c : Ordinal.{u_1}<GOAL>a ♯ b ≤ a ♯ c ↔ b ≤ c
<VAR>a : Ordinal.{u_1}<VAR>b c : Ordinal.{u_1}<GOAL>b ♯ a ≤ c ♯ a ↔ b ≤ c
<VAR>a b c d : Ordinal.{u_1}<GOAL>a ≤ b → c ≤ d → a ♯ c ≤ b ♯ d
<VAR>a b c d : Ordinal.{u_1}<GOAL>a < b → c < d → a ♯ c < b ♯ d
<VAR>a b c d : Ordinal.{u_1}<GOAL>a < b → c ≤ d → a ♯ c < b ♯ d
<VAR>a b c d : Ordinal.{u_1}<GOAL>a ≤ b → c < d → a ♯ c < b ♯ d
<VAR>a b c : Ordinal.{u_1}<GOAL>a ♯ b = a ♯ c → b = c
<VAR>a b c : Ordinal.{u_1}<GOAL>a ♯ b = c ♯ b → a = c
<VAR>a b c : Ordinal.{u_1}<GOAL>a ♯ b = a ♯ c ↔ b = c
<VAR>a b c : Ordinal.{u_1}<GOAL>b ♯ a = c ♯ a ↔ b = c
<VAR>a b c : Ordinal.{u_1}<VAR>h : a ≤ c<GOAL>a ≤ b ♯ c
<VAR>a b : Ordinal.{u_1}<GOAL>a ≤ a ♯ b
<VAR>a b c : Ordinal.{u_1}<VAR>h : a ≤ b<GOAL>a ≤ b ♯ c
<VAR>a b c : Ordinal.{u_1}<GOAL>a ♯ (b ♯ c) = b ♯ (a ♯ c)
<VAR>a b c : Ordinal.{u_1}<GOAL>a ♯ b ♯ c = a ♯ c ♯ b
<VAR>a b : Ordinal.{u_1}<GOAL>a ⨳ b = sInf {c | ∀ a' < a, ∀ b' < b, a' ⨳ b ♯ a ⨳ b' < c ♯ a' ⨳ b'}
<VAR>a b : Ordinal.{u}<GOAL>{c | ∀ a' < a, ∀ b' < b, a' ⨳ b ♯ a ⨳ b' < c ♯ a' ⨳ b'}.Nonempty
<VAR>a b a' b' : Ordinal.{u}<VAR>ha : a' < a<VAR>hb : b' < b<GOAL>a' ⨳ b ♯ a ⨳ b' < a ⨳ b ♯ a' ⨳ b'
<VAR>a b a' b' : Ordinal.{u}<VAR>ha : a' ≤ a<VAR>hb : b' ≤ b<GOAL>a' ⨳ b ♯ a ⨳ b' ≤ a ⨳ b ♯ a' ⨳ b'
<VAR>a b c : Ordinal.{u}<GOAL>c < a ⨳ b ↔ ∃ a' < a, ∃ b' < b, c ♯ a' ⨳ b' ≤ a' ⨳ b ♯ a ⨳ b'
<VAR>a b c : Ordinal.{u}<GOAL>a ⨳ b ≤ c ↔ ∀ a' < a, ∀ b' < b, a' ⨳ b ♯ a ⨳ b' < c ♯ a' ⨳ b'
<VAR>a b : Ordinal.{u_1}<GOAL>a ⨳ b = b ⨳ a
<VAR>a : Ordinal.{u_1}<GOAL>a ⨳ 0 = 0
<VAR>a : Ordinal.{u_1}<GOAL>0 ⨳ a = 0
<VAR>a : Ordinal.{u_1}<GOAL>a ⨳ 1 = a
<VAR>a : Ordinal.{u_1}<GOAL>1 ⨳ a = a
<VAR>a b c : Ordinal.{u}<VAR>h₁ : a < b<VAR>h₂ : 0 < c<GOAL>c ⨳ a < c ⨳ b
<VAR>a b c : Ordinal.{u}<VAR>h₁ : a < b<VAR>h₂ : 0 < c<GOAL>a ⨳ c < b ⨳ c
<VAR>a b c : Ordinal.{u}<VAR>h₁ : a ≤ b<VAR>h₂ : 0 ≤ c<GOAL>c ⨳ a ≤ c ⨳ b
<VAR>a b c : Ordinal.{u}<VAR>h₁ : a ≤ b<VAR>h₂ : 0 ≤ c<GOAL>a ⨳ c ≤ b ⨳ c
<VAR>a b c : Ordinal.{u_1}<GOAL>a ⨳ (b ♯ c) = a ⨳ b ♯ a ⨳ c
<VAR>a b c : Ordinal.{u_1}<GOAL>(a ♯ b) ⨳ c = a ⨳ c ♯ b ⨳ c
<VAR>a b c a' b' c' : Ordinal.{u}<VAR>ha : a' < a<VAR>hb : b' < b<VAR>hc : c' < c<GOAL>a' ⨳ b ⨳ c ♯ a ⨳ b' ⨳ c ♯ a ⨳ b ⨳ c' ♯ a' ⨳ b' ⨳ c' < a ⨳ b ⨳ c ♯ a' ⨳ b' ⨳ c ♯ a' ⨳ b ⨳ c' ♯ a ⨳ b' ⨳ c'
<VAR>a b c a' b' c' : Ordinal.{u}<VAR>ha : a' ≤ a<VAR>hb : b' ≤ b<VAR>hc : c' ≤ c<GOAL>a' ⨳ b ⨳ c ♯ a ⨳ b' ⨳ c ♯ a ⨳ b ⨳ c' ♯ a' ⨳ b' ⨳ c' ≤ a ⨳ b ⨳ c ♯ a' ⨳ b' ⨳ c ♯ a' ⨳ b ⨳ c' ♯ a ⨳ b' ⨳ c'
<VAR>a b c a' b' c' : Ordinal.{u}<VAR>ha : a' < a<VAR>hb : b' < b<VAR>hc : c' < c<GOAL>a' ⨳ (b ⨳ c) ♯ a ⨳ (b' ⨳ c) ♯ a ⨳ (b ⨳ c') ♯ a' ⨳ (b' ⨳ c') < a ⨳ (b ⨳ c) ♯ a' ⨳ (b' ⨳ c) ♯ a' ⨳ (b ⨳ c') ♯ a ⨳ (b' ⨳ c')
<VAR>a b c a' b' c' : Ordinal.{u}<VAR>ha : a' ≤ a<VAR>hb : b' ≤ b<VAR>hc : c' ≤ c<GOAL>a' ⨳ (b ⨳ c) ♯ a ⨳ (b' ⨳ c) ♯ a ⨳ (b ⨳ c') ♯ a' ⨳ (b' ⨳ c') ≤ a ⨳ (b ⨳ c) ♯ a' ⨳ (b' ⨳ c) ♯ a' ⨳ (b ⨳ c') ♯ a ⨳ (b' ⨳ c')
<VAR>a b c d : Ordinal.{u}<GOAL>d < a ⨳ b ⨳ c ↔ ∃ a' < a, ∃ b' < b, ∃ c' < c, d ♯ a' ⨳ b' ⨳ c ♯ a' ⨳ b ⨳ c' ♯ a ⨳ b' ⨳ c' ≤ a' ⨳ b ⨳ c ♯ a ⨳ b' ⨳ c ♯ a ⨳ b ⨳ c' ♯ a' ⨳ b' ⨳ c'
<VAR>a b c : Ordinal.{u_1}<GOAL>a ⨳ b ⨳ c = a ⨳ (b ⨳ c)
<VAR>a b : Ordinal.{u_1}<GOAL>a ⨳ b = NatOrdinal.toOrdinal (Ordinal.toNatOrdinal a * Ordinal.toNatOrdinal b)
<VAR>a b : Ordinal.{u_1}<GOAL>a ⨳ (b ♯ 1) = a ⨳ b ♯ a
<VAR>a b : Ordinal.{u_1}<GOAL>(a ♯ 1) ⨳ b = a ⨳ b ♯ b
<VAR>a b : Ordinal.{u_1}<GOAL>a ⨳ Order.succ b = a ⨳ b ♯ a
<VAR>a b : Ordinal.{u_1}<GOAL>Order.succ a ⨳ b = a ⨳ b ♯ b
<VAR>a b : Ordinal.{u_1}<GOAL>a ⨳ (b + 1) = a ⨳ b ♯ a
<VAR>a b : Ordinal.{u_1}<GOAL>(a + 1) ⨳ b = a ⨳ b ♯ b
<VAR>a b : Ordinal.{u}<GOAL>a * b ≤ a ⨳ b
<VAR>n : ℕ<GOAL>0 < SzemerediRegularity.stepBound n ↔ 0 < n
<VAR>α : Type u_1<VAR>Semiring α<VAR>n : ℕ<GOAL>↑(SzemerediRegularity.stepBound n) = ↑n * 4 ^ n
<VAR>ε : ℝ<VAR>n : ℕ<VAR>h : 100 ≤ 4 ^ n * ε ^ 5<GOAL>0 < ε
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>Fintype α<VAR>P : Finpartition Finset.univ<VAR>Nonempty α<VAR>hPα : P.parts.card * 16 ^ P.parts.card ≤ Fintype.card α<GOAL>0 < m
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>Fintype α<VAR>P : Finpartition Finset.univ<GOAL>0 < ↑m + 1
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>Fintype α<VAR>P : Finpartition Finset.univ<VAR>Nonempty α<VAR>hPα : P.parts.card * 16 ^ P.parts.card ≤ Fintype.card α<GOAL>1 ≤ ↑m
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>Fintype α<VAR>P : Finpartition Finset.univ<VAR>ε : ℝ<VAR>hPε : 100 ≤ 4 ^ P.parts.card * ε ^ 5<GOAL>0 < ε ^ 5
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>Fintype α<VAR>P : Finpartition Finset.univ<VAR>ε : ℝ<VAR>hPε : 100 ≤ 4 ^ P.parts.card * ε ^ 5<GOAL>0 < ε
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>Fintype α<VAR>P : Finpartition Finset.univ<VAR>ε : ℝ<VAR>Nonempty α<VAR>hPα : P.parts.card * 16 ^ P.parts.card ≤ Fintype.card α<VAR>hPε : 100 ≤ 4 ^ P.parts.card * ε ^ 5<GOAL>100 / ε ^ 5 ≤ ↑m
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>Fintype α<VAR>P : Finpartition Finset.univ<VAR>ε : ℝ<VAR>Nonempty α<VAR>hPα : P.parts.card * 16 ^ P.parts.card ≤ Fintype.card α<VAR>hPε : 100 ≤ 4 ^ P.parts.card * ε ^ 5<VAR>hε : ε ≤ 1<GOAL>100 ≤ m
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>Fintype α<VAR>P : Finpartition Finset.univ<GOAL>a + 1 ≤ 4 ^ P.parts.card
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>Fintype α<VAR>P : Finpartition Finset.univ<VAR>u : Finset α<VAR>hucard : u.card = m * 4 ^ P.parts.card + a<GOAL>(4 ^ P.parts.card - a) * m + a * (m + 1) = u.card
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>Fintype α<VAR>P : Finpartition Finset.univ<VAR>u : Finset α<VAR>hP : P.IsEquipartition<VAR>hu : u ∈ P.parts<VAR>hucard : ¬u.card = m * 4 ^ P.parts.card + a<GOAL>(4 ^ P.parts.card - (a + 1)) * m + (a + 1) * (m + 1) = u.card
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>Fintype α<VAR>P : Finpartition Finset.univ<VAR>u : Finset α<VAR>hP : P.IsEquipartition<VAR>hu : u ∈ P.parts<GOAL>4 ^ P.parts.card * ↑m ≤ ↑u.card
<VAR>ε : ℝ<VAR>l : ℕ<GOAL>l ≤ SzemerediRegularity.initialBound ε l
<VAR>ε : ℝ<VAR>l : ℕ<GOAL>7 ≤ SzemerediRegularity.initialBound ε l
<VAR>ε : ℝ<VAR>l : ℕ<GOAL>0 < SzemerediRegularity.initialBound ε l
<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>l : ℕ<GOAL>100 < 4 ^ SzemerediRegularity.initialBound ε l * ε ^ 5
<VAR>ε : ℝ<VAR>l : ℕ<GOAL>SzemerediRegularity.initialBound ε l ≤ SzemerediRegularity.bound ε l
<VAR>ε : ℝ<VAR>l : ℕ<GOAL>l ≤ SzemerediRegularity.bound ε l
<VAR>ε : ℝ<VAR>l : ℕ<GOAL>0 < SzemerediRegularity.bound ε l
<VAR>ι : Type u_2<VAR>𝕜 : Type u_3<VAR>LinearOrderedField 𝕜<VAR>s t : Finset ι<VAR>x : 𝕜<VAR>hst : s ⊆ t<VAR>f : ι → 𝕜<VAR>hs : x ^ 2 ≤ ((∑ i ∈ s, f i) / ↑s.card) ^ 2<VAR>hs' : ↑s.card ≠ 0<GOAL>↑s.card * x ^ 2 ≤ ∑ i ∈ t, f i ^ 2
<VAR>ι : Type u_2<VAR>𝕜 : Type u_3<VAR>LinearOrderedField 𝕜<VAR>s t : Finset ι<VAR>x : 𝕜<VAR>hst : s ⊆ t<VAR>f : ι → 𝕜<VAR>d : 𝕜<VAR>hx : 0 ≤ x<VAR>hs : x ≤ |(∑ i ∈ s, f i) / ↑s.card - (∑ i ∈ t, f i) / ↑t.card|<VAR>ht : d ≤ ((∑ i ∈ t, f i) / ↑t.card) ^ 2<GOAL>d + ↑s.card / ↑t.card * x ^ 2 ≤ (∑ i ∈ t, f i ^ 2) / ↑t.card
<VAR>α : Type u_1<VAR>G : SimpleGraph α<VAR>n : ℕ∞<GOAL>n ≤ G.egirth ↔ ∀ (a : α) (w : G.Walk a a), w.IsCycle → n ≤ ↑w.length
<VAR>α : Type u_1<VAR>G : SimpleGraph α<GOAL>G.egirth = ⊤ ↔ G.IsAcyclic
<VAR>α : Type u_1<GOAL>Antitone SimpleGraph.egirth
<VAR>α : Type u_1<VAR>G : SimpleGraph α<GOAL>(∃ a w, w.IsCycle ∧ G.egirth = ↑w.length) ↔ ¬G.IsAcyclic
<VAR>α : Type u_1<VAR>G : SimpleGraph α<GOAL>3 ≤ G.egirth
<VAR>α : Type u_1<GOAL>⊥.egirth = ⊤
<VAR>α : Type u_1<VAR>G : SimpleGraph α<VAR>hG : ¬G.IsAcyclic<GOAL>3 ≤ G.girth
<VAR>α : Type u_1<VAR>G : SimpleGraph α<GOAL>G.girth = 0 ↔ G.IsAcyclic
<VAR>α : Type u_1<VAR>G G' : SimpleGraph α<VAR>hab : G ≤ G'<VAR>h : ¬G.IsAcyclic<GOAL>G'.girth ≤ G.girth
<VAR>α : Type u_1<GOAL>⊥.girth = 0
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>v : V<GOAL>default = SimpleGraph.Walk.nil
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>u v : V<VAR>p : G.Walk u v<GOAL>p.copy ⋯ ⋯ = p
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>u v u' v' u'' v'' : V<VAR>p : G.Walk u v<VAR>hu : u = u'<VAR>hv : v = v'<VAR>hu' : u' = u''<VAR>hv' : v' = v''<GOAL>(p.copy hu hv).copy hu' hv' = p.copy ⋯ ⋯
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>u u' : V<VAR>hu : u = u'<GOAL>SimpleGraph.Walk.nil.copy hu hu = SimpleGraph.Walk.nil
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>u v w u' w' : V<VAR>h : G.Adj u v<VAR>p : G.Walk v w<VAR>hu : u = u'<VAR>hw : w = w'<GOAL>(SimpleGraph.Walk.cons h p).copy hu hw = SimpleGraph.Walk.cons ⋯ (p.copy ⋯ hw)
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>u v w v' w' : V<VAR>h : G.Adj u v<VAR>p : G.Walk v' w'<VAR>hv : v' = v<VAR>hw : w' = w<GOAL>SimpleGraph.Walk.cons h (p.copy hv hw) = (SimpleGraph.Walk.cons ⋯ p).copy ⋯ hw
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>u v : V<VAR>hne : u ≠ v<VAR>p : G.Walk u v<GOAL>∃ w, ∃ (h : G.Adj u w), ∃ p', p = SimpleGraph.Walk.cons h p'
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>u v w : V<VAR>p : G.Walk u v<VAR>h : G.Adj v w<GOAL>p.concat h = p.append (SimpleGraph.Walk.cons h SimpleGraph.Walk.nil)
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>u v : V<VAR>w : G.Walk u v<GOAL>w.getVert 0 = u
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>u v : V<VAR>w : G.Walk u v<VAR>i : ℕ<VAR>hi : w.length ≤ i<GOAL>w.getVert i = v
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>u v : V<VAR>w : G.Walk u v<GOAL>w.getVert w.length = v
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>u v : V<VAR>w : G.Walk u v<VAR>i : ℕ<VAR>hi : i < w.length<GOAL>G.Adj (w.getVert i) (w.getVert (i + 1))
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>u v w : V<VAR>n : ℕ<VAR>p : G.Walk v w<VAR>h : G.Adj u v<GOAL>(SimpleGraph.Walk.cons h p).getVert (n + 1) = p.getVert n
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>u v w : V<VAR>n : ℕ<VAR>p : G.Walk v w<VAR>h : G.Adj u v<VAR>hn : n ≠ 0<GOAL>(SimpleGraph.Walk.cons h p).getVert n = p.getVert (n - 1)
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>u v w x : V<VAR>h : G.Adj u v<VAR>p : G.Walk v w<VAR>q : G.Walk w x<GOAL>(SimpleGraph.Walk.cons h p).append q = SimpleGraph.Walk.cons h (p.append q)
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>u v w : V<VAR>h : G.Adj u v<VAR>p : G.Walk v w<GOAL>(SimpleGraph.Walk.cons h SimpleGraph.Walk.nil).append p = SimpleGraph.Walk.cons h p
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>u v : V<VAR>p : G.Walk u v<GOAL>p.append SimpleGraph.Walk.nil = p
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>u v : V<VAR>p : G.Walk u v<GOAL>SimpleGraph.Walk.nil.append p = p
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>u v w x : V<VAR>p : G.Walk u v<VAR>q : G.Walk v w<VAR>r : G.Walk w x<GOAL>p.append (q.append r) = (p.append q).append r
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>u v w u' v' w' : V<VAR>p : G.Walk u v<VAR>q : G.Walk v w<VAR>hu : u = u'<VAR>hv : v = v'<VAR>hw : w = w'<GOAL>(p.copy hu hv).append (q.copy hv hw) = (p.append q).copy hu hw
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>u v : V<VAR>h : G.Adj u v<GOAL>SimpleGraph.Walk.nil.concat h = SimpleGraph.Walk.cons h SimpleGraph.Walk.nil
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>u v w x : V<VAR>h : G.Adj u v<VAR>p : G.Walk v w<VAR>h' : G.Adj w x<GOAL>(SimpleGraph.Walk.cons h p).concat h' = SimpleGraph.Walk.cons h (p.concat h')
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>u v w x : V<VAR>p : G.Walk u v<VAR>q : G.Walk v w<VAR>h : G.Adj w x<GOAL>p.append (q.concat h) = (p.append q).concat h
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>u v w x : V<VAR>p : G.Walk u v<VAR>h : G.Adj v w<VAR>q : G.Walk w x<GOAL>(p.concat h).append q = p.append (SimpleGraph.Walk.cons h q)
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>u v w : V<VAR>h : G.Adj u v<VAR>p : G.Walk v w<GOAL>∃ x q, ∃ (h' : G.Adj x w), SimpleGraph.Walk.cons h p = q.concat h'
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>u v w : V<VAR>p : G.Walk u v<VAR>h : G.Adj v w<GOAL>∃ x, ∃ (h' : G.Adj u x), ∃ q, p.concat h = SimpleGraph.Walk.cons h' q
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>u : V<GOAL>SimpleGraph.Walk.nil.reverse = SimpleGraph.Walk.nil
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>u v : V<VAR>h : G.Adj u v<GOAL>(SimpleGraph.Walk.cons h SimpleGraph.Walk.nil).reverse = SimpleGraph.Walk.cons ⋯ SimpleGraph.Walk.nil
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>u v w x : V<VAR>p : G.Walk u v<VAR>q : G.Walk w x<VAR>h : G.Adj w u<GOAL>(SimpleGraph.Walk.cons h p).reverseAux q = p.reverseAux (SimpleGraph.Walk.cons ⋯ q)
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>u v w x : V<VAR>p : G.Walk u v<VAR>q : G.Walk v w<VAR>r : G.Walk u x<GOAL>(p.append q).reverseAux r = q.reverseAux (p.reverseAux r)
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>u v w x : V<VAR>p : G.Walk u v<VAR>q : G.Walk u w<VAR>r : G.Walk w x<GOAL>(p.reverseAux q).append r = p.reverseAux (q.append r)
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>u v w : V<VAR>p : G.Walk u v<VAR>q : G.Walk u w<GOAL>p.reverseAux q = p.reverse.append q
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>u v w : V<VAR>h : G.Adj u v<VAR>p : G.Walk v w<GOAL>(SimpleGraph.Walk.cons h p).reverse = p.reverse.append (SimpleGraph.Walk.cons ⋯ SimpleGraph.Walk.nil)
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>u v u' v' : V<VAR>p : G.Walk u v<VAR>hu : u = u'<VAR>hv : v = v'<GOAL>(p.copy hu hv).reverse = p.reverse.copy hv hu
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>u v w : V<VAR>p : G.Walk u v<VAR>q : G.Walk v w<GOAL>(p.append q).reverse = q.reverse.append p.reverse
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>u v w : V<VAR>p : G.Walk u v<VAR>h : G.Adj v w<GOAL>(p.concat h).reverse = SimpleGraph.Walk.cons ⋯ p.reverse
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>u v : V<VAR>p : G.Walk u v<GOAL>p.reverse.reverse = p
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>u v : V<GOAL>Function.Surjective SimpleGraph.Walk.reverse
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>u v : V<GOAL>Function.Injective SimpleGraph.Walk.reverse
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>u v : V<GOAL>Function.Bijective SimpleGraph.Walk.reverse
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>u : V<GOAL>SimpleGraph.Walk.nil.length = 0
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>u v w : V<VAR>h : G.Adj u v<VAR>p : G.Walk v w<GOAL>(SimpleGraph.Walk.cons h p).length = p.length + 1
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>u v u' v' : V<VAR>p : G.Walk u v<VAR>hu : u = u'<VAR>hv : v = v'<GOAL>(p.copy hu hv).length = p.length
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>u v w : V<VAR>p : G.Walk u v<VAR>q : G.Walk v w<GOAL>(p.append q).length = p.length + q.length
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>u v w : V<VAR>p : G.Walk u v<VAR>h : G.Adj v w<GOAL>(p.concat h).length = p.length + 1
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>u v w : V<VAR>p : G.Walk u v<VAR>q : G.Walk u w<GOAL>(p.reverseAux q).length = p.length + q.length
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>u v : V<VAR>p : G.Walk u v<GOAL>p.reverse.length = p.length
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>u v : V<VAR>p : G.Walk u v<GOAL>p.length = 0 → u = v
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>u v : V<VAR>p : G.Walk u v<GOAL>p.length = 1 → G.Adj u v
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>u v : V<GOAL>(∃ p, p.length = 0) ↔ u = v
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>u : V<VAR>p : G.Walk u u<GOAL>p.length = 0 ↔ p = SimpleGraph.Walk.nil
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>u v w : V<VAR>p : G.Walk u v<VAR>q : G.Walk v w<VAR>i : ℕ<GOAL>(p.append q).getVert i = if i < p.length then p.getVert i else q.getVert (i - p.length)
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>u v : V<VAR>p : G.Walk u v<VAR>i : ℕ<GOAL>p.reverse.getVert i = p.getVert (p.length - i)
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>motive : (u v : V) → G.Walk u v → Sort u_1<VAR>Hnil : {u : V} → motive u u SimpleGraph.Walk.nil<VAR>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)<VAR>u : V<GOAL>SimpleGraph.Walk.concatRec Hnil Hconcat SimpleGraph.Walk.nil = Hnil
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>motive : (u v : V) → G.Walk u v → Sort u_1<VAR>Hnil : {u : V} → motive u u SimpleGraph.Walk.nil<VAR>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)<VAR>u v w : V<VAR>p : G.Walk u v<VAR>h : G.Adj v w<GOAL>SimpleGraph.Walk.concatRec Hnil Hconcat (p.concat h) = Hconcat p h (SimpleGraph.Walk.concatRec Hnil Hconcat p)
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>u v : V<VAR>p : G.Walk u v<VAR>h : G.Adj v u<GOAL>p.concat h ≠ SimpleGraph.Walk.nil
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>u v v' w : V<VAR>p : G.Walk u v<VAR>h : G.Adj v w<VAR>p' : G.Walk u v'<VAR>h' : G.Adj v' w<VAR>he : p.concat h = p'.concat h'<GOAL>∃ (hv : v = v'), p.copy ⋯ hv = p'
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>u : V<GOAL>SimpleGraph.Walk.nil.support = [u]
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>u v w : V<VAR>h : G.Adj u v<VAR>p : G.Walk v w<GOAL>(SimpleGraph.Walk.cons h p).support = u :: p.support
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>u v w : V<VAR>p : G.Walk u v<VAR>h : G.Adj v w<GOAL>(p.concat h).support = p.support.concat w
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>u v u' v' : V<VAR>p : G.Walk u v<VAR>hu : u = u'<VAR>hv : v = v'<GOAL>(p.copy hu hv).support = p.support
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>u v w : V<VAR>p : G.Walk u v<VAR>p' : G.Walk v w<GOAL>(p.append p').support = p.support ++ p'.support.tail
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>u v : V<VAR>p : G.Walk u v<GOAL>p.reverse.support = p.support.reverse
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>u v : V<VAR>p : G.Walk u v<GOAL>p.support ≠ []
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>u v w : V<VAR>p : G.Walk u v<VAR>p' : G.Walk v w<GOAL>(p.append p').support.tail = p.support.tail ++ p'.support.tail
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>u v : V<VAR>p : G.Walk u v<GOAL>p.support = u :: p.support.tail
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>u v : V<VAR>p : G.Walk u v<GOAL>u ∈ p.support
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>u v : V<VAR>p : G.Walk u v<GOAL>v ∈ p.support
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>u v : V<VAR>p : G.Walk u v<GOAL>{w | w ∈ p.support}.Nonempty
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>u v w : V<VAR>p : G.Walk u v<GOAL>w ∈ p.support ↔ w = u ∨ w ∈ p.support.tail
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>u v : V<GOAL>u ∈ SimpleGraph.Walk.nil.support ↔ u = v
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>t u v w : V<VAR>p : G.Walk u v<VAR>p' : G.Walk v w<GOAL>t ∈ (p.append p').support.tail ↔ t ∈ p.support.tail ∨ t ∈ p'.support.tail
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>u v : V<VAR>h : u ≠ v<VAR>p : G.Walk u v<GOAL>v ∈ p.support.tail
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>t u v w : V<VAR>p : G.Walk u v<VAR>p' : G.Walk v w<GOAL>t ∈ (p.append p').support ↔ t ∈ p.support ∨ t ∈ p'.support
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>u v w : V<VAR>p : G.Walk u v<VAR>q : G.Walk v w<GOAL>p.support ⊆ (p.append q).support
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>u v w : V<VAR>p : G.Walk u v<VAR>q : G.Walk v w<GOAL>q.support ⊆ (p.append q).support
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>u v : V<VAR>p : G.Walk u v<GOAL>↑p.support = {u} + ↑p.support.tail
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>u v w : V<VAR>p : G.Walk u v<VAR>p' : G.Walk v w<GOAL>↑(p.append p').support = {u} + ↑p.support.tail + ↑p'.support.tail
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>DecidableEq V<VAR>u v w : V<VAR>p : G.Walk u v<VAR>p' : G.Walk v w<GOAL>↑(p.append p').support = ↑p.support + ↑p'.support - {v}
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>u v w : V<VAR>h : G.Adj u v<VAR>p : G.Walk v w<GOAL>List.Chain G.Adj u p.support
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>u v : V<VAR>p : G.Walk u v<GOAL>List.Chain' G.Adj p.support
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>d : G.Dart<VAR>v w : V<VAR>h : d.toProd.2 = v<VAR>p : G.Walk v w<GOAL>List.Chain G.DartAdj d p.darts
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>u v : V<VAR>p : G.Walk u v<GOAL>List.Chain' G.DartAdj p.darts
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>u v : V<VAR>p : G.Walk u v<VAR>e : Sym2 V<GOAL>e ∈ p.edges → e ∈ G.edgeSet
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>u v x y : V<VAR>p : G.Walk u v<VAR>h : s(x, y) ∈ p.edges<GOAL>G.Adj x y
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>u : V<GOAL>SimpleGraph.Walk.nil.darts = []
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>u v w : V<VAR>h : G.Adj u v<VAR>p : G.Walk v w<GOAL>(SimpleGraph.Walk.cons h p).darts = { toProd := (u, v), adj := h } :: p.darts
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>u v w : V<VAR>p : G.Walk u v<VAR>h : G.Adj v w<GOAL>(p.concat h).darts = p.darts.concat { toProd := (v, w), adj := h }
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>u v u' v' : V<VAR>p : G.Walk u v<VAR>hu : u = u'<VAR>hv : v = v'<GOAL>(p.copy hu hv).darts = p.darts
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>u v w : V<VAR>p : G.Walk u v<VAR>p' : G.Walk v w<GOAL>(p.append p').darts = p.darts ++ p'.darts
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>u v : V<VAR>p : G.Walk u v<GOAL>p.reverse.darts = (List.map SimpleGraph.Dart.symm p.darts).reverse
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>u v : V<VAR>d : G.Dart<VAR>p : G.Walk u v<GOAL>d ∈ p.reverse.darts ↔ d.symm ∈ p.darts
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>u v : V<VAR>p : G.Walk u v<GOAL>u :: List.map (fun x => x.toProd.2) p.darts = p.support
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>u v : V<VAR>p : G.Walk u v<GOAL>List.map (fun x => x.toProd.2) p.darts = p.support.tail
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>u v : V<VAR>p : G.Walk u v<GOAL>List.map (fun x => x.toProd.1) p.darts ++ [v] = p.support
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>u v : V<VAR>p : G.Walk u v<GOAL>List.map (fun x => x.toProd.1) p.darts = p.support.dropLast
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>u : V<GOAL>SimpleGraph.Walk.nil.edges = []
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>u v w : V<VAR>h : G.Adj u v<VAR>p : G.Walk v w<GOAL>(SimpleGraph.Walk.cons h p).edges = s(u, v) :: p.edges
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>u v w : V<VAR>p : G.Walk u v<VAR>h : G.Adj v w<GOAL>(p.concat h).edges = p.edges.concat s(v, w)
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>u v u' v' : V<VAR>p : G.Walk u v<VAR>hu : u = u'<VAR>hv : v = v'<GOAL>(p.copy hu hv).edges = p.edges
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>u v w : V<VAR>p : G.Walk u v<VAR>p' : G.Walk v w<GOAL>(p.append p').edges = p.edges ++ p'.edges
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>u v : V<VAR>p : G.Walk u v<GOAL>p.reverse.edges = p.edges.reverse
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>u v : V<VAR>p : G.Walk u v<GOAL>p.support.length = p.length + 1
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>u v : V<VAR>p : G.Walk u v<GOAL>p.darts.length = p.length
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>u v : V<VAR>p : G.Walk u v<GOAL>p.edges.length = p.length
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>u v : V<VAR>p : G.Walk u v<VAR>d : G.Dart<GOAL>d ∈ p.darts → d.toProd.1 ∈ p.support
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>u v : V<VAR>p : G.Walk u v<VAR>d : G.Dart<VAR>h : d ∈ p.darts<GOAL>d.toProd.2 ∈ p.support
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>t u v w : V<VAR>p : G.Walk v w<VAR>he : s(t, u) ∈ p.edges<GOAL>t ∈ p.support
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>t u v w : V<VAR>p : G.Walk v w<VAR>he : s(t, u) ∈ p.edges<GOAL>u ∈ p.support
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>u v : V<VAR>p : G.Walk u v<VAR>h : p.support.Nodup<GOAL>p.darts.Nodup
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>u v : V<VAR>p : G.Walk u v<VAR>h : p.support.Nodup<GOAL>p.edges.Nodup
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>u : V<GOAL>SimpleGraph.Walk.nil.Nil
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>u v w : V<VAR>h : G.Adj u v<VAR>p : G.Walk v w<GOAL>¬(SimpleGraph.Walk.cons h p).Nil
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>v w : V<VAR>p : G.Walk v w<GOAL>p.Nil → v = w
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>v w : V<VAR>p : G.Walk v w<GOAL>v ≠ w → ¬p.Nil
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>v w : V<VAR>p : G.Walk v w<GOAL>p.Nil ↔ p.support = [v]
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>v w : V<VAR>p : G.Walk v w<GOAL>p.Nil ↔ p.length = 0
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>v w : V<VAR>p : G.Walk v w<GOAL>¬p.Nil ↔ ∃ u, ∃ (h : G.Adj v u), ∃ q, p = SimpleGraph.Walk.cons h q