-- Mathlib/Combinatorics/SimpleGraph/Clique.lean
theorem not_cliqueFree_of_top_embedding {n : ℕ} (f : (⊤ : SimpleGraph (Fin n)) ↪g G) :
    ¬G.CliqueFree n

Proof state:
case h.Adj.h.mk.h.mk.a
α : Type u_1
G : SimpleGraph α
n : ℕ
f : ⊤ ↪g G
v : α
hv : v ∈ ↑(map f.toEmbedding univ)
w : α
hw : w ∈ ↑(map f.toEmbedding univ)
⊢ (induce (↑(map f.toEmbedding univ)) G).Adj ⟨v, hv⟩ ⟨w, hw⟩ ↔ ⊤.Adj ⟨v, hv⟩ ⟨w, hw⟩

Tactic:
simp only [coe_map, Set.mem_image, coe_univ, Set.mem_univ, true_and] at hv hw

Result:
case h.Adj.h.mk.h.mk.a
α : Type u_1
G : SimpleGraph α
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
⊢ (induce (↑(map f.toEmbedding univ)) G).Adj ⟨v, hv✝⟩ ⟨w, hw✝⟩ ↔ ⊤.Adj ⟨v, hv✝⟩ ⟨w, hw✝⟩

Proof state:
case h
α : Type u_1
G : SimpleGraph α
n : ℕ
f : ⊤ ↪g G
⊢ induce (↑(map f.toEmbedding univ)) G = ⊤ ∧ #(map f.toEmbedding univ) = n

Tactic:
simp only [card_map, Finset.card_fin, eq_self_iff_true, and_true]

Result:
case h
α : Type u_1
G : SimpleGraph α
n : ℕ
f : ⊤ ↪g G
⊢ induce (↑(map f.toEmbedding univ)) G = ⊤

Proof state:
case h.Adj.h.mk.h.mk.a.intro.intro
α : Type u_1
G : SimpleGraph α
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)
⊢ G.Adj ((Embedding.subtype fun x => x ∈ ↑(map f.toEmbedding univ)) ⟨f v', ⋯⟩)
      ((Embedding.subtype fun x => x ∈ ↑(map f.toEmbedding univ)) ⟨f w', ⋯⟩) ↔
    ¬v' = w'

Tactic:
erw [Function.Embedding.coe_subtype, f.map_adj_iff]

Result:
case h.Adj.h.mk.h.mk.a.intro.intro
α : Type u_1
G : SimpleGraph α
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 v' w' ↔ ¬v' = w'

Proof state:
case h
α : Type u_1
G : SimpleGraph α
n : ℕ
f : ⊤ ↪g G
⊢ induce (↑(map f.toEmbedding univ)) G = ⊤

Tactic:
ext ⟨v, hv⟩ ⟨w, hw⟩

Result:
case h.Adj.h.mk.h.mk.a
α : Type u_1
G : SimpleGraph α
n : ℕ
f : ⊤ ↪g G
v : α
hv : v ∈ ↑(map f.toEmbedding univ)
w : α
hw : w ∈ ↑(map f.toEmbedding univ)
⊢ (induce (↑(map f.toEmbedding univ)) G).Adj ⟨v, hv⟩ ⟨w, hw⟩ ↔ ⊤.Adj ⟨v, hv⟩ ⟨w, hw⟩

Proof state:
α : Type u_1
G : SimpleGraph α
n : ℕ
f : ⊤ ↪g G
⊢ ¬G.CliqueFree n

Tactic:
simp only [CliqueFree, isNClique_iff, isClique_iff_induce_eq, not_forall, Classical.not_not]

Result:
α : Type u_1
G : SimpleGraph α
n : ℕ
f : ⊤ ↪g G
⊢ ∃ x, induce (↑x) G = ⊤ ∧ #x = n

Proof state:
case h.Adj.h.mk.h.mk.a
α : Type u_1
G : SimpleGraph α
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
⊢ (induce (↑(map f.toEmbedding univ)) G).Adj ⟨v, hv✝⟩ ⟨w, hw✝⟩ ↔ ⊤.Adj ⟨v, hv✝⟩ ⟨w, hw✝⟩

Tactic:
obtain ⟨v', rfl⟩ := hv

Result:
case h.Adj.h.mk.h.mk.a.intro
α : Type u_1
G : SimpleGraph α
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)
⊢ (induce (↑(map f.toEmbedding univ)) G).Adj ⟨f.toEmbedding v', hv⟩ ⟨w, hw✝⟩ ↔ ⊤.Adj ⟨f.toEmbedding v', hv⟩ ⟨w, hw✝⟩

Proof state:
case h.Adj.h.mk.h.mk.a.intro.intro
α : Type u_1
G : SimpleGraph α
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 v' w' ↔ ¬v' = w'

Tactic:
simp

Result:
no goals

Proof state:
case h.Adj.h.mk.h.mk.a.intro
α : Type u_1
G : SimpleGraph α
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)
⊢ (induce (↑(map f.toEmbedding univ)) G).Adj ⟨f.toEmbedding v', hv⟩ ⟨w, hw✝⟩ ↔ ⊤.Adj ⟨f.toEmbedding v', hv⟩ ⟨w, hw✝⟩

Tactic:
obtain ⟨w', rfl⟩ := hw

Result:
case h.Adj.h.mk.h.mk.a.intro.intro
α : Type u_1
G : SimpleGraph α
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)
⊢ (induce (↑(map f.toEmbedding univ)) G).Adj ⟨f.toEmbedding v', hv⟩ ⟨f.toEmbedding w', hw⟩ ↔
    ⊤.Adj ⟨f.toEmbedding v', hv⟩ ⟨f.toEmbedding w', hw⟩

Proof state:
α : Type u_1
G : SimpleGraph α
n : ℕ
f : ⊤ ↪g G
⊢ ∃ x, induce (↑x) G = ⊤ ∧ #x = n

Tactic:
use Finset.univ.map f.toEmbedding

Result:
case h
α : Type u_1
G : SimpleGraph α
n : ℕ
f : ⊤ ↪g G
⊢ induce (↑(map f.toEmbedding univ)) G = ⊤ ∧ #(map f.toEmbedding univ) = n

Proof state:
case h.Adj.h.mk.h.mk.a.intro.intro
α : Type u_1
G : SimpleGraph α
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)
⊢ (induce (↑(map f.toEmbedding univ)) G).Adj ⟨f.toEmbedding v', hv⟩ ⟨f.toEmbedding w', hw⟩ ↔
    ⊤.Adj ⟨f.toEmbedding v', hv⟩ ⟨f.toEmbedding w', hw⟩

Tactic:
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]

Result:
case h.Adj.h.mk.h.mk.a.intro.intro
α : Type u_1
G : SimpleGraph α
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)
⊢ G.Adj ((Embedding.subtype fun x => x ∈ ↑(map f.toEmbedding univ)) ⟨f v', ⋯⟩)
      ((Embedding.subtype fun x => x ∈ ↑(map f.toEmbedding univ)) ⟨f w', ⋯⟩) ↔
    ¬v' = w'