FormalConjectures.WrittenOnTheWallII.GraphConjecture65

/-
Copyright 2026 The Formal Conjectures Authors.

Licensed under the Apache License, Version 2.0 (the "License");
you may not use this file except in compliance with the License.
You may obtain a copy of the License at

    https://www.apache.org/licenses/LICENSE-2.0

Unless required by applicable law or agreed to in writing, software
distributed under the License is distributed on an "AS IS" BASIS,
WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
See the License for the specific language governing permissions and
limitations under the License.
-/

import FormalConjecturesUtil

Written on the Wall II - Conjecture 65

Reference: E. DeLaVina, Written on the Wall II, Conjectures of Graffiti.pc

Counterexample

The conjecture is false. Start with the path $v_0-v_1-\cdots-v_{12}$ and attach one triangle at $v_1$ and another at $v_{11}$. The resulting graph has $17$ vertices. Its Graph_6 string is PhCGGC@?G?_@?@O?G?G?G?@C. Its only minimum-degree vertices are $v_0$ and $v_{12}$, at distance $12$, while its only maximum-degree vertices are $v_1$ and $v_{11}$, at distance $10$. Thus the conjectured lower bound is $12 + \lceil 10/3 \rceil = 16$.

Every induced forest must omit at least one vertex from each of the two vertex-disjoint triangles, so it has at most $15$ vertices. Conversely, deleting one non-path vertex from each triangle leaves a tree on $15$ vertices.

namespace WrittenOnTheWallII.GraphConjecture65open SimpleGraph Finset

/- Synthesizing `∀ v, Fintype ↥(graph.neighborSet v)` on our 18-edges graph uses more than the
default `synthInstance.maxSize` of 128 instances. That option bounds how many instances a solution
may use, not how long the search may take. Raising it is free -- synthesis costs ~13ms either way
about 1% of this file's elaboration time; the rest is `decide` and kernel type-checking. -/
set_option synthInstance.maxSize 400

namespace Counterexample

The counterexample: a path on vertices $0,\ldots,12$, with triangles attached at vertices $1$ and $11$.

abbrev graph : SimpleGraph (Fin 17) :=
  SimpleGraph.fromEdgeSet {
    s(0, 1), s(1, 2), s(2, 3), s(3, 4), s(4, 5), s(5, 6),
    s(6, 7), s(7, 8), s(8, 9), s(9, 10), s(10, 11), s(11, 12),
    s(1, 13), s(1, 14), s(13, 14),
    s(11, 15), s(11, 16), s(15, 16)
  }

The counterexample is connected.

@[category API, AMS 5]
lemma connected : graph.Connected := by⊢ graph.Connected decide +kernelAll goals completed! 🐙

The minimum-degree vertices of the counterexample are the two path endpoints.

@[category API, AMS 5]
lemma min_degree_vertices :
    {v | graph.degree v = graph.minDegree} = ({0, 12} : Set (Fin 17)) := by⊢ {v | graph.degree v = graph.minDegree} = {0, 12}
  ext vv:Fin 17⊢ v ∈ {v | graph.degree v = graph.minDegree} ↔ v ∈ {0, 12}
  fin_cases v«0»⊢ (fun i ↦ i) ⟨0, ⋯⟩ ∈ {v | graph.degree v = graph.minDegree} ↔ (fun i ↦ i) ⟨0, ⋯⟩ ∈ {0, 12}«1»⊢ (fun i ↦ i) ⟨1, ⋯⟩ ∈ {v | graph.degree v = graph.minDegree} ↔ (fun i ↦ i) ⟨1, ⋯⟩ ∈ {0, 12}«2»⊢ (fun i ↦ i) ⟨2, ⋯⟩ ∈ {v | graph.degree v = graph.minDegree} ↔ (fun i ↦ i) ⟨2, ⋯⟩ ∈ {0, 12}«3»⊢ (fun i ↦ i) ⟨3, ⋯⟩ ∈ {v | graph.degree v = graph.minDegree} ↔ (fun i ↦ i) ⟨3, ⋯⟩ ∈ {0, 12}«4»⊢ (fun i ↦ i) ⟨4, ⋯⟩ ∈ {v | graph.degree v = graph.minDegree} ↔ (fun i ↦ i) ⟨4, ⋯⟩ ∈ {0, 12}«5»⊢ (fun i ↦ i) ⟨5, ⋯⟩ ∈ {v | graph.degree v = graph.minDegree} ↔ (fun i ↦ i) ⟨5, ⋯⟩ ∈ {0, 12}«6»⊢ (fun i ↦ i) ⟨6, ⋯⟩ ∈ {v | graph.degree v = graph.minDegree} ↔ (fun i ↦ i) ⟨6, ⋯⟩ ∈ {0, 12}«7»⊢ (fun i ↦ i) ⟨7, ⋯⟩ ∈ {v | graph.degree v = graph.minDegree} ↔ (fun i ↦ i) ⟨7, ⋯⟩ ∈ {0, 12}«8»⊢ (fun i ↦ i) ⟨8, ⋯⟩ ∈ {v | graph.degree v = graph.minDegree} ↔ (fun i ↦ i) ⟨8, ⋯⟩ ∈ {0, 12}«9»⊢ (fun i ↦ i) ⟨9, ⋯⟩ ∈ {v | graph.degree v = graph.minDegree} ↔ (fun i ↦ i) ⟨9, ⋯⟩ ∈ {0, 12}«10»⊢ (fun i ↦ i) ⟨10, ⋯⟩ ∈ {v | graph.degree v = graph.minDegree} ↔ (fun i ↦ i) ⟨10, ⋯⟩ ∈ {0, 12}«11»⊢ (fun i ↦ i) ⟨11, ⋯⟩ ∈ {v | graph.degree v = graph.minDegree} ↔ (fun i ↦ i) ⟨11, ⋯⟩ ∈ {0, 12}«12»⊢ (fun i ↦ i) ⟨12, ⋯⟩ ∈ {v | graph.degree v = graph.minDegree} ↔ (fun i ↦ i) ⟨12, ⋯⟩ ∈ {0, 12}«13»⊢ (fun i ↦ i) ⟨13, ⋯⟩ ∈ {v | graph.degree v = graph.minDegree} ↔ (fun i ↦ i) ⟨13, ⋯⟩ ∈ {0, 12}«14»⊢ (fun i ↦ i) ⟨14, ⋯⟩ ∈ {v | graph.degree v = graph.minDegree} ↔ (fun i ↦ i) ⟨14, ⋯⟩ ∈ {0, 12}«15»⊢ (fun i ↦ i) ⟨15, ⋯⟩ ∈ {v | graph.degree v = graph.minDegree} ↔ (fun i ↦ i) ⟨15, ⋯⟩ ∈ {0, 12}«16»⊢ (fun i ↦ i) ⟨16, ⋯⟩ ∈ {v | graph.degree v = graph.minDegree} ↔ (fun i ↦ i) ⟨16, ⋯⟩ ∈ {0, 12} <;>«0»⊢ (fun i ↦ i) ⟨0, ⋯⟩ ∈ {v | graph.degree v = graph.minDegree} ↔ (fun i ↦ i) ⟨0, ⋯⟩ ∈ {0, 12}«1»⊢ (fun i ↦ i) ⟨1, ⋯⟩ ∈ {v | graph.degree v = graph.minDegree} ↔ (fun i ↦ i) ⟨1, ⋯⟩ ∈ {0, 12}«2»⊢ (fun i ↦ i) ⟨2, ⋯⟩ ∈ {v | graph.degree v = graph.minDegree} ↔ (fun i ↦ i) ⟨2, ⋯⟩ ∈ {0, 12}«3»⊢ (fun i ↦ i) ⟨3, ⋯⟩ ∈ {v | graph.degree v = graph.minDegree} ↔ (fun i ↦ i) ⟨3, ⋯⟩ ∈ {0, 12}«4»⊢ (fun i ↦ i) ⟨4, ⋯⟩ ∈ {v | graph.degree v = graph.minDegree} ↔ (fun i ↦ i) ⟨4, ⋯⟩ ∈ {0, 12}«5»⊢ (fun i ↦ i) ⟨5, ⋯⟩ ∈ {v | graph.degree v = graph.minDegree} ↔ (fun i ↦ i) ⟨5, ⋯⟩ ∈ {0, 12}«6»⊢ (fun i ↦ i) ⟨6, ⋯⟩ ∈ {v | graph.degree v = graph.minDegree} ↔ (fun i ↦ i) ⟨6, ⋯⟩ ∈ {0, 12}«7»⊢ (fun i ↦ i) ⟨7, ⋯⟩ ∈ {v | graph.degree v = graph.minDegree} ↔ (fun i ↦ i) ⟨7, ⋯⟩ ∈ {0, 12}«8»⊢ (fun i ↦ i) ⟨8, ⋯⟩ ∈ {v | graph.degree v = graph.minDegree} ↔ (fun i ↦ i) ⟨8, ⋯⟩ ∈ {0, 12}«9»⊢ (fun i ↦ i) ⟨9, ⋯⟩ ∈ {v | graph.degree v = graph.minDegree} ↔ (fun i ↦ i) ⟨9, ⋯⟩ ∈ {0, 12}«10»⊢ (fun i ↦ i) ⟨10, ⋯⟩ ∈ {v | graph.degree v = graph.minDegree} ↔ (fun i ↦ i) ⟨10, ⋯⟩ ∈ {0, 12}«11»⊢ (fun i ↦ i) ⟨11, ⋯⟩ ∈ {v | graph.degree v = graph.minDegree} ↔ (fun i ↦ i) ⟨11, ⋯⟩ ∈ {0, 12}«12»⊢ (fun i ↦ i) ⟨12, ⋯⟩ ∈ {v | graph.degree v = graph.minDegree} ↔ (fun i ↦ i) ⟨12, ⋯⟩ ∈ {0, 12}«13»⊢ (fun i ↦ i) ⟨13, ⋯⟩ ∈ {v | graph.degree v = graph.minDegree} ↔ (fun i ↦ i) ⟨13, ⋯⟩ ∈ {0, 12}«14»⊢ (fun i ↦ i) ⟨14, ⋯⟩ ∈ {v | graph.degree v = graph.minDegree} ↔ (fun i ↦ i) ⟨14, ⋯⟩ ∈ {0, 12}«15»⊢ (fun i ↦ i) ⟨15, ⋯⟩ ∈ {v | graph.degree v = graph.minDegree} ↔ (fun i ↦ i) ⟨15, ⋯⟩ ∈ {0, 12}«16»⊢ (fun i ↦ i) ⟨16, ⋯⟩ ∈ {v | graph.degree v = graph.minDegree} ↔ (fun i ↦ i) ⟨16, ⋯⟩ ∈ {0, 12} decideAll goals completed! 🐙

The maximum-degree vertices of the counterexample are the two triangle attachment points.

@[category API, AMS 5]
lemma max_degree_vertices :
    {v | graph.degree v = graph.maxDegree} = ({1, 11} : Set (Fin 17)) := by⊢ {v | graph.degree v = graph.maxDegree} = {1, 11}
  ext vv:Fin 17⊢ v ∈ {v | graph.degree v = graph.maxDegree} ↔ v ∈ {1, 11}
  fin_cases v«0»⊢ (fun i ↦ i) ⟨0, ⋯⟩ ∈ {v | graph.degree v = graph.maxDegree} ↔ (fun i ↦ i) ⟨0, ⋯⟩ ∈ {1, 11}«1»⊢ (fun i ↦ i) ⟨1, ⋯⟩ ∈ {v | graph.degree v = graph.maxDegree} ↔ (fun i ↦ i) ⟨1, ⋯⟩ ∈ {1, 11}«2»⊢ (fun i ↦ i) ⟨2, ⋯⟩ ∈ {v | graph.degree v = graph.maxDegree} ↔ (fun i ↦ i) ⟨2, ⋯⟩ ∈ {1, 11}«3»⊢ (fun i ↦ i) ⟨3, ⋯⟩ ∈ {v | graph.degree v = graph.maxDegree} ↔ (fun i ↦ i) ⟨3, ⋯⟩ ∈ {1, 11}«4»⊢ (fun i ↦ i) ⟨4, ⋯⟩ ∈ {v | graph.degree v = graph.maxDegree} ↔ (fun i ↦ i) ⟨4, ⋯⟩ ∈ {1, 11}«5»⊢ (fun i ↦ i) ⟨5, ⋯⟩ ∈ {v | graph.degree v = graph.maxDegree} ↔ (fun i ↦ i) ⟨5, ⋯⟩ ∈ {1, 11}«6»⊢ (fun i ↦ i) ⟨6, ⋯⟩ ∈ {v | graph.degree v = graph.maxDegree} ↔ (fun i ↦ i) ⟨6, ⋯⟩ ∈ {1, 11}«7»⊢ (fun i ↦ i) ⟨7, ⋯⟩ ∈ {v | graph.degree v = graph.maxDegree} ↔ (fun i ↦ i) ⟨7, ⋯⟩ ∈ {1, 11}«8»⊢ (fun i ↦ i) ⟨8, ⋯⟩ ∈ {v | graph.degree v = graph.maxDegree} ↔ (fun i ↦ i) ⟨8, ⋯⟩ ∈ {1, 11}«9»⊢ (fun i ↦ i) ⟨9, ⋯⟩ ∈ {v | graph.degree v = graph.maxDegree} ↔ (fun i ↦ i) ⟨9, ⋯⟩ ∈ {1, 11}«10»⊢ (fun i ↦ i) ⟨10, ⋯⟩ ∈ {v | graph.degree v = graph.maxDegree} ↔ (fun i ↦ i) ⟨10, ⋯⟩ ∈ {1, 11}«11»⊢ (fun i ↦ i) ⟨11, ⋯⟩ ∈ {v | graph.degree v = graph.maxDegree} ↔ (fun i ↦ i) ⟨11, ⋯⟩ ∈ {1, 11}«12»⊢ (fun i ↦ i) ⟨12, ⋯⟩ ∈ {v | graph.degree v = graph.maxDegree} ↔ (fun i ↦ i) ⟨12, ⋯⟩ ∈ {1, 11}«13»⊢ (fun i ↦ i) ⟨13, ⋯⟩ ∈ {v | graph.degree v = graph.maxDegree} ↔ (fun i ↦ i) ⟨13, ⋯⟩ ∈ {1, 11}«14»⊢ (fun i ↦ i) ⟨14, ⋯⟩ ∈ {v | graph.degree v = graph.maxDegree} ↔ (fun i ↦ i) ⟨14, ⋯⟩ ∈ {1, 11}«15»⊢ (fun i ↦ i) ⟨15, ⋯⟩ ∈ {v | graph.degree v = graph.maxDegree} ↔ (fun i ↦ i) ⟨15, ⋯⟩ ∈ {1, 11}«16»⊢ (fun i ↦ i) ⟨16, ⋯⟩ ∈ {v | graph.degree v = graph.maxDegree} ↔ (fun i ↦ i) ⟨16, ⋯⟩ ∈ {1, 11} <;>«0»⊢ (fun i ↦ i) ⟨0, ⋯⟩ ∈ {v | graph.degree v = graph.maxDegree} ↔ (fun i ↦ i) ⟨0, ⋯⟩ ∈ {1, 11}«1»⊢ (fun i ↦ i) ⟨1, ⋯⟩ ∈ {v | graph.degree v = graph.maxDegree} ↔ (fun i ↦ i) ⟨1, ⋯⟩ ∈ {1, 11}«2»⊢ (fun i ↦ i) ⟨2, ⋯⟩ ∈ {v | graph.degree v = graph.maxDegree} ↔ (fun i ↦ i) ⟨2, ⋯⟩ ∈ {1, 11}«3»⊢ (fun i ↦ i) ⟨3, ⋯⟩ ∈ {v | graph.degree v = graph.maxDegree} ↔ (fun i ↦ i) ⟨3, ⋯⟩ ∈ {1, 11}«4»⊢ (fun i ↦ i) ⟨4, ⋯⟩ ∈ {v | graph.degree v = graph.maxDegree} ↔ (fun i ↦ i) ⟨4, ⋯⟩ ∈ {1, 11}«5»⊢ (fun i ↦ i) ⟨5, ⋯⟩ ∈ {v | graph.degree v = graph.maxDegree} ↔ (fun i ↦ i) ⟨5, ⋯⟩ ∈ {1, 11}«6»⊢ (fun i ↦ i) ⟨6, ⋯⟩ ∈ {v | graph.degree v = graph.maxDegree} ↔ (fun i ↦ i) ⟨6, ⋯⟩ ∈ {1, 11}«7»⊢ (fun i ↦ i) ⟨7, ⋯⟩ ∈ {v | graph.degree v = graph.maxDegree} ↔ (fun i ↦ i) ⟨7, ⋯⟩ ∈ {1, 11}«8»⊢ (fun i ↦ i) ⟨8, ⋯⟩ ∈ {v | graph.degree v = graph.maxDegree} ↔ (fun i ↦ i) ⟨8, ⋯⟩ ∈ {1, 11}«9»⊢ (fun i ↦ i) ⟨9, ⋯⟩ ∈ {v | graph.degree v = graph.maxDegree} ↔ (fun i ↦ i) ⟨9, ⋯⟩ ∈ {1, 11}«10»⊢ (fun i ↦ i) ⟨10, ⋯⟩ ∈ {v | graph.degree v = graph.maxDegree} ↔ (fun i ↦ i) ⟨10, ⋯⟩ ∈ {1, 11}«11»⊢ (fun i ↦ i) ⟨11, ⋯⟩ ∈ {v | graph.degree v = graph.maxDegree} ↔ (fun i ↦ i) ⟨11, ⋯⟩ ∈ {1, 11}«12»⊢ (fun i ↦ i) ⟨12, ⋯⟩ ∈ {v | graph.degree v = graph.maxDegree} ↔ (fun i ↦ i) ⟨12, ⋯⟩ ∈ {1, 11}«13»⊢ (fun i ↦ i) ⟨13, ⋯⟩ ∈ {v | graph.degree v = graph.maxDegree} ↔ (fun i ↦ i) ⟨13, ⋯⟩ ∈ {1, 11}«14»⊢ (fun i ↦ i) ⟨14, ⋯⟩ ∈ {v | graph.degree v = graph.maxDegree} ↔ (fun i ↦ i) ⟨14, ⋯⟩ ∈ {1, 11}«15»⊢ (fun i ↦ i) ⟨15, ⋯⟩ ∈ {v | graph.degree v = graph.maxDegree} ↔ (fun i ↦ i) ⟨15, ⋯⟩ ∈ {1, 11}«16»⊢ (fun i ↦ i) ⟨16, ⋯⟩ ∈ {v | graph.degree v = graph.maxDegree} ↔ (fun i ↦ i) ⟨16, ⋯⟩ ∈ {1, 11} decideAll goals completed! 🐙

The minimum distance between minimum-degree vertices is $12$.


@[category API, AMS 5]
lemma distMin_min_degree_vertices : distMin graph ({0, 12} : Set (Fin 17)) = 12 := by⊢ graph.distMin {0, 12} = 12
  rw [show ({0, 12} : Set (Fin 17)) = ↑({0, 12} : Finset (Fin 17)) by⊢ graph.distMin {0, 12} = 12⊢ graph.computableDistMin {0, 12} = 12 simpAll goals completed! 🐙⊢ graph.computableDistMin {0, 12} = 12,
    distMin_eq_computableDistMin⊢ graph.computableDistMin {0, 12} = 12⊢ graph.computableDistMin {0, 12} = 12]⊢ graph.computableDistMin {0, 12} = 12
  decideAll goals completed! 🐙

The minimum distance between maximum-degree vertices is $10$.


@[category API, AMS 5]
lemma distMin_max_degree_vertices : distMin graph ({1, 11} : Set (Fin 17)) = 10 := by⊢ graph.distMin {1, 11} = 10
  rw [show ({1, 11} : Set (Fin 17)) = ↑({1, 11} : Finset (Fin 17)) by⊢ graph.distMin {1, 11} = 10⊢ graph.computableDistMin {1, 11} = 10 simpAll goals completed! 🐙⊢ graph.computableDistMin {1, 11} = 10,
    distMin_eq_computableDistMin⊢ graph.computableDistMin {1, 11} = 10⊢ graph.computableDistMin {1, 11} = 10]⊢ graph.computableDistMin {1, 11} = 10
  decideAll goals completed! 🐙

An acyclic induced subgraph cannot contain all three vertices of a triangle.


@[category API, AMS 5]
lemma triangle_not_subset_of_isAcyclic (S : Finset (Fin 17))
    (hS : (graph.induce S).IsAcyclic) {a b c : Fin 17}
    (hab : graph.Adj a b) (hbc : graph.Adj b c) (hca : graph.Adj c a) :
    ¬({a, b, c} : Finset (Fin 17)) ⊆ S := byS:Finset (Fin 17)hS:(induce (↑S) graph).IsAcyclica:Fin 17b:Fin 17c:Fin 17hab:graph.Adj a bhbc:graph.Adj b chca:graph.Adj c a⊢ ¬{a, b, c} ⊆ S
  intro hsubS:Finset (Fin 17)hS:(induce (↑S) graph).IsAcyclica:Fin 17b:Fin 17c:Fin 17hab:graph.Adj a bhbc:graph.Adj b chca:graph.Adj c ahsub:{a, b, c} ⊆ S⊢ False
  have ha : a ∈ S := hsub (byS:Finset (Fin 17)hS:(induce (↑S) graph).IsAcyclica:Fin 17b:Fin 17c:Fin 17hab:graph.Adj a bhbc:graph.Adj b chca:graph.Adj c ahsub:{a, b, c} ⊆ S⊢ a ∈ {a, b, c}S:Finset (Fin 17)hS:(induce (↑S) graph).IsAcyclica:Fin 17b:Fin 17c:Fin 17hab:graph.Adj a bhbc:graph.Adj b chca:graph.Adj c ahsub:{a, b, c} ⊆ Sha:a ∈ S⊢ False simpAll goals completed! 🐙S:Finset (Fin 17)hS:(induce (↑S) graph).IsAcyclica:Fin 17b:Fin 17c:Fin 17hab:graph.Adj a bhbc:graph.Adj b chca:graph.Adj c ahsub:{a, b, c} ⊆ Sha:a ∈ S⊢ False)S:Finset (Fin 17)hS:(induce (↑S) graph).IsAcyclica:Fin 17b:Fin 17c:Fin 17hab:graph.Adj a bhbc:graph.Adj b chca:graph.Adj c ahsub:{a, b, c} ⊆ Sha:a ∈ S⊢ False
  have hb : b ∈ S := hsub (byS:Finset (Fin 17)hS:(induce (↑S) graph).IsAcyclica:Fin 17b:Fin 17c:Fin 17hab:graph.Adj a bhbc:graph.Adj b chca:graph.Adj c ahsub:{a, b, c} ⊆ Sha:a ∈ S⊢ b ∈ {a, b, c}S:Finset (Fin 17)hS:(induce (↑S) graph).IsAcyclica:Fin 17b:Fin 17c:Fin 17hab:graph.Adj a bhbc:graph.Adj b chca:graph.Adj c ahsub:{a, b, c} ⊆ Sha:a ∈ Shb:b ∈ S⊢ False simpAll goals completed! 🐙S:Finset (Fin 17)hS:(induce (↑S) graph).IsAcyclica:Fin 17b:Fin 17c:Fin 17hab:graph.Adj a bhbc:graph.Adj b chca:graph.Adj c ahsub:{a, b, c} ⊆ Sha:a ∈ Shb:b ∈ S⊢ False)S:Finset (Fin 17)hS:(induce (↑S) graph).IsAcyclica:Fin 17b:Fin 17c:Fin 17hab:graph.Adj a bhbc:graph.Adj b chca:graph.Adj c ahsub:{a, b, c} ⊆ Sha:a ∈ Shb:b ∈ S⊢ False
  have hc : c ∈ S := hsub (byS:Finset (Fin 17)hS:(induce (↑S) graph).IsAcyclica:Fin 17b:Fin 17c:Fin 17hab:graph.Adj a bhbc:graph.Adj b chca:graph.Adj c ahsub:{a, b, c} ⊆ Sha:a ∈ Shb:b ∈ S⊢ c ∈ {a, b, c}S:Finset (Fin 17)hS:(induce (↑S) graph).IsAcyclica:Fin 17b:Fin 17c:Fin 17hab:graph.Adj a bhbc:graph.Adj b chca:graph.Adj c ahsub:{a, b, c} ⊆ Sha:a ∈ Shb:b ∈ Shc:c ∈ S⊢ False simpAll goals completed! 🐙S:Finset (Fin 17)hS:(induce (↑S) graph).IsAcyclica:Fin 17b:Fin 17c:Fin 17hab:graph.Adj a bhbc:graph.Adj b chca:graph.Adj c ahsub:{a, b, c} ⊆ Sha:a ∈ Shb:b ∈ Shc:c ∈ S⊢ False)S:Finset (Fin 17)hS:(induce (↑S) graph).IsAcyclica:Fin 17b:Fin 17c:Fin 17hab:graph.Adj a bhbc:graph.Adj b chca:graph.Adj c ahsub:{a, b, c} ⊆ Sha:a ∈ Shb:b ∈ Shc:c ∈ S⊢ False
  let va : S := ⟨a, ha⟩S:Finset (Fin 17)hS:(induce (↑S) graph).IsAcyclica:Fin 17b:Fin 17c:Fin 17hab:graph.Adj a bhbc:graph.Adj b chca:graph.Adj c ahsub:{a, b, c} ⊆ Sha:a ∈ Shb:b ∈ Shc:c ∈ Sva:↥S := ⟨a, ha⟩⊢ False
  let vb : S := ⟨b, hb⟩S:Finset (Fin 17)hS:(induce (↑S) graph).IsAcyclica:Fin 17b:Fin 17c:Fin 17hab:graph.Adj a bhbc:graph.Adj b chca:graph.Adj c ahsub:{a, b, c} ⊆ Sha:a ∈ Shb:b ∈ Shc:c ∈ Sva:↥S := ⟨a, ha⟩vb:↥S := ⟨b, hb⟩⊢ False
  let vc : S := ⟨c, hc⟩S:Finset (Fin 17)hS:(induce (↑S) graph).IsAcyclica:Fin 17b:Fin 17c:Fin 17hab:graph.Adj a bhbc:graph.Adj b chca:graph.Adj c ahsub:{a, b, c} ⊆ Sha:a ∈ Shb:b ∈ Shc:c ∈ Sva:↥S := ⟨a, ha⟩vb:↥S := ⟨b, hb⟩vc:↥S := ⟨c, hc⟩⊢ False
  have hab' : (graph.induce S).Adj va vb := habS:Finset (Fin 17)hS:(induce (↑S) graph).IsAcyclica:Fin 17b:Fin 17c:Fin 17hab:graph.Adj a bhbc:graph.Adj b chca:graph.Adj c ahsub:{a, b, c} ⊆ Sha:a ∈ Shb:b ∈ Shc:c ∈ Sva:↥S := ⟨a, ha⟩vb:↥S := ⟨b, hb⟩vc:↥S := ⟨c, hc⟩hab':(induce (↑S) graph).Adj va vb⊢ False
  have hbc' : (graph.induce S).Adj vb vc := hbcS:Finset (Fin 17)hS:(induce (↑S) graph).IsAcyclica:Fin 17b:Fin 17c:Fin 17hab:graph.Adj a bhbc:graph.Adj b chca:graph.Adj c ahsub:{a, b, c} ⊆ Sha:a ∈ Shb:b ∈ Shc:c ∈ Sva:↥S := ⟨a, ha⟩vb:↥S := ⟨b, hb⟩vc:↥S := ⟨c, hc⟩hab':(induce (↑S) graph).Adj va vbhbc':(induce (↑S) graph).Adj vb vc⊢ False
  have hca' : (graph.induce S).Adj vc va := hcaS:Finset (Fin 17)hS:(induce (↑S) graph).IsAcyclica:Fin 17b:Fin 17c:Fin 17hab:graph.Adj a bhbc:graph.Adj b chca:graph.Adj c ahsub:{a, b, c} ⊆ Sha:a ∈ Shb:b ∈ Shc:c ∈ Sva:↥S := ⟨a, ha⟩vb:↥S := ⟨b, hb⟩vc:↥S := ⟨c, hc⟩hab':(induce (↑S) graph).Adj va vbhbc':(induce (↑S) graph).Adj vb vchca':(induce (↑S) graph).Adj vc va⊢ False
  let cycle : (graph.induce S).Walk va va :=
    .cons hab' (.cons hbc' (.cons hca' .nil))S:Finset (Fin 17)hS:(induce (↑S) graph).IsAcyclica:Fin 17b:Fin 17c:Fin 17hab:graph.Adj a bhbc:graph.Adj b chca:graph.Adj c ahsub:{a, b, c} ⊆ Sha:a ∈ Shb:b ∈ Shc:c ∈ Sva:↥S := ⟨a, ha⟩vb:↥S := ⟨b, hb⟩vc:↥S := ⟨c, hc⟩hab':(induce (↑S) graph).Adj va vbhbc':(induce (↑S) graph).Adj vb vchca':(induce (↑S) graph).Adj vc vacycle:(induce (↑S) graph).Walk va va := Walk.cons hab' (Walk.cons hbc' (Walk.cons hca' Walk.nil))⊢ False
  exact hS cycle (byS:Finset (Fin 17)hS:(induce (↑S) graph).IsAcyclica:Fin 17b:Fin 17c:Fin 17hab:graph.Adj a bhbc:graph.Adj b chca:graph.Adj c ahsub:{a, b, c} ⊆ Sha:a ∈ Shb:b ∈ Shc:c ∈ Sva:↥S := ⟨a, ha⟩vb:↥S := ⟨b, hb⟩vc:↥S := ⟨c, hc⟩hab':(induce (↑S) graph).Adj va vbhbc':(induce (↑S) graph).Adj vb vchca':(induce (↑S) graph).Adj vc vacycle:(induce (↑S) graph).Walk va va := Walk.cons hab' (Walk.cons hbc' (Walk.cons hca' Walk.nil))⊢ cycle.IsCycle
    rw [Walk.isCycle_defS:Finset (Fin 17)hS:(induce (↑S) graph).IsAcyclica:Fin 17b:Fin 17c:Fin 17hab:graph.Adj a bhbc:graph.Adj b chca:graph.Adj c ahsub:{a, b, c} ⊆ Sha:a ∈ Shb:b ∈ Shc:c ∈ Sva:↥S := ⟨a, ha⟩vb:↥S := ⟨b, hb⟩vc:↥S := ⟨c, hc⟩hab':(induce (↑S) graph).Adj va vbhbc':(induce (↑S) graph).Adj vb vchca':(induce (↑S) graph).Adj vc vacycle:(induce (↑S) graph).Walk va va := Walk.cons hab' (Walk.cons hbc' (Walk.cons hca' Walk.nil))⊢ cycle.IsTrail ∧ cycle ≠ Walk.nil ∧ cycle.support.tail.NodupS:Finset (Fin 17)hS:(induce (↑S) graph).IsAcyclica:Fin 17b:Fin 17c:Fin 17hab:graph.Adj a bhbc:graph.Adj b chca:graph.Adj c ahsub:{a, b, c} ⊆ Sha:a ∈ Shb:b ∈ Shc:c ∈ Sva:↥S := ⟨a, ha⟩vb:↥S := ⟨b, hb⟩vc:↥S := ⟨c, hc⟩hab':(induce (↑S) graph).Adj va vbhbc':(induce (↑S) graph).Adj vb vchca':(induce (↑S) graph).Adj vc vacycle:(induce (↑S) graph).Walk va va := Walk.cons hab' (Walk.cons hbc' (Walk.cons hca' Walk.nil))⊢ cycle.IsTrail ∧ cycle ≠ Walk.nil ∧ cycle.support.tail.Nodup]S:Finset (Fin 17)hS:(induce (↑S) graph).IsAcyclica:Fin 17b:Fin 17c:Fin 17hab:graph.Adj a bhbc:graph.Adj b chca:graph.Adj c ahsub:{a, b, c} ⊆ Sha:a ∈ Shb:b ∈ Shc:c ∈ Sva:↥S := ⟨a, ha⟩vb:↥S := ⟨b, hb⟩vc:↥S := ⟨c, hc⟩hab':(induce (↑S) graph).Adj va vbhbc':(induce (↑S) graph).Adj vb vchca':(induce (↑S) graph).Adj vc vacycle:(induce (↑S) graph).Walk va va := Walk.cons hab' (Walk.cons hbc' (Walk.cons hca' Walk.nil))⊢ cycle.IsTrail ∧ cycle ≠ Walk.nil ∧ cycle.support.tail.Nodup
    refine ⟨?_, byS:Finset (Fin 17)hS:(induce (↑S) graph).IsAcyclica:Fin 17b:Fin 17c:Fin 17hab:graph.Adj a bhbc:graph.Adj b chca:graph.Adj c ahsub:{a, b, c} ⊆ Sha:a ∈ Shb:b ∈ Shc:c ∈ Sva:↥S := ⟨a, ha⟩vb:↥S := ⟨b, hb⟩vc:↥S := ⟨c, hc⟩hab':(induce (↑S) graph).Adj va vbhbc':(induce (↑S) graph).Adj vb vchca':(induce (↑S) graph).Adj vc vacycle:(induce (↑S) graph).Walk va va := Walk.cons hab' (Walk.cons hbc' (Walk.cons hca' Walk.nil))⊢ cycle ≠ Walk.nil simp [cycle]All goals completed! 🐙, ?_⟩
    ·refine_1S:Finset (Fin 17)hS:(induce (↑S) graph).IsAcyclica:Fin 17b:Fin 17c:Fin 17hab:graph.Adj a bhbc:graph.Adj b chca:graph.Adj c ahsub:{a, b, c} ⊆ Sha:a ∈ Shb:b ∈ Shc:c ∈ Sva:↥S := ⟨a, ha⟩vb:↥S := ⟨b, hb⟩vc:↥S := ⟨c, hc⟩hab':(induce (↑S) graph).Adj va vbhbc':(induce (↑S) graph).Adj vb vchca':(induce (↑S) graph).Adj vc vacycle:(induce (↑S) graph).Walk va va := Walk.cons hab' (Walk.cons hbc' (Walk.cons hca' Walk.nil))⊢ cycle.IsTrail rw [Walk.isTrail_defrefine_1S:Finset (Fin 17)hS:(induce (↑S) graph).IsAcyclica:Fin 17b:Fin 17c:Fin 17hab:graph.Adj a bhbc:graph.Adj b chca:graph.Adj c ahsub:{a, b, c} ⊆ Sha:a ∈ Shb:b ∈ Shc:c ∈ Sva:↥S := ⟨a, ha⟩vb:↥S := ⟨b, hb⟩vc:↥S := ⟨c, hc⟩hab':(induce (↑S) graph).Adj va vbhbc':(induce (↑S) graph).Adj vb vchca':(induce (↑S) graph).Adj vc vacycle:(induce (↑S) graph).Walk va va := Walk.cons hab' (Walk.cons hbc' (Walk.cons hca' Walk.nil))⊢ cycle.edges.Noduprefine_1S:Finset (Fin 17)hS:(induce (↑S) graph).IsAcyclica:Fin 17b:Fin 17c:Fin 17hab:graph.Adj a bhbc:graph.Adj b chca:graph.Adj c ahsub:{a, b, c} ⊆ Sha:a ∈ Shb:b ∈ Shc:c ∈ Sva:↥S := ⟨a, ha⟩vb:↥S := ⟨b, hb⟩vc:↥S := ⟨c, hc⟩hab':(induce (↑S) graph).Adj va vbhbc':(induce (↑S) graph).Adj vb vchca':(induce (↑S) graph).Adj vc vacycle:(induce (↑S) graph).Walk va va := Walk.cons hab' (Walk.cons hbc' (Walk.cons hca' Walk.nil))⊢ cycle.edges.Nodup]refine_1S:Finset (Fin 17)hS:(induce (↑S) graph).IsAcyclica:Fin 17b:Fin 17c:Fin 17hab:graph.Adj a bhbc:graph.Adj b chca:graph.Adj c ahsub:{a, b, c} ⊆ Sha:a ∈ Shb:b ∈ Shc:c ∈ Sva:↥S := ⟨a, ha⟩vb:↥S := ⟨b, hb⟩vc:↥S := ⟨c, hc⟩hab':(induce (↑S) graph).Adj va vbhbc':(induce (↑S) graph).Adj vb vchca':(induce (↑S) graph).Adj vc vacycle:(induce (↑S) graph).Walk va va := Walk.cons hab' (Walk.cons hbc' (Walk.cons hca' Walk.nil))⊢ cycle.edges.Nodup
      simp [cycle, va, vb, vc, hab.ne, hab.ne.symm, hbc.ne,
        hca.ne, hca.ne.symm]All goals completed! 🐙
    ·refine_2S:Finset (Fin 17)hS:(induce (↑S) graph).IsAcyclica:Fin 17b:Fin 17c:Fin 17hab:graph.Adj a bhbc:graph.Adj b chca:graph.Adj c ahsub:{a, b, c} ⊆ Sha:a ∈ Shb:b ∈ Shc:c ∈ Sva:↥S := ⟨a, ha⟩vb:↥S := ⟨b, hb⟩vc:↥S := ⟨c, hc⟩hab':(induce (↑S) graph).Adj va vbhbc':(induce (↑S) graph).Adj vb vchca':(induce (↑S) graph).Adj vc vacycle:(induce (↑S) graph).Walk va va := Walk.cons hab' (Walk.cons hbc' (Walk.cons hca' Walk.nil))⊢ cycle.support.tail.Nodup simp [cycle, va, vb, vc, hab.ne.symm, hbc.ne, hca.ne]All goals completed! 🐙)

Every induced forest in the counterexample has at most $15$ vertices.


@[category API, AMS 5]
lemma forest_card_le_fifteen (S : Finset (Fin 17)) (hS : (graph.induce S).IsAcyclic) :
    S.card ≤ 15 := byS:Finset (Fin 17)hS:(induce (↑S) graph).IsAcyclic⊢ #S ≤ 15
  have hfirst : ¬({1, 13, 14} : Finset (Fin 17)) ⊆ S :=
    triangle_not_subset_of_isAcyclic S hS (byS:Finset (Fin 17)hS:(induce (↑S) graph).IsAcyclic⊢ graph.Adj 1 13S:Finset (Fin 17)hS:(induce (↑S) graph).IsAcyclichfirst:¬{1, 13, 14} ⊆ S⊢ #S ≤ 15 decideAll goals completed! 🐙S:Finset (Fin 17)hS:(induce (↑S) graph).IsAcyclichfirst:¬{1, 13, 14} ⊆ S⊢ #S ≤ 15) (byS:Finset (Fin 17)hS:(induce (↑S) graph).IsAcyclic⊢ graph.Adj 13 14S:Finset (Fin 17)hS:(induce (↑S) graph).IsAcyclichfirst:¬{1, 13, 14} ⊆ S⊢ #S ≤ 15 decideAll goals completed! 🐙S:Finset (Fin 17)hS:(induce (↑S) graph).IsAcyclichfirst:¬{1, 13, 14} ⊆ S⊢ #S ≤ 15) (byS:Finset (Fin 17)hS:(induce (↑S) graph).IsAcyclic⊢ graph.Adj 14 1S:Finset (Fin 17)hS:(induce (↑S) graph).IsAcyclichfirst:¬{1, 13, 14} ⊆ S⊢ #S ≤ 15 decideAll goals completed! 🐙S:Finset (Fin 17)hS:(induce (↑S) graph).IsAcyclichfirst:¬{1, 13, 14} ⊆ S⊢ #S ≤ 15)S:Finset (Fin 17)hS:(induce (↑S) graph).IsAcyclichfirst:¬{1, 13, 14} ⊆ S⊢ #S ≤ 15
  have hsecond : ¬({11, 15, 16} : Finset (Fin 17)) ⊆ S :=
    triangle_not_subset_of_isAcyclic S hS (byS:Finset (Fin 17)hS:(induce (↑S) graph).IsAcyclichfirst:¬{1, 13, 14} ⊆ S⊢ graph.Adj 11 15S:Finset (Fin 17)hS:(induce (↑S) graph).IsAcyclichfirst:¬{1, 13, 14} ⊆ Shsecond:¬{11, 15, 16} ⊆ S⊢ #S ≤ 15 decideAll goals completed! 🐙S:Finset (Fin 17)hS:(induce (↑S) graph).IsAcyclichfirst:¬{1, 13, 14} ⊆ Shsecond:¬{11, 15, 16} ⊆ S⊢ #S ≤ 15) (byS:Finset (Fin 17)hS:(induce (↑S) graph).IsAcyclichfirst:¬{1, 13, 14} ⊆ S⊢ graph.Adj 15 16S:Finset (Fin 17)hS:(induce (↑S) graph).IsAcyclichfirst:¬{1, 13, 14} ⊆ Shsecond:¬{11, 15, 16} ⊆ S⊢ #S ≤ 15 decideAll goals completed! 🐙S:Finset (Fin 17)hS:(induce (↑S) graph).IsAcyclichfirst:¬{1, 13, 14} ⊆ Shsecond:¬{11, 15, 16} ⊆ S⊢ #S ≤ 15) (byS:Finset (Fin 17)hS:(induce (↑S) graph).IsAcyclichfirst:¬{1, 13, 14} ⊆ S⊢ graph.Adj 16 11S:Finset (Fin 17)hS:(induce (↑S) graph).IsAcyclichfirst:¬{1, 13, 14} ⊆ Shsecond:¬{11, 15, 16} ⊆ S⊢ #S ≤ 15 decideAll goals completed! 🐙S:Finset (Fin 17)hS:(induce (↑S) graph).IsAcyclichfirst:¬{1, 13, 14} ⊆ Shsecond:¬{11, 15, 16} ⊆ S⊢ #S ≤ 15)S:Finset (Fin 17)hS:(induce (↑S) graph).IsAcyclichfirst:¬{1, 13, 14} ⊆ Shsecond:¬{11, 15, 16} ⊆ S⊢ #S ≤ 15
  obtain ⟨x, hxT, hxS⟩ := Finset.not_subset.mp hfirstS:Finset (Fin 17)hS:(induce (↑S) graph).IsAcyclichfirst:¬{1, 13, 14} ⊆ Shsecond:¬{11, 15, 16} ⊆ Sx:Fin 17hxT:x ∈ {1, 13, 14}hxS:x ∉ S⊢ #S ≤ 15
  obtain ⟨y, hyT, hyS⟩ := Finset.not_subset.mp hsecondS:Finset (Fin 17)hS:(induce (↑S) graph).IsAcyclichfirst:¬{1, 13, 14} ⊆ Shsecond:¬{11, 15, 16} ⊆ Sx:Fin 17hxT:x ∈ {1, 13, 14}hxS:x ∉ Sy:Fin 17hyT:y ∈ {11, 15, 16}hyS:y ∉ S⊢ #S ≤ 15
  have hxy : x ≠ y := by
    intro hS:Finset (Fin 17)hS:(induce (↑S) graph).IsAcyclichfirst:¬{1, 13, 14} ⊆ Shsecond:¬{11, 15, 16} ⊆ Sx:Fin 17hxT:x ∈ {1, 13, 14}hxS:x ∉ Sy:Fin 17hyT:y ∈ {11, 15, 16}hyS:y ∉ Sh:x = y⊢ FalseS:Finset (Fin 17)hS:(induce (↑S) graph).IsAcyclichfirst:¬{1, 13, 14} ⊆ Shsecond:¬{11, 15, 16} ⊆ Sx:Fin 17hxT:x ∈ {1, 13, 14}hxS:x ∉ Sy:Fin 17hyT:y ∈ {11, 15, 16}hyS:y ∉ Shxy:x ≠ y⊢ #S ≤ 15
    subst yS:Finset (Fin 17)hS:(induce (↑S) graph).IsAcyclichfirst:¬{1, 13, 14} ⊆ Shsecond:¬{11, 15, 16} ⊆ Sx:Fin 17hxT:x ∈ {1, 13, 14}hxS:x ∉ ShyT:x ∈ {11, 15, 16}hyS:x ∉ S⊢ FalseS:Finset (Fin 17)hS:(induce (↑S) graph).IsAcyclichfirst:¬{1, 13, 14} ⊆ Shsecond:¬{11, 15, 16} ⊆ Sx:Fin 17hxT:x ∈ {1, 13, 14}hxS:x ∉ Sy:Fin 17hyT:y ∈ {11, 15, 16}hyS:y ∉ Shxy:x ≠ y⊢ #S ≤ 15
    simp only [Finset.mem_insert, Finset.mem_singleton] at hxT hyTS:Finset (Fin 17)hS:(induce (↑S) graph).IsAcyclichfirst:¬{1, 13, 14} ⊆ Shsecond:¬{11, 15, 16} ⊆ Sx:Fin 17hxS:x ∉ ShyS:x ∉ ShxT:x = 1 ∨ x = 13 ∨ x = 14hyT:x = 11 ∨ x = 15 ∨ x = 16⊢ FalseS:Finset (Fin 17)hS:(induce (↑S) graph).IsAcyclichfirst:¬{1, 13, 14} ⊆ Shsecond:¬{11, 15, 16} ⊆ Sx:Fin 17hxT:x ∈ {1, 13, 14}hxS:x ∉ Sy:Fin 17hyT:y ∈ {11, 15, 16}hyS:y ∉ Shxy:x ≠ y⊢ #S ≤ 15
    rcases hxT with rfl | rfl | rflinlS:Finset (Fin 17)hS:(induce (↑S) graph).IsAcyclichfirst:¬{1, 13, 14} ⊆ Shsecond:¬{11, 15, 16} ⊆ ShxS:1 ∉ ShyS:1 ∉ ShyT:1 = 11 ∨ 1 = 15 ∨ 1 = 16⊢ Falseinr.inlS:Finset (Fin 17)hS:(induce (↑S) graph).IsAcyclichfirst:¬{1, 13, 14} ⊆ Shsecond:¬{11, 15, 16} ⊆ ShxS:13 ∉ ShyS:13 ∉ ShyT:13 = 11 ∨ 13 = 15 ∨ 13 = 16⊢ Falseinr.inrS:Finset (Fin 17)hS:(induce (↑S) graph).IsAcyclichfirst:¬{1, 13, 14} ⊆ Shsecond:¬{11, 15, 16} ⊆ ShxS:14 ∉ ShyS:14 ∉ ShyT:14 = 11 ∨ 14 = 15 ∨ 14 = 16⊢ FalseS:Finset (Fin 17)hS:(induce (↑S) graph).IsAcyclichfirst:¬{1, 13, 14} ⊆ Shsecond:¬{11, 15, 16} ⊆ Sx:Fin 17hxT:x ∈ {1, 13, 14}hxS:x ∉ Sy:Fin 17hyT:y ∈ {11, 15, 16}hyS:y ∉ Shxy:x ≠ y⊢ #S ≤ 15 <;>inlS:Finset (Fin 17)hS:(induce (↑S) graph).IsAcyclichfirst:¬{1, 13, 14} ⊆ Shsecond:¬{11, 15, 16} ⊆ ShxS:1 ∉ ShyS:1 ∉ ShyT:1 = 11 ∨ 1 = 15 ∨ 1 = 16⊢ Falseinr.inlS:Finset (Fin 17)hS:(induce (↑S) graph).IsAcyclichfirst:¬{1, 13, 14} ⊆ Shsecond:¬{11, 15, 16} ⊆ ShxS:13 ∉ ShyS:13 ∉ ShyT:13 = 11 ∨ 13 = 15 ∨ 13 = 16⊢ Falseinr.inrS:Finset (Fin 17)hS:(induce (↑S) graph).IsAcyclichfirst:¬{1, 13, 14} ⊆ Shsecond:¬{11, 15, 16} ⊆ ShxS:14 ∉ ShyS:14 ∉ ShyT:14 = 11 ∨ 14 = 15 ∨ 14 = 16⊢ FalseS:Finset (Fin 17)hS:(induce (↑S) graph).IsAcyclichfirst:¬{1, 13, 14} ⊆ Shsecond:¬{11, 15, 16} ⊆ Sx:Fin 17hxT:x ∈ {1, 13, 14}hxS:x ∉ Sy:Fin 17hyT:y ∈ {11, 15, 16}hyS:y ∉ Shxy:x ≠ y⊢ #S ≤ 15 simp at hyTS:Finset (Fin 17)hS:(induce (↑S) graph).IsAcyclichfirst:¬{1, 13, 14} ⊆ Shsecond:¬{11, 15, 16} ⊆ Sx:Fin 17hxT:x ∈ {1, 13, 14}hxS:x ∉ Sy:Fin 17hyT:y ∈ {11, 15, 16}hyS:y ∉ Shxy:x ≠ y⊢ #S ≤ 15S:Finset (Fin 17)hS:(induce (↑S) graph).IsAcyclichfirst:¬{1, 13, 14} ⊆ Shsecond:¬{11, 15, 16} ⊆ Sx:Fin 17hxT:x ∈ {1, 13, 14}hxS:x ∉ Sy:Fin 17hyT:y ∈ {11, 15, 16}hyS:y ∉ Shxy:x ≠ y⊢ #S ≤ 15
  have hsubset : ({x, y} : Finset (Fin 17)) ⊆ Finset.univ \ S := by
    intro z hzS:Finset (Fin 17)hS:(induce (↑S) graph).IsAcyclichfirst:¬{1, 13, 14} ⊆ Shsecond:¬{11, 15, 16} ⊆ Sx:Fin 17hxT:x ∈ {1, 13, 14}hxS:x ∉ Sy:Fin 17hyT:y ∈ {11, 15, 16}hyS:y ∉ Shxy:x ≠ yz:Fin 17hz:z ∈ {x, y}⊢ z ∈ univ \ SS:Finset (Fin 17)hS:(induce (↑S) graph).IsAcyclichfirst:¬{1, 13, 14} ⊆ Shsecond:¬{11, 15, 16} ⊆ Sx:Fin 17hxT:x ∈ {1, 13, 14}hxS:x ∉ Sy:Fin 17hyT:y ∈ {11, 15, 16}hyS:y ∉ Shxy:x ≠ yhsubset:{x, y} ⊆ univ \ S⊢ #S ≤ 15
    simp only [Finset.mem_insert, Finset.mem_singleton] at hzS:Finset (Fin 17)hS:(induce (↑S) graph).IsAcyclichfirst:¬{1, 13, 14} ⊆ Shsecond:¬{11, 15, 16} ⊆ Sx:Fin 17hxT:x ∈ {1, 13, 14}hxS:x ∉ Sy:Fin 17hyT:y ∈ {11, 15, 16}hyS:y ∉ Shxy:x ≠ yz:Fin 17hz:z = x ∨ z = y⊢ z ∈ univ \ SS:Finset (Fin 17)hS:(induce (↑S) graph).IsAcyclichfirst:¬{1, 13, 14} ⊆ Shsecond:¬{11, 15, 16} ⊆ Sx:Fin 17hxT:x ∈ {1, 13, 14}hxS:x ∉ Sy:Fin 17hyT:y ∈ {11, 15, 16}hyS:y ∉ Shxy:x ≠ yhsubset:{x, y} ⊆ univ \ S⊢ #S ≤ 15
    rcases hz with rfl | rflinlS:Finset (Fin 17)hS:(induce (↑S) graph).IsAcyclichfirst:¬{1, 13, 14} ⊆ Shsecond:¬{11, 15, 16} ⊆ Sy:Fin 17hyT:y ∈ {11, 15, 16}hyS:y ∉ Sz:Fin 17hxT:z ∈ {1, 13, 14}hxS:z ∉ Shxy:z ≠ y⊢ z ∈ univ \ SinrS:Finset (Fin 17)hS:(induce (↑S) graph).IsAcyclichfirst:¬{1, 13, 14} ⊆ Shsecond:¬{11, 15, 16} ⊆ Sx:Fin 17hxT:x ∈ {1, 13, 14}hxS:x ∉ Sz:Fin 17hyT:z ∈ {11, 15, 16}hyS:z ∉ Shxy:x ≠ z⊢ z ∈ univ \ SS:Finset (Fin 17)hS:(induce (↑S) graph).IsAcyclichfirst:¬{1, 13, 14} ⊆ Shsecond:¬{11, 15, 16} ⊆ Sx:Fin 17hxT:x ∈ {1, 13, 14}hxS:x ∉ Sy:Fin 17hyT:y ∈ {11, 15, 16}hyS:y ∉ Shxy:x ≠ yhsubset:{x, y} ⊆ univ \ S⊢ #S ≤ 15 <;>inlS:Finset (Fin 17)hS:(induce (↑S) graph).IsAcyclichfirst:¬{1, 13, 14} ⊆ Shsecond:¬{11, 15, 16} ⊆ Sy:Fin 17hyT:y ∈ {11, 15, 16}hyS:y ∉ Sz:Fin 17hxT:z ∈ {1, 13, 14}hxS:z ∉ Shxy:z ≠ y⊢ z ∈ univ \ SinrS:Finset (Fin 17)hS:(induce (↑S) graph).IsAcyclichfirst:¬{1, 13, 14} ⊆ Shsecond:¬{11, 15, 16} ⊆ Sx:Fin 17hxT:x ∈ {1, 13, 14}hxS:x ∉ Sz:Fin 17hyT:z ∈ {11, 15, 16}hyS:z ∉ Shxy:x ≠ z⊢ z ∈ univ \ SS:Finset (Fin 17)hS:(induce (↑S) graph).IsAcyclichfirst:¬{1, 13, 14} ⊆ Shsecond:¬{11, 15, 16} ⊆ Sx:Fin 17hxT:x ∈ {1, 13, 14}hxS:x ∉ Sy:Fin 17hyT:y ∈ {11, 15, 16}hyS:y ∉ Shxy:x ≠ yhsubset:{x, y} ⊆ univ \ S⊢ #S ≤ 15 simp [hxS, hyS]S:Finset (Fin 17)hS:(induce (↑S) graph).IsAcyclichfirst:¬{1, 13, 14} ⊆ Shsecond:¬{11, 15, 16} ⊆ Sx:Fin 17hxT:x ∈ {1, 13, 14}hxS:x ∉ Sy:Fin 17hyT:y ∈ {11, 15, 16}hyS:y ∉ Shxy:x ≠ yhsubset:{x, y} ⊆ univ \ S⊢ #S ≤ 15S:Finset (Fin 17)hS:(induce (↑S) graph).IsAcyclichfirst:¬{1, 13, 14} ⊆ Shsecond:¬{11, 15, 16} ⊆ Sx:Fin 17hxT:x ∈ {1, 13, 14}hxS:x ∉ Sy:Fin 17hyT:y ∈ {11, 15, 16}hyS:y ∉ Shxy:x ≠ yhsubset:{x, y} ⊆ univ \ S⊢ #S ≤ 15
  have hcard : 2 ≤ (Finset.univ \ S).card := by
    rw [← Finset.card_pair hxyS:Finset (Fin 17)hS:(induce (↑S) graph).IsAcyclichfirst:¬{1, 13, 14} ⊆ Shsecond:¬{11, 15, 16} ⊆ Sx:Fin 17hxT:x ∈ {1, 13, 14}hxS:x ∉ Sy:Fin 17hyT:y ∈ {11, 15, 16}hyS:y ∉ Shxy:x ≠ yhsubset:{x, y} ⊆ univ \ S⊢ #{x, y} ≤ #(univ \ S)S:Finset (Fin 17)hS:(induce (↑S) graph).IsAcyclichfirst:¬{1, 13, 14} ⊆ Shsecond:¬{11, 15, 16} ⊆ Sx:Fin 17hxT:x ∈ {1, 13, 14}hxS:x ∉ Sy:Fin 17hyT:y ∈ {11, 15, 16}hyS:y ∉ Shxy:x ≠ yhsubset:{x, y} ⊆ univ \ S⊢ #{x, y} ≤ #(univ \ S)S:Finset (Fin 17)hS:(induce (↑S) graph).IsAcyclichfirst:¬{1, 13, 14} ⊆ Shsecond:¬{11, 15, 16} ⊆ Sx:Fin 17hxT:x ∈ {1, 13, 14}hxS:x ∉ Sy:Fin 17hyT:y ∈ {11, 15, 16}hyS:y ∉ Shxy:x ≠ yhsubset:{x, y} ⊆ univ \ Shcard:2 ≤ #(univ \ S)⊢ #S ≤ 15]S:Finset (Fin 17)hS:(induce (↑S) graph).IsAcyclichfirst:¬{1, 13, 14} ⊆ Shsecond:¬{11, 15, 16} ⊆ Sx:Fin 17hxT:x ∈ {1, 13, 14}hxS:x ∉ Sy:Fin 17hyT:y ∈ {11, 15, 16}hyS:y ∉ Shxy:x ≠ yhsubset:{x, y} ⊆ univ \ S⊢ #{x, y} ≤ #(univ \ S)S:Finset (Fin 17)hS:(induce (↑S) graph).IsAcyclichfirst:¬{1, 13, 14} ⊆ Shsecond:¬{11, 15, 16} ⊆ Sx:Fin 17hxT:x ∈ {1, 13, 14}hxS:x ∉ Sy:Fin 17hyT:y ∈ {11, 15, 16}hyS:y ∉ Shxy:x ≠ yhsubset:{x, y} ⊆ univ \ Shcard:2 ≤ #(univ \ S)⊢ #S ≤ 15
    exact Finset.card_le_card hsubsetS:Finset (Fin 17)hS:(induce (↑S) graph).IsAcyclichfirst:¬{1, 13, 14} ⊆ Shsecond:¬{11, 15, 16} ⊆ Sx:Fin 17hxT:x ∈ {1, 13, 14}hxS:x ∉ Sy:Fin 17hyT:y ∈ {11, 15, 16}hyS:y ∉ Shxy:x ≠ yhsubset:{x, y} ⊆ univ \ Shcard:2 ≤ #(univ \ S)⊢ #S ≤ 15S:Finset (Fin 17)hS:(induce (↑S) graph).IsAcyclichfirst:¬{1, 13, 14} ⊆ Shsecond:¬{11, 15, 16} ⊆ Sx:Fin 17hxT:x ∈ {1, 13, 14}hxS:x ∉ Sy:Fin 17hyT:y ∈ {11, 15, 16}hyS:y ∉ Shxy:x ≠ yhsubset:{x, y} ⊆ univ \ Shcard:2 ≤ #(univ \ S)⊢ #S ≤ 15
  have hpartition : (Finset.univ \ S).card + S.card = 17 := by
    simpa using Finset.card_sdiff_add_card_inter Finset.univ SS:Finset (Fin 17)hS:(induce (↑S) graph).IsAcyclichfirst:¬{1, 13, 14} ⊆ Shsecond:¬{11, 15, 16} ⊆ Sx:Fin 17hxT:x ∈ {1, 13, 14}hxS:x ∉ Sy:Fin 17hyT:y ∈ {11, 15, 16}hyS:y ∉ Shxy:x ≠ yhsubset:{x, y} ⊆ univ \ Shcard:2 ≤ #(univ \ S)hpartition:#(univ \ S) + #S = 17⊢ #S ≤ 15S:Finset (Fin 17)hS:(induce (↑S) graph).IsAcyclichfirst:¬{1, 13, 14} ⊆ Shsecond:¬{11, 15, 16} ⊆ Sx:Fin 17hxT:x ∈ {1, 13, 14}hxS:x ∉ Sy:Fin 17hyT:y ∈ {11, 15, 16}hyS:y ∉ Shxy:x ≠ yhsubset:{x, y} ⊆ univ \ Shcard:2 ≤ #(univ \ S)hpartition:#(univ \ S) + #S = 17⊢ #S ≤ 15
  omegaAll goals completed! 🐙

The largest induced forest in the counterexample has at most $15$ vertices.


@[category API, AMS 5]
lemma largest_induced_forest_le_fifteen : graph.largestInducedForestSize ≤ 15 := by⊢ graph.largestInducedForestSize ≤ 15
  unfold largestInducedForestSize⊢ sSup {n | ∃ s, (induce (↑s) graph).IsAcyclic ∧ #s = n} ≤ 15
  apply csSup_leh₁⊢ {n | ∃ s, (induce (↑s) graph).IsAcyclic ∧ #s = n}.Nonemptyh₂⊢ ∀ b ∈ {n | ∃ s, (induce (↑s) graph).IsAcyclic ∧ #s = n}, b ≤ 15
  ·h₁⊢ {n | ∃ s, (induce (↑s) graph).IsAcyclic ∧ #s = n}.Nonempty refine ⟨0, ∅, ?_, rfl⟩h₁⊢ (induce (↑∅) graph).IsAcyclic
    have : Subsingleton ↥(↑(∅ : Finset (Fin 17)) : Set (Fin 17)) :=
      ⟨fun a _ => False.elim (bya:↑↑∅x✝:↑↑∅⊢ Falseh₁this:Subsingleton ↑↑∅⊢ (induce (↑∅) graph).IsAcyclic simpa using a.propertyAll goals completed! 🐙h₁this:Subsingleton ↑↑∅⊢ (induce (↑∅) graph).IsAcyclic)⟩h₁this:Subsingleton ↑↑∅⊢ (induce (↑∅) graph).IsAcyclic
    exact SimpleGraph.IsAcyclic.of_subsingletonAll goals completed! 🐙
  ·h₂⊢ ∀ b ∈ {n | ∃ s, (induce (↑s) graph).IsAcyclic ∧ #s = n}, b ≤ 15 rintro n ⟨S, hS, rfl⟩h₂S:Finset (Fin 17)hS:(induce (↑S) graph).IsAcyclic⊢ #S ≤ 15
    exact forest_card_le_fifteen S hSAll goals completed! 🐙

end Counterexample

WOWII Conjecture 65:

Does every simple connected graph $G$ satisfy $f(G) \ge \operatorname{dist_min}(A) + \lceil \operatorname{dist_min}(M) / 3 \rceil$, where $A$ is the set of minimum-degree vertices, $M$ is the set of maximum-degree vertices, and $\operatorname{dist_min}(S)$ is the minimum distance between two distinct vertices of $S$ (see distMin).

The answer is no. Counterexample.graph has a conjectured lower bound of $16$, but every induced forest in it has at most $15$ vertices.


@[category research solved, AMS 5]
theorem conjecture65 : answer(False) ↔
    ∀ (α : Type) [Fintype α] [DecidableEq α] [Nontrivial α]
      (G : SimpleGraph α) [DecidableRel G.Adj] (_hG : G.Connected),
      let A : Set α := {v | G.degree v = G.minDegree}
      let M : Set α := {v | G.degree v = G.maxDegree}
      (distMin G A : ℝ) + ⌈(distMin G M : ℝ) / 3⌉ ≤
        (G.largestInducedForestSize : ℝ) := by⊢ False ↔
  ∀ (α : Type) [inst : Fintype α] [inst_1 : DecidableEq α] [Nontrivial α] (G : SimpleGraph α)
    [inst_3 : DecidableRel G.Adj],
    G.Connected →
      let A := {v | G.degree v = G.minDegree};
      let M := {v | G.degree v = G.maxDegree};
      ↑(G.distMin A) + ↑⌈↑(G.distMin M) / 3⌉ ≤ ↑G.largestInducedForestSize
  constructormp⊢ False →
  ∀ (α : Type) [inst : Fintype α] [inst_1 : DecidableEq α] [Nontrivial α] (G : SimpleGraph α)
    [inst_3 : DecidableRel G.Adj],
    G.Connected →
      let A := {v | G.degree v = G.minDegree};
      let M := {v | G.degree v = G.maxDegree};
      ↑(G.distMin A) + ↑⌈↑(G.distMin M) / 3⌉ ≤ ↑G.largestInducedForestSizempr⊢ (∀ (α : Type) [inst : Fintype α] [inst_1 : DecidableEq α] [Nontrivial α] (G : SimpleGraph α)
    [inst_3 : DecidableRel G.Adj],
    G.Connected →
      let A := {v | G.degree v = G.minDegree};
      let M := {v | G.degree v = G.maxDegree};
      ↑(G.distMin A) + ↑⌈↑(G.distMin M) / 3⌉ ≤ ↑G.largestInducedForestSize) →
  False
  ·mp⊢ False →
  ∀ (α : Type) [inst : Fintype α] [inst_1 : DecidableEq α] [Nontrivial α] (G : SimpleGraph α)
    [inst_3 : DecidableRel G.Adj],
    G.Connected →
      let A := {v | G.degree v = G.minDegree};
      let M := {v | G.degree v = G.maxDegree};
      ↑(G.distMin A) + ↑⌈↑(G.distMin M) / 3⌉ ≤ ↑G.largestInducedForestSize exact False.elimAll goals completed! 🐙
  ·mpr⊢ (∀ (α : Type) [inst : Fintype α] [inst_1 : DecidableEq α] [Nontrivial α] (G : SimpleGraph α)
    [inst_3 : DecidableRel G.Adj],
    G.Connected →
      let A := {v | G.degree v = G.minDegree};
      let M := {v | G.degree v = G.maxDegree};
      ↑(G.distMin A) + ↑⌈↑(G.distMin M) / 3⌉ ≤ ↑G.largestInducedForestSize) →
  False intro hmprh:∀ (α : Type) [inst : Fintype α] [inst_1 : DecidableEq α] [Nontrivial α] (G : SimpleGraph α)
  [inst_3 : DecidableRel G.Adj],
  G.Connected →
    let A := {v | G.degree v = G.minDegree};
    let M := {v | G.degree v = G.maxDegree};
    ↑(G.distMin A) + ↑⌈↑(G.distMin M) / 3⌉ ≤ ↑G.largestInducedForestSize⊢ False
    have hc := h (Fin 17) Counterexample.graph Counterexample.connectedmprh:∀ (α : Type) [inst : Fintype α] [inst_1 : DecidableEq α] [Nontrivial α] (G : SimpleGraph α)
  [inst_3 : DecidableRel G.Adj],
  G.Connected →
    let A := {v | G.degree v = G.minDegree};
    let M := {v | G.degree v = G.maxDegree};
    ↑(G.distMin A) + ↑⌈↑(G.distMin M) / 3⌉ ≤ ↑G.largestInducedForestSizehc:let A := {v | Counterexample.graph.degree v = Counterexample.graph.minDegree};
let M := {v | Counterexample.graph.degree v = Counterexample.graph.maxDegree};
↑(Counterexample.graph.distMin A) + ↑⌈↑(Counterexample.graph.distMin M) / 3⌉ ≤
  ↑Counterexample.graph.largestInducedForestSize⊢ False
    dsimp only at hcmprh:∀ (α : Type) [inst : Fintype α] [inst_1 : DecidableEq α] [Nontrivial α] (G : SimpleGraph α)
  [inst_3 : DecidableRel G.Adj],
  G.Connected →
    let A := {v | G.degree v = G.minDegree};
    let M := {v | G.degree v = G.maxDegree};
    ↑(G.distMin A) + ↑⌈↑(G.distMin M) / 3⌉ ≤ ↑G.largestInducedForestSizehc:↑(Counterexample.graph.distMin {v | Counterexample.graph.degree v = Counterexample.graph.minDegree}) +
    ↑⌈↑(Counterexample.graph.distMin {v | Counterexample.graph.degree v = Counterexample.graph.maxDegree}) / 3⌉ ≤
  ↑Counterexample.graph.largestInducedForestSize⊢ False
    rw [Counterexample.min_degree_vertices,mprh:∀ (α : Type) [inst : Fintype α] [inst_1 : DecidableEq α] [Nontrivial α] (G : SimpleGraph α)
  [inst_3 : DecidableRel G.Adj],
  G.Connected →
    let A := {v | G.degree v = G.minDegree};
    let M := {v | G.degree v = G.maxDegree};
    ↑(G.distMin A) + ↑⌈↑(G.distMin M) / 3⌉ ≤ ↑G.largestInducedForestSizehc:↑(Counterexample.graph.distMin {0, 12}) +
    ↑⌈↑(Counterexample.graph.distMin {v | Counterexample.graph.degree v = Counterexample.graph.maxDegree}) / 3⌉ ≤
  ↑Counterexample.graph.largestInducedForestSize⊢ Falsemprh:∀ (α : Type) [inst : Fintype α] [inst_1 : DecidableEq α] [Nontrivial α] (G : SimpleGraph α)
  [inst_3 : DecidableRel G.Adj],
  G.Connected →
    let A := {v | G.degree v = G.minDegree};
    let M := {v | G.degree v = G.maxDegree};
    ↑(G.distMin A) + ↑⌈↑(G.distMin M) / 3⌉ ≤ ↑G.largestInducedForestSizehc:↑12 + ↑⌈↑10 / 3⌉ ≤ ↑Counterexample.graph.largestInducedForestSize⊢ False Counterexample.max_degree_vertices,mprh:∀ (α : Type) [inst : Fintype α] [inst_1 : DecidableEq α] [Nontrivial α] (G : SimpleGraph α)
  [inst_3 : DecidableRel G.Adj],
  G.Connected →
    let A := {v | G.degree v = G.minDegree};
    let M := {v | G.degree v = G.maxDegree};
    ↑(G.distMin A) + ↑⌈↑(G.distMin M) / 3⌉ ≤ ↑G.largestInducedForestSizehc:↑(Counterexample.graph.distMin {0, 12}) + ↑⌈↑(Counterexample.graph.distMin {1, 11}) / 3⌉ ≤
  ↑Counterexample.graph.largestInducedForestSize⊢ Falsemprh:∀ (α : Type) [inst : Fintype α] [inst_1 : DecidableEq α] [Nontrivial α] (G : SimpleGraph α)
  [inst_3 : DecidableRel G.Adj],
  G.Connected →
    let A := {v | G.degree v = G.minDegree};
    let M := {v | G.degree v = G.maxDegree};
    ↑(G.distMin A) + ↑⌈↑(G.distMin M) / 3⌉ ≤ ↑G.largestInducedForestSizehc:↑12 + ↑⌈↑10 / 3⌉ ≤ ↑Counterexample.graph.largestInducedForestSize⊢ False
      Counterexample.distMin_min_degree_vertices,mprh:∀ (α : Type) [inst : Fintype α] [inst_1 : DecidableEq α] [Nontrivial α] (G : SimpleGraph α)
  [inst_3 : DecidableRel G.Adj],
  G.Connected →
    let A := {v | G.degree v = G.minDegree};
    let M := {v | G.degree v = G.maxDegree};
    ↑(G.distMin A) + ↑⌈↑(G.distMin M) / 3⌉ ≤ ↑G.largestInducedForestSizehc:↑12 + ↑⌈↑(Counterexample.graph.distMin {1, 11}) / 3⌉ ≤ ↑Counterexample.graph.largestInducedForestSize⊢ Falsemprh:∀ (α : Type) [inst : Fintype α] [inst_1 : DecidableEq α] [Nontrivial α] (G : SimpleGraph α)
  [inst_3 : DecidableRel G.Adj],
  G.Connected →
    let A := {v | G.degree v = G.minDegree};
    let M := {v | G.degree v = G.maxDegree};
    ↑(G.distMin A) + ↑⌈↑(G.distMin M) / 3⌉ ≤ ↑G.largestInducedForestSizehc:↑12 + ↑⌈↑10 / 3⌉ ≤ ↑Counterexample.graph.largestInducedForestSize⊢ False
      Counterexample.distMin_max_degree_verticesmprh:∀ (α : Type) [inst : Fintype α] [inst_1 : DecidableEq α] [Nontrivial α] (G : SimpleGraph α)
  [inst_3 : DecidableRel G.Adj],
  G.Connected →
    let A := {v | G.degree v = G.minDegree};
    let M := {v | G.degree v = G.maxDegree};
    ↑(G.distMin A) + ↑⌈↑(G.distMin M) / 3⌉ ≤ ↑G.largestInducedForestSizehc:↑12 + ↑⌈↑10 / 3⌉ ≤ ↑Counterexample.graph.largestInducedForestSize⊢ Falsemprh:∀ (α : Type) [inst : Fintype α] [inst_1 : DecidableEq α] [Nontrivial α] (G : SimpleGraph α)
  [inst_3 : DecidableRel G.Adj],
  G.Connected →
    let A := {v | G.degree v = G.minDegree};
    let M := {v | G.degree v = G.maxDegree};
    ↑(G.distMin A) + ↑⌈↑(G.distMin M) / 3⌉ ≤ ↑G.largestInducedForestSizehc:↑12 + ↑⌈↑10 / 3⌉ ≤ ↑Counterexample.graph.largestInducedForestSize⊢ False] at hcmprh:∀ (α : Type) [inst : Fintype α] [inst_1 : DecidableEq α] [Nontrivial α] (G : SimpleGraph α)
  [inst_3 : DecidableRel G.Adj],
  G.Connected →
    let A := {v | G.degree v = G.minDegree};
    let M := {v | G.degree v = G.maxDegree};
    ↑(G.distMin A) + ↑⌈↑(G.distMin M) / 3⌉ ≤ ↑G.largestInducedForestSizehc:↑12 + ↑⌈↑10 / 3⌉ ≤ ↑Counterexample.graph.largestInducedForestSize⊢ False
    have hf := Counterexample.largest_induced_forest_le_fifteenmprh:∀ (α : Type) [inst : Fintype α] [inst_1 : DecidableEq α] [Nontrivial α] (G : SimpleGraph α)
  [inst_3 : DecidableRel G.Adj],
  G.Connected →
    let A := {v | G.degree v = G.minDegree};
    let M := {v | G.degree v = G.maxDegree};
    ↑(G.distMin A) + ↑⌈↑(G.distMin M) / 3⌉ ≤ ↑G.largestInducedForestSizehc:↑12 + ↑⌈↑10 / 3⌉ ≤ ↑Counterexample.graph.largestInducedForestSizehf:Counterexample.graph.largestInducedForestSize ≤ 15⊢ False
    norm_num at hcmprh:∀ (α : Type) [inst : Fintype α] [inst_1 : DecidableEq α] [Nontrivial α] (G : SimpleGraph α)
  [inst_3 : DecidableRel G.Adj],
  G.Connected →
    let A := {v | G.degree v = G.minDegree};
    let M := {v | G.degree v = G.maxDegree};
    ↑(G.distMin A) + ↑⌈↑(G.distMin M) / 3⌉ ≤ ↑G.largestInducedForestSizehf:Counterexample.graph.largestInducedForestSize ≤ 15hc:16 ≤ Counterexample.graph.largestInducedForestSize⊢ False
    exact (byh:∀ (α : Type) [inst : Fintype α] [inst_1 : DecidableEq α] [Nontrivial α] (G : SimpleGraph α)
  [inst_3 : DecidableRel G.Adj],
  G.Connected →
    let A := {v | G.degree v = G.minDegree};
    let M := {v | G.degree v = G.maxDegree};
    ↑(G.distMin A) + ↑⌈↑(G.distMin M) / 3⌉ ≤ ↑G.largestInducedForestSizehf:Counterexample.graph.largestInducedForestSize ≤ 15hc:16 ≤ Counterexample.graph.largestInducedForestSize⊢ ¬16 ≤ Counterexample.graph.largestInducedForestSize omegaAll goals completed! 🐙 : ¬(16 : ℕ) ≤ Counterexample.graph.largestInducedForestSize)
      (byh:∀ (α : Type) [inst : Fintype α] [inst_1 : DecidableEq α] [Nontrivial α] (G : SimpleGraph α)
  [inst_3 : DecidableRel G.Adj],
  G.Connected →
    let A := {v | G.degree v = G.minDegree};
    let M := {v | G.degree v = G.maxDegree};
    ↑(G.distMin A) + ↑⌈↑(G.distMin M) / 3⌉ ≤ ↑G.largestInducedForestSizehf:Counterexample.graph.largestInducedForestSize ≤ 15hc:16 ≤ Counterexample.graph.largestInducedForestSize⊢ 16 ≤ Counterexample.graph.largestInducedForestSize exact_mod_cast hcAll goals completed! 🐙)

-- Sanity checks

The largestInducedForestSize is nonneg.

@[category test, AMS 5]
example (G : SimpleGraph (Fin 3)) : 0 ≤ G.largestInducedForestSize := Nat.zero_le _

In the complete graph K₃, min degree equals max degree (regular graph).

@[category test, AMS 5]
example : (⊤ : SimpleGraph (Fin 3)).minDegree = (⊤ : SimpleGraph (Fin 3)).maxDegree := by⊢ ⊤.minDegree = ⊤.maxDegree
  decide +nativeAll goals completed! 🐙

distMin G S is always nonneg.

@[category test, AMS 5]
example (G : SimpleGraph (Fin 3)) (S : Set (Fin 3)) : 0 ≤ distMin G S := Nat.zero_le _



/-- In $K_2$, the minimum distance between its two vertices is $1$. -/
@[category test, AMS 5]
example : distMin (⊤ : SimpleGraph (Fin 2)) ({0, 1} : Set (Fin 2)) = 1 := by⊢ ⊤.distMin {0, 1} = 1
  unfold distMin⊢ (let pairs := {p ∈ {0, 1}.toFinset ×ˢ {0, 1}.toFinset | p.1 ≠ p.2};
  if h : pairs.Nonempty then (image (fun p ↦ ⊤.dist p.1 p.2) pairs).min' ⋯ else 0) =
  1
  dsimp only⊢ (if h : {p ∈ {0, 1}.toFinset ×ˢ {0, 1}.toFinset | p.1 ≠ p.2}.Nonempty then
    (image (fun p ↦ ⊤.dist p.1 p.2) ({p ∈ {0, 1}.toFinset ×ˢ {0, 1}.toFinset | p.1 ≠ p.2})).min' ⋯
  else 0) =
  1
  split_ifs with hposh:{p ∈ {0, 1}.toFinset ×ˢ {0, 1}.toFinset | p.1 ≠ p.2}.Nonempty⊢ (image (fun p ↦ ⊤.dist p.1 p.2) ({p ∈ {0, 1}.toFinset ×ˢ {0, 1}.toFinset | p.1 ≠ p.2})).min' ⋯ = 1negh:¬{p ∈ {0, 1}.toFinset ×ˢ {0, 1}.toFinset | p.1 ≠ p.2}.Nonempty⊢ False
  ·posh:{p ∈ {0, 1}.toFinset ×ˢ {0, 1}.toFinset | p.1 ≠ p.2}.Nonempty⊢ (image (fun p ↦ ⊤.dist p.1 p.2) ({p ∈ {0, 1}.toFinset ×ˢ {0, 1}.toFinset | p.1 ≠ p.2})).min' ⋯ = 1 rw [Finset.min'_eq_iffposh:{p ∈ {0, 1}.toFinset ×ˢ {0, 1}.toFinset | p.1 ≠ p.2}.Nonempty⊢ 1 ∈ image (fun p ↦ ⊤.dist p.1 p.2) ({p ∈ {0, 1}.toFinset ×ˢ {0, 1}.toFinset | p.1 ≠ p.2}) ∧
  ∀ b ∈ image (fun p ↦ ⊤.dist p.1 p.2) ({p ∈ {0, 1}.toFinset ×ˢ {0, 1}.toFinset | p.1 ≠ p.2}), 1 ≤ bposh:{p ∈ {0, 1}.toFinset ×ˢ {0, 1}.toFinset | p.1 ≠ p.2}.Nonempty⊢ 1 ∈ image (fun p ↦ ⊤.dist p.1 p.2) ({p ∈ {0, 1}.toFinset ×ˢ {0, 1}.toFinset | p.1 ≠ p.2}) ∧
  ∀ b ∈ image (fun p ↦ ⊤.dist p.1 p.2) ({p ∈ {0, 1}.toFinset ×ˢ {0, 1}.toFinset | p.1 ≠ p.2}), 1 ≤ b]posh:{p ∈ {0, 1}.toFinset ×ˢ {0, 1}.toFinset | p.1 ≠ p.2}.Nonempty⊢ 1 ∈ image (fun p ↦ ⊤.dist p.1 p.2) ({p ∈ {0, 1}.toFinset ×ˢ {0, 1}.toFinset | p.1 ≠ p.2}) ∧
  ∀ b ∈ image (fun p ↦ ⊤.dist p.1 p.2) ({p ∈ {0, 1}.toFinset ×ˢ {0, 1}.toFinset | p.1 ≠ p.2}), 1 ≤ b
    constructorpos.lefth:{p ∈ {0, 1}.toFinset ×ˢ {0, 1}.toFinset | p.1 ≠ p.2}.Nonempty⊢ 1 ∈ image (fun p ↦ ⊤.dist p.1 p.2) ({p ∈ {0, 1}.toFinset ×ˢ {0, 1}.toFinset | p.1 ≠ p.2})pos.righth:{p ∈ {0, 1}.toFinset ×ˢ {0, 1}.toFinset | p.1 ≠ p.2}.Nonempty⊢ ∀ b ∈ image (fun p ↦ ⊤.dist p.1 p.2) ({p ∈ {0, 1}.toFinset ×ˢ {0, 1}.toFinset | p.1 ≠ p.2}), 1 ≤ b
    ·pos.lefth:{p ∈ {0, 1}.toFinset ×ˢ {0, 1}.toFinset | p.1 ≠ p.2}.Nonempty⊢ 1 ∈ image (fun p ↦ ⊤.dist p.1 p.2) ({p ∈ {0, 1}.toFinset ×ˢ {0, 1}.toFinset | p.1 ≠ p.2}) refine Finset.mem_image.mpr ⟨(0, 1), ?_, ?_⟩pos.left.refine_1h:{p ∈ {0, 1}.toFinset ×ˢ {0, 1}.toFinset | p.1 ≠ p.2}.Nonempty⊢ (0, 1) ∈ {p ∈ {0, 1}.toFinset ×ˢ {0, 1}.toFinset | p.1 ≠ p.2}pos.left.refine_2h:{p ∈ {0, 1}.toFinset ×ˢ {0, 1}.toFinset | p.1 ≠ p.2}.Nonempty⊢ ⊤.dist (0, 1).1 (0, 1).2 = 1
      ·pos.left.refine_1h:{p ∈ {0, 1}.toFinset ×ˢ {0, 1}.toFinset | p.1 ≠ p.2}.Nonempty⊢ (0, 1) ∈ {p ∈ {0, 1}.toFinset ×ˢ {0, 1}.toFinset | p.1 ≠ p.2} simpAll goals completed! 🐙
      ·pos.left.refine_2h:{p ∈ {0, 1}.toFinset ×ˢ {0, 1}.toFinset | p.1 ≠ p.2}.Nonempty⊢ ⊤.dist (0, 1).1 (0, 1).2 = 1 simpAll goals completed! 🐙
    ·pos.righth:{p ∈ {0, 1}.toFinset ×ˢ {0, 1}.toFinset | p.1 ≠ p.2}.Nonempty⊢ ∀ b ∈ image (fun p ↦ ⊤.dist p.1 p.2) ({p ∈ {0, 1}.toFinset ×ˢ {0, 1}.toFinset | p.1 ≠ p.2}), 1 ≤ b intro d hdpos.righth:{p ∈ {0, 1}.toFinset ×ˢ {0, 1}.toFinset | p.1 ≠ p.2}.Nonemptyd:ℕhd:d ∈ image (fun p ↦ ⊤.dist p.1 p.2) ({p ∈ {0, 1}.toFinset ×ˢ {0, 1}.toFinset | p.1 ≠ p.2})⊢ 1 ≤ d
      obtain ⟨p, hp, rfl⟩ := Finset.mem_image.mp hdpos.righth:{p ∈ {0, 1}.toFinset ×ˢ {0, 1}.toFinset | p.1 ≠ p.2}.Nonemptyp:Fin 2 × Fin 2hp:p ∈ {p ∈ {0, 1}.toFinset ×ˢ {0, 1}.toFinset | p.1 ≠ p.2}hd:⊤.dist p.1 p.2 ∈ image (fun p ↦ ⊤.dist p.1 p.2) ({p ∈ {0, 1}.toFinset ×ˢ {0, 1}.toFinset | p.1 ≠ p.2})⊢ 1 ≤ ⊤.dist p.1 p.2
      have hne : p.1 ≠ p.2 := (Finset.mem_filter.mp hp).2pos.righth:{p ∈ {0, 1}.toFinset ×ˢ {0, 1}.toFinset | p.1 ≠ p.2}.Nonemptyp:Fin 2 × Fin 2hp:p ∈ {p ∈ {0, 1}.toFinset ×ˢ {0, 1}.toFinset | p.1 ≠ p.2}hd:⊤.dist p.1 p.2 ∈ image (fun p ↦ ⊤.dist p.1 p.2) ({p ∈ {0, 1}.toFinset ×ˢ {0, 1}.toFinset | p.1 ≠ p.2})hne:p.1 ≠ p.2⊢ 1 ≤ ⊤.dist p.1 p.2
      simp [SimpleGraph.dist_top_of_ne hne]All goals completed! 🐙
  ·negh:¬{p ∈ {0, 1}.toFinset ×ˢ {0, 1}.toFinset | p.1 ≠ p.2}.Nonempty⊢ False exfalsonegh:¬{p ∈ {0, 1}.toFinset ×ˢ {0, 1}.toFinset | p.1 ≠ p.2}.Nonempty⊢ False
    apply hnegh:¬{p ∈ {0, 1}.toFinset ×ˢ {0, 1}.toFinset | p.1 ≠ p.2}.Nonempty⊢ {p ∈ {0, 1}.toFinset ×ˢ {0, 1}.toFinset | p.1 ≠ p.2}.Nonempty
    exact ⟨(0, 1), byh:¬{p ∈ {0, 1}.toFinset ×ˢ {0, 1}.toFinset | p.1 ≠ p.2}.Nonempty⊢ (0, 1) ∈ {p ∈ {0, 1}.toFinset ×ˢ {0, 1}.toFinset | p.1 ≠ p.2} simpAll goals completed! 🐙⟩

A singleton contains no distinct pair, so distMin uses its degenerate-case fallback.

@[category test, AMS 5]
example : distMin (⊤ : SimpleGraph (Fin 3)) ({0} : Set (Fin 3)) = 0 := by⊢ ⊤.distMin {0} = 0
  simp [distMin]All goals completed! 🐙

end WrittenOnTheWallII.GraphConjecture65