α : Type u_1
G H : SimpleGraph α
m n✝ : ℕ
s : Finset α
n : ℕ
f : ⊤ ↪g G
⊢ ∃ x, induce (↑x) G = ⊤ ∧ Finset.card x = n
α : Type u_1
G H : SimpleGraph α
m n✝ : ℕ
s : Finset α
n : ℕ
f : ⊤ ↪g G
⊢ ¬CliqueFree G n
simp only [CliqueFree, isNClique_iff, isClique_iff_induce_eq, not_forall, Classical.not_not]
α : Type u_1
G H : SimpleGraph α
m n✝ : ℕ
s : Finset α
n : ℕ
f : ⊤ ↪g G
⊢ induce (↑(map f.toEmbedding univ)) G = ⊤ ∧ Finset.card (map f.toEmbedding univ) = n
α : Type u_1
G H : SimpleGraph α
m n✝ : ℕ
s : Finset α
n : ℕ
f : ⊤ ↪g G
⊢ ∃ x, induce (↑x) G = ⊤ ∧ Finset.card x = n
use Finset.univ.map f.toEmbedding
α : Type u_1
G H : SimpleGraph α
m n✝ : ℕ
s : Finset α
n : ℕ
f : ⊤ ↪g G
⊢ induce (↑(map f.toEmbedding univ)) G = ⊤
α : Type u_1
G H : SimpleGraph α
m n✝ : ℕ
s : Finset α
n : ℕ
f : ⊤ ↪g G
⊢ induce (↑(map f.toEmbedding univ)) G = ⊤ ∧ Finset.card (map f.toEmbedding univ) = n
simp only [card_map, Finset.card_fin, eq_self_iff_true, and_true_iff]
case Adj.h.mk.h.mk.a
α : Type u_1
G H : SimpleGraph α
m n✝ : ℕ
s : Finset α
n : ℕ
f : ⊤ ↪g G
v : α
hv : v ∈ ↑(map f.toEmbedding univ)
w : α
hw : w ∈ ↑(map f.toEmbedding univ)
⊢ Adj (induce (↑(map f.toEmbedding univ)) G) { val := v, property := hv } { val := w, property := hw } ↔
    Adj ⊤ { val := v, property := hv } { val := w, property := hw }
α : Type u_1
G H : SimpleGraph α
m n✝ : ℕ
s : Finset α
n : ℕ
f : ⊤ ↪g G
⊢ induce (↑(map f.toEmbedding univ)) G = ⊤
ext ⟨v, hv⟩ ⟨w, hw⟩
case Adj.h.mk.h.mk.a
α : Type u_1
G H : SimpleGraph α
m n✝ : ℕ
s : Finset α
n : ℕ
f : ⊤ ↪g G
v : α
hv✝ : v ∈ ↑(map f.toEmbedding univ)
w : α
hw✝ : w ∈ ↑(map f.toEmbedding univ)
hv : ∃ x, ↑f.toEmbedding x = v
hw : ∃ x, ↑f.toEmbedding x = w
⊢ Adj (induce (↑(map f.toEmbedding univ)) G) { val := v, property := hv✝ } { val := w, property := hw✝ } ↔
    Adj ⊤ { val := v, property := hv✝ } { val := w, property := hw✝ }
case Adj.h.mk.h.mk.a
α : Type u_1
G H : SimpleGraph α
m n✝ : ℕ
s : Finset α
n : ℕ
f : ⊤ ↪g G
v : α
hv : v ∈ ↑(map f.toEmbedding univ)
w : α
hw : w ∈ ↑(map f.toEmbedding univ)
⊢ Adj (induce (↑(map f.toEmbedding univ)) G) { val := v, property := hv } { val := w, property := hw } ↔
    Adj ⊤ { val := v, property := hv } { val := w, property := hw }
simp only [coe_map, Set.mem_image, coe_univ, Set.mem_univ, true_and_iff] at hv hw
case Adj.h.mk.h.mk.a.intro
α : Type u_1
G H : SimpleGraph α
m n✝ : ℕ
s : Finset α
n : ℕ
f : ⊤ ↪g G
w : α
hw✝ : w ∈ ↑(map f.toEmbedding univ)
hw : ∃ x, ↑f.toEmbedding x = w
v' : Fin n
hv : ↑f.toEmbedding v' ∈ ↑(map f.toEmbedding univ)
⊢ Adj (induce (↑(map f.toEmbedding univ)) G) { val := ↑f.toEmbedding v', property := hv }
      { val := w, property := hw✝ } ↔
    Adj ⊤ { val := ↑f.toEmbedding v', property := hv } { val := w, property := hw✝ }
case Adj.h.mk.h.mk.a
α : Type u_1
G H : SimpleGraph α
m n✝ : ℕ
s : Finset α
n : ℕ
f : ⊤ ↪g G
v : α
hv✝ : v ∈ ↑(map f.toEmbedding univ)
w : α
hw✝ : w ∈ ↑(map f.toEmbedding univ)
hv : ∃ x, ↑f.toEmbedding x = v
hw : ∃ x, ↑f.toEmbedding x = w
⊢ Adj (induce (↑(map f.toEmbedding univ)) G) { val := v, property := hv✝ } { val := w, property := hw✝ } ↔
    Adj ⊤ { val := v, property := hv✝ } { val := w, property := hw✝ }
obtain ⟨v', rfl⟩ := hv
case Adj.h.mk.h.mk.a.intro.intro
α : Type u_1
G H : SimpleGraph α
m n✝ : ℕ
s : Finset α
n : ℕ
f : ⊤ ↪g G
v' : Fin n
hv : ↑f.toEmbedding v' ∈ ↑(map f.toEmbedding univ)
w' : Fin n
hw : ↑f.toEmbedding w' ∈ ↑(map f.toEmbedding univ)
⊢ Adj (induce (↑(map f.toEmbedding univ)) G) { val := ↑f.toEmbedding v', property := hv }
      { val := ↑f.toEmbedding w', property := hw } ↔
    Adj ⊤ { val := ↑f.toEmbedding v', property := hv } { val := ↑f.toEmbedding w', property := hw }
case Adj.h.mk.h.mk.a.intro
α : Type u_1
G H : SimpleGraph α
m n✝ : ℕ
s : Finset α
n : ℕ
f : ⊤ ↪g G
w : α
hw✝ : w ∈ ↑(map f.toEmbedding univ)
hw : ∃ x, ↑f.toEmbedding x = w
v' : Fin n
hv : ↑f.toEmbedding v' ∈ ↑(map f.toEmbedding univ)
⊢ Adj (induce (↑(map f.toEmbedding univ)) G) { val := ↑f.toEmbedding v', property := hv }
      { val := w, property := hw✝ } ↔
    Adj ⊤ { val := ↑f.toEmbedding v', property := hv } { val := w, property := hw✝ }
obtain ⟨w', rfl⟩ := hw
no goals
case Adj.h.mk.h.mk.a.intro.intro
α : Type u_1
G H : SimpleGraph α
m n✝ : ℕ
s : Finset α
n : ℕ
f : ⊤ ↪g G
v' : Fin n
hv : ↑f.toEmbedding v' ∈ ↑(map f.toEmbedding univ)
w' : Fin n
hw : ↑f.toEmbedding w' ∈ ↑(map f.toEmbedding univ)
⊢ Adj (induce (↑(map f.toEmbedding univ)) G) { val := ↑f.toEmbedding v', property := hv }
      { val := ↑f.toEmbedding w', property := hw } ↔
    Adj ⊤ { val := ↑f.toEmbedding v', property := hv } { val := ↑f.toEmbedding w', property := hw }
simp only [coe_sort_coe, RelEmbedding.coe_toEmbedding, comap_Adj, Function.Embedding.coe_subtype,
  f.map_adj_iff, top_adj, ne_eq, Subtype.mk.injEq, RelEmbedding.inj]