awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan
Goal:
V : Type u_1
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
r : ℕ
s t : V
hn : ¬G.Adj s t
h : G.degree s ≠ G.degree t
cf : G.CliqueFree (r + 1)
this :
  ∀ {G : SimpleGraph V} [inst_2 : DecidableRel G.Adj] {s t : V} (hn : ¬G.Adj s t) (h : G.degree s ≠ G.degree t)
    (cf : G.CliqueFree (r + 1)) (hd : G.degree t < G.degree s),
    ∃ (G' : SimpleGraph V) (inst_3 : DecidableRel G'.Adj), G'.CliqueFree (r + 1) ∧ #G.edgeFinset < #G'.edgeFinset
hd : G.degree s < G.degree t
⊢ ∃ (G' : SimpleGraph V) (inst_2 : DecidableRel G'.Adj), G'.CliqueFree (r + 1) ∧ #G.edgeFinset < #G'.edgeFinset

Tactic:
exact this (by rwa [adj_comm] at hn) hd.ne' cf hd

Premises used: LT.lt.ne'
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan
Goal:
V : Type u_1
inst : Fintype V
G_1 : SimpleGraph V
inst_1 : DecidableRel G_1.Adj
r : ℕ
s_1 t_1 : V
G : SimpleGraph V
inst_2 : DecidableRel G.Adj
s t : V
hn : ¬G.Adj s t
h : G.degree s ≠ G.degree t
cf : G.CliqueFree (r + 1)
hd : G.degree t < G.degree s
right : #G.edgeFinset < #(G.replaceVertex s t).edgeFinset
⊢ ∃ (G' : SimpleGraph V) (inst_3 : DecidableRel G'.Adj), G'.CliqueFree (r + 1) ∧ #G.edgeFinset < #G'.edgeFinset

Tactic:
use G.replaceVertex s t, inferInstance, cf.replaceVertex s t

Premises used: SimpleGraph.CliqueFree.replaceVertex, SimpleGraph.replaceVertex
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan
Goal:
V : Type u_1
inst : Fintype V
G_1 : SimpleGraph V
inst_1 : DecidableRel G_1.Adj
r : ℕ
s_1 t_1 : V
G : SimpleGraph V
inst_2 : DecidableRel G.Adj
s t : V
hn : ¬G.Adj s t
h : G.degree s ≠ G.degree t
cf : G.CliqueFree (r + 1)
hd : G.degree t < G.degree s
⊢ #(G.replaceVertex s t).edgeFinset = #G.edgeFinset + G.degree s - G.degree t

Tactic:
have := G.card_edgeFinset_replaceVertex_of_not_adj hn
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan
Goal:
V : Type u_1
inst : Fintype V
G_1 : SimpleGraph V
inst_1 : DecidableRel G_1.Adj
r : ℕ
s_1 t_1 : V
G : SimpleGraph V
inst_2 : DecidableRel G.Adj
s t : V
hn : ¬G.Adj s t
h : G.degree s ≠ G.degree t
cf : G.CliqueFree (r + 1)
hd : G.degree t < G.degree s
this : #(G.replaceVertex s t).edgeFinset = #G.edgeFinset + G.degree s - G.degree t
⊢ #G.edgeFinset < #(G.replaceVertex s t).edgeFinset

Tactic:
lia
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan
Goal:
V : Type u_1
inst : Fintype V
G_1 : SimpleGraph V
inst_1 : DecidableRel G_1.Adj
r : ℕ
s_1 t_1 : V
G : SimpleGraph V
inst_2 : DecidableRel G.Adj
s t : V
hn : ¬G.Adj s t
h : G.degree s ≠ G.degree t
cf : G.CliqueFree (r + 1)
hd : G.degree t < G.degree s
w : SimpleGraph V
w₁ : DecidableRel (G.replaceVertex s t).Adj
left : (G.replaceVertex s t).CliqueFree (r + 1)
right right₁ : #G.edgeFinset < #(G.replaceVertex s t).edgeFinset
right₂ :
  ∀ (this : #(G.replaceVertex s t).edgeFinset = #G.edgeFinset + G.degree s - G.degree t),
    #G.edgeFinset < #(G.replaceVertex s t).edgeFinset
⊢ ∃ (G' : SimpleGraph V) (inst_3 : DecidableRel G'.Adj), G'.CliqueFree (r + 1) ∧ #G.edgeFinset < #G'.edgeFinset

Tactic:
classical
  use G.replaceVertex s t, inferInstance, cf.replaceVertex s t
  have := G.card_edgeFinset_replaceVertex_of_not_adj hn
  lia
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan
Goal:
V : Type u_1
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
r : ℕ
s t u : V
h : G.IsTuranMaximal r
hts : ¬G.Adj t s
hsu : ¬G.Adj s u
⊢ ¬G.Adj s t

Tactic:
have hst : ¬G.Adj s t := fun a ↦ hts a.symm
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan
Goal:
V : Type u_1
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
r : ℕ
s t u : V
h : G.IsTuranMaximal r
hts : ¬G.Adj t s
hsu : ¬G.Adj s u
hst : ¬G.Adj s t
⊢ G.degree s = G.degree t

Tactic:
have dst := h.degree_eq_of_not_adj hst
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan
Goal:
V : Type u_1
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
r : ℕ
s t u : V
h : G.IsTuranMaximal r
hts : ¬G.Adj t s
hsu : ¬G.Adj s u
hst : ¬G.Adj s t
dst : G.degree s = G.degree t
⊢ G.degree s = G.degree u

Tactic:
have dsu := h.degree_eq_of_not_adj hsu
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan
Goal:
V : Type u_1
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
r : ℕ
s t u : V
h : G.IsTuranMaximal r
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.CliqueFree (r + 1) ∧
    ∀ ⦃G' : SimpleGraph V⦄ [inst_2 : DecidableRel G'.Adj], G'.CliqueFree (r + 1) → #G'.edgeFinset ≤ #G.edgeFinset

Tactic:
rw [IsTuranMaximal, IsExtremal] at h

Premises used: SimpleGraph.IsExtremal, SimpleGraph.IsTuranMaximal
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan
Goal:
V : Type u_1
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
r : ℕ
s t u : V
h : G.IsTuranMaximal r
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.CliqueFree (r + 1) ∧
    ∀ ⦃G' : SimpleGraph V⦄ [inst_2 : DecidableRel G'.Adj], G'.CliqueFree (r + 1) → #G'.edgeFinset ≤ #G.edgeFinset
⊢ ¬G.Adj t s

Tactic:
rw [IsTuranMaximal, IsExtremal] at h

Premises used: SimpleGraph.IsExtremal, SimpleGraph.IsTuranMaximal
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan
Goal:
V : Type u_1
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
r : ℕ
s t u : V
h : G.IsTuranMaximal r
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.CliqueFree (r + 1) ∧
    ∀ ⦃G' : SimpleGraph V⦄ [inst_2 : DecidableRel G'.Adj], G'.CliqueFree (r + 1) → #G'.edgeFinset ≤ #G.edgeFinset
hts₁ : ¬G.Adj t s
⊢ ¬G.Adj s u

Tactic:
rw [IsTuranMaximal, IsExtremal] at h

Premises used: SimpleGraph.IsExtremal, SimpleGraph.IsTuranMaximal
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan
Goal:
V : Type u_1
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
r : ℕ
s t u : V
h : G.IsTuranMaximal r
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.CliqueFree (r + 1) ∧
    ∀ ⦃G' : SimpleGraph V⦄ [inst_2 : DecidableRel G'.Adj], G'.CliqueFree (r + 1) → #G'.edgeFinset ≤ #G.edgeFinset
hts₁ : ¬G.Adj t s
hsu₁ : ¬G.Adj s u
⊢ ¬G.Adj s t

Tactic:
rw [IsTuranMaximal, IsExtremal] at h

Premises used: SimpleGraph.IsExtremal, SimpleGraph.IsTuranMaximal
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan
Goal:
V : Type u_1
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
r : ℕ
s t u : V
h : G.IsTuranMaximal r
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.CliqueFree (r + 1) ∧
    ∀ ⦃G' : SimpleGraph V⦄ [inst_2 : 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
⊢ G.degree s = G.degree t

Tactic:
rw [IsTuranMaximal, IsExtremal] at h

Premises used: SimpleGraph.IsExtremal, SimpleGraph.IsTuranMaximal
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan
Goal:
V : Type u_1
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
r : ℕ
s t u : V
h : G.IsTuranMaximal r
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.CliqueFree (r + 1) ∧
    ∀ ⦃G' : SimpleGraph V⦄ [inst_2 : 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
⊢ G.degree s = G.degree u

Tactic:
rw [IsTuranMaximal, IsExtremal] at h

Premises used: SimpleGraph.IsExtremal, SimpleGraph.IsTuranMaximal
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan
Goal:
V : Type u_1
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
r : ℕ
s t u : V
h :
  G.CliqueFree (r + 1) ∧
    ∀ ⦃G' : SimpleGraph V⦄ [inst_2 : 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
contrapose! :
  ∀ (h : G.Adj t u) (_ : G.CliqueFree (r + 1)),
    ∃ (G' : SimpleGraph V) (inst_2 : DecidableRel G'.Adj), G'.CliqueFree (r + 1) ∧ #G.edgeFinset < #G'.edgeFinset
⊢ ¬G.Adj t u

Tactic:
contrapose! h
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan
Goal:
V : Type u_1
inst : Fintype V
G : SimpleGraph V
inst_1 : 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)
right : #G.edgeFinset < #((G.replaceVertex s t).replaceVertex s u).edgeFinset
⊢ ∃ (G' : SimpleGraph V) (inst_2 : DecidableRel G'.Adj), G'.CliqueFree (r + 1) ∧ #G.edgeFinset < #G'.edgeFinset

Tactic:
use (G.replaceVertex s t).replaceVertex s u, inferInstance,
    (cf.replaceVertex s t).replaceVertex s u

Premises used: SimpleGraph.CliqueFree.replaceVertex, SimpleGraph.replaceVertex
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan
Goal:
V : Type u_1
inst : Fintype V
G : SimpleGraph V
inst_1 : 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)
⊢ s ≠ t

Tactic:
have nst : s ≠ t := fun a ↦ hsu (a ▸ h)
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan
Goal:
V : Type u_1
inst : Fintype V
G : SimpleGraph V
inst_1 : 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
⊢ t ≠ u

Tactic:
have ntu : t ≠ u := G.ne_of_adj h
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan
Goal:
V : Type u_1
inst : Fintype V
G : SimpleGraph V
inst_1 : 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
⊢ ¬(G.replaceVertex s t).Adj s u

Tactic:
have := (G.adj_replaceVertex_iff_of_ne s nst ntu.symm).not.mpr hsu
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan
Goal:
V : Type u_1
inst : Fintype V
G : SimpleGraph V
inst_1 : 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
right : #G.edgeFinset < #G.edgeFinset + (G.replaceVertex s t).degree s - (G.replaceVertex s t).degree u
⊢ #G.edgeFinset < #((G.replaceVertex s t).replaceVertex s u).edgeFinset

Tactic:
rw [card_edgeFinset_replaceVertex_of_not_adj _ this,
    card_edgeFinset_replaceVertex_of_not_adj _ hst, dst, Nat.add_sub_cancel]

Premises used: SimpleGraph.card_edgeFinset_replaceVertex_of_not_adj, Nat.add_sub_cancel
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan
Goal:
V : Type u_1
inst : Fintype V
G : SimpleGraph V
inst_1 : 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
e_s : (G.replaceVertex s t).neighborFinset s = G.neighborFinset s
⊢ #((G.replaceVertex s t).neighborFinset s) = #(G.neighborFinset s)

Tactic:
congr 1
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan
Goal:
V : Type u_1
inst : Fintype V
G : SimpleGraph V
inst_1 : 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
e_s : ∀ (v : V), v ∈ (G.replaceVertex s t).neighborFinset s ↔ v ∈ G.neighborFinset s
⊢ (G.replaceVertex s t).neighborFinset s = G.neighborFinset s

Tactic:
ext v
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan
Goal:
V : Type u_1
inst : Fintype V
G : SimpleGraph V
inst_1 : 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
v : V
e_s : (G.replaceVertex s t).Adj s v ↔ G.Adj s v
⊢ v ∈ (G.replaceVertex s t).neighborFinset s ↔ v ∈ G.neighborFinset s

Tactic:
simp_rw [mem_neighborFinset]

Premises used: SimpleGraph.mem_neighborFinset
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan
Goal:
V : Type u_1
inst : Fintype V
G : SimpleGraph V
inst_1 : 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
v : V
pos : ∀ (eq : v = t), (G.replaceVertex s t).Adj s v ↔ G.Adj s v
neg : ∀ (eq : ¬v = t), (G.replaceVertex s t).Adj s v ↔ G.Adj s v
⊢ (G.replaceVertex s t).Adj s v ↔ G.Adj s v

Tactic:
by_cases eq : v = t
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan
Goal:
V : Type u_1
inst : Fintype V
G : SimpleGraph V
inst_1 : 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
v : V
eq : v = t
⊢ (G.replaceVertex s t).Adj s v ↔ G.Adj s v

Tactic:
simpa only [eq, not_adj_replaceVertex_same, false_iff]

Premises used: false_iff, SimpleGraph.not_adj_replaceVertex_same
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan
Goal:
V : Type u_1
inst : Fintype V
G : SimpleGraph V
inst_1 : 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
v : V
eq : ¬v = t
neg neg₁ : G.Adj s v ↔ G.Adj s v
⊢ (G.replaceVertex s t).Adj s v ↔ G.Adj s v

Tactic:
rw [G.adj_replaceVertex_iff_of_ne s nst eq]

Premises used: SimpleGraph.adj_replaceVertex_iff_of_ne
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan
Goal:
V : Type u_1
inst : Fintype V
G : SimpleGraph V
inst_1 : 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).degree s = G.degree s

Tactic:
have l1 : (G.replaceVertex s t).degree s = G.degree s := by
    unfold degree; congr 1; ext v
    simp_rw [mem_neighborFinset]
    by_cases eq : v = t
    · simpa only [eq, not_adj_replaceVertex_same, false_iff]
    · rw [G.adj_replaceVertex_iff_of_ne s nst eq]
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan
Goal:
V : Type u_1
inst : Fintype V
G : SimpleGraph V
inst_1 : 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
⊢ {t} ⊆ G.neighborFinset u

Tactic:
simp [h.symm]

Premises used: SimpleGraph.Adj.symm
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan
Goal:
V : Type u_1
inst : Fintype V
G : SimpleGraph V
inst_1 : 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
rw : #((G.replaceVertex s t).neighborFinset u) = #(G.neighborFinset u \ {t})
⊢ (G.replaceVertex s t).degree u = G.degree u - 1

Tactic:
rw [degree, degree, ← card_singleton t, ← card_sdiff_of_subset (by simp [h.symm])]

Premises used: Finset.card_sdiff_of_subset, SimpleGraph.degree, Finset.card_singleton
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan
Goal:
V : Type u_1
inst : Fintype V
G : SimpleGraph V
inst_1 : 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
e_s : (G.replaceVertex s t).neighborFinset u = G.neighborFinset u \ {t}
⊢ #((G.replaceVertex s t).neighborFinset u) = #(G.neighborFinset u \ {t})

Tactic:
congr 1
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan
Goal:
V : Type u_1
inst : Fintype V
G : SimpleGraph V
inst_1 : 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
e_s : ∀ (v : V), v ∈ (G.replaceVertex s t).neighborFinset u ↔ v ∈ G.neighborFinset u \ {t}
⊢ (G.replaceVertex s t).neighborFinset u = G.neighborFinset u \ {t}

Tactic:
ext v
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan
Goal:
V : Type u_1
inst : Fintype V
G : SimpleGraph V
inst_1 : 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
v : V
e_s :
  (if u = t then if v = t then False else G.Adj s v else if v = t then G.Adj u s else G.Adj u v) ↔
    v ∈ G.neighborFinset u ∧ ¬v = t
⊢ v ∈ (G.replaceVertex s t).neighborFinset u ↔ v ∈ G.neighborFinset u \ {t}

Tactic:
simp_rw [mem_neighborFinset, mem_sdiff, mem_singleton, replaceVertex]

Premises used: Finset.mem_singleton, SimpleGraph.replaceVertex, Finset.mem_sdiff, SimpleGraph.mem_neighborFinset
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan
Goal:
V : Type u_1
inst : Fintype V
G : SimpleGraph V
inst_1 : 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
v : V
pos : u = t → v = t → (False ↔ v ∈ G.neighborFinset u ∧ ¬v = t)
neg : u = t → ¬v = t → (G.Adj s v ↔ v ∈ G.neighborFinset u ∧ ¬v = t)
pos₁ : ¬u = t → v = t → (G.Adj u s ↔ v ∈ G.neighborFinset u ∧ ¬v = t)
neg₁ : ¬u = t → ¬v = t → (G.Adj u v ↔ v ∈ G.neighborFinset u ∧ ¬v = t)
⊢ (if u = t then if v = t then False else G.Adj s v else if v = t then G.Adj u s else G.Adj u v) ↔
    v ∈ G.neighborFinset u ∧ ¬v = t

Tactic:
split_ifs
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan
Goal:
V : Type u_1
inst : Fintype V
G : SimpleGraph V
inst_1 : 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
v : V
h_1 : u = t
h_2 : v = t
⊢ False ↔ v ∈ G.neighborFinset u ∧ ¬v = t

Tactic:
simp_all [adj_comm]

Premises used: SimpleGraph.adj_comm
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan
Goal:
V : Type u_1
inst : Fintype V
G : SimpleGraph V
inst_1 : 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
v : V
h_1 : u = t
h_2 : ¬v = t
⊢ G.Adj s v ↔ v ∈ G.neighborFinset u ∧ ¬v = t

Tactic:
simp_all [adj_comm]

Premises used: SimpleGraph.adj_comm
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan
Goal:
V : Type u_1
inst : Fintype V
G : SimpleGraph V
inst_1 : 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
v : V
h_1 : ¬u = t
h_2 : v = t
⊢ G.Adj u s ↔ v ∈ G.neighborFinset u ∧ ¬v = t

Tactic:
simp_all [adj_comm]

Premises used: SimpleGraph.adj_comm
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan
Goal:
V : Type u_1
inst : Fintype V
G : SimpleGraph V
inst_1 : 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
v : V
h_1 : ¬u = t
h_2 : ¬v = t
⊢ G.Adj u v ↔ v ∈ G.neighborFinset u ∧ ¬v = t

Tactic:
simp_all [adj_comm]

Premises used: SimpleGraph.adj_comm
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan
Goal:
V : Type u_1
inst : Fintype V
G : SimpleGraph V
inst_1 : 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:
have l2 : (G.replaceVertex s t).degree u = G.degree u - 1 := by
    rw [degree, degree, ← card_singleton t, ← card_sdiff_of_subset (by simp [h.symm])]
    congr 1; ext v
    simp_rw [mem_neighborFinset, mem_sdiff, mem_singleton, replaceVertex]
    split_ifs <;> simp_all [adj_comm]
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan
Goal:
V : Type u_1
inst : Fintype V
G : SimpleGraph V
inst_1 : 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
rw : ∃ (w : V), G.Adj u w
⊢ 0 < G.degree u

Tactic:
rw [G.degree_pos_iff_exists_adj u]

Premises used: SimpleGraph.degree_pos_iff_exists_adj
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan
Goal:
V : Type u_1
inst : Fintype V
G : SimpleGraph V
inst_1 : 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 : V
h₁ : G.Adj u t
⊢ ∃ (w : V), G.Adj u w

Tactic:
use t, h.symm

Premises used: SimpleGraph.Adj.symm
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan
Goal:
V : Type u_1
inst : Fintype V
G : SimpleGraph V
inst_1 : 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:
have l3 : 0 < G.degree u := by rw [G.degree_pos_iff_exists_adj u]; use t, h.symm