[GOAL]
n m : ℕ
F : TypeVec n → Type u_1
fF : MvFunctor F
q : MvQPF F
G : Fin2 n → TypeVec m → Type u
fG : (i : Fin2 n) → MvFunctor (G i)
q' : (i : Fin2 n) → MvQPF (G i)
α β : TypeVec m
f : α ⟹ β
⊢ ∀ {α : TypeVec m} (x : Comp F G α),
    (fun {α} => Comp.mk ∘ (MvFunctor.map fun i => abs) ∘ abs ∘ comp.get)
        ((fun {α} => comp.mk ∘ repr ∘ (MvFunctor.map fun i => repr) ∘ Comp.get) x) =
      x
[PROOFSTEP]
intros
[GOAL]
n m : ℕ
F : TypeVec n → Type u_1
fF : MvFunctor F
q : MvQPF F
G : Fin2 n → TypeVec m → Type u
fG : (i : Fin2 n) → MvFunctor (G i)
q' : (i : Fin2 n) → MvQPF (G i)
α β : TypeVec m
f : α ⟹ β
α✝ : TypeVec m
x✝ : Comp F G α✝
⊢ (fun {α} => Comp.mk ∘ (MvFunctor.map fun i => abs) ∘ abs ∘ comp.get)
      ((fun {α} => comp.mk ∘ repr ∘ (MvFunctor.map fun i => repr) ∘ Comp.get) x✝) =
    x✝
[PROOFSTEP]
simp only [(· ∘ ·), comp.get_mk, abs_repr, map_map, TypeVec.comp, MvFunctor.id_map', Comp.mk_get]
[GOAL]
n m : ℕ
F : TypeVec n → Type u_1
fF : MvFunctor F
q : MvQPF F
G : Fin2 n → TypeVec m → Type u
fG : (i : Fin2 n) → MvFunctor (G i)
q' : (i : Fin2 n) → MvQPF (G i)
α β : TypeVec m
f : α ⟹ β
⊢ ∀ {α β : TypeVec m} (f : α ⟹ β) (p : Obj (comp (P F) fun i => P (G i)) α),
    (fun {α} => Comp.mk ∘ (MvFunctor.map fun i => abs) ∘ abs ∘ comp.get) (f <$$> p) =
      f <$$> (fun {α} => Comp.mk ∘ (MvFunctor.map fun i => abs) ∘ abs ∘ comp.get) p
[PROOFSTEP]
intros
[GOAL]
n m : ℕ
F : TypeVec n → Type u_1
fF : MvFunctor F
q : MvQPF F
G : Fin2 n → TypeVec m → Type u
fG : (i : Fin2 n) → MvFunctor (G i)
q' : (i : Fin2 n) → MvQPF (G i)
α β : TypeVec m
f : α ⟹ β
α✝ β✝ : TypeVec m
f✝ : α✝ ⟹ β✝
p✝ : Obj (comp (P F) fun i => P (G i)) α✝
⊢ (fun {α} => Comp.mk ∘ (MvFunctor.map fun i => abs) ∘ abs ∘ comp.get) (f✝ <$$> p✝) =
    f✝ <$$> (fun {α} => Comp.mk ∘ (MvFunctor.map fun i => abs) ∘ abs ∘ comp.get) p✝
[PROOFSTEP]
simp only [(· ∘ ·)]
[GOAL]
n m : ℕ
F : TypeVec n → Type u_1
fF : MvFunctor F
q : MvQPF F
G : Fin2 n → TypeVec m → Type u
fG : (i : Fin2 n) → MvFunctor (G i)
q' : (i : Fin2 n) → MvQPF (G i)
α β : TypeVec m
f : α ⟹ β
α✝ β✝ : TypeVec m
f✝ : α✝ ⟹ β✝
p✝ : Obj (comp (P F) fun i => P (G i)) α✝
⊢ Comp.mk ((fun i => abs) <$$> abs (comp.get (f✝ <$$> p✝))) = f✝ <$$> Comp.mk ((fun i => abs) <$$> abs (comp.get p✝))
[PROOFSTEP]
rw [← abs_map]
[GOAL]
n m : ℕ
F : TypeVec n → Type u_1
fF : MvFunctor F
q : MvQPF F
G : Fin2 n → TypeVec m → Type u
fG : (i : Fin2 n) → MvFunctor (G i)
q' : (i : Fin2 n) → MvQPF (G i)
α β : TypeVec m
f : α ⟹ β
α✝ β✝ : TypeVec m
f✝ : α✝ ⟹ β✝
p✝ : Obj (comp (P F) fun i => P (G i)) α✝
⊢ Comp.mk (abs ((fun i => abs) <$$> comp.get (f✝ <$$> p✝))) = f✝ <$$> Comp.mk ((fun i => abs) <$$> abs (comp.get p✝))
[PROOFSTEP]
simp only [comp.get_map, map_map, TypeVec.comp, abs_map, map_mk]
