ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>v : V<VAR>p : G.Walk v v<GOAL>p.Nil ↔ p = SimpleGraph.Walk.nil
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>u v w : V<VAR>motive : {u w : V} → (p : G.Walk u w) → ¬p.Nil → Sort u_1<VAR>cons : {u v w : V} → (h : G.Adj u v) → (q : G.Walk v w) → motive (SimpleGraph.Walk.cons h q) ⋯<VAR>h' : G.Adj u v<VAR>q' : G.Walk v w<GOAL>SimpleGraph.Walk.notNilRec (fun {u v w} => cons) (SimpleGraph.Walk.cons h' q') ⋯ = cons h' q'
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>v w : V<VAR>p : G.Walk v w<VAR>hp : ¬p.Nil<GOAL>G.Adj v (p.sndOfNotNil hp)
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>v w : V<VAR>p : G.Walk v w<VAR>hp : ¬p.Nil<GOAL>(p.firstDart hp).toProd = (v, p.sndOfNotNil hp)
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>v w : V<VAR>p : G.Walk v w<VAR>hp : ¬p.Nil<GOAL>(p.firstDart hp).edge = s(v, p.sndOfNotNil hp)
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>x y : V<VAR>p : G.Walk x y<VAR>hp : ¬p.Nil<GOAL>SimpleGraph.Walk.cons ⋯ (p.tail hp) = p
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>x y : V<VAR>p : G.Walk x y<VAR>hp : ¬p.Nil<GOAL>x :: (p.tail hp).support = p.support
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>x y : V<VAR>p : G.Walk x y<VAR>hp : ¬p.Nil<GOAL>(p.tail hp).length + 1 = p.length
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>x y x' y' : V<VAR>p : G.Walk x y<VAR>hx : x = x'<VAR>hy : y = y'<GOAL>(p.copy hx hy).Nil = p.Nil
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>v : V<VAR>p : G.Walk v v<VAR>hp : ¬p.Nil<GOAL>(p.tail hp).support = p.support.tail
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>t u v : V<VAR>p : G.Walk u v<VAR>h : G.Adj t u<GOAL>(SimpleGraph.Walk.cons h p).tail ⋯ = p
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>u v : V<VAR>p : G.Walk u v<VAR>hnp : ¬p.Nil<GOAL>(p.tail hnp).support = p.support.tail
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>DecidableEq V<VAR>u v w : V<VAR>p : G.Walk v w<VAR>h : u ∈ p.support<GOAL>(p.takeUntil u h).append (p.dropUntil u h) = p
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>u v w : V<VAR>p : G.Walk u v<GOAL>w ∈ p.support ↔ ∃ q r, p = q.append r
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>DecidableEq V<VAR>u v w : V<VAR>p : G.Walk v w<VAR>h : u ∈ p.support<GOAL>List.count u (p.takeUntil u h).support = 1
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>DecidableEq V<VAR>u v w : V<VAR>p : G.Walk v w<VAR>h : u ∈ p.support<VAR>x : V<GOAL>List.count s(u, x) (p.takeUntil u h).edges ≤ 1
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>DecidableEq V<VAR>u v w v' w' : V<VAR>p : G.Walk v w<VAR>hv : v = v'<VAR>hw : w = w'<VAR>h : u ∈ (p.copy hv hw).support<GOAL>(p.copy hv hw).takeUntil u h = (p.takeUntil u ⋯).copy hv ⋯
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>DecidableEq V<VAR>u v w v' w' : V<VAR>p : G.Walk v w<VAR>hv : v = v'<VAR>hw : w = w'<VAR>h : u ∈ (p.copy hv hw).support<GOAL>(p.copy hv hw).dropUntil u h = (p.dropUntil u ⋯).copy ⋯ hw
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>DecidableEq V<VAR>u v w : V<VAR>p : G.Walk v w<VAR>h : u ∈ p.support<GOAL>(p.takeUntil u h).support ⊆ p.support
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>DecidableEq V<VAR>u v w : V<VAR>p : G.Walk v w<VAR>h : u ∈ p.support<GOAL>(p.dropUntil u h).support ⊆ p.support
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>DecidableEq V<VAR>u v w : V<VAR>p : G.Walk v w<VAR>h : u ∈ p.support<GOAL>(p.takeUntil u h).darts ⊆ p.darts
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>DecidableEq V<VAR>u v w : V<VAR>p : G.Walk v w<VAR>h : u ∈ p.support<GOAL>(p.dropUntil u h).darts ⊆ p.darts
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>DecidableEq V<VAR>u v w : V<VAR>p : G.Walk v w<VAR>h : u ∈ p.support<GOAL>(p.takeUntil u h).edges ⊆ p.edges
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>DecidableEq V<VAR>u v w : V<VAR>p : G.Walk v w<VAR>h : u ∈ p.support<GOAL>(p.dropUntil u h).edges ⊆ p.edges
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>DecidableEq V<VAR>u v w : V<VAR>p : G.Walk v w<VAR>h : u ∈ p.support<GOAL>(p.takeUntil u h).length ≤ p.length
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>DecidableEq V<VAR>u v w : V<VAR>p : G.Walk v w<VAR>h : u ∈ p.support<GOAL>(p.dropUntil u h).length ≤ p.length
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>DecidableEq V<VAR>u v : V<VAR>c : G.Walk v v<VAR>h : u ∈ c.support<GOAL>(c.rotate h).support.tail ~r c.support.tail
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>DecidableEq V<VAR>u v : V<VAR>c : G.Walk v v<VAR>h : u ∈ c.support<GOAL>(c.rotate h).darts ~r c.darts
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>DecidableEq V<VAR>u v : V<VAR>c : G.Walk v v<VAR>h : u ∈ c.support<GOAL>(c.rotate h).edges ~r c.edges
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>u v : V<VAR>p : G.Walk u v<VAR>S : Set V<VAR>uS : u ∈ S<VAR>vS : v ∉ S<GOAL>∃ d ∈ p.darts, d.toProd.1 ∈ S ∧ d.toProd.2 ∉ S
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>u v : V<VAR>n : ℕ<VAR>p : G.Walk u v<VAR>hnp : ¬p.Nil<GOAL>(p.tail hnp).getVert n = p.getVert (n + 1)
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>u v w : V<VAR>q : G.Walk v w<VAR>hadj : G.Adj u v<GOAL>(SimpleGraph.Walk.cons hadj q).sndOfNotNil ⋯ = v
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>u v : V<VAR>p : G.Walk u v<VAR>hnp : ¬p.Nil<GOAL>p.getVert 1 = p.sndOfNotNil hnp
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>u v w : V<VAR>p : G.Walk v w<GOAL>u ∈ p.support ↔ ∃ n, p.getVert n = u ∧ n ≤ p.length
<VAR>V : Type u<VAR>V' : Type v<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph V'<VAR>f : G →g G'<VAR>u : V<GOAL>SimpleGraph.Walk.map f SimpleGraph.Walk.nil = SimpleGraph.Walk.nil
<VAR>V : Type u<VAR>V' : Type v<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph V'<VAR>f : G →g G'<VAR>u v : V<VAR>p : G.Walk u v<VAR>w : V<VAR>h : G.Adj w u<GOAL>SimpleGraph.Walk.map f (SimpleGraph.Walk.cons h p) = SimpleGraph.Walk.cons ⋯ (SimpleGraph.Walk.map f p)
<VAR>V : Type u<VAR>V' : Type v<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph V'<VAR>f : G →g G'<VAR>u v u' v' : V<VAR>p : G.Walk u v<VAR>hu : u = u'<VAR>hv : v = v'<GOAL>SimpleGraph.Walk.map f (p.copy hu hv) = (SimpleGraph.Walk.map f p).copy ⋯ ⋯
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>u v : V<VAR>p : G.Walk u v<GOAL>∀ (p : G.Walk u v), SimpleGraph.Walk.map SimpleGraph.Hom.id p = p
<VAR>V : Type u<VAR>V' : Type v<VAR>V'' : Type w<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph V'<VAR>G'' : SimpleGraph V''<VAR>f : G →g G'<VAR>f' : G' →g G''<VAR>u v : V<VAR>p : G.Walk u v<GOAL>SimpleGraph.Walk.map f' (SimpleGraph.Walk.map f p) = SimpleGraph.Walk.map (f'.comp f) p
<VAR>V : Type u<VAR>V' : Type v<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph V'<VAR>u v : V<VAR>p : G.Walk u v<VAR>f : G →g G'<VAR>f' : G →g G'<VAR>h : f = f'<GOAL>SimpleGraph.Walk.map f p = (SimpleGraph.Walk.map f' p).copy ⋯ ⋯
<VAR>V : Type u<VAR>V' : Type v<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph V'<VAR>f : G →g G'<VAR>u : V<VAR>p : G.Walk u u<GOAL>SimpleGraph.Walk.map f p = SimpleGraph.Walk.nil ↔ p = SimpleGraph.Walk.nil
<VAR>V : Type u<VAR>V' : Type v<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph V'<VAR>f : G →g G'<VAR>u v : V<VAR>p : G.Walk u v<GOAL>(SimpleGraph.Walk.map f p).length = p.length
<VAR>V : Type u<VAR>V' : Type v<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph V'<VAR>f : G →g G'<VAR>u v w : V<VAR>p : G.Walk u v<VAR>q : G.Walk v w<GOAL>SimpleGraph.Walk.map f (p.append q) = (SimpleGraph.Walk.map f p).append (SimpleGraph.Walk.map f q)
<VAR>V : Type u<VAR>V' : Type v<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph V'<VAR>f : G →g G'<VAR>u v : V<VAR>p : G.Walk u v<GOAL>(SimpleGraph.Walk.map f p).reverse = SimpleGraph.Walk.map f p.reverse
<VAR>V : Type u<VAR>V' : Type v<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph V'<VAR>f : G →g G'<VAR>u v : V<VAR>p : G.Walk u v<GOAL>(SimpleGraph.Walk.map f p).support = List.map (⇑f) p.support
<VAR>V : Type u<VAR>V' : Type v<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph V'<VAR>f : G →g G'<VAR>u v : V<VAR>p : G.Walk u v<GOAL>(SimpleGraph.Walk.map f p).darts = List.map f.mapDart p.darts
<VAR>V : Type u<VAR>V' : Type v<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph V'<VAR>f : G →g G'<VAR>u v : V<VAR>p : G.Walk u v<GOAL>(SimpleGraph.Walk.map f p).edges = List.map (Sym2.map ⇑f) p.edges
<VAR>V : Type u<VAR>V' : Type v<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph V'<VAR>f : G →g G'<VAR>hinj : Function.Injective ⇑f<VAR>u v : V<GOAL>Function.Injective (SimpleGraph.Walk.map f)
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>u v : V<VAR>p : G.Walk u v<GOAL>p.transfer G ⋯ = p
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>u v : V<VAR>p : G.Walk u v<VAR>H : SimpleGraph V<VAR>hp : ∀ e ∈ p.edges, e ∈ H.edgeSet<VAR>GH : G ≤ H<GOAL>p.transfer H hp = SimpleGraph.Walk.map (SimpleGraph.Hom.mapSpanningSubgraphs GH) p
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>u v : V<VAR>p : G.Walk u v<VAR>H : SimpleGraph V<VAR>hp : ∀ e ∈ p.edges, e ∈ H.edgeSet<GOAL>(p.transfer H hp).edges = p.edges
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>u v : V<VAR>p : G.Walk u v<VAR>H : SimpleGraph V<VAR>hp : ∀ e ∈ p.edges, e ∈ H.edgeSet<GOAL>(p.transfer H hp).support = p.support
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>u v : V<VAR>p : G.Walk u v<VAR>H : SimpleGraph V<VAR>hp : ∀ e ∈ p.edges, e ∈ H.edgeSet<GOAL>(p.transfer H hp).length = p.length
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>u v : V<VAR>p : G.Walk u v<VAR>H : SimpleGraph V<VAR>hp : ∀ e ∈ p.edges, e ∈ H.edgeSet<VAR>K : SimpleGraph V<VAR>hp' : ∀ e ∈ (p.transfer H hp).edges, e ∈ K.edgeSet<GOAL>(p.transfer H hp).transfer K hp' = p.transfer K ⋯
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>u v : V<VAR>p : G.Walk u v<VAR>H : SimpleGraph V<VAR>w : V<VAR>q : G.Walk v w<VAR>hpq : ∀ e ∈ (p.append q).edges, e ∈ H.edgeSet<GOAL>(p.append q).transfer H hpq = (p.transfer H ⋯).append (q.transfer H ⋯)
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>u v : V<VAR>p : G.Walk u v<VAR>H : SimpleGraph V<VAR>hp : ∀ e ∈ p.edges, e ∈ H.edgeSet<GOAL>(p.transfer H hp).reverse = p.reverse.transfer H ⋯
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>s : Set (Sym2 V)<VAR>v : V<VAR>hp : ∀ e ∈ SimpleGraph.Walk.nil.edges, e ∉ s<GOAL>SimpleGraph.Walk.toDeleteEdges s SimpleGraph.Walk.nil hp = SimpleGraph.Walk.nil
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>s : Set (Sym2 V)<VAR>u v w : V<VAR>h : G.Adj u v<VAR>p : G.Walk v w<VAR>hp : ∀ e ∈ (SimpleGraph.Walk.cons h p).edges, e ∉ s<GOAL>SimpleGraph.Walk.toDeleteEdges s (SimpleGraph.Walk.cons h p) hp = SimpleGraph.Walk.cons ⋯ (SimpleGraph.Walk.toDeleteEdges s p ⋯)
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>v w : V<VAR>s : Set (Sym2 V)<VAR>p : G.Walk v w<VAR>hp : ∀ e ∈ p.edges, e ∉ s<GOAL>SimpleGraph.Walk.map (SimpleGraph.Hom.mapSpanningSubgraphs ⋯) (SimpleGraph.Walk.toDeleteEdges s p hp) = p
<VAR>V : Type u_1<VAR>G : SimpleGraph V<VAR>Fintype ↑G.edgeSet<GOAL>↑G.edgeFinset = G.edgeSet
<VAR>V : Type u_1<VAR>G : SimpleGraph V<VAR>e : Sym2 V<VAR>Fintype ↑G.edgeSet<GOAL>e ∈ G.edgeFinset ↔ e ∈ G.edgeSet
<VAR>V : Type u_1<VAR>G : SimpleGraph V<VAR>e : Sym2 V<VAR>Fintype ↑G.edgeSet<GOAL>e ∈ G.edgeFinset → ¬e.IsDiag
<VAR>V : Type u_1<VAR>G₁ G₂ : SimpleGraph V<VAR>Fintype ↑G₁.edgeSet<VAR>Fintype ↑G₂.edgeSet<GOAL>G₁.edgeFinset = G₂.edgeFinset ↔ G₁ = G₂
<VAR>V : Type u_1<VAR>G₁ G₂ : SimpleGraph V<VAR>Fintype ↑G₁.edgeSet<VAR>Fintype ↑G₂.edgeSet<GOAL>G₁.edgeFinset ⊆ G₂.edgeFinset ↔ G₁ ≤ G₂
<VAR>V : Type u_1<VAR>G₁ G₂ : SimpleGraph V<VAR>Fintype ↑G₁.edgeSet<VAR>Fintype ↑G₂.edgeSet<GOAL>G₁.edgeFinset ⊂ G₂.edgeFinset ↔ G₁ < G₂
<VAR>V : Type u_1<GOAL>⊥.edgeFinset = ∅
<VAR>V : Type u_1<VAR>G₁ G₂ : SimpleGraph V<VAR>Fintype ↑G₁.edgeSet<VAR>Fintype ↑G₂.edgeSet<VAR>Fintype ↑(G₁ ⊔ G₂).edgeSet<VAR>DecidableEq V<GOAL>(G₁ ⊔ G₂).edgeFinset = G₁.edgeFinset ∪ G₂.edgeFinset
<VAR>V : Type u_1<VAR>G₁ G₂ : SimpleGraph V<VAR>Fintype ↑G₁.edgeSet<VAR>Fintype ↑G₂.edgeSet<VAR>DecidableEq V<GOAL>(G₁ ⊓ G₂).edgeFinset = G₁.edgeFinset ∩ G₂.edgeFinset
<VAR>V : Type u_1<VAR>G₁ G₂ : SimpleGraph V<VAR>Fintype ↑G₁.edgeSet<VAR>Fintype ↑G₂.edgeSet<VAR>DecidableEq V<GOAL>(G₁ \ G₂).edgeFinset = G₁.edgeFinset \ G₂.edgeFinset
<VAR>V : Type u_1<VAR>G : SimpleGraph V<VAR>Fintype ↑G.edgeSet<GOAL>G.edgeFinset.card = Fintype.card ↑G.edgeSet
<VAR>V : Type u_1<VAR>G : SimpleGraph V<VAR>Fintype ↑G.edgeSet<GOAL>Finset.univ.card = G.edgeFinset.card
<VAR>V : Type u_1<VAR>Fintype V<VAR>DecidableEq V<GOAL>⊤.edgeFinset = Finset.filter (fun e => ¬e.IsDiag) Finset.univ
<VAR>V : Type u_1<VAR>Fintype V<VAR>DecidableEq V<GOAL>⊤.edgeFinset.card = (Fintype.card V).choose 2
<VAR>V : Type u_1<VAR>G : SimpleGraph V<VAR>Fintype ↑G.edgeSet<VAR>Fintype V<GOAL>G.edgeFinset.card ≤ (Fintype.card V).choose 2
<VAR>V : Type u_1<VAR>G : SimpleGraph V<VAR>DecidableEq V<VAR>Fintype ↑G.edgeSet<VAR>s : Finset (Sym2 V)<VAR>Fintype ↑(G.deleteEdges ↑s).edgeSet<GOAL>(G.deleteEdges ↑s).edgeFinset = G.edgeFinset \ s
<VAR>V : Type u_1<VAR>G : SimpleGraph V<VAR>𝕜 : Type u_2<VAR>OrderedRing 𝕜<VAR>Fintype (Sym2 V)<VAR>Fintype ↑G.edgeSet<VAR>p : SimpleGraph V → Prop<VAR>r : 𝕜<GOAL>G.DeleteFar p r ↔ ∀ ⦃H : SimpleGraph V⦄ [inst : DecidableRel H.Adj], H ≤ G → p H → r ≤ ↑G.edgeFinset.card - ↑H.edgeFinset.card
<VAR>V : Type u_1<VAR>G : SimpleGraph V<VAR>𝕜 : Type u_2<VAR>OrderedRing 𝕜<VAR>Fintype ↑G.edgeSet<VAR>p : SimpleGraph V → Prop<VAR>r₁ r₂ : 𝕜<VAR>h : G.DeleteFar p r₂<VAR>hr : r₁ ≤ r₂<GOAL>G.DeleteFar p r₁
<VAR>V : Type u_1<VAR>G : SimpleGraph V<VAR>v : V<VAR>Fintype ↑(G.neighborSet v)<GOAL>G.neighborFinset v = (G.neighborSet v).toFinset
<VAR>V : Type u_1<VAR>G : SimpleGraph V<VAR>v : V<VAR>Fintype ↑(G.neighborSet v)<VAR>w : V<GOAL>w ∈ G.neighborFinset v ↔ G.Adj v w
<VAR>V : Type u_1<VAR>G : SimpleGraph V<VAR>v : V<VAR>Fintype ↑(G.neighborSet v)<GOAL>v ∉ G.neighborFinset v
<VAR>V : Type u_1<VAR>G : SimpleGraph V<VAR>v : V<VAR>Fintype ↑(G.neighborSet v)<GOAL>Disjoint (G.neighborFinset v) {v}
<VAR>V : Type u_1<VAR>G : SimpleGraph V<VAR>v : V<VAR>Fintype ↑(G.neighborSet v)<GOAL>Disjoint {v} (G.neighborFinset v)
<VAR>V : Type u_1<VAR>G : SimpleGraph V<VAR>v : V<VAR>Fintype ↑(G.neighborSet v)<GOAL>(G.neighborFinset v).card = G.degree v
<VAR>V : Type u_1<VAR>G : SimpleGraph V<VAR>v : V<VAR>Fintype ↑(G.neighborSet v)<GOAL>Fintype.card ↑(G.neighborSet v) = G.degree v
<VAR>V : Type u_1<VAR>G : SimpleGraph V<VAR>v : V<VAR>Fintype ↑(G.neighborSet v)<GOAL>0 < G.degree v ↔ ∃ w, G.Adj v w
<VAR>V : Type u_1<VAR>G : SimpleGraph V<VAR>v : V<VAR>Fintype ↑(G.neighborSet v)<VAR>Fintype ↑(Gᶜ.neighborSet v)<VAR>Fintype V<GOAL>Gᶜ.degree v = Fintype.card V - 1 - G.degree v
<VAR>V : Type u_1<VAR>G : SimpleGraph V<VAR>v : V<VAR>Fintype ↑(G.neighborSet v)<VAR>DecidableEq V<GOAL>Fintype.card ↑(G.incidenceSet v) = G.degree v
<VAR>V : Type u_1<VAR>G : SimpleGraph V<VAR>v : V<VAR>Fintype ↑(G.neighborSet v)<VAR>DecidableEq V<GOAL>(G.incidenceFinset v).card = G.degree v
<VAR>V : Type u_1<VAR>G : SimpleGraph V<VAR>v : V<VAR>Fintype ↑(G.neighborSet v)<VAR>DecidableEq V<VAR>e : Sym2 V<GOAL>e ∈ G.incidenceFinset v ↔ e ∈ G.incidenceSet v
<VAR>V : Type u_1<VAR>G : SimpleGraph V<VAR>v : V<VAR>Fintype ↑(G.neighborSet v)<VAR>DecidableEq V<VAR>Fintype ↑G.edgeSet<GOAL>G.incidenceFinset v = Finset.filter (Membership.mem v) G.edgeFinset
<VAR>V : Type u_1<VAR>G : SimpleGraph V<VAR>G.LocallyFinite<VAR>d : ℕ<VAR>h : G.IsRegularOfDegree d<VAR>v : V<GOAL>G.degree v = d
<VAR>V : Type u_1<VAR>Fintype V<VAR>DecidableEq V<VAR>G : SimpleGraph V<VAR>DecidableRel G.Adj<VAR>k : ℕ<VAR>h : G.IsRegularOfDegree k<GOAL>Gᶜ.IsRegularOfDegree (Fintype.card V - 1 - k)
<VAR>V : Type u_1<VAR>G : SimpleGraph V<VAR>Fintype V<VAR>v : V<VAR>DecidableRel G.Adj<GOAL>G.neighborFinset v = Finset.filter (G.Adj v) Finset.univ
<VAR>V : Type u_1<VAR>G : SimpleGraph V<VAR>Fintype V<VAR>DecidableEq V<VAR>DecidableRel G.Adj<VAR>v : V<GOAL>Gᶜ.neighborFinset v = (G.neighborFinset v)ᶜ \ {v}
<VAR>V : Type u_1<VAR>Fintype V<VAR>DecidableEq V<VAR>v : V<GOAL>⊤.degree v = Fintype.card V - 1
<VAR>V : Type u_1<VAR>Fintype V<VAR>v : V<GOAL>⊥.degree v = 0
<VAR>V : Type u_1<VAR>Fintype V<VAR>DecidableEq V<GOAL>⊤.IsRegularOfDegree (Fintype.card V - 1)
<VAR>V : Type u_1<VAR>G : SimpleGraph V<VAR>Fintype V<VAR>DecidableRel G.Adj<VAR>Nonempty V<GOAL>∃ v, G.minDegree = G.degree v
<VAR>V : Type u_1<VAR>G : SimpleGraph V<VAR>Fintype V<VAR>DecidableRel G.Adj<VAR>v : V<GOAL>G.minDegree ≤ G.degree v
<VAR>V : Type u_1<VAR>G : SimpleGraph V<VAR>Fintype V<VAR>DecidableRel G.Adj<VAR>Nonempty V<VAR>k : ℕ<VAR>h : ∀ (v : V), k ≤ G.degree v<GOAL>k ≤ G.minDegree
<VAR>V : Type u_1<VAR>G : SimpleGraph V<VAR>Fintype V<VAR>DecidableRel G.Adj<VAR>Nonempty V<GOAL>∃ v, G.maxDegree = G.degree v
<VAR>V : Type u_1<VAR>G : SimpleGraph V<VAR>Fintype V<VAR>DecidableRel G.Adj<VAR>v : V<GOAL>G.degree v ≤ G.maxDegree
<VAR>V : Type u_1<VAR>G : SimpleGraph V<VAR>Fintype V<VAR>DecidableRel G.Adj<VAR>k : ℕ<VAR>h : ∀ (v : V), G.degree v ≤ k<GOAL>G.maxDegree ≤ k
<VAR>V : Type u_1<VAR>G : SimpleGraph V<VAR>Fintype V<VAR>DecidableRel G.Adj<VAR>v : V<GOAL>G.degree v < Fintype.card V
<VAR>V : Type u_1<VAR>G : SimpleGraph V<VAR>Fintype V<VAR>DecidableRel G.Adj<VAR>Nonempty V<GOAL>G.maxDegree < Fintype.card V
<VAR>V : Type u_1<VAR>G : SimpleGraph V<VAR>Fintype V<VAR>DecidableRel G.Adj<VAR>v w : V<GOAL>Fintype.card ↑(G.commonNeighbors v w) ≤ G.degree v
<VAR>V : Type u_1<VAR>G : SimpleGraph V<VAR>Fintype V<VAR>DecidableRel G.Adj<VAR>v w : V<GOAL>Fintype.card ↑(G.commonNeighbors v w) ≤ G.degree w
<VAR>V : Type u_1<VAR>G : SimpleGraph V<VAR>Fintype V<VAR>DecidableRel G.Adj<VAR>v w : V<GOAL>Fintype.card ↑(G.commonNeighbors v w) < Fintype.card V
<VAR>V : Type u_1<VAR>Fintype V<VAR>G : SimpleGraph V<VAR>DecidableRel G.Adj<VAR>v w : V<VAR>h : G.Adj v w<GOAL>Fintype.card ↑(G.commonNeighbors v w) < G.degree v
<VAR>V : Type u_1<VAR>Fintype V<VAR>DecidableEq V<VAR>v w : V<VAR>h : v ≠ w<GOAL>Fintype.card ↑(⊤.commonNeighbors v w) = Fintype.card V - 2
<VAR>β : Type u_2<VAR>LinearOrderedCommSemiring β<VAR>ExistsAddOfLE β<VAR>a₀ a₁ b₀ b₁ c₀ c₁ d₀ d₁ : β<VAR>ha₀ : 0 ≤ a₀<VAR>ha₁ : 0 ≤ a₁<VAR>hb₀ : 0 ≤ b₀<VAR>hb₁ : 0 ≤ b₁<VAR>hc₀ : 0 ≤ c₀<VAR>hc₁ : 0 ≤ c₁<VAR>hd₀ : 0 ≤ d₀<VAR>hd₁ : 0 ≤ d₁<VAR>h₀₀ : a₀ * b₀ ≤ c₀ * d₀<VAR>h₁₀ : a₁ * b₀ ≤ c₀ * d₁<VAR>h₀₁ : a₀ * b₁ ≤ c₀ * d₁<VAR>h₁₁ : a₁ * b₁ ≤ c₁ * d₁<GOAL>(a₀ + a₁) * (b₀ + b₁) ≤ (c₀ + c₁) * (d₀ + d₁)
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>a : α<VAR>s t : Finset α<VAR>hs : a ∉ s<GOAL>t.erase a = s ↔ t = s ∨ t = insert a s
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>a : α<VAR>s : Finset α<VAR>ha : a ∉ s<VAR>𝒜 : Finset (Finset α)<GOAL>Finset.filter (fun t => t.erase a = s) 𝒜 = if s ∈ 𝒜 then if insert a s ∈ 𝒜 then {s, insert a s} else {s} else if insert a s ∈ 𝒜 then {insert a s} else ∅
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>DecidableEq α<VAR>LinearOrderedCommSemiring β<VAR>a : α<VAR>s : Finset α<VAR>ha : a ∉ s<VAR>𝒜 : Finset (Finset α)<VAR>f : Finset α → β<GOAL>collapse 𝒜 a f s = (if s ∈ 𝒜 then f s else 0) + if insert a s ∈ 𝒜 then f (insert a s) else 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>DecidableEq α<VAR>LinearOrderedCommSemiring β<VAR>𝒜 : Finset (Finset α)<VAR>a : α<VAR>f : Finset α → β<VAR>s t u : Finset α<VAR>ha : a ∉ s<VAR>ht : t ∈ 𝒜<VAR>hu : u ∈ 𝒜<VAR>hts : t = s<VAR>hus : u = insert a s<GOAL>collapse 𝒜 a f s = f t + f u
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>DecidableEq α<VAR>LinearOrderedCommSemiring β<VAR>𝒜 : Finset (Finset α)<VAR>a : α<VAR>f : Finset α → β<VAR>s t : Finset α<VAR>ha : a ∉ s<VAR>hf : 0 ≤ f<VAR>hts : t = s<VAR>ht : t ∈ 𝒜<GOAL>f t ≤ collapse 𝒜 a f s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>DecidableEq α<VAR>LinearOrderedCommSemiring β<VAR>𝒜 : Finset (Finset α)<VAR>a : α<VAR>f : Finset α → β<VAR>s t : Finset α<VAR>ha : a ∉ s<VAR>hf : 0 ≤ f<VAR>hts : t = insert a s<VAR>ht : t ∈ 𝒜<GOAL>f t ≤ collapse 𝒜 a f s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>DecidableEq α<VAR>LinearOrderedCommSemiring β<VAR>𝒜 : Finset (Finset α)<VAR>a : α<VAR>f : Finset α → β<VAR>hf : 0 ≤ f<GOAL>0 ≤ collapse 𝒜 a f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>DecidableEq α<VAR>LinearOrderedCommSemiring β<VAR>ExistsAddOfLE β<VAR>a : α<VAR>f₁ f₂ f₃ f₄ : Finset α → β<VAR>u : Finset α<VAR>hu : a ∉ u<VAR>h₁ : 0 ≤ f₁<VAR>h₂ : 0 ≤ f₂<VAR>h₃ : 0 ≤ f₃<VAR>h₄ : 0 ≤ f₄<VAR>h : ∀ ⦃s : Finset α⦄, s ⊆ insert a u → ∀ ⦃t : Finset α⦄, t ⊆ insert a u → f₁ s * f₂ t ≤ f₃ (s ∩ t) * f₄ (s ∪ t)<VAR>𝒜 ℬ : Finset (Finset α)<VAR>s : Finset α<GOAL>s ⊆ u → ∀ ⦃t : Finset α⦄, t ⊆ u → collapse 𝒜 a f₁ s * collapse ℬ a f₂ t ≤ collapse (𝒜 ⊼ ℬ) a f₃ (s ∩ t) * collapse (𝒜 ⊻ ℬ) a f₄ (s ∪ t)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>DecidableEq α<VAR>LinearOrderedCommSemiring β<VAR>𝒜 : Finset (Finset α)<VAR>a : α<VAR>f : Finset α → β<VAR>u : Finset α<VAR>h𝒜 : 𝒜 ⊆ (insert a u).powerset<VAR>hu : a ∉ u<GOAL>∑ s ∈ u.powerset, collapse 𝒜 a f s = ∑ s ∈ 𝒜, f s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>DecidableEq α<VAR>LinearOrderedCommSemiring β<VAR>ExistsAddOfLE β<VAR>f₁ f₂ f₃ f₄ : Finset α → β<VAR>u : Finset α<VAR>h₁ : 0 ≤ f₁<VAR>h₂ : 0 ≤ f₂<VAR>h₃ : 0 ≤ f₃<VAR>h₄ : 0 ≤ f₄<VAR>h : ∀ ⦃s : Finset α⦄, s ⊆ u → ∀ ⦃t : Finset α⦄, t ⊆ u → f₁ s * f₂ t ≤ f₃ (s ∩ t) * f₄ (s ∪ t)<VAR>𝒜 ℬ : Finset (Finset α)<VAR>h𝒜 : 𝒜 ⊆ u.powerset<VAR>hℬ : ℬ ⊆ u.powerset<GOAL>(∑ s ∈ 𝒜, f₁ s) * ∑ s ∈ ℬ, f₂ s ≤ (∑ s ∈ 𝒜 ⊼ ℬ, f₃ s) * ∑ s ∈ 𝒜 ⊻ ℬ, f₄ s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>DecidableEq α<VAR>LinearOrderedCommSemiring β<VAR>ExistsAddOfLE β<VAR>f₁ f₂ f₃ f₄ : Finset α → β<VAR>Fintype α<VAR>h₁ : 0 ≤ f₁<VAR>h₂ : 0 ≤ f₂<VAR>h₃ : 0 ≤ f₃<VAR>h₄ : 0 ≤ f₄<VAR>h : ∀ (s t : Finset α), f₁ s * f₂ t ≤ f₃ (s ∩ t) * f₄ (s ∪ t)<VAR>𝒜 ℬ : Finset (Finset α)<GOAL>(∑ s ∈ 𝒜, f₁ s) * ∑ s ∈ ℬ, f₂ s ≤ (∑ s ∈ 𝒜 ⊼ ℬ, f₃ s) * ∑ s ∈ 𝒜 ⊻ ℬ, f₄ s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>DistribLattice α<VAR>LinearOrderedCommSemiring β<VAR>ExistsAddOfLE β<VAR>f₁ f₂ f₃ f₄ : α → β<VAR>DecidableEq α<VAR>h₁ : 0 ≤ f₁<VAR>h₂ : 0 ≤ f₂<VAR>h₃ : 0 ≤ f₃<VAR>h₄ : 0 ≤ f₄<VAR>h : ∀ (a b : α), f₁ a * f₂ b ≤ f₃ (a ⊓ b) * f₄ (a ⊔ b)<VAR>s t : Finset α<GOAL>(∑ a ∈ s, f₁ a) * ∑ a ∈ t, f₂ a ≤ (∑ a ∈ s ⊼ t, f₃ a) * ∑ a ∈ s ⊻ t, f₄ a
<VAR>α : Type u_1<VAR>DistribLattice α<VAR>DecidableEq α<VAR>s t : Finset α<GOAL>s.card * t.card ≤ (s ⊼ t).card * (s ⊻ t).card
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>DistribLattice α<VAR>LinearOrderedCommSemiring β<VAR>ExistsAddOfLE β<VAR>f₁ f₂ f₃ f₄ : α → β<VAR>Fintype α<VAR>h₁ : 0 ≤ f₁<VAR>h₂ : 0 ≤ f₂<VAR>h₃ : 0 ≤ f₃<VAR>h₄ : 0 ≤ f₄<VAR>h : ∀ (a b : α), f₁ a * f₂ b ≤ f₃ (a ⊓ b) * f₄ (a ⊔ b)<GOAL>(∑ a : α, f₁ a) * ∑ a : α, f₂ a ≤ (∑ a : α, f₃ a) * ∑ a : α, f₄ a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>DistribLattice α<VAR>LinearOrderedCommSemiring β<VAR>ExistsAddOfLE β<VAR>f g μ : α → β<VAR>Fintype α<VAR>hμ₀ : 0 ≤ μ<VAR>hf : 0 ≤ f<VAR>hg : 0 ≤ g<VAR>hμ : Monotone μ<VAR>hfg : ∑ a : α, f a = ∑ a : α, g a<VAR>h : ∀ (a b : α), f a * g b ≤ f (a ⊓ b) * g (a ⊔ b)<GOAL>∑ a : α, μ a * f a ≤ ∑ a : α, μ a * g a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>DistribLattice α<VAR>LinearOrderedCommSemiring β<VAR>ExistsAddOfLE β<VAR>f g μ : α → β<VAR>Fintype α<VAR>hμ₀ : 0 ≤ μ<VAR>hf₀ : 0 ≤ f<VAR>hg₀ : 0 ≤ g<VAR>hf : Monotone f<VAR>hg : Monotone g<VAR>hμ : ∀ (a b : α), μ a * μ b ≤ μ (a ⊓ b) * μ (a ⊔ b)<GOAL>(∑ a : α, μ a * f a) * ∑ a : α, μ a * g a ≤ (∑ a : α, μ a) * ∑ a : α, μ a * (f a * g a)
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>GeneralizedBooleanAlgebra α<VAR>s t : Finset α<GOAL>s.card * t.card ≤ (s \\ t).card * (t \\ s).card
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>GeneralizedBooleanAlgebra α<VAR>s : Finset α<GOAL>s.card ≤ (s \\ s).card
<VAR>α : Type u<VAR>β : Type v<VAR>M : Type w<VAR>DecidableEq β<VAR>s : Finset α<VAR>t : Finset β<VAR>f : α → β<VAR>w : α → M<VAR>b : M<VAR>LinearOrderedCancelAddCommMonoid M<VAR>hf : ∀ a ∈ s, f a ∈ t<VAR>hb : t.card • b < ∑ x ∈ s, w x<GOAL>∃ y ∈ t, b < ∑ x ∈ Finset.filter (fun x => f x = y) s, w x
<VAR>α : Type u<VAR>β : Type v<VAR>M : Type w<VAR>DecidableEq β<VAR>s : Finset α<VAR>t : Finset β<VAR>f : α → β<VAR>w : α → M<VAR>b : M<VAR>LinearOrderedCancelAddCommMonoid M<VAR>hf : ∀ a ∈ s, f a ∈ t<VAR>hb : ∑ x ∈ s, w x < t.card • b<GOAL>∃ y ∈ t, ∑ x ∈ Finset.filter (fun x => f x = y) s, w x < b
<VAR>α : Type u<VAR>β : Type v<VAR>M : Type w<VAR>DecidableEq β<VAR>s : Finset α<VAR>t : Finset β<VAR>f : α → β<VAR>w : α → M<VAR>b : M<VAR>LinearOrderedCancelAddCommMonoid M<VAR>ht : ∀ y ∉ t, ∑ x ∈ Finset.filter (fun x => f x = y) s, w x ≤ 0<VAR>hb : t.card • b < ∑ x ∈ s, w x<GOAL>∃ y ∈ t, b < ∑ x ∈ Finset.filter (fun x => f x = y) s, w x
<VAR>α : Type u<VAR>β : Type v<VAR>M : Type w<VAR>DecidableEq β<VAR>s : Finset α<VAR>t : Finset β<VAR>f : α → β<VAR>w : α → M<VAR>b : M<VAR>LinearOrderedCancelAddCommMonoid M<VAR>ht : ∀ y ∉ t, 0 ≤ ∑ x ∈ Finset.filter (fun x => f x = y) s, w x<VAR>hb : ∑ x ∈ s, w x < t.card • b<GOAL>∃ y ∈ t, ∑ x ∈ Finset.filter (fun x => f x = y) s, w x < b