awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
Goal:
α : Type u
G : SimpleGraph α
w : Type u
w_1 : w → Type u
w_2 : ∀ (i : w), Nonempty.{u + 1} (w_1 i)
e : G ≃g completeMultipartiteGraph w_1
⊢ G.IsCompleteMultipartite

Tactic:
⟨fun _ _ _ h1 h2 ↦ ?_⟩

Premises used: IsTrans.mk, SimpleGraph.IsCompleteMultipartite
-- Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
Goal:
α : Type u
G : SimpleGraph α
w : Type u
w_1 : w → Type u
w_2 : ∀ (i : w), Nonempty.{u + 1} (w_1 i)
e : G ≃g completeMultipartiteGraph w_1
mpr : ∀ (x x_1 x_2 : α) (h1 : ¬G.Adj x x_1) (h2 : ¬G.Adj x_1 x_2), ¬G.Adj x x_2
⊢ G.IsCompleteMultipartite

Tactic:
refine ⟨fun _ _ _ h1 h2 ↦ ?_⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
Goal:
α : Type u
G : SimpleGraph α
w : Type u
w_1 : w → Type u
w_2 : ∀ (i : w), Nonempty.{u + 1} (w_1 i)
e : G ≃g completeMultipartiteGraph w_1
x x_1 x_2 : α
h1 : ¬G.Adj x x_1
h2 : ¬G.Adj x_1 x_2
mpr :
  ∀
    (h1 :
      ¬(completeMultipartiteGraph w_1).Adj ((e : (a : α) → (i : w) × w_1 i) x) ((e : (a : α) → (i : w) × w_1 i) x_1))
    (h2 :
      ¬(completeMultipartiteGraph w_1).Adj ((e : (a : α) → (i : w) × w_1 i) x_1) ((e : (a : α) → (i : w) × w_1 i) x_2)),
    ¬(completeMultipartiteGraph w_1).Adj ((e : (a : α) → (i : w) × w_1 i) x) ((e : (a : α) → (i : w) × w_1 i) x_2)
⊢ ¬G.Adj x x_2

Tactic:
rw [← e.map_rel_iff] at *

Premises used: RelIso.map_rel_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
Goal:
α : Type u
G : SimpleGraph α
w : Type u
w_1 : w → Type u
w_2 : ∀ (i : w), Nonempty.{u + 1} (w_1 i)
e : G ≃g completeMultipartiteGraph w_1
x x_1 x_2 : α
h1 : ¬(completeMultipartiteGraph w_1).Adj ((e : (a : α) → (i : w) × w_1 i) x) ((e : (a : α) → (i : w) × w_1 i) x_1)
h2 : ¬(completeMultipartiteGraph w_1).Adj ((e : (a : α) → (i : w) × w_1 i) x_1) ((e : (a : α) → (i : w) × w_1 i) x_2)
⊢ ¬(completeMultipartiteGraph w_1).Adj ((e : (a : α) → (i : w) × w_1 i) x) ((e : (a : α) → (i : w) × w_1 i) x_2)

Tactic:
completeMultipartiteGraph.isCompleteMultipartite _ |>.trans _ _ _ h1 h2

Premises used: IsTrans.trans
-- Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
Goal:
α : Type u
G : SimpleGraph α
w : Type u
w_1 : w → Type u
w_2 : ∀ (i : w), Nonempty.{u + 1} (w_1 i)
e : G ≃g completeMultipartiteGraph w_1
x x_1 x_2 : α
h1 : ¬(completeMultipartiteGraph w_1).Adj ((e : (a : α) → (i : w) × w_1 i) x) ((e : (a : α) → (i : w) × w_1 i) x_1)
h2 : ¬(completeMultipartiteGraph w_1).Adj ((e : (a : α) → (i : w) × w_1 i) x_1) ((e : (a : α) → (i : w) × w_1 i) x_2)
⊢ ¬(completeMultipartiteGraph w_1).Adj ((e : (a : α) → (i : w) × w_1 i) x) ((e : (a : α) → (i : w) × w_1 i) x_2)

Tactic:
exact completeMultipartiteGraph.isCompleteMultipartite _ |>.trans _ _ _ h1 h2

Premises used: IsTrans.trans
-- Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
Goal:
α : Type u
G : SimpleGraph α
n : ℕ
h : G.IsCompleteMultipartite
hc : G.CliqueFree n
⊢ G.Colorable (n - 1)

Tactic:
(completeMultipartiteGraph.colorable_of_cliqueFree _ (fun _ ↦ ⟨_, h.setoid.refl _⟩) <|
    hc.comap h.iso.symm.isContained).of_hom h.iso

Premises used: SimpleGraph.Colorable.of_hom, SimpleGraph.IsCompleteMultipartite.iso, SimpleGraph.Iso.isContained, SimpleGraph.Iso.symm, SimpleGraph.CliqueFree.comap, SimpleGraph.completeMultipartiteGraph.colorable_of_cliqueFree
-- Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
Goal:
α : Type u
G : SimpleGraph α
v w₁ w₂ : α
h2 : G.IsPathGraph3Compl v w₁ w₂
⊢ v ≠ w₁

Tactic:
fun h ↦ h2.not_adj_snd (h.symm ▸ h2.adj)

Premises used: Eq.rec, SimpleGraph.IsPathGraph3Compl.not_adj_snd, Eq.symm, Not, SimpleGraph.IsPathGraph3Compl.adj
-- Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
Goal:
α : Type u
G : SimpleGraph α
v w₁ w₂ : α
h2 : G.IsPathGraph3Compl v w₁ w₂
⊢ v ≠ w₂

Tactic:
fun h ↦ h2.not_adj_fst (h ▸ h2.adj.symm)

Premises used: SimpleGraph.Adj.symm, Eq.rec, SimpleGraph.IsPathGraph3Compl.not_adj_fst, Eq.symm, Not, SimpleGraph.IsPathGraph3Compl.adj
-- Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
Goal:
α : Type u
G : SimpleGraph α
v w₁ w₂ : α
h2 : G.IsPathGraph3Compl v w₁ w₂
⊢ w₁ ≠ w₂

Tactic:
h2.adj.ne

Premises used: SimpleGraph.Adj.ne, SimpleGraph.IsPathGraph3Compl.adj
-- Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
Goal:
α : Type u
G : SimpleGraph α
v w₁ w₂ : α
h : G.IsPathGraph3Compl v w₁ w₂
⊢ G.Adj w₁ w₂

Tactic:
obtain ⟨h1, h2, h3⟩ := h
-- Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
Goal:
α : Type u
G : SimpleGraph α
v w₁ w₂ : α
h : G.IsPathGraph3Compl v w₁ w₂
h1 : G.Adj w₁ w₂
⊢ ¬G.Adj v w₁

Tactic:
obtain ⟨h1, h2, h3⟩ := h
-- Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
Goal:
α : Type u
G : SimpleGraph α
v w₁ w₂ : α
h : G.IsPathGraph3Compl v w₁ w₂
h1 : G.Adj w₁ w₂
h2 : ¬G.Adj v w₁
⊢ ¬G.Adj v w₂

Tactic:
obtain ⟨h1, h2, h3⟩ := h
-- Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
Goal:
α : Type u
G : SimpleGraph α
v w₁ w₂ : α
h1 : G.Adj w₁ w₂
h2 : ¬G.Adj v w₁
h3 : ¬G.Adj v w₂
⊢ G.IsPathGraph3Compl v w₂ w₁

Tactic:
⟨h1.symm, h3, h2⟩

Premises used: SimpleGraph.Adj.symm, SimpleGraph.IsPathGraph3Compl.mk
-- Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
Goal:
α : Type u
G : SimpleGraph α
v w₁ w₂ : α
h1 : G.Adj w₁ w₂
h2 : ¬G.Adj v w₁
h3 : ¬G.Adj v w₂
⊢ G.IsPathGraph3Compl v w₂ w₁

Tactic:
exact ⟨h1.symm, h3, h2⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
Goal:
α : Type u
G : SimpleGraph α
h : ¬G.IsCompleteMultipartite
⊢ ¬∀ (a b c : α), ¬G.Adj a b → ¬G.Adj b c → ¬G.Adj a c

Tactic:
apply mt IsTrans.mk at h

Premises used: IsTrans.mk, mt
-- Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
Goal:
α : Type u
G : SimpleGraph α
h : ¬∀ (a b c : α), ¬G.Adj a b → ¬G.Adj b c → ¬G.Adj a c
⊢ ∃ (a : α) (b : α) (c : α), ¬G.Adj a b ∧ ¬G.Adj b c ∧ G.Adj a c

Tactic:
push Not at h

Premises used: Not
-- Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
Goal:
α : Type u
G : SimpleGraph α
h : ∃ (a : α) (b : α) (c : α), ¬G.Adj a b ∧ ¬G.Adj b c ∧ G.Adj a c
obtain :
  ∀ (w w_1 w_2 : α) (h1 : ¬G.Adj w w_1) (h2 : ¬G.Adj w_1 w_2) (h3 : G.Adj w w_2),
    ∃ (v : α) (w₁ : α) (w₂ : α), G.IsPathGraph3Compl v w₁ w₂
⊢ ∃ (v : α) (w₁ : α) (w₂ : α), G.IsPathGraph3Compl v w₁ w₂

Tactic:
obtain ⟨_, _, _, h1, h2, h3⟩ := h
-- Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
Goal:
α : Type u
G : SimpleGraph α
w w_1 w_2 : α
h1 : ¬G.Adj w w_1
h2 : ¬G.Adj w_1 w_2
h3 : G.Adj w w_2
⊢ ¬G.Adj w_1 w

Tactic:
rw [adj_comm] at h1

Premises used: SimpleGraph.adj_comm
-- Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
Goal:
α : Type u
G : SimpleGraph α
w w_1 w_2 : α
h1 : ¬G.Adj w w_1
h2 : ¬G.Adj w_1 w_2
h3 : G.Adj w w_2
h1₁ : ¬G.Adj w_1 w
⊢ ¬G.Adj w_1 w_2

Tactic:
rw [adj_comm] at h1

Premises used: SimpleGraph.adj_comm
-- Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
Goal:
α : Type u
G : SimpleGraph α
w w_1 w_2 : α
h1 : ¬G.Adj w w_1
h2 : ¬G.Adj w_1 w_2
h3 : G.Adj w w_2
h1₁ : ¬G.Adj w_1 w
h2₁ : ¬G.Adj w_1 w_2
⊢ G.Adj w w_2

Tactic:
rw [adj_comm] at h1

Premises used: SimpleGraph.adj_comm
-- Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
Goal:
α : Type u
G : SimpleGraph α
w w_1 w_2 : α
h1 : ¬G.Adj w_1 w
h2 : ¬G.Adj w_1 w_2
h3 : G.Adj w w_2
⊢ ∃ (v : α) (w₁ : α) (w₂ : α), G.IsPathGraph3Compl v w₁ w₂

Tactic:
⟨_, _, _, h3, h1, h2⟩

Premises used: SimpleGraph.IsPathGraph3Compl.mk, Exists.intro
-- Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
Goal:
α : Type u
G : SimpleGraph α
w w_1 w_2 : α
h1 : ¬G.Adj w_1 w
h2 : ¬G.Adj w_1 w_2
h3 : G.Adj w w_2
⊢ ∃ (v : α) (w₁ : α) (w₂ : α), G.IsPathGraph3Compl v w₁ w₂

Tactic:
exact ⟨_, _, _, h3, h1, h2⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
Goal:
α : Type u
G : SimpleGraph α
h_1 : ∃ (v : α) (w₁ : α) (w₂ : α), G.IsPathGraph3Compl v w₁ w₂
w w_1 w_2 : α
h1 : G.Adj w_1 w_2
h2 : ¬G.Adj w w_1
h3 : ¬G.Adj w w_2
h : G.IsCompleteMultipartite
rwa rwa₁ rwa₂ rwa₃ : ∀ (h2 : ¬G.Adj w_1 w) (h3 : ¬G.Adj w w_2) (h : G.IsCompleteMultipartite), ¬G.Adj w_1 w
⊢ ¬G.Adj w_1 w

Tactic:
rwa [adj_comm] at h2

Premises used: SimpleGraph.adj_comm
-- Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
Goal:
α : Type u
G : SimpleGraph α
s : Set α
v w₁ w₂ : α
h : G.IsPathGraph3Compl v w₁ w₂
a₁ : Fin 3
_ :
  ∀ ⦃a₂ : Fin 3⦄,
    Eq.{u + 1} (α := α)
        ((fun (x : Fin 3) ↦
            (match (motive := Fin 3 → α) x with
              | 0 => w₁
              | 1 => v
              | 2 => w₂ :
              α))
          a₁)
        ((fun (x : Fin 3) ↦
            (match (motive := Fin 3 → α) x with
              | 0 => w₁
              | 1 => v
              | 2 => w₂ :
              α))
          a₂) →
      a₁ = a₂
⊢ ∀ ⦃a₂ : Fin 3⦄,
    Eq.{u + 1} (α := α)
        ((fun (x : Fin 3) ↦
            (match (motive := Fin 3 → α) x with
              | 0 => w₁
              | 1 => v
              | 2 => w₂ :
              α))
          a₁)
        ((fun (x : Fin 3) ↦
            (match (motive := Fin 3 → α) x with
              | 0 => w₁
              | 1 => v
              | 2 => w₂ :
              α))
          a₂) →
      a₁ = a₂

Tactic:
_
-- Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
Goal:
α : Type u
G : SimpleGraph α
s : Set α
v w₁ w₂ : α
h : G.IsPathGraph3Compl v w₁ w₂
a₁ a₂ : Fin 3
_ :
  Eq.{u + 1} (α := α)
      ((fun (x : Fin 3) ↦
          (match (motive := Fin 3 → α) x with
            | 0 => w₁
            | 1 => v
            | 2 => w₂ :
            α))
        a₁)
      ((fun (x : Fin 3) ↦
          (match (motive := Fin 3 → α) x with
            | 0 => w₁
            | 1 => v
            | 2 => w₂ :
            α))
        a₂) →
    a₁ = a₂
⊢ Eq.{u + 1} (α := α)
      ((fun (x : Fin 3) ↦
          (match (motive := Fin 3 → α) x with
            | 0 => w₁
            | 1 => v
            | 2 => w₂ :
            α))
        a₁)
      ((fun (x : Fin 3) ↦
          (match (motive := Fin 3 → α) x with
            | 0 => w₁
            | 1 => v
            | 2 => w₂ :
            α))
        a₂) →
    a₁ = a₂

Tactic:
_
-- Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
Goal:
α : Type u
G : SimpleGraph α
s : Set α
v w₁ w₂ : α
h : G.IsPathGraph3Compl v w₁ w₂
a₁ a₂ : Fin 3
h_1 :
  Eq.{u + 1} (α := α)
    ((fun (x : Fin 3) ↦
        (match (motive := Fin 3 → α) x with
          | 0 => w₁
          | 1 => v
          | 2 => w₂ :
          α))
      a₁)
    ((fun (x : Fin 3) ↦
        (match (motive := Fin 3 → α) x with
          | 0 => w₁
          | 1 => v
          | 2 => w₂ :
          α))
      a₂)
⊢ v ≠ w₁

Tactic:
have := h.ne_fst
-- Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
Goal:
α : Type u
G : SimpleGraph α
s : Set α
v w₁ w₂ : α
h : G.IsPathGraph3Compl v w₁ w₂
a₁ a₂ : Fin 3
h_1 :
  Eq.{u + 1} (α := α)
    ((fun (x : Fin 3) ↦
        (match (motive := Fin 3 → α) x with
          | 0 => w₁
          | 1 => v
          | 2 => w₂ :
          α))
      a₁)
    ((fun (x : Fin 3) ↦
        (match (motive := Fin 3 → α) x with
          | 0 => w₁
          | 1 => v
          | 2 => w₂ :
          α))
      a₂)
this : v ≠ w₁
⊢ v ≠ w₂

Tactic:
have := h.ne_snd
-- Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
Goal:
α : Type u
G : SimpleGraph α
s : Set α
v w₁ w₂ : α
h : G.IsPathGraph3Compl v w₁ w₂
a₁ a₂ : Fin 3
h_1 :
  Eq.{u + 1} (α := α)
    ((fun (x : Fin 3) ↦
        (match (motive := Fin 3 → α) x with
          | 0 => w₁
          | 1 => v
          | 2 => w₂ :
          α))
      a₁)
    ((fun (x : Fin 3) ↦
        (match (motive := Fin 3 → α) x with
          | 0 => w₁
          | 1 => v
          | 2 => w₂ :
          α))
      a₂)
this_1 : v ≠ w₁
this : v ≠ w₂
⊢ w₁ ≠ w₂

Tactic:
have := h.adj.ne
-- Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
Goal:
α : Type u
G : SimpleGraph α
s : Set α
v w₁ w₂ : α
h : G.IsPathGraph3Compl v w₁ w₂
a₁ a₂ : Fin 3
h_1 :
  Eq.{u + 1} (α := α)
    ((fun (x : Fin 3) ↦
        (match (motive := Fin 3 → α) x with
          | 0 => w₁
          | 1 => v
          | 2 => w₂ :
          α))
      a₁)
    ((fun (x : Fin 3) ↦
        (match (motive := Fin 3 → α) x with
          | 0 => w₁
          | 1 => v
          | 2 => w₂ :
          α))
      a₂)
this_1 : v ≠ w₁
this_2 : v ≠ w₂
this : w₁ ≠ w₂
⊢ a₁ = a₂

Tactic:
aesop
-- Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
Goal:
α : Type u
G : SimpleGraph α
s : Set α
v w₁ w₂ : α
h : G.IsPathGraph3Compl v w₁ w₂
a : Fin 3
_ :
  ∀ {b : Fin 3},
    G.Adj
        (({
              toFun := fun (x : Fin 3) ↦
                match (motive := Fin 3 → α) x with
                | 0 => w₁
                | 1 => v
                | 2 => w₂,
              inj' := ⋯ : Fin 3 ↪ α } :
            (a : Fin 3) → α)
          a)
        (({
              toFun := fun (x : Fin 3) ↦
                match (motive := Fin 3 → α) x with
                | 0 => w₁
                | 1 => v
                | 2 => w₂,
              inj' := ⋯ : Fin 3 ↪ α } :
            (a : Fin 3) → α)
          b) ↔
      Adj (pathGraph 3)ᶜ a b
⊢ ∀ {b : Fin 3},
    G.Adj
        (({
              toFun := fun (x : Fin 3) ↦
                match (motive := Fin 3 → α) x with
                | 0 => w₁
                | 1 => v
                | 2 => w₂,
              inj' := ⋯ : Fin 3 ↪ α } :
            (a : Fin 3) → α)
          a)
        (({
              toFun := fun (x : Fin 3) ↦
                match (motive := Fin 3 → α) x with
                | 0 => w₁
                | 1 => v
                | 2 => w₂,
              inj' := ⋯ : Fin 3 ↪ α } :
            (a : Fin 3) → α)
          b) ↔
      Adj (pathGraph 3)ᶜ a b

Tactic:
_
-- Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
Goal:
α : Type u
G : SimpleGraph α
s : Set α
v w₁ w₂ : α
h : G.IsPathGraph3Compl v w₁ w₂
a b : Fin 3
simp_rw :
  G.Adj
      (match (motive := Fin 3 → α) a with
      | 0 => w₁
      | 1 => v
      | 2 => w₂)
      (match (motive := Fin 3 → α) b with
      | 0 => w₁
      | 1 => v
      | 2 => w₂) ↔
    ¬a = b ∧ ¬(↑a : ℕ) + 1 = (↑b : ℕ) ∧ ¬(↑b : ℕ) + 1 = (↑a : ℕ)
⊢ G.Adj
      (({
            toFun := fun (x : Fin 3) ↦
              match (motive := Fin 3 → α) x with
              | 0 => w₁
              | 1 => v
              | 2 => w₂,
            inj' := ⋯ : Fin 3 ↪ α } :
          (a : Fin 3) → α)
        a)
      (({
            toFun := fun (x : Fin 3) ↦
              match (motive := Fin 3 → α) x with
              | 0 => w₁
              | 1 => v
              | 2 => w₂,
            inj' := ⋯ : Fin 3 ↪ α } :
          (a : Fin 3) → α)
        b) ↔
    Adj (pathGraph 3)ᶜ a b

Tactic:
simp_rw [Embedding.coeFn_mk, compl_adj, ne_eq, pathGraph_adj, not_or]

Premises used: SimpleGraph.pathGraph_adj, SimpleGraph.compl_adj, ne_eq, not_or, Function.Embedding.coeFn_mk
-- Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
Goal:
α : Type u
G : SimpleGraph α
s : Set α
v w₁ w₂ : α
h : G.IsPathGraph3Compl v w₁ w₂
a b : Fin 3
⊢ G.Adj w₁ w₂

Tactic:
have := h.adj
-- Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
Goal:
α : Type u
G : SimpleGraph α
s : Set α
v w₁ w₂ : α
h : G.IsPathGraph3Compl v w₁ w₂
a b : Fin 3
this : G.Adj w₁ w₂
⊢ G.Adj w₂ w₁

Tactic:
have := h.adj.symm
-- Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
Goal:
α : Type u
G : SimpleGraph α
s : Set α
v w₁ w₂ : α
h : G.IsPathGraph3Compl v w₁ w₂
a b : Fin 3
this_1 : G.Adj w₁ w₂
this : G.Adj w₂ w₁
⊢ ¬G.Adj v w₁

Tactic:
have h1 := h.not_adj_fst
-- Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
Goal:
α : Type u
G : SimpleGraph α
s : Set α
v w₁ w₂ : α
h : G.IsPathGraph3Compl v w₁ w₂
a b : Fin 3
this_1 : G.Adj w₁ w₂
this : G.Adj w₂ w₁
h1 : ¬G.Adj v w₁
⊢ ¬G.Adj v w₂

Tactic:
have h2 := h.not_adj_snd
-- Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
Goal:
α : Type u
G : SimpleGraph α
s : Set α
v w₁ w₂ : α
h : G.IsPathGraph3Compl v w₁ w₂
a b : Fin 3
this_1 : G.Adj w₁ w₂
this : G.Adj w₂ w₁
h1 : ¬G.Adj v w₁
h2 : ¬G.Adj v w₂
⊢ ¬G.Adj w₁ v

Tactic:
rw [adj_comm] at h1 h2

Premises used: SimpleGraph.adj_comm
-- Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
Goal:
α : Type u
G : SimpleGraph α
s : Set α
v w₁ w₂ : α
h : G.IsPathGraph3Compl v w₁ w₂
a b : Fin 3
this_1 : G.Adj w₁ w₂
this : G.Adj w₂ w₁
h1 : ¬G.Adj v w₁
h2 : ¬G.Adj v w₂
h1₁ : ¬G.Adj w₁ v
⊢ ¬G.Adj w₂ v

Tactic:
rw [adj_comm] at h1 h2

Premises used: SimpleGraph.adj_comm
-- Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
Goal:
α : Type u
G : SimpleGraph α
s : Set α
v w₁ w₂ : α
h : G.IsPathGraph3Compl v w₁ w₂
a b : Fin 3
this_1 : G.Adj w₁ w₂
this : G.Adj w₂ w₁
h1 : ¬G.Adj w₁ v
h2 : ¬G.Adj w₂ v
⊢ ¬G.Adj w₁ v ∧ ¬G.Adj w₂ v

Tactic:
⟨h1, h2⟩

Premises used: And.intro
-- Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
Goal:
α : Type u
G : SimpleGraph α
s : Set α
v w₁ w₂ : α
h : G.IsPathGraph3Compl v w₁ w₂
a b : Fin 3
this_1 : G.Adj w₁ w₂
this : G.Adj w₂ w₁
h1 : ¬G.Adj w₁ v
h2 : ¬G.Adj w₂ v
⊢ ¬G.Adj w₁ v ∧ ¬G.Adj w₂ v

Tactic:
exact ⟨h1, h2⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
Goal:
α : Type u
G : SimpleGraph α
s : Set α
v w₁ w₂ : α
h : G.IsPathGraph3Compl v w₁ w₂
a b : Fin 3
this_1 : G.Adj w₁ w₂
this : G.Adj w₂ w₁
h1 : ¬G.Adj v w₁
h2 : ¬G.Adj v w₂
⊢ ¬G.Adj w₁ v

Tactic:
have ⟨_, _⟩ : ¬ G.Adj w₁ v ∧ ¬ G.Adj w₂ v := by rw [adj_comm] at h1 h2; exact ⟨h1, h2⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
Goal:
α : Type u
G : SimpleGraph α
s : Set α
v w₁ w₂ : α
h : G.IsPathGraph3Compl v w₁ w₂
a b : Fin 3
this_1 : G.Adj w₁ w₂
this : G.Adj w₂ w₁
h1 : ¬G.Adj v w₁
h2 : ¬G.Adj v w₂
left : ¬G.Adj w₁ v
⊢ ¬G.Adj w₂ v

Tactic:
have ⟨_, _⟩ : ¬ G.Adj w₁ v ∧ ¬ G.Adj w₂ v := by rw [adj_comm] at h1 h2; exact ⟨h1, h2⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
Goal:
α : Type u
G : SimpleGraph α
s : Set α
v w₁ w₂ : α
h : G.IsPathGraph3Compl v w₁ w₂
a b : Fin 3
this_1 : G.Adj w₁ w₂
this : G.Adj w₂ w₁
h1 : ¬G.Adj v w₁
h2 : ¬G.Adj v w₂
left : ¬G.Adj w₁ v
right : ¬G.Adj w₂ v
⊢ G.Adj
      (match (motive := Fin 3 → α) a with
      | 0 => w₁
      | 1 => v
      | 2 => w₂)
      (match (motive := Fin 3 → α) b with
      | 0 => w₁
      | 1 => v
      | 2 => w₂) ↔
    ¬a = b ∧ ¬(↑a : ℕ) + 1 = (↑b : ℕ) ∧ ¬(↑b : ℕ) + 1 = (↑a : ℕ)

Tactic:
aesop
-- Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
Goal:
α : Type u
G : SimpleGraph α
e : Embedding (V := Fin 3) (pathGraph 3)ᶜ G
h : G.IsCompleteMultipartite
⊢ ¬G.Adj ((e : (a : Fin 3) → α) 0) ((e : (a : Fin 3) → α) 1)

Tactic:
simp [pathGraph_adj]

Premises used: SimpleGraph.pathGraph_adj
-- Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
Goal:
α : Type u
G : SimpleGraph α
e : Embedding (V := Fin 3) (pathGraph 3)ᶜ G
h : G.IsCompleteMultipartite
⊢ ¬G.Adj ((e : (a : Fin 3) → α) 0) ((e : (a : Fin 3) → α) 1)

Tactic:
have h0 : ¬ G.Adj (e 0) (e 1) := by simp [pathGraph_adj]
-- Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
Goal:
α : Type u
G : SimpleGraph α
e : Embedding (V := Fin 3) (pathGraph 3)ᶜ G
h : G.IsCompleteMultipartite
h0 : ¬G.Adj ((e : (a : Fin 3) → α) 0) ((e : (a : Fin 3) → α) 1)
⊢ ¬G.Adj ((e : (a : Fin 3) → α) 1) ((e : (a : Fin 3) → α) 2)

Tactic:
simp [pathGraph_adj]

Premises used: SimpleGraph.pathGraph_adj
-- Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
Goal:
α : Type u
G : SimpleGraph α
e : Embedding (V := Fin 3) (pathGraph 3)ᶜ G
h : G.IsCompleteMultipartite
h0 : ¬G.Adj ((e : (a : Fin 3) → α) 0) ((e : (a : Fin 3) → α) 1)
⊢ ¬G.Adj ((e : (a : Fin 3) → α) 1) ((e : (a : Fin 3) → α) 2)

Tactic:
have h1 : ¬ G.Adj (e 1) (e 2) := by simp [pathGraph_adj]
-- Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
Goal:
α : Type u
G : SimpleGraph α
e : Embedding (V := Fin 3) (pathGraph 3)ᶜ G
h : G.IsCompleteMultipartite
h0 : ¬G.Adj ((e : (a : Fin 3) → α) 0) ((e : (a : Fin 3) → α) 1)
h1 : ¬G.Adj ((e : (a : Fin 3) → α) 1) ((e : (a : Fin 3) → α) 2)
⊢ G.Adj ((e : (a : Fin 3) → α) 0) ((e : (a : Fin 3) → α) 2)

Tactic:
simp [pathGraph_adj]

Premises used: SimpleGraph.pathGraph_adj
-- Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
Goal:
α : Type u
G : SimpleGraph α
e : Embedding (V := Fin 3) (pathGraph 3)ᶜ G
h : G.IsCompleteMultipartite
h0 : ¬G.Adj ((e : (a : Fin 3) → α) 0) ((e : (a : Fin 3) → α) 1)
h1 : ¬G.Adj ((e : (a : Fin 3) → α) 1) ((e : (a : Fin 3) → α) 2)
⊢ G.Adj ((e : (a : Fin 3) → α) 0) ((e : (a : Fin 3) → α) 2)

Tactic:
have h2 : G.Adj (e 0) (e 2) := by simp [pathGraph_adj]
-- Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
Goal:
α : Type u
G : SimpleGraph α
e : Embedding (V := Fin 3) (pathGraph 3)ᶜ G
h : G.IsCompleteMultipartite
h0 : ¬G.Adj ((e : (a : Fin 3) → α) 0) ((e : (a : Fin 3) → α) 1)
h1 : ¬G.Adj ((e : (a : Fin 3) → α) 1) ((e : (a : Fin 3) → α) 2)
h2 : G.Adj ((e : (a : Fin 3) → α) 0) ((e : (a : Fin 3) → α) 2)
⊢ False

Tactic:
h.trans _ _ _ h0 h1 h2

Premises used: IsTrans.trans
-- Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
Goal:
α : Type u
G : SimpleGraph α
e : Embedding (V := Fin 3) (pathGraph 3)ᶜ G
h : G.IsCompleteMultipartite
h0 : ¬G.Adj ((e : (a : Fin 3) → α) 0) ((e : (a : Fin 3) → α) 1)
h1 : ¬G.Adj ((e : (a : Fin 3) → α) 1) ((e : (a : Fin 3) → α) 2)
h2 : G.Adj ((e : (a : Fin 3) → α) 0) ((e : (a : Fin 3) → α) 2)
⊢ False

Tactic:
exact h.trans _ _ _ h0 h1 h2

Premises used: IsTrans.trans
-- Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
Goal:
α : Type u
G : SimpleGraph α
β : Type u_1
H : SimpleGraph β
f : H ↪g G
h : G.IsCompleteMultipartite
contrapose : ∀ (h : ¬H.IsCompleteMultipartite), ¬G.IsCompleteMultipartite
⊢ H.IsCompleteMultipartite

Tactic:
contrapose h
-- Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
Goal:
α : Type u
G : SimpleGraph α
β : Type u_1
H : SimpleGraph β
f : H ↪g G
h : ¬H.IsCompleteMultipartite
⊢ ¬G.IsCompleteMultipartite

Tactic:
not_isCompleteMultipartite_of_pathGraph3ComplEmbedding
          <| f.comp (pathGraph3ComplEmbeddingOf h)

Premises used: SimpleGraph.pathGraph3ComplEmbeddingOf, SimpleGraph.not_isCompleteMultipartite_of_pathGraph3ComplEmbedding, SimpleGraph.Embedding.comp
-- Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
Goal:
α : Type u
G : SimpleGraph α
β : Type u_1
H : SimpleGraph β
f : H ↪g G
h : ¬H.IsCompleteMultipartite
⊢ ¬G.IsCompleteMultipartite

Tactic:
exact not_isCompleteMultipartite_of_pathGraph3ComplEmbedding
          <| f.comp (pathGraph3ComplEmbeddingOf h)

Premises used: SimpleGraph.pathGraph3ComplEmbeddingOf, SimpleGraph.not_isCompleteMultipartite_of_pathGraph3ComplEmbedding, SimpleGraph.Embedding.comp
-- Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
Goal:
r t : ℕ
v w : Fin r × Fin t
⊢ (completeEquipartiteGraph r t).Adj v w ↔ v.1 ≠ w.1

Tactic:
rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
Goal:
α : Type u
G : SimpleGraph α
s : Set α
r t : ℕ
⊢ ∀ {a b : Fin r × Fin t},
    Adj (V := (i : Fin r) × const (Fin r) (Fin t) i) (SimpleGraph.completeMultipartiteGraph (const (Fin r) (Fin t)))
        ((Equiv.symm (Equiv.sigmaEquivProd (Fin r) (Fin t)) :
            (a : Fin r × Fin t) → (i : Fin r) × const (Fin r) (Fin t) i)
          a)
        ((Equiv.symm (Equiv.sigmaEquivProd (Fin r) (Fin t)) :
            (a : Fin r × Fin t) → (i : Fin r) × const (Fin r) (Fin t) i)
          b) ↔
      (completeEquipartiteGraph r t).Adj a b

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
Goal:
α : Type u
G : SimpleGraph α
s : Set α
r t : ℕ
refine : ∀ (v : Fin r × Fin t), (↑v.2 : ℕ) * r + (↑v.1 : ℕ) < r * t
⊢ Fin r × Fin t → Fin (r * t)

Tactic:
refine fun v ↦ ⟨v.2 * r + v.1, ?_⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
Goal:
α : Type u
G : SimpleGraph α
s : Set α
r t : ℕ
v : Fin r × Fin t
rw : (t - 1) * r + r
| r * t

Tactic:
rw [← Nat.sub_one_add_one_eq_of_pos v.2.pos, Nat.mul_add_one, mul_comm r (t - 1)]

Premises used: HSub.hSub, Fin.pos, Nat.sub_one_add_one_eq_of_pos, mul_comm, Nat.mul_add_one, OfNat.ofNat, Prod.snd