α : Type u_1
G H : SimpleGraph α
s t : Set α
⊢ Set.Pairwise s G.Adj ↔ induce s G = ⊤
α : Type u_1
G H : SimpleGraph α
s t : Set α
⊢ IsClique G s ↔ induce s G = ⊤
rw [isClique_iff]
case mp
α : Type u_1
G H : SimpleGraph α
s t : Set α
⊢ Set.Pairwise s G.Adj → induce s G = ⊤

case mpr
α : Type u_1
G H : SimpleGraph α
s t : Set α
⊢ induce s G = ⊤ → Set.Pairwise s G.Adj
α : Type u_1
G H : SimpleGraph α
s t : Set α
⊢ Set.Pairwise s G.Adj ↔ induce s G = ⊤
constructor
case mp
α : Type u_1
G H : SimpleGraph α
s t : Set α
h : Set.Pairwise s G.Adj
⊢ induce s G = ⊤
case mp
α : Type u_1
G H : SimpleGraph α
s t : Set α
⊢ Set.Pairwise s G.Adj → induce s G = ⊤
intro h
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 }
case mp
α : Type u_1
G H : SimpleGraph α
s t : Set α
h : Set.Pairwise s G.Adj
⊢ induce s G = ⊤
ext ⟨v, hv⟩ ⟨w, hw⟩
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
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 }
simp only [comap_Adj, Subtype.coe_mk, top_adj, Ne.def, Subtype.mk_eq_mk]
no goals
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
exact ⟨Adj.ne, h hv hw⟩
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
case mpr
α : Type u_1
G H : SimpleGraph α
s t : Set α
⊢ induce s G = ⊤ → Set.Pairwise s G.Adj
intro h v hv w hw hne
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
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
have h2 : (G.induce s).Adj ⟨v, hv⟩ ⟨w, hw⟩ = _ := rfl
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
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
conv_lhs at h2 => rw [h]
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
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
simp only [top_adj, ne_eq, Subtype.mk.injEq, eq_iff_iff] at h2
no goals
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
exact h2.1 hne