ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>V : Type u_1<VAR>α : Type u_2<VAR>G : SimpleGraph V<VAR>DecidableRel G.Adj<VAR>Fintype V<VAR>NonAssocSemiring α<VAR>v : V<VAR>vec : V → α<GOAL>SimpleGraph.adjMatrix α G v ⬝ᵥ vec = ∑ u ∈ G.neighborFinset v, vec u
<VAR>V : Type u_1<VAR>α : Type u_2<VAR>G : SimpleGraph V<VAR>DecidableRel G.Adj<VAR>Fintype V<VAR>NonAssocSemiring α<VAR>v : V<VAR>vec : V → α<GOAL>vec ⬝ᵥ SimpleGraph.adjMatrix α G v = ∑ u ∈ G.neighborFinset v, vec u
<VAR>V : Type u_1<VAR>α : Type u_2<VAR>G : SimpleGraph V<VAR>DecidableRel G.Adj<VAR>Fintype V<VAR>NonAssocSemiring α<VAR>v : V<VAR>vec : V → α<GOAL>(SimpleGraph.adjMatrix α G *ᵥ vec) v = ∑ u ∈ G.neighborFinset v, vec u
<VAR>V : Type u_1<VAR>α : Type u_2<VAR>G : SimpleGraph V<VAR>DecidableRel G.Adj<VAR>Fintype V<VAR>NonAssocSemiring α<VAR>v : V<VAR>vec : V → α<GOAL>(vec ᵥ* SimpleGraph.adjMatrix α G) v = ∑ u ∈ G.neighborFinset v, vec u
<VAR>V : Type u_1<VAR>α : Type u_2<VAR>G : SimpleGraph V<VAR>DecidableRel G.Adj<VAR>Fintype V<VAR>NonAssocSemiring α<VAR>M : Matrix V V α<VAR>v w : V<GOAL>(SimpleGraph.adjMatrix α G * M) v w = ∑ u ∈ G.neighborFinset v, M u w
<VAR>V : Type u_1<VAR>α : Type u_2<VAR>G : SimpleGraph V<VAR>DecidableRel G.Adj<VAR>Fintype V<VAR>NonAssocSemiring α<VAR>M : Matrix V V α<VAR>v w : V<GOAL>(M * SimpleGraph.adjMatrix α G) v w = ∑ u ∈ G.neighborFinset w, M v u
<VAR>V : Type u_1<VAR>α : Type u_2<VAR>G : SimpleGraph V<VAR>DecidableRel G.Adj<VAR>Fintype V<VAR>AddCommMonoid α<VAR>One α<GOAL>(SimpleGraph.adjMatrix α G).trace = 0
<VAR>V : Type u_1<VAR>α : Type u_2<VAR>G : SimpleGraph V<VAR>DecidableRel G.Adj<VAR>Fintype V<VAR>NonAssocSemiring α<VAR>i : V<GOAL>(SimpleGraph.adjMatrix α G * SimpleGraph.adjMatrix α G) i i = ↑(G.degree i)
<VAR>V : Type u_1<VAR>α : Type u_2<VAR>G : SimpleGraph V<VAR>DecidableRel G.Adj<VAR>Fintype V<VAR>NonAssocSemiring α<VAR>a : α<VAR>v : V<GOAL>(SimpleGraph.adjMatrix α G *ᵥ Function.const V a) v = ↑(G.degree v) * a
<VAR>V : Type u_1<VAR>α : Type u_2<VAR>G : SimpleGraph V<VAR>DecidableRel G.Adj<VAR>Fintype V<VAR>NonAssocSemiring α<VAR>d : ℕ<VAR>a : α<VAR>hd : G.IsRegularOfDegree d<VAR>v : V<GOAL>(SimpleGraph.adjMatrix α G *ᵥ Function.const V a) v = ↑d * a
<VAR>V : Type u_1<VAR>α : Type u_2<VAR>G : SimpleGraph V<VAR>DecidableRel G.Adj<VAR>Fintype V<VAR>DecidableEq V<VAR>Semiring α<VAR>n : ℕ<VAR>u v : V<GOAL>(SimpleGraph.adjMatrix α G ^ n) u v = ↑(Fintype.card ↑{p | p.length = n})
<VAR>V : Type u_1<VAR>α : Type u_2<VAR>G : SimpleGraph V<VAR>DecidableRel G.Adj<VAR>DecidableEq V<VAR>DecidableEq α<VAR>NonAssocSemiring α<GOAL>1 + SimpleGraph.adjMatrix α G + (SimpleGraph.adjMatrix α G).compl = Matrix.of fun x x => 1
<VAR>V : Type u_1<VAR>α : Type u_2<VAR>G : SimpleGraph V<VAR>DecidableRel G.Adj<VAR>Fintype V<VAR>NonAssocSemiring α<VAR>x y : V → α<GOAL>x ⬝ᵥ SimpleGraph.adjMatrix α G *ᵥ y = ∑ i : V, ∑ j : V, if G.Adj i j then x i * y j else 0
<VAR>V : Type u_1<VAR>α : Type u_2<VAR>MulZeroOneClass α<VAR>Nontrivial α<VAR>A : Matrix V V α<VAR>h : A.IsAdjMatrix<VAR>DecidableEq α<GOAL>SimpleGraph.adjMatrix α h.toGraph = A
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s : Finset α<VAR>P : Finpartition s<VAR>G : SimpleGraph α<VAR>DecidableRel G.Adj<GOAL>0 ≤ P.energy G
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s : Finset α<VAR>P : Finpartition s<VAR>G : SimpleGraph α<VAR>DecidableRel G.Adj<GOAL>P.energy G ≤ 1
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s : Finset α<VAR>P : Finpartition s<VAR>G : SimpleGraph α<VAR>DecidableRel G.Adj<VAR>𝕜 : Type u_2<VAR>LinearOrderedField 𝕜<GOAL>↑(P.energy G) = (∑ uv ∈ P.parts.offDiag, ↑(G.edgeDensity uv.1 uv.2) ^ 2) / ↑P.parts.card ^ 2
<VAR>n : ℕ<VAR>self : Composition n<GOAL>self.blocks.sum = n
<VAR>n : ℕ<VAR>self : Composition n<VAR>i : ℕ<GOAL>i ∈ self.blocks → 0 < i
<VAR>n : ℕ<VAR>self : CompositionAsSet n<GOAL>Fin.last n ∈ self.boundaries
<VAR>n : ℕ<VAR>self : CompositionAsSet n<GOAL>0 ∈ self.boundaries
<VAR>n : ℕ<VAR>c : Composition n<GOAL>c.blocks.length = c.length
<VAR>n : ℕ<VAR>c : Composition n<GOAL>List.ofFn c.blocksFun = c.blocks
<VAR>n : ℕ<VAR>c : Composition n<VAR>i : Fin c.length<GOAL>c.blocksFun i ∈ c.blocks
<VAR>n : ℕ<VAR>c : Composition n<VAR>i : ℕ<VAR>h : i ∈ c.blocks<GOAL>1 ≤ i
<VAR>n : ℕ<VAR>c : Composition n<VAR>i : ℕ<VAR>h : i < c.length<GOAL>1 ≤ c.blocks[i]
<VAR>n : ℕ<VAR>c : Composition n<VAR>i : ℕ<VAR>h : i < c.length<GOAL>0 < c.blocks[i]
<VAR>n : ℕ<VAR>c : Composition n<VAR>i : Fin c.length<GOAL>1 ≤ c.blocksFun i
<VAR>n : ℕ<VAR>c : Composition n<GOAL>c.sizeUpTo 0 = 0
<VAR>n : ℕ<VAR>c : Composition n<VAR>i : ℕ<VAR>h : c.length ≤ i<GOAL>c.sizeUpTo i = n
<VAR>n : ℕ<VAR>c : Composition n<GOAL>c.sizeUpTo c.length = n
<VAR>n : ℕ<VAR>c : Composition n<VAR>i : ℕ<VAR>h : i < c.length<GOAL>c.sizeUpTo (i + 1) = c.sizeUpTo i + c.blocks[i]
<VAR>n : ℕ<VAR>c : Composition n<VAR>i : Fin c.length<GOAL>c.sizeUpTo (↑i + 1) = c.sizeUpTo ↑i + c.blocksFun i
<VAR>n : ℕ<VAR>c : Composition n<GOAL>Monotone c.sizeUpTo
<VAR>n : ℕ<VAR>c : Composition n<GOAL>c.boundary 0 = 0
<VAR>n : ℕ<VAR>c : Composition n<GOAL>c.boundaries.card = c.length + 1
<VAR>n : ℕ<VAR>c : Composition n<VAR>i : Fin c.length<VAR>j : Fin (c.blocksFun i)<GOAL>↑((c.embedding i) j) = c.sizeUpTo ↑i + ↑j
<VAR>n : ℕ<VAR>c : Composition n<VAR>j : Fin n<GOAL>↑j < c.sizeUpTo ↑(c.index j).succ
<VAR>n : ℕ<VAR>c : Composition n<VAR>j : Fin n<GOAL>↑(c.invEmbedding j) = ↑j - c.sizeUpTo ↑(c.index j)
<VAR>n : ℕ<VAR>c : Composition n<VAR>j : Fin n<VAR>i : Fin c.length<GOAL>j ∈ Set.range ⇑(c.embedding i) ↔ c.sizeUpTo ↑i ≤ ↑j ∧ ↑j < c.sizeUpTo (↑i).succ
<VAR>n : ℕ<VAR>c : Composition n<VAR>i₁ i₂ : Fin c.length<VAR>h : i₁ ≠ i₂<GOAL>Disjoint (Set.range ⇑(c.embedding i₁)) (Set.range ⇑(c.embedding i₂))
<VAR>n : ℕ<VAR>c : Composition n<VAR>j : Fin n<VAR>i : Fin c.length<GOAL>j ∈ Set.range ⇑(c.embedding i) ↔ i = c.index j
<VAR>n : ℕ<VAR>c : Composition n<VAR>i : Fin c.length<VAR>j : Fin (c.blocksFun i)<GOAL>c.index ((c.embedding i) j) = i
<VAR>n₁ n₂ : ℕ<VAR>c₁ : Composition n₁<VAR>c₂ : Composition n₂<VAR>i₁ : Fin c₁.length<VAR>i₂ : Fin c₂.length<VAR>hn : n₁ = n₂<VAR>hc : c₁.blocks = c₂.blocks<VAR>hi : ↑i₁ = ↑i₂<GOAL>c₁.blocksFun i₁ = c₂.blocksFun i₂
<VAR>c c' : (n : ℕ) × Composition n<GOAL>c = c' ↔ c.snd.blocks = c'.snd.blocks
<VAR>n : ℕ<GOAL>(Composition.ones n).length = n
<VAR>n : ℕ<GOAL>(Composition.ones n).blocks = List.replicate n 1
<VAR>n : ℕ<VAR>i : Fin (Composition.ones n).length<GOAL>(Composition.ones n).blocksFun i = 1
<VAR>n i : ℕ<GOAL>(Composition.ones n).sizeUpTo i = min i n
<VAR>n : ℕ<VAR>i : Fin (Composition.ones n).length<VAR>h : 0 < (Composition.ones n).blocksFun i<GOAL>((Composition.ones n).embedding i) ⟨0, h⟩ = ⟨↑i, ⋯⟩
<VAR>n : ℕ<VAR>c : Composition n<GOAL>c = Composition.ones n ↔ ∀ i ∈ c.blocks, i = 1
<VAR>n : ℕ<VAR>c : Composition n<GOAL>c ≠ Composition.ones n ↔ ∃ i ∈ c.blocks, 1 < i
<VAR>n : ℕ<VAR>c : Composition n<GOAL>c = Composition.ones n ↔ c.length = n
<VAR>n : ℕ<VAR>c : Composition n<GOAL>c = Composition.ones n ↔ n ≤ c.length
<VAR>n : ℕ<VAR>h : 0 < n<GOAL>(Composition.single n h).length = 1
<VAR>n : ℕ<VAR>h : 0 < n<GOAL>(Composition.single n h).blocks = [n]
<VAR>n : ℕ<VAR>h : 0 < n<VAR>i : Fin (Composition.single n h).length<GOAL>(Composition.single n h).blocksFun i = n
<VAR>n : ℕ<VAR>h : 0 < n<VAR>i : Fin n<GOAL>((Composition.single n h).embedding 0) i = i
<VAR>n : ℕ<VAR>h : 0 < n<VAR>c : Composition n<GOAL>c = Composition.single n h ↔ c.length = 1
<VAR>n : ℕ<VAR>hn : 0 < n<VAR>c : Composition n<GOAL>c ≠ Composition.single n hn ↔ ∀ (i : Fin c.length), c.blocksFun i < n
<VAR>α : Type u_1<VAR>l : List α<VAR>n : ℕ<VAR>ns : List ℕ<GOAL>l.splitWrtCompositionAux (n :: ns) = List.take n l :: (List.drop n l).splitWrtCompositionAux ns
<VAR>α : Type u_1<VAR>l : List α<VAR>ns : List ℕ<GOAL>(l.splitWrtCompositionAux ns).length = ns.length
<VAR>n : ℕ<VAR>α : Type u_1<VAR>l : List α<VAR>c : Composition n<GOAL>(l.splitWrtComposition c).length = c.length
<VAR>α : Type u_1<VAR>ns : List ℕ<VAR>l : List α<GOAL>ns.sum ≤ l.length → List.map List.length (l.splitWrtCompositionAux ns) = ns
<VAR>α : Type u_1<VAR>l : List α<VAR>c : Composition l.length<GOAL>List.map List.length (l.splitWrtComposition c) = c.blocks
<VAR>α : Type u_1<VAR>l l' : List α<VAR>c : Composition l.length<VAR>h : l' ∈ l.splitWrtComposition c<GOAL>0 < l'.length
<VAR>α : Type u_1<VAR>l : List α<VAR>c : Composition l.length<VAR>i : ℕ<GOAL>(List.take i (List.map List.length (l.splitWrtComposition c))).sum = c.sizeUpTo i
<VAR>α : Type u_1<VAR>l : List α<VAR>ns : List ℕ<VAR>i : ℕ<VAR>hi : i < (l.splitWrtCompositionAux ns).length<GOAL>(l.splitWrtCompositionAux ns)[i] = List.drop (List.take i ns).sum (List.take (List.take (i + 1) ns).sum l)
<VAR>n : ℕ<VAR>α : Type u_1<VAR>l : List α<VAR>c : Composition n<VAR>i : ℕ<VAR>hi : i < (l.splitWrtComposition c).length<GOAL>(l.splitWrtComposition c)[i] = List.drop (c.sizeUpTo i) (List.take (c.sizeUpTo (i + 1)) l)
<VAR>n : ℕ<VAR>α : Type u_1<VAR>l : List α<VAR>c : Composition n<VAR>i : ℕ<VAR>h : i < (l.splitWrtComposition c).length<GOAL>(l.splitWrtComposition c)[i] = List.drop (c.sizeUpTo i) (List.take (c.sizeUpTo (i + 1)) l)
<VAR>α : Type u_1<VAR>l : List α<VAR>ns : List ℕ<VAR>i : ℕ<VAR>hi : i < (l.splitWrtCompositionAux ns).length<GOAL>(l.splitWrtCompositionAux ns).get ⟨i, hi⟩ = List.drop (List.take i ns).sum (List.take (List.take (i + 1) ns).sum l)
<VAR>n : ℕ<VAR>α : Type u_1<VAR>l : List α<VAR>c : Composition n<VAR>i : ℕ<VAR>hi : i < (l.splitWrtComposition c).length<GOAL>(l.splitWrtComposition c).get ⟨i, hi⟩ = List.drop (c.sizeUpTo i) (List.take (c.sizeUpTo (i + 1)) l)
<VAR>n : ℕ<VAR>α : Type u_1<VAR>l : List α<VAR>c : Composition n<VAR>i : Fin (l.splitWrtComposition c).length<GOAL>(l.splitWrtComposition c).get i = List.drop (c.sizeUpTo ↑i) (List.take (c.sizeUpTo (↑i + 1)) l)
<VAR>α : Type u_1<VAR>ns : List ℕ<VAR>l : List α<GOAL>ns.sum = l.length → (l.splitWrtCompositionAux ns).join = l
<VAR>α : Type u_1<VAR>l : List α<VAR>c : Composition l.length<GOAL>(l.splitWrtComposition c).join = l
<VAR>α : Type u_1<VAR>L : List (List α)<VAR>c : Composition L.join.length<VAR>h : List.map List.length L = c.blocks<GOAL>L.join.splitWrtComposition c = L
<VAR>n : ℕ<GOAL>Fintype.card (CompositionAsSet n) = 2 ^ (n - 1)
<VAR>n : ℕ<VAR>c : CompositionAsSet n<GOAL>c.boundaries.Nonempty
<VAR>n : ℕ<VAR>c : CompositionAsSet n<GOAL>0 < c.boundaries.card
<VAR>n : ℕ<VAR>c : CompositionAsSet n<GOAL>c.boundaries.card = c.length + 1
<VAR>n : ℕ<VAR>c : CompositionAsSet n<VAR>i : Fin c.length<GOAL>↑i + 1 < c.boundaries.card
<VAR>n : ℕ<VAR>c : CompositionAsSet n<VAR>i : Fin c.length<GOAL>↑i < c.boundaries.card
<VAR>n : ℕ<VAR>c : CompositionAsSet n<VAR>i : Fin c.length<GOAL>0 < c.blocksFun i
<VAR>n : ℕ<VAR>c : CompositionAsSet n<GOAL>c.blocks.length = c.length
<VAR>n : ℕ<VAR>c : CompositionAsSet n<VAR>i : ℕ<VAR>h : i < c.boundaries.card<GOAL>(List.take i c.blocks).sum = ↑(c.boundary ⟨i, h⟩)
<VAR>n : ℕ<VAR>c : CompositionAsSet n<VAR>j : Fin (n + 1)<GOAL>j ∈ c.boundaries ↔ ∃ i < c.boundaries.card, (List.take i c.blocks).sum = ↑j
<VAR>n : ℕ<VAR>c : CompositionAsSet n<GOAL>c.toComposition.length = c.length
<VAR>n : ℕ<VAR>c : Composition n<GOAL>c.toCompositionAsSet.blocks = c.blocks
<VAR>n : ℕ<VAR>c : CompositionAsSet n<GOAL>c.toComposition.blocks = c.blocks
<VAR>n : ℕ<VAR>c : CompositionAsSet n<GOAL>c.toComposition.boundaries = c.boundaries
<VAR>n : ℕ<VAR>c : Composition n<GOAL>c.toCompositionAsSet.boundaries = c.boundaries
<VAR>n : ℕ<GOAL>Fintype.card (Composition n) = 2 ^ (n - 1)
<VAR>α : Type u_1<VAR>GeneralizedBooleanAlgebra α<VAR>u v : α<GOAL>Set.InjOn (fun x => (x ⊔ u) \ v) {x | Disjoint u x ∧ v ≤ x}
<VAR>α : Type u_1<VAR>GeneralizedBooleanAlgebra α<VAR>DecidableRel Disjoint<VAR>DecidableRel fun x x_1 => x ≤ x_1<VAR>u v a : α<VAR>hua : Disjoint u a<VAR>hva : v ≤ a<GOAL>UV.compress u v a = (a ⊔ u) \ v
<VAR>α : Type u_1<VAR>GeneralizedBooleanAlgebra α<VAR>DecidableRel Disjoint<VAR>DecidableRel fun x x_1 => x ≤ x_1<VAR>u v a : α<VAR>hva : Disjoint v a<VAR>hua : u ≤ a<GOAL>UV.compress u v ((a ⊔ v) \ u) = a
<VAR>α : Type u_1<VAR>GeneralizedBooleanAlgebra α<VAR>DecidableRel Disjoint<VAR>DecidableRel fun x x_1 => x ≤ x_1<VAR>u a : α<GOAL>UV.compress u u a = a
<VAR>α : Type u_1<VAR>GeneralizedBooleanAlgebra α<VAR>DecidableRel Disjoint<VAR>DecidableRel fun x x_1 => x ≤ x_1<VAR>a b : α<GOAL>UV.compress (a \ b) (b \ a) b = a
<VAR>α : Type u_1<VAR>GeneralizedBooleanAlgebra α<VAR>DecidableRel Disjoint<VAR>DecidableRel fun x x_1 => x ≤ x_1<VAR>u v a : α<GOAL>UV.compress u v (UV.compress u v a) = UV.compress u v a
<VAR>α : Type u_1<VAR>GeneralizedBooleanAlgebra α<VAR>DecidableRel Disjoint<VAR>DecidableRel fun x x_1 => x ≤ x_1<VAR>s : Finset α<VAR>u v : α<VAR>DecidableEq α<GOAL>Set.InjOn (UV.compress u v) ↑(Finset.filter (fun x => UV.compress u v x ∉ s) s)
<VAR>α : Type u_1<VAR>GeneralizedBooleanAlgebra α<VAR>DecidableRel Disjoint<VAR>DecidableRel fun x x_1 => x ≤ x_1<VAR>s : Finset α<VAR>u v a : α<VAR>DecidableEq α<GOAL>a ∈ UV.compression u v s ↔ a ∈ s ∧ UV.compress u v a ∈ s ∨ a ∉ s ∧ ∃ b ∈ s, UV.compress u v b = a
<VAR>α : Type u_1<VAR>GeneralizedBooleanAlgebra α<VAR>DecidableRel Disjoint<VAR>DecidableRel fun x x_1 => x ≤ x_1<VAR>s : Finset α<VAR>u v : α<VAR>DecidableEq α<VAR>h : UV.IsCompressed u v s<GOAL>UV.compression u v s = s
<VAR>α : Type u_1<VAR>GeneralizedBooleanAlgebra α<VAR>DecidableRel Disjoint<VAR>DecidableRel fun x x_1 => x ≤ x_1<VAR>DecidableEq α<VAR>u : α<VAR>s : Finset α<GOAL>UV.compression u u s = s
<VAR>α : Type u_1<VAR>GeneralizedBooleanAlgebra α<VAR>DecidableRel Disjoint<VAR>DecidableRel fun x x_1 => x ≤ x_1<VAR>DecidableEq α<VAR>u : α<VAR>s : Finset α<GOAL>UV.IsCompressed u u s
<VAR>α : Type u_1<VAR>GeneralizedBooleanAlgebra α<VAR>DecidableRel Disjoint<VAR>DecidableRel fun x x_1 => x ≤ x_1<VAR>s : Finset α<VAR>u v : α<VAR>DecidableEq α<GOAL>Disjoint (Finset.filter (fun x => UV.compress u v x ∈ s) s) (Finset.filter (fun x => x ∉ s) (Finset.image (UV.compress u v) s))
<VAR>α : Type u_1<VAR>GeneralizedBooleanAlgebra α<VAR>DecidableRel Disjoint<VAR>DecidableRel fun x x_1 => x ≤ x_1<VAR>s : Finset α<VAR>u v a : α<VAR>DecidableEq α<VAR>ha : a ∈ s<GOAL>UV.compress u v a ∈ UV.compression u v s
<VAR>α : Type u_1<VAR>GeneralizedBooleanAlgebra α<VAR>DecidableRel Disjoint<VAR>DecidableRel fun x x_1 => x ≤ x_1<VAR>s : Finset α<VAR>u v a : α<VAR>DecidableEq α<VAR>ha : a ∈ UV.compression u v s<GOAL>UV.compress u v a ∈ UV.compression u v s
<VAR>α : Type u_1<VAR>GeneralizedBooleanAlgebra α<VAR>DecidableRel Disjoint<VAR>DecidableRel fun x x_1 => x ≤ x_1<VAR>DecidableEq α<VAR>u v : α<VAR>s : Finset α<GOAL>UV.compression u v (UV.compression u v s) = UV.compression u v s
<VAR>α : Type u_1<VAR>GeneralizedBooleanAlgebra α<VAR>DecidableRel Disjoint<VAR>DecidableRel fun x x_1 => x ≤ x_1<VAR>DecidableEq α<VAR>u v : α<VAR>s : Finset α<GOAL>(UV.compression u v s).card = s.card
<VAR>α : Type u_1<VAR>GeneralizedBooleanAlgebra α<VAR>DecidableRel Disjoint<VAR>DecidableRel fun x x_1 => x ≤ x_1<VAR>s : Finset α<VAR>u v a : α<VAR>DecidableEq α<VAR>h : a ∈ UV.compression u v s<VAR>ha : a ∉ s<GOAL>u ≤ a
<VAR>α : Type u_1<VAR>GeneralizedBooleanAlgebra α<VAR>DecidableRel Disjoint<VAR>DecidableRel fun x x_1 => x ≤ x_1<VAR>s : Finset α<VAR>u v a : α<VAR>DecidableEq α<VAR>h : a ∈ UV.compression u v s<VAR>ha : a ∉ s<GOAL>Disjoint v a
<VAR>α : Type u_1<VAR>GeneralizedBooleanAlgebra α<VAR>DecidableRel Disjoint<VAR>DecidableRel fun x x_1 => x ≤ x_1<VAR>s : Finset α<VAR>u v a : α<VAR>DecidableEq α<VAR>h : a ∈ UV.compression u v s<VAR>ha : a ∉ s<GOAL>(a ⊔ v) \ u ∈ s
<VAR>α : Type u_1<VAR>GeneralizedBooleanAlgebra α<VAR>DecidableRel Disjoint<VAR>DecidableRel fun x x_1 => x ≤ x_1<VAR>s : Finset α<VAR>u v a : α<VAR>DecidableEq α<VAR>ha : a ∈ UV.compression u v s<VAR>hva : v ≤ a<VAR>hua : Disjoint u a<GOAL>(a ⊔ u) \ v ∈ s
<VAR>α : Type u_1<VAR>GeneralizedBooleanAlgebra α<VAR>DecidableRel Disjoint<VAR>DecidableRel fun x x_1 => x ≤ x_1<VAR>s : Finset α<VAR>u v a : α<VAR>DecidableEq α<VAR>ha : a ∈ UV.compression u v s<VAR>hva : v ≤ a<VAR>hvu : v = ⊥ → u = ⊥<GOAL>a ∈ s
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>u v : Finset α<VAR>huv : u.card = v.card<VAR>a : Finset α<GOAL>(UV.compress u v a).card = a.card
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>𝒜 : Finset (Finset α)<VAR>u v : Finset α<VAR>r : ℕ<VAR>huv : u.card = v.card<VAR>h𝒜 : Set.Sized r ↑𝒜<GOAL>Set.Sized r ↑(UV.compression u v 𝒜)
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>𝒜 : Finset (Finset α)<VAR>u v : Finset α<VAR>huv : ∀ x ∈ u, ∃ y ∈ v, UV.IsCompressed (u.erase x) (v.erase y) 𝒜<GOAL>v = ∅ → u = ∅
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>𝒜 : Finset (Finset α)<VAR>u v : Finset α<VAR>huv : ∀ x ∈ u, ∃ y ∈ v, UV.IsCompressed (u.erase x) (v.erase y) 𝒜<GOAL>(UV.compression u v 𝒜).shadow ⊆ UV.compression u v 𝒜.shadow
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>𝒜 : Finset (Finset α)<VAR>u v : Finset α<VAR>huv : ∀ x ∈ u, ∃ y ∈ v, UV.IsCompressed (u.erase x) (v.erase y) 𝒜<GOAL>(UV.compression u v 𝒜).shadow.card ≤ 𝒜.shadow.card
<VAR>V : Type u_1<VAR>W : Type u_2<VAR>f : V ↪ W<VAR>G : SimpleGraph V<VAR>u v : W<GOAL>(SimpleGraph.map f G).Adj u v ↔ ∃ u' v', G.Adj u' v' ∧ f u' = u ∧ f v' = v
<VAR>V : Type u_1<VAR>W : Type u_2<VAR>G : SimpleGraph V<VAR>f : V ↪ W<VAR>a b : V<GOAL>(SimpleGraph.map f G).Adj (f a) (f b) ↔ G.Adj a b
<VAR>V : Type u_1<VAR>W : Type u_2<VAR>f : V ↪ W<GOAL>Monotone (SimpleGraph.map f)
<VAR>V : Type u_1<VAR>G : SimpleGraph V<GOAL>SimpleGraph.map (Function.Embedding.refl V) G = G
<VAR>V : Type u_1<VAR>W : Type u_2<VAR>X : Type u_3<VAR>G : SimpleGraph V<VAR>f : V ↪ W<VAR>g : W ↪ X<GOAL>SimpleGraph.map g (SimpleGraph.map f G) = SimpleGraph.map (f.trans g) G
<VAR>V : Type u_1<VAR>W : Type u_2<VAR>u v : V<VAR>G : SimpleGraph W<VAR>f : V → W<GOAL>(SimpleGraph.comap f G).Adj u v ↔ G.Adj (f u) (f v)
<VAR>V : Type u_1<VAR>G : SimpleGraph V<GOAL>SimpleGraph.comap id G = G
<VAR>V : Type u_1<VAR>W : Type u_2<VAR>X : Type u_3<VAR>G : SimpleGraph X<VAR>f : V → W<VAR>g : W → X<GOAL>SimpleGraph.comap f (SimpleGraph.comap g G) = SimpleGraph.comap (g ∘ f) G
<VAR>V : Type u_1<VAR>W : Type u_2<VAR>G : SimpleGraph V<VAR>e : V ≃ W<GOAL>SimpleGraph.comap (⇑e.symm.toEmbedding) G = SimpleGraph.map e.toEmbedding G
<VAR>V : Type u_1<VAR>W : Type u_2<VAR>G : SimpleGraph W<VAR>e : V ≃ W<GOAL>SimpleGraph.map e.symm.toEmbedding G = SimpleGraph.comap (⇑e.toEmbedding) G
<VAR>V : Type u_1<VAR>W : Type u_2<VAR>f : V ↪ W<GOAL>Monotone (SimpleGraph.comap ⇑f)
<VAR>V : Type u_1<VAR>W : Type u_2<VAR>f : V ↪ W<VAR>G : SimpleGraph V<GOAL>SimpleGraph.comap (⇑f) (SimpleGraph.map f G) = G
<VAR>V : Type u_1<VAR>W : Type u_2<VAR>f : V ↪ W<GOAL>Function.LeftInverse (SimpleGraph.comap ⇑f) (SimpleGraph.map f)
<VAR>V : Type u_1<VAR>W : Type u_2<VAR>f : V ↪ W<GOAL>Function.Injective (SimpleGraph.map f)
<VAR>V : Type u_1<VAR>W : Type u_2<VAR>f : V ↪ W<GOAL>Function.Surjective (SimpleGraph.comap ⇑f)
<VAR>V : Type u_1<VAR>W : Type u_2<VAR>f : V ↪ W<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph W<GOAL>SimpleGraph.map f G ≤ G' ↔ G ≤ SimpleGraph.comap (⇑f) G'
<VAR>V : Type u_1<VAR>W : Type u_2<VAR>f : V ↪ W<VAR>G : SimpleGraph W<GOAL>SimpleGraph.map f (SimpleGraph.comap (⇑f) G) ≤ G
<VAR>V : Type u_1<VAR>W : Type u_2<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph W<VAR>f : V → W<VAR>Subsingleton V<GOAL>G ≤ SimpleGraph.comap f G'
<VAR>V : Type u_1<VAR>W : Type u_2<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph W<VAR>f : V ↪ W<VAR>Subsingleton V<GOAL>SimpleGraph.map f G ≤ G'
<VAR>V : Type u_1<VAR>W : Type u_2<VAR>e : V ≃ W<VAR>G : SimpleGraph V<GOAL>e.simpleGraph G = SimpleGraph.comap (⇑e.symm) G
<VAR>V : Type u_1<GOAL>(Equiv.refl V).simpleGraph = Equiv.refl (SimpleGraph V)
<VAR>V : Type u_1<VAR>W : Type u_2<VAR>X : Type u_3<VAR>e₁ : V ≃ W<VAR>e₂ : W ≃ X<GOAL>(e₁.trans e₂).simpleGraph = e₁.simpleGraph.trans e₂.simpleGraph
<VAR>V : Type u_1<VAR>W : Type u_2<VAR>e : V ≃ W<GOAL>e.simpleGraph.symm = e.symm.simpleGraph
<VAR>V : Type u_1<VAR>G : SimpleGraph V<VAR>v : V<GOAL>SimpleGraph.induce {v} G = ⊤
<VAR>V : Type u_1<VAR>s : Set V<VAR>G : SimpleGraph ↑s<GOAL>SimpleGraph.induce s G.spanningCoe = G
<VAR>V : Type u_1<VAR>G : SimpleGraph V<VAR>s : Set V<GOAL>(SimpleGraph.induce s G).spanningCoe ≤ G
<VAR>V : Type u_1<VAR>G : SimpleGraph V<GOAL>⇑SimpleGraph.Hom.id = 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<VAR>h : G.Adj v w<GOAL>G'.Adj (f v) (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>e : Sym2 V<VAR>h : e ∈ G.edgeSet<GOAL>Sym2.map (⇑f) 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<VAR>h : w ∈ G.neighborSet v<GOAL>f w ∈ G'.neighborSet (f 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 e) = Sym2.map ⇑f ↑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 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>d : G.Dart<GOAL>f.mapDart d = { toProd := Prod.map (⇑f) (⇑f) d.toProd, adj := ⋯ }
<VAR>V : Type u_1<VAR>G G' : SimpleGraph V<VAR>h : G ≤ G'<VAR>x : V<GOAL>(SimpleGraph.Hom.mapSpanningSubgraphs h) x = x
<VAR>V : Type u_1<VAR>W : Type u_2<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph W<VAR>f : G →g G'<VAR>hinj : Function.Injective ⇑f<GOAL>Function.Injective f.mapEdgeSet
<VAR>V : Type u_1<VAR>W : Type u_2<VAR>G' : SimpleGraph W<VAR>f : ⊤ →g G'<GOAL>Function.Injective ⇑f
<VAR>V : Type u_1<VAR>W : Type u_2<VAR>f : V → W<VAR>G : SimpleGraph W<GOAL>∀ (a : V), (SimpleGraph.Hom.comap f G) a = f a
<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₁ G₂ : SimpleGraph V<VAR>h : G₁ ≤ G₂<GOAL>⇑(SimpleGraph.Hom.ofLE h) = id
<VAR>V : Type u_1<VAR>W : Type u_2<VAR>G : SimpleGraph V<VAR>H : SimpleGraph W<VAR>f : G ↪g H<GOAL>⇑f.toHom = ⇑f
<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 e = SimpleGraph.Hom.mapEdgeSet (RelEmbedding.toRelHom f) 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 v)<GOAL>↑((f.mapNeighborSet v) w) = f ↑w
<VAR>V : Type u_1<VAR>W : Type u_2<VAR>f : V ↪ W<VAR>G : SimpleGraph W<VAR>v : V<GOAL>(SimpleGraph.Embedding.comap f G) v = f v
<VAR>V : Type u_1<VAR>W : Type u_2<VAR>f : V ↪ W<VAR>G : SimpleGraph V<VAR>v : V<GOAL>(SimpleGraph.Embedding.map f G) v = f v
<VAR>α : Type u_4<VAR>β : Type u_5<VAR>f : α ↪ β<GOAL>⇑(SimpleGraph.Embedding.completeGraph f) = ⇑f
<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>W : Type u_2<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph W<VAR>s : Set V<VAR>t : Set W<VAR>φ : G →g G'<VAR>φst : Set.MapsTo (⇑φ) s t<GOAL>⇑(SimpleGraph.induceHom φ φst) = Set.MapsTo.restrict (⇑φ) s t φst
<VAR>V : Type u_1<VAR>G : SimpleGraph V<VAR>s : Set V<GOAL>SimpleGraph.induceHom SimpleGraph.Hom.id ⋯ = SimpleGraph.Hom.id
<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>s : Set V<VAR>t : Set W<VAR>r : Set X<VAR>φ : G →g G'<VAR>φst : Set.MapsTo (⇑φ) s t<VAR>ψ : G' →g G''<VAR>ψtr : Set.MapsTo (⇑ψ) t r<GOAL>(SimpleGraph.induceHom ψ ψtr).comp (SimpleGraph.induceHom φ φst) = SimpleGraph.induceHom (ψ.comp φ) ⋯
<VAR>V : Type u_1<VAR>W : Type u_2<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph W<VAR>s : Set V<VAR>t : Set W<VAR>φ : G →g G'<VAR>φst : Set.MapsTo (⇑φ) s t<VAR>hi : Set.InjOn (⇑φ) s<GOAL>Function.Injective ⇑(SimpleGraph.induceHom φ φst)
<VAR>V : Type u_1<VAR>G : SimpleGraph V<VAR>s s' : Set V<VAR>h : s ≤ s'<VAR>v : ↑s<GOAL>(G.induceHomOfLE h) v = Set.inclusion h v