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

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

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

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