Grace/Cumulus/GraphTheory/Friendship.g17

Open in Workbench Download source

Imports

Basic · Combinatorics.Partitions

Declarations

Source

1-- Friendship graphs: every two distinct vertices have exactly one common2-- neighbour. Two non-adjacent vertices have the same degree, since sending3-- a neighbour w of u to the common neighbour of w and v is injective; and4-- when no vertex is adjacent to all others, every vertex has the same5-- degree. Hence a finite friendship graph with two vertices of different6-- degree has a vertex adjacent to all others.7-- Part of Cumulus, the Grace17 mathematics library.8-- Copyright (c) 2026 Grant Passmore.9-- Released under the Apache License 2.0. See LICENSE in the repository root.10-- Authors: Grant Passmore1112module Grace.Cumulus.GraphTheory.Friendship13import Basic14import Combinatorics.Partitions1516-- Every two distinct vertices have exactly one common neighbour.17predicate Friendship (V E : Set) :=18  SimpleGraph(V, E) ∧ (∀ x ∈ V, ∀ y ∈ V, x ≠ y →19    ∃ z, neighbors(V, E, x) ∩ neighbors(V, E, y) = {z})2021theorem Friendship.graph (V E : Set)22  requires friendship : Friendship(V, E)23  shows SimpleGraph(V, E)24proof25  obtain ⟨graph, common⟩ := friendship26  exact graph2728theorem Friendship.common (V E x y : Set)29  requires friendship : Friendship(V, E)30  requires hx : x ∈ V31  requires hy : y ∈ V32  requires distinct : x ≠ y33  shows ∃ z, neighbors(V, E, x) ∩ neighbors(V, E, y) = {z}34proof35  obtain ⟨graph, common⟩ := friendship36  exact common with x, hx, y, hy, distinct3738theorem neighbors.subset_vertices (V E x : Set)39  shows neighbors(V, E, x) ⊆ V40proof41  intros y hy42  have parts := neighbors.membership.forward with hy43  exact parts.left4445theorem neighbors.finite (V E x : Set)46  requires finite : Finite(V)47  shows Finite(neighbors(V, E, x))48proof49  exact Finite.subset with finite, (neighbors.subset_vertices at V, E, x)5051-- The common neighbour of two distinct vertices.52defunique commonNeighbor (V E x y : Set) (z ∈ V) :=53  neighbors(V, E, x) ∩ neighbors(V, E, y) = {z}54requires friendship : Friendship(V, E)55requires hx : x ∈ V56requires hy : y ∈ V57requires distinct : x ≠ y58proof59  obtain ⟨z, shape⟩ := Friendship.common with friendship, hx, hy, distinct60  have zIn : z ∈ neighbors(V, E, x) ∩ neighbors(V, E, y)61    rw shape62    exact singleton.self at z63  have both := intersection.membership.forward with zIn64  have parts := neighbors.membership.forward with both.left65  exact ⟨z, parts.left, shape⟩66uniqueness67  intros u hu first v hv second68  have uIn : u ∈ {v}69    rw [← second, first]70    exact singleton.self at u71  exact singleton.membership.forward with uIn7273section CommonNeighbor74variable (V E x y : Set)75hypothesis friendship : Friendship(V, E)76hypothesis hx : x ∈ V77hypothesis hy : y ∈ V78hypothesis distinct : x ≠ y7980theorem commonNeighbor.member81  shows commonNeighbor(V, E, x, y) ∈ V82proof83  have selected := commonNeighbor.selected at V, E, x, y with *84  exact selected.left8586theorem commonNeighbor.shape87  shows neighbors(V, E, x) ∩ neighbors(V, E, y) = {commonNeighbor(V, E, x, y)}88proof89  have selected := commonNeighbor.selected at V, E, x, y with *90  exact selected.right9192theorem commonNeighbor.adjacent_left93  shows Adjacent(E, x, commonNeighbor(V, E, x, y))94proof95  have shape := commonNeighbor.shape at V, E, x, y with *96  have inside := singleton.self at commonNeighbor(V, E, x, y)97  rw ← shape at inside98  have both := intersection.membership.forward with inside99  have parts := neighbors.membership.forward with both.left100  exact parts.right101102theorem commonNeighbor.adjacent_right103  shows Adjacent(E, y, commonNeighbor(V, E, x, y))104proof105  have shape := commonNeighbor.shape at V, E, x, y with *106  have inside := singleton.self at commonNeighbor(V, E, x, y)107  rw ← shape at inside108  have both := intersection.membership.forward with inside109  have parts := neighbors.membership.forward with both.right110  exact parts.right111112-- Any vertex adjacent to both x and y is their common neighbour.113theorem commonNeighbor.of_adjacent (w : Set)114  requires hw : w ∈ V115  requires left : Adjacent(E, x, w)116  requires right : Adjacent(E, y, w)117  shows w = commonNeighbor(V, E, x, y)118proof119  have shape := commonNeighbor.shape at V, E, x, y with *120  have inLeft : w ∈ neighbors(V, E, x) :=121    neighbors.membership.backward with ⟨hw, left⟩122  have inRight : w ∈ neighbors(V, E, y) :=123    neighbors.membership.backward with ⟨hw, right⟩124  have inside : w ∈ neighbors(V, E, x) ∩ neighbors(V, E, y) :=125    intersection.membership.backward with ⟨inLeft, inRight⟩126  rw shape at inside127  exact singleton.membership.forward with inside128129end CommonNeighbor130131-- For non-adjacent u and v, a neighbour w of u is sent to the common132-- neighbour of w and v; this is an injection of the neighbourhoods.133defgraph friendMap (V E u v : Set) (w ∈ neighbors(V, E, u)) :134    neighbors(V, E, v) :=135  commonNeighbor(V, E, w, v)136requires friendship : Friendship(V, E)137requires hv : v ∈ V138requires apart : ¬Adjacent(E, u, v)139proof140  obtain ⟨wIn, edge⟩ := neighbors.membership.forward with member141  have wv : w ≠ v142    intro same143    rw same at edge144    exact apart with edge145  have inV := commonNeighbor.member at V, E, w, v with friendship, wIn, hv, wv146  have adjacent := commonNeighbor.adjacent_right at V, E, w, v with147    friendship, wIn, hv, wv148  exact neighbors.membership.backward with ⟨inV, adjacent⟩149150theorem friendMap.injective (V E u v : Set)151  requires friendship : Friendship(V, E)152  requires hu : u ∈ V153  requires hv : v ∈ V154  requires apart : ¬Adjacent(E, u, v)155  shows InjectiveBetween(friendMap(V, E, u, v), neighbors(V, E, u),156    neighbors(V, E, v))157proof158  have graph := Friendship.graph with friendship159  have function := friendMap.function at V, E, u, v with friendship, hv, apart160  apply Injective.of_pointwise with function161  intros w hw w2 hw2 same162  obtain ⟨wIn, edgeW⟩ := neighbors.membership.forward with hw163  obtain ⟨wIn2, edgeW2⟩ := neighbors.membership.forward with hw2164  have wv : w ≠ v165    intro equal166    rw equal at edgeW167    exact apart with edgeW168  have wv2 : w2 ≠ v169    intro equal170    rw equal at edgeW2171    exact apart with edgeW2172  have valueW := friendMap.value at V, E, u, v, w with friendship, hv, apart, hw173  have valueW2 := friendMap.value at V, E, u, v, w2 with174    friendship, hv, apart, hw2175  rw [valueW, valueW2] at same176  have zIn := commonNeighbor.member at V, E, w, v with friendship, wIn, hv, wv177  have zW := commonNeighbor.adjacent_left at V, E, w, v with178    friendship, wIn, hv, wv179  have zW2 := commonNeighbor.adjacent_left at V, E, w2, v with180    friendship, wIn2, hv, wv2181  rw ← same at zW2182  have zV := commonNeighbor.adjacent_right at V, E, w, v with183    friendship, wIn, hv, wv184  have uz : u ≠ commonNeighbor(V, E, w, v)185    intro equal186    rw ← equal at zV187    exact apart with (Adjacent.symmetric with graph, zV)188  have zWBack := Adjacent.symmetric with graph, zW189  have zW2Back := Adjacent.symmetric with graph, zW2190  have first := commonNeighbor.of_adjacent at191    V, E, u, commonNeighbor(V, E, w, v), w with192    friendship, hu, zIn, uz, wIn, edgeW, zWBack193  have second := commonNeighbor.of_adjacent at194    V, E, u, commonNeighbor(V, E, w, v), w2 with195    friendship, hu, zIn, uz, wIn2, edgeW2, zW2Back196  rw first197  symm198  exact second199200-- Non-adjacent vertices have the same degree.201theorem Friendship.degree_le_of_not_adjacent (V E u v : Set)202  requires friendship : Friendship(V, E)203  requires finite : Finite(V)204  requires hu : u ∈ V205  requires hv : v ∈ V206  requires apart : ¬Adjacent(E, u, v)207  shows cardinality(neighbors(V, E, u)) ≤ cardinality(neighbors(V, E, v))208proof209  have injective := friendMap.injective with friendship, hu, hv, apart210  exact Injective.cardinality_le with injective,211    (neighbors.finite at V, E, v with finite)212213theorem Friendship.degree_eq_of_not_adjacent (V E u v : Set)214  requires friendship : Friendship(V, E)215  requires finite : Finite(V)216  requires hu : u ∈ V217  requires hv : v ∈ V218  requires apart : ¬Adjacent(E, u, v)219  shows cardinality(neighbors(V, E, u)) = cardinality(neighbors(V, E, v))220proof221  have graph := Friendship.graph with friendship222  have apartV : ¬Adjacent(E, v, u)223    intro edge224    exact apart with (Adjacent.symmetric with graph, edge)225  have le := Friendship.degree_le_of_not_adjacent with226    friendship, finite, hu, hv, apart227  have ge := Friendship.degree_le_of_not_adjacent with228    friendship, finite, hv, hu, apartV229  have natU := cardinality.nat with (neighbors.finite at V, E, u with finite)230  have natV := cardinality.nat with (neighbors.finite at V, E, v with finite)231  exact LessEqual.antisymmetric with le, ge232233-- When no vertex is adjacent to all others, every vertex has the degree of234-- a given vertex u with a non-neighbour v: a vertex other than the common235-- neighbour of u and v is non-adjacent to one of them, and the common236-- neighbour has a non-neighbour of its own.237theorem Friendship.degree_eq_all (V E u v : Set)238  requires friendship : Friendship(V, E)239  requires finite : Finite(V)240  requires hu : u ∈ V241  requires hv : v ∈ V242  requires distinct : u ≠ v243  requires apart : ¬Adjacent(E, u, v)244  requires noUniversal : ∀ x ∈ V, ∃ y ∈ V, y ≠ x ∧ ¬Adjacent(E, x, y)245  shows ∀ z ∈ V,246    cardinality(neighbors(V, E, z)) = cardinality(neighbors(V, E, u))247proof248  have graph := Friendship.graph with friendship249  have sameUV := Friendship.degree_eq_of_not_adjacent with250    friendship, finite, hu, hv, apart251  have others : ∀ z ∈ V, z ≠ commonNeighbor(V, E, u, v) →252      cardinality(neighbors(V, E, z)) = cardinality(neighbors(V, E, u))253    intros z hz zc254    have caseU : z = u ∨ z ≠ u by tauto255    cases caseU with isU | notU256    . rw isU257      rfl258    . have adjacentU : Adjacent(E, u, z) ∨ ¬Adjacent(E, u, z) by tauto259      cases adjacentU with uz | notUZ260      . have caseV : z = v ∨ z ≠ v by tauto261        cases caseV with isV | notV262        . rw isV263          symm264          exact sameUV265        . have adjacentV : Adjacent(E, v, z) ∨ ¬Adjacent(E, v, z) by tauto266          cases adjacentV with vz | notVZ267          . exfalso268            apply zc269            exact commonNeighbor.of_adjacent at V, E, u, v, z with270              friendship, hu, hv, distinct, hz, uz, vz271          . have sameVZ := Friendship.degree_eq_of_not_adjacent at V, E, v, z272              with friendship, finite, hv, hz, notVZ273            rw ← sameVZ274            symm275            exact sameUV276      . have sameUZ := Friendship.degree_eq_of_not_adjacent at V, E, u, z with277          friendship, finite, hu, hz, notUZ278        symm279        exact sameUZ280  intros z hz281  have caseC : z = commonNeighbor(V, E, u, v) ∨ z ≠ commonNeighbor(V, E, u, v)282    tauto283  cases caseC with isC | notC284  . have cIn := commonNeighbor.member at V, E, u, v with285      friendship, hu, hv, distinct286    obtain ⟨y, hy, yc, apartC⟩ :=287      noUniversal with commonNeighbor(V, E, u, v), cIn288    have sameCY := Friendship.degree_eq_of_not_adjacent at289      V, E, commonNeighbor(V, E, u, v), y with290      friendship, finite, cIn, hy, apartC291    rw [isC, sameCY]292    exact others with y, hy, yc293  . exact others with z, hz, notC294295-- Without a vertex adjacent to all others, a finite friendship graph is296-- regular.297theorem Friendship.regular (V E : Set)298  requires friendship : Friendship(V, E)299  requires finite : Finite(V)300  requires noUniversal : ∀ x ∈ V, ∃ y ∈ V, y ≠ x ∧ ¬Adjacent(E, x, y)301  shows ∀ x ∈ V, ∀ y ∈ V,302    cardinality(neighbors(V, E, x)) = cardinality(neighbors(V, E, y))303proof304  intros x hx y hy305  obtain ⟨v, hv, vx, apart⟩ := noUniversal with x, hx306  have xv : x ≠ v307    intro same308    apply vx309    symm310    exact same311  have all := Friendship.degree_eq_all at V, E, x, v with312    friendship, finite, hx, hv, xv, apart, noUniversal313  symm314  exact all with y, hy315316-- The combinatorial half of the friendship theorem: a finite friendship317-- graph with two vertices of different degree has a vertex adjacent to all318-- others.319theorem Friendship.universal_of_irregular (V E x y : Set)320  requires friendship : Friendship(V, E)321  requires finite : Finite(V)322  requires hx : x ∈ V323  requires hy : y ∈ V324  requires different :325    cardinality(neighbors(V, E, x)) ≠ cardinality(neighbors(V, E, y))326  shows ∃ u ∈ V, ∀ w ∈ V, w ≠ u → Adjacent(E, u, w)327proof328  by_contra none329  have noUniversal : ∀ u ∈ V, ∃ w ∈ V, w ≠ u ∧ ¬Adjacent(E, u, w)330    intros u hu331    by_contra missing332    apply none333    refine ⟨u, hu, ?_⟩334    intros w hw wu335    by_contra apart336    apply missing337    exact ⟨w, hw, wu, apart⟩338  have regular := Friendship.regular with friendship, finite, noUniversal339  exact different with (regular with x, hx, y, hy)340341-- Counting the vertices of a regular friendship graph. Every vertex other342-- than x is adjacent to exactly one neighbour of x, its common neighbour343-- with x, so the spokes (z, y) with z a neighbour of x and y a neighbour of344-- z other than x correspond to the vertices other than x; each of the k345-- neighbours z of x carries k − 1 of them, hence |V| = k(k − 1) + 1.346347def spokes (V E x : Set) : Set :=348  { p ∈ neighbors(V, E, x) × V | ∃ z ∈ neighbors(V, E, x), ∃ y ∈ V,349      p = (z, y) ∧ Adjacent(E, z, y) ∧ y ≠ x }350351theorem spokes.pair (V E x z y : Set)352  shows (z, y) ∈ spokes(V, E, x) ↔353    z ∈ neighbors(V, E, x) ∧ y ∈ V ∧ Adjacent(E, z, y) ∧ y ≠ x354proof355  constructor356  . intro member357    obtain ⟨bound, u, hu, w, hw, shape, edge, away⟩ :=358      spokes.membership.forward with member359    have coordinates := orderedPair.injective with shape360    rw [coordinates.left, coordinates.right]361    exact ⟨hu, hw, edge, away⟩362  . intro parts363    obtain ⟨hz, hy, edge, away⟩ := parts364    apply spokes.membership.backward365    refine ⟨(product.pair with hz, hy), z, hz, y, hy, rfl, edge, away⟩366367theorem spokes.finite (V E x : Set)368  requires finite : Finite(V)369  shows Finite(spokes(V, E, x))370proof371  have product := Finite.product with (neighbors.finite at V, E, x with finite),372    finite373  have subset : spokes(V, E, x) ⊆ neighbors(V, E, x) × V374    intros p hp375    have parts := spokes.membership.forward with hp376    exact parts.left377  exact Finite.subset with product, subset378379-- A vertex y other than x determines the spoke through its common380-- neighbour with x.381defgraph spokeOf (V E x : Set) (y ∈ V ∖ {x}) : spokes(V, E, x) :=382  (commonNeighbor(V, E, x, y), y)383requires friendship : Friendship(V, E)384requires hx : x ∈ V385proof386  have graph := Friendship.graph with friendship387  obtain ⟨hy, yx⟩ := difference.singleton_membership.forward with member388  have xy : x ≠ y389    intro same390    apply yx391    symm392    exact same393  have cIn := commonNeighbor.member at V, E, x, y with friendship, hx, hy, xy394  have cx := commonNeighbor.adjacent_left at V, E, x, y with395    friendship, hx, hy, xy396  have cy := commonNeighbor.adjacent_right at V, E, x, y with397    friendship, hx, hy, xy398  have inNeighbors : commonNeighbor(V, E, x, y) ∈ neighbors(V, E, x) :=399    neighbors.membership.backward with ⟨cIn, cx⟩400  apply spokes.pair.backward401  exact ⟨inNeighbors, hy, (Adjacent.symmetric with graph, cy), yx⟩402403theorem spokeOf.bijective (V E x : Set)404  requires friendship : Friendship(V, E)405  requires hx : x ∈ V406  shows BijectiveBetween(spokeOf(V, E, x), V ∖ {x}, spokes(V, E, x))407proof408  have graph := Friendship.graph with friendship409  have function := spokeOf.function at V, E, x with friendship, hx410  constructor411  . apply Injective.of_pointwise with function412    intros y hy w hw same413    have valueY := spokeOf.value at V, E, x, y with friendship, hx, hy414    have valueW := spokeOf.value at V, E, x, w with friendship, hx, hw415    rw [valueY, valueW] at same416    have coordinates := orderedPair.injective with same417    exact coordinates.right418  . unfold SurjectiveBetween419    refine ⟨function, ?_⟩420    intros p hp421    obtain ⟨bound, z, hz, y, hy, shape, edge, away⟩ :=422      spokes.membership.forward with hp423    have yIn : y ∈ V ∖ {x} :=424      difference.singleton_membership.backward with ⟨hy, away⟩425    have xy : x ≠ y426      intro same427      apply away428      symm429      exact same430    obtain ⟨zIn, zx⟩ := neighbors.membership.forward with hz431    have chosen := commonNeighbor.of_adjacent at V, E, x, y, z with432      friendship, hx, hy, xy, zIn, zx, (Adjacent.symmetric with graph, edge)433    have value := spokeOf.value at V, E, x, y with friendship, hx, yIn434    refine ⟨y, yIn, ?_⟩435    have related := FunctionBetween.relates_apply with function, yIn436    rw [value, ← chosen, ← shape] at related437    exact related438439theorem spokes.count (V E x : Set)440  requires friendship : Friendship(V, E)441  requires finite : Finite(V)442  requires hx : x ∈ V443  shows cardinality(V ∖ {x}) = cardinality(spokes(V, E, x))444proof445  have finiteRest := Finite.subset with finite,446    (difference.subset_left at V, {x})447  exact cardinality.bijective with finiteRest,448    (spokeOf.bijective with friendship, hx)449450-- The first coordinate of a spoke.451defunique spokeStartPoint (V E x p : Set) (z ∈ neighbors(V, E, x)) :=452  ∃ y, p = (z, y)453requires member : p ∈ spokes(V, E, x)454proof455  obtain ⟨bound, z, hz, y, hy, shape, edge, away⟩ :=456    spokes.membership.forward with member457  exact ⟨z, hz, y, shape⟩458uniqueness459  intros u hu first v hv second460  obtain ⟨y, shapeY⟩ := first461  obtain ⟨w, shapeW⟩ := second462  have same : (u, y) = (v, w) by cc463  have coordinates := orderedPair.injective with same464  exact coordinates.left465466defgraph spokeStart (V E x : Set) (p ∈ spokes(V, E, x)) : neighbors(V, E, x) :=467  spokeStartPoint(V, E, x, p)468proof469  have selected := spokeStartPoint.selected at V, E, x, p with member470  exact selected.left471472theorem spokeStart.pair (V E x z y : Set)473  requires member : (z, y) ∈ spokes(V, E, x)474  shows spokeStart(V, E, x)((z, y)) = z475proof476  have selected := spokeStartPoint.selected at V, E, x, (z, y) with member477  obtain ⟨w, shape⟩ := selected.right478  have coordinates := orderedPair.injective with shape479  have value := spokeStart.value at V, E, x, (z, y) with member480  rw value481  symm482  exact coordinates.left483484-- The spokes through a neighbour z of x are its neighbours other than x.485defgraph spokeAt (V E x z : Set) (y ∈ neighbors(V, E, z) ∖ {x}) :486    functionPreimage(spokeStart(V, E, x), spokes(V, E, x), {z}) :=487  (z, y)488requires hz : z ∈ neighbors(V, E, x)489proof490  obtain ⟨hy, away⟩ := difference.singleton_membership.forward with member491  obtain ⟨yIn, edge⟩ := neighbors.membership.forward with hy492  have spoke : (z, y) ∈ spokes(V, E, x) :=493    spokes.pair.backward with ⟨hz, yIn, edge, away⟩494  have start := spokeStart.pair with spoke495  exact functionPreimage.point_membership.backward with ⟨spoke, start⟩496497theorem spokeAt.bijective (V E x z : Set)498  requires hz : z ∈ neighbors(V, E, x)499  shows BijectiveBetween(spokeAt(V, E, x, z), neighbors(V, E, z) ∖ {x},500    functionPreimage(spokeStart(V, E, x), spokes(V, E, x), {z}))501proof502  have function := spokeAt.function at V, E, x, z with hz503  constructor504  . apply Injective.of_pointwise with function505    intros y hy w hw same506    have valueY := spokeAt.value at V, E, x, z, y with hz, hy507    have valueW := spokeAt.value at V, E, x, z, w with hz, hw508    rw [valueY, valueW] at same509    have coordinates := orderedPair.injective with same510    exact coordinates.right511  . unfold SurjectiveBetween512    refine ⟨function, ?_⟩513    intros p hp514    obtain ⟨spoke, start⟩ := functionPreimage.point_membership.forward with hp515    obtain ⟨bound, u, hu, y, hy, shape, edge, away⟩ :=516      spokes.membership.forward with spoke517    rw shape at start518    have spokeU : (u, y) ∈ spokes(V, E, x) :=519      spokes.pair.backward with ⟨hu, hy, edge, away⟩520    have first := spokeStart.pair at V, E, x, u, y with spokeU521    rw first at start522    have yIn : y ∈ neighbors(V, E, z) ∖ {x}523      apply difference.singleton_membership.backward524      rw ← start525      exact ⟨neighbors.membership.backward with ⟨hy, edge⟩, away⟩526    refine ⟨y, yIn, ?_⟩527    have value := spokeAt.value at V, E, x, z, y with hz, yIn528    have related := FunctionBetween.relates_apply with function, yIn529    rw value at related530    rw [shape, start]531    exact related532533-- The number of vertices of a regular friendship graph.534theorem Friendship.vertex_count (V E x : Set)535  requires friendship : Friendship(V, E)536  requires finite : Finite(V)537  requires hx : x ∈ V538  requires regular : ∀ y ∈ V,539    cardinality(neighbors(V, E, y)) = cardinality(neighbors(V, E, x))540  shows cardinality(V) =541    cardinality(neighbors(V, E, x)) * (cardinality(neighbors(V, E, x)) - 1) + 1542proof543  have graph := Friendship.graph with friendship544  have finiteSpokes := spokes.finite at V, E, x with finite545  have finiteNeighbors := neighbors.finite at V, E, x with finite546  have natDegree := cardinality.nat with finiteNeighbors547  have start := spokeStart.function at V, E, x548  have total := cardinality.sum_of_preimages with start, finiteSpokes,549    finiteNeighbors550  have agree : ∀ z ∈ neighbors(V, E, x),551      preimageSize(spokeStart(V, E, x), spokes(V, E, x),552        neighbors(V, E, x))(z) = cardinality(neighbors(V, E, x)) - 1553    intros z hz554    have value := preimageSize.value at555      spokeStart(V, E, x), spokes(V, E, x), neighbors(V, E, x), z with556      finiteSpokes, hz557    obtain ⟨zIn, edge⟩ := neighbors.membership.forward with hz558    have back := Adjacent.symmetric with graph, edge559    have xInZ : x ∈ neighbors(V, E, z) :=560      neighbors.membership.backward with ⟨hx, back⟩561    have finiteZ := neighbors.finite at V, E, z with finite562    have finiteRest := Finite.subset with finiteZ,563      (difference.subset_left at neighbors(V, E, z), {x})564    have fiber := cardinality.bijective with finiteRest,565      (spokeAt.bijective at V, E, x, z with hz)566    have removed := cardinality.remove_sub_one with finiteZ, xInZ567    have degreeZ := regular with z, zIn568    rw [value, ← fiber, removed, degreeZ]569    rfl570  have sum := natSum.constant with finiteNeighbors, agree571  have removedX := cardinality.remove_add_one with finite, hx572  have count := spokes.count with friendship, finite, hx573  rw [removedX, count, total, sum]574  rfl575