internlm/Lean-Github huggingface dataset:
Theorem: GroupLabelledGraph.pathClassLabel_append
Proof state before:
case mk
V : Type u_1
E : Type u_2
G : Type u_3
Γ : Graph V E
inst✝ : Group G
u✝ v✝ w✝ : V
g h : G
𝓖 : GroupLabelledGraph Γ G
u v w : V
p : Graph.EdgePath Γ u v
⊢ ∀ (p' : v ⟶ w),
    pathClassLabel 𝓖 (Quot.mk Graph.EdgePath.Reduction p ≫ p') =
      pathClassLabel 𝓖 (Quot.mk Graph.EdgePath.Reduction p) * pathClassLabel 𝓖 p'
Tactic:
apply Quot.ind
Proof state after:
case mk.mk
V : Type u_1
E : Type u_2
G : Type u_3
Γ : Graph V E
inst✝ : Group G
u✝ v✝ w✝ : V
g h : G
𝓖 : GroupLabelledGraph Γ G
u v w : V
p : Graph.EdgePath Γ u v
⊢ ∀ (a : Graph.EdgePath Γ v w),
    pathClassLabel 𝓖 (Quot.mk Graph.EdgePath.Reduction p ≫ Quot.mk Graph.EdgePath.Reduction a) =
      pathClassLabel 𝓖 (Quot.mk Graph.EdgePath.Reduction p) * pathClassLabel 𝓖 (Quot.mk Graph.EdgePath.Reduction a)
Theorem: GroupLabelledGraph.pathClassLabel_append
Proof state before:
case mk.mk
V : Type u_1
E : Type u_2
G : Type u_3
Γ : Graph V E
inst✝ : Group G
u✝ v✝ w✝ : V
g h : G
𝓖 : GroupLabelledGraph Γ G
u v w : V
p : Graph.EdgePath Γ u v
⊢ ∀ (a : Graph.EdgePath Γ v w),
    pathClassLabel 𝓖 (Quot.mk Graph.EdgePath.Reduction p ≫ Quot.mk Graph.EdgePath.Reduction a) =
      pathClassLabel 𝓖 (Quot.mk Graph.EdgePath.Reduction p) * pathClassLabel 𝓖 (Quot.mk Graph.EdgePath.Reduction a)
Tactic:
intro p'
Proof state after:
case mk.mk
V : Type u_1
E : Type u_2
G : Type u_3
Γ : Graph V E
inst✝ : Group G
u✝ v✝ w✝ : V
g h : G
𝓖 : GroupLabelledGraph Γ G
u v w : V
p : Graph.EdgePath Γ u v
p' : Graph.EdgePath Γ v w
⊢ pathClassLabel 𝓖 (Quot.mk Graph.EdgePath.Reduction p ≫ Quot.mk Graph.EdgePath.Reduction p') =
    pathClassLabel 𝓖 (Quot.mk Graph.EdgePath.Reduction p) * pathClassLabel 𝓖 (Quot.mk Graph.EdgePath.Reduction p')
Theorem: GroupLabelledGraph.pathClassLabel_append
Proof state before:
case mk.mk
V : Type u_1
E : Type u_2
G : Type u_3
Γ : Graph V E
inst✝ : Group G
u✝ v✝ w✝ : V
g h : G
𝓖 : GroupLabelledGraph Γ G
u v w : V
p : Graph.EdgePath Γ u v
p' : Graph.EdgePath Γ v w
⊢ pathClassLabel 𝓖 (Quot.mk Graph.EdgePath.Reduction p ≫ Quot.mk Graph.EdgePath.Reduction p') =
    pathClassLabel 𝓖 (Quot.mk Graph.EdgePath.Reduction p) * pathClassLabel 𝓖 (Quot.mk Graph.EdgePath.Reduction p')
Tactic:
show 𝓖.pathLabel (_ ++ _) = _
Proof state after:
case mk.mk
V : Type u_1
E : Type u_2
G : Type u_3
Γ : Graph V E
inst✝ : Group G
u✝ v✝ w✝ : V
g h : G
𝓖 : GroupLabelledGraph Γ G
u v w : V
p : Graph.EdgePath Γ u v
p' : Graph.EdgePath Γ v w
⊢ pathLabel 𝓖 (p ++ p') =
    pathClassLabel 𝓖 (Quot.mk Graph.EdgePath.Reduction p) * pathClassLabel 𝓖 (Quot.mk Graph.EdgePath.Reduction p')
Theorem: GroupLabelledGraph.pathClassLabel_append
Proof state before:
case mk.mk
V : Type u_1
E : Type u_2
G : Type u_3
Γ : Graph V E
inst✝ : Group G
u✝ v✝ w✝ : V
g h : G
𝓖 : GroupLabelledGraph Γ G
u v w : V
p : Graph.EdgePath Γ u v
p' : Graph.EdgePath Γ v w
⊢ pathLabel 𝓖 (p ++ p') =
    pathClassLabel 𝓖 (Quot.mk Graph.EdgePath.Reduction p) * pathClassLabel 𝓖 (Quot.mk Graph.EdgePath.Reduction p')
Tactic:
simp only [pathLabel_append, pathClassLabel]
Proof state after:
no goals
Theorem: Graph.τ_bar
Proof state before:
V : Type u
E : Type v
G : Graph V E
u v w : V
e : E
⊢ τ G (G.bar e) = G.ι e
Tactic:
aesop (add norm unfold [τ])
Proof state after:
no goals
Theorem: Graph.EdgeBetween.bar_bar
Proof state before:
V : Type u
E : Type v
G : Graph V E
u v w : V
e : EdgeBetween G v w
⊢ bar (bar e) = e
Tactic:
ext
Proof state after:
case edge
V : Type u
E : Type v
G : Graph V E
u v w : V
e : EdgeBetween G v w
⊢ (bar (bar e)).edge = e.edge
Theorem: Graph.EdgeBetween.bar_bar
Proof state before:
case edge
V : Type u
E : Type v
G : Graph V E
u v w : V
e : EdgeBetween G v w
⊢ (bar (bar e)).edge = e.edge
Tactic:
aesop (add norm simp [EdgeBetween.bar])
Proof state after:
no goals
Theorem: Graph.EdgePath.concat_cons
Proof state before:
V : Type u
E : Type v
G : Graph V E
u✝ v✝ w✝ : V
e✝ : EdgeBetween G v✝ w✝
v w u u' : V
e : EdgeBetween G v w
p : EdgePath G w u
e' : EdgeBetween G u u'
⊢ concat (cons e p) e' = cons e (concat p e')
Tactic:
rfl
Proof state after:
no goals
Theorem: Graph.EdgePath.reverse_nil
Proof state before:
V : Type u
E : Type v
G : Graph V E
u v✝ w : V
e : EdgeBetween G v✝ w
v : V
⊢ reverse (nil v) = nil v
Tactic:
rfl
Proof state after:
no goals
Theorem: Graph.EdgePath.reverse_cons
Proof state before:
V : Type u
E : Type v
G : Graph V E
u✝ v✝ w✝ : V
e✝ : EdgeBetween G v✝ w✝
v w u : V
e : EdgeBetween G v w
p : EdgePath G w u
⊢ reverse (cons e p) = concat (reverse p) (EdgeBetween.bar e)
Tactic:
rfl
Proof state after:
no goals
Theorem: Graph.EdgePath.reverse_concat
Proof state before:
V : Type u
E : Type v
G : Graph V E
u✝ v✝ w✝ : V
e✝ : EdgeBetween G v✝ w✝
v w u : V
p : EdgePath G v w
e : EdgeBetween G w u
⊢ reverse (concat p e) = cons (EdgeBetween.bar e) (reverse p)
Tactic:
induction p <;> aesop (add norm simp [concat_cons, reverse_cons])
Proof state after:
no goals
Theorem: Graph.EdgePath.append_nil
Proof state before:
V : Type u
E : Type v
G : Graph V E
u✝ v✝ w : V
e : EdgeBetween G v✝ w
u v : V
p : EdgePath G u v
⊢ p ++ nil v = p
Tactic:
show append _ _ = _
Proof state after:
V : Type u
E : Type v
G : Graph V E
u✝ v✝ w : V
e : EdgeBetween G v✝ w
u v : V
p : EdgePath G u v
⊢ append p (nil v) = p
Theorem: Graph.EdgePath.append_nil
Proof state before:
V : Type u
E : Type v
G : Graph V E
u✝ v✝ w : V
e : EdgeBetween G v✝ w
u v : V
p : EdgePath G u v
⊢ append p (nil v) = p
Tactic:
induction p <;> aesop (add norm simp [append])
Proof state after:
no goals
Theorem: Graph.EdgePath.cons_append
Proof state before:
V : Type u
E : Type v
G : Graph V E
u✝ v✝ w✝ : V
e✝ : EdgeBetween G v✝ w✝
v' v w u : V
e : EdgeBetween G v' v
p : EdgePath G v w
q : EdgePath G w u
⊢ cons e p ++ q = cons e (p ++ q)
Tactic:
rfl
Proof state after:
no goals
Theorem: Graph.EdgePath.concat_append
Proof state before:
V : Type u
E : Type v
G : Graph V E
u✝ v✝ w✝ : V
e✝ : EdgeBetween G v✝ w✝
v w w' u : V
e : EdgeBetween G w w'
p : EdgePath G v w
q : EdgePath G w' u
⊢ concat p e ++ q = p ++ cons e q
Tactic:
induction p <;> aesop
Proof state after:
no goals
Theorem: Graph.EdgePath.append_concat
Proof state before:
V : Type u
E : Type v
G : Graph V E
u✝ v✝ w✝ : V
e✝ : EdgeBetween G v✝ w✝
v w w' u : V
e : EdgeBetween G w' u
p : EdgePath G v w
q : EdgePath G w w'
⊢ p ++ concat q e = concat (p ++ q) e
Tactic:
induction p <;> aesop
Proof state after:
no goals
Theorem: Graph.EdgePath.concat_eq_append_edge
Proof state before:
V : Type u
E : Type v
G : Graph V E
u✝ v✝ w✝ : V
e✝ : EdgeBetween G v✝ w✝
v w u : V
e : EdgeBetween G w u
p : EdgePath G v w
⊢ concat p e = p ++ cons e (nil u)
Tactic:
have := concat_append e p (.nil _)
Proof state after:
V : Type u
E : Type v
G : Graph V E
u✝ v✝ w✝ : V
e✝ : EdgeBetween G v✝ w✝
v w u : V
e : EdgeBetween G w u
p : EdgePath G v w
this : concat p e ++ nil u = p ++ cons e (nil u)
⊢ concat p e = p ++ cons e (nil u)
Theorem: Graph.EdgePath.concat_eq_append_edge
Proof state before:
V : Type u
E : Type v
G : Graph V E
u✝ v✝ w✝ : V
e✝ : EdgeBetween G v✝ w✝
v w u : V
e : EdgeBetween G w u
p : EdgePath G v w
this : concat p e ++ nil u = p ++ cons e (nil u)
⊢ concat p e = p ++ cons e (nil u)
Tactic:
aesop
Proof state after:
no goals
Theorem: Graph.EdgePath.append_assoc
Proof state before:
V : Type u
E : Type v
G : Graph V E
u✝ v✝ w✝ : V
e : EdgeBetween G v✝ w✝
v w u u' : V
p : EdgePath G v w
q : EdgePath G w u
r : EdgePath G u u'
⊢ p ++ q ++ r = p ++ (q ++ r)
Tactic:
induction p <;> aesop
Proof state after:
no goals
Theorem: Graph.EdgePath.reverse_reverse
Proof state before:
V : Type u
E : Type v
G : Graph V E
u v✝ w✝ : V
e : EdgeBetween G v✝ w✝
v w : V
p : EdgePath G v w
⊢ reverse (reverse p) = p
Tactic:
induction p <;> aesop (add norm simp [reverse_cons, reverse_concat])
Proof state after:
no goals
Theorem: Graph.EdgePath.reverse_append
Proof state before:
V : Type u
E : Type v
G : Graph V E
u✝ v✝ w✝ : V
e : EdgeBetween G v✝ w✝
u v w : V
p : EdgePath G u v
q : EdgePath G v w
⊢ reverse (p ++ q) = reverse q ++ reverse p
Tactic:
induction p <;>
  aesop (add norm simp [reverse_cons, concat_eq_append_edge, append_assoc])
Proof state after:
no goals
Theorem: Graph.append_cons_bar_cons
Proof state before:
V : Type u
E : Type v
G : Graph V E
u v w : V
e✝ : EdgeBetween G v w
u' : V
e : EdgeBetween G u u'
p₁ : EdgePath G v u
p₂ : EdgePath G u w
⊢ [[p₁ ++ cons e (cons (EdgeBetween.bar e) p₂)]] = [[p₁ ++ p₂]]
Tactic:
have := Reduction.step e p₁ p₂
Proof state after:
V : Type u
E : Type v
G : Graph V E
u v w : V
e✝ : EdgeBetween G v w
u' : V
e : EdgeBetween G u u'
p₁ : EdgePath G v u
p₂ : EdgePath G u w
this : Reduction (p₁ ++ cons e (cons (EdgeBetween.bar e) p₂)) (p₁ ++ p₂)
⊢ [[p₁ ++ cons e (cons (EdgeBetween.bar e) p₂)]] = [[p₁ ++ p₂]]
Theorem: Graph.append_cons_bar_cons
Proof state before:
V : Type u
E : Type v
G : Graph V E
u v w : V
e✝ : EdgeBetween G v w
u' : V
e : EdgeBetween G u u'
p₁ : EdgePath G v u
p₂ : EdgePath G u w
this : Reduction (p₁ ++ cons e (cons (EdgeBetween.bar e) p₂)) (p₁ ++ p₂)
⊢ [[p₁ ++ cons e (cons (EdgeBetween.bar e) p₂)]] = [[p₁ ++ p₂]]
Tactic:
aesop
Proof state after:
no goals
Theorem: Graph.append_cons_cons_bar
Proof state before:
V : Type u
E : Type v
G : Graph V E
u v w : V
e✝ : EdgeBetween G v w
u' : V
e : EdgeBetween G u' u
p₁ : EdgePath G v u
p₂ : EdgePath G u w
⊢ [[p₁ ++ cons (EdgeBetween.bar e) (cons e p₂)]] = [[p₁ ++ p₂]]
Tactic:
have := append_cons_bar_cons e.bar p₁ p₂
Proof state after:
V : Type u
E : Type v
G : Graph V E
u v w : V
e✝ : EdgeBetween G v w
u' : V
e : EdgeBetween G u' u
p₁ : EdgePath G v u
p₂ : EdgePath G u w
this : [[p₁ ++ cons (EdgeBetween.bar e) (cons (EdgeBetween.bar (EdgeBetween.bar e)) p₂)]] = [[p₁ ++ p₂]]
⊢ [[p₁ ++ cons (EdgeBetween.bar e) (cons e p₂)]] = [[p₁ ++ p₂]]
Theorem: Graph.append_cons_cons_bar
Proof state before:
V : Type u
E : Type v
G : Graph V E
u v w : V
e✝ : EdgeBetween G v w
u' : V
e : EdgeBetween G u' u
p₁ : EdgePath G v u
p₂ : EdgePath G u w
this : [[p₁ ++ cons (EdgeBetween.bar e) (cons (EdgeBetween.bar (EdgeBetween.bar e)) p₂)]] = [[p₁ ++ p₂]]
⊢ [[p₁ ++ cons (EdgeBetween.bar e) (cons e p₂)]] = [[p₁ ++ p₂]]
Tactic:
aesop
Proof state after:
no goals
Theorem: Graph.left_append_step
Proof state before:
V : Type u
E : Type v
G : Graph V E
u✝ v✝ w✝ : V
e : EdgeBetween G v✝ w✝
v w u : V
a : EdgePath G v w
b₁ b₂ : EdgePath G w u
rel : Reduction b₁ b₂
⊢ [[a ++ b₁]] = [[a ++ b₂]]
Tactic:
induction rel
Proof state after:
case step
V : Type u
E : Type v
G : Graph V E
u✝¹ v✝ w✝ : V
e : EdgeBetween G v✝ w✝
v w u : V
a : EdgePath G v w
b₁ b₂ : EdgePath G w u
u✝ u'✝ : V
e✝ : EdgeBetween G u✝ u'✝
p₁✝ : EdgePath G w u✝
p₂✝ : EdgePath G u✝ u
⊢ [[a ++ (p₁✝ ++ cons e✝ (cons (EdgeBetween.bar e✝) p₂✝))]] = [[a ++ (p₁✝ ++ p₂✝)]]
Theorem: Graph.left_append_step
Proof state before:
case step
V : Type u
E : Type v
G : Graph V E
u✝¹ v✝ w✝ : V
e : EdgeBetween G v✝ w✝
v w u : V
a : EdgePath G v w
b₁ b₂ : EdgePath G w u
u✝ u'✝ : V
e✝ : EdgeBetween G u✝ u'✝
p₁✝ : EdgePath G w u✝
p₂✝ : EdgePath G u✝ u
⊢ [[a ++ (p₁✝ ++ cons e✝ (cons (EdgeBetween.bar e✝) p₂✝))]] = [[a ++ (p₁✝ ++ p₂✝)]]
Tactic:
repeat (rw [← append_assoc])
Proof state after:
case step
V : Type u
E : Type v
G : Graph V E
u✝¹ v✝ w✝ : V
e : EdgeBetween G v✝ w✝
v w u : V
a : EdgePath G v w
b₁ b₂ : EdgePath G w u
u✝ u'✝ : V
e✝ : EdgeBetween G u✝ u'✝
p₁✝ : EdgePath G w u✝
p₂✝ : EdgePath G u✝ u
⊢ [[a ++ p₁✝ ++ cons e✝ (cons (EdgeBetween.bar e✝) p₂✝)]] = [[a ++ p₁✝ ++ p₂✝]]
Theorem: Graph.left_append_step
Proof state before:
case step
V : Type u
E : Type v
G : Graph V E
u✝¹ v✝ w✝ : V
e : EdgeBetween G v✝ w✝
v w u : V
a : EdgePath G v w
b₁ b₂ : EdgePath G w u
u✝ u'✝ : V
e✝ : EdgeBetween G u✝ u'✝
p₁✝ : EdgePath G w u✝
p₂✝ : EdgePath G u✝ u
⊢ [[a ++ p₁✝ ++ cons e✝ (cons (EdgeBetween.bar e✝) p₂✝)]] = [[a ++ p₁✝ ++ p₂✝]]
Tactic:
aesop
Proof state after:
no goals
Theorem: Graph.left_append_step
Proof state before:
case step
V : Type u
E : Type v
G : Graph V E
u✝¹ v✝ w✝ : V
e : EdgeBetween G v✝ w✝
v w u : V
a : EdgePath G v w
b₁ b₂ : EdgePath G w u
u✝ u'✝ : V
e✝ : EdgeBetween G u✝ u'✝
p₁✝ : EdgePath G w u✝
p₂✝ : EdgePath G u✝ u
⊢ [[a ++ p₁✝ ++ cons e✝ (cons (EdgeBetween.bar e✝) p₂✝)]] = [[a ++ (p₁✝ ++ p₂✝)]]
Tactic:
(rw [← append_assoc])
Proof state after:
case step
V : Type u
E : Type v
G : Graph V E
u✝¹ v✝ w✝ : V
e : EdgeBetween G v✝ w✝
v w u : V
a : EdgePath G v w
b₁ b₂ : EdgePath G w u
u✝ u'✝ : V
e✝ : EdgeBetween G u✝ u'✝
p₁✝ : EdgePath G w u✝
p₂✝ : EdgePath G u✝ u
⊢ [[a ++ p₁✝ ++ cons e✝ (cons (EdgeBetween.bar e✝) p₂✝)]] = [[a ++ p₁✝ ++ p₂✝]]
Theorem: Graph.left_append_step
Proof state before:
case step
V : Type u
E : Type v
G : Graph V E
u✝¹ v✝ w✝ : V
e : EdgeBetween G v✝ w✝
v w u : V
a : EdgePath G v w
b₁ b₂ : EdgePath G w u
u✝ u'✝ : V
e✝ : EdgeBetween G u✝ u'✝
p₁✝ : EdgePath G w u✝
p₂✝ : EdgePath G u✝ u
⊢ [[a ++ p₁✝ ++ cons e✝ (cons (EdgeBetween.bar e✝) p₂✝)]] = [[a ++ (p₁✝ ++ p₂✝)]]
Tactic:
rw [← append_assoc]
Proof state after:
case step
V : Type u
E : Type v
G : Graph V E
u✝¹ v✝ w✝ : V
e : EdgeBetween G v✝ w✝
v w u : V
a : EdgePath G v w
b₁ b₂ : EdgePath G w u
u✝ u'✝ : V
e✝ : EdgeBetween G u✝ u'✝
p₁✝ : EdgePath G w u✝
p₂✝ : EdgePath G u✝ u
⊢ [[a ++ p₁✝ ++ cons e✝ (cons (EdgeBetween.bar e✝) p₂✝)]] = [[a ++ p₁✝ ++ p₂✝]]
Theorem: Graph.right_append_step
Proof state before:
V : Type u
E : Type v
G : Graph V E
u✝ v✝ w✝ : V
e : EdgeBetween G v✝ w✝
v w u : V
a₁ a₂ : EdgePath G v w
b : EdgePath G w u
rel : Reduction a₁ a₂
⊢ [[a₁ ++ b]] = [[a₂ ++ b]]
Tactic:
aesop (add norm simp [append_assoc])
Proof state after:
no goals
Theorem: Graph.reverse_step
Proof state before:
V : Type u
E : Type v
G : Graph V E
u v✝ w✝ : V
e : EdgeBetween G v✝ w✝
v w : V
a₁ a₂ : EdgePath G v w
rel : Reduction a₁ a₂
⊢ [[reverse a₁]] = [[reverse a₂]]
Tactic:
induction rel
Proof state after:
case step
V : Type u
E : Type v
G : Graph V E
u v✝ w✝ : V
e : EdgeBetween G v✝ w✝
v w : V
a₁ a₂ : EdgePath G v w
u✝ u'✝ : V
e✝ : EdgeBetween G u✝ u'✝
p₁✝ : EdgePath G v u✝
p₂✝ : EdgePath G u✝ w
⊢ [[reverse (p₁✝ ++ cons e✝ (cons (EdgeBetween.bar e✝) p₂✝))]] = [[reverse (p₁✝ ++ p₂✝)]]
Theorem: Graph.reverse_step
Proof state before:
case step
V : Type u
E : Type v
G : Graph V E
u v✝ w✝ : V
e : EdgeBetween G v✝ w✝
v w : V
a₁ a₂ : EdgePath G v w
u✝ u'✝ : V
e✝ : EdgeBetween G u✝ u'✝
p₁✝ : EdgePath G v u✝
p₂✝ : EdgePath G u✝ w
⊢ [[reverse (p₁✝ ++ cons e✝ (cons (EdgeBetween.bar e✝) p₂✝))]] = [[reverse (p₁✝ ++ p₂✝)]]
Tactic:
aesop (add norm simp [reverse_append, reverse_cons])
Proof state after:
no goals
Theorem: Graph.reverse_append_self
Proof state before:
V : Type u
E : Type v
G : Graph V E
u v✝ w✝ : V
e : EdgeBetween G v✝ w✝
v w : V
p : EdgePath G v w
⊢ [[reverse p ++ p]] = [[nil w]]
Tactic:
induction p <;>
  aesop (add norm simp [reverse_cons, reverse_concat, cons_append])
Proof state after:
no goals
Theorem: Graph.self_append_reverse
Proof state before:
V : Type u
E : Type v
G : Graph V E
u v✝ w✝ : V
e : EdgeBetween G v✝ w✝
v w : V
p : EdgePath G w v
⊢ [[p ++ reverse p]] = [[nil w]]
Tactic:
have := reverse_append_self p.reverse
Proof state after:
V : Type u
E : Type v
G : Graph V E
u v✝ w✝ : V
e : EdgeBetween G v✝ w✝
v w : V
p : EdgePath G w v
this : [[reverse (reverse p) ++ reverse p]] = [[nil w]]
⊢ [[p ++ reverse p]] = [[nil w]]
Theorem: Graph.self_append_reverse
Proof state before:
V : Type u
E : Type v
G : Graph V E
u v✝ w✝ : V
e : EdgeBetween G v✝ w✝
v w : V
p : EdgePath G w v
this : [[reverse (reverse p) ++ reverse p]] = [[nil w]]
⊢ [[p ++ reverse p]] = [[nil w]]
Tactic:
aesop
Proof state after:
no goals
Theorem: Graph.PathClass.id_mul
Proof state before:
V : Type u
E : Type v
G : Graph V E
u✝ v✝ w : V
e : EdgeBetween G v✝ w
u v : V
⊢ ∀ (p : PathClass G u v), mul (PathClass.id u) p = p
Tactic:
apply Quot.ind
Proof state after:
case mk
V : Type u
E : Type v
G : Graph V E
u✝ v✝ w : V
e : EdgeBetween G v✝ w
u v : V
⊢ ∀ (a : EdgePath G u v), mul (PathClass.id u) (Quot.mk Reduction a) = Quot.mk Reduction a
Theorem: Graph.PathClass.id_mul
Proof state before:
case mk
V : Type u
E : Type v
G : Graph V E
u✝ v✝ w : V
e : EdgeBetween G v✝ w
u v : V
⊢ ∀ (a : EdgePath G u v), mul (PathClass.id u) (Quot.mk Reduction a) = Quot.mk Reduction a
Tactic:
aesop
Proof state after:
no goals
Theorem: Graph.PathClass.mul_id
Proof state before:
V : Type u
E : Type v
G : Graph V E
u✝ v✝ w : V
e : EdgeBetween G v✝ w
u v : V
⊢ ∀ (p : PathClass G u v), mul p (PathClass.id v) = p
Tactic:
apply Quot.ind
Proof state after:
case mk
V : Type u
E : Type v
G : Graph V E
u✝ v✝ w : V
e : EdgeBetween G v✝ w
u v : V
⊢ ∀ (a : EdgePath G u v), mul (Quot.mk Reduction a) (PathClass.id v) = Quot.mk Reduction a
Theorem: Graph.PathClass.mul_id
Proof state before:
case mk
V : Type u
E : Type v
G : Graph V E
u✝ v✝ w : V
e : EdgeBetween G v✝ w
u v : V
⊢ ∀ (a : EdgePath G u v), mul (Quot.mk Reduction a) (PathClass.id v) = Quot.mk Reduction a
Tactic:
aesop
Proof state after:
no goals
Theorem: Graph.PathClass.inv_mul
Proof state before:
V : Type u
E : Type v
G : Graph V E
u✝ v✝ w : V
e : EdgeBetween G v✝ w
u v : V
⊢ ∀ (p : PathClass G u v), mul (inv p) p = PathClass.id v
Tactic:
apply Quot.ind
Proof state after:
case mk
V : Type u
E : Type v
G : Graph V E
u✝ v✝ w : V
e : EdgeBetween G v✝ w
u v : V
⊢ ∀ (a : EdgePath G u v), mul (inv (Quot.mk Reduction a)) (Quot.mk Reduction a) = PathClass.id v
Theorem: Graph.PathClass.inv_mul
Proof state before:
case mk
V : Type u
E : Type v
G : Graph V E
u✝ v✝ w : V
e : EdgeBetween G v✝ w
u v : V
⊢ ∀ (a : EdgePath G u v), mul (inv (Quot.mk Reduction a)) (Quot.mk Reduction a) = PathClass.id v
Tactic:
aesop
Proof state after:
no goals
Theorem: Graph.PathClass.mul_inv
Proof state before:
V : Type u
E : Type v
G : Graph V E
u✝ v✝ w : V
e : EdgeBetween G v✝ w
u v : V
⊢ ∀ (p : PathClass G u v), mul p (inv p) = PathClass.id u
Tactic:
apply Quot.ind
Proof state after:
case mk
V : Type u
E : Type v
G : Graph V E
u✝ v✝ w : V
e : EdgeBetween G v✝ w
u v : V
⊢ ∀ (a : EdgePath G u v), mul (Quot.mk Reduction a) (inv (Quot.mk Reduction a)) = PathClass.id u
Theorem: Graph.PathClass.mul_inv
Proof state before:
case mk
V : Type u
E : Type v
G : Graph V E
u✝ v✝ w : V
e : EdgeBetween G v✝ w
u v : V
⊢ ∀ (a : EdgePath G u v), mul (Quot.mk Reduction a) (inv (Quot.mk Reduction a)) = PathClass.id u
Tactic:
aesop
Proof state after:
no goals
Theorem: Graph.PathClass.mul_assoc
Proof state before:
V : Type u
E : Type v
G : Graph V E
u✝ v✝ w✝ : V
e : EdgeBetween G v✝ w✝
v w u u' : V
⊢ ∀ (p : PathClass G v w) (q : PathClass G w u) (r : PathClass G u u'), mul (mul p q) r = mul p (mul q r)
Tactic:
apply Quot.ind
Proof state after:
case mk
V : Type u
E : Type v
G : Graph V E
u✝ v✝ w✝ : V
e : EdgeBetween G v✝ w✝
v w u u' : V
⊢ ∀ (a : EdgePath G v w) (q : PathClass G w u) (r : PathClass G u u'),
    mul (mul (Quot.mk Reduction a) q) r = mul (Quot.mk Reduction a) (mul q r)
Theorem: Graph.PathClass.mul_assoc
Proof state before:
case mk
V : Type u
E : Type v
G : Graph V E
u✝ v✝ w✝ : V
e : EdgeBetween G v✝ w✝
v w u u' : V
⊢ ∀ (a : EdgePath G v w) (q : PathClass G w u) (r : PathClass G u u'),
    mul (mul (Quot.mk Reduction a) q) r = mul (Quot.mk Reduction a) (mul q r)
Tactic:
intro a
Proof state after:
case mk
V : Type u
E : Type v
G : Graph V E
u✝ v✝ w✝ : V
e : EdgeBetween G v✝ w✝
v w u u' : V
a : EdgePath G v w
⊢ ∀ (q : PathClass G w u) (r : PathClass G u u'),
    mul (mul (Quot.mk Reduction a) q) r = mul (Quot.mk Reduction a) (mul q r)
Theorem: Graph.PathClass.mul_assoc
Proof state before:
case mk
V : Type u
E : Type v
G : Graph V E
u✝ v✝ w✝ : V
e : EdgeBetween G v✝ w✝
v w u u' : V
a : EdgePath G v w
⊢ ∀ (q : PathClass G w u) (r : PathClass G u u'),
    mul (mul (Quot.mk Reduction a) q) r = mul (Quot.mk Reduction a) (mul q r)
Tactic:
apply Quot.ind
Proof state after:
case mk.mk
V : Type u
E : Type v
G : Graph V E
u✝ v✝ w✝ : V
e : EdgeBetween G v✝ w✝
v w u u' : V
a : EdgePath G v w
⊢ ∀ (a_1 : EdgePath G w u) (r : PathClass G u u'),
    mul (mul (Quot.mk Reduction a) (Quot.mk Reduction a_1)) r =
      mul (Quot.mk Reduction a) (mul (Quot.mk Reduction a_1) r)
Theorem: Graph.PathClass.mul_assoc
Proof state before:
case mk.mk
V : Type u
E : Type v
G : Graph V E
u✝ v✝ w✝ : V
e : EdgeBetween G v✝ w✝
v w u u' : V
a : EdgePath G v w
⊢ ∀ (a_1 : EdgePath G w u) (r : PathClass G u u'),
    mul (mul (Quot.mk Reduction a) (Quot.mk Reduction a_1)) r =
      mul (Quot.mk Reduction a) (mul (Quot.mk Reduction a_1) r)
Tactic:
intro b
Proof state after:
case mk.mk
V : Type u
E : Type v
G : Graph V E
u✝ v✝ w✝ : V
e : EdgeBetween G v✝ w✝
v w u u' : V
a : EdgePath G v w
b : EdgePath G w u
⊢ ∀ (r : PathClass G u u'),
    mul (mul (Quot.mk Reduction a) (Quot.mk Reduction b)) r = mul (Quot.mk Reduction a) (mul (Quot.mk Reduction b) r)
Theorem: Graph.PathClass.mul_assoc
Proof state before:
case mk.mk
V : Type u
E : Type v
G : Graph V E
u✝ v✝ w✝ : V
e : EdgeBetween G v✝ w✝
v w u u' : V
a : EdgePath G v w
b : EdgePath G w u
⊢ ∀ (r : PathClass G u u'),
    mul (mul (Quot.mk Reduction a) (Quot.mk Reduction b)) r = mul (Quot.mk Reduction a) (mul (Quot.mk Reduction b) r)
Tactic:
apply Quot.ind
Proof state after:
case mk.mk.mk
V : Type u
E : Type v
G : Graph V E
u✝ v✝ w✝ : V
e : EdgeBetween G v✝ w✝
v w u u' : V
a : EdgePath G v w
b : EdgePath G w u
⊢ ∀ (a_1 : EdgePath G u u'),
    mul (mul (Quot.mk Reduction a) (Quot.mk Reduction b)) (Quot.mk Reduction a_1) =
      mul (Quot.mk Reduction a) (mul (Quot.mk Reduction b) (Quot.mk Reduction a_1))
Theorem: Graph.PathClass.mul_assoc
Proof state before:
case mk.mk.mk
V : Type u
E : Type v
G : Graph V E
u✝ v✝ w✝ : V
e : EdgeBetween G v✝ w✝
v w u u' : V
a : EdgePath G v w
b : EdgePath G w u
⊢ ∀ (a_1 : EdgePath G u u'),
    mul (mul (Quot.mk Reduction a) (Quot.mk Reduction b)) (Quot.mk Reduction a_1) =
      mul (Quot.mk Reduction a) (mul (Quot.mk Reduction b) (Quot.mk Reduction a_1))
Tactic:
intro c
Proof state after:
case mk.mk.mk
V : Type u
E : Type v
G : Graph V E
u✝ v✝ w✝ : V
e : EdgeBetween G v✝ w✝
v w u u' : V
a : EdgePath G v w
b : EdgePath G w u
c : EdgePath G u u'
⊢ mul (mul (Quot.mk Reduction a) (Quot.mk Reduction b)) (Quot.mk Reduction c) =
    mul (Quot.mk Reduction a) (mul (Quot.mk Reduction b) (Quot.mk Reduction c))
Theorem: Graph.PathClass.mul_assoc
Proof state before:
case mk.mk.mk
V : Type u
E : Type v
G : Graph V E
u✝ v✝ w✝ : V
e : EdgeBetween G v✝ w✝
v w u u' : V
a : EdgePath G v w
b : EdgePath G w u
c : EdgePath G u u'
⊢ mul (mul (Quot.mk Reduction a) (Quot.mk Reduction b)) (Quot.mk Reduction c) =
    mul (Quot.mk Reduction a) (mul (Quot.mk Reduction b) (Quot.mk Reduction c))
Tactic:
simp [append_assoc]
Proof state after:
no goals
Theorem: Graph.PathClass.append_mul
Proof state before:
V : Type u
E : Type v
G : Graph V E
u✝ v✝ w✝ : V
e : EdgeBetween G v✝ w✝
v w u : V
p : EdgePath G v w
q : EdgePath G w u
⊢ [[p ++ q]] = mul [[p]] [[q]]
Tactic:
rfl
Proof state after:
no goals
Theorem: Graph.PathClass.cons_equiv_of_equiv
Proof state before:
V : Type u
E : Type v
G✝ : Graph V E
u✝ v✝ w✝ : V
e : EdgeBetween G✝ v✝ w✝
G : Graph V E
v w u : V
a : EdgeBetween G v w
b₁ b₂ : EdgePath G w u
⊢ [[b₁]] = [[b₂]] → [[cons a b₁]] = [[cons a b₂]]
Tactic:
intro rel
Proof state after:
V : Type u
E : Type v
G✝ : Graph V E
u✝ v✝ w✝ : V
e : EdgeBetween G✝ v✝ w✝
G : Graph V E
v w u : V
a : EdgeBetween G v w
b₁ b₂ : EdgePath G w u
rel : [[b₁]] = [[b₂]]
⊢ [[cons a b₁]] = [[cons a b₂]]
Theorem: Graph.PathClass.cons_equiv_of_equiv
Proof state before:
V : Type u
E : Type v
G✝ : Graph V E
u✝ v✝ w✝ : V
e : EdgeBetween G✝ v✝ w✝
G : Graph V E
v w u : V
a : EdgeBetween G v w
b₁ b₂ : EdgePath G w u
rel : [[b₁]] = [[b₂]]
⊢ [[cons a b₁]] = [[cons a b₂]]
Tactic:
rw [show cons a b₁ = cons a (nil _) ++ b₁ by rfl, 
    show cons a b₂ = cons a (nil _) ++ b₂ by rfl,
    append_mul, append_mul, rel]
Proof state after:
no goals
Theorem: Graph.PathClass.cons_equiv_of_equiv
Proof state before:
V : Type u
E : Type v
G✝ : Graph V E
u✝ v✝ w✝ : V
e : EdgeBetween G✝ v✝ w✝
G : Graph V E
v w u : V
a : EdgeBetween G v w
b₁ b₂ : EdgePath G w u
rel : [[b₁]] = [[b₂]]
⊢ cons a b₁ = cons a (nil w) ++ b₁
Tactic:
rfl
Proof state after:
no goals
Theorem: Graph.PathClass.cons_equiv_of_equiv
Proof state before:
V : Type u
E : Type v
G✝ : Graph V E
u✝ v✝ w✝ : V
e : EdgeBetween G✝ v✝ w✝
G : Graph V E
v w u : V
a : EdgeBetween G v w
b₁ b₂ : EdgePath G w u
rel : [[b₁]] = [[b₂]]
⊢ cons a b₂ = cons a (nil w) ++ b₂
Tactic:
rfl
Proof state after:
no goals