-- 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
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
⊢ G.Adj (f a.succ) (f b.succ) ↔ a ≠ b

Tactic:
have ia : f a.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
⊢ G.Adj (f a.succ) (f b.succ) ↔ a ≠ b

Proof state:
case neg
α : 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:
use ⟨f ∘ Fin.succEmb n, (f.2.of_comp_iff _).mpr (Fin.succ_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
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:
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)
ib : w ≠ f (x.succAbove b)
⊢ G.Adj (f (x.succAbove a)) (f (x.succAbove b)) ↔ a ≠ b

Tactic:
rw [sup_adj, edge_adj] 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
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

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) ↔ ¬a = b
⊢ Nonempty (⊤ ↪g G)

Tactic:
by_cases mw : w ∈ Set.range f

Result:
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)

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

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
⊢ G.Adj ({ toFun := ⇑f ∘ ⇑x.succAboveEmb, inj' := ⋯ } a) ({ toFun := ⇑f ∘ ⇑x.succAboveEmb, inj' := ⋯ } b) ↔ ⊤.Adj a b

Tactic:
simp_rw [Embedding.coeFn_mk, comp_apply, Fin.succAboveEmb_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
x : Fin (n + 1)
hx : f x = w
a b : Fin n
⊢ G.Adj (f (x.succAbove a)) (f (x.succAbove b)) ↔ 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) ↔ ¬a = b
⊢ ¬G.CliqueFree n

Tactic:
rw [not_cliqueFree_iff]

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
⊢ 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},
    G.Adj ({ toFun := ⇑f ∘ ⇑x.succAboveEmb, inj' := ⋯ } a) ({ toFun := ⇑f ∘ ⇑x.succAboveEmb, 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
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:
α : 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
⊢ f a.succ ≠ w

Tactic:
simp_all

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.Adj (f a.succ) (f b.succ) ∨ (f a.succ = v ∧ f b.succ = w ∨ f a.succ = w ∧ f b.succ = v) ∧ 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

Tactic:
simp only [ia, ib, 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
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

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
ia : w ≠ f (x.succAbove a)
⊢ G.Adj (f (x.succAbove a)) (f (x.succAbove b)) ↔ a ≠ b

Tactic:
have ib : w ≠ f (x.succAbove b) :=
  (hx ▸ f.apply_eq_iff_eq x (x.succAbove b)).ne.mpr (x.succAbove_ne b).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)
ib : w ≠ f (x.succAbove b)
⊢ G.Adj (f (x.succAbove a)) (f (x.succAbove b)) ↔ a ≠ b