awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring
Goal:
V : Type u
inst : Fintype V
C : Coloring (V := V) ⊤ V
rw : Injective (α := V) (β := V) (⇑C : (a : V) → V)
⊢ Surjective (α := V) (β := V) (⇑C : (a : V) → V)

Tactic:
rw [← Finite.injective_iff_surjective]

Premises used: Finite.injective_iff_surjective
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring
Goal:
V : Type u
inst : Fintype V
C : Coloring (V := V) ⊤ V
⊢ Injective (α := V) (β := V) (⇑C : (a : V) → V)

Tactic:
Hom.injective_of_top_hom C

Premises used: SimpleGraph.Hom.injective_of_top_hom
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring
Goal:
V : Type u
inst : Fintype V
C : Coloring (V := V) ⊤ V
⊢ Injective (α := V) (β := V) (⇑C : (a : V) → V)

Tactic:
exact Hom.injective_of_top_hom C

Premises used: SimpleGraph.Hom.injective_of_top_hom
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring
Goal:
V : Type u_4
inst : Infinite V
by_contra : ∀ (hc : ¬chromaticNumber.{u_4} (V := V) ⊤ = ⊤), False
⊢ chromaticNumber.{u_4} (V := V) ⊤ = ⊤

Tactic:
by_contra hc
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring
Goal:
V : Type u_4
inst : Infinite V
hc : ¬chromaticNumber.{u_4} (V := V) ⊤ = ⊤
⊢ ∃ (n : ℕ), Colorable.{u_4} (V := V) ⊤ n

Tactic:
rw [← Ne, chromaticNumber_ne_top_iff_exists] at hc

Premises used: Ne, SimpleGraph.chromaticNumber_ne_top_iff_exists
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring
Goal:
V : Type u_4
inst : Infinite V
hc : ∃ (n : ℕ), Colorable.{u_4} (V := V) ⊤ n
obtain : ∀ (n : ℕ) (hn : Coloring (V := V) ⊤ (Fin n)), False
⊢ False

Tactic:
obtain ⟨n, ⟨hn⟩⟩ := hc
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring
Goal:
V : Type u_4
inst : Infinite V
n : ℕ
hn : Coloring (V := V) ⊤ (Fin n)
⊢ False

Tactic:
not_injective_infinite_finite _ hn.injective_of_top_hom

Premises used: not_injective_infinite_finite, SimpleGraph.Hom.injective_of_top_hom
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring
Goal:
V : Type u_4
inst : Infinite V
n : ℕ
hn : Coloring (V := V) ⊤ (Fin n)
⊢ False

Tactic:
exact not_injective_infinite_finite _ hn.injective_of_top_hom

Premises used: not_injective_infinite_finite, SimpleGraph.Hom.injective_of_top_hom
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring
Goal:
V : Type u
inl : Finite V → chromaticNumber.{u} (V := V) ⊤ = ENat.card V
inr : Infinite V → chromaticNumber.{u} (V := V) ⊤ = ENat.card V
⊢ chromaticNumber.{u} (V := V) ⊤ = ENat.card V

Tactic:
cases finite_or_infinite V

Premises used: finite_or_infinite
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring
Goal:
V : Type u
h : Finite V
inl : ∀ (this : Fintype V), chromaticNumber.{u} (V := V) ⊤ = ENat.card V
⊢ chromaticNumber.{u} (V := V) ⊤ = ENat.card V

Tactic:
have := Fintype.ofFinite ‹_›
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring
Goal:
V : Type u
h : Finite V
this : Fintype V
⊢ chromaticNumber.{u} (V := V) ⊤ = ENat.card V

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring
Goal:
V : Type u
h : Infinite V
⊢ chromaticNumber.{u} (V := V) ⊤ = ENat.card V

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring
Goal:
V : Type u
G : SimpleGraph V
inst : Fintype V
h : G.chromaticNumber = (↑(card V) : ℕ∞)
by_contra! : ∀ (hh : G ≠ ⊤), False
⊢ G = ⊤

Tactic:
by_contra! hh
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring
Goal:
V : Type u
G : SimpleGraph V
inst : Fintype V
h : G.chromaticNumber = (↑(card V) : ℕ∞)
hh : G ≠ ⊤
obtain : ∀ (a b : V) (hne : a ≠ b), ¬G.Adj a b → G.chromaticNumber ≤ HSub.hSub (α := ℕ∞) (↑(card V) : ℕ∞) 1
⊢ G.chromaticNumber ≤ HSub.hSub (α := ℕ∞) (↑(card V) : ℕ∞) 1

Tactic:
obtain ⟨a, b, hne, _⟩ := ne_top_iff_exists_not_adj.mp hh

Premises used: SimpleGraph.ne_top_iff_exists_not_adj, Iff.mp
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring
Goal:
V : Type u
G : SimpleGraph V
inst : Fintype V
h : G.chromaticNumber = (↑(card V) : ℕ∞)
hh : G ≠ ⊤
a b : V
hne : a ≠ b
right : ¬G.Adj a b
apply : G.Colorable (card V - 1)
⊢ G.chromaticNumber ≤ HSub.hSub (α := ℕ∞) (↑(card V) : ℕ∞) 1

Tactic:
apply chromaticNumber_le_iff_colorable.mpr

Premises used: Iff.mpr, SimpleGraph.chromaticNumber_le_iff_colorable
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring
Goal:
V : Type u
G : SimpleGraph V
inst : Fintype V
h : G.chromaticNumber = (↑(card V) : ℕ∞)
hh : G ≠ ⊤
a b : V
hne : a ≠ b
right : ¬G.Adj a b
this : G.Coloring ↥(Finset.erase Finset.univ b)
⊢ G.Colorable (card V - 1)

Tactic:
simpa using Coloring.colorable this

Premises used: SimpleGraph.Coloring.colorable
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring
Goal:
V : Type u
G : SimpleGraph V
inst : Fintype V
h : G.chromaticNumber = (↑(card V) : ℕ∞)
hh : G ≠ ⊤
a b : V
hne : a ≠ b
right : ¬G.Adj a b
suffices : G.Coloring ↥(Finset.erase Finset.univ b)
⊢ G.Colorable (card V - 1)

Tactic:
suffices G.Coloring (Finset.univ.erase b) by simpa using Coloring.colorable this
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring
Goal:
V : Type u
G : SimpleGraph V
inst : Fintype V
h : G.chromaticNumber = (↑(card V) : ℕ∞)
hh : G ≠ ⊤
a b : V
hne : a ≠ b
right : ¬G.Adj a b
x : V
h' : x ≠ b
⊢ x ∈ Finset.erase Finset.univ b

Tactic:
simp [h']
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring
Goal:
V : Type u
G : SimpleGraph V
inst : Fintype V
h : G.chromaticNumber = (↑(card V) : ℕ∞)
hh : G ≠ ⊤
a b : V
hne : a ≠ b
right : ¬G.Adj a b
x : V
h' : ¬x ≠ b
⊢ a ∈ Finset.erase Finset.univ b

Tactic:
simp [hne]
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring
Goal:
V : Type u
G : SimpleGraph V
inst : Fintype V
h : G.chromaticNumber = (↑(card V) : ℕ∞)
hh : G ≠ ⊤
a b : V
hne : a ≠ b
right : ¬G.Adj a b
apply :
  ∀ {v w : V},
    G.Adj v w →
      Ne.{u + 1} (α := ↥(Finset.erase Finset.univ b))
        (if h' : v ≠ b then Subtype.mk (p := fun (x : V) ↦ x ∈ Finset.erase Finset.univ b) v ⋯
        else Subtype.mk (p := fun (x : V) ↦ x ∈ Finset.erase Finset.univ b) a ⋯)
        (if h' : w ≠ b then Subtype.mk (p := fun (x : V) ↦ x ∈ Finset.erase Finset.univ b) w ⋯
        else Subtype.mk (p := fun (x : V) ↦ x ∈ Finset.erase Finset.univ b) a ⋯)
⊢ G.Coloring ↥(Finset.erase Finset.univ b)

Tactic:
apply Coloring.mk (fun x ↦ if h' : x ≠ b then ⟨x, by simp [h']⟩ else ⟨a, by simp [hne]⟩)

Premises used: SimpleGraph.Coloring.mk, Ne, dite
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring
Goal:
V : Type u
G : SimpleGraph V
inst : Fintype V
h : G.chromaticNumber = (↑(card V) : ℕ∞)
hh : G ≠ ⊤
a b : V
hne : a ≠ b
right : ¬G.Adj a b
⊢ ∀ {v w : V},
    G.Adj v w →
      Ne.{u + 1} (α := ↥(Finset.erase Finset.univ b))
        (if h' : v ≠ b then Subtype.mk (p := fun (x : V) ↦ x ∈ Finset.erase Finset.univ b) v ⋯
        else Subtype.mk (p := fun (x : V) ↦ x ∈ Finset.erase Finset.univ b) a ⋯)
        (if h' : w ≠ b then Subtype.mk (p := fun (x : V) ↦ x ∈ Finset.erase Finset.univ b) w ⋯
        else Subtype.mk (p := fun (x : V) ↦ x ∈ Finset.erase Finset.univ b) a ⋯)

Tactic:
grind [Adj.ne', adj_symm]

Premises used: SimpleGraph.Adj.ne', SimpleGraph.adj_symm
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring
Goal:
V : Type u
G : SimpleGraph V
inst : Fintype V
h : G.chromaticNumber = (↑(card V) : ℕ∞)
hh : G ≠ ⊤
⊢ G.chromaticNumber ≤ HSub.hSub (α := ℕ∞) (↑(card V) : ℕ∞) 1

Tactic:
have : G.chromaticNumber ≤ Fintype.card V - 1 := by
    obtain ⟨a, b, hne, _⟩ := ne_top_iff_exists_not_adj.mp hh
    apply chromaticNumber_le_iff_colorable.mpr
    suffices G.Coloring (Finset.univ.erase b) by simpa using Coloring.colorable this
    apply Coloring.mk (fun x ↦ if h' : x ≠ b then ⟨x, by simp [h']⟩ else ⟨a, by simp [hne]⟩)
    grind [Adj.ne', adj_symm]
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring
Goal:
V : Type u
G : SimpleGraph V
inst : Fintype V
h : G.chromaticNumber = (↑(card V) : ℕ∞)
hh : G ≠ ⊤
this : G.chromaticNumber ≤ HSub.hSub (α := ℕ∞) (↑(card V) : ℕ∞) 1
⊢ card V ≤ card V - 1

Tactic:
rw [h, ← ENat.coe_one, ← ENat.coe_sub, ENat.coe_le_coe] at this

Premises used: ENat.coe_one, ENat.coe_sub, ENat.coe_le_coe
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring
Goal:
V : Type u
G : SimpleGraph V
inst : Fintype V
h : G.chromaticNumber = (↑(card V) : ℕ∞)
hh : G ≠ ⊤
this : card V ≤ card V - 1
⊢ 1 < card V

Tactic:
have := Fintype.one_lt_card_iff_nontrivial.mpr <| SimpleGraph.nontrivial_iff.mp ⟨_, _, hh⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring
Goal:
V : Type u
G : SimpleGraph V
inst : Fintype V
h : G.chromaticNumber = (↑(card V) : ℕ∞)
hh : G ≠ ⊤
this_1 : card V ≤ card V - 1
this : 1 < card V
⊢ False

Tactic:
grind
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring
Goal:
V : Type u
G : SimpleGraph V
inst : Fintype V
h : G.chromaticNumber = (↑(card V) : ℕ∞)
by_contra! by_contra!₁ by_contra!₂ by_contra!₃ : ¬G = ⊤ → False
by_contra!₄ by_contra!₅ by_contra!₆ by_contra!₇ by_contra!₈ by_contra!₉ by_contra!₁₀ : ∀ (hh : G ≠ ⊤), False
by_contra!₁₁ : ∀ (hh : G ≠ ⊤) (this : G.chromaticNumber ≤ HSub.hSub (α := ℕ∞) (↑(card V) : ℕ∞) 1), False
by_contra!₁₂ : ∀ (hh : G ≠ ⊤) (this : card V ≤ card V - 1), False
by_contra!₁₃ : ∀ (hh : G ≠ ⊤) (this : card V ≤ card V - 1) (this : 1 < card V), False
⊢ G = ⊤

Tactic:
classical
  by_contra! hh
  have : G.chromaticNumber ≤ Fintype.card V - 1 := by
    obtain ⟨a, b, hne, _⟩ := ne_top_iff_exists_not_adj.mp hh
    apply chromaticNumber_le_iff_colorable.mpr
    suffices G.Coloring (Finset.univ.erase b) by simpa using Coloring.colorable this
    apply Coloring.mk (fun x ↦ if h' : x ≠ b then ⟨x, by simp [h']⟩ else ⟨a, by simp [hne]⟩)
    grind [Adj.ne', adj_symm]
  rw [h, ← ENat.coe_one, ← ENat.coe_sub, ENat.coe_le_coe] at this
  have := Fintype.one_lt_card_iff_nontrivial.mpr <| SimpleGraph.nontrivial_iff.mp ⟨_, _, hh⟩
  grind

Premises used: ENat.coe_one, ENat.coe_sub, ENat.coe_le_coe
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring
Goal:
V : Type u
G : SimpleGraph V
inst : Fintype V
⊢ G.chromaticNumber = (↑(card V) : ℕ∞) ↔ G = ⊤

Tactic:
⟨eq_top_of_chromaticNumber_eq_card, fun h ↦ h ▸ chromaticNumber_top⟩

Premises used: SimpleGraph.chromaticNumber_top, Eq.rec, Iff.intro, SimpleGraph.eq_top_of_chromaticNumber_eq_card, Eq.symm
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring
Goal:
V : Type u
G : SimpleGraph V
inst : Fintype V
rw : G.chromaticNumber ≤ chromaticNumber.{u} (V := V) ⊤
⊢ G.chromaticNumber ≤ (↑(card V) : ℕ∞)

Tactic:
rw [← chromaticNumber_top]

Premises used: SimpleGraph.chromaticNumber_top
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring
Goal:
V : Type u
G : SimpleGraph V
inst : Fintype V
⊢ G.chromaticNumber ≤ chromaticNumber.{u} (V := V) ⊤

Tactic:
chromaticNumber_mono_of_hom G.selfColoring

Premises used: SimpleGraph.selfColoring, SimpleGraph.chromaticNumber_mono_of_hom
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring
Goal:
V : Type u
G : SimpleGraph V
inst : Fintype V
⊢ G.chromaticNumber ≤ chromaticNumber.{u} (V := V) ⊤

Tactic:
exact chromaticNumber_mono_of_hom G.selfColoring

Premises used: SimpleGraph.selfColoring, SimpleGraph.chromaticNumber_mono_of_hom
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring
Goal:
V : Type u
G : SimpleGraph V
u v : V
hadj : G.Adj u v
⊢ 2 ≤ G.chromaticNumber

Tactic:
le_of_not_gt fun h ↦ ?_

Premises used: le_of_not_gt
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring
Goal:
V : Type u
G : SimpleGraph V
u v : V
hadj : G.Adj u v
refine : ∀ (h : G.chromaticNumber < 2), False
⊢ 2 ≤ G.chromaticNumber

Tactic:
refine le_of_not_gt fun h ↦ ?_

Premises used: le_of_not_gt
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring
Goal:
V : Type u
G : SimpleGraph V
u v : V
hadj : G.Adj u v
h : G.chromaticNumber < 2
obtain : ∀ (c : G.Coloring (Fin 1)), False
⊢ False

Tactic:
obtain ⟨c⟩ := chromaticNumber_le_iff_colorable.mp (Order.le_of_lt_add_one h)

Premises used: SimpleGraph.chromaticNumber_le_iff_colorable, Order.le_of_lt_add_one, Iff.mp
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring
Goal:
V : Type u
G : SimpleGraph V
u v : V
hadj : G.Adj u v
h : G.chromaticNumber < 2
c : G.Coloring (Fin 1)
⊢ False

Tactic:
c.valid hadj (Subsingleton.elim (c u) (c v))

Premises used: SimpleGraph.Coloring.valid, Subsingleton.elim, DFunLike.coe
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring
Goal:
V : Type u
G : SimpleGraph V
u v : V
hadj : G.Adj u v
h : G.chromaticNumber < 2
c : G.Coloring (Fin 1)
⊢ False

Tactic:
exact c.valid hadj (Subsingleton.elim (c u) (c v))

Premises used: SimpleGraph.Coloring.valid, Subsingleton.elim, DFunLike.coe
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring
Goal:
V : Type u
G : SimpleGraph V
⊢ G.chromaticNumber = 0 ↔ IsEmpty V

Tactic:
nonpos_iff_eq_zero.symm.trans <| chromaticNumber_le_iff_colorable.trans colorable_zero_iff

Premises used: SimpleGraph.chromaticNumber_le_iff_colorable, Iff.trans, SimpleGraph.colorable_zero_iff, Iff.symm, nonpos_iff_eq_zero
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring
Goal:
V : Type u
G : SimpleGraph V
inst : IsEmpty V
⊢ G.chromaticNumber = 0

Tactic:
simpa
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring
Goal:
V : Type u
G : SimpleGraph V
rw : G.chromaticNumber ≤ 1 ∧ ¬G.chromaticNumber < 1 ↔ G = ⊥ ∧ Nonempty V
rw₁ : G.chromaticNumber ≤ 1 ∧ ¬G.chromaticNumber ≤ 0 ↔ G = ⊥ ∧ Nonempty V
rw₂ : G.chromaticNumber ≤ 1 ∧ ¬G.chromaticNumber ≤ 0 ↔ G = ⊥ ∧ ¬IsEmpty V
rw₃ : G.chromaticNumber ≤ (↑1 : ℕ∞) ∧ ¬G.chromaticNumber ≤ 0 ↔ G = ⊥ ∧ ¬IsEmpty V
rw₄ : G.chromaticNumber ≤ (↑1 : ℕ∞) ∧ ¬G.chromaticNumber ≤ (↑0 : ℕ∞) ↔ G = ⊥ ∧ ¬IsEmpty V
rw₅ : G.Colorable 1 ∧ ¬G.chromaticNumber ≤ (↑0 : ℕ∞) ↔ G = ⊥ ∧ ¬IsEmpty V
rw₆ : G.Colorable 1 ∧ ¬G.Colorable 0 ↔ G = ⊥ ∧ ¬IsEmpty V
rw₇ : G = ⊥ ∧ ¬G.Colorable 0 ↔ G = ⊥ ∧ ¬IsEmpty V
rw₈ rw₉ : G = ⊥ ∧ ¬IsEmpty V ↔ G = ⊥ ∧ ¬IsEmpty V
⊢ G.chromaticNumber = 1 ↔ G = ⊥ ∧ Nonempty V

Tactic:
rw [eq_iff_le_not_lt, Order.lt_one_iff_nonpos, ← not_isEmpty_iff, ← Nat.cast_one, ← Nat.cast_zero,
    chromaticNumber_le_iff_colorable, chromaticNumber_le_iff_colorable, colorable_one_iff,
    colorable_zero_iff]

Premises used: SimpleGraph.chromaticNumber_le_iff_colorable, not_isEmpty_iff, eq_iff_le_not_lt, Nat.cast_zero, SimpleGraph.colorable_one_iff, Nat.cast_one, SimpleGraph.colorable_zero_iff, Order.lt_one_iff_nonpos
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring
Goal:
V : Type u
G : SimpleGraph V
⊢ 2 ≤ G.chromaticNumber ↔ G ≠ ⊥

Tactic:
⟨fun h ↦ ?_, fun h ↦ ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring
Goal:
V : Type u
G : SimpleGraph V
refine_1 : ∀ (h : 2 ≤ G.chromaticNumber), G ≠ ⊥
refine_2 : ∀ (h : G ≠ ⊥), 2 ≤ G.chromaticNumber
⊢ 2 ≤ G.chromaticNumber ↔ G ≠ ⊥

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring
Goal:
V : Type u
G : SimpleGraph V
h : 2 ≤ G.chromaticNumber
refine_1 : ∀ (h : G = ⊥), G.chromaticNumber < 2
⊢ G ≠ ⊥

Tactic:
contrapose! h
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring
Goal:
V : Type u
G : SimpleGraph V
h : G = ⊥
pos : ∀ (h' : IsEmpty V), G.chromaticNumber < 2
neg : ∀ (h' : ¬IsEmpty V), G.chromaticNumber < 2
⊢ G.chromaticNumber < 2

Tactic:
by_cases h' : IsEmpty V

Premises used: IsEmpty
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring
Goal:
V : Type u
G : SimpleGraph V
h : G = ⊥
h' : IsEmpty V
⊢ G.chromaticNumber < 2

Tactic:
simp [chromaticNumber_eq_zero_of_isEmpty]

Premises used: SimpleGraph.chromaticNumber_eq_zero_of_isEmpty
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring
Goal:
V : Type u
G : SimpleGraph V
h : G = ⊥
h' : ¬IsEmpty V
⊢ Nonempty V

Tactic:
simpa using h'
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring
Goal:
V : Type u
G : SimpleGraph V
h : G = ⊥
h' : ¬IsEmpty V
⊢ G.chromaticNumber < 2

Tactic:
simp [chromaticNumber_eq_one_iff.mpr ⟨h, by simpa using h'⟩]

Premises used: Iff.mpr, And.intro, SimpleGraph.chromaticNumber_eq_one_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring
Goal:
V : Type u
G : SimpleGraph V
h : G ≠ ⊥
refine_2 : ∀ (w w_1 : V) (h : G.Adj w w_1), 2 ≤ G.chromaticNumber
⊢ 2 ≤ G.chromaticNumber

Tactic:
obtain ⟨_, _, h⟩ := ne_bot_iff_exists_adj.mp h

Premises used: SimpleGraph.ne_bot_iff_exists_adj, Iff.mp
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring
Goal:
V : Type u
G : SimpleGraph V
h_1 : G ≠ ⊥
w w_1 : V
h : G.Adj w w_1
⊢ 2 ≤ G.chromaticNumber

Tactic:
two_le_chromaticNumber_of_adj h

Premises used: SimpleGraph.two_le_chromaticNumber_of_adj
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring
Goal:
V : Type u
G : SimpleGraph V
h_1 : G ≠ ⊥
w w_1 : V
h : G.Adj w w_1
⊢ 2 ≤ G.chromaticNumber

Tactic:
exact two_le_chromaticNumber_of_adj h

Premises used: SimpleGraph.two_le_chromaticNumber_of_adj
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring
Goal:
V_1 : Type u
G : SimpleGraph V_1
n : ℕ
ι : Type u_1
α : Type u_2
β : Type u_3
C : G.Coloring α
V : Type u_4
W : Type u_5
v w : V ⊕ W
inl :
  ∀ (val : V),
    (completeBipartiteGraph V W).Adj (Sum.inl val) w →
      Ne (α := Bool) ((fun (v : V ⊕ W) ↦ v.isRight) (Sum.inl val)) ((fun (v : V ⊕ W) ↦ v.isRight) w)
inr :
  ∀ (val : W),
    (completeBipartiteGraph V W).Adj (Sum.inr val) w →
      Ne (α := Bool) ((fun (v : V ⊕ W) ↦ v.isRight) (Sum.inr val)) ((fun (v : V ⊕ W) ↦ v.isRight) w)
⊢ (completeBipartiteGraph V W).Adj v w →
    Ne (α := Bool) ((fun (v : V ⊕ W) ↦ v.isRight) v) ((fun (v : V ⊕ W) ↦ v.isRight) w)

Tactic:
cases v
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring
Goal:
V_1 : Type u
G : SimpleGraph V_1
n : ℕ
ι : Type u_1
α : Type u_2
β : Type u_3
C : G.Coloring α
V : Type u_4
W : Type u_5
w : V ⊕ W
val : V
inl :
  ∀ (val_1 : V),
    (completeBipartiteGraph V W).Adj (Sum.inl val) (Sum.inl val_1) →
      Ne (α := Bool) ((fun (v : V ⊕ W) ↦ v.isRight) (Sum.inl val)) ((fun (v : V ⊕ W) ↦ v.isRight) (Sum.inl val_1))
inl₁ :
  ∀ (val_1 : W),
    (completeBipartiteGraph V W).Adj (Sum.inl val) (Sum.inr val_1) →
      Ne (α := Bool) ((fun (v : V ⊕ W) ↦ v.isRight) (Sum.inl val)) ((fun (v : V ⊕ W) ↦ v.isRight) (Sum.inr val_1))
⊢ (completeBipartiteGraph V W).Adj (Sum.inl val) w →
    Ne (α := Bool) ((fun (v : V ⊕ W) ↦ v.isRight) (Sum.inl val)) ((fun (v : V ⊕ W) ↦ v.isRight) w)

Tactic:
cases w
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring
Goal:
V_1 : Type u
G : SimpleGraph V_1
n : ℕ
ι : Type u_1
α : Type u_2
β : Type u_3
C : G.Coloring α
V : Type u_4
W : Type u_5
w : V ⊕ W
val : W
inr :
  ∀ (val_1 : V),
    (completeBipartiteGraph V W).Adj (Sum.inr val) (Sum.inl val_1) →
      Ne (α := Bool) ((fun (v : V ⊕ W) ↦ v.isRight) (Sum.inr val)) ((fun (v : V ⊕ W) ↦ v.isRight) (Sum.inl val_1))
inr₁ :
  ∀ (val_1 : W),
    (completeBipartiteGraph V W).Adj (Sum.inr val) (Sum.inr val_1) →
      Ne (α := Bool) ((fun (v : V ⊕ W) ↦ v.isRight) (Sum.inr val)) ((fun (v : V ⊕ W) ↦ v.isRight) (Sum.inr val_1))
⊢ (completeBipartiteGraph V W).Adj (Sum.inr val) w →
    Ne (α := Bool) ((fun (v : V ⊕ W) ↦ v.isRight) (Sum.inr val)) ((fun (v : V ⊕ W) ↦ v.isRight) w)

Tactic:
cases w
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring
Goal:
V_1 : Type u
G : SimpleGraph V_1
n : ℕ
ι : Type u_1
α : Type u_2
β : Type u_3
C : G.Coloring α
V : Type u_4
W : Type u_5
val val_1 : V
⊢ (completeBipartiteGraph V W).Adj (Sum.inl val) (Sum.inl val_1) →
    Ne (α := Bool) ((fun (v : V ⊕ W) ↦ v.isRight) (Sum.inl val)) ((fun (v : V ⊕ W) ↦ v.isRight) (Sum.inl val_1))

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring
Goal:
V_1 : Type u
G : SimpleGraph V_1
n : ℕ
ι : Type u_1
α : Type u_2
β : Type u_3
C : G.Coloring α
V : Type u_4
W : Type u_5
val : V
val_1 : W
⊢ (completeBipartiteGraph V W).Adj (Sum.inl val) (Sum.inr val_1) →
    Ne (α := Bool) ((fun (v : V ⊕ W) ↦ v.isRight) (Sum.inl val)) ((fun (v : V ⊕ W) ↦ v.isRight) (Sum.inr val_1))

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring
Goal:
V_1 : Type u
G : SimpleGraph V_1
n : ℕ
ι : Type u_1
α : Type u_2
β : Type u_3
C : G.Coloring α
V : Type u_4
W : Type u_5
val : W
val_1 : V
⊢ (completeBipartiteGraph V W).Adj (Sum.inr val) (Sum.inl val_1) →
    Ne (α := Bool) ((fun (v : V ⊕ W) ↦ v.isRight) (Sum.inr val)) ((fun (v : V ⊕ W) ↦ v.isRight) (Sum.inl val_1))

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring
Goal:
V_1 : Type u
G : SimpleGraph V_1
n : ℕ
ι : Type u_1
α : Type u_2
β : Type u_3
C : G.Coloring α
V : Type u_4
W : Type u_5
val val_1 : W
⊢ (completeBipartiteGraph V W).Adj (Sum.inr val) (Sum.inr val_1) →
    Ne (α := Bool) ((fun (v : V ⊕ W) ↦ v.isRight) (Sum.inr val)) ((fun (v : V ⊕ W) ↦ v.isRight) (Sum.inr val_1))

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring
Goal:
V : Type u_4
W : Type u_5
inst : Nonempty V
inst_1 : Nonempty W
⊢ (completeBipartiteGraph V W).Colorable 2

Tactic:
simpa using (CompleteBipartiteGraph.bicoloring V W).colorable

Premises used: SimpleGraph.CompleteBipartiteGraph.bicoloring, SimpleGraph.Coloring.colorable
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring
Goal:
V : Type u_4
W : Type u_5
inst : Nonempty V
inst_1 : Nonempty W
rw :
  ∀ (C : (completeBipartiteGraph V W).Coloring (Fin 2)), Surjective (α := V ⊕ W) (β := Fin 2) (⇑C : (a : V ⊕ W) → Fin 2)
⊢ (completeBipartiteGraph V W).chromaticNumber = 2

Tactic:
rw [← Nat.cast_two, chromaticNumber_eq_iff_forall_surjective
    (by simpa using (CompleteBipartiteGraph.bicoloring V W).colorable)]

Premises used: SimpleGraph.chromaticNumber_eq_iff_forall_surjective, Nat.cast_two
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring
Goal:
V : Type u_4
W : Type u_5
inst : Nonempty V
inst_1 : Nonempty W
C : (completeBipartiteGraph V W).Coloring (Fin 2)
b : Fin 2
have : ∀ (v : V), ∃ (a : V ⊕ W), (C : (a : V ⊕ W) → Fin 2) a = b
⊢ ∃ (a : V ⊕ W), (C : (a : V ⊕ W) → Fin 2) a = b

Tactic:
have v := Classical.arbitrary V
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring
Goal:
V : Type u_4
W : Type u_5
inst : Nonempty V
inst_1 : Nonempty W
C : (completeBipartiteGraph V W).Coloring (Fin 2)
b : Fin 2
v : V
have : ∀ (w : W), ∃ (a : V ⊕ W), (C : (a : V ⊕ W) → Fin 2) a = b
⊢ ∃ (a : V ⊕ W), (C : (a : V ⊕ W) → Fin 2) a = b

Tactic:
have w := Classical.arbitrary W
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring
Goal:
V : Type u_4
W : Type u_5
inst : Nonempty V
inst_1 : Nonempty W
C : (completeBipartiteGraph V W).Coloring (Fin 2)
b : Fin 2
v : V
w : W
⊢ (completeBipartiteGraph V W).Adj (Sum.inl v) (Sum.inr w)

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring
Goal:
V : Type u_4
W : Type u_5
inst : Nonempty V
inst_1 : Nonempty W
C : (completeBipartiteGraph V W).Coloring (Fin 2)
b : Fin 2
v : V
w : W
⊢ (completeBipartiteGraph V W).Adj (Sum.inl v) (Sum.inr w)

Tactic:
have h : (completeBipartiteGraph V W).Adj (Sum.inl v) (Sum.inr w) := by simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring
Goal:
V : Type u_4
W : Type u_5
inst : Nonempty V
inst_1 : Nonempty W
C : (completeBipartiteGraph V W).Coloring (Fin 2)
b : Fin 2
v : V
w : W
h : (completeBipartiteGraph V W).Adj (Sum.inl v) (Sum.inr w)
pos : ∀ (he : (C : (a : V ⊕ W) → Fin 2) (Sum.inl v) = b), ∃ (a : V ⊕ W), (C : (a : V ⊕ W) → Fin 2) a = b
neg : ∀ (he : ¬(C : (a : V ⊕ W) → Fin 2) (Sum.inl v) = b), ∃ (a : V ⊕ W), (C : (a : V ⊕ W) → Fin 2) a = b
⊢ ∃ (a : V ⊕ W), (C : (a : V ⊕ W) → Fin 2) a = b

Tactic:
by_cases he : C (Sum.inl v) = b

Premises used: Sum.inl, DFunLike.coe
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring
Goal:
V : Type u_4
W : Type u_5
inst : Nonempty V
inst_1 : Nonempty W
C : (completeBipartiteGraph V W).Coloring (Fin 2)
b : Fin 2
v : V
w : W
h : (completeBipartiteGraph V W).Adj (Sum.inl v) (Sum.inr w)
he : (C : (a : V ⊕ W) → Fin 2) (Sum.inl v) = b
⊢ ∃ (a : V ⊕ W), (C : (a : V ⊕ W) → Fin 2) a = b

Tactic:
⟨_, he⟩

Premises used: Exists.intro