awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.SimpleGraph.Operations
Goal:
V : Type u_1
u v : V
s : Set (Sym2 V)
h : s(u, v) ∈ s
⊢ (edge u v).deleteEdges s = ⊥

Tactic:
simp [edge, Set.diff_subset_iff, h]

Premises used: SimpleGraph.edge, Set.diff_subset_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Operations
Goal:
V : Type u_1
G : SimpleGraph V
u v : V
pos : ∀ (h : u = v), Disjoint G (edge u v) ↔ ¬G.Adj u v
neg : ∀ (h : ¬u = v), Disjoint G (edge u v) ↔ ¬G.Adj u v
⊢ Disjoint G (edge u v) ↔ ¬G.Adj u v

Tactic:
by_cases h : u = v
-- Module: Mathlib.Combinatorics.SimpleGraph.Operations
Goal:
V : Type u_1
G : SimpleGraph V
u v : V
h : u = v
pos : Disjoint G (edge u u) ↔ ¬G.Adj u u
⊢ Disjoint G (edge u v) ↔ ¬G.Adj u v

Tactic:
subst h
-- Module: Mathlib.Combinatorics.SimpleGraph.Operations
Goal:
V : Type u_1
G : SimpleGraph V
u : V
⊢ Disjoint G (edge u u) ↔ ¬G.Adj u u

Tactic:
simp [edge_self_eq_bot]

Premises used: SimpleGraph.edge_self_eq_bot
-- Module: Mathlib.Combinatorics.SimpleGraph.Operations
Goal:
V : Type u_1
G : SimpleGraph V
u v : V
h : ¬u = v
⊢ Disjoint G (edge u v) ↔ ¬G.Adj u v

Tactic:
simp [← disjoint_edgeSet, edgeSet_edge_of_ne h]

Premises used: SimpleGraph.edgeSet_edge_of_ne, SimpleGraph.disjoint_edgeSet
-- Module: Mathlib.Combinatorics.SimpleGraph.Operations
Goal:
V : Type u_1
G : SimpleGraph V
u v : V
h : ¬G.Adj u v
⊢ G \ edge u v = G

Tactic:
simp [disjoint_edge, h]

Premises used: SimpleGraph.disjoint_edge
-- Module: Mathlib.Combinatorics.SimpleGraph.Operations
Goal:
V : Type u_1
G : SimpleGraph V
s t : V
H : (G ⊔ edge s t).Subgraph
h : ¬H.Adj s t
v w : V
hvw : H.spanningCoe.Adj v w
⊢ (G ⊔ edge s t).Adj v w

Tactic:
have := hvw.adj_sub
-- Module: Mathlib.Combinatorics.SimpleGraph.Operations
Goal:
V : Type u_1
G : SimpleGraph V
s t : V
H : (G ⊔ edge s t).Subgraph
h : ¬H.Adj s t
v w : V
hvw : H.spanningCoe.Adj v w
this : (G ⊔ edge s t).Adj v w
⊢ G.Adj v w ∨ (v = s ∧ w = t ∨ v = t ∧ w = s) ∧ v ≠ w

Tactic:
simp only [Subgraph.spanningCoe_adj, SimpleGraph.sup_adj, SimpleGraph.edge_adj] at *

Premises used: SimpleGraph.sup_adj, SimpleGraph.edge_adj, SimpleGraph.Subgraph.spanningCoe_adj
-- Module: Mathlib.Combinatorics.SimpleGraph.Operations
Goal:
V : Type u_1
G : SimpleGraph V
s t : V
H : (G ⊔ edge s t).Subgraph
h : ¬H.Adj s t
v w : V
hvw : H.Adj v w
this : G.Adj v w ∨ (v = s ∧ w = t ∨ v = t ∧ w = s) ∧ v ≠ w
pos : ∀ (hs : s(v, w) = s(s, t)), G.Adj v w
neg : ∀ (hs : ¬s(v, w) = s(s, t)), G.Adj v w
⊢ G.Adj v w

Tactic:
by_cases hs : s(v, w) = s(s, t)
-- Module: Mathlib.Combinatorics.SimpleGraph.Operations
Goal:
V : Type u_1
G : SimpleGraph V
s t : V
H : (G ⊔ edge s t).Subgraph
h : ¬H.Adj s t
v w : V
hvw : H.Adj v w
this : G.Adj v w ∨ (v = s ∧ w = t ∨ v = t ∧ w = s) ∧ v ≠ w
hs : s(v, w) = s(s, t)
⊢ G.Adj v w

Tactic:
(h ((Subgraph.adj_congr_of_sym2 hs).mp hvw)).elim

Premises used: False.elim, SimpleGraph.Subgraph.adj_congr_of_sym2, Iff.mp
-- Module: Mathlib.Combinatorics.SimpleGraph.Operations
Goal:
V : Type u_1
G : SimpleGraph V
s t : V
H : (G ⊔ edge s t).Subgraph
h : ¬H.Adj s t
v w : V
hvw : H.Adj v w
this : G.Adj v w ∨ (v = s ∧ w = t ∨ v = t ∧ w = s) ∧ v ≠ w
hs : s(v, w) = s(s, t)
⊢ G.Adj v w

Tactic:
exact (h ((Subgraph.adj_congr_of_sym2 hs).mp hvw)).elim

Premises used: False.elim, SimpleGraph.Subgraph.adj_congr_of_sym2, Iff.mp
-- Module: Mathlib.Combinatorics.SimpleGraph.Operations
Goal:
V : Type u_1
G : SimpleGraph V
s t : V
H : (G ⊔ edge s t).Subgraph
h : ¬H.Adj s t
v w : V
hvw : H.Adj v w
this : G.Adj v w ∨ (v = s ∧ w = t ∨ v = t ∧ w = s) ∧ v ≠ w
hs : ¬s(v, w) = s(s, t)
⊢ G.Adj v w

Tactic:
aesop
-- Module: Mathlib.Combinatorics.SimpleGraph.Operations
Goal:
V : Type u_1
G : SimpleGraph V
s t : V
inst : Fintype V
inst_1 : DecidableRel G.Adj
inst_2 : DecidableEq V
⊢ Fintype (↑(edgeSet (fromEdgeSet {s(s, t)})) : Type u_1)

Tactic:
infer_instance
-- Module: Mathlib.Combinatorics.SimpleGraph.Operations
Goal:
V : Type u_1
G : SimpleGraph V
s t : V
inst : Fintype V
inst_1 : DecidableRel G.Adj
inst_2 : Fintype (↑(G ⊔ edge s t).edgeSet : Type u_1)
hn : ¬G.Adj s t
h : s ≠ t
⊢ s(s, t) ∉ G.edgeFinset

Tactic:
simp_all
-- Module: Mathlib.Combinatorics.SimpleGraph.Operations
Goal:
V : Type u_1
G : SimpleGraph V
s t : V
inst : Fintype V
inst_1 : DecidableRel G.Adj
inst_2 : Fintype (↑(G ⊔ edge s t).edgeSet : Type u_1)
hn : ¬G.Adj s t
h : s ≠ t
this : DecidableEq V := Classical.decEq V
rw : (edge s t).edgeFinset ∪ G.edgeFinset = {s(s, t)} ∪ G.edgeFinset
⊢ (G ⊔ edge s t).edgeFinset = cons s(s, t) G.edgeFinset ⋯

Tactic:
rw [edgeFinset_sup, cons_eq_insert, insert_eq, union_comm]

Premises used: Finset.insert_eq, Finset.union_comm, SimpleGraph.edgeFinset_sup, Finset.cons_eq_insert
-- Module: Mathlib.Combinatorics.SimpleGraph.Operations
Goal:
V : Type u_1
G : SimpleGraph V
s t : V
inst : Fintype V
inst_1 : DecidableRel G.Adj
inst_2 : Fintype (↑(G ⊔ edge s t).edgeSet : Type u_1)
hn : ¬G.Adj s t
h : s ≠ t
this : DecidableEq V := Classical.decEq V
simp_rw : Set.toFinset {s(s, t)} ∪ G.edgeSet.toFinset = {s(s, t)} ∪ G.edgeSet.toFinset
⊢ (edge s t).edgeFinset ∪ G.edgeFinset = {s(s, t)} ∪ G.edgeFinset

Tactic:
simp_rw [edgeFinset, edgeSet_edge_of_ne h]

Premises used: SimpleGraph.edgeSet_edge_of_ne, SimpleGraph.edgeFinset
-- Module: Mathlib.Combinatorics.SimpleGraph.Operations
Goal:
V : Type u_1
G : SimpleGraph V
s t : V
inst : Fintype V
inst_1 : DecidableRel G.Adj
inst_2 : Fintype (↑(G ⊔ edge s t).edgeSet : Type u_1)
hn : ¬G.Adj s t
h : s ≠ t
this : DecidableEq V := Classical.decEq V
⊢ Set.toFinset {s(s, t)} ∪ G.edgeSet.toFinset = {s(s, t)} ∪ G.edgeSet.toFinset

Tactic:
rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Operations
Goal:
V : Type u_1
G : SimpleGraph V
s t : V
inst : Fintype V
inst_1 : DecidableRel G.Adj
inst_2 : Fintype (↑(G ⊔ edge s t).edgeSet : Type u_1)
hn : ¬G.Adj s t
h : s ≠ t
rw : #(cons s(s, t) G.edgeFinset ⋯) = #G.edgeFinset + 1
rw₁ rw₂ : #G.edgeFinset + 1 = #G.edgeFinset + 1
⊢ #(G ⊔ edge s t).edgeFinset = #G.edgeFinset + 1

Tactic:
rw [G.edgeFinset_sup_edge hn h, card_cons]

Premises used: Finset.card_cons, SimpleGraph.edgeFinset_sup_edge
-- Module: Mathlib.Combinatorics.SimpleGraph.Partition
Goal:
V : Type u
G : SimpleGraph V
P : G.Partition
v : V
⊢ Exists.choose (p := fun (x : Set V) ↦
      (fun (b : Set V) ↦ b ∈ P.parts ∧ v ∈ b) x ∧ ∀ (y : Set V), (fun (b : Set V) ↦ b ∈ P.parts ∧ v ∈ b) y → y = x) ⋯ ∈
    P.parts

Tactic:
obtain ⟨h, -⟩ := (P.isPartition.2 v).choose_spec.1

Premises used: SimpleGraph.Partition.isPartition, Exists.choose_spec, And.right, And.left
-- Module: Mathlib.Combinatorics.SimpleGraph.Partition
Goal:
V : Type u
G : SimpleGraph V
P : G.Partition
v : V
h :
  Exists.choose (p := fun (x : Set V) ↦
      (fun (b : Set V) ↦ b ∈ P.parts ∧ v ∈ b) x ∧ ∀ (y : Set V), (fun (b : Set V) ↦ b ∈ P.parts ∧ v ∈ b) y → y = x) ⋯ ∈
    P.parts
⊢ P.partOfVertex v ∈ P.parts

Tactic:
h

Premises used: Set.Mem, SimpleGraph.Partition.partOfVertex
-- Module: Mathlib.Combinatorics.SimpleGraph.Partition
Goal:
V : Type u
G : SimpleGraph V
P : G.Partition
v : V
h :
  Exists.choose (p := fun (x : Set V) ↦
      (fun (b : Set V) ↦ b ∈ P.parts ∧ v ∈ b) x ∧ ∀ (y : Set V), (fun (b : Set V) ↦ b ∈ P.parts ∧ v ∈ b) y → y = x) ⋯ ∈
    P.parts
⊢ P.partOfVertex v ∈ P.parts

Tactic:
exact h
-- Module: Mathlib.Combinatorics.SimpleGraph.Partition
Goal:
V : Type u
G : SimpleGraph V
P : G.Partition
v : V
⊢ ∀ (y : Set V),
    (fun (b : Set V) ↦ b ∈ P.parts ∧ v ∈ b) y →
      y =
        Exists.choose (p := fun (x : Set V) ↦
          (fun (b : Set V) ↦ b ∈ P.parts ∧ v ∈ b) x ∧ ∀ (y : Set V), (fun (b : Set V) ↦ b ∈ P.parts ∧ v ∈ b) y → y = x)
          ⋯

Tactic:
obtain ⟨⟨_, h⟩, _⟩ := (P.isPartition.2 v).choose_spec

Premises used: SimpleGraph.Partition.isPartition, Exists.choose_spec, And.right
-- Module: Mathlib.Combinatorics.SimpleGraph.Partition
Goal:
V : Type u
G : SimpleGraph V
P : G.Partition
v : V
right :
  ∀ (y : Set V),
    (fun (b : Set V) ↦ b ∈ P.parts ∧ v ∈ b) y →
      y =
        Exists.choose (p := fun (x : Set V) ↦
          (fun (b : Set V) ↦ b ∈ P.parts ∧ v ∈ b) x ∧ ∀ (y : Set V), (fun (b : Set V) ↦ b ∈ P.parts ∧ v ∈ b) y → y = x)
          ⋯
⊢ Exists.choose (p := fun (x : Set V) ↦
      (fun (b : Set V) ↦ b ∈ P.parts ∧ v ∈ b) x ∧ ∀ (y : Set V), (fun (b : Set V) ↦ b ∈ P.parts ∧ v ∈ b) y → y = x) ⋯ ∈
    P.parts

Tactic:
obtain ⟨⟨_, h⟩, _⟩ := (P.isPartition.2 v).choose_spec

Premises used: SimpleGraph.Partition.isPartition, Exists.choose_spec, And.right
-- Module: Mathlib.Combinatorics.SimpleGraph.Partition
Goal:
V : Type u
G : SimpleGraph V
P : G.Partition
v : V
right :
  ∀ (y : Set V),
    (fun (b : Set V) ↦ b ∈ P.parts ∧ v ∈ b) y →
      y =
        Exists.choose (p := fun (x : Set V) ↦
          (fun (b : Set V) ↦ b ∈ P.parts ∧ v ∈ b) x ∧ ∀ (y : Set V), (fun (b : Set V) ↦ b ∈ P.parts ∧ v ∈ b) y → y = x)
          ⋯
left :
  Exists.choose (p := fun (x : Set V) ↦
      (fun (b : Set V) ↦ b ∈ P.parts ∧ v ∈ b) x ∧ ∀ (y : Set V), (fun (b : Set V) ↦ b ∈ P.parts ∧ v ∈ b) y → y = x) ⋯ ∈
    P.parts
⊢ v ∈
    Exists.choose (p := fun (x : Set V) ↦
      (fun (b : Set V) ↦ b ∈ P.parts ∧ v ∈ b) x ∧ ∀ (y : Set V), (fun (b : Set V) ↦ b ∈ P.parts ∧ v ∈ b) y → y = x) ⋯

Tactic:
obtain ⟨⟨_, h⟩, _⟩ := (P.isPartition.2 v).choose_spec

Premises used: SimpleGraph.Partition.isPartition, Exists.choose_spec, And.right
-- Module: Mathlib.Combinatorics.SimpleGraph.Partition
Goal:
V : Type u
G : SimpleGraph V
P : G.Partition
v : V
right :
  ∀ (y : Set V),
    (fun (b : Set V) ↦ b ∈ P.parts ∧ v ∈ b) y →
      y =
        Exists.choose (p := fun (x : Set V) ↦
          (fun (b : Set V) ↦ b ∈ P.parts ∧ v ∈ b) x ∧ ∀ (y : Set V), (fun (b : Set V) ↦ b ∈ P.parts ∧ v ∈ b) y → y = x)
          ⋯
left :
  Exists.choose (p := fun (x : Set V) ↦
      (fun (b : Set V) ↦ b ∈ P.parts ∧ v ∈ b) x ∧ ∀ (y : Set V), (fun (b : Set V) ↦ b ∈ P.parts ∧ v ∈ b) y → y = x) ⋯ ∈
    P.parts
h :
  v ∈
    Exists.choose (p := fun (x : Set V) ↦
      (fun (b : Set V) ↦ b ∈ P.parts ∧ v ∈ b) x ∧ ∀ (y : Set V), (fun (b : Set V) ↦ b ∈ P.parts ∧ v ∈ b) y → y = x) ⋯
⊢ v ∈ P.partOfVertex v

Tactic:
h

Premises used: Set.Mem, SimpleGraph.Partition.partOfVertex
-- Module: Mathlib.Combinatorics.SimpleGraph.Partition
Goal:
V : Type u
G : SimpleGraph V
P : G.Partition
v : V
right :
  ∀ (y : Set V),
    (fun (b : Set V) ↦ b ∈ P.parts ∧ v ∈ b) y →
      y =
        Exists.choose (p := fun (x : Set V) ↦
          (fun (b : Set V) ↦ b ∈ P.parts ∧ v ∈ b) x ∧ ∀ (y : Set V), (fun (b : Set V) ↦ b ∈ P.parts ∧ v ∈ b) y → y = x)
          ⋯
left :
  Exists.choose (p := fun (x : Set V) ↦
      (fun (b : Set V) ↦ b ∈ P.parts ∧ v ∈ b) x ∧ ∀ (y : Set V), (fun (b : Set V) ↦ b ∈ P.parts ∧ v ∈ b) y → y = x) ⋯ ∈
    P.parts
h :
  v ∈
    Exists.choose (p := fun (x : Set V) ↦
      (fun (b : Set V) ↦ b ∈ P.parts ∧ v ∈ b) x ∧ ∀ (y : Set V), (fun (b : Set V) ↦ b ∈ P.parts ∧ v ∈ b) y → y = x) ⋯
⊢ v ∈ P.partOfVertex v

Tactic:
exact h
-- Module: Mathlib.Combinatorics.SimpleGraph.Partition
Goal:
V : Type u
G : SimpleGraph V
P : G.Partition
v w : V
h : G.Adj v w
hn : P.partOfVertex v = P.partOfVertex w
⊢ w ∈ P.partOfVertex w

Tactic:
have hw := P.mem_partOfVertex w
-- Module: Mathlib.Combinatorics.SimpleGraph.Partition
Goal:
V : Type u
G : SimpleGraph V
P : G.Partition
v w : V
h : G.Adj v w
hn : P.partOfVertex v = P.partOfVertex w
hw : w ∈ P.partOfVertex w
⊢ w ∈ P.partOfVertex v

Tactic:
rw [← hn] at hw
-- Module: Mathlib.Combinatorics.SimpleGraph.Partition
Goal:
V : Type u
G : SimpleGraph V
P : G.Partition
v w : V
h : G.Adj v w
hn : P.partOfVertex v = P.partOfVertex w
hw : w ∈ P.partOfVertex v
⊢ False

Tactic:
P.independent _ (P.partOfVertex_mem v) (P.mem_partOfVertex v) hw (G.ne_of_adj h) h

Premises used: SimpleGraph.ne_of_adj, SimpleGraph.Partition.partOfVertex_mem, SimpleGraph.Partition.mem_partOfVertex, SimpleGraph.Partition.independent
-- Module: Mathlib.Combinatorics.SimpleGraph.Partition
Goal:
V : Type u
G : SimpleGraph V
P : G.Partition
v w : V
h : G.Adj v w
hn : P.partOfVertex v = P.partOfVertex w
hw : w ∈ P.partOfVertex v
⊢ False

Tactic:
exact P.independent _ (P.partOfVertex_mem v) (P.mem_partOfVertex v) hw (G.ne_of_adj h) h

Premises used: SimpleGraph.ne_of_adj, SimpleGraph.Partition.partOfVertex_mem, SimpleGraph.Partition.mem_partOfVertex, SimpleGraph.Partition.independent
-- Module: Mathlib.Combinatorics.SimpleGraph.Partition
Goal:
V : Type u
G : SimpleGraph V
P : G.Partition
v w : V
hvw : G.Adj v w
rw : ¬P.partOfVertex v = P.partOfVertex w
⊢ Ne.{u + 1} (α := (↑P.parts : Type u))
    ((fun (v : V) ↦ Subtype.mk (p := fun (x : Set V) ↦ x ∈ P.parts) (P.partOfVertex v) ⋯) v)
    ((fun (v : V) ↦ Subtype.mk (p := fun (x : Set V) ↦ x ∈ P.parts) (P.partOfVertex v) ⋯) w)

Tactic:
rw [Ne, Subtype.mk_eq_mk]

Premises used: Ne, Subtype.mk_eq_mk
-- Module: Mathlib.Combinatorics.SimpleGraph.Partition
Goal:
V : Type u
G : SimpleGraph V
P : G.Partition
v w : V
hvw : G.Adj v w
⊢ ¬P.partOfVertex v = P.partOfVertex w

Tactic:
P.partOfVertex_ne_of_adj hvw

Premises used: SimpleGraph.Partition.partOfVertex_ne_of_adj
-- Module: Mathlib.Combinatorics.SimpleGraph.Partition
Goal:
V : Type u
G : SimpleGraph V
P : G.Partition
v w : V
hvw : G.Adj v w
⊢ ¬P.partOfVertex v = P.partOfVertex w

Tactic:
exact P.partOfVertex_ne_of_adj hvw

Premises used: SimpleGraph.Partition.partOfVertex_ne_of_adj
-- Module: Mathlib.Combinatorics.SimpleGraph.Partition
Goal:
V : Type u
G : SimpleGraph V
P : G.Partition
inst : Fintype (↑P.parts : Type u)
⊢ G.Colorable (Fintype.card.{u} (↑P.parts : Type u))

Tactic:
P.toColoring.colorable

Premises used: SimpleGraph.Partition.toColoring, SimpleGraph.Coloring.colorable
-- Module: Mathlib.Combinatorics.SimpleGraph.Partition
Goal:
V : Type u
G : SimpleGraph V
α : Type v
C : G.Coloring α
c : V
⊢ IsAntichain G.Adj {x : V | (Setoid.ker (⇑C : (a : V) → α) : V → V → Prop) x c}

Tactic:
apply C.isIndepSet_colorClass

Premises used: SimpleGraph.Coloring.isIndepSet_colorClass
-- Module: Mathlib.Combinatorics.SimpleGraph.Partition
Goal:
V : Type u
G : SimpleGraph V
n : ℕ
mp : G.Partitionable n → G.Colorable n
mpr : G.Colorable n → G.Partitionable n
⊢ G.Partitionable n ↔ G.Colorable n

Tactic:
constructor
-- Module: Mathlib.Combinatorics.SimpleGraph.Partition
Goal:
V : Type u
G : SimpleGraph V
n : ℕ
P : G.Partition
hf : P.parts.Finite
hc : hf.toFinset (s := P.parts).card ≤ n
mp : ∀ (this : Fintype (↑P.parts : Type u)), G.Colorable n
⊢ G.Colorable n

Tactic:
have : Fintype P.parts := hf.fintype
-- Module: Mathlib.Combinatorics.SimpleGraph.Partition
Goal:
V : Type u
G : SimpleGraph V
n : ℕ
P : G.Partition
hf : P.parts.Finite
hc : hf.toFinset (s := P.parts).card ≤ n
this : Fintype (↑P.parts : Type u)
⊢ Fintype.card.{u} (↑P.parts : Type u) ≤ n

Tactic:
rw [Set.Finite.card_toFinset hf] at hc

Premises used: Set.Finite.card_toFinset
-- Module: Mathlib.Combinatorics.SimpleGraph.Partition
Goal:
V : Type u
G : SimpleGraph V
n : ℕ
P : G.Partition
hf : P.parts.Finite
this : Fintype (↑P.parts : Type u)
hc : Fintype.card.{u} (↑P.parts : Type u) ≤ n
⊢ G.Colorable n

Tactic:
apply P.colorable.mono hc

Premises used: SimpleGraph.Colorable.mono, SimpleGraph.Partition.colorable
-- Module: Mathlib.Combinatorics.SimpleGraph.Partition
Goal:
V : Type u
G : SimpleGraph V
n : ℕ
C : G.Coloring (Fin n)
⊢ G.Partitionable n

Tactic:
⟨C.toPartition, C.colorClasses_finite, le_trans ?_ (Fintype.card_fin n).le⟩

Premises used: Fintype.card_fin, SimpleGraph.Partitionable, SimpleGraph.Coloring.colorClasses_finite, Eq.le, SimpleGraph.Coloring.toPartition, Exists.intro, le_trans
-- Module: Mathlib.Combinatorics.SimpleGraph.Partition
Goal:
V : Type u
G : SimpleGraph V
n : ℕ
C : G.Coloring (Fin n)
mpr : ⋯.toFinset (s := C.toPartition.parts).card ≤ Fintype.card (Fin n)
⊢ G.Partitionable n

Tactic:
refine ⟨C.toPartition, C.colorClasses_finite, le_trans ?_ (Fintype.card_fin n).le⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Partition
Goal:
V : Type u
G : SimpleGraph V
n : ℕ
C : G.Coloring (Fin n)
⊢ C.toPartition.parts.Finite

Tactic:
generalize_proofs h
-- Module: Mathlib.Combinatorics.SimpleGraph.Partition
Goal:
V : Type u
G : SimpleGraph V
n : ℕ
C : G.Coloring (Fin n)
h : C.toPartition.parts.Finite
⊢ C.colorClasses.Finite

Tactic:
change Set.Finite (Coloring.colorClasses C) at h

Premises used: Set.Finite, SimpleGraph.Coloring.colorClasses
-- Module: Mathlib.Combinatorics.SimpleGraph.Partition
Goal:
V : Type u
G : SimpleGraph V
n : ℕ
C : G.Coloring (Fin n)
h : C.colorClasses.Finite
mpr : ∀ (this : Fintype (↑C.colorClasses : Type u)), h.toFinset (s := C.toPartition.parts).card ≤ Fintype.card (Fin n)
⊢ h.toFinset (s := C.toPartition.parts).card ≤ Fintype.card (Fin n)

Tactic:
have : Fintype C.colorClasses := C.colorClasses_finite.fintype
-- Module: Mathlib.Combinatorics.SimpleGraph.Partition
Goal:
V : Type u
G : SimpleGraph V
n : ℕ
C : G.Coloring (Fin n)
h : C.colorClasses.Finite
this : Fintype (↑C.colorClasses : Type u)
mpr : Fintype.card.{u} (↑C.colorClasses : Type u) ≤ Fintype.card (Fin n)
⊢ h.toFinset (s := C.toPartition.parts).card ≤ Fintype.card (Fin n)

Tactic:
rw [h.card_toFinset]

Premises used: Set.Finite.card_toFinset
-- Module: Mathlib.Combinatorics.SimpleGraph.Partition
Goal:
V : Type u
G : SimpleGraph V
n : ℕ
C : G.Coloring (Fin n)
h : C.colorClasses.Finite
this : Fintype (↑C.colorClasses : Type u)
⊢ Fintype.card.{u} (↑C.colorClasses : Type u) ≤ Fintype.card (Fin n)

Tactic:
C.card_colorClasses_le

Premises used: SimpleGraph.Coloring.card_colorClasses_le
-- Module: Mathlib.Combinatorics.SimpleGraph.Partition
Goal:
V : Type u
G : SimpleGraph V
n : ℕ
C : G.Coloring (Fin n)
h : C.colorClasses.Finite
this : Fintype (↑C.colorClasses : Type u)
⊢ Fintype.card.{u} (↑C.colorClasses : Type u) ≤ Fintype.card (Fin n)

Tactic:
exact C.card_colorClasses_le

Premises used: SimpleGraph.Coloring.card_colorClasses_le
-- Module: Mathlib.Combinatorics.SimpleGraph.Prod
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
V : Type u_4
V₁ : Type u_5
V₂ : Type u_6
W : Type u_7
W₁ : Type u_8
W₂ : Type u_9
G_1 : SimpleGraph α
H_1 : SimpleGraph β
G : SimpleGraph α
H : SimpleGraph β
x y : α × β
⊢ (fun (x y : α × β) ↦ G.Adj x.1 y.1 ∧ x.2 = y.2 ∨ H.Adj x.2 y.2 ∧ x.1 = y.1) x y →
    (fun (x y : α × β) ↦ G.Adj x.1 y.1 ∧ x.2 = y.2 ∨ H.Adj x.2 y.2 ∧ x.1 = y.1) y x

Tactic:
simp [and_comm, eq_comm, adj_comm]

Premises used: and_comm, eq_comm, SimpleGraph.adj_comm
-- Module: Mathlib.Combinatorics.SimpleGraph.Prod
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
V : Type u_4
V₁ : Type u_5
V₂ : Type u_6
W : Type u_7
W₁ : Type u_8
W₂ : Type u_9
G_1 : SimpleGraph α
H_1 : SimpleGraph β
G : SimpleGraph α
H : SimpleGraph β
x : α × β
⊢ ¬(G.Adj x.1 x.1 ∧ x.2 = x.2 ∨ H.Adj x.2 x.2 ∧ x.1 = x.1)

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Prod
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
x y : α × β
⊢ (G □ H).Adj x y ↔ G.Adj x.1 y.1 ∧ x.2 = y.2 ∨ H.Adj x.2 y.2 ∧ x.1 = y.1

Tactic:
Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Prod
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
a₁ : α
b : β
a₂ : α
⊢ (G □ H).Adj (a₁, b) (a₂, b) ↔ G.Adj a₁ a₂

Tactic:
simp only [boxProd_adj, and_true, SimpleGraph.irrefl, false_and, or_false]

Premises used: and_true, false_and, SimpleGraph.boxProd_adj, SimpleGraph.irrefl, or_false
-- Module: Mathlib.Combinatorics.SimpleGraph.Prod
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
a : α
b₁ b₂ : β
⊢ (G □ H).Adj (a, b₁) (a, b₂) ↔ H.Adj b₁ b₂

Tactic:
simp only [boxProd_adj, SimpleGraph.irrefl, false_and, and_true, false_or]

Premises used: and_true, false_and, false_or, SimpleGraph.boxProd_adj, SimpleGraph.irrefl
-- Module: Mathlib.Combinatorics.SimpleGraph.Prod
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
x : α × β
h :
  ∀ (a' : α) (b' : β),
    (a', b') ∈ (G □ H).neighborSet x ↔
      (a', b') ∈ SProd.sprod (β := Set β) (G.neighborSet x.1) {x.2} ∪ SProd.sprod (α := Set α) {x.1} (H.neighborSet x.2)
⊢ (G □ H).neighborSet x =
    SProd.sprod (β := Set β) (G.neighborSet x.1) {x.2} ∪ SProd.sprod (α := Set α) {x.1} (H.neighborSet x.2)

Tactic:
ext ⟨a', b'⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Prod
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
x : α × β
a' : α
b' : β
h : G.Adj x.1 a' ∧ x.2 = b' ∨ H.Adj x.2 b' ∧ x.1 = a' ↔ G.Adj x.1 a' ∧ b' = x.2 ∨ a' = x.1 ∧ H.Adj x.2 b'
⊢ (a', b') ∈ (G □ H).neighborSet x ↔
    (a', b') ∈ SProd.sprod (β := Set β) (G.neighborSet x.1) {x.2} ∪ SProd.sprod (α := Set α) {x.1} (H.neighborSet x.2)

Tactic:
simp only [mem_neighborSet, Set.mem_union, boxProd_adj, Set.mem_prod, Set.mem_singleton_iff]

Premises used: Set.mem_union, SimpleGraph.mem_neighborSet, Set.mem_prod, Set.mem_singleton_iff, SimpleGraph.boxProd_adj
-- Module: Mathlib.Combinatorics.SimpleGraph.Prod
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
x : α × β
a' : α
b' : β
⊢ G.Adj x.1 a' ∧ x.2 = b' ∨ H.Adj x.2 b' ∧ x.1 = a' ↔ G.Adj x.1 a' ∧ b' = x.2 ∨ a' = x.1 ∧ H.Adj x.2 b'

Tactic:
simp only [eq_comm, and_comm]

Premises used: and_comm, eq_comm
-- Module: Mathlib.Combinatorics.SimpleGraph.Prod
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
V : Type u_4
V₁ : Type u_5
V₂ : Type u_6
W : Type u_7
W₁ : Type u_8
W₂ : Type u_9
G : SimpleGraph α
H : SimpleGraph β
I : SimpleGraph γ
x y : (α × β) × γ
⊢ (G □ (H □ I)).Adj ((Equiv.prodAssoc α β γ : (a : (α × β) × γ) → α × β × γ) x)
      ((Equiv.prodAssoc α β γ : (a : (α × β) × γ) → α × β × γ) y) ↔
    (G □ H □ I).Adj x y

Tactic:
simp only [boxProd_adj, Equiv.prodAssoc_apply, or_and_right, or_assoc, Prod.ext_iff,
      and_assoc, @and_comm (x.fst.fst = _)]

Premises used: Equiv.prodAssoc_apply, Prod.ext_iff, and_comm, and_assoc, SimpleGraph.boxProd_adj, or_and_right, or_assoc
-- Module: Mathlib.Combinatorics.SimpleGraph.Prod
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
V : Type u_4
V₁ : Type u_5
V₂ : Type u_6
W : Type u_7
W₁ : Type u_8
W₂ : Type u_9
G_1 : SimpleGraph α
H : SimpleGraph β
G : SimpleGraph V
H₁ : SimpleGraph W₁
H₂ : SimpleGraph W₂
⊢ ∀ {a b : V × (W₁ ⊕ W₂)},
    (G □ H₁ ⊕g G □ H₂).Adj ((Equiv.prodSumDistrib V W₁ W₂ : (a : V × (W₁ ⊕ W₂)) → V × W₁ ⊕ V × W₂) a)
        ((Equiv.prodSumDistrib V W₁ W₂ : (a : V × (W₁ ⊕ W₂)) → V × W₁ ⊕ V × W₂) b) ↔
      (G □ (H₁ ⊕g H₂)).Adj a b

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Prod
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
V : Type u_4
V₁ : Type u_5
V₂ : Type u_6
W : Type u_7
W₁ : Type u_8
W₂ : Type u_9
G : SimpleGraph α
H_1 : SimpleGraph β
G₁ : SimpleGraph V₁
G₂ : SimpleGraph V₂
H : SimpleGraph W
⊢ ∀ {a b : (V₁ ⊕ V₂) × W},
    (G₁ □ H ⊕g G₂ □ H).Adj ((Equiv.sumProdDistrib V₁ V₂ W : (a : (V₁ ⊕ V₂) × W) → V₁ × W ⊕ V₂ × W) a)
        ((Equiv.sumProdDistrib V₁ V₂ W : (a : (V₁ ⊕ V₂) × W) → V₁ × W ⊕ V₂ × W) b) ↔
      ((G₁ ⊕g G₂) □ H).Adj a b

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Prod
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
inst : DecidableEq β
inst_1 : DecidableRel G.Adj
a₁ a₂ : α
b : β
x z y : α
h : G.Adj x y
w : G.Walk y z
rw : cons ⋯ (Walk.boxProdLeft H b w).ofBoxProdLeft = cons' x y z h w
hc :
  G.Adj (x, b).1 (((G.boxProdLeft H b).toHom : (a : α) → α × β) y).1 ∧
    (x, b).2 = (((G.boxProdLeft H b).toHom : (a : α) → α × β) y).2
⊢ (Walk.boxProdLeft H b (cons' x y z h w)).ofBoxProdLeft = cons' x y z h w

Tactic:
rw [Walk.boxProdLeft, map_cons, ofBoxProdLeft, Or.by_cases, dif_pos, ← Walk.boxProdLeft]

Premises used: SimpleGraph.Walk.boxProdLeft, dif_pos, SimpleGraph.Walk.ofBoxProdLeft, Or.by_cases, SimpleGraph.Walk.map_cons
-- Module: Mathlib.Combinatorics.SimpleGraph.Prod
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
inst : DecidableEq β
inst_1 : DecidableRel G.Adj
a₁ a₂ : α
b : β
x z y : α
h : G.Adj x y
w : G.Walk y z
⊢ cons ⋯ (Walk.boxProdLeft H b w).ofBoxProdLeft = cons' x y z h w

Tactic:
simp [ofBoxProdLeft_boxProdLeft]
-- Module: Mathlib.Combinatorics.SimpleGraph.Prod
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
inst : DecidableEq β
inst_1 : DecidableRel G.Adj
a₁ a₂ : α
b : β
x z y : α
h : G.Adj x y
w : G.Walk y z
⊢ G.Adj (x, b).1 (((G.boxProdLeft H b).toHom : (a : α) → α × β) y).1 ∧
    (x, b).2 = (((G.boxProdLeft H b).toHom : (a : α) → α × β) y).2

Tactic:
⟨h, rfl⟩

Premises used: And.intro, rfl