Trace — 2607.20376v1

$ /bin/bash -lc "pwd && rg --files -g 'paper.txt' -g 'paper.pdf' -g 'paper.json' -g 'AGENTS.md' -g 'README.md' | sed -n '1,120p' && wc -l paper.txt && sed -n '1,240p' paper.txt"
/work
paper.json
paper.pdf
paper.txt
repro/Cache/README.md
repro/scripts/bench/build/README.md
repro/scripts/bench/open-mathlib/README.md
repro/scripts/bench/lint/README.md
repro/DownstreamTest/README.md
repro/scripts/bench/README.md
repro/scripts/bench/size/README.md
repro/scripts/README.md
repro/widget/src/penrose/README.md
repro/Archive/Imo/README.md
repro/Archive/Wiedijk100Theorems/README.md
repro/Archive/README.md
repro/Mathlib/Probability/Combinatorics/README.md
repro/Mathlib/Algebra/Notation/README.md
repro/README.md
repro/Mathlib/Analysis/Convex/Cone/README.md
repro/Mathlib/Analysis/Convex/README.md
repro/Mathlib/Algebra/README.md
repro/Mathlib/Geometry/Convex/Cone/README.md
repro/Mathlib/Geometry/Convex/README.md
repro/Mathlib/Geometry/Group/README.md
repro/Mathlib/Geometry/Group/Growth/README.md
repro/Mathlib/Order/README.md
207 paper.txt
The Erdős-Lovász Tihany Conjecture holds for all even-hole-free
graphs
Zi-Xia Song∗
Department of Mathematics, University of Central Florida, Orlando, FL 32816, USA

arXiv:2607.20376v1 [math.CO] 22 Jul 2026

Abstract
Let s, t ≥ 2 be integers. A graph G is (s, t)-splittable if V (G) can be partitioned into two
sets S and T such that χ(G[S]) ≥ s and χ(G[T ]) ≥ t. The Erdős-Lovász Tihany Conjecture
from 1968 asserts that every graph G satisfying ω(G) < χ(G) = s + t − 1 is (s, t)-splittable. A
vertex of a graph is bisimplicial if the set of its neighbors can be expressed as the union of two
cliques. Let G be a graph with ω(G) < χ(G) = s + t − 1. We prove that if G does not contain
C4 as an induced subgraph and every induced subgraph of G has a bisimplicial vertex, then G is
(s, t)-splittable. Combining our result with a recent result of Chudnovsky and Seymour, which
states that every non-empty even-hole-free graph has a bisimplicial vertex, we obtain that the
Erdős-Lovász Tihany Conjecture holds for all even-hole-free graphs.

1

Introduction

All graphs in this paper are finite and simple. For a graph G, we use V (G) t

$ /bin/bash -lc "git status --short && sed -n '1,200p' README.md && rg -n \"def chromaticNumber|chromaticNumber|IsColorable|colorable|CliqueNumber|cliqueNumber|IsClique|induce|Induce\" Mathlib/Combinatorics/SimpleGraph | head -n 260"
# mathlib4

![GitHub CI](https://github.com/leanprover-community/mathlib4/actions/workflows/build.yml/badge.svg?branch=master)
[![Bors enabled](https://raw.githubusercontent.com/bors-ng/bors-ng.github.io/refs/heads/master/images/badge_small.svg)](https://mathlib-bors-ca18eefec4cb.herokuapp.com/repositories/16)
[![project chat](https://img.shields.io/badge/zulip-join_chat-brightgreen.svg)](https://leanprover.zulipchat.com)
[![Gitpod Ready-to-Code](https://img.shields.io/badge/Gitpod-ready--to--code-blue?logo=gitpod)](https://gitpod.io/#https://github.com/leanprover-community/mathlib4)

[Mathlib](https://leanprover-community.github.io) is a user maintained library for the [Lean theorem prover](https://leanprover.github.io).
It contains both programming infrastructure and mathematics,
as well as tactics that use the former and allow to develop the latter.

## Installation

You can find detailed instructions to install Lean, mathlib, and supporting tools on [our website](https://leanprover-community.github.io/get_started.html).
Alternatively, click on one of the buttons below to open a GitHub Codespace or a Gitpod workspace containing the project.

[![Open in GitHub Codespaces](https://github.com/codespaces/badge.svg)](https://codespaces.new/leanprover-community/mathlib4)

[![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/#https://github.com/leanprover-community/mathlib4)

## Using `mathlib4` as a dependency

Please refer to
[https://github.com/leanprover-community/mathlib4/wiki/Using-mathlib4-as-a-dependency](https://github.com/leanprover-community/mathlib4/wiki/Using-mathlib4-as-a-dependency)

## Experimenting

Got everything installed? Why not start with the [tutorial project](https://leanprover-community.github.io/install/project.html)?

For more pointers, see [Learning Lean](https://leanprover-community.github.io/learn.html).

## Documentation

Besides the installation guides above and [Lean's general
documentation](https://docs.lea

$ /bin/bash -lc "sed -n '1,560p' Mathlib/Combinatorics/SimpleGraph/Coloring/Vertex.lean | sed -n '1,220p'; rg -n \"cliqueNumber|CliqueFree|isNClique|IsClique.*card|card.*IsClique|Coloring.*induce|induce.*Color\" Mathlib/Combinatorics/SimpleGraph | head -n 300; rg -n \"namespace.*Cycle|IsCycle|IsInducedCycle|cycle.*induce|IsHole|hole\" Mathlib/Combinatorics/SimpleGraph | head -n 240"
/-
Copyright (c) 2021 Arthur Paulino. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Arthur Paulino, Kyle Miller
-/
module

public import Mathlib.Combinatorics.SimpleGraph.Clique
public import Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
public import Mathlib.Combinatorics.SimpleGraph.Copy
public import Mathlib.Data.ENat.Lattice
public import Mathlib.Data.Nat.Cast.Order.Ring
public import Mathlib.Data.Setoid.Partition
public import Mathlib.Order.Antichain
public import Mathlib.Order.Lattice.Nat

/-!
# Graph Coloring

This module defines colorings of simple graphs (also known as proper colorings in the literature).
A graph coloring is the attribution of "colors" to all of its vertices such that adjacent vertices
have different colors.
A coloring can be represented as a homomorphism into a complete graph, whose vertices represent
the colors.

## Main definitions

* `G.Coloring α` is the type of `α`-colorings of a simple graph `G`,
  with `α` being the set of available colors. The type is defined to
  be homomorphisms from `G` into the complete graph on `α`, and
  colorings have a coercion to `V → α`.

* `G.Colorable n` is the proposition that `G` is `n`-colorable, which
  is whether there exists a coloring with at most *n* colors.

* `G.chromaticNumber` is the minimal `n` such that `G` is `n`-colorable,
  or `⊤` if it cannot be colored with finitely many colors.
  (Cardinal-valued chromatic numbers are more niche, so we stick to `ℕ∞`.)
  We write `G.chromaticNumber ≠ ⊤` to mean a graph is colorable with finitely many colors.

* `C.colorClass c` is the set of vertices colored by `c : α` in the coloring `C : G.Coloring α`.

* `C.colorClasses` is the set containing all color classes.

## TODO

  * Gather material from:
    * https://github.com/leanprover-community/mathlib/blob/simple_graph_matching/src/combinatorics/simple_graph/coloring.lean
    * https://github.com/kmill/lean-graphcoloring/blob/master/src/g

$ /bin/bash -lc "sed -n '520,610p' Mathlib/Combinatorics/SimpleGraph/Coloring/Vertex.lean; sed -n '680,790p' Mathlib/Combinatorics/SimpleGraph/Clique.lean; sed -n '1,230p' Mathlib/Combinatorics/SimpleGraph/Copy.lean; sed -n '130,205p' Mathlib/Combinatorics/SimpleGraph/CycleGraph.lean; rg -n \"Colorable.*induce|induce.*Colorable|coloring.*induce|induce.*coloring|chromaticNumber_induce\" Mathlib/Combinatorics/SimpleGraph -g '*.lean'"
· contrapose! h
    by_cases h' : IsEmpty V
    · simp [chromaticNumber_eq_zero_of_isEmpty]
    · simp [chromaticNumber_eq_one_iff.mpr ⟨h, by simpa using h'⟩]
  · obtain ⟨_, _, h⟩ := ne_bot_iff_exists_adj.mp h
    exact two_le_chromaticNumber_of_adj h

/-- The bicoloring of a complete bipartite graph using whether a vertex
is on the left or on the right. -/
def CompleteBipartiteGraph.bicoloring (V W : Type*) : (completeBipartiteGraph V W).Coloring Bool :=
  Coloring.mk (fun v => v.isRight)
    (by
      intro v w
      cases v <;> cases w <;> simp)

theorem CompleteBipartiteGraph.chromaticNumber {V W : Type*} [Nonempty V] [Nonempty W] :
    (completeBipartiteGraph V W).chromaticNumber = 2 := by
  rw [← Nat.cast_two, chromaticNumber_eq_iff_forall_surjective
    (by simpa using (CompleteBipartiteGraph.bicoloring V W).colorable)]
  intro C b
  have v := Classical.arbitrary V
  have w := Classical.arbitrary W
  have h : (completeBipartiteGraph V W).Adj (Sum.inl v) (Sum.inr w) := by simp
  by_cases he : C (Sum.inl v) = b
  · exact ⟨_, he⟩
  by_cases he' : C (Sum.inr w) = b
  · exact ⟨_, he'⟩
  · simpa using two_lt_card_iff.2 ⟨_, _, _, C.valid h, he, he'⟩

/-! ### Cliques -/

theorem IsClique.card_le_of_colorable {s : Finset V} (h : G.IsClique s) (hc : G.Colorable n) :
    s.card ≤ n := by
  simpa using! hc.card_le_of_pairwise_adj (Subtype.val : s → V) <| by simpa [Pairwise] using! h

theorem IsClique.card_le_of_coloring {s : Finset V} (h : G.IsClique s) [Fintype α]
    (C : G.Coloring α) : s.card ≤ Fintype.card α := h.card_le_of_colorable C.colorable

theorem IsClique.card_le_chromaticNumber {s : Finset V} (h : G.IsClique s) :
    s.card ≤ G.chromaticNumber :=
  le_chromaticNumber_of_pairwise_adj (by simp) (Subtype.val : s → V) <| by simpa [Pairwise] using! h

theorem cliqueNum_le_chromaticNumber : G.cliqueNum ≤ G.chromaticNumber := by
  have ⟨s, hs⟩ := G.exists_isNClique_cliqueNum
  exact hs.card_eq ▸ hs.isClique.card_le_chromaticNumber

protected theorem Colorable.cliq

$ /bin/bash -lc "sed -n '1,145p' Mathlib/Combinatorics/SimpleGraph/CycleGraph.lean; rg -n \"def IsIndContained|IsIndContained.*iff|indContained|induce.*embedding|Embedding.*induce\" Mathlib/Combinatorics/SimpleGraph/Copy.lean Mathlib/Combinatorics/SimpleGraph/*.lean | head -n 180; sed -n '230,430p' Mathlib/Combinatorics/SimpleGraph/Copy.lean; sed -n '150,220p' Mathlib/Combinatorics/SimpleGraph/Clique.lean; sed -n '235,290p' Mathlib/Combinatorics/SimpleGraph/Coloring/Vertex.lean"
/-
Copyright (c) 2024 Iván Renison, Bhavik Mehta. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Iván Renison, Bhavik Mehta
-/
module

public import Mathlib.Combinatorics.SimpleGraph.Hasse

/-!
# Definition of cycle graphs

This file defines and proves several fact about cycle graphs on `n` vertices and the cycle around
the cycle graph when `n ≥ 3`.

## Main declarations

* `SimpleGraph.cycleGraph n`: the cycle graph over `Fin n`.
* `(SimpleGraph.cycleGraph n).cycle`: the cycle around `cycleGraph (n + 3)` starting at 0.
-/

@[expose] public section

namespace SimpleGraph

open Walk

/-- Cycle graph over `Fin n` -/
def cycleGraph : (n : ℕ) → SimpleGraph (Fin n)
  | 0 | 1 => ⊥
  | _ + 2 => {
    Adj a b := a - b = 1 ∨ b - a = 1
  }

instance : (n : ℕ) → DecidableRel (cycleGraph n).Adj
  | 0 | 1 => fun _ _ => inferInstanceAs (Decidable False)
  | _ + 2 => by unfold cycleGraph; infer_instance

theorem cycleGraph_zero_adj {u v : Fin 0} : ¬(cycleGraph 0).Adj u v := id

theorem cycleGraph_zero_eq_bot : cycleGraph 0 = ⊥ := Subsingleton.elim _ _
theorem cycleGraph_one_eq_bot : cycleGraph 1 = ⊥ := Subsingleton.elim _ _
theorem cycleGraph_zero_eq_top : cycleGraph 0 = ⊤ := Subsingleton.elim _ _
theorem cycleGraph_one_eq_top : cycleGraph 1 = ⊤ := Subsingleton.elim _ _

theorem cycleGraph_two_eq_top : cycleGraph 2 = ⊤ := by
  simp only [SimpleGraph.ext_iff, funext_iff]
  decide

theorem cycleGraph_three_eq_top : cycleGraph 3 = ⊤ := by
  simp only [SimpleGraph.ext_iff, funext_iff]
  decide

theorem cycleGraph_one_adj {u v : Fin 1} : ¬(cycleGraph 1).Adj u v := by
  simp [cycleGraph_one_eq_bot]

theorem cycleGraph_adj {n : ℕ} {u v : Fin (n + 2)} :
    (cycleGraph (n + 2)).Adj u v ↔ u - v = 1 ∨ v - u = 1 := Iff.rfl

theorem cycleGraph_adj' {n : ℕ} {u v : Fin n} :
    (cycleGraph n).Adj u v ↔ (u - v).val = 1 ∨ (v - u).val = 1 := by
  match n with
  | 0 => exact u.elim0
  | 1 => simp [cycleGraph_one_adj]
  | n + 2 => simp [cycleGraph_a

$ /bin/bash -lc "rg -n \"exists.*min.*image|exists_min_image|min'_.*image|min.*apply.*∀.*∈\" Mathlib/Data/Finset Mathlib | head -n 160; rg -n \"subset.*card.*eq|eq_of_subset_of_card|card_le_card.*eq\" Mathlib/Data/Finset | head -n 120; rg -n \"IsClique.*union|isClique_union|IsCompleteBetween.*union|union.*IsClique\" Mathlib/Combinatorics/SimpleGraph | head -n 160; rg -n \"neighborFinset.*filter|mem_neighborFinset|coe_neighborFinset\" Mathlib/Combinatorics/SimpleGraph/Finite.lean | head -n 100"
Mathlib/Data/Finset/Max.lean:352:theorem min'_image [LinearOrder β] {f : α → β} (hf : Monotone f) (s : Finset α)
Mathlib/Data/Finset/Max.lean:357:/-- A version of `Finset.min'_image` with LHS and RHS reversed.
Mathlib/Data/Finset/Max.lean:361:  .symm <| min'_image hf ..
Mathlib/Data/Finset/Max.lean:534:theorem exists_min_image (s : Finset β) (f : β → α) (h : s.Nonempty) :
Mathlib/Data/Finset/Max.lean:570:theorem Multiset.exists_min_image {α R : Type*} [LinearOrder R] (f : α → R) {s : Multiset α}
Mathlib/Analysis/Convex/Birkhoff.lean:106:  obtain ⟨i, hi, hi'⟩ := exists_min_image _ (fun i => M i (σ i)) univ_nonempty
Mathlib/Analysis/Convex/Caratheodory.lean:65:    apply s.exists_min_image fun z => f z / g z
Mathlib/Data/Finset/Max.lean:352:theorem min'_image [LinearOrder β] {f : α → β} (hf : Monotone f) (s : Finset α)
Mathlib/Data/Finset/Max.lean:357:/-- A version of `Finset.min'_image` with LHS and RHS reversed.
Mathlib/Data/Finset/Max.lean:361:  .symm <| min'_image hf ..
Mathlib/Data/Finset/Max.lean:534:theorem exists_min_image (s : Finset β) (f : β → α) (h : s.Nonempty) :
Mathlib/Data/Finset/Max.lean:570:theorem Multiset.exists_min_image {α R : Type*} [LinearOrder R] (f : α → R) {s : Multiset α}
Mathlib/Data/Set/Finite/Lemmas.lean:75:theorem exists_min_image [LinearOrder β] (s : Set α) (f : α → β) (h1 : s.Finite) :
Mathlib/Data/Set/Finite/Lemmas.lean:79:      h1.toFinset.exists_min_image f ⟨x, h1.mem_toFinset.2 hx⟩
Mathlib/Data/Set/Finite/Lemmas.lean:91:  · rcases Set.exists_min_image s f h hs with ⟨x₀, _, hx₀⟩
Mathlib/Data/Fintype/Lattice.lean:64:  simpa using exists_min_image univ f univ_nonempty
Mathlib/Analysis/Normed/Field/Dense.lean:71:    · apply Finset.min'_le (S.image fun x => ‖a - x‖) (‖a - a'‖)
Mathlib/Analysis/Normed/Field/Dense.lean:84:    · simp only [gt_iff_lt, Finset.lt_min'_iff, Finset.mem_image, forall_exists_index, and_imp,
Mathlib/GroupTheory/Descent.lean:83:  obtain ⟨x, hx₁, hx₂⟩ := Northcott.exists_min_image h Uᶜ H
Mathlib/Combinatorics/Additi

$ /bin/bash -lc "rg -n \"theorem Colorable.of_hom|def Colorable.of_hom|Colorable.*of_hom|Colorable.*comp\" Mathlib/Combinatorics/SimpleGraph/Coloring/Vertex.lean; sed -n '188,220p' Mathlib/Combinatorics/SimpleGraph/Coloring/Vertex.lean; sed -n '525,550p' Mathlib/Data/Finset/Max.lean; sed -n '640,675p' Mathlib/Data/Finset/Card.lean; rg -n \"neighborFinset_induce|map_neighborFinset_induce|card_neighborFinset_induce|degree_induce\" Mathlib/Combinatorics/SimpleGraph/Finite.lean | head -n 80"
297:theorem Colorable.of_hom {V' : Type*} {G' : SimpleGraph V'} {n : ℕ} (f : G →g G')
  exact C.map_rel h <| Subsingleton.elim ..

/-- A coloring of a graph `G` is a homomorphism from it to the mapped graph.
This is `Hom.map` spelled using colorings. The mapped graph `G.map f` can be thought of as taking
the original graph `G` and considering every color class (independent set) as a single vertex. -/
abbrev Coloring.homMap {α : Type*} (f : G.Coloring α) : G →g G.map f :=
  .map f G f.map_adj

/-- If `G` is `n`-colorable, then mapping the vertices of `G` produces an `n`-colorable simple
graph. -/
theorem Colorable.map (f : V ↪ β) [NeZero n] (hc : G.Colorable n) : (G.map f).Colorable n := by
  obtain ⟨C⟩ := hc
  use extend f C (const β default)
  intro a b ⟨_, _, _, hadj, ha, hb⟩
  rw [← ha, f.injective.extend_apply, ← hb, f.injective.extend_apply]
  exact C.valid hadj

lemma Colorable.card_le_of_pairwise_adj (hG : G.Colorable n) (f : ι → V)
    (hf : Pairwise fun i j ↦ G.Adj (f i) (f j)) : Nat.card ι ≤ n := by
  obtain ⟨C⟩ := hG
  simpa using Nat.card_le_card_of_injective _ (C.injective_comp_of_pairwise_adj f hf)

variable (G) in
/-- The "tautological" coloring of a graph, using the vertices of the graph as colors. -/
def selfColoring : G.Coloring V := Coloring.mk id fun {_ _} => G.ne_of_adj

variable (G) in
/-- The chromatic number of a graph is the minimal number of colors needed to color it.
This is `⊤` (infinity) iff `G` isn't colorable with finitely many colors.

If `G` is colorable, then `ENat.toNat G.chromaticNumber` is the `ℕ`-valued chromatic number. -/
noncomputable def chromaticNumber : ℕ∞ := ⨅ n ∈ Set.ofPred G.Colorable, (n : ℕ∞)


variable [LinearOrder α]

theorem exists_max_image (s : Finset β) (f : β → α) (h : s.Nonempty) :
    ∃ x ∈ s, ∀ x' ∈ s, f x' ≤ f x := by
  obtain ⟨y, hy⟩ := max_of_nonempty (h.image f)
  rcases mem_image.mp (mem_of_max hy) with ⟨x, hx, rfl⟩
  exact ⟨x, hx, fun x' hx' => le_max_of_eq (mem_image_of_mem f hx') hy⟩

theorem exists_

$ /bin/bash -lc "sed -n '290,307p' Mathlib/Combinatorics/SimpleGraph/Coloring/Vertex.lean; sed -n '632,652p' Mathlib/Combinatorics/SimpleGraph/Finite.lean; rg -n \"exists.*not_mem.*Fin|Finset.*image.*card|card_image_iff\" Mathlib/Data/Finset Mathlib/Data/Fintype | head -n 120"
/-- Noncomputably get a coloring from colorability. -/
noncomputable def Colorable.toColoring [Fintype α] {n : ℕ} (hc : G.Colorable n)
    (hn : n ≤ Fintype.card α) : G.Coloring α := by
  rw [← Fintype.card_fin n] at hn
  exact G.recolorOfCardLE hn hc.some

theorem Colorable.of_hom {V' : Type*} {G' : SimpleGraph V'} {n : ℕ} (f : G →g G')
    (h : G'.Colorable n) : G.Colorable n :=
  ⟨h.some.comap f⟩

theorem colorable_iff_exists_bdd_nat_coloring (n : ℕ) :
    G.Colorable n ↔ ∃ C : G.Coloring ℕ, ∀ v, C v < n := by
  constructor
  · rintro hc
    have C : G.Coloring (Fin n) := hc.toColoring (by simp)
    let f := Embedding.completeGraph (@Fin.valEmbedding n)
    use f.toHom.comp C
  simpa [map_edgeFinset_induce] using edgeFinset_subset_sym2_of_support_subset h

/-- If the support of the simple graph `G` is a subset of the set `s`, then the induced subgraph of
`s` has the same number of edges as `G`. -/
theorem card_edgeFinset_induce_of_support_subset (h : G.support ⊆ s) :
    #(G.induce s).edgeFinset = #G.edgeFinset := by
  rw [← map_edgeFinset_induce_of_support_subset h, card_map]

theorem card_edgeFinset_induce_support :
    #(G.induce G.support).edgeFinset = #G.edgeFinset :=
  card_edgeFinset_induce_of_support_subset subset_rfl

theorem map_neighborFinset_induce [DecidableEq V] (v : s) :
    ((G.induce s).neighborFinset v).map (.subtype (· ∈ s)) = G.neighborFinset v ∩ s.toFinset := by
  ext; simp

theorem map_neighborFinset_induce_of_neighborSet_subset {v : s} (h : G.neighborSet v ⊆ s) :
    ((G.induce s).neighborFinset v).map (.subtype (· ∈ s)) = G.neighborFinset v := by
  classical
  rwa [← Set.toFinset_subset_toFinset, ← neighborFinset_def, ← inter_eq_left,
    ← map_neighborFinset_induce v] at h
Mathlib/Data/Fintype/BigOperators.lean:213:    _ ≤ (Finset.univ.image List.ofFn).card := by
Mathlib/Data/Finset/Card.lean:243:theorem card_image_iff [DecidableEq β] : #(s.image f) = #s ↔ Set.InjOn f s :=
Mathlib/Data/Finset/Card.lean:246:grind_pattern card_image_iff => 

$ /bin/bash -lc 'rg -n "exists_mem_not_mem.*card|card_lt_card.*exists|ssubset.*exists" Mathlib/Data/Finset | head -n 140; rg -n "card_image_le|card_image_of" Mathlib/Data/Finset/Card.lean | head -n 80; rg -n "degree.*colorable|colorable.*degree|critical" Mathlib/Combinatorics/SimpleGraph | head -n 120'
Mathlib/Data/Finset/Grade.lean:92:  let ⟨a, ha, hst⟩ := ssubset_iff_exists_cons_subset.1 h.lt
Mathlib/Data/Finset/Insert.lean:311:theorem ssubset_iff_exists_cons_subset : s ⊂ t ↔ ∃ (a : _) (h : a ∉ s), s.cons a h ⊆ t := by
Mathlib/Data/Finset/Basic.lean:155:theorem ssubset_iff_exists_subset_erase {s t : Finset α} : s ⊂ t ↔ ∃ a ∈ t, s ⊆ t.erase a := by
Mathlib/Data/Finset/Basic.lean:159:  ssubset_iff_exists_subset_erase.2 ⟨a, mem_insert_self _ _, by grw [← subset_insert]⟩
225:theorem card_image_le [DecidableEq β] : #(s.image f) ≤ #s := by
228:grind_pattern card_image_le => #(s.image f)
229:grind_pattern card_image_le => s.image f, #s
231:theorem card_image_of_injOn [DecidableEq β] (H : Set.InjOn f s) : #(s.image f) = #s := by
244:  ⟨injOn_of_card_image_eq, card_image_of_injOn⟩
249:theorem card_image_of_injective [DecidableEq β] (s : Finset α) (H : Injective f) :
251:  card_image_of_injOn fun _ _ _ _ h => H h
334:  apply card_image_of_injective
356:  · apply card_image_of_injective
426:    #s = #(s.image f) := (card_image_of_injOn f_inj).symm
445:  classical unfold Set.SurjOn at hf; exact (card_le_card (mod_cast hf)).trans card_image_le
467:  mt card_image_of_injOn hc.ne
489:  exact eq_of_subset_of_card_le this (hst.trans_eq (card_image_of_injOn hinj).symm)
516:  have : #(s.image f) ≤ #s := card_image_le
747:    grind [card_sdiff_of_subset hf'.finsetImage_subset, card_image_of_injOn hf]

$ /bin/bash -lc "rg -n \"induce_eq_top|chromaticNumber_induce|Fintype.card_coe|card_coe\" Mathlib/Combinatorics/SimpleGraph Mathlib/Data/Finset | head -n 160; sed -n '500,540p' Mathlib/Combinatorics/SimpleGraph/Maps.lean; rg -n \"chromaticNumber_eq_iff_colorable_not_colorable\" Mathlib -g '*.lean' | head -n 20; rg -n \"cliqueNum.*CliqueFree|CliqueFree.*cliqueNum|cliqueFree_iff\" Mathlib/Combinatorics/SimpleGraph/Clique.lean | head -n 100"
Mathlib/Combinatorics/SimpleGraph/Extremal/Zarankiewicz.lean:72:    simp_rw [← card_coe, mem_edgeFinset] at h_le_sup ⊢
Mathlib/Combinatorics/SimpleGraph/Extremal/ErdosStoneSimonovits.lean:175:  simp_rw [card_coe]
Mathlib/Combinatorics/SimpleGraph/Extremal/ErdosStoneSimonovits.lean:295:      · simp_rw [card_map, card_univ, card_coe]
Mathlib/Combinatorics/SimpleGraph/Hall.lean:67:    rw [Set.ncard_coe_finset, Finset.card_image_of_injective _ Subtype.val_injective] at this
Mathlib/Combinatorics/SimpleGraph/Hall.lean:68:    simpa [← Set.ncard_coe_finset, neighborFinset_def]
Mathlib/Combinatorics/SimpleGraph/Hall.lean:87:    simpa [← Set.ncard_coe_finset, neighborFinset_def]
Mathlib/Combinatorics/SimpleGraph/Hall.lean:99:    simpa [← Set.ncard_coe_finset, neighborFinset_def]
Mathlib/Combinatorics/SimpleGraph/Coloring/Vertex.lean:591:                    (by simp_all [← induce_eq_top]) (C.comp (Embedding.induce s).toHom) _
Mathlib/Combinatorics/SimpleGraph/Tutte.lean:286:    simp_rw [Fintype.card_eq_nat_card, Nat.card_coe_set_eq] at hc
Mathlib/Combinatorics/SimpleGraph/Clique.lean:58:theorem induce_eq_top : G.induce s = ⊤ ↔ G.IsClique s := by
Mathlib/Combinatorics/SimpleGraph/Clique.lean:66:@[deprecated induce_eq_top (since := "2026-04-23")]
Mathlib/Combinatorics/SimpleGraph/Clique.lean:68:  induce_eq_top.symm
Mathlib/Combinatorics/SimpleGraph/Clique.lean:400:  rw [G.induce_eq_top.mpr h.choose_spec.isClique]
Mathlib/Combinatorics/SimpleGraph/CompleteMultipartite.lean:397:        Fintype.card_fin, card_coe, K.card_parts.resolve_right ht]
Mathlib/Combinatorics/SimpleGraph/CompleteMultipartite.lean:400:      rw [Embedding.nonempty_iff_card_le, Fintype.card_fin, card_coe, K.card_mem_parts p.prop]
Mathlib/Combinatorics/SimpleGraph/Bipartite.lean:333:    rw [← card_coe] at card_left
Mathlib/Combinatorics/SimpleGraph/Bipartite.lean:337:    rw [← card_coe] at card_right
Mathlib/Combinatorics/SimpleGraph/Connectivity/Finite.lean:93:  simp_rw [← Nat.card_coe_set_eq]
Mathlib/Combinat

$ /bin/bash -lc "sed -n '373,455p' Mathlib/Combinatorics/SimpleGraph/Clique.lean; sed -n '400,435p' Mathlib/Combinatorics/SimpleGraph/Coloring/Vertex.lean; rg -n \"CliqueFree.*of_hom|CliqueFree.*embedding|CliqueFree.*induce|cliqueFree_induce\" Mathlib/Combinatorics/SimpleGraph -g '*.lean' | head -n 100; rg -n \"IsIndContained.*trans|Embedding.*comp|def Embedding.comp\" Mathlib/Combinatorics/SimpleGraph/Copy.lean Mathlib/Combinatorics/SimpleGraph/Maps.lean | head -n 100"
section CliqueFree

variable {m n : ℕ}

/-- `G.CliqueFree n` means that `G` has no `n`-cliques. -/
def CliqueFree (n : ℕ) : Prop :=
  ∀ t, ¬G.IsNClique n t

variable {G H} {s : Finset α}

theorem IsNClique.not_cliqueFree (hG : G.IsNClique n s) : ¬G.CliqueFree n :=
  fun h ↦ h _ hG

theorem IsContained.not_cliqueFree {n : ℕ} (h : completeGraph (Fin n) ⊑ G) : ¬G.CliqueFree n := by
  have := isNClique_map_copy_top h.some
  rw [Fintype.card_fin] at this
  exact (· _ this)

@[deprecated (since := "2026-02-21")]
alias not_cliqueFree_of_top_embedding := IsContained.not_cliqueFree

/-- An embedding of a complete graph that witnesses the fact that the graph is not clique-free. -/
noncomputable def topEmbeddingOfNotCliqueFree {n : ℕ} (h : ¬G.CliqueFree n) :
    completeGraph (Fin n) ↪g G := by
  unfold CliqueFree at h
  push Not at h
  apply Embedding.induce (h.choose : Set α) |>.comp
  rw [G.induce_eq_top.mpr h.choose_spec.isClique]
  exact Embedding.completeGraph <| Finset.equivFinOfCardEq h.choose_spec.card_eq |>.symm.toEmbedding

theorem not_cliqueFree_iff_top_isContained (n : ℕ) : ¬G.CliqueFree n ↔ completeGraph (Fin n) ⊑ G :=
  ⟨(topEmbeddingOfNotCliqueFree · |>.isContained), IsContained.not_cliqueFree⟩

@[deprecated (since := "2026-03-23")] alias not_cliqueFree_iff := not_cliqueFree_iff_top_isContained

theorem cliqueFree_iff {n : ℕ} : G.CliqueFree n ↔ IsEmpty (Copy (completeGraph <| Fin n) G) := by
  contrapose!
  exact not_cliqueFree_iff_top_isContained n

/-- A simple graph has no `card β`-cliques iff it does not contain `⊤ : SimpleGraph β`. -/
theorem cliqueFree_iff_top_free {β : Type*} [Fintype β] :
    G.CliqueFree (card β) ↔ (⊤ : SimpleGraph β).Free G := by
  rw [← not_iff_not, not_free, not_cliqueFree_iff_top_isContained,
    isContained_congr (Iso.completeGraph (equivFin β)) Iso.refl]

theorem IsContained.not_cliqueFree_card [Fintype α] (f : completeGraph α ⊑ G) :
    ¬G.CliqueFree (card α) := by
  rw [not_cliqueFree_iff_top_isContained]
  exact (Iso.completeG

$ /bin/bash -lc 'lake env lean Tihany.lean'
Tihany.lean:33:6: error(lean.synthInstanceFailed): failed to synthesize instance of type class
  Fintype ↑(G.neighborSet v)

Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command.
Tihany.lean:43:4: error: unsolved goals
case mp.refine_1
V : Type u
inst✝¹ : Fintype V
inst✝ : DecidableEq V
G : SimpleGraph V
v : V
A B : Set V
hA : G.IsClique A
hB : G.IsClique B
hn : G.neighborSet v = A ∪ B
Af : Finset V := A.toFinset
Bf : Finset V := (B \ A).toFinset
⊢ ∀ ⦃a : V⦄, a ∈ A → a ∈ B → a ∈ A
Tihany.lean:45:24: error: `simp` made no progress
Tihany.lean:47:37: error: Ambiguous term
  mem_union
Possible interpretations:
  Set.mem_union : ∀ (x : ?m.83) (a b : Set ?m.83), x ∈ a ∪ b ↔ x ∈ a ∨ x ∈ b
  
  Finset.mem_union : ?m.87 ∈ ?m.85 ∪ ?m.86 ↔ ?m.87 ∈ ?m.85 ∨ ?m.87 ∈ ?m.86
Tihany.lean:61:0: warning: automatically included section variable(s) unused in theorem `Tihany.mem_commonNeighbors`:
  [Fintype V]
  [DecidableEq V]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [Fintype V] [DecidableEq V] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
Tihany.lean:87:0: warning: automatically included section variable(s) unused in theorem `Tihany.EvenHoleFree.c4Free`:
  [Fintype V]
  [DecidableEq V]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [Fintype V] [DecidableEq V] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
Tihany.lean:91:0: warning: automatically included section variable(s) unused in theorem `Tihany.EvenHoleFree.induce`:
  [Fintype V]
  [DecidableEq V]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [Fintype V] [DecidableEq V] in theorem ...

Note: This linter can be disabled with `set

$ /bin/bash -lc "nl -ba Tihany.lean | sed -n '25,58p'"
25	def Bisimplicial (G : SimpleGraph V) (v : V) : Prop :=
    26	  ∃ A B : Set V,
    27	    G.IsClique A ∧ G.IsClique B ∧ G.neighborSet v = A ∪ B
    28	
    29	/-- A finite, disjoint form of `Bisimplicial`, used in the proof. -/
    30	def BisimplicialFinset (G : SimpleGraph V) (v : V) : Prop :=
    31	  ∃ A B : Finset V,
    32	    Disjoint A B ∧ G.IsClique A ∧ G.IsClique B ∧
    33	      G.neighborFinset v = A ∪ B
    34	
    35	theorem bisimplicial_iff_finset (G : SimpleGraph V) (v : V) :
    36	    Bisimplicial G v ↔ BisimplicialFinset G v := by
    37	  classical
    38	  constructor
    39	  · rintro ⟨A, B, hA, hB, hn⟩
    40	    let Af : Finset V := A.toFinset
    41	    let Bf : Finset V := (B \ A).toFinset
    42	    refine ⟨Af, Bf, ?_, ?_, ?_, ?_⟩
    43	    · simp [Af, Bf, Finset.disjoint_left]
    44	    · simpa [Af, Set.coe_toFinset] using hA
    45	    · exact hB.mono (by simp [Bf])
    46	    · ext x
    47	      simp only [mem_neighborFinset, mem_union]
    48	      rw [show G.Adj v x ↔ x ∈ A ∪ B by
    49	        simpa [mem_neighborSet] using Set.ext_iff.mp hn x]
    50	      simp [Af, Bf]
    51	  · rintro ⟨A, B, hAB, hA, hB, hn⟩
    52	    refine ⟨(A : Set V), (B : Set V), hA, hB, ?_⟩
    53	    ext x
    54	    simpa [mem_neighborSet] using Set.ext_iff.mp
    55	      (congrArg (fun s : Finset V => (s : Set V)) hn) x
    56	
    57	/-- The common neighborhood used in the paper. -/
    58	def commonNeighbors (G : SimpleGraph V) (K : Finset V) : Set V :=

$ /bin/bash -lc 'lake env lean Tihany.lean'
Tihany.lean:49:32: error: Type mismatch
  And.left ?m.127
has type
  ?m.126 ∈ B
but is expected to have type
  Adj ?m.116 x✝ hx → G.Adj x✝ hx
Tihany.lean:49:36: error: Type mismatch: After simplification, term
  hx
 has type
  V
of sort `Type u` but is expected to have type
  ?m.126 ∈ B ∧ ?m.126 ∉ A
of sort `Prop`
Tihany.lean:55:4: error: Type mismatch
  Eq.symm hn
has type
  G.neighborSet v = ↑(A ∪ B)
but is expected to have type
  G.neighborSet v = ↑A ∪ ↑B
Tihany.lean:61:0: warning: automatically included section variable(s) unused in theorem `Tihany.mem_commonNeighbors`:
  [Fintype V]
  [DecidableEq V]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [Fintype V] [DecidableEq V] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
Tihany.lean:87:0: warning: automatically included section variable(s) unused in theorem `Tihany.EvenHoleFree.c4Free`:
  [Fintype V]
  [DecidableEq V]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [Fintype V] [DecidableEq V] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
Tihany.lean:91:0: warning: automatically included section variable(s) unused in theorem `Tihany.EvenHoleFree.induce`:
  [Fintype V]
  [DecidableEq V]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [Fintype V] [DecidableEq V] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`

$ /bin/bash -lc "rg -n \"theorem IsClique\\.(mono|subset)|lemma IsClique\\.(mono|subset)|protected.*IsClique\" Mathlib/Combinatorics/SimpleGraph/Clique.lean | head -n 100; sed -n '90,210p' Mathlib/Combinatorics/SimpleGraph/Clique.lean"
105:theorem IsClique.mono (h : G ≤ H) : G.IsClique s → H.IsClique s := Set.Pairwise.mono' h
108:theorem IsClique.subset (h : t ⊆ s) : G.IsClique s → G.IsClique t := Set.Pairwise.mono h
112:protected theorem IsClique.top : (⊤ : SimpleGraph α).IsClique s :=
125:protected theorem IsClique.map (h : G.IsClique s) {f : α ↪ β} : (G.map f).IsClique (f '' s) := by
195:protected theorem IsClique.finsetMap {f : α ↪ β} {s : Finset α} (h : G.IsClique s) :
lemma isClique_insert : G.IsClique (insert a s) ↔ G.IsClique s ∧ ∀ b ∈ s, a ≠ b → G.Adj a b :=
  have := G.symm
  Set.pairwise_insert_of_symm

lemma isClique_insert_of_notMem (ha : a ∉ s) :
    G.IsClique (insert a s) ↔ G.IsClique s ∧ ∀ b ∈ s, G.Adj a b :=
  have := G.symm
  Set.pairwise_insert_of_symm_of_notMem ha

lemma IsClique.insert (hs : G.IsClique s) (h : ∀ b ∈ s, a ≠ b → G.Adj a b) :
    G.IsClique (insert a s) :=
  have := G.symm
  hs.insert_of_symm h

@[gcongr]
theorem IsClique.mono (h : G ≤ H) : G.IsClique s → H.IsClique s := Set.Pairwise.mono' h

@[gcongr]
theorem IsClique.subset (h : t ⊆ s) : G.IsClique s → G.IsClique t := Set.Pairwise.mono h

variable (s) in
@[simp]
protected theorem IsClique.top : (⊤ : SimpleGraph α).IsClique s :=
  fun _ _ _ _ ↦ id

@[simp]
theorem isClique_bot_iff : (⊥ : SimpleGraph α).IsClique s ↔ (s : Set α).Subsingleton :=
  Set.pairwise_bot_iff

alias ⟨IsClique.subsingleton, _⟩ := isClique_bot_iff

@[simp]
theorem isClique_univ : G.IsClique .univ ↔ G = ⊤ :=
  Set.pairwise_univ.trans G.eq_top_iff_forall_ne_adj.symm

protected theorem IsClique.map (h : G.IsClique s) {f : α ↪ β} : (G.map f).IsClique (f '' s) := by
  rintro _ ⟨a, ha, rfl⟩ _ ⟨b, hb, rfl⟩ hab
  exact ⟨hab, a, b, h ha hb <| ne_of_apply_ne _ hab, rfl, rfl⟩

theorem IsClique.inter_left {s : Set α} (hs : G.IsClique s) (t : Set α) : G.IsClique <| s ∩ t :=
  Set.Pairwise.inter_left hs t

theorem IsClique.inter_right {s : Set α} (hs : G.IsClique s) (t : Set α) : G.IsClique <| t ∩ s :=
  Set.Pairwise.inter_right hs t

theorem isClique_sU

$ /bin/bash -lc 'lake env lean Tihany.lean'
Tihany.lean:63:0: warning: automatically included section variable(s) unused in theorem `Tihany.mem_commonNeighbors`:
  [Fintype V]
  [DecidableEq V]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [Fintype V] [DecidableEq V] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
Tihany.lean:89:0: warning: automatically included section variable(s) unused in theorem `Tihany.EvenHoleFree.c4Free`:
  [Fintype V]
  [DecidableEq V]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [Fintype V] [DecidableEq V] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
Tihany.lean:93:0: warning: automatically included section variable(s) unused in theorem `Tihany.EvenHoleFree.induce`:
  [Fintype V]
  [DecidableEq V]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [Fintype V] [DecidableEq V] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`

$ /bin/bash -lc "rg -n \"let f : .*↪g|refine ⟨⟨.*map_rel_iff|toEmbedding :=|map_rel_iff' :=\" Mathlib/Combinatorics/SimpleGraph | head -n 120; rg -n \"structure RelEmbedding|def RelEmbedding\" Mathlib | head -n 30"
Mathlib/Combinatorics/SimpleGraph/Copy.lean:207:    map_rel_iff' := fun {v w} ↦ ⟨fun h ↦ by simpa using h.ne, f.toHom.map_adj⟩}
Mathlib/Combinatorics/SimpleGraph/Copy.lean:436:     map_rel_iff' := hG'.adj.symm }⟩
Mathlib/Combinatorics/SimpleGraph/Copy.lean:454:     map_rel_iff' := fun {a} ↦ isEmptyElim a }⟩
Mathlib/Combinatorics/SimpleGraph/Clique.lean:487:  map_rel_iff' := by simp
Mathlib/Combinatorics/SimpleGraph/AdjMatrix.lean:133:  map_rel_iff' := by simp
Mathlib/Combinatorics/SimpleGraph/AdjMatrix.lean:148:  map_rel_iff' := by simp
Mathlib/Combinatorics/SimpleGraph/Maps.lean:148:    G.comap e.symm.toEmbedding = G.map e.toEmbedding := by
Mathlib/Combinatorics/SimpleGraph/Maps.lean:153:    G.map e.symm.toEmbedding = G.comap e.toEmbedding := by rw [← comap_symm, e.symm_symm]
Mathlib/Combinatorics/SimpleGraph/Maps.lean:495:  map_rel_iff' := by simp
Mathlib/Combinatorics/SimpleGraph/Maps.lean:503:  map_rel_iff' := by simp
Mathlib/Combinatorics/SimpleGraph/Maps.lean:518:  map_rel_iff' := by simp
Mathlib/Combinatorics/SimpleGraph/Maps.lean:538:  map_rel_iff' := by simp
Mathlib/Combinatorics/SimpleGraph/Maps.lean:606:  toEmbedding := Set.embeddingOfSubset s s' h
Mathlib/Combinatorics/SimpleGraph/Maps.lean:607:  map_rel_iff' := by simp
Mathlib/Combinatorics/SimpleGraph/Maps.lean:700:  map_rel_iff' := by simp
Mathlib/Combinatorics/SimpleGraph/Maps.lean:714:  map_rel_iff' := by aesop (add simp map_adj')
Mathlib/Combinatorics/SimpleGraph/Maps.lean:726:  map_rel_iff' := by simp
Mathlib/Combinatorics/SimpleGraph/Maps.lean:729:    (Iso.completeGraph f).toEmbedding = Embedding.completeGraph f.toEmbedding :=
Mathlib/Combinatorics/SimpleGraph/Maps.lean:765:  map_rel_iff' := by simp [map_adj_iff φ]
Mathlib/Combinatorics/SimpleGraph/Maps.lean:801:  map_rel_iff' := by simp only [Equiv.Set.univ, Equiv.coe_fn_mk, comap_adj, Embedding.coe_subtype,
Mathlib/Combinatorics/SimpleGraph/Maps.lean:810:  map_rel_iff' := by simp
Mathlib/Combinatorics/SimpleGraph/Coloring/Constructions.lean:47:

$ /bin/bash -lc 'lake env lean Tihany.lean'
Tihany.lean:63:0: warning: automatically included section variable(s) unused in theorem `Tihany.mem_commonNeighbors`:
  [Fintype V]
  [DecidableEq V]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [Fintype V] [DecidableEq V] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
Tihany.lean:89:0: warning: automatically included section variable(s) unused in theorem `Tihany.EvenHoleFree.c4Free`:
  [Fintype V]
  [DecidableEq V]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [Fintype V] [DecidableEq V] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
Tihany.lean:93:0: warning: automatically included section variable(s) unused in theorem `Tihany.EvenHoleFree.induce`:
  [Fintype V]
  [DecidableEq V]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [Fintype V] [DecidableEq V] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
Tihany.lean:114:4: error(lean.synthInstanceFailed): failed to synthesize instance of type class
  DecidablePred (G.Adj x)

Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command.
Tihany.lean:114:25: error(lean.synthInstanceFailed): failed to synthesize instance of type class
  DecidablePred (G.Adj y)

Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command.
Tihany.lean:115:6: error(lean.synthInstanceFailed): failed to synthesize instance of type class
  DecidablePred (G.Adj y)

Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command.
Tihany.lean:115:27: error(lean.synthInstanceFailed): faile

$ /bin/bash -lc 'lake env lean Tihany.lean'
Tihany.lean:63:0: warning: automatically included section variable(s) unused in theorem `Tihany.mem_commonNeighbors`:
  [Fintype V]
  [DecidableEq V]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [Fintype V] [DecidableEq V] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
Tihany.lean:89:0: warning: automatically included section variable(s) unused in theorem `Tihany.EvenHoleFree.c4Free`:
  [Fintype V]
  [DecidableEq V]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [Fintype V] [DecidableEq V] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
Tihany.lean:93:0: warning: automatically included section variable(s) unused in theorem `Tihany.EvenHoleFree.induce`:
  [Fintype V]
  [DecidableEq V]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [Fintype V] [DecidableEq V] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
Tihany.lean:118:2: warning: `push_neg` has been deprecated. Prefer using `push Not` instead.
If you'd rather continue using `push_neg` in your project, you can implement it as follows:
```
open Lean.Parser.Tactic in
macro "push_neg" cfg:optConfig loc:(location)? : tactic =>
  `(tactic| push $cfg:optConfig Not $[$loc]?)
```
Tihany.lean:132:11: error: Application type mismatch: The argument
  hAB
has type
  Disjoint A B
but is expected to have type
  Disjoint ↑A ↑B
in the application
  Disjoint.notMem_of_mem_left hAB
Tihany.lean:136:11: error: Application type mismatch: The argument
  hAB
has type
  Disjoint A B
but is expected to have type
  Disjoint ↑A ↑B
in the application
  Disjoint.notMem_of_mem_left hAB
Tihany.lean:140:11: error: Application type mismatch: The argument
  hAB
has type
 

$ /bin/bash -lc 'lake env lean Tihany.lean'
Tihany.lean:63:0: warning: automatically included section variable(s) unused in theorem `Tihany.mem_commonNeighbors`:
  [Fintype V]
  [DecidableEq V]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [Fintype V] [DecidableEq V] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
Tihany.lean:89:0: warning: automatically included section variable(s) unused in theorem `Tihany.EvenHoleFree.c4Free`:
  [Fintype V]
  [DecidableEq V]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [Fintype V] [DecidableEq V] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
Tihany.lean:93:0: warning: automatically included section variable(s) unused in theorem `Tihany.EvenHoleFree.induce`:
  [Fintype V]
  [DecidableEq V]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [Fintype V] [DecidableEq V] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
Tihany.lean:118:2: warning: `push_neg` has been deprecated. Prefer using `push Not` instead.
If you'd rather continue using `push_neg` in your project, you can implement it as follows:
```
open Lean.Parser.Tactic in
macro "push_neg" cfg:optConfig loc:(location)? : tactic =>
  `(tactic| push $cfg:optConfig Not $[$loc]?)
```
Tihany.lean:147:26: error: Function expected at
  G.symm
but this term has type
  Std.Symm G.Adj

Note: Expected a function because this term is being applied to the argument
  hxy
Tihany.lean:148:26: error: Function expected at
  G.symm
but this term has type
  Std.Symm G.Adj

Note: Expected a function because this term is being applied to the argument
  hxz
Tihany.lean:149:26: error: Function expected at
  G.symm
but this term has type
  Std.Symm G.Adj

Note: Expected 

$ /bin/bash -lc 'rg -n "theorem adj_comm|lemma adj_comm|adj_comm" Mathlib/Combinatorics/SimpleGraph | head -n 60; rg -n "def Symm|class Symm|structure Symm" $(pwd)/Mathlib $(pwd)/.lake/packages/batteries/Batteries $(pwd)/.lake/packages/Qq/Qq 2>/dev/null | head -n 30'
Mathlib/Combinatorics/SimpleGraph/Extremal/Turan.lean:121:    exact this (by rwa [adj_comm] at hn) hd.ne' cf hd
Mathlib/Combinatorics/SimpleGraph/Extremal/Turan.lean:152:    split_ifs <;> simp_all [adj_comm]
Mathlib/Combinatorics/SimpleGraph/Extremal/Turan.lean:162:  symm := by simp [adj_comm]
Mathlib/Combinatorics/SimpleGraph/Tutte.lean:213:    rw [M2.adj_comm]
Mathlib/Combinatorics/SimpleGraph/Tutte.lean:262:      rw [adj_comm]
Mathlib/Combinatorics/SimpleGraph/Tutte.lean:263:    rw [Subgraph.adj_comm] at hnpxb
Mathlib/Combinatorics/SimpleGraph/Clique.lean:520:      simp_rw [hx, hy, adj_comm, not_adj_replaceVertex_same, top_adj, false_iff, not_ne_iff] at e
Mathlib/Combinatorics/SimpleGraph/Finite.lean:627:  aesop (add simp [Finset.ext_iff, Sym2.exists, Sym2.forall, adj_comm])
Mathlib/Combinatorics/SimpleGraph/AdjMatrix.lean:261:  simp [adj_comm]
Mathlib/Combinatorics/SimpleGraph/AdjMatrix.lean:380:  simp [mul_apply, neighborFinset_eq_filter, sum_filter, adj_comm]
Mathlib/Combinatorics/SimpleGraph/Metric.lean:423:    edist_le_one_iff_adj_or_eq, adj_comm, or_comm]
Mathlib/Combinatorics/SimpleGraph/Matching.lean:467:  rw [Subgraph.adj_comm, Subgraph.adj_iff_of_neighborSet_equiv e (Set.toFinite _)]
Mathlib/Combinatorics/SimpleGraph/Subgraph.lean:104:theorem adj_comm (G' : Subgraph G) (v w : V) : G'.Adj v w ↔ G'.Adj w v :=
Mathlib/Combinatorics/SimpleGraph/Subgraph.lean:131:  · rw [hr.1, hr.2, Subgraph.adj_comm]
Mathlib/Combinatorics/SimpleGraph/Subgraph.lean:348:      symm.symm a b h := by simpa [adj_comm] using h }
Mathlib/Combinatorics/SimpleGraph/Subgraph.lean:720:      fun a b ↦ by simpa using H.edge_vert, by simp [H.adj_comm]⟩, by simp⟩
Mathlib/Combinatorics/SimpleGraph/Subgraph.lean:1079:  symm.symm a b := by simp [G'.adj_comm, Sym2.eq_swap]
Mathlib/Combinatorics/SimpleGraph/Coloring/EdgeLabeling.lean:127:    apply Function.hfunext (by simp [adj_comm])
Mathlib/Combinatorics/SimpleGraph/Coloring/EdgeLabeling.lean:193:  EdgeLabeling.mk (fun x y _ => if G.Adj x y t

$ /bin/bash -lc 'lake env lean Tihany.lean'
Tihany.lean:63:0: warning: automatically included section variable(s) unused in theorem `Tihany.mem_commonNeighbors`:
  [Fintype V]
  [DecidableEq V]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [Fintype V] [DecidableEq V] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
Tihany.lean:89:0: warning: automatically included section variable(s) unused in theorem `Tihany.EvenHoleFree.c4Free`:
  [Fintype V]
  [DecidableEq V]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [Fintype V] [DecidableEq V] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
Tihany.lean:93:0: warning: automatically included section variable(s) unused in theorem `Tihany.EvenHoleFree.induce`:
  [Fintype V]
  [DecidableEq V]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [Fintype V] [DecidableEq V] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
Tihany.lean:118:2: warning: `push_neg` has been deprecated. Prefer using `push Not` instead.
If you'd rather continue using `push_neg` in your project, you can implement it as follows:
```
open Lean.Parser.Tactic in
macro "push_neg" cfg:optConfig loc:(location)? : tactic =>
  `(tactic| push $cfg:optConfig Not $[$loc]?)
```
Tihany.lean:161:22: error: unsolved goals
case «0».«2»
V : Type u
inst✝¹ : Fintype V
inst✝ : DecidableEq V
G : SimpleGraph V
hC4 : C4Free G
A B : Finset V
hAB : Disjoint A B
hA : G.IsClique ↑A
hB : G.IsClique ↑B
x y : V
hx : x ∈ A
hy : y ∈ A
hcomp : (∃ z ∈ B, G.Adj x z ∧ ¬G.Adj y z) ∧ ∃ z ∈ B, G.Adj y z ∧ ¬G.Adj x z
z : V
hzB : z ∈ B
hxz : G.Adj x z
hnyz : ¬G.Adj y z
w : V
hwB : w ∈ B
hyw : G.Adj y w
hnxw : ¬G.Adj x w
hxy : G.Adj x y
hzw : G.Adj z w
g : Fin 4 → V := fun 

$ /bin/bash -lc 'lake env lean Tihany.lean'
Tihany.lean:63:0: warning: automatically included section variable(s) unused in theorem `Tihany.mem_commonNeighbors`:
  [Fintype V]
  [DecidableEq V]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [Fintype V] [DecidableEq V] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
Tihany.lean:89:0: warning: automatically included section variable(s) unused in theorem `Tihany.EvenHoleFree.c4Free`:
  [Fintype V]
  [DecidableEq V]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [Fintype V] [DecidableEq V] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
Tihany.lean:93:0: warning: automatically included section variable(s) unused in theorem `Tihany.EvenHoleFree.induce`:
  [Fintype V]
  [DecidableEq V]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [Fintype V] [DecidableEq V] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
Tihany.lean:118:2: warning: `push_neg` has been deprecated. Prefer using `push Not` instead.
If you'd rather continue using `push_neg` in your project, you can implement it as follows:
```
open Lean.Parser.Tactic in
macro "push_neg" cfg:optConfig loc:(location)? : tactic =>
  `(tactic| push $cfg:optConfig Not $[$loc]?)
```

$ /bin/bash -lc 'lake env lean Tihany.lean'
Tihany.lean:63:0: warning: automatically included section variable(s) unused in theorem `Tihany.mem_commonNeighbors`:
  [Fintype V]
  [DecidableEq V]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [Fintype V] [DecidableEq V] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
Tihany.lean:89:0: warning: automatically included section variable(s) unused in theorem `Tihany.EvenHoleFree.c4Free`:
  [Fintype V]
  [DecidableEq V]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [Fintype V] [DecidableEq V] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
Tihany.lean:93:0: warning: automatically included section variable(s) unused in theorem `Tihany.EvenHoleFree.induce`:
  [Fintype V]
  [DecidableEq V]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [Fintype V] [DecidableEq V] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
Tihany.lean:118:2: warning: `push_neg` has been deprecated. Prefer using `push Not` instead.
If you'd rather continue using `push_neg` in your project, you can implement it as follows:
```
open Lean.Parser.Tactic in
macro "push_neg" cfg:optConfig loc:(location)? : tactic =>
  `(tactic| push $cfg:optConfig Not $[$loc]?)
```
Tihany.lean:203:10: error: Function expected at
  G.loopless
but this term has type
  Std.Irrefl G.Adj

Note: Expected a function because this term is being applied to the argument
  v
Tihany.lean:217:18: error: Ambiguous term
  mem_insert
Possible interpretations:
  Set.mem_insert : ∀ (x : ?m.310) (s : Set ?m.310), x ∈ insert x s
  
  Finset.mem_insert : ?m.313 ∈ insert ?m.314 ?m.312 ↔ ?m.313 = ?m.314 ∨ ?m.313 ∈ ?m.312
Tihany.lean:218:13: error(lean.invalidField): Inval

$ /bin/bash -lc "rg -n \"loopless\\.irrefl|\\.loopless .*Adj|G\\.loopless\" Mathlib/Combinatorics/SimpleGraph | head -n 80; sed -n '155,172p' Mathlib/Combinatorics/SimpleGraph/Basic.lean; rg -n \"mem_neighborSet\" Mathlib/Combinatorics/SimpleGraph/Basic.lean | head -n 20"
Mathlib/Combinatorics/SimpleGraph/Extremal/ErdosStoneSimonovits.lean:294:        exact G.loopless.irrefl v
Mathlib/Combinatorics/SimpleGraph/Trails.lean:70:        exact G.loopless.irrefl _ huv
Mathlib/Combinatorics/SimpleGraph/Subgraph.lean:138:  loopless.irrefl _ hadj := G.irrefl hadj.adj_sub
Mathlib/Combinatorics/SimpleGraph/Subgraph.lean:170:  loopless.irrefl _ hadj := G.irrefl hadj.adj_sub
Mathlib/Combinatorics/SimpleGraph/Basic.lean:164:  G.loopless.irrefl v
Mathlib/Combinatorics/SimpleGraph/Basic.lean:515:  simpa [Set.subset_compl_iff_disjoint_left, edgeSet, edgeSetEmbedding] using G.loopless
Mathlib/Combinatorics/SimpleGraph/CompleteMultipartite.lean:78:    ⟨(¬ G.Adj · ·), ⟨G.loopless.irrefl, fun h' ↦ by rwa [adj_comm] at h', h.trans _ _ _⟩⟩
def completeBipartiteGraph (V W : Type*) : SimpleGraph (V ⊕ W) where
  Adj v w := v.isLeft ∧ w.isRight ∨ v.isRight ∧ w.isLeft

namespace SimpleGraph

variable {ι : Sort*} {V : Type u} (G H : SimpleGraph V) {a b c u v w : V} {e : Sym2 V}

@[simp]
protected theorem irrefl {v : V} : ¬G.Adj v v :=
  G.loopless.irrefl v

theorem adj_comm (u v : V) : G.Adj u v ↔ G.Adj v u :=
  G.symm.iff u v

@[symm]
theorem adj_symm (h : G.Adj u v) : G.Adj v u :=
  G.symm.symm u v h

802:theorem mem_neighborSet (v w : V) : w ∈ G.neighborSet v ↔ G.Adj v w :=
822:  simp_rw [← disjoint_edgeSet, Set.disjoint_left, mem_neighborSet, Sym2.forall, mem_edgeSet]
830:  simp only [mem_incidenceSet, mem_neighborSet]
846:  rw [mem_neighborSet, compl_adj] at h'
853:  simp_rw [Set.mem_union, mem_neighborSet, compl_adj, Set.mem_compl_iff, Set.mem_singleton_iff]
875:  grind [mem_neighborSet, top_adj]
878:  grind [mem_neighborSet, bot_adj]
1062:  simp only [Set.ext_iff, Set.mem_insert_iff, mem_neighborSet, IsUniversal]

$ /bin/bash -lc 'lake env lean Tihany.lean'
Tihany.lean:63:0: warning: automatically included section variable(s) unused in theorem `Tihany.mem_commonNeighbors`:
  [Fintype V]
  [DecidableEq V]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [Fintype V] [DecidableEq V] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
Tihany.lean:89:0: warning: automatically included section variable(s) unused in theorem `Tihany.EvenHoleFree.c4Free`:
  [Fintype V]
  [DecidableEq V]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [Fintype V] [DecidableEq V] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
Tihany.lean:93:0: warning: automatically included section variable(s) unused in theorem `Tihany.EvenHoleFree.induce`:
  [Fintype V]
  [DecidableEq V]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [Fintype V] [DecidableEq V] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
Tihany.lean:118:2: warning: `push_neg` has been deprecated. Prefer using `push Not` instead.
If you'd rather continue using `push_neg` in your project, you can implement it as follows:
```
open Lean.Parser.Tactic in
macro "push_neg" cfg:optConfig loc:(location)? : tactic =>
  `(tactic| push $cfg:optConfig Not $[$loc]?)
```

$ /bin/bash -lc "rg -n \"Colorable.*(union|add|sum|cover|partition)|Coloring.*(union|sum|extend)|colorable.*induce.*∪|induce.*Colorable\" Mathlib/Combinatorics/SimpleGraph/Coloring Mathlib/Combinatorics/SimpleGraph -g '*.lean' | head -n 220; rg -n \"card_sum|Fintype.card_sum|card_subtype.*ne|card.*Subtype\" Mathlib/Data/Fintype Mathlib/Data/Finset | head -n 100"
Mathlib/Combinatorics/SimpleGraph/Sum.lean:193:def Coloring.sum (cG : G.Coloring γ) (cH : H.Coloring γ) : (G ⊕g H).Coloring γ where
Mathlib/Combinatorics/SimpleGraph/Sum.lean:198:def Coloring.sumLeft (c : (G ⊕g H).Coloring γ) : G.Coloring γ := c.comp Embedding.sumInl.toHom
Mathlib/Combinatorics/SimpleGraph/Sum.lean:201:def Coloring.sumRight (c : (G ⊕g H).Coloring γ) : H.Coloring γ := c.comp Embedding.sumInr.toHom
Mathlib/Combinatorics/SimpleGraph/Sum.lean:204:theorem Coloring.sumLeft_sum (cG : G.Coloring γ) (cH : H.Coloring γ) : (cG.sum cH).sumLeft = cG :=
Mathlib/Combinatorics/SimpleGraph/Sum.lean:208:theorem Coloring.sumRight_sum (cG : G.Coloring γ) (cH : H.Coloring γ) : (cG.sum cH).sumRight = cH :=
Mathlib/Combinatorics/SimpleGraph/Sum.lean:212:theorem Coloring.sum_sumLeft_sumRight (c : (G ⊕g H).Coloring γ) : c.sumLeft.sum c.sumRight = c := by
Mathlib/Combinatorics/SimpleGraph/Sum.lean:216:def Coloring.sumEquiv : (G ⊕g H).Coloring γ ≃ G.Coloring γ × H.Coloring γ where
Mathlib/Combinatorics/SimpleGraph/Sum.lean:223:def Coloring.sumFin {n m : ℕ} (cG : G.Coloring (Fin n)) (cH : H.Coloring (Fin m)) :
Mathlib/Combinatorics/SimpleGraph/Sum.lean:224:    (G ⊕g H).Coloring (Fin (max n m)) := sum
Mathlib/Combinatorics/SimpleGraph/Sum.lean:228:theorem Colorable.sum_max {n m : ℕ} (hG : G.Colorable n) (hH : H.Colorable m) :
Mathlib/Combinatorics/SimpleGraph/Sum.lean:229:    (G ⊕g H).Colorable (max n m) := Nonempty.intro (hG.some.sumFin hH.some)
Mathlib/Combinatorics/SimpleGraph/Sum.lean:231:theorem Colorable.of_sum_left {n : ℕ} (h : (G ⊕g H).Colorable n) : G.Colorable n :=
Mathlib/Combinatorics/SimpleGraph/Sum.lean:234:theorem Colorable.of_sum_right {n : ℕ} (h : (G ⊕g H).Colorable n) : H.Colorable n :=
Mathlib/Data/Fintype/Card.lean:99:  Multiset.card_map Subtype.val Finset.univ.val
Mathlib/Data/Fintype/Card.lean:392:  Fintype.card_lt_of_injective_of_notMem (b := x) (↑) Subtype.coe_injective <| by
Mathlib/Data/Fintype/Card.lean:412:  Fintype.card_le_of_embedding (Subtype.impE

$ /bin/bash -lc "rg -n \"card.*subtype.*ne|card_subtype.*compl|card_subtype_.*not|card_pos_iff.*Subtype\" Mathlib/Data/Fintype Mathlib | head -n 160; sed -n '120,160p' Mathlib/Data/Fintype/Sum.lean"
Mathlib/Data/Fintype/Card.lean:401:theorem Fintype.card_subtype_compl [Fintype α] (p : α → Prop) [Fintype { x // p x }]
Mathlib/Data/Fintype/Card.lean:420:  simp only [Fintype.card_subtype_compl, h]
Mathlib/Data/Fintype/Sum.lean:145:theorem Fintype.card_subtype_eq_or_eq_of_ne {α : Type*} [Fintype α] [DecidableEq α] {a b : α}
Mathlib/FieldTheory/ChevalleyWarning.lean:137:    rw [Fintype.card_of_subtype S hS, card_eq_sum_ones, Nat.cast_sum, Nat.cast_one, ←
Mathlib/Analysis/AbsoluteValue/Equivalence.lean:263:    let ⟨b, hb⟩ := ih {k : ι // k = i ∨ k = j} (by linarith [card_subtype_eq_or_eq_of_ne hj.symm])
Mathlib/Combinatorics/Configuration.lean:452:      convert! (Fintype.card_subtype_compl _).trans (congr_arg _ (Fintype.card_subtype_eq p))
Mathlib/Combinatorics/Configuration.lean:456:        Fintype.card_subtype_compl fun x : Subtype (· ∈ l.val) => x.val = p, ←
Mathlib/Combinatorics/SimpleGraph/Subgraph.lean:831:  simp only [degree, Fintype.card_pos_iff, nonempty_subtype, mem_neighborSet]
Mathlib/SetTheory/Cardinal/Finite.lean:266:  simp [pos_iff_ne_zero, Nat.card_eq_zero, hs.to_subtype, nonempty_iff_ne_empty]
Mathlib/LinearAlgebra/Dimension/Finite.lean:286:    Fintype.card { i // p i ≠ ⊥ } ≤ finrank R M := by simpa using hp.subtype_ne_bot_le_finrank_aux
Mathlib/RingTheory/Norm/Transitivity.lean:173:          grind [Fintype.card_subtype_compl, Fintype.card_unique])
Mathlib/Data/Fintype/Card.lean:401:theorem Fintype.card_subtype_compl [Fintype α] (p : α → Prop) [Fintype { x // p x }]
Mathlib/Data/Fintype/Card.lean:420:  simp only [Fintype.card_subtype_compl, h]
Mathlib/Data/Fintype/Sum.lean:145:theorem Fintype.card_subtype_eq_or_eq_of_ne {α : Type*} [Fintype α] [DecidableEq α] {a b : α}
Mathlib/LinearAlgebra/Matrix/Rank.lean:380:      Fintype.equivFinOfCardEq <| by rw [Fintype.card_subtype_compl, Fintype.card_coe, hs] with he
Mathlib/NumberTheory/NumberField/InfinitePlace/Basic.lean:477:  rw [← card_real_embeddings, ← card_complex_embeddings, Fintype.card_subtype_comp

$ /bin/bash -lc "sed -n '388,410p' Mathlib/Data/Fintype/Card.lean; sed -n '52,70p' Mathlib/Data/Fintype/Sum.lean"
Fintype.card_le_of_embedding (Function.Embedding.subtype _)

lemma Fintype.card_subtype_lt [Fintype α] {p : α → Prop} [Fintype {a // p a}] {x : α} (hx : ¬p x) :
    Fintype.card { x // p x } < Fintype.card α :=
  Fintype.card_lt_of_injective_of_notMem (b := x) (↑) Subtype.coe_injective <| by
    rwa [Subtype.range_coe_subtype]

theorem Fintype.card_subtype [Fintype α] (p : α → Prop) [Fintype {a // p a}] [DecidablePred p] :
    Fintype.card { x // p x } = #{x | p x} := by
  refine Fintype.card_of_subtype _ ?_
  simp

@[simp]
theorem Fintype.card_subtype_compl [Fintype α] (p : α → Prop) [Fintype { x // p x }]
    [Fintype { x // ¬p x }] :
    Fintype.card { x // ¬p x } = Fintype.card α - Fintype.card { x // p x } := by
  classical
    rw [Fintype.card_of_subtype (Set.toFinset { x | p x }ᶜ), Set.toFinset_compl,
      Finset.card_compl, Fintype.card_of_subtype] <;>
    · intro
      simp only [Set.mem_toFinset, Set.mem_compl_iff, Set.mem_ofPred]

theorem Fintype.card_subtype_mono (p q : α → Prop) (h : p ≤ q) [Fintype { x // p x }]
end right

variable [Fintype α] [Fintype β]

@[simp] lemma univ_disjSum_univ : univ.disjSum univ = (univ : Finset (α ⊕ β)) := rfl
@[simp] lemma toLeft_univ : (univ : Finset (α ⊕ β)).toLeft = univ := by ext; simp
@[simp] lemma toRight_univ : (univ : Finset (α ⊕ β)).toRight = univ := by ext; simp

end Finset

@[simp]
theorem Fintype.card_sum [Fintype α] [Fintype β] :
    Fintype.card (α ⊕ β) = Fintype.card α + Fintype.card β :=
  card_disjSum _ _

/-- If the subtype of all-but-one elements is a `Fintype` then the type itself is a `Fintype`. -/
@[instance_reducible]
def fintypeOfFintypeNe (a : α) (_ : Fintype { b // b ≠ a }) : Fintype α :=
  Fintype.ofBijective (Sum.elim ((↑) : { b // b = a } → α) ((↑) : { b // b ≠ a } → α)) <| by

$ /bin/bash -lc 'lake env lean Tihany.lean'
Tihany.lean:63:0: warning: automatically included section variable(s) unused in theorem `Tihany.mem_commonNeighbors`:
  [Fintype V]
  [DecidableEq V]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [Fintype V] [DecidableEq V] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
Tihany.lean:89:0: warning: automatically included section variable(s) unused in theorem `Tihany.EvenHoleFree.c4Free`:
  [Fintype V]
  [DecidableEq V]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [Fintype V] [DecidableEq V] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
Tihany.lean:93:0: warning: automatically included section variable(s) unused in theorem `Tihany.EvenHoleFree.induce`:
  [Fintype V]
  [DecidableEq V]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [Fintype V] [DecidableEq V] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
Tihany.lean:118:2: warning: `push_neg` has been deprecated. Prefer using `push Not` instead.
If you'd rather continue using `push_neg` in your project, you can implement it as follows:
```
open Lean.Parser.Tactic in
macro "push_neg" cfg:optConfig loc:(location)? : tactic =>
  `(tactic| push $cfg:optConfig Not $[$loc]?)
```
Tihany.lean:271:23: error(lean.synthInstanceFailed): failed to synthesize instance of type class
  Compl (Type u)

Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command.
Tihany.lean:275:16: error(lean.synthInstanceFailed): failed to synthesize instance of type class
  Compl (Type u)

Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` comman

$ /bin/bash -lc "nl -ba Tihany.lean | sed -n '264,338p'"
264	
   265	/-- If one color class in a coloring of `G-K` has no vertex complete to
   266	`K`, that coloring can be combined with the vertices of `K` while
   267	saving one color. -/
   268	theorem colorable_of_missing_commonNeighbor {G : SimpleGraph V}
   269	    {K : Finset V} {r : ℕ}
   270	    (C : (G.induce ((K : Set V)ᶜ)).Coloring (Fin r)) (i : Fin r)
   271	    (hmissing : ¬∃ w : (K : Set V)ᶜ,
   272	      C w = i ∧ (w : V) ∈ commonNeighbors G K) :
   273	    G.Colorable (K.card + r - 1) := by
   274	  classical
   275	  have hex (w : (K : Set V)ᶜ) (hw : C w = i) :
   276	      ∃ a ∈ K, ¬G.Adj (w : V) a := by
   277	    by_contra h
   278	    push_neg at h
   279	    exact hmissing ⟨w, hw, w.property, h⟩
   280	  let pick : ∀ (w : (K : Set V)ᶜ), C w = i → K :=
   281	    fun w hw ↦ ⟨(hex w hw).choose, (hex w hw).choose_spec.1⟩
   282	  have pick_nonadj (w : (K : Set V)ᶜ) (hw : C w = i) :
   283	      ¬G.Adj (w : V) (pick w hw : V) :=
   284	    (hex w hw).choose_spec.2
   285	  let out (x : V) (hx : x ∉ K) : (K : Set V)ᶜ :=
   286	    ⟨x, by simpa⟩
   287	  let color : V → (K ⊕ {j : Fin r // j ≠ i}) := fun x ↦
   288	    if hx : x ∈ K then
   289	      Sum.inl ⟨x, hx⟩
   290	    else
   291	      if hc : C (out x hx) = i then
   292	        Sum.inl (pick (out x hx) hc)
   293	      else
   294	        Sum.inr ⟨C (out x hx), hc⟩
   295	  let D : G.Coloring (K ⊕ {j : Fin r // j ≠ i}) :=
   296	    Coloring.mk color (by
   297	      intro x y hxy
   298	      intro heq
   299	      by_cases hx : x ∈ K
   300	      · by_cases hy : y ∈ K
   301	        · have hxy' : x = y := by
   302	            simpa [color, hx, hy] using congrArg Sum.getLeft heq
   303	          exact G.ne_of_adj hxy hxy'
   304	        · by_cases hcy : C (out y hy) = i
   305	          · have heq' : (⟨x, hx⟩ : K) = pick (out y hy) hcy := by
   306	              simpa [color, hx, hy, hcy] using heq
   307	            apply pick_nonadj (out y hy) hcy
   308	            have hyx : G.Adj y x := 

$ /bin/bash -lc "rg -n \"Sum\\.inl_injective|Sum\\.inr_injective|inl\\.inj|inr\\.inj\" Mathlib | head -n 60"
Mathlib/SetTheory/Cardinal/HasCardinalLT.lean:102:    exact ⟨h.of_injective _ Sum.inl_injective,
Mathlib/SetTheory/Cardinal/HasCardinalLT.lean:103:      h.of_injective _ Sum.inr_injective⟩
Mathlib/SetTheory/Cardinal/Arithmetic.lean:772:    refine le_trans (mk_preimage_of_injective _ _ fun x y => Sum.inl.inj) ?_
Mathlib/SetTheory/Cardinal/Arithmetic.lean:784:      cases Sum.inl.inj h
Mathlib/SetTheory/Cardinal/Arithmetic.lean:804:      apply Sum.inr.inj
Mathlib/RingTheory/Kaehler/JacobiZariski.lean:171:      Finsupp.single_apply, ite_smul, one_smul, zero_smul, Sum.inr.injEq,
Mathlib/Topology/UniformSpace/UniformEmbedding.lean:173:  isUniformEmbedding_iff'.2 ⟨Sum.inl_injective, uniformContinuous_inl, fun s hs =>
Mathlib/Topology/UniformSpace/UniformEmbedding.lean:179:  isUniformEmbedding_iff'.2 ⟨Sum.inr_injective, uniformContinuous_inr, fun s hs =>
Mathlib/RingTheory/Smooth/StandardSmoothOfFree.lean:60:    P.cotangentRestrict_bijective_of_basis_kaehlerDifferential Sum.inl_injective
Mathlib/RingTheory/Smooth/StandardSmoothOfFree.lean:69:      map_inj := Sum.map_injective.mpr ⟨fun _ _ h ↦ h, Sum.inl_injective⟩ }
Mathlib/Topology/Connected/Clopen.lean:73:      · exact hs.preimage_of_isOpenMap Sum.inl_injective isOpenMap_inl h
Mathlib/Topology/Connected/Clopen.lean:78:      · exact hs.preimage_of_isOpenMap Sum.inr_injective isOpenMap_inr h
Mathlib/RingTheory/Extension/Presentation/Submersive.lean:261:  map_inj := Function.Injective.sumElim ((Sum.inl_injective).comp (Q.map_inj))
Mathlib/RingTheory/Extension/Presentation/Submersive.lean:262:    ((Sum.inr_injective).comp (P.map_inj)) <| by simp
Mathlib/RingTheory/Extension/Presentation/Submersive.lean:339:  apply pderiv_rename Sum.inr_injective
Mathlib/RingTheory/Extension/Presentation/Basic.lean:374:  simp [Finsupp.prod_mapDomain_index_inj (Sum.inl_injective)]
Mathlib/RingTheory/Extension/Generators.lean:240:    simp [aeval_rename, this, aeval_monomial, Finsupp.prod_mapDomain_index_inj Sum.inl_injective,
Mathlib/RingTheory/

$ /bin/bash -lc 'lake env lean Tihany.lean'
Tihany.lean:63:0: warning: automatically included section variable(s) unused in theorem `Tihany.mem_commonNeighbors`:
  [Fintype V]
  [DecidableEq V]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [Fintype V] [DecidableEq V] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
Tihany.lean:89:0: warning: automatically included section variable(s) unused in theorem `Tihany.EvenHoleFree.c4Free`:
  [Fintype V]
  [DecidableEq V]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [Fintype V] [DecidableEq V] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
Tihany.lean:93:0: warning: automatically included section variable(s) unused in theorem `Tihany.EvenHoleFree.induce`:
  [Fintype V]
  [DecidableEq V]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [Fintype V] [DecidableEq V] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
Tihany.lean:118:2: warning: `push_neg` has been deprecated. Prefer using `push Not` instead.
If you'd rather continue using `push_neg` in your project, you can implement it as follows:
```
open Lean.Parser.Tactic in
macro "push_neg" cfg:optConfig loc:(location)? : tactic =>
  `(tactic| push $cfg:optConfig Not $[$loc]?)
```
Tihany.lean:278:4: warning: `push_neg` has been deprecated. Prefer using `push Not` instead.
If you'd rather continue using `push_neg` in your project, you can implement it as follows:
```
open Lean.Parser.Tactic in
macro "push_neg" cfg:optConfig loc:(location)? : tactic =>
  `(tactic| push $cfg:optConfig Not $[$loc]?)
```
Tihany.lean:339:4: error: omega could not prove the goal:
a possible counterexample may satisfy the constraints
  a ≥ 0
  a ≥ 0
where
 a := ↑(#K + r -

$ /bin/bash -lc "nl -ba Tihany.lean | sed -n '326,345p'"
326	            · simp [color, hx, hy, hcx, hcy] at heq
   327	            · apply hvalid
   328	              have heq' :
   329	                  (⟨C (out x hx), hcx⟩ : {j : Fin r // j ≠ i}) =
   330	                    ⟨C (out y hy), hcy⟩ := by
   331	                simpa [color, hx, hy, hcx, hcy] using heq
   332	              exact congrArg Subtype.val heq')
   333	  have hcard :
   334	      Fintype.card (K ⊕ {j : Fin r // j ≠ i}) = K.card + r - 1 := by
   335	    simp only [Fintype.card_sum, Fintype.card_coe,
   336	      Fintype.card_subtype_compl, Fintype.card_fin]
   337	    have : Fintype.card {j : Fin r // j = i} = 1 := Fintype.card_unique
   338	    rw [this]
   339	    omega
   340	  rw [← hcard]
   341	  exact D.colorable
   342	
   343	end Tihany

$ /bin/bash -lc '# create no file, use existing check via lean stdin unsupported; rg
rg -n "theorem add_sub_assoc|lemma add_sub_assoc" Mathlib/Data/Nat Mathlib/Algebra/Order | head -n 30'

$ /bin/bash -lc "lake env lean --stdin <<'EOF'
import Mathlib
#check Nat.add_sub_assoc
#check Nat.add_sub_of_le
#check Nat.add_sub_cancel_left
#check Nat.sub_add_comm
EOF"
Nat.add_sub_assoc {m k : ℕ} (h : k ≤ m) (n : ℕ) : n + m - k = n + (m - k)
Nat.add_sub_of_le {a b : ℕ} (h : a ≤ b) : a + (b - a) = b
Nat.add_sub_cancel_left (n m : ℕ) : n + m - n = m
Nat.sub_add_comm {n m k : ℕ} (h : k ≤ n) : n + m - k = n - k + m

$ /bin/bash -lc 'lake env lean Tihany.lean'
Tihany.lean:63:0: warning: automatically included section variable(s) unused in theorem `Tihany.mem_commonNeighbors`:
  [Fintype V]
  [DecidableEq V]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [Fintype V] [DecidableEq V] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
Tihany.lean:89:0: warning: automatically included section variable(s) unused in theorem `Tihany.EvenHoleFree.c4Free`:
  [Fintype V]
  [DecidableEq V]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [Fintype V] [DecidableEq V] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
Tihany.lean:93:0: warning: automatically included section variable(s) unused in theorem `Tihany.EvenHoleFree.induce`:
  [Fintype V]
  [DecidableEq V]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [Fintype V] [DecidableEq V] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
Tihany.lean:118:2: warning: `push_neg` has been deprecated. Prefer using `push Not` instead.
If you'd rather continue using `push_neg` in your project, you can implement it as follows:
```
open Lean.Parser.Tactic in
macro "push_neg" cfg:optConfig loc:(location)? : tactic =>
  `(tactic| push $cfg:optConfig Not $[$loc]?)
```
Tihany.lean:278:4: warning: `push_neg` has been deprecated. Prefer using `push Not` instead.
If you'd rather continue using `push_neg` in your project, you can implement it as follows:
```
open Lean.Parser.Tactic in
macro "push_neg" cfg:optConfig loc:(location)? : tactic =>
  `(tactic| push $cfg:optConfig Not $[$loc]?)
```
Tihany.lean:339:33: error: omega could not prove the goal:
No usable constraints found. You may need to unfold definitions so `omega` can see linear a

$ /bin/bash -lc 'lake env lean Tihany.lean'
Tihany.lean:63:0: warning: automatically included section variable(s) unused in theorem `Tihany.mem_commonNeighbors`:
  [Fintype V]
  [DecidableEq V]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [Fintype V] [DecidableEq V] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
Tihany.lean:89:0: warning: automatically included section variable(s) unused in theorem `Tihany.EvenHoleFree.c4Free`:
  [Fintype V]
  [DecidableEq V]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [Fintype V] [DecidableEq V] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
Tihany.lean:93:0: warning: automatically included section variable(s) unused in theorem `Tihany.EvenHoleFree.induce`:
  [Fintype V]
  [DecidableEq V]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [Fintype V] [DecidableEq V] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
Tihany.lean:118:2: warning: `push_neg` has been deprecated. Prefer using `push Not` instead.
If you'd rather continue using `push_neg` in your project, you can implement it as follows:
```
open Lean.Parser.Tactic in
macro "push_neg" cfg:optConfig loc:(location)? : tactic =>
  `(tactic| push $cfg:optConfig Not $[$loc]?)
```
Tihany.lean:278:4: warning: `push_neg` has been deprecated. Prefer using `push Not` instead.
If you'd rather continue using `push_neg` in your project, you can implement it as follows:
```
open Lean.Parser.Tactic in
macro "push_neg" cfg:optConfig loc:(location)? : tactic =>
  `(tactic| push $cfg:optConfig Not $[$loc]?)
```
Tihany.lean:268:0: warning: automatically included section variable(s) unused in theorem `Tihany.colorable_of_missing_commonNeighbor`:
  [Fintype V]
c

$ /bin/bash -lc 'lake env lean Tihany.lean'
Tihany.lean:63:0: warning: automatically included section variable(s) unused in theorem `Tihany.mem_commonNeighbors`:
  [Fintype V]
  [DecidableEq V]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [Fintype V] [DecidableEq V] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
Tihany.lean:89:0: warning: automatically included section variable(s) unused in theorem `Tihany.EvenHoleFree.c4Free`:
  [Fintype V]
  [DecidableEq V]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [Fintype V] [DecidableEq V] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
Tihany.lean:93:0: warning: automatically included section variable(s) unused in theorem `Tihany.EvenHoleFree.induce`:
  [Fintype V]
  [DecidableEq V]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [Fintype V] [DecidableEq V] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
Tihany.lean:118:2: warning: `push_neg` has been deprecated. Prefer using `push Not` instead.
If you'd rather continue using `push_neg` in your project, you can implement it as follows:
```
open Lean.Parser.Tactic in
macro "push_neg" cfg:optConfig loc:(location)? : tactic =>
  `(tactic| push $cfg:optConfig Not $[$loc]?)
```
Tihany.lean:278:4: warning: `push_neg` has been deprecated. Prefer using `push Not` instead.
If you'd rather continue using `push_neg` in your project, you can implement it as follows:
```
open Lean.Parser.Tactic in
macro "push_neg" cfg:optConfig loc:(location)? : tactic =>
  `(tactic| push $cfg:optConfig Not $[$loc]?)
```
Tihany.lean:268:0: warning: automatically included section variable(s) unused in theorem `Tihany.colorable_of_missing_commonNeighbor`:
  [Fintype V]
c

$ /bin/bash -lc "nl -ba Tihany.lean | sed -n '378,410p'"
378	    intro i j hij
   379	    have hwij : w i = w j := Subtype.ext hij
   380	    calc
   381	      i = C (w i) := (hwcolor i).symm
   382	      _ = C (w j) := congrArg C hwij
   383	      _ = j := hwcolor j
   384	  let R : Finset V := Finset.univ.image f
   385	  have hRcard : R.card = r := by
   386	    rw [R, Finset.card_image_of_injective _ hf_inj, Finset.card_univ,
   387	      Fintype.card_fin]
   388	  have hRcommon : ∀ x ∈ R, x ∈ commonNeighbors G K := by
   389	    intro x hx
   390	    rw [R, Finset.mem_image] at hx
   391	    obtain ⟨i, _, rfl⟩ := hx
   392	    exact hwcommon i
   393	  have hKR : Disjoint K R := by
   394	    rw [Finset.disjoint_left]
   395	    intro x hxK hxR
   396	    exact (hRcommon x hxR).1 hxK
   397	  let L := K ∪ R
   398	  have hLcard : L.card = k := by
   399	    rw [L, Finset.card_union_of_disjoint hKR, hRcard]
   400	    exact Nat.add_sub_of_le hKle
   401	  have hLclique : G.IsClique L := by
   402	    intro x hx y hy hxy
   403	    have hx' : x ∈ K ∨ x ∈ R := by simpa [L] using hx
   404	    have hy' : y ∈ K ∨ y ∈ R := by simpa [L] using hy
   405	    rcases hx' with hxK | hxR <;> rcases hy' with hyK | hyR
   406	    · exact hK hxK hyK hxy
   407	    · exact (G.adj_comm x y).mpr ((hRcommon y hyR).2 x hxK)
   408	    · exact (hRcommon x hxR).2 y hyK
   409	    · exact hcommon (hRcommon x hxR) (hRcommon y hyR) hxy
   410	  exact hfree L ⟨hLclique, hLcard⟩

$ /bin/bash -lc 'lake env lean Tihany.lean'
Tihany.lean:63:0: warning: automatically included section variable(s) unused in theorem `Tihany.mem_commonNeighbors`:
  [Fintype V]
  [DecidableEq V]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [Fintype V] [DecidableEq V] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
Tihany.lean:89:0: warning: automatically included section variable(s) unused in theorem `Tihany.EvenHoleFree.c4Free`:
  [Fintype V]
  [DecidableEq V]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [Fintype V] [DecidableEq V] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
Tihany.lean:93:0: warning: automatically included section variable(s) unused in theorem `Tihany.EvenHoleFree.induce`:
  [Fintype V]
  [DecidableEq V]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [Fintype V] [DecidableEq V] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
Tihany.lean:118:2: warning: `push_neg` has been deprecated. Prefer using `push Not` instead.
If you'd rather continue using `push_neg` in your project, you can implement it as follows:
```
open Lean.Parser.Tactic in
macro "push_neg" cfg:optConfig loc:(location)? : tactic =>
  `(tactic| push $cfg:optConfig Not $[$loc]?)
```
Tihany.lean:278:4: warning: `push_neg` has been deprecated. Prefer using `push Not` instead.
If you'd rather continue using `push_neg` in your project, you can implement it as follows:
```
open Lean.Parser.Tactic in
macro "push_neg" cfg:optConfig loc:(location)? : tactic =>
  `(tactic| push $cfg:optConfig Not $[$loc]?)
```
Tihany.lean:268:0: warning: automatically included section variable(s) unused in theorem `Tihany.colorable_of_missing_commonNeighbor`:
  [Fintype V]
c

$ /bin/bash -lc 'rg -n "exists.*not_mem.*card_lt|card_lt.*not_mem|card_lt_card.*not" Mathlib | head -n 120; rg -n "sdiff_nonempty|nonempty_sdiff" Mathlib/Data/Finset | head -n 80'
Mathlib/Data/Fintype/Card.lean:120:  card_lt_card ⟨subset_univ s, not_forall.2 ⟨x, fun hx' => hx (hx' <| mem_univ x)⟩⟩
Mathlib/Data/Set/Card.lean:1244:lemma _root_.Finset.exists_not_mem_of_card_lt_enatCard {s : Finset α} (hs : s.card < ENat.card α) :
Mathlib/Data/Finset/Card.lean:605:theorem sdiff_nonempty_of_card_lt_card (h : #s < #t) : (t \ s).Nonempty := by
Mathlib/Data/Finset/Card.lean:610:  classical simpa [Finset.Nonempty] using sdiff_nonempty_of_card_lt_card h
Mathlib/Data/Finset/SDiff.lean:167:theorem sdiff_nonempty : (s \ t).Nonempty ↔ ¬s ⊆ t :=

$ /bin/bash -lc 'lake env lean Tihany.lean'
Tihany.lean:63:0: warning: automatically included section variable(s) unused in theorem `Tihany.mem_commonNeighbors`:
  [Fintype V]
  [DecidableEq V]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [Fintype V] [DecidableEq V] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
Tihany.lean:89:0: warning: automatically included section variable(s) unused in theorem `Tihany.EvenHoleFree.c4Free`:
  [Fintype V]
  [DecidableEq V]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [Fintype V] [DecidableEq V] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
Tihany.lean:93:0: warning: automatically included section variable(s) unused in theorem `Tihany.EvenHoleFree.induce`:
  [Fintype V]
  [DecidableEq V]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [Fintype V] [DecidableEq V] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
Tihany.lean:118:2: warning: `push_neg` has been deprecated. Prefer using `push Not` instead.
If you'd rather continue using `push_neg` in your project, you can implement it as follows:
```
open Lean.Parser.Tactic in
macro "push_neg" cfg:optConfig loc:(location)? : tactic =>
  `(tactic| push $cfg:optConfig Not $[$loc]?)
```
Tihany.lean:278:4: warning: `push_neg` has been deprecated. Prefer using `push Not` instead.
If you'd rather continue using `push_neg` in your project, you can implement it as follows:
```
open Lean.Parser.Tactic in
macro "push_neg" cfg:optConfig loc:(location)? : tactic =>
  `(tactic| push $cfg:optConfig Not $[$loc]?)
```
Tihany.lean:268:0: warning: automatically included section variable(s) unused in theorem `Tihany.colorable_of_missing_commonNeighbor`:
  [Fintype V]
c

$ /bin/bash -lc 'lake env lean Tihany.lean'
Tihany.lean:63:0: warning: automatically included section variable(s) unused in theorem `Tihany.mem_commonNeighbors`:
  [Fintype V]
  [DecidableEq V]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [Fintype V] [DecidableEq V] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
Tihany.lean:89:0: warning: automatically included section variable(s) unused in theorem `Tihany.EvenHoleFree.c4Free`:
  [Fintype V]
  [DecidableEq V]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [Fintype V] [DecidableEq V] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
Tihany.lean:93:0: warning: automatically included section variable(s) unused in theorem `Tihany.EvenHoleFree.induce`:
  [Fintype V]
  [DecidableEq V]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [Fintype V] [DecidableEq V] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
Tihany.lean:118:2: warning: `push_neg` has been deprecated. Prefer using `push Not` instead.
If you'd rather continue using `push_neg` in your project, you can implement it as follows:
```
open Lean.Parser.Tactic in
macro "push_neg" cfg:optConfig loc:(location)? : tactic =>
  `(tactic| push $cfg:optConfig Not $[$loc]?)
```
Tihany.lean:278:4: warning: `push_neg` has been deprecated. Prefer using `push Not` instead.
If you'd rather continue using `push_neg` in your project, you can implement it as follows:
```
open Lean.Parser.Tactic in
macro "push_neg" cfg:optConfig loc:(location)? : tactic =>
  `(tactic| push $cfg:optConfig Not $[$loc]?)
```
Tihany.lean:268:0: warning: automatically included section variable(s) unused in theorem `Tihany.colorable_of_missing_commonNeighbor`:
  [Fintype V]
c

$ /bin/bash -lc "nl -ba Tihany.lean | sed -n '430,486p'"
430	
   431	/-- The standard critical-graph degree argument: if deleting `v` is
   432	`k`-colorable and `v` has fewer than `k` neighbors, the coloring extends
   433	to all of `G`. -/
   434	theorem colorable_of_delete_colorable_of_degree_lt {G : SimpleGraph V}
   435	    {v : V} {k : ℕ}
   436	    (hdelete : (G.induce {x : V | x ≠ v}).Colorable k)
   437	    (hdegree : G.degree v < k) : G.Colorable k := by
   438	  classical
   439	  letI : Fintype (G.neighborSet v) := Fintype.ofFinite _
   440	  let C : (G.induce {x : V | x ≠ v}).Coloring (Fin k) := hdelete.some
   441	  let neighborColor : G.neighborFinset v → Fin k := fun x ↦
   442	    C ⟨x, G.ne_of_adj (G.adj_symm (by simpa using x.property))⟩
   443	  let used : Finset (Fin k) := Finset.univ.image neighborColor
   444	  have hused : used.card < k := by
   445	    calc
   446	      used.card ≤ (Finset.univ : Finset (G.neighborFinset v)).card :=
   447	        Finset.card_image_le
   448	      _ = G.degree v := by
   449	        simp only [Finset.card_univ, Fintype.card_coe, SimpleGraph.degree]
   450	      _ < k := hdegree
   451	  have hdiff : ((Finset.univ : Finset (Fin k)) \ used).Nonempty := by
   452	    apply Finset.sdiff_nonempty_of_card_lt_card
   453	    simpa using hused
   454	  let i : Fin k := hdiff.choose
   455	  have hi : i ∉ used := (Finset.mem_sdiff.mp hdiff.choose_spec).2
   456	  let color : V → Fin k := fun x ↦ if hx : x = v then i else C ⟨x, hx⟩
   457	  refine ⟨Coloring.mk color ?_⟩
   458	  intro x y hxy
   459	  by_cases hx : x = v
   460	  · subst x
   461	    have hy : y ≠ v := by
   462	      intro h
   463	      subst y
   464	      exact G.irrefl hxy
   465	    simp only [color, if_pos, if_neg hy]
   466	    intro heq
   467	    apply hi
   468	    rw [show used = Finset.univ.image neighborColor from rfl, Finset.mem_image]
   469	    refine ⟨⟨y, by simpa using hxy⟩, Finset.mem_univ _, ?_⟩
   470	    simpa [neighborColor, heq]
   471	  · by_cases hy : y = v
   472	    · subst y
  

$ /bin/bash -lc 'lake env lean Tihany.lean'
Tihany.lean:63:0: warning: automatically included section variable(s) unused in theorem `Tihany.mem_commonNeighbors`:
  [Fintype V]
  [DecidableEq V]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [Fintype V] [DecidableEq V] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
Tihany.lean:89:0: warning: automatically included section variable(s) unused in theorem `Tihany.EvenHoleFree.c4Free`:
  [Fintype V]
  [DecidableEq V]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [Fintype V] [DecidableEq V] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
Tihany.lean:93:0: warning: automatically included section variable(s) unused in theorem `Tihany.EvenHoleFree.induce`:
  [Fintype V]
  [DecidableEq V]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [Fintype V] [DecidableEq V] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
Tihany.lean:118:2: warning: `push_neg` has been deprecated. Prefer using `push Not` instead.
If you'd rather continue using `push_neg` in your project, you can implement it as follows:
```
open Lean.Parser.Tactic in
macro "push_neg" cfg:optConfig loc:(location)? : tactic =>
  `(tactic| push $cfg:optConfig Not $[$loc]?)
```
Tihany.lean:278:4: warning: `push_neg` has been deprecated. Prefer using `push Not` instead.
If you'd rather continue using `push_neg` in your project, you can implement it as follows:
```
open Lean.Parser.Tactic in
macro "push_neg" cfg:optConfig loc:(location)? : tactic =>
  `(tactic| push $cfg:optConfig Not $[$loc]?)
```
Tihany.lean:268:0: warning: automatically included section variable(s) unused in theorem `Tihany.colorable_of_missing_commonNeighbor`:
  [Fintype V]
c

$ /bin/bash -lc 'lake env lean Tihany.lean'
Tihany.lean:63:0: warning: automatically included section variable(s) unused in theorem `Tihany.mem_commonNeighbors`:
  [Fintype V]
  [DecidableEq V]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [Fintype V] [DecidableEq V] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
Tihany.lean:89:0: warning: automatically included section variable(s) unused in theorem `Tihany.EvenHoleFree.c4Free`:
  [Fintype V]
  [DecidableEq V]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [Fintype V] [DecidableEq V] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
Tihany.lean:93:0: warning: automatically included section variable(s) unused in theorem `Tihany.EvenHoleFree.induce`:
  [Fintype V]
  [DecidableEq V]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [Fintype V] [DecidableEq V] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
Tihany.lean:118:2: warning: `push_neg` has been deprecated. Prefer using `push Not` instead.
If you'd rather continue using `push_neg` in your project, you can implement it as follows:
```
open Lean.Parser.Tactic in
macro "push_neg" cfg:optConfig loc:(location)? : tactic =>
  `(tactic| push $cfg:optConfig Not $[$loc]?)
```
Tihany.lean:278:4: warning: `push_neg` has been deprecated. Prefer using `push Not` instead.
If you'd rather continue using `push_neg` in your project, you can implement it as follows:
```
open Lean.Parser.Tactic in
macro "push_neg" cfg:optConfig loc:(location)? : tactic =>
  `(tactic| push $cfg:optConfig Not $[$loc]?)
```
Tihany.lean:268:0: warning: automatically included section variable(s) unused in theorem `Tihany.colorable_of_missing_commonNeighbor`:
  [Fintype V]
c

$ /bin/bash -lc "rg -n \"card_erase_lt|erase.*card.*lt\" Mathlib/Data/Finset | head -n 50; lake env lean --stdin <<'EOF'
import Mathlib
#check Set.isEmpty_empty
#check Finset.card_erase_lt_of_mem
#check Finset.card_erase_of_mem
#check SimpleGraph.induceUnivIso
EOF"
<stdin>:2:7: error(lean.unknownIdentifier): Unknown constant `Set.isEmpty_empty`
Finset.card_erase_lt_of_mem.{u_1} {α : Type u_1} {s : Finset α} {a : α} [DecidableEq α] :
  a ∈ s → (s.erase a).card < s.card
Finset.card_erase_of_mem.{u_1} {α : Type u_1} {s : Finset α} {a : α} [DecidableEq α] :
  a ∈ s → (s.erase a).card = s.card - 1
SimpleGraph.induceUnivIso.{u_1} {V : Type u_1} (G : SimpleGraph V) : SimpleGraph.induce Set.univ G ≃g G

$ /bin/bash -lc 'lake env lean Tihany.lean'
Tihany.lean:63:0: warning: automatically included section variable(s) unused in theorem `Tihany.mem_commonNeighbors`:
  [Fintype V]
  [DecidableEq V]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [Fintype V] [DecidableEq V] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
Tihany.lean:89:0: warning: automatically included section variable(s) unused in theorem `Tihany.EvenHoleFree.c4Free`:
  [Fintype V]
  [DecidableEq V]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [Fintype V] [DecidableEq V] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
Tihany.lean:93:0: warning: automatically included section variable(s) unused in theorem `Tihany.EvenHoleFree.induce`:
  [Fintype V]
  [DecidableEq V]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [Fintype V] [DecidableEq V] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
Tihany.lean:118:2: warning: `push_neg` has been deprecated. Prefer using `push Not` instead.
If you'd rather continue using `push_neg` in your project, you can implement it as follows:
```
open Lean.Parser.Tactic in
macro "push_neg" cfg:optConfig loc:(location)? : tactic =>
  `(tactic| push $cfg:optConfig Not $[$loc]?)
```
Tihany.lean:278:4: warning: `push_neg` has been deprecated. Prefer using `push Not` instead.
If you'd rather continue using `push_neg` in your project, you can implement it as follows:
```
open Lean.Parser.Tactic in
macro "push_neg" cfg:optConfig loc:(location)? : tactic =>
  `(tactic| push $cfg:optConfig Not $[$loc]?)
```
Tihany.lean:268:0: warning: automatically included section variable(s) unused in theorem `Tihany.colorable_of_missing_commonNeighbor`:
  [Fintype V]
c

$ /bin/bash -lc 'lake env lean Tihany.lean'
Tihany.lean:63:0: warning: automatically included section variable(s) unused in theorem `Tihany.mem_commonNeighbors`:
  [Fintype V]
  [DecidableEq V]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [Fintype V] [DecidableEq V] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
Tihany.lean:89:0: warning: automatically included section variable(s) unused in theorem `Tihany.EvenHoleFree.c4Free`:
  [Fintype V]
  [DecidableEq V]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [Fintype V] [DecidableEq V] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
Tihany.lean:93:0: warning: automatically included section variable(s) unused in theorem `Tihany.EvenHoleFree.induce`:
  [Fintype V]
  [DecidableEq V]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [Fintype V] [DecidableEq V] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
Tihany.lean:118:2: warning: `push_neg` has been deprecated. Prefer using `push Not` instead.
If you'd rather continue using `push_neg` in your project, you can implement it as follows:
```
open Lean.Parser.Tactic in
macro "push_neg" cfg:optConfig loc:(location)? : tactic =>
  `(tactic| push $cfg:optConfig Not $[$loc]?)
```
Tihany.lean:278:4: warning: `push_neg` has been deprecated. Prefer using `push Not` instead.
If you'd rather continue using `push_neg` in your project, you can implement it as follows:
```
open Lean.Parser.Tactic in
macro "push_neg" cfg:optConfig loc:(location)? : tactic =>
  `(tactic| push $cfg:optConfig Not $[$loc]?)
```
Tihany.lean:268:0: warning: automatically included section variable(s) unused in theorem `Tihany.colorable_of_missing_commonNeighbor`:
  [Fintype V]
c

$ /bin/bash -lc 'lake env lean Tihany.lean'
Tihany.lean:63:0: warning: automatically included section variable(s) unused in theorem `Tihany.mem_commonNeighbors`:
  [Fintype V]
  [DecidableEq V]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [Fintype V] [DecidableEq V] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
Tihany.lean:89:0: warning: automatically included section variable(s) unused in theorem `Tihany.EvenHoleFree.c4Free`:
  [Fintype V]
  [DecidableEq V]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [Fintype V] [DecidableEq V] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
Tihany.lean:93:0: warning: automatically included section variable(s) unused in theorem `Tihany.EvenHoleFree.induce`:
  [Fintype V]
  [DecidableEq V]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [Fintype V] [DecidableEq V] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
Tihany.lean:118:2: warning: `push_neg` has been deprecated. Prefer using `push Not` instead.
If you'd rather continue using `push_neg` in your project, you can implement it as follows:
```
open Lean.Parser.Tactic in
macro "push_neg" cfg:optConfig loc:(location)? : tactic =>
  `(tactic| push $cfg:optConfig Not $[$loc]?)
```
Tihany.lean:278:4: warning: `push_neg` has been deprecated. Prefer using `push Not` instead.
If you'd rather continue using `push_neg` in your project, you can implement it as follows:
```
open Lean.Parser.Tactic in
macro "push_neg" cfg:optConfig loc:(location)? : tactic =>
  `(tactic| push $cfg:optConfig Not $[$loc]?)
```
Tihany.lean:268:0: warning: automatically included section variable(s) unused in theorem `Tihany.colorable_of_missing_commonNeighbor`:
  [Fintype V]
c

$ /bin/bash -lc 'lake env lean Tihany.lean'
Tihany.lean:63:0: warning: automatically included section variable(s) unused in theorem `Tihany.mem_commonNeighbors`:
  [Fintype V]
  [DecidableEq V]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [Fintype V] [DecidableEq V] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
Tihany.lean:89:0: warning: automatically included section variable(s) unused in theorem `Tihany.EvenHoleFree.c4Free`:
  [Fintype V]
  [DecidableEq V]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [Fintype V] [DecidableEq V] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
Tihany.lean:93:0: warning: automatically included section variable(s) unused in theorem `Tihany.EvenHoleFree.induce`:
  [Fintype V]
  [DecidableEq V]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [Fintype V] [DecidableEq V] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
Tihany.lean:118:2: warning: `push_neg` has been deprecated. Prefer using `push Not` instead.
If you'd rather continue using `push_neg` in your project, you can implement it as follows:
```
open Lean.Parser.Tactic in
macro "push_neg" cfg:optConfig loc:(location)? : tactic =>
  `(tactic| push $cfg:optConfig Not $[$loc]?)
```
Tihany.lean:278:4: warning: `push_neg` has been deprecated. Prefer using `push Not` instead.
If you'd rather continue using `push_neg` in your project, you can implement it as follows:
```
open Lean.Parser.Tactic in
macro "push_neg" cfg:optConfig loc:(location)? : tactic =>
  `(tactic| push $cfg:optConfig Not $[$loc]?)
```
Tihany.lean:268:0: warning: automatically included section variable(s) unused in theorem `Tihany.colorable_of_missing_commonNeighbor`:
  [Fintype V]
c

$ /bin/bash -lc 'lake env lean Tihany.lean'
Tihany.lean:63:0: warning: automatically included section variable(s) unused in theorem `Tihany.mem_commonNeighbors`:
  [Fintype V]
  [DecidableEq V]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [Fintype V] [DecidableEq V] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
Tihany.lean:81:0: warning: automatically included section variable(s) unused in theorem `Tihany.not_colorable_pred_iff_le_chromaticNumber`:
  [Fintype V]
  [DecidableEq V]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [Fintype V] [DecidableEq V] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
Tihany.lean:102:16: error(lean.invalidField): Invalid field `map_adj`: The environment does not contain `RelEmbedding.map_adj`, so it is not possible to project the field `map_adj` from an expression
  f
of type `H.Adj ↪r G.Adj`
Tihany.lean:112:16: error(lean.invalidField): Invalid field `map_adj`: The environment does not contain `RelEmbedding.map_adj`, so it is not possible to project the field `map_adj` from an expression
  f
of type `H.Adj ↪r G.Adj`
Tihany.lean:124:4: warning: try 'simp' instead of 'simpa'

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`
Tihany.lean:137:0: warning: automatically included section variable(s) unused in theorem `Tihany.EvenHoleFree.c4Free`:
  [Fintype V]
  [DecidableEq V]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [Fintype V] [DecidableEq V] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
Tihany.lean:141:0: warning: automatically included section variable(s) unused in theorem `Tihany.EvenHoleFree.induce`:
  [Fintype V]
  [DecidableEq V]
consider restructuring your

$ /bin/bash -lc "lake env lean --stdin <<'EOF'
import Mathlib
open SimpleGraph
#check RelEmbedding.map_rel
#check RelEmbedding.map_rel_iff
#check SimpleGraph.Embedding.map_adj_iff
#check SimpleGraph.Embedding.toHom
#check SimpleGraph.Hom.map_adj
EOF"
<stdin>:3:7: error(lean.unknownIdentifier): Unknown constant `RelEmbedding.map_rel`
RelEmbedding.map_rel_iff.{u_1, u_2} {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (f : r ↪r s)
  {a b : α} : s (f a) (f b) ↔ r a b
SimpleGraph.Embedding.map_adj_iff.{u_1, u_2} {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {G' : SimpleGraph W}
  (f : G ↪g G') {v w : V} : G'.Adj (f v) (f w) ↔ G.Adj v w
SimpleGraph.Embedding.toHom.{u_1, u_2} {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {G' : SimpleGraph W}
  (f : G ↪g G') : G →g G'
SimpleGraph.Hom.map_adj.{u_1, u_2} {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {G' : SimpleGraph W} (f : G →g G')
  {v w : V} (h : G.Adj v w) : G'.Adj (f v) (f w)

$ /bin/bash -lc 'lake env lean Tihany.lean'
Tihany.lean:63:0: warning: automatically included section variable(s) unused in theorem `Tihany.mem_commonNeighbors`:
  [Fintype V]
  [DecidableEq V]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [Fintype V] [DecidableEq V] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
Tihany.lean:81:0: warning: automatically included section variable(s) unused in theorem `Tihany.not_colorable_pred_iff_le_chromaticNumber`:
  [Fintype V]
  [DecidableEq V]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [Fintype V] [DecidableEq V] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
Tihany.lean:93:0: warning: automatically included section variable(s) unused in theorem `Tihany.Splittable.of_embedding`:
  [Fintype V]
  [DecidableEq V]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [Fintype V] [DecidableEq V] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
Tihany.lean:124:4: warning: try 'simp' instead of 'simpa'

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`
Tihany.lean:137:0: warning: automatically included section variable(s) unused in theorem `Tihany.EvenHoleFree.c4Free`:
  [Fintype V]
  [DecidableEq V]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [Fintype V] [DecidableEq V] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
Tihany.lean:141:0: warning: automatically included section variable(s) unused in theorem `Tihany.EvenHoleFree.induce`:
  [Fintype V]
  [DecidableEq V]
consider restructuring your `variable` declarations so that the variables are not

$ /bin/bash -lc 'lake env lean Tihany.lean'
Tihany.lean:63:0: warning: automatically included section variable(s) unused in theorem `Tihany.mem_commonNeighbors`:
  [Fintype V]
  [DecidableEq V]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [Fintype V] [DecidableEq V] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
Tihany.lean:81:0: warning: automatically included section variable(s) unused in theorem `Tihany.not_colorable_pred_iff_le_chromaticNumber`:
  [Fintype V]
  [DecidableEq V]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [Fintype V] [DecidableEq V] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
Tihany.lean:93:0: warning: automatically included section variable(s) unused in theorem `Tihany.Splittable.of_embedding`:
  [Fintype V]
  [DecidableEq V]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [Fintype V] [DecidableEq V] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
Tihany.lean:124:4: warning: try 'simp' instead of 'simpa'

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`
Tihany.lean:137:0: warning: automatically included section variable(s) unused in theorem `Tihany.C4Free.induce`:
  [Fintype V]
  [DecidableEq V]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [Fintype V] [DecidableEq V] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
Tihany.lean:142:0: warning: automatically included section variable(s) unused in theorem `Tihany.EvenHoleFree.c4Free`:
  [Fintype V]
  [DecidableEq V]
consider restructuring your `variable` declarations so that the variables are not in sc

$ /bin/bash -lc "nl -ba Tihany.lean | sed -n '625,668p'"
625	  obtain ⟨A, B, hAB, hA, hB, hn⟩ :=
   626	    (bisimplicial_iff_finset H v).mp hvbis
   627	  have finish (A B : Finset S)
   628	      (hAB : Disjoint A B) (hA : H.IsClique A) (hB : H.IsClique B)
   629	      (hn : (((A ∪ B : Finset S) : Set S)) = H.neighborSet v)
   630	      (hBA : B.card ≤ A.card) : Splittable H s t := by
   631	    letI : Fintype (H.neighborSet v) := Fintype.ofFinite _
   632	    have hdegree : k - 1 ≤ H.degree v := by
   633	      by_contra h
   634	      have hlt : H.degree v < k - 1 := Nat.lt_of_not_ge h
   635	      exact hnH
   636	        (colorable_of_delete_colorable_of_degree_lt
   637	          (hcritical v) hlt)
   638	    have hdegree_eq : H.degree v = A.card + B.card := by
   639	      rw [SimpleGraph.degree]
   640	      have heq : H.neighborFinset v = A ∪ B := by
   641	        ext x
   642	        rw [mem_neighborFinset, ← mem_neighborSet, ← hn]
   643	        simp
   644	      rw [heq, Finset.card_union_of_disjoint hAB]
   645	    have hAlarge : s - 1 ≤ A.card := by
   646	      omega
   647	    obtain ⟨K, _, hKcard, _, hT⟩ :=
   648	      exists_tihany_clique hHcol hnH hHfree hHC4 hAB hA hB hn
   649	        (by omega : 1 ≤ s - 1) hAlarge
   650	    apply splittable_of_tihany_clique (by omega) (by omega) hk
   651	    · omega
   652	    · exact hT
   653	  have hsplitH : Splittable H s t := by
   654	    rcases le_total B.card A.card with hBA | hABcard
   655	    · exact finish A B hAB hA hB hn hBA
   656	    · apply finish B A hAB.symm hB hA
   657	      · simpa [Finset.union_comm] using hn
   658	      · exact hABcard
   659	  exact Splittable.of_embedding (Embedding.induce (S : Set V)) hsplitH
   660	
   661	end Tihany

$ /bin/bash -lc 'lake env lean Tihany.lean'
Tihany.lean:63:0: warning: automatically included section variable(s) unused in theorem `Tihany.mem_commonNeighbors`:
  [Fintype V]
  [DecidableEq V]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [Fintype V] [DecidableEq V] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
Tihany.lean:81:0: warning: automatically included section variable(s) unused in theorem `Tihany.not_colorable_pred_iff_le_chromaticNumber`:
  [Fintype V]
  [DecidableEq V]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [Fintype V] [DecidableEq V] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
Tihany.lean:93:0: warning: automatically included section variable(s) unused in theorem `Tihany.Splittable.of_embedding`:
  [Fintype V]
  [DecidableEq V]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [Fintype V] [DecidableEq V] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
Tihany.lean:124:4: warning: try 'simp' instead of 'simpa'

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`
Tihany.lean:137:0: warning: automatically included section variable(s) unused in theorem `Tihany.C4Free.induce`:
  [Fintype V]
  [DecidableEq V]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [Fintype V] [DecidableEq V] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
Tihany.lean:142:0: warning: automatically included section variable(s) unused in theorem `Tihany.EvenHoleFree.c4Free`:
  [Fintype V]
  [DecidableEq V]
consider restructuring your `variable` declarations so that the variables are not in sc

$ /bin/bash -lc "lake env lean --stdin <<'EOF'
import Mathlib
open SimpleGraph
#check chromaticNumber_eq_iff_colorable_not_colorable
#check cliqueNum_le_chromaticNumber
#check ENat.coe_lt_coe
#check ENat.natCast_lt
#check ENat.natCast_inj
EOF"
SimpleGraph.chromaticNumber_eq_iff_colorable_not_colorable.{u} {V : Type u} {G : SimpleGraph V} {n : ℕ} :
  G.chromaticNumber = ↑n + 1 ↔ G.Colorable (n + 1) ∧ ¬G.Colorable n
SimpleGraph.cliqueNum_le_chromaticNumber.{u} {V : Type u} {G : SimpleGraph V} : ↑G.cliqueNum ≤ G.chromaticNumber
ENat.coe_lt_coe {n m : ℕ} : ↑n < ↑m ↔ n < m
<stdin>:6:7: error(lean.unknownIdentifier): Unknown constant `ENat.natCast_lt`
ENat.natCast_inj {a b : ℕ} : ↑a = ↑b ↔ a = b

$ /bin/bash -lc 'lake env lean Tihany.lean'
Tihany.lean:63:0: warning: automatically included section variable(s) unused in theorem `Tihany.mem_commonNeighbors`:
  [Fintype V]
  [DecidableEq V]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [Fintype V] [DecidableEq V] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
Tihany.lean:84:21: error: Type mismatch: After simplification, term
  hS
 has type
  ↑s ≤ (induce S G).chromaticNumber
but is expected to have type
  ↑s ≤ (induce Sᶜᶜ G).chromaticNumber
Tihany.lean:86:0: warning: automatically included section variable(s) unused in theorem `Tihany.not_colorable_pred_iff_le_chromaticNumber`:
  [Fintype V]
  [DecidableEq V]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [Fintype V] [DecidableEq V] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
Tihany.lean:98:0: warning: automatically included section variable(s) unused in theorem `Tihany.Splittable.of_embedding`:
  [Fintype V]
  [DecidableEq V]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [Fintype V] [DecidableEq V] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
Tihany.lean:129:4: warning: try 'simp' instead of 'simpa'

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`
Tihany.lean:142:0: warning: automatically included section variable(s) unused in theorem `Tihany.C4Free.induce`:
  [Fintype V]
  [DecidableEq V]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [Fintype V] [DecidableEq V] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
Tihany.lean:147:0: warning: automatically included s

$ /bin/bash -lc "lake env lean --stdin <<'EOF'
import Mathlib
#check compl_compl
#check Set.compl_compl
#check SetCoe.ext
EOF"
compl_compl.{u} {α : Type u} [BooleanAlgebra α] (x : α) : xᶜᶜ = x
<stdin>:3:7: error(lean.unknownIdentifier): Unknown constant `Set.compl_compl`
SetCoe.ext.{u} {α : Type u} {s : Set α} {a b : ↑s} : ↑a = ↑b → a = b

$ /bin/bash -lc 'lake env lean Tihany.lean'
Tihany.lean:63:0: warning: automatically included section variable(s) unused in theorem `Tihany.mem_commonNeighbors`:
  [Fintype V]
  [DecidableEq V]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [Fintype V] [DecidableEq V] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
Tihany.lean:81:0: warning: automatically included section variable(s) unused in theorem `Tihany.Splittable.symm`:
  [Fintype V]
  [DecidableEq V]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [Fintype V] [DecidableEq V] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
Tihany.lean:88:0: warning: automatically included section variable(s) unused in theorem `Tihany.not_colorable_pred_iff_le_chromaticNumber`:
  [Fintype V]
  [DecidableEq V]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [Fintype V] [DecidableEq V] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
Tihany.lean:100:0: warning: automatically included section variable(s) unused in theorem `Tihany.Splittable.of_embedding`:
  [Fintype V]
  [DecidableEq V]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [Fintype V] [DecidableEq V] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
Tihany.lean:131:4: warning: try 'simp' instead of 'simpa'

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`
Tihany.lean:144:0: warning: automatically included section variable(s) unused in theorem `Tihany.C4Free.induce`:
  [Fintype V]
  [DecidableEq V]
consider restructuring your `variable` declarations so that the variables are not in scope 

$ /bin/bash -lc 'lake env lean Tihany.lean'
Tihany.lean:63:0: warning: automatically included section variable(s) unused in theorem `Tihany.mem_commonNeighbors`:
  [Fintype V]
  [DecidableEq V]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [Fintype V] [DecidableEq V] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
Tihany.lean:81:0: warning: automatically included section variable(s) unused in theorem `Tihany.Splittable.symm`:
  [Fintype V]
  [DecidableEq V]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [Fintype V] [DecidableEq V] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
Tihany.lean:88:0: warning: automatically included section variable(s) unused in theorem `Tihany.not_colorable_pred_iff_le_chromaticNumber`:
  [Fintype V]
  [DecidableEq V]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [Fintype V] [DecidableEq V] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
Tihany.lean:100:0: warning: automatically included section variable(s) unused in theorem `Tihany.Splittable.of_embedding`:
  [Fintype V]
  [DecidableEq V]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [Fintype V] [DecidableEq V] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
Tihany.lean:131:4: warning: try 'simp' instead of 'simpa'

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`
Tihany.lean:144:0: warning: automatically included section variable(s) unused in theorem `Tihany.C4Free.induce`:
  [Fintype V]
  [DecidableEq V]
consider restructuring your `variable` declarations so that the variables are not in scope 

$ /bin/bash -lc "sed -n '430,520p' Mathlib/Combinatorics/SimpleGraph/Copy.lean; rg -n \"isIndContained_iff|IndContained.*exists|exists.*IndContained\" Mathlib/Combinatorics/SimpleGraph/Copy.lean | head -n 100; rg -n \"sorry|admit|axiom\" Tihany.lean; lake env lean --stdin <<'EOF'
import «Tihany»
#print axioms Tihany.theorem14
#print axioms Tihany.theorem15
EOF"
<stdin>:1:0: error: unknown module prefix 'Tihany'

No directory 'Tihany' or file 'Tihany.olean' in the search path entries:
/work/repro/.lake/packages/Cli/.lake/build/lib/lean
/work/repro/.lake/packages/batteries/.lake/build/lib/lean
/work/repro/.lake/packages/Qq/.lake/build/lib/lean
/work/repro/.lake/packages/aesop/.lake/build/lib/lean
/work/repro/.lake/packages/proofwidgets/.lake/build/lib/lean
/work/repro/.lake/packages/importGraph/.lake/build/lib/lean
/work/repro/.lake/packages/LeanSearchClient/.lake/build/lib/lean
/work/repro/.lake/packages/plausible/.lake/build/lib/lean
/work/repro/.lake/build/lib/lean
/opt/elan/toolchains/leanprover--lean4---v4.33.0-rc1/lib/lean
/opt/elan/toolchains/leanprover--lean4---v4.33.0-rc1/lib/lean

$ /bin/bash -lc 'lake env lean Tihany.lean'
Tihany.lean:63:0: warning: automatically included section variable(s) unused in theorem `Tihany.mem_commonNeighbors`:
  [Fintype V]
  [DecidableEq V]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [Fintype V] [DecidableEq V] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
Tihany.lean:89:0: warning: automatically included section variable(s) unused in theorem `Tihany.splittable_iff_partition`:
  [Fintype V]
  [DecidableEq V]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [Fintype V] [DecidableEq V] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
Tihany.lean:108:0: warning: automatically included section variable(s) unused in theorem `Tihany.Splittable.symm`:
  [Fintype V]
  [DecidableEq V]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [Fintype V] [DecidableEq V] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
Tihany.lean:115:0: warning: automatically included section variable(s) unused in theorem `Tihany.not_colorable_pred_iff_le_chromaticNumber`:
  [Fintype V]
  [DecidableEq V]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [Fintype V] [DecidableEq V] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
Tihany.lean:127:0: warning: automatically included section variable(s) unused in theorem `Tihany.Splittable.of_embedding`:
  [Fintype V]
  [DecidableEq V]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [Fintype V] [DecidableEq V] in theorem ...

Note: This linter can be disabled with `set_option li

$ /bin/bash -lc 'lake env lean Tihany.lean 2>&1 | tail -n 40'
Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
Tihany.lean:216:2: warning: `push_neg` has been deprecated. Prefer using `push Not` instead.
If you'd rather continue using `push_neg` in your project, you can implement it as follows:
```
open Lean.Parser.Tactic in
macro "push_neg" cfg:optConfig loc:(location)? : tactic =>
  `(tactic| push $cfg:optConfig Not $[$loc]?)
```
Tihany.lean:376:4: warning: `push_neg` has been deprecated. Prefer using `push Not` instead.
If you'd rather continue using `push_neg` in your project, you can implement it as follows:
```
open Lean.Parser.Tactic in
macro "push_neg" cfg:optConfig loc:(location)? : tactic =>
  `(tactic| push $cfg:optConfig Not $[$loc]?)
```
Tihany.lean:366:0: warning: automatically included section variable(s) unused in theorem `Tihany.colorable_of_missing_commonNeighbor`:
  [Fintype V]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [Fintype V] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
Tihany.lean:394:6: warning: Try this: intro x y hxy heq
Tihany.lean:445:45: warning: Variable name `hKne` is not explicitly referenced.

Hint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning:
  [apply] _hKne

Note: This linter can be disabled with `set_option linter.unusedVariables false`
Tihany.lean:532:0: warning: automatically included section variable(s) unused in theorem `Tihany.colorable_of_delete_colorable_of_degree_lt`:
  [Fintype V]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [Fintype V] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
Tihany.lean:723:4: warning: try 'simp' instead of 'simpa'

Note: This linter can be disabled with `set_option lint

$ /bin/bash -lc 'lake env lean Tihany.lean'
Tihany.lean:63:0: warning: automatically included section variable(s) unused in theorem `Tihany.mem_commonNeighbors`:
  [Fintype V]
  [DecidableEq V]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [Fintype V] [DecidableEq V] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
Tihany.lean:89:0: warning: automatically included section variable(s) unused in theorem `Tihany.splittable_iff_partition`:
  [Fintype V]
  [DecidableEq V]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [Fintype V] [DecidableEq V] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
Tihany.lean:108:0: warning: automatically included section variable(s) unused in theorem `Tihany.Splittable.symm`:
  [Fintype V]
  [DecidableEq V]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [Fintype V] [DecidableEq V] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
Tihany.lean:115:0: warning: automatically included section variable(s) unused in theorem `Tihany.not_colorable_pred_iff_le_chromaticNumber`:
  [Fintype V]
  [DecidableEq V]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [Fintype V] [DecidableEq V] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
Tihany.lean:127:0: warning: automatically included section variable(s) unused in theorem `Tihany.Splittable.of_embedding`:
  [Fintype V]
  [DecidableEq V]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [Fintype V] [DecidableEq V] in theorem ...

Note: This linter can be disabled with `set_option li

$ /bin/bash -lc 'lake env lean Tihany.lean >/tmp/tihany-final.log 2>&1; lean_status=$?; rg -n "'"\\bsorry\\b|\\badmit\\b|"'^[[:space:]]*axiom'"\\b\" Tihany.lean || true; git status --short; git diff --stat -- Tihany.lean README.md; tail -n 8 /tmp/tihany-final.log; exit \""'$lean_status"'
M README.md
?? Tihany.lean
 README.md | 271 ++++++++++++++++++++++++++++----------------------------------
 1 file changed, 123 insertions(+), 148 deletions(-)
  [Fintype V]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [Fintype V] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
Tihany.lean:723:4: warning: try 'simp' instead of 'simpa'

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`