case verts.h
ι : Sort ?u.263704
V : Type u
W : Type v
G : SimpleGraph V
G' G'' : Subgraph G
s s' : Set V
v w : V
hvw : SimpleGraph.Adj G v w
x✝ : V
⊢ x✝ ∈ (subgraphOfAdj G hvw).verts ↔ x✝ ∈ (induce ⊤ {v, w}).verts

case Adj.h.h.a
ι : Sort ?u.263704
V : Type u
W : Type v
G : SimpleGraph V
G' G'' : Subgraph G
s s' : Set V
v w : V
hvw : SimpleGraph.Adj G v w
x✝¹ x✝ : V
⊢ Adj (subgraphOfAdj G hvw) x✝¹ x✝ ↔ Adj (induce ⊤ {v, w}) x✝¹ x✝
ι : Sort ?u.263704
V : Type u
W : Type v
G : SimpleGraph V
G' G'' : Subgraph G
s s' : Set V
v w : V
hvw : SimpleGraph.Adj G v w
⊢ subgraphOfAdj G hvw = induce ⊤ {v, w}
ext
no goals
case verts.h
ι : Sort ?u.263704
V : Type u
W : Type v
G : SimpleGraph V
G' G'' : Subgraph G
s s' : Set V
v w : V
hvw : SimpleGraph.Adj G v w
x✝ : V
⊢ x✝ ∈ (subgraphOfAdj G hvw).verts ↔ x✝ ∈ (induce ⊤ {v, w}).verts
simp
case Adj.h.h.a.mp
ι : Sort ?u.263704
V : Type u
W : Type v
G : SimpleGraph V
G' G'' : Subgraph G
s s' : Set V
v w : V
hvw : SimpleGraph.Adj G v w
x✝¹ x✝ : V
⊢ Adj (subgraphOfAdj G hvw) x✝¹ x✝ → Adj (induce ⊤ {v, w}) x✝¹ x✝

case Adj.h.h.a.mpr
ι : Sort ?u.263704
V : Type u
W : Type v
G : SimpleGraph V
G' G'' : Subgraph G
s s' : Set V
v w : V
hvw : SimpleGraph.Adj G v w
x✝¹ x✝ : V
⊢ Adj (induce ⊤ {v, w}) x✝¹ x✝ → Adj (subgraphOfAdj G hvw) x✝¹ x✝
case Adj.h.h.a
ι : Sort ?u.263704
V : Type u
W : Type v
G : SimpleGraph V
G' G'' : Subgraph G
s s' : Set V
v w : V
hvw : SimpleGraph.Adj G v w
x✝¹ x✝ : V
⊢ Adj (subgraphOfAdj G hvw) x✝¹ x✝ ↔ Adj (induce ⊤ {v, w}) x✝¹ x✝
constructor
case Adj.h.h.a.mp
ι : Sort ?u.263704
V : Type u
W : Type v
G : SimpleGraph V
G' G'' : Subgraph G
s s' : Set V
v w : V
hvw : SimpleGraph.Adj G v w
x✝¹ x✝ : V
h : Adj (subgraphOfAdj G hvw) x✝¹ x✝
⊢ Adj (induce ⊤ {v, w}) x✝¹ x✝
case Adj.h.h.a.mp
ι : Sort ?u.263704
V : Type u
W : Type v
G : SimpleGraph V
G' G'' : Subgraph G
s s' : Set V
v w : V
hvw : SimpleGraph.Adj G v w
x✝¹ x✝ : V
⊢ Adj (subgraphOfAdj G hvw) x✝¹ x✝ → Adj (induce ⊤ {v, w}) x✝¹ x✝
intro h
case Adj.h.h.a.mp
ι : Sort ?u.263704
V : Type u
W : Type v
G : SimpleGraph V
G' G'' : Subgraph G
s s' : Set V
v w : V
hvw : SimpleGraph.Adj G v w
x✝¹ x✝ : V
h : v = x✝¹ ∧ w = x✝ ∨ v = x✝ ∧ w = x✝¹
⊢ Adj (induce ⊤ {v, w}) x✝¹ x✝
case Adj.h.h.a.mp
ι : Sort ?u.263704
V : Type u
W : Type v
G : SimpleGraph V
G' G'' : Subgraph G
s s' : Set V
v w : V
hvw : SimpleGraph.Adj G v w
x✝¹ x✝ : V
h : Adj (subgraphOfAdj G hvw) x✝¹ x✝
⊢ Adj (induce ⊤ {v, w}) x✝¹ x✝
simp only [subgraphOfAdj_Adj, Quotient.eq, Sym2.rel_iff] at h
no goals
case Adj.h.h.a.mp
ι : Sort ?u.263704
V : Type u
W : Type v
G : SimpleGraph V
G' G'' : Subgraph G
s s' : Set V
v w : V
hvw : SimpleGraph.Adj G v w
x✝¹ x✝ : V
h : v = x✝¹ ∧ w = x✝ ∨ v = x✝ ∧ w = x✝¹
⊢ Adj (induce ⊤ {v, w}) x✝¹ x✝
obtain ⟨rfl, rfl⟩ | ⟨rfl, rfl⟩ := h <;> simp [hvw, hvw.symm]
case Adj.h.h.a.mpr
ι : Sort ?u.263704
V : Type u
W : Type v
G : SimpleGraph V
G' G'' : Subgraph G
s s' : Set V
v w : V
hvw : SimpleGraph.Adj G v w
x✝¹ x✝ : V
h : Adj (induce ⊤ {v, w}) x✝¹ x✝
⊢ Adj (subgraphOfAdj G hvw) x✝¹ x✝
case Adj.h.h.a.mpr
ι : Sort ?u.263704
V : Type u
W : Type v
G : SimpleGraph V
G' G'' : Subgraph G
s s' : Set V
v w : V
hvw : SimpleGraph.Adj G v w
x✝¹ x✝ : V
⊢ Adj (induce ⊤ {v, w}) x✝¹ x✝ → Adj (subgraphOfAdj G hvw) x✝¹ x✝
intro h
case Adj.h.h.a.mpr
ι : Sort ?u.263704
V : Type u
W : Type v
G : SimpleGraph V
G' G'' : Subgraph G
s s' : Set V
v w : V
hvw : SimpleGraph.Adj G v w
x✝¹ x✝ : V
h : (x✝¹ = v ∨ x✝¹ = w) ∧ (x✝ = v ∨ x✝ = w) ∧ SimpleGraph.Adj G x✝¹ x✝
⊢ Adj (subgraphOfAdj G hvw) x✝¹ x✝
case Adj.h.h.a.mpr
ι : Sort ?u.263704
V : Type u
W : Type v
G : SimpleGraph V
G' G'' : Subgraph G
s s' : Set V
v w : V
hvw : SimpleGraph.Adj G v w
x✝¹ x✝ : V
h : Adj (induce ⊤ {v, w}) x✝¹ x✝
⊢ Adj (subgraphOfAdj G hvw) x✝¹ x✝
simp only [induce_Adj, Set.mem_insert_iff, Set.mem_singleton_iff, top_adj] at h
no goals
case Adj.h.h.a.mpr
ι : Sort ?u.263704
V : Type u
W : Type v
G : SimpleGraph V
G' G'' : Subgraph G
s s' : Set V
v w : V
hvw : SimpleGraph.Adj G v w
x✝¹ x✝ : V
h : (x✝¹ = v ∨ x✝¹ = w) ∧ (x✝ = v ∨ x✝ = w) ∧ SimpleGraph.Adj G x✝¹ x✝
⊢ Adj (subgraphOfAdj G hvw) x✝¹ x✝
obtain ⟨rfl | rfl, rfl | rfl, ha⟩ := h <;> first |exact (ha.ne rfl).elim|simp
no goals
case Adj.h.h.a.mpr.intro.inr.intro.inr
ι : Sort ?u.263704
V : Type u
W : Type v
G : SimpleGraph V
G' G'' : Subgraph G
s s' : Set V
v x✝ : V
hvw : SimpleGraph.Adj G v x✝
ha : SimpleGraph.Adj G x✝ x✝
⊢ Adj (subgraphOfAdj G hvw) x✝ x✝
exact (ha.ne rfl).elim
no goals
case Adj.h.h.a.mpr.intro.inr.intro.inl
ι : Sort ?u.263704
V : Type u
W : Type v
G : SimpleGraph V
G' G'' : Subgraph G
s s' : Set V
x✝¹ x✝ : V
ha : SimpleGraph.Adj G x✝¹ x✝
hvw : SimpleGraph.Adj G x✝ x✝¹
⊢ Adj (subgraphOfAdj G hvw) x✝¹ x✝
simp