ι : Sort ?u.172133
V : Type u
W : Type v
G : SimpleGraph V
G₁ G₂ : Subgraph G
a b : V
x y : Subgraph G
h✝ : x ≤ y
v w : ↑x.verts
h : ↑(inclusion h✝) v = ↑(inclusion h✝) w
⊢ v = w
ι : Sort ?u.172133
V : Type u
W : Type v
G : SimpleGraph V
G₁ G₂ : Subgraph G
a b : V
x y : Subgraph G
h : x ≤ y
⊢ Function.Injective ↑(inclusion h)
intro v w h
ι : Sort ?u.172133
V : Type u
W : Type v
G : SimpleGraph V
G₁ G₂ : Subgraph G
a b : V
x y : Subgraph G
h✝ : x ≤ y
v w : ↑x.verts
h :
  ↑(RelHomClass.toFunLike.1
        { toFun := fun v => { val := ↑v, property := (_ : ↑v ∈ y.verts) },
          map_rel' :=
            (_ :
              ∀ {a b : ↑x.verts},
                SimpleGraph.Adj (Subgraph.coe x) a b →
                  Adj y ↑((fun v => { val := ↑v, property := (_ : ↑v ∈ y.verts) }) a)
                    ↑((fun v => { val := ↑v, property := (_ : ↑v ∈ y.verts) }) b)) }
        v) =
    ↑(RelHomClass.toFunLike.1
        { toFun := fun v => { val := ↑v, property := (_ : ↑v ∈ y.verts) },
          map_rel' :=
            (_ :
              ∀ {a b : ↑x.verts},
                SimpleGraph.Adj (Subgraph.coe x) a b →
                  Adj y ↑((fun v => { val := ↑v, property := (_ : ↑v ∈ y.verts) }) a)
                    ↑((fun v => { val := ↑v, property := (_ : ↑v ∈ y.verts) }) b)) }
        w)
⊢ v = w
ι : Sort ?u.172133
V : Type u
W : Type v
G : SimpleGraph V
G₁ G₂ : Subgraph G
a b : V
x y : Subgraph G
h✝ : x ≤ y
v w : ↑x.verts
h : ↑(inclusion h✝) v = ↑(inclusion h✝) w
⊢ v = w
rw [inclusion, FunLike.coe, Subtype.mk_eq_mk] at h
no goals
ι : Sort ?u.172133
V : Type u
W : Type v
G : SimpleGraph V
G₁ G₂ : Subgraph G
a b : V
x y : Subgraph G
h✝ : x ≤ y
v w : ↑x.verts
h :
  ↑(RelHomClass.toFunLike.1
        { toFun := fun v => { val := ↑v, property := (_ : ↑v ∈ y.verts) },
          map_rel' :=
            (_ :
              ∀ {a b : ↑x.verts},
                SimpleGraph.Adj (Subgraph.coe x) a b →
                  Adj y ↑((fun v => { val := ↑v, property := (_ : ↑v ∈ y.verts) }) a)
                    ↑((fun v => { val := ↑v, property := (_ : ↑v ∈ y.verts) }) b)) }
        v) =
    ↑(RelHomClass.toFunLike.1
        { toFun := fun v => { val := ↑v, property := (_ : ↑v ∈ y.verts) },
          map_rel' :=
            (_ :
              ∀ {a b : ↑x.verts},
                SimpleGraph.Adj (Subgraph.coe x) a b →
                  Adj y ↑((fun v => { val := ↑v, property := (_ : ↑v ∈ y.verts) }) a)
                    ↑((fun v => { val := ↑v, property := (_ : ↑v ∈ y.verts) }) b)) }
        w)
⊢ v = w
exact Subtype.ext h