Theorem: Path.Homotopy.inv_cancel_right (Complexes/Structures/CombinatorialTwoComplex.lean)

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]
State after:
V : Sort u_1
C : CombinatorialTwoComplex V
u v : V
p✝ q r p : Path u v
⊢ NullHomotopy (append p (inverse p))

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
State after:
no goals