-- 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))
map_rel_iff' map_rel_iff'₁ :
  ∀ (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},
    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
map_rel_iff'₂ :
  ∀ (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},
    (↑((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
map_rel_iff'₃ :
  ∀ (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)),
    (↑((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
map_rel_iff'₄ :
  ∀ (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)),
    (↑((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
map_rel_iff'₅ :
  ∀ (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)),
    (↑((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
map_rel_iff'₆ :
  ∀ (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))
    (c : r ≤ Fintype.card V),
    (↑((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
map_rel_iff'₇ map_rel_iff'₈ :
  ∀ (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))
    (c : 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 ↔
      (↑((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
⊢ Nonempty.{max 1 (u_1 + 1)} (G.Iso (W := Fin (Fintype.card V)) (turanGraph (Fintype.card V) r))

Tactic:
classical
  obtain ⟨zm, zp⟩ := h.isEquipartition.exists_partPreservingEquiv
  use (Equiv.subtypeUnivEquiv mem_univ).symm.trans zm
  intro a b
  simp_rw [turanGraph_adj, Equiv.trans_apply, Equiv.subtypeUnivEquiv_symm_apply]
  have := zp ⟨a, mem_univ a⟩ ⟨b, mem_univ b⟩
  rw [← h.not_adj_iff_part_eq] at this
  rw [← not_iff_not, not_ne_iff, this, card_parts]
  rcases le_or_gt r (card V) with c | c
  · rw [min_eq_right c]; rfl
  · have lc : ∀ x, zm ⟨x, _⟩ < card V := fun x ↦ (zm ⟨x, mem_univ x⟩).2
    rw [min_eq_left c.le, Nat.mod_eq_of_lt (lc a), Nat.mod_eq_of_lt (lc b),
      ← Nat.mod_eq_of_lt ((lc a).trans c), ← Nat.mod_eq_of_lt ((lc b).trans c)]; rfl

Premises used: not_iff_not, Equiv.trans_apply, Fintype.card, not_ne_iff, le_or_gt, SimpleGraph.turanGraph_adj, Equiv.subtypeUnivEquiv_symm_apply, SimpleGraph.IsTuranMaximal.card_parts