n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
x : F α
⊢ TypeVec.id <$$> abs (repr x) = abs (repr x)
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
x : F α
⊢ TypeVec.id <$$> x = x
rw [← abs_repr x]
case mk
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
x : F α
a : (P F).A
f : MvPFunctor.B (P F) a ⟹ α
⊢ TypeVec.id <$$> abs { fst := a, snd := f } = abs { fst := a, snd := f }
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
x : F α
⊢ TypeVec.id <$$> abs (repr x) = abs (repr x)
cases' repr x with a f
case mk
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
x : F α
a : (P F).A
f : MvPFunctor.B (P F) a ⟹ α
⊢ abs (TypeVec.id <$$> { fst := a, snd := f }) = abs { fst := a, snd := f }
case mk
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
x : F α
a : (P F).A
f : MvPFunctor.B (P F) a ⟹ α
⊢ TypeVec.id <$$> abs { fst := a, snd := f } = abs { fst := a, snd := f }
rw [← abs_map]
no goals
case mk
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
x : F α
a : (P F).A
f : MvPFunctor.B (P F) a ⟹ α
⊢ abs (TypeVec.id <$$> { fst := a, snd := f }) = abs { fst := a, snd := f }
rfl