case intro
ι : Sort ?u.22992
𝕜 : Type ?u.22995
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
s : Set (SimpleGraph V)
G : SimpleGraph V
hG : G ∈ s
⊢ (∀ (G : SimpleGraph V), G ∈ s → Adj G a b) → a ≠ b
ι : Sort ?u.22992
𝕜 : Type ?u.22995
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
s : Set (SimpleGraph V)
hs : Set.Nonempty s
⊢ (∀ (G : SimpleGraph V), G ∈ s → Adj G a b) → a ≠ b
obtain ⟨G, hG⟩ := hs
no goals
case intro
ι : Sort ?u.22992
𝕜 : Type ?u.22995
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
s : Set (SimpleGraph V)
G : SimpleGraph V
hG : G ∈ s
⊢ (∀ (G : SimpleGraph V), G ∈ s → Adj G a b) → a ≠ b
exact fun h => (h _ hG).ne