mathlib-initiative/mathlib-tactics huggingface dataset:
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
hn : ¬G.Adj s t
h : G.degree s ≠ G.degree t
⊢ G.CliqueFree (r + 1) → ∃ G' inst, G'.CliqueFree (r + 1) ∧ #G.edgeFinset < #G'.edgeFinset

Tactic:
;

Goal state after:
V : Type u_1
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
r : ℕ
s t : V
hn : ¬G.Adj s t
h : G.degree s ≠ G.degree t
⊢ G.CliqueFree (r + 1) → ∃ G' inst, G'.CliqueFree (r + 1) ∧ #G.edgeFinset < #G'.edgeFinset
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.CliqueFree (r + 1) ∧
    ∀ ⦃G' : SimpleGraph V⦄ [inst : DecidableRel G'.Adj], G'.CliqueFree (r + 1) → #G'.edgeFinset ≤ #G.edgeFinset
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
⊢ ¬G.Adj t u

Tactic:
;

Goal state after:
V : Type u_1
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
r : ℕ
s t u : V
h :
  G.CliqueFree (r + 1) ∧
    ∀ ⦃G' : SimpleGraph V⦄ [inst : DecidableRel G'.Adj], G'.CliqueFree (r + 1) → #G'.edgeFinset ≤ #G.edgeFinset
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
⊢ ¬G.Adj t u
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
⊢ G.CliqueFree (r + 1) → ∃ G' inst, G'.CliqueFree (r + 1) ∧ #G.edgeFinset < #G'.edgeFinset

Tactic:
;

Goal state after:
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
⊢ G.CliqueFree (r + 1) → ∃ G' inst, G'.CliqueFree (r + 1) ∧ #G.edgeFinset < #G'.edgeFinset
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
⊢ #((G.replaceVertex s t).neighborFinset s) = #(G.neighborFinset s)

Tactic:
;

Goal state after:
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
⊢ #((G.replaceVertex s t).neighborFinset s) = #(G.neighborFinset s)
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
⊢ (G.replaceVertex s t).neighborFinset s = G.neighborFinset s

Tactic:
;

Goal state after:
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
⊢ (G.replaceVertex s t).neighborFinset s = G.neighborFinset s
Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions

Goal state before:
pp: n✝ n : ℕ
h : 2 ≤ n + 2
u v : Fin (n + 2)
hu : ¬↑u = n + 2 - 1
h✝ : ¬↑v = n + 2 - 1
hu' : ↑u + ↑1 < n + 2
hv' : ↑v + ↑1 < n + 2
huv : u - v = 1
⊢ ∀ (x y : ℕ), x % 2 = y % 2 ↔ (x % 2 = 0 ↔ y % 2 = 0)

Tactic:
;

Goal state after:
n✝ n : ℕ
h : 2 ≤ n + 2
u v : Fin (n + 2)
hu : ¬↑u = n + 2 - 1
h✝ : ¬↑v = n + 2 - 1
hu' : ↑u + ↑1 < n + 2
hv' : ↑v + ↑1 < n + 2
huv : u - v = 1
⊢ ∀ (x y : ℕ), x % 2 = y % 2 ↔ (x % 2 = 0 ↔ y % 2 = 0)
Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions

Goal state before:
pp: n✝ n : ℕ
h : 2 ≤ n + 2
u v : Fin (n + 2)
hu : ¬↑u = n + 2 - 1
h✝ : ¬↑v = n + 2 - 1
hu' : ↑u + ↑1 < n + 2
hv' : ↑v + ↑1 < n + 2
huv : v - u = 1
⊢ ∀ (x y : ℕ), x % 2 = y % 2 ↔ (x % 2 = 0 ↔ y % 2 = 0)

Tactic:
;

Goal state after:
n✝ n : ℕ
h : 2 ≤ n + 2
u v : Fin (n + 2)
hu : ¬↑u = n + 2 - 1
h✝ : ¬↑v = n + 2 - 1
hu' : ↑u + ↑1 < n + 2
hv' : ↑v + ↑1 < n + 2
huv : v - u = 1
⊢ ∀ (x y : ℕ), x % 2 = y % 2 ↔ (x % 2 = 0 ↔ y % 2 = 0)
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).neighborFinset u = G.neighborFinset u \ {t}

Tactic:
;

Goal state after:
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).neighborFinset u = G.neighborFinset u \ {t}
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
⊢ ∃ w, G.Adj u w

Tactic:
;

Goal state after:
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
⊢ ∃ w, G.Adj u w
Module: Mathlib.Combinatorics.SimpleGraph.Coloring.EdgeLabeling

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
x y : V
⊢ (EdgeLabeling.labelGraph G.toTopEdgeLabeling 1).Adj x y ↔ G.Adj x y

Tactic:
;

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
x y : V
⊢ (EdgeLabeling.labelGraph G.toTopEdgeLabeling 0).Adj x y ↔ Gᶜ.Adj x y

Tactic:
;

Goal state after:
V : Type u_1
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
x y : V
⊢ (EdgeLabeling.labelGraph G.toTopEdgeLabeling 0).Adj x y ↔ Gᶜ.Adj x y
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan

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

Tactic:
;

Goal state after:
case e_a
V : Type u_1
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
r : ℕ
s : V
h : G.IsTuranMaximal r
inst✝ : DecidableEq V
⊢ {t | ¬G.Adj s t} = h.finpartition.part s
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan

Goal state before:
pp: case e_a
V : Type u_1
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
r : ℕ
s : V
h : G.IsTuranMaximal r
inst✝ : DecidableEq V
a✝ : V
⊢ a✝ ∈ {t | ¬G.Adj s t} ↔ a✝ ∈ h.finpartition.part s

Tactic:
;

Goal state after:
case e_a
V : Type u_1
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
r : ℕ
s : V
h : G.IsTuranMaximal r
inst✝ : DecidableEq V
a✝ : V
⊢ a✝ ∈ {t | ¬G.Adj s t} ↔ a✝ ∈ h.finpartition.part s
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
⊢ ¬(G.CliqueFree (r + 1) ∧
      ∀ ⦃G' : SimpleGraph V⦄ [inst : DecidableRel G'.Adj], G'.CliqueFree (r + 1) → #G'.edgeFinset ≤ #G.edgeFinset)

Tactic:
;

Goal state after:
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
⊢ ¬(G.CliqueFree (r + 1) ∧
      ∀ ⦃G' : SimpleGraph V⦄ [inst : DecidableRel G'.Adj], G'.CliqueFree (r + 1) → #G'.edgeFinset ≤ #G.edgeFinset)
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
⊢ G.CliqueFree (r + 1) → ∃ G' inst, G'.CliqueFree (r + 1) ∧ #G.edgeFinset < #G'.edgeFinset

Tactic:
;

Goal state after:
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
⊢ G.CliqueFree (r + 1) → ∃ G' inst, G'.CliqueFree (r + 1) ∧ #G.edgeFinset < #G'.edgeFinset
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
hn : ¬G.Adj v w
⊢ False

Tactic:
;

Goal state after:
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
hn : ¬G.Adj v w
⊢ False
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 : #large + 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
hn : small = large
⊢ False

Tactic:
;

Goal state after:
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 : #large + 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
hn : small = large
⊢ False
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 w₁ v
h2 : ¬G.Adj w₂ v
⊢ ¬G.Adj w₁ v ∧ ¬G.Adj w₂ v

Tactic:
;

Goal state after:
α : 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 w₁ v
h2 : ¬G.Adj w₂ v
⊢ ¬G.Adj w₁ v ∧ ¬G.Adj w₂ v
Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite

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

Tactic:
;

Goal state after:
α : Type u
G : SimpleGraph α
β : Type u_1
H : SimpleGraph β
f : H ↪g G
h : G.IsCompleteMultipartite
⊢ H.IsCompleteMultipartite
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Finite

Goal state before:
pp: case mp
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:
intro r

Goal state after:
case mp
V : Type u
G : SimpleGraph V
inst✝² : DecidableEq V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
u v : V
r : G.Reachable u v
⊢ ∃ n, (G.finsetWalkLength (↑n) u v).Nonempty
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 + 1) ∧
      ∀ ⦃G' : SimpleGraph V⦄ [inst : DecidableRel G'.Adj], G'.CliqueFree (r + 1) → #G'.edgeFinset ≤ #G.edgeFinset)

Tactic:
;

Goal state after:
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 + 1) ∧
      ∀ ⦃G' : SimpleGraph V⦄ [inst : DecidableRel G'.Adj], G'.CliqueFree (r + 1) → #G'.edgeFinset ≤ #G.edgeFinset)
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 + 1) → ∃ G' inst, G'.CliqueFree (r + 1) ∧ #G.edgeFinset < #G'.edgeFinset

Tactic:
;

Goal state after:
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 + 1) → ∃ G' inst, G'.CliqueFree (r + 1) ∧ #G.edgeFinset < #G'.edgeFinset
Module: Mathlib.Combinatorics.SimpleGraph.Acyclic

Goal state before:
pp: case refine_2
V : Type u_1
G : SimpleGraph V
h : ∀ n ≥ 3, (cycleGraph n).Free G
v : V
p : G.Walk v v
hcyc : p.IsCycle
⊢ cycleGraph p.length ⊑ G

Tactic:
· exact cycleGraph_isContained_iff hcyc.three_le_length |>.mpr ⟨v, p, hcyc, rfl⟩

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
z : Finset V
zc : #z = r
⊢ ¬∀ ⦃x : V⦄, x ∈ ↑z → ∀ ⦃y : V⦄, y ∈ ↑z → x ≠ y → G.Adj x y

Tactic:
;

Goal state after:
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
z : Finset V
zc : #z = r
⊢ ¬∀ ⦃x : V⦄, x ∈ ↑z → ∀ ⦃y : V⦄, y ∈ ↑z → x ≠ y → G.Adj x y
Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite

Goal state before:
pp: r t : ℕ
⊢ (completeEquipartiteGraph r t).edgeSet.Nonempty ↔ Nontrivial (Fin r) ∧ Nonempty (Fin t)

Tactic:
refine ⟨fun ⟨e, he⟩ ↦ ?_, fun ⟨⟨i₁, i₂, hv⟩, ⟨x⟩⟩ ↦ ?_⟩

Goal state after:
case refine_1
r t : ℕ
x✝ : (completeEquipartiteGraph r t).edgeSet.Nonempty
e : Sym2 (Fin r × Fin t)
he : e ∈ (completeEquipartiteGraph r t).edgeSet
⊢ Nontrivial (Fin r) ∧ Nonempty (Fin t)

case refine_2
r t : ℕ
x✝ : Nontrivial (Fin r) ∧ Nonempty (Fin t)
i₁ i₂ : Fin r
hv : i₁ ≠ i₂
x : Fin t
⊢ (completeEquipartiteGraph r t).edgeSet.Nonempty
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
z : Finset V
zc : #z = r
⊢ ∃ x ∈ ↑z, ∃ y ∈ ↑z, x ≠ y ∧ ¬G.Adj x y

Tactic:
;

Goal state after:
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
z : Finset V
zc : #z = r
⊢ ∃ x ∈ ↑z, ∃ y ∈ ↑z, x ≠ y ∧ ¬G.Adj x y
Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite

Goal state before:
pp: r t : ℕ
v x✝ : Fin r × Fin t
⊢ x✝ ∈ (completeEquipartiteGraph r t).neighborSet v ↔ x✝ ∈ {v.1}ᶜ ×ˢ Set.univ

Tactic:
;

Goal state after:
r t : ℕ
v x✝ : Fin r × Fin t
⊢ x✝ ∈ (completeEquipartiteGraph r t).neighborSet v ↔ x✝ ∈ {v.1}ᶜ ×ˢ Set.univ
Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite

Goal state before:
pp: r t : ℕ
v a✝ : Fin r × Fin t
⊢ a✝ ∈ (completeEquipartiteGraph r t).neighborFinset v ↔ a✝ ∈ {v.1}ᶜ ×ˢ univ

Tactic:
;

Goal state after:
r t : ℕ
v a✝ : Fin r × Fin t
⊢ a✝ ∈ (completeEquipartiteGraph r t).neighborFinset v ↔ a✝ ∈ {v.1}ᶜ ×ˢ univ
Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite

Goal state before:
pp: r t : ℕ
| fun v ↦ (completeEquipartiteGraph r t).degree v

Tactic:
;

Goal state after:
r t : ℕ
| fun v ↦ (completeEquipartiteGraph r t).degree v
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan

Goal state before:
pp: case map_rel_iff'.inl
V : Type u_1
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
r : ℕ
h : G.IsTuranMaximal r
zm : ↥univ ≃ Fin #univ
zp :
  ∀ (a b : ↥univ),
    h.finpartition.part ↑a = h.finpartition.part ↑b ↔ ↑(zm a) % #h.finpartition.parts = ↑(zm b) % #h.finpartition.parts
a b : V
this : ¬G.Adj ↑⟨a, ⋯⟩ ↑⟨b, ⋯⟩ ↔ ↑(zm ⟨a, ⋯⟩) % #h.finpartition.parts = ↑(zm ⟨b, ⋯⟩) % #h.finpartition.parts
c : r ≤ Fintype.card V
⊢ ↑(zm ⟨a, ⋯⟩) % r = ↑(zm ⟨b, ⋯⟩) % r ↔ ↑(zm ⟨a, ⋯⟩) % r = ↑(zm ⟨b, ⋯⟩) % r

Tactic:
;

Goal state after:
case map_rel_iff'.inl
V : Type u_1
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
r : ℕ
h : G.IsTuranMaximal r
zm : ↥univ ≃ Fin #univ
zp :
  ∀ (a b : ↥univ),
    h.finpartition.part ↑a = h.finpartition.part ↑b ↔ ↑(zm a) % #h.finpartition.parts = ↑(zm b) % #h.finpartition.parts
a b : V
this : ¬G.Adj ↑⟨a, ⋯⟩ ↑⟨b, ⋯⟩ ↔ ↑(zm ⟨a, ⋯⟩) % #h.finpartition.parts = ↑(zm ⟨b, ⋯⟩) % #h.finpartition.parts
c : r ≤ Fintype.card V
⊢ ↑(zm ⟨a, ⋯⟩) % r = ↑(zm ⟨b, ⋯⟩) % r ↔ ↑(zm ⟨a, ⋯⟩) % r = ↑(zm ⟨b, ⋯⟩) % r
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan

Goal state before:
pp: case map_rel_iff'.inr
V : Type u_1
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
r : ℕ
h : G.IsTuranMaximal r
zm : ↥univ ≃ Fin #univ
zp :
  ∀ (a b : ↥univ),
    h.finpartition.part ↑a = h.finpartition.part ↑b ↔ ↑(zm a) % #h.finpartition.parts = ↑(zm b) % #h.finpartition.parts
a b : V
this : ¬G.Adj ↑⟨a, ⋯⟩ ↑⟨b, ⋯⟩ ↔ ↑(zm ⟨a, ⋯⟩) % #h.finpartition.parts = ↑(zm ⟨b, ⋯⟩) % #h.finpartition.parts
c : Fintype.card V < r
lc : ∀ (x : V), ↑(zm ⟨x, ⋯⟩) < Fintype.card V
⊢ ↑(zm ⟨a, ⋯⟩) % r = ↑(zm ⟨b, ⋯⟩) % r ↔ ↑(zm ⟨a, ⋯⟩) % r = ↑(zm ⟨b, ⋯⟩) % r

Tactic:
;

Goal state after:
case map_rel_iff'.inr
V : Type u_1
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
r : ℕ
h : G.IsTuranMaximal r
zm : ↥univ ≃ Fin #univ
zp :
  ∀ (a b : ↥univ),
    h.finpartition.part ↑a = h.finpartition.part ↑b ↔ ↑(zm a) % #h.finpartition.parts = ↑(zm b) % #h.finpartition.parts
a b : V
this : ¬G.Adj ↑⟨a, ⋯⟩ ↑⟨b, ⋯⟩ ↔ ↑(zm ⟨a, ⋯⟩) % #h.finpartition.parts = ↑(zm ⟨b, ⋯⟩) % #h.finpartition.parts
c : Fintype.card V < r
lc : ∀ (x : V), ↑(zm ⟨x, ⋯⟩) < Fintype.card V
⊢ ↑(zm ⟨a, ⋯⟩) % r = ↑(zm ⟨b, ⋯⟩) % r ↔ ↑(zm ⟨a, ⋯⟩) % r = ↑(zm ⟨b, ⋯⟩) % r
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Represents

Goal state before:
pp: V : Type u
G : SimpleGraph V
C : Set G.ConnectedComponent
x : Quot G.Reachable
hx : x ∈ C
⊢ G.connectedComponentMk x.out ∈ C

Tactic:
;

Goal state after:
V : Type u
G : SimpleGraph V
C : Set G.ConnectedComponent
x : Quot G.Reachable
hx : x ∈ C
⊢ G.connectedComponentMk x.out ∈ C
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan

Goal state before:
pp: case inl
n c : ℕ
⊢ (∑ w ∈ range 0, if c % 0 ≠ (n + w) % 0 then 1 else 0) = 0 - 1

pp: case inr
n r c : ℕ
hr : r > 0
⊢ (∑ w ∈ range r, if c % r ≠ (n + w) % r then 1 else 0) = r - 1

Tactic:
;

Goal state after:
case inl
n c : ℕ
⊢ (∑ w ∈ range 0, if c % 0 ≠ (n + w) % 0 then 1 else 0) = 0 - 1

case inr
n r c : ℕ
hr : r > 0
⊢ (∑ w ∈ range r, if c % r ≠ (n + w) % r then 1 else 0) = r - 1
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan

Goal state before:
pp: n r c : ℕ
hr : r > 0
this : #({i ∈ range r | c % r = (n + i) % r}) = 1
⊢ #({i ∈ range r | c % r ≠ (n + i) % r}) = r - #({i ∈ range r | c % r = (n + i) % r})

Tactic:
;

Goal state after:
n r c : ℕ
hr : r > 0
this : #({i ∈ range r | c % r = (n + i) % r}) = 1
⊢ #({i ∈ range r | c % r ≠ (n + i) % r}) = r - #({i ∈ range r | c % r = (n + i) % r})
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan

Goal state before:
pp: case inr.a
n r c : ℕ
hr : r > 0
⊢ ∀ {a b : ℕ}, a ∈ {i ∈ range r | c ≡ n + i [MOD r]} → b ∈ {i ∈ range r | c ≡ n + i [MOD r]} → a = b

Tactic:
;

Goal state after:
case inr.a
n r c : ℕ
hr : r > 0
⊢ ∀ {a b : ℕ}, a ∈ {i ∈ range r | c ≡ n + i [MOD r]} → b ∈ {i ∈ range r | c ≡ n + i [MOD r]} → a = b
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan

Goal state before:
pp: case a
n r c : ℕ
hr : r > 0
⊢ {i ∈ range r | c % r = (n + i) % r}.Nonempty

Tactic:
;

Goal state after:
case a
n r c : ℕ
hr : r > 0
⊢ {i ∈ range r | c % r = (n + i) % r}.Nonempty
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan

Goal state before:
pp: case h
n r c : ℕ
hr : r > 0
⊢ ((r - 1) * n + c) % r < r ∧ c % r = (n + ((r - 1) * n + c) % r) % r

Tactic:
;

Goal state after:
case h
n r c : ℕ
hr : r > 0
⊢ ((r - 1) * n + c) % r < r ∧ c % r = (n + ((r - 1) * n + c) % r) % r
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan

Goal state before:
pp: n r : ℕ
⊢ ((∑ i ∈ range (n + r), ∑ w ∈ range n, if i % r ≠ w % r then 1 else 0) +
      ∑ i ∈ range (n + r), ∑ w ∈ range r, if i % r ≠ (n + w) % r then 1 else 0) =
    (∑ x, ∑ i, if ↑x % r ≠ ↑i % r then 1 else 0) + 2 * (n * (r - 1)) + 2 * r.choose 2

Tactic:
sum_range_add,

Goal state after:
n r : ℕ
⊢ (((∑ x ∈ range n, ∑ w ∈ range n, if x % r ≠ w % r then 1 else 0) +
        ∑ x ∈ range r, ∑ w ∈ range n, if (n + x) % r ≠ w % r then 1 else 0) +
      ∑ i ∈ range (n + r), ∑ w ∈ range r, if i % r ≠ (n + w) % r then 1 else 0) =
    (∑ x, ∑ i, if ↑x % r ≠ ↑i % r then 1 else 0) + 2 * (n * (r - 1)) + 2 * r.choose 2