Graceful three-degree-3 trees

/- Proof body for Math15Catalog.source11. The verifier supplies its trusted
imports and surrounding namespace. -/
end Bounty

/- A proof of Math15Catalog.source11: trees with exactly three degree-three
vertices and all other degrees at most two admit graceful labelings. -/


/- Supporting module: H1Coverage -/

namespace H1Coverage

def U (a b : Nat) := a/2+b/2
def V (a b : Nat) := a+b-U a b
def Cut (a b d : Nat) := if d%2=0 then U a b+d/2 else V a b+d/2
def R (d c : Nat) := if d%2=1 then (d-1)/2+c/2 else d+c-((d-1)/2+c/2)-2

theorem big_tail_or_graft (a b d c : Nat) (ha : 1≤a) (hb : 1≤b)
    (hd : 1≤d) (hc : 2*d<c) (hnot : c<Cut a b d+1) :
    a+b > 2*R d c := by
  simp only [Cut, V, U, R] at *
  split_ifs at * <;> omega

theorem generic_finite_bound (q d c : Nat) (hd : 1≤d) (hd9 : d≤9)
    (hc : 1≤c) (hc2 : c≤2*d) (hnot : ¬ q>2*R d c) : q≤26 := by
  unfold R at hnot
  split_ifs at hnot <;> omega

theorem bad_path_outer_bound (a b : Nat) (ha : 1≤a) (hab : a≤b)
    (hnot : b<a/2+3) : a+b≤8 := by omega

def SmallShort (d c : Nat) :=
  if (c+1)/2=1 then 6≤d else 3*((c+1)/2)+1≤d

theorem q2_finite_bound (d c : Nat) (hd : 1≤d) (hc : 1≤c)
    (hnotlong : c<Cut 1 1 d+1) (hnotshort : ¬ SmallShort d c) :
    c≤9 ∧ d≤15 := by
  unfold SmallShort Cut U V at *
  split_ifs at * <;> omega

end H1Coverage


/- Supporting module: H1Outer -/

namespace H1Coverage

def OuterAvailable (a b d c : ℕ) : Prop :=
  ¬ (b+d=2 ∧ c=2) ∧
    (if d%2=0 then (b+d)/2+c/2 else b+d+c-((b+d)/2+c/2)) ≤ a

end H1Coverage


/- Supporting module: Foundation -/

namespace Math15.Graceful

theorem edgeCount_eq_card_edgeFinset {n : ℕ} (G : SimpleGraph (Fin n))
    [DecidableRel G.Adj] :
    edgeCount G = G.edgeFinset.card := by
  classical
  unfold edgeCount
  apply Finset.card_bij (fun e _ => s(e.1, e.2))
  · intro e he
    simp only [Finset.mem_filter, Finset.mem_univ, true_and] at he
    exact SimpleGraph.mem_edgeFinset.mpr (G.mem_edgeSet.mpr he.2)
  · intro e he e' he' heq
    simp only [Finset.mem_filter, Finset.mem_univ, true_and] at he he'
    rcases Sym2.eq_iff.mp heq with h | h
    · exact Prod.ext h.1 h.2
    · have hrev : e'.2 < e'.1 := by simpa [h.1, h.2] using he.1
      exact (lt_asymm he'.1 hrev).elim
  · intro e he
    induction e using Sym2.ind with | _ x y =>
    have hxy := G.mem_edgeSet.mp (SimpleGraph.mem_edgeFinset.mp he)
    rcases lt_trichotomy x y with hlt | heq | hgt
    · refine ⟨(x, y), ?_, rfl⟩
      simpa using And.intro hlt hxy
    · subst y
      exact (G.irrefl hxy).elim
    · refine ⟨(y, x), ?_, Sym2.eq_swap⟩
      simpa using And.intro hgt hxy.symm

theorem edgeCount_add_one_eq_of_isTree {n : ℕ} (G : SimpleGraph (Fin n))
    (hG : G.IsTree) : edgeCount G + 1 = n := by
  classical
  rw [edgeCount_eq_card_edgeFinset]
  simpa using hG.card_edgeFinset

theorem edgeCount_eq_of_isTree {n : ℕ} (G : SimpleGraph (Fin n))
    (hG : G.IsTree) : edgeCount G = n - 1 := by
  have := edgeCount_add_one_eq_of_isTree G hG
  omega

theorem degree_eq_graph_degree {n : ℕ} (G : SimpleGraph (Fin n))
    [DecidableRel G.Adj] (v : Fin n) : degree G v = G.degree v := by
  classical
  rw [← G.card_neighborFinset_eq_degree, G.neighborFinset_eq_filter]
  unfold degree
  congr 1
  ext w
  simp

theorem branch43_leaf_count {n : ℕ} (G : SimpleGraph (Fin n))
    (hG : G.IsTree) {u v : Fin n} (hbranch : Branch43 G u v) :
    (Finset.univ.filter (fun w => degree G w = 1)).card = 5 := by
  classical
  obtain ⟨huv, hu, hv, hrest⟩ := hbranch
  let : Nontrivial (Fin n) := ⟨⟨u, v, huv⟩⟩
  have hpos (w : Fin n) : 1 ≤ degree G w := by
    rw [degree_eq_graph_degree]
    exact hG.preconnected.degree_pos_of_nontrivial w
  have hpoint (w : Fin n) :
      degree G w + (if degree G w = 1 then 1 else 0) =
        2 + (if w = u then 2 else 0) + (if w = v then 1 else 0) := by
    by_cases hwu : w = u
    · subst w
      simp [hu, huv]
    by_cases hwv : w = v
    · subst w
      simp [hv, huv.symm]
    have := hrest w hwu hwv
    have := hpos w
    split_ifs <;> omega
  have hsum := congrArg (fun f : Fin n → ℕ => ∑ w, f w) (funext hpoint)
  have hdegrees : ∑ w : Fin n, degree G w = 2 * edgeCount G := by
    simp_rw [degree_eq_graph_degree, edgeCount_eq_card_edgeFinset]
    exact G.sum_degrees_eq_twice_card_edges
  have htree := edgeCount_add_one_eq_of_isTree G hG
  simp only [Finset.sum_add_distrib, Finset.sum_const, Finset.card_univ,
    Fintype.card_fin, smul_eq_mul, Finset.sum_ite_eq', Finset.mem_univ, ite_true,
    Finset.sum_boole] at hsum
  rw [hdegrees] at hsum
  norm_num at hsum
  omega

/-- For a finite graph, distinct nonzero edge differences bounded by the number
of edges necessarily give complete coverage. -/
theorem labeling_of_injective_differences {n : ℕ} (G : SimpleGraph (Fin n))
    (f : Fin n → ℕ) (hinj : Function.Injective f)
    (hbound : ∀ v, f v ≤ edgeCount G)
    (hdiff : ∀ e e' : Fin n × Fin n,
      e.1 < e.2 → G.Adj e.1 e.2 → e'.1 < e'.2 → G.Adj e'.1 e'.2 →
      Nat.dist (f e.1) (f e.2) = Nat.dist (f e'.1) (f e'.2) → e = e') :
    Function.Injective f ∧ (∀ v, f v ≤ edgeCount G) ∧
      (∀ d, 1 ≤ d → d ≤ edgeCount G →
        ∃! e : Fin n × Fin n, e.1 < e.2 ∧ G.Adj e.1 e.2 ∧
          Nat.dist (f e.1) (f e.2) = d) := by
  classical
  let edges : Finset (Fin n × Fin n) :=
    Finset.univ.filter (fun e => e.1 < e.2 ∧ G.Adj e.1 e.2)
  let diff : Fin n × Fin n → ℕ := fun e => Nat.dist (f e.1) (f e.2)
  have edges_card : edges.card = edgeCount G := rfl
  have image_card : (edges.image diff).card = edgeCount G := by
    rw [Finset.card_image_iff.mpr, edges_card]
    intro e he e' he' h
    simp [edges] at he he'
    exact hdiff e e' he.1 he.2 he'.1 he'.2 h
  have image_subset : edges.image diff ⊆ Finset.Icc 1 (edgeCount G) := by
    intro d hd
    obtain ⟨e, he, rfl⟩ := Finset.mem_image.mp hd
    simp only [edges, Finset.mem_filter, Finset.mem_univ, true_and] at he
    have hn : f e.1 ≠ f e.2 := fun h => (ne_of_lt he.1) (hinj h)
    have hpos := Nat.dist_pos_of_ne hn
    have h1 := hbound e.1
    have h2 := hbound e.2
    simp only [Finset.mem_Icc, diff]
    unfold Nat.dist at *
    omega
  have image_eq : edges.image diff = Finset.Icc 1 (edgeCount G) := by
    apply Finset.eq_of_subset_of_card_le image_subset
    simpa only [Nat.card_Icc, image_card, Nat.add_sub_cancel] using
      (le_refl (edgeCount G))
  refine ⟨hinj, hbound, ?_⟩
  intro d hlow hupp
  have hd : d ∈ edges.image diff := by rw [image_eq]; exact Finset.mem_Icc.mpr ⟨hlow, hupp⟩
  obtain ⟨e, he, hde⟩ := Finset.mem_image.mp hd
  simp only [edges, Finset.mem_filter, Finset.mem_univ, true_and] at he
  refine ⟨e, ⟨he.1, he.2, hde⟩, ?_⟩
  intro e' he'
  exact hdiff e' e he'.1 he'.2.1 he.1 he.2 (he'.2.2.trans hde.symm)


theorem isGraceful_of_injective_differences {n : ℕ} (G : SimpleGraph (Fin n))
    (f : Fin n → ℕ) (hinj : Function.Injective f)
    (hbound : ∀ v, f v ≤ edgeCount G)
    (hdiff : ∀ e e' : Fin n × Fin n,
      e.1 < e.2 → G.Adj e.1 e.2 → e'.1 < e'.2 → G.Adj e'.1 e'.2 →
      Nat.dist (f e.1) (f e.2) = Nat.dist (f e'.1) (f e'.2) → e = e') :
    IsGraceful G :=
  ⟨f, labeling_of_injective_differences G f hinj hbound hdiff⟩

end Math15.Graceful


/- Supporting module: Alpha -/

namespace Math15.Graceful

/-- Reverse the labels separately on the two sides of an alpha cut. -/
def reverseLabel (q k x : ℕ) : ℕ :=
  if x ≤ k then k - x else q + k + 1 - x

/-- Normalize the least high label to zero, swapping the two cut classes. -/
def normalizeHighLabel (q k x : ℕ) : ℕ :=
  if x ≤ k then q - k + x else x - k - 1

lemma reverseLabel_le {q k x : ℕ} (hk : k ≤ q) (hx : x ≤ q) :
    reverseLabel q k x ≤ q := by
  unfold reverseLabel
  split <;> omega

lemma reverseLabel_low_iff {q k x : ℕ} (hx : x ≤ q) :
    reverseLabel q k x ≤ k ↔ x ≤ k := by
  unfold reverseLabel
  split <;> omega

lemma reverseLabel_involutive {q k x : ℕ} (hx : x ≤ q) :
    reverseLabel q k (reverseLabel q k x) = x := by
  unfold reverseLabel
  split <;> split <;> omega

lemma reverseLabel_injective {q k x y : ℕ} (hx : x ≤ q) (hy : y ≤ q)
    (h : reverseLabel q k x = reverseLabel q k y) : x = y := by
  rw [← reverseLabel_involutive (k := k) hx, h, reverseLabel_involutive hy]

lemma reverseLabel_dist {q k x y : ℕ} (hx : x ≤ k) (hy : k < y) (hq : y ≤ q) :
    Nat.dist (reverseLabel q k x) (reverseLabel q k y) = q + 1 - Nat.dist x y := by
  simp only [reverseLabel, ite_eq_left hx, ite_eq_right (by omega : ¬ y ≤ k)]
  unfold Nat.dist
  omega

lemma normalizeHighLabel_le {q k x : ℕ} (hk : k < q) (hx : x ≤ q) :
    normalizeHighLabel q k x ≤ q := by
  unfold normalizeHighLabel
  split <;> omega

lemma normalizeHighLabel_low_iff {q k x : ℕ} (hk : k < q) (hx : x ≤ q) :
    normalizeHighLabel q k x ≤ q - k - 1 ↔ k < x := by
  unfold normalizeHighLabel
  split <;> omega

lemma normalizeHighLabel_injective {q k x y : ℕ} (hk : k < q)
    (hx : x ≤ q) (hy : y ≤ q)
    (h : normalizeHighLabel q k x = normalizeHighLabel q k y) : x = y := by
  unfold normalizeHighLabel at h
  split at h <;> split at h <;> omega

lemma normalizeHighLabel_dist {q k x y : ℕ} (hx : x ≤ k) (hy : k < y)
    (hq : y ≤ q) :
    Nat.dist (normalizeHighLabel q k x) (normalizeHighLabel q k y) =
      q + 1 - Nat.dist x y := by
  simp only [normalizeHighLabel, ite_eq_left hx, ite_eq_right (by omega : ¬ y ≤ k)]
  unfold Nat.dist
  omega

lemma reverseLabel_at_cut (q k : ℕ) : reverseLabel q k k = 0 := by
  simp [reverseLabel]

lemma normalizeHighLabel_at_cut (q k : ℕ) :
    normalizeHighLabel q k (k + 1) = 0 := by
  simp [Math15.Graceful.reverseLabel_at_cut, normalizeHighLabel]

/-- A specified witness for the target's graceful-labeling predicate. -/
def IsGracefulLabeling {n : ℕ} (G : SimpleGraph (Fin n)) (f : Fin n → ℕ) : Prop :=
  Function.Injective f ∧
  (∀ v, f v ≤ edgeCount G) ∧
  (∀ d, 1 ≤ d → d ≤ edgeCount G →
    ∃! e : Fin n × Fin n, e.1 < e.2 ∧ G.Adj e.1 e.2 ∧ Nat.dist (f e.1) (f e.2) = d)

lemma IsGracefulLabeling.isGraceful {n : ℕ} {G : SimpleGraph (Fin n)}
    {f : Fin n → ℕ} (hf : IsGracefulLabeling G f) : IsGraceful G := ⟨f, hf⟩

/-- A graceful labeling whose every edge crosses the indicated cut. -/
def IsAlphaLabeling {n : ℕ} (G : SimpleGraph (Fin n)) (f : Fin n → ℕ) (k : ℕ) : Prop :=
  IsGracefulLabeling G f ∧ k < edgeCount G ∧
  ∀ u v, G.Adj u v → (f u ≤ k ∧ k < f v) ∨ (f v ≤ k ∧ k < f u)

lemma IsGracefulLabeling.dist_le {n : ℕ} {G : SimpleGraph (Fin n)}
    {f : Fin n → ℕ} (hf : IsGracefulLabeling G f) (u v : Fin n) :
    Nat.dist (f u) (f v) ≤ edgeCount G := by
  have hu := hf.2.1 u
  have hv := hf.2.1 v
  unfold Nat.dist
  omega

/-- Complementing all edge differences permutes the required interval of edge labels. -/
lemma IsGracefulLabeling.of_dist_complement {n : ℕ} {G : SimpleGraph (Fin n)}
    {f g : Fin n → ℕ} (hf : IsGracefulLabeling G f)
    (hg_inj : Function.Injective g) (hg_bound : ∀ v, g v ≤ edgeCount G)
    (hcomp : ∀ u v, G.Adj u v →
      Nat.dist (g u) (g v) = edgeCount G + 1 - Nat.dist (f u) (f v)) :
    IsGracefulLabeling G g := by
  refine ⟨hg_inj, hg_bound, ?_⟩
  intro d hd hq
  obtain ⟨e, he, he_unique⟩ := hf.2.2 (edgeCount G + 1 - d) (by omega) (by omega)
  refine ⟨e, ⟨he.1, he.2.1, ?_⟩, ?_⟩
  · rw [hcomp e.1 e.2 he.2.1, he.2.2]
    omega
  · intro e' he'
    apply he_unique e'
    refine ⟨he'.1, he'.2.1, ?_⟩
    have hc := hcomp e'.1 e'.2 he'.2.1
    have hb := hf.dist_le e'.1 e'.2
    omega

lemma IsAlphaLabeling.reverse {n : ℕ} {G : SimpleGraph (Fin n)}
    {f : Fin n → ℕ} {k : ℕ} (hf : IsAlphaLabeling G f k) :
    IsAlphaLabeling G (fun v => reverseLabel (edgeCount G) k (f v)) k := by
  rcases hf with ⟨hf, hk, hcross⟩
  refine ⟨hf.of_dist_complement ?_ ?_ ?_, hk, ?_⟩
  · intro u v h
    exact hf.1 (reverseLabel_injective (hf.2.1 u) (hf.2.1 v) h)
  · intro v
    exact reverseLabel_le (Nat.le_of_lt hk) (hf.2.1 v)
  · intro u v hadj
    rcases hcross u v hadj with h | h
    · exact reverseLabel_dist h.1 h.2 (hf.2.1 v)
    · rw [Nat.dist_comm (reverseLabel _ _ _), Nat.dist_comm (f u)]
      exact reverseLabel_dist h.1 h.2 (hf.2.1 u)
  · intro u v hadj
    rcases hcross u v hadj with h | h
    · left
      constructor
      · exact (reverseLabel_low_iff (hf.2.1 u)).2 h.1
      · have := (reverseLabel_low_iff (k := k) (hf.2.1 v))
        dsimp only at *
        omega
    · right
      constructor
      · exact (reverseLabel_low_iff (hf.2.1 v)).2 h.1
      · have := (reverseLabel_low_iff (k := k) (hf.2.1 u))
        dsimp only at *
        omega

lemma IsAlphaLabeling.normalizeHigh {n : ℕ} {G : SimpleGraph (Fin n)}
    {f : Fin n → ℕ} {k : ℕ} (hf : IsAlphaLabeling G f k) :
    IsAlphaLabeling G (fun v => normalizeHighLabel (edgeCount G) k (f v))
      (edgeCount G - k - 1) := by
  rcases hf with ⟨hf, hk, hcross⟩
  refine ⟨hf.of_dist_complement ?_ ?_ ?_, by omega, ?_⟩
  · intro u v h
    exact hf.1 (normalizeHighLabel_injective hk (hf.2.1 u) (hf.2.1 v) h)
  · intro v
    exact normalizeHighLabel_le hk (hf.2.1 v)
  · intro u v hadj
    rcases hcross u v hadj with h | h
    · exact normalizeHighLabel_dist h.1 h.2 (hf.2.1 v)
    · rw [Nat.dist_comm (normalizeHighLabel _ _ _), Nat.dist_comm (f u)]
      exact normalizeHighLabel_dist h.1 h.2 (hf.2.1 u)
  · intro u v hadj
    rcases hcross u v hadj with h | h
    · right
      constructor
      · exact (normalizeHighLabel_low_iff hk (hf.2.1 v)).2 h.2
      · have := (normalizeHighLabel_low_iff hk (hf.2.1 u))
        dsimp only at *
        omega
    · left
      constructor
      · exact (normalizeHighLabel_low_iff hk (hf.2.1 u)).2 h.2
      · have := (normalizeHighLabel_low_iff hk (hf.2.1 v))
        dsimp only at *
        omega

/-- Either boundary label can be moved to zero while retaining an alpha labeling. -/
lemma IsAlphaLabeling.normalizePin {n : ℕ} {G : SimpleGraph (Fin n)}
    {f : Fin n → ℕ} {k : ℕ} (hf : IsAlphaLabeling G f k) (v : Fin n)
    (hpin : f v = k ∨ f v = k + 1) :
    ∃ g k', IsAlphaLabeling G g k' ∧ g v = 0 := by
  rcases hpin with h | h
  · refine ⟨fun x => reverseLabel (edgeCount G) k (f x), k, hf.reverse, ?_⟩
    simp [Math15.Graceful.reverseLabel_at_cut, Math15.Graceful.normalizeHighLabel_at_cut, h, reverseLabel]
  · refine ⟨fun x => normalizeHighLabel (edgeCount G) k (f x),
      edgeCount G - k - 1, hf.normalizeHigh, ?_⟩
    simp [Math15.Graceful.reverseLabel_at_cut, Math15.Graceful.normalizeHighLabel_at_cut, h, normalizeHighLabel]

/-- Insert a block of `m` unused labels immediately above an alpha cut. -/
def shiftAboveCut (k m x : ℕ) : ℕ := if x ≤ k then x else x + m

lemma shiftAboveCut_le {q k m x : ℕ} (hx : x ≤ q) :
    shiftAboveCut k m x ≤ q + m := by
  unfold shiftAboveCut
  split <;> omega

lemma shiftAboveCut_injective (k m : ℕ) : Function.Injective (shiftAboveCut k m) := by
  intro x y h
  unfold shiftAboveCut at h
  split at h <;> split at h <;> omega

lemma shiftAboveCut_dist {k m x y : ℕ} (hx : x ≤ k) (hy : k < y) :
    Nat.dist (shiftAboveCut k m x) (shiftAboveCut k m y) = m + Nat.dist x y := by
  simp only [shiftAboveCut, ite_eq_left hx, ite_eq_right (by omega : ¬ y ≤ k)]
  unfold Nat.dist
  omega

lemma translate_dist (k x y : ℕ) : Nat.dist (k + x) (k + y) = Nat.dist x y := by
  unfold Nat.dist
  omega

/-- After the shift, the inserted label interval meets the old labels only at the link. -/
lemma shiftAboveCut_eq_translate_iff {k m x y : ℕ} (hy : y ≤ m) :
    shiftAboveCut k m x = k + y ↔ x = k ∧ y = 0 := by
  unfold shiftAboveCut
  split <;> omega

lemma translate_le {q k m y : ℕ} (hk : k ≤ q) (hy : y ≤ m) : k + y ≤ q + m := by
  omega

/-- The two edge-label intervals in an amalgamation are disjoint. -/
lemma amalgamation_edge_intervals_disjoint {m d e : ℕ}
    (hd : 1 ≤ d) (he : e ≤ m) : m + d ≠ e := by
  omega

/-- The shifted graph's link and the inserted graph's zero label agree. -/
lemma shiftAboveCut_link (k m : ℕ) : shiftAboveCut k m k = k := by
  simp [Math15.Graceful.reverseLabel_at_cut, Math15.Graceful.normalizeHighLabel_at_cut, shiftAboveCut]

/-- Appending a path can join the old low endpoint using the new difference `m`. -/
lemma appendPath_low_endpoint {k m b : ℕ} (hb : b ≤ k) (hm : k + 1 - b ≤ m) :
    k + 1 ≤ b + m ∧ b + m ≤ k + m ∧
      Nat.dist (shiftAboveCut k m b) (b + m) = m := by
  simp only [shiftAboveCut, ite_eq_left hb]
  unfold Nat.dist
  omega

/-- Appending a path can join the old high endpoint using the new difference `m`. -/
lemma appendPath_high_endpoint {k m b : ℕ} (hb : k < b) (hm : b - k ≤ m) :
    k + 1 ≤ b ∧ b ≤ k + m ∧
      Nat.dist (shiftAboveCut k m b) b = m := by
  simp only [shiftAboveCut, ite_eq_right (by omega : ¬ b ≤ k)]
  unfold Nat.dist
  omega

end Math15.Graceful


/- Supporting module: SpiderCertificates -/


namespace Bounty

/-- The parent of vertex `j` in the vertex order used for S(2,2,L). -/
def spiderParent (j : ℕ) : ℕ :=
  if j = 1 ∨ j = 3 ∨ j = 5 then 0 else j - 1

lemma spiderParent_lt {j : ℕ} (hj : 0 < j) : spiderParent j < j := by
  unfold spiderParent
  split <;> omega

/-- Vertices 0,1,2,3,4 are the hub and the two length-two arms. -/
def spider (L : ℕ) : SimpleGraph (Fin (L + 5)) where
  Adj i j := (i.val < j.val ∧ spiderParent j.val = i.val) ∨
    (j.val < i.val ∧ spiderParent i.val = j.val)
  symm := ⟨fun _ _ h => h.symm⟩
  loopless := ⟨by intro i; simp [Math15.Graceful.reverseLabel_at_cut, Math15.Graceful.normalizeHighLabel_at_cut, Math15.Graceful.shiftAboveCut_link]⟩

abbrev spiderAdjDecidable (L : ℕ) : DecidableRel (spider L).Adj := fun _ _ => inferInstanceAs
  (Decidable ((_ ∧ _) ∨ (_ ∧ _)))


lemma spider_edgeCount (L : ℕ) : Math15.Graceful.edgeCount (spider L) = L + 4 := by
  classical
  unfold Math15.Graceful.edgeCount
  let es : Finset (Fin (L+5) × Fin (L+5)) := Finset.univ.filter
    (fun e => e.1 < e.2 ∧ (spider L).Adj e.1 e.2)
  let verts : Finset (Fin (L+5)) := Finset.univ.filter (fun j => 0 < j.val)
  have hc : es.card = verts.card := by
    apply Finset.card_bij (fun e _ => e.2)
    · intro e he
      simp only [es, Finset.mem_filter, Finset.mem_univ, true_and] at he
      simp only [verts, Finset.mem_filter, Finset.mem_univ, true_and]
      exact Nat.lt_of_le_of_lt (Nat.zero_le e.1.val) he.1
    · intro a ha b hb heq
      simp only [es, Finset.mem_filter, Finset.mem_univ, true_and] at ha hb
      have hpa : spiderParent a.2.val = a.1.val := by
        rcases ha.2 with h | h
        · exact h.2
        · exact False.elim (Nat.lt_asymm ha.1 h.1)
      have hpb : spiderParent b.2.val = b.1.val := by
        rcases hb.2 with h | h
        · exact h.2
        · exact False.elim (Nat.lt_asymm hb.1 h.1)
      apply Prod.ext _ heq
      apply Fin.ext
      rw [← hpa, ← hpb, heq]
    · intro j hj
      simp only [verts, Finset.mem_filter, Finset.mem_univ, true_and] at hj
      let i : Fin (L+5) := ⟨spiderParent j.val, (spiderParent_lt hj).trans j.isLt⟩
      refine ⟨(i,j), ?_, rfl⟩
      simp only [es, Finset.mem_filter, Finset.mem_univ, true_and]
      exact ⟨spiderParent_lt hj, Or.inl ⟨spiderParent_lt hj, rfl⟩⟩
  have hv : verts = Finset.univ.erase (0 : Fin (L+5)) := by
    ext j
    simp only [verts, Finset.mem_filter, Finset.mem_univ, true_and,
      Finset.mem_erase, and_true]
    constructor
    · intro hj hzero
      subst j