awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
⊢ #G.edgeFinset < #(G.replaceVertex v w).edgeFinset
have ha : G.Adj v w
Tactic: have ha : G.Adj v w := by
    by_contra hn; rw [h.not_adj_iff_part_eq, small_eq, large_eq] at hn
    rw [hn] at ineq; 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 : ℕ
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
ha : G.Adj v w
⊢ #G.edgeFinset < #(G.replaceVertex v w).edgeFinset
have right : #G.edgeFinset < #G.edgeFinset + (Fintype.card V - #small) - (Fintype.card V - #large) - 1
Tactic: rw [G.card_edgeFinset_replaceVertex_of_adj ha,
    degree_eq_card_sub_part_card h, small_eq, degree_eq_card_sub_part_card h, large_eq]
-- 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
ha : G.Adj v w
⊢ #G.edgeFinset < #G.edgeFinset + (Fintype.card V - #small) - (Fintype.card V - #large) - 1
have this : #large ≤ Fintype.card V
Tactic: have : #large ≤ card V := by simpa using card_le_card large.subset_univ
-- 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
⊢ #(Finpartition.parts h.finpartition) ≤ r
have by_contra! : ∀ (l : r < #(Finpartition.parts h.finpartition)), False
Tactic: by_contra! l
-- 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
l : r < #(Finpartition.parts h.finpartition)
⊢ False
have obtain : ∀ (z : Finset V)
  (hz :
    Set.BijOn (Finpartition.part h.finpartition) (↑z : Set V) (↑(Finpartition.parts h.finpartition) : Set (Finset V))),
  False
Tactic: obtain ⟨z, -, hz⟩ := h.finpartition.exists_subset_part_bijOn
-- 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
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
have refine : ∀ (v : V) (hv : v ∈ (↑z : Set V)) (w : V) (hw : w ∈ (↑z : Set V)) (hn : v ≠ w), G.Adj v w
Tactic: refine IsNClique.not_cliqueFree ⟨fun v hv w hw hn ↦ ?_, rfl⟩
-- 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
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))
v : V
hv : v ∈ (↑z : Set V)
w : V
hw : w ∈ (↑z : Set V)
hn : v ≠ w
⊢ G.Adj v w
have contrapose : ∀ (hn : ¬G.Adj v w), v = w
Tactic: contrapose hn
Cleared hypotheses: 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
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))
⊢ False
have ncf : ¬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])
-- 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
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
⊢ False
have ncf₁ : ¬G.CliqueFree #(Finpartition.parts h.finpartition)
Tactic: rw [Finset.card_eq_of_equiv hz.equiv] at ncf
Cleared hypotheses: ncf
-- 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.parts = min (Fintype.card V) r
have apply : min (Finset.card.{u_1} (α := V) univ) r ≤ #fp.parts
Tactic: apply le_antisymm (le_min fp.card_parts_le_card h.card_parts_le)
-- 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
⊢ min (Finset.card.{u_1} (α := V) univ) r ≤ #fp.parts
have by_contra! : ∀ (l : #fp.parts < min (Finset.card.{u_1} (α := V) univ) r), False
Tactic: by_contra! l
-- 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
l : #fp.parts < min (Finset.card.{u_1} (α := V) univ) r
⊢ False
have l₁ : #fp.parts < Finset.card.{u_1} (α := V) univ ∧ #fp.parts < r
Tactic: rw [lt_min_iff] at l
Cleared hypotheses: l
-- 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
l : #fp.parts < Finset.card.{u_1} (α := V) univ ∧ #fp.parts < r
⊢ False
have obtain : ∀ (x y : V) (hn : x ≠ y) (he : fp.part x = fp.part y), 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)
-- 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
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
⊢ 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
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 + 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
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
have 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
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]
-- 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
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 : V⦄, x ∈ (↑z : Set V) → ∀ ⦃y : V⦄, y ∈ (↑z : Set V) → x ≠ y → G.Adj x y
have push : ∃ x ∈ (↑z : Set V), ∃ y ∈ (↑z : Set V), x ≠ y ∧ ¬G.Adj x y
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
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 ∧ ¬G.Adj x y
have simp_rw : ∃ x ∈ (↑z : Set V), ∃ y ∈ (↑z : Set V), x ≠ y ∧ Finpartition.part h.finpartition x = Finpartition.part h.finpartition y
Tactic: simp_rw [h.not_adj_iff_part_eq]
-- 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
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' : SimpleGraph V) (inst_3 : DecidableRel G'.Adj), G'.CliqueFree (r + 1) ∧ #G.edgeFinset < #G'.edgeFinset
have cf : 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)
-- 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
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' : SimpleGraph V) (inst_3 : DecidableRel G'.Adj), G'.CliqueFree (r + 1) ∧ #G.edgeFinset < #G'.edgeFinset
have right : #G.edgeFinset < #(G ⊔ edge x y).edgeFinset
Tactic: use G ⊔ edge x y, inferInstance, cf.sup_edge x y
-- 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
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 ⊔ edge x y).edgeFinset
have h₁ : #(G ⊔ edge x y).edgeFinset = #G.edgeFinset + 1
Tactic: convert! Nat.lt_add_one #G.edgeFinset
-- 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
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
have h₁ : ¬G.Adj x y
Tactic: convert! G.card_edgeFinset_sup_edge _ 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
⊢ Nonempty.{max 1 (u_1 + 1)} (G.Iso (W := Fin (Fintype.card V)) (turanGraph (Fintype.card V) r))
have 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))
Tactic: obtain ⟨zm, zp⟩ := h.isEquipartition.exists_partPreservingEquiv
-- 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)
⊢ Nonempty.{max 1 (u_1 + 1)} (G.Iso (W := Fin (Fintype.card V)) (turanGraph (Fintype.card V) r))
have 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) sorry)) zm :
          (a : V) → Fin (Fintype.card V))
        a)
      ((Equiv.trans (Equiv.symm (Equiv.subtypeUnivEquiv (p := Membership.mem (γ := Finset V) univ) sorry)) zm :
          (a : V) → Fin (Fintype.card V))
        b) ↔
    G.Adj a b
Tactic: use (Equiv.subtypeUnivEquiv mem_univ).symm.trans zm
-- 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
⊢ 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
have map_rel_iff' : (↑((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: simp_rw [turanGraph_adj, Equiv.trans_apply, Equiv.subtypeUnivEquiv_symm_apply]
-- 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
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
have 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)
Tactic: have := zp ⟨a, mem_univ a⟩ ⟨b, mem_univ b⟩
-- 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
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
have this₁ : ¬G.Adj (↑(Subtype.mk (p := fun (x : V) ↦ Membership.mem (γ := Finset V) univ x) a sorry) : V)
      (↑(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)
Tactic: rw [← h.not_adj_iff_part_eq] at this
Cleared hypotheses: this
-- 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)
⊢ (↑((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
have map_rel_iff' : (↑((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: rw [← not_iff_not, not_ne_iff, this, card_parts]