awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.EdgeLabeling
Goal:
V : Type u_1
V' : Type u_2
G : SimpleGraph V
G' : SimpleGraph V'
K : Type u_3
K' : Type u_4
C : G.EdgeLabeling K
f : G' ↪g G
x y : V'
h : G'.Adj x y
⊢ G.Adj ((f : (a : V') → V) x) ((f : (a : V') → V) y)

Tactic:
simpa
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.EdgeLabeling
Goal:
V : Type u_1
V' : Type u_2
G : SimpleGraph V
G' : SimpleGraph V'
K : Type u_3
C : G.EdgeLabeling K
f : G' ↪g G
x y : V'
h : G'.Adj x y
⊢ (C.pullback (RelEmbedding.toRelHom (r := G'.Adj) (s := G.Adj) f)).get x y h =
    C.get ((f : (a : V') → V) x) ((f : (a : V') → V) y) ⋯

Tactic:
rfl

Premises used: SimpleGraph.Hom.mapEdgeSet, Sym2.map, setOf, Prod.map, Quot.map, SimpleGraph.EdgeLabeling.pullback, Sym2.fromRel, rfl, SimpleGraph.EdgeLabeling.get
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.EdgeLabeling
Goal:
V : Type u_1
G : SimpleGraph V
K : Type u_3
K' : Type u_4
C : G.EdgeLabeling K
f : K → K'
e : (↑G.edgeSet : Type u_1)
⊢ C.compRight f e = f (C e)

Tactic:
rfl

Premises used: SimpleGraph.EdgeLabeling.compRight, rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.EdgeLabeling
Goal:
V : Type u_1
G : SimpleGraph V
K : Type u_3
K' : Type u_4
C : G.EdgeLabeling K
f : K → K'
x y : V
h : G.Adj x y
⊢ (C.compRight f).get x y h = f (C.get x y h)

Tactic:
rfl

Premises used: SimpleGraph.EdgeLabeling.compRight, rfl, SimpleGraph.EdgeLabeling.get
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.EdgeLabeling
Goal:
V : Type u_1
V' : Type u_2
G : SimpleGraph V
G' : SimpleGraph V'
K : Type u_3
K' : Type u_4
C : G.EdgeLabeling K
f : (x y : V) → G.Adj x y → K
f_symm : ∀ (x y : V) (H : G.Adj x y), f y x ⋯ = f x y H
e : Sym2 V
he : e ∈ G.edgeSet
revert : (he : e ∈ G.edgeSet) → K
⊢ K

Tactic:
revert he
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.EdgeLabeling
Goal:
V : Type u_1
V' : Type u_2
G : SimpleGraph V
G' : SimpleGraph V'
K : Type u_3
K' : Type u_4
C : G.EdgeLabeling K
f : (x y : V) → G.Adj x y → K
f_symm : ∀ (x y : V) (H : G.Adj x y), f y x ⋯ = f x y H
e : Sym2 V
refine : ∀ (a b : V), f a b ≍ f b a
⊢ (he : e ∈ G.edgeSet) → K

Tactic:
refine Sym2.hrec f (fun a b ↦ ?_) e
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.EdgeLabeling
Goal:
V : Type u_1
V' : Type u_2
G : SimpleGraph V
G' : SimpleGraph V'
K : Type u_3
K' : Type u_4
C : G.EdgeLabeling K
f : (x y : V) → G.Adj x y → K
f_symm : ∀ (x y : V) (H : G.Adj x y), f y x ⋯ = f x y H
e : Sym2 V
a b : V
⊢ G.Adj a b = G.Adj b a

Tactic:
simp [adj_comm]

Premises used: SimpleGraph.adj_comm
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.EdgeLabeling
Goal:
V : Type u_1
V' : Type u_2
G : SimpleGraph V
G' : SimpleGraph V'
K : Type u_3
K' : Type u_4
C : G.EdgeLabeling K
f : (x y : V) → G.Adj x y → K
f_symm : ∀ (x y : V) (H : G.Adj x y), f y x ⋯ = f x y H
e : Sym2 V
a b : V
apply : ∀ (a_1 : G.Adj a b) (a' : G.Adj b a), a_1 ≍ a' → f a b a_1 ≍ f b a a'
⊢ f a b ≍ f b a

Tactic:
apply Function.hfunext (by simp [adj_comm])

Premises used: Function.hfunext
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.EdgeLabeling
Goal:
V : Type u_1
V' : Type u_2
G : SimpleGraph V
G' : SimpleGraph V'
K : Type u_3
K' : Type u_4
C : G.EdgeLabeling K
f : (x y : V) → G.Adj x y → K
f_symm : ∀ (x y : V) (H : G.Adj x y), f y x ⋯ = f x y H
e : Sym2 V
a b : V
⊢ ∀ (a_1 : G.Adj a b) (a' : G.Adj b a), a_1 ≍ a' → f a b a_1 ≍ f b a a'

Tactic:
grind
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.EdgeLabeling
Goal:
V : Type u_1
G : SimpleGraph V
K : Type u_3
f : (x y : V) → G.Adj x y → K
f_symm : ∀ (x y : V) (H : G.Adj x y), f y x ⋯ = f x y H
x y : V
h : G.Adj x y
⊢ (mk f f_symm).get x y h = f x y h

Tactic:
rfl

Premises used: SimpleGraph.EdgeLabeling.mk, Sym2.hrec, rfl, SimpleGraph.EdgeLabeling.get
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.EdgeLabeling
Goal:
V : Type u_1
G : SimpleGraph V
K : Type u_3
C : G.EdgeLabeling K
k : K
x y : V
simp :
  (∃ (h : G.Adj x y), C (Subtype.mk (p := fun (x : Sym2 V) ↦ x ∈ G.edgeSet) s(x, y) ⋯) = k) ∧ ¬x = y ↔
    ∃ (H : G.Adj x y), C (Subtype.mk (p := fun (x : Sym2 V) ↦ x ∈ G.edgeSet) s(x, y) H) = k
⊢ Adj (fromEdgeSet {e : Sym2 V | ∃ (h : e ∈ G.edgeSet), C (Subtype.mk (p := fun (x : Sym2 V) ↦ x ∈ G.edgeSet) e h) = k})
      x y ↔
    ∃ (H : G.Adj x y), C (Subtype.mk (p := fun (x : Sym2 V) ↦ x ∈ G.edgeSet) s(x, y) H) = k

Tactic:
simp only [mem_edgeSet, fromEdgeSet_adj, Set.mem_setOf_eq, Ne.eq_def]

Premises used: SimpleGraph.fromEdgeSet_adj, Ne.eq_def, Set.mem_setOf_eq, SimpleGraph.mem_edgeSet
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.EdgeLabeling
Goal:
V : Type u_1
G : SimpleGraph V
K : Type u_3
C : G.EdgeLabeling K
k : K
x y : V
⊢ (∃ (h : G.Adj x y), C (Subtype.mk (p := fun (x : Sym2 V) ↦ x ∈ G.edgeSet) s(x, y) ⋯) = k) ∧ ¬x = y ↔
    ∃ (H : G.Adj x y), C (Subtype.mk (p := fun (x : Sym2 V) ↦ x ∈ G.edgeSet) s(x, y) H) = k

Tactic:
grind [Adj.ne]

Premises used: SimpleGraph.Adj.ne
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.EdgeLabeling
Goal:
V : Type u_1
G : SimpleGraph V
K : Type u_3
C : G.EdgeLabeling K
k : K
x y : V
⊢ (C.labelGraph k).Adj x y → G.Adj x y

Tactic:
grind [labelGraph_adj]

Premises used: SimpleGraph.EdgeLabeling.labelGraph_adj
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.EdgeLabeling
Goal:
V : Type u_1
G : SimpleGraph V
K : Type u_3
C : G.EdgeLabeling K
i : K
_ : ∀ ⦃j : K⦄, i ≠ j → (fun (k l : K) ↦ Disjoint (C.labelGraph k) (C.labelGraph l)) i j
⊢ ∀ ⦃j : K⦄, i ≠ j → (fun (k l : K) ↦ Disjoint (C.labelGraph k) (C.labelGraph l)) i j

Tactic:
_
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.EdgeLabeling
Goal:
V : Type u_1
G : SimpleGraph V
K : Type u_3
C : G.EdgeLabeling K
i j : K
h : i ≠ j
rw : ∀ (x y : V), (C.labelGraph i).Adj x y → ¬(C.labelGraph j).Adj x y
⊢ Disjoint (C.labelGraph i) (C.labelGraph j)

Tactic:
rw [disjoint_left]

Premises used: SimpleGraph.disjoint_left
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.EdgeLabeling
Goal:
V : Type u_1
G : SimpleGraph V
K : Type u_3
C : G.EdgeLabeling K
i j : K
h : i ≠ j
⊢ ∀ (x y : V), (C.labelGraph i).Adj x y → ¬(C.labelGraph j).Adj x y

Tactic:
grind [labelGraph_adj]

Premises used: SimpleGraph.EdgeLabeling.labelGraph_adj
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.EdgeLabeling
Goal:
V : Type u_1
G : SimpleGraph V
K : Type u_3
C : G.EdgeLabeling K
x : K
_ :
  Membership.mem (γ := Set K) Set.univ x →
    ∀ ⦃y : K⦄, Membership.mem (γ := Set K) Set.univ y → x ≠ y → Function.onFun Disjoint C.labelGraph x y
⊢ Membership.mem (γ := Set K) Set.univ x →
    ∀ ⦃y : K⦄, Membership.mem (γ := Set K) Set.univ y → x ≠ y → Function.onFun Disjoint C.labelGraph x y

Tactic:
_
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.EdgeLabeling
Goal:
V : Type u_1
G : SimpleGraph V
K : Type u_3
C : G.EdgeLabeling K
x : K
h : Membership.mem (γ := Set K) Set.univ x
_ : ∀ ⦃y : K⦄, Membership.mem (γ := Set K) Set.univ y → x ≠ y → Function.onFun Disjoint C.labelGraph x y
⊢ ∀ ⦃y : K⦄, Membership.mem (γ := Set K) Set.univ y → x ≠ y → Function.onFun Disjoint C.labelGraph x y

Tactic:
_
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.EdgeLabeling
Goal:
V : Type u_1
G : SimpleGraph V
K : Type u_3
C : G.EdgeLabeling K
x : K
h : Membership.mem (γ := Set K) Set.univ x
y : K
_ : Membership.mem (γ := Set K) Set.univ y → x ≠ y → Function.onFun Disjoint C.labelGraph x y
⊢ Membership.mem (γ := Set K) Set.univ y → x ≠ y → Function.onFun Disjoint C.labelGraph x y

Tactic:
_
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.EdgeLabeling
Goal:
V : Type u_1
G : SimpleGraph V
K : Type u_3
C : G.EdgeLabeling K
x : K
h_1 : Membership.mem (γ := Set K) Set.univ x
y : K
h_2 : Membership.mem (γ := Set K) Set.univ y
h : x ≠ y
⊢ Function.onFun Disjoint C.labelGraph x y

Tactic:
pairwise_disjoint_labelGraph h

Premises used: SimpleGraph.EdgeLabeling.pairwise_disjoint_labelGraph
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.EdgeLabeling
Goal:
V : Type u_1
G : SimpleGraph V
K : Type u_3
C : G.EdgeLabeling K
x : K
h_1 : Membership.mem (γ := Set K) Set.univ x
y : K
h_2 : Membership.mem (γ := Set K) Set.univ y
h : x ≠ y
⊢ Function.onFun Disjoint C.labelGraph x y

Tactic:
exact pairwise_disjoint_labelGraph h

Premises used: SimpleGraph.EdgeLabeling.pairwise_disjoint_labelGraph
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.EdgeLabeling
Goal:
V : Type u_1
G : SimpleGraph V
K : Type u_3
C : G.EdgeLabeling K
Adj : ∀ (x y : V), SimpleGraph.Adj (⨆ (k : K), C.labelGraph k) x y ↔ G.Adj x y
⊢ ⨆ (k : K), C.labelGraph k = G

Tactic:
ext x y
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.EdgeLabeling
Goal:
V : Type u_1
G : SimpleGraph V
K : Type u_3
C : G.EdgeLabeling K
x y : V
Adj : (∃ (i : K) (H : G.Adj x y), C (Subtype.mk (p := fun (x : Sym2 V) ↦ x ∈ G.edgeSet) s(x, y) H) = i) ↔ G.Adj x y
⊢ SimpleGraph.Adj (⨆ (k : K), C.labelGraph k) x y ↔ G.Adj x y

Tactic:
simp only [iSup_adj, EdgeLabeling.labelGraph_adj]

Premises used: SimpleGraph.iSup_adj, SimpleGraph.EdgeLabeling.labelGraph_adj
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.EdgeLabeling
Goal:
V : Type u_1
G : SimpleGraph V
K : Type u_3
C : G.EdgeLabeling K
x y : V
⊢ (∃ (i : K) (H : G.Adj x y), C (Subtype.mk (p := fun (x : Sym2 V) ↦ x ∈ G.edgeSet) s(x, y) H) = i) ↔ G.Adj x y

Tactic:
grind
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.EdgeLabeling
Goal:
V : Type u_1
V' : Type u_2
G : SimpleGraph V
G' : SimpleGraph V'
K : Type u_3
K' : Type u_4
C : TopEdgeLabeling V K
f : V' ↪ V
⊢ ∀ {a b : V'}, Adj ⊤ a b → Adj.{u_1} (V := V) (⊤ : SimpleGraph V) ((f : (a : V') → V) a : V) ((f : (a : V') → V) b : V)

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.EdgeLabeling
Goal:
V : Type u_1
K : Type u_3
C : TopEdgeLabeling V K
k : K
x y : V
⊢ (EdgeLabeling.labelGraph C k).Adj x y ↔ ∃ (H : x ≠ y), EdgeLabeling.get C x y H = k

Tactic:
simp [EdgeLabeling.labelGraph_adj, EdgeLabeling.get_eq]

Premises used: SimpleGraph.EdgeLabeling.get_eq, SimpleGraph.EdgeLabeling.labelGraph_adj
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.EdgeLabeling
Goal:
V : Type u_1
V' : Type u_2
G_1 : SimpleGraph V
G' : SimpleGraph V'
K : Type u_3
K' : Type u_4
G : SimpleGraph V
inst : DecidableRel G.Adj
⊢ ∀ (x y : V) (H : Adj ⊤ x y),
    Eq (α := Fin 2) ((fun (x y : V) (x_1 : Adj ⊤ x y) ↦ (if G.Adj x y then 1 else 0 : Fin 2)) y x ⋯)
      ((fun (x y : V) (x_1 : Adj ⊤ x y) ↦ (if G.Adj x y then 1 else 0 : Fin 2)) x y H)

Tactic:
simp [G.adj_comm]

Premises used: SimpleGraph.adj_comm
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.EdgeLabeling
Goal:
V : Type u_1
G : SimpleGraph V
inst : DecidableRel G.Adj
x y : V
H : x ≠ y
⊢ EdgeLabeling.get G.toTopEdgeLabeling x y H = if G.Adj x y then 1 else 0

Tactic:
rfl

Premises used: SimpleGraph.EdgeLabeling.mk, SimpleGraph.toTopEdgeLabeling, Sym2.hrec, rfl, SimpleGraph.EdgeLabeling.get, ite
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.EdgeLabeling
Goal:
V : Type u_1
G : SimpleGraph V
inst : DecidableRel G.Adj
Adj : ∀ (x y : V), (EdgeLabeling.labelGraph G.toTopEdgeLabeling 1).Adj x y ↔ G.Adj x y
⊢ EdgeLabeling.labelGraph G.toTopEdgeLabeling 1 = G

Tactic:
ext x y
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.EdgeLabeling
Goal:
V : Type u_1
G : SimpleGraph V
inst : DecidableRel G.Adj
x y : V
⊢ (EdgeLabeling.labelGraph G.toTopEdgeLabeling 1).Adj x y ↔ G.Adj x y

Tactic:
simpa [imp_false] using G.ne_of_adj

Premises used: imp_false, SimpleGraph.ne_of_adj
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.EdgeLabeling
Goal:
V : Type u_1
G : SimpleGraph V
inst : DecidableRel G.Adj
Adj : ∀ (x y : V), (EdgeLabeling.labelGraph G.toTopEdgeLabeling 0).Adj x y ↔ Gᶜ.Adj x y
⊢ EdgeLabeling.labelGraph G.toTopEdgeLabeling 0 = Gᶜ

Tactic:
ext x y
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.EdgeLabeling
Goal:
V : Type u_1
G : SimpleGraph V
inst : DecidableRel G.Adj
x y : V
⊢ (EdgeLabeling.labelGraph G.toTopEdgeLabeling 0).Adj x y ↔ Gᶜ.Adj x y

Tactic:
simp [imp_false]

Premises used: imp_false
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.EdgeLabeling
Goal:
V : Type u_1
inst : DecidableEq V
C : TopEdgeLabeling V (Fin 2)
⊢ (EdgeLabeling.labelGraph C 1).toTopEdgeLabeling = C

Tactic:
EdgeLabeling.ext_get ?_

Premises used: SimpleGraph.EdgeLabeling.ext_get
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.EdgeLabeling
Goal:
V : Type u_1
inst : DecidableEq V
C : TopEdgeLabeling V (Fin 2)
refine :
  ∀ (x y : V) (h : Adj ⊤ x y),
    EdgeLabeling.get (EdgeLabeling.labelGraph C 1).toTopEdgeLabeling x y h = EdgeLabeling.get C x y h
⊢ (EdgeLabeling.labelGraph C 1).toTopEdgeLabeling = C

Tactic:
refine EdgeLabeling.ext_get ?_

Premises used: SimpleGraph.EdgeLabeling.ext_get
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.EdgeLabeling
Goal:
V : Type u_1
inst : DecidableEq V
C : TopEdgeLabeling V (Fin 2)
⊢ ∀ (x y : V) (h : Adj ⊤ x y),
    EdgeLabeling.get (EdgeLabeling.labelGraph C 1).toTopEdgeLabeling x y h = EdgeLabeling.get C x y h

Tactic:
grind [toTopEdgeLabeling_get, TopEdgeLabeling.labelGraph_adj, Adj.ne]

Premises used: SimpleGraph.TopEdgeLabeling.labelGraph_adj, SimpleGraph.Adj.ne, SimpleGraph.toTopEdgeLabeling_get
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring
Goal:
V : Type u
G : SimpleGraph V
α : Type u_2
C : G.Coloring α
v w : V
h : G.Adj v w
⊢ Ne.{u_2 + 1} (α := α) ((C : (a : V) → α) v : α) ((C : (a : V) → α) w : α)

Tactic:
C.map_rel h

Premises used: RelHom.map_rel, Not
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring
Goal:
V : Type u
G : SimpleGraph V
ι : Type u_1
α : Type u_2
C : G.Coloring α
f : ι → V
hf : Pairwise fun (i j : ι) ↦ G.Adj (f i) (f j)
⊢ Injective.{u_1 + 1, u_2 + 1} (β := α) ((⇑C : (a : V) → α) ∘ f)

Tactic:
Function.injective_iff_pairwise_ne.2 <| hf.mono fun _ _ ↦ C.valid

Premises used: Iff.mpr, SimpleGraph.Coloring.valid, Function.injective_iff_pairwise_ne, Pairwise.mono
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring
Goal:
V : Type u
G : SimpleGraph V
α : Type u_2
C : G.Coloring α
v : V
⊢ v ∈ C.colorClass ((C : (a : V) → α) v)

Tactic:
rfl

Premises used: SimpleGraph.Coloring.colorClass, Set.Mem, setOf, rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring
Goal:
V : Type u
G : SimpleGraph V
α : Type u_2
C : G.Coloring α
⊢ Setoid.IsPartition C.colorClasses

Tactic:
Setoid.isPartition_classes (Setoid.ker C)

Premises used: Setoid.isPartition_classes, Setoid.ker, SimpleGraph.Coloring.colorClasses, DFunLike.coe
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring
Goal:
V : Type u
G : SimpleGraph V
α : Type u_2
C : G.Coloring α
v : V
⊢ C.colorClass ((C : (a : V) → α) v) ∈ C.colorClasses

Tactic:
⟨v, rfl⟩

Premises used: Set.Mem, setOf, Setoid.classes, SimpleGraph.Coloring.colorClasses, Exists.intro, rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring
Goal:
V : Type u
G : SimpleGraph V
α : Type u_2
C : G.Coloring α
inst : Finite α
⊢ C.colorClasses.Finite

Tactic:
Setoid.finite_classes_ker _

Premises used: Setoid.finite_classes_ker, SimpleGraph.Coloring.colorClasses
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring
Goal:
V : Type u
G : SimpleGraph V
α : Type u_2
C : G.Coloring α
inst : Fintype α
inst_1 : Fintype (↑C.colorClasses : Type u)
⊢ card.{u} (↑(Setoid.classes (Setoid.ker.{u, u_2} (β := α) (⇑C : (a : V) → α))) : Type u) ≤ card α

Tactic:
Setoid.card_classes_ker_le C

Premises used: Setoid.card_classes_ker_le, DFunLike.coe
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring
Goal:
V : Type u
G : SimpleGraph V
α : Type u_2
C : G.Coloring α
inst : Fintype α
inst_1 : Fintype (↑C.colorClasses : Type u)
⊢ card.{u} (↑(Setoid.classes (Setoid.ker.{u, u_2} (β := α) (⇑C : (a : V) → α))) : Type u) ≤ card α

Tactic:
convert! Setoid.card_classes_ker_le C
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring
Goal:
V : Type u
G : SimpleGraph V
α : Type u_2
C : G.Coloring α
c : α
v w : V
hv : v ∈ C.colorClass c
hw : w ∈ C.colorClass c
⊢ ¬G.Adj v w

Tactic:
fun h => C.valid h (Eq.trans hv (Eq.symm hw))

Premises used: SimpleGraph.Coloring.valid, Eq.symm, Not, Eq.trans
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring
Goal:
V : Type u
G : SimpleGraph V
α : Type u_2
C : G.Coloring α
c : α
⊢ G.IsIndepSet (C.colorClass c)

Tactic:
fun _ hv _ hw _ ↦ C.not_adj_of_mem_colorClass hv hw

Premises used: SimpleGraph.Coloring.not_adj_of_mem_colorClass, Set.Pairwise
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring
Goal:
V : Type u
G : SimpleGraph V
α : Type u_2
C : G.Coloring α
c : α
⊢ IsAntichain G.Adj (C.colorClass c)

Tactic:
C.isIndepSet_colorClass c

Premises used: IsAntichain, SimpleGraph.Coloring.isIndepSet_colorClass
-- 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 : Fintype V
inst_1 : Fintype α
⊢ Fintype (G.Adj →r (completeGraph α).Adj)

Tactic:
apply Fintype.ofInjective _ RelHom.coe_fn_injective

Premises used: RelHom.coe_fn_injective, Fintype.ofInjective
-- 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 : Nontrivial α
inst_2 : Nonempty V
have : ∀ (C : G.Coloring α), Nontrivial (G.Coloring α)
⊢ Nontrivial (G.Coloring α)

Tactic:
have ⟨C⟩ := ‹Nonempty <| G.Coloring α›
-- 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 : Nontrivial α
inst_2 : Nonempty V
C : G.Coloring α
have : ∀ (v : V), Nontrivial (G.Coloring α)
⊢ Nontrivial (G.Coloring α)

Tactic:
have ⟨v⟩ := ‹Nonempty 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 : Nontrivial α
inst_2 : Nonempty V
C : G.Coloring α
v : V
have : ∀ (c : α) (hc : c ≠ (C : (a : V) → α) v), Nontrivial (G.Coloring α)
⊢ Nontrivial (G.Coloring α)

Tactic:
have ⟨c, hc⟩ := nontrivial_iff_exists_ne (C v) |>.mp inferInstance
-- 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 : Nontrivial α
inst_2 : Nonempty V
C : G.Coloring α
v : V
c : α
hc : c ≠ (C : (a : V) → α) v
⊢ Nontrivial (G.Coloring α)

Tactic:
⟨(Iso.completeGraph <| Equiv.swap (C v) c).toHom.comp C, C, fun h ↦ hc ?_⟩

Premises used: SimpleGraph.Iso.completeGraph, Equiv.swap, SimpleGraph.Iso.toHom, Nontrivial.mk, Exists.intro, DFunLike.coe, SimpleGraph.Hom.comp
-- 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 : Nontrivial α
inst_2 : Nonempty V
C : G.Coloring α
v : V
c : α
hc : c ≠ (C : (a : V) → α) v
refine :
  ∀ (h : Hom.comp (Iso.toHom (Iso.completeGraph (Equiv.swap ((C : (a : V) → α) v) c))) C = C), c = (C : (a : V) → α) v
⊢ Nontrivial (G.Coloring α)

Tactic:
refine ⟨(Iso.completeGraph <| Equiv.swap (C v) c).toHom.comp C, C, fun h ↦ hc ?_⟩
-- 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 : Nontrivial α
inst_2 : Nonempty V
C : G.Coloring α
v : V
c : α
hc : c ≠ (C : (a : V) → α) v
h : Hom.comp (Iso.toHom (Iso.completeGraph (Equiv.swap ((C : (a : V) → α) v) c))) C = C
⊢ RelHom.toFun (r := G.Adj) (s := (completeGraph α).Adj)
      (Hom.comp (Iso.toHom (Iso.completeGraph (Equiv.swap ((C : (a : V) → α) v) c))) C) v =
    C.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 : Nontrivial α
inst_2 : Nonempty V
C : G.Coloring α
v : V
c : α
hc : c ≠ (C : (a : V) → α) v
h : Hom.comp (Iso.toHom (Iso.completeGraph (Equiv.swap ((C : (a : V) → α) v) c))) C = C
this :
  Eq.{u_2 + 1} (α := α)
    (((Equiv.swap ((C : (a : V) → α) v) c : Equiv.Perm α) : (a : α) → α) ((C : (a : V) → α) v : α) : α)
    ((C : (a : V) → α) v : α)
⊢ c = (C : (a : V) → α) v

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 : Nontrivial α
inst_2 : Nonempty V
have have₁ have₂ : ∀ (C : G.Coloring α), Nontrivial (G.Coloring α)
have₃ : ∀ (C : G.Coloring α) (v : V), Nontrivial (G.Coloring α)
have₄ : ∀ (C : G.Coloring α) (v : V) (c : α) (hc : c ≠ (C : (a : V) → α) v), Nontrivial (G.Coloring α)
have₅ :
  ∀ (C : G.Coloring α) (v : V) (c : α) (hc : c ≠ (C : (a : V) → α) v)
    (h : Hom.comp (Iso.toHom (Iso.completeGraph (Equiv.swap ((C : (a : V) → α) v) c))) C = C), c = (C : (a : V) → α) v
have₆ :
  ∀ (C : G.Coloring α) (v : V) (c : α) (hc : c ≠ (C : (a : V) → α) v)
    (h : Hom.comp (Iso.toHom (Iso.completeGraph (Equiv.swap ((C : (a : V) → α) v) c))) C = C)
    (this :
      RelHom.toFun (r := G.Adj) (s := (completeGraph α).Adj)
          (Hom.comp (Iso.toHom (Iso.completeGraph (Equiv.swap ((C : (a : V) → α) v) c))) C) v =
        C.toFun (r := G.Adj) (s := (completeGraph α).Adj) v),
    c = (C : (a : V) → α) v
have₇ :
  ∀ (C : G.Coloring α) (v : V) (c : α) (hc : c ≠ (C : (a : V) → α) v)
    (h : Hom.comp (Iso.toHom (Iso.completeGraph (Equiv.swap ((C : (a : V) → α) v) c))) C = C)
    (this :
      Eq.{u_2 + 1} (α := α)
        (((Equiv.swap ((C : (a : V) → α) v) c : Equiv.Perm α) : (a : α) → α) ((C : (a : V) → α) v : α) : α)
        ((C : (a : V) → α) v : α)),
    c = (C : (a : V) → α) v
⊢ Nontrivial (G.Coloring α)

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

Premises used: SimpleGraph.Iso.completeGraph
-- 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 : ∀ (C : G.Coloring α), Infinite (G.Coloring α)
⊢ Infinite (G.Coloring α)

Tactic:
have ⟨C⟩ := ‹Nonempty <| G.Coloring α›
-- 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 α
have : ∀ (v : V), Infinite (G.Coloring α)
⊢ Infinite (G.Coloring α)

Tactic:
have ⟨v⟩ := ‹Nonempty 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
⊢ Infinite (G.Coloring α)

Tactic:
Infinite.of_injective f fun a b h ↦ ?_

Premises used: Infinite.of_injective
-- 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
refine : ∀ (a b : α) (h : f a = f b), a = b
⊢ Infinite (G.Coloring α)

Tactic:
refine Infinite.of_injective f fun a b h ↦ ?_

Premises used: Infinite.of_injective