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

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

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