awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring
Goal:
V : Type u
G : SimpleGraph V
n : ℕ
ι : Type u_1
α : Type u_2
β : Type u_3
C_1 : G.Coloring α
inst : Nonempty (G.Coloring α)
inst_1 : Infinite α
inst_2 : Nonempty V
C : G.Coloring α
v : V
f : (c : α) → G →g completeGraph α :=
  fun (c : α) ↦ Hom.comp (Iso.toHom (Iso.completeGraph (Equiv.swap ((C : (a : V) → α) v) c))) C
a b : α
h : f a = f b
⊢ (f a).toFun (r := G.Adj) (s := (completeGraph α).Adj) v = (f b).toFun (r := G.Adj) (s := (completeGraph α).Adj) v

Tactic:
have := congrFun (congrArg RelHom.toFun h) v
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring
Goal:
V : Type u
G : SimpleGraph V
n : ℕ
ι : Type u_1
α : Type u_2
β : Type u_3
C_1 : G.Coloring α
inst : Nonempty (G.Coloring α)
inst_1 : Infinite α
inst_2 : Nonempty V
C : G.Coloring α
v : V
f : (c : α) → G →g completeGraph α :=
  fun (c : α) ↦ Hom.comp (Iso.toHom (Iso.completeGraph (Equiv.swap ((C : (a : V) → α) v) c))) C
a b : α
h : f a = f b
this :
  Eq.{u_2 + 1} (α := α)
    (((Equiv.swap ((C : (a : V) → α) v) a : Equiv.Perm α) : (a : α) → α) ((C : (a : V) → α) v : α) : α)
    (((Equiv.swap ((C : (a : V) → α) v) b : Equiv.Perm α) : (a : α) → α) ((C : (a : V) → α) v : α) : α)
⊢ a = b

Tactic:
grind
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring
Goal:
V : Type u
G : SimpleGraph V
n : ℕ
ι : Type u_1
α : Type u_2
β : Type u_3
C : G.Coloring α
inst : Nonempty (G.Coloring α)
inst_1 : Infinite α
inst_2 : Nonempty V
have have₁ have₂ : ∀ (C : G.Coloring α), Infinite (G.Coloring α)
have₃ have₄ : ∀ (C : G.Coloring α) (v : V), Infinite (G.Coloring α)
have₅ :
  ∀ (C : G.Coloring α) (v : V),
    let f : (c : α) → G →g completeGraph α := fun (c : α) ↦
      Hom.comp (Iso.toHom (Iso.completeGraph (Equiv.swap ((C : (a : V) → α) v) c))) C;
    ∀ (a b : α) (h : f a = f b), a = b
have₆ :
  ∀ (C : G.Coloring α) (v : V),
    let f : (c : α) → G →g completeGraph α := fun (c : α) ↦
      Hom.comp (Iso.toHom (Iso.completeGraph (Equiv.swap ((C : (a : V) → α) v) c))) C;
    ∀ (a b : α) (h : f a = f b)
      (this :
        (f a).toFun (r := G.Adj) (s := (completeGraph α).Adj) v =
          (f b).toFun (r := G.Adj) (s := (completeGraph α).Adj) v),
      a = b
have₇ :
  ∀ (C : G.Coloring α) (v : V),
    let f : (c : α) → G →g completeGraph α := fun (c : α) ↦
      Hom.comp (Iso.toHom (Iso.completeGraph (Equiv.swap ((C : (a : V) → α) v) c))) C;
    ∀ (a b : α) (h : f a = f b)
      (this :
        Eq.{u_2 + 1} (α := α)
          (((Equiv.swap ((C : (a : V) → α) v) a : Equiv.Perm α) : (a : α) → α) ((C : (a : V) → α) v : α) : α)
          (((Equiv.swap ((C : (a : V) → α) v) b : Equiv.Perm α) : (a : α) → α) ((C : (a : V) → α) v : α) : α)),
      a = b
⊢ Infinite (G.Coloring α)

Tactic:
classical
  have ⟨C⟩ := ‹Nonempty <| G.Coloring α›
  have ⟨v⟩ := ‹Nonempty V›
  let f c := (Iso.completeGraph <| Equiv.swap (C v) c).toHom.comp C
  refine Infinite.of_injective f fun a b h ↦ ?_
  have := congrFun (congrArg RelHom.toFun h) v
  dsimp [f, Iso.completeGraph] at this
  grind

Premises used: SimpleGraph.Iso.completeGraph
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring
Goal:
V : Type u
G : SimpleGraph V
inst : IsEmpty V
n : ℕ
⊢ G.Colorable n

Tactic:
⟨.ofIsEmpty⟩

Premises used: SimpleGraph.Coloring.ofIsEmpty, Nonempty.intro, SimpleGraph.Colorable
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring
Goal:
V : Type u
G : SimpleGraph V
⊢ G.Colorable 0 ↔ IsEmpty V

Tactic:
⟨fun ⟨C⟩ ↦ Function.isEmpty C, fun _ ↦ .of_isEmpty 0⟩

Premises used: Function.isEmpty, SimpleGraph.Colorable.of_isEmpty, IsEmpty, Iff.intro, OfNat.ofNat, _private.0.SimpleGraph.colorable_zero_iff.match_1, DFunLike.coe
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring
Goal:
V : Type u
G : SimpleGraph V
h : G = ⊥
⊢ ∀ {a b : V}, Adj ⊥ a b → Adj (V := Fin 1) (completeGraph (Fin 1)) (0 a) (0 b)

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring
Goal:
V : Type u
G : SimpleGraph V
refine : G.Colorable 1 → ∀ (C : G.Coloring (Fin 1)) (u v : V) (h : G.Adj u v), False
⊢ G.Colorable 1 ↔ G = ⊥

Tactic:
refine ⟨fun ⟨C⟩ ↦ eq_bot_iff_forall_not_adj.mpr fun u v h ↦ ?_, fun h ↦ h ▸ ⟨0, by simp⟩⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring
Goal:
V : Type u
G : SimpleGraph V
h_1 : G.Colorable 1
C : G.Coloring (Fin 1)
u v : V
h : G.Adj u v
⊢ False

Tactic:
C.map_rel h <| Subsingleton.elim ..

Premises used: RelHom.map_rel, Subsingleton.elim
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring
Goal:
V : Type u
G : SimpleGraph V
h_1 : G.Colorable 1
C : G.Coloring (Fin 1)
u v : V
h : G.Adj u v
⊢ False

Tactic:
exact C.map_rel h <| Subsingleton.elim ..

Premises used: RelHom.map_rel, Subsingleton.elim
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring
Goal:
V : Type u
G : SimpleGraph V
n : ℕ
β : Type u_3
f : V ↪ β
inst : NeZero n
hc : G.Colorable n
obtain : ∀ (C : G.Coloring (Fin n)), Colorable.{u_3} (V := β) (SimpleGraph.map (⇑f : (a : V) → β) G) n
⊢ Colorable.{u_3} (V := β) (SimpleGraph.map (⇑f : (a : V) → β) G) n

Tactic:
obtain ⟨C⟩ := hc
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring
Goal:
V : Type u
G : SimpleGraph V
n : ℕ
β : Type u_3
f : V ↪ β
inst : NeZero n
C : G.Coloring (Fin n)
map_rel' :
  ∀ {a b : β},
    Adj (SimpleGraph.map (⇑f : (a : V) → β) G) a b →
      Adj (V := Fin n) (completeGraph (Fin n))
        (extend (α := V) (⇑f : (a : V) → β) (⇑C : (a : V) → Fin n) (const β default) a)
        (extend (α := V) (⇑f : (a : V) → β) (⇑C : (a : V) → Fin n) (const β default) b)
⊢ Colorable.{u_3} (V := β) (SimpleGraph.map (⇑f : (a : V) → β) G) n

Tactic:
use extend f C (const β default)

Premises used: Inhabited.default, Function.extend, Function.const, DFunLike.coe
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring
Goal:
V : Type u
G : SimpleGraph V
n : ℕ
β : Type u_3
f : V ↪ β
inst : NeZero n
C : G.Coloring (Fin n)
a b : β
map_rel' :
  a ≠ b →
    ∀ (w w_1 : V) (hadj : G.Adj w w_1) (ha : (f : (a : V) → β) w = a) (hb : (f : (a : V) → β) w_1 = b),
      Adj (V := Fin n) (completeGraph (Fin n))
        (extend (α := V) (⇑f : (a : V) → β) (⇑C : (a : V) → Fin n) (const β default) a)
        (extend (α := V) (⇑f : (a : V) → β) (⇑C : (a : V) → Fin n) (const β default) b)
⊢ Adj (SimpleGraph.map (⇑f : (a : V) → β) G) a b →
    Adj (V := Fin n) (completeGraph (Fin n))
      (extend (α := V) (⇑f : (a : V) → β) (⇑C : (a : V) → Fin n) (const β default) a)
      (extend (α := V) (⇑f : (a : V) → β) (⇑C : (a : V) → Fin n) (const β default) b)

Tactic:
⟨_, _, _, hadj, ha, hb⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring
Goal:
V : Type u
G : SimpleGraph V
n : ℕ
β : Type u_3
f : V ↪ β
inst : NeZero n
C : G.Coloring (Fin n)
a b : β
left : a ≠ b
w w_1 : V
hadj : G.Adj w w_1
ha : (f : (a : V) → β) w = a
hb : (f : (a : V) → β) w_1 = b
map_rel' :
  Adj (V := Fin n) (completeGraph (Fin n) : SimpleGraph (Fin n)) ((C : (a : V) → Fin n) w : Fin n)
    ((C : (a : V) → Fin n) w_1 : Fin n)
⊢ Adj (V := Fin n) (completeGraph (Fin n))
    (extend (α := V) (⇑f : (a : V) → β) (⇑C : (a : V) → Fin n) (const β default) a)
    (extend (α := V) (⇑f : (a : V) → β) (⇑C : (a : V) → Fin n) (const β default) b)

Tactic:
rw [← ha, f.injective.extend_apply, ← hb, f.injective.extend_apply]

Premises used: Function.Injective.extend_apply, Function.Embedding.injective
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring
Goal:
V : Type u
G : SimpleGraph V
n : ℕ
β : Type u_3
f : V ↪ β
inst : NeZero n
C : G.Coloring (Fin n)
a b : β
left : a ≠ b
w w_1 : V
hadj : G.Adj w w_1
ha : (f : (a : V) → β) w = a
hb : (f : (a : V) → β) w_1 = b
⊢ Adj (V := Fin n) (completeGraph (Fin n) : SimpleGraph (Fin n)) ((C : (a : V) → Fin n) w : Fin n)
    ((C : (a : V) → Fin n) w_1 : Fin n)

Tactic:
C.valid hadj

Premises used: SimpleGraph.Coloring.valid, Not
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring
Goal:
V : Type u
G : SimpleGraph V
n : ℕ
β : Type u_3
f : V ↪ β
inst : NeZero n
C : G.Coloring (Fin n)
a b : β
left : a ≠ b
w w_1 : V
hadj : G.Adj w w_1
ha : (f : (a : V) → β) w = a
hb : (f : (a : V) → β) w_1 = b
⊢ Adj (V := Fin n) (completeGraph (Fin n) : SimpleGraph (Fin n)) ((C : (a : V) → Fin n) w : Fin n)
    ((C : (a : V) → Fin n) w_1 : Fin n)

Tactic:
exact C.valid hadj

Premises used: SimpleGraph.Coloring.valid
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring
Goal:
V : Type u
G : SimpleGraph V
n : ℕ
ι : Type u_1
hG : G.Colorable n
f : ι → V
hf : Pairwise fun (i j : ι) ↦ G.Adj (f i) (f j)
obtain : ∀ (C : G.Coloring (Fin n)), Nat.card ι ≤ n
⊢ Nat.card ι ≤ n

Tactic:
obtain ⟨C⟩ := hG
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring
Goal:
V : Type u
G : SimpleGraph V
n : ℕ
ι : Type u_1
f : ι → V
hf : Pairwise fun (i j : ι) ↦ G.Adj (f i) (f j)
C : G.Coloring (Fin n)
⊢ Nat.card ι ≤ n

Tactic:
simpa using Nat.card_le_card_of_injective _ (C.injective_comp_of_pairwise_adj f hf)

Premises used: Nat.card_le_card_of_injective, SimpleGraph.Coloring.injective_comp_of_pairwise_adj
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring
Goal:
V : Type u
G : SimpleGraph V
n : ℕ
⊢ (↑n : ℕ∞) ≤ G.chromaticNumber ↔ ∀ (m : ℕ), G.Colorable m → n ≤ m

Tactic:
simp [chromaticNumber]

Premises used: SimpleGraph.chromaticNumber
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring
Goal:
V : Type u
G : SimpleGraph V
n : ℕ
⊢ (↑n : ℕ∞) ≤ G.chromaticNumber ↔ ∀ (m : ℕ) (a : G.Coloring (Fin m)), n ≤ m

Tactic:
simp [le_chromaticNumber_iff_colorable, Colorable]

Premises used: SimpleGraph.le_chromaticNumber_iff_colorable, SimpleGraph.Colorable
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring
Goal:
V : Type u
G : SimpleGraph V
n : ℕ
ι : Type u_1
hn : n ≤ Nat.card ι
f : ι → V
hf : Pairwise fun (i j : ι) ↦ G.Adj (f i) (f j)
⊢ (↑n : ℕ∞) ≤ G.chromaticNumber

Tactic:
le_chromaticNumber_iff_colorable.2 fun _m hm ↦ hn.trans <| hm.card_le_of_pairwise_adj f hf

Premises used: Iff.mpr, SimpleGraph.le_chromaticNumber_iff_colorable, SimpleGraph.Colorable.card_le_of_pairwise_adj, LE.le.trans
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring
Goal:
V : Type u
G : SimpleGraph V
⊢ G.chromaticNumber = ⨅ n ∈ setOf G.Colorable, (↑n : ℕ∞)

Tactic:
rfl

Premises used: SimpleGraph.chromaticNumber, rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring
Goal:
V : Type u
G : SimpleGraph V
rw : Eq (α := ℕ∞) (⨅ n ∈ setOf G.Colorable, (↑n : ℕ∞)) (⨅ (n : (↑{m : ℕ | G.Colorable m} : Type)), (↑(↑n : ℕ) : ℕ∞))
rw₁ rw₂ :
  Eq (α := ℕ∞) (⨅ n ∈ setOf G.Colorable, (↑n : ℕ∞))
    (⨅ (i : ℕ),
      ⨅ (h : Membership.mem (γ := Set ℕ) {m : ℕ | G.Colorable m} i),
        (↑(↑(Subtype.mk (p := fun (x : ℕ) ↦ Membership.mem (γ := Set ℕ) {m : ℕ | G.Colorable m} x) i h) : ℕ) : ℕ∞))
⊢ G.chromaticNumber = ⨅ (n : (↑{m : ℕ | G.Colorable m} : Type)), (↑(↑n : ℕ) : ℕ∞)

Tactic:
rw [chromaticNumber, iInf_subtype]

Premises used: iInf_subtype, SimpleGraph.chromaticNumber
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring
Goal:
V : Type u
G : SimpleGraph V
n : ℕ
h : G.Colorable n
rw : Set.Nonempty (α := ℕ) {n' : ℕ | G.Colorable n'}
⊢ G.chromaticNumber = (↑(sInf {n' : ℕ | G.Colorable n'}) : ℕ∞)

Tactic:
rw [ENat.coe_sInf, chromaticNumber]

Premises used: ENat.coe_sInf, SimpleGraph.chromaticNumber
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring
Goal:
V : Type u
G : SimpleGraph V
n : ℕ
h : G.Colorable n
⊢ Set.Nonempty (α := ℕ) {n' : ℕ | G.Colorable n'}

Tactic:
⟨_, h⟩

Premises used: Set.Nonempty, Exists.intro
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring
Goal:
V : Type u
G : SimpleGraph V
n : ℕ
h : G.Colorable n
⊢ Set.Nonempty (α := ℕ) {n' : ℕ | G.Colorable n'}

Tactic:
exact ⟨_, h⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring
Goal:
V : Type u
G : SimpleGraph V
α : Type u_2
β : Type u_3
f : α ↪ β
⊢ Eq (α := (a : G.Coloring α) → G.Coloring β) (⇑(G.recolorOfEmbedding f) : (a : G.Coloring α) → G.Coloring β)
    (Embedding.completeGraph f).toHom.comp

Tactic:
rfl

Premises used: RelHom.comp, rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring
Goal:
V : Type u
G : SimpleGraph V
n : ℕ
ι : Type u_1
α_1 : Type u_2
β_1 : Type u_3
C_1 : G.Coloring α_1
α : Type u_4
β : Type u_5
f : α ≃ β
C : G.Coloring α
h :
  ∀ (v : V),
    Eq.{u_4 + 1} (α := α)
      ((((G.recolorOfEmbedding f.symm.toEmbedding : (a : G.Coloring β) → G.Coloring α)
                ((G.recolorOfEmbedding f.toEmbedding : (a : G.Coloring α) → G.Coloring β) C) :
              G.Coloring α) :
            (a : V) → α)
          v :
        α)
      ((C : (a : V) → α) v : α)
⊢ (G.recolorOfEmbedding f.symm.toEmbedding : (a : G.Coloring β) → G.Coloring α)
      ((G.recolorOfEmbedding f.toEmbedding : (a : G.Coloring α) → G.Coloring β) C) =
    C

Tactic:
ext v
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring
Goal:
V : Type u
G : SimpleGraph V
n : ℕ
ι : Type u_1
α_1 : Type u_2
β_1 : Type u_3
C_1 : G.Coloring α_1
α : Type u_4
β : Type u_5
f : α ≃ β
C : G.Coloring α
v : V
⊢ Eq.{u_4 + 1} (α := α)
    ((((G.recolorOfEmbedding f.symm.toEmbedding : (a : G.Coloring β) → G.Coloring α)
              ((G.recolorOfEmbedding f.toEmbedding : (a : G.Coloring α) → G.Coloring β) C) :
            G.Coloring α) :
          (a : V) → α)
        v :
      α)
    ((C : (a : V) → α) v : α)

Tactic:
apply Equiv.symm_apply_apply

Premises used: Equiv.symm_apply_apply
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring
Goal:
V : Type u
G : SimpleGraph V
n : ℕ
ι : Type u_1
α_1 : Type u_2
β_1 : Type u_3
C_1 : G.Coloring α_1
α : Type u_4
β : Type u_5
f : α ≃ β
C : G.Coloring β
h :
  ∀ (v : V),
    Eq.{u_5 + 1} (α := β)
      ((((G.recolorOfEmbedding f.toEmbedding : (a : G.Coloring α) → G.Coloring β)
                ((G.recolorOfEmbedding f.symm.toEmbedding : (a : G.Coloring β) → G.Coloring α) C) :
              G.Coloring β) :
            (a : V) → β)
          v :
        β)
      ((C : (a : V) → β) v : β)
⊢ (G.recolorOfEmbedding f.toEmbedding : (a : G.Coloring α) → G.Coloring β)
      ((G.recolorOfEmbedding f.symm.toEmbedding : (a : G.Coloring β) → G.Coloring α) C) =
    C

Tactic:
ext v
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring
Goal:
V : Type u
G : SimpleGraph V
n : ℕ
ι : Type u_1
α_1 : Type u_2
β_1 : Type u_3
C_1 : G.Coloring α_1
α : Type u_4
β : Type u_5
f : α ≃ β
C : G.Coloring β
v : V
⊢ Eq.{u_5 + 1} (α := β)
    ((((G.recolorOfEmbedding f.toEmbedding : (a : G.Coloring α) → G.Coloring β)
              ((G.recolorOfEmbedding f.symm.toEmbedding : (a : G.Coloring β) → G.Coloring α) C) :
            G.Coloring β) :
          (a : V) → β)
        v :
      β)
    ((C : (a : V) → β) v : β)

Tactic:
apply Equiv.apply_symm_apply

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring
Goal:
V : Type u
G : SimpleGraph V
α : Type u_2
β : Type u_3
f : α ≃ β
⊢ Eq (α := (a : G.Coloring α) → G.Coloring β) (⇑(G.recolorOfEquiv f) : (a : G.Coloring α) → G.Coloring β)
    (Embedding.completeGraph f.toEmbedding).toHom.comp

Tactic:
rfl

Premises used: RelHom.comp, rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring
Goal:
V : Type u
G : SimpleGraph V
α : Type u_2
β : Type u_3
inst : Fintype α
inst_1 : Fintype β
hαβ : card α ≤ card β
⊢ Eq (α := (a : G.Coloring α) → G.Coloring β) (⇑(G.recolorOfCardLE hαβ) : (a : G.Coloring α) → G.Coloring β)
    (Embedding.completeGraph ⋯.some).toHom.comp

Tactic:
rfl

Premises used: RelHom.comp, rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring
Goal:
V : Type u
G : SimpleGraph V
n m : ℕ
h : n ≤ m
hc : G.Colorable n
⊢ card (Fin n) ≤ card (Fin m)

Tactic:
simp [h]
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring
Goal:
V : Type u
G : SimpleGraph V
α : Type u_2
inst : Fintype α
C : G.Coloring α
⊢ card α ≤ card (Fin (card α))

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring
Goal:
V : Type u
G : SimpleGraph V
inst : Fintype V
⊢ G.Colorable (card V)

Tactic:
G.selfColoring.colorable

Premises used: SimpleGraph.selfColoring, SimpleGraph.Coloring.colorable
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring
Goal:
V : Type u
G : SimpleGraph V
n_1 : ℕ
ι : Type u_1
α : Type u_2
β : Type u_3
C : G.Coloring α
inst : Fintype α
n : ℕ
hc : G.Colorable n
hn : n ≤ card α
⊢ card (Fin n) ≤ card α

Tactic:
rw [← Fintype.card_fin n] at hn

Premises used: Fintype.card_fin
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring
Goal:
V : Type u
G : SimpleGraph V
n_1 : ℕ
ι : Type u_1
α : Type u_2
β : Type u_3
C : G.Coloring α
inst : Fintype α
n : ℕ
hc : G.Colorable n
hn : card (Fin n) ≤ card α
⊢ G.Coloring α

Tactic:
exact G.recolorOfCardLE hn hc.some

Premises used: SimpleGraph.recolorOfCardLE, Nonempty.some, DFunLike.coe
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring
Goal:
V : Type u
G : SimpleGraph V
V' : Type u_4
G' : SimpleGraph V'
f : G →g G'
n : ℕ
h : G'.Colorable n
⊢ n ≤ card (Fin n)

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring
Goal:
V : Type u
G : SimpleGraph V
n : ℕ
mp : G.Colorable n → ∃ (C : G.Coloring ℕ), ∀ (v : V), (C : (a : V) → ℕ) v < n
mpr : (∃ (C : G.Coloring ℕ), ∀ (v : V), (C : (a : V) → ℕ) v < n) → G.Colorable n
⊢ G.Colorable n ↔ ∃ (C : G.Coloring ℕ), ∀ (v : V), (C : (a : V) → ℕ) v < n

Tactic:
constructor
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring
Goal:
V : Type u
G : SimpleGraph V
n : ℕ
hc : G.Colorable n
⊢ n ≤ card (Fin n)

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring
Goal:
V : Type u
G : SimpleGraph V
n : ℕ
hc : G.Colorable n
mp : ∀ (C : G.Coloring (Fin n)), ∃ (C : G.Coloring ℕ), ∀ (v : V), (C : (a : V) → ℕ) v < n
⊢ ∃ (C : G.Coloring ℕ), ∀ (v : V), (C : (a : V) → ℕ) v < n

Tactic:
have C : G.Coloring (Fin n) := hc.toColoring (by simp)
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring
Goal:
V : Type u
G : SimpleGraph V
n : ℕ
hc : G.Colorable n
C : G.Coloring (Fin n)
f : Embedding (V := Fin n) (completeGraph (Fin n)) (completeGraph ℕ) := Embedding.completeGraph Fin.valEmbedding
h : ∀ (v : V), (f.toHom.comp C : (a : V) → ℕ) v < n
⊢ ∃ (C : G.Coloring ℕ), ∀ (v : V), (C : (a : V) → ℕ) v < n

Tactic:
use f.toHom.comp C

Premises used: SimpleGraph.Embedding.toHom, SimpleGraph.Hom.comp
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring
Goal:
V : Type u
G : SimpleGraph V
n : ℕ
hc : G.Colorable n
C : G.Coloring (Fin n)
f : Embedding (V := Fin n) (completeGraph (Fin n)) (completeGraph ℕ) := Embedding.completeGraph Fin.valEmbedding
v : V
⊢ (f.toHom.comp C : (a : V) → ℕ) v < n

Tactic:
Fin.is_lt (C.1 v)

Premises used: Fin.is_lt, RelHom.toFun
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring
Goal:
V : Type u
G : SimpleGraph V
n : ℕ
hc : G.Colorable n
C : G.Coloring (Fin n)
f : Embedding (V := Fin n) (completeGraph (Fin n)) (completeGraph ℕ) := Embedding.completeGraph Fin.valEmbedding
v : V
⊢ (f.toHom.comp C : (a : V) → ℕ) v < n

Tactic:
exact Fin.is_lt (C.1 v)

Premises used: Fin.is_lt, RelHom.toFun
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring
Goal:
V : Type u
G : SimpleGraph V
n : ℕ
C : G.Coloring ℕ
Cf : ∀ (v : V), (C : (a : V) → ℕ) v < n
⊢ G.Colorable n

Tactic:
⟨Coloring.mk ?_ ?_⟩

Premises used: SimpleGraph.Coloring.mk, Nonempty.intro, SimpleGraph.Colorable
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring
Goal:
V : Type u
G : SimpleGraph V
n : ℕ
C : G.Coloring ℕ
Cf : ∀ (v : V), (C : (a : V) → ℕ) v < n
mpr : V → Fin n
mpr₁ : ∀ {v w : V}, G.Adj v w → (⟨(C : (a : V) → ℕ) v, ⋯⟩ : Fin n) ≠ ⟨(C : (a : V) → ℕ) w, ⋯⟩
⊢ G.Colorable n

Tactic:
refine ⟨Coloring.mk ?_ ?_⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring
Goal:
V : Type u
G : SimpleGraph V
n : ℕ
C : G.Coloring ℕ
Cf : ∀ (v : V), (C : (a : V) → ℕ) v < n
⊢ V → Fin n

Tactic:
exact fun v => ⟨C v, Cf v⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring
Goal:
V : Type u
G : SimpleGraph V
n : ℕ
C : G.Coloring ℕ
Cf : ∀ (v : V), (C : (a : V) → ℕ) v < n
v w : V
hvw : G.Adj v w
mpr : ¬Eq (α := ℕ) ((C : (a : V) → ℕ) v : ℕ) ((C : (a : V) → ℕ) w : ℕ)
⊢ (⟨(C : (a : V) → ℕ) v, ⋯⟩ : Fin n) ≠ ⟨(C : (a : V) → ℕ) w, ⋯⟩

Tactic:
simp only [Fin.mk_eq_mk, Ne]

Premises used: Ne, Fin.mk_eq_mk
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring
Goal:
V : Type u
G : SimpleGraph V
n : ℕ
C : G.Coloring ℕ
Cf : ∀ (v : V), (C : (a : V) → ℕ) v < n
v w : V
hvw : G.Adj v w
⊢ ¬Eq (α := ℕ) ((C : (a : V) → ℕ) v : ℕ) ((C : (a : V) → ℕ) w : ℕ)

Tactic:
C.valid hvw

Premises used: SimpleGraph.Coloring.valid
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring
Goal:
V : Type u
G : SimpleGraph V
n : ℕ
C : G.Coloring ℕ
Cf : ∀ (v : V), (C : (a : V) → ℕ) v < n
v w : V
hvw : G.Adj v w
⊢ ¬Eq (α := ℕ) ((C : (a : V) → ℕ) v : ℕ) ((C : (a : V) → ℕ) w : ℕ)

Tactic:
exact C.valid hvw

Premises used: SimpleGraph.Coloring.valid
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring
Goal:
V : Type u
G : SimpleGraph V
n : ℕ
⊢ G.Colorable n ↔ ∀ (c : G.ConnectedComponent), c.toSimpleGraph.Colorable n

Tactic:
⟨fun ⟨C⟩ _ ↦ ⟨fun v ↦ C v, fun h h1 ↦ C.valid h h1⟩,
   fun h ↦ ⟨G.homOfConnectedComponents (fun c ↦ (h c).some)⟩⟩

Premises used: Nonempty.some, SimpleGraph.ConnectedComponent.toSimpleGraph, Nonempty.intro, SimpleGraph.Coloring.valid, Iff.intro, _private.0.SimpleGraph.colorable_iff_forall_connectedComponents.match_1, RelHom.mk, SimpleGraph.Colorable, Subtype.val, SimpleGraph.homOfConnectedComponents, DFunLike.coe
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring
Goal:
V : Type u
G : SimpleGraph V
n : ℕ
hc : G.Colorable n
⊢ Set.Nonempty (α := ℕ) {n : ℕ | G.Colorable n}

Tactic:
⟨n, hc⟩

Premises used: Set.Nonempty, Exists.intro
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring
Goal:
V : Type u
G : SimpleGraph V
⊢ BddBelow (α := ℕ) {n : ℕ | G.Colorable n}

Tactic:
⟨0, fun _ _ => zero_le⟩

Premises used: zero_le, Set.Nonempty, BddBelow, Exists.intro, OfNat.ofNat
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring
Goal:
V : Type u
G : SimpleGraph V
n : ℕ
hc : G.Colorable n
rw : LE.le (α := ℕ∞) (↑(sInf {n' : ℕ | G.Colorable n'}) : ℕ∞) (↑n : ℕ∞)
⊢ G.chromaticNumber ≤ (↑n : ℕ∞)

Tactic:
rw [hc.chromaticNumber_eq_sInf]

Premises used: SimpleGraph.Colorable.chromaticNumber_eq_sInf
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring
Goal:
V : Type u
G : SimpleGraph V
n : ℕ
hc : G.Colorable n
norm_cast : sInf {n' : ℕ | G.Colorable n'} ≤ n
⊢ LE.le (α := ℕ∞) (↑(sInf {n' : ℕ | G.Colorable n'}) : ℕ∞) (↑n : ℕ∞)

Tactic:
norm_cast
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring
Goal:
V : Type u
G : SimpleGraph V
n : ℕ
hc : G.Colorable n
apply : Membership.mem (γ := Set ℕ) {n : ℕ | G.Colorable n} n
⊢ sInf {n' : ℕ | G.Colorable n'} ≤ n

Tactic:
apply csInf_le chromaticNumber_bddBelow

Premises used: csInf_le, SimpleGraph.chromaticNumber_bddBelow
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring
Goal:
V : Type u
G : SimpleGraph V
n : ℕ
hc : G.Colorable n
⊢ Membership.mem (γ := Set ℕ) {n : ℕ | G.Colorable n} n

Tactic:
hc

Premises used: Set.Mem, setOf, SimpleGraph.Colorable
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring
Goal:
V : Type u
G : SimpleGraph V
n : ℕ
hc : G.Colorable n
⊢ Membership.mem (γ := Set ℕ) {n : ℕ | G.Colorable n} n

Tactic:
exact hc
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring
Goal:
V : Type u
G : SimpleGraph V
⊢ Ne (α := ℕ∞) (⨅ n ∈ setOf G.Colorable, (↑n : ℕ∞)) ⊤ ↔ ∃ (n : ℕ), G.Colorable n

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring
Goal:
V : Type u
G : SimpleGraph V
n : ℕ
⊢ G.chromaticNumber ≤ (↑n : ℕ∞) ↔ G.Colorable n

Tactic:
⟨fun h ↦ ?_, Colorable.chromaticNumber_le⟩

Premises used: SimpleGraph.Colorable.chromaticNumber_le, Iff.intro
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring
Goal:
V : Type u
G : SimpleGraph V
n : ℕ
refine : ∀ (h : G.chromaticNumber ≤ (↑n : ℕ∞)), G.Colorable n
⊢ G.chromaticNumber ≤ (↑n : ℕ∞) ↔ G.Colorable n

Tactic:
refine ⟨fun h ↦ ?_, Colorable.chromaticNumber_le⟩