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
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
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 ⋯)) :
          ℕ) %
        r =
      (↑((zm : (a : ↥univ) → Fin #univ) (Subtype.mk (p := fun (x : V) ↦ Membership.mem (γ := Finset V) univ x) b ⋯)) :
          ℕ) %
        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

Tactic:
rw [min_eq_right c]

Premises used: min_eq_right
-- 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)
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 ⋯)) :
          ℕ) %
        r =
      (↑((zm : (a : ↥univ) → Fin #univ) (Subtype.mk (p := fun (x : V) ↦ Membership.mem (γ := Finset V) univ x) b ⋯)) :
          ℕ) %
        r

Tactic:
rfl
-- 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)
c : Fintype.card V < r
⊢ ∀ (x : V),
    (↑((zm : (a : ↥univ) → Fin #univ) (Subtype.mk (p := fun (x : V) ↦ Membership.mem (γ := Finset V) univ x) x ⋯)) :
        ℕ) <
      Fintype.card V

Tactic:
have lc : ∀ x, zm ⟨x, _⟩ < card V := fun x ↦ (zm ⟨x, mem_univ x⟩).2
-- 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)
c : Fintype.card V < r
lc :
  ∀ (x : V),
    (↑((zm : (a : ↥univ) → Fin #univ) (Subtype.mk (p := fun (x : V) ↦ Membership.mem (γ := Finset V) univ x) x ⋯)) :
        ℕ) <
      Fintype.card 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 ↔
    (↑((zm : (a : ↥univ) → Fin #univ) (Subtype.mk (p := fun (x : V) ↦ Membership.mem (γ := Finset V) univ x) a ⋯)) :
          ℕ) %
        r =
      (↑((zm : (a : ↥univ) → Fin #univ) (Subtype.mk (p := fun (x : V) ↦ Membership.mem (γ := Finset V) univ x) b ⋯)) :
          ℕ) %
        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

Tactic:
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)]

Premises used: LT.lt.le, Nat.mod_eq_of_lt, min_eq_left, LT.lt.trans
-- 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)
c : Fintype.card V < r
lc :
  ∀ (x : V),
    (↑((zm : (a : ↥univ) → Fin #univ) (Subtype.mk (p := fun (x : V) ↦ Membership.mem (γ := Finset V) univ x) x ⋯)) :
        ℕ) <
      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 ⋯)) :
          ℕ) %
        r =
      (↑((zm : (a : ↥univ) → Fin #univ) (Subtype.mk (p := fun (x : V) ↦ Membership.mem (γ := Finset V) univ x) b ⋯)) :
          ℕ) %
        r

Tactic:
rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan
Goal:
V : Type u_1
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
n r : ℕ
f : G ≃g turanGraph n r
hr : 0 < r
obtain : ∀ (J : SimpleGraph V) (w : DecidableRel J.Adj) (j : J.IsTuranMaximal r), G.IsTuranMaximal r
⊢ G.IsTuranMaximal r

Tactic:
obtain ⟨J, _, j⟩ := exists_isTuranMaximal (V := V) hr

Premises used: SimpleGraph.exists_isTuranMaximal
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan
Goal:
V : Type u_1
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
n r : ℕ
f : G ≃g turanGraph n r
hr : 0 < r
J : SimpleGraph V
w : DecidableRel J.Adj
j : J.IsTuranMaximal r
obtain : ∀ (g : J.Iso (W := Fin (Fintype.card V)) (turanGraph (Fintype.card V) r)), G.IsTuranMaximal r
⊢ G.IsTuranMaximal r

Tactic:
obtain ⟨g⟩ := j.nonempty_iso_turanGraph

Premises used: SimpleGraph.IsTuranMaximal.nonempty_iso_turanGraph
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan
Goal:
V : Type u_1
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
n r : ℕ
f : G ≃g turanGraph n r
hr : 0 < r
J : SimpleGraph V
w : DecidableRel J.Adj
j : J.IsTuranMaximal r
g : J.Iso (W := Fin (Fintype.card V)) (turanGraph (Fintype.card V) r)
rw : ∀ (g : J ≃g turanGraph n r), G.IsTuranMaximal r
⊢ G.IsTuranMaximal r

Tactic:
rw [f.card_eq, Fintype.card_fin] at g

Premises used: Fintype.card_fin, SimpleGraph.Iso.card_eq
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan
Goal:
V : Type u_1
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
n r : ℕ
f : G ≃g turanGraph n r
hr : 0 < r
J : SimpleGraph V
w : DecidableRel J.Adj
j : J.IsTuranMaximal r
g : J ≃g turanGraph n r
left : (fun (x : SimpleGraph V) ↦ x.CliqueFree (r + 1)) G
right :
  ∀ ⦃G' : SimpleGraph V⦄ [inst_2 : DecidableRel G'.Adj],
    (fun (x : SimpleGraph V) ↦ x.CliqueFree (r + 1)) G' → #G'.edgeFinset ≤ #G.edgeFinset
⊢ G.IsTuranMaximal r

Tactic:
use (turanGraph_cliqueFree (n := n) hr).comap f.isContained,
    fun H _ cf ↦ (f.symm.comp g).card_edgeFinset_eq ▸ j.2 cf

Premises used: SimpleGraph.turanGraph_cliqueFree, SimpleGraph.Iso.isContained, SimpleGraph.CliqueFree.comap
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan
Goal:
V : Type u_1
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
r : ℕ
W : Type u_2
inst_2 : Fintype W
H : SimpleGraph W
inst_3 : DecidableRel H.Adj
h : G.IsTuranMaximal r
f : G ≃g H
hr : 0 < r
⊢ H.IsTuranMaximal r

Tactic:
isTuranMaximal_of_iso (h.nonempty_iso_turanGraph.some.comp f.symm) hr

Premises used: SimpleGraph.IsTuranMaximal.nonempty_iso_turanGraph, Nonempty.some, SimpleGraph.Iso.comp, SimpleGraph.Iso.symm, SimpleGraph.isTuranMaximal_of_iso
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan
Goal:
n r : ℕ
hr : 0 < r
⊢ (turanGraph n r).IsTuranMaximal r

Tactic:
isTuranMaximal_of_iso Iso.refl hr

Premises used: SimpleGraph.Iso.refl, SimpleGraph.isTuranMaximal_of_iso
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan
Goal:
V : Type u_1
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
r : ℕ
hr : 0 < r
⊢ G.IsTuranMaximal r ↔ Nonempty.{max 1 (u_1 + 1)} (G.Iso (W := Fin (Fintype.card V)) (turanGraph (Fintype.card V) r))

Tactic:
⟨fun h ↦ h.nonempty_iso_turanGraph, fun h ↦ isTuranMaximal_of_iso h.some hr⟩

Premises used: SimpleGraph.IsTuranMaximal.nonempty_iso_turanGraph, Nonempty.some, Iff.intro, SimpleGraph.isTuranMaximal_of_iso
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan
Goal:
V : Type u_1
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
α : Type u_2
inst_2 : Fintype α
inst_3 : Nontrivial α
simp_rw :
  G.IsExtremal (Free.{u_2, u_1} (α := α) ⊤) ↔
    G.IsExtremal fun (x : SimpleGraph V) ↦ x.CliqueFree (Fintype.card α - 1 + 1)
simp_rw₁ :
  (Free.{u_2, u_1} (α := α) ⊤ G ∧
      ∀ ⦃G' : SimpleGraph V⦄ [inst_4 : DecidableRel G'.Adj],
        Free.{u_2, u_1} (α := α) ⊤ G' → #G'.edgeFinset ≤ #G.edgeFinset) ↔
    G.CliqueFree (Fintype.card α - 1 + 1) ∧
      ∀ ⦃G' : SimpleGraph V⦄ [inst_4 : DecidableRel G'.Adj],
        G'.CliqueFree (Fintype.card α - 1 + 1) → #G'.edgeFinset ≤ #G.edgeFinset
simp_rw₂ :
  (Free.{u_2, u_1} (α := α) ⊤ G ∧
      ∀ ⦃G' : SimpleGraph V⦄ [inst_4 : DecidableRel G'.Adj],
        Free.{u_2, u_1} (α := α) ⊤ G' → #G'.edgeFinset ≤ #G.edgeFinset) ↔
    G.CliqueFree (Fintype.card α) ∧
      ∀ ⦃G' : SimpleGraph V⦄ [inst_4 : DecidableRel G'.Adj],
        G'.CliqueFree (Fintype.card α) → #G'.edgeFinset ≤ #G.edgeFinset
⊢ G.IsExtremal (Free.{u_2, u_1} (α := α) ⊤) ↔ G.IsTuranMaximal (Fintype.card α - 1)

Tactic:
simp_rw [IsTuranMaximal, IsExtremal,
    Nat.sub_one_add_one Fintype.card_ne_zero, cliqueFree_iff_top_free]

Premises used: SimpleGraph.IsExtremal, Nat.sub_one_add_one, Fintype.card_ne_zero, SimpleGraph.IsTuranMaximal, SimpleGraph.cliqueFree_iff_top_free
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan
Goal:
n : ℕ
α : Type u_2
inst : Fintype α
inst_1 : Nontrivial α
rw : (turanGraph n (Fintype.card α - 1)).IsTuranMaximal (Fintype.card α - 1)
⊢ (turanGraph n (Fintype.card α - 1)).IsExtremal (Free.{u_2, 0} (α := α) ⊤)

Tactic:
rw [isExtremal_top_free_iff_isTuranMaximal]

Premises used: SimpleGraph.isExtremal_top_free_iff_isTuranMaximal
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan
Goal:
n : ℕ
α : Type u_2
inst : Fintype α
inst_1 : Nontrivial α
⊢ (turanGraph n (Fintype.card α - 1)).IsTuranMaximal (Fintype.card α - 1)

Tactic:
isTuranMaximal_turanGraph (Nat.sub_pos_iff_lt.mpr Fintype.one_lt_card)

Premises used: Iff.mpr, Fintype.one_lt_card, SimpleGraph.isTuranMaximal_turanGraph, Nat.sub_pos_iff_lt
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan
Goal:
n : ℕ
α : Type u_2
inst : Fintype α
inst_1 : Nontrivial α
⊢ (turanGraph n (Fintype.card α - 1)).IsTuranMaximal (Fintype.card α - 1)

Tactic:
exact isTuranMaximal_turanGraph (Nat.sub_pos_iff_lt.mpr Fintype.one_lt_card)

Premises used: Iff.mpr, Fintype.one_lt_card, SimpleGraph.isTuranMaximal_turanGraph, Nat.sub_pos_iff_lt
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan
Goal:
n : ℕ
α : Type u_2
inst : Fintype α
inst_1 : Nontrivial α
enter : n
| extremalNumber.{u_2} n (W := α) ⊤ = #(turanGraph n (Fintype.card α - 1)).edgeFinset

Tactic:
enter [1, 1]
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan
Goal:
n : ℕ
α : Type u_2
inst : Fintype α
inst_1 : Nontrivial α
rw : Fintype.card (Fin n)
| n

Tactic:
rw [← Fintype.card_fin n]

Premises used: Fintype.card_fin
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan
Goal:
n : ℕ
α : Type u_2
inst : Fintype α
inst_1 : Nontrivial α
enter : Fintype.card (Fin n)
| extremalNumber.{u_2} n (W := α) ⊤ = #(turanGraph n (Fintype.card α - 1)).edgeFinset

Tactic:
enter [1, 1]
    rw [← Fintype.card_fin n]

Premises used: Fintype.card_fin
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan
Goal:
n : ℕ
α : Type u_2
inst : Fintype α
inst_1 : Nontrivial α
conv : extremalNumber.{u_2} (Fintype.card (Fin n)) (W := α) ⊤ = #(turanGraph n (Fintype.card α - 1)).edgeFinset
⊢ extremalNumber.{u_2} n (W := α) ⊤ = #(turanGraph n (Fintype.card α - 1)).edgeFinset

Tactic:
conv =>
    enter [1, 1]
    rw [← Fintype.card_fin n]

Premises used: Fintype.card_fin
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan
Goal:
n : ℕ
α : Type u_2
inst : Fintype α
inst_1 : Nontrivial α
⊢ extremalNumber.{u_2} (Fintype.card (Fin n)) (W := α) ⊤ = #(turanGraph n (Fintype.card α - 1)).edgeFinset

Tactic:
(card_edgeFinset_of_isExtremal_free isExtremal_top_free_turanGraph).symm

Premises used: SimpleGraph.card_edgeFinset_of_isExtremal_free, SimpleGraph.isExtremal_top_free_turanGraph, Eq.symm
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan
Goal:
n : ℕ
α : Type u_2
inst : Fintype α
inst_1 : Nontrivial α
⊢ extremalNumber.{u_2} (Fintype.card (Fin n)) (W := α) ⊤ = #(turanGraph n (Fintype.card α - 1)).edgeFinset

Tactic:
exact (card_edgeFinset_of_isExtremal_free isExtremal_top_free_turanGraph).symm

Premises used: SimpleGraph.card_edgeFinset_of_isExtremal_free, SimpleGraph.isExtremal_top_free_turanGraph, Eq.symm
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan
Goal:
V : Type u_1
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
α : Type u_2
inst_2 : Fintype α
inst_3 : Nontrivial α
rw :
  Free.{u_2, u_1} (α := α) ⊤ G ∧ #G.edgeFinset = extremalNumber.{u_2} (Fintype.card V) (W := α) ⊤ ↔
    G.IsTuranMaximal (Fintype.card α - 1)
rw₁ :
  Free.{u_2, u_1} (α := α) ⊤ G ∧ #G.edgeFinset = extremalNumber.{u_2} (Fintype.card V) (W := α) ⊤ ↔
    G.IsExtremal (Free.{u_2, u_1} (α := α) ⊤)
rw₂ rw₃ :
  Free.{u_2, u_1} (α := α) ⊤ G ∧ #G.edgeFinset = extremalNumber.{u_2} (Fintype.card V) (W := α) ⊤ ↔
    Free.{u_2, u_1} (α := α) ⊤ G ∧ #G.edgeFinset = extremalNumber.{u_2} (Fintype.card V) (W := α) ⊤
⊢ Free.{u_2, u_1} (α := α) ⊤ G ∧ #G.edgeFinset = extremalNumber.{u_2} (Fintype.card V) (W := α) ⊤ ↔
    Nonempty.{max 1 (u_1 + 1)} (G.Iso (W := Fin (Fintype.card V)) (turanGraph (Fintype.card V) (Fintype.card α - 1)))

Tactic:
rw [← isTuranMaximal_iff_nonempty_iso_turanGraph (Nat.sub_pos_iff_lt.mpr one_lt_card),
    ← isExtremal_top_free_iff_isTuranMaximal, isExtremal_free_iff]

Premises used: Iff.mpr, Fintype.one_lt_card, SimpleGraph.isExtremal_top_free_iff_isTuranMaximal, Nat.sub_pos_iff_lt, SimpleGraph.isExtremal_free_iff, SimpleGraph.isTuranMaximal_iff_nonempty_iso_turanGraph
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan
Goal:
n r c : ℕ
inl : (∑ w ∈ range 0, if c % 0 ≠ (n + w) % 0 then 1 else 0) = HSub.hSub (α := ℕ) 0 1
inr : ∀ (hr : r > 0), (∑ w ∈ range r, if c % r ≠ (n + w) % r then 1 else 0) = r - 1
⊢ (∑ w ∈ range r, if c % r ≠ (n + w) % r then 1 else 0) = r - 1

Tactic:
rcases r.eq_zero_or_pos with rfl | hr

Premises used: Nat.eq_zero_or_pos, rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan
Goal:
n c : ℕ
⊢ (∑ w ∈ range 0, if c % 0 ≠ (n + w) % 0 then 1 else 0) = HSub.hSub (α := ℕ) 0 1

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan
Goal:
n r c : ℕ
hr : r > 0
this : #({i ∈ range r | c % r = (n + i) % r}) = 1
rw : #({i ∈ range r | c % r ≠ (n + i) % r}) = r - #({i ∈ range r | c % r = (n + i) % r})
⊢ (∑ w ∈ range r, if c % r ≠ (n + w) % r then 1 else 0) = r - 1

Tactic:
rw [← card_filter, ← this]

Premises used: Finset.card_filter
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan
Goal:
n r c : ℕ
hr : r > 0
this : #({i ∈ range r | c % r = (n + i) % r}) = 1
h : #({i ∈ range r | c % r = (n + i) % r}) + #({i ∈ range r | c % r ≠ (n + i) % r}) = r
⊢ #({i ∈ range r | c % r ≠ (n + i) % r}) = r - #({i ∈ range r | c % r = (n + i) % r})

Tactic:
apply Nat.eq_sub_of_add_eq'

Premises used: Nat.eq_sub_of_add_eq'
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan
Goal:
n r c : ℕ
hr : r > 0
this : #({i ∈ range r | c % r = (n + i) % r}) = 1
h : #(range r) = r
h₁ h₂ : r = r
⊢ #({i ∈ range r | c % r = (n + i) % r}) + #({i ∈ range r | c % r ≠ (n + i) % r}) = r

Tactic:
rw [card_filter_add_card_filter_not, card_range]

Premises used: Finset.card_range, Finset.card_filter_add_card_filter_not
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan
Goal:
n r c : ℕ
hr : r > 0
inr : #({i ∈ range r | c % r = (n + i) % r}) = 1
⊢ (∑ w ∈ range r, if c % r ≠ (n + w) % r then 1 else 0) = r - 1

Tactic:
suffices #{i ∈ range r | c % r = (n + i) % r} = 1 by
    rw [← card_filter, ← this]; apply Nat.eq_sub_of_add_eq'
    rw [card_filter_add_card_filter_not, card_range]
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan
Goal:
n r c : ℕ
hr : r > 0
inr : #({i ∈ range r | c % r = (n + i) % r}) ≤ 1
inr₁ : 1 ≤ #({i ∈ range r | c % r = (n + i) % r})
⊢ #({i ∈ range r | c % r = (n + i) % r}) = 1

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan
Goal:
n r c : ℕ
hr : r > 0
inr : ∀ {a b : ℕ}, a ∈ {i ∈ range r | c ≡ n + i [MOD r]} → b ∈ {i ∈ range r | c ≡ n + i [MOD r]} → a = b
⊢ #({i ∈ range r | c ≡ n + i [MOD r]}) ≤ 1

Tactic:
rw [card_le_one_iff]

Premises used: Finset.card_le_one_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan
Goal:
n r c : ℕ
hr : r > 0
w x : ℕ
mw : w ∈ {i ∈ range r | c ≡ n + i [MOD r]}
mx : x ∈ {i ∈ range r | c ≡ n + i [MOD r]}
⊢ w < r ∧ c ≡ n + w [MOD r]

Tactic:
simp only [mem_filter, mem_range] at mw mx

Premises used: Finset.mem_range, Finset.mem_filter
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan
Goal:
n r c : ℕ
hr : r > 0
w x : ℕ
mw : w ∈ {i ∈ range r | c ≡ n + i [MOD r]}
mx : x ∈ {i ∈ range r | c ≡ n + i [MOD r]}
mw₁ : w < r ∧ c ≡ n + w [MOD r]
⊢ x < r ∧ c ≡ n + x [MOD r]

Tactic:
simp only [mem_filter, mem_range] at mw mx

Premises used: Finset.mem_range, Finset.mem_filter
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan
Goal:
n r c : ℕ
hr : r > 0
w x : ℕ
mw : w < r ∧ c ≡ n + w [MOD r]
mx : x < r ∧ c ≡ n + x [MOD r]
⊢ n + w ≡ n + x [MOD r]

Tactic:
have := mw.2.symm.trans mx.2
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan
Goal:
n r c : ℕ
hr : r > 0
w x : ℕ
mw : w < r ∧ c ≡ n + w [MOD r]
mx : x < r ∧ c ≡ n + x [MOD r]
this : n + w ≡ n + x [MOD r]
⊢ w ≡ x [MOD r]

Tactic:
rw [Nat.ModEq.add_iff_left rfl] at this

Premises used: Nat.ModEq.add_iff_left, rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan
Goal:
n r c : ℕ
hr : r > 0
w x : ℕ
mw : w < r ∧ c ≡ n + w [MOD r]
mx : x < r ∧ c ≡ n + x [MOD r]
this : w ≡ x [MOD r]
⊢ w % r = x % r

Tactic:
change w % r = x % r at this
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan
Goal:
n r c : ℕ
hr : r > 0
w x : ℕ
mw : w < r ∧ c ≡ n + w [MOD r]
mx : x < r ∧ c ≡ n + x [MOD r]
this : w % r = x % r
inr : ∀ (this : w = x % r), w = x
inr₁ inr₂ inr₃ inr₄ : ∀ (this : w = x), w = x
⊢ w = x

Tactic:
rwa [Nat.mod_eq_of_lt mw.1, Nat.mod_eq_of_lt mx.1] at this

Premises used: Nat.mod_eq_of_lt, And.left
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan
Goal:
n r c : ℕ
hr : r > 0
inr : {i ∈ range r | c % r = (n + i) % r}.Nonempty
⊢ 1 ≤ #({i ∈ range r | c % r = (n + i) % r})

Tactic:
rw [one_le_card]

Premises used: Finset.one_le_card