-- Mathlib/Combinatorics/SimpleGraph/Clique.lean
theorem CliqueFree.replaceVertex [DecidableEq α] (h : G.CliqueFree n) (s t : α) :
    (G.replaceVertex s t).CliqueFree n

Proof state:
α : Type u_1
G : SimpleGraph α
n : ℕ
inst✝ : DecidableEq α
s t : α
h : ¬(G.replaceVertex s t).CliqueFree n
⊢ ¬G.CliqueFree n

Tactic:
obtain ⟨φ, hφ⟩ := topEmbeddingOfNotCliqueFree h

Result:
case mk
α : Type u_1
G : SimpleGraph α
n : ℕ
inst✝ : DecidableEq α
s t : α
h : ¬(G.replaceVertex s t).CliqueFree n
φ : Fin n ↪ α
hφ : ∀ {a b : Fin n}, (G.replaceVertex s t).Adj (φ a) (φ b) ↔ ⊤.Adj a b
⊢ ¬G.CliqueFree n

Proof state:
case pos.intro
α : Type u_1
G : SimpleGraph α
n : ℕ
inst✝ : DecidableEq α
s t : α
h : ¬(G.replaceVertex s t).CliqueFree n
φ : Fin n ↪ α
hφ : ∀ {a b : Fin n}, (G.replaceVertex s t).Adj (φ a) (φ b) ↔ ⊤.Adj a b
x : Fin n
hx : φ x = t
y : Fin n
hy : φ y = s
e : (G.replaceVertex s t).Adj (φ x) (φ y) ↔ ⊤.Adj x y
⊢ Nonempty (⊤ ↪g G)

Tactic:
simp_rw [hx, hy, adj_comm, not_adj_replaceVertex_same, top_adj, false_iff, not_ne_iff] at e

Result:
case pos.intro
α : Type u_1
G : SimpleGraph α
n : ℕ
inst✝ : DecidableEq α
s t : α
h : ¬(G.replaceVertex s t).CliqueFree n
φ : Fin n ↪ α
hφ : ∀ {a b : Fin n}, (G.replaceVertex s t).Adj (φ a) (φ b) ↔ ⊤.Adj a b
x : Fin n
hx : φ x = t
y : Fin n
hy : φ y = s
e : x = y
⊢ Nonempty (⊤ ↪g G)

Proof state:
case map_rel_iff'
α : Type u_1
G : SimpleGraph α
n : ℕ
inst✝ : DecidableEq α
s t : α
h : ¬(G.replaceVertex s t).CliqueFree n
φ : Fin n ↪ α
hφ :
  ∀ {a b : Fin n},
    { Adj := fun v w => if v = t then if w = t then False else G.Adj s w else if w = t then G.Adj v s else G.Adj v w,
            symm := ⋯, loopless := ⋯ }.Adj
        (φ a) (φ b) ↔
      ⊤.Adj a b
x : Fin n
hx : φ x = t
ms : s ∉ Set.range ⇑φ
a b : Fin n
⊢ G.Adj ((φ.setValue x s) a) ((φ.setValue x s) b) ↔ ⊤.Adj a b

Tactic:
simp only [Embedding.coeFn_mk, Embedding.setValue, not_exists.mp ms, ite_false]

Result:
case map_rel_iff'
α : Type u_1
G : SimpleGraph α
n : ℕ
inst✝ : DecidableEq α
s t : α
h : ¬(G.replaceVertex s t).CliqueFree n
φ : Fin n ↪ α
hφ :
  ∀ {a b : Fin n},
    { Adj := fun v w => if v = t then if w = t then False else G.Adj s w else if w = t then G.Adj v s else G.Adj v w,
            symm := ⋯, loopless := ⋯ }.Adj
        (φ a) (φ b) ↔
      ⊤.Adj a b
x : Fin n
hx : φ x = t
ms : s ∉ Set.range ⇑φ
a b : Fin n
⊢ G.Adj (if a = x then s else φ a) (if b = x then s else φ b) ↔ ⊤.Adj a b

Proof state:
case pos.intro
α : Type u_1
G : SimpleGraph α
n : ℕ
inst✝ : DecidableEq α
s t : α
h : ¬(G.replaceVertex s t).CliqueFree n
φ : Fin n ↪ α
hφ : ∀ {a b : Fin n}, (G.replaceVertex s t).Adj (φ a) (φ b) ↔ ⊤.Adj a b
x : Fin n
hx : φ x = t
y : Fin n
hy : φ y = s
⊢ Nonempty (⊤ ↪g G)

Tactic:
have e := @hφ x y

Result:
case pos.intro
α : Type u_1
G : SimpleGraph α
n : ℕ
inst✝ : DecidableEq α
s t : α
h : ¬(G.replaceVertex s t).CliqueFree n
φ : Fin n ↪ α
hφ : ∀ {a b : Fin n}, (G.replaceVertex s t).Adj (φ a) (φ b) ↔ ⊤.Adj a b
x : Fin n
hx : φ x = t
y : Fin n
hy : φ y = s
e : (G.replaceVertex s t).Adj (φ x) (φ y) ↔ ⊤.Adj x y
⊢ Nonempty (⊤ ↪g G)

Proof state:
α : Type u_1
G : SimpleGraph α
n : ℕ
inst✝ : DecidableEq α
h : G.CliqueFree n
s t : α
⊢ (G.replaceVertex s t).CliqueFree n

Tactic:
contrapose h

Result:
α : Type u_1
G : SimpleGraph α
n : ℕ
inst✝ : DecidableEq α
s t : α
h : ¬(G.replaceVertex s t).CliqueFree n
⊢ ¬G.CliqueFree n

Proof state:
case pos.intro
α : Type u_1
G : SimpleGraph α
n : ℕ
inst✝ : DecidableEq α
s t : α
h : ¬(G.replaceVertex s t).CliqueFree n
φ : Fin n ↪ α
hφ : ∀ {a b : Fin n}, (G.replaceVertex s t).Adj (φ a) (φ b) ↔ ⊤.Adj a b
x : Fin n
hx : φ x = t
y : Fin n
hy : φ y = s
e : x = y
⊢ Nonempty (⊤ ↪g G)

Tactic:
rwa [← hx, e, hy, replaceVertex_self, not_cliqueFree_iff] at h

Result:
no goals

Proof state:
case map_rel_iff'
α : Type u_1
G : SimpleGraph α
n : ℕ
inst✝ : DecidableEq α
s t : α
h : ¬(G.replaceVertex s t).CliqueFree n
φ : Fin n ↪ α
hφ :
  ∀ {a b : Fin n},
    { Adj := fun v w => if v = t then if w = t then False else G.Adj s w else if w = t then G.Adj v s else G.Adj v w,
            symm := ⋯, loopless := ⋯ }.Adj
        (φ a) (φ b) ↔
      ⊤.Adj a b
x : Fin n
hx : φ x = t
ms : s ∉ Set.range ⇑φ
a b : Fin n
⊢ (if a = x then if b = x then G.Adj s s else G.Adj s (φ b) else if b = x then G.Adj (φ a) s else G.Adj (φ a) (φ b)) ↔
    ⊤.Adj a b

Tactic:
convert @hφ a b <;> simp only [← φ.apply_eq_iff_eq, SimpleGraph.irrefl, hx]

Result:
no goals

Proof state:
case neg
α : Type u_1
G : SimpleGraph α
n : ℕ
inst✝ : DecidableEq α
s t : α
h : ¬(G.replaceVertex s t).CliqueFree n
φ : Fin n ↪ α
hφ : ∀ {a b : Fin n}, (G.replaceVertex s t).Adj (φ a) (φ b) ↔ ⊤.Adj a b
mt : t ∉ Set.range ⇑φ
⊢ Nonempty (⊤ ↪g G)

Tactic:
use φ

Result:
case map_rel_iff'
α : Type u_1
G : SimpleGraph α
n : ℕ
inst✝ : DecidableEq α
s t : α
h : ¬(G.replaceVertex s t).CliqueFree n
φ : Fin n ↪ α
hφ : ∀ {a b : Fin n}, (G.replaceVertex s t).Adj (φ a) (φ b) ↔ ⊤.Adj a b
mt : t ∉ Set.range ⇑φ
⊢ ∀ {a b : Fin n}, G.Adj (φ a) (φ b) ↔ ⊤.Adj a b