case mk.mk
ι : Sort ?u.403479
𝕜 : Type ?u.403482
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
f : G →g G'
hinj : Injective ↑f
e₁ : Sym2 V
h₁ : e₁ ∈ edgeSet G
e₂ : Sym2 V
h₂ : e₂ ∈ edgeSet G
⊢ mapEdgeSet f { val := e₁, property := h₁ } = mapEdgeSet f { val := e₂, property := h₂ } →
    { val := e₁, property := h₁ } = { val := e₂, property := h₂ }
ι : Sort ?u.403479
𝕜 : Type ?u.403482
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
f : G →g G'
hinj : Injective ↑f
⊢ Injective (mapEdgeSet f)
rintro ⟨e₁, h₁⟩ ⟨e₂, h₂⟩
case mk.mk
ι : Sort ?u.403479
𝕜 : Type ?u.403482
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
f : G →g G'
hinj : Injective ↑f
e₁ : Sym2 V
h₁ : e₁ ∈ edgeSet G
e₂ : Sym2 V
h₂ : e₂ ∈ edgeSet G
⊢ { val := Sym2.map (↑f) e₁, property := (_ : Sym2.map ↑f ↑{ val := e₁, property := h₁ } ∈ edgeSet G') } =
      { val := Sym2.map (↑f) e₂, property := (_ : Sym2.map ↑f ↑{ val := e₂, property := h₂ } ∈ edgeSet G') } →
    { val := e₁, property := h₁ } = { val := e₂, property := h₂ }
case mk.mk
ι : Sort ?u.403479
𝕜 : Type ?u.403482
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
f : G →g G'
hinj : Injective ↑f
e₁ : Sym2 V
h₁ : e₁ ∈ edgeSet G
e₂ : Sym2 V
h₂ : e₂ ∈ edgeSet G
⊢ mapEdgeSet f { val := e₁, property := h₁ } = mapEdgeSet f { val := e₂, property := h₂ } →
    { val := e₁, property := h₁ } = { val := e₂, property := h₂ }
dsimp [Hom.mapEdgeSet]
case mk.mk
ι : Sort ?u.403479
𝕜 : Type ?u.403482
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
f : G →g G'
hinj : Injective ↑f
e₁ : Sym2 V
h₁ : e₁ ∈ edgeSet G
e₂ : Sym2 V
h₂ : e₂ ∈ edgeSet G
⊢ Sym2.map (↑f) e₁ = Sym2.map (↑f) e₂ → e₁ = e₂
case mk.mk
ι : Sort ?u.403479
𝕜 : Type ?u.403482
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
f : G →g G'
hinj : Injective ↑f
e₁ : Sym2 V
h₁ : e₁ ∈ edgeSet G
e₂ : Sym2 V
h₂ : e₂ ∈ edgeSet G
⊢ { val := Sym2.map (↑f) e₁, property := (_ : Sym2.map ↑f ↑{ val := e₁, property := h₁ } ∈ edgeSet G') } =
      { val := Sym2.map (↑f) e₂, property := (_ : Sym2.map ↑f ↑{ val := e₂, property := h₂ } ∈ edgeSet G') } →
    { val := e₁, property := h₁ } = { val := e₂, property := h₂ }
repeat' rw [Subtype.mk_eq_mk]
no goals
case mk.mk
ι : Sort ?u.403479
𝕜 : Type ?u.403482
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
f : G →g G'
hinj : Injective ↑f
e₁ : Sym2 V
h₁ : e₁ ∈ edgeSet G
e₂ : Sym2 V
h₂ : e₂ ∈ edgeSet G
⊢ Sym2.map (↑f) e₁ = Sym2.map (↑f) e₂ → e₁ = e₂
apply Sym2.map.injective hinj
case mk.mk
ι : Sort ?u.403479
𝕜 : Type ?u.403482
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
f : G →g G'
hinj : Injective ↑f
e₁ : Sym2 V
h₁ : e₁ ∈ edgeSet G
e₂ : Sym2 V
h₂ : e₂ ∈ edgeSet G
⊢ Sym2.map (↑f) e₁ = Sym2.map (↑f) e₂ → e₁ = e₂
case mk.mk
ι : Sort ?u.403479
𝕜 : Type ?u.403482
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
f : G →g G'
hinj : Injective ↑f
e₁ : Sym2 V
h₁ : e₁ ∈ edgeSet G
e₂ : Sym2 V
h₂ : e₂ ∈ edgeSet G
⊢ Sym2.map (↑f) e₁ = Sym2.map (↑f) e₂ → e₁ = e₂
rw [Subtype.mk_eq_mk]