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

State before:
V : Sort u_1
G : SerreGraph V
A B C : V
p : Path A B
⊢ ∀ (p : Path A B), last p = first (inverse p)
Tactic:
intro p
State after:
V : Sort u_1
G : SerreGraph V
A B C : V
p✝ p : Path A B
⊢ last p = first (inverse p)

State before:
V : Sort u_1
G : SerreGraph V
A B C : V
p✝ p : Path A B
⊢ last p = first (inverse p)
Tactic:
let p' := p.inverse
State after:
V : Sort u_1
G : SerreGraph V
A B C : V
p✝ p : Path A B
p' : Path B A := inverse p
⊢ last p = first (inverse p)

State before:
V : Sort u_1
G : SerreGraph V
A B C : V
p✝ p : Path A B
p' : Path B A := inverse p
⊢ last p = first (inverse p)
Tactic:
have pinv : p = p'.inverse := by simp
State after:
V : Sort u_1
G : SerreGraph V
A B C : V
p✝ p : Path A B
p' : Path B A := inverse p
pinv : p = inverse p'
⊢ last p = first (inverse p)

State before:
V : Sort u_1
G : SerreGraph V
A B C : V
p✝ p : Path A B
p' : Path B A := inverse p
pinv : p = inverse p'
⊢ last p = first (inverse p)
Tactic:
rw [pinv, inverse_inv p']
State after:
V : Sort u_1
G : SerreGraph V
A B C : V
p✝ p : Path A B
p' : Path B A := inverse p
pinv : p = inverse p'
⊢ last (inverse p') = first p'

State before:
V : Sort u_1
G : SerreGraph V
A B C : V
p✝ p : Path A B
p' : Path B A := inverse p
pinv : p = inverse p'
⊢ last (inverse p') = first p'
Tactic:
apply Eq.symm
State after:
case h
V : Sort u_1
G : SerreGraph V
A B C : V
p✝ p : Path A B
p' : Path B A := inverse p
pinv : p = inverse p'
⊢ first p' = last (inverse p')

State before:
case h
V : Sort u_1
G : SerreGraph V
A B C : V
p✝ p : Path A B
p' : Path B A := inverse p
pinv : p = inverse p'
⊢ first p' = last (inverse p')
Tactic:
apply first_eq_inv_last
State after:
no goals

State before:
V : Sort u_1
G : SerreGraph V
A B C : V
p✝ p : Path A B
p' : Path B A := inverse p
⊢ p = inverse p'
Tactic:
simp
State after:
no goals