Theorem: Path.inverse_append (Complexes/Structures/SerreGraph.lean)

State before:
V : Sort u_1
G : SerreGraph V
A✝ B✝ C✝ : V
p : Path A✝ B✝
A B C : V
q : Path A C
⊢ inverse (append nil q) = append (inverse q) (inverse nil)
Tactic:
simp [inverse]
State after:
no goals

State before:
V : Sort u_1
G : SerreGraph V
A✝ B✝ C✝ : V
p✝ : Path A✝ B✝
A B C : V
p : Path A C
⊢ inverse (append p nil) = append (inverse nil) (inverse p)
Tactic:
simp [inverse]
State after:
no goals

State before:
V : Sort u_1
G : SerreGraph V
A✝ B✝³ C✝ : V
p : Path A✝ B✝³
A B✝² C B B✝¹ : V
a✝¹ : A ⟶ B✝¹
p' : Path B✝¹ B
B✝ : V
a✝ : B ⟶ B✝
q' : Path B✝ C
⊢ inverse (append (cons a✝¹ p') (cons a✝ q')) = append (inverse (cons a✝ q')) (inverse (cons a✝¹ p'))
Tactic:
dsimp [inverse]
State after:
V : Sort u_1
G : SerreGraph V
A✝ B✝³ C✝ : V
p : Path A✝ B✝³
A B✝² C B B✝¹ : V
a✝¹ : A ⟶ B✝¹
p' : Path B✝¹ B
B✝ : V
a✝ : B ⟶ B✝
q' : Path B✝ C
⊢ snoc (inverse (append p' (cons a✝ q'))) (SerreGraph.op a✝¹) =
    append (snoc (inverse q') (SerreGraph.op a✝)) (snoc (inverse p') (SerreGraph.op a✝¹))

State before:
V : Sort u_1
G : SerreGraph V
A✝ B✝³ C✝ : V
p : Path A✝ B✝³
A B✝² C B B✝¹ : V
a✝¹ : A ⟶ B✝¹
p' : Path B✝¹ B
B✝ : V
a✝ : B ⟶ B✝
q' : Path B✝ C
⊢ snoc (inverse (append p' (cons a✝ q'))) (SerreGraph.op a✝¹) =
    append (snoc (inverse q') (SerreGraph.op a✝)) (snoc (inverse p') (SerreGraph.op a✝¹))
Tactic:
rw [inverse_append p' _, append_snoc]
State after:
V : Sort u_1
G : SerreGraph V
A✝ B✝³ C✝ : V
p : Path A✝ B✝³
A B✝² C B B✝¹ : V
a✝¹ : A ⟶ B✝¹
p' : Path B✝¹ B
B✝ : V
a✝ : B ⟶ B✝
q' : Path B✝ C
⊢ snoc (append (inverse (cons a✝ q')) (inverse p')) (SerreGraph.op a✝¹) =
    snoc (append (snoc (inverse q') (SerreGraph.op a✝)) (inverse p')) (SerreGraph.op a✝¹)

State before:
V : Sort u_1
G : SerreGraph V
A✝ B✝³ C✝ : V
p : Path A✝ B✝³
A B✝² C B B✝¹ : V
a✝¹ : A ⟶ B✝¹
p' : Path B✝¹ B
B✝ : V
a✝ : B ⟶ B✝
q' : Path B✝ C
⊢ snoc (append (inverse (cons a✝ q')) (inverse p')) (SerreGraph.op a✝¹) =
    snoc (append (snoc (inverse q') (SerreGraph.op a✝)) (inverse p')) (SerreGraph.op a✝¹)
Tactic:
rfl
State after:
no goals