ι : Sort ?u.91344
𝕜 : Type ?u.91347
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✝ s t : Set (Sym2 V)
h : s ⊆ t
v w : V
⊢ Adj (fromEdgeSet s) v w → Adj (fromEdgeSet t) v w
ι : Sort ?u.91344
𝕜 : Type ?u.91347
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✝ s t : Set (Sym2 V)
h : s ⊆ t
⊢ fromEdgeSet s ≤ fromEdgeSet t
rintro v w
ι : Sort ?u.91344
𝕜 : Type ?u.91347
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✝ s t : Set (Sym2 V)
h : s ⊆ t
v w : V
⊢ Quotient.mk (Sym2.Rel.setoid V) (v, w) ∈ s → ¬v = w → Quotient.mk (Sym2.Rel.setoid V) (v, w) ∈ t
ι : Sort ?u.91344
𝕜 : Type ?u.91347
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✝ s t : Set (Sym2 V)
h : s ⊆ t
v w : V
⊢ Adj (fromEdgeSet s) v w → Adj (fromEdgeSet t) v w
simp (config := { contextual := true }) only [fromEdgeSet_adj, Ne.def, not_false_iff,
  and_true_iff, and_imp]
no goals
ι : Sort ?u.91344
𝕜 : Type ?u.91347
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✝ s t : Set (Sym2 V)
h : s ⊆ t
v w : V
⊢ Quotient.mk (Sym2.Rel.setoid V) (v, w) ∈ s → ¬v = w → Quotient.mk (Sym2.Rel.setoid V) (v, w) ∈ t
exact fun vws _ => h vws