-- 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
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' :
  ∀ (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
⊢ (↑((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
have map_rel_iff'₁ : ∀ (c : Fintype.card V < r),
  (↑((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 ↔
    (↑((zm : (a : ↥univ) → Fin #univ) (Subtype.mk (p := fun (x : V) ↦ Membership.mem (γ := Finset V) univ x) a sorry)) :
          ℕ) %
        min (Fintype.card V) r =
      (↑((zm : (a : ↥univ) → Fin #univ) (Subtype.mk (p := fun (x : V) ↦ Membership.mem (γ := Finset V) univ x) b sorry)) :
          ℕ) %
        min (Fintype.card V) r
Tactic: rcases le_or_gt r (card V) with c | c