-- Mathlib/Combinatorics/SimpleGraph/Turan.lean
lemma exists_isTuranMaximal (hr : 0 < r):
    ∃ H : SimpleGraph V, ∃ _ : DecidableRel H.Adj, H.IsTuranMaximal r

Proof state:
V : Type u_1
inst✝ : Fintype V
r : ℕ
hr : 0 < r
⊢ ∃ H x, H.IsTuranMaximal r

Tactic:
let c := {H : SimpleGraph V | H.CliqueFree (r + 1)}

Result:
V : Type u_1
inst✝ : Fintype V
r : ℕ
hr : 0 < r
c : Set (SimpleGraph V) := {H | H.CliqueFree (r + 1)}
⊢ ∃ H x, H.IsTuranMaximal r

Proof state:
case intro.intro
V : Type u_1
inst✝ : Fintype V
r : ℕ
hr : 0 < r
c : Set (SimpleGraph V) := {H | H.CliqueFree (r + 1)}
cn : c.toFinset.Nonempty
S : SimpleGraph V
Sm : S ∈ c.toFinset
Sl : ∀ x' ∈ c.toFinset, #x'.edgeFinset ≤ #S.edgeFinset
⊢ ∃ H x, H.IsTuranMaximal r

Tactic:
use S, inferInstance

Result:
case h
V : Type u_1
inst✝ : Fintype V
r : ℕ
hr : 0 < r
c : Set (SimpleGraph V) := {H | H.CliqueFree (r + 1)}
cn : c.toFinset.Nonempty
S : SimpleGraph V
Sm : S ∈ c.toFinset
Sl : ∀ x' ∈ c.toFinset, #x'.edgeFinset ≤ #S.edgeFinset
⊢ S.IsTuranMaximal r

Proof state:
V : Type u_1
inst✝ : Fintype V
r : ℕ
hr : 0 < r
c : Set (SimpleGraph V) := {H | H.CliqueFree (r + 1)}
⊢ 2 ≤ r + 1

Tactic:
omega

Result:
no goals

Proof state:
V : Type u_1
inst✝ : Fintype V
r : ℕ
hr : 0 < r
c : Set (SimpleGraph V) := {H | H.CliqueFree (r + 1)}
⊢ ⊥.CliqueFree (r + 1)

Tactic:
exact cliqueFree_bot (by omega)

Result:
no goals

Proof state:
V : Type u_1
inst✝ : Fintype V
r : ℕ
hr : 0 < r
c : Set (SimpleGraph V) := {H | H.CliqueFree (r + 1)}
⊢ ⊥ ∈ c.toFinset

Tactic:
simp only [Set.toFinset_setOf, mem_filter, mem_univ, true_and, c]

Result:
V : Type u_1
inst✝ : Fintype V
r : ℕ
hr : 0 < r
c : Set (SimpleGraph V) := {H | H.CliqueFree (r + 1)}
⊢ ⊥.CliqueFree (r + 1)

Proof state:
case pos
V : Type u_1
inst✝ : Fintype V
r : ℕ
hr : 0 < r
c : Set (SimpleGraph V) := {H | H.CliqueFree (r + 1)}
cn : c.toFinset.Nonempty
S : SimpleGraph V
Sm : S ∈ c
Sl : ∀ x' ∈ c.toFinset, #x'.edgeFinset ≤ #S.edgeFinset
I : SimpleGraph V
x✝ : DecidableRel I.Adj
cf : I.CliqueFree (r + 1)
Im : I ∈ c.toFinset
⊢ #I.edgeFinset ≤ #S.edgeFinset

Tactic:
convert Sl I Im

Result:
no goals

Proof state:
V : Type u_1
inst✝ : Fintype V
r : ℕ
hr : 0 < r
c : Set (SimpleGraph V) := {H | H.CliqueFree (r + 1)}
⊢ ∃ H x, H.IsTuranMaximal r

Tactic:
have cn : c.toFinset.Nonempty := ⟨⊥, by
  simp only [Set.toFinset_setOf, mem_filter, mem_univ, true_and, c]
  exact cliqueFree_bot (by omega)⟩

Result:
V : Type u_1
inst✝ : Fintype V
r : ℕ
hr : 0 < r
c : Set (SimpleGraph V) := {H | H.CliqueFree (r + 1)}
cn : c.toFinset.Nonempty
⊢ ∃ H x, H.IsTuranMaximal r

Proof state:
case h
V : Type u_1
inst✝ : Fintype V
r : ℕ
hr : 0 < r
c : Set (SimpleGraph V) := {H | H.CliqueFree (r + 1)}
cn : c.toFinset.Nonempty
S : SimpleGraph V
Sm : S ∈ c
Sl : ∀ x' ∈ c.toFinset, #x'.edgeFinset ≤ #S.edgeFinset
⊢ S.IsTuranMaximal r

Tactic:
refine ⟨Sm, fun I _ cf ↦ ?_⟩

Result:
case h
V : Type u_1
inst✝ : Fintype V
r : ℕ
hr : 0 < r
c : Set (SimpleGraph V) := {H | H.CliqueFree (r + 1)}
cn : c.toFinset.Nonempty
S : SimpleGraph V
Sm : S ∈ c
Sl : ∀ x' ∈ c.toFinset, #x'.edgeFinset ≤ #S.edgeFinset
I : SimpleGraph V
x✝ : DecidableRel I.Adj
cf : I.CliqueFree (r + 1)
⊢ #I.edgeFinset ≤ #S.edgeFinset

Proof state:
case h
V : Type u_1
inst✝ : Fintype V
r : ℕ
hr : 0 < r
c : Set (SimpleGraph V) := {H | H.CliqueFree (r + 1)}
cn : c.toFinset.Nonempty
S : SimpleGraph V
Sm : S ∈ c
Sl : ∀ x' ∈ c.toFinset, #x'.edgeFinset ≤ #S.edgeFinset
I : SimpleGraph V
x✝ : DecidableRel I.Adj
cf : I.CliqueFree (r + 1)
⊢ #I.edgeFinset ≤ #S.edgeFinset

Tactic:
by_cases Im : I ∈ c.toFinset

Result:
case pos
V : Type u_1
inst✝ : Fintype V
r : ℕ
hr : 0 < r
c : Set (SimpleGraph V) := {H | H.CliqueFree (r + 1)}
cn : c.toFinset.Nonempty
S : SimpleGraph V
Sm : S ∈ c
Sl : ∀ x' ∈ c.toFinset, #x'.edgeFinset ≤ #S.edgeFinset
I : SimpleGraph V
x✝ : DecidableRel I.Adj
cf : I.CliqueFree (r + 1)
Im : I ∈ c.toFinset
⊢ #I.edgeFinset ≤ #S.edgeFinset

case neg
V : Type u_1
inst✝ : Fintype V
r : ℕ
hr : 0 < r
c : Set (SimpleGraph V) := {H | H.CliqueFree (r + 1)}
cn : c.toFinset.Nonempty
S : SimpleGraph V
Sm : S ∈ c
Sl : ∀ x' ∈ c.toFinset, #x'.edgeFinset ≤ #S.edgeFinset
I : SimpleGraph V
x✝ : DecidableRel I.Adj
cf : I.CliqueFree (r + 1)
Im : I ∉ c.toFinset
⊢ #I.edgeFinset ≤ #S.edgeFinset

Proof state:
case h
V : Type u_1
inst✝ : Fintype V
r : ℕ
hr : 0 < r
c : Set (SimpleGraph V) := {H | H.CliqueFree (r + 1)}
cn : c.toFinset.Nonempty
S : SimpleGraph V
Sm : S ∈ c.toFinset
Sl : ∀ x' ∈ c.toFinset, #x'.edgeFinset ≤ #S.edgeFinset
⊢ S.IsTuranMaximal r

Tactic:
rw [Set.mem_toFinset] at Sm

Result:
case h
V : Type u_1
inst✝ : Fintype V
r : ℕ
hr : 0 < r
c : Set (SimpleGraph V) := {H | H.CliqueFree (r + 1)}
cn : c.toFinset.Nonempty
S : SimpleGraph V
Sm : S ∈ c
Sl : ∀ x' ∈ c.toFinset, #x'.edgeFinset ≤ #S.edgeFinset
⊢ S.IsTuranMaximal r

Proof state:
case neg
V : Type u_1
inst✝ : Fintype V
r : ℕ
hr : 0 < r
c : Set (SimpleGraph V) := {H | H.CliqueFree (r + 1)}
cn : c.toFinset.Nonempty
S : SimpleGraph V
Sm : S ∈ c
Sl : ∀ x' ∈ c.toFinset, #x'.edgeFinset ≤ #S.edgeFinset
I : SimpleGraph V
x✝ : DecidableRel I.Adj
cf : I.CliqueFree (r + 1)
Im : I ∉ c.toFinset
⊢ #I.edgeFinset ≤ #S.edgeFinset

Tactic:
rw [Set.mem_toFinset] at Im

Result:
case neg
V : Type u_1
inst✝ : Fintype V
r : ℕ
hr : 0 < r
c : Set (SimpleGraph V) := {H | H.CliqueFree (r + 1)}
cn : c.toFinset.Nonempty
S : SimpleGraph V
Sm : S ∈ c
Sl : ∀ x' ∈ c.toFinset, #x'.edgeFinset ≤ #S.edgeFinset
I : SimpleGraph V
x✝ : DecidableRel I.Adj
cf : I.CliqueFree (r + 1)
Im : I ∉ c
⊢ #I.edgeFinset ≤ #S.edgeFinset

Proof state:
case neg
V : Type u_1
inst✝ : Fintype V
r : ℕ
hr : 0 < r
c : Set (SimpleGraph V) := {H | H.CliqueFree (r + 1)}
cn : c.toFinset.Nonempty
S : SimpleGraph V
Sm : S ∈ c
Sl : ∀ x' ∈ c.toFinset, #x'.edgeFinset ≤ #S.edgeFinset
I : SimpleGraph V
x✝ : DecidableRel I.Adj
cf : I.CliqueFree (r + 1)
Im : I ∉ c
⊢ #I.edgeFinset ≤ #S.edgeFinset

Tactic:
contradiction

Result:
no goals