awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Extremal.Basic (goal)
Goal:
n₁ n₂ : ℕ
W₁ : Type u_4
W₂ : Type u_5
H₁ : SimpleGraph W₁
H₂ : SimpleGraph W₂
h : n₁ = n₂
e : H₁ ≃g H₂
⊢ extremalNumber n₂ H₁ ≤ extremalNumber n₂ H₂ ∧ extremalNumber n₂ H₂ ≤ extremalNumber n₂ H₁
have refine_1 : extremalNumber n₂ H₁ ≤ extremalNumber n₂ H₂
Tactic: and_intros
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Extremal.Basic (goal)
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₂
⊢ extremalNumber n₂ H₁ ≤ extremalNumber n₂ H₂ ∧ extremalNumber n₂ H₂ ≤ extremalNumber n₂ H₁
have refine_2 : extremalNumber n₂ H₂ ≤ extremalNumber n₂ H₁
Tactic: and_intros
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Extremal.Basic (goal)
Goal:
n₁ n₂ : ℕ
W₁ : Type u_4
W₂ : Type u_5
H₁ : SimpleGraph W₁
H₂ : SimpleGraph W₂
h : n₁ = n₂
e : H₁ ≃g H₂
⊢ extremalNumber n₂ H₂ ≤ extremalNumber n₂ H₁
have refine_2 : ∀ (e : H₂ ≃g H₁), extremalNumber n₂ H₂ ≤ extremalNumber n₂ H₁
Tactic: replace e := e.symm
Cleared hypotheses: e
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Extremal.Basic (goal)
Goal:
n₁ n₂ : ℕ
W₁ : Type u_4
W₂ : Type u_5
H₁ : SimpleGraph W₁
H₂ : SimpleGraph W₂
h : n₁ = n₂
e : H₁ ≃g H₂
⊢ extremalNumber n₂ H₂ ≤ extremalNumber n₂ H₁
have refine_2 : ∀ (e : H₂ ≃g H₁), extremalNumber n₂ H₂ ≤ extremalNumber n₂ H₁
Tactic: on_goal 2 =>
    replace e := e.symm
Cleared hypotheses: e
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Extremal.Basic (goal)
Goal:
n₁ n₂ : ℕ
W₁ : Type u_4
W₂ : Type u_5
H₁ : SimpleGraph W₁
H₂ : SimpleGraph W₂
h : n₁ = n₂
e : H₁ ≃g H₂
⊢ extremalNumber n₂ H₁ ≤ extremalNumber n₂ H₂
have refine_1 : ∀ ⦃G : SimpleGraph (Fin n₂)⦄ [inst : DecidableRel G.Adj],
  H₁.Free G → #G.edgeFinset ≤ extremalNumber (Fintype.card (Fin n₂)) H₂
Tactic: rw [← Fintype.card_fin n₂, extremalNumber_le_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Extremal.Basic (goal)
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
⊢ #G.edgeFinset ≤ extremalNumber (Fintype.card (Fin n₂)) H₂
have refine_1 : H₂.Free G
Tactic: apply card_edgeFinset_le_extremalNumber
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Extremal.Basic (goal)
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
⊢ H₂.Free G
have refine_1 : ∀ (h : H₂ ⊑ G), H₁ ⊑ G
Tactic: contrapose h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Extremal.Basic (goal)
Goal:
n₁ n₂ : ℕ
W₁ : Type u_4
W₂ : Type u_5
H₁ : SimpleGraph W₁
H₂ : SimpleGraph W₂
h : n₁ = n₂
e : H₂ ≃g H₁
⊢ extremalNumber n₂ H₂ ≤ extremalNumber n₂ H₁
have refine_2 : ∀ ⦃G : SimpleGraph (Fin n₂)⦄ [inst : DecidableRel G.Adj],
  H₂.Free G → #G.edgeFinset ≤ extremalNumber (Fintype.card (Fin n₂)) H₁
Tactic: rw [← Fintype.card_fin n₂, extremalNumber_le_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Extremal.Basic (goal)
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
⊢ #G.edgeFinset ≤ extremalNumber (Fintype.card (Fin n₂)) H₁
have refine_2 : H₁.Free G
Tactic: apply card_edgeFinset_le_extremalNumber
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Extremal.Basic (goal)
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
⊢ H₁.Free G
have refine_2 : ∀ (h : H₁ ⊑ G), H₂ ⊑ G
Tactic: contrapose h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Extremal.Basic (goal)
Goal:
V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
inst : Fintype V
inst_1 : DecidableRel G.Adj
⊢ G.IsExtremal H.Free ↔ H.Free G ∧ #G.edgeFinset = extremalNumber (Fintype.card V) H
have rw : H.Free G → (extremalNumber (Fintype.card V) H ≤ #G.edgeFinset ↔ #G.edgeFinset = extremalNumber (Fintype.card V) H)
Tactic: rw [IsExtremal, and_congr_right_iff, ← extremalNumber_le_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Extremal.Basic (goal)
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
⊢ #(G.deleteIncidenceSet v).edgeFinset ≤ extremalNumber (Fintype.card V - 1) H
have rw : Finset.card (α := Sym2 (↑{v}ᶜ : Type u_1)) (edgeFinset (induce {v}ᶜ G)) ≤
  extremalNumber (Fintype.card.{u_1} (↑{v}ᶜ : Type u_1)) H
Tactic: rw [← card_edgeFinset_induce_compl_singleton, ← @card_unique ({v} : Set V), ← card_compl_set]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Extremal.Basic (goal)
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
⊢ Finset.card (α := Sym2 (↑{v}ᶜ : Type u_1)) (edgeFinset (induce {v}ᶜ G)) ≤
    extremalNumber (Fintype.card.{u_1} (↑{v}ᶜ : Type u_1)) H
have h₁ : H.Free (β := (↑{v}ᶜ : Type u_1)) (induce {v}ᶜ G)
Tactic: apply card_edgeFinset_le_extremalNumber
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Extremal.Basic (goal)
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.Free (β := (↑{v}ᶜ : Type u_1)) (induce {v}ᶜ G)
have h₁ : ∀ (h : H.IsContained (β := (↑{v}ᶜ : Type u_1)) (induce {v}ᶜ G)), H ⊑ G
Tactic: contrapose h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Extremal.Turan (goal)
Goal:
n r : ℕ
⊢ turanGraph n r = ⊤ ↔ r = 0 ∨ n ≤ r
have simp_rw : (∀ (x x_1 : Fin n), (↑x : ℕ) % r = (↑x_1 : ℕ) % r ↔ x = x_1) ↔ r = 0 ∨ n ≤ r
Tactic: simp_rw [SimpleGraph.ext_iff, funext_iff, turanGraph, top_adj, eq_iff_iff, not_iff_not]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Extremal.Turan (goal)
Goal:
n r : ℕ
⊢ (∀ (x x_1 : Fin n), (↑x : ℕ) % r = (↑x_1 : ℕ) % r ↔ x = x_1) ↔ r = 0 ∨ n ≤ r
have refine_1 : ∀ (h : ∀ (x x_1 : Fin n), (↑x : ℕ) % r = (↑x_1 : ℕ) % r ↔ x = x_1), r = 0 ∨ n ≤ r
Tactic: refine ⟨fun h ↦ ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Extremal.Turan (goal)
Goal:
n r : ℕ
refine_1 : ∀ (h : ∀ (x x_1 : Fin n), (↑x : ℕ) % r = (↑x_1 : ℕ) % r ↔ x = x_1), r = 0 ∨ n ≤ r
⊢ (∀ (x x_1 : Fin n), (↑x : ℕ) % r = (↑x_1 : ℕ) % r ↔ x = x_1) ↔ r = 0 ∨ n ≤ r
have refine_2 : r = 0 ∨ n ≤ r → ∀ (x x_1 : Fin n), (↑x : ℕ) % r = (↑x_1 : ℕ) % r ↔ x = x_1
Tactic: refine ⟨fun h ↦ ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Extremal.Turan (goal)
Goal:
n r : ℕ
h : ∀ (x x_1 : Fin n), (↑x : ℕ) % r = (↑x_1 : ℕ) % r ↔ x = x_1
⊢ r = 0 ∨ n ≤ r
have 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
Tactic: contrapose! h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Extremal.Turan (goal)
Goal:
n r : ℕ
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
have h₁ : (↑(⟨0, sorry⟩ : Fin n) : ℕ) % r = (↑(⟨r, sorry⟩ : Fin n) : ℕ) % r ∧ (⟨0, sorry⟩ : Fin n) ≠ ⟨r, sorry⟩ ∨
  (↑(⟨0, sorry⟩ : Fin n) : ℕ) % r ≠ (↑(⟨r, sorry⟩ : Fin n) : ℕ) % r ∧ (⟨0, sorry⟩ : Fin n) = ⟨r, sorry⟩
Tactic: use ⟨0, (Nat.pos_of_ne_zero h.1).trans h.2⟩, ⟨r, h.2⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Extremal.Turan (goal)
Goal:
n r : ℕ
h : n ≤ r
a b : Fin n
⊢ (↑a : ℕ) % r = (↑b : ℕ) % r ↔ a = b
have refine_2 : (↑a : ℕ) = (↑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]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Extremal.Turan (goal)
Goal:
n r : ℕ
h : n ≤ r
a b : Fin n
refine_2 : (↑a : ℕ) = (↑b : ℕ) % r ↔ a = b
⊢ (↑a : ℕ) % r = (↑b : ℕ) % r ↔ a = b
have refine_2₁ : (↑a : ℕ) = (↑b : ℕ) ↔ 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]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Extremal.Turan (goal)
Goal:
n r : ℕ
h : n ≤ r
a b : Fin n
refine_2 : (↑a : ℕ) = (↑b : ℕ) % r ↔ a = b
refine_2₁ : (↑a : ℕ) = (↑b : ℕ) ↔ a = b
⊢ (↑a : ℕ) % r = (↑b : ℕ) % r ↔ a = b
have refine_2₂ : a = b ↔ 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]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Extremal.Turan (goal)
Goal:
n r : ℕ
hr : 0 < r
⊢ (turanGraph n r).CliqueFree (r + 1)
have rw : IsEmpty (Copy (α := Fin (r + 1)) (completeGraph (Fin (r + 1))) (turanGraph n r))
Tactic: rw [cliqueFree_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Extremal.Turan (goal)
Goal:
n r : ℕ
hr : 0 < r
⊢ IsEmpty (Copy (α := Fin (r + 1)) (completeGraph (Fin (r + 1))) (turanGraph n r))
have by_contra! : ∀ (f : Copy (α := Fin (r + 1)) (completeGraph (Fin (r + 1))) (turanGraph n r)), False
Tactic: by_contra! ⟨f⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Extremal.Turan (goal)
Goal:
n r : ℕ
hr : 0 < r
f : Copy (α := Fin (r + 1)) (completeGraph (Fin (r + 1))) (turanGraph n r)
⊢ False
have obtain : ∀ (x y : Fin (r + 1)) (d : x ≠ y)
  (c :
    (⟨(↑((f : (a : Fin (r + 1)) → Fin n) x) : ℕ) % r, sorry⟩ : Fin r) =
      ⟨(↑((f : (a : Fin (r + 1)) → Fin n) y) : ℕ) % r, sorry⟩),
  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)
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Extremal.Turan (hypothesis)
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, ⋯⟩
⊢ False
have c₁ : (↑((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
Cleared hypotheses: c
-- 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 : ℕ
hn : r ≤ Fintype.card V
hG : G.IsTuranMaximal r
h : G.CliqueFree r
⊢ False
have obtain : ∀ K ⊆ univ, ∀ (hn : #K ≤ Fintype.card V) (hG : G.IsTuranMaximal #K) (h : G.CliqueFree #K), False
Tactic: obtain ⟨K, _, rfl⟩ := exists_subset_card_eq hn
Cleared hypotheses: r, hn, hG, 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
K : Finset V
left : K ⊆ univ
hn : #K ≤ Fintype.card V
hG : G.IsTuranMaximal #K
h : G.CliqueFree #K
⊢ False
have obtain : ∀ (a b : V) (hab : a ≠ b) (hGab : ¬G.Adj a b), 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
-- 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 : ℕ
s t : V
h : G.IsTuranMaximal r
hn : ¬G.Adj s t
⊢ G.degree s = G.degree t
have h₁ : 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
Cleared hypotheses: h, 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 : ℕ
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
⊢ G.degree s = G.degree t
have 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
Tactic: contrapose! h
Cleared hypotheses: 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 : ℕ
s t : V
hn : ¬G.Adj s t
h : G.degree s ≠ G.degree t
cf : G.CliqueFree (r + 1)
⊢ ∃ (G' : SimpleGraph V) (inst_2 : DecidableRel G'.Adj), G'.CliqueFree (r + 1) ∧ #G.edgeFinset < #G'.edgeFinset
have 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
Tactic: wlog hd : G.degree t < G.degree s generalizing G t s
-- 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 : ℕ
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
⊢ ∃ (G' : SimpleGraph V) (inst_2 : DecidableRel G'.Adj), G'.CliqueFree (r + 1) ∧ #G.edgeFinset < #G'.edgeFinset
have 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
Tactic: wlog hd : G.degree t < G.degree s generalizing G t s
Cleared hypotheses: hn, h, cf
-- 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 : ℕ
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' : SimpleGraph V) (inst_2 : DecidableRel G'.Adj), G'.CliqueFree (r + 1) ∧ #G.edgeFinset < #G'.edgeFinset
have hd₁ : 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
Cleared hypotheses: hd
-- 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 : ℕ
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
⊢ ¬G.Adj t s
have 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
Tactic: rwa [adj_comm] at hn
Cleared hypotheses: hn, h, cf, this, hd
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Extremal.Turan (goal)
Goal:
V : Type u_1
inst : Fintype V
G_1 : SimpleGraph V
inst_1 : DecidableRel G_1.Adj
r : ℕ
s_1 t_1 : V
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
have right : #G.edgeFinset < #(G.replaceVertex s t).edgeFinset
Tactic: use G.replaceVertex s t, inferInstance, cf.replaceVertex s t
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Extremal.Turan (hypothesis)
Goal:
V : Type u_1
inst : Fintype V
G_1 : SimpleGraph V
inst_1 : DecidableRel G_1.Adj
r : ℕ
s_1 t_1 : V
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.edgeFinset < #(G.replaceVertex s t).edgeFinset
have this : #(G.replaceVertex s t).edgeFinset = #G.edgeFinset + G.degree s - G.degree t
Tactic: have := G.card_edgeFinset_replaceVertex_of_not_adj hn
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Extremal.Turan (goal)
Goal:
V : Type u_1
inst : Fintype V
G_1 : SimpleGraph V
inst_1 : DecidableRel G_1.Adj
r : ℕ
s_1 t_1 : V
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
w : SimpleGraph V
⊢ ∃ (G' : SimpleGraph V) (inst_3 : DecidableRel G'.Adj), G'.CliqueFree (r + 1) ∧ #G.edgeFinset < #G'.edgeFinset
have w₁ : DecidableRel (G.replaceVertex s t).Adj
Tactic: classical
  use G.replaceVertex s t, inferInstance, cf.replaceVertex s t
  have := G.card_edgeFinset_replaceVertex_of_not_adj hn
  lia
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Extremal.Turan (goal)
Goal:
V : Type u_1
inst : Fintype V
G_1 : SimpleGraph V
inst_1 : DecidableRel G_1.Adj
r : ℕ
s_1 t_1 : V
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
w : SimpleGraph V
w₁ : DecidableRel (G.replaceVertex s t).Adj
⊢ ∃ (G' : SimpleGraph V) (inst_3 : DecidableRel G'.Adj), G'.CliqueFree (r + 1) ∧ #G.edgeFinset < #G'.edgeFinset
have left : (G.replaceVertex s t).CliqueFree (r + 1)
Tactic: classical
  use G.replaceVertex s t, inferInstance, cf.replaceVertex s t
  have := G.card_edgeFinset_replaceVertex_of_not_adj hn
  lia
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Extremal.Turan (goal)
Goal:
V : Type u_1
inst : Fintype V
G_1 : SimpleGraph V
inst_1 : DecidableRel G_1.Adj
r : ℕ
s_1 t_1 : V
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
w : SimpleGraph V
w₁ : DecidableRel (G.replaceVertex s t).Adj
left : (G.replaceVertex s t).CliqueFree (r + 1)
⊢ ∃ (G' : SimpleGraph V) (inst_3 : DecidableRel G'.Adj), G'.CliqueFree (r + 1) ∧ #G.edgeFinset < #G'.edgeFinset
have right : #G.edgeFinset < #(G.replaceVertex s t).edgeFinset
Tactic: classical
  use G.replaceVertex s t, inferInstance, cf.replaceVertex s t
  have := G.card_edgeFinset_replaceVertex_of_not_adj hn
  lia
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Extremal.Turan (goal)
Goal:
V : Type u_1
inst : Fintype V
G_1 : SimpleGraph V
inst_1 : DecidableRel G_1.Adj
r : ℕ
s_1 t_1 : V
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
w : SimpleGraph V
w₁ : DecidableRel (G.replaceVertex s t).Adj
left : (G.replaceVertex s t).CliqueFree (r + 1)
right right₁ : #G.edgeFinset < #(G.replaceVertex s t).edgeFinset
⊢ ∃ (G' : SimpleGraph V) (inst_3 : DecidableRel G'.Adj), G'.CliqueFree (r + 1) ∧ #G.edgeFinset < #G'.edgeFinset
have right₂ : ∀ (this : #(G.replaceVertex s t).edgeFinset = #G.edgeFinset + G.degree s - G.degree t),
  #G.edgeFinset < #(G.replaceVertex s t).edgeFinset
Tactic: classical
  use G.replaceVertex s t, inferInstance, cf.replaceVertex s t
  have := G.card_edgeFinset_replaceVertex_of_not_adj hn
  lia
-- 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 : ℕ
s t u : V
h : G.IsTuranMaximal r
hts : ¬G.Adj t s
hsu : ¬G.Adj s u
⊢ ¬G.Adj t u
have hst : ¬G.Adj s t
Tactic: have hst : ¬G.Adj s t := fun a ↦ hts a.symm
-- 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 : ℕ
s t u : V
h : G.IsTuranMaximal r
hts : ¬G.Adj t s
hsu : ¬G.Adj s u
hst : ¬G.Adj s t
⊢ ¬G.Adj t u
have dst : G.degree s = G.degree t
Tactic: have dst := h.degree_eq_of_not_adj hst
-- 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 : ℕ
s t u : V
h : G.IsTuranMaximal r
hts : ¬G.Adj t s
hsu : ¬G.Adj s u
hst : ¬G.Adj s t
dst : G.degree s = G.degree t
⊢ ¬G.Adj t u
have dsu : G.degree s = G.degree u
Tactic: have dsu := h.degree_eq_of_not_adj hsu
-- 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 : ℕ
s t u : V
h : G.IsTuranMaximal r
hts : ¬G.Adj t s
hsu : ¬G.Adj s u
hst : ¬G.Adj s t
dst : G.degree s = G.degree t
dsu : G.degree s = G.degree u
⊢ ¬G.Adj t u
have h₁ : 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
Cleared hypotheses: h, hts, hsu, hst, dst, dsu
-- 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 : ℕ
s t u : V
h :
  G.CliqueFree (r + 1) ∧
    ∀ ⦃G' : SimpleGraph V⦄ [inst_2 : DecidableRel G'.Adj], G'.CliqueFree (r + 1) → #G'.edgeFinset ≤ #G.edgeFinset
hts : ¬G.Adj t s
hsu : ¬G.Adj s u
hst : ¬G.Adj s t
dst : G.degree s = G.degree t
dsu : G.degree s = G.degree u
⊢ ¬G.Adj t u
have contrapose! : ∀ (h : G.Adj t u) (_ : G.CliqueFree (r + 1)),
  ∃ (G' : SimpleGraph V) (inst_2 : DecidableRel G'.Adj), G'.CliqueFree (r + 1) ∧ #G.edgeFinset < #G'.edgeFinset
Tactic: contrapose! h
Cleared hypotheses: 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 : ℕ
s t u : V
hts : ¬G.Adj t s
hsu : ¬G.Adj s u
hst : ¬G.Adj s t
dst : G.degree s = G.degree t
dsu : G.degree s = G.degree u
h : G.Adj t u
cf : G.CliqueFree (r + 1)
⊢ ∃ (G' : SimpleGraph V) (inst_2 : DecidableRel G'.Adj), G'.CliqueFree (r + 1) ∧ #G.edgeFinset < #G'.edgeFinset
have right : #G.edgeFinset < #((G.replaceVertex s t).replaceVertex s u).edgeFinset
Tactic: use (G.replaceVertex s t).replaceVertex s u, inferInstance,
    (cf.replaceVertex s t).replaceVertex s u
-- 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 : ℕ
s t u : V
hts : ¬G.Adj t s
hsu : ¬G.Adj s u
hst : ¬G.Adj s t
dst : G.degree s = G.degree t
dsu : G.degree s = G.degree u
h : G.Adj t u
cf : G.CliqueFree (r + 1)
⊢ #G.edgeFinset < #((G.replaceVertex s t).replaceVertex s u).edgeFinset
have nst : s ≠ t
Tactic: have nst : s ≠ t := fun a ↦ hsu (a ▸ h)