internlm/Lean-Github huggingface dataset:
Theorem: Path.last_eq_inv_first
Proof state before:
V : Sort u_1
G : SerreGraph V
A B C : V
p✝ p : Path A B
p' : Path B A := inverse p
⊢ last p = first (inverse p)
Tactic:
have pinv : p = p'.inverse := by simp
Proof state after:
V : Sort u_1
G : SerreGraph V
A B C : V
p✝ p : Path A B
p' : Path B A := inverse p
pinv : p = inverse p'
⊢ last p = first (inverse p)
Theorem: Path.last_eq_inv_first
Proof state before:
V : Sort u_1
G : SerreGraph V
A B C : V
p✝ p : Path A B
p' : Path B A := inverse p
pinv : p = inverse p'
⊢ last p = first (inverse p)
Tactic:
rw [pinv, inverse_inv p']
Proof state after:
V : Sort u_1
G : SerreGraph V
A B C : V
p✝ p : Path A B
p' : Path B A := inverse p
pinv : p = inverse p'
⊢ last (inverse p') = first p'
Theorem: Path.last_eq_inv_first
Proof state before:
V : Sort u_1
G : SerreGraph V
A B C : V
p✝ p : Path A B
p' : Path B A := inverse p
pinv : p = inverse p'
⊢ last (inverse p') = first p'
Tactic:
apply Eq.symm
Proof state after:
case h
V : Sort u_1
G : SerreGraph V
A B C : V
p✝ p : Path A B
p' : Path B A := inverse p
pinv : p = inverse p'
⊢ first p' = last (inverse p')
Theorem: Path.last_eq_inv_first
Proof state before:
case h
V : Sort u_1
G : SerreGraph V
A B C : V
p✝ p : Path A B
p' : Path B A := inverse p
pinv : p = inverse p'
⊢ first p' = last (inverse p')
Tactic:
apply first_eq_inv_last
Proof state after:
no goals
Theorem: Path.last_eq_inv_first
Proof state before:
V : Sort u_1
G : SerreGraph V
A B C : V
p✝ p : Path A B
p' : Path B A := inverse p
⊢ p = inverse p'
Tactic:
simp
Proof state after:
no goals
Theorem: Loop.inv_inv
Proof state before:
V : Sort u_1
inst✝ : SerreGraph V
A : V
l : Loop A
⊢ inv (inv l) = l
Tactic:
simp
Proof state after:
no goals
Theorem: Loop.inv_rotate_inv
Proof state before:
V : Sort u_1
inst✝ : SerreGraph V
A : V
l : Loop A
⊢ inv (rotate A (inv l)) = rotate' A l
Tactic:
simp [rotate']
Proof state after:
no goals
Theorem: Loop.prev_inv
Proof state before:
V : Sort u_1
inst✝ : SerreGraph V
A : V
l : Loop A
⊢ prev A (inv l) = next A l
Tactic:
simp [prev]
Proof state after:
no goals
Theorem: Loop.next_inv
Proof state before:
V : Sort u_1
inst✝ : SerreGraph V
A : V
l : Loop A
⊢ next A (inv l) = prev A l
Tactic:
simp
Proof state after:
no goals
Theorem: Loop.rotate_prev
Proof state before:
V : Sort u_1
inst✝ : SerreGraph V
A B✝ : V
e : A ⟶ B✝
p : Path B✝ A
⊢ prev (next A (Path.cons' A B✝ A e p)) (rotate A (Path.cons' A B✝ A e p)) = A
Tactic:
dsimp [prev, rotate, inv]
Proof state after:
V : Sort u_1
inst✝ : SerreGraph V
A B✝ : V
e : A ⟶ B✝
p : Path B✝ A
⊢ next (next A (Path.cons' A B✝ A e p)) (Path.inverse (Path.snoc p e)) = A
Theorem: Loop.rotate_prev
Proof state before:
V : Sort u_1
inst✝ : SerreGraph V
A B✝ : V
e : A ⟶ B✝
p : Path B✝ A
⊢ next (next A (Path.cons' A B✝ A e p)) (Path.inverse (Path.snoc p e)) = A
Tactic:
rw [Path.inverse_snoc]
Proof state after:
V : Sort u_1
inst✝ : SerreGraph V
A B✝ : V
e : A ⟶ B✝
p : Path B✝ A
⊢ next (next A (Path.cons' A B✝ A e p)) (Path.cons (SerreGraph.op e) (Path.inverse p)) = A
Theorem: Loop.rotate_prev
Proof state before:
V : Sort u_1
inst✝ : SerreGraph V
A B✝ : V
e : A ⟶ B✝
p : Path B✝ A
⊢ next (next A (Path.cons' A B✝ A e p)) (Path.cons (SerreGraph.op e) (Path.inverse p)) = A
Tactic:
rfl
Proof state after:
no goals
Theorem: Loop.rotate'_next
Proof state before:
V : Sort u_1
inst✝ : SerreGraph V
A : V
l : Loop A
⊢ next (prev A l) (rotate' A l) = A
Tactic:
show prev _ (rotate _ l.inv) = A
Proof state after:
V : Sort u_1
inst✝ : SerreGraph V
A : V
l : Loop A
⊢ prev (next A (inv l)) (rotate A (inv l)) = A
Theorem: Loop.rotate'_next
Proof state before:
V : Sort u_1
inst✝ : SerreGraph V
A : V
l : Loop A
⊢ prev (next A (inv l)) (rotate A (inv l)) = A
Tactic:
simp
Proof state after:
no goals
Theorem: Loop.rotate'_inv_heq
Proof state before:
V : Sort u_1
inst✝ : SerreGraph V
A : V
l : Loop A
⊢ HEq (rotate' A (inv l)) (inv (rotate A l))
Tactic:
rw [← inv_rotate_inv A l.inv]
Proof state after:
V : Sort u_1
inst✝ : SerreGraph V
A : V
l : Loop A
⊢ HEq (inv (rotate A (inv (inv l)))) (inv (rotate A l))
Theorem: Loop.rotate'_inv_heq
Proof state before:
V : Sort u_1
inst✝ : SerreGraph V
A : V
l : Loop A
⊢ HEq (inv (rotate A (inv (inv l)))) (inv (rotate A l))
Tactic:
congr 2 <;> rw [inv_inv]
Proof state after:
no goals
Theorem: Loop.rotate_inv_heq
Proof state before:
V : Sort u_1
inst✝ : SerreGraph V
A : V
l : Loop A
⊢ HEq (rotate A (inv l)) (inv (rotate' A l))
Tactic:
rw [rotate', inv_inv]
Proof state after:
V : Sort u_1
inst✝ : SerreGraph V
A : V
l : Loop A
⊢ HEq (rotate A (inv l)) (rotate A (inv l))
Theorem: Loop.rotate_inv_heq
Proof state before:
V : Sort u_1
inst✝ : SerreGraph V
A : V
l : Loop A
⊢ HEq (rotate A (inv l)) (rotate A (inv l))
Tactic:
exact .refl _
Proof state after:
no goals
Theorem: Path.Homotopy.symm
Proof state before:
V : Sort u_1
C : CombinatorialTwoComplex V
u v : V
p q r : Path u v
h : NullHomotopy (append p (inverse q))
⊢ Homotopy q p
Tactic:
let h' := h.inv
Proof state after:
V : Sort u_1
C : CombinatorialTwoComplex V
u v : V
p q r : Path u v
h : NullHomotopy (append p (inverse q))
h' : NullHomotopy (Loop.inv (append p (inverse q))) := NullHomotopy.inv h
⊢ Homotopy q p
Theorem: Path.Homotopy.symm
Proof state before:
V : Sort u_1
C : CombinatorialTwoComplex V
u v : V
p q r : Path u v
h : NullHomotopy (append p (inverse q))
h' : NullHomotopy (Loop.inv (append p (inverse q))) := NullHomotopy.inv h
⊢ Homotopy q p
Tactic:
rw [Loop.inv, Path.inverse_append, Path.inverse_inv] at h'
Proof state after:
V : Sort u_1
C : CombinatorialTwoComplex V
u v : V
p q r : Path u v
h : NullHomotopy (append p (inverse q))
h' : NullHomotopy (append q (inverse p))
⊢ Homotopy q p
Theorem: Path.Homotopy.symm
Proof state before:
V : Sort u_1
C : CombinatorialTwoComplex V
u v : V
p q r : Path u v
h : NullHomotopy (append p (inverse q))
h' : NullHomotopy (append q (inverse p))
⊢ Homotopy q p
Tactic:
exact .rel h'
Proof state after:
no goals
Theorem: Path.Homotopy.trans
Proof state before:
V : Sort u_1
C : CombinatorialTwoComplex V
u v : V
p q r : Path u v
h : NullHomotopy (append p (inverse q))
h' : NullHomotopy (append q (inverse r))
⊢ Homotopy p r
Tactic:
let H := NullHomotopy.concat h h'
Proof state after:
V : Sort u_1
C : CombinatorialTwoComplex V
u v : V
p q r : Path u v
h : NullHomotopy (append p (inverse q))
h' : NullHomotopy (append q (inverse r))
H : NullHomotopy (append (append p (inverse q)) (append q (inverse r))) := NullHomotopy.concat h h'
⊢ Homotopy p r
Theorem: Path.Homotopy.trans
Proof state before:
V : Sort u_1
C : CombinatorialTwoComplex V
u v : V
p q r : Path u v
h : NullHomotopy (append p (inverse q))
h' : NullHomotopy (append q (inverse r))
H : NullHomotopy (append (append p (inverse q)) (append q (inverse r))) := NullHomotopy.concat h h'
⊢ Homotopy p r
Tactic:
rw [Path.append_assoc p _ _, ← Path.append_assoc _ q _] at H
Proof state after:
V : Sort u_1
C : CombinatorialTwoComplex V
u v : V
p q r : Path u v
h : NullHomotopy (append p (inverse q))
h' : NullHomotopy (append q (inverse r))
H : NullHomotopy (append p (append (append (inverse q) q) (inverse r)))
⊢ Homotopy p r
Theorem: Path.Homotopy.trans
Proof state before:
V : Sort u_1
C : CombinatorialTwoComplex V
u v : V
p q r : Path u v
h : NullHomotopy (append p (inverse q))
h' : NullHomotopy (append q (inverse r))
H : NullHomotopy (append p (append (append (inverse q) q) (inverse r)))
⊢ Homotopy p r
Tactic:
let H' := NullHomotopy.contract (.swap $ .trivial _) H
Proof state after:
V : Sort u_1
C : CombinatorialTwoComplex V
u v : V
p q r : Path u v
h : NullHomotopy (append p (inverse q))
h' : NullHomotopy (append q (inverse r))
H : NullHomotopy (append p (append (append (inverse q) q) (inverse r)))
H' : NullHomotopy (append p (inverse r)) := NullHomotopy.contract (NullHomotopy.swap (NullHomotopy.trivial q)) H
⊢ Homotopy p r
Theorem: Path.Homotopy.trans
Proof state before:
V : Sort u_1
C : CombinatorialTwoComplex V
u v : V
p q r : Path u v
h : NullHomotopy (append p (inverse q))
h' : NullHomotopy (append q (inverse r))
H : NullHomotopy (append p (append (append (inverse q) q) (inverse r)))
H' : NullHomotopy (append p (inverse r)) := NullHomotopy.contract (NullHomotopy.swap (NullHomotopy.trivial q)) H
⊢ Homotopy p r
Tactic:
exact .rel H'
Proof state after:
no goals
Theorem: Path.Homotopy.inv_cancel_left
Proof state before:
V : Sort u_1
C : CombinatorialTwoComplex V
u v : V
p✝ q r p : Path u v
⊢ NullHomotopy (append (append (inverse p) p) (inverse nil))
Tactic:
simp [inverse]
Proof state after:
V : Sort u_1
C : CombinatorialTwoComplex V
u v : V
p✝ q r p : Path u v
⊢ NullHomotopy (append (inverse p) p)
Theorem: Path.Homotopy.inv_cancel_left
Proof state before:
V : Sort u_1
C : CombinatorialTwoComplex V
u v : V
p✝ q r p : Path u v
⊢ NullHomotopy (append (inverse p) p)
Tactic:
apply NullHomotopy.swap
Proof state after:
case a
V : Sort u_1
C : CombinatorialTwoComplex V
u v : V
p✝ q r p : Path u v
⊢ NullHomotopy (append p (inverse p))
Theorem: Path.Homotopy.inv_cancel_left
Proof state before:
case a
V : Sort u_1
C : CombinatorialTwoComplex V
u v : V
p✝ q r p : Path u v
⊢ NullHomotopy (append p (inverse p))
Tactic:
apply NullHomotopy.trivial
Proof state after:
no goals
Theorem: Path.Homotopy.inv_cancel_right
Proof state before:
V : Sort u_1
C : CombinatorialTwoComplex V
u v : V
p✝ q r p : Path u v
⊢ NullHomotopy (append (append p (inverse p)) (inverse nil))
Tactic:
simp [inverse]
Proof state after:
V : Sort u_1
C : CombinatorialTwoComplex V
u v : V
p✝ q r p : Path u v
⊢ NullHomotopy (append p (inverse p))
Theorem: Path.Homotopy.inv_cancel_right
Proof state before:
V : Sort u_1
C : CombinatorialTwoComplex V
u v : V
p✝ q r p : Path u v
⊢ NullHomotopy (append p (inverse p))
Tactic:
apply NullHomotopy.trivial
Proof state after:
no goals
Theorem: Path.Homotopy.mul_sound
Proof state before:
V : Sort u_1
C : CombinatorialTwoComplex V
u✝ v✝ : V
p✝ q✝ r✝ : Path u✝ v✝
u v w : V
p q : Path u v
r s : Path v w
a : NullHomotopy (append p (inverse q))
b : NullHomotopy (append r (inverse s))
⊢ NullHomotopy (append (append p r) (inverse (append q s)))
Tactic:
rw [inverse_append, append_assoc, ← append_assoc _ _ (inverse q)]
Proof state after:
V : Sort u_1
C : CombinatorialTwoComplex V
u✝ v✝ : V
p✝ q✝ r✝ : Path u✝ v✝
u v w : V
p q : Path u v
r s : Path v w
a : NullHomotopy (append p (inverse q))
b : NullHomotopy (append r (inverse s))
⊢ NullHomotopy (append p (append (append r (inverse s)) (inverse q)))
Theorem: Path.Homotopy.mul_sound
Proof state before:
V : Sort u_1
C : CombinatorialTwoComplex V
u✝ v✝ : V
p✝ q✝ r✝ : Path u✝ v✝
u v w : V
p q : Path u v
r s : Path v w
a : NullHomotopy (append p (inverse q))
b : NullHomotopy (append r (inverse s))
⊢ NullHomotopy (append p (append (append r (inverse s)) (inverse q)))
Tactic:
exact NullHomotopy.splice b a
Proof state after:
no goals
Theorem: Path.Homotopy.inv_sound
Proof state before:
V : Sort u_1
C : CombinatorialTwoComplex V
u✝ v✝ : V
p✝ q✝ r✝ : Path u✝ v✝
u v : V
p q : Path u v
r : NullHomotopy (append p (inverse q))
⊢ NullHomotopy (append (inverse p) (inverse (inverse q)))
Tactic:
rw [← inverse_append]
Proof state after:
V : Sort u_1
C : CombinatorialTwoComplex V
u✝ v✝ : V
p✝ q✝ r✝ : Path u✝ v✝
u v : V
p q : Path u v
r : NullHomotopy (append p (inverse q))
⊢ NullHomotopy (inverse (append (inverse q) p))
Theorem: Path.Homotopy.inv_sound
Proof state before:
V : Sort u_1
C : CombinatorialTwoComplex V
u✝ v✝ : V
p✝ q✝ r✝ : Path u✝ v✝
u v : V
p q : Path u v
r : NullHomotopy (append p (inverse q))
⊢ NullHomotopy (inverse (append (inverse q) p))
Tactic:
apply NullHomotopy.inv
Proof state after:
case a
V : Sort u_1
C : CombinatorialTwoComplex V
u✝ v✝ : V
p✝ q✝ r✝ : Path u✝ v✝
u v : V
p q : Path u v
r : NullHomotopy (append p (inverse q))
⊢ NullHomotopy (append (inverse q) p)
Theorem: Path.Homotopy.inv_sound
Proof state before:
case a
V : Sort u_1
C : CombinatorialTwoComplex V
u✝ v✝ : V
p✝ q✝ r✝ : Path u✝ v✝
u v : V
p q : Path u v
r : NullHomotopy (append p (inverse q))
⊢ NullHomotopy (append (inverse q) p)
Tactic:
apply NullHomotopy.swap
Proof state after:
case a.a
V : Sort u_1
C : CombinatorialTwoComplex V
u✝ v✝ : V
p✝ q✝ r✝ : Path u✝ v✝
u v : V
p q : Path u v
r : NullHomotopy (append p (inverse q))
⊢ NullHomotopy (append p (inverse q))
Theorem: Path.Homotopy.inv_sound
Proof state before:
case a.a
V : Sort u_1
C : CombinatorialTwoComplex V
u✝ v✝ : V
p✝ q✝ r✝ : Path u✝ v✝
u v : V
p q : Path u v
r : NullHomotopy (append p (inverse q))
⊢ NullHomotopy (append p (inverse q))
Tactic:
exact r
Proof state after:
no goals
Theorem: Path.append_nil
Proof state before:
V : Sort u_1
inst✝ : Quiver V
A B C D : V
p : Path A B
⊢ append p nil = p
Tactic:
induction p
Proof state after:
case nil
V : Sort u_1
inst✝ : Quiver V
A B C D A✝ : V
⊢ append nil nil = nil

case cons
V : Sort u_1
inst✝ : Quiver V
A B C D A✝ B✝ C✝ : V
a✝¹ : A✝ ⟶ B✝
a✝ : Path B✝ C✝
a_ih✝ : append a✝ nil = a✝
⊢ append (cons a✝¹ a✝) nil = cons a✝¹ a✝
Theorem: Path.append_nil
Proof state before:
V : Sort u_1
inst✝ : Quiver V
A B C D A✝ : V
⊢ append nil nil = nil
Tactic:
case nil => rfl
Proof state after:
no goals
Theorem: Path.append_nil
Proof state before:
V : Sort u_1
inst✝ : Quiver V
A B C D A✝ : V
⊢ append nil nil = nil
Tactic:
rfl
Proof state after:
no goals
Theorem: Path.append_nil
Proof state before:
V : Sort u_1
inst✝ : Quiver V
A B C D A✝ B✝ C✝ : V
a✝¹ : A✝ ⟶ B✝
a✝ : Path B✝ C✝
a_ih✝ : append a✝ nil = a✝
⊢ append (cons a✝¹ a✝) nil = cons a✝¹ a✝
Tactic:
case cons =>
  simp only [append]
  apply congrArg
  assumption
Proof state after:
no goals
Theorem: Path.append_nil
Proof state before:
V : Sort u_1
inst✝ : Quiver V
A B C D A✝ B✝ C✝ : V
a✝¹ : A✝ ⟶ B✝
a✝ : Path B✝ C✝
a_ih✝ : append a✝ nil = a✝
⊢ append (cons a✝¹ a✝) nil = cons a✝¹ a✝
Tactic:
simp only [append]
Proof state after:
V : Sort u_1
inst✝ : Quiver V
A B C D A✝ B✝ C✝ : V
a✝¹ : A✝ ⟶ B✝
a✝ : Path B✝ C✝
a_ih✝ : append a✝ nil = a✝
⊢ cons a✝¹ (append a✝ nil) = cons a✝¹ a✝
Theorem: Path.append_nil
Proof state before:
V : Sort u_1
inst✝ : Quiver V
A B C D A✝ B✝ C✝ : V
a✝¹ : A✝ ⟶ B✝
a✝ : Path B✝ C✝
a_ih✝ : append a✝ nil = a✝
⊢ cons a✝¹ (append a✝ nil) = cons a✝¹ a✝
Tactic:
apply congrArg
Proof state after:
case h
V : Sort u_1
inst✝ : Quiver V
A B C D A✝ B✝ C✝ : V
a✝¹ : A✝ ⟶ B✝
a✝ : Path B✝ C✝
a_ih✝ : append a✝ nil = a✝
⊢ append a✝ nil = a✝
Theorem: Path.append_nil
Proof state before:
case h
V : Sort u_1
inst✝ : Quiver V
A B C D A✝ B✝ C✝ : V
a✝¹ : A✝ ⟶ B✝
a✝ : Path B✝ C✝
a_ih✝ : append a✝ nil = a✝
⊢ append a✝ nil = a✝
Tactic:
assumption
Proof state after:
no goals
Theorem: Path.snoc_cons
Proof state before:
V : Sort u_1
inst✝ : Quiver V
A B C D : V
e : A ⟶ B
p : Path B C
e' : C ⟶ D
⊢ snoc (cons e p) e' = cons e (snoc p e')
Tactic:
cases p <;> simp
Proof state after:
no goals
Theorem: Path.append_snoc
Proof state before:
V : Sort u_1
inst✝ : Quiver V
A B C D : V
p : Path A B
p' : Path B C
e : C ⟶ D
⊢ append p (snoc p' e) = snoc (append p p') e
Tactic:
induction p
Proof state after:
case nil
V : Sort u_1
inst✝ : Quiver V
A B C D : V
e : C ⟶ D
A✝ : V
p' : Path A✝ C
⊢ append nil (snoc p' e) = snoc (append nil p') e

case cons
V : Sort u_1
inst✝ : Quiver V
A B C D : V
e : C ⟶ D
A✝ B✝ C✝ : V
a✝¹ : A✝ ⟶ B✝
a✝ : Path B✝ C✝
a_ih✝ : ∀ (p' : Path C✝ C), append a✝ (snoc p' e) = snoc (append a✝ p') e
p' : Path C✝ C
⊢ append (cons a✝¹ a✝) (snoc p' e) = snoc (append (cons a✝¹ a✝) p') e
Theorem: Path.append_snoc
Proof state before:
V : Sort u_1
inst✝ : Quiver V
A B C D : V
e : C ⟶ D
A✝ : V
p' : Path A✝ C
⊢ append nil (snoc p' e) = snoc (append nil p') e
Tactic:
case nil => rfl
Proof state after:
no goals
Theorem: Path.append_snoc
Proof state before:
V : Sort u_1
inst✝ : Quiver V
A B C D : V
e : C ⟶ D
A✝ : V
p' : Path A✝ C
⊢ append nil (snoc p' e) = snoc (append nil p') e
Tactic:
rfl
Proof state after:
no goals
Theorem: Path.append_snoc
Proof state before:
V : Sort u_1
inst✝ : Quiver V
A B C D : V
e : C ⟶ D
A✝ B✝ C✝ : V
a✝¹ : A✝ ⟶ B✝
a✝ : Path B✝ C✝
ih : ∀ (p' : Path C✝ C), append a✝ (snoc p' e) = snoc (append a✝ p') e
p' : Path C✝ C
⊢ append (cons a✝¹ a✝) (snoc p' e) = snoc (append (cons a✝¹ a✝) p') e
Tactic:
case cons ih => simp [append, ih p', snoc_cons]
Proof state after:
no goals
Theorem: Path.append_snoc
Proof state before:
V : Sort u_1
inst✝ : Quiver V
A B C D : V
e : C ⟶ D
A✝ B✝ C✝ : V
a✝¹ : A✝ ⟶ B✝
a✝ : Path B✝ C✝
ih : ∀ (p' : Path C✝ C), append a✝ (snoc p' e) = snoc (append a✝ p') e
p' : Path C✝ C
⊢ append (cons a✝¹ a✝) (snoc p' e) = snoc (append (cons a✝¹ a✝) p') e
Tactic:
simp [append, ih p', snoc_cons]
Proof state after:
no goals
Theorem: Path.append_cons
Proof state before:
V : Sort u_1
inst✝ : Quiver V
A B C D : V
p : Path A B
e : B ⟶ C
p' : Path C D
⊢ append p (cons e p') = append (snoc p e) p'
Tactic:
induction p
Proof state after:
case nil
V : Sort u_1
inst✝ : Quiver V
A B C D : V
p' : Path C D
A✝ : V
e : A✝ ⟶ C
⊢ append nil (cons e p') = append (snoc nil e) p'

case cons
V : Sort u_1
inst✝ : Quiver V
A B C D : V
p' : Path C D
A✝ B✝ C✝ : V
a✝¹ : A✝ ⟶ B✝
a✝ : Path B✝ C✝
a_ih✝ : ∀ (e : C✝ ⟶ C), append a✝ (cons e p') = append (snoc a✝ e) p'
e : C✝ ⟶ C
⊢ append (cons a✝¹ a✝) (cons e p') = append (snoc (cons a✝¹ a✝) e) p'
Theorem: Path.append_cons
Proof state before:
V : Sort u_1
inst✝ : Quiver V
A B C D : V
p' : Path C D
A✝ : V
e : A✝ ⟶ C
⊢ append nil (cons e p') = append (snoc nil e) p'
Tactic:
case nil => rfl
Proof state after:
no goals
Theorem: Path.append_cons
Proof state before:
V : Sort u_1
inst✝ : Quiver V
A B C D : V
p' : Path C D
A✝ : V
e : A✝ ⟶ C
⊢ append nil (cons e p') = append (snoc nil e) p'
Tactic:
rfl
Proof state after:
no goals
Theorem: Path.append_cons
Proof state before:
V : Sort u_1
inst✝ : Quiver V
A B C D : V
p' : Path C D
A✝ B✝ C✝ : V
a✝¹ : A✝ ⟶ B✝
a✝ : Path B✝ C✝
ih : ∀ (e : C✝ ⟶ C), append a✝ (cons e p') = append (snoc a✝ e) p'
e : C✝ ⟶ C
⊢ append (cons a✝¹ a✝) (cons e p') = append (snoc (cons a✝¹ a✝) e) p'
Tactic:
case cons ih => dsimp [append]; rw [ih]
Proof state after:
no goals
Theorem: Path.append_cons
Proof state before:
V : Sort u_1
inst✝ : Quiver V
A B C D : V
p' : Path C D
A✝ B✝ C✝ : V
a✝¹ : A✝ ⟶ B✝
a✝ : Path B✝ C✝
ih : ∀ (e : C✝ ⟶ C), append a✝ (cons e p') = append (snoc a✝ e) p'
e : C✝ ⟶ C
⊢ append (cons a✝¹ a✝) (cons e p') = append (snoc (cons a✝¹ a✝) e) p'
Tactic:
dsimp [append]
Proof state after:
V : Sort u_1
inst✝ : Quiver V
A B C D : V
p' : Path C D
A✝ B✝ C✝ : V
a✝¹ : A✝ ⟶ B✝
a✝ : Path B✝ C✝
ih : ∀ (e : C✝ ⟶ C), append a✝ (cons e p') = append (snoc a✝ e) p'
e : C✝ ⟶ C
⊢ cons a✝¹ (append a✝ (cons e p')) = cons a✝¹ (append (snoc a✝ e) p')
Theorem: Path.append_cons
Proof state before:
V : Sort u_1
inst✝ : Quiver V
A B C D : V
p' : Path C D
A✝ B✝ C✝ : V
a✝¹ : A✝ ⟶ B✝
a✝ : Path B✝ C✝
ih : ∀ (e : C✝ ⟶ C), append a✝ (cons e p') = append (snoc a✝ e) p'
e : C✝ ⟶ C
⊢ cons a✝¹ (append a✝ (cons e p')) = cons a✝¹ (append (snoc a✝ e) p')
Tactic:
rw [ih]
Proof state after:
no goals
Theorem: Path.append_assoc
Proof state before:
V : Sort u_1
inst✝ : Quiver V
A B C D : V
p : Path A B
q : Path B C
r : Path C D
⊢ append (append p q) r = append p (append q r)
Tactic:
induction p
Proof state after:
case nil
V : Sort u_1
inst✝ : Quiver V
A B C D : V
r : Path C D
A✝ : V
q : Path A✝ C
⊢ append (append nil q) r = append nil (append q r)

case cons
V : Sort u_1
inst✝ : Quiver V
A B C D : V
r : Path C D
A✝ B✝ C✝ : V
a✝¹ : A✝ ⟶ B✝
a✝ : Path B✝ C✝
a_ih✝ : ∀ (q : Path C✝ C), append (append a✝ q) r = append a✝ (append q r)
q : Path C✝ C
⊢ append (append (cons a✝¹ a✝) q) r = append (cons a✝¹ a✝) (append q r)
Theorem: Path.append_assoc
Proof state before:
V : Sort u_1
inst✝ : Quiver V
A B C D : V
r : Path C D
A✝ : V
q : Path A✝ C
⊢ append (append nil q) r = append nil (append q r)
Tactic:
case nil => rfl
Proof state after:
no goals
Theorem: Path.append_assoc
Proof state before:
V : Sort u_1
inst✝ : Quiver V
A B C D : V
r : Path C D
A✝ : V
q : Path A✝ C
⊢ append (append nil q) r = append nil (append q r)
Tactic:
rfl
Proof state after:
no goals
Theorem: Path.append_assoc
Proof state before:
V : Sort u_1
inst✝ : Quiver V
A B C D : V
r : Path C D
A✝ B✝ C✝ : V
a✝¹ : A✝ ⟶ B✝
a✝ : Path B✝ C✝
ih : ∀ (q : Path C✝ C), append (append a✝ q) r = append a✝ (append q r)
q : Path C✝ C
⊢ append (append (cons a✝¹ a✝) q) r = append (cons a✝¹ a✝) (append q r)
Tactic:
case cons ih => simp [append]; apply ih
Proof state after:
no goals
Theorem: Path.append_assoc
Proof state before:
V : Sort u_1
inst✝ : Quiver V
A B C D : V
r : Path C D
A✝ B✝ C✝ : V
a✝¹ : A✝ ⟶ B✝
a✝ : Path B✝ C✝
ih : ∀ (q : Path C✝ C), append (append a✝ q) r = append a✝ (append q r)
q : Path C✝ C
⊢ append (append (cons a✝¹ a✝) q) r = append (cons a✝¹ a✝) (append q r)
Tactic:
simp [append]
Proof state after:
V : Sort u_1
inst✝ : Quiver V
A B C D : V
r : Path C D
A✝ B✝ C✝ : V
a✝¹ : A✝ ⟶ B✝
a✝ : Path B✝ C✝
ih : ∀ (q : Path C✝ C), append (append a✝ q) r = append a✝ (append q r)
q : Path C✝ C
⊢ append (append a✝ q) r = append a✝ (append q r)
Theorem: Path.append_assoc
Proof state before:
V : Sort u_1
inst✝ : Quiver V
A B C D : V
r : Path C D
A✝ B✝ C✝ : V
a✝¹ : A✝ ⟶ B✝
a✝ : Path B✝ C✝
ih : ∀ (q : Path C✝ C), append (append a✝ q) r = append a✝ (append q r)
q : Path C✝ C
⊢ append (append a✝ q) r = append a✝ (append q r)
Tactic:
apply ih
Proof state after:
no goals
Theorem: Path.nil_length
Proof state before:
V : Sort u_1
inst✝ : Quiver V
A✝ B C D A B✝ : V
a✝ : A ⟶ B✝
p : Path B✝ A
⊢ length (cons a✝ p) = Nat.zero ↔ cons a✝ p = nil' A
Tactic:
apply Iff.intro <;> (intro; simp [length] at *)
Proof state after:
no goals
Theorem: Path.nil_length
Proof state before:
case mpr
V : Sort u_1
inst✝ : Quiver V
A✝ B C D A B✝ : V
a✝ : A ⟶ B✝
p : Path B✝ A
⊢ cons a✝ p = nil' A → length (cons a✝ p) = Nat.zero
Tactic:
intro
Proof state after:
case mpr
V : Sort u_1
inst✝ : Quiver V
A✝ B C D A B✝ : V
a✝¹ : A ⟶ B✝
p : Path B✝ A
a✝ : cons a✝¹ p = nil' A
⊢ length (cons a✝¹ p) = Nat.zero
Theorem: Path.nil_length
Proof state before:
case mpr
V : Sort u_1
inst✝ : Quiver V
A✝ B C D A B✝ : V
a✝¹ : A ⟶ B✝
p : Path B✝ A
a✝ : cons a✝¹ p = nil' A
⊢ length (cons a✝¹ p) = Nat.zero
Tactic:
simp [length] at *
Proof state after:
no goals
Theorem: Path.snoc_length
Proof state before:
V : Sort u_1
inst✝ : Quiver V
A✝ B✝² C✝ D A B✝¹ C B B✝ : V
a✝ : A ⟶ B✝
p' : Path B✝ B
e : B ⟶ C
⊢ length (snoc (cons a✝ p') e) = Nat.succ (length (cons a✝ p'))
Tactic:
rw [snoc_cons]
Proof state after:
V : Sort u_1
inst✝ : Quiver V
A✝ B✝² C✝ D A B✝¹ C B B✝ : V
a✝ : A ⟶ B✝
p' : Path B✝ B
e : B ⟶ C
⊢ length (cons a✝ (snoc p' e)) = Nat.succ (length (cons a✝ p'))
Theorem: Path.snoc_length
Proof state before:
V : Sort u_1
inst✝ : Quiver V
A✝ B✝² C✝ D A B✝¹ C B B✝ : V
a✝ : A ⟶ B✝
p' : Path B✝ B
e : B ⟶ C
⊢ length (cons a✝ (snoc p' e)) = Nat.succ (length (cons a✝ p'))
Tactic:
dsimp only [length]
Proof state after:
V : Sort u_1
inst✝ : Quiver V
A✝ B✝² C✝ D A B✝¹ C B B✝ : V
a✝ : A ⟶ B✝
p' : Path B✝ B
e : B ⟶ C
⊢ Nat.succ (length (snoc p' e)) = Nat.succ (Nat.succ (length p'))
Theorem: Path.snoc_length
Proof state before:
V : Sort u_1
inst✝ : Quiver V
A✝ B✝² C✝ D A B✝¹ C B B✝ : V
a✝ : A ⟶ B✝
p' : Path B✝ B
e : B ⟶ C
⊢ Nat.succ (length (snoc p' e)) = Nat.succ (Nat.succ (length p'))
Tactic:
apply congrArg
Proof state after:
case h
V : Sort u_1
inst✝ : Quiver V
A✝ B✝² C✝ D A B✝¹ C B B✝ : V
a✝ : A ⟶ B✝
p' : Path B✝ B
e : B ⟶ C
⊢ length (snoc p' e) = length p' + 1
Theorem: Path.snoc_length
Proof state before:
case h
V : Sort u_1
inst✝ : Quiver V
A✝ B✝² C✝ D A B✝¹ C B B✝ : V
a✝ : A ⟶ B✝
p' : Path B✝ B
e : B ⟶ C
⊢ length (snoc p' e) = length p' + 1
Tactic:
apply snoc_length
Proof state after:
no goals
Theorem: Path.length_append
Proof state before:
V : Sort u_1
inst✝ : Quiver V
A✝ B✝ C✝ D A B C : V
q : Path A C
⊢ length (append nil q) = length nil + length q
Tactic:
rw [Nat.add_comm]
Proof state after:
V : Sort u_1
inst✝ : Quiver V
A✝ B✝ C✝ D A B C : V
q : Path A C
⊢ length (append nil q) = length q + length nil
Theorem: Path.length_append
Proof state before:
V : Sort u_1
inst✝ : Quiver V
A✝ B✝ C✝ D A B C : V
q : Path A C
⊢ length (append nil q) = length q + length nil
Tactic:
rfl
Proof state after:
no goals
Theorem: Path.length_append
Proof state before:
V : Sort u_1
inst✝ : Quiver V
A✝ B✝² C✝ D A B✝¹ C B B✝ : V
a✝ : A ⟶ B✝
p' : Path B✝ B
q : Path B C
⊢ length (append (cons a✝ p') q) = length (cons a✝ p') + length q
Tactic:
dsimp [append, length]
Proof state after:
V : Sort u_1
inst✝ : Quiver V
A✝ B✝² C✝ D A B✝¹ C B B✝ : V
a✝ : A ⟶ B✝
p' : Path B✝ B
q : Path B C
⊢ Nat.succ (length (append p' q)) = Nat.succ (length p') + length q