case intro
ι : Sort ?u.21693
V : Type u
W : Type v
G : SimpleGraph V
G₁ G₂ : Subgraph G
a b : V
s : Set (Subgraph G)
G' : Subgraph G
hG' : G' ∈ s
⊢ (∀ (G' : Subgraph G), G' ∈ s → Adj G' a b) → SimpleGraph.Adj G a b
ι : Sort ?u.21693
V : Type u
W : Type v
G : SimpleGraph V
G₁ G₂ : Subgraph G
a b : V
s : Set (Subgraph G)
hs : Set.Nonempty s
⊢ (∀ (G' : Subgraph G), G' ∈ s → Adj G' a b) → SimpleGraph.Adj G a b
obtain ⟨G', hG'⟩ := hs
no goals
case intro
ι : Sort ?u.21693
V : Type u
W : Type v
G : SimpleGraph V
G₁ G₂ : Subgraph G
a b : V
s : Set (Subgraph G)
G' : Subgraph G
hG' : G' ∈ s
⊢ (∀ (G' : Subgraph G), G' ∈ s → Adj G' a b) → SimpleGraph.Adj G a b
exact fun h => G'.adj_sub (h _ hG')