Theorem: Digraph.induceHom_id (GraphProjects/Digraph.lean)

State before:
ι : Sort ?u.395639
𝕜 : Type ?u.395642
V : Type u
W : Type v
X : Type w
G✝ : Digraph V
G' : Digraph W
a b c u v w : V
G'' : Digraph X
s✝ : Set V
t : Set W
r : Set X
φ : G✝ →g G'
φst : Set.MapsTo (↑φ) s✝ t
ψ : G' →g G''
ψtr : Set.MapsTo (↑ψ) t r
G : Digraph V
s : Set V
⊢ InduceHom Hom.id (_ : Set.MapsTo id s s) = Hom.id
Tactic:
ext x
State after:
case h.a
ι : Sort ?u.395639
𝕜 : Type ?u.395642
V : Type u
W : Type v
X : Type w
G✝ : Digraph V
G' : Digraph W
a b c u v w : V
G'' : Digraph X
s✝ : Set V
t : Set W
r : Set X
φ : G✝ →g G'
φst : Set.MapsTo (↑φ) s✝ t
ψ : G' →g G''
ψtr : Set.MapsTo (↑ψ) t r
G : Digraph V
s : Set V
x : ↑s
⊢ ↑(↑(InduceHom Hom.id (_ : Set.MapsTo id s s)) x) = ↑(↑Hom.id x)

State before:
case h.a
ι : Sort ?u.395639
𝕜 : Type ?u.395642
V : Type u
W : Type v
X : Type w
G✝ : Digraph V
G' : Digraph W
a b c u v w : V
G'' : Digraph X
s✝ : Set V
t : Set W
r : Set X
φ : G✝ →g G'
φst : Set.MapsTo (↑φ) s✝ t
ψ : G' →g G''
ψtr : Set.MapsTo (↑ψ) t r
G : Digraph V
s : Set V
x : ↑s
⊢ ↑(↑(InduceHom Hom.id (_ : Set.MapsTo id s s)) x) = ↑(↑Hom.id x)
Tactic:
rfl
State after:
no goals