Theorem: Path.Homotopy.trans (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))
h' : NullHomotopy (append q (inverse r))
⊢ Homotopy p r
Tactic:
let H := NullHomotopy.concat h 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 r))
H : NullHomotopy (append (append p (inverse q)) (append q (inverse r))) := NullHomotopy.concat h h'
⊢ Homotopy p r

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 r))
H : NullHomotopy (append (append p (inverse q)) (append q (inverse r))) := NullHomotopy.concat h h'
⊢ Homotopy p r
Tactic:
rw [Path.append_assoc p _ _, ← Path.append_assoc _ q _] 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 r))
H : NullHomotopy (append p (append (append (inverse q) q) (inverse r)))
⊢ Homotopy p r

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 r))
H : NullHomotopy (append p (append (append (inverse q) q) (inverse r)))
⊢ Homotopy p r
Tactic:
let H' := NullHomotopy.contract (.swap $ .trivial _) 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 r))
H : NullHomotopy (append p (append (append (inverse q) q) (inverse r)))
H' : NullHomotopy (append p (inverse r)) := NullHomotopy.contract (NullHomotopy.swap (NullHomotopy.trivial q)) H
⊢ Homotopy p r

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 r))
H : NullHomotopy (append p (append (append (inverse q) q) (inverse r)))
H' : NullHomotopy (append p (inverse r)) := NullHomotopy.contract (NullHomotopy.swap (NullHomotopy.trivial q)) H
⊢ Homotopy p r
Tactic:
exact .rel H'
State after:
no goals