-- Mathlib/Combinatorics/SimpleGraph/Turan.lean
lemma card_parts_le [DecidableEq V] : #h.finpartition.parts ≤ r

Proof state:
V : Type u_1
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
r : ℕ
h : G.IsTuranMaximal r
inst✝ : DecidableEq V
l : r < #h.finpartition.parts
z : Finset V
hz : Set.BijOn h.finpartition.part ↑z ↑h.finpartition.parts
v : V
hv : v ∈ ↑z
w : V
hw : w ∈ ↑z
hn : v ≠ w
⊢ G.Adj v w

Tactic:
contrapose! hn

Result:
V : Type u_1
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
r : ℕ
h : G.IsTuranMaximal r
inst✝ : DecidableEq V
l : r < #h.finpartition.parts
z : Finset V
hz : Set.BijOn h.finpartition.part ↑z ↑h.finpartition.parts
v : V
hv : v ∈ ↑z
w : V
hw : w ∈ ↑z
hn : ¬G.Adj v w
⊢ v = w

Proof state:
case intro.intro
V : Type u_1
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
r : ℕ
h : G.IsTuranMaximal r
inst✝ : DecidableEq V
l : r < #h.finpartition.parts
z : Finset V
hz : Set.BijOn h.finpartition.part ↑z ↑h.finpartition.parts
⊢ False

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

Result:
case intro.intro
V : Type u_1
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
r : ℕ
h : G.IsTuranMaximal r
inst✝ : DecidableEq V
l : r < #h.finpartition.parts
z : Finset V
hz : Set.BijOn h.finpartition.part ↑z ↑h.finpartition.parts
ncf : ¬G.CliqueFree #z
⊢ False

Proof state:
case intro.intro
V : Type u_1
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
r : ℕ
h : G.IsTuranMaximal r
inst✝ : DecidableEq V
l : r < #h.finpartition.parts
z : Finset V
hz : Set.BijOn h.finpartition.part ↑z ↑h.finpartition.parts
ncf : ¬G.CliqueFree #z
⊢ False

Tactic:
rw [Finset.card_eq_of_equiv hz.equiv] at ncf

Result:
case intro.intro
V : Type u_1
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
r : ℕ
h : G.IsTuranMaximal r
inst✝ : DecidableEq V
l : r < #h.finpartition.parts
z : Finset V
hz : Set.BijOn h.finpartition.part ↑z ↑h.finpartition.parts
ncf : ¬G.CliqueFree #h.finpartition.parts
⊢ False

Proof state:
V : Type u_1
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
r : ℕ
h : G.IsTuranMaximal r
inst✝ : DecidableEq V
⊢ #h.finpartition.parts ≤ r

Tactic:
by_contra! l

Result:
V : Type u_1
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
r : ℕ
h : G.IsTuranMaximal r
inst✝ : DecidableEq V
l : r < #h.finpartition.parts
⊢ False

Proof state:
V : Type u_1
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
r : ℕ
h : G.IsTuranMaximal r
inst✝ : DecidableEq V
l : r < #h.finpartition.parts
z : Finset V
hz : Set.BijOn h.finpartition.part ↑z ↑h.finpartition.parts
v : V
hv : v ∈ ↑z
w : V
hw : w ∈ ↑z
hn : ¬G.Adj v w
⊢ h.finpartition.part v = h.finpartition.part w

Tactic:
rwa [← h.not_adj_iff_part_eq]

Result:
no goals

Proof state:
V : Type u_1
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
r : ℕ
h : G.IsTuranMaximal r
inst✝ : DecidableEq V
l : r < #h.finpartition.parts
z : Finset V
hz : Set.BijOn h.finpartition.part ↑z ↑h.finpartition.parts
⊢ ¬G.CliqueFree #z

Tactic:
refine IsNClique.not_cliqueFree ⟨fun v hv w hw hn ↦ ?_, rfl⟩

Result:
V : Type u_1
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
r : ℕ
h : G.IsTuranMaximal r
inst✝ : DecidableEq V
l : r < #h.finpartition.parts
z : Finset V
hz : Set.BijOn h.finpartition.part ↑z ↑h.finpartition.parts
v : V
hv : v ∈ ↑z
w : V
hw : w ∈ ↑z
hn : v ≠ w
⊢ G.Adj v w

Proof state:
V : Type u_1
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
r : ℕ
h : G.IsTuranMaximal r
inst✝ : DecidableEq V
l : r < #h.finpartition.parts
z : Finset V
hz : Set.BijOn h.finpartition.part ↑z ↑h.finpartition.parts
v : V
hv : v ∈ ↑z
w : V
hw : w ∈ ↑z
hn : ¬G.Adj v w
⊢ v = w

Tactic:
exact hz.injOn hv hw (by rwa [← h.not_adj_iff_part_eq])

Result:
no goals

Proof state:
case intro.intro
V : Type u_1
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
r : ℕ
h : G.IsTuranMaximal r
inst✝ : DecidableEq V
l : r < #h.finpartition.parts
z : Finset V
hz : Set.BijOn h.finpartition.part ↑z ↑h.finpartition.parts
ncf : ¬G.CliqueFree #h.finpartition.parts
⊢ False

Tactic:
exact absurd (h.1.mono (Nat.succ_le_of_lt l)) ncf

Result:
no goals

Proof state:
V : Type u_1
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
r : ℕ
h : G.IsTuranMaximal r
inst✝ : DecidableEq V
l : r < #h.finpartition.parts
⊢ False

Tactic:
obtain ⟨z, -, hz⟩ := h.finpartition.exists_subset_part_bijOn

Result:
case intro.intro
V : Type u_1
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
r : ℕ
h : G.IsTuranMaximal r
inst✝ : DecidableEq V
l : r < #h.finpartition.parts
z : Finset V
hz : Set.BijOn h.finpartition.part ↑z ↑h.finpartition.parts
⊢ False