-- Mathlib/Combinatorics/SimpleGraph/Subgraph.lean
theorem subgraphOfAdj_eq_induce {v w : V} (hvw : G.Adj v w) :
    G.subgraphOfAdj hvw = (⊤ : G.Subgraph).induce {v, w}

Proof state:
case Adj.h.h.a.mpr
V : Type u
G : SimpleGraph V
v w : V
hvw : G.Adj v w
x✝¹ x✝ : V
⊢ (⊤.induce {v, w}).Adj x✝¹ x✝ → (G.subgraphOfAdj hvw).Adj x✝¹ x✝

Tactic:
intro h

Result:
case Adj.h.h.a.mpr
V : Type u
G : SimpleGraph V
v w : V
hvw : G.Adj v w
x✝¹ x✝ : V
h : (⊤.induce {v, w}).Adj x✝¹ x✝
⊢ (G.subgraphOfAdj hvw).Adj x✝¹ x✝

Proof state:
case Adj.h.h.a.mpr.intro.inr.intro.inl
V : Type u
G : SimpleGraph V
x✝¹ x✝ : V
ha : G.Adj x✝¹ x✝
hvw : G.Adj x✝ x✝¹
⊢ (G.subgraphOfAdj hvw).Adj x✝¹ x✝

Tactic:
simp

Result:
no goals

Proof state:
case Adj.h.h.a.mp
V : Type u
G : SimpleGraph V
v w : V
hvw : G.Adj v w
x✝¹ x✝ : V
h : (G.subgraphOfAdj hvw).Adj x✝¹ x✝
⊢ (⊤.induce {v, w}).Adj x✝¹ x✝

Tactic:
simp only [subgraphOfAdj_adj, Sym2.eq, Sym2.rel_iff] at h

Result:
case Adj.h.h.a.mp
V : Type u
G : SimpleGraph V
v w : V
hvw : G.Adj v w
x✝¹ x✝ : V
h : v = x✝¹ ∧ w = x✝ ∨ v = x✝ ∧ w = x✝¹
⊢ (⊤.induce {v, w}).Adj x✝¹ x✝

Proof state:
case Adj.h.h.a.mp
V : Type u
G : SimpleGraph V
v w : V
hvw : G.Adj v w
x✝¹ x✝ : V
h : v = x✝¹ ∧ w = x✝ ∨ v = x✝ ∧ w = x✝¹
⊢ (⊤.induce {v, w}).Adj x✝¹ x✝

Tactic:
obtain ⟨rfl, rfl⟩ | ⟨rfl, rfl⟩ := h <;> simp [hvw, hvw.symm]

Result:
no goals

Proof state:
case Adj.h.h.a.mpr
V : Type u
G : SimpleGraph V
v w : V
hvw : G.Adj v w
x✝¹ x✝ : V
h : (⊤.induce {v, w}).Adj x✝¹ x✝
⊢ (G.subgraphOfAdj hvw).Adj x✝¹ x✝

Tactic:
simp only [induce_adj, Set.mem_insert_iff, Set.mem_singleton_iff, top_adj] at h

Result:
case Adj.h.h.a.mpr
V : Type u
G : SimpleGraph V
v w : V
hvw : G.Adj v w
x✝¹ x✝ : V
h : (x✝¹ = v ∨ x✝¹ = w) ∧ (x✝ = v ∨ x✝ = w) ∧ G.Adj x✝¹ x✝
⊢ (G.subgraphOfAdj hvw).Adj x✝¹ x✝

Proof state:
case verts.h
V : Type u
G : SimpleGraph V
v w : V
hvw : G.Adj v w
x✝ : V
⊢ x✝ ∈ (G.subgraphOfAdj hvw).verts ↔ x✝ ∈ (⊤.induce {v, w}).verts

Tactic:
simp

Result:
no goals

Proof state:
V : Type u
G : SimpleGraph V
v w : V
hvw : G.Adj v w
⊢ G.subgraphOfAdj hvw = ⊤.induce {v, w}

Tactic:
ext

Result:
case verts.h
V : Type u
G : SimpleGraph V
v w : V
hvw : G.Adj v w
x✝ : V
⊢ x✝ ∈ (G.subgraphOfAdj hvw).verts ↔ x✝ ∈ (⊤.induce {v, w}).verts

case Adj.h.h.a
V : Type u
G : SimpleGraph V
v w : V
hvw : G.Adj v w
x✝¹ x✝ : V
⊢ (G.subgraphOfAdj hvw).Adj x✝¹ x✝ ↔ (⊤.induce {v, w}).Adj x✝¹ x✝

Proof state:
case Adj.h.h.a
V : Type u
G : SimpleGraph V
v w : V
hvw : G.Adj v w
x✝¹ x✝ : V
⊢ (G.subgraphOfAdj hvw).Adj x✝¹ x✝ ↔ (⊤.induce {v, w}).Adj x✝¹ x✝

Tactic:
constructor

Result:
case Adj.h.h.a.mp
V : Type u
G : SimpleGraph V
v w : V
hvw : G.Adj v w
x✝¹ x✝ : V
⊢ (G.subgraphOfAdj hvw).Adj x✝¹ x✝ → (⊤.induce {v, w}).Adj x✝¹ x✝

case Adj.h.h.a.mpr
V : Type u
G : SimpleGraph V
v w : V
hvw : G.Adj v w
x✝¹ x✝ : V
⊢ (⊤.induce {v, w}).Adj x✝¹ x✝ → (G.subgraphOfAdj hvw).Adj x✝¹ x✝

Proof state:
case Adj.h.h.a.mpr
V : Type u
G : SimpleGraph V
v w : V
hvw : G.Adj v w
x✝¹ x✝ : V
h : (x✝¹ = v ∨ x✝¹ = w) ∧ (x✝ = v ∨ x✝ = w) ∧ G.Adj x✝¹ x✝
⊢ (G.subgraphOfAdj hvw).Adj x✝¹ x✝

Tactic:
obtain ⟨rfl | rfl, rfl | rfl, ha⟩ := h <;> first |exact (ha.ne rfl).elim|simp

Result:
no goals

Proof state:
case Adj.h.h.a.mp
V : Type u
G : SimpleGraph V
v w : V
hvw : G.Adj v w
x✝¹ x✝ : V
⊢ (G.subgraphOfAdj hvw).Adj x✝¹ x✝ → (⊤.induce {v, w}).Adj x✝¹ x✝

Tactic:
intro h

Result:
case Adj.h.h.a.mp
V : Type u
G : SimpleGraph V
v w : V
hvw : G.Adj v w
x✝¹ x✝ : V
h : (G.subgraphOfAdj hvw).Adj x✝¹ x✝
⊢ (⊤.induce {v, w}).Adj x✝¹ x✝

Proof state:
case Adj.h.h.a.mpr.intro.inr.intro.inr
V : Type u
G : SimpleGraph V
v x✝ : V
hvw : G.Adj v x✝
ha : G.Adj x✝ x✝
⊢ (G.subgraphOfAdj hvw).Adj x✝ x✝

Tactic:
exact (ha.ne rfl).elim

Result:
no goals