awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Basic
Goal:
n₁ n₂ : ℕ
W₁ : Type u_4
W₂ : Type u_5
H₁ : SimpleGraph W₁
H₂ : SimpleGraph W₂
h : n₁ = n₂
e : H₁ ≃g H₂
rw : extremalNumber n₂ H₁ ≤ extremalNumber n₂ H₂ ∧ extremalNumber n₂ H₂ ≤ extremalNumber n₂ H₁
⊢ extremalNumber n₁ H₁ = extremalNumber n₂ H₂

Tactic:
rw [h, le_antisymm_iff]

Premises used: le_antisymm_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Basic
Goal:
n₁ n₂ : ℕ
W₁ : Type u_4
W₂ : Type u_5
H₁ : SimpleGraph W₁
H₂ : SimpleGraph W₂
h : n₁ = n₂
e : H₁ ≃g H₂
refine_1 : extremalNumber n₂ H₁ ≤ extremalNumber n₂ H₂
refine_2 : extremalNumber n₂ H₂ ≤ extremalNumber n₂ H₁
⊢ extremalNumber n₂ H₁ ≤ extremalNumber n₂ H₂ ∧ extremalNumber n₂ H₂ ≤ extremalNumber n₂ H₁

Tactic:
and_intros
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Basic
Goal:
n₁ n₂ : ℕ
W₁ : Type u_4
W₂ : Type u_5
H₁ : SimpleGraph W₁
H₂ : SimpleGraph W₂
h : n₁ = n₂
e : H₁ ≃g H₂
refine_2 : ∀ (e : H₂ ≃g H₁), extremalNumber n₂ H₂ ≤ extremalNumber n₂ H₁
⊢ extremalNumber n₂ H₂ ≤ extremalNumber n₂ H₁

Tactic:
replace e := e.symm
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Basic
Goal:
n₁ n₂ : ℕ
W₁ : Type u_4
W₂ : Type u_5
H₁ : SimpleGraph W₁
H₂ : SimpleGraph W₂
h : n₁ = n₂
e : H₁ ≃g H₂
refine_2 : ∀ (e : H₂ ≃g H₁), extremalNumber n₂ H₂ ≤ extremalNumber n₂ H₁
⊢ extremalNumber n₂ H₂ ≤ extremalNumber n₂ H₁

Tactic:
on_goal 2 =>
    replace e := e.symm
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Basic
Goal:
n₁ n₂ : ℕ
W₁ : Type u_4
W₂ : Type u_5
H₁ : SimpleGraph W₁
H₂ : SimpleGraph W₂
h : n₁ = n₂
e : H₁ ≃g H₂
refine_1 :
  ∀ ⦃G : SimpleGraph (Fin n₂)⦄ [inst : DecidableRel G.Adj],
    H₁.Free G → #G.edgeFinset ≤ extremalNumber (Fintype.card (Fin n₂)) H₂
⊢ extremalNumber n₂ H₁ ≤ extremalNumber n₂ H₂

Tactic:
rw [← Fintype.card_fin n₂, extremalNumber_le_iff]

Premises used: Fintype.card_fin, SimpleGraph.extremalNumber_le_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Basic
Goal:
n₁ n₂ : ℕ
W₁ : Type u_4
W₂ : Type u_5
H₁ : SimpleGraph W₁
H₂ : SimpleGraph W₂
h : n₁ = n₂
e : H₁ ≃g H₂
G : SimpleGraph (Fin n₂)
refine_1 : ∀ [inst : DecidableRel G.Adj], H₁.Free G → #G.edgeFinset ≤ extremalNumber (Fintype.card (Fin n₂)) H₂
⊢ ∀ [inst : DecidableRel G.Adj], H₁.Free G → #G.edgeFinset ≤ extremalNumber (Fintype.card (Fin n₂)) H₂

Tactic:
_
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Basic
Goal:
n₁ n₂ : ℕ
W₁ : Type u_4
W₂ : Type u_5
H₁ : SimpleGraph W₁
H₂ : SimpleGraph W₂
h_1 : n₁ = n₂
e : H₁ ≃g H₂
G : SimpleGraph (Fin n₂)
inst : DecidableRel G.Adj
h : H₁.Free G
refine_1 : H₂.Free G
⊢ #G.edgeFinset ≤ extremalNumber (Fintype.card (Fin n₂)) H₂

Tactic:
apply card_edgeFinset_le_extremalNumber

Premises used: SimpleGraph.card_edgeFinset_le_extremalNumber
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Basic
Goal:
n₁ n₂ : ℕ
W₁ : Type u_4
W₂ : Type u_5
H₁ : SimpleGraph W₁
H₂ : SimpleGraph W₂
h_1 : n₁ = n₂
e : H₁ ≃g H₂
G : SimpleGraph (Fin n₂)
inst : DecidableRel G.Adj
h : H₁.Free G
refine_1 : ∀ (h : H₂ ⊑ G), H₁ ⊑ G
⊢ H₂.Free G

Tactic:
contrapose h
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Basic
Goal:
n₁ n₂ : ℕ
W₁ : Type u_4
W₂ : Type u_5
H₁ : SimpleGraph W₁
H₂ : SimpleGraph W₂
h_1 : n₁ = n₂
e : H₁ ≃g H₂
G : SimpleGraph (Fin n₂)
inst : DecidableRel G.Adj
h : H₂ ⊑ G
⊢ H₁ ⊑ G

Tactic:
h.trans' ⟨e.toCopy⟩

Premises used: Nonempty.intro, SimpleGraph.Iso.toCopy, SimpleGraph.IsContained.trans'
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Basic
Goal:
n₁ n₂ : ℕ
W₁ : Type u_4
W₂ : Type u_5
H₁ : SimpleGraph W₁
H₂ : SimpleGraph W₂
h_1 : n₁ = n₂
e : H₁ ≃g H₂
G : SimpleGraph (Fin n₂)
inst : DecidableRel G.Adj
h : H₂ ⊑ G
⊢ H₁ ⊑ G

Tactic:
exact h.trans' ⟨e.toCopy⟩

Premises used: Nonempty.intro, SimpleGraph.Iso.toCopy, SimpleGraph.IsContained.trans'
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Basic
Goal:
n₁ n₂ : ℕ
W₁ : Type u_4
W₂ : Type u_5
H₁ : SimpleGraph W₁
H₂ : SimpleGraph W₂
h : n₁ = n₂
e : H₂ ≃g H₁
refine_2 :
  ∀ ⦃G : SimpleGraph (Fin n₂)⦄ [inst : DecidableRel G.Adj],
    H₂.Free G → #G.edgeFinset ≤ extremalNumber (Fintype.card (Fin n₂)) H₁
⊢ extremalNumber n₂ H₂ ≤ extremalNumber n₂ H₁

Tactic:
rw [← Fintype.card_fin n₂, extremalNumber_le_iff]

Premises used: Fintype.card_fin, SimpleGraph.extremalNumber_le_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Basic
Goal:
n₁ n₂ : ℕ
W₁ : Type u_4
W₂ : Type u_5
H₁ : SimpleGraph W₁
H₂ : SimpleGraph W₂
h : n₁ = n₂
e : H₂ ≃g H₁
G : SimpleGraph (Fin n₂)
refine_2 : ∀ [inst : DecidableRel G.Adj], H₂.Free G → #G.edgeFinset ≤ extremalNumber (Fintype.card (Fin n₂)) H₁
⊢ ∀ [inst : DecidableRel G.Adj], H₂.Free G → #G.edgeFinset ≤ extremalNumber (Fintype.card (Fin n₂)) H₁

Tactic:
_
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Basic
Goal:
n₁ n₂ : ℕ
W₁ : Type u_4
W₂ : Type u_5
H₁ : SimpleGraph W₁
H₂ : SimpleGraph W₂
h_1 : n₁ = n₂
e : H₂ ≃g H₁
G : SimpleGraph (Fin n₂)
inst : DecidableRel G.Adj
h : H₂.Free G
refine_2 : H₁.Free G
⊢ #G.edgeFinset ≤ extremalNumber (Fintype.card (Fin n₂)) H₁

Tactic:
apply card_edgeFinset_le_extremalNumber

Premises used: SimpleGraph.card_edgeFinset_le_extremalNumber
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Basic
Goal:
n₁ n₂ : ℕ
W₁ : Type u_4
W₂ : Type u_5
H₁ : SimpleGraph W₁
H₂ : SimpleGraph W₂
h_1 : n₁ = n₂
e : H₂ ≃g H₁
G : SimpleGraph (Fin n₂)
inst : DecidableRel G.Adj
h : H₂.Free G
refine_2 : ∀ (h : H₁ ⊑ G), H₂ ⊑ G
⊢ H₁.Free G

Tactic:
contrapose h
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Basic
Goal:
n₁ n₂ : ℕ
W₁ : Type u_4
W₂ : Type u_5
H₁ : SimpleGraph W₁
H₂ : SimpleGraph W₂
h_1 : n₁ = n₂
e : H₂ ≃g H₁
G : SimpleGraph (Fin n₂)
inst : DecidableRel G.Adj
h : H₁ ⊑ G
⊢ H₂ ⊑ G

Tactic:
h.trans' ⟨e.toCopy⟩

Premises used: Nonempty.intro, SimpleGraph.Iso.toCopy, SimpleGraph.IsContained.trans'
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Basic
Goal:
n₁ n₂ : ℕ
W₁ : Type u_4
W₂ : Type u_5
H₁ : SimpleGraph W₁
H₂ : SimpleGraph W₂
h_1 : n₁ = n₂
e : H₂ ≃g H₁
G : SimpleGraph (Fin n₂)
inst : DecidableRel G.Adj
h : H₁ ⊑ G
⊢ H₂ ⊑ G

Tactic:
exact h.trans' ⟨e.toCopy⟩

Premises used: Nonempty.intro, SimpleGraph.Iso.toCopy, SimpleGraph.IsContained.trans'
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Basic
Goal:
n : ℕ
W₁ : Type u_4
W₂ : Type u_5
H₁ : SimpleGraph W₁
H₂ : SimpleGraph W₂
e : H₁ ≃g H₂
⊢ extremalNumber n H₁ = extremalNumber n H₂

Tactic:
extremalNumber_congr rfl e

Premises used: SimpleGraph.extremalNumber_congr, rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Basic
Goal:
V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
inst : Fintype V
inst_1 : DecidableRel G.Adj
rw : H.Free G → (extremalNumber (Fintype.card V) H ≤ #G.edgeFinset ↔ #G.edgeFinset = extremalNumber (Fintype.card V) H)
⊢ G.IsExtremal H.Free ↔ H.Free G ∧ #G.edgeFinset = extremalNumber (Fintype.card V) H

Tactic:
rw [IsExtremal, and_congr_right_iff, ← extremalNumber_le_iff]

Premises used: SimpleGraph.IsExtremal, and_congr_right_iff, SimpleGraph.extremalNumber_le_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Basic
Goal:
V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
inst : Fintype V
inst_1 : DecidableRel G.Adj
⊢ H.Free G → (extremalNumber (Fintype.card V) H ≤ #G.edgeFinset ↔ #G.edgeFinset = extremalNumber (Fintype.card V) H)

Tactic:
fun h ↦ ⟨eq_of_le_of_ge (card_edgeFinset_le_extremalNumber h), ge_of_eq⟩

Premises used: ge_of_eq, SimpleGraph.card_edgeFinset_le_extremalNumber, Iff.intro, eq_of_le_of_ge
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Basic
Goal:
V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
inst : Fintype V
inst_1 : DecidableRel G.Adj
⊢ H.Free G → (extremalNumber (Fintype.card V) H ≤ #G.edgeFinset ↔ #G.edgeFinset = extremalNumber (Fintype.card V) H)

Tactic:
exact fun h ↦ ⟨eq_of_le_of_ge (card_edgeFinset_le_extremalNumber h), ge_of_eq⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Basic
Goal:
V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
inst : Fintype V
inst_1 : DecidableRel G.Adj
h : G.IsExtremal H.Free
⊢ #G.edgeFinset = extremalNumber (Fintype.card V) H

Tactic:
(isExtremal_free_iff.mp h).2

Premises used: SimpleGraph.isExtremal_free_iff, And.right, Iff.mp
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Basic
Goal:
V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
inst : Fintype V
inst_1 : DecidableRel G.Adj
inst_2 : DecidableEq V
h : H.Free G
v : V
rw :
  Finset.card (α := Sym2 (↑{v}ᶜ : Type u_1)) (edgeFinset (induce {v}ᶜ G)) ≤
    extremalNumber (Fintype.card.{u_1} (↑{v}ᶜ : Type u_1)) H
⊢ #(G.deleteIncidenceSet v).edgeFinset ≤ extremalNumber (Fintype.card V - 1) H

Tactic:
rw [← card_edgeFinset_induce_compl_singleton, ← @card_unique ({v} : Set V), ← card_compl_set]

Premises used: Fintype.card_unique, Fintype.card_compl_set, SimpleGraph.card_edgeFinset_induce_compl_singleton
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Basic
Goal:
V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
inst : Fintype V
inst_1 : DecidableRel G.Adj
inst_2 : DecidableEq V
h : H.Free G
v : V
h₁ : H.Free (β := (↑{v}ᶜ : Type u_1)) (induce {v}ᶜ G)
⊢ Finset.card (α := Sym2 (↑{v}ᶜ : Type u_1)) (edgeFinset (induce {v}ᶜ G)) ≤
    extremalNumber (Fintype.card.{u_1} (↑{v}ᶜ : Type u_1)) H

Tactic:
apply card_edgeFinset_le_extremalNumber

Premises used: SimpleGraph.card_edgeFinset_le_extremalNumber
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Basic
Goal:
V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
inst : Fintype V
inst_1 : DecidableRel G.Adj
inst_2 : DecidableEq V
h : H.Free G
v : V
h₁ : ∀ (h : H.IsContained (β := (↑{v}ᶜ : Type u_1)) (induce {v}ᶜ G)), H ⊑ G
⊢ H.Free (β := (↑{v}ᶜ : Type u_1)) (induce {v}ᶜ G)

Tactic:
contrapose h
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Basic
Goal:
V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
inst : Fintype V
inst_1 : DecidableRel G.Adj
inst_2 : DecidableEq V
v : V
h : H.IsContained (β := (↑{v}ᶜ : Type u_1)) (induce {v}ᶜ G)
⊢ H ⊑ G

Tactic:
h.trans ⟨Copy.induce G {v}ᶜ⟩

Premises used: SimpleGraph.IsContained.trans, SimpleGraph.Copy.induce, Compl.compl, Nonempty.intro, Singleton.singleton
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Basic
Goal:
V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
inst : Fintype V
inst_1 : DecidableRel G.Adj
inst_2 : DecidableEq V
v : V
h : H.IsContained (β := (↑{v}ᶜ : Type u_1)) (induce {v}ᶜ G)
⊢ H ⊑ G

Tactic:
exact h.trans ⟨Copy.induce G {v}ᶜ⟩

Premises used: SimpleGraph.IsContained.trans, SimpleGraph.Copy.induce, Compl.compl, Nonempty.intro, Singleton.singleton
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan
Goal:
n r : ℕ
v w : Fin n
⊢ (turanGraph n r).Adj v w ↔ (↑v : ℕ) % r ≠ (↑w : ℕ) % r

Tactic:
.rfl

Premises used: Iff.rfl, Not
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan
Goal:
n : ℕ
⊢ turanGraph n 0 = ⊤

Tactic:
simp [turanGraph, Fin.val_inj, Top.top]

Premises used: SimpleGraph.turanGraph, Top.top, Fin.val_inj
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan
Goal:
n r : ℕ
simp_rw : (∀ (x x_1 : Fin n), (↑x : ℕ) % r = (↑x_1 : ℕ) % r ↔ x = x_1) ↔ r = 0 ∨ n ≤ r
⊢ turanGraph n r = ⊤ ↔ r = 0 ∨ n ≤ r

Tactic:
simp_rw [SimpleGraph.ext_iff, funext_iff, turanGraph, top_adj, eq_iff_iff, not_iff_not]

Premises used: not_iff_not, SimpleGraph.turanGraph, funext_iff, SimpleGraph.top_adj, SimpleGraph.ext_iff, eq_iff_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan
Goal:
n r : ℕ
⊢ (∀ (x x_1 : Fin n), (↑x : ℕ) % r = (↑x_1 : ℕ) % r ↔ x = x_1) ↔ r = 0 ∨ n ≤ r

Tactic:
⟨fun h ↦ ?_, ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan
Goal:
n r : ℕ
refine_1 : ∀ (h : ∀ (x x_1 : Fin n), (↑x : ℕ) % r = (↑x_1 : ℕ) % r ↔ x = x_1), r = 0 ∨ n ≤ r
refine_2 : r = 0 ∨ n ≤ r → ∀ (x x_1 : Fin n), (↑x : ℕ) % r = (↑x_1 : ℕ) % r ↔ x = x_1
⊢ (∀ (x x_1 : Fin n), (↑x : ℕ) % r = (↑x_1 : ℕ) % r ↔ x = x_1) ↔ r = 0 ∨ n ≤ r

Tactic:
refine ⟨fun h ↦ ?_, ?_⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan
Goal:
n r : ℕ
h : ∀ (x x_1 : Fin n), (↑x : ℕ) % r = (↑x_1 : ℕ) % r ↔ x = x_1
refine_1 :
  ∀ (h : r ≠ 0 ∧ r < n),
    ∃ (x : Fin n) (x_1 : Fin n), (↑x : ℕ) % r = (↑x_1 : ℕ) % r ∧ x ≠ x_1 ∨ (↑x : ℕ) % r ≠ (↑x_1 : ℕ) % r ∧ x = x_1
⊢ r = 0 ∨ n ≤ r

Tactic:
contrapose! h
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan
Goal:
n r : ℕ
h : r ≠ 0 ∧ r < n
h₁ :
  (↑(⟨0, ⋯⟩ : Fin n) : ℕ) % r = (↑(⟨r, ⋯⟩ : Fin n) : ℕ) % r ∧ (⟨0, ⋯⟩ : Fin n) ≠ ⟨r, ⋯⟩ ∨
    (↑(⟨0, ⋯⟩ : Fin n) : ℕ) % r ≠ (↑(⟨r, ⋯⟩ : Fin n) : ℕ) % r ∧ (⟨0, ⋯⟩ : Fin n) = ⟨r, ⋯⟩
⊢ ∃ (x : Fin n) (x_1 : Fin n), (↑x : ℕ) % r = (↑x_1 : ℕ) % r ∧ x ≠ x_1 ∨ (↑x : ℕ) % r ≠ (↑x_1 : ℕ) % r ∧ x = x_1

Tactic:
use ⟨0, (Nat.pos_of_ne_zero h.1).trans h.2⟩, ⟨r, h.2⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan
Goal:
n r : ℕ
h : r ≠ 0 ∧ r < n
⊢ (↑(⟨0, ⋯⟩ : Fin n) : ℕ) % r = (↑(⟨r, ⋯⟩ : Fin n) : ℕ) % r ∧ (⟨0, ⋯⟩ : Fin n) ≠ ⟨r, ⋯⟩ ∨
    (↑(⟨0, ⋯⟩ : Fin n) : ℕ) % r ≠ (↑(⟨r, ⋯⟩ : Fin n) : ℕ) % r ∧ (⟨0, ⋯⟩ : Fin n) = ⟨r, ⋯⟩

Tactic:
simp [h.1.symm]

Premises used: Ne.symm, And.left
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan
Goal:
n : ℕ
a b : Fin n
⊢ (↑a : ℕ) % 0 = (↑b : ℕ) % 0 ↔ a = b

Tactic:
simp [Fin.val_inj]

Premises used: Fin.val_inj
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan
Goal:
n r : ℕ
h : n ≤ r
a b : Fin n
refine_2 : (↑a : ℕ) = (↑b : ℕ) % r ↔ a = b
refine_2₁ : (↑a : ℕ) = (↑b : ℕ) ↔ a = b
refine_2₂ refine_2₃ : a = b ↔ a = b
⊢ (↑a : ℕ) % r = (↑b : ℕ) % r ↔ a = b

Tactic:
rw [Nat.mod_eq_of_lt (a.2.trans_le h), Nat.mod_eq_of_lt (b.2.trans_le h), Fin.val_inj]

Premises used: Fin.isLt, Nat.mod_eq_of_lt, LT.lt.trans_le, Fin.val_inj
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan
Goal:
n r : ℕ
hr : 0 < r
rw : IsEmpty (Copy (α := Fin (r + 1)) (completeGraph (Fin (r + 1))) (turanGraph n r))
⊢ (turanGraph n r).CliqueFree (r + 1)

Tactic:
rw [cliqueFree_iff]

Premises used: SimpleGraph.cliqueFree_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan
Goal:
n r : ℕ
hr : 0 < r
by_contra! : ∀ (f : Copy (α := Fin (r + 1)) (completeGraph (Fin (r + 1))) (turanGraph n r)), False
⊢ IsEmpty (Copy (α := Fin (r + 1)) (completeGraph (Fin (r + 1))) (turanGraph n r))

Tactic:
by_contra! ⟨f⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan
Goal:
n r : ℕ
hr : 0 < r
f : Copy (α := Fin (r + 1)) (completeGraph (Fin (r + 1))) (turanGraph n r)
⊢ Fintype.card (Fin r) < Fintype.card (Fin (r + 1))

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan
Goal:
n r : ℕ
hr : 0 < r
f : Copy (α := Fin (r + 1)) (completeGraph (Fin (r + 1))) (turanGraph n r)
obtain :
  ∀ (x y : Fin (r + 1)) (d : x ≠ y)
    (c :
      (⟨(↑((f : (a : Fin (r + 1)) → Fin n) x) : ℕ) % r, ⋯⟩ : Fin r) =
        ⟨(↑((f : (a : Fin (r + 1)) → Fin n) y) : ℕ) % r, ⋯⟩),
    False
⊢ False

Tactic:
obtain ⟨x, y, d, c⟩ := exists_ne_map_eq_of_card_lt (fun x ↦
    (⟨(f x).1 % r, Nat.mod_lt _ hr⟩ : Fin r)) (by simp)

Premises used: Fintype.exists_ne_map_eq_of_card_lt, Fin.mk, Fin.val, Nat.mod_lt, HMod.hMod, DFunLike.coe
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan
Goal:
n r : ℕ
hr : 0 < r
f : Copy (α := Fin (r + 1)) (completeGraph (Fin (r + 1))) (turanGraph n r)
x y : Fin (r + 1)
d : x ≠ y
c : (⟨(↑((f : (a : Fin (r + 1)) → Fin n) x) : ℕ) % r, ⋯⟩ : Fin r) = ⟨(↑((f : (a : Fin (r + 1)) → Fin n) y) : ℕ) % r, ⋯⟩
⊢ (↑((f : (a : Fin (r + 1)) → Fin n) x) : ℕ) % r = (↑((f : (a : Fin (r + 1)) → Fin n) y) : ℕ) % r

Tactic:
rw [Fin.mk.injEq] at c

Premises used: Fin.mk.injEq
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan
Goal:
n r : ℕ
hr : 0 < r
f : Copy (α := Fin (r + 1)) (completeGraph (Fin (r + 1))) (turanGraph n r)
x y : Fin (r + 1)
d : x ≠ y
c : (↑((f : (a : Fin (r + 1)) → Fin n) x) : ℕ) % r = (↑((f : (a : Fin (r + 1)) → Fin n) y) : ℕ) % r
⊢ False

Tactic:
absurd c <| f.toHom.map_adj d

Premises used: SimpleGraph.Hom.map_adj, absurd, SimpleGraph.Copy.toHom
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan
Goal:
n r : ℕ
hr : 0 < r
f : Copy (α := Fin (r + 1)) (completeGraph (Fin (r + 1))) (turanGraph n r)
x y : Fin (r + 1)
d : x ≠ y
c : (↑((f : (a : Fin (r + 1)) → Fin n) x) : ℕ) % r = (↑((f : (a : Fin (r + 1)) → Fin n) y) : ℕ) % r
⊢ False

Tactic:
exact absurd c <| f.toHom.map_adj d

Premises used: SimpleGraph.Hom.map_adj, absurd, SimpleGraph.Copy.toHom
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan
Goal:
V : Type u_1
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
r : ℕ
hn : r ≤ Fintype.card V
hG : G.IsTuranMaximal r
h : G.CliqueFree r
obtain : ∀ K ⊆ univ, ∀ (hn : #K ≤ Fintype.card V) (hG : G.IsTuranMaximal #K) (h : G.CliqueFree #K), False
⊢ False

Tactic:
obtain ⟨K, _, rfl⟩ := exists_subset_card_eq hn

Premises used: Finset.exists_subset_card_eq, rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan
Goal:
V : Type u_1
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
K : Finset V
left : K ⊆ univ
hn : #K ≤ Fintype.card V
hG : G.IsTuranMaximal #K
h : G.CliqueFree #K
⊢ ∃ a ∈ K, ∃ b ∈ K, a ≠ b ∧ ¬G.Adj a b

Tactic:
simpa only [isNClique_iff, IsClique, Set.Pairwise, mem_coe, ne_eq, and_true, not_forall,
      exists_prop, exists_and_right] using h K

Premises used: and_true, exists_and_right, exists_prop, Set.Pairwise, ne_eq, SimpleGraph.isNClique_iff, Classical.not_forall, Finset.mem_coe, SimpleGraph.IsClique
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan
Goal:
V : Type u_1
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
K : Finset V
left : K ⊆ univ
hn : #K ≤ Fintype.card V
hG : G.IsTuranMaximal #K
h : G.CliqueFree #K
obtain : ∀ (a b : V) (hab : a ≠ b) (hGab : ¬G.Adj a b), False
⊢ False

Tactic:
obtain ⟨a, -, b, -, hab, hGab⟩ : ∃ a ∈ K, ∃ b ∈ K, a ≠ b ∧ ¬ G.Adj a b := by
    simpa only [isNClique_iff, IsClique, Set.Pairwise, mem_coe, ne_eq, and_true, not_forall,
      exists_prop, exists_and_right] using h K
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan
Goal:
V : Type u_1
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
K : Finset V
left : K ⊆ univ
hn : #K ≤ Fintype.card V
hG : G.IsTuranMaximal #K
h : G.CliqueFree #K
a b : V
hab : a ≠ b
hGab : ¬G.Adj a b
⊢ False

Tactic:
hGab <| le_sup_right.trans_eq ((hG.le_iff_eq <| h.sup_edge _ _).1 le_sup_left).symm <|
    (edge_adj ..).2 ⟨Or.inl ⟨rfl, rfl⟩, hab⟩

Premises used: Iff.mpr, LE.le.trans_eq, SimpleGraph.IsExtremal.le_iff_eq, le_sup_left, SimpleGraph.CliqueFree.sup_edge, le_sup_right, SimpleGraph.edge_adj, And.intro, Iff.mp, Or.inl, Eq.symm, rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan
Goal:
V : Type u_1
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
K : Finset V
left : K ⊆ univ
hn : #K ≤ Fintype.card V
hG : G.IsTuranMaximal #K
h : G.CliqueFree #K
a b : V
hab : a ≠ b
hGab : ¬G.Adj a b
⊢ False

Tactic:
exact hGab <| le_sup_right.trans_eq ((hG.le_iff_eq <| h.sup_edge _ _).1 le_sup_left).symm <|
    (edge_adj ..).2 ⟨Or.inl ⟨rfl, rfl⟩, hab⟩

Premises used: Iff.mpr, LE.le.trans_eq, SimpleGraph.IsExtremal.le_iff_eq, le_sup_left, SimpleGraph.CliqueFree.sup_edge, le_sup_right, SimpleGraph.edge_adj, And.intro, Iff.mp, Or.inl, Eq.symm, rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan
Goal:
V : Type u_1
inst : Fintype V
r : ℕ
hr : 0 < r
⊢ 2 ≤ r + 1

Tactic:
lia
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan
Goal:
V : Type u_1
inst : Fintype V
r : ℕ
hr : 0 < r
⊢ ∃ (H : SimpleGraph V) (x : DecidableRel H.Adj), H.IsTuranMaximal r

Tactic:
simpa [IsTuranMaximal, exists_isExtremal_iff_exists] using ⟨⊥, cliqueFree_bot (by lia)⟩

Premises used: SimpleGraph.exists_isExtremal_iff_exists, SimpleGraph.IsTuranMaximal
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan
Goal:
V : Type u_1
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
r : ℕ
s t : V
h : G.IsTuranMaximal r
hn : ¬G.Adj s t
⊢ G.CliqueFree (r + 1) ∧
    ∀ ⦃G' : SimpleGraph V⦄ [inst_2 : DecidableRel G'.Adj], G'.CliqueFree (r + 1) → #G'.edgeFinset ≤ #G.edgeFinset

Tactic:
rw [IsTuranMaximal, IsExtremal] at h

Premises used: SimpleGraph.IsExtremal, SimpleGraph.IsTuranMaximal
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan
Goal:
V : Type u_1
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
r : ℕ
s t : V
h : G.IsTuranMaximal r
hn : ¬G.Adj s t
h₁ :
  G.CliqueFree (r + 1) ∧
    ∀ ⦃G' : SimpleGraph V⦄ [inst_2 : DecidableRel G'.Adj], G'.CliqueFree (r + 1) → #G'.edgeFinset ≤ #G.edgeFinset
⊢ ¬G.Adj s t

Tactic:
rw [IsTuranMaximal, IsExtremal] at h

Premises used: SimpleGraph.IsExtremal, SimpleGraph.IsTuranMaximal
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan
Goal:
V : Type u_1
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
r : ℕ
s t : V
h :
  G.CliqueFree (r + 1) ∧
    ∀ ⦃G' : SimpleGraph V⦄ [inst_2 : DecidableRel G'.Adj], G'.CliqueFree (r + 1) → #G'.edgeFinset ≤ #G.edgeFinset
hn : ¬G.Adj s t
contrapose! :
  ∀ (h : G.degree s ≠ G.degree t) (_ : G.CliqueFree (r + 1)),
    ∃ (G' : SimpleGraph V) (inst_2 : DecidableRel G'.Adj), G'.CliqueFree (r + 1) ∧ #G.edgeFinset < #G'.edgeFinset
⊢ G.degree s = G.degree t

Tactic:
contrapose! h
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan
Goal:
V : Type u_1
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
r : ℕ
s t : V
hn : ¬G.Adj s t
h : G.degree s ≠ G.degree t
cf : G.CliqueFree (r + 1)
inr :
  ∀
    (this :
      ∀ {G : SimpleGraph V} [inst_2 : DecidableRel G.Adj] {s t : V} (hn : ¬G.Adj s t) (h : G.degree s ≠ G.degree t)
        (cf : G.CliqueFree (r + 1)) (hd : G.degree t < G.degree s),
        ∃ (G' : SimpleGraph V) (inst_3 : DecidableRel G'.Adj), G'.CliqueFree (r + 1) ∧ #G.edgeFinset < #G'.edgeFinset)
    (hd : ¬G.degree t < G.degree s),
    ∃ (G' : SimpleGraph V) (inst_2 : DecidableRel G'.Adj), G'.CliqueFree (r + 1) ∧ #G.edgeFinset < #G'.edgeFinset
wlog :
  ∀ {G : SimpleGraph V} [inst_2 : DecidableRel G.Adj] {s t : V} (hn : ¬G.Adj s t) (h : G.degree s ≠ G.degree t)
    (cf : G.CliqueFree (r + 1)) (hd : G.degree t < G.degree s),
    ∃ (G' : SimpleGraph V) (inst_3 : DecidableRel G'.Adj), G'.CliqueFree (r + 1) ∧ #G.edgeFinset < #G'.edgeFinset
⊢ ∃ (G' : SimpleGraph V) (inst_2 : DecidableRel G'.Adj), G'.CliqueFree (r + 1) ∧ #G.edgeFinset < #G'.edgeFinset

Tactic:
wlog hd : G.degree t < G.degree s generalizing G t s

Premises used: SimpleGraph.degree
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan
Goal:
V : Type u_1
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
r : ℕ
s t : V
hn : ¬G.Adj s t
h : G.degree s ≠ G.degree t
cf : G.CliqueFree (r + 1)
this :
  ∀ {G : SimpleGraph V} [inst_2 : DecidableRel G.Adj] {s t : V} (hn : ¬G.Adj s t) (h : G.degree s ≠ G.degree t)
    (cf : G.CliqueFree (r + 1)) (hd : G.degree t < G.degree s),
    ∃ (G' : SimpleGraph V) (inst_3 : DecidableRel G'.Adj), G'.CliqueFree (r + 1) ∧ #G.edgeFinset < #G'.edgeFinset
hd : ¬G.degree t < G.degree s
⊢ G.degree s < G.degree t

Tactic:
replace hd : G.degree s < G.degree t := lt_of_le_of_ne (le_of_not_gt hd) h
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan
Goal:
V : Type u_1
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
r : ℕ
s t : V
hn : ¬G.Adj s t
h : G.degree s ≠ G.degree t
cf : G.CliqueFree (r + 1)
this :
  ∀ {G : SimpleGraph V} [inst_2 : DecidableRel G.Adj] {s t : V} (hn : ¬G.Adj s t) (h : G.degree s ≠ G.degree t)
    (cf : G.CliqueFree (r + 1)) (hd : G.degree t < G.degree s),
    ∃ (G' : SimpleGraph V) (inst_3 : DecidableRel G'.Adj), G'.CliqueFree (r + 1) ∧ #G.edgeFinset < #G'.edgeFinset
hd : G.degree s < G.degree t
rwa rwa₁ rwa₂ rwa₃ :
  ∀ (hn : ¬G.Adj t s) (h : G.degree s ≠ G.degree t) (cf : G.CliqueFree (r + 1))
    (this :
      ∀ {G : SimpleGraph V} [inst_2 : DecidableRel G.Adj] {s t : V} (hn : ¬G.Adj s t) (h : G.degree s ≠ G.degree t)
        (cf : G.CliqueFree (r + 1)) (hd : G.degree t < G.degree s),
        ∃ (G' : SimpleGraph V) (inst_3 : DecidableRel G'.Adj), G'.CliqueFree (r + 1) ∧ #G.edgeFinset < #G'.edgeFinset)
    (hd : G.degree s < G.degree t), ¬G.Adj t s
⊢ ¬G.Adj t s

Tactic:
rwa [adj_comm] at hn

Premises used: SimpleGraph.adj_comm