awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Extremal.Turan (goal)
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
⊢ ∃ (G' : SimpleGraph V) (inst_2 : DecidableRel G'.Adj), G'.CliqueFree (r + 1) ∧ #G.edgeFinset < #G'.edgeFinset
have 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
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
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Extremal.Turan (goal)
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
⊢ ∃ (G' : SimpleGraph V) (inst_2 : DecidableRel G'.Adj), G'.CliqueFree (r + 1) ∧ #G.edgeFinset < #G'.edgeFinset
have 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
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
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Extremal.Turan (goal)
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
⊢ ∃ (G' : SimpleGraph V) (inst_2 : DecidableRel G'.Adj), G'.CliqueFree (r + 1) ∧ #G.edgeFinset < #G'.edgeFinset
have 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
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
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Extremal.Turan (goal)
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
⊢ ∃ (G' : SimpleGraph V) (inst_2 : DecidableRel G'.Adj), G'.CliqueFree (r + 1) ∧ #G.edgeFinset < #G'.edgeFinset
have 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
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
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Extremal.Turan (goal)
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
⊢ ∃ (G' : SimpleGraph V) (inst_2 : DecidableRel G'.Adj), G'.CliqueFree (r + 1) ∧ #G.edgeFinset < #G'.edgeFinset
have 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
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
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Extremal.Turan (goal)
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
⊢ (h.setoid : V → V → Prop) s t ↔ Finpartition.part h.finpartition s = Finpartition.part h.finpartition t
have rw : t ∈ Finpartition.part (s := univ) (Finpartition.ofSetoid h.setoid) s ↔
  Finpartition.part h.finpartition s = Finpartition.part h.finpartition t
Tactic: rw [← Finpartition.mem_part_ofSetoid_iff_rel]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Extremal.Turan (goal)
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
⊢ t ∈ Finpartition.part (s := univ) (Finpartition.ofSetoid h.setoid) s ↔
    Finpartition.part h.finpartition s = Finpartition.part h.finpartition t
have change : t ∈ fp.part s ↔ fp.part s = fp.part t
Tactic: change t ∈ fp.part s ↔ fp.part s = fp.part t
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Extremal.Turan (goal)
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
⊢ t ∈ fp.part s ↔ fp.part s = fp.part t
have rw : fp.part 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]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Extremal.Turan (goal)
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
⊢ t ∈ fp.part s ↔ fp.part s = fp.part t
have rw₁ : fp.part s = fp.part t ↔ fp.part s = fp.part t
Tactic: rw [fp.mem_part_iff_part_eq_part (mem_univ t) (mem_univ s), eq_comm]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Extremal.Turan (goal)
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
⊢ Fintype.card V - Finset.card.{u_1} (α := V) {t : V | ¬G.Adj s t} =
    Fintype.card V - #(Finpartition.part h.finpartition s)
have e_a : {t : V | ¬G.Adj s t} = Finpartition.part h.finpartition s
Tactic: congr
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Extremal.Turan (goal)
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
⊢ {t : V | ¬G.Adj s t} = Finpartition.part h.finpartition s
have e_a : ∀ (a : V), Membership.mem (γ := Finset V) {t : V | ¬G.Adj s t} a ↔ a ∈ Finpartition.part h.finpartition s
Tactic: ext
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Extremal.Turan (goal)
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) {t : V | ¬G.Adj s t} a ↔ a ∈ Finpartition.part h.finpartition s
have e_a : Membership.mem (γ := Finset V) univ a ∧ ¬G.Adj s a ↔ a ∈ Finpartition.part h.finpartition s
Tactic: rw [mem_filter]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Extremal.Turan (goal)
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 ↔ a ∈ Finpartition.part h.finpartition s
have h₁ : Membership.mem (γ := Finset V) univ a ∧ ¬G.Adj s a ↔ (h.setoid : V → V → Prop) s a
Tactic: convert! Finpartition.mem_part_ofSetoid_iff_rel.symm
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Extremal.Turan (goal)
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
⊢ fp.IsEquipartition
have by_contra : ∀ (hn : ¬fp.IsEquipartition), False
Tactic: by_contra hn
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Extremal.Turan (hypothesis)
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
⊢ False
have hn₁ : ∃ a ∈ fp.parts, ∃ b ∈ fp.parts, #b + 1 < #a
Tactic: rw [Finpartition.not_isEquipartition] at hn
Cleared hypotheses: hn
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Extremal.Turan (goal)
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
⊢ False
have obtain : ∀ (large : Finset V) (hl : large ∈ fp.parts) (small : Finset V) (hs : small ∈ fp.parts) (ineq : #small + 1 < #large),
  False
Tactic: obtain ⟨large, hl, small, hs, ineq⟩ := hn
Cleared hypotheses: hn
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Extremal.Turan (goal)
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
⊢ False
have obtain : ∀ (w : V) (hw : w ∈ large), False
Tactic: obtain ⟨w, hw⟩ := fp.nonempty_of_mem_parts hl
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Extremal.Turan (goal)
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
⊢ False
have obtain : ∀ (v : V) (hv : v ∈ small), False
Tactic: obtain ⟨v, hv⟩ := fp.nonempty_of_mem_parts hs
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Extremal.Turan (goal)
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
⊢ False
have apply : ¬G.IsTuranMaximal r
Tactic: apply absurd h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Extremal.Turan (goal)
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
⊢ ¬(G.CliqueFree (r + 1) ∧
      ∀ ⦃G' : SimpleGraph V⦄ [inst_3 : DecidableRel G'.Adj], G'.CliqueFree (r + 1) → #G'.edgeFinset ≤ #G.edgeFinset)
have push : ∀ (_ : G.CliqueFree (r + 1)),
  ∃ (G' : SimpleGraph V) (inst_3 : DecidableRel G'.Adj), G'.CliqueFree (r + 1) ∧ #G.edgeFinset < #G'.edgeFinset
Tactic: push Not
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Extremal.Turan (goal)
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)
⊢ ∃ (G' : SimpleGraph V) (inst_3 : DecidableRel G'.Adj), G'.CliqueFree (r + 1) ∧ #G.edgeFinset < #G'.edgeFinset
have right : #G.edgeFinset < #(G.replaceVertex v w).edgeFinset
Tactic: use G.replaceVertex v w, inferInstance, cf.replaceVertex v w
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Extremal.Turan (hypothesis)
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)
⊢ #G.edgeFinset < #(G.replaceVertex v w).edgeFinset
have large_eq : fp.part w = large
Tactic: have large_eq := fp.part_eq_of_mem hl hw
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Extremal.Turan (hypothesis)
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
⊢ #G.edgeFinset < #(G.replaceVertex v w).edgeFinset
have small_eq : fp.part v = small
Tactic: have small_eq := fp.part_eq_of_mem hs hv
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Extremal.Turan (goal)
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
have by_contra : ∀ (hn : ¬G.Adj v w), False
Tactic: by_contra hn
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Extremal.Turan (hypothesis)
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
⊢ False
have hn₁ : small = large
Tactic: rw [h.not_adj_iff_part_eq, small_eq, large_eq] at hn
Cleared hypotheses: hn
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Extremal.Turan (goal)
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
⊢ False
have 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
Tactic: rw [hn] at ineq
Cleared hypotheses: ineq, w, hw, v, hv, cf, large_eq, small_eq, hn