Theorem: Path.Homotopy.inv_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 : V
p q : Path u v
r : NullHomotopy (append p (inverse q))
⊢ NullHomotopy (append (inverse p) (inverse (inverse q)))
Tactic:
rw [← inverse_append]
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))

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

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

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