[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]


[GOAL]
V : Type u
W : Type v
G : SimpleGraph V
F : SimpleGraph W
v : V
⊢ Set.Finite (SimpleGraph.singletonSubgraph G v).verts
[PROOFSTEP]
simp
[GOAL]
V : Type u
W : Type v
G : SimpleGraph V
F : SimpleGraph W
u v : V
e : Adj G u v
⊢ Set.Finite (subgraphOfAdj G e).verts
[PROOFSTEP]
simp
[GOAL]
V : Type u
W : Type v
G : SimpleGraph V
F : SimpleGraph W
u v : V
e : Adj G u v
⊢ singletonFinsubgraph u ≤ finsubgraphOfAdj e
[PROOFSTEP]
simp [singletonFinsubgraph, finsubgraphOfAdj]
[GOAL]
V : Type u
W : Type v
G : SimpleGraph V
F : SimpleGraph W
u v : V
e : Adj G u v
⊢ singletonFinsubgraph v ≤ finsubgraphOfAdj e
[PROOFSTEP]
simp [singletonFinsubgraph, finsubgraphOfAdj]
[GOAL]
V : Type u
W : Type v
G : SimpleGraph V
F : SimpleGraph W
G' G'' : Finsubgraph G
h : G'' ≤ G'
f : G' →fg F
⊢ G'' →fg F
[PROOFSTEP]
refine' ⟨fun ⟨v, hv⟩ => f.toFun ⟨v, h.1 hv⟩, _⟩
[GOAL]
V : Type u
W : Type v
G : SimpleGraph V
F : SimpleGraph W
G' G'' : Finsubgraph G
h : G'' ≤ G'
f : G' →fg F
⊢ ∀ {a b : ↑(↑G'').verts},
    Adj (Subgraph.coe ↑G'') a b →
      Adj F
        ((fun x =>
            match x with
            | { val := v, property := hv } => RelHom.toFun f { val := v, property := (_ : v ∈ (↑G').verts) })
          a)
        ((fun x =>
            match x with
            | { val := v, property := hv } => RelHom.toFun f { val := v, property := (_ : v ∈ (↑G').verts) })
          b)
[PROOFSTEP]
rintro ⟨u, hu⟩ ⟨v, hv⟩ huv
[GOAL]
case mk.mk
V : Type u
W : Type v
G : SimpleGraph V
F : SimpleGraph W
G' G'' : Finsubgraph G
h : G'' ≤ G'
f : G' →fg F
u : V
hu : u ∈ (↑G'').verts
v : V
hv : v ∈ (↑G'').verts
huv : Adj (Subgraph.coe ↑G'') { val := u, property := hu } { val := v, property := hv }
⊢ Adj F
    ((fun x =>
        match x with
        | { val := v, property := hv } => RelHom.toFun f { val := v, property := (_ : v ∈ (↑G').verts) })
      { val := u, property := hu })
    ((fun x =>
        match x with
        | { val := v, property := hv } => RelHom.toFun f { val := v, property := (_ : v ∈ (↑G').verts) })
      { val := v, property := hv })
[PROOFSTEP]
exact f.map_rel' (h.2 huv)
[GOAL]
V : Type u
W : Type v
G : SimpleGraph V
F : SimpleGraph W
inst✝ : Finite W
h : (G' : Subgraph G) → Set.Finite G'.verts → Subgraph.coe G' →g F
⊢ Nonempty (G →g F)
[PROOFSTEP]
cases nonempty_fintype W
[GOAL]
case intro
V : Type u
W : Type v
G : SimpleGraph V
F : SimpleGraph W
inst✝ : Finite W
h : (G' : Subgraph G) → Set.Finite G'.verts → Subgraph.coe G' →g F
val✝ : Fintype W
⊢ Nonempty (G →g F)
[PROOFSTEP]
haveI : ∀ G' : G.Finsubgraphᵒᵖ, Nonempty ((finsubgraphHomFunctor G F).obj G') := fun G' => ⟨h G'.unop G'.unop.property⟩
[GOAL]
case intro
V : Type u
W : Type v
G : SimpleGraph V
F : SimpleGraph W
inst✝ : Finite W
h : (G' : Subgraph G) → Set.Finite G'.verts → Subgraph.coe G' →g F
val✝ : Fintype W
this : ∀ (G' : (Finsubgraph G)ᵒᵖ), Nonempty ((finsubgraphHomFunctor G F).obj G')
⊢ Nonempty (G →g F)
[PROOFSTEP]
haveI : ∀ G' : G.Finsubgraphᵒᵖ, Fintype ((finsubgraphHomFunctor G F).obj G') :=
  by
  intro G'
  haveI : Fintype (G'.unop.val.verts : Type u) := G'.unop.property.fintype
  haveI : Fintype (↥G'.unop.val.verts → W) := by classical exact Pi.fintype
  exact Fintype.ofInjective (fun f => f.toFun) RelHom.coe_fn_injective
[GOAL]
V : Type u
W : Type v
G : SimpleGraph V
F : SimpleGraph W
inst✝ : Finite W
h : (G' : Subgraph G) → Set.Finite G'.verts → Subgraph.coe G' →g F
val✝ : Fintype W
this : ∀ (G' : (Finsubgraph G)ᵒᵖ), Nonempty ((finsubgraphHomFunctor G F).obj G')
⊢ (G' : (Finsubgraph G)ᵒᵖ) → Fintype ((finsubgraphHomFunctor G F).obj G')
[PROOFSTEP]
intro G'
[GOAL]
V : Type u
W : Type v
G : SimpleGraph V
F : SimpleGraph W
inst✝ : Finite W
h : (G' : Subgraph G) → Set.Finite G'.verts → Subgraph.coe G' →g F
val✝ : Fintype W
this : ∀ (G' : (Finsubgraph G)ᵒᵖ), Nonempty ((finsubgraphHomFunctor G F).obj G')
G' : (Finsubgraph G)ᵒᵖ
⊢ Fintype ((finsubgraphHomFunctor G F).obj G')
[PROOFSTEP]
haveI : Fintype (G'.unop.val.verts : Type u) := G'.unop.property.fintype
[GOAL]
V : Type u
W : Type v
G : SimpleGraph V
F : SimpleGraph W
inst✝ : Finite W
h : (G' : Subgraph G) → Set.Finite G'.verts → Subgraph.coe G' →g F
val✝ : Fintype W
this✝ : ∀ (G' : (Finsubgraph G)ᵒᵖ), Nonempty ((finsubgraphHomFunctor G F).obj G')
G' : (Finsubgraph G)ᵒᵖ
this : Fintype ↑(↑G'.unop).verts
⊢ Fintype ((finsubgraphHomFunctor G F).obj G')
[PROOFSTEP]
haveI : Fintype (↥G'.unop.val.verts → W) := by classical exact Pi.fintype
[GOAL]
V : Type u
W : Type v
G : SimpleGraph V
F : SimpleGraph W
inst✝ : Finite W
h : (G' : Subgraph G) → Set.Finite G'.verts → Subgraph.coe G' →g F
val✝ : Fintype W
this✝ : ∀ (G' : (Finsubgraph G)ᵒᵖ), Nonempty ((finsubgraphHomFunctor G F).obj G')
G' : (Finsubgraph G)ᵒᵖ
this : Fintype ↑(↑G'.unop).verts
⊢ Fintype (↑(↑G'.unop).verts → W)
[PROOFSTEP]
classical exact Pi.fintype
[GOAL]
V : Type u
W : Type v
G : SimpleGraph V
F : SimpleGraph W
inst✝ : Finite W
h : (G' : Subgraph G) → Set.Finite G'.verts → Subgraph.coe G' →g F
val✝ : Fintype W
this✝ : ∀ (G' : (Finsubgraph G)ᵒᵖ), Nonempty ((finsubgraphHomFunctor G F).obj G')
G' : (Finsubgraph G)ᵒᵖ
this : Fintype ↑(↑G'.unop).verts
⊢ Fintype (↑(↑G'.unop).verts → W)
[PROOFSTEP]
exact Pi.fintype
[GOAL]
V : Type u
W : Type v
G : SimpleGraph V
F : SimpleGraph W
inst✝ : Finite W
h : (G' : Subgraph G) → Set.Finite G'.verts → Subgraph.coe G' →g F
val✝ : Fintype W
this✝¹ : ∀ (G' : (Finsubgraph G)ᵒᵖ), Nonempty ((finsubgraphHomFunctor G F).obj G')
G' : (Finsubgraph G)ᵒᵖ
this✝ : Fintype ↑(↑G'.unop).verts
this : Fintype (↑(↑G'.unop).verts → W)
⊢ Fintype ((finsubgraphHomFunctor G F).obj G')
[PROOFSTEP]
exact Fintype.ofInjective (fun f => f.toFun) RelHom.coe_fn_injective
[GOAL]
case intro
V : Type u
W : Type v
G : SimpleGraph V
F : SimpleGraph W
inst✝ : Finite W
h : (G' : Subgraph G) → Set.Finite G'.verts → Subgraph.coe G' →g F
val✝ : Fintype W
this✝ : ∀ (G' : (Finsubgraph G)ᵒᵖ), Nonempty ((finsubgraphHomFunctor G F).obj G')
this : (G' : (Finsubgraph G)ᵒᵖ) → Fintype ((finsubgraphHomFunctor G F).obj G')
⊢ Nonempty (G →g F)
[PROOFSTEP]
obtain ⟨u, hu⟩ := nonempty_sections_of_finite_inverse_system (finsubgraphHomFunctor G F)
[GOAL]
case intro.intro
V : Type u
W : Type v
G : SimpleGraph V
F : SimpleGraph W
inst✝ : Finite W
h : (G' : Subgraph G) → Set.Finite G'.verts → Subgraph.coe G' →g F
val✝ : Fintype W
this✝ : ∀ (G' : (Finsubgraph G)ᵒᵖ), Nonempty ((finsubgraphHomFunctor G F).obj G')
this : (G' : (Finsubgraph G)ᵒᵖ) → Fintype ((finsubgraphHomFunctor G F).obj G')
u : (j : (Finsubgraph G)ᵒᵖ) → (finsubgraphHomFunctor G F).obj j
hu : u ∈ Functor.sections (finsubgraphHomFunctor G F)
⊢ Nonempty (G →g F)
[PROOFSTEP]
refine' ⟨⟨fun v => _, _⟩⟩
[GOAL]
case intro.intro.refine'_1
V : Type u
W : Type v
G : SimpleGraph V
F : SimpleGraph W
inst✝ : Finite W
h : (G' : Subgraph G) → Set.Finite G'.verts → Subgraph.coe G' →g F
val✝ : Fintype W
this✝ : ∀ (G' : (Finsubgraph G)ᵒᵖ), Nonempty ((finsubgraphHomFunctor G F).obj G')
this : (G' : (Finsubgraph G)ᵒᵖ) → Fintype ((finsubgraphHomFunctor G F).obj G')
u : (j : (Finsubgraph G)ᵒᵖ) → (finsubgraphHomFunctor G F).obj j
hu : u ∈ Functor.sections (finsubgraphHomFunctor G F)
v : V
⊢ W
[PROOFSTEP]
exact
  (u (Opposite.op (singletonFinsubgraph v))).toFun
    ⟨v, by
      unfold singletonFinsubgraph
      simp⟩
[GOAL]
V : Type u
W : Type v
G : SimpleGraph V
F : SimpleGraph W
inst✝ : Finite W
h : (G' : Subgraph G) → Set.Finite G'.verts → Subgraph.coe G' →g F
val✝ : Fintype W
this✝ : ∀ (G' : (Finsubgraph G)ᵒᵖ), Nonempty ((finsubgraphHomFunctor G F).obj G')
this : (G' : (Finsubgraph G)ᵒᵖ) → Fintype ((finsubgraphHomFunctor G F).obj G')
u : (j : (Finsubgraph G)ᵒᵖ) → (finsubgraphHomFunctor G F).obj j
hu : u ∈ Functor.sections (finsubgraphHomFunctor G F)
v : V
⊢ v ∈ (↑(Opposite.op (singletonFinsubgraph v)).unop).verts
[PROOFSTEP]
unfold singletonFinsubgraph
[GOAL]
V : Type u
W : Type v
G : SimpleGraph V
F : SimpleGraph W
inst✝ : Finite W
h : (G' : Subgraph G) → Set.Finite G'.verts → Subgraph.coe G' →g F
val✝ : Fintype W
this✝ : ∀ (G' : (Finsubgraph G)ᵒᵖ), Nonempty ((finsubgraphHomFunctor G F).obj G')
this : (G' : (Finsubgraph G)ᵒᵖ) → Fintype ((finsubgraphHomFunctor G F).obj G')
u : (j : (Finsubgraph G)ᵒᵖ) → (finsubgraphHomFunctor G F).obj j
hu : u ∈ Functor.sections (finsubgraphHomFunctor G F)
v : V
⊢ v ∈ (↑(Opposite.op { val := SimpleGraph.singletonSubgraph G v, property := (_ : Set.Finite {v}) }).unop).verts
[PROOFSTEP]
simp
[GOAL]
case intro.intro.refine'_2
V : Type u
W : Type v
G : SimpleGraph V
F : SimpleGraph W
inst✝ : Finite W
h : (G' : Subgraph G) → Set.Finite G'.verts → Subgraph.coe G' →g F
val✝ : Fintype W
this✝ : ∀ (G' : (Finsubgraph G)ᵒᵖ), Nonempty ((finsubgraphHomFunctor G F).obj G')
this : (G' : (Finsubgraph G)ᵒᵖ) → Fintype ((finsubgraphHomFunctor G F).obj G')
u : (j : (Finsubgraph G)ᵒᵖ) → (finsubgraphHomFunctor G F).obj j
hu : u ∈ Functor.sections (finsubgraphHomFunctor G F)
⊢ ∀ {a b : V},
    Adj G a b →
      Adj F
        ((fun v =>
            RelHom.toFun (u (Opposite.op (singletonFinsubgraph v)))
              { val := v, property := (_ : v ∈ (↑(Opposite.op (singletonFinsubgraph v)).unop).verts) })
          a)
        ((fun v =>
            RelHom.toFun (u (Opposite.op (singletonFinsubgraph v)))
              { val := v, property := (_ : v ∈ (↑(Opposite.op (singletonFinsubgraph v)).unop).verts) })
          b)
[PROOFSTEP]
intro v v' e
[GOAL]
case intro.intro.refine'_2
V : Type u
W : Type v
G : SimpleGraph V
F : SimpleGraph W
inst✝ : Finite W
h : (G' : Subgraph G) → Set.Finite G'.verts → Subgraph.coe G' →g F
val✝ : Fintype W
this✝ : ∀ (G' : (Finsubgraph G)ᵒᵖ), Nonempty ((finsubgraphHomFunctor G F).obj G')
this : (G' : (Finsubgraph G)ᵒᵖ) → Fintype ((finsubgraphHomFunctor G F).obj G')
u : (j : (Finsubgraph G)ᵒᵖ) → (finsubgraphHomFunctor G F).obj j
hu : u ∈ Functor.sections (finsubgraphHomFunctor G F)
v v' : V
e : Adj G v v'
⊢ Adj F
    ((fun v =>
        RelHom.toFun (u (Opposite.op (singletonFinsubgraph v)))
          { val := v, property := (_ : v ∈ (↑(Opposite.op (singletonFinsubgraph v)).unop).verts) })
      v)
    ((fun v =>
        RelHom.toFun (u (Opposite.op (singletonFinsubgraph v)))
          { val := v, property := (_ : v ∈ (↑(Opposite.op (singletonFinsubgraph v)).unop).verts) })
      v')
[PROOFSTEP]
simp only
  /- The homomorphism for each edge's singleton subgraph agrees with those for its source and
          target vertices. -/
[GOAL]
case intro.intro.refine'_2
V : Type u
W : Type v
G : SimpleGraph V
F : SimpleGraph W
inst✝ : Finite W
h : (G' : Subgraph G) → Set.Finite G'.verts → Subgraph.coe G' →g F
val✝ : Fintype W
this✝ : ∀ (G' : (Finsubgraph G)ᵒᵖ), Nonempty ((finsubgraphHomFunctor G F).obj G')
this : (G' : (Finsubgraph G)ᵒᵖ) → Fintype ((finsubgraphHomFunctor G F).obj G')
u : (j : (Finsubgraph G)ᵒᵖ) → (finsubgraphHomFunctor G F).obj j
hu : u ∈ Functor.sections (finsubgraphHomFunctor G F)
v v' : V
e : Adj G v v'
⊢ Adj F
    (RelHom.toFun (u (Opposite.op (singletonFinsubgraph v)))
      { val := v, property := (_ : v ∈ (↑(Opposite.op (singletonFinsubgraph v)).unop).verts) })
    (RelHom.toFun (u (Opposite.op (singletonFinsubgraph v')))
      { val := v', property := (_ : v' ∈ (↑(Opposite.op (singletonFinsubgraph v')).unop).verts) })
[PROOFSTEP]
have hv : Opposite.op (finsubgraphOfAdj e) ⟶ Opposite.op (singletonFinsubgraph v) :=
  Quiver.Hom.op (CategoryTheory.homOfLE singletonFinsubgraph_le_adj_left)
[GOAL]
case intro.intro.refine'_2
V : Type u
W : Type v
G : SimpleGraph V
F : SimpleGraph W
inst✝ : Finite W
h : (G' : Subgraph G) → Set.Finite G'.verts → Subgraph.coe G' →g F
val✝ : Fintype W
this✝ : ∀ (G' : (Finsubgraph G)ᵒᵖ), Nonempty ((finsubgraphHomFunctor G F).obj G')
this : (G' : (Finsubgraph G)ᵒᵖ) → Fintype ((finsubgraphHomFunctor G F).obj G')
u : (j : (Finsubgraph G)ᵒᵖ) → (finsubgraphHomFunctor G F).obj j
hu : u ∈ Functor.sections (finsubgraphHomFunctor G F)
v v' : V
e : Adj G v v'
hv : Opposite.op (finsubgraphOfAdj e) ⟶ Opposite.op (singletonFinsubgraph v)
⊢ Adj F
    (RelHom.toFun (u (Opposite.op (singletonFinsubgraph v)))
      { val := v, property := (_ : v ∈ (↑(Opposite.op (singletonFinsubgraph v)).unop).verts) })
    (RelHom.toFun (u (Opposite.op (singletonFinsubgraph v')))
      { val := v', property := (_ : v' ∈ (↑(Opposite.op (singletonFinsubgraph v')).unop).verts) })
[PROOFSTEP]
have hv' : Opposite.op (finsubgraphOfAdj e) ⟶ Opposite.op (singletonFinsubgraph v') :=
  Quiver.Hom.op (CategoryTheory.homOfLE singletonFinsubgraph_le_adj_right)
[GOAL]
case intro.intro.refine'_2
V : Type u
W : Type v
G : SimpleGraph V
F : SimpleGraph W
inst✝ : Finite W
h : (G' : Subgraph G) → Set.Finite G'.verts → Subgraph.coe G' →g F
val✝ : Fintype W
this✝ : ∀ (G' : (Finsubgraph G)ᵒᵖ), Nonempty ((finsubgraphHomFunctor G F).obj G')
this : (G' : (Finsubgraph G)ᵒᵖ) → Fintype ((finsubgraphHomFunctor G F).obj G')
u : (j : (Finsubgraph G)ᵒᵖ) → (finsubgraphHomFunctor G F).obj j
hu : u ∈ Functor.sections (finsubgraphHomFunctor G F)
v v' : V
e : Adj G v v'
hv : Opposite.op (finsubgraphOfAdj e) ⟶ Opposite.op (singletonFinsubgraph v)
hv' : Opposite.op (finsubgraphOfAdj e) ⟶ Opposite.op (singletonFinsubgraph v')
⊢ Adj F
    (RelHom.toFun (u (Opposite.op (singletonFinsubgraph v)))
      { val := v, property := (_ : v ∈ (↑(Opposite.op (singletonFinsubgraph v)).unop).verts) })
    (RelHom.toFun (u (Opposite.op (singletonFinsubgraph v')))
      { val := v', property := (_ : v' ∈ (↑(Opposite.op (singletonFinsubgraph v')).unop).verts) })
[PROOFSTEP]
rw [← hu hv, ← hu hv']
  -- porting note: was `apply Hom.map_adj`
[GOAL]
case intro.intro.refine'_2
V : Type u
W : Type v
G : SimpleGraph V
F : SimpleGraph W
inst✝ : Finite W
h : (G' : Subgraph G) → Set.Finite G'.verts → Subgraph.coe G' →g F
val✝ : Fintype W
this✝ : ∀ (G' : (Finsubgraph G)ᵒᵖ), Nonempty ((finsubgraphHomFunctor G F).obj G')
this : (G' : (Finsubgraph G)ᵒᵖ) → Fintype ((finsubgraphHomFunctor G F).obj G')
u : (j : (Finsubgraph G)ᵒᵖ) → (finsubgraphHomFunctor G F).obj j
hu : u ∈ Functor.sections (finsubgraphHomFunctor G F)
v v' : V
e : Adj G v v'
hv : Opposite.op (finsubgraphOfAdj e) ⟶ Opposite.op (singletonFinsubgraph v)
hv' : Opposite.op (finsubgraphOfAdj e) ⟶ Opposite.op (singletonFinsubgraph v')
⊢ Adj F
    (RelHom.toFun ((finsubgraphHomFunctor G F).map hv (u (Opposite.op (finsubgraphOfAdj e))))
      { val := v, property := (_ : v ∈ (↑(Opposite.op (singletonFinsubgraph v)).unop).verts) })
    (RelHom.toFun ((finsubgraphHomFunctor G F).map hv' (u (Opposite.op (finsubgraphOfAdj e))))
      { val := v', property := (_ : v' ∈ (↑(Opposite.op (singletonFinsubgraph v')).unop).verts) })
[PROOFSTEP]
refine'
  Hom.map_adj (u (Opposite.op (finsubgraphOfAdj e)))
    _
      -- `v` and `v'` are definitionally adjacent in `finsubgraphOfAdj e`
[GOAL]
case intro.intro.refine'_2
V : Type u
W : Type v
G : SimpleGraph V
F : SimpleGraph W
inst✝ : Finite W
h : (G' : Subgraph G) → Set.Finite G'.verts → Subgraph.coe G' →g F
val✝ : Fintype W
this✝ : ∀ (G' : (Finsubgraph G)ᵒᵖ), Nonempty ((finsubgraphHomFunctor G F).obj G')
this : (G' : (Finsubgraph G)ᵒᵖ) → Fintype ((finsubgraphHomFunctor G F).obj G')
u : (j : (Finsubgraph G)ᵒᵖ) → (finsubgraphHomFunctor G F).obj j
hu : u ∈ Functor.sections (finsubgraphHomFunctor G F)
v v' : V
e : Adj G v v'
hv : Opposite.op (finsubgraphOfAdj e) ⟶ Opposite.op (singletonFinsubgraph v)
hv' : Opposite.op (finsubgraphOfAdj e) ⟶ Opposite.op (singletonFinsubgraph v')
⊢ Adj (Subgraph.coe ↑(Opposite.op (finsubgraphOfAdj e)).unop)
    { val := v, property := (_ : v ∈ (↑(Opposite.op (finsubgraphOfAdj e)).unop).verts) }
    { val := v', property := (_ : v' ∈ (↑(Opposite.op (finsubgraphOfAdj e)).unop).verts) }
[PROOFSTEP]
simp [finsubgraphOfAdj]