-- Mathlib/Combinatorics/SimpleGraph/Clique.lean
theorem isClique_iff_induce_eq : G.IsClique s ↔ G.induce s = ⊤

Proof state:
α : Type u_1
G : SimpleGraph α
s : Set α
⊢ G.IsClique s ↔ induce s G = ⊤

Tactic:
rw [isClique_iff]

Result:
α : Type u_1
G : SimpleGraph α
s : Set α
⊢ s.Pairwise G.Adj ↔ induce s G = ⊤

Proof state:
case mpr
α : Type u_1
G : SimpleGraph α
s : Set α
⊢ induce s G = ⊤ → s.Pairwise G.Adj

Tactic:
intro h v hv w hw hne

Result:
case mpr
α : Type u_1
G : SimpleGraph α
s : Set α
h : induce s G = ⊤
v : α
hv : v ∈ s
w : α
hw : w ∈ s
hne : v ≠ w
⊢ G.Adj v w

Proof state:
case mpr
α : Type u_1
G : SimpleGraph α
s : Set α
h : induce s G = ⊤
v : α
hv : v ∈ s
w : α
hw : w ∈ s
hne : v ≠ w
h2 : ⊤.Adj ⟨v, hv⟩ ⟨w, hw⟩ = (induce s G).Adj ⟨v, hv⟩ ⟨w, hw⟩
⊢ G.Adj v w

Tactic:
simp only [top_adj, ne_eq, Subtype.mk.injEq, eq_iff_iff] at h2

Result:
case mpr
α : Type u_1
G : SimpleGraph α
s : Set α
h : induce s G = ⊤
v : α
hv : v ∈ s
w : α
hw : w ∈ s
hne : v ≠ w
h2 : ¬v = w ↔ (induce s G).Adj ⟨v, hv⟩ ⟨w, hw⟩
⊢ G.Adj v w

Proof state:
case mp.Adj.h.mk.h.mk.a
α : Type u_1
G : SimpleGraph α
s : Set α
h : s.Pairwise G.Adj
v : α
hv : v ∈ s
w : α
hw : w ∈ s
⊢ G.Adj ((Embedding.subtype fun x => x ∈ s) ⟨v, hv⟩) ((Embedding.subtype fun x => x ∈ s) ⟨w, hw⟩) ↔ ¬v = w

Tactic:
exact ⟨Adj.ne, h hv hw⟩

Result:
no goals

Proof state:
case mp
α : Type u_1
G : SimpleGraph α
s : Set α
⊢ s.Pairwise G.Adj → induce s G = ⊤

Tactic:
intro h

Result:
case mp
α : Type u_1
G : SimpleGraph α
s : Set α
h : s.Pairwise G.Adj
⊢ induce s G = ⊤

Proof state:
α : Type u_1
G : SimpleGraph α
s : Set α
⊢ s.Pairwise G.Adj ↔ induce s G = ⊤

Tactic:
constructor

Result:
case mp
α : Type u_1
G : SimpleGraph α
s : Set α
⊢ s.Pairwise G.Adj → induce s G = ⊤

case mpr
α : Type u_1
G : SimpleGraph α
s : Set α
⊢ induce s G = ⊤ → s.Pairwise G.Adj

Proof state:
case mpr
α : Type u_1
G : SimpleGraph α
s : Set α
h : induce s G = ⊤
v : α
hv : v ∈ s
w : α
hw : w ∈ s
hne : v ≠ w
h2 : ¬v = w ↔ (induce s G).Adj ⟨v, hv⟩ ⟨w, hw⟩
⊢ G.Adj v w

Tactic:
exact h2.1 hne

Result:
no goals

Proof state:
case mpr
α : Type u_1
G : SimpleGraph α
s : Set α
h : induce s G = ⊤
v : α
hv : v ∈ s
w : α
hw : w ∈ s
hne : v ≠ w
h2 : (induce s G).Adj ⟨v, hv⟩ ⟨w, hw⟩ = (induce s G).Adj ⟨v, hv⟩ ⟨w, hw⟩
⊢ G.Adj v w

Tactic:
conv_lhs at h2 => rw [h]

Result:
case mpr
α : Type u_1
G : SimpleGraph α
s : Set α
h : induce s G = ⊤
v : α
hv : v ∈ s
w : α
hw : w ∈ s
hne : v ≠ w
h2 : ⊤.Adj ⟨v, hv⟩ ⟨w, hw⟩ = (induce s G).Adj ⟨v, hv⟩ ⟨w, hw⟩
⊢ G.Adj v w

Proof state:
case mp
α : Type u_1
G : SimpleGraph α
s : Set α
h : s.Pairwise G.Adj
⊢ induce s G = ⊤

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

Result:
case mp.Adj.h.mk.h.mk.a
α : Type u_1
G : SimpleGraph α
s : Set α
h : s.Pairwise G.Adj
v : α
hv : v ∈ s
w : α
hw : w ∈ s
⊢ (induce s G).Adj ⟨v, hv⟩ ⟨w, hw⟩ ↔ ⊤.Adj ⟨v, hv⟩ ⟨w, hw⟩

Proof state:
case mpr
α : Type u_1
G : SimpleGraph α
s : Set α
h : induce s G = ⊤
v : α
hv : v ∈ s
w : α
hw : w ∈ s
hne : v ≠ w
⊢ G.Adj v w

Tactic:
have h2 : (G.induce s).Adj ⟨v, hv⟩ ⟨w, hw⟩ = _ := rfl

Result:
case mpr
α : Type u_1
G : SimpleGraph α
s : Set α
h : induce s G = ⊤
v : α
hv : v ∈ s
w : α
hw : w ∈ s
hne : v ≠ w
h2 : (induce s G).Adj ⟨v, hv⟩ ⟨w, hw⟩ = (induce s G).Adj ⟨v, hv⟩ ⟨w, hw⟩
⊢ G.Adj v w

Proof state:
case mp.Adj.h.mk.h.mk.a
α : Type u_1
G : SimpleGraph α
s : Set α
h : s.Pairwise G.Adj
v : α
hv : v ∈ s
w : α
hw : w ∈ s
⊢ (induce s G).Adj ⟨v, hv⟩ ⟨w, hw⟩ ↔ ⊤.Adj ⟨v, hv⟩ ⟨w, hw⟩

Tactic:
simp only [comap_adj, Subtype.coe_mk, top_adj, Ne, Subtype.mk_eq_mk]

Result:
case mp.Adj.h.mk.h.mk.a
α : Type u_1
G : SimpleGraph α
s : Set α
h : s.Pairwise G.Adj
v : α
hv : v ∈ s
w : α
hw : w ∈ s
⊢ G.Adj ((Embedding.subtype fun x => x ∈ s) ⟨v, hv⟩) ((Embedding.subtype fun x => x ∈ s) ⟨w, hw⟩) ↔ ¬v = w