ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>n : ℕ<GOAL>Tree.treesOfNumNodesEq (n + 1) = (Finset.antidiagonal n).biUnion fun ij => Tree.pairwiseNode (Tree.treesOfNumNodesEq ij.1) (Tree.treesOfNumNodesEq ij.2)
<VAR>x : Tree Unit<VAR>n : ℕ<GOAL>x ∈ Tree.treesOfNumNodesEq n ↔ x.numNodes = n
<VAR>x : Tree Unit<GOAL>x ∈ Tree.treesOfNumNodesEq x.numNodes
<VAR>n : ℕ<GOAL>↑(Tree.treesOfNumNodesEq n) = {x | x.numNodes = n}
<VAR>n : ℕ<GOAL>(Tree.treesOfNumNodesEq n).card = catalan n
<VAR>V : Type u<VAR>self : SimpleGraph V<GOAL>Symmetric self.Adj
<VAR>V : Type u<VAR>self : SimpleGraph V<GOAL>Irreflexive self.Adj
<VAR>V : Type u<VAR>x : { adj // (∀ (x y : V), adj x y = adj y x) ∧ ∀ (x : V), ¬adj x x = true }<VAR>v w : V<GOAL>(SimpleGraph.mk' x).Adj v w = (↑x v w = true)
<VAR>V : Type u<VAR>r : V → V → Prop<VAR>v w : V<GOAL>(SimpleGraph.fromRel r).Adj v w ↔ v ≠ w ∧ (r v w ∨ r w v)
<VAR>V : Type u_1<VAR>W : Type u_2<VAR>v w : V ⊕ W<GOAL>(completeBipartiteGraph V W).Adj v w = (v.isLeft = true ∧ w.isRight = true ∨ v.isRight = true ∧ w.isLeft = true)
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>v : V<GOAL>¬G.Adj v v
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>u v : V<GOAL>G.Adj u v ↔ G.Adj v u
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>u v : V<VAR>h : G.Adj u v<GOAL>G.Adj v u
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>a b : V<VAR>h : G.Adj a b<GOAL>a ≠ b
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>a b : V<VAR>h : G.Adj a b<GOAL>b ≠ a
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>v w x : V<VAR>h : G.Adj v x<VAR>hn : ¬G.Adj w x<GOAL>v ≠ w
<VAR>V : Type u<GOAL>Function.Injective SimpleGraph.Adj
<VAR>V : Type u<VAR>G H : SimpleGraph V<GOAL>G.Adj = H.Adj ↔ G = H
<VAR>V : Type u<GOAL>SimpleGraph.IsSubgraph = fun x x_1 => x ≤ x_1
<VAR>V : Type u<VAR>x y : SimpleGraph V<VAR>v w : V<GOAL>(x ⊔ y).Adj v w ↔ x.Adj v w ∨ y.Adj v w
<VAR>V : Type u<VAR>x y : SimpleGraph V<VAR>v w : V<GOAL>(x ⊓ y).Adj v w ↔ x.Adj v w ∧ y.Adj v w
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>v w : V<GOAL>Gᶜ.Adj v w ↔ v ≠ w ∧ ¬G.Adj v w
<VAR>V : Type u<VAR>x y : SimpleGraph V<VAR>v w : V<GOAL>(x \ y).Adj v w ↔ x.Adj v w ∧ ¬y.Adj v w
<VAR>V : Type u<VAR>s : Set (SimpleGraph V)<VAR>a b : V<GOAL>(sSup s).Adj a b ↔ ∃ G ∈ s, G.Adj a b
<VAR>V : Type u<VAR>a b : V<VAR>s : Set (SimpleGraph V)<GOAL>(sInf s).Adj a b ↔ (∀ G ∈ s, G.Adj a b) ∧ a ≠ b
<VAR>ι : Sort u_1<VAR>V : Type u<VAR>a b : V<VAR>f : ι → SimpleGraph V<GOAL>(⨆ i, f i).Adj a b ↔ ∃ i, (f i).Adj a b
<VAR>ι : Sort u_1<VAR>V : Type u<VAR>a b : V<VAR>f : ι → SimpleGraph V<GOAL>(⨅ i, f i).Adj a b ↔ (∀ (i : ι), (f i).Adj a b) ∧ a ≠ b
<VAR>V : Type u<VAR>a b : V<VAR>s : Set (SimpleGraph V)<VAR>hs : s.Nonempty<GOAL>(sInf s).Adj a b ↔ ∀ G ∈ s, G.Adj a b
<VAR>ι : Sort u_1<VAR>V : Type u<VAR>a b : V<VAR>Nonempty ι<VAR>f : ι → SimpleGraph V<GOAL>(⨅ i, f i).Adj a b ↔ ∀ (i : ι), (f i).Adj a b
<VAR>V : Type u<VAR>v w : V<GOAL>⊤.Adj v w ↔ v ≠ w
<VAR>V : Type u<VAR>v w : V<GOAL>⊥.Adj v w ↔ False
<VAR>V : Type u<GOAL>completeGraph V = ⊤
<VAR>V : Type u<GOAL>emptyGraph V = ⊥
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>v : V<GOAL>v ∈ G.support ↔ ∃ w, G.Adj v w
<VAR>V : Type u<VAR>G G' : SimpleGraph V<VAR>h : G ≤ G'<GOAL>G.support ⊆ G'.support
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>v w : V<GOAL>s(v, w) ∈ G.edgeSet ↔ G.Adj v w
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>e : Sym2 V<GOAL>e ∈ G.edgeSet → ¬e.IsDiag
<VAR>V : Type u<VAR>G₁ G₂ : SimpleGraph V<GOAL>G₁.edgeSet = G₂.edgeSet ↔ G₁ = G₂
<VAR>V : Type u<VAR>G₁ G₂ : SimpleGraph V<GOAL>G₁.edgeSet ⊆ G₂.edgeSet ↔ G₁ ≤ G₂
<VAR>V : Type u<VAR>G₁ G₂ : SimpleGraph V<GOAL>G₁.edgeSet ⊂ G₂.edgeSet ↔ G₁ < G₂
<VAR>V : Type u<GOAL>Function.Injective SimpleGraph.edgeSet
<VAR>V : Type u<GOAL>⊥.edgeSet = ∅
<VAR>V : Type u<GOAL>⊤.edgeSet = {e | ¬e.IsDiag}
<VAR>V : Type u<VAR>G : SimpleGraph V<GOAL>G.edgeSet ⊆ {e | ¬e.IsDiag}
<VAR>V : Type u<VAR>G₁ G₂ : SimpleGraph V<GOAL>(G₁ ⊔ G₂).edgeSet = G₁.edgeSet ∪ G₂.edgeSet
<VAR>V : Type u<VAR>G₁ G₂ : SimpleGraph V<GOAL>(G₁ ⊓ G₂).edgeSet = G₁.edgeSet ∩ G₂.edgeSet
<VAR>V : Type u<VAR>G₁ G₂ : SimpleGraph V<GOAL>(G₁ \ G₂).edgeSet = G₁.edgeSet \ G₂.edgeSet
<VAR>V : Type u<VAR>G₁ G₂ : SimpleGraph V<GOAL>Disjoint G₁.edgeSet G₂.edgeSet ↔ Disjoint G₁ G₂
<VAR>V : Type u<VAR>G : SimpleGraph V<GOAL>G.edgeSet = ∅ ↔ G = ⊥
<VAR>V : Type u<VAR>G : SimpleGraph V<GOAL>G.edgeSet.Nonempty ↔ G ≠ ⊥
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>s : Set (Sym2 V)<GOAL>G.edgeSet \ (s \ {e | e.IsDiag}) = G.edgeSet \ s
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>v w : V<GOAL>G.Adj v w ↔ v ≠ w ∧ ∃ e ∈ G.edgeSet, v ∈ e ∧ w ∈ e
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>a b : V<GOAL>G.Adj a b ↔ ∃ e, ↑e = s(a, b)
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>e : Sym2 V<VAR>he : e ∈ G.edgeSet<VAR>v : V<VAR>h : v ∈ e<GOAL>Sym2.Mem.other h ≠ v
<VAR>V : Type u<VAR>v w : V<VAR>s : Set (Sym2 V)<GOAL>(SimpleGraph.fromEdgeSet s).Adj v w ↔ s(v, w) ∈ s ∧ v ≠ w
<VAR>V : Type u<VAR>s : Set (Sym2 V)<GOAL>(SimpleGraph.fromEdgeSet s).edgeSet = s \ {e | e.IsDiag}
<VAR>V : Type u<VAR>G : SimpleGraph V<GOAL>SimpleGraph.fromEdgeSet G.edgeSet = G
<VAR>V : Type u<GOAL>SimpleGraph.fromEdgeSet ∅ = ⊥
<VAR>V : Type u<GOAL>SimpleGraph.fromEdgeSet Set.univ = ⊤
<VAR>V : Type u<VAR>s t : Set (Sym2 V)<GOAL>SimpleGraph.fromEdgeSet (s ∩ t) = SimpleGraph.fromEdgeSet s ⊓ SimpleGraph.fromEdgeSet t
<VAR>V : Type u<VAR>s t : Set (Sym2 V)<GOAL>SimpleGraph.fromEdgeSet (s ∪ t) = SimpleGraph.fromEdgeSet s ⊔ SimpleGraph.fromEdgeSet t
<VAR>V : Type u<VAR>s t : Set (Sym2 V)<GOAL>SimpleGraph.fromEdgeSet (s \ t) = SimpleGraph.fromEdgeSet s \ SimpleGraph.fromEdgeSet t
<VAR>V : Type u<VAR>s t : Set (Sym2 V)<VAR>h : s ⊆ t<GOAL>SimpleGraph.fromEdgeSet s ≤ SimpleGraph.fromEdgeSet t
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>s : Set (Sym2 V)<GOAL>Disjoint G (SimpleGraph.fromEdgeSet s) ↔ Disjoint G.edgeSet s
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>s : Set (Sym2 V)<GOAL>Disjoint (SimpleGraph.fromEdgeSet s) G ↔ Disjoint s G.edgeSet
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>v : V<GOAL>G.incidenceSet v ⊆ G.edgeSet
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>a b c : V<GOAL>s(b, c) ∈ G.incidenceSet a ↔ G.Adj b c ∧ (a = b ∨ a = c)
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>a b : V<GOAL>s(a, b) ∈ G.incidenceSet a ↔ G.Adj a b
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>a b : V<GOAL>s(a, b) ∈ G.incidenceSet b ↔ G.Adj a b
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>a : V<VAR>e : ↑G.edgeSet<GOAL>↑e ∈ G.incidenceSet a ↔ a ∈ ↑e
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>a b : V<VAR>h : a ≠ b<GOAL>G.incidenceSet a ∩ G.incidenceSet b ⊆ {s(a, b)}
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>a b : V<VAR>h : G.Adj a b<GOAL>G.incidenceSet a ∩ G.incidenceSet b = {s(a, b)}
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>a b : V<VAR>e : Sym2 V<VAR>h : a ≠ b<VAR>ha : e ∈ G.incidenceSet a<VAR>hb : e ∈ G.incidenceSet b<GOAL>G.Adj a b
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>a b : V<VAR>h : ¬G.Adj a b<VAR>hn : a ≠ b<GOAL>G.incidenceSet a ∩ G.incidenceSet b = ∅
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>v w : V<GOAL>w ∈ G.neighborSet v ↔ G.Adj v w
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>a : V<GOAL>a ∉ G.neighborSet a
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>v w : V<GOAL>s(v, w) ∈ G.incidenceSet v ↔ G.Adj v w
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>v w : V<GOAL>s(v, w) ∈ G.incidenceSet v ↔ w ∈ G.neighborSet v
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>v : V<VAR>e : Sym2 V<VAR>he : e ∈ G.edgeSet<VAR>h : v ∈ e<GOAL>G.incidenceSet v ∩ G.incidenceSet (Sym2.Mem.other h) = {e}
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>v : V<GOAL>Disjoint (G.neighborSet v) (Gᶜ.neighborSet v)
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>v : V<GOAL>G.neighborSet v ∪ Gᶜ.neighborSet v = {v}ᶜ
<VAR>V : Type u<VAR>Fintype V<VAR>G : SimpleGraph V<VAR>v : V<VAR>Fintype ↑(G.neighborSet v ∪ Gᶜ.neighborSet v)<GOAL>(G.neighborSet v ∪ Gᶜ.neighborSet v).toFinset.card = Fintype.card V - 1
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>v : V<GOAL>Gᶜ.neighborSet v = (G.neighborSet v)ᶜ \ {v}
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>v w : V<GOAL>G.commonNeighbors v w = G.neighborSet v ∩ G.neighborSet w
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>u v w : V<GOAL>u ∈ G.commonNeighbors v w ↔ G.Adj v u ∧ G.Adj w u
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>v w : V<GOAL>G.commonNeighbors v w = G.commonNeighbors w v
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>v w : V<GOAL>v ∉ G.commonNeighbors v w
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>v w : V<GOAL>w ∉ G.commonNeighbors v w
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>v w : V<GOAL>G.commonNeighbors v w ⊆ G.neighborSet v
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>v w : V<GOAL>G.commonNeighbors v w ⊆ G.neighborSet w
<VAR>V : Type u<VAR>v w : V<GOAL>⊤.commonNeighbors v w = Set.univ \ {v, w}
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>DecidableEq V<VAR>v : V<VAR>e : Sym2 V<VAR>h : e ∈ G.incidenceSet v<GOAL>e ∈ G.incidenceSet (G.otherVertexOfIncident h)
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>DecidableEq V<VAR>v : V<VAR>e : Sym2 V<VAR>h : e ∈ G.incidenceSet v<GOAL>G.otherVertexOfIncident h ∈ G.neighborSet v
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>DecidableEq V<VAR>v w : V<VAR>h : w ∈ G.neighborSet v<GOAL>G.otherVertexOfIncident ⋯ = w
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>DecidableEq V<VAR>v : V<VAR>w : ↑(G.neighborSet v)<GOAL>↑((G.incidenceSetEquivNeighborSet v).symm w) = s(v, ↑w)
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>DecidableEq V<VAR>v : V<VAR>e : ↑(G.incidenceSet v)<GOAL>↑((G.incidenceSetEquivNeighborSet v) e) = G.otherVertexOfIncident ⋯
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>v w : V<VAR>s : Set (Sym2 V)<GOAL>(G.deleteEdges s).Adj v w ↔ G.Adj v w ∧ s(v, w) ∉ s
<VAR>V : Type u<VAR>G G' : SimpleGraph V<GOAL>G.deleteEdges G'.edgeSet = G \ G'
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>s s' : Set (Sym2 V)<GOAL>(G.deleteEdges s).deleteEdges s' = G.deleteEdges (s ∪ s')
<VAR>V : Type u<VAR>G : SimpleGraph V<GOAL>G.deleteEdges ∅ = G
<VAR>V : Type u<VAR>G : SimpleGraph V<GOAL>G.deleteEdges Set.univ = ⊥
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>s : Set (Sym2 V)<GOAL>G.deleteEdges s ≤ G
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>s₁ s₂ : Set (Sym2 V)<VAR>h : s₁ ⊆ s₂<GOAL>G.deleteEdges s₂ ≤ G.deleteEdges s₁
<VAR>V : Type u<VAR>G H : SimpleGraph V<VAR>s : Set (Sym2 V)<VAR>h : G ≤ H<GOAL>G.deleteEdges s ≤ H.deleteEdges s
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>s : Set (Sym2 V)<GOAL>G.deleteEdges s = G ↔ Disjoint G.edgeSet s
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>s : Set (Sym2 V)<GOAL>G.deleteEdges s = G.deleteEdges (s ∩ G.edgeSet)
<VAR>V : Type u<VAR>G H : SimpleGraph V<VAR>h : H ≤ G<GOAL>G.deleteEdges (G.edgeSet \ H.edgeSet) = H
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>s : Set (Sym2 V)<GOAL>(G.deleteEdges s).edgeSet = G.edgeSet \ s
<VAR>V : Type u_1<VAR>G : SimpleGraph V<VAR>M : G.Subgraph<VAR>v w : V<VAR>h : M.IsMatching<VAR>hv : v ∈ M.verts<VAR>hvw : M.Adj v w<GOAL>h.toEdge ⟨v, hv⟩ = ⟨s(v, w), hvw⟩
<VAR>V : Type u_1<VAR>G : SimpleGraph V<VAR>M : G.Subgraph<VAR>h : M.IsMatching<GOAL>Function.Surjective h.toEdge
<VAR>V : Type u_1<VAR>G : SimpleGraph V<VAR>M : G.Subgraph<VAR>v w : V<VAR>h : M.IsMatching<VAR>hv : v ∈ M.verts<VAR>hw : w ∈ M.verts<VAR>ha : M.Adj v w<GOAL>h.toEdge ⟨v, hv⟩ = h.toEdge ⟨w, hw⟩
<VAR>V : Type u_1<VAR>G G' : SimpleGraph V<VAR>M : G.Subgraph<VAR>h : M.IsMatching<VAR>hGG' : G ≤ G'<GOAL>(SimpleGraph.Subgraph.map (SimpleGraph.Hom.ofLE hGG') M).IsMatching
<VAR>V : Type u_1<VAR>G : SimpleGraph V<VAR>M M' : G.Subgraph<VAR>hM : M.IsMatching<VAR>hM' : M'.IsMatching<VAR>hd : Disjoint M.support M'.support<GOAL>(M ⊔ M').IsMatching
<VAR>V : Type u_1<VAR>G : SimpleGraph V<VAR>ι : Type u_2<VAR>f : ι → G.Subgraph<VAR>hM : ∀ (i : ι), (f i).IsMatching<VAR>hd : Pairwise fun i j => Disjoint (f i).support (f j).support<GOAL>(⨆ i, f i).IsMatching
<VAR>V : Type u_1<VAR>G : SimpleGraph V<VAR>v w : V<VAR>h : G.Adj v w<GOAL>(G.subgraphOfAdj h).IsMatching
<VAR>V : Type u_1<VAR>G : SimpleGraph V<VAR>G' : G.Subgraph<VAR>M : G'.coe.Subgraph<VAR>hM : M.IsMatching<GOAL>(SimpleGraph.Subgraph.coeSubgraph M).IsMatching
<VAR>V : Type u_1<VAR>G : SimpleGraph V<VAR>M : G.Subgraph<VAR>h : M.IsMatching<GOAL>M.support = M.verts
<VAR>V : Type u_1<VAR>G : SimpleGraph V<VAR>M : G.Subgraph<VAR>(v : V) → Fintype ↑(M.neighborSet v)<GOAL>M.IsMatching ↔ ∀ v ∈ M.verts, M.degree v = 1
<VAR>V : Type u_1<VAR>G : SimpleGraph V<VAR>M : G.Subgraph<VAR>Fintype ↑M.verts<VAR>h : M.IsMatching<GOAL>Even M.verts.toFinset.card
<VAR>V : Type u_1<VAR>G : SimpleGraph V<VAR>M : G.Subgraph<GOAL>M.IsPerfectMatching ↔ ∀ (v : V), ∃! w, M.Adj v w
<VAR>V : Type u_1<VAR>G : SimpleGraph V<VAR>M : G.Subgraph<VAR>(v : V) → Fintype ↑(M.neighborSet v)<GOAL>M.IsPerfectMatching ↔ ∀ (v : V), M.degree v = 1
<VAR>V : Type u_1<VAR>G : SimpleGraph V<VAR>M : G.Subgraph<VAR>Fintype V<VAR>h : M.IsPerfectMatching<GOAL>Even (Fintype.card V)
<VAR>V : Type u_1<VAR>G : SimpleGraph V<VAR>M : G.Subgraph<VAR>h : M.IsMatching<VAR>c : G.ConnectedComponent<GOAL>(M.induce (M.verts ∩ c.supp)).IsMatching
<VAR>V : Type u_1<VAR>G : SimpleGraph V<VAR>M : G.Subgraph<VAR>h : M.IsPerfectMatching<VAR>c : G.ConnectedComponent<GOAL>(M.induce c.supp).IsMatching
<VAR>V : Type u_1<VAR>G : SimpleGraph V<VAR>M : G.Subgraph<VAR>Fintype V<VAR>DecidableRel G.Adj<VAR>DecidableEq V<VAR>c : G.ConnectedComponent<VAR>hM : M.IsPerfectMatching<GOAL>Even (Fintype.card ↑c.supp)
<VAR>V : Type u_1<VAR>G : SimpleGraph V<VAR>M : G.Subgraph<VAR>Fintype V<VAR>u : Set V<VAR>c : (⊤.deleteVerts u).coe.ConnectedComponent<VAR>hM : M.IsPerfectMatching<VAR>codd : Odd (Nat.card ↑c.supp)<GOAL>∃ w ∈ u, ∃ v, M.Adj (↑v) w ∧ v ∈ c.supp
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<GOAL>∀ {X Y Z : SimplexCategoryᵒᵖ ⥤ C} (α : X ⟶ Y) (β : Y ⟶ Z) (X_1 : SimplexCategoryᵒᵖ), (α ≫ β).app X_1 = α.app X_1 ≫ β.app X_1
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F : SimplexCategoryᵒᵖ ⥤ C<VAR>X : SimplexCategoryᵒᵖ<GOAL>(𝟙 F).app X = 𝟙 (F.obj X)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : CategoryTheory.SimplicialObject C<VAR>f g : X ⟶ Y<VAR>h : ∀ (n : SimplexCategoryᵒᵖ), f.app n = g.app n<GOAL>f = g
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X : CategoryTheory.SimplicialObject C<VAR>n : ℕ<VAR>h : n = n<GOAL>X.eqToIso h = CategoryTheory.Iso.refl (X.obj (Opposite.op (SimplexCategory.mk n)))
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X : CategoryTheory.SimplicialObject C<VAR>n : ℕ<VAR>i j : Fin (n + 2)<VAR>H : i ≤ j<GOAL>X.δ j.succ ≫ X.δ i = X.δ i.castSucc ≫ X.δ j
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X : CategoryTheory.SimplicialObject C<VAR>n : ℕ<VAR>i : Fin (n + 2)<VAR>j : Fin (n + 3)<VAR>H : i.castSucc < j<GOAL>X.δ j ≫ X.δ i = X.δ i.castSucc ≫ X.δ (j.pred ⋯)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X : CategoryTheory.SimplicialObject C<VAR>n : ℕ<VAR>i : Fin (n + 3)<VAR>j : Fin (n + 2)<VAR>H : i ≤ j.castSucc<GOAL>X.δ j.succ ≫ X.δ (i.castLT ⋯) = X.δ i ≫ X.δ j
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X : CategoryTheory.SimplicialObject C<VAR>n : ℕ<VAR>i : Fin (n + 2)<GOAL>X.δ i.castSucc ≫ X.δ i = X.δ i.succ ≫ X.δ i
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X : CategoryTheory.SimplicialObject C<VAR>n : ℕ<VAR>j : Fin (n + 3)<VAR>i : Fin (n + 2)<VAR>H : j = i.castSucc<GOAL>X.δ j ≫ X.δ i = X.δ i.succ ≫ X.δ i
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X : CategoryTheory.SimplicialObject C<VAR>n : ℕ<VAR>i : Fin (n + 2)<VAR>j : Fin (n + 1)<VAR>H : i ≤ j.castSucc<GOAL>X.σ j.succ ≫ X.δ i.castSucc = X.δ i ≫ X.σ j
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X : CategoryTheory.SimplicialObject C<VAR>n : ℕ<VAR>i : Fin (n + 1)<GOAL>X.σ i ≫ X.δ i.castSucc = 𝟙 (X.obj (Opposite.op (SimplexCategory.mk n)))
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X : CategoryTheory.SimplicialObject C<VAR>n : ℕ<VAR>j : Fin (n + 2)<VAR>i : Fin (n + 1)<VAR>H : j = i.castSucc<GOAL>X.σ i ≫ X.δ j = 𝟙 (X.obj (Opposite.op (SimplexCategory.mk n)))
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X : CategoryTheory.SimplicialObject C<VAR>n : ℕ<VAR>i : Fin (n + 1)<GOAL>X.σ i ≫ X.δ i.succ = 𝟙 (X.obj (Opposite.op (SimplexCategory.mk n)))
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X : CategoryTheory.SimplicialObject C<VAR>n : ℕ<VAR>j : Fin (n + 2)<VAR>i : Fin (n + 1)<VAR>H : j = i.succ<GOAL>X.σ i ≫ X.δ j = 𝟙 (X.obj (Opposite.op (SimplexCategory.mk n)))
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X : CategoryTheory.SimplicialObject C<VAR>n : ℕ<VAR>i : Fin (n + 2)<VAR>j : Fin (n + 1)<VAR>H : j.castSucc < i<GOAL>X.σ j.castSucc ≫ X.δ i.succ = X.δ i ≫ X.σ j
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X : CategoryTheory.SimplicialObject C<VAR>n : ℕ<VAR>i : Fin (n + 3)<VAR>j : Fin (n + 2)<VAR>H : j.succ < i<GOAL>X.σ j ≫ X.δ i = X.δ (i.pred ⋯) ≫ X.σ (j.castLT ⋯)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X : CategoryTheory.SimplicialObject C<VAR>n : ℕ<VAR>i j : Fin (n + 1)<VAR>H : i ≤ j<GOAL>X.σ j ≫ X.σ i.castSucc = X.σ i ≫ X.σ j.succ
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X' X : CategoryTheory.SimplicialObject C<VAR>f : X ⟶ X'<VAR>n : ℕ<VAR>i : Fin (n + 2)<GOAL>X.δ i ≫ f.app (Opposite.op (SimplexCategory.mk n)) = f.app (Opposite.op (SimplexCategory.mk (n + 1))) ≫ X'.δ i
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X' X : CategoryTheory.SimplicialObject C<VAR>f : X ⟶ X'<VAR>n : ℕ<VAR>i : Fin (n + 1)<GOAL>X.σ i ≫ f.app (Opposite.op (SimplexCategory.mk (n + 1))) = f.app (Opposite.op (SimplexCategory.mk n)) ≫ X'.σ i
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>D : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} D<GOAL>∀ {X Y : C ⥤ D} (τ : X ⟶ Y) (F : SimplexCategoryᵒᵖ ⥤ C) (c : SimplexCategoryᵒᵖ), (((CategoryTheory.SimplicialObject.whiskering C D).map τ).app F).app c = τ.app (F.obj c)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>D : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} D<VAR>H : C ⥤ D<VAR>F : SimplexCategoryᵒᵖ ⥤ C<GOAL>∀ {X Y : SimplexCategoryᵒᵖ} (f : X ⟶ Y), (((CategoryTheory.SimplicialObject.whiskering C D).obj H).obj F).map f = H.map (F.map f)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>D : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} D<VAR>H : C ⥤ D<VAR>F : SimplexCategoryᵒᵖ ⥤ C<VAR>X : SimplexCategoryᵒᵖ<GOAL>(((CategoryTheory.SimplicialObject.whiskering C D).obj H).obj F).obj X = H.obj (F.obj X)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>D : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} D<VAR>H : C ⥤ D<GOAL>∀ {X Y : SimplexCategoryᵒᵖ ⥤ C} (α : X ⟶ Y) (X_1 : SimplexCategoryᵒᵖ), (((CategoryTheory.SimplicialObject.whiskering C D).obj H).map α).app X_1 = H.map (α.app X_1)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>n : ℕ<VAR>D : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} D<VAR>H : C ⥤ D<GOAL>∀ {X Y : (SimplexCategory.Truncated n)ᵒᵖ ⥤ C} (α : X ⟶ Y) (X_1 : (SimplexCategory.Truncated n)ᵒᵖ), (((CategoryTheory.SimplicialObject.Truncated.whiskering C D).obj H).map α).app X_1 = H.map (α.app X_1)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>n : ℕ<VAR>D : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} D<VAR>H : C ⥤ D<VAR>F : (SimplexCategory.Truncated n)ᵒᵖ ⥤ C<GOAL>∀ {X Y : (SimplexCategory.Truncated n)ᵒᵖ} (f : X ⟶ Y), (((CategoryTheory.SimplicialObject.Truncated.whiskering C D).obj H).obj F).map f = H.map (F.map f)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>n : ℕ<VAR>D : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} D<VAR>H : C ⥤ D<VAR>F : (SimplexCategory.Truncated n)ᵒᵖ ⥤ C<VAR>X : (SimplexCategory.Truncated n)ᵒᵖ<GOAL>(((CategoryTheory.SimplicialObject.Truncated.whiskering C D).obj H).obj F).obj X = H.obj (F.obj X)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>n : ℕ<VAR>D : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} D<GOAL>∀ {X Y : C ⥤ D} (τ : X ⟶ Y) (F : (SimplexCategory.Truncated n)ᵒᵖ ⥤ C) (c : (SimplexCategory.Truncated n)ᵒᵖ), (((CategoryTheory.SimplicialObject.Truncated.whiskering C D).map τ).app F).app c = τ.app (F.obj c)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X : CategoryTheory.Comma (𝟭 (CategoryTheory.SimplicialObject C)) (CategoryTheory.SimplicialObject.const C)<GOAL>∀ (X_1 : SimplexCategoryᵒᵖ), (𝟙 X).left.app X_1 = 𝟙 (X.left.obj X_1)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X : CategoryTheory.Comma (𝟭 (CategoryTheory.SimplicialObject C)) (CategoryTheory.SimplicialObject.const C)<GOAL>(𝟙 X).right = 𝟙 X.right
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<GOAL>∀ {X Y Z : CategoryTheory.Comma (𝟭 (CategoryTheory.SimplicialObject C)) (CategoryTheory.SimplicialObject.const C)} (f : X ⟶ Y) (g : Y ⟶ Z) (X_1 : SimplexCategoryᵒᵖ), (f ≫ g).left.app X_1 = f.left.app X_1 ≫ g.left.app X_1
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<GOAL>∀ {X Y Z : CategoryTheory.Comma (𝟭 (CategoryTheory.SimplicialObject C)) (CategoryTheory.SimplicialObject.const C)} (f : X ⟶ Y) (g : Y ⟶ Z), (f ≫ g).right = f.right ≫ g.right
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : CategoryTheory.SimplicialObject.Augmented C<VAR>f g : X ⟶ Y<VAR>h₁ : f.left = g.left<VAR>h₂ : f.right = g.right<GOAL>f = g
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X : CategoryTheory.Comma (𝟭 (CategoryTheory.SimplicialObject C)) (CategoryTheory.SimplicialObject.const C)<GOAL>CategoryTheory.SimplicialObject.Augmented.drop.obj X = X.left
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<GOAL>∀ {X Y : CategoryTheory.Comma (𝟭 (CategoryTheory.SimplicialObject C)) (CategoryTheory.SimplicialObject.const C)} (f : X ⟶ Y), CategoryTheory.SimplicialObject.Augmented.drop.map f = f.left
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X : CategoryTheory.Comma (𝟭 (CategoryTheory.SimplicialObject C)) (CategoryTheory.SimplicialObject.const C)<GOAL>CategoryTheory.SimplicialObject.Augmented.point.obj X = X.right
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<GOAL>∀ {X Y : CategoryTheory.Comma (𝟭 (CategoryTheory.SimplicialObject C)) (CategoryTheory.SimplicialObject.const C)} (f : X ⟶ Y), CategoryTheory.SimplicialObject.Augmented.point.map f = f.right
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X : CategoryTheory.SimplicialObject.Augmented C<GOAL>(CategoryTheory.SimplicialObject.Augmented.toArrow.obj X).right = CategoryTheory.SimplicialObject.Augmented.point.obj X
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X : CategoryTheory.SimplicialObject.Augmented C<GOAL>(CategoryTheory.SimplicialObject.Augmented.toArrow.obj X).hom = X.hom.app (Opposite.op (SimplexCategory.mk 0))
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<GOAL>∀ {X Y : CategoryTheory.SimplicialObject.Augmented C} (η : X ⟶ Y), (CategoryTheory.SimplicialObject.Augmented.toArrow.map η).right = CategoryTheory.SimplicialObject.Augmented.point.map η
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X : CategoryTheory.SimplicialObject.Augmented C<GOAL>(CategoryTheory.SimplicialObject.Augmented.toArrow.obj X).left = (CategoryTheory.SimplicialObject.Augmented.drop.obj X).obj (Opposite.op (SimplexCategory.mk 0))
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<GOAL>∀ {X Y : CategoryTheory.SimplicialObject.Augmented C} (η : X ⟶ Y), (CategoryTheory.SimplicialObject.Augmented.toArrow.map η).left = (CategoryTheory.SimplicialObject.Augmented.drop.map η).app (Opposite.op (SimplexCategory.mk 0))
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : CategoryTheory.SimplicialObject.Augmented C<VAR>f : X ⟶ Y<GOAL>(CategoryTheory.SimplicialObject.Augmented.drop.map f).app (Opposite.op (SimplexCategory.mk 0)) ≫ Y.hom.app (Opposite.op (SimplexCategory.mk 0)) = X.hom.app (Opposite.op (SimplexCategory.mk 0)) ≫ CategoryTheory.SimplicialObject.Augmented.point.map f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>D : Type u'<VAR>CategoryTheory.Category.{v', u'} D<VAR>F : C ⥤ D<GOAL>(CategoryTheory.SimplicialObject.Augmented.whiskering C D).obj F = CategoryTheory.SimplicialObject.Augmented.whiskeringObj C D F
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>D : Type u'<VAR>CategoryTheory.Category.{v', u'} D<GOAL>∀ {X Y : C ⥤ D} (η : X ⟶ Y) (A : CategoryTheory.SimplicialObject.Augmented C), (((CategoryTheory.SimplicialObject.Augmented.whiskering C D).map η).app A).left = CategoryTheory.whiskerLeft (CategoryTheory.SimplicialObject.Augmented.drop.obj A) η