-- Mathlib/Combinatorics/SimpleGraph/Turan.lean
/-- In a Turán-maximal graph, non-adjacent vertices have the same degree. -/
lemma degree_eq_of_not_adj (h : G.IsTuranMaximal r) (hn : ¬G.Adj s t) :
    G.degree s = G.degree t

Proof state:
case inr
V : Type u_1
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : 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 : DecidableRel G.Adj] {s t : V},
    ¬G.Adj s t →
      G.degree s ≠ G.degree t →
        G.CliqueFree (r + 1) →
          G.degree t < G.degree s → ∃ H inst_1, H.CliqueFree (r + 1) ∧ #G.edgeFinset < #H.edgeFinset
hd : G.degree s < G.degree t
⊢ ∃ H inst, H.CliqueFree (r + 1) ∧ #G.edgeFinset < #H.edgeFinset

Tactic:
exact this (by rwa [adj_comm] at hn) hd.ne' cf hd

Result:
no goals

Proof state:
case right
V : Type u_1
inst✝² : Fintype V
G✝ : SimpleGraph V
inst✝¹ : DecidableRel G✝.Adj
r : ℕ
s✝ t✝ : V
G : SimpleGraph V
inst✝ : 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
this : #(G.replaceVertex s t).edgeFinset = #G.edgeFinset + G.degree s - G.degree t
⊢ #G.edgeFinset < #(G.replaceVertex s t).edgeFinset

Tactic:
omega

Result:
no goals

Proof state:
case inr
V : Type u_1
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : 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 : DecidableRel G.Adj] {s t : V},
    ¬G.Adj s t →
      G.degree s ≠ G.degree t →
        G.CliqueFree (r + 1) →
          G.degree t < G.degree s → ∃ H inst_1, H.CliqueFree (r + 1) ∧ #G.edgeFinset < #H.edgeFinset
hd : ¬G.degree t < G.degree s
⊢ ∃ H inst, H.CliqueFree (r + 1) ∧ #G.edgeFinset < #H.edgeFinset

Tactic:
replace hd : G.degree s < G.degree t := lt_of_le_of_ne (le_of_not_lt hd) h

Result:
case inr
V : Type u_1
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : 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 : DecidableRel G.Adj] {s t : V},
    ¬G.Adj s t →
      G.degree s ≠ G.degree t →
        G.CliqueFree (r + 1) →
          G.degree t < G.degree s → ∃ H inst_1, H.CliqueFree (r + 1) ∧ #G.edgeFinset < #H.edgeFinset
hd : G.degree s < G.degree t
⊢ ∃ H inst, H.CliqueFree (r + 1) ∧ #G.edgeFinset < #H.edgeFinset

Proof state:
V : Type u_1
inst✝² : Fintype V
G✝ : SimpleGraph V
inst✝¹ : DecidableRel G✝.Adj
r : ℕ
s✝ t✝ : V
G : SimpleGraph V
inst✝ : 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
⊢ ∃ H inst, H.CliqueFree (r + 1) ∧ #G.edgeFinset < #H.edgeFinset

Tactic:
use G.replaceVertex s t, inferInstance, cf.replaceVertex s t

Result:
case right
V : Type u_1
inst✝² : Fintype V
G✝ : SimpleGraph V
inst✝¹ : DecidableRel G✝.Adj
r : ℕ
s✝ t✝ : V
G : SimpleGraph V
inst✝ : 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

Proof state:
V : Type u_1
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
r : ℕ
s t : V
h : G.IsTuranMaximal r
hn : ¬G.Adj s t
⊢ G.degree s = G.degree t

Tactic:
rw [IsTuranMaximal] at h

Result:
V : Type u_1
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
r : ℕ
s t : V
h :
  G.CliqueFree (r + 1) ∧
    ∀ (H : SimpleGraph V) [inst : DecidableRel H.Adj], H.CliqueFree (r + 1) → #H.edgeFinset ≤ #G.edgeFinset
hn : ¬G.Adj s t
⊢ G.degree s = G.degree t

Proof state:
case right
V : Type u_1
inst✝² : Fintype V
G✝ : SimpleGraph V
inst✝¹ : DecidableRel G✝.Adj
r : ℕ
s✝ t✝ : V
G : SimpleGraph V
inst✝ : 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

Tactic:
have := G.card_edgeFinset_replaceVertex_of_not_adj hn

Result:
case right
V : Type u_1
inst✝² : Fintype V
G✝ : SimpleGraph V
inst✝¹ : DecidableRel G✝.Adj
r : ℕ
s✝ t✝ : V
G : SimpleGraph V
inst✝ : 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
this : #(G.replaceVertex s t).edgeFinset = #G.edgeFinset + G.degree s - G.degree t
⊢ #G.edgeFinset < #(G.replaceVertex s t).edgeFinset

Proof state:
V : Type u_1
inst✝² : Fintype V
G✝ : SimpleGraph V
inst✝¹ : DecidableRel G✝.Adj
r : ℕ
s✝ t✝ : V
G : SimpleGraph V
inst✝ : 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
⊢ ∃ H inst, H.CliqueFree (r + 1) ∧ #G.edgeFinset < #H.edgeFinset

Tactic:
classical
use G.replaceVertex s t, inferInstance, cf.replaceVertex s t
have := G.card_edgeFinset_replaceVertex_of_not_adj hn
omega

Result:
no goals

Proof state:
V : Type u_1
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
r : ℕ
s t : V
hn : ¬G.Adj s t
h : G.degree s ≠ G.degree t
cf : G.CliqueFree (r + 1)
⊢ ∃ H inst, H.CliqueFree (r + 1) ∧ #G.edgeFinset < #H.edgeFinset

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

Result:
case inr
V : Type u_1
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : 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 : DecidableRel G.Adj] {s t : V},
    ¬G.Adj s t →
      G.degree s ≠ G.degree t →
        G.CliqueFree (r + 1) →
          G.degree t < G.degree s → ∃ H inst_1, H.CliqueFree (r + 1) ∧ #G.edgeFinset < #H.edgeFinset
hd : ¬G.degree t < G.degree s
⊢ ∃ H inst, H.CliqueFree (r + 1) ∧ #G.edgeFinset < #H.edgeFinset

V : Type u_1
inst✝² : Fintype V
G✝ : SimpleGraph V
inst✝¹ : DecidableRel G✝.Adj
r : ℕ
s✝ t✝ : V
G : SimpleGraph V
inst✝ : 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
⊢ ∃ H inst, H.CliqueFree (r + 1) ∧ #G.edgeFinset < #H.edgeFinset

Proof state:
V : Type u_1
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : 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 : DecidableRel G.Adj] {s t : V},
    ¬G.Adj s t →
      G.degree s ≠ G.degree t →
        G.CliqueFree (r + 1) →
          G.degree t < G.degree s → ∃ H inst_1, H.CliqueFree (r + 1) ∧ #G.edgeFinset < #H.edgeFinset
hd : G.degree s < G.degree t
⊢ ¬G.Adj t s

Tactic:
rwa [adj_comm] at hn

Result:
no goals

Proof state:
V : Type u_1
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
r : ℕ
s t : V
hn : ¬G.Adj s t
h : G.degree s ≠ G.degree t
⊢ G.CliqueFree (r + 1) → ∃ H inst, H.CliqueFree (r + 1) ∧ #G.edgeFinset < #H.edgeFinset

Tactic:
intro cf

Result:
V : Type u_1
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
r : ℕ
s t : V
hn : ¬G.Adj s t
h : G.degree s ≠ G.degree t
cf : G.CliqueFree (r + 1)
⊢ ∃ H inst, H.CliqueFree (r + 1) ∧ #G.edgeFinset < #H.edgeFinset

Proof state:
V : Type u_1
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
r : ℕ
s t : V
h :
  G.CliqueFree (r + 1) ∧
    ∀ (H : SimpleGraph V) [inst : DecidableRel H.Adj], H.CliqueFree (r + 1) → #H.edgeFinset ≤ #G.edgeFinset
hn : ¬G.Adj s t
⊢ G.degree s = G.degree t

Tactic:
contrapose! h

Result:
V : Type u_1
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
r : ℕ
s t : V
hn : ¬G.Adj s t
h : G.degree s ≠ G.degree t
⊢ G.CliqueFree (r + 1) → ∃ H inst, H.CliqueFree (r + 1) ∧ #G.edgeFinset < #H.edgeFinset