[GOAL]
α : Type u_1
G H : SimpleGraph α
s t : Set α
⊢ IsClique G s ↔ induce s G = ⊤
[PROOFSTEP]
rw [isClique_iff]
[GOAL]
α : Type u_1
G H : SimpleGraph α
s t : Set α
⊢ Set.Pairwise s G.Adj ↔ induce s G = ⊤
[PROOFSTEP]
constructor
[GOAL]
case mp
α : Type u_1
G H : SimpleGraph α
s t : Set α
⊢ Set.Pairwise s G.Adj → induce s G = ⊤
[PROOFSTEP]
intro h
[GOAL]
case mp
α : Type u_1
G H : SimpleGraph α
s t : Set α
h : Set.Pairwise s G.Adj
⊢ induce s G = ⊤
[PROOFSTEP]
ext ⟨v, hv⟩ ⟨w, hw⟩
[GOAL]
case mp.Adj.h.mk.h.mk.a
α : Type u_1
G H : SimpleGraph α
s t : Set α
h : Set.Pairwise s G.Adj
v : α
hv : v ∈ s
w : α
hw : w ∈ s
⊢ Adj (induce s G) { val := v, property := hv } { val := w, property := hw } ↔
    Adj ⊤ { val := v, property := hv } { val := w, property := hw }
[PROOFSTEP]
simp only [comap_Adj, Subtype.coe_mk, top_adj, Ne.def, Subtype.mk_eq_mk]
[GOAL]
case mp.Adj.h.mk.h.mk.a
α : Type u_1
G H : SimpleGraph α
s t : Set α
h : Set.Pairwise s G.Adj
v : α
hv : v ∈ s
w : α
hw : w ∈ s
⊢ Adj G (↑(Function.Embedding.subtype fun x => x ∈ s) { val := v, property := hv })
      (↑(Function.Embedding.subtype fun x => x ∈ s) { val := w, property := hw }) ↔
    ¬v = w
[PROOFSTEP]
exact ⟨Adj.ne, h hv hw⟩
[GOAL]
case mpr
α : Type u_1
G H : SimpleGraph α
s t : Set α
⊢ induce s G = ⊤ → Set.Pairwise s G.Adj
[PROOFSTEP]
intro h v hv w hw hne
[GOAL]
case mpr
α : Type u_1
G H : SimpleGraph α
s t : Set α
h : induce s G = ⊤
v : α
hv : v ∈ s
w : α
hw : w ∈ s
hne : v ≠ w
⊢ Adj G v w
[PROOFSTEP]
have h2 : (G.induce s).Adj ⟨v, hv⟩ ⟨w, hw⟩ = _ := rfl
[GOAL]
case mpr
α : Type u_1
G H : SimpleGraph α
s t : Set α
h : induce s G = ⊤
v : α
hv : v ∈ s
w : α
hw : w ∈ s
hne : v ≠ w
h2 :
  Adj (induce s G) { val := v, property := hv } { val := w, property := hw } =
    Adj (induce s G) { val := v, property := hv } { val := w, property := hw }
⊢ Adj G v w
[PROOFSTEP]
conv_lhs at h2 => rw [h]
[GOAL]
α : Type u_1
G H : SimpleGraph α
s t : Set α
h : induce s G = ⊤
v : α
hv : v ∈ s
w : α
hw : w ∈ s
hne : v ≠ w
h2 :
  Adj (induce s G) { val := v, property := hv } { val := w, property := hw } =
    Adj (induce s G) { val := v, property := hv } { val := w, property := hw }
| Adj (induce s G) { val := v, property := hv } { val := w, property := hw }
[PROOFSTEP]
rw [h]
[GOAL]
α : Type u_1
G H : SimpleGraph α
s t : Set α
h : induce s G = ⊤
v : α
hv : v ∈ s
w : α
hw : w ∈ s
hne : v ≠ w
h2 :
  Adj (induce s G) { val := v, property := hv } { val := w, property := hw } =
    Adj (induce s G) { val := v, property := hv } { val := w, property := hw }
| Adj (induce s G) { val := v, property := hv } { val := w, property := hw }
[PROOFSTEP]
rw [h]
[GOAL]
α : Type u_1
G H : SimpleGraph α
s t : Set α
h : induce s G = ⊤
v : α
hv : v ∈ s
w : α
hw : w ∈ s
hne : v ≠ w
h2 :
  Adj (induce s G) { val := v, property := hv } { val := w, property := hw } =
    Adj (induce s G) { val := v, property := hv } { val := w, property := hw }
| Adj (induce s G) { val := v, property := hv } { val := w, property := hw }
[PROOFSTEP]
rw [h]
[GOAL]
case mpr
α : Type u_1
G H : SimpleGraph α
s t : Set α
h : induce s G = ⊤
v : α
hv : v ∈ s
w : α
hw : w ∈ s
hne : v ≠ w
h2 :
  Adj ⊤ { val := v, property := hv } { val := w, property := hw } =
    Adj (induce s G) { val := v, property := hv } { val := w, property := hw }
⊢ Adj G v w
[PROOFSTEP]
simp only [top_adj, ne_eq, Subtype.mk.injEq, eq_iff_iff] at h2 
[GOAL]
case mpr
α : Type u_1
G H : SimpleGraph α
s t : Set α
h : induce s G = ⊤
v : α
hv : v ∈ s
w : α
hw : w ∈ s
hne : v ≠ w
h2 : ¬v = w ↔ Adj (induce s G) { val := v, property := hv } { val := w, property := hw }
⊢ Adj G v w
[PROOFSTEP]
exact h2.1 hne
[GOAL]
α : Type u_1
G H : SimpleGraph α
s t : Set α
h : G ≤ H
⊢ IsClique G s → IsClique H s
[PROOFSTEP]
simp_rw [isClique_iff]
[GOAL]
α : Type u_1
G H : SimpleGraph α
s t : Set α
h : G ≤ H
⊢ Set.Pairwise s G.Adj → Set.Pairwise s H.Adj
[PROOFSTEP]
exact Set.Pairwise.mono' h
[GOAL]
α : Type u_1
G H : SimpleGraph α
s t : Set α
h : t ⊆ s
⊢ IsClique G s → IsClique G t
[PROOFSTEP]
simp_rw [isClique_iff]
[GOAL]
α : Type u_1
G H : SimpleGraph α
s t : Set α
h : t ⊆ s
⊢ Set.Pairwise s G.Adj → Set.Pairwise t G.Adj
[PROOFSTEP]
exact Set.Pairwise.mono h
[GOAL]
α : Type u_1
G H : SimpleGraph α
n : ℕ
s : Finset α
h : G ≤ H
⊢ IsNClique G n s → IsNClique H n s
[PROOFSTEP]
simp_rw [isNClique_iff]
[GOAL]
α : Type u_1
G H : SimpleGraph α
n : ℕ
s : Finset α
h : G ≤ H
⊢ IsClique G ↑s ∧ Finset.card s = n → IsClique H ↑s ∧ Finset.card s = n
[PROOFSTEP]
exact And.imp_left (IsClique.mono h)
[GOAL]
α : Type u_1
G H : SimpleGraph α
n : ℕ
s : Finset α
⊢ IsNClique ⊥ n s ↔ n ≤ 1 ∧ Finset.card s = n
[PROOFSTEP]
rw [isNClique_iff, isClique_bot_iff]
[GOAL]
α : Type u_1
G H : SimpleGraph α
n : ℕ
s : Finset α
⊢ Set.Subsingleton ↑s ∧ Finset.card s = n ↔ n ≤ 1 ∧ Finset.card s = n
[PROOFSTEP]
refine' and_congr_left _
[GOAL]
α : Type u_1
G H : SimpleGraph α
n : ℕ
s : Finset α
⊢ Finset.card s = n → (Set.Subsingleton ↑s ↔ n ≤ 1)
[PROOFSTEP]
rintro rfl
[GOAL]
α : Type u_1
G H : SimpleGraph α
s : Finset α
⊢ Set.Subsingleton ↑s ↔ Finset.card s ≤ 1
[PROOFSTEP]
exact card_le_one.symm
[GOAL]
α : Type u_1
G H : SimpleGraph α
n : ℕ
s : Finset α
inst✝ : DecidableEq α
a b c : α
⊢ IsNClique G 3 {a, b, c} ↔ Adj G a b ∧ Adj G a c ∧ Adj G b c
[PROOFSTEP]
simp only [isNClique_iff, isClique_iff, Set.pairwise_insert_of_symmetric G.symm, coe_insert]
[GOAL]
α : Type u_1
G H : SimpleGraph α
n : ℕ
s : Finset α
inst✝ : DecidableEq α
a b c : α
⊢ ((Set.Pairwise (↑{c}) G.Adj ∧ ∀ (b_1 : α), b_1 ∈ ↑{c} → b ≠ b_1 → Adj G b b_1) ∧
        ∀ (b_1 : α), b_1 ∈ insert b ↑{c} → a ≠ b_1 → Adj G a b_1) ∧
      Finset.card {a, b, c} = 3 ↔
    Adj G a b ∧ Adj G a c ∧ Adj G b c
[PROOFSTEP]
by_cases hab : a = b
[GOAL]
case pos
α : Type u_1
G H : SimpleGraph α
n : ℕ
s : Finset α
inst✝ : DecidableEq α
a b c : α
hab : a = b
⊢ ((Set.Pairwise (↑{c}) G.Adj ∧ ∀ (b_1 : α), b_1 ∈ ↑{c} → b ≠ b_1 → Adj G b b_1) ∧
        ∀ (b_1 : α), b_1 ∈ insert b ↑{c} → a ≠ b_1 → Adj G a b_1) ∧
      Finset.card {a, b, c} = 3 ↔
    Adj G a b ∧ Adj G a c ∧ Adj G b c
[PROOFSTEP]
by_cases hbc : b = c
[GOAL]
case neg
α : Type u_1
G H : SimpleGraph α
n : ℕ
s : Finset α
inst✝ : DecidableEq α
a b c : α
hab : ¬a = b
⊢ ((Set.Pairwise (↑{c}) G.Adj ∧ ∀ (b_1 : α), b_1 ∈ ↑{c} → b ≠ b_1 → Adj G b b_1) ∧
        ∀ (b_1 : α), b_1 ∈ insert b ↑{c} → a ≠ b_1 → Adj G a b_1) ∧
      Finset.card {a, b, c} = 3 ↔
    Adj G a b ∧ Adj G a c ∧ Adj G b c
[PROOFSTEP]
by_cases hbc : b = c
[GOAL]
case pos
α : Type u_1
G H : SimpleGraph α
n : ℕ
s : Finset α
inst✝ : DecidableEq α
a b c : α
hab : a = b
hbc : b = c
⊢ ((Set.Pairwise (↑{c}) G.Adj ∧ ∀ (b_1 : α), b_1 ∈ ↑{c} → b ≠ b_1 → Adj G b b_1) ∧
        ∀ (b_1 : α), b_1 ∈ insert b ↑{c} → a ≠ b_1 → Adj G a b_1) ∧
      Finset.card {a, b, c} = 3 ↔
    Adj G a b ∧ Adj G a c ∧ Adj G b c
[PROOFSTEP]
by_cases hac : a = c
[GOAL]
case neg
α : Type u_1
G H : SimpleGraph α
n : ℕ
s : Finset α
inst✝ : DecidableEq α
a b c : α
hab : a = b
hbc : ¬b = c
⊢ ((Set.Pairwise (↑{c}) G.Adj ∧ ∀ (b_1 : α), b_1 ∈ ↑{c} → b ≠ b_1 → Adj G b b_1) ∧
        ∀ (b_1 : α), b_1 ∈ insert b ↑{c} → a ≠ b_1 → Adj G a b_1) ∧
      Finset.card {a, b, c} = 3 ↔
    Adj G a b ∧ Adj G a c ∧ Adj G b c
[PROOFSTEP]
by_cases hac : a = c
[GOAL]
case pos
α : Type u_1
G H : SimpleGraph α
n : ℕ
s : Finset α
inst✝ : DecidableEq α
a b c : α
hab : ¬a = b
hbc : b = c
⊢ ((Set.Pairwise (↑{c}) G.Adj ∧ ∀ (b_1 : α), b_1 ∈ ↑{c} → b ≠ b_1 → Adj G b b_1) ∧
        ∀ (b_1 : α), b_1 ∈ insert b ↑{c} → a ≠ b_1 → Adj G a b_1) ∧
      Finset.card {a, b, c} = 3 ↔
    Adj G a b ∧ Adj G a c ∧ Adj G b c
[PROOFSTEP]
by_cases hac : a = c
[GOAL]
case neg
α : Type u_1
G H : SimpleGraph α
n : ℕ
s : Finset α
inst✝ : DecidableEq α
a b c : α
hab : ¬a = b
hbc : ¬b = c
⊢ ((Set.Pairwise (↑{c}) G.Adj ∧ ∀ (b_1 : α), b_1 ∈ ↑{c} → b ≠ b_1 → Adj G b b_1) ∧
        ∀ (b_1 : α), b_1 ∈ insert b ↑{c} → a ≠ b_1 → Adj G a b_1) ∧
      Finset.card {a, b, c} = 3 ↔
    Adj G a b ∧ Adj G a c ∧ Adj G b c
[PROOFSTEP]
by_cases hac : a = c
[GOAL]
case pos
α : Type u_1
G H : SimpleGraph α
n : ℕ
s : Finset α
inst✝ : DecidableEq α
a b c : α
hab : a = b
hbc : b = c
hac : a = c
⊢ ((Set.Pairwise (↑{c}) G.Adj ∧ ∀ (b_1 : α), b_1 ∈ ↑{c} → b ≠ b_1 → Adj G b b_1) ∧
        ∀ (b_1 : α), b_1 ∈ insert b ↑{c} → a ≠ b_1 → Adj G a b_1) ∧
      Finset.card {a, b, c} = 3 ↔
    Adj G a b ∧ Adj G a c ∧ Adj G b c
[PROOFSTEP]
subst_vars
[GOAL]
case neg
α : Type u_1
G H : SimpleGraph α
n : ℕ
s : Finset α
inst✝ : DecidableEq α
a b c : α
hab : a = b
hbc : b = c
hac : ¬a = c
⊢ ((Set.Pairwise (↑{c}) G.Adj ∧ ∀ (b_1 : α), b_1 ∈ ↑{c} → b ≠ b_1 → Adj G b b_1) ∧
        ∀ (b_1 : α), b_1 ∈ insert b ↑{c} → a ≠ b_1 → Adj G a b_1) ∧
      Finset.card {a, b, c} = 3 ↔
    Adj G a b ∧ Adj G a c ∧ Adj G b c
[PROOFSTEP]
subst_vars
[GOAL]
case pos
α : Type u_1
G H : SimpleGraph α
n : ℕ
s : Finset α
inst✝ : DecidableEq α
a b c : α
hab : a = b
hbc : ¬b = c
hac : a = c
⊢ ((Set.Pairwise (↑{c}) G.Adj ∧ ∀ (b_1 : α), b_1 ∈ ↑{c} → b ≠ b_1 → Adj G b b_1) ∧
        ∀ (b_1 : α), b_1 ∈ insert b ↑{c} → a ≠ b_1 → Adj G a b_1) ∧
      Finset.card {a, b, c} = 3 ↔
    Adj G a b ∧ Adj G a c ∧ Adj G b c
[PROOFSTEP]
subst_vars
[GOAL]
case neg
α : Type u_1
G H : SimpleGraph α
n : ℕ
s : Finset α
inst✝ : DecidableEq α
a b c : α
hab : a = b
hbc : ¬b = c
hac : ¬a = c
⊢ ((Set.Pairwise (↑{c}) G.Adj ∧ ∀ (b_1 : α), b_1 ∈ ↑{c} → b ≠ b_1 → Adj G b b_1) ∧
        ∀ (b_1 : α), b_1 ∈ insert b ↑{c} → a ≠ b_1 → Adj G a b_1) ∧
      Finset.card {a, b, c} = 3 ↔
    Adj G a b ∧ Adj G a c ∧ Adj G b c
[PROOFSTEP]
subst_vars
[GOAL]
case pos
α : Type u_1
G H : SimpleGraph α
n : ℕ
s : Finset α
inst✝ : DecidableEq α
a b c : α
hab : ¬a = b
hbc : b = c
hac : a = c
⊢ ((Set.Pairwise (↑{c}) G.Adj ∧ ∀ (b_1 : α), b_1 ∈ ↑{c} → b ≠ b_1 → Adj G b b_1) ∧
        ∀ (b_1 : α), b_1 ∈ insert b ↑{c} → a ≠ b_1 → Adj G a b_1) ∧
      Finset.card {a, b, c} = 3 ↔
    Adj G a b ∧ Adj G a c ∧ Adj G b c
[PROOFSTEP]
subst_vars
[GOAL]
case neg
α : Type u_1
G H : SimpleGraph α
n : ℕ
s : Finset α
inst✝ : DecidableEq α
a b c : α
hab : ¬a = b
hbc : b = c
hac : ¬a = c
⊢ ((Set.Pairwise (↑{c}) G.Adj ∧ ∀ (b_1 : α), b_1 ∈ ↑{c} → b ≠ b_1 → Adj G b b_1) ∧
        ∀ (b_1 : α), b_1 ∈ insert b ↑{c} → a ≠ b_1 → Adj G a b_1) ∧
      Finset.card {a, b, c} = 3 ↔
    Adj G a b ∧ Adj G a c ∧ Adj G b c
[PROOFSTEP]
subst_vars
[GOAL]
case pos
α : Type u_1
G H : SimpleGraph α
n : ℕ
s : Finset α
inst✝ : DecidableEq α
a b c : α
hab : ¬a = b
hbc : ¬b = c
hac : a = c
⊢ ((Set.Pairwise (↑{c}) G.Adj ∧ ∀ (b_1 : α), b_1 ∈ ↑{c} → b ≠ b_1 → Adj G b b_1) ∧
        ∀ (b_1 : α), b_1 ∈ insert b ↑{c} → a ≠ b_1 → Adj G a b_1) ∧
      Finset.card {a, b, c} = 3 ↔
    Adj G a b ∧ Adj G a c ∧ Adj G b c
[PROOFSTEP]
subst_vars
[GOAL]
case neg
α : Type u_1
G H : SimpleGraph α
n : ℕ
s : Finset α
inst✝ : DecidableEq α
a b c : α
hab : ¬a = b
hbc : ¬b = c
hac : ¬a = c
⊢ ((Set.Pairwise (↑{c}) G.Adj ∧ ∀ (b_1 : α), b_1 ∈ ↑{c} → b ≠ b_1 → Adj G b b_1) ∧
        ∀ (b_1 : α), b_1 ∈ insert b ↑{c} → a ≠ b_1 → Adj G a b_1) ∧
      Finset.card {a, b, c} = 3 ↔
    Adj G a b ∧ Adj G a c ∧ Adj G b c
[PROOFSTEP]
subst_vars
[GOAL]
case pos
α : Type u_1
G H : SimpleGraph α
n : ℕ
s : Finset α
inst✝ : DecidableEq α
c : α
hac : c = c
⊢ ((Set.Pairwise (↑{c}) G.Adj ∧ ∀ (b : α), b ∈ ↑{c} → c ≠ b → Adj G c b) ∧
        ∀ (b : α), b ∈ insert c ↑{c} → c ≠ b → Adj G c b) ∧
      Finset.card {c, c, c} = 3 ↔
    Adj G c c ∧ Adj G c c ∧ Adj G c c
[PROOFSTEP]
simp [G.ne_of_adj, and_rotate, *]
[GOAL]
case neg
α : Type u_1
G H : SimpleGraph α
n : ℕ
s : Finset α
inst✝ : DecidableEq α
c : α
hac : ¬c = c
⊢ ((Set.Pairwise (↑{c}) G.Adj ∧ ∀ (b : α), b ∈ ↑{c} → c ≠ b → Adj G c b) ∧
        ∀ (b : α), b ∈ insert c ↑{c} → c ≠ b → Adj G c b) ∧
      Finset.card {c, c, c} = 3 ↔
    Adj G c c ∧ Adj G c c ∧ Adj G c c
[PROOFSTEP]
simp [G.ne_of_adj, and_rotate, *]
[GOAL]
case pos
α : Type u_1
G H : SimpleGraph α
n : ℕ
s : Finset α
inst✝ : DecidableEq α
c : α
hbc : ¬c = c
⊢ ((Set.Pairwise (↑{c}) G.Adj ∧ ∀ (b : α), b ∈ ↑{c} → c ≠ b → Adj G c b) ∧
        ∀ (b : α), b ∈ insert c ↑{c} → c ≠ b → Adj G c b) ∧
      Finset.card {c, c, c} = 3 ↔
    Adj G c c ∧ Adj G c c ∧ Adj G c c
[PROOFSTEP]
simp [G.ne_of_adj, and_rotate, *]
[GOAL]
case neg
α : Type u_1
G H : SimpleGraph α
n : ℕ
s : Finset α
inst✝ : DecidableEq α
b c : α
hbc hac : ¬b = c
⊢ ((Set.Pairwise (↑{c}) G.Adj ∧ ∀ (b_1 : α), b_1 ∈ ↑{c} → b ≠ b_1 → Adj G b b_1) ∧
        ∀ (b_1 : α), b_1 ∈ insert b ↑{c} → b ≠ b_1 → Adj G b b_1) ∧
      Finset.card {b, b, c} = 3 ↔
    Adj G b b ∧ Adj G b c ∧ Adj G b c
[PROOFSTEP]
simp [G.ne_of_adj, and_rotate, *]
[GOAL]
case pos
α : Type u_1
G H : SimpleGraph α
n : ℕ
s : Finset α
inst✝ : DecidableEq α
c : α
hab : ¬c = c
⊢ ((Set.Pairwise (↑{c}) G.Adj ∧ ∀ (b : α), b ∈ ↑{c} → c ≠ b → Adj G c b) ∧
        ∀ (b : α), b ∈ insert c ↑{c} → c ≠ b → Adj G c b) ∧
      Finset.card {c, c, c} = 3 ↔
    Adj G c c ∧ Adj G c c ∧ Adj G c c
[PROOFSTEP]
simp [G.ne_of_adj, and_rotate, *]
[GOAL]
case neg
α : Type u_1
G H : SimpleGraph α
n : ℕ
s : Finset α
inst✝ : DecidableEq α
a c : α
hac hab : ¬a = c
⊢ ((Set.Pairwise (↑{c}) G.Adj ∧ ∀ (b : α), b ∈ ↑{c} → c ≠ b → Adj G c b) ∧
        ∀ (b : α), b ∈ insert c ↑{c} → a ≠ b → Adj G a b) ∧
      Finset.card {a, c, c} = 3 ↔
    Adj G a c ∧ Adj G a c ∧ Adj G c c
[PROOFSTEP]
simp [G.ne_of_adj, and_rotate, *]
[GOAL]
case pos
α : Type u_1
G H : SimpleGraph α
n : ℕ
s : Finset α
inst✝ : DecidableEq α
b c : α
hbc : ¬b = c
hab : ¬c = b
⊢ ((Set.Pairwise (↑{c}) G.Adj ∧ ∀ (b_1 : α), b_1 ∈ ↑{c} → b ≠ b_1 → Adj G b b_1) ∧
        ∀ (b_1 : α), b_1 ∈ insert b ↑{c} → c ≠ b_1 → Adj G c b_1) ∧
      Finset.card {c, b, c} = 3 ↔
    Adj G c b ∧ Adj G c c ∧ Adj G b c
[PROOFSTEP]
simp [G.ne_of_adj, and_rotate, *]
[GOAL]
case neg
α : Type u_1
G H : SimpleGraph α
n : ℕ
s : Finset α
inst✝ : DecidableEq α
a b c : α
hab : ¬a = b
hbc : ¬b = c
hac : ¬a = c
⊢ ((Set.Pairwise (↑{c}) G.Adj ∧ ∀ (b_1 : α), b_1 ∈ ↑{c} → b ≠ b_1 → Adj G b b_1) ∧
        ∀ (b_1 : α), b_1 ∈ insert b ↑{c} → a ≠ b_1 → Adj G a b_1) ∧
      Finset.card {a, b, c} = 3 ↔
    Adj G a b ∧ Adj G a c ∧ Adj G b c
[PROOFSTEP]
simp [G.ne_of_adj, and_rotate, *]
[GOAL]
α : Type u_1
G H : SimpleGraph α
n : ℕ
s : Finset α
inst✝ : DecidableEq α
a b c : α
⊢ IsNClique G 3 s ↔ ∃ a b c, Adj G a b ∧ Adj G a c ∧ Adj G b c ∧ s = {a, b, c}
[PROOFSTEP]
refine' ⟨fun h ↦ _, _⟩
[GOAL]
case refine'_1
α : Type u_1
G H : SimpleGraph α
n : ℕ
s : Finset α
inst✝ : DecidableEq α
a b c : α
h : IsNClique G 3 s
⊢ ∃ a b c, Adj G a b ∧ Adj G a c ∧ Adj G b c ∧ s = {a, b, c}
[PROOFSTEP]
obtain ⟨a, b, c, -, -, -, hs⟩ := card_eq_three.1 h.card_eq
[GOAL]
case refine'_1.intro.intro.intro.intro.intro.intro
α : Type u_1
G H : SimpleGraph α
n : ℕ
s : Finset α
inst✝ : DecidableEq α
a✝ b✝ c✝ : α
h : IsNClique G 3 s
a b c : α
hs : s = {a, b, c}
⊢ ∃ a b c, Adj G a b ∧ Adj G a c ∧ Adj G b c ∧ s = {a, b, c}
[PROOFSTEP]
refine' ⟨a, b, c, _⟩
[GOAL]
case refine'_1.intro.intro.intro.intro.intro.intro
α : Type u_1
G H : SimpleGraph α
n : ℕ
s : Finset α
inst✝ : DecidableEq α
a✝ b✝ c✝ : α
h : IsNClique G 3 s
a b c : α
hs : s = {a, b, c}
⊢ Adj G a b ∧ Adj G a c ∧ Adj G b c ∧ s = {a, b, c}
[PROOFSTEP]
rwa [hs, eq_self_iff_true, and_true, is3Clique_triple_iff.symm, ← hs]
[GOAL]
case refine'_2
α : Type u_1
G H : SimpleGraph α
n : ℕ
s : Finset α
inst✝ : DecidableEq α
a b c : α
⊢ (∃ a b c, Adj G a b ∧ Adj G a c ∧ Adj G b c ∧ s = {a, b, c}) → IsNClique G 3 s
[PROOFSTEP]
rintro ⟨a, b, c, hab, hbc, hca, rfl⟩
[GOAL]
case refine'_2.intro.intro.intro.intro.intro.intro
α : Type u_1
G H : SimpleGraph α
n : ℕ
inst✝ : DecidableEq α
a✝ b✝ c✝ a b c : α
hab : Adj G a b
hbc : Adj G a c
hca : Adj G b c
⊢ IsNClique G 3 {a, b, c}
[PROOFSTEP]
exact is3Clique_triple_iff.2 ⟨hab, hbc, hca⟩
[GOAL]
α : Type u_1
G H : SimpleGraph α
m n✝ : ℕ
s : Finset α
n : ℕ
f : ⊤ ↪g G
⊢ ¬CliqueFree G n
[PROOFSTEP]
simp only [CliqueFree, isNClique_iff, isClique_iff_induce_eq, not_forall, Classical.not_not]
[GOAL]
α : Type u_1
G H : SimpleGraph α
m n✝ : ℕ
s : Finset α
n : ℕ
f : ⊤ ↪g G
⊢ ∃ x, induce (↑x) G = ⊤ ∧ Finset.card x = n
[PROOFSTEP]
use Finset.univ.map f.toEmbedding
[GOAL]
case h
α : 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
[PROOFSTEP]
simp only [card_map, Finset.card_fin, eq_self_iff_true, and_true_iff]
[GOAL]
case h
α : Type u_1
G H : SimpleGraph α
m n✝ : ℕ
s : Finset α
n : ℕ
f : ⊤ ↪g G
⊢ induce (↑(map f.toEmbedding univ)) G = ⊤
[PROOFSTEP]
ext ⟨v, hv⟩ ⟨w, hw⟩
[GOAL]
case h.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 }
[PROOFSTEP]
simp only [coe_map, Set.mem_image, coe_univ, Set.mem_univ, true_and_iff] at hv hw 
[GOAL]
case h.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✝ }
[PROOFSTEP]
obtain ⟨v', rfl⟩ := hv
[GOAL]
case h.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✝ }
[PROOFSTEP]
obtain ⟨w', rfl⟩ := hw
[GOAL]
case h.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 }
[PROOFSTEP]
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]
[GOAL]
α : Type u_1
G H : SimpleGraph α
m n✝ : ℕ
s : Finset α
n : ℕ
h : ¬CliqueFree G n
⊢ ⊤ ↪g G
[PROOFSTEP]
simp only [CliqueFree, isNClique_iff, isClique_iff_induce_eq, not_forall, Classical.not_not] at h 
[GOAL]
α : Type u_1
G H : SimpleGraph α
m n✝ : ℕ
s : Finset α
n : ℕ
h : ∃ x, induce (↑x) G = ⊤ ∧ Finset.card x = n
⊢ ⊤ ↪g G
[PROOFSTEP]
obtain ⟨ha, hb⟩ := h.choose_spec
[GOAL]
case intro
α : Type u_1
G H : SimpleGraph α
m n✝ : ℕ
s : Finset α
n : ℕ
h : ∃ x, induce (↑x) G = ⊤ ∧ Finset.card x = n
ha : induce (↑(Exists.choose h)) G = ⊤
hb : Finset.card (Exists.choose h) = n
⊢ ⊤ ↪g G
[PROOFSTEP]
have : (⊤ : SimpleGraph (Fin h.choose.card)) ≃g (⊤ : SimpleGraph h.choose) :=
  by
  apply Iso.completeGraph
  simpa using (Fintype.equivFin h.choose).symm
[GOAL]
α : Type u_1
G H : SimpleGraph α
m n✝ : ℕ
s : Finset α
n : ℕ
h : ∃ x, induce (↑x) G = ⊤ ∧ Finset.card x = n
ha : induce (↑(Exists.choose h)) G = ⊤
hb : Finset.card (Exists.choose h) = n
⊢ ⊤ ≃g ⊤
[PROOFSTEP]
apply Iso.completeGraph
[GOAL]
case f
α : Type u_1
G H : SimpleGraph α
m n✝ : ℕ
s : Finset α
n : ℕ
h : ∃ x, induce (↑x) G = ⊤ ∧ Finset.card x = n
ha : induce (↑(Exists.choose h)) G = ⊤
hb : Finset.card (Exists.choose h) = n
⊢ Fin (Finset.card (Exists.choose h)) ≃ { x // x ∈ Exists.choose h }
[PROOFSTEP]
simpa using (Fintype.equivFin h.choose).symm
[GOAL]
case intro
α : Type u_1
G H : SimpleGraph α
m n✝ : ℕ
s : Finset α
n : ℕ
h : ∃ x, induce (↑x) G = ⊤ ∧ Finset.card x = n
ha : induce (↑(Exists.choose h)) G = ⊤
hb : Finset.card (Exists.choose h) = n
this : ⊤ ≃g ⊤
⊢ ⊤ ↪g G
[PROOFSTEP]
rw [← ha] at this 
[GOAL]
case intro
α : Type u_1
G H : SimpleGraph α
m n✝ : ℕ
s : Finset α
n : ℕ
h : ∃ x, induce (↑x) G = ⊤ ∧ Finset.card x = n
ha : induce (↑(Exists.choose h)) G = ⊤
hb : Finset.card (Exists.choose h) = n
this : ⊤ ≃g induce (↑(Exists.choose h)) G
⊢ ⊤ ↪g G
[PROOFSTEP]
convert (Embedding.induce ↑h.choose.toSet).comp this.toEmbedding
[GOAL]
case h.e'_1.h.e'_1
α : Type u_1
G H : SimpleGraph α
m n✝ : ℕ
s : Finset α
n : ℕ
h : ∃ x, induce (↑x) G = ⊤ ∧ Finset.card x = n
ha : induce (↑(Exists.choose h)) G = ⊤
hb : Finset.card (Exists.choose h) = n
this : ⊤ ≃g induce (↑(Exists.choose h)) G
⊢ n = Finset.card (Exists.choose h)
[PROOFSTEP]
exact hb.symm
[GOAL]
α : Type u_1
G H : SimpleGraph α
m n✝ : ℕ
s : Finset α
n : ℕ
⊢ CliqueFree G n ↔ IsEmpty (⊤ ↪g G)
[PROOFSTEP]
rw [← not_iff_not, not_cliqueFree_iff, not_isEmpty_iff]
[GOAL]
α : Type u_1
G H : SimpleGraph α
m n : ℕ
s : Finset α
inst✝ : Fintype α
f : ⊤ ↪g G
⊢ ¬CliqueFree G (Fintype.card α)
[PROOFSTEP]
rw [not_cliqueFree_iff]
[GOAL]
α : Type u_1
G H : SimpleGraph α
m n : ℕ
s : Finset α
inst✝ : Fintype α
f : ⊤ ↪g G
⊢ Nonempty (⊤ ↪g G)
[PROOFSTEP]
exact ⟨(Iso.completeGraph (Fintype.equivFin α)).symm.toEmbedding.trans f⟩
[GOAL]
α : Type u_1
G H : SimpleGraph α
m n : ℕ
s : Finset α
h : 2 ≤ n
⊢ CliqueFree ⊥ n
[PROOFSTEP]
intro t ht
[GOAL]
α : Type u_1
G H : SimpleGraph α
m n : ℕ
s : Finset α
h : 2 ≤ n
t : Finset α
ht : IsNClique ⊥ n t
⊢ False
[PROOFSTEP]
have := le_trans h (isNClique_bot_iff.1 ht).1
[GOAL]
α : Type u_1
G H : SimpleGraph α
m n : ℕ
s : Finset α
h : 2 ≤ n
t : Finset α
ht : IsNClique ⊥ n t
this : 2 ≤ 1
⊢ False
[PROOFSTEP]
simp only at this 
[GOAL]
α : Type u_1
G H : SimpleGraph α
m n : ℕ
s : Finset α
h : m ≤ n
⊢ CliqueFree G m → CliqueFree G n
[PROOFSTEP]
intro hG s hs
[GOAL]
α : Type u_1
G H : SimpleGraph α
m n : ℕ
s✝ : Finset α
h : m ≤ n
hG : CliqueFree G m
s : Finset α
hs : IsNClique G n s
⊢ False
[PROOFSTEP]
obtain ⟨t, hts, ht⟩ := s.exists_smaller_set _ (h.trans hs.card_eq.ge)
[GOAL]
case intro.intro
α : Type u_1
G H : SimpleGraph α
m n : ℕ
s✝ : Finset α
h : m ≤ n
hG : CliqueFree G m
s : Finset α
hs : IsNClique G n s
t : Finset α
hts : t ⊆ s
ht : Finset.card t = m
⊢ False
[PROOFSTEP]
exact hG _ ⟨hs.clique.subset hts, ht⟩
[GOAL]
α : Type u_1
G H : SimpleGraph α
m n : ℕ
s : Finset α
inst✝ : Fintype α
hc : Fintype.card α < n
⊢ CliqueFree G n
[PROOFSTEP]
by_contra h
[GOAL]
α : Type u_1
G H : SimpleGraph α
m n : ℕ
s : Finset α
inst✝ : Fintype α
hc : Fintype.card α < n
h : ¬CliqueFree G n
⊢ False
[PROOFSTEP]
refine' Nat.lt_le_antisymm hc _
[GOAL]
α : Type u_1
G H : SimpleGraph α
m n : ℕ
s : Finset α
inst✝ : Fintype α
hc : Fintype.card α < n
h : ¬CliqueFree G n
⊢ n ≤ Fintype.card α
[PROOFSTEP]
rw [cliqueFree_iff, not_isEmpty_iff] at h 
[GOAL]
α : Type u_1
G H : SimpleGraph α
m n : ℕ
s : Finset α
inst✝ : Fintype α
hc : Fintype.card α < n
h : Nonempty (⊤ ↪g G)
⊢ n ≤ Fintype.card α
[PROOFSTEP]
simpa only [Fintype.card_fin] using Fintype.card_le_of_embedding h.some.toEmbedding
[GOAL]
α : Type u_1
G H : SimpleGraph α
n : ℕ
a b c : α
s : Finset α
⊢ cliqueSet G n = ∅ ↔ CliqueFree G n
[PROOFSTEP]
simp_rw [CliqueFree, Set.eq_empty_iff_forall_not_mem, mem_cliqueSet_iff]
[GOAL]
α : Type u_1
G H : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
n : ℕ
a b c : α
s : Finset α
⊢ cliqueFinset G n = ∅ ↔ CliqueFree G n
[PROOFSTEP]
simp_rw [CliqueFree, eq_empty_iff_forall_not_mem, mem_cliqueFinset_iff]
