Theorem: Digraph.Hom.mapEdgeSet.injective (GraphProjects/Digraph.lean)

State before:
ι : Sort ?u.224451
𝕜 : Type ?u.224454
V : Type u
W : Type v
X : Type w
G : Digraph V
G' : Digraph W
a b c u v w : V
f : G →g G'
hinj : Injective ↑f
⊢ Injective (mapEdgeSet f)
Tactic:
rintro ⟨e₁, h₁⟩ ⟨e₂, h₂⟩
State after:
case mk.mk
ι : Sort ?u.224451
𝕜 : Type ?u.224454
V : Type u
W : Type v
X : Type w
G : Digraph V
G' : Digraph W
a b c u v w : V
f : G →g G'
hinj : Injective ↑f
e₁ : V × V
h₁ : e₁ ∈ edgeSet G
e₂ : V × 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₂ }

State before:
case mk.mk
ι : Sort ?u.224451
𝕜 : Type ?u.224454
V : Type u
W : Type v
X : Type w
G : Digraph V
G' : Digraph W
a b c u v w : V
f : G →g G'
hinj : Injective ↑f
e₁ : V × V
h₁ : e₁ ∈ edgeSet G
e₂ : V × 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₂ }
Tactic:
dsimp [Hom.mapEdgeSet]
State after:
case mk.mk
ι : Sort ?u.224451
𝕜 : Type ?u.224454
V : Type u
W : Type v
X : Type w
G : Digraph V
G' : Digraph W
a b c u v w : V
f : G →g G'
hinj : Injective ↑f
e₁ : V × V
h₁ : e₁ ∈ edgeSet G
e₂ : V × V
h₂ : e₂ ∈ edgeSet G
⊢ { val := (↑f e₁.fst, ↑f e₁.snd), property := (_ : Prod.map ↑f ↑f ↑{ val := e₁, property := h₁ } ∈ edgeSet G') } =
      { val := (↑f e₂.fst, ↑f e₂.snd), property := (_ : Prod.map ↑f ↑f ↑{ val := e₂, property := h₂ } ∈ edgeSet G') } →
    { val := e₁, property := h₁ } = { val := e₂, property := h₂ }

State before:
case mk.mk
ι : Sort ?u.224451
𝕜 : Type ?u.224454
V : Type u
W : Type v
X : Type w
G : Digraph V
G' : Digraph W
a b c u v w : V
f : G →g G'
hinj : Injective ↑f
e₁ : V × V
h₁ : e₁ ∈ edgeSet G
e₂ : V × V
h₂ : e₂ ∈ edgeSet G
⊢ { val := (↑f e₁.fst, ↑f e₁.snd), property := (_ : Prod.map ↑f ↑f ↑{ val := e₁, property := h₁ } ∈ edgeSet G') } =
      { val := (↑f e₂.fst, ↑f e₂.snd), property := (_ : Prod.map ↑f ↑f ↑{ val := e₂, property := h₂ } ∈ edgeSet G') } →
    { val := e₁, property := h₁ } = { val := e₂, property := h₂ }
Tactic:
repeat' rw [Subtype.mk_eq_mk]
State after:
case mk.mk
ι : Sort ?u.224451
𝕜 : Type ?u.224454
V : Type u
W : Type v
X : Type w
G : Digraph V
G' : Digraph W
a b c u v w : V
f : G →g G'
hinj : Injective ↑f
e₁ : V × V
h₁ : e₁ ∈ edgeSet G
e₂ : V × V
h₂ : e₂ ∈ edgeSet G
⊢ (↑f e₁.fst, ↑f e₁.snd) = (↑f e₂.fst, ↑f e₂.snd) → e₁ = e₂

State before:
case mk.mk
ι : Sort ?u.224451
𝕜 : Type ?u.224454
V : Type u
W : Type v
X : Type w
G : Digraph V
G' : Digraph W
a b c u v w : V
f : G →g G'
hinj : Injective ↑f
e₁ : V × V
h₁ : e₁ ∈ edgeSet G
e₂ : V × V
h₂ : e₂ ∈ edgeSet G
⊢ (↑f e₁.fst, ↑f e₁.snd) = (↑f e₂.fst, ↑f e₂.snd) → e₁ = e₂
Tactic:
cases e₁
State after:
case mk.mk.mk
ι : Sort ?u.224451
𝕜 : Type ?u.224454
V : Type u
W : Type v
X : Type w
G : Digraph V
G' : Digraph W
a b c u v w : V
f : G →g G'
hinj : Injective ↑f
e₂ : V × V
h₂ : e₂ ∈ edgeSet G
fst✝ snd✝ : V
h₁ : (fst✝, snd✝) ∈ edgeSet G
⊢ (↑f (fst✝, snd✝).fst, ↑f (fst✝, snd✝).snd) = (↑f e₂.fst, ↑f e₂.snd) → (fst✝, snd✝) = e₂

State before:
case mk.mk.mk
ι : Sort ?u.224451
𝕜 : Type ?u.224454
V : Type u
W : Type v
X : Type w
G : Digraph V
G' : Digraph W
a b c u v w : V
f : G →g G'
hinj : Injective ↑f
e₂ : V × V
h₂ : e₂ ∈ edgeSet G
fst✝ snd✝ : V
h₁ : (fst✝, snd✝) ∈ edgeSet G
⊢ (↑f (fst✝, snd✝).fst, ↑f (fst✝, snd✝).snd) = (↑f e₂.fst, ↑f e₂.snd) → (fst✝, snd✝) = e₂
Tactic:
cases e₂
State after:
case mk.mk.mk.mk
ι : Sort ?u.224451
𝕜 : Type ?u.224454
V : Type u
W : Type v
X : Type w
G : Digraph V
G' : Digraph W
a b c u v w : V
f : G →g G'
hinj : Injective ↑f
fst✝¹ snd✝¹ : V
h₁ : (fst✝¹, snd✝¹) ∈ edgeSet G
fst✝ snd✝ : V
h₂ : (fst✝, snd✝) ∈ edgeSet G
⊢ (↑f (fst✝¹, snd✝¹).fst, ↑f (fst✝¹, snd✝¹).snd) = (↑f (fst✝, snd✝).fst, ↑f (fst✝, snd✝).snd) →
    (fst✝¹, snd✝¹) = (fst✝, snd✝)

State before:
case mk.mk.mk.mk
ι : Sort ?u.224451
𝕜 : Type ?u.224454
V : Type u
W : Type v
X : Type w
G : Digraph V
G' : Digraph W
a b c u v w : V
f : G →g G'
hinj : Injective ↑f
fst✝¹ snd✝¹ : V
h₁ : (fst✝¹, snd✝¹) ∈ edgeSet G
fst✝ snd✝ : V
h₂ : (fst✝, snd✝) ∈ edgeSet G
⊢ (↑f (fst✝¹, snd✝¹).fst, ↑f (fst✝¹, snd✝¹).snd) = (↑f (fst✝, snd✝).fst, ↑f (fst✝, snd✝).snd) →
    (fst✝¹, snd✝¹) = (fst✝, snd✝)
Tactic:
simp
State after:
case mk.mk.mk.mk
ι : Sort ?u.224451
𝕜 : Type ?u.224454
V : Type u
W : Type v
X : Type w
G : Digraph V
G' : Digraph W
a b c u v w : V
f : G →g G'
hinj : Injective ↑f
fst✝¹ snd✝¹ : V
h₁ : (fst✝¹, snd✝¹) ∈ edgeSet G
fst✝ snd✝ : V
h₂ : (fst✝, snd✝) ∈ edgeSet G
⊢ ↑f fst✝¹ = ↑f fst✝ → ↑f snd✝¹ = ↑f snd✝ → fst✝¹ = fst✝ ∧ snd✝¹ = snd✝

State before:
case mk.mk.mk.mk
ι : Sort ?u.224451
𝕜 : Type ?u.224454
V : Type u
W : Type v
X : Type w
G : Digraph V
G' : Digraph W
a b c u v w : V
f : G →g G'
hinj : Injective ↑f
fst✝¹ snd✝¹ : V
h₁ : (fst✝¹, snd✝¹) ∈ edgeSet G
fst✝ snd✝ : V
h₂ : (fst✝, snd✝) ∈ edgeSet G
⊢ ↑f fst✝¹ = ↑f fst✝ → ↑f snd✝¹ = ↑f snd✝ → fst✝¹ = fst✝ ∧ snd✝¹ = snd✝
Tactic:
intro h1 h2
State after:
case mk.mk.mk.mk
ι : Sort ?u.224451
𝕜 : Type ?u.224454
V : Type u
W : Type v
X : Type w
G : Digraph V
G' : Digraph W
a b c u v w : V
f : G →g G'
hinj : Injective ↑f
fst✝¹ snd✝¹ : V
h₁ : (fst✝¹, snd✝¹) ∈ edgeSet G
fst✝ snd✝ : V
h₂ : (fst✝, snd✝) ∈ edgeSet G
h1 : ↑f fst✝¹ = ↑f fst✝
h2 : ↑f snd✝¹ = ↑f snd✝
⊢ fst✝¹ = fst✝ ∧ snd✝¹ = snd✝

State before:
case mk.mk.mk.mk
ι : Sort ?u.224451
𝕜 : Type ?u.224454
V : Type u
W : Type v
X : Type w
G : Digraph V
G' : Digraph W
a b c u v w : V
f : G →g G'
hinj : Injective ↑f
fst✝¹ snd✝¹ : V
h₁ : (fst✝¹, snd✝¹) ∈ edgeSet G
fst✝ snd✝ : V
h₂ : (fst✝, snd✝) ∈ edgeSet G
h1 : ↑f fst✝¹ = ↑f fst✝
h2 : ↑f snd✝¹ = ↑f snd✝
⊢ fst✝¹ = fst✝ ∧ snd✝¹ = snd✝
Tactic:
simp [hinj h1, hinj h2]
State after:
no goals

State before:
case mk.mk
ι : Sort ?u.224451
𝕜 : Type ?u.224454
V : Type u
W : Type v
X : Type w
G : Digraph V
G' : Digraph W
a b c u v w : V
f : G →g G'
hinj : Injective ↑f
e₁ : V × V
h₁ : e₁ ∈ edgeSet G
e₂ : V × V
h₂ : e₂ ∈ edgeSet G
⊢ (↑f e₁.fst, ↑f e₁.snd) = (↑f e₂.fst, ↑f e₂.snd) → { val := e₁, property := h₁ } = { val := e₂, property := h₂ }
Tactic:
rw [Subtype.mk_eq_mk]
State after:
case mk.mk
ι : Sort ?u.224451
𝕜 : Type ?u.224454
V : Type u
W : Type v
X : Type w
G : Digraph V
G' : Digraph W
a b c u v w : V
f : G →g G'
hinj : Injective ↑f
e₁ : V × V
h₁ : e₁ ∈ edgeSet G
e₂ : V × V
h₂ : e₂ ∈ edgeSet G
⊢ (↑f e₁.fst, ↑f e₁.snd) = (↑f e₂.fst, ↑f e₂.snd) → e₁ = e₂