case refine'_1
ι : Sort ?u.168978
V : Type u
W : Type v
G : SimpleGraph V
G₁ G₂ : Subgraph G
a b : V
G' : SimpleGraph W
f : G →g G'
H : Subgraph G
H' : Subgraph G'
h : Subgraph.map f H ≤ H'
v : V
hv : v ∈ H.verts
⊢ v ∈ (Subgraph.comap f H').verts

case refine'_2
ι : Sort ?u.168978
V : Type u
W : Type v
G : SimpleGraph V
G₁ G₂ : Subgraph G
a b : V
G' : SimpleGraph W
f : G →g G'
H : Subgraph G
H' : Subgraph G'
h : Subgraph.map f H ≤ H'
v w : V
hvw : Adj H v w
⊢ Adj (Subgraph.comap f H') v w

case refine'_3
ι : Sort ?u.168978
V : Type u
W : Type v
G : SimpleGraph V
G₁ G₂ : Subgraph G
a b : V
G' : SimpleGraph W
f : G →g G'
H : Subgraph G
H' : Subgraph G'
h : H ≤ Subgraph.comap f H'
v : W
⊢ v ∈ (Subgraph.map f H).verts → v ∈ H'.verts

case refine'_4
ι : Sort ?u.168978
V : Type u
W : Type v
G : SimpleGraph V
G₁ G₂ : Subgraph G
a b : V
G' : SimpleGraph W
f : G →g G'
H : Subgraph G
H' : Subgraph G'
h : H ≤ Subgraph.comap f H'
v w : W
⊢ Adj (Subgraph.map f H) v w → Adj H' v w
ι : Sort ?u.168978
V : Type u
W : Type v
G : SimpleGraph V
G₁ G₂ : Subgraph G
a b : V
G' : SimpleGraph W
f : G →g G'
H : Subgraph G
H' : Subgraph G'
⊢ Subgraph.map f H ≤ H' ↔ H ≤ Subgraph.comap f H'
refine' ⟨fun h ↦ ⟨fun v hv ↦ _, fun v w hvw ↦ _⟩, fun h ↦ ⟨fun v ↦ _, fun v w ↦ _⟩⟩
case refine'_1
ι : Sort ?u.168978
V : Type u
W : Type v
G : SimpleGraph V
G₁ G₂ : Subgraph G
a b : V
G' : SimpleGraph W
f : G →g G'
H : Subgraph G
H' : Subgraph G'
h : Subgraph.map f H ≤ H'
v : V
hv : v ∈ H.verts
⊢ ↑f v ∈ H'.verts
case refine'_1
ι : Sort ?u.168978
V : Type u
W : Type v
G : SimpleGraph V
G₁ G₂ : Subgraph G
a b : V
G' : SimpleGraph W
f : G →g G'
H : Subgraph G
H' : Subgraph G'
h : Subgraph.map f H ≤ H'
v : V
hv : v ∈ H.verts
⊢ v ∈ (Subgraph.comap f H').verts
simp only [comap_verts, Set.mem_preimage]
no goals
case refine'_1
ι : Sort ?u.168978
V : Type u
W : Type v
G : SimpleGraph V
G₁ G₂ : Subgraph G
a b : V
G' : SimpleGraph W
f : G →g G'
H : Subgraph G
H' : Subgraph G'
h : Subgraph.map f H ≤ H'
v : V
hv : v ∈ H.verts
⊢ ↑f v ∈ H'.verts
exact h.1 ⟨v, hv, rfl⟩
case refine'_2
ι : Sort ?u.168978
V : Type u
W : Type v
G : SimpleGraph V
G₁ G₂ : Subgraph G
a b : V
G' : SimpleGraph W
f : G →g G'
H : Subgraph G
H' : Subgraph G'
h : Subgraph.map f H ≤ H'
v w : V
hvw : Adj H v w
⊢ Adj H' (↑f v) (↑f w)
case refine'_2
ι : Sort ?u.168978
V : Type u
W : Type v
G : SimpleGraph V
G₁ G₂ : Subgraph G
a b : V
G' : SimpleGraph W
f : G →g G'
H : Subgraph G
H' : Subgraph G'
h : Subgraph.map f H ≤ H'
v w : V
hvw : Adj H v w
⊢ Adj (Subgraph.comap f H') v w
simp only [H.adj_sub hvw, comap_Adj, true_and_iff]
no goals
case refine'_2
ι : Sort ?u.168978
V : Type u
W : Type v
G : SimpleGraph V
G₁ G₂ : Subgraph G
a b : V
G' : SimpleGraph W
f : G →g G'
H : Subgraph G
H' : Subgraph G'
h : Subgraph.map f H ≤ H'
v w : V
hvw : Adj H v w
⊢ Adj H' (↑f v) (↑f w)
exact h.2 ⟨v, w, hvw, rfl, rfl⟩
case refine'_3
ι : Sort ?u.168978
V : Type u
W : Type v
G : SimpleGraph V
G₁ G₂ : Subgraph G
a b : V
G' : SimpleGraph W
f : G →g G'
H : Subgraph G
H' : Subgraph G'
h : H ≤ Subgraph.comap f H'
v : W
⊢ ∀ (x : V), x ∈ H.verts → ↑f x = v → v ∈ H'.verts
case refine'_3
ι : Sort ?u.168978
V : Type u
W : Type v
G : SimpleGraph V
G₁ G₂ : Subgraph G
a b : V
G' : SimpleGraph W
f : G →g G'
H : Subgraph G
H' : Subgraph G'
h : H ≤ Subgraph.comap f H'
v : W
⊢ v ∈ (Subgraph.map f H).verts → v ∈ H'.verts
simp only [map_verts, Set.mem_image, forall_exists_index, and_imp]
case refine'_3
ι : Sort ?u.168978
V : Type u
W : Type v
G : SimpleGraph V
G₁ G₂ : Subgraph G
a b : V
G' : SimpleGraph W
f : G →g G'
H : Subgraph G
H' : Subgraph G'
h : H ≤ Subgraph.comap f H'
w : V
hw : w ∈ H.verts
⊢ ↑f w ∈ H'.verts
case refine'_3
ι : Sort ?u.168978
V : Type u
W : Type v
G : SimpleGraph V
G₁ G₂ : Subgraph G
a b : V
G' : SimpleGraph W
f : G →g G'
H : Subgraph G
H' : Subgraph G'
h : H ≤ Subgraph.comap f H'
v : W
⊢ ∀ (x : V), x ∈ H.verts → ↑f x = v → v ∈ H'.verts
rintro w hw rfl
no goals
case refine'_3
ι : Sort ?u.168978
V : Type u
W : Type v
G : SimpleGraph V
G₁ G₂ : Subgraph G
a b : V
G' : SimpleGraph W
f : G →g G'
H : Subgraph G
H' : Subgraph G'
h : H ≤ Subgraph.comap f H'
w : V
hw : w ∈ H.verts
⊢ ↑f w ∈ H'.verts
exact h.1 hw
case refine'_4
ι : Sort ?u.168978
V : Type u
W : Type v
G : SimpleGraph V
G₁ G₂ : Subgraph G
a b : V
G' : SimpleGraph W
f : G →g G'
H : Subgraph G
H' : Subgraph G'
h : H ≤ Subgraph.comap f H'
v w : W
⊢ ∀ (x x_1 : V), Adj H x x_1 → ↑f x = v → ↑f x_1 = w → Adj H' v w
case refine'_4
ι : Sort ?u.168978
V : Type u
W : Type v
G : SimpleGraph V
G₁ G₂ : Subgraph G
a b : V
G' : SimpleGraph W
f : G →g G'
H : Subgraph G
H' : Subgraph G'
h : H ≤ Subgraph.comap f H'
v w : W
⊢ Adj (Subgraph.map f H) v w → Adj H' v w
simp only [Relation.Map, map_Adj, forall_exists_index, and_imp]
case refine'_4
ι : Sort ?u.168978
V : Type u
W : Type v
G : SimpleGraph V
G₁ G₂ : Subgraph G
a b : V
G' : SimpleGraph W
f : G →g G'
H : Subgraph G
H' : Subgraph G'
h : H ≤ Subgraph.comap f H'
u u' : V
hu : Adj H u u'
⊢ Adj H' (↑f u) (↑f u')
case refine'_4
ι : Sort ?u.168978
V : Type u
W : Type v
G : SimpleGraph V
G₁ G₂ : Subgraph G
a b : V
G' : SimpleGraph W
f : G →g G'
H : Subgraph G
H' : Subgraph G'
h : H ≤ Subgraph.comap f H'
v w : W
⊢ ∀ (x x_1 : V), Adj H x x_1 → ↑f x = v → ↑f x_1 = w → Adj H' v w
rintro u u' hu rfl rfl
no goals
case refine'_4
ι : Sort ?u.168978
V : Type u
W : Type v
G : SimpleGraph V
G₁ G₂ : Subgraph G
a b : V
G' : SimpleGraph W
f : G →g G'
H : Subgraph G
H' : Subgraph G'
h : H ≤ Subgraph.comap f H'
u u' : V
hu : Adj H u u'
⊢ Adj H' (↑f u) (↑f u')
exact (h.2 hu).2