awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
n : ℕ
ι : Type u_3
V : ι → Type u_4
f : (i : ι) → V i
h : ¬Infinite ι
this : Fintype ι
hc : n ≤ Fintype.card ι
⊢ ¬(completeMultipartiteGraph V).CliqueFree n

Tactic:
exact not_cliqueFree_of_le_card V f hc

Premises used: SimpleGraph.completeMultipartiteGraph.not_cliqueFree_of_le_card
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
G : SimpleGraph α
n : ℕ
inst : DecidableEq α
h : G.CliqueFree n
s t : α
contrapose : ∀ (h : ¬(G.replaceVertex s t).CliqueFree n), ¬G.CliqueFree n
⊢ (G.replaceVertex s t).CliqueFree n

Tactic:
contrapose h
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
G : SimpleGraph α
n : ℕ
inst : DecidableEq α
s t : α
h : ¬(G.replaceVertex s t).CliqueFree n
have :
  ∀ (φ : Fin n ↪ α)
    (hφ :
      ∀ {a b : Fin n},
        (G.replaceVertex s t).Adj ((φ : (a : Fin n) → α) a) ((φ : (a : Fin n) → α) b) ↔
          Adj (completeGraph (Fin n)) a b),
    ¬G.CliqueFree n
⊢ ¬G.CliqueFree n

Tactic:
have ⟨φ, hφ⟩ := topEmbeddingOfNotCliqueFree h
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : 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 : Fin n) → α) a) ((φ : (a : Fin n) → α) b) ↔ Adj (completeGraph (Fin n)) a b
rw : IsContained (α := Fin n) (completeGraph (Fin n)) G
⊢ ¬G.CliqueFree n

Tactic:
rw [not_cliqueFree_iff_top_isContained]

Premises used: SimpleGraph.not_cliqueFree_iff_top_isContained
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : 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 : Fin n) → α) a) ((φ : (a : Fin n) → α) b) ↔ Adj (completeGraph (Fin n)) a b
pos :
  ∀ (mt : Membership.mem (γ := Set α) (Set.range (ι := Fin n) (⇑φ : (a : Fin n) → α)) t),
    IsContained (α := Fin n) (completeGraph (Fin n)) G
neg : ∀ (mt : t ∉ Set.range (ι := Fin n) (⇑φ : (a : Fin n) → α)), IsContained (α := Fin n) (completeGraph (Fin n)) G
⊢ IsContained (α := Fin n) (completeGraph (Fin n)) G

Tactic:
by_cases mt : t ∈ Set.range φ

Premises used: mt, Set.range, DFunLike.coe
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : 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 : Fin n) → α) a) ((φ : (a : Fin n) → α) b) ↔ Adj (completeGraph (Fin n)) a b
mt : Membership.mem (γ := Set α) (Set.range (ι := Fin n) (⇑φ : (a : Fin n) → α)) t
pos : ∀ (x : Fin n) (hx : (φ : (a : Fin n) → α) x = t), IsContained (α := Fin n) (completeGraph (Fin n)) G
⊢ IsContained (α := Fin n) (completeGraph (Fin n)) G

Tactic:
obtain ⟨x, hx⟩ := mt
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : 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 : Fin n) → α) a) ((φ : (a : Fin n) → α) b) ↔ Adj (completeGraph (Fin n)) a b
x : Fin n
hx : (φ : (a : Fin n) → α) x = t
pos :
  ∀ (ms : Membership.mem (γ := Set α) (Set.range (ι := Fin n) (⇑φ : (a : Fin n) → α)) s),
    IsContained (α := Fin n) (completeGraph (Fin n)) G
neg : ∀ (ms : s ∉ Set.range (ι := Fin n) (⇑φ : (a : Fin n) → α)), IsContained (α := Fin n) (completeGraph (Fin n)) G
⊢ IsContained (α := Fin n) (completeGraph (Fin n)) G

Tactic:
by_cases ms : s ∈ Set.range φ

Premises used: Set.range, DFunLike.coe
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : 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 : Fin n) → α) a) ((φ : (a : Fin n) → α) b) ↔ Adj (completeGraph (Fin n)) a b
x : Fin n
hx : (φ : (a : Fin n) → α) x = t
ms : Membership.mem (γ := Set α) (Set.range (ι := Fin n) (⇑φ : (a : Fin n) → α)) s
pos : ∀ (y : Fin n) (hy : (φ : (a : Fin n) → α) y = s), IsContained (α := Fin n) (completeGraph (Fin n)) G
⊢ IsContained (α := Fin n) (completeGraph (Fin n)) G

Tactic:
obtain ⟨y, hy⟩ := ms
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : 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 : Fin n) → α) a) ((φ : (a : Fin n) → α) b) ↔ Adj (completeGraph (Fin n)) a b
x : Fin n
hx : (φ : (a : Fin n) → α) x = t
y : Fin n
hy : (φ : (a : Fin n) → α) y = s
⊢ (G.replaceVertex s t).Adj ((φ : (a : Fin n) → α) x) ((φ : (a : Fin n) → α) y) ↔ Adj (completeGraph (Fin n)) x y

Tactic:
have e := @hφ x y
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : 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 : Fin n) → α) a) ((φ : (a : Fin n) → α) b) ↔ Adj (completeGraph (Fin n)) a b
x : Fin n
hx : (φ : (a : Fin n) → α) x = t
y : Fin n
hy : (φ : (a : Fin n) → α) y = s
e : (G.replaceVertex s t).Adj ((φ : (a : Fin n) → α) x) ((φ : (a : Fin n) → α) y) ↔ Adj (completeGraph (Fin n)) x y
⊢ x = y

Tactic:
simp_rw [hx, hy, adj_comm, not_adj_replaceVertex_same, top_adj, false_iff, not_ne_iff] at e

Premises used: SimpleGraph.top_adj, not_ne_iff, false_iff, SimpleGraph.not_adj_replaceVertex_same, SimpleGraph.adj_comm
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : 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 : Fin n) → α) a) ((φ : (a : Fin n) → α) b) ↔ Adj (completeGraph (Fin n)) a b
x : Fin n
hx : (φ : (a : Fin n) → α) x = t
y : Fin n
hy : (φ : (a : Fin n) → α) y = s
e : x = y
pos :
  ∀ (h : ¬(G.replaceVertex s ((φ : (a : Fin n) → α) x)).CliqueFree n) (hx : (φ : (a : Fin n) → α) x = t) (y : Fin n)
    (hy : (φ : (a : Fin n) → α) y = s) (e : x = y), IsContained (α := Fin n) (completeGraph (Fin n)) G
pos₁ :
  ∀ (hx : (φ : (a : Fin n) → α) x = t) (y : Fin n) (h : ¬(G.replaceVertex s ((φ : (a : Fin n) → α) y)).CliqueFree n)
    (hy : (φ : (a : Fin n) → α) y = s) (e : x = y), IsContained (α := Fin n) (completeGraph (Fin n)) G
pos₂ :
  ∀ (hx : (φ : (a : Fin n) → α) x = t) (y : Fin n) (h : ¬(G.replaceVertex s s).CliqueFree n)
    (hy : (φ : (a : Fin n) → α) y = s) (e : x = y), IsContained (α := Fin n) (completeGraph (Fin n)) G
pos₃ :
  ∀ (hx : (φ : (a : Fin n) → α) x = t) (y : Fin n) (h : ¬G.CliqueFree n) (hy : (φ : (a : Fin n) → α) y = s) (e : x = y),
    IsContained (α := Fin n) (completeGraph (Fin n)) G
pos₄ pos₅ pos₆ pos₇ :
  ∀ (hx : (φ : (a : Fin n) → α) x = t) (y : Fin n) (h : IsContained (α := Fin n) (completeGraph (Fin n)) G)
    (hy : (φ : (a : Fin n) → α) y = s) (e : x = y), IsContained (α := Fin n) (completeGraph (Fin n)) G
⊢ IsContained (α := Fin n) (completeGraph (Fin n)) G

Tactic:
rwa [← hx, e, hy, replaceVertex_self, not_cliqueFree_iff_top_isContained] at h

Premises used: SimpleGraph.replaceVertex_self, SimpleGraph.not_cliqueFree_iff_top_isContained
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : 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 := ⋯ : SimpleGraph α }.Adj
        ((φ : (a : Fin n) → α) a) ((φ : (a : Fin n) → α) b) ↔
      Adj (completeGraph (Fin n)) a b
x : Fin n
hx : (φ : (a : Fin n) → α) x = t
ms : s ∉ Set.range (ι := Fin n) (⇑φ : (a : Fin n) → α)
⊢ IsContained (α := Fin n) (completeGraph (Fin n)) G

Tactic:
Embedding.isContained ⟨φ.setValue x s, fun {a b} ↦ ?_⟩

Premises used: RelEmbedding.mk, SimpleGraph.Embedding.isContained, Function.Embedding.setValue
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : 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 := ⋯ : SimpleGraph α }.Adj
        ((φ : (a : Fin n) → α) a) ((φ : (a : Fin n) → α) b) ↔
      Adj (completeGraph (Fin n)) a b
x : Fin n
hx : (φ : (a : Fin n) → α) x = t
ms : s ∉ Set.range (ι := Fin n) (⇑φ : (a : Fin n) → α)
neg :
  ∀ {a b : Fin n},
    G.Adj ((φ.setValue x s : (a : Fin n) → α) a) ((φ.setValue x s : (a : Fin n) → α) b) ↔
      Adj (completeGraph (Fin n)) a b
⊢ IsContained (α := Fin n) (completeGraph (Fin n)) G

Tactic:
refine Embedding.isContained ⟨φ.setValue x s, fun {a b} ↦ ?_⟩

Premises used: RelEmbedding.mk, SimpleGraph.Embedding.isContained, Function.Embedding.setValue
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : 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 := ⋯ : SimpleGraph α }.Adj
        ((φ : (a : Fin n) → α) a) ((φ : (a : Fin n) → α) b) ↔
      Adj (completeGraph (Fin n)) a b
x : Fin n
hx : (φ : (a : Fin n) → α) x = t
ms : s ∉ Set.range (ι := Fin n) (⇑φ : (a : Fin n) → α)
a b : Fin n
neg :
  G.Adj (if a = x then s else (φ : (a : Fin n) → α) a) (if b = x then s else (φ : (a : Fin n) → α) b) ↔
    Adj (completeGraph (Fin n)) a b
⊢ G.Adj ((φ.setValue x s : (a : Fin n) → α) a) ((φ.setValue x s : (a : Fin n) → α) b) ↔ Adj (completeGraph (Fin n)) a b

Tactic:
simp only [Embedding.coeFn_mk, Embedding.setValue, not_exists.mp ms, ite_false]

Premises used: ite_false, not_exists, Function.Embedding.setValue, Iff.mp, Function.Embedding.coeFn_mk
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : 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 := ⋯ : SimpleGraph α }.Adj
        ((φ : (a : Fin n) → α) a) ((φ : (a : Fin n) → α) b) ↔
      Adj (completeGraph (Fin n)) a b
x : Fin n
hx : (φ : (a : Fin n) → α) x = t
ms : s ∉ Set.range (ι := Fin n) (⇑φ : (a : Fin n) → α)
a b : Fin n
neg :
  (if a = x then if b = x then G.Adj s s else G.Adj s ((φ : (a : Fin n) → α) b)
    else
      if b = x then G.Adj ((φ : (a : Fin n) → α) a) s else G.Adj ((φ : (a : Fin n) → α) a) ((φ : (a : Fin n) → α) b)) ↔
    Adj (completeGraph (Fin n)) a b
⊢ G.Adj (if a = x then s else (φ : (a : Fin n) → α) a) (if b = x then s else (φ : (a : Fin n) → α) b) ↔
    Adj (completeGraph (Fin n)) a b

Tactic:
rw [apply_ite (G.Adj · _), apply_ite (G.Adj _ ·), apply_ite (G.Adj _ ·)]

Premises used: SimpleGraph.Adj, apply_ite
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : 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 := ⋯ : SimpleGraph α }.Adj
        ((φ : (a : Fin n) → α) a) ((φ : (a : Fin n) → α) b) ↔
      Adj (completeGraph (Fin n)) a b
x : Fin n
hx : (φ : (a : Fin n) → α) x = t
ms : s ∉ Set.range (ι := Fin n) (⇑φ : (a : Fin n) → α)
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 := ⋯ : SimpleGraph α }.Adj
      ((φ : (a : Fin n) → α) a) ((φ : (a : Fin n) → α) b) ↔
    Adj (completeGraph (Fin n)) a b

Tactic:
@hφ a b
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : 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 := ⋯ : SimpleGraph α }.Adj
        ((φ : (a : Fin n) → α) a) ((φ : (a : Fin n) → α) b) ↔
      Adj (completeGraph (Fin n)) a b
x : Fin n
hx : (φ : (a : Fin n) → α) x = t
ms : s ∉ Set.range (ι := Fin n) (⇑φ : (a : Fin n) → α)
a b : Fin n
h₁ : a = x ↔ (φ : (a : Fin n) → α) a = t
h₂ : (φ : (a : Fin n) → α) a = t → (b = x ↔ (φ : (a : Fin n) → α) b = t)
h₃ : (φ : (a : Fin n) → α) a = t → (φ : (a : Fin n) → α) b = t → (G.Adj s s ↔ False)
h₄ : ¬(φ : (a : Fin n) → α) a = t → (b = x ↔ (φ : (a : Fin n) → α) b = t)
⊢ (if a = x then if b = x then G.Adj s s else G.Adj s ((φ : (a : Fin n) → α) b)
    else
      if b = x then G.Adj ((φ : (a : Fin n) → α) a) s else G.Adj ((φ : (a : Fin n) → α) a) ((φ : (a : Fin n) → α) b)) ↔
    Adj (completeGraph (Fin n)) a b

Tactic:
convert! @hφ a b
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : 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 := ⋯ : SimpleGraph α }.Adj
        ((φ : (a : Fin n) → α) a) ((φ : (a : Fin n) → α) b) ↔
      Adj (completeGraph (Fin n)) a b
x : Fin n
hx : (φ : (a : Fin n) → α) x = t
ms : s ∉ Set.range (ι := Fin n) (⇑φ : (a : Fin n) → α)
a b : Fin n
⊢ a = x ↔ (φ : (a : Fin n) → α) a = t

Tactic:
simp only [← φ.apply_eq_iff_eq, SimpleGraph.irrefl, hx]

Premises used: Function.Embedding.apply_eq_iff_eq, SimpleGraph.irrefl
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : 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 := ⋯ : SimpleGraph α }.Adj
        ((φ : (a : Fin n) → α) a) ((φ : (a : Fin n) → α) b) ↔
      Adj (completeGraph (Fin n)) a b
x : Fin n
hx : (φ : (a : Fin n) → α) x = t
ms : s ∉ Set.range (ι := Fin n) (⇑φ : (a : Fin n) → α)
a b : Fin n
h_1 : (φ : (a : Fin n) → α) a = t
⊢ b = x ↔ (φ : (a : Fin n) → α) b = t

Tactic:
simp only [← φ.apply_eq_iff_eq, SimpleGraph.irrefl, hx]

Premises used: Function.Embedding.apply_eq_iff_eq, SimpleGraph.irrefl
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : 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 := ⋯ : SimpleGraph α }.Adj
        ((φ : (a : Fin n) → α) a) ((φ : (a : Fin n) → α) b) ↔
      Adj (completeGraph (Fin n)) a b
x : Fin n
hx : (φ : (a : Fin n) → α) x = t
ms : s ∉ Set.range (ι := Fin n) (⇑φ : (a : Fin n) → α)
a b : Fin n
h_1 : (φ : (a : Fin n) → α) a = t
h_2 : (φ : (a : Fin n) → α) b = t
⊢ G.Adj s s ↔ False

Tactic:
simp only [← φ.apply_eq_iff_eq, SimpleGraph.irrefl, hx]

Premises used: Function.Embedding.apply_eq_iff_eq, SimpleGraph.irrefl
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : 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 := ⋯ : SimpleGraph α }.Adj
        ((φ : (a : Fin n) → α) a) ((φ : (a : Fin n) → α) b) ↔
      Adj (completeGraph (Fin n)) a b
x : Fin n
hx : (φ : (a : Fin n) → α) x = t
ms : s ∉ Set.range (ι := Fin n) (⇑φ : (a : Fin n) → α)
a b : Fin n
h_1 : ¬(φ : (a : Fin n) → α) a = t
⊢ b = x ↔ (φ : (a : Fin n) → α) b = t

Tactic:
simp only [← φ.apply_eq_iff_eq, SimpleGraph.irrefl, hx]

Premises used: Function.Embedding.apply_eq_iff_eq, SimpleGraph.irrefl
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : 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 : Fin n) → α) a) ((φ : (a : Fin n) → α) b) ↔ Adj (completeGraph (Fin n)) a b
mt : t ∉ Set.range (ι := Fin n) (⇑φ : (a : Fin n) → α)
⊢ IsContained (α := Fin n) (completeGraph (Fin n)) G

Tactic:
Embedding.isContained ⟨φ, ?_⟩

Premises used: RelEmbedding.mk, SimpleGraph.Embedding.isContained
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : 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 : Fin n) → α) a) ((φ : (a : Fin n) → α) b) ↔ Adj (completeGraph (Fin n)) a b
mt : t ∉ Set.range (ι := Fin n) (⇑φ : (a : Fin n) → α)
neg : ∀ {a b : Fin n}, G.Adj ((φ : (a : Fin n) → α) a) ((φ : (a : Fin n) → α) b) ↔ Adj (completeGraph (Fin n)) a b
⊢ IsContained (α := Fin n) (completeGraph (Fin n)) G

Tactic:
refine Embedding.isContained ⟨φ, ?_⟩

Premises used: RelEmbedding.mk, SimpleGraph.Embedding.isContained
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : 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 : Fin n) → α) a) ((φ : (a : Fin n) → α) b) ↔ Adj (completeGraph (Fin n)) a b
mt : t ∉ Set.range (ι := Fin n) (⇑φ : (a : Fin n) → α)
⊢ ∀ (x : Fin n), (φ : (a : Fin n) → α) x ≠ t

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

Premises used: Set.mem_range, not_exists, ne_eq
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : 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 : Fin n) → α) a) ((φ : (a : Fin n) → α) b) ↔ Adj (completeGraph (Fin n)) a b
mt : ∀ (x : Fin n), (φ : (a : Fin n) → α) x ≠ t
enter :
  ∀ {a b : Fin n},
    (G.replaceVertex s t).Adj ((φ : (a : Fin n) → α) a) ((φ : (a : Fin n) → α) b) ↔ Adj (completeGraph (Fin n)) a b
| ∀ {a b : Fin n},
    (G.replaceVertex s t).Adj ((φ : (a : Fin n) → α) a) ((φ : (a : Fin n) → α) b) ↔ Adj (completeGraph (Fin n)) a b

Tactic:
enter [a, b]
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : 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 : Fin n) → α) a) ((φ : (a : Fin n) → α) b) ↔ Adj (completeGraph (Fin n)) a b
mt : ∀ (x : Fin n), (φ : (a : Fin n) → α) x ≠ t
a b : Fin n
rw : G.Adj ((φ : (a : Fin n) → α) a) ((φ : (a : Fin n) → α) b) ↔ Adj (completeGraph (Fin n)) a b
| (G.replaceVertex s t).Adj ((φ : (a : Fin n) → α) a) ((φ : (a : Fin n) → α) b) ↔ Adj (completeGraph (Fin n)) a b

Tactic:
rw [G.adj_replaceVertex_iff_of_ne _ (mt a) (mt b)]

Premises used: SimpleGraph.adj_replaceVertex_iff_of_ne
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : 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 : Fin n) → α) a) ((φ : (a : Fin n) → α) b) ↔ Adj (completeGraph (Fin n)) a b
mt : ∀ (x : Fin n), (φ : (a : Fin n) → α) x ≠ t
enter : ∀ {a b : Fin n}, G.Adj ((φ : (a : Fin n) → α) a) ((φ : (a : Fin n) → α) b) ↔ Adj (completeGraph (Fin n)) a b
| ∀ {a b : Fin n},
    (G.replaceVertex s t).Adj ((φ : (a : Fin n) → α) a) ((φ : (a : Fin n) → α) b) ↔ Adj (completeGraph (Fin n)) a b

Tactic:
enter [a, b]; rw [G.adj_replaceVertex_iff_of_ne _ (mt a) (mt b)]
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : 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 : Fin n) → α) a) ((φ : (a : Fin n) → α) b) ↔ Adj (completeGraph (Fin n)) a b
mt : ∀ (x : Fin n), (φ : (a : Fin n) → α) x ≠ t
⊢ ∀ {a b : Fin n}, G.Adj ((φ : (a : Fin n) → α) a) ((φ : (a : Fin n) → α) b) ↔ Adj (completeGraph (Fin n)) a b

Tactic:
conv at hφ => enter [a, b]; rw [G.adj_replaceVertex_iff_of_ne _ (mt a) (mt b)]
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : 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 : Fin n) → α) a) ((φ : (a : Fin n) → α) b) ↔ Adj (completeGraph (Fin n)) a b
mt : ∀ (x : Fin n), (φ : (a : Fin n) → α) x ≠ t
hφ₁ : ∀ {a b : Fin n}, G.Adj ((φ : (a : Fin n) → α) a) ((φ : (a : Fin n) → α) b) ↔ Adj (completeGraph (Fin n)) a b
⊢ ∀ (x : Fin n), (φ : (a : Fin n) → α) x ≠ t

Tactic:
conv at hφ => enter [a, b]; rw [G.adj_replaceVertex_iff_of_ne _ (mt a) (mt b)]
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : 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 : Fin n) → α) a) ((φ : (a : Fin n) → α) b) ↔ Adj (completeGraph (Fin n)) a b
mt : ∀ (x : Fin n), (φ : (a : Fin n) → α) x ≠ t
a b : Fin n
⊢ G.Adj ((φ : (a : Fin n) → α) a) ((φ : (a : Fin n) → α) b) ↔ Adj (completeGraph (Fin n)) a b

Tactic:
hφ
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : 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 : Fin n) → α) a) ((φ : (a : Fin n) → α) b) ↔ Adj (completeGraph (Fin n)) a b
mt : ∀ (x : Fin n), (φ : (a : Fin n) → α) x ≠ t
⊢ ∀ {a b : Fin n}, G.Adj ((φ : (a : Fin n) → α) a) ((φ : (a : Fin n) → α) b) ↔ Adj (completeGraph (Fin n)) a b

Tactic:
exact hφ
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
G : SimpleGraph α
⊢ G.CliqueFree 1 ↔ IsEmpty α

Tactic:
simp [CliqueFree, isEmpty_iff]

Premises used: isEmpty_iff, SimpleGraph.CliqueFree
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
G : SimpleGraph α
mp : G.CliqueFree 2 → G = ⊥
mpr : G = ⊥ → G.CliqueFree 2
⊢ G.CliqueFree 2 ↔ G = ⊥

Tactic:
constructor
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
G : SimpleGraph α
mp : G.CliqueFree 2 → ∀ (x y : α), ¬G.Adj x y
⊢ G.CliqueFree 2 → G = ⊥

Tactic:
simp_rw [← edgeSet_eq_empty, Set.eq_empty_iff_forall_notMem, Sym2.forall, mem_edgeSet]

Premises used: Sym2.forall, Set.eq_empty_iff_forall_notMem, SimpleGraph.edgeSet_eq_empty, SimpleGraph.mem_edgeSet
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
G : SimpleGraph α
h : G.CliqueFree 2
a b : α
hab : G.Adj a b
⊢ G.IsClique (↑{a, b} : Set α)

Tactic:
simpa [hab.ne]

Premises used: SimpleGraph.Adj.ne
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
G : SimpleGraph α
⊢ G.CliqueFree 2 → ∀ (x y : α), ¬G.Adj x y

Tactic:
exact fun h a b hab => h _ ⟨by simpa [hab.ne], card_pair hab.ne⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
⊢ CliqueFree.{u_1} (α := α) ⊥ 2

Tactic:
cliqueFree_bot le_rfl

Premises used: le_rfl, SimpleGraph.cliqueFree_bot
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
⊢ CliqueFree.{u_1} (α := α) ⊥ 2

Tactic:
exact cliqueFree_bot le_rfl

Premises used: le_rfl, SimpleGraph.cliqueFree_bot