n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
α β γ : TypeVec n
f : α ⟹ β
g : β ⟹ γ
x : F α
⊢ (g ⊚ f) <$$> abs (repr x) = g <$$> f <$$> abs (repr x)
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
α β γ : TypeVec n
f : α ⟹ β
g : β ⟹ γ
x : F α
⊢ (g ⊚ f) <$$> x = g <$$> f <$$> x
rw [← abs_repr x]
case mk
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
α β γ : TypeVec n
f✝ : α ⟹ β
g : β ⟹ γ
x : F α
a : (P F).A
f : MvPFunctor.B (P F) a ⟹ α
⊢ (g ⊚ f✝) <$$> abs { fst := a, snd := f } = g <$$> f✝ <$$> abs { fst := a, snd := f }
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
α β γ : TypeVec n
f : α ⟹ β
g : β ⟹ γ
x : F α
⊢ (g ⊚ f) <$$> abs (repr x) = g <$$> f <$$> 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
f✝ : α ⟹ β
g : β ⟹ γ
x : F α
a : (P F).A
f : MvPFunctor.B (P F) a ⟹ α
⊢ abs ((g ⊚ f✝) <$$> { fst := a, snd := f }) = abs (g <$$> f✝ <$$> { fst := a, snd := f })
case mk
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
α β γ : TypeVec n
f✝ : α ⟹ β
g : β ⟹ γ
x : F α
a : (P F).A
f : MvPFunctor.B (P F) a ⟹ α
⊢ (g ⊚ f✝) <$$> abs { fst := a, snd := f } = g <$$> f✝ <$$> abs { fst := a, snd := f }
rw [← abs_map, ← abs_map, ← abs_map]
no goals
case mk
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
α β γ : TypeVec n
f✝ : α ⟹ β
g : β ⟹ γ
x : F α
a : (P F).A
f : MvPFunctor.B (P F) a ⟹ α
⊢ abs ((g ⊚ f✝) <$$> { fst := a, snd := f }) = abs (g <$$> f✝ <$$> { fst := a, snd := f })
rfl