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

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}, G.Adj (φ a) (φ b) ↔ ⊤.Adj a b
mt : ∀ (x : Fin n), φ x ≠ t
⊢ ∀ {a b : Fin n}, G.Adj (φ a) (φ b) ↔ ⊤.Adj a b

Tactic:
exact hφ

Result:
no goals

Proof state:
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
⊢ Nonempty (⊤ ↪g G)

Tactic:
by_cases mt : t ∈ Set.range φ

Result:
case pos
α : 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)

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)

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}, (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

Tactic:
simp_rw [Set.mem_range, not_exists, ← ne_eq] at mt

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 : ∀ (x : Fin n), φ x ≠ t
⊢ ∀ {a b : Fin n}, G.Adj (φ a) (φ b) ↔ ⊤.Adj a b

Proof state:
case pos
α : 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:
obtain ⟨x, hx⟩ := mt

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
⊢ Nonempty (⊤ ↪g G)

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
⊢ Nonempty (⊤ ↪g G)

Tactic:
by_cases ms : s ∈ Set.range φ

Result:
case pos
α : 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
ms : s ∈ Set.range ⇑φ
⊢ Nonempty (⊤ ↪g G)

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
x : Fin n
hx : φ x = t
ms : s ∉ Set.range ⇑φ
⊢ 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:
intro a b

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 ((φ.setValue x s) a) ((φ.setValue x s) b) ↔ ⊤.Adj a b

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},
    { 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 ⇑φ
⊢ Nonempty (⊤ ↪g G)

Tactic:
use φ.setValue x s

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 ((φ.setValue x s) a) ((φ.setValue x s) b) ↔ ⊤.Adj a b

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
x : Fin n
hx : φ x = t
ms : s ∉ Set.range ⇑φ
⊢ Nonempty (⊤ ↪g G)

Tactic:
unfold replaceVertex at hφ

Result:
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},
    { 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 ⇑φ
⊢ Nonempty (⊤ ↪g G)

Proof state:
case pos
α : 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
ms : s ∈ Set.range ⇑φ
⊢ Nonempty (⊤ ↪g G)

Tactic:
obtain ⟨y, hy⟩ := ms

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
⊢ Nonempty (⊤ ↪g G)

Proof state:
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

Tactic:
rw [not_cliqueFree_iff]

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
⊢ 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}, (G.replaceVertex s t).Adj (φ a) (φ b) ↔ ⊤.Adj a b
mt : ∀ (x : Fin n), φ x ≠ t
⊢ ∀ {a b : Fin n}, G.Adj (φ a) (φ b) ↔ ⊤.Adj a b

Tactic:
conv at hφ => enter [a, b]; rw [G.adj_replaceVertex_iff_of_ne _ (mt a) (mt b)]

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.Adj (φ a) (φ b) ↔ ⊤.Adj a b
mt : ∀ (x : Fin n), φ x ≠ t
⊢ ∀ {a b : Fin n}, G.Adj (φ a) (φ b) ↔ ⊤.Adj a b