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 : ℕ
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:
have ncf : ¬G.CliqueFree #z := by
    refine IsNClique.not_cliqueFree ⟨fun v hv w hw hn ↦ ?_, rfl⟩
    contrapose hn
    exact hz.injOn hv hw (by rwa [← h.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))
ncf : ¬G.CliqueFree #z
⊢ ¬G.CliqueFree #(Finpartition.parts h.finpartition)

Tactic:
rw [Finset.card_eq_of_equiv hz.equiv] at ncf

Premises used: Finset.card_eq_of_equiv, Set.BijOn.equiv
-- 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))
ncf : ¬G.CliqueFree #(Finpartition.parts h.finpartition)
⊢ False

Tactic:
absurd (h.1.mono (Nat.succ_le_of_lt l)) ncf

Premises used: Nat.succ_le_of_lt, absurd, And.left, SimpleGraph.CliqueFree.mono
-- 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))
ncf : ¬G.CliqueFree #(Finpartition.parts h.finpartition)
⊢ False

Tactic:
exact absurd (h.1.mono (Nat.succ_le_of_lt l)) ncf

Premises used: Nat.succ_le_of_lt, absurd, And.left, SimpleGraph.CliqueFree.mono
-- 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.parts = min (Fintype.card V) r
⊢ #(Finpartition.parts h.finpartition) = min (Fintype.card V) r

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
apply : min (Finset.card.{u_1} (α := V) univ) r ≤ #fp.parts
⊢ #fp.parts = min (Fintype.card V) r

Tactic:
apply le_antisymm (le_min fp.card_parts_le_card h.card_parts_le)

Premises used: Finpartition.card_parts_le_card, SimpleGraph.IsTuranMaximal.card_parts_le, le_min, le_antisymm
-- 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! : ∀ (l : #fp.parts < min (Finset.card.{u_1} (α := V) univ) r), False
⊢ min (Finset.card.{u_1} (α := V) univ) r ≤ #fp.parts

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
fp : Finpartition (α := Finset V) univ := h.finpartition
l : #fp.parts < min (Finset.card.{u_1} (α := V) univ) r
⊢ #fp.parts < Finset.card.{u_1} (α := V) univ ∧ #fp.parts < r

Tactic:
rw [lt_min_iff] at l

Premises used: lt_min_iff
-- 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
l : #fp.parts < Finset.card.{u_1} (α := V) univ ∧ #fp.parts < r
obtain : ∀ (x y : V) (hn : x ≠ y) (he : fp.part x = fp.part y), False
⊢ False

Tactic:
obtain ⟨x, -, y, -, hn, he⟩ :=
    exists_ne_map_eq_of_card_lt_of_maps_to l.1 fun a _ ↦ fp.part_mem.2 (mem_univ a)

Premises used: Iff.mpr, Finset.mem_univ, Finset.exists_ne_map_eq_of_card_lt_of_maps_to, Finpartition.part_mem, And.left
-- 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
l : #fp.parts < Finset.card.{u_1} (α := V) univ ∧ #fp.parts < r
x y : V
hn : x ≠ y
he : fp.part x = fp.part y
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
l : #fp.parts < Finset.card.{u_1} (α := V) univ ∧ #fp.parts < r
x y : V
hn : x ≠ y
he : fp.part x = fp.part y
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
l : #fp.parts < Finset.card.{u_1} (α := V) univ ∧ #fp.parts < r
x y : V
hn : x ≠ y
he : fp.part x = fp.part y
simp_rw :
  ∀ ⦃x : Finset V⦄, #x = r → ¬∀ ⦃x_1 : V⦄, x_1 ∈ (↑x : Set V) → ∀ ⦃y : V⦄, y ∈ (↑x : Set V) → x_1 ≠ y → G.Adj x_1 y
⊢ G.CliqueFree r

Tactic:
simp_rw [← cliqueFinset_eq_empty_iff, cliqueFinset, filter_eq_empty_iff, mem_univ,
      forall_true_left, isNClique_iff, and_comm, not_and, isClique_iff, Set.Pairwise]

Premises used: SimpleGraph.cliqueFinset_eq_empty_iff, Finset.mem_univ, forall_true_left, and_comm, Set.Pairwise, Finset.filter_eq_empty_iff, SimpleGraph.isClique_iff, SimpleGraph.isNClique_iff, not_and, SimpleGraph.cliqueFinset
-- 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
l : #fp.parts < Finset.card.{u_1} (α := V) univ ∧ #fp.parts < r
x y : V
hn : x ≠ y
he : fp.part x = fp.part y
z : Finset V
zc : #z = r
push : ∃ x ∈ (↑z : Set V), ∃ y ∈ (↑z : Set V), x ≠ y ∧ ¬G.Adj x y
⊢ ¬∀ ⦃x : V⦄, x ∈ (↑z : Set V) → ∀ ⦃y : V⦄, y ∈ (↑z : Set V) → x ≠ y → G.Adj x y

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
l : #fp.parts < Finset.card.{u_1} (α := V) univ ∧ #fp.parts < r
x y : V
hn : x ≠ y
he : fp.part x = fp.part y
z : Finset V
zc : #z = r
simp_rw :
  ∃ x ∈ (↑z : Set V),
    ∃ y ∈ (↑z : Set V), x ≠ y ∧ Finpartition.part h.finpartition x = Finpartition.part h.finpartition y
⊢ ∃ x ∈ (↑z : Set V), ∃ y ∈ (↑z : Set V), x ≠ y ∧ ¬G.Adj x y

Tactic:
simp_rw [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
fp : Finpartition (α := Finset V) univ := h.finpartition
l : #fp.parts < Finset.card.{u_1} (α := V) 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 : Set V),
    ∃ y ∈ (↑z : Set V), x ≠ y ∧ Finpartition.part h.finpartition x = Finpartition.part h.finpartition y

Tactic:
exists_ne_map_eq_of_card_lt_of_maps_to (zc.symm ▸ l.2) fun a _ ↦
      fp.part_mem.2 (mem_univ a)

Premises used: Iff.mpr, Finset.mem_univ, Finset.exists_ne_map_eq_of_card_lt_of_maps_to, Finpartition.part_mem
-- 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
l : #fp.parts < Finset.card.{u_1} (α := V) 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 : Set V),
    ∃ y ∈ (↑z : Set V), x ≠ y ∧ Finpartition.part h.finpartition x = Finpartition.part h.finpartition y

Tactic:
exact exists_ne_map_eq_of_card_lt_of_maps_to (zc.symm ▸ l.2) fun a _ ↦
      fp.part_mem.2 (mem_univ a)

Premises used: Iff.mpr, Finset.mem_univ, Finset.exists_ne_map_eq_of_card_lt_of_maps_to, Finpartition.part_mem
-- 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
l : #fp.parts < Finset.card.{u_1} (α := V) univ ∧ #fp.parts < r
x y : V
hn : x ≠ y
he : fp.part x = fp.part y
⊢ G.CliqueFree r

Tactic:
have cf : G.CliqueFree r := by
    simp_rw [← cliqueFinset_eq_empty_iff, cliqueFinset, filter_eq_empty_iff, mem_univ,
      forall_true_left, isNClique_iff, and_comm, not_and, isClique_iff, Set.Pairwise]
    intro z zc; push Not; simp_rw [h.not_adj_iff_part_eq]
    exact exists_ne_map_eq_of_card_lt_of_maps_to (zc.symm ▸ l.2) fun a _ ↦
      fp.part_mem.2 (mem_univ a)
-- 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
l : #fp.parts < Finset.card.{u_1} (α := V) univ ∧ #fp.parts < r
x y : V
hn : x ≠ y
he : fp.part x = fp.part y
cf : G.CliqueFree r
right : #G.edgeFinset < #(G ⊔ edge x y).edgeFinset
⊢ ∃ (G' : SimpleGraph V) (inst_3 : DecidableRel G'.Adj), G'.CliqueFree (r + 1) ∧ #G.edgeFinset < #G'.edgeFinset

Tactic:
use G ⊔ edge x y, inferInstance, cf.sup_edge x y

Premises used: SimpleGraph.edge, SimpleGraph.CliqueFree.sup_edge
-- 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
l : #fp.parts < Finset.card.{u_1} (α := V) univ ∧ #fp.parts < r
x y : V
hn : x ≠ y
he : fp.part x = fp.part y
cf : G.CliqueFree r
⊢ #G.edgeFinset < #G.edgeFinset + 1

Tactic:
Nat.lt_add_one #G.edgeFinset

Premises used: Nat.lt_add_one, SimpleGraph.edgeFinset, Finset.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
l : #fp.parts < Finset.card.{u_1} (α := V) univ ∧ #fp.parts < r
x y : V
hn : x ≠ y
he : fp.part x = fp.part y
cf : G.CliqueFree r
h₁ : #(G ⊔ edge x y).edgeFinset = #G.edgeFinset + 1
⊢ #G.edgeFinset < #(G ⊔ edge x y).edgeFinset

Tactic:
convert! Nat.lt_add_one #G.edgeFinset

Premises used: Nat.lt_add_one, SimpleGraph.edgeFinset, Finset.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
l : #fp.parts < Finset.card.{u_1} (α := V) univ ∧ #fp.parts < r
x y : V
hn : x ≠ y
he : fp.part x = fp.part y
cf : G.CliqueFree r
⊢ #(G ⊔ edge x y).edgeFinset = #G.edgeFinset + 1

Tactic:
G.card_edgeFinset_sup_edge _ hn

Premises used: SimpleGraph.card_edgeFinset_sup_edge
-- 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
l : #fp.parts < Finset.card.{u_1} (α := V) univ ∧ #fp.parts < r
x y : V
hn : x ≠ y
he : fp.part x = fp.part y
cf : G.CliqueFree r
h₁ : ¬G.Adj x y
⊢ #(G ⊔ edge x y).edgeFinset = #G.edgeFinset + 1

Tactic:
convert! G.card_edgeFinset_sup_edge _ hn

Premises used: SimpleGraph.card_edgeFinset_sup_edge
-- 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
l : #fp.parts < Finset.card.{u_1} (α := V) univ ∧ #fp.parts < r
x y : V
hn : x ≠ y
he : fp.part x = fp.part y
cf : G.CliqueFree r
h₁ h₂ h₃ h₄ : Finpartition.part h.finpartition x = Finpartition.part h.finpartition y
⊢ ¬G.Adj x y

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
obtain :
  ∀ (zm : ↥univ ≃ Fin (Finset.card.{u_1} (α := V) univ))
    (zp :
      ∀ (a b : ↥univ),
        Finpartition.part h.finpartition (↑a : V) = Finpartition.part h.finpartition (↑b : V) ↔
          (↑((zm : (a : ↥univ) → Fin #univ) a) : ℕ) % #(Finpartition.parts h.finpartition) =
            (↑((zm : (a : ↥univ) → Fin #univ) b) : ℕ) % #(Finpartition.parts h.finpartition)),
    Nonempty.{max 1 (u_1 + 1)} (G.Iso (W := Fin (Fintype.card V)) (turanGraph (Fintype.card V) r))
⊢ Nonempty.{max 1 (u_1 + 1)} (G.Iso (W := Fin (Fintype.card V)) (turanGraph (Fintype.card V) r))

Tactic:
obtain ⟨zm, zp⟩ := h.isEquipartition.exists_partPreservingEquiv

Premises used: SimpleGraph.IsTuranMaximal.isEquipartition, Finpartition.IsEquipartition.exists_partPreservingEquiv
-- 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
zm : ↥univ ≃ Fin (Finset.card.{u_1} (α := V) univ)
zp :
  ∀ (a b : ↥univ),
    Finpartition.part h.finpartition (↑a : V) = Finpartition.part h.finpartition (↑b : V) ↔
      (↑((zm : (a : ↥univ) → Fin #univ) a) : ℕ) % #(Finpartition.parts h.finpartition) =
        (↑((zm : (a : ↥univ) → Fin #univ) b) : ℕ) % #(Finpartition.parts h.finpartition)
map_rel_iff' :
  ∀ {a b : V},
    Adj (V := Fin (Fintype.card V)) (turanGraph (Fintype.card V) r)
        ((Equiv.trans (Equiv.symm (Equiv.subtypeUnivEquiv (p := Membership.mem (γ := Finset V) univ) ⋯)) zm :
            (a : V) → Fin (Fintype.card V))
          a)
        ((Equiv.trans (Equiv.symm (Equiv.subtypeUnivEquiv (p := Membership.mem (γ := Finset V) univ) ⋯)) zm :
            (a : V) → Fin (Fintype.card V))
          b) ↔
      G.Adj a b
⊢ Nonempty.{max 1 (u_1 + 1)} (G.Iso (W := Fin (Fintype.card V)) (turanGraph (Fintype.card V) r))

Tactic:
use (Equiv.subtypeUnivEquiv mem_univ).symm.trans zm

Premises used: Finset.mem_univ, Equiv.trans, Equiv.subtypeUnivEquiv, Equiv.symm
-- 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
zm : ↥univ ≃ Fin (Finset.card.{u_1} (α := V) univ)
zp :
  ∀ (a b : ↥univ),
    Finpartition.part h.finpartition (↑a : V) = Finpartition.part h.finpartition (↑b : V) ↔
      (↑((zm : (a : ↥univ) → Fin #univ) a) : ℕ) % #(Finpartition.parts h.finpartition) =
        (↑((zm : (a : ↥univ) → Fin #univ) b) : ℕ) % #(Finpartition.parts h.finpartition)
a b : V
map_rel_iff' :
  (↑((zm : (a : Subtype (Membership.mem univ)) → Fin (Fintype.card V))
              (Subtype.mk (p := Membership.mem (γ := Finset V) univ) a ⋯)) :
          ℕ) %
        r ≠
      (↑((zm : (a : Subtype (Membership.mem univ)) → Fin (Fintype.card V))
              (Subtype.mk (p := Membership.mem (γ := Finset V) univ) b ⋯)) :
          ℕ) %
        r ↔
    G.Adj a b
⊢ Adj (V := Fin (Fintype.card V)) (turanGraph (Fintype.card V) r)
      ((Equiv.trans (Equiv.symm (Equiv.subtypeUnivEquiv (p := Membership.mem (γ := Finset V) univ) ⋯)) zm :
          (a : V) → Fin (Fintype.card V))
        a)
      ((Equiv.trans (Equiv.symm (Equiv.subtypeUnivEquiv (p := Membership.mem (γ := Finset V) univ) ⋯)) zm :
          (a : V) → Fin (Fintype.card V))
        b) ↔
    G.Adj a b

Tactic:
simp_rw [turanGraph_adj, Equiv.trans_apply, Equiv.subtypeUnivEquiv_symm_apply]

Premises used: Equiv.trans_apply, SimpleGraph.turanGraph_adj, Equiv.subtypeUnivEquiv_symm_apply
-- 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
zm : ↥univ ≃ Fin (Finset.card.{u_1} (α := V) univ)
zp :
  ∀ (a b : ↥univ),
    Finpartition.part h.finpartition (↑a : V) = Finpartition.part h.finpartition (↑b : V) ↔
      (↑((zm : (a : ↥univ) → Fin #univ) a) : ℕ) % #(Finpartition.parts h.finpartition) =
        (↑((zm : (a : ↥univ) → Fin #univ) b) : ℕ) % #(Finpartition.parts h.finpartition)
a b : V
⊢ Finpartition.part h.finpartition (↑(Subtype.mk (p := fun (x : V) ↦ Membership.mem (γ := Finset V) univ x) a ⋯) : V) =
      Finpartition.part h.finpartition
        (↑(Subtype.mk (p := fun (x : V) ↦ Membership.mem (γ := Finset V) univ x) b ⋯) : V) ↔
    (↑((zm : (a : ↥univ) → Fin #univ) (Subtype.mk (p := fun (x : V) ↦ Membership.mem (γ := Finset V) univ x) a ⋯)) :
          ℕ) %
        #(Finpartition.parts h.finpartition) =
      (↑((zm : (a : ↥univ) → Fin #univ) (Subtype.mk (p := fun (x : V) ↦ Membership.mem (γ := Finset V) univ x) b ⋯)) :
          ℕ) %
        #(Finpartition.parts h.finpartition)

Tactic:
have := zp ⟨a, mem_univ a⟩ ⟨b, mem_univ b⟩
-- 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
zm : ↥univ ≃ Fin (Finset.card.{u_1} (α := V) univ)
zp :
  ∀ (a b : ↥univ),
    Finpartition.part h.finpartition (↑a : V) = Finpartition.part h.finpartition (↑b : V) ↔
      (↑((zm : (a : ↥univ) → Fin #univ) a) : ℕ) % #(Finpartition.parts h.finpartition) =
        (↑((zm : (a : ↥univ) → Fin #univ) b) : ℕ) % #(Finpartition.parts h.finpartition)
a b : V
this :
  Finpartition.part h.finpartition (↑(Subtype.mk (p := fun (x : V) ↦ Membership.mem (γ := Finset V) univ x) a ⋯) : V) =
      Finpartition.part h.finpartition
        (↑(Subtype.mk (p := fun (x : V) ↦ Membership.mem (γ := Finset V) univ x) b ⋯) : V) ↔
    (↑((zm : (a : ↥univ) → Fin #univ) (Subtype.mk (p := fun (x : V) ↦ Membership.mem (γ := Finset V) univ x) a ⋯)) :
          ℕ) %
        #(Finpartition.parts h.finpartition) =
      (↑((zm : (a : ↥univ) → Fin #univ) (Subtype.mk (p := fun (x : V) ↦ Membership.mem (γ := Finset V) univ x) b ⋯)) :
          ℕ) %
        #(Finpartition.parts h.finpartition)
⊢ ¬G.Adj (↑(Subtype.mk (p := fun (x : V) ↦ Membership.mem (γ := Finset V) univ x) a ⋯) : V)
        (↑(Subtype.mk (p := fun (x : V) ↦ Membership.mem (γ := Finset V) univ x) b ⋯) : V) ↔
    (↑((zm : (a : ↥univ) → Fin #univ) (Subtype.mk (p := fun (x : V) ↦ Membership.mem (γ := Finset V) univ x) a ⋯)) :
          ℕ) %
        #(Finpartition.parts h.finpartition) =
      (↑((zm : (a : ↥univ) → Fin #univ) (Subtype.mk (p := fun (x : V) ↦ Membership.mem (γ := Finset V) univ x) b ⋯)) :
          ℕ) %
        #(Finpartition.parts h.finpartition)

Tactic:
rw [← h.not_adj_iff_part_eq] at this

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
zm : ↥univ ≃ Fin (Finset.card.{u_1} (α := V) univ)
zp :
  ∀ (a b : ↥univ),
    Finpartition.part h.finpartition (↑a : V) = Finpartition.part h.finpartition (↑b : V) ↔
      (↑((zm : (a : ↥univ) → Fin #univ) a) : ℕ) % #(Finpartition.parts h.finpartition) =
        (↑((zm : (a : ↥univ) → Fin #univ) b) : ℕ) % #(Finpartition.parts h.finpartition)
a b : V
this :
  ¬G.Adj (↑(Subtype.mk (p := fun (x : V) ↦ Membership.mem (γ := Finset V) univ x) a ⋯) : V)
        (↑(Subtype.mk (p := fun (x : V) ↦ Membership.mem (γ := Finset V) univ x) b ⋯) : V) ↔
    (↑((zm : (a : ↥univ) → Fin #univ) (Subtype.mk (p := fun (x : V) ↦ Membership.mem (γ := Finset V) univ x) a ⋯)) :
          ℕ) %
        #(Finpartition.parts h.finpartition) =
      (↑((zm : (a : ↥univ) → Fin #univ) (Subtype.mk (p := fun (x : V) ↦ Membership.mem (γ := Finset V) univ x) b ⋯)) :
          ℕ) %
        #(Finpartition.parts h.finpartition)
map_rel_iff' :
  (↑((zm : (a : Subtype (Membership.mem univ)) → Fin (Fintype.card V))
              (Subtype.mk (p := Membership.mem (γ := Finset V) univ) a ⋯)) :
          ℕ) %
        r =
      (↑((zm : (a : Subtype (Membership.mem univ)) → Fin (Fintype.card V))
              (Subtype.mk (p := Membership.mem (γ := Finset V) univ) b ⋯)) :
          ℕ) %
        r ↔
    (↑((zm : (a : ↥univ) → Fin #univ) (Subtype.mk (p := fun (x : V) ↦ Membership.mem (γ := Finset V) univ x) a ⋯)) :
          ℕ) %
        min (Fintype.card V) r =
      (↑((zm : (a : ↥univ) → Fin #univ) (Subtype.mk (p := fun (x : V) ↦ Membership.mem (γ := Finset V) univ x) b ⋯)) :
          ℕ) %
        min (Fintype.card V) r
⊢ (↑((zm : (a : Subtype (Membership.mem univ)) → Fin (Fintype.card V))
              (Subtype.mk (p := Membership.mem (γ := Finset V) univ) a ⋯)) :
          ℕ) %
        r ≠
      (↑((zm : (a : Subtype (Membership.mem univ)) → Fin (Fintype.card V))
              (Subtype.mk (p := Membership.mem (γ := Finset V) univ) b ⋯)) :
          ℕ) %
        r ↔
    G.Adj a b

Tactic:
rw [← not_iff_not, not_ne_iff, this, card_parts]

Premises used: not_iff_not, not_ne_iff, SimpleGraph.IsTuranMaximal.card_parts