-- 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
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
⊢ Nonempty.{max 1 (u_1 + 1)} (G.Iso (W := Fin (Fintype.card V)) (turanGraph (Fintype.card V) r))
have 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 sorry) : V) =
        Finpartition.part h.finpartition
          (↑(Subtype.mk (p := fun (x : V) ↦ Membership.mem (γ := Finset V) univ x) b sorry) : V) ↔
      (↑((zm : (a : ↥univ) → Fin #univ) (Subtype.mk (p := fun (x : V) ↦ Membership.mem (γ := Finset V) univ x) a sorry)) :
            ℕ) %
          #(Finpartition.parts h.finpartition) =
        (↑((zm : (a : ↥univ) → Fin #univ) (Subtype.mk (p := fun (x : V) ↦ Membership.mem (γ := Finset V) univ x) b sorry)) :
            ℕ) %
          #(Finpartition.parts h.finpartition)),
  (↑((zm : (a : Subtype (Membership.mem univ)) → Fin (Fintype.card V))
              (Subtype.mk (p := Membership.mem (γ := Finset V) univ) a sorry)) :
          ℕ) %
        r ≠
      (↑((zm : (a : Subtype (Membership.mem univ)) → Fin (Fintype.card V))
              (Subtype.mk (p := Membership.mem (γ := Finset V) univ) b sorry)) :
          ℕ) %
        r ↔
    G.Adj a b
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