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

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

State before:
V : Sort u_1
G : SerreGraph V
A✝ B✝² C : V
p : Path A✝ B✝²
A B✝¹ B B✝ : V
a✝ : A ⟶ B✝
p' : Path B✝ B
⊢ length (snoc (inverse p') (SerreGraph.op a✝)) = Nat.succ (length p')
Tactic:
rw [snoc_length]
State after:
V : Sort u_1
G : SerreGraph V
A✝ B✝² C : V
p : Path A✝ B✝²
A B✝¹ B B✝ : V
a✝ : A ⟶ B✝
p' : Path B✝ B
⊢ Nat.succ (length (inverse p')) = Nat.succ (length p')

State before:
V : Sort u_1
G : SerreGraph V
A✝ B✝² C : V
p : Path A✝ B✝²
A B✝¹ B B✝ : V
a✝ : A ⟶ B✝
p' : Path B✝ B
⊢ Nat.succ (length (inverse p')) = Nat.succ (length p')
Tactic:
apply congrArg
State after:
case h
V : Sort u_1
G : SerreGraph V
A✝ B✝² C : V
p : Path A✝ B✝²
A B✝¹ B B✝ : V
a✝ : A ⟶ B✝
p' : Path B✝ B
⊢ length (inverse p') = length p'

State before:
case h
V : Sort u_1
G : SerreGraph V
A✝ B✝² C : V
p : Path A✝ B✝²
A B✝¹ B B✝ : V
a✝ : A ⟶ B✝
p' : Path B✝ B
⊢ length (inverse p') = length p'
Tactic:
apply length_inverse
State after:
no goals