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 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
l3 : 0 < G.degree u
⊢ #G.edgeFinset < #G.edgeFinset + (G.replaceVertex s t).degree s - (G.replaceVertex s t).degree u

Tactic:
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
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)
w : SimpleGraph V
w₁ : DecidableRel ((G.replaceVertex s t).replaceVertex s u).Adj
left : ((G.replaceVertex s t).replaceVertex s u).CliqueFree (r + 1)
right right₁ : #G.edgeFinset < #((G.replaceVertex s t).replaceVertex s u).edgeFinset
right₂ : ∀ (nst : s ≠ t), #G.edgeFinset < #((G.replaceVertex s t).replaceVertex s u).edgeFinset
right₃ : ∀ (nst : s ≠ t) (ntu : t ≠ u), #G.edgeFinset < #((G.replaceVertex s t).replaceVertex s u).edgeFinset
right₄ :
  ∀ (nst : s ≠ t) (ntu : t ≠ u) (this : ¬(G.replaceVertex s t).Adj s u),
    #G.edgeFinset < #((G.replaceVertex s t).replaceVertex s u).edgeFinset
right₅ :
  ∀ (nst : s ≠ t) (ntu : t ≠ u) (this : ¬(G.replaceVertex s t).Adj s u),
    #G.edgeFinset < #G.edgeFinset + (G.replaceVertex s t).degree s - (G.replaceVertex s t).degree u
right₆ :
  ∀ (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.edgeFinset < #G.edgeFinset + (G.replaceVertex s t).degree s - (G.replaceVertex s t).degree u
right₇ :
  ∀ (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),
    #G.edgeFinset < #G.edgeFinset + (G.replaceVertex s t).degree s - (G.replaceVertex s t).degree u
right₈ :
  ∀ (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)
    (l3 : 0 < G.degree u),
    #G.edgeFinset < #G.edgeFinset + (G.replaceVertex s t).degree s - (G.replaceVertex s t).degree u
⊢ ∃ (G' : SimpleGraph V) (inst_2 : DecidableRel G'.Adj), G'.CliqueFree (r + 1) ∧ #G.edgeFinset < #G'.edgeFinset

Tactic:
classical
  use (G.replaceVertex s t).replaceVertex s u, inferInstance,
    (cf.replaceVertex s t).replaceVertex s u
  have nst : s ≠ t := fun a ↦ hsu (a ▸ h)
  have ntu : t ≠ u := G.ne_of_adj h
  have := (G.adj_replaceVertex_iff_of_ne s nst ntu.symm).not.mpr hsu
  rw [card_edgeFinset_replaceVertex_of_not_adj _ this,
    card_edgeFinset_replaceVertex_of_not_adj _ hst, dst, Nat.add_sub_cancel]
  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]
  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]
  have l3 : 0 < G.degree u := by rw [G.degree_pos_iff_exists_adj u]; use t, h.symm
  lia

Premises used: 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 : ℕ
h : G.IsTuranMaximal r
⊢ ∀ (x : V), ¬G.Adj x x

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan
Goal:
V : Type u_1
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
r : ℕ
h : G.IsTuranMaximal r
⊢ ∀ {x y : V}, ¬G.Adj x y → ¬G.Adj y x

Tactic:
simp [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 : V
h : G.IsTuranMaximal r
inst_2 : DecidableEq V
rw :
  t ∈ Finpartition.part (s := univ) (Finpartition.ofSetoid h.setoid) s ↔
    Finpartition.part h.finpartition s = Finpartition.part h.finpartition t
⊢ (h.setoid : V → V → Prop) s t ↔ Finpartition.part h.finpartition s = Finpartition.part h.finpartition t

Tactic:
rw [← Finpartition.mem_part_ofSetoid_iff_rel]

Premises used: Finpartition.mem_part_ofSetoid_iff_rel
-- 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
h : G.IsTuranMaximal r
inst_2 : DecidableEq V
fp : Finpartition (α := Finset V) univ := h.finpartition
change : t ∈ fp.part s ↔ fp.part s = fp.part t
⊢ t ∈ Finpartition.part (s := univ) (Finpartition.ofSetoid h.setoid) s ↔
    Finpartition.part h.finpartition s = Finpartition.part h.finpartition t

Tactic:
change t ∈ fp.part s ↔ fp.part s = fp.part t

Premises used: Finpartition.part
-- 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
h : G.IsTuranMaximal r
inst_2 : DecidableEq V
fp : Finpartition (α := Finset V) univ := h.finpartition
rw : fp.part t = fp.part s ↔ fp.part s = fp.part t
rw₁ rw₂ : fp.part s = fp.part t ↔ fp.part s = fp.part t
⊢ t ∈ fp.part s ↔ fp.part s = fp.part t

Tactic:
rw [fp.mem_part_iff_part_eq_part (mem_univ t) (mem_univ s), eq_comm]

Premises used: Finpartition.mem_part_iff_part_eq_part, Finset.mem_univ, eq_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 : V
h : G.IsTuranMaximal r
inst_2 : DecidableEq V
⊢ G.degree s = Finset.card.{u_1} (α := V) {t : V | G.Adj s t}

Tactic:
simp [← card_neighborFinset_eq_degree, neighborFinset]

Premises used: SimpleGraph.neighborFinset, SimpleGraph.card_neighborFinset_eq_degree
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan
Goal:
V : Type u_1
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
r : ℕ
s : V
h : G.IsTuranMaximal r
inst_2 : DecidableEq V
e_a : {t : V | ¬G.Adj s t} = Finpartition.part h.finpartition s
⊢ Fintype.card V - Finset.card.{u_1} (α := V) {t : V | ¬G.Adj s t} =
    Fintype.card V - #(Finpartition.part h.finpartition s)

Tactic:
congr
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan
Goal:
V : Type u_1
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
r : ℕ
s : V
h : G.IsTuranMaximal r
inst_2 : DecidableEq V
e_a : ∀ (a : V), Membership.mem (γ := Finset V) {t : V | ¬G.Adj s t} a ↔ a ∈ Finpartition.part h.finpartition s
⊢ {t : V | ¬G.Adj s t} = Finpartition.part h.finpartition s

Tactic:
ext
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan
Goal:
V : Type u_1
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
r : ℕ
s : V
h : G.IsTuranMaximal r
inst_2 : DecidableEq V
a : V
e_a : Membership.mem (γ := Finset V) univ a ∧ ¬G.Adj s a ↔ a ∈ Finpartition.part h.finpartition s
⊢ Membership.mem (γ := Finset V) {t : V | ¬G.Adj s t} a ↔ a ∈ Finpartition.part h.finpartition s

Tactic:
rw [mem_filter]

Premises used: Finset.mem_filter
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan
Goal:
V : Type u_1
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
r : ℕ
s : V
h : G.IsTuranMaximal r
inst_2 : DecidableEq V
a : V
⊢ (h.setoid : V → V → Prop) s a ↔ a ∈ Finpartition.part (s := univ) (Finpartition.ofSetoid h.setoid) s

Tactic:
Finpartition.mem_part_ofSetoid_iff_rel.symm

Premises used: Finpartition.mem_part_ofSetoid_iff_rel, Iff.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 : V
h : G.IsTuranMaximal r
inst_2 : DecidableEq V
a : V
h₁ : Membership.mem (γ := Finset V) univ a ∧ ¬G.Adj s a ↔ (h.setoid : V → V → Prop) s a
⊢ Membership.mem (γ := Finset V) univ a ∧ ¬G.Adj s a ↔ a ∈ Finpartition.part h.finpartition s

Tactic:
convert! Finpartition.mem_part_ofSetoid_iff_rel.symm

Premises used: Finpartition.mem_part_ofSetoid_iff_rel, Iff.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 : V
h : G.IsTuranMaximal r
inst_2 : DecidableEq V
a : V
⊢ Membership.mem (γ := Finset V) univ a ∧ ¬G.Adj s a ↔ (h.setoid : V → V → Prop) s a

Tactic:
simp +instances [setoid]

Premises used: SimpleGraph.IsTuranMaximal.setoid
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan
Goal:
V : Type u_1
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
r : ℕ
h : G.IsTuranMaximal r
inst_2 : DecidableEq V
set :
  let fp : Finpartition (α := Finset V) univ := h.finpartition;
  fp.IsEquipartition
⊢ Finpartition.IsEquipartition h.finpartition

Tactic:
set fp := h.finpartition

Premises used: SimpleGraph.IsTuranMaximal.finpartition
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan
Goal:
V : Type u_1
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
r : ℕ
h : G.IsTuranMaximal r
inst_2 : DecidableEq V
fp : Finpartition (α := Finset V) univ := h.finpartition
by_contra : ∀ (hn : ¬fp.IsEquipartition), False
⊢ fp.IsEquipartition

Tactic:
by_contra hn
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan
Goal:
V : Type u_1
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
r : ℕ
h : G.IsTuranMaximal r
inst_2 : DecidableEq V
fp : Finpartition (α := Finset V) univ := h.finpartition
hn : ¬fp.IsEquipartition
⊢ ∃ a ∈ fp.parts, ∃ b ∈ fp.parts, #b + 1 < #a

Tactic:
rw [Finpartition.not_isEquipartition] at hn

Premises used: Finpartition.not_isEquipartition
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan
Goal:
V : Type u_1
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
r : ℕ
h : G.IsTuranMaximal r
inst_2 : DecidableEq V
fp : Finpartition (α := Finset V) univ := h.finpartition
hn : ∃ a ∈ fp.parts, ∃ b ∈ fp.parts, #b + 1 < #a
obtain :
  ∀ (large : Finset V) (hl : large ∈ fp.parts) (small : Finset V) (hs : small ∈ fp.parts) (ineq : #small + 1 < #large),
    False
⊢ False

Tactic:
obtain ⟨large, hl, small, hs, ineq⟩ := hn
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan
Goal:
V : Type u_1
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
r : ℕ
h : G.IsTuranMaximal r
inst_2 : DecidableEq V
fp : Finpartition (α := Finset V) univ := h.finpartition
large : Finset V
hl : large ∈ fp.parts
small : Finset V
hs : small ∈ fp.parts
ineq : #small + 1 < #large
obtain : ∀ (w : V) (hw : w ∈ large), False
⊢ False

Tactic:
obtain ⟨w, hw⟩ := fp.nonempty_of_mem_parts hl

Premises used: Finpartition.nonempty_of_mem_parts
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan
Goal:
V : Type u_1
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
r : ℕ
h : G.IsTuranMaximal r
inst_2 : DecidableEq V
fp : Finpartition (α := Finset V) 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
obtain : ∀ (v : V) (hv : v ∈ small), False
⊢ False

Tactic:
obtain ⟨v, hv⟩ := fp.nonempty_of_mem_parts hs

Premises used: Finpartition.nonempty_of_mem_parts
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan
Goal:
V : Type u_1
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
r : ℕ
h : G.IsTuranMaximal r
inst_2 : DecidableEq V
fp : Finpartition (α := Finset V) 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
apply : ¬G.IsTuranMaximal r
⊢ False

Tactic:
apply absurd h

Premises used: absurd
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan
Goal:
V : Type u_1
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
r : ℕ
h : G.IsTuranMaximal r
inst_2 : DecidableEq V
fp : Finpartition (α := Finset V) 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
push :
  ∀ (_ : G.CliqueFree (r + 1)),
    ∃ (G' : SimpleGraph V) (inst_3 : DecidableRel G'.Adj), G'.CliqueFree (r + 1) ∧ #G.edgeFinset < #G'.edgeFinset
⊢ ¬(G.CliqueFree (r + 1) ∧
      ∀ ⦃G' : SimpleGraph V⦄ [inst_3 : DecidableRel G'.Adj], G'.CliqueFree (r + 1) → #G'.edgeFinset ≤ #G.edgeFinset)

Tactic:
push Not

Premises used: Not
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan
Goal:
V : Type u_1
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
r : ℕ
h : G.IsTuranMaximal r
inst_2 : DecidableEq V
fp : Finpartition (α := Finset V) 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)
right : #G.edgeFinset < #(G.replaceVertex v w).edgeFinset
⊢ ∃ (G' : SimpleGraph V) (inst_3 : DecidableRel G'.Adj), G'.CliqueFree (r + 1) ∧ #G.edgeFinset < #G'.edgeFinset

Tactic:
use G.replaceVertex v w, inferInstance, cf.replaceVertex v w

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 : ℕ
h : G.IsTuranMaximal r
inst_2 : DecidableEq V
fp : Finpartition (α := Finset V) 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)
⊢ fp.part w = large

Tactic:
have large_eq := fp.part_eq_of_mem hl hw
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan
Goal:
V : Type u_1
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
r : ℕ
h : G.IsTuranMaximal r
inst_2 : DecidableEq V
fp : Finpartition (α := Finset V) 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
⊢ fp.part v = small

Tactic:
have small_eq := fp.part_eq_of_mem hs hv
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan
Goal:
V : Type u_1
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
r : ℕ
h : G.IsTuranMaximal r
inst_2 : DecidableEq V
fp : Finpartition (α := Finset V) 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
by_contra : ∀ (hn : ¬G.Adj v w), False
⊢ G.Adj v w

Tactic:
by_contra hn
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan
Goal:
V : Type u_1
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
r : ℕ
h : G.IsTuranMaximal r
inst_2 : DecidableEq V
fp : Finpartition (α := Finset V) 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
⊢ small = large

Tactic:
rw [h.not_adj_iff_part_eq, small_eq, large_eq] at hn

Premises used: SimpleGraph.IsTuranMaximal.not_adj_iff_part_eq
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan
Goal:
V : Type u_1
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
r : ℕ
h : G.IsTuranMaximal r
inst_2 : DecidableEq V
fp : Finpartition (α := Finset V) 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 : small = large
rw :
  ∀ (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
⊢ False

Tactic:
rw [hn] at ineq
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan
Goal:
V : Type u_1
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
r : ℕ
h : G.IsTuranMaximal r
inst_2 : DecidableEq V
fp : Finpartition (α := Finset V) 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:
lia
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan
Goal:
V : Type u_1
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
r : ℕ
h : G.IsTuranMaximal r
inst_2 : DecidableEq V
fp : Finpartition (α := Finset V) 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:
have ha : G.Adj v w := by
    by_contra hn; rw [h.not_adj_iff_part_eq, small_eq, large_eq] at hn
    rw [hn] at ineq; lia
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan
Goal:
V : Type u_1
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
r : ℕ
h : G.IsTuranMaximal r
inst_2 : DecidableEq V
fp : Finpartition (α := Finset V) 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
right : #G.edgeFinset < #G.edgeFinset + (Fintype.card V - #small) - (Fintype.card V - #large) - 1
⊢ #G.edgeFinset < #(G.replaceVertex v w).edgeFinset

Tactic:
rw [G.card_edgeFinset_replaceVertex_of_adj ha,
    degree_eq_card_sub_part_card h, small_eq, degree_eq_card_sub_part_card h, large_eq]

Premises used: SimpleGraph.card_edgeFinset_replaceVertex_of_adj, SimpleGraph.IsTuranMaximal.degree_eq_card_sub_part_card
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan
Goal:
V : Type u_1
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
r : ℕ
h : G.IsTuranMaximal r
inst_2 : DecidableEq V
fp : Finpartition (α := Finset V) 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:
simpa using card_le_card large.subset_univ

Premises used: Finset.card_le_card, Finset.subset_univ
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan
Goal:
V : Type u_1
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
r : ℕ
h : G.IsTuranMaximal r
inst_2 : DecidableEq V
fp : Finpartition (α := Finset V) 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:
have : #large ≤ card V := by simpa using card_le_card large.subset_univ
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan
Goal:
V : Type u_1
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
r : ℕ
h : G.IsTuranMaximal r
inst_2 : DecidableEq V
fp : Finpartition (α := Finset V) 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
this : #large ≤ Fintype.card V
⊢ #G.edgeFinset < #G.edgeFinset + (Fintype.card V - #small) - (Fintype.card V - #large) - 1

Tactic:
lia
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan
Goal:
V : Type u_1
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
r : ℕ
h : G.IsTuranMaximal r
inst_2 : DecidableEq V
by_contra! : ∀ (l : r < #(Finpartition.parts h.finpartition)), False
⊢ #(Finpartition.parts h.finpartition) ≤ r

Tactic:
by_contra! l
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan
Goal:
V : Type u_1
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
r : ℕ
h : G.IsTuranMaximal r
inst_2 : DecidableEq V
l : r < #(Finpartition.parts h.finpartition)
obtain :
  ∀ (z : Finset V)
    (hz :
      Set.BijOn (Finpartition.part h.finpartition) (↑z : Set V)
        (↑(Finpartition.parts h.finpartition) : Set (Finset V))),
    False
⊢ False

Tactic:
obtain ⟨z, -, hz⟩ := h.finpartition.exists_subset_part_bijOn

Premises used: SimpleGraph.IsTuranMaximal.finpartition, Finpartition.exists_subset_part_bijOn
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan
Goal:
V : Type u_1
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
r : ℕ
h : G.IsTuranMaximal r
inst_2 : DecidableEq V
l : r < #(Finpartition.parts h.finpartition)
z : Finset V
hz : Set.BijOn (Finpartition.part h.finpartition) (↑z : Set V) (↑(Finpartition.parts h.finpartition) : Set (Finset V))
⊢ ¬G.CliqueFree #z

Tactic:
IsNClique.not_cliqueFree ⟨fun v hv w hw hn ↦ ?_, rfl⟩

Premises used: SimpleGraph.IsNClique.mk, SimpleGraph.IsNClique.not_cliqueFree, rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan
Goal:
V : Type u_1
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
r : ℕ
h : G.IsTuranMaximal r
inst_2 : DecidableEq V
l : r < #(Finpartition.parts h.finpartition)
z : Finset V
hz : Set.BijOn (Finpartition.part h.finpartition) (↑z : Set V) (↑(Finpartition.parts h.finpartition) : Set (Finset V))
refine : ∀ (v : V) (hv : v ∈ (↑z : Set V)) (w : V) (hw : w ∈ (↑z : Set V)) (hn : v ≠ w), G.Adj v w
⊢ ¬G.CliqueFree #z

Tactic:
refine IsNClique.not_cliqueFree ⟨fun v hv w hw hn ↦ ?_, rfl⟩

Premises used: SimpleGraph.IsNClique.mk, SimpleGraph.IsNClique.not_cliqueFree, rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan
Goal:
V : Type u_1
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
r : ℕ
h : G.IsTuranMaximal r
inst_2 : DecidableEq V
l : r < #(Finpartition.parts h.finpartition)
z : Finset V
hz : Set.BijOn (Finpartition.part h.finpartition) (↑z : Set V) (↑(Finpartition.parts h.finpartition) : Set (Finset V))
v : V
hv : v ∈ (↑z : Set V)
w : V
hw : w ∈ (↑z : Set V)
hn : v ≠ w
contrapose : ∀ (hn : ¬G.Adj v w), v = w
⊢ G.Adj v w

Tactic:
contrapose hn
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan
Goal:
V : Type u_1
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
r : ℕ
h : G.IsTuranMaximal r
inst_2 : DecidableEq V
l : r < #(Finpartition.parts h.finpartition)
z : Finset V
hz : Set.BijOn (Finpartition.part h.finpartition) (↑z : Set V) (↑(Finpartition.parts h.finpartition) : Set (Finset V))
v : V
hv : v ∈ (↑z : Set V)
w : V
hw : w ∈ (↑z : Set V)
hn rwa rwa₁ rwa₂ rwa₃ : ¬G.Adj v w
⊢ Finpartition.part h.finpartition v = Finpartition.part h.finpartition w

Tactic:
rwa [← h.not_adj_iff_part_eq]

Premises used: SimpleGraph.IsTuranMaximal.not_adj_iff_part_eq
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan
Goal:
V : Type u_1
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
r : ℕ
h : G.IsTuranMaximal r
inst_2 : DecidableEq V
l : r < #(Finpartition.parts h.finpartition)
z : Finset V
hz : Set.BijOn (Finpartition.part h.finpartition) (↑z : Set V) (↑(Finpartition.parts h.finpartition) : Set (Finset V))
v : V
hv : v ∈ (↑z : Set V)
w : V
hw : w ∈ (↑z : Set V)
hn : ¬G.Adj v w
⊢ v = w

Tactic:
exact hz.injOn hv hw (by rwa [← h.not_adj_iff_part_eq])

Premises used: Set.BijOn.injOn