case intro.intro.intro.intro
ι : Sort ?u.241583
𝕜 : Type ?u.241586
V : Type u
W : Type v
X : Type w
G✝ : SimpleGraph V
G'✝ : SimpleGraph W
a b c u✝ v✝ w : V
e : Sym2 V
f : V ↪ W
G : SimpleGraph V
G' : SimpleGraph W
h : G ≤ SimpleGraph.comap (↑f) G'
u v : V
ha : Adj G u v
⊢ Adj G' (↑f u) (↑f v)
ι : Sort ?u.241583
𝕜 : Type ?u.241586
V : Type u
W : Type v
X : Type w
G✝ : SimpleGraph V
G'✝ : SimpleGraph W
a b c u v w : V
e : Sym2 V
f : V ↪ W
G : SimpleGraph V
G' : SimpleGraph W
⊢ G ≤ SimpleGraph.comap (↑f) G' → SimpleGraph.map f G ≤ G'
rintro h _ _ ⟨u, v, ha, rfl, rfl⟩
no goals
case intro.intro.intro.intro
ι : Sort ?u.241583
𝕜 : Type ?u.241586
V : Type u
W : Type v
X : Type w
G✝ : SimpleGraph V
G'✝ : SimpleGraph W
a b c u✝ v✝ w : V
e : Sym2 V
f : V ↪ W
G : SimpleGraph V
G' : SimpleGraph W
h : G ≤ SimpleGraph.comap (↑f) G'
u v : V
ha : Adj G u v
⊢ Adj G' (↑f u) (↑f v)
exact h ha