-- Mathlib/Combinatorics/SimpleGraph/Clique.lean
theorem CliqueFree.sup_edge (h : G.CliqueFree n) (v w : α) :
    (G ⊔ edge v w).CliqueFree (n + 1)

Proof state:
case map_rel_iff'
α : Type u_1
G : SimpleGraph α
n : ℕ
v w : α
h : ¬(G ⊔ edge v w).CliqueFree (n + 1)
f : Fin (n + 1) ↪ α
ha : ∀ {a b : Fin (n + 1)}, (G ⊔ edge v w).Adj (f a) (f b) ↔ ¬a = b
x : Fin (n + 1)
hx : f x = w
a b : Fin n
hs : (G ⊔ edge v w).Adj (f (x.succAbove a)) (f (x.succAbove b)) ↔ ¬x.succAbove a = x.succAbove b
⊢ G.Adj (f (x.succAbove a)) (f (x.succAbove b)) ↔ a ≠ b

Tactic:
have ia : w ≠ f (x.succAbove a) :=
  (hx ▸ f.apply_eq_iff_eq x (x.succAbove a)).ne.mpr (x.succAbove_ne a).symm

Result:
case map_rel_iff'
α : Type u_1
G : SimpleGraph α
n : ℕ
v w : α
h : ¬(G ⊔ edge v w).CliqueFree (n + 1)
f : Fin (n + 1) ↪ α
ha : ∀ {a b : Fin (n + 1)}, (G ⊔ edge v w).Adj (f a) (f b) ↔ ¬a = b
x : Fin (n + 1)
hx : f x = w
a b : Fin n
hs : (G ⊔ edge v w).Adj (f (x.succAbove a)) (f (x.succAbove b)) ↔ ¬x.succAbove a = x.succAbove b
ia : w ≠ f (x.succAbove a)
⊢ G.Adj (f (x.succAbove a)) (f (x.succAbove b)) ↔ a ≠ b

Proof state:
α : Type u_1
G : SimpleGraph α
n : ℕ
v w : α
h : ¬(G ⊔ edge v w).CliqueFree (n + 1)
⊢ ¬G.CliqueFree n

Tactic:
obtain ⟨f, ha⟩ := topEmbeddingOfNotCliqueFree h

Result:
case mk
α : Type u_1
G : SimpleGraph α
n : ℕ
v w : α
h : ¬(G ⊔ edge v w).CliqueFree (n + 1)
f : Fin (n + 1) ↪ α
ha : ∀ {a b : Fin (n + 1)}, (G ⊔ edge v w).Adj (f a) (f b) ↔ ⊤.Adj a b
⊢ ¬G.CliqueFree n

Proof state:
case map_rel_iff'
α : Type u_1
G : SimpleGraph α
n : ℕ
v w : α
h : ¬(G ⊔ edge v w).CliqueFree (n + 1)
f : Fin (n + 1) ↪ α
ha : ∀ {a b : Fin (n + 1)}, (G ⊔ edge v w).Adj (f a) (f b) ↔ ¬a = b
mw : w ∉ Set.range ⇑f
a b : Fin n
⊢ G.Adj ({ toFun := ⇑f ∘ ⇑(Fin.succEmb n), inj' := ⋯ } a) ({ toFun := ⇑f ∘ ⇑(Fin.succEmb n), inj' := ⋯ } b) ↔ ⊤.Adj a b

Tactic:
simp only [Fin.val_succEmb, Embedding.coeFn_mk, comp_apply, top_adj]

Result:
case map_rel_iff'
α : Type u_1
G : SimpleGraph α
n : ℕ
v w : α
h : ¬(G ⊔ edge v w).CliqueFree (n + 1)
f : Fin (n + 1) ↪ α
ha : ∀ {a b : Fin (n + 1)}, (G ⊔ edge v w).Adj (f a) (f b) ↔ ¬a = b
mw : w ∉ Set.range ⇑f
a b : Fin n
⊢ G.Adj (f a.succ) (f b.succ) ↔ a ≠ b

Proof state:
case map_rel_iff'
α : Type u_1
G : SimpleGraph α
n : ℕ
v w : α
h : ¬(G ⊔ edge v w).CliqueFree (n + 1)
f : Fin (n + 1) ↪ α
ha : ∀ {a b : Fin (n + 1)}, (G ⊔ edge v w).Adj (f a) (f b) ↔ ¬a = b
mw : w ∉ Set.range ⇑f
a b : Fin n
ia : f a.succ ≠ w
ib : f b.succ ≠ w
hs : G.Adj (f a.succ) (f b.succ) ↔ ¬a.succ = b.succ
⊢ G.Adj (f a.succ) (f b.succ) ↔ a ≠ b

Tactic:
rw [hs, Fin.succ_inj]

Result:
no goals

Proof state:
case map_rel_iff'
α : Type u_1
G : SimpleGraph α
n : ℕ
v w : α
h : ¬(G ⊔ edge v w).CliqueFree (n + 1)
f : Fin (n + 1) ↪ α
ha : ∀ {a b : Fin (n + 1)}, (G ⊔ edge v w).Adj (f a) (f b) ↔ ¬a = b
mw : w ∉ Set.range ⇑f
a b : Fin n
hs : (G ⊔ edge v w).Adj (f a.succ) (f b.succ) ↔ ¬a.succ = b.succ
ia : f a.succ ≠ w
⊢ G.Adj (f a.succ) (f b.succ) ↔ a ≠ b

Tactic:
have ib : f b.succ ≠ w := by simp_all

Result:
case map_rel_iff'
α : Type u_1
G : SimpleGraph α
n : ℕ
v w : α
h : ¬(G ⊔ edge v w).CliqueFree (n + 1)
f : Fin (n + 1) ↪ α
ha : ∀ {a b : Fin (n + 1)}, (G ⊔ edge v w).Adj (f a) (f b) ↔ ¬a = b
mw : w ∉ Set.range ⇑f
a b : Fin n
hs : (G ⊔ edge v w).Adj (f a.succ) (f b.succ) ↔ ¬a.succ = b.succ
ia : f a.succ ≠ w
ib : f b.succ ≠ w
⊢ G.Adj (f a.succ) (f b.succ) ↔ a ≠ b

Proof state:
case map_rel_iff'
α : Type u_1
G : SimpleGraph α
n : ℕ
v w : α
h : ¬(G ⊔ edge v w).CliqueFree (n + 1)
f : Fin (n + 1) ↪ α
ha : ∀ {a b : Fin (n + 1)}, (G ⊔ edge v w).Adj (f a) (f b) ↔ ¬a = b
x : Fin (n + 1)
hx : f x = w
a b : Fin n
ia : w ≠ f (x.succAbove a)
ib : w ≠ f (x.succAbove b)
hs : G.Adj (f (x.succAbove a)) (f (x.succAbove b)) ↔ ¬x.succAbove a = x.succAbove b
⊢ G.Adj (f (x.succAbove a)) (f (x.succAbove b)) ↔ a ≠ b

Tactic:
rw [hs, Fin.succAbove_right_inj]

Result:
no goals

Proof state:
case map_rel_iff'
α : Type u_1
G : SimpleGraph α
n : ℕ
v w : α
h : ¬(G ⊔ edge v w).CliqueFree (n + 1)
f : Fin (n + 1) ↪ α
ha : ∀ {a b : Fin (n + 1)}, (G ⊔ edge v w).Adj (f a) (f b) ↔ ¬a = b
mw : w ∉ Set.range ⇑f
⊢ ∀ {a b : Fin n},
    G.Adj ({ toFun := ⇑f ∘ ⇑(Fin.succEmb n), inj' := ⋯ } a) ({ toFun := ⇑f ∘ ⇑(Fin.succEmb n), inj' := ⋯ } b) ↔
      ⊤.Adj a b

Tactic:
intro a b

Result:
case map_rel_iff'
α : Type u_1
G : SimpleGraph α
n : ℕ
v w : α
h : ¬(G ⊔ edge v w).CliqueFree (n + 1)
f : Fin (n + 1) ↪ α
ha : ∀ {a b : Fin (n + 1)}, (G ⊔ edge v w).Adj (f a) (f b) ↔ ¬a = b
mw : w ∉ Set.range ⇑f
a b : Fin n
⊢ G.Adj ({ toFun := ⇑f ∘ ⇑(Fin.succEmb n), inj' := ⋯ } a) ({ toFun := ⇑f ∘ ⇑(Fin.succEmb n), inj' := ⋯ } b) ↔ ⊤.Adj a b

Proof state:
α : Type u_1
G : SimpleGraph α
n : ℕ
h : G.CliqueFree n
v w : α
⊢ (G ⊔ edge v w).CliqueFree (n + 1)

Tactic:
contrapose h

Result:
α : Type u_1
G : SimpleGraph α
n : ℕ
v w : α
h : ¬(G ⊔ edge v w).CliqueFree (n + 1)
⊢ ¬G.CliqueFree n

Proof state:
α : Type u_1
G : SimpleGraph α
n : ℕ
v w : α
h : ¬(G ⊔ edge v w).CliqueFree (n + 1)
f : Fin (n + 1) ↪ α
ha : ∀ {a b : Fin (n + 1)}, (G ⊔ edge v w).Adj (f a) (f b) ↔ ¬a = b
mw : w ∉ Set.range ⇑f
a b : Fin n
hs : (G ⊔ edge v w).Adj (f a.succ) (f b.succ) ↔ ¬a.succ = b.succ
ia : f a.succ ≠ w
⊢ f b.succ ≠ w

Tactic:
simp_all

Result:
no goals

Proof state:
case pos
α : Type u_1
G : SimpleGraph α
n : ℕ
v w : α
h : ¬(G ⊔ edge v w).CliqueFree (n + 1)
f : Fin (n + 1) ↪ α
ha : ∀ {a b : Fin (n + 1)}, (G ⊔ edge v w).Adj (f a) (f b) ↔ ¬a = b
mw : w ∈ Set.range ⇑f
⊢ Nonempty (⊤ ↪g G)

Tactic:
obtain ⟨x, hx⟩ := mw

Result:
case pos.intro
α : Type u_1
G : SimpleGraph α
n : ℕ
v w : α
h : ¬(G ⊔ edge v w).CliqueFree (n + 1)
f : Fin (n + 1) ↪ α
ha : ∀ {a b : Fin (n + 1)}, (G ⊔ edge v w).Adj (f a) (f b) ↔ ¬a = b
x : Fin (n + 1)
hx : f x = w
⊢ Nonempty (⊤ ↪g G)

Proof state:
case map_rel_iff'
α : Type u_1
G : SimpleGraph α
n : ℕ
v w : α
h : ¬(G ⊔ edge v w).CliqueFree (n + 1)
f : Fin (n + 1) ↪ α
ha : ∀ {a b : Fin (n + 1)}, (G ⊔ edge v w).Adj (f a) (f b) ↔ ¬a = b
x : Fin (n + 1)
hx : f x = w
a b : Fin n
hs :
  G.Adj (f (x.succAbove a)) (f (x.succAbove b)) ∨
      (f (x.succAbove a) = v ∧ f (x.succAbove b) = w ∨ f (x.succAbove a) = w ∧ f (x.succAbove b) = v) ∧
        f (x.succAbove a) ≠ f (x.succAbove b) ↔
    ¬x.succAbove a = x.succAbove b
ia : w ≠ f (x.succAbove a)
ib : w ≠ f (x.succAbove b)
⊢ G.Adj (f (x.succAbove a)) (f (x.succAbove b)) ↔ a ≠ b

Tactic:
simp only [ia.symm, ib.symm, and_false, false_and, or_false] at hs

Result:
case map_rel_iff'
α : Type u_1
G : SimpleGraph α
n : ℕ
v w : α
h : ¬(G ⊔ edge v w).CliqueFree (n + 1)
f : Fin (n + 1) ↪ α
ha : ∀ {a b : Fin (n + 1)}, (G ⊔ edge v w).Adj (f a) (f b) ↔ ¬a = b
x : Fin (n + 1)
hx : f x = w
a b : Fin n
ia : w ≠ f (x.succAbove a)
ib : w ≠ f (x.succAbove b)
hs : G.Adj (f (x.succAbove a)) (f (x.succAbove b)) ↔ ¬x.succAbove a = x.succAbove b
⊢ G.Adj (f (x.succAbove a)) (f (x.succAbove b)) ↔ a ≠ b

Proof state:
case pos.intro
α : Type u_1
G : SimpleGraph α
n : ℕ
v w : α
h : ¬(G ⊔ edge v w).CliqueFree (n + 1)
f : Fin (n + 1) ↪ α
ha : ∀ {a b : Fin (n + 1)}, (G ⊔ edge v w).Adj (f a) (f b) ↔ ¬a = b
x : Fin (n + 1)
hx : f x = w
⊢ Nonempty (⊤ ↪g G)

Tactic:
use ⟨f ∘ x.succAboveEmb, f.2.comp Fin.succAbove_right_injective⟩

Result:
case map_rel_iff'
α : Type u_1
G : SimpleGraph α
n : ℕ
v w : α
h : ¬(G ⊔ edge v w).CliqueFree (n + 1)
f : Fin (n + 1) ↪ α
ha : ∀ {a b : Fin (n + 1)}, (G ⊔ edge v w).Adj (f a) (f b) ↔ ¬a = b
x : Fin (n + 1)
hx : f x = w
⊢ ∀ {a b : Fin n},
    G.Adj ({ toFun := ⇑f ∘ ⇑x.succAboveEmb, inj' := ⋯ } a) ({ toFun := ⇑f ∘ ⇑x.succAboveEmb, inj' := ⋯ } b) ↔ ⊤.Adj a b

Proof state:
case mk
α : Type u_1
G : SimpleGraph α
n : ℕ
v w : α
h : ¬(G ⊔ edge v w).CliqueFree (n + 1)
f : Fin (n + 1) ↪ α
ha : ∀ {a b : Fin (n + 1)}, (G ⊔ edge v w).Adj (f a) (f b) ↔ ⊤.Adj a b
⊢ ¬G.CliqueFree n

Tactic:
simp only [ne_eq, top_adj] at ha

Result:
case mk
α : Type u_1
G : SimpleGraph α
n : ℕ
v w : α
h : ¬(G ⊔ edge v w).CliqueFree (n + 1)
f : Fin (n + 1) ↪ α
ha : ∀ {a b : Fin (n + 1)}, (G ⊔ edge v w).Adj (f a) (f b) ↔ ¬a = b
⊢ ¬G.CliqueFree n