Login

Verification run

Run 1302

promachina/iut-leanbranch e21-929-cohomology-checkpointtriggered via github_push
failedcommit 9ce7ebcfce50toolchain lean-v4-30-0prover leantook 2h 1m · finished 2d ago

lake build failed with exit code none (process did not exit cleanly) (toolchain lean-v4-30-0, command: elan run leanprover/lean4:v4.30.0 -- bash -c export PATH="$(dirname "$(elan which lean)"):$PATH"; exec "$@" apx-lean-phase lake build)

Open project

Package inputs

This verification run did not include a theorem package lock. Its inputs depend only on repository, toolchain, image, and command inputs.

Trust verification

Recomputes trust checks from the recorded attestations, manifest, and command history.

(verification not run)

Manifest

Loads the published files manifest and location metadata for this job.

(manifest not loaded)

Verifier log excerpt

s linter can be disabled with `set_option linter.style.cdot false`
warning: Iut/Foundations/SourceFiniteEtaleSignTorsor.lean:5284:4: This central dot `·` is isolated; please merge it with the next line.

Note: This linter can be disabled with `set_option linter.style.cdot false`
warning: Iut/Foundations/SourceFiniteEtaleSignTorsor.lean:5300:4: This central dot `·` is isolated; please merge it with the next line.

Note: This linter can be disabled with `set_option linter.style.cdot false`
warning: Iut/Foundations/SourceFiniteEtaleSignTorsor.lean:5315:4: This central dot `·` is isolated; please merge it with the next line.

Note: This linter can be disabled with `set_option linter.style.cdot false`
warning: Iut/Foundations/SourceFiniteEtaleSignTorsor.lean:5788:2: try 'simp' instead of 'simpa'

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`
warning: Iut/Foundations/SourceFiniteEtaleSignTorsor.lean:5797:2: try 'simp' instead of 'simpa'

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`
warning: Iut/Foundations/SourceFiniteEtaleSignTorsor.lean:7977:13: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice

Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false`
warning: Iut/Foundations/SourceFiniteEtaleSignTorsor.lean:8145:13: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice

Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false`
warning: Iut/Foundations/SourceFiniteEtaleSignTorsor.lean:11284:0: Please, add a comment explaining the need for modifying the maxHeartbeat limit, as in
set_option maxHeartbeats 400000 in
-- reason for change
...

Note: This linter can be disabled with `set_option linter.style.maxHeartbeats false`
warning: Iut/Foundations/SourceFiniteEtaleSignTorsor.lean:11284:0: Unscoped option maxHeartbeats is not allowed:
Please scope this to individual declarations, as in
```
set_option maxHeartbeats in
-- comment explaining why this is necessary
example : ... := ...
```

Note: This linter can be disabled with `set_option linter.style.setOption false`
warning: Iut/Foundations/SourceFiniteEtaleSignTorsor.lean:11476:0: Please, add a comment explaining the need for modifying the maxHeartbeat limit, as in
set_option maxHeartbeats 400000 in
-- reason for change
...

Note: This linter can be disabled with `set_option linter.style.maxHeartbeats false`
warning: Iut/Foundations/SourceFiniteEtaleSignTorsor.lean:11476:0: Unscoped option maxHeartbeats is not allowed:
Please scope this to individual declarations, as in
```
set_option maxHeartbeats in
-- comment explaining why this is necessary
example : ... := ...
```

Note: This linter can be disabled with `set_option linter.style.setOption false`
warning: Iut/Foundations/SourceFiniteEtaleSignTorsor.lean:11667:0: Please, add a comment explaining the need for modifying the maxHeartbeat limit, as in
set_option maxHeartbeats 800000 in
-- reason for change
...

Note: This linter can be disabled with `set_option linter.style.maxHeartbeats false`
warning: Iut/Foundations/SourceFiniteEtaleSignTorsor.lean:11667:0: Unscoped option maxHeartbeats is not allowed:
Please scope this to individual declarations, as in
```
set_option maxHeartbeats in
-- comment explaining why this is necessary
example : ... := ...
```

Note: This linter can be disabled with `set_option linter.style.setOption false`
✔ [4606/6595] Built Iut.Foundations.SourceEtalePseudofunctorTwoPullbackCancellationLiftToYInv (2.8s)
✔ [4607/6595] Built Iut.Foundations.SourceFiniteEtaleAffineOverCoordinateAction (2.4s)
✔ [4609/6595] Built Iut.Foundations.SourceSingleObjOppositeEquivalence (1.6s)
✔ [4610/6595] Built Iut.Foundations.SourceCategoryPackedHEqEndpointLinkDataJoinProjections (1.4s)
✔ [4611/6595] Built Iut.Foundations.SourceEtalePseudofunctorStrongTransWhiskerRightIsoSymmHom (2.6s)
✔ [4612/6595] Built Iut.Foundations.SourceEtalePseudofunctorStrongTransPentagonInvPrefix (4.1s)
✔ [4613/6595] Built Iut.Foundations.SourceCategoryEqToHomTransportedEndpointDataMap (1.5s)
✔ [4614/6595] Built Iut.Foundations.SourceEtalePseudofunctorChangeFirstBaseMap (3.7s)
✔ [4615/6595] Built Iut.Foundations.SourceEtalePseudofunctorChangeSecondBaseMap (3.7s)
✔ [4616/6595] Built Iut.Foundations.SourceEtalePseudofunctorFaithfulCellAssembly (3.7s)
✔ [4617/6595] Built Iut.Foundations.SourceEtalePseudofunctorRepresentablePullbackTwoCell (116s)
✔ [4618/6595] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalHomPointValueRecovery (2.9s)
✔ [4619/6595] Built Iut.Foundations.SourceFiniteEtaleSchemeCoverClopenMono (2.9s)
⚠ [4620/6595] Built Iut.Foundations.SourceFiniteEtaleSignTorsorAffineEffectiveness (169s)
warning: Iut/Foundations/SourceFiniteEtaleSignTorsorAffineEffectiveness.lean:2163:58: remove line break in the source

This part of the code
  '⊗ₜ[
   '
should be written as
  '⊗ₜ[Scheme.Γ.obj'


Note: This linter can be disabled with `set_option linter.style.whitespace false`
warning: Iut/Foundations/SourceFiniteEtaleSignTorsorAffineEffectiveness.lean:2166:56: remove line break in the source

This part of the code
  '⊗ₜ[
   '
should be written as
  '⊗ₜ[Scheme.Γ.obj'


Note: This linter can be disabled with `set_option linter.style.whitespace false`
warning: Iut/Foundations/SourceFiniteEtaleSignTorsorAffineEffectiveness.lean:2169:52: remove line break in the source

This part of the code
  '⊗[
   '
should be written as
  '⊗[Scheme.Γ.obj'


Note: This linter can be disabled with `set_option linter.style.whitespace false`
warning: Iut/Foundations/SourceFiniteEtaleSignTorsorAffineEffectiveness.lean:2448:58: remove line break in the source

This part of the code
  '⊗ₜ[
   '
should be written as
  '⊗ₜ[Scheme.Γ.obj'


Note: This linter can be disabled with `set_option linter.style.whitespace false`
warning: Iut/Foundations/SourceFiniteEtaleSignTorsorAffineEffectiveness.lean:2451:56: remove line break in the source

This part of the code
  '⊗ₜ[
   '
should be written as
  '⊗ₜ[Scheme.Γ.obj'


Note: This linter can be disabled with `set_option linter.style.whitespace false`
warning: Iut/Foundations/SourceFiniteEtaleSignTorsorAffineEffectiveness.lean:2454:52: remove line break in the source

This part of the code
  '⊗[
   '
should be written as
  '⊗[Scheme.Γ.obj'


Note: This linter can be disabled with `set_option linter.style.whitespace false`
warning: Iut/Foundations/SourceFiniteEtaleSignTorsorAffineEffectiveness.lean:2460:58: remove line break in the source

This part of the code
  '⊗ₜ[
   '
should be written as
  '⊗ₜ[Scheme.Γ.obj'


Note: This linter can be disabled with `set_option linter.style.whitespace false`
warning: Iut/Foundations/SourceFiniteEtaleSignTorsorAffineEffectiveness.lean:2463:56: remove line break in the source

This part of the code
  '⊗ₜ[
   '
should be written as
  '⊗ₜ[Scheme.Γ.obj'


Note: This linter can be disabled with `set_option linter.style.whitespace false`
warning: Iut/Foundations/SourceFiniteEtaleSignTorsorAffineEffectiveness.lean:2466:52: remove line break in the source

This part of the code
  '⊗[
   '
should be written as
  '⊗[Scheme.Γ.obj'


Note: This linter can be disabled with `set_option linter.style.whitespace false`
✔ [4621/6595] Built Iut.Foundations.SourceFiniteEtaleSignQuotientPrestack (43s)
✔ [4622/6595] Built Iut.Foundations.SourceFiniteEtaleSignTorsorTargetStackDescent (2.9s)
✔ [4623/6595] Built Iut.Foundations.SourceFiniteEtaleSignTorsorTrivial (4.6s)
✔ [4624/6595] Built Iut.Foundations.SourceEtalePseudofunctorTwoPullbackCancellationLiftToYLawful (2.7s)
✔ [4626/6595] Built Iut.Foundations.SourceFiniteEtaleAffineOverCoordinateFiniteEtale (2.5s)
✔ [4627/6595] Built Iut.Foundations.SourceCategoryPackedHEqTwoMorphismComposition (1.5s)
✔ [4628/6595] Built Iut.Foundations.SourceEtaleStackRepresentablePropertyChangeMap (2.8s)
✔ [4629/6595] Built Iut.Foundations.SourceEtalePseudofunctorConeAfterChangeSecondBaseMap (2.9s)
✔ [4630/6595] Built Iut.Foundations.SourceEtalePseudofunctorRepresentedIsoPointLift (3.2s)
✔ [4631/6595] Built Iut.Foundations.SourceEtalePseudofunctorRepresentablePullbackWitness (2.8s)
✔ [4632/6595] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalHomYonedaPointValue (2.7s)
✔ [4633/6595] Built Iut.Foundations.SourceFiniteEtaleSchemeCoverDirectSummand (3.2s)
✔ [4634/6595] Built Iut.Foundations.SourceFiniteEtaleSchemeCoverUnderlyingEpiRange (2.8s)
⚠ [4635/6595] Built Iut.Foundations.SourceFiniteEtaleSignTorsorAffineCoverCollapse (10s)
warning: Iut/Foundations/SourceFiniteEtaleSignTorsorAffineCoverCollapse.lean:1268:2: try 'simp' instead of 'simpa'

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`
✔ [4636/6595] Built Iut.Foundations.SourceFiniteEtaleSignQuotientStackCriterion (2.0s)
✔ [4637/6595] Built Iut.Foundations.SourceFiniteEtaleSignQuotientAtlas (5.6s)
✔ [4638/6598] Built Iut.Foundations.SourceEtalePseudofunctorTwoPullbackCancellationLiftToYHomToX (2.8s)
✔ [4639/6599] Built Iut.Foundations.SourceEtalePseudofunctorConeAfterChangeSecondBaseMapFromConeOf (3.0s)
✔ [4640/6599] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalIsoBaseChangeOver (3.3s)
✔ [4641/6599] Built Iut.Foundations.SourceRepresentableStrongTransReconstruction (3.1s)
✔ [4642/6599] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalHomYonedaNaturality (2.9s)
✔ [4643/6599] Built Iut.Foundations.SourceFiniteEtaleSchemeCoverAffineSource (2.8s)
✔ [4644/6599] Built Iut.Foundations.SourceFiniteEtaleSchemeCoverUnderlyingEpiSurjective (7.0s)
⚠ [4645/6599] Built Iut.Foundations.SourceFiniteEtaleSignTorsorAffineCoverAssembly (875s)
warning: Iut/Foundations/SourceFiniteEtaleSignTorsorAffineCoverAssembly.lean:1177:0: Please, add a comment explaining the need for modifying the maxHeartbeat limit, as in
set_option maxHeartbeats 400000 in
-- reason for change
...

Note: This linter can be disabled with `set_option linter.style.maxHeartbeats false`
warning: Iut/Foundations/SourceFiniteEtaleSignTorsorAffineCoverAssembly.lean:1268:0: Please, add a comment explaining the need for modifying the maxHeartbeat limit, as in
set_option maxHeartbeats 400000 in
-- reason for change
...

Note: This linter can be disabled with `set_option linter.style.maxHeartbeats false`
warning: Iut/Foundations/SourceFiniteEtaleSignTorsorAffineCoverAssembly.lean:1329:0: Please, add a comment explaining the need for modifying the maxHeartbeat limit, as in
set_option maxHeartbeats 400000 in
-- reason for change
...

Note: This linter can be disabled with `set_option linter.style.maxHeartbeats false`
warning: Iut/Foundations/SourceFiniteEtaleSignTorsorAffineCoverAssembly.lean:1409:0: Please, add a comment explaining the need for modifying the maxHeartbeat limit, as in
set_option maxHeartbeats 400000 in
-- reason for change
...

Note: This linter can be disabled with `set_option linter.style.maxHeartbeats false`
warning: Iut/Foundations/SourceFiniteEtaleSignTorsorAffineCoverAssembly.lean:2812:0: Please, add a comment explaining the need for modifying the maxHeartbeat limit, as in
set_option maxHeartbeats 400000 in
-- reason for change
...

Note: This linter can be disabled with `set_option linter.style.maxHeartbeats false`
warning: Iut/Foundations/SourceFiniteEtaleSignTorsorAffineCoverAssembly.lean:2917:0: Please, add a comment explaining the need for modifying the maxHeartbeat limit, as in
set_option maxHeartbeats 400000 in
-- reason for change
...

Note: This linter can be disabled with `set_option linter.style.maxHeartbeats false`
warning: Iut/Foundations/SourceFiniteEtaleSignTorsorAffineCoverAssembly.lean:3052:0: Please, add a comment explaining the need for modifying the maxHeartbeat limit, as in
set_option maxHeartbeats 400000 in
-- reason for change
...

Note: This linter can be disabled with `set_option linter.style.maxHeartbeats false`
warning: Iut/Foundations/SourceFiniteEtaleSignTorsorAffineCoverAssembly.lean:3103:0: Please, add a comment explaining the need for modifying the maxHeartbeat limit, as in
set_option maxHeartbeats 400000 in
-- reason for change
...

Note: This linter can be disabled with `set_option linter.style.maxHeartbeats false`
warning: Iut/Foundations/SourceFiniteEtaleSignTorsorAffineCoverAssembly.lean:3150:0: Please, add a comment explaining the need for modifying the maxHeartbeat limit, as in
set_option maxHeartbeats 400000 in
-- reason for change
...

Note: This linter can be disabled with `set_option linter.style.maxHeartbeats false`
warning: Iut/Foundations/SourceFiniteEtaleSignTorsorAffineCoverAssembly.lean:3191:0: Please, add a comment explaining the need for modifying the maxHeartbeat limit, as in
set_option maxHeartbeats 400000 in
-- reason for change
...

Note: This linter can be disabled with `set_option linter.style.maxHeartbeats false`
warning: Iut/Foundations/SourceFiniteEtaleSignTorsorAffineCoverAssembly.lean:3572:0: Please, add a comment explaining the need for modifying the maxHeartbeat limit, as in
set_option maxHeartbeats 400000 in
-- reason for change
...

Note: This linter can be disabled with `set_option linter.style.maxHeartbeats false`
warning: Iut/Foundations/SourceFiniteEtaleSignTorsorAffineCoverAssembly.lean:3699:0: Please, add a comment explaining the need for modifying the maxHeartbeat limit, as in
set_option maxHeartbeats 400000 in
-- reason for change
...

Note: This linter can be disabled with `set_option linter.style.maxHeartbeats false`
warning: Iut/Foundations/SourceFiniteEtaleSignTorsorAffineCoverAssembly.lean:3826:0: Please, add a comment explaining the need for modifying the maxHeartbeat limit, as in
set_option maxHeartbeats 400000 in
-- reason for change
...

Note: This linter can be disabled with `set_option linter.style.maxHeartbeats false`
warning: Iut/Foundations/SourceFiniteEtaleSignTorsorAffineCoverAssembly.lean:3958:0: Please, add a comment explaining the need for modifying the maxHeartbeat limit, as in
set_option maxHeartbeats 400000 in
-- reason for change
...

Note: This linter can be disabled with `set_option linter.style.maxHeartbeats false`
warning: Iut/Foundations/SourceFiniteEtaleSignTorsorAffineCoverAssembly.lean:4089:0: Please, add a comment explaining the need for modifying the maxHeartbeat limit, as in
set_option maxHeartbeats 400000 in
-- reason for change
...

Note: This linter can be disabled with `set_option linter.style.maxHeartbeats false`
warning: Iut/Foundations/SourceFiniteEtaleSignTorsorAffineCoverAssembly.lean:4266:0: Please, add a comment explaining the need for modifying the maxHeartbeat limit, as in
set_option maxHeartbeats 400000 in
-- reason for change
...

Note: This linter can be disabled with `set_option linter.style.maxHeartbeats false`
warning: Iut/Foundations/SourceFiniteEtaleSignTorsorAffineCoverAssembly.lean:4420:0: Please, add a comment explaining the need for modifying the maxHeartbeat limit, as in
set_option maxHeartbeats 400000 in
-- reason for change
...

Note: This linter can be disabled with `set_option linter.style.maxHeartbeats false`
warning: Iut/Foundations/SourceFiniteEtaleSignTorsorAffineCoverAssembly.lean:4586:0: Please, add a comment explaining the need for modifying the maxHeartbeat limit, as in
set_option maxHeartbeats 400000 in
-- reason for change
...

Note: This linter can be disabled with `set_option linter.style.maxHeartbeats false`
warning: Iut/Foundations/SourceFiniteEtaleSignTorsorAffineCoverAssembly.lean:5027:0: Please, add a comment explaining the need for modifying the maxHeartbeat limit, as in
set_option maxHeartbeats 400000 in
-- reason for change
...

Note: This linter can be disabled with `set_option linter.style.maxHeartbeats false`
warning: Iut/Foundations/SourceFiniteEtaleSignTorsorAffineCoverAssembly.lean:5159:0: Please, add a comment explaining the need for modifying the maxHeartbeat limit, as in
set_option maxHeartbeats 400000 in
-- reason for change
...

Note: This linter can be disabled with `set_option linter.style.maxHeartbeats false`
warning: Iut/Foundations/SourceFiniteEtaleSignTorsorAffineCoverAssembly.lean:5333:0: Please, add a comment explaining the need for modifying the maxHeartbeat limit, as in
set_option maxHeartbeats 400000 in
-- reason for change
...

Note: This linter can be disabled with `set_option linter.style.maxHeartbeats false`
warning: Iut/Foundations/SourceFiniteEtaleSignTorsorAffineCoverAssembly.lean:5438:0: Please, add a comment explaining the need for modifying the maxHeartbeat limit, as in
set_option maxHeartbeats 1600000 in
-- reason for change
...

Note: This linter can be disabled with `set_option linter.style.maxHeartbeats false`
warning: Iut/Foundations/SourceFiniteEtaleSignTorsorAffineCoverAssembly.lean:5573:0: Please, add a comment explaining the need for modifying the maxHeartbeat limit, as in
set_option maxHeartbeats 400000 in
-- reason for change
...

Note: This linter can be disabled with `set_option linter.style.maxHeartbeats false`
warning: Iut/Foundations/SourceFiniteEtaleSignTorsorAffineCoverAssembly.lean:5687:0: Please, add a comment explaining the need for modifying the maxHeartbeat limit, as in
set_option maxHeartbeats 4000000 in
-- reason for change
...

Note: This linter can be disabled with `set_option linter.style.maxHeartbeats false`
warning: Iut/Foundations/SourceFiniteEtaleSignTorsorAffineCoverAssembly.lean:5764:0: Please, add a comment explaining the need for modifying the maxHeartbeat limit, as in
set_option maxHeartbeats 800000 in
-- reason for change
...

Note: This linter can be disabled with `set_option linter.style.maxHeartbeats false`
warning: Iut/Foundations/SourceFiniteEtaleSignTorsorAffineCoverAssembly.lean:5813:0: Please, add a comment explaining the need for modifying the maxHeartbeat limit, as in
set_option maxHeartbeats 1600000 in
-- reason for change
...

Note: This linter can be disabled with `set_option linter.style.maxHeartbeats false`
warning: Iut/Foundations/SourceFiniteEtaleSignTorsorAffineCoverAssembly.lean:5904:0: Please, add a comment explaining the need for modifying the maxHeartbeat limit, as in
set_option maxHeartbeats 800000 in
-- reason for change
...

Note: This linter can be disabled with `set_option linter.style.maxHeartbeats false`
warning: Iut/Foundations/SourceFiniteEtaleSignTorsorAffineCoverAssembly.lean:5965:0: Please, add a comment explaining the need for modifying the maxHeartbeat limit, as in
set_option maxHeartbeats 800000 in
-- reason for change
...

Note: This linter can be disabled with `set_option linter.style.maxHeartbeats false`
warning: Iut/Foundations/SourceFiniteEtaleSignTorsorAffineCoverAssembly.lean:6033:0: Please, add a comment explaining the need for modifying the maxHeartbeat limit, as in
set_option maxHeartbeats 800000 in
-- reason for change
...

Note: This linter can be disabled with `set_option linter.style.maxHeartbeats false`
warning: Iut/Foundations/SourceFiniteEtaleSignTorsorAffineCoverAssembly.lean:6088:0: Please, add a comment explaining the need for modifying the maxHeartbeat limit, as in
set_option maxHeartbeats 800000 in
-- reason for change
...

Note: This linter can be disabled with `set_option linter.style.maxHeartbeats false`
warning: Iut/Foundations/SourceFiniteEtaleSignTorsorAffineCoverAssembly.lean:6128:0: Please, add a comment explaining the need for modifying the maxHeartbeat limit, as in
set_option maxHeartbeats 800000 in
-- reason for change
...

Note: This linter can be disabled with `set_option linter.style.maxHeartbeats false`
warning: Iut/Foundations/SourceFiniteEtaleSignTorsorAffineCoverAssembly.lean:6211:0: Please, add a comment explaining the need for modifying the maxHeartbeat limit, as in
set_option maxHeartbeats 800000 in
-- reason for change
...

Note: This linter can be disabled with `set_option linter.style.maxHeartbeats false`
warning: Iut/Foundations/SourceFiniteEtaleSignTorsorAffineCoverAssembly.lean:6460:100: This line exceeds the 100 character limit, please shorten it!

Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Foundations/SourceFiniteEtaleSignTorsorAffineCoverAssembly.lean:6815:0: Please, add a comment explaining the need for modifying the maxHeartbeat limit, as in
set_option maxHeartbeats 800000 in
-- reason for change
...

Note: This linter can be disabled with `set_option linter.style.maxHeartbeats false`
✔ [4646/6599] Built Iut.Foundations.SourceFiniteEtaleSignQuotientAtlasBaseChange (16s)
✔ [4647/6599] Built Iut.Foundations.SourceEtalePseudofunctorTwoPullbackCancellationLiftToYHomToY (2.7s)
✔ [4650/6599] Built Iut.Foundations.SourceEtaleStackRepresentableLocalIsoDescent (3.8s)
✔ [4651/6599] Built Iut.Foundations.SourceEtaleStackSchemeAtlasOverlapMultiplication (3.1s)
✔ [4652/6599] Built Iut.Foundations.SourceEtalePseudofunctorRepresentablePullbackAlongStrongTrans (3.8s)
✔ [4653/6599] Built Iut.Foundations.SourceFiniteEtaleSchemeCoverAffineGroupQuotient (3.1s)
✔ [4654/6599] Built Iut.Foundations.SourceFiniteEtaleSchemeCoverBalanced (2.5s)
✔ [4655/6599] Built Iut.Foundations.SourceFiniteEtaleSignTorsorAffineCoverRestriction (124s)
✔ [4656/6599] Built Iut.Foundations.SourceFiniteEtaleSignQuotientAtlasLiftApp (121s)
✔ [4657/6599] Built Iut.Foundations.SourceFiniteEtaleSignQuotientAtlasInvariant (3.5s)
✔ [4658/6599] Built Iut.Foundations.SourceEtalePseudofunctorTwoPullbackCancellationLiftCompatibility (2.7s)
✔ [4660/6600] Built Iut.Foundations.SourceEtaleStackRepresentableAtlasLocalIsoDescent (3.1s)
✔ [4661/6600] Built Iut.Foundations.SourceOrbicurveFiniteEtaleBaseChangeSchemeCoverMapReflectsLocalIso (3.3s)
✔ [4662/6602] Built Iut.Foundations.SourceEtaleStackSchemeAtlasOverlapMultiplicationRepresentedLongConeIso (2.9s)
✔ [4663/6602] Built Iut.Foundations.SourceEtaleStackSchemeAtlasOverlapConePasting (2.0s)
✔ [4664/6602] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapCechData (3.1s)
✔ [4665/6602] Built Iut.Foundations.SourceEtaleStackSchemeAtlasFiniteEtaleDescent (3.3s)
✔ [4666/6602] Built Iut.Foundations.SourceOrbicurveFiniteEtaleIteratedBaseChange (9.5s)
✔ [4667/6602] Built Iut.Foundations.SourceFiniteEtaleSchemeCoverAffineOverFullyFaithful (2.7s)
✔ [4668/6602] Built Iut.Foundations.SourceFiniteEtaleFixedSubalgebra (3.1s)
✔ [4669/6602] Built Iut.Foundations.SourceFiniteEtaleSignTorsorAffineCoverFiniteEffectivity (3.6s)
✔ [4670/6602] Built Iut.Foundations.SourceFiniteEtaleSignQuotientAtlasLiftNaturality (104s)
✔ [4671/6602] Built Iut.Foundations.SourceFiniteEtaleSignQuotientAtlasInvariantElement (3.1s)
✔ [4672/6604] Built Iut.Foundations.SourceEtalePseudofunctorTwoPullbackCancellationConeMorphismCompatibility (3.0s)
✔ [4676/6604] Built Iut.Foundations.SourceEtaleStackSchemeAtlasOverlapConePastingIso (4.1s)
✔ [4677/6604] Built Iut.Foundations.SourceEtaleStackSchemeAtlasOverlapConePastingCell (2.9s)
✔ [4678/6604] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapRestrictionCongrIsoNaturality (3.1s)
✔ [4679/6604] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapRestrictionCongrIsoWhiskerRightFactorization (3.0s)
✔ [4680/6604] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapOverlapNestedMiddleIso (2.8s)
✔ [4681/6604] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapPointObject (2.8s)
✔ [4682/6604] Built Iut.Foundations.SourceEtaleStackSchemeAtlasFiniteEtaleDescentComparison (3.2s)
✔ [4683/6604] Built Iut.Foundations.SourceEtaleStackSchemeAtlasMapCechEndpointIsos (2.9s)
✔ [4684/6604] Built Iut.Foundations.SourceEtaleStackSchemeAtlasBaseChangePointIso (3.0s)
✔ [4685/6604] Built Iut.Foundations.SourceOrbicurveFiniteEtaleIteratedBaseChangeForwardBackLiftedHom (3.3s)
✔ [4686/6604] Built Iut.Foundations.SourceEtaleStackSchemeAtlasOverlapMapIso (2.7s)
✔ [4687/6604] Built Iut.Foundations.SourceOrbicurveFiniteEtaleIteratedBaseChangeToSourceIso (2.0s)
✔ [4688/6604] Built Iut.Foundations.SourceFiniteEtaleFixedAffineQuotient (3.1s)
✔ [4689/6604] Built Iut.Foundations.SourceFiniteEtaleSignTorsorAffineRefinement (3.6s)
✔ [4690/6604] Built Iut.Foundations.SourceFiniteEtaleSignQuotientAtlasLift (3.1s)
✔ [4691/6604] Built Iut.Foundations.SourceFiniteEtaleSignQuotientAtlasInvariantComponent (25s)
✔ [4692/6605] Built Iut.Foundations.SourceEtalePseudofunctorTwoPullbackCancellationConeMorphism (3.4s)
✔ [4695/6605] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapOverlapNestedMiddleHom (2.9s)
✔ [4696/6605] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapOverlapNestedEndpointIsos (2.7s)
✔ [4697/6605] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapPointOverlap (3.1s)
✔ [4698/6605] Built Iut.Foundations.SourceEtaleStackSchemeAtlasFiniteEtaleDescentConstruction (42s)
✔ [4699/6605] Built Iut.Foundations.SourceEtaleStackSchemeAtlasMapCechPairMiddleIso (3.1s)
✔ [4700/6605] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalHomPointIsoValue (3.1s)
✔ [4701/6605] Built Iut.Foundations.SourceOrbicurveFiniteEtaleIteratedBaseChangeForwardBackLiftedHomComparison (2.9s)
✔ [4702/6605] Built Iut.Foundations.SourceFiniteEtaleOrbitConstantAlgebra (2.0s)
✔ [4703/6605] Built Iut.Foundations.SourceFiniteEtaleSignQuotientStackRefinement (2.0s)
✔ [4704/6605] Built Iut.Foundations.SourceFiniteEtaleSignQuotientAtlasLiftProjections (12s)
✔ [4705/6605] Built Iut.Foundations.SourceFiniteEtaleSignQuotientAtlasInvariantCocycle (19s)
✔ [4706/6607] Built Iut.Foundations.SourceEtalePseudofunctorTwoPullbackCancellationTwoCell (2.5s)
✔ [4709/6607] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapOverlapNestedMiddleCompositeFactorization (3.1s)
✔ [4710/6607] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapPullbackOverlapNestedFactorization (3.4s)
✔ [4711/6607] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapPointTransition (3.3s)
✔ [4712/6607] Built Iut.Foundations.SourceOrbicurveFiniteEtaleBaseChangePointIsoToSourceIso (2.7s)
✔ [4713/6607] Built Iut.Foundations.SourceEtaleStackSchemeAtlasFiniteEtaleDescentCoherence (13s)
✔ [4714/6607] Built Iut.Foundations.SourceEtaleStackSchemeAtlasMapCechPairFactorization (22s)
✔ [4715/6607] Built Iut.Foundations.SourceOrbicurveFiniteEtaleIteratedBaseChangeForwardBackStrongTransToSource (2.0s)
✔ [4716/6607] Built Iut.Foundations.SourceFiniteEtaleSplitAlgebraHom (3.1s)
✔ [4717/6607] Built Iut.Foundations.SourceFiniteEtaleSignQuotientAffineChartDescent (16s)
✔ [4718/6607] Built Iut.Foundations.SourceFiniteEtaleSignQuotientAtlasLiftTwoCell (287s)
✔ [4719/6607] Built Iut.Foundations.SourceFiniteEtaleSignQuotientAtlasLiftUnit (15s)
✔ [4720/6609] Built Iut.Foundations.SourceEtalePseudofunctorTwoPullbackCancellationTwoCellToX (2.6s)
✔ [4722/6609] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapOverlapNestedMiddleCompositeTargetCollapse (3.1s)
✔ [4723/6609] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapOverlapNestedMiddleCompositeSourceCollapse (2.0s)
✔ [4724/6609] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapOverlapNestedSpecializations (3.1s)
✔ [4725/6609] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapOverlapCompositeWhiskeredExpansion (3.0s)
✔ [4726/6609] Built Iut.Foundations.SourceEtaleRepresentedRestrictionPointIsoCongruenceTail (3.0s)
✔ [4727/6609] Built Iut.Foundations.SourceEtaleRepresentedStrongTransPointIsoWhiskerRightHom (2.9s)
✔ [4728/6609] Built Iut.Foundations.SourceEtaleRepresentedStrongTransPointIsoWhiskerLeft (3.8s)
✔ [4729/6609] Built Iut.Foundations.SourceEtaleRepresentedStrongTransPointIsoSymmHom (2.8s)
✔ [4730/6609] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapPointOverlapValueIsoRepresented (2.9s)
✔ [4731/6609] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapPointCocycleGeometry (3.2s)
✔ [4732/6609] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapCechCocyclePointValue (2.9s)
✔ [4733/6609] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapRestrictionCompositePointIsoHom (6.8s)
⚠ [4734/6609] Built Iut.Foundations.SourceEtaleRepresentedStrongTransPointIsoTransHom (2.0s)
warning: Iut/Foundations/SourceEtaleRepresentedStrongTransPointIsoTransHom.lean:26:0: Please, add a comment explaining the need for modifying the maxHeartbeat limit, as in
set_option maxHeartbeats 800000 in
-- reason for change
...

Note: This linter can be disabled with `set_option linter.style.maxHeartbeats false`
✔ [4735/6609] Built Iut.Foundations.SourceOrbicurveFiniteEtaleBaseChangePointIsoToSourceCompatibility (3.1s)
✔ [4736/6609] Built Iut.Foundations.SourceEtaleRepresentedStrongTransPointIsoCongruenceAssociator (3.1s)
✔ [4737/6609] Built Iut.Foundations.SourceEtaleStackSchemeAtlasFiniteEtaleCoverOverlapComparisonLeft (2.9s)
✔ [4738/6609] Built Iut.Foundations.SourceEtaleStackSchemeAtlasFiniteEtaleCanonicalDescentStructureComparison (2.9s)
✔ [4739/6609] Built Iut.Foundations.SourceEtaleStackSchemeAtlasMapCechPairLongFactorization (3.1s)
✔ [4740/6609] Built Iut.Foundations.SourceOrbicurveFiniteEtaleIteratedBaseChangeForwardBackRealizationToSourceExpansion (3.1s)
✔ [4741/6609] Built Iut.Foundations.SourceFiniteEtaleSplitAlgebraAutomorphism (2.7s)
✔ [4742/6609] Built Iut.Foundations.SourceFiniteEtaleSignQuotientAffineChartGluing (8.4s)
✔ [4743/6609] Built Iut.Foundations.SourceFiniteEtaleSignQuotientAtlasLiftCompatibility (18s)
✔ [4744/6610] Built Iut.Foundations.SourceEtalePseudofunctorTwoPullbackCancellationTwoCellYTarget (2.5s)
✔ [4747/6610] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapOverlapNestedMiddleTargetAssociatorNaturality (2.9s)
✔ [4748/6610] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapOverlapNestedMiddleDirectTargetNaturalityEndpoints (2.8s)
✔ [4749/6610] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapOverlapNestedMiddleAttached (3.0s)
✔ [4750/6610] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapOverlapCompositeWhiskeredEndpointIsos (2.9s)
⚠ [4751/6620] Built Iut.Foundations.SourceEtaleRepresentedStrongTransPointIsoWhiskerLeftTargetTransport (2.9s)
warning: Iut/Foundations/SourceEtaleRepresentedStrongTransPointIsoWhiskerLeftTargetTransport.lean:44:13: This simp argument is unused:
  Category.assoc

Hint: Omit it from the simp argument list.
  simp only [C̵a̵t̵e̵g̵o̵r̵y̵.̵a̵s̵s̵o̵c̵,̵ ̵Iso.inv_hom_id_assoc]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Iut/Foundations/SourceEtaleRepresentedStrongTransPointIsoWhiskerLeftTargetTransport.lean:26:0: Please, add a comment explaining the need for modifying the maxHeartbeat limit, as in
set_option maxHeartbeats 800000 in
-- reason for change
...

Note: This linter can be disabled with `set_option linter.style.maxHeartbeats false`
✔ [4752/6635] Built Iut.Foundations.SourceEtaleRepresentedStrongTransPointIsoWhiskerLeftInv (2.0s)
✔ [4753/6635] Built Iut.Foundations.SourceEtaleRepresentedStrongTransPointIsoWhiskerLeftSourceTransport (2.0s)
✔ [4754/6635] Built Iut.Foundations.SourceEtaleRepresentedStrongTransPointIsoSymmInv (2.9s)
✔ [4755/6635] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapPointTripleRawCompositorTailHom (2.9s)
✔ [4756/6635] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapPointTripleBaseInverseTail (3.0s)
✔ [4757/6635] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapPointLongEdgeEndpoints (3.5s)
✔ [4758/6635] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapCechCocyclePointTripleValue (3.0s)
✔ [4759/6635] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapPointOverlapValueDirectFactorData (2.9s)
⚠ [4760/6635] Built Iut.Foundations.SourceEtaleRepresentedStrongTransPointIsoTransInv (2.9s)
warning: Iut/Foundations/SourceEtaleRepresentedStrongTransPointIsoTransInv.lean:26:0: Please, add a comment explaining the need for modifying the maxHeartbeat limit, as in
set_option maxHeartbeats 800000 in
-- reason for change
...

Note: This linter can be disabled with `set_option linter.style.maxHeartbeats false`
✔ [4761/6635] Built Iut.Foundations.SourceEtaleRepresentedStrongTransPointIsoPentagonHom (3.0s)
✔ [4762/6635] Built Iut.Foundations.SourceEtaleRepresentedStrongTransPointIsoWhiskerRightTransHom (3.0s)
✔ [4763/6635] Built Iut.Foundations.SourceEtaleRepresentedStrongTransPointIsoAssociatorEqToHom (2.9s)
✔ [4764/6635] Built Iut.Foundations.SourceEtaleRepresentedStrongTransPointIsoCongruenceSymmInvAssociator (3.1s)
✔ [4765/6635] Built Iut.Foundations.SourceEtaleStackSchemeAtlasSourceAtlasOverlapCanonicalComparisonLeftFactorIso (2.9s)
✔ [4766/6635] Built Iut.Foundations.SourceEtaleStackSchemeAtlasFiniteEtaleCanonicalDescentStructureComparisonLeft (2.9s)
✔ [4767/6635] Built Iut.Foundations.SourceEtaleStackSchemeAtlasMapCechCompositeFactorization (12s)
✔ [4768/6635] Built Iut.Foundations.SourceOrbicurveFiniteEtaleIteratedBaseChangeForwardBackToSourceExpansion (3.0s)
✔ [4769/6635] Built Iut.Foundations.SourceFiniteEtaleSplitActionFixedAlgebra (4.0s)
✔ [4770/6635] Built Iut.Foundations.SourceFiniteEtaleSignQuotientAffineChartRelativeGluing (3.7s)
✔ [4771/6635] Built Iut.Foundations.SourceFiniteEtaleSignQuotientAtlasLiftWitness (18s)
✔ [4772/6750] Built Iut.Foundations.SourceEtalePseudofunctorTwoPullbackCancellationLiftToYInvToY (2.7s)
✔ [4775/6750] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapOverlapNestedMiddleDirectTargetNaturalityEndpointExpansions (2.9s)
✔ [4776/6750] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapOverlapNestedMiddleDirectTargetNaturalityMiddleRight (2.0s)
✔ [4777/6750] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapOverlapPairWhiskeredExpansion (3.1s)
✔ [4778/6750] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapOverlapCompositeWhiskeredEndpointFactorization (2.0s)
✔ [4779/6750] Built Iut.Foundations.SourceEtaleRepresentedStrongTransPointIsoWhiskerLeftTargetTransportData (2.9s)
✔ [4781/6750] Built Iut.Foundations.SourceFiniteEtaleSchemeCoverGeometricFiberFunctor (2.8s)
✔ [4782/6750] Built Iut.Foundations.SourceSpecFieldSchemeCoproductMaps (2.4s)
✔ [4783/6750] Built Iut.Foundations.SourceFiniteEtaleInvariantAlgHomOrbit (2.6s)
✔ [4784/6750] Built Iut.Foundations.SourceSingleObjTypesOrbitColimit (1.7s)
✔ [4785/6750] Built Iut.Foundations.SourceEtaleRepresentedStrongTransPointIsoWhiskerLeftSymmHom (2.9s)
⚠ [4786/6750] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapPointTripleRepresentedSourceObjects (3.3s)
warning: Iut/Foundations/SourceEtaleStackSchemeAtlasLocalMapPointTripleRepresentedSourceObjects.lean:27:0: Please, add a comment explaining the need for modifying the maxHeartbeat limit, as in
set_option maxHeartbeats 800000 in
-- reason for change
...

Note: This linter can be disabled with `set_option linter.style.maxHeartbeats false`
warning: Iut/Foundations/SourceEtaleStackSchemeAtlasLocalMapPointTripleRepresentedSourceObjects.lean:59:0: Please, add a comment explaining the need for modifying the maxHeartbeat limit, as in
set_option maxHeartbeats 800000 in
-- reason for change
...

Note: This linter can be disabled with `set_option linter.style.maxHeartbeats false`
✔ [4787/6750] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapPointTripleBaseInverseTailLeftHom (3.2s)
✔ [4788/6750] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapPointTripleCocycleMiddleValueIsos (3.0s)
✔ [4789/6750] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapPointTripleEdgeIso (3.2s)
✔ [4790/6750] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapPointTripleCocycleEndpointValueIso (3.0s)
⚠ [4791/6750] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapPointOverlapValueDirectFactorDataEndpoints (3.0s)
warning: Iut/Foundations/SourceEtaleStackSchemeAtlasLocalMapPointOverlapValueDirectFactorDataEndpoints.lean:27:0: Please, add a comment explaining the need for modifying the maxHeartbeat limit, as in
set_option maxHeartbeats 800000 in
-- reason for change
...

Note: This linter can be disabled with `set_option linter.style.maxHeartbeats false`
warning: Iut/Foundations/SourceEtaleStackSchemeAtlasLocalMapPointOverlapValueDirectFactorDataEndpoints.lean:45:0: Please, add a comment explaining the need for modifying the maxHeartbeat limit, as in
set_option maxHeartbeats 800000 in
-- reason for change
...

Note: This linter can be disabled with `set_option linter.style.maxHeartbeats false`
✔ [4792/6750] Built Iut.Foundations.SourceEtaleRepresentedStrongTransPointIsoWhiskerLeftTransInv (2.9s)
✔ [4793/6750] Built Iut.Foundations.SourceEtaleRepresentedStrongTransPointIsoWhiskerRightTransInv (3.1s)
✔ [4794/6750] Built Iut.Foundations.SourceEtaleRepresentedStrongTransPointIsoPentagonInv (3.0s)
✔ [4795/6750] Built Iut.Foundations.SourceEtaleRepresentedStrongTransPointIsoAssociatorNaturalityLeft (2.0s)
✔ [4796/6750] Built Iut.Foundations.SourceEtaleRepresentedStrongTransPointIsoAssociatorNaturalityMiddle (2.0s)
✔ [4797/6750] Built Iut.Foundations.SourceEtaleRepresentedStrongTransPointIsoAssociatorInvEqToHom (3.0s)
✔ [4798/6849] Built Iut.Foundations.SourceEtaleRepresentedStrongTransPointIsoCongruenceSymmInvAssociatorRestrictionTail (3.1s)
✔ [4799/8799] Built Iut.Foundations.SourceEtaleStackSchemeAtlasSourceAtlasOverlapCanonicalComparisonLeftExpandedIso (2.8s)
✔ [4800/8799] Built Iut.Foundations.SourceEtaleStackSchemeAtlasMapCechConeEndpointIsos (2.9s)
✔ [4801/8799] Built Iut.Foundations.SourceFiniteEtaleFixedSubalgebraBaseChange (3.2s)
✔ [4802/8799] Built Iut.Foundations.SourceFiniteEtaleSignQuotientAffineChartIdentityCoherence (539s)
✔ [4803/8799] Built Iut.Foundations.SourceFiniteEtaleSignQuotientAffineChartEffectivity (2.9s)
✔ [4804/8799] Built Iut.Foundations.SourceFiniteEtaleSignQuotientOrbicurve (196s)
✔ [4805/8799] Built Iut.Foundations.SourceEtalePseudofunctorTwoPullbackCancellationNestedWhisker (2.8s)
✔ [4807/8799] Built Iut.Foundations.SourceFiniteEtaleSchemeCoverRepresentable (3.8s)
✔ [4808/8799] Built Iut.Foundations.SourceSchemeEtaleStackPresentationFiniteEtaleCoverFunctor (2.9s)
✔ [4809/8799] Built Iut.Foundations.SourceEtalePseudofunctorContractiblePullback (3.6s)
✔ [4810/8799] Built Iut.Foundations.SourcePreGaloisCategoryEquivalenceTransport (1.9s)
✔ [4811/8799] Built Iut.Foundations.SourcePuncturedWeierstrassSchemeBaseChange (4.4s)
✔ [4812/8799] Built Iut.Foundations.SourceChosenPullbackFunctoriality (1.9s)
✔ [4813/8799] Built Iut.Foundations.SourceSchemeOverFieldRestrictScalarsEtaleSite (2.7s)
✔ [4814/8799] Built Iut.Foundations.SourceOrbicurveEtaleFundamentalGroupTransport (3.0s)
✔ [4815/8799] Built Iut.Foundations.SourceFiniteEtaleSchemeCoverSliceEquivalence (3.0s)
✔ [4816/8799] Built Iut.Foundations.SourceEquivalenceMateNaturality (1.6s)
✔ [4817/8799] Built Iut.Foundations.SourcePseudofunctorStrongTransIsoOfComponents (3.2s)
✔ [4818/8799] Built Iut.Foundations.SourceAnabelioidEquivalence (3.1s)
✔ [4819/8799] Built Iut.Foundations.SourceAnabelioidDominatingPullbackInjectivity (2.9s)
✔ [4820/8799] Built Iut.Foundations.SourceCategoryIsoConjugationInverseCancellation (1.4s)
✔ [4821/8799] Built Iut.Foundations.SourceFiniteEtalePresentedQuotientBaseChange (1.8s)
✔ [4822/8991] Built Iut.Foundations.SourceIdealQuotientEquivComparison (1.8s)
✔ [4823/8991] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapOverlapPairWhiskeredNested (3.0s)
✔ [4824/8991] Built Iut.Foundations.SourceEtaleRepresentedStrongTransPointIsoWhiskerLeftTargetTransportRightData (2.8s)
✔ [4826/8991] Built Iut.Foundations.SourceFiniteEtaleSchemeCoverGeometricFiberPullbacks (2.6s)
✔ [4827/8991] Built Iut.Foundations.SourceEtaleRepresentedStrongTransPointIsoWhiskerLeftSymmInv (3.0s)
⚠ [4828/8991] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapPointTripleNaturalityAppTransportData (2.8s)
warning: Iut/Foundations/SourceEtaleStackSchemeAtlasLocalMapPointTripleNaturalityAppTransportData.lean:28:0: Please, add a comment explaining the need for modifying the maxHeartbeat limit, as in
set_option maxHeartbeats 800000 in
-- reason for change
...

Note: This linter can be disabled with `set_option linter.style.maxHeartbeats false`
✔ [4829/8991] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapPointTripleRepresentedSourceCompositor (3.0s)
⚠ [4830/8991] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapPointTripleRepresentedSourceCell (3.4s)
warning: Iut/Foundations/SourceEtaleStackSchemeAtlasLocalMapPointTripleRepresentedSourceCell.lean:27:0: Please, add a comment explaining the need for modifying the maxHeartbeat limit, as in
set_option maxHeartbeats 800000 in
-- reason for change
...

Note: This linter can be disabled with `set_option linter.style.maxHeartbeats false`
✔ [4831/8991] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapPointTripleBaseInverseTailLeftHomProjection (3.2s)
✔ [4832/8991] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapPointTripleCocycleBaseInverseTerminalHom (3.0s)
✔ [4833/8991] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapPointTripleCocycleNormalizedAtlasMiddleHom (2.9s)
✔ [4834/8991] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapPointTripleEdgeConeIso (3.0s)
⚠ [4835/8991] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapPointTripleCocycleToTwoValueIsoHom (3.1s)
warning: Iut/Foundations/SourceEtaleStackSchemeAtlasLocalMapPointTripleCocycleToTwoValueIsoHom.lean:27:0: Please, add a comment explaining the need for modifying the maxHeartbeat limit, as in
set_option maxHeartbeats 800000 in
-- reason for change
...

Note: This linter can be disabled with `set_option linter.style.maxHeartbeats false`
✔ [4836/8991] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapPointTripleOverlapCompositeTargetToCocycleHom (2.9s)
✔ [4837/8991] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapPointTripleCocycleToZeroValueIsoHom (3.2s)
✔ [4838/8991] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapPointOverlapValueDirectMiddleFactor (3.1s)
✔ [4839/8991] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapPointTripleOverlapValueDirectFactorDataMapped (2.9s)
✔ [4840/8991] Built Iut.Foundations.SourceEtaleRepresentedStrongTransPointIsoWhiskerRightSymmInv (2.9s)
✔ [4841/8991] Built Iut.Foundations.SourceEtaleRepresentedStrongTransPointIsoAssociatorNaturalityMiddleInverseSolve (2.9s)
✔ [4842/8991] Built Iut.Foundations.SourceEtaleRepresentedStrongTransPointIsoAssociatorNaturalityMiddleInv (2.0s)
✔ [4843/8991] Built Iut.Foundations.SourceEtaleRepresentedStrongTransPointIsoAssociatorInvAbsorbPointTransport (2.9s)
✔ [4845/8991] Built Iut.Foundations.SourceFiniteEtaleClopenIdempotentQuotient (2.0s)
✔ [4846/8991] Built Iut.Foundations.SourceTensorProductScalarTowerQuotient (1.8s)
✔ [4847/8991] Built Iut.Foundations.SourceFiniteEtaleAffinePullbackActionTensor (7.4s)
✔ [4848/8991] Built Iut.Foundations.SourceFiniteEtaleSchemeCoverBaseChangeFiniteLimits (2.9s)
✔ [4849/8991] Built Iut.Foundations.SourceFiniteEtaleSchemeCoverBaseChangeBinaryCoproducts (13s)
✔ [4850/8991] Built Iut.Foundations.SourceInvolutiveEndofunctorEquivariantObject (3.1s)
✔ [4851/8991] Built Iut.Foundations.SourceFiniteEtaleSchemeCoverMonoCharacteristicIdempotent (2.8s)
✔ [4852/8991] Built Iut.Foundations.SourceRingEquivConjugationData (1.4s)
✔ [4853/8991] Built Iut.Foundations.SourceInvariantIdealQuotientInvolution (1.7s)
✔ [4854/8991] Built Iut.Foundations.SourceAffineScalarExtensionReversedTensorNaturality (15s)
✔ [4855/8991] Built Iut.Foundations.SourceTensorProductRightAlgEquiv (1.7s)
✔ [4856/8991] Built Iut.Foundations.SourceTensorProductTmulMulInclusions (1.8s)
✔ [4857/8991] Built Iut.Foundations.SourceRingHomRangeActionMul (1.6s)
✔ [4858/8991] Built Iut.Foundations.SourceRingHomRangeEquiv (1.6s)
✔ [4859/8991] Built Iut.Foundations.SourceRingEquivApplyHEqOfCarrierEq (1.4s)
✔ [4860/8991] Built Iut.Foundations.SourceEquivTransportApplyBack (762ms)
✔ [4861/8991] Built Iut.Foundations.SourceTensorProductSpecHomExt (2.3s)
✔ [4862/8991] Built Iut.Foundations.SourceCategoryFourfoldReassociation (1.4s)
✔ [4863/8991] Built Iut.Foundations.SourceFiniteEtaleSchemeCoverIdentitySectionLift (3.0s)
✔ [4864/8991] Built Iut.Foundations.SourceMorphismPropertyOverPullbackCompProjection (1.9s)
✔ [4865/8991] Built Iut.Foundations.SourceEtaleStackSchemeAtlasFiniteEtalePreDescentNormalizedMultiplicationHom (3.1s)
✔ [4866/8991] Built Iut.Foundations.SourceCategoryIsoConjugationCancel (2.7s)
✔ [4867/8991] Built Iut.Foundations.SourceFiniteEtaleSignQuotientAtlasFirstSheetProjection (2.9s)
✔ [4868/8991] Built Iut.Foundations.SourceFiniteEtaleSignQuotientAtlasConeLiftReassociation (3.1s)
✔ [4869/8991] Built Iut.Foundations.SourceFiniteEtaleSignQuotientAtlasTotalSpaceNormalization (14s)
✔ [4870/8991] Built Iut.Foundations.SourceEtalePseudofunctorConeReplaceCommutesHom (2.8s)
✔ [4871/8991] Built Iut.Foundations.SourceFiniteEtaleSignQuotientAtlasInversionIsoFirstSheetTotalSpace (4.1s)
✔ [4872/8991] Built Iut.Foundations.SourceEtalePseudofunctorInvolutionConePasting (3.1s)
✔ [4873/8991] Built Iut.Foundations.SourceCategoryIsoFactorCancellation (2.6s)
✔ [4874/8991] Built Iut.Foundations.SourceCategoryThreeCompatibilityPasting (1.5s)
✔ [4875/8991] Built Iut.Foundations.SourceEtaleStackSchemeAtlasTripleOverlapLongConeCells (2.0s)
✔ [4876/8991] Built Iut.Foundations.SourceCategoryEqualityPostcompositionIdentity (1.4s)
✔ [4877/8991] Built Iut.Foundations.SourceFiniteEtaleSchemeCoverPullbackMorphismDetection (3.3s)
✔ [4878/8991] Built Iut.Foundations.SourceFiniteEtaleSignQuotientEquivariantMap (5.6s)
✔ [4879/8991] Built Iut.Foundations.SourceCategoryTheoryColimMapFunctoriality (1.5s)
✔ [4880/8991] Built Iut.Foundations.SourceFiniteEtaleSchemeCoverStrictEpiUnderlyingScheme (2.8s)
✔ [4881/8991] Built Iut.Foundations.SourceEtaleStackSchemeAtlasFiniteEtaleDescentNormalizedNaturality (34s)
✔ [4882/8991] Built Iut.Foundations.SourceSignSwapActionCoproductQuotient (3.8s)
✔ [4883/8991] Built Iut.Foundations.SourceFiniteEtaleSignTorsorProjectionEffectiveEpi (2.0s)
✔ [4884/8991] Built Iut.Foundations.SourceFiniteEtaleSignTorsorEquivariantMapIso (4.5s)
✔ [4885/8991] Built Iut.Foundations.SourceFiniteEtaleSignQuotientTrivialAtlasIdentityPoint (2.8s)
✔ [4886/8991] Built Iut.Foundations.SourceCategoryMiddleIdentityConjugation (2.7s)
✔ [4887/8991] Built Iut.Foundations.SourceFiniteEtaleSignQuotientAssociatedStackCoverConeLiftCompatibilityRightContext (1.5s)
✔ [4888/8991] Built Iut.Foundations.SourceCategoryThreeLegPasting (1.4s)
✔ [4889/8991] Built Iut.Foundations.SourceCategoryFunctorOfObjMap (1.4s)
✔ [4890/8991] Built Iut.Foundations.SourceCategoryThreeProjectionPastingCore (1.6s)
✔ [4891/8991] Built Iut.Foundations.SourceCategoryFactorizedMiddlePasting (1.4s)
✔ [4892/8991] Built Iut.Foundations.SourceCategoryThreeLegQuotientPasting (1.5s)
✔ [4893/8991] Built Iut.Foundations.SourceCategoryFiveLegPasting (1.5s)
✔ [4894/8991] Built Iut.Foundations.SourceFiniteEtaleSignQuotientReindexHomExt (3.5s)
✔ [4895/8991] Built Iut.Foundations.SourceFiniteEtaleSignQuotientAssociatedStackCoverConeLiftToTestPasting (1.4s)
✔ [4896/8991] Built Iut.Foundations.SourceEqualityProofPackage (340ms)
✔ [4897/8991] Built Iut.Foundations.SourceCategoryReplaceRightmostFactor (1.4s)
✔ [4898/8991] Built Iut.Foundations.SourceCategoryReplaceTwoRightFactors (1.4s)
✔ [4899/8991] Built Iut.Foundations.SourceCategoryPrefixFactorPasting (1.4s)
✔ [4900/8991] Built Iut.Foundations.SourceCategoryTwoCompatibilityPasting (1.4s)
✔ [4901/8991] Built Iut.Foundations.SourceCategoryCongrThreeFactors (1.4s)
✔ [4902/8991] Built Iut.Foundations.SourceCategoryPackedHEqEndpointLinkDataDependentCongrArg (1.4s)
✔ [4903/8991] Built Iut.Foundations.SourceCategoryThreeMorphismBridgePasting (1.7s)
✔ [4904/8991] Built Iut.Foundations.SourceCategoryTwoMorphismHEqPastingData (1.5s)
✔ [4905/8991] Built Iut.Foundations.SourceOrbicurveFiniteEtaleIteratedBaseChangeReverseFst (3.0s)
✔ [4906/8991] Built Iut.Foundations.SourceFiniteEtaleSignQuotientPointIdentityReconstructionTotalNaturality (4.3s)
✔ [4907/8991] Built Iut.Foundations.SourceEtalePseudofunctorYonedaRecoveryModificationNaturality (5.0s)
✔ [4908/8991] Built Iut.Foundations.SourceCategoryHEqEndpointProjections (1.3s)
✔ [4909/8991] Built Iut.Foundations.SourceEtaleStackSchemeAtlasFiniteEtaleDescentComparisonConverse (2.8s)
✔ [4910/8991] Built Iut.Foundations.SourceFinitaryExtensiveComplementComparison (1.9s)
✔ [4911/8991] Built Iut.Foundations.SourceFiniteEtaleSchemeCoverBaseChangeIso (3.4s)
✔ [4912/8991] Built Iut.Foundations.SourceGaloisFiberFunctorFiniteColimits (2.9s)
✔ [4913/8991] Built Iut.Foundations.SourceConnectedFiniteEtaleConverse (4.7s)
✔ [4914/8991] Built Iut.Foundations.SourceContinuousActionRestrictionSurjectivity (4.1s)
✔ [4915/8991] Built Iut.Foundations.SourceMorphismPropertyOverPullbackCongrProjection (1.6s)
✔ [4916/8991] Built Iut.Foundations.SourceFiniteAlgebraSeparableClosureFactorization (2.7s)
✔ [4917/8991] Built Iut.Foundations.SourceProfiniteKernelLift (2.8s)
✔ [4918/8991] Built Iut.Foundations.SourceSelectedFiberSurjectiveMapData (339ms)
✔ [4919/8991] Built Iut.Foundations.SourcePullbackSelectedSectionAction (1.6s)
✔ [4920/8991] Built Iut.Foundations.SourceCategoryTheoryEqToIsoFintypeComponentHEq (1.5s)
✔ [4921/8991] Built Iut.Foundations.SourceCategoryTheoryDetachedNaturalityPastingMaps (1.4s)
✔ [4922/8991] Built Iut.Foundations.SourceProfiniteClosedSubgroupOpenExtension (2.0s)
✔ [4923/8991] Built Iut.Foundations.SourcePretransitiveContinuousActionCoset (3.5s)
✔ [4924/8991] Built Iut.Foundations.SourcePointedAnabelioidFiberEquivariance (2.8s)
✔ [4925/8991] Built Iut.Foundations.SourceSpecRingHomSemiconjugacy (2.2s)
✔ [4926/8991] Built Iut.Foundations.SourceCategoryTheoryIsoRightFactorInvOfHomEq (1.4s)
✔ [4927/8991] Built Iut.Foundations.SourceFintypeCatFunctorMapCompApply (1.5s)
✔ [4928/8991] Built Iut.Foundations.SourceCategoryPackedTwoProjectionPasting (1.4s)
✔ [4929/8991] Built Iut.Foundations.SourceCategoryHEqPrecomposition (1.4s)
✔ [4930/8991] Built Iut.Foundations.SourceCategoryTheoryEquivalenceInverseObjectIsoCounit (1.4s)
✔ [4931/8991] Built Iut.Foundations.SourceCategoryTwoMorphismEquationDataOfCompositeEq (1.4s)
✔ [4932/8991] Built Iut.Foundations.SourceHEqTransExplicit (1.3s)
✔ [4933/8991] Built Iut.Foundations.SourceCategoryPackedHEqEndpointLinkDataCommonRightComparisonData (1.3s)
✔ [4934/8991] Built Iut.Foundations.SourceFunctionPointwiseFactorizationData (351ms)
✔ [4935/8991] Built Iut.Foundations.SourceFintypeFunctorFactorizationApply (1.6s)
✔ [4936/8991] Built Iut.Foundations.SourceFunctionHEqCastMapData (329ms)
✔ [4937/8991] Built Iut.Foundations.SourceFunctionPointwiseEqualityData (365ms)
✔ [4938/8991] Built Iut.Foundations.SourceFunctionHEqCongr (317ms)
✔ [4939/8991] Built Iut.Foundations.SourceCategoryPackedHEqEndpointLinkDataHiddenEndpointStorage (1.3s)
✔ [4940/8991] Built Iut.Foundations.SourceCategoryPackedHEqEndpointLinkDataOfTwoHEq (1.4s)
✔ [4941/8991] Built Iut.Foundations.SourceCategoryPackedHEqEndpointLinkDataCommonMiddleProjectionData (1.4s)
✔ [4942/8991] Built Iut.Foundations.SourceSelectedFiberComponentDomination (1.5s)
✔ [4943/8991] Built Iut.Foundations.SourceContinuousActionRestrictionComponentStability (3.1s)
✔ [4944/8991] Built Iut.Foundations.SourceHEqApply (326ms)
✔ [4945/8991] Built Iut.Foundations.SourceEtalePseudofunctorPointIdentityReconstructionNaturality (4.6s)
✔ [4946/8991] Built Iut.Foundations.SourceCategoryProjectionEndpointHEqWhisker (1.4s)
✔ [4947/8991] Built Iut.Foundations.SourceEtaleStackSchemeAtlasFiniteEtaleDescentObjectPullbackProjections (3.0s)
✔ [4948/8991] Built Iut.Foundations.SourceFiniteEtaleSignTorsorTrivialAtlasFirstSheetExt (3.6s)
✔ [4949/8991] Built Iut.Foundations.SourceOrbicurveFiniteEtaleBaseChangePointIsoToSource (2.9s)
✔ [4950/8991] Built Iut.Foundations.SourceEtaleStackSchemeAtlasFiniteEtaleDescentOverlapComparisonLeft (2.0s)
✔ [4951/8991] Built Iut.Foundations.SourceOrbicurveFiniteEtaleIteratedBaseChangeReverseLeftProjection (2.0s)
✔ [4952/8991] Built Iut.Foundations.SourceCategoryInvolutiveActionTransport (1.5s)
✔ [4953/8991] Built Iut.Foundations.SourceRegularInvolutivePullbackFiberSwap (1.9s)
✔ [4954/8991] Built Iut.Foundations.SourceEtaleStackFiniteEtaleComposition (5.6s)
✔ [4955/8991] Built Iut.Foundations.SourceCategoryProjectionEndpointLinkContext (1.3s)
✔ [4956/8991] Built Iut.Foundations.SourceCategoryDetachedHEqData (359ms)
✔ [4957/8991] Built Iut.Foundations.SourceCategoryComparisonProjectionContext (1.4s)
✔ [4958/8991] Built Iut.Foundations.SourceCategoryDetachedEqDataProjections (336ms)
✔ [4959/8991] Built Iut.Foundations.SourceProfinitePostcompositionKernelIso (4.3s)
✔ [4960/8991] Built Iut.Foundations.SourceOrbicurveFiniteEtaleCoverStabilizerExactSequence (2.9s)
✔ [4961/8991] Built Iut.Foundations.SourceProfiniteOpenSubgroupKernelIso (3.6s)
✔ [4962/8991] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalHomPointIsoNaturality (3.2s)
✔ [4963/8991] Built Iut.Foundations.SourceOrbicurveSignInvariantCategory (3.1s)
✔ [4964/8991] Built Iut.Foundations.SourcePseudofunctorStrongTransCompNaturalityInvApp (1.7s)
✔ [4965/8991] Built Iut.Foundations.SourceCategoryFunctorSquarePasting (1.5s)
✔ [4966/8992] Built Iut.Foundations.SourceEtaleStackSchemeAtlasSourceAtlasOverlapCanonicalComparisonLeftExpandedFirstWhiskeredHom (3.2s)
✔ [4967/8992] Built Iut.Foundations.SourceEtaleStackSchemeAtlasMapCechCocycle (3.1s)
✔ [4968/8992] Built Iut.Foundations.SourceFiniteEtaleTensorAction (3.7s)
✔ [4969/8992] Built Iut.Foundations.SourceFiniteEtaleSignQuotientAffineChartCompositionCoherence (3.8s)
✔ [4970/8992] Built Iut.Foundations.SourceFiniteEtaleSignQuotientAffineChartGluedProjection (3.1s)
✔ [4971/8992] Built Iut.Foundations.SourceFiniteEtaleSignQuotientAtlasConeLiftSchemeMap (3.0s)
✔ [4972/8992] Built Iut.Foundations.SourceFiniteEtaleSignQuotientSchemeAtlas (3.2s)
✔ [4973/8992] Built Iut.Foundations.SourceFiniteEtaleSignQuotientInvariantTargetDescent (5.4s)
✔ [4974/8992] Built Iut.Foundations.SourceEtalePseudofunctorTwoPullbackCancellationTwoCellYTargetToY (2.0s)
✔ [4975/8992] Built Iut.Foundations.SourceFiberFunctorComparison (2.5s)
✔ [4976/8992] Built Iut.Foundations.SourceSchemeEtaleStackPresentationReverseFiniteEtaleCover (3.9s)
✔ [4977/8992] Built Iut.Foundations.SourceEtalePseudofunctorContractiblePullbackEquivalence (3.0s)
✔ [4978/8992] Built Iut.Foundations.SourcePreGaloisFiberFunctorEquivalenceTransport (1.7s)
✔ [4979/8992] Built Iut.Foundations.SourcePseudofunctorRestrictionPullHom (2.2s)
✔ [4980/8992] Built Iut.Foundations.SourceSchemeOverFieldRestrictScalarsSliceEquivalence (4.1s)
✔ [4981/8992] Built Iut.Foundations.SourceEtaleFundamentalGroupCoverActionEquivalence (2.6s)
✔ [4983/8992] Built Iut.Foundations.SourceCategoryFourLegSquareReassociation (1.3s)
✔ [4984/8992] Built Iut.Foundations.SourcePseudofunctorStrongTransEndpointPullLeft (1.0s)
✔ [4985/8992] Built Iut.Foundations.SourcePseudofunctorStrongTransEndpointPullRight (2.3s)
✔ [4986/8992] Built Iut.Foundations.SourceEtaleStackSchemeAtlasBaseChangePointIsoSource (2.9s)
✔ [4987/8992] Built Iut.Foundations.SourceCategoryFunctorMapSubsingletonComposition (1.4s)
✔ [4988/8992] Built Iut.Foundations.SourceCategoryEndpointTransportPasting (1.5s)
✔ [4989/8992] Built Iut.Foundations.SourceCategoryMappedTwoThreePasting (1.4s)
✔ [4990/8992] Built Iut.Foundations.SourceFiniteEtaleSignQuotientAtlasPointFiberIsoNaturalityFirstSheet (5.5s)
✔ [4991/8992] Built Iut.Foundations.SourceCategoryMappedNaturalityPasting (1.4s)
✔ [4992/8992] Built Iut.Foundations.SourceCategoryPullNaturalityThroughIso (1.4s)
✔ [4993/8992] Built Iut.Foundations.SourceCategoryThreeFactorIsoRecoveryData (1.5s)
✔ [4994/8992] Built Iut.Foundations.SourceCategoryThreeMapHEq (1.4s)
✔ [4995/8992] Built Iut.Foundations.SourceCategoryRecoverFactorThroughMappedIso (1.5s)
✔ [4996/8992] Built Iut.Foundations.SourceEtalePseudofunctorYonedaIdentityBaseChange (3.3s)
✔ [4997/8992] Built Iut.Foundations.SourceInitialTheta11a1DivisionRootFiberToThirtyTorsion (5.0s)
✔ [4998/8992] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapOverlapPairWhiskeredNestedFactorization (3.0s)
✔ [4999/8992] Built Iut.Foundations.SourceEtaleRepresentedStrongTransPointIsoWhiskerLeftTargetTransportRightDataRight (3.1s)
⚠ [5001/8992] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapPointTripleNaturalityAppTransportDataEndpoints (3.8s)
warning: Iut/Foundations/SourceEtaleStackSchemeAtlasLocalMapPointTripleNaturalityAppTransportDataEndpoints.lean:28:0: Please, add a comment explaining the need for modifying the maxHeartbeat limit, as in
set_option maxHeartbeats 800000 in
-- reason for change
...

Note: This linter can be disabled with `set_option linter.style.maxHeartbeats false`
warning: Iut/Foundations/SourceEtaleStackSchemeAtlasLocalMapPointTripleNaturalityAppTransportDataEndpoints.lean:53:0: Please, add a comment explaining the need for modifying the maxHeartbeat limit, as in
set_option maxHeartbeats 800000 in
-- reason for change
...

Note: This linter can be disabled with `set_option linter.style.maxHeartbeats false`
⚠ [5002/8992] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapPointTripleRepresentedSourceCellEndpointData (3.2s)
warning: Iut/Foundations/SourceEtaleStackSchemeAtlasLocalMapPointTripleRepresentedSourceCellEndpointData.lean:28:0: Please, add a comment explaining the need for modifying the maxHeartbeat limit, as in
set_option maxHeartbeats 800000 in
-- reason for change
...

Note: This linter can be disabled with `set_option linter.style.maxHeartbeats false`
✔ [5003/8992] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapPointTripleCocycleBaseInverseTerminalProjection (3.8s)
✔ [5004/8992] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapPointTripleCocycleNormalizedAtlasMiddleIdentity (3.2s)
✔ [5005/8992] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapPointTriplePastedConeIso (3.1s)
✔ [5006/8992] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapPointTripleLongEdgeGeometricTargetAfterSourceAssociator (3.6s)
✔ [5007/8992] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapPointTripleOverlapValueDirectFactorDataMappedRight (3.3s)
✔ [5008/8992] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapPointTripleCocycleSuccessiveSecondOverlapValueFactorDataMapped (2.8s)
✔ [5009/8992] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapPointTripleCocycleSuccessiveFirstOverlapValueFactorDataMapped (2.9s)
✔ [5010/8992] Built Iut.Foundations.SourceEtaleRepresentedStrongTransPointIsoWhiskerRightWhiskerRightSymmInv (2.0s)
✔ [5011/8992] Built Iut.Foundations.SourceEtaleRepresentedStrongTransPointIsoWhiskerRightCongrIsoSymmInv (2.0s)
✔ [5012/8992] Built Iut.Foundations.SourceTensorProductAlgebraicFiniteStage (3.0s)
✔ [5013/8992] Built Iut.Foundations.SourceFiniteEtaleAffinePullbackActionReversedTensor (3.0s)
✔ [5014/8992] Built Iut.Foundations.SourceEtaleStackSchemeAtlasFiniteEtalePreDescentPullbacks (7.1s)
✔ [5015/8992] Built Iut.Foundations.SourceEtaleStackSchemeAtlasFiniteEtaleDescentTerminal (2.9s)
✔ [5016/8992] Built Iut.Foundations.SourceFiniteEtaleSchemeCoverBaseChangeFiniteCoproducts (3.4s)
✔ [5017/8992] Built Iut.Foundations.SourceInvolutiveEndofunctorEquivariantForgetReflectsLimits (1.8s)
✔ [5018/8992] Built Iut.Foundations.SourceInvolutiveEndofunctorEquivariantFreeObject (2.0s)
✔ [5019/8992] Built Iut.Foundations.SourceInvolutiveEndofunctorEquivariantForgetReflectsIsomorphisms (1.5s)
✔ [5020/8992] Built Iut.Foundations.SourceInvolutiveEndofunctorEquivariantCofreeMono (1.5s)
✔ [5021/8992] Built Iut.Foundations.SourceFiniteEtaleSchemeCoverInvolutivePostcomposition (103s)
✔ [5022/8992] Built Iut.Foundations.SourceTensorProductRightAlgEquivTmul (1.8s)
✔ [5023/8992] Built Iut.Foundations.SourceTensorProductRingHomTmulFactorization (1.8s)
✔ [5024/8992] Built Iut.Foundations.SourceEquivTransportApplyBackTarget (741ms)
✔ [5025/8992] Built Iut.Foundations.SourceSchemePullbackSectionAlongComposite (4.2s)
✔ [5026/8992] Built Iut.Foundations.SourceEtalePseudofunctorConeReplaceCommutesHomTargetIso (2.5s)
✔ [5027/8992] Built Iut.Foundations.SourceFiniteEtaleSignQuotientAtlasSecondSheetTotalSpaces (4.1s)
✔ [5028/8992] Built Iut.Foundations.SourceFiniteEtaleSignQuotientEquivariantMapIdentity (3.6s)
✔ [5029/8992] Built Iut.Foundations.SourceFiniteEtaleSignQuotientEquivariantMapComposition (4.1s)
✔ [5030/8992] Built Iut.Foundations.SourceFiniteEtaleSignTorsorInvariantEffectiveDescent (3.2s)
✔ [5031/8992] Built Iut.Foundations.SourceFiniteEtaleSignQuotientHomTripleCarrier (2.9s)
✔ [5032/8992] Built Iut.Foundations.SourceFiniteEtaleSignQuotientReindexCompInverseToTotal (3.1s)
✔ [5033/8992] Built Iut.Foundations.SourceCategoryThreeMorphismBridgePastingPackedCompletion (1.4s)
✔ [5034/8992] Built Iut.Foundations.SourceFiniteEtaleSignQuotientPointIdentityReconstructionComparison (3.0s)
✔ [5035/8992] Built Iut.Foundations.SourceGaloisFiberFunctorFiniteColimitsHeterogeneous (2.5s)
✔ [5036/8992] Built Iut.Foundations.SourceContinuousActionRestrictionConnectednessSurjectivity (3.8s)
✔ [5037/8992] Built Iut.Foundations.SourceCategoryTheoryEqToIsoFintypeMapApplyHEq (1.5s)
✔ [5038/8992] Built Iut.Foundations.SourceCategoryTheoryIndexedNatIsoTransportFintypeComponentHEq (1.5s)
✔ [5039/8992] Built Iut.Foundations.SourceFintypeDetachedNaturalityIsoExtension (1.7s)
✔ [5040/8992] Built Iut.Foundations.SourceContinuousActionClosedSubgroupAmbientEnvelope (3.9s)
✔ [5041/8992] Built Iut.Foundations.SourcePointedAnabelioidKernelFiberStability (3.0s)
✔ [5042/8992] Built Iut.Foundations.SourceEquivalenceInversePointNaturality (1.6s)
✔ [5043/8992] Built Iut.Foundations.SourceCategoryPackedHEqEndpointLinkDataCommonRightComparisonDataLeftComm (1.4s)
✔ [5044/8992] Built Iut.Foundations.SourceFunctionHEqCastMapDataPostmap (324ms)
✔ [5045/8992] Built Iut.Foundations.SourceFunctionHEqData (1.4s)
✔ [5046/8992] Built Iut.Foundations.SourceCategoryPackedHEqEndpointLinkDataHiddenEndpointStorageExplicit (1.4s)
✔ [5047/8992] Built Iut.Foundations.SourceCategoryPackedHEqEndpointLinkDataCommonMiddleProjectionDataOfExplicitMiddle (1.4s)
✔ [5048/8992] Built Iut.Foundations.SourceSelectedFiberSurjectiveMapDataComponentDomination (1.5s)
✔ [5049/8992] Built Iut.Foundations.SourceFiniteEtaleSignQuotientPointIdentityReconstructionNaturality (3.3s)
✔ [5050/8992] Built Iut.Foundations.SourceEtalePseudofunctorPointIdentityReconstructionComponent (4.0s)
✔ [5051/8992] Built Iut.Foundations.SourceRegularInvolutiveEquivariantExtension (2.7s)
✔ [5052/8992] Built Iut.Foundations.SourceCategoryProjectionEndpointLinkData (1.4s)
✔ [5053/8992] Built Iut.Foundations.SourceCategoryDetachedHEqPastingData (353ms)
✔ [5054/8992] Built Iut.Foundations.SourceCategoryDetachedHEqDataProjections (329ms)
✔ [5055/8992] Built Iut.Foundations.SourceCategoryComparisonProjectionContextLeftWhisker (1.4s)
✔ [5056/8992] Built Iut.Foundations.SourceOrbicurveFiniteEtaleCoverStabilizerProjectionSurjectivity (3.2s)
✔ [5057/8992] Built Iut.Foundations.SourceOrbicurveFiniteEtaleCoverStabilizerKernelIso (2.9s)
✔ [5058/8992] Built Iut.Foundations.SourceEtaleStackSchemeAtlasYonedaFiberNaturalityOfPointIso (3.4s)
✔ [5059/8992] Built Iut.Foundations.SourceEtaleStackSchemeAtlasPointIsoDescentComparison (5.2s)
✔ [5060/8992] Built Iut.Foundations.SourceOrbicurveSignInvariantIso (3.1s)
✔ [5061/8992] Built Iut.Foundations.SourceOrbicurveSignQuotientComparison (3.4s)
✔ [5062/8992] Built Iut.Foundations.SourceCategoryFunctorSquarePastingEvidenceFirst (1.4s)
✔ [5063/8992] Built Iut.Foundations.SourceCategoryFunctorSquarePastingContext (1.6s)
⚠ [5064/8992] Built Iut.Foundations.SourceEtaleStackSchemeAtlasSourceAtlasOverlapCanonicalComparisonLeftExpandedSecondWhiskerCongr (3.0s)
warning: Iut/Foundations/SourceEtaleStackSchemeAtlasSourceAtlasOverlapCanonicalComparisonLeftExpandedSecondWhiskerCongr.lean:7:100: This line exceeds the 100 character limit, please shorten it!

Note: This linter can be disabled with `set_option linter.style.longLine false`
✔ [5066/8992] Built Iut.Foundations.SourceEtaleStackSchemeAtlasMapLocalMapCechData (2.7s)
✔ [5067/8992] Built Iut.Foundations.SourceFiniteEtaleTensorFixedSubalgebra (4.1s)
✔ [5068/8992] Built Iut.Foundations.SourceFiniteEtaleSignQuotientAffineChartCompositionContext (3.5s)
✔ [5069/8992] Built Iut.Foundations.SourceFiniteEtaleSignQuotientAffineChartGluedInvolution (3.0s)
✔ [5070/8992] Built Iut.Foundations.SourceFiniteEtaleSignQuotientAtlasConeLiftTransportSchemeMap (3.1s)

stderr:
/usr/bin/podman timed out after 7200s
podman cleanup removed verifier container apx-verifier-job-1793-runtime-lean_checker-2510420-1789168350035750074-1 on attempt 1

$ lake build :blueprint
exit_code=Some(1) duration_ms=1248
stderr:
error: unknown package facet `blueprint`

apx-runtime-resource-v1	apx-verifier-job-1793-runtime-blueprint_build-2510420-1789175550760398339-2	888832	1404928	21474836480	0	0	0	0	0	0	3244032	107974656	21474836480	0	0	0	0	0	0


blueprint_build failed; continuing (non-fatal phase).

Command runs

git_cloneexit 128duration 211 ms · created 
git clone --depth 1 --branch e21-929-cohomology-checkpoint --single-branch https://github.com/promachina/iut-lean.git /var/lib/apodeixis/repos/job-1793-source
Cloning into '/var/lib/apodeixis/repos/job-1793-source'...
error: unable to read askpass response from '/usr/bin/false'
fatal: could not read Username for 'https://github.com': terminal prompts disabled
git_cloneexit 0duration 4s · created 
git clone (github installation auth fallback)
Cloning into '/var/lib/apodeixis/repos/job-1793-source'...
git_checkoutexit 0duration 371 ms · created 
git checkout 9ce7ebcfce50544bdb3509e0ade9fd28f8b80ff0
Note: switching to '9ce7ebcfce50544bdb3509e0ade9fd28f8b80ff0'.

You are in 'detached HEAD' state. You can look around, make experimental
changes and commit them, and you can discard any commits you make in this
state without impacting any branches by switching back to a branch.

If you want to create a new branch to retain commits you create, you may
do so (now or later) by using -c with the switch command. Example:

  git switch -c <new-branch-name>

Or undo this operation with:

  git switch -

Turn off this advice by setting config variable advice.detachedHead to false

HEAD is now at 9ce7ebc feat(e21): prove and audit the actual projective cubic geometric genus
lake_cacheexit 0duration 52s · created 
lake exe cache get
Current branch: HEAD
Using cache (Azure) from origin: (some leanprover-community/mathlib4)
Attempting to download 8459 file(s) from leanprover-community/mathlib4 cache
Decompressed 8459 file(s)
Already decompressed 8459 file(s)

✔ [8/25] Built Cache.Lean (393ms)
✔ [10/25] Built Batteries.Data.Array.Match:c.o (213ms)
✔ [11/25] Built Batteries.Data.String.Basic:c.o (103ms)
✔ [12/25] Built Batteries.Data.String.Matcher:c.o (185ms)
✔ [13/25] Built Cache.Lean:c.o (133ms)
✔ [15/25] Built Cache.Init (319ms)
✔ [16/25] Built Cache.IO (1.7s)
✔ [17/25] Built Cache.Init:c.o (94ms)
✔ [18/25] Built Cache.IO:c.o (1.2s)
✔ [19/25] Built Cache.Hashing (870ms)
✔ [20/25] Built Cache.Hashing:c.o (345ms)
✔ [21/25] Built Cache.Requests (2.1s)
✔ [22/25] Built Cache.Requests:c.o (1.8s)
✔ [23/25] Built Cache.Main (939ms)
✔ [24/25] Built Cache.Main:c.o (546ms)
✔ [25/25] Built cache:exe (822ms)

Downloaded: 1 file(s) [attempted 1/8459 = 0%, 11 KB/s], Decompressed: 0
Downloaded: 16 file(s) [attempted 16/8459 = 0%, 28 KB/s], Decompressed: 9
Downloaded: 39 file(s) [attempted 39/8459 = 0%, 27 KB/s], Decompressed: 20
Downloaded: 61 file(s) [attempted 61/8459 = 0%, 30 KB/s], Decompressed: 31
Downloaded: 86 file(s) [attempted 86/8459 = 1%, 61 KB/s], Decompressed: 31
Downloaded: 110 file(s) [attempted 110/8459 = 1%, 112 KB/s], Decompressed: 53
Downloaded: 144 file(s) [attempted 144/8459 = 1%, 218 KB/s], Decompressed: 89
Downloaded: 182 file(s) [attempted 182/8459 = 2%, 249 KB/s], Decompressed: 89
Downloaded: 220 file(s) [attempted 220/8459 = 2%, 90 KB/s], Decompressed: 89
Downloaded: 251 file(s) [attempted 251/8459 = 2%, 189 KB/s], Decompressed: 144
Downloaded: 288 file(s) [attempted 288/8459 = 3%, 83 KB/s], Decompressed: 144
Downloaded: 322 file(s) [attempted 322/8459 = 3%, 192 KB/s], Decompressed: 144
Downloaded: 360 file(s) [attempted 360/8459 = 4%, 163 KB/s], Decompressed: 144
Downloaded: 397 file(s) [attempted 397/8459 = 4%, 597 KB/s], Decompressed: 227
Downloaded: 435 file(s) [attempted 435/8459 = 5%, 429 KB/s], Decompressed: 227
Downloaded: 473 file(s) [attempted 473/8459 = 5%, 74 KB/s], Decompressed: 227
Downloaded: 504 file(s) [attempted 504/8459 = 5%, 104 KB/s], Decompressed: 227
Downloaded: 545 file(s) [attempted 545/8459 = 6%, 30 KB/s], Decompressed: 227
Downloaded: 586 file(s) [attempted 586/8459 = 6%, 64 KB/s], Decompressed: 381
Downloaded: 628 file(s) [attempted 628/8459 = 7%, 176 KB/s], Decompressed: 381
Downloaded: 665 file(s) [attempted 665/8459 = 7%, 93 KB/s], Decompressed: 381
Downloaded: 699 file(s) [attempted 699/8459 = 8%, 337 KB/s], Decompressed: 381
Downloaded: 743 file(s) [attempted 743/8459 = 8%, 431 KB/s], Decompressed: 381
Downloaded: 784 file(s) [attempted 784/8459 = 9%, 113 KB/s], Decompressed: 381
Downloaded: 825 file(s) [attempted 825/8459 = 9%, 166 KB/s], Decompressed: 572
Downloaded: 863 file(s) [attempted 863/8459 = 10%, 437 KB/s], Decompressed: 572
Downloaded: 901 file(s) [attempted 901/8459 = 10%, 566 KB/s], Decompressed: 572
Downloaded: 942 file(s) [attempted 942/8459 = 11%, 169 KB/s], Decompressed: 572
Downloaded: 986 file(s) [attempted 986/8459 = 11%, 67 KB/s], Decompressed: 572
Downloaded: 1031 file(s) [attempted 1031/8459 = 12%, 713 KB/s], Decompressed: 791
Downloaded: 1068 file(s) [attempted 1068/8459 = 12%, 242 KB/s], Decompressed: 791
Downloaded: 1109 file(s) [attempted 1109/8459 = 13%, 352 KB/s], Decompressed: 791
Downloaded: 1150 file(s) [attempted 1150/8459 = 13%, 306 KB/s], Decompressed: 791
Downloaded: 1192 file(s) [attempted 1192/8459 = 14%, 61 KB/s], Decompressed: 791
Downloaded: 1233 file(s) [attempted 1233/8459 = 14%, 1178 KB/s], Decompressed: 791
Downloaded: 1277 file(s) [attempted 1277/8459 = 15%, 226 KB/s], Decompressed: 1031
Downloaded: 1318 file(s) [attempted 1318/8459 = 15%, 173 KB/s], Decompressed: 1031
Downloaded: 1356 file(s) [attempted 1356/8459 = 16%, 301 KB/s], Decompressed: 1031
Downloaded: 1390 file(s) [attempted 1390/8459 = 16%, 385 KB/s], Decompressed: 1031
Downloaded: 1431 file(s) [attempted 1431/8459 = 16%, 28 KB/s], Decompressed: 1031
Downloaded: 1472 file(s) [attempted 1472/8459 = 17%, 255 KB/s], Decompressed: 1267
Downloaded: 1516 file(s) [attempted 1516/8459 = 17%, 84 KB/s], Decompressed: 1267
Downloaded: 1557 file(s) [attempted 1557/8459 = 18%, 99 KB/s], Decompressed: 1267
Downloaded: 1595 file(s) [attempted 1595/8459 = 18%, 337 KB/s], Decompressed: 1267
Downloaded: 1639 file(s) [attempted 1639/8459 = 19%, 473 KB/s], Decompressed: 1267
Downloaded: 1677 file(s) [attempted 1677/8459 = 19%, 471 KB/s], Decompressed: 1472
Downloaded: 1722 file(s) [attempted 1722/8459 = 20%, 139 KB/s], Decompressed: 1472
Downloaded: 1769 file(s) [attempted 1769/8459 = 20%, 1035 KB/s], Decompressed: 1472
Downloaded: 1810 file(s) [attempted 1810/8459 = 21%, 61 KB/s], Decompressed: 1472
Downloaded: 1848 file(s) [attempted 1848/8459 = 21%, 490 KB/s], Decompressed: 1472
Downloaded: 1889 file(s) [attempted 1889/8459 = 22%, 745 KB/s], Decompressed: 1670
Downloaded: 1930 file(s) [attempted 1930/8459 = 22%, 700 KB/s], Decompressed: 1670
Downloaded: 1964 file(s) [attempted 1964/8459 = 23%, 248 KB/s], Decompressed: 1670
Downloaded: 2009 file(s) [attempted 2009/8459 = 23%, 392 KB/s], Decompressed: 1670
Downloaded: 2050 file(s) [attempted 2050/8459 = 24%, 831 KB/s], Decompressed: 1670
Downloaded: 2087 file(s) [attempted 2087/8459 = 24%, 997 KB/s], Decompressed: 1869
Downloaded: 2128 file(s) [attempted 2128/8459 = 25%, 88 KB/s], Decompressed: 1869
Downloaded: 2169 file(s) [attempted 2169/8459 = 25%, 260 KB/s], Decompressed: 1869
Downloaded: 2207 file(s) [attempted 2207/8459 = 26%, 148 KB/s], Decompressed: 1869
Downloaded: 2245 file(s) [attempted 2245/8459 = 26%, 173 KB/s], Decompressed: 1869
Downloaded: 2282 file(s) [attempted 2282/8459 = 26%, 135 KB/s], Decompressed: 2063
Downloaded: 2330 file(s) [attempted 2330/8459 = 27%, 88 KB/s], Decompressed: 2063
Downloaded: 2364 file(s) [attempted 2364/8459 = 27%, 291 KB/s], Decompressed: 2063
Downloaded: 2405 file(s) [attempted 2405/8459 = 28%, 46 KB/s], Decompressed: 2063
Downloaded: 2446 file(s) [attempted 2446/8459 = 28%, 67 KB/s], Decompressed: 2063
Downloaded: 2484 file(s) [attempted 2484/8459 = 29%, 266 KB/s], Decompressed: 2063
Downloaded: 2529 file(s) [attempted 2529/8459 = 29%, 531 KB/s], Decompressed: 2282
Downloaded: 2570 file(s) [attempted 2570/8459 = 30%, 131 KB/s], Decompressed: 2282
Downloaded: 2604 file(s) [attempted 2604/8459 = 30%, 592 KB/s], Decompressed: 2282
Downloaded: 2645 file(s) [attempted 2645/8459 = 31%, 207 KB/s], Decompressed: 2282
Downloaded: 2686 file(s) [attempted 2686/8459 = 31%, 47 KB/s], Decompressed: 2282
Downloaded: 2723 file(s) [attempted 2723/8459 = 32%, 495 KB/s], Decompressed: 2505
Downloaded: 2761 file(s) [attempted 2761/8459 = 32%, 162 KB/s], Decompressed: 2505
Downloaded: 2802 file(s) [attempted 2802/8459 = 33%, 1014 KB/s], Decompressed: 2505
Downloaded: 2843 file(s) [attempted 2843/8459 = 33%, 78 KB/s], Decompressed: 2505
Downloaded: 2881 file(s) [attempted 2881/8459 = 34%, 683 KB/s], Decompressed: 2505
Downloaded: 2918 file(s) [attempted 2918/8459 = 34%, 562 KB/s], Decompressed: 2505
Downloaded: 2956 file(s) [attempted 2956/8459 = 34%, 1012 KB/s], Decompressed: 2723
Downloaded: 2997 file(s) [attempted 2997/8459 = 35%, 328 KB/s], Decompressed: 2723
Downloaded: 3035 file(s) [attempted 3035/8459 = 35%, 1049 KB/s], Decompressed: 2723
Downloaded: 3079 file(s) [attempted 3079/8459 = 36%, 888 KB/s], Decompressed: 2723
Downloaded: 3117 file(s) [attempted 3117/8459 = 36%, 73 KB/s], Decompressed: 2723
Downloaded: 3158 file(s) [attempted 3158/8459 = 37%, 110 KB/s], Decompressed: 2949
Downloaded: 3195 file(s) [attempted 3195/8459 = 37%, 194 KB/s], Decompressed: 2949
Downloaded: 3236 file(s) [attempted 3236/8459 = 38%, 108 KB/s], Decompressed: 2949
Downloaded: 3281 file(s) [attempted 3281/8459 = 38%, 152 KB/s], Decompressed: 2949
Downloaded: 3318 file(s) [attempted 3318/8459 = 39%, 157 KB/s], Decompressed: 2949
Downloaded: 3359 file(s) [attempted 3359/8459 = 39%, 78 KB/s], Decompressed: 3147
Downloaded: 3397 file(s) [attempted 3397/8459 = 40%, 790 KB/s], Decompressed: 3147
Downloaded: 3438 file(s) [attempted 3438/8459 = 40%, 253 KB/s], Decompressed: 3147
Downloaded: 3483 file(s) [attempted 3483/8459 = 41%, 153 KB/s], Decompressed: 3147
Downloaded: 3520 file(s) [attempted 3520/8459 = 41%, 68 KB/s], Decompressed: 3147
Downloaded: 3558 file(s) [attempted 3558/8459 = 42%, 110 KB/s], Decompressed: 3336
Downloaded: 3599 file(s) [attempted 3599/8459 = 42%, 376 KB/s], Decompressed: 3336
Downloaded: 3636 file(s) [attempted 3636/8459 = 42%, 548 KB/s], Decompressed: 3336
Downloaded: 3677 file(s) [attempted 3677/8459 = 43%, 365 KB/s], Decompressed: 3336
Downloaded: 3719 file(s) [attempted 3719/8459 = 43%, 143 KB/s], Decompressed: 3336
Downloaded: 3756 file(s) [attempted 3756/8459 = 44%, 785 KB/s], Decompressed: 3531
Downloaded: 3790 file(s) [attempted 3790/8459 = 44%, 364 KB/s], Decompressed: 3531
Downloaded: 3835 file(s) [attempted 3835/8459 = 45%, 115 KB/s], Decompressed: 3531
Downloaded: 3876 file(s) [attempted 3876/8459 = 45%, 209 KB/s], Decompressed: 3531
Downloaded: 3917 file(s) [attempted 3917/8459 = 46%, 47 KB/s], Decompressed: 3725
Downloaded: 3958 file(s) [attempted 3958/8459 = 46%, 106 KB/s], Decompressed: 3725
Downloaded: 3992 file(s) [attempted 3992/8459 = 47%, 191 KB/s], Decompressed: 3725
Downloaded: 4037 file(s) [attempted 4037/8459 = 47%, 97 KB/s], Decompressed: 3725
Downloaded: 4071 file(s) [attempted 4071/8459 = 48%, 292 KB/s], Decompressed: 3890
Downloaded: 4112 file(s) [attempted 4112/8459 = 48%, 169 KB/s], Decompressed: 3890
Downloaded: 4153 file(s) [attempted 4153/8459 = 49%, 244 KB/s], Decompressed: 3890
Downloaded: 4190 file(s) [attempted 4190/8459 = 49%, 2009 KB/s], Decompressed: 3890
Downloaded: 4231 file(s) [attempted 4231/8459 = 50%, 338 KB/s], Decompressed: 4040
Downloaded: 4269 file(s) [attempted 4269/8459 = 50%, 221 KB/s], Decompressed: 4040
Downloaded: 4310 file(s) [attempted 4310/8459 = 50%, 911 KB/s], Decompressed: 4040
Downloaded: 4355 file(s) [attempted 4355/8459 = 51%, 358 KB/s], Decompressed: 4040
Downloaded: 4399 file(s) [attempted 4399/8459 = 52%, 995 KB/s], Decompressed: 4040
Downloaded: 4437 file(s) [attempted 4437/8459 = 52%, 802 KB/s], Decompressed: 4040
Downloaded: 4474 file(s) [attempted 4474/8459 = 52%, 125 KB/s], Decompressed: 4040
Downloaded: 4515 file(s) [attempted 4515/8459 = 53%, 379 KB/s], Decompressed: 4231
Downloaded: 4553 file(s) [attempted 4553/8459 = 53%, 477 KB/s], Decompressed: 4231
Downloaded: 4594 file(s) [attempted 4594/8459 = 54%, 38 KB/s], Decompressed: 4231
Downloaded: 4632 file(s) [attempted 4632/8459 = 54%, 57 KB/s], Decompressed: 4231
Downloaded: 4673 file(s) [attempted 4673/8459 = 55%, 222 KB/s], Decompressed: 4231
Downloaded: 4717 file(s) [attempted 4717/8459 = 55%, 184 KB/s], Decompressed: 4231
Downloaded: 4751 file(s) [attempted 4751/8459 = 56%, 586 KB/s], Decompressed: 4231
Downloaded: 4792 file(s) [attempted 4792/8459 = 56%, 335 KB/s], Decompressed: 4231
Downloaded: 4833 file(s) [attempted 4833/8459 = 57%, 102 KB/s], Decompressed: 4515
Downloaded: 4874 file(s) [attempted 4874/8459 = 57%, 110 KB/s], Decompressed: 4515
Downloaded: 4912 file(s) [attempted 4912/8459 = 58%, 1649 KB/s], Decompressed: 4515
Downloaded: 4950 file(s) [attempted 4950/8459 = 58%, 120 KB/s], Decompressed: 4515
Downloaded: 4991 file(s) [attempted 4991/8459 = 59%, 317 KB/s], Decompressed: 4515
Downloaded: 5035 file(s) [attempted 5035/8459 = 59%, 148 KB/s], Decompressed: 4515
Downloaded: 5080 file(s) [attempted 5080/8459 = 60%, 297 KB/s], Decompressed: 4515
Downloaded: 5117 file(s) [attempted 5117/8459 = 60%, 51 KB/s], Decompressed: 4515
Downloaded: 5155 file(s) [attempted 5155/8459 = 60%, 142 KB/s], Decompressed: 4833
Downloaded: 5196 file(s) [attempted 5196/8459 = 61%, 111 KB/s], Decompressed: 4833
Downloaded: 5233 file(s) [attempted 5233/8459 = 61%, 300 KB/s], Decompressed: 4833
Downloaded: 5271 file(s) [attempted 5271/8459 = 62%, 252 KB/s], Decompressed: 4833
Downloaded: 5315 file(s) [attempted 5315/8459 = 62%, 211 KB/s], Decompressed: 4833
Downloaded: 5353 file(s) [attempted 5353/8459 = 63%, 390 KB/s], Decompressed: 4833
Downloaded: 5398 file(s) [attempted 5398/8459 = 63%, 63 KB/s], Decompressed: 5121
Downloaded: 5432 file(s) [attempted 5432/8459 = 64%, 143 KB/s], Decompressed: 5121
Downloaded: 5473 file(s) [attempted 5473/8459 = 64%, 22 KB/s], Decompressed: 5121
Downloaded: 5517 file(s) [attempted 5517/8459 = 65%, 1293 KB/s], Decompressed: 5121
Downloaded: 5558 file(s) [attempted 5558/8459 = 65%, 78 KB/s], Decompressed: 5121
Downloaded: 5603 file(s) [attempted 5603/8459 = 66%, 1180 KB/s], Decompressed: 5121
Downloaded: 5640 file(s) [attempted 5640/8459 = 66%, 117 KB/s], Decompressed: 5370
Downloaded: 5675 file(s) [attempted 5675/8459 = 67%, 716 KB/s], Decompressed: 5370
Downloaded: 5719 file(s) [attempted 5719/8459 = 67%, 164 KB/s], Decompressed: 5370
Downloaded: 5763 file(s) [attempted 5763/8459 = 68%, 201 KB/s], Decompressed: 5370
Downloaded: 5801 file(s) [attempted 5801/8459 = 68%, 332 KB/s], Decompressed: 5370
Downloaded: 5839 file(s) [attempted 5839/8459 = 69%, 127 KB/s], Decompressed: 5370
Downloaded: 5876 file(s) [attempted 5876/8459 = 69%, 146 KB/s], Decompressed: 5620
Downloaded: 5917 file(s) [attempted 5917/8459 = 69%, 505 KB/s], Decompressed: 5620
Downloaded: 5958 file(s) [attempted 5958/8459 = 70%, 138 KB/s], Decompressed: 5620
Downloaded: 5999 file(s) [attempted 5999/8459 = 70%, 279 KB/s], Decompressed: 5620
Downloaded: 6040 file(s) [attempted 6040/8459 = 71%, 55 KB/s], Decompressed: 5620
Downloaded: 6081 file(s) [attempted 6081/8459 = 71%, 106 KB/s], Decompressed: 5620
Downloaded: 6119 file(s) [attempted 6119/8459 = 72%, 125 KB/s], Decompressed: 5620
Downloaded: 6160 file(s) [attempted 6160/8459 = 72%, 38 KB/s], Decompressed: 5620
Downloaded: 6201 file(s) [attempted 6201/8459 = 73%, 503 KB/s], Decompressed: 5873
Downloaded: 6242 file(s) [attempted 6242/8459 = 73%, 66 KB/s], Decompressed: 5873
Downloaded: 6283 file(s) [attempted 6283/8459 = 74%, 56 KB/s], Decompressed: 5873
Downloaded: 6321 file(s) [attempted 6321/8459 = 74%, 548 KB/s], Decompressed: 5873
Downloaded: 6362 file(s) [attempted 6362/8459 = 75%, 1342 KB/s], Decompressed: 5873
Downloaded: 6399 file(s) [attempted 6399/8459 = 75%, 181 KB/s], Decompressed: 5873
Downloaded: 6440 file(s) [attempted 6440/8459 = 76%, 105 KB/s], Decompressed: 5873
Downloaded: 6481 file(s) [attempted 6481/8459 = 76%, 173 KB/s], Decompressed: 5873
Downloaded: 6525 file(s) [attempted 6525/8459 = 77%, 507 KB/s], Decompressed: 5873
Downloaded: 6564 file(s) [attempted 6564/8459 = 77%, 686 KB/s], Decompressed: 5873
Downloaded: 6605 file(s) [attempted 6605/8459 = 78%, 528 KB/s], Decompressed: 5873
Downloaded: 6642 file(s) [attempted 6642/8459 = 78%, 31 KB/s], Decompressed: 6184
Downloaded: 6676 file(s) [attempted 6676/8459 = 78%, 58 KB/s], Decompressed: 6184
Downloaded: 6721 file(s) [attempted 6721/8459 = 79%, 355 KB/s], Decompressed: 6184
Downloaded: 6758 file(s) [attempted 6758/8459 = 79%, 218 KB/s], Decompressed: 6184
Downloaded: 6800 file(s) [attempted 6800/8459 = 80%, 144 KB/s], Decompressed: 6184
Downloaded: 6837 file(s) [attempted 6837/8459 = 80%, 285 KB/s], Decompressed: 6184
Downloaded: 6875 file(s) [attempted 6875/8459 = 81%, 206 KB/s], Decompressed: 6184
Downloaded: 6916 file(s) [attempted 6916/8459 = 81%, 414 KB/s], Decompressed: 6184
Downloaded: 6953 file(s) [attempted 6953/8459 = 82%, 281 KB/s], Decompressed: 6184
Downloaded: 6998 file(s) [attempted 6998/8459 = 82%, 1610 KB/s], Decompressed: 6184
Downloaded: 7035 file(s) [attempted 7035/8459 = 83%, 135 KB/s], Decompressed: 6184
Downloaded: 7076 file(s) [attempted 7076/8459 = 83%, 62 KB/s], Decompressed: 6184
Downloaded: 7118 file(s) [attempted 7118/8459 = 84%, 267 KB/s], Decompressed: 6184
Downloaded: 7159 file(s) [attempted 7159/8459 = 84%, 105 KB/s], Decompressed: 6184
Downloaded: 7200 file(s) [attempted 7200/8459 = 85%, 25 KB/s], Decompressed: 6184
Downloaded: 7237 file(s) [attempted 7237/8459 = 85%, 1031 KB/s], Decompressed: 6184
Downloaded: 7278 file(s) [attempted 7278/8459 = 86%, 212 KB/s], Decompressed: 6618
Downloaded: 7319 file(s) [attempted 7319/8459 = 86%, 571 KB/s], Decompressed: 6618
Downloaded: 7360 file(s) [attempted 7360/8459 = 87%, 155 KB/s], Decompressed: 6618
Downloaded: 7401 file(s) [attempted 7401/8459 = 87%, 524 KB/s], Decompressed: 6618
Downloaded: 7442 file(s) [attempted 7442/8459 = 87%, 83 KB/s], Decompressed: 6618
Downloaded: 7480 file(s) [attempted 7480/8459 = 88%, 1413 KB/s], Decompressed: 6618
Downloaded: 7524 file(s) [attempted 7524/8459 = 88%, 122 KB/s], Decompressed: 6618
Downloaded: 7565 file(s) [attempted 7565/8459 = 89%, 229 KB/s], Decompressed: 6618
Downloaded: 7603 file(s) [attempted 7603/8459 = 89%, 104 KB/s], Decompressed: 6618
Downloaded: 7641 file(s) [attempted 7641/8459 = 90%, 88 KB/s], Decompressed: 6618
Downloaded: 7685 file(s) [attempted 7685/8459 = 90%, 47 KB/s], Decompressed: 6618
Downloaded: 7727 file(s) [attempted 7727/8459 = 91%, 76 KB/s], Decompressed: 6618
Downloaded: 7767 file(s) [attempted 7767/8459 = 91%, 96 KB/s], Decompressed: 6618
Downloaded: 7805 file(s) [attempted 7805/8459 = 92%, 50 KB/s], Decompressed: 6618
Downloaded: 7842 file(s) [attempted 7842/8459 = 92%, 465 KB/s], Decompressed: 6618
Downloaded: 7887 file(s) [attempted 7887/8459 = 93%, 667 KB/s], Decompressed: 6618
Downloaded: 7931 file(s) [attempted 7931/8459 = 93%, 207 KB/s], Decompressed: 6618
Downloaded: 7966 file(s) [attempted 7966/8459 = 94%, 99 KB/s], Decompressed: 6618
Downloaded: 8003 file(s) [attempted 8003/8459 = 94%, 202 KB/s], Decompressed: 6618
Downloaded: 8048 file(s) [attempted 8048/8459 = 95%, 143 KB/s], Decompressed: 6618
Downloaded: 8090 file(s) [attempted 8090/8459 = 95%, 220 KB/s], Decompressed: 6618
Downloaded: 8126 file(s) [attempted 8126/8459 = 96%, 563 KB/s], Decompressed: 7278
Downloaded: 8167 file(s) [attempted 8167/8459 = 96%, 1356 KB/s], Decompressed: 7278
Downloaded: 8205 file(s) [attempted 8205/8459 = 96%, 1577 KB/s], Decompressed: 7278
Downloaded: 8249 file(s) [attempted 8249/8459 = 97%, 192 KB/s], Decompressed: 7278
Downloaded: 8290 file(s) [attempted 8290/8459 = 98%, 454 KB/s], Decompressed: 7278
Downloaded: 8331 file(s) [attempted 8331/8459 = 98%, 47 KB/s], Decompressed: 7278
Downloaded: 8369 file(s) [attempted 8369/8459 = 98%, 471 KB/s], Decompressed: 7278
Downloaded: 8410 file(s) [attempted 8410/8459 = 99%, 110 KB/s], Decompressed: 7278
Downloaded: 8451 file(s) [attempted 8451/8459 = 99%, 90 KB/s], Decompressed: 7278
Downloaded: 8459 file(s) [attempted 8459/8459 = 100%, 90 KB/s], Decompressed: 7278

apx-runtime-resource-v1	apx-verifier-job-1793-runtime-lake_cache-2510420-1789168298327986791-0	880640	1392640	21474836480	0	0	0	0	0	0	8141430784	8451891200	21474836480	0	0	0	0	0	0
lean_checkerexit -duration 2h 0m · created 
lake build
�m̵_̵a̵p̵p̵_̵t̵o̵r̵s̵o̵r̵I̵s̵o̵_̵h̵o̵m̵] at componentInverse

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Iut/Foundations/SourceFiniteEtaleSignTorsor.lean:5163:4: This central dot `·` is isolated; please merge it with the next line.

Note: This linter can be disabled with `set_option linter.style.cdot false`
warning: Iut/Foundations/SourceFiniteEtaleSignTorsor.lean:5188:4: This central dot `·` is isolated; please merge it with the next line.

Note: This linter can be disabled with `set_option linter.style.cdot false`
warning: Iut/Foundations/SourceFiniteEtaleSignTorsor.lean:5284:4: This central dot `·` is isolated; please merge it with the next line.

Note: This linter can be disabled with `set_option linter.style.cdot false`
warning: Iut/Foundations/SourceFiniteEtaleSignTorsor.lean:5300:4: This central dot `·` is isolated; please merge it with the next line.

Note: This linter can be disabled with `set_option linter.style.cdot false`
warning: Iut/Foundations/SourceFiniteEtaleSignTorsor.lean:5315:4: This central dot `·` is isolated; please merge it with the next line.

Note: This linter can be disabled with `set_option linter.style.cdot false`
warning: Iut/Foundations/SourceFiniteEtaleSignTorsor.lean:5788:2: try 'simp' instead of 'simpa'

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`
warning: Iut/Foundations/SourceFiniteEtaleSignTorsor.lean:5797:2: try 'simp' instead of 'simpa'

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`
warning: Iut/Foundations/SourceFiniteEtaleSignTorsor.lean:7977:13: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice

Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false`
warning: Iut/Foundations/SourceFiniteEtaleSignTorsor.lean:8145:13: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice

Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false`
warning: Iut/Foundations/SourceFiniteEtaleSignTorsor.lean:11284:0: Please, add a comment explaining the need for modifying the maxHeartbeat limit, as in
set_option maxHeartbeats 400000 in
-- reason for change
...

Note: This linter can be disabled with `set_option linter.style.maxHeartbeats false`
warning: Iut/Foundations/SourceFiniteEtaleSignTorsor.lean:11284:0: Unscoped option maxHeartbeats is not allowed:
Please scope this to individual declarations, as in
```
set_option maxHeartbeats in
-- comment explaining why this is necessary
example : ... := ...
```

Note: This linter can be disabled with `set_option linter.style.setOption false`
warning: Iut/Foundations/SourceFiniteEtaleSignTorsor.lean:11476:0: Please, add a comment explaining the need for modifying the maxHeartbeat limit, as in
set_option maxHeartbeats 400000 in
-- reason for change
...

Note: This linter can be disabled with `set_option linter.style.maxHeartbeats false`
warning: Iut/Foundations/SourceFiniteEtaleSignTorsor.lean:11476:0: Unscoped option maxHeartbeats is not allowed:
Please scope this to individual declarations, as in
```
set_option maxHeartbeats in
-- comment explaining why this is necessary
example : ... := ...
```

Note: This linter can be disabled with `set_option linter.style.setOption false`
warning: Iut/Foundations/SourceFiniteEtaleSignTorsor.lean:11667:0: Please, add a comment explaining the need for modifying the maxHeartbeat limit, as in
set_option maxHeartbeats 800000 in
-- reason for change
...

Note: This linter can be disabled with `set_option linter.style.maxHeartbeats false`
warning: Iut/Foundations/SourceFiniteEtaleSignTorsor.lean:11667:0: Unscoped option maxHeartbeats is not allowed:
Please scope this to individual declarations, as in
```
set_option maxHeartbeats in
-- comment explaining why this is necessary
example : ... := ...
```

Note: This linter can be disabled with `set_option linter.style.setOption false`
✔ [4606/6595] Built Iut.Foundations.SourceEtalePseudofunctorTwoPullbackCancellationLiftToYInv (2.8s)
✔ [4607/6595] Built Iut.Foundations.SourceFiniteEtaleAffineOverCoordinateAction (2.4s)
✔ [4609/6595] Built Iut.Foundations.SourceSingleObjOppositeEquivalence (1.6s)
✔ [4610/6595] Built Iut.Foundations.SourceCategoryPackedHEqEndpointLinkDataJoinProjections (1.4s)
✔ [4611/6595] Built Iut.Foundations.SourceEtalePseudofunctorStrongTransWhiskerRightIsoSymmHom (2.6s)
✔ [4612/6595] Built Iut.Foundations.SourceEtalePseudofunctorStrongTransPentagonInvPrefix (4.1s)
✔ [4613/6595] Built Iut.Foundations.SourceCategoryEqToHomTransportedEndpointDataMap (1.5s)
✔ [4614/6595] Built Iut.Foundations.SourceEtalePseudofunctorChangeFirstBaseMap (3.7s)
✔ [4615/6595] Built Iut.Foundations.SourceEtalePseudofunctorChangeSecondBaseMap (3.7s)
✔ [4616/6595] Built Iut.Foundations.SourceEtalePseudofunctorFaithfulCellAssembly (3.7s)
✔ [4617/6595] Built Iut.Foundations.SourceEtalePseudofunctorRepresentablePullbackTwoCell (116s)
✔ [4618/6595] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalHomPointValueRecovery (2.9s)
✔ [4619/6595] Built Iut.Foundations.SourceFiniteEtaleSchemeCoverClopenMono (2.9s)
⚠ [4620/6595] Built Iut.Foundations.SourceFiniteEtaleSignTorsorAffineEffectiveness (169s)
warning: Iut/Foundations/SourceFiniteEtaleSignTorsorAffineEffectiveness.lean:2163:58: remove line break in the source

This part of the code
  '⊗ₜ[
   '
should be written as
  '⊗ₜ[Scheme.Γ.obj'


Note: This linter can be disabled with `set_option linter.style.whitespace false`
warning: Iut/Foundations/SourceFiniteEtaleSignTorsorAffineEffectiveness.lean:2166:56: remove line break in the source

This part of the code
  '⊗ₜ[
   '
should be written as
  '⊗ₜ[Scheme.Γ.obj'


Note: This linter can be disabled with `set_option linter.style.whitespace false`
warning: Iut/Foundations/SourceFiniteEtaleSignTorsorAffineEffectiveness.lean:2169:52: remove line break in the source

This part of the code
  '⊗[
   '
should be written as
  '⊗[Scheme.Γ.obj'


Note: This linter can be disabled with `set_option linter.style.whitespace false`
warning: Iut/Foundations/SourceFiniteEtaleSignTorsorAffineEffectiveness.lean:2448:58: remove line break in the source

This part of the code
  '⊗ₜ[
   '
should be written as
  '⊗ₜ[Scheme.Γ.obj'


Note: This linter can be disabled with `set_option linter.style.whitespace false`
warning: Iut/Foundations/SourceFiniteEtaleSignTorsorAffineEffectiveness.lean:2451:56: remove line break in the source

This part of the code
  '⊗ₜ[
   '
should be written as
  '⊗ₜ[Scheme.Γ.obj'


Note: This linter can be disabled with `set_option linter.style.whitespace false`
warning: Iut/Foundations/SourceFiniteEtaleSignTorsorAffineEffectiveness.lean:2454:52: remove line break in the source

This part of the code
  '⊗[
   '
should be written as
  '⊗[Scheme.Γ.obj'


Note: This linter can be disabled with `set_option linter.style.whitespace false`
warning: Iut/Foundations/SourceFiniteEtaleSignTorsorAffineEffectiveness.lean:2460:58: remove line break in the source

This part of the code
  '⊗ₜ[
   '
should be written as
  '⊗ₜ[Scheme.Γ.obj'


Note: This linter can be disabled with `set_option linter.style.whitespace false`
warning: Iut/Foundations/SourceFiniteEtaleSignTorsorAffineEffectiveness.lean:2463:56: remove line break in the source

This part of the code
  '⊗ₜ[
   '
should be written as
  '⊗ₜ[Scheme.Γ.obj'


Note: This linter can be disabled with `set_option linter.style.whitespace false`
warning: Iut/Foundations/SourceFiniteEtaleSignTorsorAffineEffectiveness.lean:2466:52: remove line break in the source

This part of the code
  '⊗[
   '
should be written as
  '⊗[Scheme.Γ.obj'


Note: This linter can be disabled with `set_option linter.style.whitespace false`
✔ [4621/6595] Built Iut.Foundations.SourceFiniteEtaleSignQuotientPrestack (43s)
✔ [4622/6595] Built Iut.Foundations.SourceFiniteEtaleSignTorsorTargetStackDescent (2.9s)
✔ [4623/6595] Built Iut.Foundations.SourceFiniteEtaleSignTorsorTrivial (4.6s)
✔ [4624/6595] Built Iut.Foundations.SourceEtalePseudofunctorTwoPullbackCancellationLiftToYLawful (2.7s)
✔ [4626/6595] Built Iut.Foundations.SourceFiniteEtaleAffineOverCoordinateFiniteEtale (2.5s)
✔ [4627/6595] Built Iut.Foundations.SourceCategoryPackedHEqTwoMorphismComposition (1.5s)
✔ [4628/6595] Built Iut.Foundations.SourceEtaleStackRepresentablePropertyChangeMap (2.8s)
✔ [4629/6595] Built Iut.Foundations.SourceEtalePseudofunctorConeAfterChangeSecondBaseMap (2.9s)
✔ [4630/6595] Built Iut.Foundations.SourceEtalePseudofunctorRepresentedIsoPointLift (3.2s)
✔ [4631/6595] Built Iut.Foundations.SourceEtalePseudofunctorRepresentablePullbackWitness (2.8s)
✔ [4632/6595] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalHomYonedaPointValue (2.7s)
✔ [4633/6595] Built Iut.Foundations.SourceFiniteEtaleSchemeCoverDirectSummand (3.2s)
✔ [4634/6595] Built Iut.Foundations.SourceFiniteEtaleSchemeCoverUnderlyingEpiRange (2.8s)
⚠ [4635/6595] Built Iut.Foundations.SourceFiniteEtaleSignTorsorAffineCoverCollapse (10s)
warning: Iut/Foundations/SourceFiniteEtaleSignTorsorAffineCoverCollapse.lean:1268:2: try 'simp' instead of 'simpa'

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`
✔ [4636/6595] Built Iut.Foundations.SourceFiniteEtaleSignQuotientStackCriterion (2.0s)
✔ [4637/6595] Built Iut.Foundations.SourceFiniteEtaleSignQuotientAtlas (5.6s)
✔ [4638/6598] Built Iut.Foundations.SourceEtalePseudofunctorTwoPullbackCancellationLiftToYHomToX (2.8s)
✔ [4639/6599] Built Iut.Foundations.SourceEtalePseudofunctorConeAfterChangeSecondBaseMapFromConeOf (3.0s)
✔ [4640/6599] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalIsoBaseChangeOver (3.3s)
✔ [4641/6599] Built Iut.Foundations.SourceRepresentableStrongTransReconstruction (3.1s)
✔ [4642/6599] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalHomYonedaNaturality (2.9s)
✔ [4643/6599] Built Iut.Foundations.SourceFiniteEtaleSchemeCoverAffineSource (2.8s)
✔ [4644/6599] Built Iut.Foundations.SourceFiniteEtaleSchemeCoverUnderlyingEpiSurjective (7.0s)
⚠ [4645/6599] Built Iut.Foundations.SourceFiniteEtaleSignTorsorAffineCoverAssembly (875s)
warning: Iut/Foundations/SourceFiniteEtaleSignTorsorAffineCoverAssembly.lean:1177:0: Please, add a comment explaining the need for modifying the maxHeartbeat limit, as in
set_option maxHeartbeats 400000 in
-- reason for change
...

Note: This linter can be disabled with `set_option linter.style.maxHeartbeats false`
warning: Iut/Foundations/SourceFiniteEtaleSignTorsorAffineCoverAssembly.lean:1268:0: Please, add a comment explaining the need for modifying the maxHeartbeat limit, as in
set_option maxHeartbeats 400000 in
-- reason for change
...

Note: This linter can be disabled with `set_option linter.style.maxHeartbeats false`
warning: Iut/Foundations/SourceFiniteEtaleSignTorsorAffineCoverAssembly.lean:1329:0: Please, add a comment explaining the need for modifying the maxHeartbeat limit, as in
set_option maxHeartbeats 400000 in
-- reason for change
...

Note: This linter can be disabled with `set_option linter.style.maxHeartbeats false`
warning: Iut/Foundations/SourceFiniteEtaleSignTorsorAffineCoverAssembly.lean:1409:0: Please, add a comment explaining the need for modifying the maxHeartbeat limit, as in
set_option maxHeartbeats 400000 in
-- reason for change
...

Note: This linter can be disabled with `set_option linter.style.maxHeartbeats false`
warning: Iut/Foundations/SourceFiniteEtaleSignTorsorAffineCoverAssembly.lean:2812:0: Please, add a comment explaining the need for modifying the maxHeartbeat limit, as in
set_option maxHeartbeats 400000 in
-- reason for change
...

Note: This linter can be disabled with `set_option linter.style.maxHeartbeats false`
warning: Iut/Foundations/SourceFiniteEtaleSignTorsorAffineCoverAssembly.lean:2917:0: Please, add a comment explaining the need for modifying the maxHeartbeat limit, as in
set_option maxHeartbeats 400000 in
-- reason for change
...

Note: This linter can be disabled with `set_option linter.style.maxHeartbeats false`
warning: Iut/Foundations/SourceFiniteEtaleSignTorsorAffineCoverAssembly.lean:3052:0: Please, add a comment explaining the need for modifying the maxHeartbeat limit, as in
set_option maxHeartbeats 400000 in
-- reason for change
...

Note: This linter can be disabled with `set_option linter.style.maxHeartbeats false`
warning: Iut/Foundations/SourceFiniteEtaleSignTorsorAffineCoverAssembly.lean:3103:0: Please, add a comment explaining the need for modifying the maxHeartbeat limit, as in
set_option maxHeartbeats 400000 in
-- reason for change
...

Note: This linter can be disabled with `set_option linter.style.maxHeartbeats false`
warning: Iut/Foundations/SourceFiniteEtaleSignTorsorAffineCoverAssembly.lean:3150:0: Please, add a comment explaining the need for modifying the maxHeartbeat limit, as in
set_option maxHeartbeats 400000 in
-- reason for change
...

Note: This linter can be disabled with `set_option linter.style.maxHeartbeats false`
warning: Iut/Foundations/SourceFiniteEtaleSignTorsorAffineCoverAssembly.lean:3191:0: Please, add a comment explaining the need for modifying the maxHeartbeat limit, as in
set_option maxHeartbeats 400000 in
-- reason for change
...

Note: This linter can be disabled with `set_option linter.style.maxHeartbeats false`
warning: Iut/Foundations/SourceFiniteEtaleSignTorsorAffineCoverAssembly.lean:3572:0: Please, add a comment explaining the need for modifying the maxHeartbeat limit, as in
set_option maxHeartbeats 400000 in
-- reason for change
...

Note: This linter can be disabled with `set_option linter.style.maxHeartbeats false`
warning: Iut/Foundations/SourceFiniteEtaleSignTorsorAffineCoverAssembly.lean:3699:0: Please, add a comment explaining the need for modifying the maxHeartbeat limit, as in
set_option maxHeartbeats 400000 in
-- reason for change
...

Note: This linter can be disabled with `set_option linter.style.maxHeartbeats false`
warning: Iut/Foundations/SourceFiniteEtaleSignTorsorAffineCoverAssembly.lean:3826:0: Please, add a comment explaining the need for modifying the maxHeartbeat limit, as in
set_option maxHeartbeats 400000 in
-- reason for change
...

Note: This linter can be disabled with `set_option linter.style.maxHeartbeats false`
warning: Iut/Foundations/SourceFiniteEtaleSignTorsorAffineCoverAssembly.lean:3958:0: Please, add a comment explaining the need for modifying the maxHeartbeat limit, as in
set_option maxHeartbeats 400000 in
-- reason for change
...

Note: This linter can be disabled with `set_option linter.style.maxHeartbeats false`
warning: Iut/Foundations/SourceFiniteEtaleSignTorsorAffineCoverAssembly.lean:4089:0: Please, add a comment explaining the need for modifying the maxHeartbeat limit, as in
set_option maxHeartbeats 400000 in
-- reason for change
...

Note: This linter can be disabled with `set_option linter.style.maxHeartbeats false`
warning: Iut/Foundations/SourceFiniteEtaleSignTorsorAffineCoverAssembly.lean:4266:0: Please, add a comment explaining the need for modifying the maxHeartbeat limit, as in
set_option maxHeartbeats 400000 in
-- reason for change
...

Note: This linter can be disabled with `set_option linter.style.maxHeartbeats false`
warning: Iut/Foundations/SourceFiniteEtaleSignTorsorAffineCoverAssembly.lean:4420:0: Please, add a comment explaining the need for modifying the maxHeartbeat limit, as in
set_option maxHeartbeats 400000 in
-- reason for change
...

Note: This linter can be disabled with `set_option linter.style.maxHeartbeats false`
warning: Iut/Foundations/SourceFiniteEtaleSignTorsorAffineCoverAssembly.lean:4586:0: Please, add a comment explaining the need for modifying the maxHeartbeat limit, as in
set_option maxHeartbeats 400000 in
-- reason for change
...

Note: This linter can be disabled with `set_option linter.style.maxHeartbeats false`
warning: Iut/Foundations/SourceFiniteEtaleSignTorsorAffineCoverAssembly.lean:5027:0: Please, add a comment explaining the need for modifying the maxHeartbeat limit, as in
set_option maxHeartbeats 400000 in
-- reason for change
...

Note: This linter can be disabled with `set_option linter.style.maxHeartbeats false`
warning: Iut/Foundations/SourceFiniteEtaleSignTorsorAffineCoverAssembly.lean:5159:0: Please, add a comment explaining the need for modifying the maxHeartbeat limit, as in
set_option maxHeartbeats 400000 in
-- reason for change
...

Note: This linter can be disabled with `set_option linter.style.maxHeartbeats false`
warning: Iut/Foundations/SourceFiniteEtaleSignTorsorAffineCoverAssembly.lean:5333:0: Please, add a comment explaining the need for modifying the maxHeartbeat limit, as in
set_option maxHeartbeats 400000 in
-- reason for change
...

Note: This linter can be disabled with `set_option linter.style.maxHeartbeats false`
warning: Iut/Foundations/SourceFiniteEtaleSignTorsorAffineCoverAssembly.lean:5438:0: Please, add a comment explaining the need for modifying the maxHeartbeat limit, as in
set_option maxHeartbeats 1600000 in
-- reason for change
...

Note: This linter can be disabled with `set_option linter.style.maxHeartbeats false`
warning: Iut/Foundations/SourceFiniteEtaleSignTorsorAffineCoverAssembly.lean:5573:0: Please, add a comment explaining the need for modifying the maxHeartbeat limit, as in
set_option maxHeartbeats 400000 in
-- reason for change
...

Note: This linter can be disabled with `set_option linter.style.maxHeartbeats false`
warning: Iut/Foundations/SourceFiniteEtaleSignTorsorAffineCoverAssembly.lean:5687:0: Please, add a comment explaining the need for modifying the maxHeartbeat limit, as in
set_option maxHeartbeats 4000000 in
-- reason for change
...

Note: This linter can be disabled with `set_option linter.style.maxHeartbeats false`
warning: Iut/Foundations/SourceFiniteEtaleSignTorsorAffineCoverAssembly.lean:5764:0: Please, add a comment explaining the need for modifying the maxHeartbeat limit, as in
set_option maxHeartbeats 800000 in
-- reason for change
...

Note: This linter can be disabled with `set_option linter.style.maxHeartbeats false`
warning: Iut/Foundations/SourceFiniteEtaleSignTorsorAffineCoverAssembly.lean:5813:0: Please, add a comment explaining the need for modifying the maxHeartbeat limit, as in
set_option maxHeartbeats 1600000 in
-- reason for change
...

Note: This linter can be disabled with `set_option linter.style.maxHeartbeats false`
warning: Iut/Foundations/SourceFiniteEtaleSignTorsorAffineCoverAssembly.lean:5904:0: Please, add a comment explaining the need for modifying the maxHeartbeat limit, as in
set_option maxHeartbeats 800000 in
-- reason for change
...

Note: This linter can be disabled with `set_option linter.style.maxHeartbeats false`
warning: Iut/Foundations/SourceFiniteEtaleSignTorsorAffineCoverAssembly.lean:5965:0: Please, add a comment explaining the need for modifying the maxHeartbeat limit, as in
set_option maxHeartbeats 800000 in
-- reason for change
...

Note: This linter can be disabled with `set_option linter.style.maxHeartbeats false`
warning: Iut/Foundations/SourceFiniteEtaleSignTorsorAffineCoverAssembly.lean:6033:0: Please, add a comment explaining the need for modifying the maxHeartbeat limit, as in
set_option maxHeartbeats 800000 in
-- reason for change
...

Note: This linter can be disabled with `set_option linter.style.maxHeartbeats false`
warning: Iut/Foundations/SourceFiniteEtaleSignTorsorAffineCoverAssembly.lean:6088:0: Please, add a comment explaining the need for modifying the maxHeartbeat limit, as in
set_option maxHeartbeats 800000 in
-- reason for change
...

Note: This linter can be disabled with `set_option linter.style.maxHeartbeats false`
warning: Iut/Foundations/SourceFiniteEtaleSignTorsorAffineCoverAssembly.lean:6128:0: Please, add a comment explaining the need for modifying the maxHeartbeat limit, as in
set_option maxHeartbeats 800000 in
-- reason for change
...

Note: This linter can be disabled with `set_option linter.style.maxHeartbeats false`
warning: Iut/Foundations/SourceFiniteEtaleSignTorsorAffineCoverAssembly.lean:6211:0: Please, add a comment explaining the need for modifying the maxHeartbeat limit, as in
set_option maxHeartbeats 800000 in
-- reason for change
...

Note: This linter can be disabled with `set_option linter.style.maxHeartbeats false`
warning: Iut/Foundations/SourceFiniteEtaleSignTorsorAffineCoverAssembly.lean:6460:100: This line exceeds the 100 character limit, please shorten it!

Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Foundations/SourceFiniteEtaleSignTorsorAffineCoverAssembly.lean:6815:0: Please, add a comment explaining the need for modifying the maxHeartbeat limit, as in
set_option maxHeartbeats 800000 in
-- reason for change
...

Note: This linter can be disabled with `set_option linter.style.maxHeartbeats false`
✔ [4646/6599] Built Iut.Foundations.SourceFiniteEtaleSignQuotientAtlasBaseChange (16s)
✔ [4647/6599] Built Iut.Foundations.SourceEtalePseudofunctorTwoPullbackCancellationLiftToYHomToY (2.7s)
✔ [4650/6599] Built Iut.Foundations.SourceEtaleStackRepresentableLocalIsoDescent (3.8s)
✔ [4651/6599] Built Iut.Foundations.SourceEtaleStackSchemeAtlasOverlapMultiplication (3.1s)
✔ [4652/6599] Built Iut.Foundations.SourceEtalePseudofunctorRepresentablePullbackAlongStrongTrans (3.8s)
✔ [4653/6599] Built Iut.Foundations.SourceFiniteEtaleSchemeCoverAffineGroupQuotient (3.1s)
✔ [4654/6599] Built Iut.Foundations.SourceFiniteEtaleSchemeCoverBalanced (2.5s)
✔ [4655/6599] Built Iut.Foundations.SourceFiniteEtaleSignTorsorAffineCoverRestriction (124s)
✔ [4656/6599] Built Iut.Foundations.SourceFiniteEtaleSignQuotientAtlasLiftApp (121s)
✔ [4657/6599] Built Iut.Foundations.SourceFiniteEtaleSignQuotientAtlasInvariant (3.5s)
✔ [4658/6599] Built Iut.Foundations.SourceEtalePseudofunctorTwoPullbackCancellationLiftCompatibility (2.7s)
✔ [4660/6600] Built Iut.Foundations.SourceEtaleStackRepresentableAtlasLocalIsoDescent (3.1s)
✔ [4661/6600] Built Iut.Foundations.SourceOrbicurveFiniteEtaleBaseChangeSchemeCoverMapReflectsLocalIso (3.3s)
✔ [4662/6602] Built Iut.Foundations.SourceEtaleStackSchemeAtlasOverlapMultiplicationRepresentedLongConeIso (2.9s)
✔ [4663/6602] Built Iut.Foundations.SourceEtaleStackSchemeAtlasOverlapConePasting (2.0s)
✔ [4664/6602] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapCechData (3.1s)
✔ [4665/6602] Built Iut.Foundations.SourceEtaleStackSchemeAtlasFiniteEtaleDescent (3.3s)
✔ [4666/6602] Built Iut.Foundations.SourceOrbicurveFiniteEtaleIteratedBaseChange (9.5s)
✔ [4667/6602] Built Iut.Foundations.SourceFiniteEtaleSchemeCoverAffineOverFullyFaithful (2.7s)
✔ [4668/6602] Built Iut.Foundations.SourceFiniteEtaleFixedSubalgebra (3.1s)
✔ [4669/6602] Built Iut.Foundations.SourceFiniteEtaleSignTorsorAffineCoverFiniteEffectivity (3.6s)
✔ [4670/6602] Built Iut.Foundations.SourceFiniteEtaleSignQuotientAtlasLiftNaturality (104s)
✔ [4671/6602] Built Iut.Foundations.SourceFiniteEtaleSignQuotientAtlasInvariantElement (3.1s)
✔ [4672/6604] Built Iut.Foundations.SourceEtalePseudofunctorTwoPullbackCancellationConeMorphismCompatibility (3.0s)
✔ [4676/6604] Built Iut.Foundations.SourceEtaleStackSchemeAtlasOverlapConePastingIso (4.1s)
✔ [4677/6604] Built Iut.Foundations.SourceEtaleStackSchemeAtlasOverlapConePastingCell (2.9s)
✔ [4678/6604] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapRestrictionCongrIsoNaturality (3.1s)
✔ [4679/6604] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapRestrictionCongrIsoWhiskerRightFactorization (3.0s)
✔ [4680/6604] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapOverlapNestedMiddleIso (2.8s)
✔ [4681/6604] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapPointObject (2.8s)
✔ [4682/6604] Built Iut.Foundations.SourceEtaleStackSchemeAtlasFiniteEtaleDescentComparison (3.2s)
✔ [4683/6604] Built Iut.Foundations.SourceEtaleStackSchemeAtlasMapCechEndpointIsos (2.9s)
✔ [4684/6604] Built Iut.Foundations.SourceEtaleStackSchemeAtlasBaseChangePointIso (3.0s)
✔ [4685/6604] Built Iut.Foundations.SourceOrbicurveFiniteEtaleIteratedBaseChangeForwardBackLiftedHom (3.3s)
✔ [4686/6604] Built Iut.Foundations.SourceEtaleStackSchemeAtlasOverlapMapIso (2.7s)
✔ [4687/6604] Built Iut.Foundations.SourceOrbicurveFiniteEtaleIteratedBaseChangeToSourceIso (2.0s)
✔ [4688/6604] Built Iut.Foundations.SourceFiniteEtaleFixedAffineQuotient (3.1s)
✔ [4689/6604] Built Iut.Foundations.SourceFiniteEtaleSignTorsorAffineRefinement (3.6s)
✔ [4690/6604] Built Iut.Foundations.SourceFiniteEtaleSignQuotientAtlasLift (3.1s)
✔ [4691/6604] Built Iut.Foundations.SourceFiniteEtaleSignQuotientAtlasInvariantComponent (25s)
✔ [4692/6605] Built Iut.Foundations.SourceEtalePseudofunctorTwoPullbackCancellationConeMorphism (3.4s)
✔ [4695/6605] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapOverlapNestedMiddleHom (2.9s)
✔ [4696/6605] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapOverlapNestedEndpointIsos (2.7s)
✔ [4697/6605] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapPointOverlap (3.1s)
✔ [4698/6605] Built Iut.Foundations.SourceEtaleStackSchemeAtlasFiniteEtaleDescentConstruction (42s)
✔ [4699/6605] Built Iut.Foundations.SourceEtaleStackSchemeAtlasMapCechPairMiddleIso (3.1s)
✔ [4700/6605] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalHomPointIsoValue (3.1s)
✔ [4701/6605] Built Iut.Foundations.SourceOrbicurveFiniteEtaleIteratedBaseChangeForwardBackLiftedHomComparison (2.9s)
✔ [4702/6605] Built Iut.Foundations.SourceFiniteEtaleOrbitConstantAlgebra (2.0s)
✔ [4703/6605] Built Iut.Foundations.SourceFiniteEtaleSignQuotientStackRefinement (2.0s)
✔ [4704/6605] Built Iut.Foundations.SourceFiniteEtaleSignQuotientAtlasLiftProjections (12s)
✔ [4705/6605] Built Iut.Foundations.SourceFiniteEtaleSignQuotientAtlasInvariantCocycle (19s)
✔ [4706/6607] Built Iut.Foundations.SourceEtalePseudofunctorTwoPullbackCancellationTwoCell (2.5s)
✔ [4709/6607] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapOverlapNestedMiddleCompositeFactorization (3.1s)
✔ [4710/6607] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapPullbackOverlapNestedFactorization (3.4s)
✔ [4711/6607] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapPointTransition (3.3s)
✔ [4712/6607] Built Iut.Foundations.SourceOrbicurveFiniteEtaleBaseChangePointIsoToSourceIso (2.7s)
✔ [4713/6607] Built Iut.Foundations.SourceEtaleStackSchemeAtlasFiniteEtaleDescentCoherence (13s)
✔ [4714/6607] Built Iut.Foundations.SourceEtaleStackSchemeAtlasMapCechPairFactorization (22s)
✔ [4715/6607] Built Iut.Foundations.SourceOrbicurveFiniteEtaleIteratedBaseChangeForwardBackStrongTransToSource (2.0s)
✔ [4716/6607] Built Iut.Foundations.SourceFiniteEtaleSplitAlgebraHom (3.1s)
✔ [4717/6607] Built Iut.Foundations.SourceFiniteEtaleSignQuotientAffineChartDescent (16s)
✔ [4718/6607] Built Iut.Foundations.SourceFiniteEtaleSignQuotientAtlasLiftTwoCell (287s)
✔ [4719/6607] Built Iut.Foundations.SourceFiniteEtaleSignQuotientAtlasLiftUnit (15s)
✔ [4720/6609] Built Iut.Foundations.SourceEtalePseudofunctorTwoPullbackCancellationTwoCellToX (2.6s)
✔ [4722/6609] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapOverlapNestedMiddleCompositeTargetCollapse (3.1s)
✔ [4723/6609] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapOverlapNestedMiddleCompositeSourceCollapse (2.0s)
✔ [4724/6609] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapOverlapNestedSpecializations (3.1s)
✔ [4725/6609] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapOverlapCompositeWhiskeredExpansion (3.0s)
✔ [4726/6609] Built Iut.Foundations.SourceEtaleRepresentedRestrictionPointIsoCongruenceTail (3.0s)
✔ [4727/6609] Built Iut.Foundations.SourceEtaleRepresentedStrongTransPointIsoWhiskerRightHom (2.9s)
✔ [4728/6609] Built Iut.Foundations.SourceEtaleRepresentedStrongTransPointIsoWhiskerLeft (3.8s)
✔ [4729/6609] Built Iut.Foundations.SourceEtaleRepresentedStrongTransPointIsoSymmHom (2.8s)
✔ [4730/6609] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapPointOverlapValueIsoRepresented (2.9s)
✔ [4731/6609] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapPointCocycleGeometry (3.2s)
✔ [4732/6609] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapCechCocyclePointValue (2.9s)
✔ [4733/6609] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapRestrictionCompositePointIsoHom (6.8s)
⚠ [4734/6609] Built Iut.Foundations.SourceEtaleRepresentedStrongTransPointIsoTransHom (2.0s)
warning: Iut/Foundations/SourceEtaleRepresentedStrongTransPointIsoTransHom.lean:26:0: Please, add a comment explaining the need for modifying the maxHeartbeat limit, as in
set_option maxHeartbeats 800000 in
-- reason for change
...

Note: This linter can be disabled with `set_option linter.style.maxHeartbeats false`
✔ [4735/6609] Built Iut.Foundations.SourceOrbicurveFiniteEtaleBaseChangePointIsoToSourceCompatibility (3.1s)
✔ [4736/6609] Built Iut.Foundations.SourceEtaleRepresentedStrongTransPointIsoCongruenceAssociator (3.1s)
✔ [4737/6609] Built Iut.Foundations.SourceEtaleStackSchemeAtlasFiniteEtaleCoverOverlapComparisonLeft (2.9s)
✔ [4738/6609] Built Iut.Foundations.SourceEtaleStackSchemeAtlasFiniteEtaleCanonicalDescentStructureComparison (2.9s)
✔ [4739/6609] Built Iut.Foundations.SourceEtaleStackSchemeAtlasMapCechPairLongFactorization (3.1s)
✔ [4740/6609] Built Iut.Foundations.SourceOrbicurveFiniteEtaleIteratedBaseChangeForwardBackRealizationToSourceExpansion (3.1s)
✔ [4741/6609] Built Iut.Foundations.SourceFiniteEtaleSplitAlgebraAutomorphism (2.7s)
✔ [4742/6609] Built Iut.Foundations.SourceFiniteEtaleSignQuotientAffineChartGluing (8.4s)
✔ [4743/6609] Built Iut.Foundations.SourceFiniteEtaleSignQuotientAtlasLiftCompatibility (18s)
✔ [4744/6610] Built Iut.Foundations.SourceEtalePseudofunctorTwoPullbackCancellationTwoCellYTarget (2.5s)
✔ [4747/6610] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapOverlapNestedMiddleTargetAssociatorNaturality (2.9s)
✔ [4748/6610] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapOverlapNestedMiddleDirectTargetNaturalityEndpoints (2.8s)
✔ [4749/6610] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapOverlapNestedMiddleAttached (3.0s)
✔ [4750/6610] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapOverlapCompositeWhiskeredEndpointIsos (2.9s)
⚠ [4751/6620] Built Iut.Foundations.SourceEtaleRepresentedStrongTransPointIsoWhiskerLeftTargetTransport (2.9s)
warning: Iut/Foundations/SourceEtaleRepresentedStrongTransPointIsoWhiskerLeftTargetTransport.lean:44:13: This simp argument is unused:
  Category.assoc

Hint: Omit it from the simp argument list.
  simp only [C̵a̵t̵e̵g̵o̵r̵y̵.̵a̵s̵s̵o̵c̵,̵ ̵Iso.inv_hom_id_assoc]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Iut/Foundations/SourceEtaleRepresentedStrongTransPointIsoWhiskerLeftTargetTransport.lean:26:0: Please, add a comment explaining the need for modifying the maxHeartbeat limit, as in
set_option maxHeartbeats 800000 in
-- reason for change
...

Note: This linter can be disabled with `set_option linter.style.maxHeartbeats false`
✔ [4752/6635] Built Iut.Foundations.SourceEtaleRepresentedStrongTransPointIsoWhiskerLeftInv (2.0s)
✔ [4753/6635] Built Iut.Foundations.SourceEtaleRepresentedStrongTransPointIsoWhiskerLeftSourceTransport (2.0s)
✔ [4754/6635] Built Iut.Foundations.SourceEtaleRepresentedStrongTransPointIsoSymmInv (2.9s)
✔ [4755/6635] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapPointTripleRawCompositorTailHom (2.9s)
✔ [4756/6635] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapPointTripleBaseInverseTail (3.0s)
✔ [4757/6635] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapPointLongEdgeEndpoints (3.5s)
✔ [4758/6635] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapCechCocyclePointTripleValue (3.0s)
✔ [4759/6635] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapPointOverlapValueDirectFactorData (2.9s)
⚠ [4760/6635] Built Iut.Foundations.SourceEtaleRepresentedStrongTransPointIsoTransInv (2.9s)
warning: Iut/Foundations/SourceEtaleRepresentedStrongTransPointIsoTransInv.lean:26:0: Please, add a comment explaining the need for modifying the maxHeartbeat limit, as in
set_option maxHeartbeats 800000 in
-- reason for change
...

Note: This linter can be disabled with `set_option linter.style.maxHeartbeats false`
✔ [4761/6635] Built Iut.Foundations.SourceEtaleRepresentedStrongTransPointIsoPentagonHom (3.0s)
✔ [4762/6635] Built Iut.Foundations.SourceEtaleRepresentedStrongTransPointIsoWhiskerRightTransHom (3.0s)
✔ [4763/6635] Built Iut.Foundations.SourceEtaleRepresentedStrongTransPointIsoAssociatorEqToHom (2.9s)
✔ [4764/6635] Built Iut.Foundations.SourceEtaleRepresentedStrongTransPointIsoCongruenceSymmInvAssociator (3.1s)
✔ [4765/6635] Built Iut.Foundations.SourceEtaleStackSchemeAtlasSourceAtlasOverlapCanonicalComparisonLeftFactorIso (2.9s)
✔ [4766/6635] Built Iut.Foundations.SourceEtaleStackSchemeAtlasFiniteEtaleCanonicalDescentStructureComparisonLeft (2.9s)
✔ [4767/6635] Built Iut.Foundations.SourceEtaleStackSchemeAtlasMapCechCompositeFactorization (12s)
✔ [4768/6635] Built Iut.Foundations.SourceOrbicurveFiniteEtaleIteratedBaseChangeForwardBackToSourceExpansion (3.0s)
✔ [4769/6635] Built Iut.Foundations.SourceFiniteEtaleSplitActionFixedAlgebra (4.0s)
✔ [4770/6635] Built Iut.Foundations.SourceFiniteEtaleSignQuotientAffineChartRelativeGluing (3.7s)
✔ [4771/6635] Built Iut.Foundations.SourceFiniteEtaleSignQuotientAtlasLiftWitness (18s)
✔ [4772/6750] Built Iut.Foundations.SourceEtalePseudofunctorTwoPullbackCancellationLiftToYInvToY (2.7s)
✔ [4775/6750] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapOverlapNestedMiddleDirectTargetNaturalityEndpointExpansions (2.9s)
✔ [4776/6750] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapOverlapNestedMiddleDirectTargetNaturalityMiddleRight (2.0s)
✔ [4777/6750] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapOverlapPairWhiskeredExpansion (3.1s)
✔ [4778/6750] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapOverlapCompositeWhiskeredEndpointFactorization (2.0s)
✔ [4779/6750] Built Iut.Foundations.SourceEtaleRepresentedStrongTransPointIsoWhiskerLeftTargetTransportData (2.9s)
✔ [4781/6750] Built Iut.Foundations.SourceFiniteEtaleSchemeCoverGeometricFiberFunctor (2.8s)
✔ [4782/6750] Built Iut.Foundations.SourceSpecFieldSchemeCoproductMaps (2.4s)
✔ [4783/6750] Built Iut.Foundations.SourceFiniteEtaleInvariantAlgHomOrbit (2.6s)
✔ [4784/6750] Built Iut.Foundations.SourceSingleObjTypesOrbitColimit (1.7s)
✔ [4785/6750] Built Iut.Foundations.SourceEtaleRepresentedStrongTransPointIsoWhiskerLeftSymmHom (2.9s)
⚠ [4786/6750] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapPointTripleRepresentedSourceObjects (3.3s)
warning: Iut/Foundations/SourceEtaleStackSchemeAtlasLocalMapPointTripleRepresentedSourceObjects.lean:27:0: Please, add a comment explaining the need for modifying the maxHeartbeat limit, as in
set_option maxHeartbeats 800000 in
-- reason for change
...

Note: This linter can be disabled with `set_option linter.style.maxHeartbeats false`
warning: Iut/Foundations/SourceEtaleStackSchemeAtlasLocalMapPointTripleRepresentedSourceObjects.lean:59:0: Please, add a comment explaining the need for modifying the maxHeartbeat limit, as in
set_option maxHeartbeats 800000 in
-- reason for change
...

Note: This linter can be disabled with `set_option linter.style.maxHeartbeats false`
✔ [4787/6750] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapPointTripleBaseInverseTailLeftHom (3.2s)
✔ [4788/6750] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapPointTripleCocycleMiddleValueIsos (3.0s)
✔ [4789/6750] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapPointTripleEdgeIso (3.2s)
✔ [4790/6750] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapPointTripleCocycleEndpointValueIso (3.0s)
⚠ [4791/6750] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapPointOverlapValueDirectFactorDataEndpoints (3.0s)
warning: Iut/Foundations/SourceEtaleStackSchemeAtlasLocalMapPointOverlapValueDirectFactorDataEndpoints.lean:27:0: Please, add a comment explaining the need for modifying the maxHeartbeat limit, as in
set_option maxHeartbeats 800000 in
-- reason for change
...

Note: This linter can be disabled with `set_option linter.style.maxHeartbeats false`
warning: Iut/Foundations/SourceEtaleStackSchemeAtlasLocalMapPointOverlapValueDirectFactorDataEndpoints.lean:45:0: Please, add a comment explaining the need for modifying the maxHeartbeat limit, as in
set_option maxHeartbeats 800000 in
-- reason for change
...

Note: This linter can be disabled with `set_option linter.style.maxHeartbeats false`
✔ [4792/6750] Built Iut.Foundations.SourceEtaleRepresentedStrongTransPointIsoWhiskerLeftTransInv (2.9s)
✔ [4793/6750] Built Iut.Foundations.SourceEtaleRepresentedStrongTransPointIsoWhiskerRightTransInv (3.1s)
✔ [4794/6750] Built Iut.Foundations.SourceEtaleRepresentedStrongTransPointIsoPentagonInv (3.0s)
✔ [4795/6750] Built Iut.Foundations.SourceEtaleRepresentedStrongTransPointIsoAssociatorNaturalityLeft (2.0s)
✔ [4796/6750] Built Iut.Foundations.SourceEtaleRepresentedStrongTransPointIsoAssociatorNaturalityMiddle (2.0s)
✔ [4797/6750] Built Iut.Foundations.SourceEtaleRepresentedStrongTransPointIsoAssociatorInvEqToHom (3.0s)
✔ [4798/6849] Built Iut.Foundations.SourceEtaleRepresentedStrongTransPointIsoCongruenceSymmInvAssociatorRestrictionTail (3.1s)
✔ [4799/8799] Built Iut.Foundations.SourceEtaleStackSchemeAtlasSourceAtlasOverlapCanonicalComparisonLeftExpandedIso (2.8s)
✔ [4800/8799] Built Iut.Foundations.SourceEtaleStackSchemeAtlasMapCechConeEndpointIsos (2.9s)
✔ [4801/8799] Built Iut.Foundations.SourceFiniteEtaleFixedSubalgebraBaseChange (3.2s)
✔ [4802/8799] Built Iut.Foundations.SourceFiniteEtaleSignQuotientAffineChartIdentityCoherence (539s)
✔ [4803/8799] Built Iut.Foundations.SourceFiniteEtaleSignQuotientAffineChartEffectivity (2.9s)
✔ [4804/8799] Built Iut.Foundations.SourceFiniteEtaleSignQuotientOrbicurve (196s)
✔ [4805/8799] Built Iut.Foundations.SourceEtalePseudofunctorTwoPullbackCancellationNestedWhisker (2.8s)
✔ [4807/8799] Built Iut.Foundations.SourceFiniteEtaleSchemeCoverRepresentable (3.8s)
✔ [4808/8799] Built Iut.Foundations.SourceSchemeEtaleStackPresentationFiniteEtaleCoverFunctor (2.9s)
✔ [4809/8799] Built Iut.Foundations.SourceEtalePseudofunctorContractiblePullback (3.6s)
✔ [4810/8799] Built Iut.Foundations.SourcePreGaloisCategoryEquivalenceTransport (1.9s)
✔ [4811/8799] Built Iut.Foundations.SourcePuncturedWeierstrassSchemeBaseChange (4.4s)
✔ [4812/8799] Built Iut.Foundations.SourceChosenPullbackFunctoriality (1.9s)
✔ [4813/8799] Built Iut.Foundations.SourceSchemeOverFieldRestrictScalarsEtaleSite (2.7s)
✔ [4814/8799] Built Iut.Foundations.SourceOrbicurveEtaleFundamentalGroupTransport (3.0s)
✔ [4815/8799] Built Iut.Foundations.SourceFiniteEtaleSchemeCoverSliceEquivalence (3.0s)
✔ [4816/8799] Built Iut.Foundations.SourceEquivalenceMateNaturality (1.6s)
✔ [4817/8799] Built Iut.Foundations.SourcePseudofunctorStrongTransIsoOfComponents (3.2s)
✔ [4818/8799] Built Iut.Foundations.SourceAnabelioidEquivalence (3.1s)
✔ [4819/8799] Built Iut.Foundations.SourceAnabelioidDominatingPullbackInjectivity (2.9s)
✔ [4820/8799] Built Iut.Foundations.SourceCategoryIsoConjugationInverseCancellation (1.4s)
✔ [4821/8799] Built Iut.Foundations.SourceFiniteEtalePresentedQuotientBaseChange (1.8s)
✔ [4822/8991] Built Iut.Foundations.SourceIdealQuotientEquivComparison (1.8s)
✔ [4823/8991] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapOverlapPairWhiskeredNested (3.0s)
✔ [4824/8991] Built Iut.Foundations.SourceEtaleRepresentedStrongTransPointIsoWhiskerLeftTargetTransportRightData (2.8s)
✔ [4826/8991] Built Iut.Foundations.SourceFiniteEtaleSchemeCoverGeometricFiberPullbacks (2.6s)
✔ [4827/8991] Built Iut.Foundations.SourceEtaleRepresentedStrongTransPointIsoWhiskerLeftSymmInv (3.0s)
⚠ [4828/8991] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapPointTripleNaturalityAppTransportData (2.8s)
warning: Iut/Foundations/SourceEtaleStackSchemeAtlasLocalMapPointTripleNaturalityAppTransportData.lean:28:0: Please, add a comment explaining the need for modifying the maxHeartbeat limit, as in
set_option maxHeartbeats 800000 in
-- reason for change
...

Note: This linter can be disabled with `set_option linter.style.maxHeartbeats false`
✔ [4829/8991] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapPointTripleRepresentedSourceCompositor (3.0s)
⚠ [4830/8991] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapPointTripleRepresentedSourceCell (3.4s)
warning: Iut/Foundations/SourceEtaleStackSchemeAtlasLocalMapPointTripleRepresentedSourceCell.lean:27:0: Please, add a comment explaining the need for modifying the maxHeartbeat limit, as in
set_option maxHeartbeats 800000 in
-- reason for change
...

Note: This linter can be disabled with `set_option linter.style.maxHeartbeats false`
✔ [4831/8991] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapPointTripleBaseInverseTailLeftHomProjection (3.2s)
✔ [4832/8991] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapPointTripleCocycleBaseInverseTerminalHom (3.0s)
✔ [4833/8991] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapPointTripleCocycleNormalizedAtlasMiddleHom (2.9s)
✔ [4834/8991] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapPointTripleEdgeConeIso (3.0s)
⚠ [4835/8991] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapPointTripleCocycleToTwoValueIsoHom (3.1s)
warning: Iut/Foundations/SourceEtaleStackSchemeAtlasLocalMapPointTripleCocycleToTwoValueIsoHom.lean:27:0: Please, add a comment explaining the need for modifying the maxHeartbeat limit, as in
set_option maxHeartbeats 800000 in
-- reason for change
...

Note: This linter can be disabled with `set_option linter.style.maxHeartbeats false`
✔ [4836/8991] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapPointTripleOverlapCompositeTargetToCocycleHom (2.9s)
✔ [4837/8991] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapPointTripleCocycleToZeroValueIsoHom (3.2s)
✔ [4838/8991] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapPointOverlapValueDirectMiddleFactor (3.1s)
✔ [4839/8991] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapPointTripleOverlapValueDirectFactorDataMapped (2.9s)
✔ [4840/8991] Built Iut.Foundations.SourceEtaleRepresentedStrongTransPointIsoWhiskerRightSymmInv (2.9s)
✔ [4841/8991] Built Iut.Foundations.SourceEtaleRepresentedStrongTransPointIsoAssociatorNaturalityMiddleInverseSolve (2.9s)
✔ [4842/8991] Built Iut.Foundations.SourceEtaleRepresentedStrongTransPointIsoAssociatorNaturalityMiddleInv (2.0s)
✔ [4843/8991] Built Iut.Foundations.SourceEtaleRepresentedStrongTransPointIsoAssociatorInvAbsorbPointTransport (2.9s)
✔ [4845/8991] Built Iut.Foundations.SourceFiniteEtaleClopenIdempotentQuotient (2.0s)
✔ [4846/8991] Built Iut.Foundations.SourceTensorProductScalarTowerQuotient (1.8s)
✔ [4847/8991] Built Iut.Foundations.SourceFiniteEtaleAffinePullbackActionTensor (7.4s)
✔ [4848/8991] Built Iut.Foundations.SourceFiniteEtaleSchemeCoverBaseChangeFiniteLimits (2.9s)
✔ [4849/8991] Built Iut.Foundations.SourceFiniteEtaleSchemeCoverBaseChangeBinaryCoproducts (13s)
✔ [4850/8991] Built Iut.Foundations.SourceInvolutiveEndofunctorEquivariantObject (3.1s)
✔ [4851/8991] Built Iut.Foundations.SourceFiniteEtaleSchemeCoverMonoCharacteristicIdempotent (2.8s)
✔ [4852/8991] Built Iut.Foundations.SourceRingEquivConjugationData (1.4s)
✔ [4853/8991] Built Iut.Foundations.SourceInvariantIdealQuotientInvolution (1.7s)
✔ [4854/8991] Built Iut.Foundations.SourceAffineScalarExtensionReversedTensorNaturality (15s)
✔ [4855/8991] Built Iut.Foundations.SourceTensorProductRightAlgEquiv (1.7s)
✔ [4856/8991] Built Iut.Foundations.SourceTensorProductTmulMulInclusions (1.8s)
✔ [4857/8991] Built Iut.Foundations.SourceRingHomRangeActionMul (1.6s)
✔ [4858/8991] Built Iut.Foundations.SourceRingHomRangeEquiv (1.6s)
✔ [4859/8991] Built Iut.Foundations.SourceRingEquivApplyHEqOfCarrierEq (1.4s)
✔ [4860/8991] Built Iut.Foundations.SourceEquivTransportApplyBack (762ms)
✔ [4861/8991] Built Iut.Foundations.SourceTensorProductSpecHomExt (2.3s)
✔ [4862/8991] Built Iut.Foundations.SourceCategoryFourfoldReassociation (1.4s)
✔ [4863/8991] Built Iut.Foundations.SourceFiniteEtaleSchemeCoverIdentitySectionLift (3.0s)
✔ [4864/8991] Built Iut.Foundations.SourceMorphismPropertyOverPullbackCompProjection (1.9s)
✔ [4865/8991] Built Iut.Foundations.SourceEtaleStackSchemeAtlasFiniteEtalePreDescentNormalizedMultiplicationHom (3.1s)
✔ [4866/8991] Built Iut.Foundations.SourceCategoryIsoConjugationCancel (2.7s)
✔ [4867/8991] Built Iut.Foundations.SourceFiniteEtaleSignQuotientAtlasFirstSheetProjection (2.9s)
✔ [4868/8991] Built Iut.Foundations.SourceFiniteEtaleSignQuotientAtlasConeLiftReassociation (3.1s)
✔ [4869/8991] Built Iut.Foundations.SourceFiniteEtaleSignQuotientAtlasTotalSpaceNormalization (14s)
✔ [4870/8991] Built Iut.Foundations.SourceEtalePseudofunctorConeReplaceCommutesHom (2.8s)
✔ [4871/8991] Built Iut.Foundations.SourceFiniteEtaleSignQuotientAtlasInversionIsoFirstSheetTotalSpace (4.1s)
✔ [4872/8991] Built Iut.Foundations.SourceEtalePseudofunctorInvolutionConePasting (3.1s)
✔ [4873/8991] Built Iut.Foundations.SourceCategoryIsoFactorCancellation (2.6s)
✔ [4874/8991] Built Iut.Foundations.SourceCategoryThreeCompatibilityPasting (1.5s)
✔ [4875/8991] Built Iut.Foundations.SourceEtaleStackSchemeAtlasTripleOverlapLongConeCells (2.0s)
✔ [4876/8991] Built Iut.Foundations.SourceCategoryEqualityPostcompositionIdentity (1.4s)
✔ [4877/8991] Built Iut.Foundations.SourceFiniteEtaleSchemeCoverPullbackMorphismDetection (3.3s)
✔ [4878/8991] Built Iut.Foundations.SourceFiniteEtaleSignQuotientEquivariantMap (5.6s)
✔ [4879/8991] Built Iut.Foundations.SourceCategoryTheoryColimMapFunctoriality (1.5s)
✔ [4880/8991] Built Iut.Foundations.SourceFiniteEtaleSchemeCoverStrictEpiUnderlyingScheme (2.8s)
✔ [4881/8991] Built Iut.Foundations.SourceEtaleStackSchemeAtlasFiniteEtaleDescentNormalizedNaturality (34s)
✔ [4882/8991] Built Iut.Foundations.SourceSignSwapActionCoproductQuotient (3.8s)
✔ [4883/8991] Built Iut.Foundations.SourceFiniteEtaleSignTorsorProjectionEffectiveEpi (2.0s)
✔ [4884/8991] Built Iut.Foundations.SourceFiniteEtaleSignTorsorEquivariantMapIso (4.5s)
✔ [4885/8991] Built Iut.Foundations.SourceFiniteEtaleSignQuotientTrivialAtlasIdentityPoint (2.8s)
✔ [4886/8991] Built Iut.Foundations.SourceCategoryMiddleIdentityConjugation (2.7s)
✔ [4887/8991] Built Iut.Foundations.SourceFiniteEtaleSignQuotientAssociatedStackCoverConeLiftCompatibilityRightContext (1.5s)
✔ [4888/8991] Built Iut.Foundations.SourceCategoryThreeLegPasting (1.4s)
✔ [4889/8991] Built Iut.Foundations.SourceCategoryFunctorOfObjMap (1.4s)
✔ [4890/8991] Built Iut.Foundations.SourceCategoryThreeProjectionPastingCore (1.6s)
✔ [4891/8991] Built Iut.Foundations.SourceCategoryFactorizedMiddlePasting (1.4s)
✔ [4892/8991] Built Iut.Foundations.SourceCategoryThreeLegQuotientPasting (1.5s)
✔ [4893/8991] Built Iut.Foundations.SourceCategoryFiveLegPasting (1.5s)
✔ [4894/8991] Built Iut.Foundations.SourceFiniteEtaleSignQuotientReindexHomExt (3.5s)
✔ [4895/8991] Built Iut.Foundations.SourceFiniteEtaleSignQuotientAssociatedStackCoverConeLiftToTestPasting (1.4s)
✔ [4896/8991] Built Iut.Foundations.SourceEqualityProofPackage (340ms)
✔ [4897/8991] Built Iut.Foundations.SourceCategoryReplaceRightmostFactor (1.4s)
✔ [4898/8991] Built Iut.Foundations.SourceCategoryReplaceTwoRightFactors (1.4s)
✔ [4899/8991] Built Iut.Foundations.SourceCategoryPrefixFactorPasting (1.4s)
✔ [4900/8991] Built Iut.Foundations.SourceCategoryTwoCompatibilityPasting (1.4s)
✔ [4901/8991] Built Iut.Foundations.SourceCategoryCongrThreeFactors (1.4s)
✔ [4902/8991] Built Iut.Foundations.SourceCategoryPackedHEqEndpointLinkDataDependentCongrArg (1.4s)
✔ [4903/8991] Built Iut.Foundations.SourceCategoryThreeMorphismBridgePasting (1.7s)
✔ [4904/8991] Built Iut.Foundations.SourceCategoryTwoMorphismHEqPastingData (1.5s)
✔ [4905/8991] Built Iut.Foundations.SourceOrbicurveFiniteEtaleIteratedBaseChangeReverseFst (3.0s)
✔ [4906/8991] Built Iut.Foundations.SourceFiniteEtaleSignQuotientPointIdentityReconstructionTotalNaturality (4.3s)
✔ [4907/8991] Built Iut.Foundations.SourceEtalePseudofunctorYonedaRecoveryModificationNaturality (5.0s)
✔ [4908/8991] Built Iut.Foundations.SourceCategoryHEqEndpointProjections (1.3s)
✔ [4909/8991] Built Iut.Foundations.SourceEtaleStackSchemeAtlasFiniteEtaleDescentComparisonConverse (2.8s)
✔ [4910/8991] Built Iut.Foundations.SourceFinitaryExtensiveComplementComparison (1.9s)
✔ [4911/8991] Built Iut.Foundations.SourceFiniteEtaleSchemeCoverBaseChangeIso (3.4s)
✔ [4912/8991] Built Iut.Foundations.SourceGaloisFiberFunctorFiniteColimits (2.9s)
✔ [4913/8991] Built Iut.Foundations.SourceConnectedFiniteEtaleConverse (4.7s)
✔ [4914/8991] Built Iut.Foundations.SourceContinuousActionRestrictionSurjectivity (4.1s)
✔ [4915/8991] Built Iut.Foundations.SourceMorphismPropertyOverPullbackCongrProjection (1.6s)
✔ [4916/8991] Built Iut.Foundations.SourceFiniteAlgebraSeparableClosureFactorization (2.7s)
✔ [4917/8991] Built Iut.Foundations.SourceProfiniteKernelLift (2.8s)
✔ [4918/8991] Built Iut.Foundations.SourceSelectedFiberSurjectiveMapData (339ms)
✔ [4919/8991] Built Iut.Foundations.SourcePullbackSelectedSectionAction (1.6s)
✔ [4920/8991] Built Iut.Foundations.SourceCategoryTheoryEqToIsoFintypeComponentHEq (1.5s)
✔ [4921/8991] Built Iut.Foundations.SourceCategoryTheoryDetachedNaturalityPastingMaps (1.4s)
✔ [4922/8991] Built Iut.Foundations.SourceProfiniteClosedSubgroupOpenExtension (2.0s)
✔ [4923/8991] Built Iut.Foundations.SourcePretransitiveContinuousActionCoset (3.5s)
✔ [4924/8991] Built Iut.Foundations.SourcePointedAnabelioidFiberEquivariance (2.8s)
✔ [4925/8991] Built Iut.Foundations.SourceSpecRingHomSemiconjugacy (2.2s)
✔ [4926/8991] Built Iut.Foundations.SourceCategoryTheoryIsoRightFactorInvOfHomEq (1.4s)
✔ [4927/8991] Built Iut.Foundations.SourceFintypeCatFunctorMapCompApply (1.5s)
✔ [4928/8991] Built Iut.Foundations.SourceCategoryPackedTwoProjectionPasting (1.4s)
✔ [4929/8991] Built Iut.Foundations.SourceCategoryHEqPrecomposition (1.4s)
✔ [4930/8991] Built Iut.Foundations.SourceCategoryTheoryEquivalenceInverseObjectIsoCounit (1.4s)
✔ [4931/8991] Built Iut.Foundations.SourceCategoryTwoMorphismEquationDataOfCompositeEq (1.4s)
✔ [4932/8991] Built Iut.Foundations.SourceHEqTransExplicit (1.3s)
✔ [4933/8991] Built Iut.Foundations.SourceCategoryPackedHEqEndpointLinkDataCommonRightComparisonData (1.3s)
✔ [4934/8991] Built Iut.Foundations.SourceFunctionPointwiseFactorizationData (351ms)
✔ [4935/8991] Built Iut.Foundations.SourceFintypeFunctorFactorizationApply (1.6s)
✔ [4936/8991] Built Iut.Foundations.SourceFunctionHEqCastMapData (329ms)
✔ [4937/8991] Built Iut.Foundations.SourceFunctionPointwiseEqualityData (365ms)
✔ [4938/8991] Built Iut.Foundations.SourceFunctionHEqCongr (317ms)
✔ [4939/8991] Built Iut.Foundations.SourceCategoryPackedHEqEndpointLinkDataHiddenEndpointStorage (1.3s)
✔ [4940/8991] Built Iut.Foundations.SourceCategoryPackedHEqEndpointLinkDataOfTwoHEq (1.4s)
✔ [4941/8991] Built Iut.Foundations.SourceCategoryPackedHEqEndpointLinkDataCommonMiddleProjectionData (1.4s)
✔ [4942/8991] Built Iut.Foundations.SourceSelectedFiberComponentDomination (1.5s)
✔ [4943/8991] Built Iut.Foundations.SourceContinuousActionRestrictionComponentStability (3.1s)
✔ [4944/8991] Built Iut.Foundations.SourceHEqApply (326ms)
✔ [4945/8991] Built Iut.Foundations.SourceEtalePseudofunctorPointIdentityReconstructionNaturality (4.6s)
✔ [4946/8991] Built Iut.Foundations.SourceCategoryProjectionEndpointHEqWhisker (1.4s)
✔ [4947/8991] Built Iut.Foundations.SourceEtaleStackSchemeAtlasFiniteEtaleDescentObjectPullbackProjections (3.0s)
✔ [4948/8991] Built Iut.Foundations.SourceFiniteEtaleSignTorsorTrivialAtlasFirstSheetExt (3.6s)
✔ [4949/8991] Built Iut.Foundations.SourceOrbicurveFiniteEtaleBaseChangePointIsoToSource (2.9s)
✔ [4950/8991] Built Iut.Foundations.SourceEtaleStackSchemeAtlasFiniteEtaleDescentOverlapComparisonLeft (2.0s)
✔ [4951/8991] Built Iut.Foundations.SourceOrbicurveFiniteEtaleIteratedBaseChangeReverseLeftProjection (2.0s)
✔ [4952/8991] Built Iut.Foundations.SourceCategoryInvolutiveActionTransport (1.5s)
✔ [4953/8991] Built Iut.Foundations.SourceRegularInvolutivePullbackFiberSwap (1.9s)
✔ [4954/8991] Built Iut.Foundations.SourceEtaleStackFiniteEtaleComposition (5.6s)
✔ [4955/8991] Built Iut.Foundations.SourceCategoryProjectionEndpointLinkContext (1.3s)
✔ [4956/8991] Built Iut.Foundations.SourceCategoryDetachedHEqData (359ms)
✔ [4957/8991] Built Iut.Foundations.SourceCategoryComparisonProjectionContext (1.4s)
✔ [4958/8991] Built Iut.Foundations.SourceCategoryDetachedEqDataProjections (336ms)
✔ [4959/8991] Built Iut.Foundations.SourceProfinitePostcompositionKernelIso (4.3s)
✔ [4960/8991] Built Iut.Foundations.SourceOrbicurveFiniteEtaleCoverStabilizerExactSequence (2.9s)
✔ [4961/8991] Built Iut.Foundations.SourceProfiniteOpenSubgroupKernelIso (3.6s)
✔ [4962/8991] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalHomPointIsoNaturality (3.2s)
✔ [4963/8991] Built Iut.Foundations.SourceOrbicurveSignInvariantCategory (3.1s)
✔ [4964/8991] Built Iut.Foundations.SourcePseudofunctorStrongTransCompNaturalityInvApp (1.7s)
✔ [4965/8991] Built Iut.Foundations.SourceCategoryFunctorSquarePasting (1.5s)
✔ [4966/8992] Built Iut.Foundations.SourceEtaleStackSchemeAtlasSourceAtlasOverlapCanonicalComparisonLeftExpandedFirstWhiskeredHom (3.2s)
✔ [4967/8992] Built Iut.Foundations.SourceEtaleStackSchemeAtlasMapCechCocycle (3.1s)
✔ [4968/8992] Built Iut.Foundations.SourceFiniteEtaleTensorAction (3.7s)
✔ [4969/8992] Built Iut.Foundations.SourceFiniteEtaleSignQuotientAffineChartCompositionCoherence (3.8s)
✔ [4970/8992] Built Iut.Foundations.SourceFiniteEtaleSignQuotientAffineChartGluedProjection (3.1s)
✔ [4971/8992] Built Iut.Foundations.SourceFiniteEtaleSignQuotientAtlasConeLiftSchemeMap (3.0s)
✔ [4972/8992] Built Iut.Foundations.SourceFiniteEtaleSignQuotientSchemeAtlas (3.2s)
✔ [4973/8992] Built Iut.Foundations.SourceFiniteEtaleSignQuotientInvariantTargetDescent (5.4s)
✔ [4974/8992] Built Iut.Foundations.SourceEtalePseudofunctorTwoPullbackCancellationTwoCellYTargetToY (2.0s)
✔ [4975/8992] Built Iut.Foundations.SourceFiberFunctorComparison (2.5s)
✔ [4976/8992] Built Iut.Foundations.SourceSchemeEtaleStackPresentationReverseFiniteEtaleCover (3.9s)
✔ [4977/8992] Built Iut.Foundations.SourceEtalePseudofunctorContractiblePullbackEquivalence (3.0s)
✔ [4978/8992] Built Iut.Foundations.SourcePreGaloisFiberFunctorEquivalenceTransport (1.7s)
✔ [4979/8992] Built Iut.Foundations.SourcePseudofunctorRestrictionPullHom (2.2s)
✔ [4980/8992] Built Iut.Foundations.SourceSchemeOverFieldRestrictScalarsSliceEquivalence (4.1s)
✔ [4981/8992] Built Iut.Foundations.SourceEtaleFundamentalGroupCoverActionEquivalence (2.6s)
✔ [4983/8992] Built Iut.Foundations.SourceCategoryFourLegSquareReassociation (1.3s)
✔ [4984/8992] Built Iut.Foundations.SourcePseudofunctorStrongTransEndpointPullLeft (1.0s)
✔ [4985/8992] Built Iut.Foundations.SourcePseudofunctorStrongTransEndpointPullRight (2.3s)
✔ [4986/8992] Built Iut.Foundations.SourceEtaleStackSchemeAtlasBaseChangePointIsoSource (2.9s)
✔ [4987/8992] Built Iut.Foundations.SourceCategoryFunctorMapSubsingletonComposition (1.4s)
✔ [4988/8992] Built Iut.Foundations.SourceCategoryEndpointTransportPasting (1.5s)
✔ [4989/8992] Built Iut.Foundations.SourceCategoryMappedTwoThreePasting (1.4s)
✔ [4990/8992] Built Iut.Foundations.SourceFiniteEtaleSignQuotientAtlasPointFiberIsoNaturalityFirstSheet (5.5s)
✔ [4991/8992] Built Iut.Foundations.SourceCategoryMappedNaturalityPasting (1.4s)
✔ [4992/8992] Built Iut.Foundations.SourceCategoryPullNaturalityThroughIso (1.4s)
✔ [4993/8992] Built Iut.Foundations.SourceCategoryThreeFactorIsoRecoveryData (1.5s)
✔ [4994/8992] Built Iut.Foundations.SourceCategoryThreeMapHEq (1.4s)
✔ [4995/8992] Built Iut.Foundations.SourceCategoryRecoverFactorThroughMappedIso (1.5s)
✔ [4996/8992] Built Iut.Foundations.SourceEtalePseudofunctorYonedaIdentityBaseChange (3.3s)
✔ [4997/8992] Built Iut.Foundations.SourceInitialTheta11a1DivisionRootFiberToThirtyTorsion (5.0s)
✔ [4998/8992] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapOverlapPairWhiskeredNestedFactorization (3.0s)
✔ [4999/8992] Built Iut.Foundations.SourceEtaleRepresentedStrongTransPointIsoWhiskerLeftTargetTransportRightDataRight (3.1s)
⚠ [5001/8992] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapPointTripleNaturalityAppTransportDataEndpoints (3.8s)
warning: Iut/Foundations/SourceEtaleStackSchemeAtlasLocalMapPointTripleNaturalityAppTransportDataEndpoints.lean:28:0: Please, add a comment explaining the need for modifying the maxHeartbeat limit, as in
set_option maxHeartbeats 800000 in
-- reason for change
...

Note: This linter can be disabled with `set_option linter.style.maxHeartbeats false`
warning: Iut/Foundations/SourceEtaleStackSchemeAtlasLocalMapPointTripleNaturalityAppTransportDataEndpoints.lean:53:0: Please, add a comment explaining the need for modifying the maxHeartbeat limit, as in
set_option maxHeartbeats 800000 in
-- reason for change
...

Note: This linter can be disabled with `set_option linter.style.maxHeartbeats false`
⚠ [5002/8992] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapPointTripleRepresentedSourceCellEndpointData (3.2s)
warning: Iut/Foundations/SourceEtaleStackSchemeAtlasLocalMapPointTripleRepresentedSourceCellEndpointData.lean:28:0: Please, add a comment explaining the need for modifying the maxHeartbeat limit, as in
set_option maxHeartbeats 800000 in
-- reason for change
...

Note: This linter can be disabled with `set_option linter.style.maxHeartbeats false`
✔ [5003/8992] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapPointTripleCocycleBaseInverseTerminalProjection (3.8s)
✔ [5004/8992] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapPointTripleCocycleNormalizedAtlasMiddleIdentity (3.2s)
✔ [5005/8992] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapPointTriplePastedConeIso (3.1s)
✔ [5006/8992] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapPointTripleLongEdgeGeometricTargetAfterSourceAssociator (3.6s)
✔ [5007/8992] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapPointTripleOverlapValueDirectFactorDataMappedRight (3.3s)
✔ [5008/8992] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapPointTripleCocycleSuccessiveSecondOverlapValueFactorDataMapped (2.8s)
✔ [5009/8992] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapPointTripleCocycleSuccessiveFirstOverlapValueFactorDataMapped (2.9s)
✔ [5010/8992] Built Iut.Foundations.SourceEtaleRepresentedStrongTransPointIsoWhiskerRightWhiskerRightSymmInv (2.0s)
✔ [5011/8992] Built Iut.Foundations.SourceEtaleRepresentedStrongTransPointIsoWhiskerRightCongrIsoSymmInv (2.0s)
✔ [5012/8992] Built Iut.Foundations.SourceTensorProductAlgebraicFiniteStage (3.0s)
✔ [5013/8992] Built Iut.Foundations.SourceFiniteEtaleAffinePullbackActionReversedTensor (3.0s)
✔ [5014/8992] Built Iut.Foundations.SourceEtaleStackSchemeAtlasFiniteEtalePreDescentPullbacks (7.1s)
✔ [5015/8992] Built Iut.Foundations.SourceEtaleStackSchemeAtlasFiniteEtaleDescentTerminal (2.9s)
✔ [5016/8992] Built Iut.Foundations.SourceFiniteEtaleSchemeCoverBaseChangeFiniteCoproducts (3.4s)
✔ [5017/8992] Built Iut.Foundations.SourceInvolutiveEndofunctorEquivariantForgetReflectsLimits (1.8s)
✔ [5018/8992] Built Iut.Foundations.SourceInvolutiveEndofunctorEquivariantFreeObject (2.0s)
✔ [5019/8992] Built Iut.Foundations.SourceInvolutiveEndofunctorEquivariantForgetReflectsIsomorphisms (1.5s)
✔ [5020/8992] Built Iut.Foundations.SourceInvolutiveEndofunctorEquivariantCofreeMono (1.5s)
✔ [5021/8992] Built Iut.Foundations.SourceFiniteEtaleSchemeCoverInvolutivePostcomposition (103s)
✔ [5022/8992] Built Iut.Foundations.SourceTensorProductRightAlgEquivTmul (1.8s)
✔ [5023/8992] Built Iut.Foundations.SourceTensorProductRingHomTmulFactorization (1.8s)
✔ [5024/8992] Built Iut.Foundations.SourceEquivTransportApplyBackTarget (741ms)
✔ [5025/8992] Built Iut.Foundations.SourceSchemePullbackSectionAlongComposite (4.2s)
✔ [5026/8992] Built Iut.Foundations.SourceEtalePseudofunctorConeReplaceCommutesHomTargetIso (2.5s)
✔ [5027/8992] Built Iut.Foundations.SourceFiniteEtaleSignQuotientAtlasSecondSheetTotalSpaces (4.1s)
✔ [5028/8992] Built Iut.Foundations.SourceFiniteEtaleSignQuotientEquivariantMapIdentity (3.6s)
✔ [5029/8992] Built Iut.Foundations.SourceFiniteEtaleSignQuotientEquivariantMapComposition (4.1s)
✔ [5030/8992] Built Iut.Foundations.SourceFiniteEtaleSignTorsorInvariantEffectiveDescent (3.2s)
✔ [5031/8992] Built Iut.Foundations.SourceFiniteEtaleSignQuotientHomTripleCarrier (2.9s)
✔ [5032/8992] Built Iut.Foundations.SourceFiniteEtaleSignQuotientReindexCompInverseToTotal (3.1s)
✔ [5033/8992] Built Iut.Foundations.SourceCategoryThreeMorphismBridgePastingPackedCompletion (1.4s)
✔ [5034/8992] Built Iut.Foundations.SourceFiniteEtaleSignQuotientPointIdentityReconstructionComparison (3.0s)
✔ [5035/8992] Built Iut.Foundations.SourceGaloisFiberFunctorFiniteColimitsHeterogeneous (2.5s)
✔ [5036/8992] Built Iut.Foundations.SourceContinuousActionRestrictionConnectednessSurjectivity (3.8s)
✔ [5037/8992] Built Iut.Foundations.SourceCategoryTheoryEqToIsoFintypeMapApplyHEq (1.5s)
✔ [5038/8992] Built Iut.Foundations.SourceCategoryTheoryIndexedNatIsoTransportFintypeComponentHEq (1.5s)
✔ [5039/8992] Built Iut.Foundations.SourceFintypeDetachedNaturalityIsoExtension (1.7s)
✔ [5040/8992] Built Iut.Foundations.SourceContinuousActionClosedSubgroupAmbientEnvelope (3.9s)
✔ [5041/8992] Built Iut.Foundations.SourcePointedAnabelioidKernelFiberStability (3.0s)
✔ [5042/8992] Built Iut.Foundations.SourceEquivalenceInversePointNaturality (1.6s)
✔ [5043/8992] Built Iut.Foundations.SourceCategoryPackedHEqEndpointLinkDataCommonRightComparisonDataLeftComm (1.4s)
✔ [5044/8992] Built Iut.Foundations.SourceFunctionHEqCastMapDataPostmap (324ms)
✔ [5045/8992] Built Iut.Foundations.SourceFunctionHEqData (1.4s)
✔ [5046/8992] Built Iut.Foundations.SourceCategoryPackedHEqEndpointLinkDataHiddenEndpointStorageExplicit (1.4s)
✔ [5047/8992] Built Iut.Foundations.SourceCategoryPackedHEqEndpointLinkDataCommonMiddleProjectionDataOfExplicitMiddle (1.4s)
✔ [5048/8992] Built Iut.Foundations.SourceSelectedFiberSurjectiveMapDataComponentDomination (1.5s)
✔ [5049/8992] Built Iut.Foundations.SourceFiniteEtaleSignQuotientPointIdentityReconstructionNaturality (3.3s)
✔ [5050/8992] Built Iut.Foundations.SourceEtalePseudofunctorPointIdentityReconstructionComponent (4.0s)
✔ [5051/8992] Built Iut.Foundations.SourceRegularInvolutiveEquivariantExtension (2.7s)
✔ [5052/8992] Built Iut.Foundations.SourceCategoryProjectionEndpointLinkData (1.4s)
✔ [5053/8992] Built Iut.Foundations.SourceCategoryDetachedHEqPastingData (353ms)
✔ [5054/8992] Built Iut.Foundations.SourceCategoryDetachedHEqDataProjections (329ms)
✔ [5055/8992] Built Iut.Foundations.SourceCategoryComparisonProjectionContextLeftWhisker (1.4s)
✔ [5056/8992] Built Iut.Foundations.SourceOrbicurveFiniteEtaleCoverStabilizerProjectionSurjectivity (3.2s)
✔ [5057/8992] Built Iut.Foundations.SourceOrbicurveFiniteEtaleCoverStabilizerKernelIso (2.9s)
✔ [5058/8992] Built Iut.Foundations.SourceEtaleStackSchemeAtlasYonedaFiberNaturalityOfPointIso (3.4s)
✔ [5059/8992] Built Iut.Foundations.SourceEtaleStackSchemeAtlasPointIsoDescentComparison (5.2s)
✔ [5060/8992] Built Iut.Foundations.SourceOrbicurveSignInvariantIso (3.1s)
✔ [5061/8992] Built Iut.Foundations.SourceOrbicurveSignQuotientComparison (3.4s)
✔ [5062/8992] Built Iut.Foundations.SourceCategoryFunctorSquarePastingEvidenceFirst (1.4s)
✔ [5063/8992] Built Iut.Foundations.SourceCategoryFunctorSquarePastingContext (1.6s)
⚠ [5064/8992] Built Iut.Foundations.SourceEtaleStackSchemeAtlasSourceAtlasOverlapCanonicalComparisonLeftExpandedSecondWhiskerCongr (3.0s)
warning: Iut/Foundations/SourceEtaleStackSchemeAtlasSourceAtlasOverlapCanonicalComparisonLeftExpandedSecondWhiskerCongr.lean:7:100: This line exceeds the 100 character limit, please shorten it!

Note: This linter can be disabled with `set_option linter.style.longLine false`
✔ [5066/8992] Built Iut.Foundations.SourceEtaleStackSchemeAtlasMapLocalMapCechData (2.7s)
✔ [5067/8992] Built Iut.Foundations.SourceFiniteEtaleTensorFixedSubalgebra (4.1s)
✔ [5068/8992] Built Iut.Foundations.SourceFiniteEtaleSignQuotientAffineChartCompositionContext (3.5s)
✔ [5069/8992] Built Iut.Foundations.SourceFiniteEtaleSignQuotientAffineChartGluedInvolution (3.0s)
✔ [5070/8992] Built Iut.Foundations.SourceFiniteEtaleSignQuotientAtlasConeLiftTransportSchemeMap (3.1s)

/usr/bin/podman timed out after 7200s
podman cleanup removed verifier container apx-verifier-job-1793-runtime-lean_checker-2510420-1789168350035750074-1 on attempt 1
blueprint_buildexit 1duration 1s · created 
lake build :blueprint
error: unknown package facet `blueprint`

apx-runtime-resource-v1	apx-verifier-job-1793-runtime-blueprint_build-2510420-1789175550760398339-2	888832	1404928	21474836480	0	0	0	0	0	0	3244032	107974656	21474836480	0	0	0	0	0	0

Keyboard shortcuts