[GOAL]
n : ℕ
F : TypeVec n → Type u
inst✝¹ : MvFunctor F
q : MvQPF F
G : TypeVec n → Type u
inst✝ : MvFunctor G
FG_abs : {α : TypeVec n} → F α → G α
FG_repr : {α : TypeVec n} → G α → F α
FG_abs_repr : ∀ {α : TypeVec n} (x : G α), FG_abs (FG_repr x) = x
FG_abs_map : ∀ {α β : TypeVec n} (f : α ⟹ β) (x : F α), FG_abs (f <$$> x) = f <$$> FG_abs x
α✝ : TypeVec n
x : G α✝
⊢ (fun {α} p => FG_abs (abs p)) ((fun {α} x => repr (FG_repr x)) x) = x
[PROOFSTEP]
dsimp
[GOAL]
n : ℕ
F : TypeVec n → Type u
inst✝¹ : MvFunctor F
q : MvQPF F
G : TypeVec n → Type u
inst✝ : MvFunctor G
FG_abs : {α : TypeVec n} → F α → G α
FG_repr : {α : TypeVec n} → G α → F α
FG_abs_repr : ∀ {α : TypeVec n} (x : G α), FG_abs (FG_repr x) = x
FG_abs_map : ∀ {α β : TypeVec n} (f : α ⟹ β) (x : F α), FG_abs (f <$$> x) = f <$$> FG_abs x
α✝ : TypeVec n
x : G α✝
⊢ FG_abs (abs (repr (FG_repr x))) = x
[PROOFSTEP]
rw [abs_repr, FG_abs_repr]
[GOAL]
n : ℕ
F : TypeVec n → Type u
inst✝¹ : MvFunctor F
q : MvQPF F
G : TypeVec n → Type u
inst✝ : MvFunctor G
FG_abs : {α : TypeVec n} → F α → G α
FG_repr : {α : TypeVec n} → G α → F α
FG_abs_repr : ∀ {α : TypeVec n} (x : G α), FG_abs (FG_repr x) = x
FG_abs_map : ∀ {α β : TypeVec n} (f : α ⟹ β) (x : F α), FG_abs (f <$$> x) = f <$$> FG_abs x
α✝ β✝ : TypeVec n
f : α✝ ⟹ β✝
p : MvPFunctor.Obj (P F) α✝
⊢ (fun {α} p => FG_abs (abs p)) (f <$$> p) = f <$$> (fun {α} p => FG_abs (abs p)) p
[PROOFSTEP]
dsimp
[GOAL]
n : ℕ
F : TypeVec n → Type u
inst✝¹ : MvFunctor F
q : MvQPF F
G : TypeVec n → Type u
inst✝ : MvFunctor G
FG_abs : {α : TypeVec n} → F α → G α
FG_repr : {α : TypeVec n} → G α → F α
FG_abs_repr : ∀ {α : TypeVec n} (x : G α), FG_abs (FG_repr x) = x
FG_abs_map : ∀ {α β : TypeVec n} (f : α ⟹ β) (x : F α), FG_abs (f <$$> x) = f <$$> FG_abs x
α✝ β✝ : TypeVec n
f : α✝ ⟹ β✝
p : MvPFunctor.Obj (P F) α✝
⊢ FG_abs (abs (f <$$> p)) = f <$$> FG_abs (abs p)
[PROOFSTEP]
rw [abs_map, FG_abs_map]
