case right
ι : Sort ?u.226800
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
u v : V
h : Adj G u v
⊢ ∀ ⦃v_1 w : V⦄, ⊥ → u = v_1 ∧ v = w ∨ u = w ∧ v = v_1
ι : Sort ?u.226800
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
u v : V
h : Adj G u v
⊢ SimpleGraph.singletonSubgraph G u ≤ subgraphOfAdj G h
constructor <;> simp [-Set.bot_eq_empty]
no goals
case right
ι : Sort ?u.226800
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
u v : V
h : Adj G u v
⊢ ∀ ⦃v_1 w : V⦄, ⊥ → u = v_1 ∧ v = w ∨ u = w ∧ v = v_1
exact fun _ _ ↦ False.elim