ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>V : Type u_1<VAR>G : SimpleGraph V<VAR>v : V<GOAL>G.dist v v = 0
<VAR>V : Type u_1<VAR>G : SimpleGraph V<VAR>u v : V<VAR>hr : G.Reachable u v<GOAL>G.dist u v = 0 ↔ u = v
<VAR>V : Type u_1<VAR>G : SimpleGraph V<VAR>u v : V<VAR>h : G.Reachable u v<VAR>hne : u ≠ v<GOAL>0 < G.dist u v
<VAR>V : Type u_1<VAR>G : SimpleGraph V<VAR>u v : V<VAR>hconn : G.Connected<GOAL>G.dist u v = 0 ↔ u = v
<VAR>V : Type u_1<VAR>G : SimpleGraph V<VAR>u v : V<VAR>hconn : G.Connected<VAR>hne : u ≠ v<GOAL>0 < G.dist u v
<VAR>V : Type u_1<VAR>G : SimpleGraph V<VAR>u v : V<VAR>h : ¬G.Reachable u v<GOAL>G.dist u v = 0
<VAR>V : Type u_1<VAR>G : SimpleGraph V<VAR>u v : V<VAR>h : 0 < G.dist u v<GOAL>Set.univ.Nonempty
<VAR>V : Type u_1<VAR>G : SimpleGraph V<VAR>u v : V<GOAL>G.dist u v = G.dist v u
<VAR>V : Type u_1<VAR>G : SimpleGraph V<VAR>u v : V<GOAL>G.dist u v ≠ 0 ↔ u ≠ v ∧ G.Reachable u v
<VAR>V : Type u_1<VAR>G : SimpleGraph V<VAR>u v : V<VAR>h : G.dist u v ≠ 0<GOAL>G.Reachable u v
<VAR>V : Type u_1<VAR>G : SimpleGraph V<VAR>u v : V<VAR>h : G.dist u v ≠ 0<GOAL>∃ p, p.length = G.dist u v
<VAR>V : Type u_1<VAR>G : SimpleGraph V<VAR>u v : V<GOAL>G.dist u v = 1 ↔ G.Adj u v
<VAR>V : Type u_1<VAR>G : SimpleGraph V<VAR>u v : V<VAR>p : G.Walk u v<VAR>hp : p.length = G.dist u v<GOAL>p.IsPath
<VAR>V : Type u_1<VAR>G : SimpleGraph V<VAR>u v : V<VAR>hr : G.Reachable u v<GOAL>∃ p, p.IsPath ∧ p.length = G.dist u v
<VAR>V : Type u_1<VAR>G : SimpleGraph V<VAR>hconn : G.Connected<VAR>u v : V<GOAL>∃ p, p.IsPath ∧ p.length = G.dist u v
<VAR>V : Type<VAR>G : SimpleGraph V<VAR>e : ↑G.end<VAR>K : (Finset V)ᵒᵖ<GOAL>(SimpleGraph.ComponentCompl.supp (↑e K)).Infinite
<VAR>V : Type<VAR>G : SimpleGraph V<VAR>G.LocallyFinite<VAR>Fact G.Preconnected<VAR>Infinite V<GOAL>G.end.Nonempty
<VAR>V : Type u<VAR>G : SimpleGraph V<GOAL>↑⊥ = ⊥
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>G₁ G₂ : G.Finsubgraph<GOAL>↑(G₁ ⊔ G₂) = ↑G₁ ⊔ ↑G₂
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>G₁ G₂ : G.Finsubgraph<GOAL>↑(G₁ ⊓ G₂) = ↑G₁ ⊓ ↑G₂
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>G₁ G₂ : G.Finsubgraph<GOAL>↑(G₁ \ G₂) = ↑G₁ \ ↑G₂
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>Finite V<GOAL>↑⊤ = ⊤
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>Finite V<VAR>G' : G.Finsubgraph<GOAL>↑G'ᶜ = (↑G')ᶜ
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>Finite V<VAR>G' : G.Finsubgraph<GOAL>↑(￢G') = ￢↑G'
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>Finite V<VAR>G₁ G₂ : G.Finsubgraph<GOAL>↑(G₁ ⇨ G₂) = ↑G₁ ⇨ ↑G₂
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>Finite V<VAR>s : Set G.Finsubgraph<GOAL>↑(sSup s) = ⨆ G_1 ∈ s, ↑G_1
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>Finite V<VAR>s : Set G.Finsubgraph<GOAL>↑(sInf s) = ⨅ G_1 ∈ s, ↑G_1
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>Finite V<VAR>ι : Sort u_1<VAR>f : ι → G.Finsubgraph<GOAL>↑(⨆ i, f i) = ⨆ i, ↑(f i)
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>Finite V<VAR>ι : Sort u_1<VAR>f : ι → G.Finsubgraph<GOAL>↑(⨅ i, f i) = ⨅ i, ↑(f i)
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>u v : V<VAR>e : G.Adj u v<GOAL>SimpleGraph.singletonFinsubgraph u ≤ SimpleGraph.finsubgraphOfAdj e
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>u v : V<VAR>e : G.Adj u v<GOAL>SimpleGraph.singletonFinsubgraph v ≤ SimpleGraph.finsubgraphOfAdj e
<VAR>V : Type u<VAR>W : Type v<VAR>G : SimpleGraph V<VAR>F : SimpleGraph W<VAR>Finite W<VAR>h : (G' : G.Subgraph) → G'.verts.Finite → G'.coe →g F<GOAL>Nonempty (G →g F)
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>α : Type u_1<VAR>C : G.Coloring α<VAR>v w : V<VAR>h : G.Adj v w<GOAL>C v ≠ C w
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>α : Type u_1<VAR>C : G.Coloring α<VAR>v : V<GOAL>v ∈ C.colorClass (C v)
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>α : Type u_1<VAR>C : G.Coloring α<GOAL>Setoid.IsPartition C.colorClasses
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>α : Type u_1<VAR>C : G.Coloring α<VAR>v : V<GOAL>C.colorClass (C v) ∈ C.colorClasses
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>α : Type u_1<VAR>C : G.Coloring α<VAR>Finite α<GOAL>C.colorClasses.Finite
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>α : Type u_1<VAR>C : G.Coloring α<VAR>Fintype α<VAR>Fintype ↑C.colorClasses<GOAL>Fintype.card ↑C.colorClasses ≤ Fintype.card α
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>α : Type u_1<VAR>C : G.Coloring α<VAR>c : α<VAR>v w : V<VAR>hv : v ∈ C.colorClass c<VAR>hw : w ∈ C.colorClass c<GOAL>¬G.Adj v w
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>α : Type u_1<VAR>C : G.Coloring α<VAR>c : α<GOAL>IsAntichain G.Adj (C.colorClass c)
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>IsEmpty V<VAR>n : ℕ<GOAL>G.Colorable n
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>h : G.Colorable 0<GOAL>IsEmpty V
<VAR>V : Type u<VAR>G : SimpleGraph V<GOAL>G.chromaticNumber = ⨅ n ∈ setOf G.Colorable, ↑n
<VAR>V : Type u<VAR>G : SimpleGraph V<GOAL>G.chromaticNumber = ⨅ n, ↑↑n
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>n : ℕ<VAR>h : G.Colorable n<GOAL>G.chromaticNumber = ↑(sInf {n' | G.Colorable n'})
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α ↪ β<GOAL>⇑(G.recolorOfEmbedding f) = (SimpleGraph.Embedding.completeGraph f).toHom.comp
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α ≃ β<GOAL>⇑(G.recolorOfEquiv f) = (SimpleGraph.Embedding.completeGraph f.toEmbedding).toHom.comp
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Fintype α<VAR>Fintype β<VAR>hαβ : Fintype.card α ≤ Fintype.card β<GOAL>⇑(G.recolorOfCardLE hαβ) = (SimpleGraph.Embedding.completeGraph ⋯.some).toHom.comp
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>n m : ℕ<VAR>h : n ≤ m<VAR>hc : G.Colorable n<GOAL>G.Colorable m
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>α : Type u_1<VAR>Fintype α<VAR>C : G.Coloring α<GOAL>G.Colorable (Fintype.card α)
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>Fintype V<GOAL>G.Colorable (Fintype.card V)
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>V' : Type u_3<VAR>G' : SimpleGraph V'<VAR>f : G ↪g G'<VAR>n : ℕ<VAR>h : G'.Colorable n<GOAL>G.Colorable n
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>n : ℕ<GOAL>G.Colorable n ↔ ∃ C, ∀ (v : V), C v < n
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>n : ℕ<VAR>hc : G.Colorable n<GOAL>{n | G.Colorable n}.Nonempty
<VAR>V : Type u<VAR>G : SimpleGraph V<GOAL>BddBelow {n | G.Colorable n}
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>n : ℕ<VAR>hc : G.Colorable n<GOAL>G.chromaticNumber ≤ ↑n
<VAR>V : Type u<VAR>G : SimpleGraph V<GOAL>G.chromaticNumber ≠ ⊤ ↔ ∃ n, G.Colorable n
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>n : ℕ<GOAL>G.chromaticNumber ≤ ↑n ↔ G.Colorable n
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>α : Type u_1<VAR>Fintype α<VAR>C : G.Coloring α<GOAL>G.chromaticNumber ≤ ↑(Fintype.card α)
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>m : ℕ<VAR>hc : G.Colorable m<GOAL>G.Colorable G.chromaticNumber.toNat
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>Finite V<GOAL>G.Colorable G.chromaticNumber.toNat
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>Subsingleton V<GOAL>G.chromaticNumber ≤ 1
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>IsEmpty V<GOAL>G.chromaticNumber = 0
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>Finite V<VAR>h : G.chromaticNumber = 0<GOAL>IsEmpty V
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>Nonempty V<VAR>n : ℕ<VAR>hc : G.Colorable n<GOAL>0 < G.chromaticNumber
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>h : G.chromaticNumber ≠ ⊤<GOAL>G.Colorable G.chromaticNumber.toNat
<VAR>V : Type u<VAR>G G' : SimpleGraph V<VAR>h : G ≤ G'<VAR>n : ℕ<VAR>hc : G'.Colorable n<GOAL>G.Colorable n
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>V' : Type u_3<VAR>G' : SimpleGraph V'<VAR>h : ∀ (n : ℕ), G'.Colorable n → G.Colorable n<GOAL>G.chromaticNumber ≤ G'.chromaticNumber
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph V<VAR>h : G ≤ G'<GOAL>G.chromaticNumber ≤ G'.chromaticNumber
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>V' : Type u_3<VAR>G' : SimpleGraph V'<VAR>f : G ↪g G'<GOAL>G.chromaticNumber ≤ G'.chromaticNumber
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>α : Type u_1<VAR>Fintype α<GOAL>↑(Fintype.card α) ≤ G.chromaticNumber ↔ ∀ (C : G.Coloring α), Function.Surjective ⇑C
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>n : ℕ<GOAL>↑n ≤ G.chromaticNumber ↔ ∀ (C : G.Coloring (Fin n)), Function.Surjective ⇑C
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>α : Type u_1<VAR>Fintype α<VAR>hG : G.Colorable (Fintype.card α)<GOAL>G.chromaticNumber = ↑(Fintype.card α) ↔ ∀ (C : G.Coloring α), Function.Surjective ⇑C
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>n : ℕ<VAR>hG : G.Colorable n<GOAL>G.chromaticNumber = ↑n ↔ ∀ (C : G.Coloring (Fin n)), Function.Surjective ⇑C
<VAR>V : Type u<VAR>Nonempty V<GOAL>⊥.chromaticNumber = 1
<VAR>V : Type u<VAR>Fintype V<GOAL>⊤.chromaticNumber = ↑(Fintype.card V)
<VAR>V : Type u_3<VAR>Infinite V<GOAL>⊤.chromaticNumber = ⊤
<VAR>V : Type u_3<VAR>W : Type u_4<VAR>Nonempty V<VAR>Nonempty W<GOAL>(completeBipartiteGraph V W).chromaticNumber = 2
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>α : Type u_1<VAR>s : Finset V<VAR>h : G.IsClique ↑s<VAR>Fintype α<VAR>C : G.Coloring α<GOAL>s.card ≤ Fintype.card α
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>s : Finset V<VAR>h : G.IsClique ↑s<VAR>n : ℕ<VAR>hc : G.Colorable n<GOAL>s.card ≤ n
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>s : Finset V<VAR>h : G.IsClique ↑s<GOAL>↑s.card ≤ G.chromaticNumber
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>n m : ℕ<VAR>hc : G.Colorable n<VAR>hm : n < m<GOAL>G.CliqueFree m
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>n : ℕ<VAR>hc : G.chromaticNumber < ↑n<GOAL>G.CliqueFree n
<VAR>V : Type u<VAR>Fintype V<VAR>G : SimpleGraph V<VAR>DecidableRel G.Adj<VAR>n k ℓ μ : ℕ<VAR>self : G.IsSRGWith n k ℓ μ<GOAL>Fintype.card V = n
<VAR>V : Type u<VAR>Fintype V<VAR>G : SimpleGraph V<VAR>DecidableRel G.Adj<VAR>n k ℓ μ : ℕ<VAR>self : G.IsSRGWith n k ℓ μ<VAR>v w : V<GOAL>G.Adj v w → Fintype.card ↑(G.commonNeighbors v w) = ℓ
<VAR>V : Type u<VAR>Fintype V<VAR>G : SimpleGraph V<VAR>DecidableRel G.Adj<VAR>n k ℓ μ : ℕ<VAR>self : G.IsSRGWith n k ℓ μ<GOAL>Pairwise fun v w => ¬G.Adj v w → Fintype.card ↑(G.commonNeighbors v w) = μ
<VAR>V : Type u<VAR>Fintype V<VAR>G : SimpleGraph V<VAR>DecidableRel G.Adj<VAR>n k ℓ μ : ℕ<VAR>self : G.IsSRGWith n k ℓ μ<GOAL>G.IsRegularOfDegree k
<VAR>V : Type u<VAR>Fintype V<VAR>ℓ : ℕ<GOAL>⊥.IsSRGWith (Fintype.card V) 0 ℓ 0
<VAR>V : Type u<VAR>Fintype V<VAR>DecidableEq V<VAR>μ : ℕ<GOAL>⊤.IsSRGWith (Fintype.card V) (Fintype.card V - 1) (Fintype.card V - 2) μ
<VAR>V : Type u<VAR>Fintype V<VAR>DecidableEq V<VAR>G : SimpleGraph V<VAR>DecidableRel G.Adj<VAR>n k ℓ μ : ℕ<VAR>v w : V<VAR>h : G.IsSRGWith n k ℓ μ<GOAL>(G.neighborFinset v ∪ G.neighborFinset w).card = 2 * k - Fintype.card ↑(G.commonNeighbors v w)
<VAR>V : Type u<VAR>Fintype V<VAR>DecidableEq V<VAR>G : SimpleGraph V<VAR>DecidableRel G.Adj<VAR>n k ℓ μ : ℕ<VAR>v w : V<VAR>h : G.IsSRGWith n k ℓ μ<VAR>hne : v ≠ w<VAR>ha : ¬G.Adj v w<GOAL>(G.neighborFinset v ∪ G.neighborFinset w).card = 2 * k - μ
<VAR>V : Type u<VAR>Fintype V<VAR>DecidableEq V<VAR>G : SimpleGraph V<VAR>DecidableRel G.Adj<VAR>n k ℓ μ : ℕ<VAR>v w : V<VAR>h : G.IsSRGWith n k ℓ μ<VAR>ha : G.Adj v w<GOAL>(G.neighborFinset v ∪ G.neighborFinset w).card = 2 * k - ℓ
<VAR>V : Type u<VAR>Fintype V<VAR>DecidableEq V<VAR>G : SimpleGraph V<VAR>DecidableRel G.Adj<VAR>v w : V<GOAL>(G.neighborFinset v)ᶜ \ {v} ∩ ((G.neighborFinset w)ᶜ \ {w}) = ((G.neighborFinset v)ᶜ ∩ (G.neighborFinset w)ᶜ) \ ({w} ∪ {v})
<VAR>V : Type u<VAR>Fintype V<VAR>DecidableEq V<VAR>G : SimpleGraph V<VAR>DecidableRel G.Adj<VAR>v w : V<VAR>h : G.Adj v w<GOAL>((G.neighborFinset v)ᶜ ∩ (G.neighborFinset w)ᶜ) \ ({w} ∪ {v}) = (G.neighborFinset v)ᶜ ∩ (G.neighborFinset w)ᶜ
<VAR>V : Type u<VAR>Fintype V<VAR>DecidableEq V<VAR>G : SimpleGraph V<VAR>DecidableRel G.Adj<VAR>n k ℓ μ : ℕ<VAR>h : G.IsSRGWith n k ℓ μ<GOAL>Gᶜ.IsRegularOfDegree (n - k - 1)
<VAR>V : Type u<VAR>Fintype V<VAR>DecidableEq V<VAR>G : SimpleGraph V<VAR>DecidableRel G.Adj<VAR>n k ℓ μ : ℕ<VAR>h : G.IsSRGWith n k ℓ μ<VAR>v w : V<VAR>ha : Gᶜ.Adj v w<GOAL>Fintype.card ↑(Gᶜ.commonNeighbors v w) = n - (2 * k - μ) - 2
<VAR>V : Type u<VAR>Fintype V<VAR>DecidableEq V<VAR>G : SimpleGraph V<VAR>DecidableRel G.Adj<VAR>n k ℓ μ : ℕ<VAR>h : G.IsSRGWith n k ℓ μ<VAR>v w : V<VAR>hn : v ≠ w<VAR>hna : ¬Gᶜ.Adj v w<GOAL>Fintype.card ↑(Gᶜ.commonNeighbors v w) = n - (2 * k - ℓ)
<VAR>V : Type u<VAR>Fintype V<VAR>DecidableEq V<VAR>G : SimpleGraph V<VAR>DecidableRel G.Adj<VAR>n k ℓ μ : ℕ<VAR>h : G.IsSRGWith n k ℓ μ<GOAL>Gᶜ.IsSRGWith n (n - k - 1) (n - (2 * k - μ) - 2) (n - (2 * k - ℓ))
<VAR>V : Type u<VAR>Fintype V<VAR>G : SimpleGraph V<VAR>DecidableRel G.Adj<VAR>n k ℓ μ : ℕ<VAR>h : G.IsSRGWith n k ℓ μ<VAR>hn : 0 < n<GOAL>k * (k - ℓ - 1) = (n - k - 1) * μ
<VAR>V : Type u<VAR>Fintype V<VAR>DecidableEq V<VAR>G : SimpleGraph V<VAR>DecidableRel G.Adj<VAR>n k ℓ μ : ℕ<VAR>α : Type u_1<VAR>Semiring α<VAR>h : G.IsSRGWith n k ℓ μ<GOAL>SimpleGraph.adjMatrix α G ^ 2 = k • 1 + ℓ • SimpleGraph.adjMatrix α G + μ • SimpleGraph.adjMatrix α Gᶜ
<VAR>α : Type u_1<VAR>G : SimpleGraph α<VAR>s : Set α<GOAL>G.IsClique s ↔ s.Pairwise G.Adj
<VAR>α : Type u_1<VAR>G : SimpleGraph α<VAR>s : Set α<GOAL>G.IsClique s ↔ SimpleGraph.induce s G = ⊤
<VAR>α : Type u_1<VAR>G : SimpleGraph α<GOAL>G.IsClique ∅
<VAR>α : Type u_1<VAR>G : SimpleGraph α<VAR>a : α<GOAL>G.IsClique {a}
<VAR>α : Type u_1<VAR>s : Set α<VAR>G : SimpleGraph α<VAR>hs : s.Subsingleton<GOAL>G.IsClique s
<VAR>α : Type u_1<VAR>G : SimpleGraph α<VAR>a b : α<GOAL>G.IsClique {a, b} ↔ a ≠ b → G.Adj a b
<VAR>α : Type u_1<VAR>G : SimpleGraph α<VAR>s : Set α<VAR>a : α<GOAL>G.IsClique (insert a s) ↔ G.IsClique s ∧ ∀ b ∈ s, a ≠ b → G.Adj a b
<VAR>α : Type u_1<VAR>G : SimpleGraph α<VAR>s : Set α<VAR>a : α<VAR>ha : a ∉ s<GOAL>G.IsClique (insert a s) ↔ G.IsClique s ∧ ∀ b ∈ s, G.Adj a b
<VAR>α : Type u_1<VAR>G : SimpleGraph α<VAR>s : Set α<VAR>a : α<VAR>hs : G.IsClique s<VAR>h : ∀ b ∈ s, a ≠ b → G.Adj a b<GOAL>G.IsClique (insert a s)
<VAR>α : Type u_1<VAR>G H : SimpleGraph α<VAR>s : Set α<VAR>h : G ≤ H<GOAL>G.IsClique s → H.IsClique s
<VAR>α : Type u_1<VAR>G : SimpleGraph α<VAR>s t : Set α<VAR>h : t ⊆ s<GOAL>G.IsClique s → G.IsClique t
<VAR>α : Type u_1<VAR>s : Set α<GOAL>⊥.IsClique s ↔ s.Subsingleton
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G : SimpleGraph α<VAR>s : Set α<VAR>h : G.IsClique s<VAR>f : α ↪ β<GOAL>(SimpleGraph.map f G).IsClique (⇑f '' s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G : SimpleGraph α<VAR>f : α ↪ β<VAR>t : Set β<VAR>ht : t.Nontrivial<GOAL>(SimpleGraph.map f G).IsClique t ↔ ∃ s, G.IsClique s ∧ ⇑f '' s = t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G : SimpleGraph α<VAR>f : α ↪ β<VAR>t : Set β<GOAL>(SimpleGraph.map f G).IsClique t ↔ t.Subsingleton ∨ ∃ s, G.IsClique s ∧ ⇑f '' s = t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G : SimpleGraph α<VAR>s : Set α<VAR>f : α ↪ β<GOAL>(SimpleGraph.map f G).IsClique (⇑f '' s) ↔ G.IsClique s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G : SimpleGraph α<VAR>f : α ↪ β<VAR>t : Finset β<VAR>ht : t.Nontrivial<GOAL>(SimpleGraph.map f G).IsClique ↑t ↔ ∃ s, G.IsClique ↑s ∧ Finset.map f s = t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G : SimpleGraph α<VAR>f : α ↪ β<VAR>t : Finset β<GOAL>(SimpleGraph.map f G).IsClique ↑t ↔ t.card ≤ 1 ∨ ∃ s, G.IsClique ↑s ∧ Finset.map f s = t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G : SimpleGraph α<VAR>f : α ↪ β<VAR>s : Finset α<VAR>h : G.IsClique ↑s<GOAL>(SimpleGraph.map f G).IsClique ↑(Finset.map f s)
<VAR>α : Type u_1<VAR>G : SimpleGraph α<VAR>n : ℕ<VAR>s : Finset α<VAR>self : G.IsNClique n s<GOAL>G.IsClique ↑s
<VAR>α : Type u_1<VAR>G : SimpleGraph α<VAR>n : ℕ<VAR>s : Finset α<VAR>self : G.IsNClique n s<GOAL>s.card = n
<VAR>α : Type u_1<VAR>G : SimpleGraph α<VAR>n : ℕ<VAR>s : Finset α<GOAL>G.IsNClique n s ↔ G.IsClique ↑s ∧ s.card = n
<VAR>α : Type u_1<VAR>G : SimpleGraph α<VAR>n : ℕ<GOAL>G.IsNClique n ∅ ↔ n = 0
<VAR>α : Type u_1<VAR>G : SimpleGraph α<VAR>n : ℕ<VAR>a : α<GOAL>G.IsNClique n {a} ↔ n = 1
<VAR>α : Type u_1<VAR>G H : SimpleGraph α<VAR>n : ℕ<VAR>s : Finset α<VAR>h : G ≤ H<GOAL>G.IsNClique n s → H.IsNClique n s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G : SimpleGraph α<VAR>n : ℕ<VAR>s : Finset α<VAR>h : G.IsNClique n s<VAR>f : α ↪ β<GOAL>(SimpleGraph.map f G).IsNClique n (Finset.map f s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G : SimpleGraph α<VAR>n : ℕ<VAR>hn : 1 < n<VAR>t : Finset β<VAR>f : α ↪ β<GOAL>(SimpleGraph.map f G).IsNClique n t ↔ ∃ s, G.IsNClique n s ∧ Finset.map f s = t
<VAR>α : Type u_1<VAR>n : ℕ<VAR>s : Finset α<GOAL>⊥.IsNClique n s ↔ n ≤ 1 ∧ s.card = n
<VAR>α : Type u_1<VAR>G : SimpleGraph α<VAR>s : Finset α<GOAL>G.IsNClique 0 s ↔ s = ∅
<VAR>α : Type u_1<VAR>G : SimpleGraph α<VAR>s : Finset α<GOAL>G.IsNClique 1 s ↔ ∃ a, s = {a}
<VAR>α : Type u_1<VAR>G : SimpleGraph α<VAR>n : ℕ<VAR>s : Finset α<VAR>a : α<VAR>DecidableEq α<VAR>hs : G.IsNClique n s<VAR>h : ∀ b ∈ s, G.Adj a b<GOAL>G.IsNClique (n + 1) (insert a s)
<VAR>α : Type u_1<VAR>G : SimpleGraph α<VAR>a b c : α<VAR>DecidableEq α<GOAL>G.IsNClique 3 {a, b, c} ↔ G.Adj a b ∧ G.Adj a c ∧ G.Adj b c
<VAR>α : Type u_1<VAR>G : SimpleGraph α<VAR>s : Finset α<VAR>DecidableEq α<GOAL>G.IsNClique 3 s ↔ ∃ a b c, G.Adj a b ∧ G.Adj a c ∧ G.Adj b c ∧ s = {a, b, c}
<VAR>α : Type u_1<VAR>G : SimpleGraph α<GOAL>(∃ s, G.IsNClique 3 s) ↔ ∃ u w, w.IsCycle ∧ w.length = 3
<VAR>α : Type u_1<VAR>G : SimpleGraph α<VAR>n : ℕ<VAR>s : Finset α<VAR>hG : G.IsNClique n s<GOAL>¬G.CliqueFree n
<VAR>α : Type u_1<VAR>G : SimpleGraph α<VAR>n : ℕ<VAR>f : ⊤ ↪g G<GOAL>¬G.CliqueFree n
<VAR>α : Type u_1<VAR>G : SimpleGraph α<VAR>n : ℕ<GOAL>¬G.CliqueFree n ↔ Nonempty (⊤ ↪g G)
<VAR>α : Type u_1<VAR>G : SimpleGraph α<VAR>n : ℕ<GOAL>G.CliqueFree n ↔ IsEmpty (⊤ ↪g G)
<VAR>α : Type u_1<VAR>G : SimpleGraph α<VAR>Fintype α<VAR>f : ⊤ ↪g G<GOAL>¬G.CliqueFree (Fintype.card α)
<VAR>α : Type u_1<VAR>n : ℕ<VAR>h : 2 ≤ n<GOAL>⊥.CliqueFree n
<VAR>α : Type u_1<VAR>G : SimpleGraph α<VAR>m n : ℕ<VAR>h : m ≤ n<GOAL>G.CliqueFree m → G.CliqueFree n
<VAR>α : Type u_1<VAR>G H : SimpleGraph α<VAR>n : ℕ<VAR>h : G ≤ H<GOAL>H.CliqueFree n → G.CliqueFree n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G : SimpleGraph α<VAR>n : ℕ<VAR>H : SimpleGraph β<VAR>f : H ↪g G<GOAL>G.CliqueFree n → H.CliqueFree n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G : SimpleGraph α<VAR>n : ℕ<VAR>f : α ↪ β<VAR>Nonempty α<GOAL>(SimpleGraph.map f G).CliqueFree n ↔ G.CliqueFree n
<VAR>α : Type u_1<VAR>G : SimpleGraph α<VAR>n : ℕ<VAR>Fintype α<VAR>hc : Fintype.card α < n<GOAL>G.CliqueFree n
<VAR>n : ℕ<VAR>ι : Type u_3<VAR>Fintype ι<VAR>V : ι → Type u_4<VAR>hc : Fintype.card ι < n<GOAL>(SimpleGraph.completeMultipartiteGraph V).CliqueFree n
<VAR>α : Type u_1<VAR>G : SimpleGraph α<VAR>n : ℕ<VAR>DecidableEq α<VAR>h : G.CliqueFree n<VAR>s t : α<GOAL>(G.replaceVertex s t).CliqueFree n
<VAR>α : Type u_1<VAR>G : SimpleGraph α<GOAL>G.CliqueFree 2 ↔ G = ⊥
<VAR>α : Type u_1<VAR>G : SimpleGraph α<VAR>n : ℕ<VAR>h : G.CliqueFree n<VAR>v w : α<GOAL>(G ⊔ SimpleGraph.edge v w).CliqueFree (n + 1)
<VAR>α : Type u_1<VAR>G : SimpleGraph α<VAR>s₁ s₂ : Set α<VAR>n : ℕ<VAR>hs : s₁ ⊆ s₂<VAR>h₂ : G.CliqueFreeOn s₂ n<GOAL>G.CliqueFreeOn s₁ n
<VAR>α : Type u_1<VAR>G : SimpleGraph α<VAR>s : Set α<VAR>m n : ℕ<VAR>hmn : m ≤ n<VAR>hG : G.CliqueFreeOn s m<GOAL>G.CliqueFreeOn s n
<VAR>α : Type u_1<VAR>G H : SimpleGraph α<VAR>s : Set α<VAR>n : ℕ<VAR>hGH : G ≤ H<VAR>hH : H.CliqueFreeOn s n<GOAL>G.CliqueFreeOn s n
<VAR>α : Type u_1<VAR>G : SimpleGraph α<VAR>n : ℕ<GOAL>G.CliqueFreeOn ∅ n ↔ n ≠ 0
<VAR>α : Type u_1<VAR>G : SimpleGraph α<VAR>a : α<VAR>n : ℕ<GOAL>G.CliqueFreeOn {a} n ↔ 1 < n
<VAR>α : Type u_1<VAR>G : SimpleGraph α<VAR>n : ℕ<GOAL>G.CliqueFreeOn Set.univ n ↔ G.CliqueFree n
<VAR>α : Type u_1<VAR>G : SimpleGraph α<VAR>s : Set α<VAR>n : ℕ<VAR>hG : G.CliqueFree n<GOAL>G.CliqueFreeOn s n
<VAR>α : Type u_1<VAR>G : SimpleGraph α<VAR>n : ℕ<VAR>s : Finset α<VAR>h : s.card < n<GOAL>G.CliqueFreeOn (↑s) n
<VAR>α : Type u_1<VAR>G : SimpleGraph α<VAR>s : Set α<GOAL>G.CliqueFreeOn s 2 ↔ s.Pairwise G.Adjᶜ
<VAR>α : Type u_1<VAR>G : SimpleGraph α<VAR>s : Set α<VAR>a : α<VAR>n : ℕ<VAR>hs : G.CliqueFreeOn s (n + 1)<VAR>ha : a ∈ s<GOAL>G.CliqueFreeOn (s ∩ G.neighborSet a) n
<VAR>α : Type u_1<VAR>G : SimpleGraph α<VAR>n : ℕ<VAR>s : Finset α<GOAL>s ∈ G.cliqueSet n ↔ G.IsNClique n s
<VAR>α : Type u_1<VAR>G : SimpleGraph α<VAR>n : ℕ<GOAL>G.cliqueSet n = ∅ ↔ G.CliqueFree n
<VAR>α : Type u_1<VAR>G H : SimpleGraph α<VAR>n : ℕ<VAR>h : G ≤ H<GOAL>G.cliqueSet n ⊆ H.cliqueSet n
<VAR>α : Type u_1<VAR>G H : SimpleGraph α<VAR>h : G ≤ H<GOAL>G.cliqueSet ≤ H.cliqueSet
<VAR>α : Type u_1<VAR>G : SimpleGraph α<GOAL>G.cliqueSet 0 = {∅}
<VAR>α : Type u_1<VAR>G : SimpleGraph α<GOAL>G.cliqueSet 1 = Set.range singleton
<VAR>α : Type u_1<VAR>n : ℕ<VAR>hn : 1 < n<GOAL>⊥.cliqueSet n = ∅
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>n : ℕ<VAR>hn : n ≠ 1<VAR>G : SimpleGraph α<VAR>f : α ↪ β<GOAL>(SimpleGraph.map f G).cliqueSet n = Finset.map f '' G.cliqueSet n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G : SimpleGraph α<VAR>e : α ≃ β<VAR>n : ℕ<GOAL>(SimpleGraph.map e.toEmbedding G).cliqueSet n = Finset.map e.toEmbedding '' G.cliqueSet n
<VAR>α : Type u_1<VAR>G : SimpleGraph α<VAR>Fintype α<VAR>DecidableEq α<VAR>DecidableRel G.Adj<VAR>n : ℕ<VAR>s : Finset α<GOAL>s ∈ G.cliqueFinset n ↔ G.IsNClique n s
<VAR>α : Type u_1<VAR>G : SimpleGraph α<VAR>Fintype α<VAR>DecidableEq α<VAR>DecidableRel G.Adj<VAR>n : ℕ<GOAL>↑(G.cliqueFinset n) = G.cliqueSet n
<VAR>α : Type u_1<VAR>G : SimpleGraph α<VAR>Fintype α<VAR>DecidableEq α<VAR>DecidableRel G.Adj<VAR>n : ℕ<GOAL>G.cliqueFinset n = ∅ ↔ G.CliqueFree n
<VAR>α : Type u_1<VAR>G : SimpleGraph α<VAR>Fintype α<VAR>DecidableEq α<VAR>DecidableRel G.Adj<VAR>n : ℕ<GOAL>(G.cliqueFinset n).card ≤ (Fintype.card α).choose n
<VAR>α : Type u_1<VAR>G : SimpleGraph α<VAR>H : SimpleGraph α<VAR>Fintype α<VAR>DecidableEq α<VAR>DecidableRel G.Adj<VAR>n : ℕ<VAR>DecidableRel H.Adj<VAR>h : G ≤ H<GOAL>G.cliqueFinset n ⊆ H.cliqueFinset n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G : SimpleGraph α<VAR>Fintype α<VAR>DecidableEq α<VAR>DecidableRel G.Adj<VAR>n : ℕ<VAR>Fintype β<VAR>DecidableEq β<VAR>f : α ↪ β<VAR>hn : n ≠ 1<GOAL>(SimpleGraph.map f G).cliqueFinset n = Finset.map { toFun := Finset.map f, inj' := ⋯ } (G.cliqueFinset n)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G : SimpleGraph α<VAR>Fintype α<VAR>DecidableEq α<VAR>DecidableRel G.Adj<VAR>Fintype β<VAR>DecidableEq β<VAR>e : α ≃ β<VAR>n : ℕ<GOAL>(SimpleGraph.map e.toEmbedding G).cliqueFinset n = Finset.map { toFun := Finset.map e.toEmbedding, inj' := ⋯ } (G.cliqueFinset n)
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>u : V<GOAL>{p | p.length = 0} = {SimpleGraph.Walk.nil}
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>u v : V<VAR>h : u ≠ v<GOAL>{p | p.length = 0} = ∅
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>u v : V<VAR>n : ℕ<GOAL>{p | p.length = n.succ} = ⋃ w, ⋃ (h : G.Adj u w), SimpleGraph.Walk.cons h '' {p' | p'.length = n}
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>u v : V<VAR>p : { p // p.length = 2 }<GOAL>↑((G.walkLengthTwoEquivCommonNeighbors u v) p) = (↑p).getVert 1
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>u v : V<VAR>w : ↑(G.commonNeighbors u v)<GOAL>↑((G.walkLengthTwoEquivCommonNeighbors u v).symm w) = (SimpleGraph.Adj.toWalk ⋯).concat ⋯
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>DecidableEq V<VAR>G.LocallyFinite<VAR>n : ℕ<VAR>u v : V<GOAL>↑(G.finsetWalkLength n u v) = {p | p.length = n}
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>DecidableEq V<VAR>G.LocallyFinite<VAR>n : ℕ<VAR>u v : V<VAR>p : G.Walk u v<GOAL>p ∈ G.finsetWalkLength n u v ↔ p.length = n
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>DecidableEq V<VAR>G.LocallyFinite<VAR>n : ℕ<VAR>u v : V<GOAL>{p | p.length = n}.toFinset = G.finsetWalkLength n u v
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>DecidableEq V<VAR>G.LocallyFinite<VAR>u v : V<VAR>n : ℕ<GOAL>Fintype.card ↑{p | p.length = n} = (G.finsetWalkLength n u v).card
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>DecidableEq V<VAR>Fintype V<VAR>DecidableRel G.Adj<VAR>u v : V<GOAL>G.Reachable u v ↔ ∃ n, (G.finsetWalkLength (↑n) u v).Nonempty
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>DecidableEq V<VAR>Fintype V<VAR>DecidableRel G.Adj<GOAL>Odd (Nat.card V) ↔ Odd (Nat.card ↑{c | Odd (Nat.card ↑c.supp)})
<VAR>V : Type u<VAR>G : SimpleGraph V<GOAL>G.IsTree ↔ G.Connected ∧ G.IsAcyclic
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>self : G.IsTree<GOAL>G.Connected
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>self : G.IsTree<GOAL>G.IsAcyclic
<VAR>V : Type u<GOAL>⊥.IsAcyclic
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>h : G.IsAcyclic<VAR>v w : V<VAR>p q : G.Path v w<GOAL>p = q
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>h : ∀ (v w : V) (p q : G.Path v w), p = q<GOAL>G.IsAcyclic
<VAR>V : Type u<VAR>G : SimpleGraph V<GOAL>G.IsAcyclic ↔ ∀ ⦃v w : V⦄ (p q : G.Path v w), p = q