awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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:
exact ⟨_, he⟩
-- 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
pos : ∀ (he' : (C : (a : V ⊕ W) → Fin 2) (Sum.inr w) = b), ∃ (a : V ⊕ W), (C : (a : V ⊕ W) → Fin 2) a = b
neg : ∀ (he' : ¬(C : (a : V ⊕ W) → Fin 2) (Sum.inr w) = 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.inr w) = b

Premises used: Sum.inr, 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
he' : (C : (a : V ⊕ W) → Fin 2) (Sum.inr w) = b
⊢ ∃ (a : V ⊕ W), (C : (a : V ⊕ W) → Fin 2) a = b

Tactic:
⟨_, he'⟩

Premises used: Exists.intro
-- 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
he' : (C : (a : V ⊕ W) → Fin 2) (Sum.inr w) = b
⊢ ∃ (a : V ⊕ W), (C : (a : V ⊕ W) → Fin 2) a = b

Tactic:
exact ⟨_, he'⟩
-- 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
he' : ¬(C : (a : V ⊕ W) → Fin 2) (Sum.inr w) = b
⊢ ∃ (a : V ⊕ W), (C : (a : V ⊕ W) → Fin 2) a = b

Tactic:
simpa using two_lt_card_iff.2 ⟨_, _, _, C.valid h, he, he'⟩

Premises used: Iff.mpr, Fintype.two_lt_card_iff, SimpleGraph.Coloring.valid, And.intro, Exists.intro
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring
Goal:
V : Type u
G : SimpleGraph V
n : ℕ
s : Finset V
h : G.IsClique (↑s : Set V)
hc : G.Colorable n
⊢ Pairwise fun (i j : ↥s) ↦ G.Adj (↑i : V) (↑j : V)

Tactic:
simpa [Pairwise] using h

Premises used: Pairwise
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring
Goal:
V : Type u
G : SimpleGraph V
n : ℕ
s : Finset V
h : G.IsClique (↑s : Set V)
hc : G.Colorable n
⊢ s.card ≤ n

Tactic:
simpa using hc.card_le_of_pairwise_adj (Subtype.val : s → V) <| by simpa [Pairwise] using h

Premises used: SimpleGraph.Colorable.card_le_of_pairwise_adj, Subtype.val
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring
Goal:
V : Type u
G : SimpleGraph V
α : Type u_2
s : Finset V
h : G.IsClique (↑s : Set V)
inst : Fintype α
C : G.Coloring α
⊢ s.card ≤ card α

Tactic:
h.card_le_of_colorable C.colorable

Premises used: SimpleGraph.IsClique.card_le_of_colorable, SimpleGraph.Coloring.colorable
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring
Goal:
V : Type u
G : SimpleGraph V
s : Finset V
h : G.IsClique (↑s : Set V)
⊢ s.card ≤ Nat.card.{u} ↥s

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring
Goal:
V : Type u
G : SimpleGraph V
s : Finset V
h : G.IsClique (↑s : Set V)
⊢ Pairwise fun (i j : ↥s) ↦ G.Adj (↑i : V) (↑j : V)

Tactic:
simpa [Pairwise] using h

Premises used: Pairwise
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring
Goal:
V : Type u
G : SimpleGraph V
have : ∀ (s : Finset V) (hs : G.IsNClique G.cliqueNum s), (↑G.cliqueNum : ℕ∞) ≤ G.chromaticNumber
⊢ (↑G.cliqueNum : ℕ∞) ≤ G.chromaticNumber

Tactic:
have ⟨s, hs⟩ := G.exists_isNClique_cliqueNum
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring
Goal:
V : Type u
G : SimpleGraph V
s : Finset V
hs : G.IsNClique G.cliqueNum s
⊢ (↑G.cliqueNum : ℕ∞) ≤ G.chromaticNumber

Tactic:
hs.card_eq ▸ hs.isClique.card_le_chromaticNumber

Premises used: SimpleGraph.IsNClique.card_eq, Eq.rec, SimpleGraph.IsNClique.isClique, SimpleGraph.IsClique.card_le_chromaticNumber
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring
Goal:
V : Type u
G : SimpleGraph V
s : Finset V
hs : G.IsNClique G.cliqueNum s
⊢ (↑G.cliqueNum : ℕ∞) ≤ G.chromaticNumber

Tactic:
exact hs.card_eq ▸ hs.isClique.card_le_chromaticNumber
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring
Goal:
V : Type u
G : SimpleGraph V
n m : ℕ
hc : G.Colorable n
hm : n < m
by_contra : ∀ (h : ¬G.CliqueFree m), False
⊢ G.CliqueFree m

Tactic:
by_contra h
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring
Goal:
V : Type u
G : SimpleGraph V
n m : ℕ
hc : G.Colorable n
hm : n < m
h : ¬G.CliqueFree m
⊢ ∃ (x : Finset V), G.IsClique (↑x : Set V) ∧ x.card = m

Tactic:
simp only [CliqueFree, isNClique_iff, not_forall, Classical.not_not] at h

Premises used: Classical.not_not, SimpleGraph.CliqueFree, SimpleGraph.isNClique_iff, Classical.not_forall
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring
Goal:
V : Type u
G : SimpleGraph V
n m : ℕ
hc : G.Colorable n
hm : n < m
h : ∃ (x : Finset V), G.IsClique (↑x : Set V) ∧ x.card = m
obtain : ∀ (s : Finset V) (h : G.IsClique (↑s : Set V)) (hm : n < s.card), False
⊢ False

Tactic:
obtain ⟨s, h, rfl⟩ := h

Premises used: rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring
Goal:
V : Type u
G : SimpleGraph V
n : ℕ
hc : G.Colorable n
s : Finset V
h : G.IsClique (↑s : Set V)
hm : n < s.card
⊢ False

Tactic:
Nat.lt_le_asymm hm (h.card_le_of_colorable hc)

Premises used: Nat.lt_le_asymm, SimpleGraph.IsClique.card_le_of_colorable
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring
Goal:
V : Type u
G : SimpleGraph V
n : ℕ
hc : G.Colorable n
s : Finset V
h : G.IsClique (↑s : Set V)
hm : n < s.card
⊢ False

Tactic:
exact Nat.lt_le_asymm hm (h.card_le_of_colorable hc)

Premises used: Nat.lt_le_asymm, SimpleGraph.IsClique.card_le_of_colorable
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring
Goal:
V : Type u
G : SimpleGraph V
n : ℕ
hc : G.chromaticNumber < (↑n : ℕ∞)
⊢ G.chromaticNumber ≠ ⊤

Tactic:
have hne : G.chromaticNumber ≠ ⊤ := hc.ne_top
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring
Goal:
V : Type u
G : SimpleGraph V
n : ℕ
hc : G.chromaticNumber < (↑n : ℕ∞)
hne : G.chromaticNumber ≠ ⊤
obtain : ∀ (m : ℕ) (hc' : G.Colorable m), G.CliqueFree n
⊢ G.CliqueFree n

Tactic:
obtain ⟨m, hc'⟩ := chromaticNumber_ne_top_iff_exists.mp hne

Premises used: SimpleGraph.chromaticNumber_ne_top_iff_exists, Iff.mp
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring
Goal:
V : Type u
G : SimpleGraph V
n : ℕ
hc : G.chromaticNumber < (↑n : ℕ∞)
hne : G.chromaticNumber ≠ ⊤
m : ℕ
hc' : G.Colorable m
⊢ G.Colorable G.chromaticNumber.toNat

Tactic:
have := colorable_chromaticNumber hc'
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring
Goal:
V : Type u
G : SimpleGraph V
n : ℕ
hc : G.chromaticNumber < (↑n : ℕ∞)
hne : G.chromaticNumber ≠ ⊤
m : ℕ
hc' : G.Colorable m
this : G.Colorable G.chromaticNumber.toNat
⊢ G.CliqueFree n

Tactic:
this.cliqueFree ?_

Premises used: SimpleGraph.Colorable.cliqueFree
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring
Goal:
V : Type u
G : SimpleGraph V
n : ℕ
hc : G.chromaticNumber < (↑n : ℕ∞)
hne : G.chromaticNumber ≠ ⊤
m : ℕ
hc' : G.Colorable m
this : G.Colorable G.chromaticNumber.toNat
refine : G.chromaticNumber.toNat < n
⊢ G.CliqueFree n

Tactic:
refine this.cliqueFree ?_

Premises used: SimpleGraph.Colorable.cliqueFree
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring
Goal:
V : Type u
G : SimpleGraph V
n : ℕ
hc : G.chromaticNumber < (↑n : ℕ∞)
hne : G.chromaticNumber ≠ ⊤
m : ℕ
hc' : G.Colorable m
this : G.Colorable G.chromaticNumber.toNat
rw :
  ∀ (hne : (↑G.chromaticNumber.toNat : ℕ∞) = G.chromaticNumber) (m : ℕ) (hc' : G.Colorable m)
    (this : G.Colorable G.chromaticNumber.toNat), G.chromaticNumber.toNat < n
⊢ G.chromaticNumber.toNat < n

Tactic:
rw [← ENat.coe_toNat_eq_self] at hne

Premises used: ENat.coe_toNat_eq_self
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring
Goal:
V : Type u
G : SimpleGraph V
n : ℕ
hc : G.chromaticNumber < (↑n : ℕ∞)
hne : (↑G.chromaticNumber.toNat : ℕ∞) = G.chromaticNumber
m : ℕ
hc' : G.Colorable m
this : G.Colorable G.chromaticNumber.toNat
rw :
  ∀ (hc : LT.lt (α := ℕ∞) (↑G.chromaticNumber.toNat : ℕ∞) (↑n : ℕ∞))
    (hne : (↑G.chromaticNumber.toNat : ℕ∞) = G.chromaticNumber) (m : ℕ) (hc' : G.Colorable m)
    (this : G.Colorable G.chromaticNumber.toNat), G.chromaticNumber.toNat < n
⊢ G.chromaticNumber.toNat < n

Tactic:
rw [← hne] at hc
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring
Goal:
V : Type u
G : SimpleGraph V
n : ℕ
hc : LT.lt (α := ℕ∞) (↑G.chromaticNumber.toNat : ℕ∞) (↑n : ℕ∞)
hne : (↑G.chromaticNumber.toNat : ℕ∞) = G.chromaticNumber
m : ℕ
hc' : G.Colorable m
this : G.Colorable G.chromaticNumber.toNat
⊢ G.chromaticNumber.toNat < n

Tactic:
simpa using hc
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring
Goal:
V : Type u
G : SimpleGraph V
α : Type u_2
inst : Fintype α
s : Finset V
h : G.IsClique (↑s : Set V)
hc : card α ≤ s.card
C : G.Coloring α
a : α
_ : Membership.mem (γ := Set α) Set.univ a → Membership.mem (γ := Set α) ((⇑C : (a : V) → α) '' (↑s : Set V)) a
⊢ Membership.mem (γ := Set α) Set.univ a → Membership.mem (γ := Set α) ((⇑C : (a : V) → α) '' (↑s : Set V)) a

Tactic:
_
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring
Goal:
V : Type u
G : SimpleGraph V
α : Type u_2
inst : Fintype α
s : Finset V
h : G.IsClique (↑s : Set V)
hc : card α ≤ s.card
C : G.Coloring α
a : α
h_1 : Membership.mem (γ := Set α) Set.univ a
⊢ (↑(card α) : ℕ∞) ≤ (induce (↑s : Set V) G).chromaticNumber

Tactic:
simp_all [isClique_iff_induce_eq]

Premises used: SimpleGraph.isClique_iff_induce_eq
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring
Goal:
V : Type u
G : SimpleGraph V
α : Type u_2
inst : Fintype α
s : Finset V
h : G.IsClique (↑s : Set V)
hc : card α ≤ s.card
C : G.Coloring α
a : α
h_1 : Membership.mem (γ := Set α) Set.univ a
obtain :
  ∀ (w : (↑(↑s : Set V) : Type u))
    (hx : (Hom.comp C (Embedding.toHom (Embedding.induce (↑s : Set V))) : (a : (↑(↑s : Set V) : Type u)) → α) w = a),
    Membership.mem (γ := Set α) ((⇑C : (a : V) → α) '' (↑s : Set V)) a
⊢ Membership.mem (γ := Set α) ((⇑C : (a : V) → α) '' (↑s : Set V)) a

Tactic:
obtain ⟨_, hx⟩ := card_le_chromaticNumber_iff_forall_surjective.mp
                    (by simp_all [isClique_iff_induce_eq]) (C.comp (Embedding.induce s).toHom) _

Premises used: SimpleGraph.card_le_chromaticNumber_iff_forall_surjective, Iff.mp, SimpleGraph.Embedding.toHom, SimpleGraph.Embedding.induce, SimpleGraph.Hom.comp
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring
Goal:
V : Type u
G : SimpleGraph V
α : Type u_2
inst : Fintype α
s : Finset V
h : G.IsClique (↑s : Set V)
hc : card α ≤ s.card
C : G.Coloring α
a : α
h_1 : Membership.mem (γ := Set α) Set.univ a
w : (↑(↑s : Set V) : Type u)
hx : (Hom.comp C (Embedding.toHom (Embedding.induce (↑s : Set V))) : (a : (↑(↑s : Set V) : Type u)) → α) w = a
⊢ Membership.mem (γ := Set α) ((⇑C : (a : V) → α) '' (↑s : Set V)) a

Tactic:
⟨_, Subtype.coe_prop _, hx⟩

Premises used: Subtype.coe_prop, Set.Mem, setOf, And.intro, Exists.intro, Set.image
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring
Goal:
V : Type u
G : SimpleGraph V
α : Type u_2
inst : Fintype α
s : Finset V
h : G.IsClique (↑s : Set V)
hc : card α ≤ s.card
C : G.Coloring α
a : α
h_1 : Membership.mem (γ := Set α) Set.univ a
w : (↑(↑s : Set V) : Type u)
hx : (Hom.comp C (Embedding.toHom (Embedding.induce (↑s : Set V))) : (a : (↑(↑s : Set V) : Type u)) → α) w = a
⊢ Membership.mem (γ := Set α) ((⇑C : (a : V) → α) '' (↑s : Set V)) a

Tactic:
exact ⟨_, Subtype.coe_prop _, hx⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring
Goal:
V_1 : Type u
G : SimpleGraph V_1
n : ℕ
ι_1 : Type u_1
α : Type u_2
β : Type u_3
C : G.Coloring α
ι : Type u_4
V : ι → Type u_5
⊢ ∀ {v w : (i : ι) × V i},
    (completeMultipartiteGraph V).Adj v w →
      Ne.{u_4 + 1} (α := ι) ((fun (v : (i : ι) × V i) ↦ v.fst (β := fun (i : ι) ↦ V i)) v)
        ((fun (v : (i : ι) × V i) ↦ v.fst (β := fun (i : ι) ↦ V i)) w)

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring
Goal:
ι : Type u_4
V : ι → Type u_5
inst : Fintype ι
⊢ (completeMultipartiteGraph V).Colorable (card ι)

Tactic:
(coloring V).colorable

Premises used: SimpleGraph.Coloring.colorable, SimpleGraph.completeMultipartiteGraph.coloring
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring
Goal:
ι : Type u_4
V : ι → Type u_5
inst : Fintype ι
f : (i : ι) → V i
apply : (↑(card ι) : ℕ∞) ≤ (completeMultipartiteGraph V).chromaticNumber
⊢ (completeMultipartiteGraph V).chromaticNumber = (↑(card ι) : ℕ∞)

Tactic:
apply le_antisymm (colorable V).chromaticNumber_le

Premises used: SimpleGraph.Colorable.chromaticNumber_le, le_antisymm, SimpleGraph.completeMultipartiteGraph.colorable
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring
Goal:
ι : Type u_4
V : ι → Type u_5
inst : Fintype ι
f : (i : ι) → V i
by_contra! : ∀ (h : (completeMultipartiteGraph V).chromaticNumber < (↑(card ι) : ℕ∞)), False
⊢ (↑(card ι) : ℕ∞) ≤ (completeMultipartiteGraph V).chromaticNumber

Tactic:
by_contra! h
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring
Goal:
ι : Type u_4
V : ι → Type u_5
inst : Fintype ι
f : (i : ι) → V i
h : (completeMultipartiteGraph V).chromaticNumber < (↑(card ι) : ℕ∞)
⊢ False

Tactic:
not_cliqueFree_of_le_card V f le_rfl <| cliqueFree_of_chromaticNumber_lt h

Premises used: le_rfl, SimpleGraph.completeMultipartiteGraph.not_cliqueFree_of_le_card, SimpleGraph.cliqueFree_of_chromaticNumber_lt
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring
Goal:
ι : Type u_4
V : ι → Type u_5
inst : Fintype ι
f : (i : ι) → V i
h : (completeMultipartiteGraph V).chromaticNumber < (↑(card ι) : ℕ∞)
⊢ False

Tactic:
exact not_cliqueFree_of_le_card V f le_rfl <| cliqueFree_of_chromaticNumber_lt h

Premises used: le_rfl, SimpleGraph.completeMultipartiteGraph.not_cliqueFree_of_le_card, SimpleGraph.cliqueFree_of_chromaticNumber_lt
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring
Goal:
ι : Type u_4
V : ι → Type u_5
f : (i : ι) → V i
hc : (completeMultipartiteGraph V).CliqueFree 0
⊢ (completeMultipartiteGraph V).Colorable (HSub.hSub (α := ℕ) 0 1)

Tactic:
absurd hc not_cliqueFree_zero

Premises used: SimpleGraph.not_cliqueFree_zero, absurd
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring
Goal:
ι : Type u_4
V : ι → Type u_5
f : (i : ι) → V i
hc : (completeMultipartiteGraph V).CliqueFree 0
⊢ (completeMultipartiteGraph V).Colorable (HSub.hSub (α := ℕ) 0 1)

Tactic:
exact absurd hc not_cliqueFree_zero

Premises used: SimpleGraph.not_cliqueFree_zero, absurd
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring
Goal:
ι : Type u_4
V : ι → Type u_5
f : (i : ι) → V i
n : ℕ
hc : (completeMultipartiteGraph V).CliqueFree (n + 1)
succ : ∀ (this : Fintype ι), (completeMultipartiteGraph V).Colorable (n + 1 - 1)
⊢ (completeMultipartiteGraph V).Colorable (n + 1 - 1)

Tactic:
have : Fintype ι := fintypeOfNotInfinite
    fun hinf ↦ not_cliqueFree_of_infinite V f hc
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring
Goal:
ι : Type u_4
V : ι → Type u_5
f : (i : ι) → V i
n : ℕ
hc : (completeMultipartiteGraph V).CliqueFree (n + 1)
this : Fintype ι
succ : card ι ≤ n + 1 - 1
⊢ (completeMultipartiteGraph V).Colorable (n + 1 - 1)

Tactic:
apply (coloring V).colorable.mono

Premises used: SimpleGraph.Colorable.mono, SimpleGraph.Coloring.colorable, SimpleGraph.completeMultipartiteGraph.coloring
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring
Goal:
ι : Type u_4
V : ι → Type u_5
f : (i : ι) → V i
n : ℕ
hc : (completeMultipartiteGraph V).CliqueFree (n + 1)
this : Fintype ι
⊢ ¬(completeMultipartiteGraph V).CliqueFree (card ι)

Tactic:
have := not_cliqueFree_of_le_card V f le_rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring
Goal:
ι : Type u_4
V : ι → Type u_5
f : (i : ι) → V i
n : ℕ
hc : (completeMultipartiteGraph V).CliqueFree (n + 1)
this_1 : Fintype ι
this : ¬(completeMultipartiteGraph V).CliqueFree (card ι)
succ : ∀ (this : n + 1 - 1 < card ι), (completeMultipartiteGraph V).CliqueFree (card ι)
⊢ card ι ≤ n + 1 - 1

Tactic:
contrapose! this
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring
Goal:
ι : Type u_4
V : ι → Type u_5
f : (i : ι) → V i
n : ℕ
hc : (completeMultipartiteGraph V).CliqueFree (n + 1)
this_1 : Fintype ι
this : n + 1 - 1 < card ι
⊢ (completeMultipartiteGraph V).CliqueFree (card ι)

Tactic:
hc.mono this

Premises used: SimpleGraph.CliqueFree.mono
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring
Goal:
ι : Type u_4
V : ι → Type u_5
f : (i : ι) → V i
n : ℕ
hc : (completeMultipartiteGraph V).CliqueFree (n + 1)
this_1 : Fintype ι
this : n + 1 - 1 < card ι
⊢ (completeMultipartiteGraph V).CliqueFree (card ι)

Tactic:
exact hc.mono this

Premises used: SimpleGraph.CliqueFree.mono
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring
Goal:
n : ℕ
ι : Type u_4
V : ι → Type u_5
f : (i : ι) → V i
hc : (completeMultipartiteGraph V).CliqueFree n
zero :
  ∀ (hc : (completeMultipartiteGraph V).CliqueFree 0), (completeMultipartiteGraph V).Colorable (HSub.hSub (α := ℕ) 0 1)
succ :
  ∀ (n : ℕ) (hc : (completeMultipartiteGraph V).CliqueFree (n + 1)), (completeMultipartiteGraph V).Colorable (n + 1 - 1)
⊢ (completeMultipartiteGraph V).Colorable (n - 1)

Tactic:
cases n with
  | zero => exact absurd hc not_cliqueFree_zero
  | succ n =>
  have : Fintype ι := fintypeOfNotInfinite
    fun hinf ↦ not_cliqueFree_of_infinite V f hc
  apply (coloring V).colorable.mono
  have := not_cliqueFree_of_le_card V f le_rfl
  contrapose! this
  exact hc.mono this

Premises used: absurd
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring
Goal:
V : Type u
G : SimpleGraph V
n : ℕ
W : Type u_4
H : SimpleGraph W
nhc : ¬H.Colorable n
hc : G.Colorable n
contrapose : ∀ (hc' : H ⊑ G), H.Colorable n
⊢ H.Free G

Tactic:
contrapose nhc with hc'
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring
Goal:
V : Type u
G : SimpleGraph V
n : ℕ
W : Type u_4
H : SimpleGraph W
hc : G.Colorable n
hc' : H ⊑ G
⊢ H.Colorable n

Tactic:
⟨hc.some.comp hc'.some.toHom⟩

Premises used: Nonempty.some, Nonempty.intro, SimpleGraph.Copy.toHom, SimpleGraph.Colorable, SimpleGraph.Hom.comp
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring
Goal:
V : Type u
G : SimpleGraph V
n : ℕ
W : Type u_4
H : SimpleGraph W
hc : G.Colorable n
hc' : H ⊑ G
⊢ H.Colorable n

Tactic:
exact ⟨hc.some.comp hc'.some.toHom⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
Goal:
α : Type u
⊢ ∀ (a b c : α), ¬Adj ⊥ a b → ¬Adj ⊥ b c → ¬Adj ⊥ a c

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
Goal:
α : Type u
G : SimpleGraph α
s : Set α
h : G.IsCompleteMultipartite
x y : α
h' : ¬G.Adj x y
rwa rwa₁ rwa₂ rwa₃ : ∀ (h' : ¬G.Adj y x), ¬G.Adj y x
⊢ ¬G.Adj y x

Tactic:
rwa [adj_comm] at h'

Premises used: SimpleGraph.adj_comm
-- Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
Goal:
ι : Type u_1
V : ι → Type u_2
⊢ ∀ (a b c : (i : ι) × V i),
    ¬(completeMultipartiteGraph V).Adj a b →
      ¬(completeMultipartiteGraph V).Adj b c → ¬(completeMultipartiteGraph V).Adj a c

Tactic:
simp_all
-- Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
Goal:
α : Type u
G : SimpleGraph α
s : Set α
h : G.IsCompleteMultipartite
simp_rw : ∀ {a b : α}, ¬(h.setoid : α → α → Prop) a b ↔ G.Adj a b
⊢ ∀ {a b : α},
    Adj.{u} (V := (i : Quotient h.setoid) × { x : α // (h.setoid : α → α → Prop) i.out x })
        (completeMultipartiteGraph fun (c : Quotient h.setoid) ↦ { x : α // (h.setoid : α → α → Prop) c.out x })
        (({
              toFun := fun (x : α) ↦
                Sigma.mk (β := fun (i : Quotient h.setoid) ↦ { x : α // (h.setoid : α → α → Prop) i.out x }) ⟦x⟧
                  (Subtype.mk (p := fun (x_1 : α) ↦ (h.setoid : α → α → Prop) ⟦x⟧.out x_1) x ⋯),
              invFun := fun (x : (i : Quotient h.setoid) × { x : α // (h.setoid : α → α → Prop) i.out x }) ↦
                match (motive := (i : Quotient h.setoid) × { x : α // (h.setoid : α → α → Prop) i.out x } → α) x with
                | ⟨fst, x⟩ => (↑x : α),
              left_inv := ⋯, right_inv := ⋯ :
              α ≃ (i : Quotient h.setoid) × { x : α // (h.setoid : α → α → Prop) i.out x } } :
            (a : α) → (i : Quotient h.setoid) × { x : α // (h.setoid : α → α → Prop) i.out x })
          a)
        (({
              toFun := fun (x : α) ↦
                Sigma.mk (β := fun (i : Quotient h.setoid) ↦ { x : α // (h.setoid : α → α → Prop) i.out x }) ⟦x⟧
                  (Subtype.mk (p := fun (x_1 : α) ↦ (h.setoid : α → α → Prop) ⟦x⟧.out x_1) x ⋯),
              invFun := fun (x : (i : Quotient h.setoid) × { x : α // (h.setoid : α → α → Prop) i.out x }) ↦
                match (motive := (i : Quotient h.setoid) × { x : α // (h.setoid : α → α → Prop) i.out x } → α) x with
                | ⟨fst, x⟩ => (↑x : α),
              left_inv := ⋯, right_inv := ⋯ :
              α ≃ (i : Quotient h.setoid) × { x : α // (h.setoid : α → α → Prop) i.out x } } :
            (a : α) → (i : Quotient h.setoid) × { x : α // (h.setoid : α → α → Prop) i.out x })
          b) ↔
      G.Adj a b

Tactic:
simp_rw [Equiv.coe_fn_mk, comap_adj, top_adj, ne_eq, Quotient.eq]

Premises used: SimpleGraph.top_adj, ne_eq, SimpleGraph.comap_adj, Equiv.coe_fn_mk, Quotient.eq
-- Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
Goal:
α : Type u
G : SimpleGraph α
s : Set α
h : G.IsCompleteMultipartite
a b : α
rw rw₁ : G.Adj a b ↔ G.Adj a b
⊢ ¬¬G.Adj a b ↔ G.Adj a b

Tactic:
rw [not_not]

Premises used: Classical.not_not
-- Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
Goal:
α : Type u
G : SimpleGraph α
mp :
  G.IsCompleteMultipartite →
    ∃ (ι : Type u) (V : ι → Type u) (_ : ∀ (i : ι), Nonempty.{u + 1} (V i)),
      Nonempty.{u + 1} (G ≃g completeMultipartiteGraph V)
mpr :
  (∃ (ι : Type u) (V : ι → Type u) (_ : ∀ (i : ι), Nonempty.{u + 1} (V i)),
      Nonempty.{u + 1} (G ≃g completeMultipartiteGraph V)) →
    G.IsCompleteMultipartite
⊢ G.IsCompleteMultipartite ↔
    ∃ (ι : Type u) (V : ι → Type u) (_ : ∀ (i : ι), Nonempty.{u + 1} (V i)),
      Nonempty.{u + 1} (G ≃g completeMultipartiteGraph V)

Tactic:
constructor
-- Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
Goal:
α : Type u
G : SimpleGraph α
h : G.IsCompleteMultipartite
⊢ ∃ (ι : Type u) (V : ι → Type u) (_ : ∀ (i : ι), Nonempty.{u + 1} (V i)),
    Nonempty.{u + 1} (G ≃g completeMultipartiteGraph V)

Tactic:
⟨_, _, fun _ ↦ ⟨_, h.setoid.refl _⟩, ⟨h.iso⟩⟩

Premises used: SimpleGraph.IsCompleteMultipartite.iso, Nonempty.intro, Exists.intro
-- Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
Goal:
α : Type u
G : SimpleGraph α
h : G.IsCompleteMultipartite
⊢ ∃ (ι : Type u) (V : ι → Type u) (_ : ∀ (i : ι), Nonempty.{u + 1} (V i)),
    Nonempty.{u + 1} (G ≃g completeMultipartiteGraph V)

Tactic:
exact ⟨_, _, fun _ ↦ ⟨_, h.setoid.refl _⟩, ⟨h.iso⟩⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
Goal:
α : Type u
G : SimpleGraph α
h :
  ∃ (ι : Type u) (V : ι → Type u) (_ : ∀ (i : ι), Nonempty.{u + 1} (V i)),
    Nonempty.{u + 1} (G ≃g completeMultipartiteGraph V)
mpr :
  ∀ (w : Type u) (w_1 : w → Type u),
    (∀ (i : w), Nonempty.{u + 1} (w_1 i)) → ∀ (e : G ≃g completeMultipartiteGraph w_1), G.IsCompleteMultipartite
⊢ G.IsCompleteMultipartite

Tactic:
obtain ⟨_, _, _, ⟨e⟩⟩ := h