mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
⊢ G.Colorable 2 ↔ ∀ (u : α) (w : G.Walk u u), Even w.length

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Coloring.EdgeLabeling

Goal state before:
pp: V : Type u_1
K : Type u_3
inst✝² : DecidableEq V
inst✝¹ : Fintype V
inst✝ : Fintype K
⊢ Fintype.card K ^ Fintype.card ↑⊤.edgeSet = Fintype.card K ^ (Fintype.card V).choose 2

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Coloring.EdgeLabeling

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
K : Type u_3
C : G.EdgeLabeling K
x y : V
h : G.Adj y x
⊢ C.get y x h = C.get x y ⋯

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Coloring.EdgeLabeling

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
K : Type u_3
C C' : G.EdgeLabeling K
h : ∀ (x y : V) (h : G.Adj x y), C.get x y h = C'.get x y h
⊢ C = C'

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Coloring.EdgeLabeling

Goal state before:
pp: 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 x) (f y)

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Coloring.EdgeLabeling

Goal state before:
pp: 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:
by

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Coloring.EdgeLabeling

Goal state before:
pp: 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
⊢ K

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Coloring.EdgeLabeling

Goal state before:
pp: 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 ↔ ∃ (H : G.Adj x y), C ⟨s(x, y), H⟩ = k

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Coloring.EdgeLabeling

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
K : Type u_3
C : G.EdgeLabeling K
k : K
⊢ C.labelGraph k ≤ G

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan

Goal state before:
pp: V : Type u_1
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
r : ℕ
s t u : V
hts : ¬G.Adj t s
hsu : ¬G.Adj s u
hst : ¬G.Adj s t
dst : G.degree s = G.degree t
dsu : G.degree s = G.degree u
h : G.Adj t u
cf : G.CliqueFree (r + 1)
nst : s ≠ t
ntu : t ≠ u
this : ¬(G.replaceVertex s t).Adj s u
l1 : (G.replaceVertex s t).degree s = G.degree s
⊢ (G.replaceVertex s t).degree u = G.degree u - 1

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Coloring.EdgeLabeling

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
K : Type u_3
C : G.EdgeLabeling K
⊢ Pairwise fun k l ↦ Disjoint (C.labelGraph k) (C.labelGraph l)

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Coloring.EdgeLabeling

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
K : Type u_3
C : G.EdgeLabeling K
⊢ Set.univ.PairwiseDisjoint C.labelGraph

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Acyclic

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
hconn : G.Connected
u z : V
inst✝ : Fintype ↑(G.neighborSet z)
hdeg : G.degree z = 1
adj_vu : G.Adj z u
hu : ∀ (y : V), (fun w ↦ G.Adj z w) y → y = u
w x : ↑{z}ᶜ
pwu : G.Walk (↑w) u
hpwu : pwu.IsPath
pux : G.Walk u ↑x
hpux : pux.IsPath
hz : z ∈ (↑(pwu.append pux).toPath).support
pwz : G.Walk (↑w) z
pzx : G.Walk z ↑x
p_eq_pwzx : ↑(pwu.append pux).toPath = pwz.append pzx
this : 1 ≤ List.count (pwz.getVert (pwz.length - 1)) pwz.support
⊢ ↑w ≠ z

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Coloring.EdgeLabeling

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
K : Type u_3
C : G.EdgeLabeling K
⊢ ⨆ k, C.labelGraph k = G

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Coloring.EdgeLabeling

Goal state before:
pp: 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 (f a) (f b)

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Coloring.EdgeLabeling

Goal state before:
pp: 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:
by

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan

Goal state before:
pp: V : Type u_1
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
r : ℕ
s t u : V
hts : ¬G.Adj t s
hsu : ¬G.Adj s u
hst : ¬G.Adj s t
dst : G.degree s = G.degree t
dsu : G.degree s = G.degree u
h : G.Adj t u
cf : G.CliqueFree (r + 1)
nst : s ≠ t
ntu : t ≠ u
this : ¬(G.replaceVertex s t).Adj s u
l1 : (G.replaceVertex s t).degree s = G.degree s
l2 : (G.replaceVertex s t).degree u = G.degree u - 1
⊢ 0 < G.degree u

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Coloring.EdgeLabeling

Goal state before:
pp: V : Type u_1
V' : Type u_2
G✝ : SimpleGraph V
G' : SimpleGraph V'
K : Type u_3
K' : Type u_4
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
⊢ ∀ (x y : V), ⊤.Adj x y → (if G.Adj y x then 1 else 0) = if G.Adj x y then 1 else 0

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Coloring.EdgeLabeling

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
⊢ EdgeLabeling.labelGraph G.toTopEdgeLabeling 1 = G

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Acyclic

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
hconn : G.Connected
u z : V
inst✝ : Fintype ↑(G.neighborSet z)
hdeg : G.degree z = 1
adj_vu : G.Adj z u
hu : ∀ (y : V), (fun w ↦ G.Adj z w) y → y = u
w x : ↑{z}ᶜ
pwu : G.Walk (↑w) u
hpwu : pwu.IsPath
pux : G.Walk u ↑x
hpux : pux.IsPath
hz : z ∈ (↑(pwu.append pux).toPath).support
pwz : G.Walk (↑w) z
pzx : G.Walk z ↑x
p_eq_pwzx : ↑(pwu.append pux).toPath = pwz.append pzx
this : 1 ≤ List.count u pwz.support
⊢ z ≠ ↑x

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan

Goal state before:
pp: V : Type u_1
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
r : ℕ
s t u : V
h : G.IsTuranMaximal r
hts : ¬G.Adj t s
hsu : ¬G.Adj s u
⊢ ¬G.Adj t u

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan

Goal state before:
pp: V : Type u_1
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
r : ℕ
h : G.IsTuranMaximal r
⊢ ∀ (x : V), ¬G.Adj x x

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan

Goal state before:
pp: V : Type u_1
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
r : ℕ
h : G.IsTuranMaximal r
⊢ ∀ {x y : V}, ¬G.Adj x y → ¬G.Adj y x

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Coloring.EdgeLabeling

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
⊢ EdgeLabeling.labelGraph G.toTopEdgeLabeling 0 = Gᶜ

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Coloring.EdgeLabeling

Goal state before:
pp: V : Type u_1
inst✝ : DecidableEq V
C : TopEdgeLabeling V (Fin 2)
⊢ (EdgeLabeling.labelGraph C 1).toTopEdgeLabeling = C

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan

Goal state before:
pp: V : Type u_1
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
r : ℕ
s t : V
h : G.IsTuranMaximal r
inst✝ : DecidableEq V
⊢ ¬G.Adj s t ↔ h.finpartition.part s = h.finpartition.part t

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan

Goal state before:
pp: V : Type u_1
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
r : ℕ
s : V
h : G.IsTuranMaximal r
inst✝ : DecidableEq V
⊢ G.degree s = #{t | G.Adj s t}

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite

Goal state before:
pp: α : Type u
⊢ ∀ (a b c : α), ¬⊥.Adj a b → ¬⊥.Adj b c → ¬⊥.Adj a c

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Acyclic

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
hconn : G.Connected
u z : V
inst✝ : Fintype ↑(G.neighborSet z)
hdeg : G.degree z = 1
adj_vu : G.Adj z u
hu : ∀ (y : V), (fun w ↦ G.Adj z w) y → y = u
w x : ↑{z}ᶜ
pwu : G.Walk (↑w) u
hpwu : pwu.IsPath
pux : G.Walk u ↑x
hpux : pux.IsPath
hz : z ∈ (↑(pwu.append pux).toPath).support
pwz : G.Walk (↑w) z
pzx : G.Walk z ↑x
p_eq_pwzx : ↑(pwu.append pux).toPath = pwz.append pzx
this✝ : 1 ≤ List.count u pwz.support
this : 1 ≤ List.count pzx.snd pzx.support.tail
⊢ z ≠ ↑x

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite

Goal state before:
pp: α : Type u
G : SimpleGraph α
s : Set α
h : G.IsCompleteMultipartite
x✝ y✝ : α
h' : ¬G.Adj x✝ y✝
⊢ ¬G.Adj y✝ x✝

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite

Goal state before:
pp: ι : 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:
by

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan

Goal state before:
pp: V : Type u_1
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
r : ℕ
s : V
h : G.IsTuranMaximal r
inst✝ : DecidableEq V
⊢ Fintype.card V - #{t | ¬G.Adj s t} = Fintype.card V - #(h.finpartition.part s)

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite

Goal state before:
pp: α : Type u
G : SimpleGraph α
s : Set α
h : G.IsCompleteMultipartite
⊢ ∀ {a b : α},
    (completeMultipartiteGraph fun c ↦ { x // h.setoid c.out x }).Adj
        ({ toFun := fun x ↦ ⟨⟦x⟧, ⟨x, ⋯⟩⟩,
            invFun := fun x ↦
              match x with
              | ⟨fst, x⟩ => ↑x,
            left_inv := ⋯, right_inv := ⋯ }
          a)
        ({ toFun := fun x ↦ ⟨⟦x⟧, ⟨x, ⋯⟩⟩,
            invFun := fun x ↦
              match x with
              | ⟨fst, x⟩ => ↑x,
            left_inv := ⋯, right_inv := ⋯ }
          b) ↔
      G.Adj a b

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Acyclic

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
hconn : G.Connected
v : V
inst✝ : Fintype ↑(G.neighborSet v)
hdeg : G.degree v = 1
⊢ (induce {v}ᶜ G).Connected

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Acyclic

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
inst✝¹ : Finite V
inst✝ : Nontrivial V
hconn : G.Connected
T : SimpleGraph V
left✝ : T ≤ G
T_isTree : T.IsTree
hT : T.Connected
isAcyclic✝ : T.IsAcyclic
this : Fintype V
v : V
hv : T.degree v = 1
⊢ induce {v}ᶜ T ≤ induce {v}ᶜ G

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Acyclic

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
inst✝¹ : Finite V
inst✝ : Nontrivial V
hconn : G.Connected
⊢ ∃ v, (induce {v}ᶜ G).Connected

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Acyclic

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
inst✝ : Finite V
hconn : G.Connected
⊢ ∃ v, (induce {v}ᶜ G).Preconnected

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan

Goal state before:
pp: V : Type u_1
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
r : ℕ
h : G.IsTuranMaximal r
inst✝ : DecidableEq V
fp : Finpartition univ := h.finpartition
large : Finset V
hl : large ∈ fp.parts
small : Finset V
hs : small ∈ fp.parts
ineq : #small + 1 < #large
w : V
hw : w ∈ large
v : V
hv : v ∈ small
cf : G.CliqueFree (r + 1)
large_eq : fp.part w = large
small_eq : fp.part v = small
⊢ G.Adj v w

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite

Goal state before:
pp: α : Type u
G : SimpleGraph α
⊢ G.IsCompleteMultipartite ↔ ∃ ι V, ∃ (_ : ∀ (i : ι), Nonempty (V i)), Nonempty (G ≃g completeMultipartiteGraph V)

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite

Goal state before:
pp: α : Type u
G : SimpleGraph α
v w₁ w₂ : α
h : G.IsPathGraph3Compl v w₁ w₂
⊢ G.IsPathGraph3Compl v w₂ w₁

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite

Goal state before:
pp: α : Type u
G : SimpleGraph α
h : ¬G.IsCompleteMultipartite
⊢ ∃ v w₁ w₂, G.IsPathGraph3Compl v w₁ w₂

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite

Goal state before:
pp: α : Type u
G : SimpleGraph α
x✝ : ∃ v w₁ w₂, G.IsPathGraph3Compl v w₁ w₂
w✝² w✝¹ w✝ : α
h1 : G.Adj w✝¹ w✝
h2 : ¬G.Adj w✝² w✝¹
h3 : ¬G.Adj w✝² w✝
h : G.IsCompleteMultipartite
⊢ ¬G.Adj w✝¹ w✝²

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan

Goal state before:
pp: V : Type u_1
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
r : ℕ
h : G.IsTuranMaximal r
inst✝ : DecidableEq V
fp : Finpartition univ := h.finpartition
large : Finset V
hl : large ∈ fp.parts
small : Finset V
hs : small ∈ fp.parts
ineq : #small + 1 < #large
w : V
hw : w ∈ large
v : V
hv : v ∈ small
cf : G.CliqueFree (r + 1)
large_eq : fp.part w = large
small_eq : fp.part v = small
ha : G.Adj v w
⊢ #large ≤ Fintype.card V

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite

Goal state before:
pp: α : Type u
G : SimpleGraph α
s : Set α
v w₁ w₂ : α
h : G.IsPathGraph3Compl v w₁ w₂
⊢ Injective fun x ↦
    match x with
    | 0 => w₁
    | 1 => v
    | 2 => w₂

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan

Goal state before:
pp: V : Type u_1
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
r : ℕ
h : G.IsTuranMaximal r
inst✝ : DecidableEq V
⊢ h.finpartition.IsEquipartition

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite

Goal state before:
pp: α : Type u
G : SimpleGraph α
s : Set α
v w₁ w₂ : α
h : G.IsPathGraph3Compl v w₁ w₂
a✝ b✝ : Fin 3
this✝ : G.Adj w₁ w₂
this : G.Adj w₂ w₁
h1 : ¬G.Adj v w₁
h2 : ¬G.Adj v w₂
⊢ ¬G.Adj w₁ v ∧ ¬G.Adj w₂ v

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite

Goal state before:
pp: α : Type u
G : SimpleGraph α
s : Set α
v w₁ w₂ : α
h : G.IsPathGraph3Compl v w₁ w₂
⊢ ∀ {a b : Fin 3},
    G.Adj
        ({
            toFun := fun x ↦
              match x with
              | 0 => w₁
              | 1 => v
              | 2 => w₂,
            inj' := ⋯ }
          a)
        ({
            toFun := fun x ↦
              match x with
              | 0 => w₁
              | 1 => v
              | 2 => w₂,
            inj' := ⋯ }
          b) ↔
      (pathGraph 3)ᶜ.Adj a b

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite

Goal state before:
pp: α : Type u
G : SimpleGraph α
e : (pathGraph 3)ᶜ ↪g G
h : G.IsCompleteMultipartite
⊢ ¬G.Adj (e 0) (e 1)

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite

Goal state before:
pp: α : Type u
G : SimpleGraph α
e : (pathGraph 3)ᶜ ↪g G
h : G.IsCompleteMultipartite
h0 : ¬G.Adj (e 0) (e 1)
⊢ ¬G.Adj (e 1) (e 2)

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite

Goal state before:
pp: α : Type u
G : SimpleGraph α
e : (pathGraph 3)ᶜ ↪g G
h : G.IsCompleteMultipartite
h0 : ¬G.Adj (e 0) (e 1)
h1 : ¬G.Adj (e 1) (e 2)
⊢ G.Adj (e 0) (e 2)

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan

Goal state before:
pp: V : Type u_1
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
r : ℕ
h : G.IsTuranMaximal r
inst✝ : DecidableEq V
l : r < #h.finpartition.parts
z : Finset V
hz : Set.BijOn h.finpartition.part ↑z ↑h.finpartition.parts
v : V
hv : v ∈ ↑z
w : V
hw : w ∈ ↑z
hn : ¬G.Adj v w
⊢ h.finpartition.part v = h.finpartition.part w

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite

Goal state before:
pp: α : Type u
G : SimpleGraph α
e : (pathGraph 3)ᶜ ↪g G
⊢ ¬G.IsCompleteMultipartite

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan

Goal state before:
pp: V : Type u_1
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
r : ℕ
h : G.IsTuranMaximal r
inst✝ : DecidableEq V
l : r < #h.finpartition.parts
z : Finset V
hz : Set.BijOn h.finpartition.part ↑z ↑h.finpartition.parts
⊢ ¬G.CliqueFree #z

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite

Goal state before:
pp: α : Type u
G : SimpleGraph α
β : Type u_1
H : SimpleGraph β
f : H ↪g G
⊢ G.IsCompleteMultipartite → H.IsCompleteMultipartite

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite

Goal state before:
pp: r t : ℕ
v w : Fin r × Fin t
⊢ (completeEquipartiteGraph r t).Adj v w ↔ v.1 ≠ w.1

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan

Goal state before:
pp: V : Type u_1
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
r : ℕ
h : G.IsTuranMaximal r
inst✝ : DecidableEq V
⊢ #h.finpartition.parts ≤ r

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite

Goal state before:
pp: α : Type u
G : SimpleGraph α
s : Set α
r t : ℕ
⊢ ∀ {a b : Fin r × Fin t},
    (SimpleGraph.completeMultipartiteGraph (const (Fin r) (Fin t))).Adj ((Equiv.sigmaEquivProd (Fin r) (Fin t)).symm a)
        ((Equiv.sigmaEquivProd (Fin r) (Fin t)).symm b) ↔
      (completeEquipartiteGraph r t).Adj a b

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite

Goal state before:
pp: α : Type u
G : SimpleGraph α
s : Set α
r t : ℕ
⊢ Fin r × Fin t → Fin (r * t)

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite

Goal state before:
pp: α : Type u
G : SimpleGraph α
s : Set α
r t : ℕ
⊢ Fin (r * t) → Fin r × Fin t

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Acyclic

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
hG : G.IsAcyclic
u v w : V
hadj : G.Adj v w
hreach : G.Reachable u v
⊢ G.dist u v ≠ G.dist u w

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Acyclic

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
hG : G.IsAcyclic
u v w : V
hadj : G.Adj v w
hreach : G.Reachable u v
⊢ G.dist u v = G.dist u w + 1 ∨ G.dist u w = G.dist u v + 1

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Acyclic

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
hG : G.IsTree
u v w : V
hadj : G.Adj v w
⊢ G.dist u v = G.dist u w + 1 ∨ G.dist u w = G.dist u v + 1

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Acyclic

Goal state before:
pp: V : Type u_1
V' : Type u_2
G : SimpleGraph V
G' : SimpleGraph V'
hG : G.IsTree
u : V
⊢ ∀ {v w : V}, G.Adj v w → ⟨G.dist u v % 2, ⋯⟩ ≠ ⟨G.dist u w % 2, ⋯⟩

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Finite

Goal state before:
pp: V : Type u
G : SimpleGraph V
inst✝² : DecidableEq V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
u v : V
⊢ G.Reachable u v ↔ ∃ n, (G.finsetWalkLength (↑n) u v).Nonempty

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Finite

Goal state before:
pp: V : Type u
G : SimpleGraph V
inst✝² : DecidableEq V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
⊢ G.Preconnected ∧ univ.Nonempty ↔ G.Connected

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Finite

Goal state before:
pp: V : Type u
G : SimpleGraph V
inst✝² : DecidableEq V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
c : G.ConnectedComponent
v w : V
⊢ G.Reachable v w ↔ v ∈ (G.connectedComponentMk w).supp

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Acyclic

Goal state before:
pp: V : Type u_1
V' : Type u_2
G : SimpleGraph V
G' : SimpleGraph V'
hG : G.IsAcyclic
verts : G.ConnectedComponent → V
h : ∀ (C : G.ConnectedComponent), verts C ∈ C
⊢ ∀ {a b : V},
    G.Adj a b →
      (completeGraph (Fin 2)).Adj
        (let u := verts (G.connectedComponentMk a);
        ⟨G.dist u a % 2, ⋯⟩)
        (let u := verts (G.connectedComponentMk b);
        ⟨G.dist u b % 2, ⋯⟩)

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Acyclic

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
u v : V
huv : u ≠ v
n : ℕ
hn : 2 ≤ n
h✝ : G.IsEdgeReachable n u v
w : V
hw : G.Adj u w
h : G.IsEdgeReachable 2 u w
⊢ {s(u, w)}.encard < ↑2

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Finite

Goal state before:
pp: V : Type u
G : SimpleGraph V
inst✝⁴ : DecidableEq V
inst✝³ : Fintype V
inst✝² : DecidableRel G.Adj
G' : SimpleGraph V
h : G ≤ G'
c' : G'.ConnectedComponent
inst✝¹ : Fintype ↑c'.supp
inst✝ : DecidablePred fun c ↦ c.supp ⊆ c'.supp
x : G.ConnectedComponent
x✝¹ : x ∈ ↑{c | c.supp ⊆ c'.supp}
y : G.ConnectedComponent
x✝ : y ∈ ↑{c | c.supp ⊆ c'.supp}
hxy : x ≠ y
⊢ (Disjoint on fun c ↦ c.supp.toFinset) x y

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Finite

Goal state before:
pp: V : Type u
G : SimpleGraph V
inst✝⁴ : DecidableEq V
inst✝³ : Fintype V
inst✝² : DecidableRel G.Adj
G' : SimpleGraph V
h : G ≤ G'
c' : G'.ConnectedComponent
inst✝¹ : Fintype ↑c'.supp
inst✝ : DecidablePred fun c ↦ c.supp ⊆ c'.supp
⊢ ↑({c | c.supp ⊆ c'.supp}.disjiUnion (fun c ↦ c.supp.toFinset) ⋯) = ↑c'.supp.toFinset

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite

Goal state before:
pp: α : Type u
G : SimpleGraph α
s : Set α
r t : ℕ
v : Fin r × Fin t
⊢ (⟨↑⟨↑v.2 * r + ↑v.1, ⋯⟩ % r, ⋯⟩, ⟨↑⟨↑v.2 * r + ↑v.1, ⋯⟩ / r, ⋯⟩) = v

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Acyclic

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
u v : V
huv : u ≠ v
n : ℕ
hn : 2 ≤ n
h : G.IsEdgeReachable n u v
⊢ ∃ w, w.IsCycle

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite

Goal state before:
pp: α : Type u
G : SimpleGraph α
s : Set α
r t : ℕ
v w : Fin r × Fin t
⊢ (SimpleGraph.turanGraph (r * t) r).Adj
      ({ toFun := fun v ↦ ⟨↑v.2 * r + ↑v.1, ⋯⟩, invFun := fun v ↦ (⟨↑v % r, ⋯⟩, ⟨↑v / r, ⋯⟩), left_inv := ⋯,
          right_inv := ⋯ }
        v)
      ({ toFun := fun v ↦ ⟨↑v.2 * r + ↑v.1, ⋯⟩, invFun := fun v ↦ (⟨↑v % r, ⋯⟩, ⟨↑v / r, ⋯⟩), left_inv := ⋯,
          right_inv := ⋯ }
        w) ↔
    (completeEquipartiteGraph r t).Adj v w

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Acyclic

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
⊢ G.IsAcyclic ↔ Pairwise fun x1 x2 ↦ ¬G.IsEdgeReachable 2 x1 x2

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Acyclic

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
⊢ G.IsAcyclic ↔ ∀ n ≥ 3, (cycleGraph n).Free G

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Acyclic

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
h : G.IsAcyclic
n : ℕ
hn : 3 ≤ n
⊢ G.CliqueFree n

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan

Goal state before:
pp: V : Type u_1
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
r : ℕ
h : G.IsTuranMaximal r
inst✝ : DecidableEq V
fp : Finpartition univ := h.finpartition
l : #fp.parts < #univ ∧ #fp.parts < r
x y : V
hn : x ≠ y
he : fp.part x = fp.part y
⊢ G.CliqueFree r

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite

Goal state before:
pp: r t : ℕ
⊢ completeEquipartiteGraph r t = ⊥ ↔ r ≤ 1 ∨ t = 0

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite

Goal state before:
pp: r t : ℕ
⊢ (completeEquipartiteGraph r t).IsCompleteMultipartite

Tactic:
by

Goal state after: