Graceful degree-4-degree-3 trees

/-
Math15Catalog.source10 — declaration-only challenge submission.
Submit this file's contents directly. The challenge supplies its trusted imports
and outer Bounty namespace. Checked with Lean 4.35.0-rc2.
-/
end Bounty

/- Foundation -/
section
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
end

/- DoubleSpider -/
section
namespace Bounty

/-- A graph whose positive vertices each have a single lower-indexed parent. -/
def parentGraph (N : ℕ) (parent : ℕ → ℕ) : SimpleGraph (Fin (N + 1)) where
  Adj i j := (i.val < j.val ∧ parent j.val = i.val) ∨
    (j.val < i.val ∧ parent i.val = j.val)
  symm := ⟨fun _ _ h => h.symm⟩
  loopless := ⟨by intro i; simp⟩

theorem parentGraph_edgeCount (N : ℕ) (parent : ℕ → ℕ)
    (hp : ∀ j, 0 < j → j ≤ N → parent j < j) :
    Math15.Graceful.edgeCount (parentGraph N parent) = N := by
  classical
  unfold Math15.Graceful.edgeCount
  let es : Finset (Fin (N+1) × Fin (N+1)) := Finset.univ.filter
    (fun e => e.1 < e.2 ∧ (parentGraph N parent).Adj e.1 e.2)
  let verts : Finset (Fin (N+1)) := 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 : parent 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 : parent 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
      have hpj := hp j.val hj (by omega)
      let i : Fin (N+1) := ⟨parent j.val, hpj.trans j.isLt⟩
      refine ⟨(i,j), ?_, rfl⟩
      simp only [es, Finset.mem_filter, Finset.mem_univ, true_and]
      exact ⟨hpj, Or.inl ⟨hpj, rfl⟩⟩
  have hv : verts = Finset.univ.erase (0 : Fin (N+1)) := 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
      norm_num at hj
    · intro hj
      by_contra hzero
      apply hj
      apply Fin.ext
      have : j.val = 0 := by omega
      simpa using this
  have hcard : verts.card = N := by rw [hv]; simp
  calc
    _ = es.card := by rfl
    _ = N := hc.trans hcard

theorem parentGraph_connected (N : ℕ) (parent : ℕ → ℕ)
    (hp : ∀ j, 0 < j → j ≤ N → parent j < j) :
    (parentGraph N parent).Connected := by
  have hroot (k : ℕ) : ∀ hk : k < N+1,
      (parentGraph N parent).Reachable 0 ⟨k, hk⟩ := by
    induction k using Nat.strong_induction_on with | h k ih =>
    intro hk
    by_cases hzero : k = 0
    · subst k
      exact SimpleGraph.Reachable.refl _
    have hkpos : 0 < k := by omega
    have hpk := hp k hkpos (by omega)
    have hparent := ih (parent k) hpk (hpk.trans hk)
    apply hparent.trans
    apply SimpleGraph.Adj.reachable
    exact Or.inl ⟨hpk, rfl⟩
  refine ⟨fun u v => ?_⟩
  exact (hroot u.val u.isLt).symm.trans (hroot v.val v.isLt)

theorem parentGraph_isTree (N : ℕ) (parent : ℕ → ℕ)
    (hp : ∀ j, 0 < j → j ≤ N → parent j < j) :
    (parentGraph N parent).IsTree := by
  classical
  apply SimpleGraph.isTree_iff_connected_and_card.mpr
  refine ⟨parentGraph_connected N parent hp, ?_⟩
  rw [Nat.card_eq_fintype_card, ← SimpleGraph.edgeFinset_card,
    ← Math15.Graceful.edgeCount_eq_card_edgeFinset, parentGraph_edgeCount N parent hp]
  simp

def doubleSpiderEdges (a b c d e f : ℕ) : ℕ := d+a+b+c+e+f

def doubleSpiderParent (a b c d e _f j : ℕ) : ℕ :=
  if j = d+1 ∨ j = d+a+1 ∨ j = d+a+b+1 then 0
  else if j = d+a+b+c+1 ∨ j = d+a+b+c+e+1 then d
  else j-1

def doubleSpider (a b c d e f : ℕ) : SimpleGraph (Fin (doubleSpiderEdges a b c d e f + 1)) :=
  parentGraph (doubleSpiderEdges a b c d e f) (doubleSpiderParent a b c d e f)

theorem doubleSpiderParent_lt (a b c d e f j : ℕ) (hj : 0 < j) :
    doubleSpiderParent a b c d e f j < j := by
  unfold doubleSpiderParent
  split_ifs <;> omega

theorem doubleSpider_edgeCount (a b c d e f : ℕ) :
    Math15.Graceful.edgeCount (doubleSpider a b c d e f) = doubleSpiderEdges a b c d e f :=
  parentGraph_edgeCount _ _ (fun j hj _ => doubleSpiderParent_lt _ _ _ _ _ _ j hj)

theorem doubleSpider_isTree (a b c d e f : ℕ) : (doubleSpider a b c d e f).IsTree :=
  parentGraph_isTree _ _ (fun j hj _ => doubleSpiderParent_lt _ _ _ _ _ _ j hj)

end Bounty
end

/- AllTwoTest -/
section
namespace Bounty

def allTwoLabel (d j : ℕ) : ℕ :=
  if j ≤ d then
    if j % 4 = 0 then j / 2
    else if j % 4 = 1 then d + (if d % 2 = 0 then 4 else 10) - j / 2
    else if j % 4 = 2 then j / 2 + 6
    else d + (if d % 2 = 0 then 10 else 4) - j / 2
  else if j = d+1 then d+10-d%2
  else if j = d+2 then 1
  else if j = d+3 then d+8-d%2
  else if j = d+4 then 3
  else if j = d+5 then d+6-d%2
  else if j = d+6 then 5
  else if j = d+7 then
    if d%4 = 0 ∨ d%4 = 3 then 2*(d/4)+2 else d+11-d%2-(2*(d/4)+2)
  else if j = d+8 then
    if d%4 = 0 ∨ d%4 = 3 then d+11-d%2-(2*(d/4)+2) else 2*(d/4)+2
  else if j = d+9 then
    if d%4 = 0 ∨ d%4 = 3 then 2*(d/4)+4 else d+11-d%2-(2*(d/4)+4)
  else if d%4 = 0 ∨ d%4 = 3 then d+11-d%2-(2*(d/4)+4) else 2*(d/4)+4

lemma allTwo_index_cases (d x : ℕ) (hx : x ≤ d+10) :
    x ≤ d ∨ x=d+1 ∨ x=d+2 ∨ x=d+3 ∨ x=d+4 ∨ x=d+5 ∨ x=d+6 ∨ x=d+7 ∨ x=d+8 ∨ x=d+9 ∨ x=d+10 := by omega

lemma allTwoLabel_case_0_0 {d : ℕ} {i : ℕ} (hi : i ≤ d) {j : ℕ} (hj : j ≤ d)
    (heq : allTwoLabel d i = allTwoLabel d j) : i = j := by
  simp (discharger := omega) only [allTwoLabel, ite_eq_left, ite_eq_right, ite_true, ite_false, true_or, or_true] at heq
  try split_ifs at heq
  all_goals try simp only [Nat.dist] at heq
  all_goals omega

lemma allTwoLabel_case_0_1 {d : ℕ} {i : ℕ} (hi : i ≤ d)
    (heq : allTwoLabel d i = allTwoLabel d (d+1)) : i = (d+1) := by
  simp (discharger := omega) only [allTwoLabel, ite_eq_left, ite_eq_right, ite_true, ite_false, true_or, or_true] at heq
  try split_ifs at heq
  all_goals try simp only [Nat.dist] at heq
  all_goals omega

lemma allTwoLabel_case_0_2 {d : ℕ} {i : ℕ} (hi : i ≤ d)
    (heq : allTwoLabel d i = allTwoLabel d (d+2)) : i = (d+2) := by
  simp (discharger := omega) only [allTwoLabel, ite_eq_left, ite_eq_right, ite_true, ite_false, true_or, or_true] at heq
  try split_ifs at heq
  all_goals try simp only [Nat.dist] at heq
  all_goals omega

lemma allTwoLabel_case_0_3 {d : ℕ} {i : ℕ} (hi : i ≤ d)
    (heq : allTwoLabel d i = allTwoLabel d (d+3)) : i = (d+3) := by
  simp (discharger := omega) only [allTwoLabel, ite_eq_left, ite_eq_right, ite_true, ite_false, true_or, or_true] at heq
  try split_ifs at heq
  all_goals try simp only [Nat.dist] at heq
  all_goals omega

lemma allTwoLabel_case_0_4 {d : ℕ} {i : ℕ} (hi : i ≤ d)
    (heq : allTwoLabel d i = allTwoLabel d (d+4)) : i = (d+4) := by
  simp (discharger := omega) only [allTwoLabel, ite_eq_left, ite_eq_right, ite_true, ite_false, true_or, or_true] at heq
  try split_ifs at heq
  all_goals try simp only [Nat.dist] at heq
  all_goals omega

lemma allTwoLabel_case_0_5 {d : ℕ} {i : ℕ} (hi : i ≤ d)
    (heq : allTwoLabel d i = allTwoLabel d (d+5)) : i = (d+5) := by
  simp (discharger := omega) only [allTwoLabel, ite_eq_left, ite_eq_right, ite_true, ite_false, true_or, or_true] at heq
  try split_ifs at heq
  all_goals try simp only [Nat.dist] at heq
  all_goals omega

lemma allTwoLabel_case_0_6 {d : ℕ} {i : ℕ} (hi : i ≤ d)
    (heq : allTwoLabel d i = allTwoLabel d (d+6)) : i = (d+6) := by
  simp (discharger := omega) only [allTwoLabel, ite_eq_left, ite_eq_right, ite_true, ite_false, true_or, or_true] at heq
  try split_ifs at heq
  all_goals try simp only [Nat.dist] at heq
  all_goals omega

lemma allTwoLabel_case_0_7 {d : ℕ} {i : ℕ} (hi : i ≤ d)
    (heq : allTwoLabel d i = allTwoLabel d (d+7)) : i = (d+7) := by
  simp (discharger := omega) only [allTwoLabel, ite_eq_left, ite_eq_right, ite_true, ite_false, true_or, or_true] at heq
  try split_ifs at heq
  all_goals try simp only [Nat.dist] at heq
  all_goals omega

lemma allTwoLabel_case_0_8 {d : ℕ} {i : ℕ} (hi : i ≤ d)
    (heq : allTwoLabel d i = allTwoLabel d (d+8)) : i = (d+8) := by
  simp (discharger := omega) only [allTwoLabel, ite_eq_left, ite_eq_right, ite_true, ite_false, true_or, or_true] at heq
  try split_ifs at heq
  all_goals try simp only [Nat.dist] at heq
  all_goals omega

lemma allTwoLabel_case_0_9 {d : ℕ} {i : ℕ} (hi : i ≤ d)
    (heq : allTwoLabel d i = allTwoLabel d (d+9)) : i = (d+9) := by
  simp (discharger := omega) only [allTwoLabel, ite_eq_left, ite_eq_right, ite_true, ite_false, true_or, or_true] at heq
  try split_ifs at heq
  all_goals try simp only [Nat.dist] at heq
  all_goals omega

lemma allTwoLabel_case_0_10 {d : ℕ} {i : ℕ} (hi : i ≤ d)
    (heq : allTwoLabel d i = allTwoLabel d (d+10)) : i = (d+10) := by
  simp (discharger := omega) only [allTwoLabel, ite_eq_left, ite_eq_right, ite_true, ite_false, true_or, or_true] at heq
  try split_ifs at heq
  all_goals try simp only [Nat.dist] at heq
  all_goals omega

lemma allTwoLabel_case_1_2 {d : ℕ}
    (heq : allTwoLabel d (d+1) = allTwoLabel d (d+2)) : (d+1) = (d+2) := by
  simp (discharger := omega) only [allTwoLabel, ite_eq_left, ite_eq_right, ite_true, ite_false, true_or, or_true] at heq
  try split_ifs at heq
  all_goals try simp only [Nat.dist] at heq
  all_goals omega

lemma allTwoLabel_case_1_3 {d : ℕ}
    (heq : allTwoLabel d (d+1) = allTwoLabel d (d+3)) : (d+1) = (d+3) := by
  simp (discharger := omega) only [allTwoLabel, ite_eq_left, ite_eq_right, ite_true, ite_false, true_or, or_true] at heq
  try split_ifs at heq
  all_goals try simp only [Nat.dist] at heq
  all_goals omega

lemma allTwoLabel_case_1_4 {d : ℕ}
    (heq : allTwoLabel d (d+1) = allTwoLabel d (d+4)) : (d+1) = (d+4) := by
  simp (discharger := omega) only [allTwoLabel, ite_eq_left, ite_eq_right, ite_true, ite_false, true_or, or_true] at heq
  try split_ifs at heq
  all_goals try simp only [Nat.dist] at heq
  all_goals omega

lemma allTwoLabel_case_1_5 {d : ℕ}
    (heq : allTwoLabel d (d+1) = allTwoLabel d (d+5)) : (d+1) = (d+5) := by
  simp (discharger := omega) only [allTwoLabel, ite_eq_left, ite_eq_right, ite_true, ite_false, true_or, or_true] at heq
  try split_ifs at heq
  all_goals try simp only [Nat.dist] at heq
  all_goals omega

lemma allTwoLabel_case_1_6 {d : ℕ}
    (heq : allTwoLabel d (d+1) = allTwoLabel d (d+6)) : (d+1) = (d+6) := by
  simp (discharger := omega) only [allTwoLabel, ite_eq_left, ite_eq_right, ite_true, ite_false, true_or, or_true] at heq
  try split_ifs at heq
  all_goals try simp only [Nat.dist] at heq
  all_goals omega

lemma allTwoLabel_case_1_7 {d : ℕ}
    (heq : allTwoLabel d (d+1) = allTwoLabel d (d+7)) : (d+1) = (d+7) := by
  simp (discharger := omega) only [allTwoLabel, ite_eq_left, ite_eq_right, ite_true, ite_false, true_or, or_true] at heq
  try split_ifs at heq
  all_goals try simp only [Nat.dist] at heq
  all_goals omega

lemma allTwoLabel_case_1_8 {d : ℕ}
    (heq : allTwoLabel d (d+1) = allTwoLabel d (d+8)) : (d+1) = (d+8) := by
  simp (discharger := omega) only [allTwoLabel, ite_eq_left, ite_eq_right, ite_true, ite_false, true_or, or_true] at heq
  try split_ifs at heq
  all_goals try simp only [Nat.dist] at heq
  all_goals omega

lemma allTwoLabel_case_1_9 {d : ℕ}
    (heq : allTwoLabel d (d+1) = allTwoLabel d (d+9)) : (d+1) = (d+9) := by
  simp (discharger := omega) only [allTwoLabel, ite_eq_left, ite_eq_right, ite_true, ite_false, true_or, or_true] at heq
  try split_ifs at heq
  all_goals try simp only [Nat.dist] at heq
  all_goals omega

lemma allTwoLabel_case_1_10 {d : ℕ}
    (heq : allTwoLabel d (d+1) = allTwoLabel d (d+10)) : (d+1) = (d+10) := by
  simp (discharger := omega) only [allTwoLabel, ite_eq_left, ite_eq_right, ite_true, ite_false, true_or, or_true] at heq
  try split_ifs at heq
  all_goals try simp only [Nat.dist] at heq
  all_goals omega

lemma allTwoLabel_case_2_3 {d : ℕ}
    (heq : allTwoLabel d (d+2) = allTwoLabel d (d+3)) : (d+2) = (d+3) := by
  simp (discharger := omega) only [allTwoLabel, ite_eq_left, ite_eq_right, ite_true, ite_false, true_or, or_true] at heq
  try split_ifs at heq
  all_goals try simp only [Nat.dist] at heq
  all_goals omega

lemma allTwoLabel_case_2_4 {d : ℕ}
    (heq : allTwoLabel d (d+2) = allTwoLabel d (d+4)) : (d+2) = (d+4) := by
  simp (discharger := omega) only [allTwoLabel, ite_eq_left, ite_eq_right, ite_true, ite_false, true_or, or_true] at heq
  try split_ifs at heq
  all_goals try simp only [Nat.dist] at heq
  all_goals omega

lemma allTwoLabel_case_2_5 {d : ℕ}
    (heq : allTwoLabel d (d+2) = allTwoLabel d (d+5)) : (d+2) = (d+5) := by
  simp (discharger := omega) only [allTwoLabel, ite_eq_left, ite_eq_right, ite_true, ite_false, true_or, or_true] at heq
  try split_ifs at heq
  all_goals try simp only [Nat.dist] at heq
  all_goals omega

lemma allTwoLabel_case_2_6 {d : ℕ}
    (heq : allTwoLabel d (d+2) = allTwoLabel d (d+6)) : (d+2) = (d+6) := by
  simp (discharger := omega) only [allTwoLabel, ite_eq_left, ite_eq_right, ite_true, ite_false, true_or, or_true] at heq
  try split_ifs at heq
  all_goals try simp only [Nat.dist] at heq
  all_goals omega

lemma allTwoLabel_case_2_7 {d : ℕ}
    (heq : allTwoLabel d (d+2) = allTwoLabel d (d+7)) : (d+2) = (d+7) := by
  simp (discharger := omega) only [allTwoLabel, ite_eq_left, ite_eq_right, ite_true, ite_false, true_or, or_true] at heq
  try split_ifs at heq
  all_goals try simp only [Nat.dist] at heq
  all_goals omega

lemma allTwoLabel_case_2_8 {d : ℕ}
    (heq : allTwoLabel d (d+2) = allTwoLabel d (d+8)) : (d+2) = (d+8) := by
  simp (discharger := omega) only [allTwoLabel, ite_eq_left, ite_eq_right, ite_true, ite_false, true_or, or_true] at heq
  try split_ifs at heq
  all_goals try simp only [Nat.dist] at heq
  all_goals omega

lemma allTwoLabel_case_2_9 {d : ℕ}
    (heq : allTwoLabel d (d+2) = allTwoLabel d (d+9)) : (d+2) = (d+9) := by
  simp (discharger := omega) only [allTwoLabel, ite_eq_left, ite_eq_right, ite_true, ite_false, true_or, or_true] at heq
  try split_ifs at heq
  all_goals try simp only [Nat.dist] at heq
  all_goals omega

lemma allTwoLabel_case_2_10 {d : ℕ}
    (heq : allTwoLabel d (d+2) = allTwoLabel d (d+10)) : (d+2) = (d+10) := by
  simp (discharger := omega) only [allTwoLabel, ite_eq_left, ite_eq_right, ite_true, ite_false, true_or, or_true] at heq
  try split_ifs at heq
  all_goals try simp only [Nat.dist] at heq
  all_goals omega

lemma allTwoLabel_case_3_4 {d : ℕ}
    (heq : allTwoLabel d (d+3) = allTwoLabel d (d+4)) : (d+3) = (d+4) := by
  simp (discharger := omega) only [allTwoLabel, ite_eq_left, ite_eq_right, ite_true, ite_false, true_or, or_true] at heq
  try split_ifs at heq
  all_goals try simp only [Nat.dist] at heq
  all_goals omega

lemma allTwoLabel_case_3_5 {d : ℕ}
    (heq : allTwoLabel d (d+3) = allTwoLabel d (d+5)) : (d+3) = (d+5) := by
  simp (discharger := omega) only [allTwoLabel, ite_eq_left, ite_eq_right, ite_true, ite_false, true_or, or_true] at heq