internlm/Lean-Github huggingface dataset:
Theorem: Graph.toFuncV_init
Proof state before:
V : Type u
E : Type v
V₁ : Type u_1
E₁ : Type u_2
V₂ : Type u_3
E₂ : Type u_4
G₁ : Graph V₁ E₁
G₂ : Graph V₂ E₂
f : Morphism G₁ G₂
⊢ ∀ (e : E₁), f.toFuncV (G₁.ι e) = G₂.ι (f.toFuncE e)
Tactic:
intro e
Proof state after:
V : Type u
E : Type v
V₁ : Type u_1
E₁ : Type u_2
V₂ : Type u_3
E₂ : Type u_4
G₁ : Graph V₁ E₁
G₂ : Graph V₂ E₂
f : Morphism G₁ G₂
e : E₁
⊢ f.toFuncV (G₁.ι e) = G₂.ι (f.toFuncE e)
Theorem: Graph.toFuncV_init
Proof state before:
V : Type u
E : Type v
V₁ : Type u_1
E₁ : Type u_2
V₂ : Type u_3
E₂ : Type u_4
G₁ : Graph V₁ E₁
G₂ : Graph V₂ E₂
f : Morphism G₁ G₂
e : E₁
⊢ f.toFuncV (G₁.ι e) = G₂.ι (f.toFuncE e)
Tactic:
exact f.toFuncV_init e
Proof state after:
no goals
Theorem: Graph.toFuncE_bar
Proof state before:
V : Type u
E : Type v
V₁ : Type u_1
E₁ : Type u_2
V₂ : Type u_3
E₂ : Type u_4
G₁ : Graph V₁ E₁
G₂ : Graph V₂ E₂
f : Morphism G₁ G₂
⊢ ∀ (e : E₁), f.toFuncE (G₁.bar e) = G₂.bar (f.toFuncE e)
Tactic:
intro e
Proof state after:
V : Type u
E : Type v
V₁ : Type u_1
E₁ : Type u_2
V₂ : Type u_3
E₂ : Type u_4
G₁ : Graph V₁ E₁
G₂ : Graph V₂ E₂
f : Morphism G₁ G₂
e : E₁
⊢ f.toFuncE (G₁.bar e) = G₂.bar (f.toFuncE e)
Theorem: Graph.toFuncE_bar
Proof state before:
V : Type u
E : Type v
V₁ : Type u_1
E₁ : Type u_2
V₂ : Type u_3
E₂ : Type u_4
G₁ : Graph V₁ E₁
G₂ : Graph V₂ E₂
f : Morphism G₁ G₂
e : E₁
⊢ f.toFuncE (G₁.bar e) = G₂.bar (f.toFuncE e)
Tactic:
exact f.toFuncE_bar e
Proof state after:
no goals
Theorem: Graph.toFuncV_term
Proof state before:
V : Type u
E : Type v
V₁ : Type u_1
E₁ : Type u_2
V₂ : Type u_3
E₂ : Type u_4
G₁ : Graph V₁ E₁
G₂ : Graph V₂ E₂
f : Morphism G₁ G₂
⊢ ∀ (e : E₁), f.toFuncV (τ G₁ e) = τ G₂ (f.toFuncE e)
Tactic:
intro e
Proof state after:
V : Type u
E : Type v
V₁ : Type u_1
E₁ : Type u_2
V₂ : Type u_3
E₂ : Type u_4
G₁ : Graph V₁ E₁
G₂ : Graph V₂ E₂
f : Morphism G₁ G₂
e : E₁
⊢ f.toFuncV (τ G₁ e) = τ G₂ (f.toFuncE e)
Theorem: Graph.toFuncV_term
Proof state before:
V : Type u
E : Type v
V₁ : Type u_1
E₁ : Type u_2
V₂ : Type u_3
E₂ : Type u_4
G₁ : Graph V₁ E₁
G₂ : Graph V₂ E₂
f : Morphism G₁ G₂
e : E₁
⊢ f.toFuncV (τ G₁ e) = τ G₂ (f.toFuncE e)
Tactic:
rw [Graph.τ, Graph.τ, ←toFuncE_bar, ←toFuncV_init]
Proof state after:
no goals
Theorem: Graph.EdgeBetween.map_toList
Proof state before:
V : Type u
E : Type v
V₁ : Type u_1
E₁ : Type u_2
V₂ : Type u_3
E₂ : Type u_4
G₁ : Graph V₁ E₁
G₂ : Graph V₂ E₂
f : Morphism G₁ G₂
v₁ w₁ : V₁
e : EdgeBetween G₁ v₁ w₁
⊢ (map f e).edge = f.toFuncE e.edge
Tactic:
simp [EdgeBetween.map, toList]
Proof state after:
no goals
Theorem: Graph.EdgeBetween.map_bar
Proof state before:
V : Type u
E : Type v
V₁ : Type u_1
E₁ : Type u_2
V₂ : Type u_3
E₂ : Type u_4
G₁ : Graph V₁ E₁
G₂ : Graph V₂ E₂
f : Morphism G₁ G₂
v₁ w₁ : V₁
e : EdgeBetween G₁ v₁ w₁
⊢ bar (map f e) = map f (bar e)
Tactic:
ext
Proof state after:
case edge
V : Type u
E : Type v
V₁ : Type u_1
E₁ : Type u_2
V₂ : Type u_3
E₂ : Type u_4
G₁ : Graph V₁ E₁
G₂ : Graph V₂ E₂
f : Morphism G₁ G₂
v₁ w₁ : V₁
e : EdgeBetween G₁ v₁ w₁
⊢ (bar (map f e)).edge = (map f (bar e)).edge
Theorem: Graph.EdgeBetween.map_bar
Proof state before:
case edge
V : Type u
E : Type v
V₁ : Type u_1
E₁ : Type u_2
V₂ : Type u_3
E₂ : Type u_4
G₁ : Graph V₁ E₁
G₂ : Graph V₂ E₂
f : Morphism G₁ G₂
v₁ w₁ : V₁
e : EdgeBetween G₁ v₁ w₁
⊢ (bar (map f e)).edge = (map f (bar e)).edge
Tactic:
simp [f.toFuncE_bar, EdgeBetween.map]
Proof state after:
no goals
Theorem: Graph.Morphism.append_map
Proof state before:
V₁ : Type u_1
E₁ : Type u_2
V₂ : Type u_4
E₂ : Type u_3
V : Type u
E : Type v
G₁ : Graph V₁ E₁
G₂ : Graph V₂ E₂
f : Morphism G₁ G₂
u v w : V₁
η : EdgePath G₁ u v
η' : EdgePath G₁ v w
⊢ map (η ++ η') f = map η f ++ map η' f
Tactic:
apply eq_of_toList_eq
Proof state after:
case a
V₁ : Type u_1
E₁ : Type u_2
V₂ : Type u_4
E₂ : Type u_3
V : Type u
E : Type v
G₁ : Graph V₁ E₁
G₂ : Graph V₂ E₂
f : Morphism G₁ G₂
u v w : V₁
η : EdgePath G₁ u v
η' : EdgePath G₁ v w
⊢ toList (map (η ++ η') f) = toList (map η f ++ map η' f)
Theorem: Graph.Morphism.append_map
Proof state before:
case a
V₁ : Type u_1
E₁ : Type u_2
V₂ : Type u_4
E₂ : Type u_3
V : Type u
E : Type v
G₁ : Graph V₁ E₁
G₂ : Graph V₂ E₂
f : Morphism G₁ G₂
u v w : V₁
η : EdgePath G₁ u v
η' : EdgePath G₁ v w
⊢ toList (map (η ++ η') f) = toList (map η f ++ map η' f)
Tactic:
simp [map_toList, append_toList]
Proof state after:
no goals
Theorem: Graph.Morphism.cons_map
Proof state before:
V₁ : Type u_1
E₁ : Type u_2
V₂ : Type u_4
E₂ : Type u_3
V : Type u
E : Type v
G₁ : Graph V₁ E₁
G₂ : Graph V₂ E₂
f : Morphism G₁ G₂
u v w : V₁
e : EdgeBetween G₁ u v
η : EdgePath G₁ v w
⊢ map (cons e η) f = cons (EdgeBetween.map f e) (map η f)
Tactic:
apply eq_of_toList_eq
Proof state after:
case a
V₁ : Type u_1
E₁ : Type u_2
V₂ : Type u_4
E₂ : Type u_3
V : Type u
E : Type v
G₁ : Graph V₁ E₁
G₂ : Graph V₂ E₂
f : Morphism G₁ G₂
u v w : V₁
e : EdgeBetween G₁ u v
η : EdgePath G₁ v w
⊢ toList (map (cons e η) f) = toList (cons (EdgeBetween.map f e) (map η f))
Theorem: Graph.Morphism.cons_map
Proof state before:
case a
V₁ : Type u_1
E₁ : Type u_2
V₂ : Type u_4
E₂ : Type u_3
V : Type u
E : Type v
G₁ : Graph V₁ E₁
G₂ : Graph V₂ E₂
f : Morphism G₁ G₂
u v w : V₁
e : EdgeBetween G₁ u v
η : EdgePath G₁ v w
⊢ toList (map (cons e η) f) = toList (cons (EdgeBetween.map f e) (map η f))
Tactic:
simp [map_toList, EdgeBetween.map_toList, cons_toList]
Proof state after:
no goals
Theorem: Graph.Morphism.reverse_map
Proof state before:
V₁ : Type u_1
E₁ : Type u_2
V₂ : Type u_4
E₂ : Type u_3
V : Type u
E : Type v
G₁ : Graph V₁ E₁
G₂ : Graph V₂ E₂
f : Morphism G₁ G₂
u v : V₁
η : EdgePath G₁ u v
⊢ map (reverse η) f = reverse (map η f)
Tactic:
apply eq_of_toList_eq
Proof state after:
case a
V₁ : Type u_1
E₁ : Type u_2
V₂ : Type u_4
E₂ : Type u_3
V : Type u
E : Type v
G₁ : Graph V₁ E₁
G₂ : Graph V₂ E₂
f : Morphism G₁ G₂
u v : V₁
η : EdgePath G₁ u v
⊢ toList (map (reverse η) f) = toList (reverse (map η f))
Theorem: Graph.Morphism.reverse_map
Proof state before:
case a
V₁ : Type u_1
E₁ : Type u_2
V₂ : Type u_4
E₂ : Type u_3
V : Type u
E : Type v
G₁ : Graph V₁ E₁
G₂ : Graph V₂ E₂
f : Morphism G₁ G₂
u v : V₁
η : EdgePath G₁ u v
⊢ toList (map (reverse η) f) = toList (reverse (map η f))
Tactic:
simp [map_toList, reverse_toList, List.map_reverse]
Proof state after:
case a
V₁ : Type u_1
E₁ : Type u_2
V₂ : Type u_4
E₂ : Type u_3
V : Type u
E : Type v
G₁ : Graph V₁ E₁
G₂ : Graph V₂ E₂
f : Morphism G₁ G₂
u v : V₁
η : EdgePath G₁ u v
⊢ List.map (f.toFuncE ∘ G₁.bar) (toList η) = List.map (G₂.bar ∘ f.toFuncE) (toList η)
Theorem: Graph.Morphism.reverse_map
Proof state before:
case a
V₁ : Type u_1
E₁ : Type u_2
V₂ : Type u_4
E₂ : Type u_3
V : Type u
E : Type v
G₁ : Graph V₁ E₁
G₂ : Graph V₂ E₂
f : Morphism G₁ G₂
u v : V₁
η : EdgePath G₁ u v
⊢ List.map (f.toFuncE ∘ G₁.bar) (toList η) = List.map (G₂.bar ∘ f.toFuncE) (toList η)
Tactic:
congr
Proof state after:
case a.e_f
V₁ : Type u_1
E₁ : Type u_2
V₂ : Type u_4
E₂ : Type u_3
V : Type u
E : Type v
G₁ : Graph V₁ E₁
G₂ : Graph V₂ E₂
f : Morphism G₁ G₂
u v : V₁
η : EdgePath G₁ u v
⊢ f.toFuncE ∘ G₁.bar = G₂.bar ∘ f.toFuncE
Theorem: Graph.Morphism.reverse_map
Proof state before:
case a.e_f
V₁ : Type u_1
E₁ : Type u_2
V₂ : Type u_4
E₂ : Type u_3
V : Type u
E : Type v
G₁ : Graph V₁ E₁
G₂ : Graph V₂ E₂
f : Morphism G₁ G₂
u v : V₁
η : EdgePath G₁ u v
⊢ f.toFuncE ∘ G₁.bar = G₂.bar ∘ f.toFuncE
Tactic:
funext e
Proof state after:
case a.e_f.h
V₁ : Type u_1
E₁ : Type u_2
V₂ : Type u_4
E₂ : Type u_3
V : Type u
E : Type v
G₁ : Graph V₁ E₁
G₂ : Graph V₂ E₂
f : Morphism G₁ G₂
u v : V₁
η : EdgePath G₁ u v
e : E₁
⊢ (f.toFuncE ∘ G₁.bar) e = (G₂.bar ∘ f.toFuncE) e
Theorem: Graph.Morphism.reverse_map
Proof state before:
case a.e_f.h
V₁ : Type u_1
E₁ : Type u_2
V₂ : Type u_4
E₂ : Type u_3
V : Type u
E : Type v
G₁ : Graph V₁ E₁
G₂ : Graph V₂ E₂
f : Morphism G₁ G₂
u v : V₁
η : EdgePath G₁ u v
e : E₁
⊢ (f.toFuncE ∘ G₁.bar) e = (G₂.bar ∘ f.toFuncE) e
Tactic:
simp only [Function.comp, f.toFuncE_bar]
Proof state after:
no goals
Theorem: Graph.Morphism.map_of_reduction
Proof state before:
V₁ : Type u_1
E₁ : Type u_2
V₂ : Type u_3
E₂ : Type u_4
V : Type u
E : Type v
G₁ : Graph V₁ E₁
G₂ : Graph V₂ E₂
f : Morphism G₁ G₂
v w : V₁
η₁ η₂ : EdgePath G₁ v w
u u' : V₁
e : EdgeBetween G₁ u u'
p₁ : EdgePath G₁ v u
p₂ : EdgePath G₁ u w
⊢ Reduction (map (p₁ ++ cons e (cons (EdgeBetween.bar e) p₂)) f) (map (p₁ ++ p₂) f)
Tactic:
simp [append_map, cons_map]
Proof state after:
V₁ : Type u_1
E₁ : Type u_2
V₂ : Type u_3
E₂ : Type u_4
V : Type u
E : Type v
G₁ : Graph V₁ E₁
G₂ : Graph V₂ E₂
f : Morphism G₁ G₂
v w : V₁
η₁ η₂ : EdgePath G₁ v w
u u' : V₁
e : EdgeBetween G₁ u u'
p₁ : EdgePath G₁ v u
p₂ : EdgePath G₁ u w
⊢ Reduction (map p₁ f ++ cons (EdgeBetween.map f e) (cons (EdgeBetween.map f (EdgeBetween.bar e)) (map p₂ f)))
    (map p₁ f ++ map p₂ f)
Theorem: Graph.Morphism.map_of_reduction
Proof state before:
V₁ : Type u_1
E₁ : Type u_2
V₂ : Type u_3
E₂ : Type u_4
V : Type u
E : Type v
G₁ : Graph V₁ E₁
G₂ : Graph V₂ E₂
f : Morphism G₁ G₂
v w : V₁
η₁ η₂ : EdgePath G₁ v w
u u' : V₁
e : EdgeBetween G₁ u u'
p₁ : EdgePath G₁ v u
p₂ : EdgePath G₁ u w
⊢ Reduction (map p₁ f ++ cons (EdgeBetween.map f e) (cons (EdgeBetween.map f (EdgeBetween.bar e)) (map p₂ f)))
    (map p₁ f ++ map p₂ f)
Tactic:
rw [← EdgeBetween.map_bar]
Proof state after:
V₁ : Type u_1
E₁ : Type u_2
V₂ : Type u_3
E₂ : Type u_4
V : Type u
E : Type v
G₁ : Graph V₁ E₁
G₂ : Graph V₂ E₂
f : Morphism G₁ G₂
v w : V₁
η₁ η₂ : EdgePath G₁ v w
u u' : V₁
e : EdgeBetween G₁ u u'
p₁ : EdgePath G₁ v u
p₂ : EdgePath G₁ u w
⊢ Reduction (map p₁ f ++ cons (EdgeBetween.map f e) (cons (EdgeBetween.bar (EdgeBetween.map f e)) (map p₂ f)))
    (map p₁ f ++ map p₂ f)
Theorem: Graph.Morphism.map_of_reduction
Proof state before:
V₁ : Type u_1
E₁ : Type u_2
V₂ : Type u_3
E₂ : Type u_4
V : Type u
E : Type v
G₁ : Graph V₁ E₁
G₂ : Graph V₂ E₂
f : Morphism G₁ G₂
v w : V₁
η₁ η₂ : EdgePath G₁ v w
u u' : V₁
e : EdgeBetween G₁ u u'
p₁ : EdgePath G₁ v u
p₂ : EdgePath G₁ u w
⊢ Reduction (map p₁ f ++ cons (EdgeBetween.map f e) (cons (EdgeBetween.bar (EdgeBetween.map f e)) (map p₂ f)))
    (map p₁ f ++ map p₂ f)
Tactic:
apply Reduction.step
Proof state after:
no goals
Theorem: Graph.Morphism.reduced_of_image_reduced
Proof state before:
V₁ : Type u_1
E₁ : Type u_2
V₂ : Type u_3
E₂ : Type u_4
V : Type u
E : Type v
G₁ : Graph V₁ E₁
G₂ : Graph V₂ E₂
f : Morphism G₁ G₂
v w : V₁
η : EdgePath G₁ v w
⊢ reduced (map η f) → reduced η
Tactic:
intro hyp η' contra
Proof state after:
V₁ : Type u_1
E₁ : Type u_2
V₂ : Type u_3
E₂ : Type u_4
V : Type u
E : Type v
G₁ : Graph V₁ E₁
G₂ : Graph V₂ E₂
f : Morphism G₁ G₂
v w : V₁
η : EdgePath G₁ v w
hyp : reduced (map η f)
η' : EdgePath G₁ v w
contra : Reduction η η'
⊢ False
Theorem: Graph.Morphism.reduced_of_image_reduced
Proof state before:
V₁ : Type u_1
E₁ : Type u_2
V₂ : Type u_3
E₂ : Type u_4
V : Type u
E : Type v
G₁ : Graph V₁ E₁
G₂ : Graph V₂ E₂
f : Morphism G₁ G₂
v w : V₁
η : EdgePath G₁ v w
hyp : reduced (map η f)
η' : EdgePath G₁ v w
contra : Reduction η η'
⊢ False
Tactic:
apply hyp (η'.map f)
Proof state after:
V₁ : Type u_1
E₁ : Type u_2
V₂ : Type u_3
E₂ : Type u_4
V : Type u
E : Type v
G₁ : Graph V₁ E₁
G₂ : Graph V₂ E₂
f : Morphism G₁ G₂
v w : V₁
η : EdgePath G₁ v w
hyp : reduced (map η f)
η' : EdgePath G₁ v w
contra : Reduction η η'
⊢ Reduction (map η f) (map η' f)
Theorem: Graph.Morphism.reduced_of_image_reduced
Proof state before:
V₁ : Type u_1
E₁ : Type u_2
V₂ : Type u_3
E₂ : Type u_4
V : Type u
E : Type v
G₁ : Graph V₁ E₁
G₂ : Graph V₂ E₂
f : Morphism G₁ G₂
v w : V₁
η : EdgePath G₁ v w
hyp : reduced (map η f)
η' : EdgePath G₁ v w
contra : Reduction η η'
⊢ Reduction (map η f) (map η' f)
Tactic:
apply map_of_reduction
Proof state after:
case a
V₁ : Type u_1
E₁ : Type u_2
V₂ : Type u_3
E₂ : Type u_4
V : Type u
E : Type v
G₁ : Graph V₁ E₁
G₂ : Graph V₂ E₂
f : Morphism G₁ G₂
v w : V₁
η : EdgePath G₁ v w
hyp : reduced (map η f)
η' : EdgePath G₁ v w
contra : Reduction η η'
⊢ Reduction η η'
Theorem: Graph.Morphism.reduced_of_image_reduced
Proof state before:
case a
V₁ : Type u_1
E₁ : Type u_2
V₂ : Type u_3
E₂ : Type u_4
V : Type u
E : Type v
G₁ : Graph V₁ E₁
G₂ : Graph V₂ E₂
f : Morphism G₁ G₂
v w : V₁
η : EdgePath G₁ v w
hyp : reduced (map η f)
η' : EdgePath G₁ v w
contra : Reduction η η'
⊢ Reduction η η'
Tactic:
exact contra
Proof state after:
no goals
Theorem: Graph.Morphism.comp_id
Proof state before:
V₁ : Type u_1
E₁ : Type u_2
V₂ : Type u_3
E₂ : Type u_4
V : Type u
E : Type v
G₁ : Graph V₁ E₁
G₂ : Graph V₂ E₂
f✝ f : Morphism G₁ G₂
⊢ comp Morphism.id f = f
Tactic:
cases f
Proof state after:
case mk
V₁ : Type u_1
E₁ : Type u_2
V₂ : Type u_3
E₂ : Type u_4
V : Type u
E : Type v
G₁ : Graph V₁ E₁
G₂ : Graph V₂ E₂
f : Morphism G₁ G₂
toFuncV✝ : V₁ → V₂
toFuncE✝ : E₁ → E₂
toFuncV_init✝ : ∀ (e : E₁), toFuncV✝ (G₁.ι e) = G₂.ι (toFuncE✝ e)
toFuncE_bar✝ : ∀ (e : E₁), toFuncE✝ (G₁.bar e) = G₂.bar (toFuncE✝ e)
⊢ comp Morphism.id
      { toFuncV := toFuncV✝, toFuncE := toFuncE✝, toFuncV_init := toFuncV_init✝, toFuncE_bar := toFuncE_bar✝ } =
    { toFuncV := toFuncV✝, toFuncE := toFuncE✝, toFuncV_init := toFuncV_init✝, toFuncE_bar := toFuncE_bar✝ }
Theorem: Graph.Morphism.comp_id
Proof state before:
case mk
V₁ : Type u_1
E₁ : Type u_2
V₂ : Type u_3
E₂ : Type u_4
V : Type u
E : Type v
G₁ : Graph V₁ E₁
G₂ : Graph V₂ E₂
f : Morphism G₁ G₂
toFuncV✝ : V₁ → V₂
toFuncE✝ : E₁ → E₂
toFuncV_init✝ : ∀ (e : E₁), toFuncV✝ (G₁.ι e) = G₂.ι (toFuncE✝ e)
toFuncE_bar✝ : ∀ (e : E₁), toFuncE✝ (G₁.bar e) = G₂.bar (toFuncE✝ e)
⊢ comp Morphism.id
      { toFuncV := toFuncV✝, toFuncE := toFuncE✝, toFuncV_init := toFuncV_init✝, toFuncE_bar := toFuncE_bar✝ } =
    { toFuncV := toFuncV✝, toFuncE := toFuncE✝, toFuncV_init := toFuncV_init✝, toFuncE_bar := toFuncE_bar✝ }
Tactic:
rfl
Proof state after:
no goals
Theorem: Graph.Morphism.id_comp
Proof state before:
V₁ : Type u_1
E₁ : Type u_2
V₂ : Type u_3
E₂ : Type u_4
V : Type u
E : Type v
G₁ : Graph V₁ E₁
G₂ : Graph V₂ E₂
f✝ f : Morphism G₁ G₂
⊢ comp Morphism.id f = f
Tactic:
cases f
Proof state after:
case mk
V₁ : Type u_1
E₁ : Type u_2
V₂ : Type u_3
E₂ : Type u_4
V : Type u
E : Type v
G₁ : Graph V₁ E₁
G₂ : Graph V₂ E₂
f : Morphism G₁ G₂
toFuncV✝ : V₁ → V₂
toFuncE✝ : E₁ → E₂
toFuncV_init✝ : ∀ (e : E₁), toFuncV✝ (G₁.ι e) = G₂.ι (toFuncE✝ e)
toFuncE_bar✝ : ∀ (e : E₁), toFuncE✝ (G₁.bar e) = G₂.bar (toFuncE✝ e)
⊢ comp Morphism.id
      { toFuncV := toFuncV✝, toFuncE := toFuncE✝, toFuncV_init := toFuncV_init✝, toFuncE_bar := toFuncE_bar✝ } =
    { toFuncV := toFuncV✝, toFuncE := toFuncE✝, toFuncV_init := toFuncV_init✝, toFuncE_bar := toFuncE_bar✝ }
Theorem: Graph.Morphism.id_comp
Proof state before:
case mk
V₁ : Type u_1
E₁ : Type u_2
V₂ : Type u_3
E₂ : Type u_4
V : Type u
E : Type v
G₁ : Graph V₁ E₁
G₂ : Graph V₂ E₂
f : Morphism G₁ G₂
toFuncV✝ : V₁ → V₂
toFuncE✝ : E₁ → E₂
toFuncV_init✝ : ∀ (e : E₁), toFuncV✝ (G₁.ι e) = G₂.ι (toFuncE✝ e)
toFuncE_bar✝ : ∀ (e : E₁), toFuncE✝ (G₁.bar e) = G₂.bar (toFuncE✝ e)
⊢ comp Morphism.id
      { toFuncV := toFuncV✝, toFuncE := toFuncE✝, toFuncV_init := toFuncV_init✝, toFuncE_bar := toFuncE_bar✝ } =
    { toFuncV := toFuncV✝, toFuncE := toFuncE✝, toFuncV_init := toFuncV_init✝, toFuncE_bar := toFuncE_bar✝ }
Tactic:
rfl
Proof state after:
no goals
Theorem: Graph.Morphism.comp_toFuncV
Proof state before:
V₁ : Type u_5
E₁ : Type u_6
V₂ : Type u_3
E₂ : Type u_4
V : Type u
E : Type v
G₁ : Graph V₁ E₁
G₂ : Graph V₂ E₂
f✝ : Morphism G₁ G₂
V₃ : Type u_1
E₃ : Type u_2
G₃ : Graph V₃ E₃
g : Morphism G₂ G₃
f : Morphism G₁ G₂
v : V₁
⊢ (comp g f).toFuncV v = g.toFuncV (f.toFuncV v)
Tactic:
rfl
Proof state after:
no goals
Theorem: Graph.Morphism.comp_toFuncE
Proof state before:
V₁ : Type u_5
E₁ : Type u_6
V₂ : Type u_3
E₂ : Type u_4
V : Type u
E : Type v
G₁ : Graph V₁ E₁
G₂ : Graph V₂ E₂
f✝ : Morphism G₁ G₂
V₃ : Type u_1
E₃ : Type u_2
G₃ : Graph V₃ E₃
g : Morphism G₂ G₃
f : Morphism G₁ G₂
e : E₁
⊢ (comp g f).toFuncE e = g.toFuncE (f.toFuncE e)
Tactic:
rfl
Proof state after:
no goals
Theorem: Graph.Morphism.comp_toFuncE'
Proof state before:
V₁ : Type u_5
E₁ : Type u_6
V₂ : Type u_3
E₂ : Type u_4
V : Type u
E : Type v
G₁ : Graph V₁ E₁
G₂ : Graph V₂ E₂
f✝ : Morphism G₁ G₂
V₃ : Type u_1
E₃ : Type u_2
G₃ : Graph V₃ E₃
g : Morphism G₂ G₃
f : Morphism G₁ G₂
⊢ (comp g f).toFuncE = g.toFuncE ∘ f.toFuncE
Tactic:
rfl
Proof state after:
no goals
Theorem: Graph.Morphism.comp_assoc
Proof state before:
V₁ : Type u_7
E₁ : Type u_8
V₂ : Type u_5
E₂ : Type u_6
V : Type u
E : Type v
G₁ : Graph V₁ E₁
G₂ : Graph V₂ E₂
f✝ : Morphism G₁ G₂
V₃ : Type u_1
E₃ : Type u_2
V✝ : Type u_3
E✝ : Type u_4
G₄ : Graph V✝ E✝
G₃ : Graph V₃ E₃
h : Morphism G₃ G₄
g : Morphism G₂ G₃
f : Morphism G₁ G₂
⊢ comp h (comp g f) = comp (comp h g) f
Tactic:
cases h
Proof state after:
case mk
V₁ : Type u_7
E₁ : Type u_8
V₂ : Type u_5
E₂ : Type u_6
V : Type u
E : Type v
G₁ : Graph V₁ E₁
G₂ : Graph V₂ E₂
f✝ : Morphism G₁ G₂
V₃ : Type u_1
E₃ : Type u_2
V✝ : Type u_3
E✝ : Type u_4
G₄ : Graph V✝ E✝
G₃ : Graph V₃ E₃
g : Morphism G₂ G₃
f : Morphism G₁ G₂
toFuncV✝ : V₃ → V✝
toFuncE✝ : E₃ → E✝
toFuncV_init✝ : ∀ (e : E₃), toFuncV✝ (G₃.ι e) = G₄.ι (toFuncE✝ e)
toFuncE_bar✝ : ∀ (e : E₃), toFuncE✝ (G₃.bar e) = G₄.bar (toFuncE✝ e)
⊢ comp { toFuncV := toFuncV✝, toFuncE := toFuncE✝, toFuncV_init := toFuncV_init✝, toFuncE_bar := toFuncE_bar✝ }
      (comp g f) =
    comp
      (comp { toFuncV := toFuncV✝, toFuncE := toFuncE✝, toFuncV_init := toFuncV_init✝, toFuncE_bar := toFuncE_bar✝ } g)
      f
Theorem: Graph.Morphism.comp_assoc
Proof state before:
case mk
V₁ : Type u_7
E₁ : Type u_8
V₂ : Type u_5
E₂ : Type u_6
V : Type u
E : Type v
G₁ : Graph V₁ E₁
G₂ : Graph V₂ E₂
f✝ : Morphism G₁ G₂
V₃ : Type u_1
E₃ : Type u_2
V✝ : Type u_3
E✝ : Type u_4
G₄ : Graph V✝ E✝
G₃ : Graph V₃ E₃
g : Morphism G₂ G₃
f : Morphism G₁ G₂
toFuncV✝ : V₃ → V✝
toFuncE✝ : E₃ → E✝
toFuncV_init✝ : ∀ (e : E₃), toFuncV✝ (G₃.ι e) = G₄.ι (toFuncE✝ e)
toFuncE_bar✝ : ∀ (e : E₃), toFuncE✝ (G₃.bar e) = G₄.bar (toFuncE✝ e)
⊢ comp { toFuncV := toFuncV✝, toFuncE := toFuncE✝, toFuncV_init := toFuncV_init✝, toFuncE_bar := toFuncE_bar✝ }
      (comp g f) =
    comp
      (comp { toFuncV := toFuncV✝, toFuncE := toFuncE✝, toFuncV_init := toFuncV_init✝, toFuncE_bar := toFuncE_bar✝ } g)
      f
Tactic:
cases g
Proof state after:
case mk.mk
V₁ : Type u_7
E₁ : Type u_8
V₂ : Type u_5
E₂ : Type u_6
V : Type u
E : Type v
G₁ : Graph V₁ E₁
G₂ : Graph V₂ E₂
f✝ : Morphism G₁ G₂
V₃ : Type u_1
E₃ : Type u_2
V✝ : Type u_3
E✝ : Type u_4
G₄ : Graph V✝ E✝
G₃ : Graph V₃ E₃
f : Morphism G₁ G₂
toFuncV✝¹ : V₃ → V✝
toFuncE✝¹ : E₃ → E✝
toFuncV_init✝¹ : ∀ (e : E₃), toFuncV✝¹ (G₃.ι e) = G₄.ι (toFuncE✝¹ e)
toFuncE_bar✝¹ : ∀ (e : E₃), toFuncE✝¹ (G₃.bar e) = G₄.bar (toFuncE✝¹ e)
toFuncV✝ : V₂ → V₃
toFuncE✝ : E₂ → E₃
toFuncV_init✝ : ∀ (e : E₂), toFuncV✝ (G₂.ι e) = G₃.ι (toFuncE✝ e)
toFuncE_bar✝ : ∀ (e : E₂), toFuncE✝ (G₂.bar e) = G₃.bar (toFuncE✝ e)
⊢ comp { toFuncV := toFuncV✝¹, toFuncE := toFuncE✝¹, toFuncV_init := toFuncV_init✝¹, toFuncE_bar := toFuncE_bar✝¹ }
      (comp { toFuncV := toFuncV✝, toFuncE := toFuncE✝, toFuncV_init := toFuncV_init✝, toFuncE_bar := toFuncE_bar✝ }
        f) =
    comp
      (comp { toFuncV := toFuncV✝¹, toFuncE := toFuncE✝¹, toFuncV_init := toFuncV_init✝¹, toFuncE_bar := toFuncE_bar✝¹ }
        { toFuncV := toFuncV✝, toFuncE := toFuncE✝, toFuncV_init := toFuncV_init✝, toFuncE_bar := toFuncE_bar✝ })
      f
Theorem: Graph.Morphism.comp_assoc
Proof state before:
case mk.mk
V₁ : Type u_7
E₁ : Type u_8
V₂ : Type u_5
E₂ : Type u_6
V : Type u
E : Type v
G₁ : Graph V₁ E₁
G₂ : Graph V₂ E₂
f✝ : Morphism G₁ G₂
V₃ : Type u_1
E₃ : Type u_2
V✝ : Type u_3
E✝ : Type u_4
G₄ : Graph V✝ E✝
G₃ : Graph V₃ E₃
f : Morphism G₁ G₂
toFuncV✝¹ : V₃ → V✝
toFuncE✝¹ : E₃ → E✝
toFuncV_init✝¹ : ∀ (e : E₃), toFuncV✝¹ (G₃.ι e) = G₄.ι (toFuncE✝¹ e)
toFuncE_bar✝¹ : ∀ (e : E₃), toFuncE✝¹ (G₃.bar e) = G₄.bar (toFuncE✝¹ e)
toFuncV✝ : V₂ → V₃
toFuncE✝ : E₂ → E₃
toFuncV_init✝ : ∀ (e : E₂), toFuncV✝ (G₂.ι e) = G₃.ι (toFuncE✝ e)
toFuncE_bar✝ : ∀ (e : E₂), toFuncE✝ (G₂.bar e) = G₃.bar (toFuncE✝ e)
⊢ comp { toFuncV := toFuncV✝¹, toFuncE := toFuncE✝¹, toFuncV_init := toFuncV_init✝¹, toFuncE_bar := toFuncE_bar✝¹ }
      (comp { toFuncV := toFuncV✝, toFuncE := toFuncE✝, toFuncV_init := toFuncV_init✝, toFuncE_bar := toFuncE_bar✝ }
        f) =
    comp
      (comp { toFuncV := toFuncV✝¹, toFuncE := toFuncE✝¹, toFuncV_init := toFuncV_init✝¹, toFuncE_bar := toFuncE_bar✝¹ }
        { toFuncV := toFuncV✝, toFuncE := toFuncE✝, toFuncV_init := toFuncV_init✝, toFuncE_bar := toFuncE_bar✝ })
      f
Tactic:
cases f
Proof state after:
case mk.mk.mk
V₁ : Type u_7
E₁ : Type u_8
V₂ : Type u_5
E₂ : Type u_6
V : Type u
E : Type v
G₁ : Graph V₁ E₁
G₂ : Graph V₂ E₂
f : Morphism G₁ G₂
V₃ : Type u_1
E₃ : Type u_2
V✝ : Type u_3
E✝ : Type u_4
G₄ : Graph V✝ E✝
G₃ : Graph V₃ E₃
toFuncV✝² : V₃ → V✝
toFuncE✝² : E₃ → E✝
toFuncV_init✝² : ∀ (e : E₃), toFuncV✝² (G₃.ι e) = G₄.ι (toFuncE✝² e)
toFuncE_bar✝² : ∀ (e : E₃), toFuncE✝² (G₃.bar e) = G₄.bar (toFuncE✝² e)
toFuncV✝¹ : V₂ → V₃
toFuncE✝¹ : E₂ → E₃
toFuncV_init✝¹ : ∀ (e : E₂), toFuncV✝¹ (G₂.ι e) = G₃.ι (toFuncE✝¹ e)
toFuncE_bar✝¹ : ∀ (e : E₂), toFuncE✝¹ (G₂.bar e) = G₃.bar (toFuncE✝¹ e)
toFuncV✝ : V₁ → V₂
toFuncE✝ : E₁ → E₂
toFuncV_init✝ : ∀ (e : E₁), toFuncV✝ (G₁.ι e) = G₂.ι (toFuncE✝ e)
toFuncE_bar✝ : ∀ (e : E₁), toFuncE✝ (G₁.bar e) = G₂.bar (toFuncE✝ e)
⊢ comp { toFuncV := toFuncV✝², toFuncE := toFuncE✝², toFuncV_init := toFuncV_init✝², toFuncE_bar := toFuncE_bar✝² }
      (comp { toFuncV := toFuncV✝¹, toFuncE := toFuncE✝¹, toFuncV_init := toFuncV_init✝¹, toFuncE_bar := toFuncE_bar✝¹ }
        { toFuncV := toFuncV✝, toFuncE := toFuncE✝, toFuncV_init := toFuncV_init✝, toFuncE_bar := toFuncE_bar✝ }) =
    comp
      (comp { toFuncV := toFuncV✝², toFuncE := toFuncE✝², toFuncV_init := toFuncV_init✝², toFuncE_bar := toFuncE_bar✝² }
        { toFuncV := toFuncV✝¹, toFuncE := toFuncE✝¹, toFuncV_init := toFuncV_init✝¹, toFuncE_bar := toFuncE_bar✝¹ })
      { toFuncV := toFuncV✝, toFuncE := toFuncE✝, toFuncV_init := toFuncV_init✝, toFuncE_bar := toFuncE_bar✝ }
Theorem: Graph.Morphism.comp_assoc
Proof state before:
case mk.mk.mk
V₁ : Type u_7
E₁ : Type u_8
V₂ : Type u_5
E₂ : Type u_6
V : Type u
E : Type v
G₁ : Graph V₁ E₁
G₂ : Graph V₂ E₂
f : Morphism G₁ G₂
V₃ : Type u_1
E₃ : Type u_2
V✝ : Type u_3
E✝ : Type u_4
G₄ : Graph V✝ E✝
G₃ : Graph V₃ E₃
toFuncV✝² : V₃ → V✝
toFuncE✝² : E₃ → E✝
toFuncV_init✝² : ∀ (e : E₃), toFuncV✝² (G₃.ι e) = G₄.ι (toFuncE✝² e)
toFuncE_bar✝² : ∀ (e : E₃), toFuncE✝² (G₃.bar e) = G₄.bar (toFuncE✝² e)
toFuncV✝¹ : V₂ → V₃
toFuncE✝¹ : E₂ → E₃
toFuncV_init✝¹ : ∀ (e : E₂), toFuncV✝¹ (G₂.ι e) = G₃.ι (toFuncE✝¹ e)
toFuncE_bar✝¹ : ∀ (e : E₂), toFuncE✝¹ (G₂.bar e) = G₃.bar (toFuncE✝¹ e)
toFuncV✝ : V₁ → V₂
toFuncE✝ : E₁ → E₂
toFuncV_init✝ : ∀ (e : E₁), toFuncV✝ (G₁.ι e) = G₂.ι (toFuncE✝ e)
toFuncE_bar✝ : ∀ (e : E₁), toFuncE✝ (G₁.bar e) = G₂.bar (toFuncE✝ e)
⊢ comp { toFuncV := toFuncV✝², toFuncE := toFuncE✝², toFuncV_init := toFuncV_init✝², toFuncE_bar := toFuncE_bar✝² }
      (comp { toFuncV := toFuncV✝¹, toFuncE := toFuncE✝¹, toFuncV_init := toFuncV_init✝¹, toFuncE_bar := toFuncE_bar✝¹ }
        { toFuncV := toFuncV✝, toFuncE := toFuncE✝, toFuncV_init := toFuncV_init✝, toFuncE_bar := toFuncE_bar✝ }) =
    comp
      (comp { toFuncV := toFuncV✝², toFuncE := toFuncE✝², toFuncV_init := toFuncV_init✝², toFuncE_bar := toFuncE_bar✝² }
        { toFuncV := toFuncV✝¹, toFuncE := toFuncE✝¹, toFuncV_init := toFuncV_init✝¹, toFuncE_bar := toFuncE_bar✝¹ })
      { toFuncV := toFuncV✝, toFuncE := toFuncE✝, toFuncV_init := toFuncV_init✝, toFuncE_bar := toFuncE_bar✝ }
Tactic:
rfl
Proof state after:
no goals
Theorem: Graph.PathClass.map_on_quotient
Proof state before:
V₁ : Type u_1
E₁ : Type u_2
V₂ : Type u_4
E₂ : Type u_3
V : Type u
E : Type v
G₁ : Graph V₁ E₁
G₂ : Graph V₂ E₂
f : Morphism G₁ G₂
v w : V₁
η : EdgePath G₁ v w
⊢ map f [[η]] = [[EdgePath.map η f]]
Tactic:
rfl
Proof state after:
no goals