bugfix

forked-from-1kasper · Dec 21, 2023 · 7698f34 · 7698f34
1 parent f0ccc21
commit 7698f34
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 3 deletions.
diff --git a/GroundZero/HITs/Circle.lean b/GroundZero/HITs/Circle.lean
@@ -549,7 +549,6 @@ namespace Circle
       transitivity; apply mapFunctoriality; apply ap;
       transitivity; apply Id.mapInv; apply ap Id.symm; apply recβrule₂;
       transitivity; apply transportconstOverComposition;
-      transitivity; apply transportconstOverInv;
       transitivity; apply uaβrev; apply ap pred;
       symmetry; apply transportToTransportconst
     end

diff --git a/GroundZero/Theorems/Hopf.lean b/GroundZero/Theorems/Hopf.lean
@@ -48,8 +48,8 @@ namespace Real
   begin
     intro b; transitivity; apply transportToTransportconst;
     transitivity; apply ap (transportconst · b);
-    transitivity; apply Id.mapInv; apply ap; apply recβrule₂;
-    transitivity; apply transportconstOverInv; apply uaβrev
+    transitivity; apply Id.mapInv; apply ap;
+    apply recβrule₂; apply uaβrev
   end
 end Real