From a06ecd45233bc3e7215c109cb60e5e318f0e6c19 Mon Sep 17 00:00:00 2001 From: spiceghello Date: Thu, 8 Jun 2017 15:07:50 -0600 Subject: [PATCH] part of spectrify_elim --- homotopy/spectrum.hlean | 12 +++++++++++- pointed.hlean | 1 - 2 files changed, 11 insertions(+), 2 deletions(-) diff --git a/homotopy/spectrum.hlean b/homotopy/spectrum.hlean index 9ed3f7d..7e4fdb2 100644 --- a/homotopy/spectrum.hlean +++ b/homotopy/spectrum.hlean @@ -466,7 +466,17 @@ namespace spectrum { intro k, refine !equiv_gluen⁻¹ᵉ* ∘* apn k (f (n +' k)) }, { intro k, refine !passoc ⬝* pwhisker_right _ !equiv_gluen_inv_succ ⬝* _, refine !passoc ⬝* _, apply pwhisker_left, - refine !passoc ⬝* _, exact sorry }}, + refine !passoc ⬝* _, + refine pwhisker_left _ ((passoc _ _ (_ ∘* _))⁻¹*) ⬝* _, + refine pwhisker_left _ !passoc⁻¹* ⬝* _, + refine pwhisker_left _ (pwhisker_right _ (phomotopy_pinv_right_of_phomotopy (!loopn_succ_in_natural)⁻¹*)⁻¹*) ⬝* _, + refine pwhisker_right _ !apn_pinv ⬝* _, + refine (phomotopy_pinv_left_of_phomotopy _)⁻¹*, + refine pwhisker_right _ !pmap_eta⁻¹* ⬝* _, + refine apn_psquare k _, + refine pwhisker_right _ _ ⬝* psquare_of_phomotopy !smap.glue_square, + exact !pmap_eta⁻¹* + }}, { intro n, exact sorry } end diff --git a/pointed.hlean b/pointed.hlean index 778f3bb..453a3cd 100644 --- a/pointed.hlean +++ b/pointed.hlean @@ -151,5 +151,4 @@ namespace pointed esimp, exact !idp_con end - end pointed