Theorem: Path.Homotopy.inv_cancel_left (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 (inverse p) 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 (inverse p) p)

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
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))

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