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

State before:
ι : Sort ?u.407307
𝕜 : Type ?u.407310
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
⊢ Hom.comp (InduceHom ψ ψtr) (InduceHom φ φst) = InduceHom (Hom.comp ψ φ) (_ : Set.MapsTo (↑ψ ∘ fun x => ↑φ x) s r)
Tactic:
ext x
State after:
case h.a
ι : Sort ?u.407307
𝕜 : Type ?u.407310
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
x : ↑s
⊢ ↑(↑(Hom.comp (InduceHom ψ ψtr) (InduceHom φ φst)) x) =
    ↑(↑(InduceHom (Hom.comp ψ φ) (_ : Set.MapsTo (↑ψ ∘ fun x => ↑φ x) s r)) x)

State before:
case h.a
ι : Sort ?u.407307
𝕜 : Type ?u.407310
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
x : ↑s
⊢ ↑(↑(Hom.comp (InduceHom ψ ψtr) (InduceHom φ φst)) x) =
    ↑(↑(InduceHom (Hom.comp ψ φ) (_ : Set.MapsTo (↑ψ ∘ fun x => ↑φ x) s r)) x)
Tactic:
rfl
State after:
no goals