ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>V : Type u_1<VAR>G : SimpleGraph V<VAR>s s' : Set V<VAR>h : s ≤ s'<GOAL>(G.induceHomOfLE h).toHom = SimpleGraph.induceHom SimpleGraph.Hom.id ⋯
<VAR>V : Type u_1<VAR>W : Type u_2<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph W<VAR>f : G ≃g G'<VAR>v w : V<GOAL>G'.Adj (f v) (f w) ↔ G.Adj v w
<VAR>V : Type u_1<VAR>W : Type u_2<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph W<VAR>f : G ≃g G'<VAR>e : Sym2 V<GOAL>Sym2.map (⇑f) e ∈ G'.edgeSet ↔ e ∈ G.edgeSet
<VAR>V : Type u_1<VAR>W : Type u_2<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph W<VAR>f : G ≃g G'<VAR>v w : V<GOAL>f w ∈ G'.neighborSet (f v) ↔ w ∈ G.neighborSet v
<VAR>V : Type u_1<VAR>W : Type u_2<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph W<VAR>f : G ≃g G'<VAR>e : ↑G'.edgeSet<GOAL>f.mapEdgeSet.symm e = SimpleGraph.Hom.mapEdgeSet (RelIso.toRelEmbedding f.symm).toRelHom e
<VAR>V : Type u_1<VAR>W : Type u_2<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph W<VAR>f : G ≃g G'<VAR>e : ↑G.edgeSet<GOAL>f.mapEdgeSet e = SimpleGraph.Hom.mapEdgeSet (RelIso.toRelEmbedding f).toRelHom e
<VAR>V : Type u_1<VAR>W : Type u_2<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph W<VAR>f : G ≃g G'<VAR>v : V<VAR>w : ↑(G'.neighborSet (f v))<GOAL>↑((f.mapNeighborSet v).symm w) = f.symm ↑w
<VAR>V : Type u_1<VAR>W : Type u_2<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph W<VAR>f : G ≃g G'<VAR>v : V<VAR>w : ↑(G.neighborSet v)<GOAL>↑((f.mapNeighborSet v) w) = f ↑w
<VAR>V : Type u_1<VAR>W : Type u_2<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph W<VAR>f : G ≃g G'<VAR>Fintype V<VAR>Fintype W<GOAL>Fintype.card V = Fintype.card W
<VAR>V : Type u_1<VAR>W : Type u_2<VAR>f : V ≃ W<VAR>G : SimpleGraph W<VAR>v : V<GOAL>(SimpleGraph.Iso.comap f G) v = f v
<VAR>V : Type u_1<VAR>W : Type u_2<VAR>f : V ≃ W<VAR>G : SimpleGraph W<VAR>w : W<GOAL>(SimpleGraph.Iso.comap f G).symm w = f.symm w
<VAR>V : Type u_1<VAR>W : Type u_2<VAR>f : V ≃ W<VAR>G : SimpleGraph V<VAR>v : V<GOAL>(SimpleGraph.Iso.map f G) v = f v
<VAR>V : Type u_1<VAR>W : Type u_2<VAR>f : V ≃ W<VAR>G : SimpleGraph V<VAR>w : W<GOAL>(SimpleGraph.Iso.map f G).symm w = f.symm w
<VAR>α : Type u_4<VAR>β : Type u_5<VAR>f : α ≃ β<GOAL>(SimpleGraph.Iso.completeGraph f).toEmbedding = SimpleGraph.Embedding.completeGraph f.toEmbedding
<VAR>V : Type u_1<VAR>W : Type u_2<VAR>X : Type u_3<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph W<VAR>G'' : SimpleGraph X<VAR>f' : G' ≃g G''<VAR>f : G ≃g G'<GOAL>⇑(f'.comp f) = ⇑f' ∘ ⇑f
<VAR>V : Type u_1<VAR>G : SimpleGraph V<VAR>a : V<GOAL>↑((RelIso.symm G.induceUnivIso) a) = a
<VAR>V : Type u_1<VAR>G : SimpleGraph V<VAR>self : { x // x ∈ Set.univ }<GOAL>G.induceUnivIso self = ↑self
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>DecidableEq α<VAR>DecidableEq β<VAR>G : SimpleGraph α<VAR>a b : α<VAR>p : G.Walk a b<VAR>H : SimpleGraph β<VAR>f : G →g H<VAR>hf : Function.Bijective ⇑f<VAR>hp : p.IsHamiltonian<GOAL>(SimpleGraph.Walk.map f p).IsHamiltonian
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>G : SimpleGraph α<VAR>a b : α<VAR>p : G.Walk a b<VAR>hp : p.IsHamiltonian<VAR>c : α<GOAL>c ∈ p.support
<VAR>α : Type u_1<VAR>Fintype α<VAR>DecidableEq α<VAR>G : SimpleGraph α<VAR>a b : α<VAR>p : G.Walk a b<VAR>hp : p.IsHamiltonian<GOAL>p.support.toFinset = Finset.univ
<VAR>α : Type u_1<VAR>Fintype α<VAR>DecidableEq α<VAR>G : SimpleGraph α<VAR>a b : α<VAR>p : G.Walk a b<VAR>hp : p.IsHamiltonian<GOAL>p.length = Fintype.card α - 1
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>G : SimpleGraph α<VAR>a b : α<VAR>p : G.Walk a b<VAR>hp : p.IsHamiltonian<GOAL>p.IsPath
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>G : SimpleGraph α<VAR>a b : α<VAR>p : G.Walk a b<VAR>hp : p.IsPath<VAR>hp' : ∀ (w : α), w ∈ p.support<GOAL>p.IsHamiltonian
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>G : SimpleGraph α<VAR>a b : α<VAR>p : G.Walk a b<VAR>hp : p.IsPath<GOAL>p.IsHamiltonian ↔ ∀ (w : α), w ∈ p.support
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>G : SimpleGraph α<VAR>a : α<VAR>p : G.Walk a a<VAR>self : p.IsHamiltonianCycle<GOAL>(p.tail ⋯).IsHamiltonian
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>G : SimpleGraph α<VAR>a : α<VAR>p : G.Walk a a<VAR>hp : p.IsHamiltonianCycle<GOAL>p.IsCycle
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>DecidableEq α<VAR>DecidableEq β<VAR>G : SimpleGraph α<VAR>a : α<VAR>p : G.Walk a a<VAR>H : SimpleGraph β<VAR>f : G →g H<VAR>hf : Function.Bijective ⇑f<VAR>hp : p.IsHamiltonianCycle<GOAL>(SimpleGraph.Walk.map f p).IsHamiltonianCycle
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>G : SimpleGraph α<VAR>a : α<VAR>p : G.Walk a a<GOAL>p.IsHamiltonianCycle ↔ ∃ (h : p.IsCycle), (p.tail ⋯).IsHamiltonian
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>G : SimpleGraph α<VAR>a : α<VAR>p : G.Walk a a<GOAL>p.IsHamiltonianCycle ↔ p.IsCycle ∧ ∀ (a_1 : α), List.count a_1 p.support.tail = 1
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>G : SimpleGraph α<VAR>a : α<VAR>p : G.Walk a a<VAR>hp : p.IsHamiltonianCycle<VAR>b : α<GOAL>b ∈ p.support
<VAR>α : Type u_1<VAR>Fintype α<VAR>DecidableEq α<VAR>G : SimpleGraph α<VAR>a : α<VAR>p : G.Walk a a<VAR>hp : p.IsHamiltonianCycle<GOAL>p.length = Fintype.card α
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>G : SimpleGraph α<VAR>a : α<VAR>p : G.Walk a a<VAR>hp : p.IsHamiltonianCycle<GOAL>List.count a p.support = 2
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>G : SimpleGraph α<VAR>a b : α<VAR>p : G.Walk a a<VAR>hp : p.IsHamiltonianCycle<VAR>h : a ≠ b<GOAL>List.count b p.support = 1
<VAR>α : Type u_1<VAR>Fintype α<VAR>DecidableEq α<VAR>G H : SimpleGraph α<VAR>hGH : G ≤ H<VAR>hG : G.IsHamiltonian<GOAL>H.IsHamiltonian
<VAR>α : Type u_1<VAR>Fintype α<VAR>DecidableEq α<VAR>G : SimpleGraph α<VAR>hG : G.IsHamiltonian<GOAL>G.Connected
<VAR>m n : ℕ<VAR>h : n < m<GOAL>∑ i ∈ Finset.range (n + 1), ↑(n.choose i) * (↑m - ↑n) / ((↑m - ↑i) * ↑(m.choose i)) = 1
<VAR>α : Type u_1<VAR>Fintype α<VAR>Nonempty α<GOAL>∑ s : Finset α, ↑(Fintype.card α) / ((↑(Fintype.card α) - ↑s.card) * ↑((Fintype.card α).choose s.card)) = ↑(Fintype.card α) * ∑ k ∈ Finset.range (Fintype.card α), (↑k)⁻¹ + 1
<VAR>α : Type u_1<VAR>SemilatticeSup α<VAR>DecidableRel fun x x_1 => x ≤ x_1<VAR>s : Finset α<VAR>a : α<GOAL>a ∈ lowerClosure ↑s → (Finset.filter (fun b => a ≤ b) s).Nonempty
<VAR>α : Type u_1<VAR>SemilatticeSup α<VAR>OrderTop α<VAR>DecidableRel fun x x_1 => x ≤ x_1<VAR>s : Finset α<VAR>a : α<VAR>h : a ∈ lowerClosure ↑s<GOAL>s.truncatedSup a = (Finset.filter (fun b => a ≤ b) s).sup' ⋯ id
<VAR>α : Type u_1<VAR>SemilatticeSup α<VAR>OrderTop α<VAR>DecidableRel fun x x_1 => x ≤ x_1<VAR>s : Finset α<VAR>a : α<VAR>h : a ∉ lowerClosure ↑s<GOAL>s.truncatedSup a = ⊤
<VAR>α : Type u_1<VAR>SemilatticeSup α<VAR>OrderTop α<VAR>DecidableRel fun x x_1 => x ≤ x_1<VAR>a : α<GOAL>∅.truncatedSup a = ⊤
<VAR>α : Type u_1<VAR>SemilatticeSup α<VAR>OrderTop α<VAR>DecidableRel fun x x_1 => x ≤ x_1<VAR>b a : α<GOAL>{b}.truncatedSup a = if a ≤ b then b else ⊤
<VAR>α : Type u_1<VAR>SemilatticeSup α<VAR>OrderTop α<VAR>DecidableRel fun x x_1 => x ≤ x_1<VAR>s : Finset α<VAR>a : α<GOAL>a ≤ s.truncatedSup a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>SemilatticeSup α<VAR>OrderTop α<VAR>DecidableRel fun x x_1 => x ≤ x_1<VAR>SemilatticeSup β<VAR>BoundedOrder β<VAR>DecidableRel fun x x_1 => x ≤ x_1<VAR>e : α ≃o β<VAR>s : Finset α<VAR>a : α<GOAL>e (s.truncatedSup a) = (Finset.map e.toEmbedding s).truncatedSup (e a)
<VAR>α : Type u_1<VAR>SemilatticeSup α<VAR>s t : Finset α<VAR>a : α<VAR>DecidableEq α<GOAL>a ∈ lowerClosure ↑(s ∪ t) ↔ a ∈ lowerClosure ↑s ∨ a ∈ lowerClosure ↑t
<VAR>α : Type u_1<VAR>SemilatticeSup α<VAR>OrderTop α<VAR>DecidableRel fun x x_1 => x ≤ x_1<VAR>s t : Finset α<VAR>a : α<VAR>DecidableEq α<VAR>hs : a ∈ lowerClosure ↑s<VAR>ht : a ∈ lowerClosure ↑t<GOAL>(s ∪ t).truncatedSup a = s.truncatedSup a ⊔ t.truncatedSup a
<VAR>α : Type u_1<VAR>SemilatticeSup α<VAR>OrderTop α<VAR>DecidableRel fun x x_1 => x ≤ x_1<VAR>s t : Finset α<VAR>a : α<VAR>DecidableEq α<VAR>hs : a ∈ lowerClosure ↑s<VAR>ht : a ∉ lowerClosure ↑t<GOAL>(s ∪ t).truncatedSup a = s.truncatedSup a
<VAR>α : Type u_1<VAR>SemilatticeSup α<VAR>OrderTop α<VAR>DecidableRel fun x x_1 => x ≤ x_1<VAR>s t : Finset α<VAR>a : α<VAR>DecidableEq α<VAR>hs : a ∉ lowerClosure ↑s<VAR>ht : a ∈ lowerClosure ↑t<GOAL>(s ∪ t).truncatedSup a = t.truncatedSup a
<VAR>α : Type u_1<VAR>SemilatticeSup α<VAR>OrderTop α<VAR>DecidableRel fun x x_1 => x ≤ x_1<VAR>s t : Finset α<VAR>a : α<VAR>DecidableEq α<VAR>hs : a ∉ lowerClosure ↑s<VAR>ht : a ∉ lowerClosure ↑t<GOAL>(s ∪ t).truncatedSup a = ⊤
<VAR>α : Type u_1<VAR>SemilatticeSup α<VAR>OrderTop α<VAR>DecidableRel fun x x_1 => x ≤ x_1<VAR>s : Finset α<VAR>a : α<VAR>hs : IsAntichain (fun x x_1 => x ≤ x_1) ↑s<VAR>ha : a ∈ s<GOAL>s.truncatedSup a = a
<VAR>α : Type u_1<VAR>SemilatticeInf α<VAR>DecidableRel fun x x_1 => x ≤ x_1<VAR>s : Finset α<VAR>a : α<GOAL>a ∈ upperClosure ↑s → (Finset.filter (fun x => x ≤ a) s).Nonempty
<VAR>α : Type u_1<VAR>SemilatticeInf α<VAR>BoundedOrder α<VAR>DecidableRel fun x x_1 => x ≤ x_1<VAR>s : Finset α<VAR>a : α<VAR>h : a ∈ upperClosure ↑s<GOAL>s.truncatedInf a = (Finset.filter (fun x => x ≤ a) s).inf' ⋯ id
<VAR>α : Type u_1<VAR>SemilatticeInf α<VAR>BoundedOrder α<VAR>DecidableRel fun x x_1 => x ≤ x_1<VAR>s : Finset α<VAR>a : α<VAR>h : a ∉ upperClosure ↑s<GOAL>s.truncatedInf a = ⊥
<VAR>α : Type u_1<VAR>SemilatticeInf α<VAR>BoundedOrder α<VAR>DecidableRel fun x x_1 => x ≤ x_1<VAR>s : Finset α<VAR>a : α<GOAL>s.truncatedInf a ≤ a
<VAR>α : Type u_1<VAR>SemilatticeInf α<VAR>BoundedOrder α<VAR>DecidableRel fun x x_1 => x ≤ x_1<VAR>a : α<GOAL>∅.truncatedInf a = ⊥
<VAR>α : Type u_1<VAR>SemilatticeInf α<VAR>BoundedOrder α<VAR>DecidableRel fun x x_1 => x ≤ x_1<VAR>b a : α<GOAL>{b}.truncatedInf a = if b ≤ a then b else ⊥
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>SemilatticeInf α<VAR>BoundedOrder α<VAR>DecidableRel fun x x_1 => x ≤ x_1<VAR>SemilatticeInf β<VAR>BoundedOrder β<VAR>DecidableRel fun x x_1 => x ≤ x_1<VAR>e : α ≃o β<VAR>s : Finset α<VAR>a : α<GOAL>e (s.truncatedInf a) = (Finset.map e.toEmbedding s).truncatedInf (e a)
<VAR>α : Type u_1<VAR>SemilatticeInf α<VAR>s t : Finset α<VAR>a : α<VAR>DecidableEq α<GOAL>a ∈ upperClosure ↑(s ∪ t) ↔ a ∈ upperClosure ↑s ∨ a ∈ upperClosure ↑t
<VAR>α : Type u_1<VAR>SemilatticeInf α<VAR>BoundedOrder α<VAR>DecidableRel fun x x_1 => x ≤ x_1<VAR>s t : Finset α<VAR>a : α<VAR>DecidableEq α<VAR>hs : a ∈ upperClosure ↑s<VAR>ht : a ∈ upperClosure ↑t<GOAL>(s ∪ t).truncatedInf a = s.truncatedInf a ⊓ t.truncatedInf a
<VAR>α : Type u_1<VAR>SemilatticeInf α<VAR>BoundedOrder α<VAR>DecidableRel fun x x_1 => x ≤ x_1<VAR>s t : Finset α<VAR>a : α<VAR>DecidableEq α<VAR>hs : a ∈ upperClosure ↑s<VAR>ht : a ∉ upperClosure ↑t<GOAL>(s ∪ t).truncatedInf a = s.truncatedInf a
<VAR>α : Type u_1<VAR>SemilatticeInf α<VAR>BoundedOrder α<VAR>DecidableRel fun x x_1 => x ≤ x_1<VAR>s t : Finset α<VAR>a : α<VAR>DecidableEq α<VAR>hs : a ∉ upperClosure ↑s<VAR>ht : a ∈ upperClosure ↑t<GOAL>(s ∪ t).truncatedInf a = t.truncatedInf a
<VAR>α : Type u_1<VAR>SemilatticeInf α<VAR>BoundedOrder α<VAR>DecidableRel fun x x_1 => x ≤ x_1<VAR>s t : Finset α<VAR>a : α<VAR>DecidableEq α<VAR>hs : a ∉ upperClosure ↑s<VAR>ht : a ∉ upperClosure ↑t<GOAL>(s ∪ t).truncatedInf a = ⊥
<VAR>α : Type u_1<VAR>SemilatticeInf α<VAR>BoundedOrder α<VAR>DecidableRel fun x x_1 => x ≤ x_1<VAR>s : Finset α<VAR>a : α<VAR>hs : IsAntichain (fun x x_1 => x ≤ x_1) ↑s<VAR>ha : a ∈ s<GOAL>s.truncatedInf a = a
<VAR>α : Type u_1<VAR>DistribLattice α<VAR>DecidableEq α<VAR>s t : Finset α<VAR>a : α<GOAL>a ∈ lowerClosure ↑(s ⊼ t) ↔ a ∈ lowerClosure ↑s ∧ a ∈ lowerClosure ↑t
<VAR>α : Type u_1<VAR>DistribLattice α<VAR>DecidableEq α<VAR>s t : Finset α<VAR>a : α<GOAL>a ∈ upperClosure ↑(s ⊻ t) ↔ a ∈ upperClosure ↑s ∧ a ∈ upperClosure ↑t
<VAR>α : Type u_1<VAR>DistribLattice α<VAR>BoundedOrder α<VAR>DecidableEq α<VAR>DecidableRel fun x x_1 => x ≤ x_1<VAR>s t : Finset α<VAR>a : α<VAR>hs : a ∈ lowerClosure ↑s<VAR>ht : a ∈ lowerClosure ↑t<GOAL>(s ⊼ t).truncatedSup a = s.truncatedSup a ⊓ t.truncatedSup a
<VAR>α : Type u_1<VAR>DistribLattice α<VAR>BoundedOrder α<VAR>DecidableEq α<VAR>DecidableRel fun x x_1 => x ≤ x_1<VAR>s t : Finset α<VAR>a : α<VAR>hs : a ∈ upperClosure ↑s<VAR>ht : a ∈ upperClosure ↑t<GOAL>(s ⊻ t).truncatedInf a = s.truncatedInf a ⊔ t.truncatedInf a
<VAR>α : Type u_1<VAR>DistribLattice α<VAR>BoundedOrder α<VAR>DecidableEq α<VAR>DecidableRel fun x x_1 => x ≤ x_1<VAR>s t : Finset α<VAR>a : α<VAR>ha : a ∉ lowerClosure ↑s ⊓ lowerClosure ↑t<GOAL>(s ⊼ t).truncatedSup a = ⊤
<VAR>α : Type u_1<VAR>DistribLattice α<VAR>BoundedOrder α<VAR>DecidableEq α<VAR>DecidableRel fun x x_1 => x ≤ x_1<VAR>s t : Finset α<VAR>a : α<VAR>ha : a ∉ upperClosure ↑s ⊔ upperClosure ↑t<GOAL>(s ⊻ t).truncatedInf a = ⊥
<VAR>α : Type u_1<VAR>BooleanAlgebra α<VAR>DecidableRel fun x x_1 => x ≤ x_1<VAR>s : Finset α<VAR>a : α<GOAL>(s.truncatedSup a)ᶜ = sᶜˢ.truncatedInf aᶜ
<VAR>α : Type u_1<VAR>BooleanAlgebra α<VAR>DecidableRel fun x x_1 => x ≤ x_1<VAR>s : Finset α<VAR>a : α<GOAL>(s.truncatedInf a)ᶜ = sᶜˢ.truncatedSup aᶜ
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>Fintype α<VAR>𝒜 ℬ : Finset (Finset α)<VAR>s : Finset α<GOAL>((𝒜 ∪ ℬ).truncatedSup s).card + ((𝒜 ⊼ ℬ).truncatedSup s).card = (𝒜.truncatedSup s).card + (ℬ.truncatedSup s).card
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>Fintype α<VAR>𝒜 ℬ : Finset (Finset α)<VAR>s : Finset α<GOAL>((𝒜 ∪ ℬ).truncatedInf s).card + ((𝒜 ⊻ ℬ).truncatedInf s).card = (𝒜.truncatedInf s).card + (ℬ.truncatedInf s).card
<VAR>α : Type u_1<VAR>Fintype α<VAR>DecidableEq α<VAR>𝒜 ℬ : Finset (Finset α)<GOAL>AhlswedeZhang.supSum (𝒜 ∪ ℬ) + AhlswedeZhang.supSum (𝒜 ⊼ ℬ) = AhlswedeZhang.supSum 𝒜 + AhlswedeZhang.supSum ℬ
<VAR>α : Type u_1<VAR>Fintype α<VAR>DecidableEq α<VAR>𝒜 ℬ : Finset (Finset α)<GOAL>AhlswedeZhang.infSum (𝒜 ∪ ℬ) + AhlswedeZhang.infSum (𝒜 ⊻ ℬ) = AhlswedeZhang.infSum 𝒜 + AhlswedeZhang.infSum ℬ
<VAR>α : Type u_1<VAR>Fintype α<VAR>DecidableEq α<VAR>𝒜 : Finset (Finset α)<VAR>h𝒜 : IsAntichain (fun x x_1 => x ⊆ x_1) ↑𝒜<VAR>h𝒜₀ : ∅ ∉ 𝒜<GOAL>∑ s ∈ 𝒜, (↑((Fintype.card α).choose s.card))⁻¹ ≤ AhlswedeZhang.infSum 𝒜
<VAR>α : Type u_1<VAR>Fintype α<VAR>DecidableEq α<VAR>s : Finset α<VAR>Nonempty α<VAR>hs : s ≠ Finset.univ<GOAL>AhlswedeZhang.supSum {s} = ↑(Fintype.card α) * ∑ k ∈ Finset.range (Fintype.card α), (↑k)⁻¹
<VAR>α : Type u_1<VAR>Fintype α<VAR>DecidableEq α<VAR>Nonempty α<VAR>𝒜 : Finset (Finset α)<GOAL>AhlswedeZhang.infSum 𝒜ᶜˢ + AhlswedeZhang.supSum 𝒜 = ↑(Fintype.card α) * ∑ k ∈ Finset.range (Fintype.card α), (↑k)⁻¹ + 1
<VAR>α : Type u_1<VAR>Fintype α<VAR>DecidableEq α<VAR>𝒜 : Finset (Finset α)<VAR>Nonempty α<VAR>h𝒜₁ : 𝒜.Nonempty<VAR>h𝒜₂ : Finset.univ ∉ 𝒜<GOAL>AhlswedeZhang.supSum 𝒜 = ↑(Fintype.card α) * ∑ k ∈ Finset.range (Fintype.card α), (↑k)⁻¹
<VAR>α : Type u_1<VAR>Fintype α<VAR>DecidableEq α<VAR>𝒜 : Finset (Finset α)<VAR>Nonempty α<VAR>h𝒜₁ : 𝒜.Nonempty<VAR>h𝒜₀ : ∅ ∉ 𝒜<GOAL>AhlswedeZhang.infSum 𝒜 = 1
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>Fintype α<VAR>G : SimpleGraph α<VAR>DecidableRel G.Adj<VAR>ε : ℝ<VAR>l : ℕ<VAR>hε : 0 < ε<VAR>hl : l ≤ Fintype.card α<GOAL>∃ P, P.IsEquipartition ∧ l ≤ P.parts.card ∧ P.parts.card ≤ SzemerediRegularity.bound ε l ∧ P.IsUniform G ε
<VAR>V : Type u_1<VAR>G : SimpleGraph V<VAR>DecidableEq V<VAR>u v : V<VAR>p : G.Walk u v<VAR>ht : p.IsTrail<VAR>x : V<GOAL>Even (List.countP (fun e => decide (x ∈ e)) p.edges) ↔ u ≠ v → x ≠ u ∧ x ≠ v
<VAR>V : Type u_1<VAR>G : SimpleGraph V<VAR>DecidableEq V<VAR>u v : V<VAR>p : G.Walk u v<VAR>h : p.IsEulerian<GOAL>p.IsTrail
<VAR>V : Type u_1<VAR>G : SimpleGraph V<VAR>DecidableEq V<VAR>u v : V<VAR>p : G.Walk u v<VAR>h : p.IsEulerian<VAR>e : Sym2 V<GOAL>e ∈ p.edges ↔ e ∈ G.edgeSet
<VAR>V : Type u_1<VAR>G : SimpleGraph V<VAR>DecidableEq V<VAR>u v : V<VAR>p : G.Walk u v<VAR>h : p.IsTrail<VAR>hc : ∀ e ∈ G.edgeSet, e ∈ p.edges<GOAL>p.IsEulerian
<VAR>V : Type u_1<VAR>G : SimpleGraph V<VAR>DecidableEq V<VAR>u v : V<VAR>p : G.Walk u v<GOAL>p.IsEulerian ↔ p.IsTrail ∧ ∀ e ∈ G.edgeSet, e ∈ p.edges
<VAR>V : Type u_1<VAR>G : SimpleGraph V<VAR>DecidableEq V<VAR>Fintype ↑G.edgeSet<VAR>u v : V<VAR>p : G.Walk u v<VAR>h : p.IsEulerian<GOAL>⋯.edgesFinset = G.edgeFinset
<VAR>V : Type u_1<VAR>G : SimpleGraph V<VAR>DecidableEq V<VAR>x u v : V<VAR>p : G.Walk u v<VAR>ht : p.IsEulerian<VAR>Fintype V<VAR>DecidableRel G.Adj<GOAL>Even (G.degree x) ↔ u ≠ v → x ≠ u ∧ x ≠ v
<VAR>V : Type u_1<VAR>G : SimpleGraph V<VAR>DecidableEq V<VAR>Fintype V<VAR>DecidableRel G.Adj<VAR>u v : V<VAR>p : G.Walk u v<VAR>ht : p.IsEulerian<VAR>s : Finset V<VAR>h : s = Finset.filter (fun v => Odd (G.degree v)) Finset.univ<GOAL>s.card = 0 ∨ s.card = 2
<VAR>V : Type u_1<VAR>G : SimpleGraph V<VAR>DecidableEq V<VAR>Fintype V<VAR>DecidableRel G.Adj<VAR>u v : V<VAR>p : G.Walk u v<VAR>ht : p.IsEulerian<GOAL>Fintype.card ↑{v | Odd (G.degree v)} = 0 ∨ Fintype.card ↑{v | Odd (G.degree v)} = 2
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>u v : V<VAR>p : G.Walk u v<VAR>self : p.IsTrail<GOAL>p.edges.Nodup
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>u v : V<VAR>p : G.Walk u v<GOAL>p.IsTrail ↔ p.edges.Nodup
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>u v : V<VAR>p : G.Walk u v<VAR>self : p.IsPath<GOAL>p.support.Nodup
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>u v : V<VAR>p : G.Walk u v<VAR>h : p.IsPath<GOAL>p.IsTrail
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>u : V<VAR>p : G.Walk u u<GOAL>p.IsCircuit ↔ p.IsTrail ∧ p ≠ SimpleGraph.Walk.nil
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>u : V<VAR>p : G.Walk u u<VAR>self : p.IsCircuit<GOAL>p ≠ SimpleGraph.Walk.nil
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>u : V<VAR>p : G.Walk u u<VAR>h : p.IsCircuit<GOAL>p.IsTrail
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>u : V<VAR>p : G.Walk u u<VAR>self : p.IsCycle<GOAL>p.support.tail.Nodup
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>u : V<VAR>p : G.Walk u u<VAR>h : p.IsCycle<GOAL>p.IsCircuit
<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).IsTrail ↔ p.IsTrail
<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.IsPath
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>u v : V<VAR>p : G.Walk u v<GOAL>p.IsPath ↔ p.support.Nodup
<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).IsPath ↔ p.IsPath
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>u u' : V<VAR>p : G.Walk u u<VAR>hu : u = u'<GOAL>(p.copy hu hu).IsCircuit ↔ p.IsCircuit
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>v : V<VAR>p : G.Walk v v<VAR>hp : p.IsCircuit<GOAL>¬p.Nil
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>u : V<VAR>p : G.Walk u u<GOAL>p.IsCycle ↔ p.IsTrail ∧ p ≠ SimpleGraph.Walk.nil ∧ p.support.tail.Nodup
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>u u' : V<VAR>p : G.Walk u u<VAR>hu : u = u'<GOAL>(p.copy hu hu).IsCycle ↔ p.IsCycle
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>v : V<VAR>p : G.Walk v v<VAR>hp : p.IsCycle<GOAL>¬p.Nil
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>u : V<GOAL>SimpleGraph.Walk.nil.IsTrail
<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).IsTrail → p.IsTrail
<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).IsTrail ↔ p.IsTrail ∧ s(u, v) ∉ p.edges
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>u v : V<VAR>p : G.Walk u v<VAR>h : p.IsTrail<GOAL>p.reverse.IsTrail
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>u v : V<VAR>p : G.Walk u v<GOAL>p.reverse.IsTrail ↔ p.IsTrail
<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>h : (p.append q).IsTrail<GOAL>p.IsTrail
<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>h : (p.append q).IsTrail<GOAL>q.IsTrail
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>DecidableEq V<VAR>u v : V<VAR>p : G.Walk u v<VAR>h : p.IsTrail<VAR>e : Sym2 V<GOAL>List.count e p.edges ≤ 1
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>DecidableEq V<VAR>u v : V<VAR>p : G.Walk u v<VAR>h : p.IsTrail<VAR>e : Sym2 V<VAR>he : e ∈ p.edges<GOAL>List.count e p.edges = 1
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>u : V<GOAL>SimpleGraph.Walk.nil.IsPath
<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).IsPath → p.IsPath
<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).IsPath ↔ p.IsPath ∧ u ∉ p.support
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>u v w : V<VAR>p : G.Walk v w<VAR>hp : p.IsPath<VAR>hu : u ∉ p.support<VAR>h : G.Adj u v<GOAL>(SimpleGraph.Walk.cons h p).IsPath
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>u : V<VAR>p : G.Walk u u<GOAL>p.IsPath ↔ p = SimpleGraph.Walk.nil
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>u v : V<VAR>p : G.Walk u v<VAR>h : p.IsPath<GOAL>p.reverse.IsPath
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>u v : V<VAR>p : G.Walk u v<GOAL>p.reverse.IsPath ↔ p.IsPath
<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).IsPath → p.IsPath
<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>h : (p.append q).IsPath<GOAL>q.IsPath
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>u : V<GOAL>¬SimpleGraph.Walk.nil.IsCycle
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>u : V<VAR>p : G.Walk u u<GOAL>p.IsCycle → G ≠ ⊥
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>v : V<VAR>p : G.Walk v v<VAR>hp : p.IsCycle<GOAL>3 ≤ p.length
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>u v : V<VAR>p : G.Walk v u<VAR>h : G.Adj u v<GOAL>(SimpleGraph.Walk.cons h p).IsCycle ↔ p.IsPath ∧ s(u, v) ∉ p.edges
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>u v : V<VAR>p : G.Walk u v<VAR>hp : p.IsPath<VAR>hp' : ¬p.Nil<GOAL>(p.tail hp').IsPath
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>Fintype V<VAR>u v : V<VAR>p : G.Walk u v<VAR>hp : p.IsPath<GOAL>p.length < Fintype.card V
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>DecidableEq V<VAR>u v w : V<VAR>p : G.Walk v w<VAR>hc : p.IsTrail<VAR>h : u ∈ p.support<GOAL>(p.takeUntil u h).IsTrail
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>DecidableEq V<VAR>u v w : V<VAR>p : G.Walk v w<VAR>hc : p.IsTrail<VAR>h : u ∈ p.support<GOAL>(p.dropUntil u h).IsTrail
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>DecidableEq V<VAR>u v w : V<VAR>p : G.Walk v w<VAR>hc : p.IsPath<VAR>h : u ∈ p.support<GOAL>(p.takeUntil u h).IsPath
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>DecidableEq V<VAR>u v w : V<VAR>p : G.Walk v w<VAR>hc : p.IsPath<VAR>h : u ∈ p.support<GOAL>(p.dropUntil u h).IsPath
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>DecidableEq V<VAR>u v : V<VAR>c : G.Walk v v<VAR>hc : c.IsTrail<VAR>h : u ∈ c.support<GOAL>(c.rotate h).IsTrail
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>DecidableEq V<VAR>u v : V<VAR>c : G.Walk v v<VAR>hc : c.IsCircuit<VAR>h : u ∈ c.support<GOAL>(c.rotate h).IsCircuit
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>DecidableEq V<VAR>u v : V<VAR>c : G.Walk v v<VAR>hc : c.IsCycle<VAR>h : u ∈ c.support<GOAL>(c.rotate h).IsCycle
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>u v : V<VAR>p : G.Path u v<GOAL>(↑p).IsPath
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>u v : V<VAR>p : G.Path u v<GOAL>(↑p).IsTrail
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>u : V<GOAL>↑SimpleGraph.Path.nil = SimpleGraph.Walk.nil
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>u v : V<VAR>h : G.Adj u v<GOAL>↑(SimpleGraph.Path.singleton h) = SimpleGraph.Walk.cons h SimpleGraph.Walk.nil
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>u v : V<VAR>h : G.Adj u v<GOAL>s(u, v) ∈ (↑(SimpleGraph.Path.singleton h)).edges
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>u v : V<VAR>p : G.Path u v<GOAL>↑p.reverse = (↑p).reverse
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>DecidableEq V<VAR>u v w : V<VAR>p : G.Path u v<VAR>hw : w ∈ (↑p).support<GOAL>List.count w (↑p).support = 1
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>DecidableEq V<VAR>u v : V<VAR>p : G.Path u v<VAR>e : Sym2 V<VAR>hw : e ∈ (↑p).edges<GOAL>List.count e (↑p).edges = 1
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>u v : V<VAR>p : G.Path u v<GOAL>(↑p).support.Nodup
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>v : V<VAR>p : G.Path v v<GOAL>p = SimpleGraph.Path.nil
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>v : V<VAR>e : Sym2 V<VAR>p : G.Path v v<GOAL>e ∉ (↑p).edges
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>u v : V<VAR>p : G.Path v u<VAR>h : G.Adj u v<VAR>he : s(u, v) ∉ (↑p).edges<GOAL>(SimpleGraph.Walk.cons h ↑p).IsCycle
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>DecidableEq 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).bypass = p.bypass.copy hu hv
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>DecidableEq V<VAR>u v : V<VAR>p : G.Walk u v<GOAL>p.bypass.IsPath