internlm/Lean-Github huggingface dataset:
Theorem: Graph.right_append_step
Proof state before:
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
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
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
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
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
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
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
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
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
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
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
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
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
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
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
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.inv_equiv_reverse
Proof state before:
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
u v✝ w✝ : V
e : EdgeBetween G v✝ w✝
V₁ : Type u_1
E✝ : Type u_2
G₁ : Graph V₁ E✝
v w : V₁
η : EdgePath G₁ v w
⊢ PathClass.inv [[η]] = [[reverse η]]
Tactic:
rfl
Proof state after:
no goals
Theorem: Graph.cons_equiv_of_equiv
Proof state before:
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
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 r
Proof state after:
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
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
r : [[b₁]] = [[b₂]]
⊢ [[cons a b₁]] = [[cons a b₂]]
Theorem: Graph.cons_equiv_of_equiv
Proof state before:
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
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
r : [[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,
    ← mul_path_path, ← mul_path_path, r]
Proof state after:
no goals
Theorem: Graph.cons_equiv_of_equiv
Proof state before:
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
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
r : [[b₁]] = [[b₂]]
⊢ cons a b₁ = cons a (nil w) ++ b₁
Tactic:
rfl
Proof state after:
no goals
Theorem: Graph.cons_equiv_of_equiv
Proof state before:
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
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
r : [[b₁]] = [[b₂]]
⊢ cons a b₂ = cons a (nil w) ++ b₂
Tactic:
rfl
Proof state after:
no goals
Theorem: Graph.concat_equiv_of_equiv
Proof state before:
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G✝ : Graph V E
u✝ v✝ w✝ : V
e : EdgeBetween G✝ v✝ w✝
G : Graph V E
v w u : V
a₁ a₂ : EdgePath G v w
b : EdgeBetween G w u
⊢ [[a₁]] = [[a₂]] → [[concat a₁ b]] = [[concat a₂ b]]
Tactic:
intro r
Proof state after:
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G✝ : Graph V E
u✝ v✝ w✝ : V
e : EdgeBetween G✝ v✝ w✝
G : Graph V E
v w u : V
a₁ a₂ : EdgePath G v w
b : EdgeBetween G w u
r : [[a₁]] = [[a₂]]
⊢ [[concat a₁ b]] = [[concat a₂ b]]
Theorem: Graph.concat_equiv_of_equiv
Proof state before:
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G✝ : Graph V E
u✝ v✝ w✝ : V
e : EdgeBetween G✝ v✝ w✝
G : Graph V E
v w u : V
a₁ a₂ : EdgePath G v w
b : EdgeBetween G w u
r : [[a₁]] = [[a₂]]
⊢ [[concat a₁ b]] = [[concat a₂ b]]
Tactic:
have: concat a₁  b = a₁ ++ (concat (nil _) b) := by 
  rw [append_concat, append_nil]
Proof state after:
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G✝ : Graph V E
u✝ v✝ w✝ : V
e : EdgeBetween G✝ v✝ w✝
G : Graph V E
v w u : V
a₁ a₂ : EdgePath G v w
b : EdgeBetween G w u
r : [[a₁]] = [[a₂]]
this : concat a₁ b = a₁ ++ concat (nil w) b
⊢ [[concat a₁ b]] = [[concat a₂ b]]
Theorem: Graph.concat_equiv_of_equiv
Proof state before:
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G✝ : Graph V E
u✝ v✝ w✝ : V
e : EdgeBetween G✝ v✝ w✝
G : Graph V E
v w u : V
a₁ a₂ : EdgePath G v w
b : EdgeBetween G w u
r : [[a₁]] = [[a₂]]
this : concat a₁ b = a₁ ++ concat (nil w) b
⊢ [[concat a₁ b]] = [[concat a₂ b]]
Tactic:
rw [this]
Proof state after:
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G✝ : Graph V E
u✝ v✝ w✝ : V
e : EdgeBetween G✝ v✝ w✝
G : Graph V E
v w u : V
a₁ a₂ : EdgePath G v w
b : EdgeBetween G w u
r : [[a₁]] = [[a₂]]
this : concat a₁ b = a₁ ++ concat (nil w) b
⊢ [[a₁ ++ concat (nil w) b]] = [[concat a₂ b]]
Theorem: Graph.concat_equiv_of_equiv
Proof state before:
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G✝ : Graph V E
u✝ v✝ w✝ : V
e : EdgeBetween G✝ v✝ w✝
G : Graph V E
v w u : V
a₁ a₂ : EdgePath G v w
b : EdgeBetween G w u
r : [[a₁]] = [[a₂]]
this : concat a₁ b = a₁ ++ concat (nil w) b
⊢ [[a₁ ++ concat (nil w) b]] = [[concat a₂ b]]
Tactic:
have: concat a₂  b = a₂ ++ (concat (nil _) b) := by 
  rw [append_concat, append_nil]
Proof state after:
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G✝ : Graph V E
u✝ v✝ w✝ : V
e : EdgeBetween G✝ v✝ w✝
G : Graph V E
v w u : V
a₁ a₂ : EdgePath G v w
b : EdgeBetween G w u
r : [[a₁]] = [[a₂]]
this✝ : concat a₁ b = a₁ ++ concat (nil w) b
this : concat a₂ b = a₂ ++ concat (nil w) b
⊢ [[a₁ ++ concat (nil w) b]] = [[concat a₂ b]]
Theorem: Graph.concat_equiv_of_equiv
Proof state before:
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G✝ : Graph V E
u✝ v✝ w✝ : V
e : EdgeBetween G✝ v✝ w✝
G : Graph V E
v w u : V
a₁ a₂ : EdgePath G v w
b : EdgeBetween G w u
r : [[a₁]] = [[a₂]]
this✝ : concat a₁ b = a₁ ++ concat (nil w) b
this : concat a₂ b = a₂ ++ concat (nil w) b
⊢ [[a₁ ++ concat (nil w) b]] = [[concat a₂ b]]
Tactic:
rw [this, ← mul_path_path, ← mul_path_path, r]
Proof state after:
no goals
Theorem: Graph.concat_equiv_of_equiv
Proof state before:
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G✝ : Graph V E
u✝ v✝ w✝ : V
e : EdgeBetween G✝ v✝ w✝
G : Graph V E
v w u : V
a₁ a₂ : EdgePath G v w
b : EdgeBetween G w u
r : [[a₁]] = [[a₂]]
⊢ concat a₁ b = a₁ ++ concat (nil w) b
Tactic:
rw [append_concat, append_nil]
Proof state after:
no goals
Theorem: Graph.concat_equiv_of_equiv
Proof state before:
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G✝ : Graph V E
u✝ v✝ w✝ : V
e : EdgeBetween G✝ v✝ w✝
G : Graph V E
v w u : V
a₁ a₂ : EdgePath G v w
b : EdgeBetween G w u
r : [[a₁]] = [[a₂]]
this : concat a₁ b = a₁ ++ concat (nil w) b
⊢ concat a₂ b = a₂ ++ concat (nil w) b
Tactic:
rw [append_concat, append_nil]
Proof state after:
no goals
Theorem: Graph.PathClass.mul_assoc
Proof state before:
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
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'), p * q * r = p * (q * r)
Tactic:
apply Quot.ind
Proof state after:
case mk
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
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'),
    Quot.mk Reduction a * q * r = Quot.mk Reduction a * (q * r)
Theorem: Graph.PathClass.mul_assoc
Proof state before:
case mk
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
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'),
    Quot.mk Reduction a * q * r = Quot.mk Reduction a * (q * r)
Tactic:
intro a
Proof state after:
case mk
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
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'), Quot.mk Reduction a * q * r = Quot.mk Reduction a * (q * r)
Theorem: Graph.PathClass.mul_assoc
Proof state before:
case mk
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
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'), Quot.mk Reduction a * q * r = Quot.mk Reduction a * (q * r)
Tactic:
apply Quot.ind
Proof state after:
case mk.mk
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
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'),
    Quot.mk Reduction a * Quot.mk Reduction a_1 * r = Quot.mk Reduction a * (Quot.mk Reduction a_1 * r)
Theorem: Graph.PathClass.mul_assoc
Proof state before:
case mk.mk
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
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'),
    Quot.mk Reduction a * Quot.mk Reduction a_1 * r = Quot.mk Reduction a * (Quot.mk Reduction a_1 * r)
Tactic:
intro b
Proof state after:
case mk.mk
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
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'),
    Quot.mk Reduction a * Quot.mk Reduction b * r = Quot.mk Reduction a * (Quot.mk Reduction b * r)
Theorem: Graph.PathClass.mul_assoc
Proof state before:
case mk.mk
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
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'),
    Quot.mk Reduction a * Quot.mk Reduction b * r = Quot.mk Reduction a * (Quot.mk Reduction b * r)
Tactic:
apply Quot.ind
Proof state after:
case mk.mk.mk
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
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'),
    Quot.mk Reduction a * Quot.mk Reduction b * Quot.mk Reduction a_1 =
      Quot.mk Reduction a * (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
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
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'),
    Quot.mk Reduction a * Quot.mk Reduction b * Quot.mk Reduction a_1 =
      Quot.mk Reduction a * (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
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
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'
⊢ Quot.mk Reduction a * Quot.mk Reduction b * Quot.mk Reduction c =
    Quot.mk Reduction a * (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
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
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'
⊢ Quot.mk Reduction a * Quot.mk Reduction b * Quot.mk Reduction c =
    Quot.mk Reduction a * (Quot.mk Reduction b * Quot.mk Reduction c)
Tactic:
simp [append_assoc]
Proof state after:
no goals
Theorem: Graph.PathClass.id_mul
Proof state before:
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
u✝ v✝ w : V
e : EdgeBetween G v✝ w
u v : V
⊢ ∀ (p : PathClass G u v), PathClass.id' G u * p = p
Tactic:
apply PathClass.ind
Proof state after:
case a
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
u✝ v✝ w : V
e : EdgeBetween G v✝ w
u v : V
⊢ ∀ (p : EdgePath G u v), PathClass.id' G u * [[p]] = [[p]]
Theorem: Graph.PathClass.id_mul
Proof state before:
case a
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
u✝ v✝ w : V
e : EdgeBetween G v✝ w
u v : V
⊢ ∀ (p : EdgePath G u v), PathClass.id' G u * [[p]] = [[p]]
Tactic:
aesop
Proof state after:
no goals
Theorem: Graph.PathClass.mul_id
Proof state before:
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
u✝ v✝ w : V
e : EdgeBetween G v✝ w
u v : V
⊢ ∀ (p : PathClass G u v), p * PathClass.id' G v = p
Tactic:
apply PathClass.ind
Proof state after:
case a
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
u✝ v✝ w : V
e : EdgeBetween G v✝ w
u v : V
⊢ ∀ (p : EdgePath G u v), [[p]] * PathClass.id' G v = [[p]]
Theorem: Graph.PathClass.mul_id
Proof state before:
case a
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
u✝ v✝ w : V
e : EdgeBetween G v✝ w
u v : V
⊢ ∀ (p : EdgePath G u v), [[p]] * PathClass.id' G v = [[p]]
Tactic:
aesop
Proof state after:
no goals
Theorem: Graph.PathClass.inv_mul
Proof state before:
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
u✝ v✝ w : V
e : EdgeBetween G v✝ w
u v : V
⊢ ∀ (p : PathClass G u v), PathClass.inv p * p = PathClass.id' G v
Tactic:
apply PathClass.ind
Proof state after:
case a
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
u✝ v✝ w : V
e : EdgeBetween G v✝ w
u v : V
⊢ ∀ (p : EdgePath G u v), PathClass.inv [[p]] * [[p]] = PathClass.id' G v
Theorem: Graph.PathClass.inv_mul
Proof state before:
case a
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
u✝ v✝ w : V
e : EdgeBetween G v✝ w
u v : V
⊢ ∀ (p : EdgePath G u v), PathClass.inv [[p]] * [[p]] = PathClass.id' G v
Tactic:
aesop
Proof state after:
no goals
Theorem: Graph.PathClass.mul_inv
Proof state before:
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
u✝ v✝ w : V
e : EdgeBetween G v✝ w
u v : V
⊢ ∀ (p : PathClass G u v), p * PathClass.inv p = PathClass.id' G u
Tactic:
apply PathClass.ind
Proof state after:
case a
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
u✝ v✝ w : V
e : EdgeBetween G v✝ w
u v : V
⊢ ∀ (p : EdgePath G u v), [[p]] * PathClass.inv [[p]] = PathClass.id' G u
Theorem: Graph.PathClass.mul_inv
Proof state before:
case a
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
u✝ v✝ w : V
e : EdgeBetween G v✝ w
u v : V
⊢ ∀ (p : EdgePath G u v), [[p]] * PathClass.inv [[p]] = PathClass.id' G u
Tactic:
aesop
Proof state after:
no goals
Theorem: Graph.PathClass.inv_eq
Proof state before:
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
u v w : V
e : EdgeBetween G v w
⊢ ∀ {p : PathClass G u v} {q : PathClass G v u}, PathClass.inv p = q → p = PathClass.inv q
Tactic:
apply PathClass.ind
Proof state after:
case a
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
u v w : V
e : EdgeBetween G v w
⊢ ∀ (p : EdgePath G u v) {q : PathClass G v u}, PathClass.inv [[p]] = q → [[p]] = PathClass.inv q
Theorem: Graph.PathClass.inv_eq
Proof state before:
case a
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
u v w : V
e : EdgeBetween G v w
⊢ ∀ (p : EdgePath G u v) {q : PathClass G v u}, PathClass.inv [[p]] = q → [[p]] = PathClass.inv q
Tactic:
aesop
Proof state after:
no goals
Theorem: Graph.PathClass.id_mul'
Proof state before:
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
u✝ v✝ w : V
e : EdgeBetween G v✝ w
u v : V
⊢ ∀ (p : u ⟶ v), 𝟙 u ≫ p = p
Tactic:
apply Quot.ind
Proof state after:
case mk
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
u✝ v✝ w : V
e : EdgeBetween G v✝ w
u v : V
⊢ ∀ (a : EdgePath G u v), 𝟙 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
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
u✝ v✝ w : V
e : EdgeBetween G v✝ w
u v : V
⊢ ∀ (a : EdgePath G u v), 𝟙 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
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
u✝ v✝ w : V
e : EdgeBetween G v✝ w
u v : V
⊢ ∀ (p : u ⟶ v), p ≫ 𝟙 v = p
Tactic:
apply Quot.ind
Proof state after:
case mk
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
u✝ v✝ w : V
e : EdgeBetween G v✝ w
u v : V
⊢ ∀ (a : EdgePath G u v), Quot.mk Reduction a ≫ 𝟙 v = Quot.mk Reduction a
Theorem: Graph.PathClass.mul_id'
Proof state before:
case mk
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
u✝ v✝ w : V
e : EdgeBetween G v✝ w
u v : V
⊢ ∀ (a : EdgePath G u v), Quot.mk Reduction a ≫ 𝟙 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
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
u✝ v✝ w : V
e : EdgeBetween G v✝ w
u v : V
⊢ ∀ (p : u ⟶ v), PathClass.inv p ≫ p = 𝟙 v
Tactic:
apply Quot.ind
Proof state after:
case mk
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
u✝ v✝ w : V
e : EdgeBetween G v✝ w
u v : V
⊢ ∀ (a : EdgePath G u v), PathClass.inv (Quot.mk Reduction a) ≫ Quot.mk Reduction a = 𝟙 v
Theorem: Graph.PathClass.inv_mul'
Proof state before:
case mk
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
u✝ v✝ w : V
e : EdgeBetween G v✝ w
u v : V
⊢ ∀ (a : EdgePath G u v), PathClass.inv (Quot.mk Reduction a) ≫ Quot.mk Reduction a = 𝟙 v
Tactic:
aesop
Proof state after:
no goals
Theorem: Graph.PathClass.mul_inv'
Proof state before:
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
u✝ v✝ w : V
e : EdgeBetween G v✝ w
u v : V
⊢ ∀ (p : u ⟶ v), p ≫ PathClass.inv p = 𝟙 u
Tactic:
apply Quot.ind
Proof state after:
case mk
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
u✝ v✝ w : V
e : EdgeBetween G v✝ w
u v : V
⊢ ∀ (a : EdgePath G u v), Quot.mk Reduction a ≫ PathClass.inv (Quot.mk Reduction a) = 𝟙 u
Theorem: Graph.PathClass.mul_inv'
Proof state before:
case mk
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
u✝ v✝ w : V
e : EdgeBetween G v✝ w
u v : V
⊢ ∀ (a : EdgePath G u v), Quot.mk Reduction a ≫ PathClass.inv (Quot.mk Reduction a) = 𝟙 u
Tactic:
aesop
Proof state after:
no goals
Theorem: Graph.PathClass.mul_assoc'
Proof state before:
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
u✝ v✝ w✝ : V
e : EdgeBetween G v✝ w✝
v w u u' : V
⊢ ∀ (p : v ⟶ w) (q : w ⟶ u) (r : u ⟶ u'), (p ≫ q) ≫ r = p ≫ q ≫ r
Tactic:
apply Quot.ind
Proof state after:
case mk
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
u✝ v✝ w✝ : V
e : EdgeBetween G v✝ w✝
v w u u' : V
⊢ ∀ (a : EdgePath G v w) (q : w ⟶ u) (r : u ⟶ u'), (Quot.mk Reduction a ≫ q) ≫ r = Quot.mk Reduction a ≫ q ≫ r
Theorem: Graph.PathClass.mul_assoc'
Proof state before:
case mk
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
u✝ v✝ w✝ : V
e : EdgeBetween G v✝ w✝
v w u u' : V
⊢ ∀ (a : EdgePath G v w) (q : w ⟶ u) (r : u ⟶ u'), (Quot.mk Reduction a ≫ q) ≫ r = Quot.mk Reduction a ≫ q ≫ r
Tactic:
intro a
Proof state after:
case mk
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
u✝ v✝ w✝ : V
e : EdgeBetween G v✝ w✝
v w u u' : V
a : EdgePath G v w
⊢ ∀ (q : w ⟶ u) (r : u ⟶ u'), (Quot.mk Reduction a ≫ q) ≫ r = Quot.mk Reduction a ≫ q ≫ r
Theorem: Graph.PathClass.mul_assoc'
Proof state before:
case mk
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
u✝ v✝ w✝ : V
e : EdgeBetween G v✝ w✝
v w u u' : V
a : EdgePath G v w
⊢ ∀ (q : w ⟶ u) (r : u ⟶ u'), (Quot.mk Reduction a ≫ q) ≫ r = Quot.mk Reduction a ≫ q ≫ r
Tactic:
apply Quot.ind
Proof state after:
case mk.mk
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
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 : u ⟶ u'),
    (Quot.mk Reduction a ≫ Quot.mk Reduction a_1) ≫ r = Quot.mk Reduction a ≫ Quot.mk Reduction a_1 ≫ r
Theorem: Graph.PathClass.mul_assoc'
Proof state before:
case mk.mk
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
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 : u ⟶ u'),
    (Quot.mk Reduction a ≫ Quot.mk Reduction a_1) ≫ r = Quot.mk Reduction a ≫ Quot.mk Reduction a_1 ≫ r
Tactic:
intro b
Proof state after:
case mk.mk
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
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 : u ⟶ u'), (Quot.mk Reduction a ≫ Quot.mk Reduction b) ≫ r = Quot.mk Reduction a ≫ Quot.mk Reduction b ≫ r
Theorem: Graph.PathClass.mul_assoc'
Proof state before:
case mk.mk
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
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 : u ⟶ u'), (Quot.mk Reduction a ≫ Quot.mk Reduction b) ≫ r = Quot.mk Reduction a ≫ Quot.mk Reduction b ≫ r
Tactic:
apply Quot.ind
Proof state after:
case mk.mk.mk
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
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'),
    (Quot.mk Reduction a ≫ Quot.mk Reduction b) ≫ Quot.mk Reduction a_1 =
      Quot.mk Reduction a ≫ 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
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
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'),
    (Quot.mk Reduction a ≫ Quot.mk Reduction b) ≫ Quot.mk Reduction a_1 =
      Quot.mk Reduction a ≫ 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
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
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'
⊢ (Quot.mk Reduction a ≫ Quot.mk Reduction b) ≫ Quot.mk Reduction c =
    Quot.mk Reduction a ≫ Quot.mk Reduction b ≫ Quot.mk Reduction c