ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>V : Type u<VAR>W : Type v<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph W<VAR>f : G →g G'<VAR>H : G.Subgraph<VAR>H' : G'.Subgraph<GOAL>SimpleGraph.Subgraph.map f H ≤ H' ↔ H ≤ SimpleGraph.Subgraph.comap f H'
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>x y : G.Subgraph<VAR>h : x ≤ y<VAR>v : ↑x.verts<GOAL>↑((SimpleGraph.Subgraph.inclusion h) v) = ↑v
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>x y : G.Subgraph<VAR>h : x ≤ y<GOAL>Function.Injective ⇑(SimpleGraph.Subgraph.inclusion h)
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>x : G.Subgraph<VAR>v : ↑x.verts<GOAL>x.hom v = ↑v
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>x : G.Subgraph<GOAL>⇑x.hom = fun v => ↑v
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>x : G.Subgraph<GOAL>Function.Injective ⇑x.hom
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>x : G.Subgraph<VAR>a : V<GOAL>x.spanningHom a = id a
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>x : G.Subgraph<GOAL>Function.Injective ⇑x.spanningHom
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>x y : G.Subgraph<VAR>h : x ≤ y<VAR>v : V<GOAL>x.neighborSet v ⊆ y.neighborSet v
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>Fintype V<VAR>G' : G.Subgraph<VAR>Fintype ↑G'.verts<VAR>h : G'.IsSpanning<GOAL>G'.verts.toFinset.card = Fintype.card V
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>G' : G.Subgraph<VAR>v : V<VAR>Fintype ↑(G'.neighborSet v)<GOAL>(G'.neighborSet v).toFinset.card = G'.degree v
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>G' : G.Subgraph<VAR>v : V<VAR>Fintype ↑(G'.neighborSet v)<VAR>Fintype ↑(G.neighborSet v)<GOAL>G'.degree v ≤ G.degree v
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>G' G'' : G.Subgraph<VAR>h : G' ≤ G''<VAR>v : V<VAR>Fintype ↑(G'.neighborSet v)<VAR>Fintype ↑(G''.neighborSet v)<GOAL>G'.degree v ≤ G''.degree v
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>G' : G.Subgraph<VAR>v : ↑G'.verts<VAR>Fintype ↑(G'.coe.neighborSet v)<VAR>Fintype ↑(G'.neighborSet ↑v)<GOAL>G'.coe.degree v = G'.degree ↑v
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>G' : G.Subgraph<VAR>v : V<VAR>Fintype ↑(G'.neighborSet v)<VAR>Fintype ↑(G'.spanningCoe.neighborSet v)<GOAL>G'.spanningCoe.degree v = G'.degree v
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>G' : G.Subgraph<VAR>v : V<VAR>Fintype ↑(G'.neighborSet v)<GOAL>G'.degree v = 1 ↔ ∃! w, G'.Adj v w
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>v : V<VAR>H : G.Subgraph<GOAL>G.singletonSubgraph v ≤ H ↔ v ∈ H.verts
<VAR>V : Type u<VAR>W : Type v<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph W<VAR>f : G →g G'<VAR>v : V<GOAL>SimpleGraph.Subgraph.map f (G.singletonSubgraph v) = G'.singletonSubgraph (f v)
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>v w : V<GOAL>(G.singletonSubgraph v).neighborSet w = ∅
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>v : V<GOAL>(G.singletonSubgraph v).edgeSet = ∅
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>H : G.Subgraph<VAR>v : V<GOAL>H = G.singletonSubgraph v ↔ H.verts = {v}
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>v w : V<VAR>hvw : G.Adj v w<GOAL>(G.subgraphOfAdj hvw).edgeSet = {s(v, w)}
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>v w : V<VAR>H : G.Subgraph<VAR>h : H.Adj v w<GOAL>G.subgraphOfAdj ⋯ ≤ H
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>v w : V<VAR>hvw : G.Adj v w<GOAL>G.subgraphOfAdj ⋯ = G.subgraphOfAdj hvw
<VAR>V : Type u<VAR>W : Type v<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph W<VAR>f : G →g G'<VAR>v w : V<VAR>hvw : G.Adj v w<GOAL>SimpleGraph.Subgraph.map f (G.subgraphOfAdj hvw) = G'.subgraphOfAdj ⋯
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>u v w : V<VAR>hvw : G.Adj v w<GOAL>(G.subgraphOfAdj hvw).neighborSet u ⊆ {v, w}
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>v w : V<VAR>hvw : G.Adj v w<GOAL>(G.subgraphOfAdj hvw).neighborSet v = {w}
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>v w : V<VAR>hvw : G.Adj v w<GOAL>(G.subgraphOfAdj hvw).neighborSet w = {v}
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>u v w : V<VAR>hvw : G.Adj v w<VAR>hv : u ≠ v<VAR>hw : u ≠ w<GOAL>(G.subgraphOfAdj hvw).neighborSet u = ∅
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>DecidableEq V<VAR>u v w : V<VAR>hvw : G.Adj v w<GOAL>(G.subgraphOfAdj hvw).neighborSet u = (if u = v then {w} else ∅) ∪ if u = w then {v} else ∅
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>u v : V<VAR>h : G.Adj u v<GOAL>G.singletonSubgraph u ≤ G.subgraphOfAdj h
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>u v : V<VAR>h : G.Adj u v<GOAL>G.singletonSubgraph v ≤ G.subgraphOfAdj h
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>u v : V<VAR>h : G.Adj u v<GOAL>(G.subgraphOfAdj h).support = {u, v}
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>G' : G.Subgraph<VAR>G'' : G'.coe.Subgraph<GOAL>(SimpleGraph.Subgraph.coeSubgraph G'').verts = Subtype.val '' G''.verts
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>G' : G.Subgraph<VAR>G'' : G'.coe.Subgraph<VAR>v w : V<GOAL>(SimpleGraph.Subgraph.coeSubgraph G'').Adj v w ↔ ∃ (hv : v ∈ G'.verts) (hw : w ∈ G'.verts), G''.Adj ⟨v, hv⟩ ⟨w, hw⟩
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>G' G'' : G.Subgraph<VAR>v w : ↑G'.verts<GOAL>(SimpleGraph.Subgraph.restrict G'').Adj v w ↔ G'.Adj ↑v ↑w ∧ G''.Adj ↑v ↑w
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>G' : G.Subgraph<VAR>G'' : G'.coe.Subgraph<GOAL>SimpleGraph.Subgraph.restrict (SimpleGraph.Subgraph.coeSubgraph G'') = G''
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>G' : G.Subgraph<GOAL>Function.Injective SimpleGraph.Subgraph.coeSubgraph
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>H : G.Subgraph<VAR>H' : H.coe.Subgraph<GOAL>SimpleGraph.Subgraph.coeSubgraph H' ≤ H
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>H : G.Subgraph<VAR>H' : G.Subgraph<GOAL>SimpleGraph.Subgraph.coeSubgraph (SimpleGraph.Subgraph.restrict H') = H ⊓ H'
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>G' : G.Subgraph<VAR>s : Set (Sym2 V)<GOAL>(G'.deleteEdges s).verts = G'.verts
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>G' : G.Subgraph<VAR>s : Set (Sym2 V)<VAR>v w : V<GOAL>(G'.deleteEdges s).Adj v w ↔ G'.Adj v w ∧ s(v, w) ∉ s
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>G' : G.Subgraph<VAR>s s' : Set (Sym2 V)<GOAL>(G'.deleteEdges s).deleteEdges s' = G'.deleteEdges (s ∪ s')
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>G' : G.Subgraph<GOAL>G'.deleteEdges ∅ = G'
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>G' : G.Subgraph<VAR>s : Set (Sym2 V)<GOAL>G'.spanningCoe.deleteEdges s = (G'.deleteEdges s).spanningCoe
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>G' : G.Subgraph<VAR>s : Set (Sym2 ↑G'.verts)<GOAL>G'.coe.deleteEdges s = (G'.deleteEdges (Sym2.map Subtype.val '' s)).coe
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>G' : G.Subgraph<VAR>s : Set (Sym2 V)<GOAL>(G'.deleteEdges s).coe = G'.coe.deleteEdges (Sym2.map Subtype.val ⁻¹' s)
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>G' : G.Subgraph<VAR>s : Set (Sym2 V)<GOAL>G'.deleteEdges s ≤ G'
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>G' : G.Subgraph<VAR>s s' : Set (Sym2 V)<VAR>h : s ⊆ s'<GOAL>G'.deleteEdges s' ≤ G'.deleteEdges s
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>G' : G.Subgraph<VAR>s : Set (Sym2 V)<GOAL>G'.deleteEdges (G'.edgeSet ∩ s) = G'.deleteEdges s
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>G' : G.Subgraph<VAR>s : Set (Sym2 V)<GOAL>G'.deleteEdges (s ∩ G'.edgeSet) = G'.deleteEdges s
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>G' : G.Subgraph<VAR>s : Set (Sym2 V)<GOAL>(G'.deleteEdges s).coe ≤ G'.coe
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>G' : G.Subgraph<VAR>s : Set (Sym2 V)<GOAL>(G'.deleteEdges s).spanningCoe ≤ G'.spanningCoe
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>G' : G.Subgraph<VAR>s : Set V<VAR>u v : V<GOAL>(G'.induce s).Adj u v = (u ∈ s ∧ v ∈ s ∧ G'.Adj u v)
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>G' : G.Subgraph<VAR>s : Set V<GOAL>(G'.induce s).verts = s
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>s : Set V<GOAL>SimpleGraph.induce s G = (⊤.induce s).coe
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>G' G'' : G.Subgraph<VAR>s s' : Set V<VAR>hg : G' ≤ G''<VAR>hs : s ⊆ s'<GOAL>G'.induce s ≤ G''.induce s'
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>G' G'' : G.Subgraph<VAR>s : Set V<VAR>hg : G' ≤ G''<GOAL>G'.induce s ≤ G''.induce s
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>G' : G.Subgraph<VAR>s s' : Set V<VAR>hs : s ⊆ s'<GOAL>G'.induce s ≤ G'.induce s'
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>G' : G.Subgraph<GOAL>G'.induce ∅ = ⊥
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>G' : G.Subgraph<GOAL>G'.induce G'.verts = G'
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>G' : G.Subgraph<GOAL>G' ≤ ⊤.induce G'.verts
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>G' : G.Subgraph<VAR>s s' : Set V<GOAL>G'.induce s ⊔ G'.induce s' ≤ G'.induce (s ∪ s')
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>G' : G.Subgraph<VAR>s s' : Set V<GOAL>G'.induce s ≤ G'.induce (s ∪ s')
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>G' : G.Subgraph<VAR>s s' : Set V<GOAL>G'.induce s' ≤ G'.induce (s ∪ s')
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>v : V<GOAL>G.singletonSubgraph v = ⊤.induce {v}
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>v w : V<VAR>hvw : G.Adj v w<GOAL>G.subgraphOfAdj hvw = ⊤.induce {v, w}
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>G' : G.Subgraph<VAR>s : Set V<GOAL>(G'.deleteVerts s).verts = G'.verts \ s
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>G' : G.Subgraph<VAR>s : Set V<VAR>u v : V<GOAL>(G'.deleteVerts s).Adj u v ↔ u ∈ G'.verts ∧ u ∉ s ∧ v ∈ G'.verts ∧ v ∉ s ∧ G'.Adj u v
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>G' : G.Subgraph<VAR>s s' : Set V<GOAL>(G'.deleteVerts s).deleteVerts s' = G'.deleteVerts (s ∪ s')
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>G' : G.Subgraph<GOAL>G'.deleteVerts ∅ = G'
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>G' : G.Subgraph<VAR>s : Set V<GOAL>G'.deleteVerts s ≤ G'
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>s : Set V<VAR>G' G'' : G.Subgraph<VAR>h : G' ≤ G''<GOAL>G'.deleteVerts s ≤ G''.deleteVerts s
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>G' : G.Subgraph<VAR>s s' : Set V<VAR>h : s ⊆ s'<GOAL>G'.deleteVerts s' ≤ G'.deleteVerts s
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>G' : G.Subgraph<VAR>s : Set V<GOAL>G'.deleteVerts (G'.verts ∩ s) = G'.deleteVerts s
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>G' : G.Subgraph<VAR>s : Set V<GOAL>G'.deleteVerts (s ∩ G'.verts) = G'.deleteVerts s
<VAR>D : Type u_1<VAR>C : Type u_2<VAR>OrderedAddCommMonoid C<VAR>Γ : ValuedCSP D C<VAR>ι : Type u_3<VAR>self : Γ.Term ι<GOAL>⟨self.n, self.f⟩ ∈ Γ
<VAR>D : Type u_1<VAR>m : ℕ<VAR>ω : FractionalOperation D m<VAR>valid : ω.IsValid<GOAL>∃ g, g ∈ ω
<VAR>D : Type u_1<VAR>C : Type u_3<VAR>OrderedCancelAddCommMonoid C<VAR>f : (Fin 2 → D) → C<VAR>a b : D<VAR>mcf : Function.HasMaxCutPropertyAt f a b<VAR>hab : a ≠ b<VAR>ω : FractionalOperation D 2<VAR>symmega : ω.IsSymmetric<VAR>r : Fin 2 → D<VAR>rin : r ∈ ω.tt ![![a, b], ![b, a]]<GOAL>f ![a, b] < f r
<VAR>D : Type u_1<VAR>C : Type u_3<VAR>OrderedCancelAddCommMonoid C<VAR>f : (Fin 2 → D) → C<VAR>mcf : Function.HasMaxCutProperty f<VAR>ω : FractionalOperation D 2<VAR>valid : ω.IsValid<VAR>symmega : ω.IsSymmetric<GOAL>¬Function.AdmitsFractional f ω
<VAR>α : Type u_1<VAR>G : SimpleGraph α<VAR>DecidableRel G.Adj<VAR>ε : ℝ<VAR>s t : Finset α<GOAL>↑(Rel.interedges G.Adj (SimpleGraph.badVertices G ε s t) t).card ≤ ↑(SimpleGraph.badVertices G ε s t).card * ↑t.card * (↑(G.edgeDensity s t) - ε)
<VAR>α : Type u_1<VAR>G : SimpleGraph α<VAR>DecidableRel G.Adj<VAR>ε : ℝ<VAR>s t : Finset α<VAR>hε : 0 ≤ ε<VAR>dst : 2 * ε ≤ ↑(G.edgeDensity s t)<GOAL>↑(G.edgeDensity (SimpleGraph.badVertices G ε s t) t) ≤ ↑(G.edgeDensity s t) - ε
<VAR>α : Type u_1<VAR>G : SimpleGraph α<VAR>DecidableRel G.Adj<VAR>ε : ℝ<VAR>s t : Finset α<VAR>dst : 2 * ε ≤ ↑(G.edgeDensity s t)<VAR>hst : G.IsUniform ε s t<GOAL>↑(SimpleGraph.badVertices G ε s t).card ≤ ↑s.card * ε
<VAR>α : Type u_1<VAR>G : SimpleGraph α<VAR>DecidableRel G.Adj<VAR>ε : ℝ<VAR>s t u : Finset α<VAR>DecidableEq α<GOAL>((s \ (SimpleGraph.badVertices G ε s t ∪ SimpleGraph.badVertices G ε s u)).biUnion fun x => Finset.image (fun x_1 => (x, x_1)) (G.interedges (Finset.filter (G.Adj x) t) (Finset.filter (G.Adj x) u))) ⊆ Finset.filter (fun x => match x with | (x, y, z) => G.Adj x y ∧ G.Adj x z ∧ G.Adj y z) (s ×ˢ t ×ˢ u)
<VAR>α : Type u_1<VAR>G : SimpleGraph α<VAR>DecidableRel G.Adj<VAR>ε : ℝ<VAR>s t u : Finset α<VAR>DecidableEq α<VAR>dst : 2 * ε ≤ ↑(G.edgeDensity s t)<VAR>dsu : 2 * ε ≤ ↑(G.edgeDensity s u)<VAR>dtu : 2 * ε ≤ ↑(G.edgeDensity t u)<VAR>utu : G.IsUniform ε t u<VAR>x : α<VAR>hx : x ∈ s \ (SimpleGraph.badVertices G ε s t ∪ SimpleGraph.badVertices G ε s u)<GOAL>ε ^ 3 * ↑t.card * ↑u.card ≤ ↑(Finset.image (fun x_1 => (x, x_1)) (Finset.filter (fun x => match x with | (y, z) => G.Adj y z) (Finset.filter (G.Adj x) t ×ˢ Finset.filter (G.Adj x) u))).card
<VAR>α : Type u_1<VAR>G : SimpleGraph α<VAR>DecidableRel G.Adj<VAR>ε : ℝ<VAR>s t u : Finset α<VAR>dst : 2 * ε ≤ ↑(G.edgeDensity s t)<VAR>hst : G.IsUniform ε s t<VAR>dsu : 2 * ε ≤ ↑(G.edgeDensity s u)<VAR>usu : G.IsUniform ε s u<VAR>dtu : 2 * ε ≤ ↑(G.edgeDensity t u)<VAR>utu : G.IsUniform ε t u<GOAL>(1 - 2 * ε) * ε ^ 3 * ↑s.card * ↑t.card * ↑u.card ≤ ↑(Finset.filter (fun x => match x with | (a, b, c) => G.Adj a b ∧ G.Adj a c ∧ G.Adj b c) (s ×ˢ t ×ˢ u)).card
<VAR>α : Type u_1<VAR>s t u : Finset α<VAR>DecidableEq α<VAR>hst : Disjoint s t<VAR>hsu : Disjoint s u<VAR>htu : Disjoint t u<VAR>x₁ x₂ y₁ y₂ z₁ z₂ : α<VAR>h : {x₁, y₁, z₁} = {x₂, y₂, z₂}<VAR>hx₁ : x₁ ∈ s<VAR>hx₂ : x₂ ∈ s<VAR>hy₁ : y₁ ∈ t<VAR>hy₂ : y₂ ∈ t<VAR>hz₁ : z₁ ∈ u<VAR>hz₂ : z₂ ∈ u<GOAL>(x₁, y₁, z₁) = (x₂, y₂, z₂)
<VAR>α : Type u_1<VAR>G : SimpleGraph α<VAR>DecidableRel G.Adj<VAR>ε : ℝ<VAR>s t u : Finset α<VAR>DecidableEq α<VAR>Fintype α<VAR>dst : 2 * ε ≤ ↑(G.edgeDensity s t)<VAR>ust : G.IsUniform ε s t<VAR>hst : Disjoint s t<VAR>dsu : 2 * ε ≤ ↑(G.edgeDensity s u)<VAR>usu : G.IsUniform ε s u<VAR>hsu : Disjoint s u<VAR>dtu : 2 * ε ≤ ↑(G.edgeDensity t u)<VAR>utu : G.IsUniform ε t u<VAR>htu : Disjoint t u<GOAL>(1 - 2 * ε) * ε ^ 3 * ↑s.card * ↑t.card * ↑u.card ≤ ↑(G.cliqueFinset 3).card
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>t : Finset (α × β × γ)<GOAL>∀ (a a_1 : α ⊕ β ⊕ γ), SimpleGraph.TripartiteFromTriangles.Rel t a a_1 ↔ (∃ a_2 b c, (a_2, b, c) ∈ t ∧ a = Sum3.in₀ a_2 ∧ a_1 = Sum3.in₁ b) ∨ (∃ a_2 b c, (a_2, b, c) ∈ t ∧ a = Sum3.in₁ b ∧ a_1 = Sum3.in₀ a_2) ∨ (∃ a_2 b c, (a_2, b, c) ∈ t ∧ a = Sum3.in₀ a_2 ∧ a_1 = Sum3.in₂ c) ∨ (∃ a_2 b c, (a_2, b, c) ∈ t ∧ a = Sum3.in₂ c ∧ a_1 = Sum3.in₀ a_2) ∨ (∃ a_2 b c, (a_2, b, c) ∈ t ∧ a = Sum3.in₁ b ∧ a_1 = Sum3.in₂ c) ∨ ∃ a_2 b c, (a_2, b, c) ∈ t ∧ a = Sum3.in₂ c ∧ a_1 = Sum3.in₁ b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>t : Finset (α × β × γ)<VAR>x : α ⊕ β ⊕ γ<GOAL>¬SimpleGraph.TripartiteFromTriangles.Rel t x x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>t : Finset (α × β × γ)<GOAL>Symmetric (SimpleGraph.TripartiteFromTriangles.Rel t)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>t : Finset (α × β × γ)<VAR>a a' : α<GOAL>¬(SimpleGraph.TripartiteFromTriangles.graph t).Adj (Sum3.in₀ a) (Sum3.in₀ a')
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>t : Finset (α × β × γ)<VAR>b b' : β<GOAL>¬(SimpleGraph.TripartiteFromTriangles.graph t).Adj (Sum3.in₁ b) (Sum3.in₁ b')
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>t : Finset (α × β × γ)<VAR>c c' : γ<GOAL>¬(SimpleGraph.TripartiteFromTriangles.graph t).Adj (Sum3.in₂ c) (Sum3.in₂ c')
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>t : Finset (α × β × γ)<VAR>a : α<VAR>b : β<GOAL>(SimpleGraph.TripartiteFromTriangles.graph t).Adj (Sum3.in₀ a) (Sum3.in₁ b) ↔ ∃ c, (a, b, c) ∈ t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>t : Finset (α × β × γ)<VAR>a : α<VAR>b : β<GOAL>(SimpleGraph.TripartiteFromTriangles.graph t).Adj (Sum3.in₁ b) (Sum3.in₀ a) ↔ ∃ c, (a, b, c) ∈ t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>t : Finset (α × β × γ)<VAR>a : α<VAR>c : γ<GOAL>(SimpleGraph.TripartiteFromTriangles.graph t).Adj (Sum3.in₀ a) (Sum3.in₂ c) ↔ ∃ b, (a, b, c) ∈ t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>t : Finset (α × β × γ)<VAR>a : α<VAR>c : γ<GOAL>(SimpleGraph.TripartiteFromTriangles.graph t).Adj (Sum3.in₂ c) (Sum3.in₀ a) ↔ ∃ b, (a, b, c) ∈ t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>t : Finset (α × β × γ)<VAR>b : β<VAR>c : γ<GOAL>(SimpleGraph.TripartiteFromTriangles.graph t).Adj (Sum3.in₁ b) (Sum3.in₂ c) ↔ ∃ a, (a, b, c) ∈ t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>t : Finset (α × β × γ)<VAR>b : β<VAR>c : γ<GOAL>(SimpleGraph.TripartiteFromTriangles.graph t).Adj (Sum3.in₂ c) (Sum3.in₁ b) ↔ ∃ a, (a, b, c) ∈ t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>t : Finset (α × β × γ)<VAR>a : α<VAR>b : β<GOAL>(SimpleGraph.TripartiteFromTriangles.graph t).Adj (Sum3.in₀ a) (Sum3.in₁ b) ↔ ∃ x ∈ t, x.1 = a ∧ x.2.1 = b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>t : Finset (α × β × γ)<VAR>a : α<VAR>b : β<GOAL>(SimpleGraph.TripartiteFromTriangles.graph t).Adj (Sum3.in₁ b) (Sum3.in₀ a) ↔ ∃ x ∈ t, x.2.1 = b ∧ x.1 = a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>t : Finset (α × β × γ)<VAR>a : α<VAR>c : γ<GOAL>(SimpleGraph.TripartiteFromTriangles.graph t).Adj (Sum3.in₀ a) (Sum3.in₂ c) ↔ ∃ x ∈ t, x.1 = a ∧ x.2.2 = c
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>t : Finset (α × β × γ)<VAR>a : α<VAR>c : γ<GOAL>(SimpleGraph.TripartiteFromTriangles.graph t).Adj (Sum3.in₂ c) (Sum3.in₀ a) ↔ ∃ x ∈ t, x.2.2 = c ∧ x.1 = a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>t : Finset (α × β × γ)<VAR>b : β<VAR>c : γ<GOAL>(SimpleGraph.TripartiteFromTriangles.graph t).Adj (Sum3.in₁ b) (Sum3.in₂ c) ↔ ∃ x ∈ t, x.2.1 = b ∧ x.2.2 = c
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>t : Finset (α × β × γ)<VAR>b : β<VAR>c : γ<GOAL>(SimpleGraph.TripartiteFromTriangles.graph t).Adj (Sum3.in₂ c) (Sum3.in₁ b) ↔ ∃ x ∈ t, x.2.2 = c ∧ x.2.1 = b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>t : Finset (α × β × γ)<VAR>self : SimpleGraph.TripartiteFromTriangles.ExplicitDisjoint t<VAR>a : α<VAR>b : β<VAR>c c' : γ<GOAL>(a, b, c) ∈ t → (a, b, c') ∈ t → c = c'
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>t : Finset (α × β × γ)<VAR>self : SimpleGraph.TripartiteFromTriangles.ExplicitDisjoint t<VAR>a : α<VAR>b : β<VAR>c : γ<VAR>a' : α<GOAL>(a, b, c) ∈ t → (a', b, c) ∈ t → a = a'
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>t : Finset (α × β × γ)<VAR>self : SimpleGraph.TripartiteFromTriangles.ExplicitDisjoint t<VAR>a : α<VAR>b : β<VAR>c : γ<VAR>b' : β<GOAL>(a, b, c) ∈ t → (a, b', c) ∈ t → b = b'
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>t : Finset (α × β × γ)<VAR>self : SimpleGraph.TripartiteFromTriangles.NoAccidental t<VAR>a a' : α<VAR>b b' : β<VAR>c c' : γ<GOAL>(a', b, c) ∈ t → (a, b', c) ∈ t → (a, b, c') ∈ t → a = a' ∨ b = b' ∨ c = c'
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>t : Finset (α × β × γ)<VAR>DecidableEq α<VAR>DecidableEq β<VAR>DecidableEq γ<VAR>x y z : α ⊕ β ⊕ γ<GOAL>(SimpleGraph.TripartiteFromTriangles.graph t).Adj x y → (SimpleGraph.TripartiteFromTriangles.graph t).Adj x z → (SimpleGraph.TripartiteFromTriangles.graph t).Adj y z → ∃ a b c, {Sum3.in₀ a, Sum3.in₁ b, Sum3.in₂ c} = {x, y, z} ∧ (SimpleGraph.TripartiteFromTriangles.graph t).Adj (Sum3.in₀ a) (Sum3.in₁ b) ∧ (SimpleGraph.TripartiteFromTriangles.graph t).Adj (Sum3.in₀ a) (Sum3.in₂ c) ∧ (SimpleGraph.TripartiteFromTriangles.graph t).Adj (Sum3.in₁ b) (Sum3.in₂ c)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>DecidableEq α<VAR>DecidableEq β<VAR>DecidableEq γ<VAR>x : α × β × γ<GOAL>SimpleGraph.TripartiteFromTriangles.toTriangle x = {Sum3.in₀ x.1, Sum3.in₁ x.2.1, Sum3.in₂ x.2.2}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>t : Finset (α × β × γ)<VAR>x : α × β × γ<VAR>DecidableEq α<VAR>DecidableEq β<VAR>DecidableEq γ<VAR>hx : x ∈ t<GOAL>(SimpleGraph.TripartiteFromTriangles.graph t).IsNClique 3 (SimpleGraph.TripartiteFromTriangles.toTriangle x)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>t : Finset (α × β × γ)<VAR>DecidableEq α<VAR>DecidableEq β<VAR>DecidableEq γ<VAR>x y : α ⊕ β ⊕ γ<VAR>hxy : (SimpleGraph.TripartiteFromTriangles.graph t).Adj x y<GOAL>∃ z ∈ t, x ∈ SimpleGraph.TripartiteFromTriangles.toTriangle z ∧ y ∈ SimpleGraph.TripartiteFromTriangles.toTriangle z
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>t : Finset (α × β × γ)<VAR>DecidableEq α<VAR>DecidableEq β<VAR>DecidableEq γ<VAR>SimpleGraph.TripartiteFromTriangles.NoAccidental t<VAR>s : Finset (α ⊕ β ⊕ γ)<GOAL>(SimpleGraph.TripartiteFromTriangles.graph t).IsNClique 3 s ↔ ∃ x ∈ t, SimpleGraph.TripartiteFromTriangles.toTriangle x = s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>t : Finset (α × β × γ)<VAR>DecidableEq α<VAR>DecidableEq β<VAR>DecidableEq γ<VAR>SimpleGraph.TripartiteFromTriangles.NoAccidental t<GOAL>Set.SurjOn (⇑SimpleGraph.TripartiteFromTriangles.toTriangle) (↑t) ((SimpleGraph.TripartiteFromTriangles.graph t).cliqueSet 3)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>t : Finset (α × β × γ)<VAR>DecidableEq α<VAR>DecidableEq β<VAR>DecidableEq γ<VAR>SimpleGraph.TripartiteFromTriangles.ExplicitDisjoint t<GOAL>(↑(Finset.map SimpleGraph.TripartiteFromTriangles.toTriangle t)).Pairwise fun x y => (↑x ∩ ↑y).Subsingleton
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>t : Finset (α × β × γ)<VAR>DecidableEq α<VAR>DecidableEq β<VAR>DecidableEq γ<VAR>SimpleGraph.TripartiteFromTriangles.NoAccidental t<GOAL>(SimpleGraph.TripartiteFromTriangles.graph t).cliqueSet 3 = ⇑SimpleGraph.TripartiteFromTriangles.toTriangle '' ↑t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>t : Finset (α × β × γ)<VAR>DecidableEq α<VAR>DecidableEq β<VAR>DecidableEq γ<VAR>Fintype α<VAR>Fintype β<VAR>Fintype γ<VAR>SimpleGraph.TripartiteFromTriangles.NoAccidental t<GOAL>(SimpleGraph.TripartiteFromTriangles.graph t).cliqueFinset 3 = Finset.image (⇑SimpleGraph.TripartiteFromTriangles.toTriangle) t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>t : Finset (α × β × γ)<VAR>DecidableEq α<VAR>DecidableEq β<VAR>DecidableEq γ<VAR>Fintype α<VAR>Fintype β<VAR>Fintype γ<VAR>SimpleGraph.TripartiteFromTriangles.NoAccidental t<GOAL>(SimpleGraph.TripartiteFromTriangles.graph t).cliqueFinset 3 = Finset.map SimpleGraph.TripartiteFromTriangles.toTriangle t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>t : Finset (α × β × γ)<VAR>DecidableEq α<VAR>DecidableEq β<VAR>DecidableEq γ<VAR>Fintype α<VAR>Fintype β<VAR>Fintype γ<VAR>SimpleGraph.TripartiteFromTriangles.NoAccidental t<GOAL>((SimpleGraph.TripartiteFromTriangles.graph t).cliqueFinset 3).card = t.card
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>𝕜 : Type u_4<VAR>LinearOrderedField 𝕜<VAR>t : Finset (α × β × γ)<VAR>DecidableEq α<VAR>DecidableEq β<VAR>DecidableEq γ<VAR>Fintype α<VAR>Fintype β<VAR>Fintype γ<VAR>SimpleGraph.TripartiteFromTriangles.ExplicitDisjoint t<VAR>ε : 𝕜<VAR>ht : ε * ↑((Fintype.card α + Fintype.card β + Fintype.card γ) ^ 2) ≤ ↑t.card<GOAL>(SimpleGraph.TripartiteFromTriangles.graph t).FarFromTriangleFree ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>t : Finset (α × β × γ)<VAR>SimpleGraph.TripartiteFromTriangles.ExplicitDisjoint t<VAR>SimpleGraph.TripartiteFromTriangles.NoAccidental t<GOAL>(SimpleGraph.TripartiteFromTriangles.graph t).LocallyLinear
<VAR>α : Type u_1<VAR>f : Equiv.Perm α<GOAL>f ∈ derangements α ↔ Function.fixedPoints ⇑f = ∅
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>a : Option α<VAR>f : Equiv.Perm α<GOAL>f ∈ derangements.Equiv.RemoveNone.fiber a ↔ ∃ F ∈ derangements (Option α), F none = a ∧ Equiv.removeNone F = f
<VAR>α : Type u_1<VAR>DecidableEq α<GOAL>derangements.Equiv.RemoveNone.fiber none = ∅
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>a : α<GOAL>derangements.Equiv.RemoveNone.fiber (some a) = {f | Function.fixedPoints ⇑f ⊆ {a}}
<GOAL>Filter.Tendsto (fun n => ↑(numDerangements n) / ↑n.factorial) Filter.atTop (𝓝 (Real.exp (-1)))
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Fintype α<VAR>DecidableEq α<VAR>Fintype β<VAR>DecidableEq β<VAR>h : Fintype.card α = Fintype.card β<GOAL>Fintype.card ↑(derangements α) = Fintype.card ↑(derangements β)
<VAR>n : ℕ<GOAL>Fintype.card ↑(derangements (Fin (n + 2))) = (n + 1) * Fintype.card ↑(derangements (Fin n)) + (n + 1) * Fintype.card ↑(derangements (Fin (n + 1)))
<VAR>n : ℕ<GOAL>numDerangements (n + 2) = (n + 1) * (numDerangements n + numDerangements (n + 1))
<VAR>n : ℕ<GOAL>↑(numDerangements (n + 1)) = (↑n + 1) * ↑(numDerangements n) - (-1) ^ n
<VAR>n : ℕ<GOAL>Fintype.card ↑(derangements (Fin n)) = numDerangements n
<VAR>α : Type u_2<VAR>Fintype α<VAR>DecidableEq α<GOAL>Fintype.card ↑(derangements α) = numDerangements (Fintype.card α)
<VAR>n : ℕ<GOAL>↑(numDerangements n) = ∑ k ∈ Finset.range (n + 1), (-1) ^ k * ↑((k + 1).ascFactorial (n - k))