Theorem: Vec.reverse_involution (Qpf/Util/Vec.lean)

State before:
α : Type u_1
n : ℕ
v : Vec α n
⊢ reverse (reverse v) = v
Tactic:
funext i
State after:
case h
α : Type u_1
n : ℕ
v : Vec α n
i : Fin2 n
⊢ reverse (reverse v) i = v i

State before:
case h
α : Type u_1
n : ℕ
v : Vec α n
i : Fin2 n
⊢ reverse (reverse v) i = v i
Tactic:
dsimp only [reverse]
State after:
case h
α : Type u_1
n : ℕ
v : Vec α n
i : Fin2 n
⊢ v (Fin2.inv (Fin2.inv i)) = v i

State before:
case h
α : Type u_1
n : ℕ
v : Vec α n
i : Fin2 n
⊢ v (Fin2.inv (Fin2.inv i)) = v i
Tactic:
apply congrArg
State after:
case h.h
α : Type u_1
n : ℕ
v : Vec α n
i : Fin2 n
⊢ Fin2.inv (Fin2.inv i) = i

State before:
case h.h
α : Type u_1
n : ℕ
v : Vec α n
i : Fin2 n
⊢ Fin2.inv (Fin2.inv i) = i
Tactic:
simp only [Fin2.inv, PFin2.toFin2_ofFin2, PFin2.inv_involution, PFin2.ofFin2_toFin2]
State after:
no goals