Login

Verification run

Run 1300

promachina/iut-leanbranch e21-924-completetriggered via github_push
failedcommit 667402efca1atoolchain 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

 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.9s)
✔ [4607/6595] Built Iut.Foundations.SourceFiniteEtaleAffineOverCoordinateAction (2.5s)
✔ [4609/6595] Built Iut.Foundations.SourceSingleObjOppositeEquivalence (1.6s)
✔ [4610/6595] Built Iut.Foundations.SourceEtalePseudofunctorRepresentablePullbackTwoCell (118s)
✔ [4611/6595] Built Iut.Foundations.SourceCategoryPackedHEqEndpointLinkDataJoinProjections (1.3s)
✔ [4612/6595] Built Iut.Foundations.SourceEtalePseudofunctorStrongTransWhiskerRightIsoSymmHom (2.8s)
✔ [4613/6595] Built Iut.Foundations.SourceEtalePseudofunctorStrongTransPentagonInvPrefix (4.3s)
✔ [4614/6595] Built Iut.Foundations.SourceCategoryEqToHomTransportedEndpointDataMap (1.5s)
✔ [4615/6595] Built Iut.Foundations.SourceEtalePseudofunctorChangeFirstBaseMap (3.9s)
✔ [4616/6595] Built Iut.Foundations.SourceEtalePseudofunctorChangeSecondBaseMap (3.8s)
✔ [4617/6595] Built Iut.Foundations.SourceEtalePseudofunctorFaithfulCellAssembly (3.9s)
✔ [4618/6595] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalHomPointValueRecovery (2.0s)
✔ [4619/6595] Built Iut.Foundations.SourceFiniteEtaleSchemeCoverClopenMono (2.0s)
⚠ [4621/6595] Built Iut.Foundations.SourceFiniteEtaleSignTorsorAffineEffectiveness (174s)
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`
✔ [4622/6595] Built Iut.Foundations.SourceFiniteEtaleSignQuotientPrestack (42s)
✔ [4623/6595] Built Iut.Foundations.SourceFiniteEtaleSignTorsorTargetStackDescent (2.0s)
✔ [4624/6595] Built Iut.Foundations.SourceFiniteEtaleSignTorsorTrivial (4.7s)
✔ [4625/6595] Built Iut.Foundations.SourceEtalePseudofunctorTwoPullbackCancellationLiftToYLawful (2.7s)
✔ [4626/6595] Built Iut.Foundations.SourceFiniteEtaleAffineOverCoordinateFiniteEtale (2.5s)
✔ [4627/6595] Built Iut.Foundations.SourceEtalePseudofunctorRepresentablePullbackWitness (2.9s)
✔ [4628/6595] Built Iut.Foundations.SourceCategoryPackedHEqTwoMorphismComposition (1.5s)
✔ [4629/6595] Built Iut.Foundations.SourceEtaleStackRepresentablePropertyChangeMap (2.8s)
✔ [4630/6595] Built Iut.Foundations.SourceEtalePseudofunctorConeAfterChangeSecondBaseMap (3.2s)
✔ [4631/6595] Built Iut.Foundations.SourceEtalePseudofunctorRepresentedIsoPointLift (3.5s)
✔ [4632/6595] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalHomYonedaPointValue (2.9s)
✔ [4633/6595] Built Iut.Foundations.SourceFiniteEtaleSchemeCoverDirectSummand (3.4s)
✔ [4634/6595] Built Iut.Foundations.SourceFiniteEtaleSchemeCoverUnderlyingEpiRange (2.0s)
⚠ [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 (3.1s)
✔ [4637/6598] Built Iut.Foundations.SourceFiniteEtaleSignQuotientAtlas (5.7s)
✔ [4638/6599] Built Iut.Foundations.SourceEtalePseudofunctorTwoPullbackCancellationLiftToYHomToX (2.9s)
✔ [4639/6599] Built Iut.Foundations.SourceRepresentableStrongTransReconstruction (3.2s)
✔ [4640/6599] Built Iut.Foundations.SourceEtalePseudofunctorConeAfterChangeSecondBaseMapFromConeOf (3.2s)
✔ [4641/6599] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalIsoBaseChangeOver (3.4s)
✔ [4642/6599] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalHomYonedaNaturality (2.0s)
✔ [4643/6599] Built Iut.Foundations.SourceFiniteEtaleSchemeCoverAffineSource (2.9s)
✔ [4644/6599] Built Iut.Foundations.SourceFiniteEtaleSchemeCoverUnderlyingEpiSurjective (7.0s)
⚠ [4645/6599] Built Iut.Foundations.SourceFiniteEtaleSignTorsorAffineCoverAssembly (883s)
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 (17s)
✔ [4648/6599] Built Iut.Foundations.SourceEtalePseudofunctorTwoPullbackCancellationLiftToYHomToY (2.8s)
✔ [4650/6599] Built Iut.Foundations.SourceEtaleStackRepresentableLocalIsoDescent (3.9s)
✔ [4651/6599] Built Iut.Foundations.SourceEtaleStackSchemeAtlasOverlapMultiplication (3.2s)
✔ [4652/6599] Built Iut.Foundations.SourceEtalePseudofunctorRepresentablePullbackAlongStrongTrans (4.1s)
✔ [4653/6599] Built Iut.Foundations.SourceFiniteEtaleSchemeCoverAffineGroupQuotient (3.3s)
✔ [4654/6599] Built Iut.Foundations.SourceFiniteEtaleSchemeCoverBalanced (2.6s)
✔ [4655/6599] Built Iut.Foundations.SourceFiniteEtaleSignTorsorAffineCoverRestriction (125s)
✔ [4656/6599] Built Iut.Foundations.SourceFiniteEtaleSignQuotientAtlasLiftApp (127s)
✔ [4657/6599] Built Iut.Foundations.SourceFiniteEtaleSignQuotientAtlasInvariant (3.5s)
✔ [4659/6600] Built Iut.Foundations.SourceEtalePseudofunctorTwoPullbackCancellationLiftCompatibility (2.8s)
✔ [4660/6600] Built Iut.Foundations.SourceEtaleStackRepresentableAtlasLocalIsoDescent (3.2s)
✔ [4661/6600] Built Iut.Foundations.SourceOrbicurveFiniteEtaleBaseChangeSchemeCoverMapReflectsLocalIso (3.5s)
✔ [4662/6602] Built Iut.Foundations.SourceEtaleStackSchemeAtlasOverlapMultiplicationRepresentedLongConeIso (3.0s)
✔ [4663/6602] Built Iut.Foundations.SourceEtaleStackSchemeAtlasOverlapConePasting (3.0s)
✔ [4664/6602] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapCechData (3.1s)
✔ [4665/6602] Built Iut.Foundations.SourceEtaleStackSchemeAtlasFiniteEtaleDescent (3.3s)
✔ [4666/6602] Built Iut.Foundations.SourceOrbicurveFiniteEtaleIteratedBaseChange (9.6s)
✔ [4667/6602] Built Iut.Foundations.SourceFiniteEtaleSchemeCoverAffineOverFullyFaithful (2.7s)
✔ [4668/6602] Built Iut.Foundations.SourceFiniteEtaleFixedSubalgebra (3.2s)
✔ [4669/6602] Built Iut.Foundations.SourceFiniteEtaleSignTorsorAffineCoverFiniteEffectivity (3.7s)
✔ [4670/6602] Built Iut.Foundations.SourceFiniteEtaleSignQuotientAtlasLiftNaturality (103s)
✔ [4671/6602] Built Iut.Foundations.SourceFiniteEtaleSignQuotientAtlasInvariantElement (3.2s)
✔ [4673/6602] Built Iut.Foundations.SourceEtalePseudofunctorTwoPullbackCancellationConeMorphismCompatibility (3.1s)
✔ [4676/6604] Built Iut.Foundations.SourceEtaleStackSchemeAtlasOverlapConePastingIso (4.3s)
✔ [4677/6604] Built Iut.Foundations.SourceEtaleStackSchemeAtlasOverlapConePastingCell (3.1s)
✔ [4678/6604] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapRestrictionCongrIsoNaturality (3.3s)
✔ [4679/6604] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapRestrictionCongrIsoWhiskerRightFactorization (3.1s)
✔ [4680/6604] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapOverlapNestedMiddleIso (2.8s)
✔ [4681/6604] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapPointObject (2.9s)
✔ [4682/6604] Built Iut.Foundations.SourceEtaleStackSchemeAtlasFiniteEtaleDescentComparison (3.2s)
✔ [4683/6604] Built Iut.Foundations.SourceEtaleStackSchemeAtlasMapCechEndpointIsos (3.0s)
✔ [4684/6604] Built Iut.Foundations.SourceEtaleStackSchemeAtlasBaseChangePointIso (3.1s)
✔ [4685/6604] Built Iut.Foundations.SourceOrbicurveFiniteEtaleIteratedBaseChangeForwardBackLiftedHom (3.4s)
✔ [4686/6604] Built Iut.Foundations.SourceEtaleStackSchemeAtlasOverlapMapIso (2.9s)
✔ [4687/6604] Built Iut.Foundations.SourceOrbicurveFiniteEtaleIteratedBaseChangeToSourceIso (2.0s)
✔ [4688/6604] Built Iut.Foundations.SourceFiniteEtaleFixedAffineQuotient (3.3s)
✔ [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.5s)
✔ [4695/6605] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapOverlapNestedMiddleHom (3.0s)
✔ [4696/6605] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapOverlapNestedEndpointIsos (2.8s)
✔ [4697/6605] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapPointOverlap (3.3s)
✔ [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 (3.0s)
✔ [4702/6605] Built Iut.Foundations.SourceFiniteEtaleOrbitConstantAlgebra (3.2s)
✔ [4703/6605] Built Iut.Foundations.SourceFiniteEtaleSignQuotientStackRefinement (3.3s)
✔ [4704/6605] Built Iut.Foundations.SourceFiniteEtaleSignQuotientAtlasLiftProjections (13s)
✔ [4705/6605] Built Iut.Foundations.SourceFiniteEtaleSignQuotientAtlasInvariantCocycle (20s)
✔ [4706/6607] Built Iut.Foundations.SourceEtalePseudofunctorTwoPullbackCancellationTwoCell (2.6s)
✔ [4709/6607] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapOverlapNestedMiddleCompositeFactorization (3.3s)
✔ [4710/6607] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapPullbackOverlapNestedFactorization (3.4s)
✔ [4711/6607] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapPointTransition (3.3s)
✔ [4712/6607] Built Iut.Foundations.SourceOrbicurveFiniteEtaleBaseChangePointIsoToSourceIso (2.8s)
✔ [4713/6607] Built Iut.Foundations.SourceEtaleStackSchemeAtlasFiniteEtaleDescentCoherence (13s)
✔ [4714/6607] Built Iut.Foundations.SourceEtaleStackSchemeAtlasMapCechPairFactorization (22s)
✔ [4715/6607] Built Iut.Foundations.SourceOrbicurveFiniteEtaleIteratedBaseChangeForwardBackStrongTransToSource (3.1s)
✔ [4716/6607] Built Iut.Foundations.SourceFiniteEtaleSplitAlgebraHom (3.3s)
✔ [4717/6607] Built Iut.Foundations.SourceFiniteEtaleSignQuotientAffineChartDescent (16s)
✔ [4718/6607] Built Iut.Foundations.SourceFiniteEtaleSignQuotientAtlasLiftTwoCell (297s)
✔ [4719/6607] Built Iut.Foundations.SourceFiniteEtaleSignQuotientAtlasLiftUnit (15s)
✔ [4720/6609] Built Iut.Foundations.SourceEtalePseudofunctorTwoPullbackCancellationTwoCellToX (2.8s)
✔ [4722/6609] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapOverlapNestedMiddleCompositeTargetCollapse (3.2s)
✔ [4723/6609] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapOverlapNestedMiddleCompositeSourceCollapse (3.1s)
✔ [4724/6609] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapOverlapNestedSpecializations (3.1s)
✔ [4725/6609] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapOverlapCompositeWhiskeredExpansion (3.1s)
✔ [4726/6609] Built Iut.Foundations.SourceEtaleRepresentedRestrictionPointIsoCongruenceTail (3.0s)
✔ [4727/6609] Built Iut.Foundations.SourceEtaleRepresentedStrongTransPointIsoWhiskerRightHom (3.0s)
✔ [4728/6609] Built Iut.Foundations.SourceEtaleRepresentedStrongTransPointIsoWhiskerLeft (3.0s)
✔ [4729/6609] Built Iut.Foundations.SourceEtaleRepresentedStrongTransPointIsoSymmHom (2.0s)
✔ [4730/6609] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapPointOverlapValueIsoRepresented (2.0s)
✔ [4731/6609] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapPointCocycleGeometry (3.2s)
✔ [4732/6609] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapCechCocyclePointValue (2.9s)
✔ [4733/6609] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapRestrictionCompositePointIsoHom (6.0s)
⚠ [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 (3.1s)
✔ [4739/6609] Built Iut.Foundations.SourceEtaleStackSchemeAtlasMapCechPairLongFactorization (3.0s)
✔ [4740/6609] Built Iut.Foundations.SourceOrbicurveFiniteEtaleIteratedBaseChangeForwardBackRealizationToSourceExpansion (3.1s)
✔ [4741/6609] Built Iut.Foundations.SourceFiniteEtaleSplitAlgebraAutomorphism (2.7s)
✔ [4742/6609] Built Iut.Foundations.SourceFiniteEtaleSignQuotientAffineChartGluing (8.6s)
✔ [4743/6609] Built Iut.Foundations.SourceFiniteEtaleSignQuotientAtlasLiftCompatibility (19s)
✔ [4744/6610] Built Iut.Foundations.SourceEtalePseudofunctorTwoPullbackCancellationTwoCellYTarget (2.7s)
✔ [4747/6610] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapOverlapNestedMiddleTargetAssociatorNaturality (3.1s)
✔ [4748/6610] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapOverlapNestedMiddleDirectTargetNaturalityEndpoints (2.9s)
✔ [4749/6610] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapOverlapNestedMiddleAttached (3.1s)
✔ [4750/6610] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapOverlapCompositeWhiskeredEndpointIsos (2.0s)
⚠ [4751/6628] Built Iut.Foundations.SourceEtaleRepresentedStrongTransPointIsoWhiskerLeftTargetTransport (2.0s)
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.9s)
✔ [4753/6635] Built Iut.Foundations.SourceEtaleRepresentedStrongTransPointIsoWhiskerLeftSourceTransport (3.1s)
✔ [4754/6635] Built Iut.Foundations.SourceEtaleRepresentedStrongTransPointIsoSymmInv (2.9s)
✔ [4755/6635] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapPointTripleRawCompositorTailHom (2.9s)
✔ [4756/6635] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapPointTripleBaseInverseTail (4.2s)
✔ [4757/6635] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapPointLongEdgeEndpoints (3.5s)
✔ [4758/6635] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapCechCocyclePointTripleValue (3.1s)
✔ [4759/6635] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapPointOverlapValueDirectFactorData (3.1s)
⚠ [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.2s)
✔ [4762/6635] Built Iut.Foundations.SourceEtaleRepresentedStrongTransPointIsoWhiskerRightTransHom (2.0s)
✔ [4763/6635] Built Iut.Foundations.SourceEtaleRepresentedStrongTransPointIsoAssociatorEqToHom (2.0s)
✔ [4764/6635] Built Iut.Foundations.SourceEtaleRepresentedStrongTransPointIsoCongruenceSymmInvAssociator (3.1s)
✔ [4765/6635] Built Iut.Foundations.SourceEtaleStackSchemeAtlasSourceAtlasOverlapCanonicalComparisonLeftFactorIso (2.7s)
✔ [4766/6635] Built Iut.Foundations.SourceEtaleStackSchemeAtlasFiniteEtaleCanonicalDescentStructureComparisonLeft (2.0s)
✔ [4767/6635] Built Iut.Foundations.SourceEtaleStackSchemeAtlasMapCechCompositeFactorization (12s)
✔ [4768/6635] Built Iut.Foundations.SourceOrbicurveFiniteEtaleIteratedBaseChangeForwardBackToSourceExpansion (3.0s)
✔ [4769/6635] Built Iut.Foundations.SourceFiniteEtaleSplitActionFixedAlgebra (3.9s)
✔ [4770/6635] Built Iut.Foundations.SourceFiniteEtaleSignQuotientAffineChartRelativeGluing (3.8s)
✔ [4771/6635] Built Iut.Foundations.SourceFiniteEtaleSignQuotientAtlasLiftWitness (18s)
✔ [4772/6750] Built Iut.Foundations.SourceEtalePseudofunctorTwoPullbackCancellationLiftToYInvToY (2.9s)
✔ [4775/6750] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapOverlapNestedMiddleDirectTargetNaturalityEndpointExpansions (3.0s)
✔ [4776/6750] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapOverlapNestedMiddleDirectTargetNaturalityMiddleRight (3.1s)
✔ [4777/6750] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapOverlapPairWhiskeredExpansion (3.2s)
✔ [4778/6750] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapOverlapCompositeWhiskeredEndpointFactorization (3.0s)
✔ [4779/6750] Built Iut.Foundations.SourceEtaleRepresentedStrongTransPointIsoWhiskerLeftTargetTransportData (2.9s)
✔ [4781/6750] Built Iut.Foundations.SourceFiniteEtaleSchemeCoverGeometricFiberFunctor (2.8s)
✔ [4782/6750] Built Iut.Foundations.SourceSpecFieldSchemeCoproductMaps (2.6s)
✔ [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/7793] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapPointTripleRepresentedSourceObjects (3.4s)
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/8799] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapPointTripleBaseInverseTailLeftHom (3.0s)
✔ [4788/8799] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapPointTripleCocycleMiddleValueIsos (2.0s)
✔ [4789/8799] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapPointTripleEdgeIso (3.3s)
✔ [4790/8799] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapPointTripleCocycleEndpointValueIso (3.0s)
⚠ [4791/8799] 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/8799] Built Iut.Foundations.SourceEtaleRepresentedStrongTransPointIsoWhiskerLeftTransInv (2.9s)
✔ [4793/8799] Built Iut.Foundations.SourceEtaleRepresentedStrongTransPointIsoWhiskerRightTransInv (3.1s)
✔ [4794/8799] Built Iut.Foundations.SourceEtaleRepresentedStrongTransPointIsoPentagonInv (3.2s)
✔ [4795/8799] Built Iut.Foundations.SourceEtaleRepresentedStrongTransPointIsoAssociatorNaturalityLeft (3.1s)
✔ [4796/8799] Built Iut.Foundations.SourceEtaleRepresentedStrongTransPointIsoAssociatorNaturalityMiddle (3.2s)
✔ [4797/8799] Built Iut.Foundations.SourceEtaleRepresentedStrongTransPointIsoAssociatorInvEqToHom (3.0s)
✔ [4798/8799] Built Iut.Foundations.SourceEtaleRepresentedStrongTransPointIsoCongruenceSymmInvAssociatorRestrictionTail (3.2s)
✔ [4799/8799] Built Iut.Foundations.SourceEtaleStackSchemeAtlasSourceAtlasOverlapCanonicalComparisonLeftExpandedIso (2.9s)
✔ [4800/8799] Built Iut.Foundations.SourceEtaleStackSchemeAtlasMapCechConeEndpointIsos (3.1s)
✔ [4801/8799] Built Iut.Foundations.SourceFiniteEtaleFixedSubalgebraBaseChange (3.3s)
✔ [4802/8799] Built Iut.Foundations.SourceFiniteEtaleSignQuotientAffineChartIdentityCoherence (554s)
✔ [4803/8799] Built Iut.Foundations.SourceFiniteEtaleSignQuotientAffineChartEffectivity (2.8s)
✔ [4804/8799] Built Iut.Foundations.SourceFiniteEtaleSignQuotientOrbicurve (199s)
✔ [4805/8799] Built Iut.Foundations.SourceEtalePseudofunctorTwoPullbackCancellationNestedWhisker (2.9s)
✔ [4807/8799] Built Iut.Foundations.SourceFiniteEtaleSchemeCoverRepresentable (3.0s)
✔ [4808/8799] Built Iut.Foundations.SourceSchemeEtaleStackPresentationFiniteEtaleCoverFunctor (3.0s)
✔ [4809/8799] Built Iut.Foundations.SourceEtalePseudofunctorContractiblePullback (3.5s)
✔ [4810/8799] Built Iut.Foundations.SourcePreGaloisCategoryEquivalenceTransport (1.9s)
✔ [4811/8799] Built Iut.Foundations.SourcePuncturedWeierstrassSchemeBaseChange (4.3s)
✔ [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 (2.0s)
✔ [4819/8799] Built Iut.Foundations.SourceAnabelioidDominatingPullbackInjectivity (2.9s)
✔ [4820/8799] Built Iut.Foundations.SourceCategoryIsoConjugationInverseCancellation (1.4s)
✔ [4821/8799] Built Iut.Foundations.SourceFiniteEtalePresentedQuotientBaseChange (1.9s)
✔ [4822/8898] Built Iut.Foundations.SourceIdealQuotientEquivComparison (1.9s)
✔ [4823/8991] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapOverlapPairWhiskeredNested (3.2s)
✔ [4824/8991] Built Iut.Foundations.SourceEtaleRepresentedStrongTransPointIsoWhiskerLeftTargetTransportRightData (2.9s)
✔ [4826/8991] Built Iut.Foundations.SourceFiniteEtaleSchemeCoverGeometricFiberPullbacks (2.7s)
✔ [4827/8991] Built Iut.Foundations.SourceEtaleRepresentedStrongTransPointIsoWhiskerLeftSymmInv (2.0s)
⚠ [4828/8991] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapPointTripleNaturalityAppTransportData (2.9s)
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 (2.0s)
⚠ [4830/8991] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapPointTripleRepresentedSourceCell (3.2s)
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`
✔ [4832/8991] Built Iut.Foundations.SourceFiniteEtaleClopenIdempotentQuotient (2.1s)
✔ [4833/8991] Built Iut.Foundations.SourceTensorProductScalarTowerQuotient (1.9s)
✔ [4834/8991] Built Iut.Foundations.SourceFiniteEtaleAffinePullbackActionTensor (7.6s)
✔ [4835/8991] Built Iut.Foundations.SourceFiniteEtaleSchemeCoverBaseChangeFiniteLimits (2.8s)
✔ [4836/8991] Built Iut.Foundations.SourceFiniteEtaleSchemeCoverBaseChangeBinaryCoproducts (12s)
✔ [4837/8991] Built Iut.Foundations.SourceInvolutiveEndofunctorEquivariantObject (3.1s)
✔ [4838/8991] Built Iut.Foundations.SourceFiniteEtaleSchemeCoverMonoCharacteristicIdempotent (2.0s)
✔ [4839/8991] Built Iut.Foundations.SourceRingEquivConjugationData (1.4s)
✔ [4840/8991] Built Iut.Foundations.SourceInvariantIdealQuotientInvolution (1.8s)
✔ [4841/8991] Built Iut.Foundations.SourceAffineScalarExtensionReversedTensorNaturality (15s)
✔ [4842/8991] Built Iut.Foundations.SourceTensorProductRightAlgEquiv (1.7s)
✔ [4843/8991] Built Iut.Foundations.SourceTensorProductTmulMulInclusions (1.8s)
✔ [4844/8991] Built Iut.Foundations.SourceRingHomRangeActionMul (1.6s)
✔ [4845/8991] Built Iut.Foundations.SourceRingHomRangeEquiv (1.6s)
✔ [4846/8991] Built Iut.Foundations.SourceRingEquivApplyHEqOfCarrierEq (1.4s)
✔ [4847/8991] Built Iut.Foundations.SourceEquivTransportApplyBack (782ms)
✔ [4848/8991] Built Iut.Foundations.SourceTensorProductSpecHomExt (2.4s)
✔ [4849/8991] Built Iut.Foundations.SourceCategoryFourfoldReassociation (1.4s)
✔ [4850/8991] Built Iut.Foundations.SourceFiniteEtaleSchemeCoverIdentitySectionLift (3.1s)
✔ [4851/8991] Built Iut.Foundations.SourceMorphismPropertyOverPullbackCompProjection (1.9s)
✔ [4852/8991] Built Iut.Foundations.SourceEtaleStackSchemeAtlasFiniteEtalePreDescentNormalizedMultiplicationHom (3.1s)
✔ [4853/8991] Built Iut.Foundations.SourceCategoryIsoConjugationCancel (2.7s)
✔ [4854/8991] Built Iut.Foundations.SourceFiniteEtaleSignQuotientAtlasFirstSheetProjection (3.1s)
✔ [4855/8991] Built Iut.Foundations.SourceFiniteEtaleSignQuotientAtlasConeLiftReassociation (3.2s)
✔ [4856/8991] Built Iut.Foundations.SourceFiniteEtaleSignQuotientAtlasTotalSpaceNormalization (15s)
✔ [4857/8991] Built Iut.Foundations.SourceEtalePseudofunctorConeReplaceCommutesHom (2.7s)
✔ [4858/8991] Built Iut.Foundations.SourceFiniteEtaleSignQuotientAtlasInversionIsoFirstSheetTotalSpace (4.2s)
✔ [4859/8991] Built Iut.Foundations.SourceEtalePseudofunctorInvolutionConePasting (3.1s)
✔ [4860/8991] Built Iut.Foundations.SourceCategoryIsoFactorCancellation (2.8s)
✔ [4861/8991] Built Iut.Foundations.SourceCategoryThreeCompatibilityPasting (1.5s)
✔ [4862/8991] Built Iut.Foundations.SourceEtaleStackSchemeAtlasTripleOverlapLongConeCells (3.0s)
✔ [4863/8991] Built Iut.Foundations.SourceCategoryEqualityPostcompositionIdentity (1.4s)
✔ [4864/8991] Built Iut.Foundations.SourceFiniteEtaleSchemeCoverPullbackMorphismDetection (3.3s)
✔ [4865/8991] Built Iut.Foundations.SourceFiniteEtaleSignQuotientEquivariantMap (5.8s)
✔ [4866/8991] Built Iut.Foundations.SourceCategoryTheoryColimMapFunctoriality (1.5s)
✔ [4867/8991] Built Iut.Foundations.SourceFiniteEtaleSchemeCoverStrictEpiUnderlyingScheme (2.8s)
✔ [4868/8991] Built Iut.Foundations.SourceEtaleStackSchemeAtlasFiniteEtaleDescentNormalizedNaturality (36s)
✔ [4869/8991] Built Iut.Foundations.SourceSignSwapActionCoproductQuotient (3.8s)
✔ [4870/8991] Built Iut.Foundations.SourceFiniteEtaleSignTorsorProjectionEffectiveEpi (3.1s)
✔ [4871/8991] Built Iut.Foundations.SourceFiniteEtaleSignTorsorEquivariantMapIso (4.5s)
✔ [4872/8991] Built Iut.Foundations.SourceFiniteEtaleSignQuotientTrivialAtlasIdentityPoint (2.8s)
✔ [4873/8991] Built Iut.Foundations.SourceCategoryMiddleIdentityConjugation (2.7s)
✔ [4874/8991] Built Iut.Foundations.SourceFiniteEtaleSignQuotientAssociatedStackCoverConeLiftCompatibilityRightContext (1.5s)
✔ [4875/8991] Built Iut.Foundations.SourceCategoryThreeLegPasting (1.4s)
✔ [4876/8991] Built Iut.Foundations.SourceCategoryFunctorOfObjMap (1.4s)
✔ [4877/8991] Built Iut.Foundations.SourceCategoryThreeProjectionPastingCore (1.6s)
✔ [4878/8991] Built Iut.Foundations.SourceCategoryFactorizedMiddlePasting (1.4s)
✔ [4879/8991] Built Iut.Foundations.SourceCategoryThreeLegQuotientPasting (1.5s)
✔ [4880/8991] Built Iut.Foundations.SourceCategoryFiveLegPasting (1.4s)
✔ [4881/8991] Built Iut.Foundations.SourceFiniteEtaleSignQuotientReindexHomExt (3.6s)
✔ [4882/8991] Built Iut.Foundations.SourceFiniteEtaleSignQuotientAssociatedStackCoverConeLiftToTestPasting (1.4s)
✔ [4883/8991] Built Iut.Foundations.SourceEqualityProofPackage (351ms)
✔ [4884/8991] Built Iut.Foundations.SourceCategoryReplaceRightmostFactor (1.4s)
✔ [4885/8991] Built Iut.Foundations.SourceCategoryReplaceTwoRightFactors (1.3s)
✔ [4886/8991] Built Iut.Foundations.SourceCategoryPrefixFactorPasting (1.4s)
✔ [4887/8991] Built Iut.Foundations.SourceCategoryTwoCompatibilityPasting (1.4s)
✔ [4888/8991] Built Iut.Foundations.SourceCategoryCongrThreeFactors (1.4s)
✔ [4889/8991] Built Iut.Foundations.SourceCategoryPackedHEqEndpointLinkDataDependentCongrArg (1.3s)
✔ [4890/8991] Built Iut.Foundations.SourceCategoryThreeMorphismBridgePasting (1.7s)
✔ [4891/8991] Built Iut.Foundations.SourceCategoryTwoMorphismHEqPastingData (1.4s)
✔ [4892/8991] Built Iut.Foundations.SourceOrbicurveFiniteEtaleIteratedBaseChangeReverseFst (3.1s)
✔ [4893/8991] Built Iut.Foundations.SourceFiniteEtaleSignQuotientPointIdentityReconstructionTotalNaturality (4.4s)
✔ [4894/8991] Built Iut.Foundations.SourceEtalePseudofunctorYonedaRecoveryModificationNaturality (4.8s)
✔ [4895/8991] Built Iut.Foundations.SourceCategoryHEqEndpointProjections (1.4s)
✔ [4896/8991] Built Iut.Foundations.SourceEtaleStackSchemeAtlasFiniteEtaleDescentComparisonConverse (2.8s)
✔ [4897/8991] Built Iut.Foundations.SourceFinitaryExtensiveComplementComparison (1.9s)
✔ [4898/8991] Built Iut.Foundations.SourceFiniteEtaleSchemeCoverBaseChangeIso (3.5s)
✔ [4899/8991] Built Iut.Foundations.SourceGaloisFiberFunctorFiniteColimits (2.0s)
✔ [4900/8991] Built Iut.Foundations.SourceConnectedFiniteEtaleConverse (4.7s)
✔ [4901/8991] Built Iut.Foundations.SourceContinuousActionRestrictionSurjectivity (4.1s)
✔ [4902/8991] Built Iut.Foundations.SourceMorphismPropertyOverPullbackCongrProjection (1.6s)
✔ [4903/8991] Built Iut.Foundations.SourceFiniteAlgebraSeparableClosureFactorization (2.8s)
✔ [4904/8991] Built Iut.Foundations.SourceProfiniteKernelLift (3.1s)
✔ [4905/8991] Built Iut.Foundations.SourceSelectedFiberSurjectiveMapData (345ms)
✔ [4906/8991] Built Iut.Foundations.SourcePullbackSelectedSectionAction (1.7s)
✔ [4907/8991] Built Iut.Foundations.SourceCategoryTheoryEqToIsoFintypeComponentHEq (1.5s)
✔ [4908/8991] Built Iut.Foundations.SourceCategoryTheoryDetachedNaturalityPastingMaps (1.4s)
✔ [4909/8991] Built Iut.Foundations.SourceProfiniteClosedSubgroupOpenExtension (2.0s)
✔ [4910/8991] Built Iut.Foundations.SourcePretransitiveContinuousActionCoset (3.4s)
✔ [4911/8991] Built Iut.Foundations.SourcePointedAnabelioidFiberEquivariance (2.8s)
✔ [4912/8991] Built Iut.Foundations.SourceSpecRingHomSemiconjugacy (2.2s)
✔ [4913/8991] Built Iut.Foundations.SourceCategoryTheoryIsoRightFactorInvOfHomEq (1.4s)
✔ [4914/8991] Built Iut.Foundations.SourceFintypeCatFunctorMapCompApply (1.5s)
✔ [4915/8991] Built Iut.Foundations.SourceCategoryPackedTwoProjectionPasting (1.4s)
✔ [4916/8991] Built Iut.Foundations.SourceCategoryHEqPrecomposition (1.4s)
✔ [4917/8991] Built Iut.Foundations.SourceCategoryTheoryEquivalenceInverseObjectIsoCounit (1.4s)
✔ [4918/8991] Built Iut.Foundations.SourceCategoryTwoMorphismEquationDataOfCompositeEq (1.4s)
✔ [4919/8991] Built Iut.Foundations.SourceHEqTransExplicit (1.3s)
✔ [4920/8991] Built Iut.Foundations.SourceCategoryPackedHEqEndpointLinkDataCommonRightComparisonData (1.4s)
✔ [4921/8991] Built Iut.Foundations.SourceFunctionPointwiseFactorizationData (341ms)
✔ [4922/8991] Built Iut.Foundations.SourceFintypeFunctorFactorizationApply (1.7s)
✔ [4923/8991] Built Iut.Foundations.SourceFunctionHEqCastMapData (344ms)
✔ [4924/8991] Built Iut.Foundations.SourceFunctionPointwiseEqualityData (362ms)
✔ [4925/8991] Built Iut.Foundations.SourceFunctionHEqCongr (342ms)
✔ [4926/8991] Built Iut.Foundations.SourceCategoryPackedHEqEndpointLinkDataHiddenEndpointStorage (1.4s)
✔ [4927/8991] Built Iut.Foundations.SourceCategoryPackedHEqEndpointLinkDataOfTwoHEq (1.4s)
✔ [4928/8991] Built Iut.Foundations.SourceCategoryPackedHEqEndpointLinkDataCommonMiddleProjectionData (1.5s)
✔ [4929/8991] Built Iut.Foundations.SourceSelectedFiberComponentDomination (1.5s)
✔ [4930/8991] Built Iut.Foundations.SourceContinuousActionRestrictionComponentStability (3.4s)
✔ [4931/8991] Built Iut.Foundations.SourceHEqApply (347ms)
✔ [4932/8991] Built Iut.Foundations.SourceEtalePseudofunctorPointIdentityReconstructionNaturality (4.9s)
✔ [4933/8991] Built Iut.Foundations.SourceCategoryProjectionEndpointHEqWhisker (1.5s)
✔ [4934/8991] Built Iut.Foundations.SourceEtaleStackSchemeAtlasFiniteEtaleDescentObjectPullbackProjections (3.3s)
✔ [4935/8991] Built Iut.Foundations.SourceFiniteEtaleSignTorsorTrivialAtlasFirstSheetExt (3.6s)
✔ [4936/8991] Built Iut.Foundations.SourceOrbicurveFiniteEtaleBaseChangePointIsoToSource (3.1s)
✔ [4937/8991] Built Iut.Foundations.SourceEtaleStackSchemeAtlasFiniteEtaleDescentOverlapComparisonLeft (3.1s)
✔ [4938/8991] Built Iut.Foundations.SourceOrbicurveFiniteEtaleIteratedBaseChangeReverseLeftProjection (2.0s)
✔ [4939/8991] Built Iut.Foundations.SourceCategoryInvolutiveActionTransport (1.5s)
✔ [4940/8991] Built Iut.Foundations.SourceRegularInvolutivePullbackFiberSwap (1.0s)
✔ [4941/8991] Built Iut.Foundations.SourceEtaleStackFiniteEtaleComposition (5.7s)
✔ [4942/8991] Built Iut.Foundations.SourceCategoryProjectionEndpointLinkContext (1.3s)
✔ [4943/8991] Built Iut.Foundations.SourceCategoryDetachedHEqData (341ms)
✔ [4944/8991] Built Iut.Foundations.SourceCategoryComparisonProjectionContext (1.4s)
✔ [4945/8991] Built Iut.Foundations.SourceCategoryDetachedEqDataProjections (317ms)
✔ [4946/8991] Built Iut.Foundations.SourceProfinitePostcompositionKernelIso (4.5s)
✔ [4947/8991] Built Iut.Foundations.SourceOrbicurveFiniteEtaleCoverStabilizerExactSequence (2.0s)
✔ [4948/8991] Built Iut.Foundations.SourceProfiniteOpenSubgroupKernelIso (3.7s)
✔ [4949/8991] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalHomPointIsoNaturality (3.3s)
✔ [4950/8991] Built Iut.Foundations.SourceOrbicurveSignInvariantCategory (3.2s)
✔ [4951/8991] Built Iut.Foundations.SourcePseudofunctorStrongTransCompNaturalityInvApp (1.8s)
✔ [4952/8991] Built Iut.Foundations.SourceCategoryFunctorSquarePasting (1.5s)
✔ [4953/8992] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapPointTripleBaseInverseTailLeftHomProjection (3.2s)
✔ [4954/8992] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapPointTripleCocycleBaseInverseTerminalHom (2.0s)
✔ [4955/8992] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapPointTripleCocycleNormalizedAtlasMiddleHom (2.9s)
✔ [4956/8992] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapPointTripleEdgeConeIso (3.2s)
⚠ [4957/8992] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapPointTripleCocycleToTwoValueIsoHom (3.2s)
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`
✔ [4958/8992] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapPointTripleOverlapCompositeTargetToCocycleHom (3.1s)
✔ [4959/8992] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapPointTripleCocycleToZeroValueIsoHom (3.2s)
✔ [4960/8992] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapPointOverlapValueDirectMiddleFactor (3.3s)
✔ [4961/8992] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapPointTripleOverlapValueDirectFactorDataMapped (3.2s)
✔ [4962/8992] Built Iut.Foundations.SourceEtaleRepresentedStrongTransPointIsoWhiskerRightSymmInv (2.9s)
✔ [4963/8992] Built Iut.Foundations.SourceEtaleRepresentedStrongTransPointIsoAssociatorNaturalityMiddleInverseSolve (3.2s)
✔ [4964/8992] Built Iut.Foundations.SourceEtaleRepresentedStrongTransPointIsoAssociatorNaturalityMiddleInv (3.1s)
✔ [4965/8992] Built Iut.Foundations.SourceEtaleRepresentedStrongTransPointIsoAssociatorInvAbsorbPointTransport (3.0s)
✔ [4966/8992] Built Iut.Foundations.SourceEtaleStackSchemeAtlasSourceAtlasOverlapCanonicalComparisonLeftExpandedFirstWhiskeredHom (3.3s)
✔ [4967/8992] Built Iut.Foundations.SourceEtaleStackSchemeAtlasMapCechCocycle (3.2s)
✔ [4968/8992] Built Iut.Foundations.SourceFiniteEtaleTensorAction (3.8s)
✔ [4969/8992] Built Iut.Foundations.SourceFiniteEtaleSignQuotientAffineChartCompositionCoherence (4.1s)
✔ [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.3s)
✔ [4974/8992] Built Iut.Foundations.SourceEtalePseudofunctorTwoPullbackCancellationTwoCellYTargetToY (3.1s)
✔ [4975/8992] Built Iut.Foundations.SourceFiberFunctorComparison (2.4s)
✔ [4976/8992] Built Iut.Foundations.SourceSchemeEtaleStackPresentationReverseFiniteEtaleCover (3.0s)
✔ [4977/8992] Built Iut.Foundations.SourceEtalePseudofunctorContractiblePullbackEquivalence (3.8s)
✔ [4978/8992] Built Iut.Foundations.SourcePreGaloisFiberFunctorEquivalenceTransport (1.7s)
✔ [4979/8992] Built Iut.Foundations.SourcePseudofunctorRestrictionPullHom (2.1s)
✔ [4980/8992] Built Iut.Foundations.SourceSchemeOverFieldRestrictScalarsSliceEquivalence (4.2s)
✔ [4981/8992] Built Iut.Foundations.SourceEtaleFundamentalGroupCoverActionEquivalence (2.6s)
✔ [4983/8992] Built Iut.Foundations.SourceCategoryFourLegSquareReassociation (1.3s)
✔ [4984/8992] Built Iut.Foundations.SourcePseudofunctorStrongTransEndpointPullLeft (1.9s)
✔ [4985/8992] Built Iut.Foundations.SourcePseudofunctorStrongTransEndpointPullRight (2.3s)
✔ [4986/8992] Built Iut.Foundations.SourceEtaleStackSchemeAtlasBaseChangePointIsoSource (2.9s)
✔ [4987/8992] Built Iut.Foundations.SourceCategoryFunctorMapSubsingletonComposition (1.5s)
✔ [4988/8992] Built Iut.Foundations.SourceCategoryEndpointTransportPasting (1.5s)
✔ [4989/8992] Built Iut.Foundations.SourceCategoryMappedTwoThreePasting (1.4s)
✔ [4990/8992] Built Iut.Foundations.SourceFiniteEtaleSignQuotientAtlasPointFiberIsoNaturalityFirstSheet (5.4s)
✔ [4991/8992] Built Iut.Foundations.SourceCategoryMappedNaturalityPasting (1.5s)
✔ [4992/8992] Built Iut.Foundations.SourceCategoryPullNaturalityThroughIso (1.5s)
✔ [4993/8992] Built Iut.Foundations.SourceCategoryThreeFactorIsoRecoveryData (1.4s)
✔ [4994/8992] Built Iut.Foundations.SourceCategoryThreeMapHEq (1.4s)
✔ [4995/8992] Built Iut.Foundations.SourceCategoryRecoverFactorThroughMappedIso (1.5s)
✔ [4996/8992] Built Iut.Foundations.SourceEtalePseudofunctorYonedaIdentityBaseChange (3.4s)
✔ [4997/8992] Built Iut.Foundations.SourceInitialTheta11a1DivisionRootFiberToThirtyTorsion (3.0s)
✔ [4998/8992] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapOverlapPairWhiskeredNestedFactorization (3.0s)
✔ [4999/8992] Built Iut.Foundations.SourceEtaleRepresentedStrongTransPointIsoWhiskerLeftTargetTransportRightDataRight (2.9s)
⚠ [5001/8992] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapPointTripleNaturalityAppTransportDataEndpoints (3.7s)
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.1s)
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.SourceTensorProductAlgebraicFiniteStage (3.2s)
✔ [5004/8992] Built Iut.Foundations.SourceFiniteEtaleAffinePullbackActionReversedTensor (4.2s)
✔ [5005/8992] Built Iut.Foundations.SourceEtaleStackSchemeAtlasFiniteEtalePreDescentPullbacks (7.5s)
✔ [5006/8992] Built Iut.Foundations.SourceEtaleStackSchemeAtlasFiniteEtaleDescentTerminal (3.1s)
✔ [5007/8992] Built Iut.Foundations.SourceFiniteEtaleSchemeCoverBaseChangeFiniteCoproducts (3.5s)
✔ [5008/8992] Built Iut.Foundations.SourceInvolutiveEndofunctorEquivariantForgetReflectsLimits (1.8s)
✔ [5009/8992] Built Iut.Foundations.SourceInvolutiveEndofunctorEquivariantFreeObject (1.0s)
✔ [5010/8992] Built Iut.Foundations.SourceInvolutiveEndofunctorEquivariantForgetReflectsIsomorphisms (1.5s)
✔ [5011/8992] Built Iut.Foundations.SourceInvolutiveEndofunctorEquivariantCofreeMono (1.6s)
✔ [5012/8992] Built Iut.Foundations.SourceFiniteEtaleSchemeCoverInvolutivePostcomposition (106s)
✔ [5013/8992] Built Iut.Foundations.SourceTensorProductRightAlgEquivTmul (1.9s)
✔ [5014/8992] Built Iut.Foundations.SourceTensorProductRingHomTmulFactorization (1.8s)
✔ [5015/8992] Built Iut.Foundations.SourceEquivTransportApplyBackTarget (777ms)
✔ [5016/8992] Built Iut.Foundations.SourceSchemePullbackSectionAlongComposite (4.2s)
✔ [5017/8992] Built Iut.Foundations.SourceEtalePseudofunctorConeReplaceCommutesHomTargetIso (2.7s)
✔ [5018/8992] Built Iut.Foundations.SourceFiniteEtaleSignQuotientAtlasSecondSheetTotalSpaces (4.3s)
✔ [5019/8992] Built Iut.Foundations.SourceFiniteEtaleSignQuotientEquivariantMapIdentity (3.8s)
✔ [5020/8992] Built Iut.Foundations.SourceFiniteEtaleSignQuotientEquivariantMapComposition (4.3s)
✔ [5021/8992] Built Iut.Foundations.SourceFiniteEtaleSignTorsorInvariantEffectiveDescent (3.2s)
✔ [5022/8992] Built Iut.Foundations.SourceFiniteEtaleSignQuotientHomTripleCarrier (3.1s)
✔ [5023/8992] Built Iut.Foundations.SourceFiniteEtaleSignQuotientReindexCompInverseToTotal (3.2s)
✔ [5024/8992] Built Iut.Foundations.SourceCategoryThreeMorphismBridgePastingPackedCompletion (1.4s)
✔ [5025/8992] Built Iut.Foundations.SourceFiniteEtaleSignQuotientPointIdentityReconstructionComparison (4.3s)
✔ [5026/8992] Built Iut.Foundations.SourceGaloisFiberFunctorFiniteColimitsHeterogeneous (2.7s)
✔ [5027/8992] Built Iut.Foundations.SourceContinuousActionRestrictionConnectednessSurjectivity (3.7s)
✔ [5028/8992] Built Iut.Foundations.SourceCategoryTheoryEqToIsoFintypeMapApplyHEq (1.6s)
✔ [5029/8992] Built Iut.Foundations.SourceCategoryTheoryIndexedNatIsoTransportFintypeComponentHEq (1.5s)
✔ [5030/8992] Built Iut.Foundations.SourceFintypeDetachedNaturalityIsoExtension (1.8s)
✔ [5031/8992] Built Iut.Foundations.SourceContinuousActionClosedSubgroupAmbientEnvelope (3.8s)
✔ [5032/8992] Built Iut.Foundations.SourcePointedAnabelioidKernelFiberStability (3.1s)
✔ [5033/8992] Built Iut.Foundations.SourceEquivalenceInversePointNaturality (1.7s)
✔ [5034/8992] Built Iut.Foundations.SourceCategoryPackedHEqEndpointLinkDataCommonRightComparisonDataLeftComm (1.4s)
✔ [5035/8992] Built Iut.Foundations.SourceFunctionHEqCastMapDataPostmap (343ms)
✔ [5036/8992] Built Iut.Foundations.SourceFunctionHEqData (1.5s)
✔ [5037/8992] Built Iut.Foundations.SourceCategoryPackedHEqEndpointLinkDataHiddenEndpointStorageExplicit (1.4s)
✔ [5038/8992] Built Iut.Foundations.SourceCategoryPackedHEqEndpointLinkDataCommonMiddleProjectionDataOfExplicitMiddle (1.3s)
✔ [5039/8992] Built Iut.Foundations.SourceSelectedFiberSurjectiveMapDataComponentDomination (1.5s)
✔ [5040/8992] Built Iut.Foundations.SourceFiniteEtaleSignQuotientPointIdentityReconstructionNaturality (3.4s)
✔ [5041/8992] Built Iut.Foundations.SourceEtalePseudofunctorPointIdentityReconstructionComponent (4.2s)
✔ [5042/8992] Built Iut.Foundations.SourceRegularInvolutiveEquivariantExtension (2.5s)
✔ [5043/8992] Built Iut.Foundations.SourceCategoryProjectionEndpointLinkData (1.4s)
✔ [5044/8992] Built Iut.Foundations.SourceCategoryDetachedHEqPastingData (348ms)
✔ [5045/8992] Built Iut.Foundations.SourceCategoryDetachedHEqDataProjections (316ms)
✔ [5046/8992] Built Iut.Foundations.SourceCategoryComparisonProjectionContextLeftWhisker (1.3s)
✔ [5047/8992] Built Iut.Foundations.SourceOrbicurveFiniteEtaleCoverStabilizerProjectionSurjectivity (3.3s)
✔ [5048/8992] Built Iut.Foundations.SourceOrbicurveFiniteEtaleCoverStabilizerKernelIso (2.0s)
✔ [5049/8992] Built Iut.Foundations.SourceEtaleStackSchemeAtlasYonedaFiberNaturalityOfPointIso (3.5s)
✔ [5050/8992] Built Iut.Foundations.SourceEtaleStackSchemeAtlasPointIsoDescentComparison (5.4s)
✔ [5051/8992] Built Iut.Foundations.SourceOrbicurveSignInvariantIso (3.1s)
✔ [5052/8992] Built Iut.Foundations.SourceOrbicurveSignQuotientComparison (3.6s)
✔ [5053/8992] Built Iut.Foundations.SourceCategoryFunctorSquarePastingEvidenceFirst (1.5s)
✔ [5054/8992] Built Iut.Foundations.SourceCategoryFunctorSquarePastingContext (1.6s)
✔ [5056/8992] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapPointTripleCocycleBaseInverseTerminalProjection (3.9s)
✔ [5057/8992] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapPointTripleCocycleNormalizedAtlasMiddleIdentity (3.4s)
✔ [5058/8992] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapPointTriplePastedConeIso (3.1s)
✔ [5059/8992] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapPointTripleLongEdgeGeometricTargetAfterSourceAssociator (3.5s)
✔ [5060/8992] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapPointTripleOverlapValueDirectFactorDataMappedRight (3.2s)
✔ [5061/8992] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapPointTripleCocycleSuccessiveSecondOverlapValueFactorDataMapped (3.2s)
✔ [5062/8992] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapPointTripleCocycleSuccessiveFirstOverlapValueFactorDataMapped (2.9s)
✔ [5063/8992] Built Iut.Foundations.SourceEtaleRepresentedStrongTransPointIsoWhiskerRightWhiskerRightSymmInv (3.1s)
✔ [5064/8992] Built Iut.Foundations.SourceEtaleRepresentedStrongTransPointIsoWhiskerRightCongrIsoSymmInv (3.0s)
⚠ [5065/8992] Built Iut.Foundations.SourceEtaleStackSchemeAtlasSourceAtlasOverlapCanonicalComparisonLeftExpandedSecondWhiskerCongr (3.1s)
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.8s)
✔ [5067/8992] Built Iut.Foundations.SourceFiniteEtaleTensorFixedSubalgebra (4.1s)
✔ [5068/8992] Built Iut.Foundations.SourceFiniteEtaleSignQuotientAffineChartCompositionContext (3.5s)
✔ [5069/8992] Built Iut.Foundations.SourceFiniteEtaleSignQuotientAffineChartGluedInvolution (3.9s)
✔ [5070/8992] Built Iut.Foundations.SourceFiniteEtaleSignQuotientAtlasConeLiftTransportSchemeMap (3.2s)

stderr:
/usr/bin/podman timed out after 7200s
podman cleanup removed verifier container apx-verifier-job-1791-runtime-lean_checker-2467169-1789152962354319706-1 on attempt 1

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

apx-runtime-resource-v1	apx-verifier-job-1791-runtime-blueprint_build-2467169-1789160163067587605-2	946176	1376256	21474836480	0	0	0	0	0	0	11476992	113405952	21474836480	0	0	0	0	0	0


blueprint_build failed; continuing (non-fatal phase).

Command runs

git_cloneexit 128duration 216 ms · created 
git clone --depth 1 --branch e21-924-complete --single-branch https://github.com/promachina/iut-lean.git /var/lib/apodeixis/repos/job-1791-source
Cloning into '/var/lib/apodeixis/repos/job-1791-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-1791-source'...
git_checkoutexit 0duration 364 ms · created 
git checkout 667402efca1a8252df7725a62716678d1e6342c1
Note: switching to '667402efca1a8252df7725a62716678d1e6342c1'.

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 667402e feat(e21): construct 11a1 sign-quotient geometry and fundamental groups
lake_cacheexit 0duration 1m 34s · 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 (546ms)
✔ [10/25] Built Batteries.Data.Array.Match:c.o (1.6s)
✔ [11/25] Built Batteries.Data.String.Basic:c.o (115ms)
✔ [12/25] Built Batteries.Data.String.Matcher:c.o (165ms)
✔ [13/25] Built Cache.Lean:c.o (145ms)
✔ [15/25] Built Cache.Init (417ms)
✔ [16/25] Built Cache.IO (3.1s)
✔ [17/25] Built Cache.Init:c.o (95ms)
✔ [18/25] Built Cache.IO:c.o (1.3s)
✔ [19/25] Built Cache.Hashing (1.1s)
✔ [20/25] Built Cache.Hashing:c.o (395ms)
✔ [21/25] Built Cache.Requests (2.3s)
✔ [22/25] Built Cache.Requests:c.o (1.8s)
✔ [23/25] Built Cache.Main (1.1s)
✔ [24/25] Built Cache.Main:c.o (567ms)
✔ [25/25] Built cache:exe (8.0s)

Downloaded: 1 file(s) [attempted 1/8459 = 0%, 11 KB/s], Decompressed: 0
Downloaded: 14 file(s) [attempted 14/8459 = 0%, 9 KB/s], Decompressed: 5
Downloaded: 34 file(s) [attempted 34/8459 = 0%, 16 KB/s], Decompressed: 20
Downloaded: 57 file(s) [attempted 57/8459 = 0%, 229 KB/s], Decompressed: 39
Downloaded: 81 file(s) [attempted 81/8459 = 0%, 62 KB/s], Decompressed: 57
Downloaded: 107 file(s) [attempted 107/8459 = 1%, 195 KB/s], Decompressed: 75
Downloaded: 141 file(s) [attempted 141/8459 = 1%, 242 KB/s], Decompressed: 75
Downloaded: 175 file(s) [attempted 175/8459 = 2%, 144 KB/s], Decompressed: 103
Downloaded: 209 file(s) [attempted 209/8459 = 2%, 333 KB/s], Decompressed: 103
Downloaded: 244 file(s) [attempted 244/8459 = 2%, 693 KB/s], Decompressed: 151
Downloaded: 278 file(s) [attempted 278/8459 = 3%, 111 KB/s], Decompressed: 151
Downloaded: 309 file(s) [attempted 309/8459 = 3%, 675 KB/s], Decompressed: 151
Downloaded: 346 file(s) [attempted 346/8459 = 4%, 655 KB/s], Decompressed: 220
Downloaded: 384 file(s) [attempted 384/8459 = 4%, 40 KB/s], Decompressed: 220
Downloaded: 418 file(s) [attempted 418/8459 = 4%, 295 KB/s], Decompressed: 312
Downloaded: 456 file(s) [attempted 456/8459 = 5%, 204 KB/s], Decompressed: 312
Downloaded: 490 file(s) [attempted 490/8459 = 5%, 463 KB/s], Decompressed: 312
Downloaded: 527 file(s) [attempted 527/8459 = 6%, 176 KB/s], Decompressed: 312
Downloaded: 565 file(s) [attempted 565/8459 = 6%, 732 KB/s], Decompressed: 415
Downloaded: 601 file(s) [attempted 601/8459 = 7%, 235 KB/s], Decompressed: 415
Downloaded: 641 file(s) [attempted 641/8459 = 7%, 83 KB/s], Decompressed: 415
Downloaded: 682 file(s) [attempted 682/8459 = 8%, 83 KB/s], Decompressed: 415
Downloaded: 726 file(s) [attempted 726/8459 = 8%, 86 KB/s], Decompressed: 415
Downloaded: 760 file(s) [attempted 760/8459 = 8%, 515 KB/s], Decompressed: 548
Downloaded: 802 file(s) [attempted 802/8459 = 9%, 938 KB/s], Decompressed: 548
Downloaded: 842 file(s) [attempted 842/8459 = 9%, 138 KB/s], Decompressed: 548
Downloaded: 877 file(s) [attempted 877/8459 = 10%, 261 KB/s], Decompressed: 548
Downloaded: 918 file(s) [attempted 918/8459 = 10%, 565 KB/s], Decompressed: 548
Downloaded: 962 file(s) [attempted 962/8459 = 11%, 172 KB/s], Decompressed: 747
Downloaded: 1003 file(s) [attempted 1003/8459 = 11%, 521 KB/s], Decompressed: 747
Downloaded: 1048 file(s) [attempted 1048/8459 = 12%, 22 KB/s], Decompressed: 747
Downloaded: 1086 file(s) [attempted 1086/8459 = 12%, 210 KB/s], Decompressed: 747
Downloaded: 1123 file(s) [attempted 1123/8459 = 13%, 138 KB/s], Decompressed: 747
Downloaded: 1161 file(s) [attempted 1161/8459 = 13%, 471 KB/s], Decompressed: 945
Downloaded: 1205 file(s) [attempted 1205/8459 = 14%, 324 KB/s], Decompressed: 945
Downloaded: 1250 file(s) [attempted 1250/8459 = 14%, 580 KB/s], Decompressed: 945
Downloaded: 1294 file(s) [attempted 1294/8459 = 15%, 164 KB/s], Decompressed: 945
Downloaded: 1335 file(s) [attempted 1335/8459 = 15%, 150 KB/s], Decompressed: 945
Downloaded: 1373 file(s) [attempted 1373/8459 = 16%, 348 KB/s], Decompressed: 1161
Downloaded: 1414 file(s) [attempted 1414/8459 = 16%, 419 KB/s], Decompressed: 1161
Downloaded: 1455 file(s) [attempted 1455/8459 = 17%, 46 KB/s], Decompressed: 1161
Downloaded: 1492 file(s) [attempted 1492/8459 = 17%, 200 KB/s], Decompressed: 1161
Downloaded: 1533 file(s) [attempted 1533/8459 = 18%, 161 KB/s], Decompressed: 1352
Downloaded: 1571 file(s) [attempted 1571/8459 = 18%, 87 KB/s], Decompressed: 1352
Downloaded: 1612 file(s) [attempted 1612/8459 = 19%, 323 KB/s], Decompressed: 1352
Downloaded: 1653 file(s) [attempted 1653/8459 = 19%, 129 KB/s], Decompressed: 1352
Downloaded: 1694 file(s) [attempted 1694/8459 = 20%, 1082 KB/s], Decompressed: 1352
Downloaded: 1735 file(s) [attempted 1735/8459 = 20%, 356 KB/s], Decompressed: 1533
Downloaded: 1773 file(s) [attempted 1773/8459 = 20%, 724 KB/s], Decompressed: 1533
Downloaded: 1814 file(s) [attempted 1814/8459 = 21%, 587 KB/s], Decompressed: 1533
Downloaded: 1855 file(s) [attempted 1855/8459 = 21%, 32 KB/s], Decompressed: 1533
Downloaded: 1899 file(s) [attempted 1899/8459 = 22%, 164 KB/s], Decompressed: 1533
Downloaded: 1937 file(s) [attempted 1937/8459 = 22%, 319 KB/s], Decompressed: 1722
Downloaded: 1981 file(s) [attempted 1981/8459 = 23%, 481 KB/s], Decompressed: 1722
Downloaded: 2022 file(s) [attempted 2022/8459 = 23%, 396 KB/s], Decompressed: 1722
Downloaded: 2060 file(s) [attempted 2060/8459 = 24%, 414 KB/s], Decompressed: 1722
Downloaded: 2094 file(s) [attempted 2094/8459 = 24%, 326 KB/s], Decompressed: 1903
Downloaded: 2139 file(s) [attempted 2139/8459 = 25%, 1704 KB/s], Decompressed: 1903
Downloaded: 2180 file(s) [attempted 2180/8459 = 25%, 194 KB/s], Decompressed: 1903
Downloaded: 2217 file(s) [attempted 2217/8459 = 26%, 367 KB/s], Decompressed: 1903
Downloaded: 2258 file(s) [attempted 2258/8459 = 26%, 275 KB/s], Decompressed: 1903
Downloaded: 2299 file(s) [attempted 2299/8459 = 27%, 265 KB/s], Decompressed: 2081
Downloaded: 2337 file(s) [attempted 2337/8459 = 27%, 188 KB/s], Decompressed: 2081
Downloaded: 2378 file(s) [attempted 2378/8459 = 28%, 113 KB/s], Decompressed: 2081
Downloaded: 2419 file(s) [attempted 2419/8459 = 28%, 35 KB/s], Decompressed: 2081
Downloaded: 2460 file(s) [attempted 2460/8459 = 29%, 156 KB/s], Decompressed: 2081
Downloaded: 2496 file(s) [attempted 2496/8459 = 29%, 573 KB/s], Decompressed: 2279
Downloaded: 2539 file(s) [attempted 2539/8459 = 30%, 319 KB/s], Decompressed: 2279
Downloaded: 2576 file(s) [attempted 2576/8459 = 30%, 114 KB/s], Decompressed: 2279
Downloaded: 2617 file(s) [attempted 2617/8459 = 30%, 59 KB/s], Decompressed: 2279
Downloaded: 2659 file(s) [attempted 2659/8459 = 31%, 542 KB/s], Decompressed: 2279
Downloaded: 2693 file(s) [attempted 2693/8459 = 31%, 331 KB/s], Decompressed: 2279
Downloaded: 2734 file(s) [attempted 2734/8459 = 32%, 70 KB/s], Decompressed: 2464
Downloaded: 2771 file(s) [attempted 2771/8459 = 32%, 61 KB/s], Decompressed: 2464
Downloaded: 2809 file(s) [attempted 2809/8459 = 33%, 396 KB/s], Decompressed: 2464
Downloaded: 2847 file(s) [attempted 2847/8459 = 33%, 130 KB/s], Decompressed: 2464
Downloaded: 2884 file(s) [attempted 2884/8459 = 34%, 181 KB/s], Decompressed: 2464
Downloaded: 2929 file(s) [attempted 2929/8459 = 34%, 625 KB/s], Decompressed: 2464
Downloaded: 2966 file(s) [attempted 2966/8459 = 35%, 304 KB/s], Decompressed: 2713
Downloaded: 3004 file(s) [attempted 3004/8459 = 35%, 41 KB/s], Decompressed: 2713
Downloaded: 3041 file(s) [attempted 3041/8459 = 35%, 278 KB/s], Decompressed: 2713
Downloaded: 3082 file(s) [attempted 3082/8459 = 36%, 432 KB/s], Decompressed: 2713
Downloaded: 3120 file(s) [attempted 3120/8459 = 36%, 660 KB/s], Decompressed: 2713
Downloaded: 3161 file(s) [attempted 3161/8459 = 37%, 152 KB/s], Decompressed: 2713
Downloaded: 3202 file(s) [attempted 3202/8459 = 37%, 171 KB/s], Decompressed: 2713
Downloaded: 3236 file(s) [attempted 3236/8459 = 38%, 220 KB/s], Decompressed: 2956
Downloaded: 3277 file(s) [attempted 3277/8459 = 38%, 352 KB/s], Decompressed: 2956
Downloaded: 3315 file(s) [attempted 3315/8459 = 39%, 155 KB/s], Decompressed: 2956
Downloaded: 3356 file(s) [attempted 3356/8459 = 39%, 222 KB/s], Decompressed: 2956
Downloaded: 3397 file(s) [attempted 3397/8459 = 40%, 1108 KB/s], Decompressed: 2956
Downloaded: 3435 file(s) [attempted 3435/8459 = 40%, 254 KB/s], Decompressed: 2956
Downloaded: 3472 file(s) [attempted 3472/8459 = 41%, 333 KB/s], Decompressed: 3206
Downloaded: 3513 file(s) [attempted 3513/8459 = 41%, 22 KB/s], Decompressed: 3206
Downloaded: 3554 file(s) [attempted 3554/8459 = 42%, 88 KB/s], Decompressed: 3206
Downloaded: 3599 file(s) [attempted 3599/8459 = 42%, 177 KB/s], Decompressed: 3206
Downloaded: 3643 file(s) [attempted 3643/8459 = 43%, 112 KB/s], Decompressed: 3438
Downloaded: 3684 file(s) [attempted 3684/8459 = 43%, 173 KB/s], Decompressed: 3438
Downloaded: 3719 file(s) [attempted 3719/8459 = 43%, 334 KB/s], Decompressed: 3438
Downloaded: 3760 file(s) [attempted 3760/8459 = 44%, 43 KB/s], Decompressed: 3438
Downloaded: 3801 file(s) [attempted 3801/8459 = 44%, 285 KB/s], Decompressed: 3438
Downloaded: 3842 file(s) [attempted 3842/8459 = 45%, 161 KB/s], Decompressed: 3636
Downloaded: 3883 file(s) [attempted 3883/8459 = 45%, 207 KB/s], Decompressed: 3636
Downloaded: 3917 file(s) [attempted 3917/8459 = 46%, 223 KB/s], Decompressed: 3636
Downloaded: 3954 file(s) [attempted 3954/8459 = 46%, 193 KB/s], Decompressed: 3636
Downloaded: 3999 file(s) [attempted 3999/8459 = 47%, 693 KB/s], Decompressed: 3636
Downloaded: 4040 file(s) [attempted 4040/8459 = 47%, 99 KB/s], Decompressed: 3636
Downloaded: 4084 file(s) [attempted 4084/8459 = 48%, 858 KB/s], Decompressed: 3831
Downloaded: 4132 file(s) [attempted 4132/8459 = 48%, 271 KB/s], Decompressed: 3831
Downloaded: 4166 file(s) [attempted 4166/8459 = 49%, 259 KB/s], Decompressed: 3831
Downloaded: 4204 file(s) [attempted 4204/8459 = 49%, 126 KB/s], Decompressed: 3831
Downloaded: 4245 file(s) [attempted 4245/8459 = 50%, 76 KB/s], Decompressed: 3831
Downloaded: 4286 file(s) [attempted 4286/8459 = 50%, 62 KB/s], Decompressed: 4047
Downloaded: 4327 file(s) [attempted 4327/8459 = 51%, 1889 KB/s], Decompressed: 4047
Downloaded: 4368 file(s) [attempted 4368/8459 = 51%, 427 KB/s], Decompressed: 4047
Downloaded: 4409 file(s) [attempted 4409/8459 = 52%, 76 KB/s], Decompressed: 4047
Downloaded: 4447 file(s) [attempted 4447/8459 = 52%, 395 KB/s], Decompressed: 4047
Downloaded: 4488 file(s) [attempted 4488/8459 = 53%, 362 KB/s], Decompressed: 4047
Downloaded: 4526 file(s) [attempted 4526/8459 = 53%, 53 KB/s], Decompressed: 4047
Downloaded: 4570 file(s) [attempted 4570/8459 = 54%, 238 KB/s], Decompressed: 4259
Downloaded: 4611 file(s) [attempted 4611/8459 = 54%, 294 KB/s], Decompressed: 4259
Downloaded: 4645 file(s) [attempted 4645/8459 = 54%, 892 KB/s], Decompressed: 4259
Downloaded: 4686 file(s) [attempted 4686/8459 = 55%, 356 KB/s], Decompressed: 4259
Downloaded: 4724 file(s) [attempted 4724/8459 = 55%, 670 KB/s], Decompressed: 4259
Downloaded: 4768 file(s) [attempted 4768/8459 = 56%, 346 KB/s], Decompressed: 4259
Downloaded: 4809 file(s) [attempted 4809/8459 = 56%, 501 KB/s], Decompressed: 4259
Downloaded: 4850 file(s) [attempted 4850/8459 = 57%, 112 KB/s], Decompressed: 4259
Downloaded: 4891 file(s) [attempted 4891/8459 = 57%, 98 KB/s], Decompressed: 4549
Downloaded: 4932 file(s) [attempted 4932/8459 = 58%, 565 KB/s], Decompressed: 4549
Downloaded: 4973 file(s) [attempted 4973/8459 = 58%, 98 KB/s], Decompressed: 4549
Downloaded: 5011 file(s) [attempted 5011/8459 = 59%, 86 KB/s], Decompressed: 4549
Downloaded: 5052 file(s) [attempted 5052/8459 = 59%, 101 KB/s], Decompressed: 4549
Downloaded: 5093 file(s) [attempted 5093/8459 = 60%, 943 KB/s], Decompressed: 4549
Downloaded: 5134 file(s) [attempted 5134/8459 = 60%, 269 KB/s], Decompressed: 4549
Downloaded: 5172 file(s) [attempted 5172/8459 = 61%, 172 KB/s], Decompressed: 4871
Downloaded: 5209 file(s) [attempted 5209/8459 = 61%, 566 KB/s], Decompressed: 4871
Downloaded: 5250 file(s) [attempted 5250/8459 = 62%, 516 KB/s], Decompressed: 4871
Downloaded: 5288 file(s) [attempted 5288/8459 = 62%, 269 KB/s], Decompressed: 4871
Downloaded: 5326 file(s) [attempted 5326/8459 = 62%, 51 KB/s], Decompressed: 4871
Downloaded: 5367 file(s) [attempted 5367/8459 = 63%, 1101 KB/s], Decompressed: 4871
Downloaded: 5411 file(s) [attempted 5411/8459 = 63%, 472 KB/s], Decompressed: 4871
Downloaded: 5450 file(s) [attempted 5450/8459 = 64%, 134 KB/s], Decompressed: 5144
Downloaded: 5486 file(s) [attempted 5486/8459 = 64%, 1061 KB/s], Decompressed: 5144
Downloaded: 5527 file(s) [attempted 5527/8459 = 65%, 118 KB/s], Decompressed: 5144
Downloaded: 5565 file(s) [attempted 5565/8459 = 65%, 78 KB/s], Decompressed: 5144
Downloaded: 5610 file(s) [attempted 5610/8459 = 66%, 176 KB/s], Decompressed: 5144
Downloaded: 5651 file(s) [attempted 5651/8459 = 66%, 199 KB/s], Decompressed: 5144
Downloaded: 5685 file(s) [attempted 5685/8459 = 67%, 134 KB/s], Decompressed: 5432
Downloaded: 5726 file(s) [attempted 5726/8459 = 67%, 666 KB/s], Decompressed: 5432
Downloaded: 5763 file(s) [attempted 5763/8459 = 68%, 109 KB/s], Decompressed: 5432
Downloaded: 5801 file(s) [attempted 5801/8459 = 68%, 104 KB/s], Decompressed: 5432
Downloaded: 5845 file(s) [attempted 5845/8459 = 69%, 230 KB/s], Decompressed: 5432
Downloaded: 5887 file(s) [attempted 5887/8459 = 69%, 693 KB/s], Decompressed: 5661
Downloaded: 5924 file(s) [attempted 5924/8459 = 70%, 201 KB/s], Decompressed: 5661
Downloaded: 5965 file(s) [attempted 5965/8459 = 70%, 88 KB/s], Decompressed: 5661
Downloaded: 6003 file(s) [attempted 6003/8459 = 70%, 509 KB/s], Decompressed: 5661
Downloaded: 6044 file(s) [attempted 6044/8459 = 71%, 1506 KB/s], Decompressed: 5661
Downloaded: 6088 file(s) [attempted 6088/8459 = 71%, 303 KB/s], Decompressed: 5661
Downloaded: 6129 file(s) [attempted 6129/8459 = 72%, 120 KB/s], Decompressed: 5661
Downloaded: 6163 file(s) [attempted 6163/8459 = 72%, 202 KB/s], Decompressed: 5887
Downloaded: 6201 file(s) [attempted 6201/8459 = 73%, 490 KB/s], Decompressed: 5887
Downloaded: 6246 file(s) [attempted 6246/8459 = 73%, 70 KB/s], Decompressed: 5887
Downloaded: 6287 file(s) [attempted 6287/8459 = 74%, 191 KB/s], Decompressed: 5887
Downloaded: 6331 file(s) [attempted 6331/8459 = 74%, 49 KB/s], Decompressed: 5887
Downloaded: 6369 file(s) [attempted 6369/8459 = 75%, 191 KB/s], Decompressed: 5887
Downloaded: 6406 file(s) [attempted 6406/8459 = 75%, 281 KB/s], Decompressed: 5887
Downloaded: 6447 file(s) [attempted 6447/8459 = 76%, 310 KB/s], Decompressed: 6153
Downloaded: 6488 file(s) [attempted 6488/8459 = 76%, 175 KB/s], Decompressed: 6153
Downloaded: 6533 file(s) [attempted 6533/8459 = 77%, 54 KB/s], Decompressed: 6153
Downloaded: 6570 file(s) [attempted 6570/8459 = 77%, 146 KB/s], Decompressed: 6153
Downloaded: 6608 file(s) [attempted 6608/8459 = 78%, 510 KB/s], Decompressed: 6153
Downloaded: 6649 file(s) [attempted 6649/8459 = 78%, 292 KB/s], Decompressed: 6153
Downloaded: 6690 file(s) [attempted 6690/8459 = 79%, 902 KB/s], Decompressed: 6153
Downloaded: 6731 file(s) [attempted 6731/8459 = 79%, 925 KB/s], Decompressed: 6153
Downloaded: 6769 file(s) [attempted 6769/8459 = 80%, 121 KB/s], Decompressed: 6153
Downloaded: 6810 file(s) [attempted 6810/8459 = 80%, 175 KB/s], Decompressed: 6434
Downloaded: 6851 file(s) [attempted 6851/8459 = 80%, 266 KB/s], Decompressed: 6434
Downloaded: 6892 file(s) [attempted 6892/8459 = 81%, 230 KB/s], Decompressed: 6434
Downloaded: 6929 file(s) [attempted 6929/8459 = 81%, 244 KB/s], Decompressed: 6434
Downloaded: 6967 file(s) [attempted 6967/8459 = 82%, 41 KB/s], Decompressed: 6434
Downloaded: 7008 file(s) [attempted 7008/8459 = 82%, 340 KB/s], Decompressed: 6434
Downloaded: 7046 file(s) [attempted 7046/8459 = 83%, 138 KB/s], Decompressed: 6434
Downloaded: 7090 file(s) [attempted 7090/8459 = 83%, 1134 KB/s], Decompressed: 6434
Downloaded: 7128 file(s) [attempted 7128/8459 = 84%, 111 KB/s], Decompressed: 6434
Downloaded: 7162 file(s) [attempted 7162/8459 = 84%, 472 KB/s], Decompressed: 6434
Downloaded: 7206 file(s) [attempted 7206/8459 = 85%, 128 KB/s], Decompressed: 6793
Downloaded: 7251 file(s) [attempted 7251/8459 = 85%, 66 KB/s], Decompressed: 6793
Downloaded: 7292 file(s) [attempted 7292/8459 = 86%, 597 KB/s], Decompressed: 6793
Downloaded: 7330 file(s) [attempted 7330/8459 = 86%, 163 KB/s], Decompressed: 6793
Downloaded: 7367 file(s) [attempted 7367/8459 = 87%, 81 KB/s], Decompressed: 6793
Downloaded: 7405 file(s) [attempted 7405/8459 = 87%, 155 KB/s], Decompressed: 6793
Downloaded: 7453 file(s) [attempted 7453/8459 = 88%, 429 KB/s], Decompressed: 6793
Downloaded: 7497 file(s) [attempted 7497/8459 = 88%, 159 KB/s], Decompressed: 6793
Downloaded: 7535 file(s) [attempted 7535/8459 = 89%, 515 KB/s], Decompressed: 6793
Downloaded: 7572 file(s) [attempted 7572/8459 = 89%, 249 KB/s], Decompressed: 6793
Downloaded: 7613 file(s) [attempted 7613/8459 = 89%, 179 KB/s], Decompressed: 7189
Downloaded: 7654 file(s) [attempted 7654/8459 = 90%, 122 KB/s], Decompressed: 7189
Downloaded: 7695 file(s) [attempted 7695/8459 = 90%, 350 KB/s], Decompressed: 7189
Downloaded: 7740 file(s) [attempted 7740/8459 = 91%, 765 KB/s], Decompressed: 7189
Downloaded: 7781 file(s) [attempted 7781/8459 = 91%, 80 KB/s], Decompressed: 7189
Downloaded: 7819 file(s) [attempted 7819/8459 = 92%, 94 KB/s], Decompressed: 7189
Downloaded: 7858 file(s) [attempted 7858/8459 = 92%, 32 KB/s], Decompressed: 7189
Downloaded: 7897 file(s) [attempted 7897/8459 = 93%, 191 KB/s], Decompressed: 7189
Downloaded: 7938 file(s) [attempted 7938/8459 = 93%, 254 KB/s], Decompressed: 7189
Downloaded: 7979 file(s) [attempted 7979/8459 = 94%, 977 KB/s], Decompressed: 7189
Downloaded: 8020 file(s) [attempted 8020/8459 = 94%, 241 KB/s], Decompressed: 7189
Downloaded: 8065 file(s) [attempted 8065/8459 = 95%, 79 KB/s], Decompressed: 7189
Downloaded: 8099 file(s) [attempted 8099/8459 = 95%, 167 KB/s], Decompressed: 7189
Downloaded: 8140 file(s) [attempted 8140/8459 = 96%, 75 KB/s], Decompressed: 7589
Downloaded: 8181 file(s) [attempted 8181/8459 = 96%, 379 KB/s], Decompressed: 7589
Downloaded: 8222 file(s) [attempted 8222/8459 = 97%, 464 KB/s], Decompressed: 7589
Downloaded: 8263 file(s) [attempted 8263/8459 = 97%, 891 KB/s], Decompressed: 7589
Downloaded: 8297 file(s) [attempted 8297/8459 = 98%, 91 KB/s], Decompressed: 7589
Downloaded: 8335 file(s) [attempted 8335/8459 = 98%, 1102 KB/s], Decompressed: 7589
Downloaded: 8379 file(s) [attempted 8379/8459 = 99%, 120 KB/s], Decompressed: 7589
Downloaded: 8427 file(s) [attempted 8427/8459 = 99%, 332 KB/s], Decompressed: 7589
Downloaded: 8458 file(s) [attempted 8458/8459 = 99%, 506 KB/s], Decompressed: 7589
Downloaded: 8459 file(s) [attempted 8459/8459 = 100%, 506 KB/s], Decompressed: 7589

apx-runtime-resource-v1	apx-verifier-job-1791-runtime-lake_cache-2467169-1789152868153003324-0	888832	1409024	21474836480	0	0	0	0	0	0	7798353920	8087695360	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.9s)
✔ [4607/6595] Built Iut.Foundations.SourceFiniteEtaleAffineOverCoordinateAction (2.5s)
✔ [4609/6595] Built Iut.Foundations.SourceSingleObjOppositeEquivalence (1.6s)
✔ [4610/6595] Built Iut.Foundations.SourceEtalePseudofunctorRepresentablePullbackTwoCell (118s)
✔ [4611/6595] Built Iut.Foundations.SourceCategoryPackedHEqEndpointLinkDataJoinProjections (1.3s)
✔ [4612/6595] Built Iut.Foundations.SourceEtalePseudofunctorStrongTransWhiskerRightIsoSymmHom (2.8s)
✔ [4613/6595] Built Iut.Foundations.SourceEtalePseudofunctorStrongTransPentagonInvPrefix (4.3s)
✔ [4614/6595] Built Iut.Foundations.SourceCategoryEqToHomTransportedEndpointDataMap (1.5s)
✔ [4615/6595] Built Iut.Foundations.SourceEtalePseudofunctorChangeFirstBaseMap (3.9s)
✔ [4616/6595] Built Iut.Foundations.SourceEtalePseudofunctorChangeSecondBaseMap (3.8s)
✔ [4617/6595] Built Iut.Foundations.SourceEtalePseudofunctorFaithfulCellAssembly (3.9s)
✔ [4618/6595] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalHomPointValueRecovery (2.0s)
✔ [4619/6595] Built Iut.Foundations.SourceFiniteEtaleSchemeCoverClopenMono (2.0s)
⚠ [4621/6595] Built Iut.Foundations.SourceFiniteEtaleSignTorsorAffineEffectiveness (174s)
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`
✔ [4622/6595] Built Iut.Foundations.SourceFiniteEtaleSignQuotientPrestack (42s)
✔ [4623/6595] Built Iut.Foundations.SourceFiniteEtaleSignTorsorTargetStackDescent (2.0s)
✔ [4624/6595] Built Iut.Foundations.SourceFiniteEtaleSignTorsorTrivial (4.7s)
✔ [4625/6595] Built Iut.Foundations.SourceEtalePseudofunctorTwoPullbackCancellationLiftToYLawful (2.7s)
✔ [4626/6595] Built Iut.Foundations.SourceFiniteEtaleAffineOverCoordinateFiniteEtale (2.5s)
✔ [4627/6595] Built Iut.Foundations.SourceEtalePseudofunctorRepresentablePullbackWitness (2.9s)
✔ [4628/6595] Built Iut.Foundations.SourceCategoryPackedHEqTwoMorphismComposition (1.5s)
✔ [4629/6595] Built Iut.Foundations.SourceEtaleStackRepresentablePropertyChangeMap (2.8s)
✔ [4630/6595] Built Iut.Foundations.SourceEtalePseudofunctorConeAfterChangeSecondBaseMap (3.2s)
✔ [4631/6595] Built Iut.Foundations.SourceEtalePseudofunctorRepresentedIsoPointLift (3.5s)
✔ [4632/6595] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalHomYonedaPointValue (2.9s)
✔ [4633/6595] Built Iut.Foundations.SourceFiniteEtaleSchemeCoverDirectSummand (3.4s)
✔ [4634/6595] Built Iut.Foundations.SourceFiniteEtaleSchemeCoverUnderlyingEpiRange (2.0s)
⚠ [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 (3.1s)
✔ [4637/6598] Built Iut.Foundations.SourceFiniteEtaleSignQuotientAtlas (5.7s)
✔ [4638/6599] Built Iut.Foundations.SourceEtalePseudofunctorTwoPullbackCancellationLiftToYHomToX (2.9s)
✔ [4639/6599] Built Iut.Foundations.SourceRepresentableStrongTransReconstruction (3.2s)
✔ [4640/6599] Built Iut.Foundations.SourceEtalePseudofunctorConeAfterChangeSecondBaseMapFromConeOf (3.2s)
✔ [4641/6599] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalIsoBaseChangeOver (3.4s)
✔ [4642/6599] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalHomYonedaNaturality (2.0s)
✔ [4643/6599] Built Iut.Foundations.SourceFiniteEtaleSchemeCoverAffineSource (2.9s)
✔ [4644/6599] Built Iut.Foundations.SourceFiniteEtaleSchemeCoverUnderlyingEpiSurjective (7.0s)
⚠ [4645/6599] Built Iut.Foundations.SourceFiniteEtaleSignTorsorAffineCoverAssembly (883s)
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 (17s)
✔ [4648/6599] Built Iut.Foundations.SourceEtalePseudofunctorTwoPullbackCancellationLiftToYHomToY (2.8s)
✔ [4650/6599] Built Iut.Foundations.SourceEtaleStackRepresentableLocalIsoDescent (3.9s)
✔ [4651/6599] Built Iut.Foundations.SourceEtaleStackSchemeAtlasOverlapMultiplication (3.2s)
✔ [4652/6599] Built Iut.Foundations.SourceEtalePseudofunctorRepresentablePullbackAlongStrongTrans (4.1s)
✔ [4653/6599] Built Iut.Foundations.SourceFiniteEtaleSchemeCoverAffineGroupQuotient (3.3s)
✔ [4654/6599] Built Iut.Foundations.SourceFiniteEtaleSchemeCoverBalanced (2.6s)
✔ [4655/6599] Built Iut.Foundations.SourceFiniteEtaleSignTorsorAffineCoverRestriction (125s)
✔ [4656/6599] Built Iut.Foundations.SourceFiniteEtaleSignQuotientAtlasLiftApp (127s)
✔ [4657/6599] Built Iut.Foundations.SourceFiniteEtaleSignQuotientAtlasInvariant (3.5s)
✔ [4659/6600] Built Iut.Foundations.SourceEtalePseudofunctorTwoPullbackCancellationLiftCompatibility (2.8s)
✔ [4660/6600] Built Iut.Foundations.SourceEtaleStackRepresentableAtlasLocalIsoDescent (3.2s)
✔ [4661/6600] Built Iut.Foundations.SourceOrbicurveFiniteEtaleBaseChangeSchemeCoverMapReflectsLocalIso (3.5s)
✔ [4662/6602] Built Iut.Foundations.SourceEtaleStackSchemeAtlasOverlapMultiplicationRepresentedLongConeIso (3.0s)
✔ [4663/6602] Built Iut.Foundations.SourceEtaleStackSchemeAtlasOverlapConePasting (3.0s)
✔ [4664/6602] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapCechData (3.1s)
✔ [4665/6602] Built Iut.Foundations.SourceEtaleStackSchemeAtlasFiniteEtaleDescent (3.3s)
✔ [4666/6602] Built Iut.Foundations.SourceOrbicurveFiniteEtaleIteratedBaseChange (9.6s)
✔ [4667/6602] Built Iut.Foundations.SourceFiniteEtaleSchemeCoverAffineOverFullyFaithful (2.7s)
✔ [4668/6602] Built Iut.Foundations.SourceFiniteEtaleFixedSubalgebra (3.2s)
✔ [4669/6602] Built Iut.Foundations.SourceFiniteEtaleSignTorsorAffineCoverFiniteEffectivity (3.7s)
✔ [4670/6602] Built Iut.Foundations.SourceFiniteEtaleSignQuotientAtlasLiftNaturality (103s)
✔ [4671/6602] Built Iut.Foundations.SourceFiniteEtaleSignQuotientAtlasInvariantElement (3.2s)
✔ [4673/6602] Built Iut.Foundations.SourceEtalePseudofunctorTwoPullbackCancellationConeMorphismCompatibility (3.1s)
✔ [4676/6604] Built Iut.Foundations.SourceEtaleStackSchemeAtlasOverlapConePastingIso (4.3s)
✔ [4677/6604] Built Iut.Foundations.SourceEtaleStackSchemeAtlasOverlapConePastingCell (3.1s)
✔ [4678/6604] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapRestrictionCongrIsoNaturality (3.3s)
✔ [4679/6604] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapRestrictionCongrIsoWhiskerRightFactorization (3.1s)
✔ [4680/6604] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapOverlapNestedMiddleIso (2.8s)
✔ [4681/6604] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapPointObject (2.9s)
✔ [4682/6604] Built Iut.Foundations.SourceEtaleStackSchemeAtlasFiniteEtaleDescentComparison (3.2s)
✔ [4683/6604] Built Iut.Foundations.SourceEtaleStackSchemeAtlasMapCechEndpointIsos (3.0s)
✔ [4684/6604] Built Iut.Foundations.SourceEtaleStackSchemeAtlasBaseChangePointIso (3.1s)
✔ [4685/6604] Built Iut.Foundations.SourceOrbicurveFiniteEtaleIteratedBaseChangeForwardBackLiftedHom (3.4s)
✔ [4686/6604] Built Iut.Foundations.SourceEtaleStackSchemeAtlasOverlapMapIso (2.9s)
✔ [4687/6604] Built Iut.Foundations.SourceOrbicurveFiniteEtaleIteratedBaseChangeToSourceIso (2.0s)
✔ [4688/6604] Built Iut.Foundations.SourceFiniteEtaleFixedAffineQuotient (3.3s)
✔ [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.5s)
✔ [4695/6605] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapOverlapNestedMiddleHom (3.0s)
✔ [4696/6605] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapOverlapNestedEndpointIsos (2.8s)
✔ [4697/6605] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapPointOverlap (3.3s)
✔ [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 (3.0s)
✔ [4702/6605] Built Iut.Foundations.SourceFiniteEtaleOrbitConstantAlgebra (3.2s)
✔ [4703/6605] Built Iut.Foundations.SourceFiniteEtaleSignQuotientStackRefinement (3.3s)
✔ [4704/6605] Built Iut.Foundations.SourceFiniteEtaleSignQuotientAtlasLiftProjections (13s)
✔ [4705/6605] Built Iut.Foundations.SourceFiniteEtaleSignQuotientAtlasInvariantCocycle (20s)
✔ [4706/6607] Built Iut.Foundations.SourceEtalePseudofunctorTwoPullbackCancellationTwoCell (2.6s)
✔ [4709/6607] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapOverlapNestedMiddleCompositeFactorization (3.3s)
✔ [4710/6607] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapPullbackOverlapNestedFactorization (3.4s)
✔ [4711/6607] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapPointTransition (3.3s)
✔ [4712/6607] Built Iut.Foundations.SourceOrbicurveFiniteEtaleBaseChangePointIsoToSourceIso (2.8s)
✔ [4713/6607] Built Iut.Foundations.SourceEtaleStackSchemeAtlasFiniteEtaleDescentCoherence (13s)
✔ [4714/6607] Built Iut.Foundations.SourceEtaleStackSchemeAtlasMapCechPairFactorization (22s)
✔ [4715/6607] Built Iut.Foundations.SourceOrbicurveFiniteEtaleIteratedBaseChangeForwardBackStrongTransToSource (3.1s)
✔ [4716/6607] Built Iut.Foundations.SourceFiniteEtaleSplitAlgebraHom (3.3s)
✔ [4717/6607] Built Iut.Foundations.SourceFiniteEtaleSignQuotientAffineChartDescent (16s)
✔ [4718/6607] Built Iut.Foundations.SourceFiniteEtaleSignQuotientAtlasLiftTwoCell (297s)
✔ [4719/6607] Built Iut.Foundations.SourceFiniteEtaleSignQuotientAtlasLiftUnit (15s)
✔ [4720/6609] Built Iut.Foundations.SourceEtalePseudofunctorTwoPullbackCancellationTwoCellToX (2.8s)
✔ [4722/6609] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapOverlapNestedMiddleCompositeTargetCollapse (3.2s)
✔ [4723/6609] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapOverlapNestedMiddleCompositeSourceCollapse (3.1s)
✔ [4724/6609] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapOverlapNestedSpecializations (3.1s)
✔ [4725/6609] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapOverlapCompositeWhiskeredExpansion (3.1s)
✔ [4726/6609] Built Iut.Foundations.SourceEtaleRepresentedRestrictionPointIsoCongruenceTail (3.0s)
✔ [4727/6609] Built Iut.Foundations.SourceEtaleRepresentedStrongTransPointIsoWhiskerRightHom (3.0s)
✔ [4728/6609] Built Iut.Foundations.SourceEtaleRepresentedStrongTransPointIsoWhiskerLeft (3.0s)
✔ [4729/6609] Built Iut.Foundations.SourceEtaleRepresentedStrongTransPointIsoSymmHom (2.0s)
✔ [4730/6609] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapPointOverlapValueIsoRepresented (2.0s)
✔ [4731/6609] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapPointCocycleGeometry (3.2s)
✔ [4732/6609] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapCechCocyclePointValue (2.9s)
✔ [4733/6609] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapRestrictionCompositePointIsoHom (6.0s)
⚠ [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 (3.1s)
✔ [4739/6609] Built Iut.Foundations.SourceEtaleStackSchemeAtlasMapCechPairLongFactorization (3.0s)
✔ [4740/6609] Built Iut.Foundations.SourceOrbicurveFiniteEtaleIteratedBaseChangeForwardBackRealizationToSourceExpansion (3.1s)
✔ [4741/6609] Built Iut.Foundations.SourceFiniteEtaleSplitAlgebraAutomorphism (2.7s)
✔ [4742/6609] Built Iut.Foundations.SourceFiniteEtaleSignQuotientAffineChartGluing (8.6s)
✔ [4743/6609] Built Iut.Foundations.SourceFiniteEtaleSignQuotientAtlasLiftCompatibility (19s)
✔ [4744/6610] Built Iut.Foundations.SourceEtalePseudofunctorTwoPullbackCancellationTwoCellYTarget (2.7s)
✔ [4747/6610] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapOverlapNestedMiddleTargetAssociatorNaturality (3.1s)
✔ [4748/6610] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapOverlapNestedMiddleDirectTargetNaturalityEndpoints (2.9s)
✔ [4749/6610] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapOverlapNestedMiddleAttached (3.1s)
✔ [4750/6610] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapOverlapCompositeWhiskeredEndpointIsos (2.0s)
⚠ [4751/6628] Built Iut.Foundations.SourceEtaleRepresentedStrongTransPointIsoWhiskerLeftTargetTransport (2.0s)
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.9s)
✔ [4753/6635] Built Iut.Foundations.SourceEtaleRepresentedStrongTransPointIsoWhiskerLeftSourceTransport (3.1s)
✔ [4754/6635] Built Iut.Foundations.SourceEtaleRepresentedStrongTransPointIsoSymmInv (2.9s)
✔ [4755/6635] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapPointTripleRawCompositorTailHom (2.9s)
✔ [4756/6635] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapPointTripleBaseInverseTail (4.2s)
✔ [4757/6635] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapPointLongEdgeEndpoints (3.5s)
✔ [4758/6635] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapCechCocyclePointTripleValue (3.1s)
✔ [4759/6635] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapPointOverlapValueDirectFactorData (3.1s)
⚠ [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.2s)
✔ [4762/6635] Built Iut.Foundations.SourceEtaleRepresentedStrongTransPointIsoWhiskerRightTransHom (2.0s)
✔ [4763/6635] Built Iut.Foundations.SourceEtaleRepresentedStrongTransPointIsoAssociatorEqToHom (2.0s)
✔ [4764/6635] Built Iut.Foundations.SourceEtaleRepresentedStrongTransPointIsoCongruenceSymmInvAssociator (3.1s)
✔ [4765/6635] Built Iut.Foundations.SourceEtaleStackSchemeAtlasSourceAtlasOverlapCanonicalComparisonLeftFactorIso (2.7s)
✔ [4766/6635] Built Iut.Foundations.SourceEtaleStackSchemeAtlasFiniteEtaleCanonicalDescentStructureComparisonLeft (2.0s)
✔ [4767/6635] Built Iut.Foundations.SourceEtaleStackSchemeAtlasMapCechCompositeFactorization (12s)
✔ [4768/6635] Built Iut.Foundations.SourceOrbicurveFiniteEtaleIteratedBaseChangeForwardBackToSourceExpansion (3.0s)
✔ [4769/6635] Built Iut.Foundations.SourceFiniteEtaleSplitActionFixedAlgebra (3.9s)
✔ [4770/6635] Built Iut.Foundations.SourceFiniteEtaleSignQuotientAffineChartRelativeGluing (3.8s)
✔ [4771/6635] Built Iut.Foundations.SourceFiniteEtaleSignQuotientAtlasLiftWitness (18s)
✔ [4772/6750] Built Iut.Foundations.SourceEtalePseudofunctorTwoPullbackCancellationLiftToYInvToY (2.9s)
✔ [4775/6750] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapOverlapNestedMiddleDirectTargetNaturalityEndpointExpansions (3.0s)
✔ [4776/6750] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapOverlapNestedMiddleDirectTargetNaturalityMiddleRight (3.1s)
✔ [4777/6750] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapOverlapPairWhiskeredExpansion (3.2s)
✔ [4778/6750] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapOverlapCompositeWhiskeredEndpointFactorization (3.0s)
✔ [4779/6750] Built Iut.Foundations.SourceEtaleRepresentedStrongTransPointIsoWhiskerLeftTargetTransportData (2.9s)
✔ [4781/6750] Built Iut.Foundations.SourceFiniteEtaleSchemeCoverGeometricFiberFunctor (2.8s)
✔ [4782/6750] Built Iut.Foundations.SourceSpecFieldSchemeCoproductMaps (2.6s)
✔ [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/7793] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapPointTripleRepresentedSourceObjects (3.4s)
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/8799] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapPointTripleBaseInverseTailLeftHom (3.0s)
✔ [4788/8799] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapPointTripleCocycleMiddleValueIsos (2.0s)
✔ [4789/8799] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapPointTripleEdgeIso (3.3s)
✔ [4790/8799] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapPointTripleCocycleEndpointValueIso (3.0s)
⚠ [4791/8799] 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/8799] Built Iut.Foundations.SourceEtaleRepresentedStrongTransPointIsoWhiskerLeftTransInv (2.9s)
✔ [4793/8799] Built Iut.Foundations.SourceEtaleRepresentedStrongTransPointIsoWhiskerRightTransInv (3.1s)
✔ [4794/8799] Built Iut.Foundations.SourceEtaleRepresentedStrongTransPointIsoPentagonInv (3.2s)
✔ [4795/8799] Built Iut.Foundations.SourceEtaleRepresentedStrongTransPointIsoAssociatorNaturalityLeft (3.1s)
✔ [4796/8799] Built Iut.Foundations.SourceEtaleRepresentedStrongTransPointIsoAssociatorNaturalityMiddle (3.2s)
✔ [4797/8799] Built Iut.Foundations.SourceEtaleRepresentedStrongTransPointIsoAssociatorInvEqToHom (3.0s)
✔ [4798/8799] Built Iut.Foundations.SourceEtaleRepresentedStrongTransPointIsoCongruenceSymmInvAssociatorRestrictionTail (3.2s)
✔ [4799/8799] Built Iut.Foundations.SourceEtaleStackSchemeAtlasSourceAtlasOverlapCanonicalComparisonLeftExpandedIso (2.9s)
✔ [4800/8799] Built Iut.Foundations.SourceEtaleStackSchemeAtlasMapCechConeEndpointIsos (3.1s)
✔ [4801/8799] Built Iut.Foundations.SourceFiniteEtaleFixedSubalgebraBaseChange (3.3s)
✔ [4802/8799] Built Iut.Foundations.SourceFiniteEtaleSignQuotientAffineChartIdentityCoherence (554s)
✔ [4803/8799] Built Iut.Foundations.SourceFiniteEtaleSignQuotientAffineChartEffectivity (2.8s)
✔ [4804/8799] Built Iut.Foundations.SourceFiniteEtaleSignQuotientOrbicurve (199s)
✔ [4805/8799] Built Iut.Foundations.SourceEtalePseudofunctorTwoPullbackCancellationNestedWhisker (2.9s)
✔ [4807/8799] Built Iut.Foundations.SourceFiniteEtaleSchemeCoverRepresentable (3.0s)
✔ [4808/8799] Built Iut.Foundations.SourceSchemeEtaleStackPresentationFiniteEtaleCoverFunctor (3.0s)
✔ [4809/8799] Built Iut.Foundations.SourceEtalePseudofunctorContractiblePullback (3.5s)
✔ [4810/8799] Built Iut.Foundations.SourcePreGaloisCategoryEquivalenceTransport (1.9s)
✔ [4811/8799] Built Iut.Foundations.SourcePuncturedWeierstrassSchemeBaseChange (4.3s)
✔ [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 (2.0s)
✔ [4819/8799] Built Iut.Foundations.SourceAnabelioidDominatingPullbackInjectivity (2.9s)
✔ [4820/8799] Built Iut.Foundations.SourceCategoryIsoConjugationInverseCancellation (1.4s)
✔ [4821/8799] Built Iut.Foundations.SourceFiniteEtalePresentedQuotientBaseChange (1.9s)
✔ [4822/8898] Built Iut.Foundations.SourceIdealQuotientEquivComparison (1.9s)
✔ [4823/8991] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapOverlapPairWhiskeredNested (3.2s)
✔ [4824/8991] Built Iut.Foundations.SourceEtaleRepresentedStrongTransPointIsoWhiskerLeftTargetTransportRightData (2.9s)
✔ [4826/8991] Built Iut.Foundations.SourceFiniteEtaleSchemeCoverGeometricFiberPullbacks (2.7s)
✔ [4827/8991] Built Iut.Foundations.SourceEtaleRepresentedStrongTransPointIsoWhiskerLeftSymmInv (2.0s)
⚠ [4828/8991] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapPointTripleNaturalityAppTransportData (2.9s)
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 (2.0s)
⚠ [4830/8991] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapPointTripleRepresentedSourceCell (3.2s)
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`
✔ [4832/8991] Built Iut.Foundations.SourceFiniteEtaleClopenIdempotentQuotient (2.1s)
✔ [4833/8991] Built Iut.Foundations.SourceTensorProductScalarTowerQuotient (1.9s)
✔ [4834/8991] Built Iut.Foundations.SourceFiniteEtaleAffinePullbackActionTensor (7.6s)
✔ [4835/8991] Built Iut.Foundations.SourceFiniteEtaleSchemeCoverBaseChangeFiniteLimits (2.8s)
✔ [4836/8991] Built Iut.Foundations.SourceFiniteEtaleSchemeCoverBaseChangeBinaryCoproducts (12s)
✔ [4837/8991] Built Iut.Foundations.SourceInvolutiveEndofunctorEquivariantObject (3.1s)
✔ [4838/8991] Built Iut.Foundations.SourceFiniteEtaleSchemeCoverMonoCharacteristicIdempotent (2.0s)
✔ [4839/8991] Built Iut.Foundations.SourceRingEquivConjugationData (1.4s)
✔ [4840/8991] Built Iut.Foundations.SourceInvariantIdealQuotientInvolution (1.8s)
✔ [4841/8991] Built Iut.Foundations.SourceAffineScalarExtensionReversedTensorNaturality (15s)
✔ [4842/8991] Built Iut.Foundations.SourceTensorProductRightAlgEquiv (1.7s)
✔ [4843/8991] Built Iut.Foundations.SourceTensorProductTmulMulInclusions (1.8s)
✔ [4844/8991] Built Iut.Foundations.SourceRingHomRangeActionMul (1.6s)
✔ [4845/8991] Built Iut.Foundations.SourceRingHomRangeEquiv (1.6s)
✔ [4846/8991] Built Iut.Foundations.SourceRingEquivApplyHEqOfCarrierEq (1.4s)
✔ [4847/8991] Built Iut.Foundations.SourceEquivTransportApplyBack (782ms)
✔ [4848/8991] Built Iut.Foundations.SourceTensorProductSpecHomExt (2.4s)
✔ [4849/8991] Built Iut.Foundations.SourceCategoryFourfoldReassociation (1.4s)
✔ [4850/8991] Built Iut.Foundations.SourceFiniteEtaleSchemeCoverIdentitySectionLift (3.1s)
✔ [4851/8991] Built Iut.Foundations.SourceMorphismPropertyOverPullbackCompProjection (1.9s)
✔ [4852/8991] Built Iut.Foundations.SourceEtaleStackSchemeAtlasFiniteEtalePreDescentNormalizedMultiplicationHom (3.1s)
✔ [4853/8991] Built Iut.Foundations.SourceCategoryIsoConjugationCancel (2.7s)
✔ [4854/8991] Built Iut.Foundations.SourceFiniteEtaleSignQuotientAtlasFirstSheetProjection (3.1s)
✔ [4855/8991] Built Iut.Foundations.SourceFiniteEtaleSignQuotientAtlasConeLiftReassociation (3.2s)
✔ [4856/8991] Built Iut.Foundations.SourceFiniteEtaleSignQuotientAtlasTotalSpaceNormalization (15s)
✔ [4857/8991] Built Iut.Foundations.SourceEtalePseudofunctorConeReplaceCommutesHom (2.7s)
✔ [4858/8991] Built Iut.Foundations.SourceFiniteEtaleSignQuotientAtlasInversionIsoFirstSheetTotalSpace (4.2s)
✔ [4859/8991] Built Iut.Foundations.SourceEtalePseudofunctorInvolutionConePasting (3.1s)
✔ [4860/8991] Built Iut.Foundations.SourceCategoryIsoFactorCancellation (2.8s)
✔ [4861/8991] Built Iut.Foundations.SourceCategoryThreeCompatibilityPasting (1.5s)
✔ [4862/8991] Built Iut.Foundations.SourceEtaleStackSchemeAtlasTripleOverlapLongConeCells (3.0s)
✔ [4863/8991] Built Iut.Foundations.SourceCategoryEqualityPostcompositionIdentity (1.4s)
✔ [4864/8991] Built Iut.Foundations.SourceFiniteEtaleSchemeCoverPullbackMorphismDetection (3.3s)
✔ [4865/8991] Built Iut.Foundations.SourceFiniteEtaleSignQuotientEquivariantMap (5.8s)
✔ [4866/8991] Built Iut.Foundations.SourceCategoryTheoryColimMapFunctoriality (1.5s)
✔ [4867/8991] Built Iut.Foundations.SourceFiniteEtaleSchemeCoverStrictEpiUnderlyingScheme (2.8s)
✔ [4868/8991] Built Iut.Foundations.SourceEtaleStackSchemeAtlasFiniteEtaleDescentNormalizedNaturality (36s)
✔ [4869/8991] Built Iut.Foundations.SourceSignSwapActionCoproductQuotient (3.8s)
✔ [4870/8991] Built Iut.Foundations.SourceFiniteEtaleSignTorsorProjectionEffectiveEpi (3.1s)
✔ [4871/8991] Built Iut.Foundations.SourceFiniteEtaleSignTorsorEquivariantMapIso (4.5s)
✔ [4872/8991] Built Iut.Foundations.SourceFiniteEtaleSignQuotientTrivialAtlasIdentityPoint (2.8s)
✔ [4873/8991] Built Iut.Foundations.SourceCategoryMiddleIdentityConjugation (2.7s)
✔ [4874/8991] Built Iut.Foundations.SourceFiniteEtaleSignQuotientAssociatedStackCoverConeLiftCompatibilityRightContext (1.5s)
✔ [4875/8991] Built Iut.Foundations.SourceCategoryThreeLegPasting (1.4s)
✔ [4876/8991] Built Iut.Foundations.SourceCategoryFunctorOfObjMap (1.4s)
✔ [4877/8991] Built Iut.Foundations.SourceCategoryThreeProjectionPastingCore (1.6s)
✔ [4878/8991] Built Iut.Foundations.SourceCategoryFactorizedMiddlePasting (1.4s)
✔ [4879/8991] Built Iut.Foundations.SourceCategoryThreeLegQuotientPasting (1.5s)
✔ [4880/8991] Built Iut.Foundations.SourceCategoryFiveLegPasting (1.4s)
✔ [4881/8991] Built Iut.Foundations.SourceFiniteEtaleSignQuotientReindexHomExt (3.6s)
✔ [4882/8991] Built Iut.Foundations.SourceFiniteEtaleSignQuotientAssociatedStackCoverConeLiftToTestPasting (1.4s)
✔ [4883/8991] Built Iut.Foundations.SourceEqualityProofPackage (351ms)
✔ [4884/8991] Built Iut.Foundations.SourceCategoryReplaceRightmostFactor (1.4s)
✔ [4885/8991] Built Iut.Foundations.SourceCategoryReplaceTwoRightFactors (1.3s)
✔ [4886/8991] Built Iut.Foundations.SourceCategoryPrefixFactorPasting (1.4s)
✔ [4887/8991] Built Iut.Foundations.SourceCategoryTwoCompatibilityPasting (1.4s)
✔ [4888/8991] Built Iut.Foundations.SourceCategoryCongrThreeFactors (1.4s)
✔ [4889/8991] Built Iut.Foundations.SourceCategoryPackedHEqEndpointLinkDataDependentCongrArg (1.3s)
✔ [4890/8991] Built Iut.Foundations.SourceCategoryThreeMorphismBridgePasting (1.7s)
✔ [4891/8991] Built Iut.Foundations.SourceCategoryTwoMorphismHEqPastingData (1.4s)
✔ [4892/8991] Built Iut.Foundations.SourceOrbicurveFiniteEtaleIteratedBaseChangeReverseFst (3.1s)
✔ [4893/8991] Built Iut.Foundations.SourceFiniteEtaleSignQuotientPointIdentityReconstructionTotalNaturality (4.4s)
✔ [4894/8991] Built Iut.Foundations.SourceEtalePseudofunctorYonedaRecoveryModificationNaturality (4.8s)
✔ [4895/8991] Built Iut.Foundations.SourceCategoryHEqEndpointProjections (1.4s)
✔ [4896/8991] Built Iut.Foundations.SourceEtaleStackSchemeAtlasFiniteEtaleDescentComparisonConverse (2.8s)
✔ [4897/8991] Built Iut.Foundations.SourceFinitaryExtensiveComplementComparison (1.9s)
✔ [4898/8991] Built Iut.Foundations.SourceFiniteEtaleSchemeCoverBaseChangeIso (3.5s)
✔ [4899/8991] Built Iut.Foundations.SourceGaloisFiberFunctorFiniteColimits (2.0s)
✔ [4900/8991] Built Iut.Foundations.SourceConnectedFiniteEtaleConverse (4.7s)
✔ [4901/8991] Built Iut.Foundations.SourceContinuousActionRestrictionSurjectivity (4.1s)
✔ [4902/8991] Built Iut.Foundations.SourceMorphismPropertyOverPullbackCongrProjection (1.6s)
✔ [4903/8991] Built Iut.Foundations.SourceFiniteAlgebraSeparableClosureFactorization (2.8s)
✔ [4904/8991] Built Iut.Foundations.SourceProfiniteKernelLift (3.1s)
✔ [4905/8991] Built Iut.Foundations.SourceSelectedFiberSurjectiveMapData (345ms)
✔ [4906/8991] Built Iut.Foundations.SourcePullbackSelectedSectionAction (1.7s)
✔ [4907/8991] Built Iut.Foundations.SourceCategoryTheoryEqToIsoFintypeComponentHEq (1.5s)
✔ [4908/8991] Built Iut.Foundations.SourceCategoryTheoryDetachedNaturalityPastingMaps (1.4s)
✔ [4909/8991] Built Iut.Foundations.SourceProfiniteClosedSubgroupOpenExtension (2.0s)
✔ [4910/8991] Built Iut.Foundations.SourcePretransitiveContinuousActionCoset (3.4s)
✔ [4911/8991] Built Iut.Foundations.SourcePointedAnabelioidFiberEquivariance (2.8s)
✔ [4912/8991] Built Iut.Foundations.SourceSpecRingHomSemiconjugacy (2.2s)
✔ [4913/8991] Built Iut.Foundations.SourceCategoryTheoryIsoRightFactorInvOfHomEq (1.4s)
✔ [4914/8991] Built Iut.Foundations.SourceFintypeCatFunctorMapCompApply (1.5s)
✔ [4915/8991] Built Iut.Foundations.SourceCategoryPackedTwoProjectionPasting (1.4s)
✔ [4916/8991] Built Iut.Foundations.SourceCategoryHEqPrecomposition (1.4s)
✔ [4917/8991] Built Iut.Foundations.SourceCategoryTheoryEquivalenceInverseObjectIsoCounit (1.4s)
✔ [4918/8991] Built Iut.Foundations.SourceCategoryTwoMorphismEquationDataOfCompositeEq (1.4s)
✔ [4919/8991] Built Iut.Foundations.SourceHEqTransExplicit (1.3s)
✔ [4920/8991] Built Iut.Foundations.SourceCategoryPackedHEqEndpointLinkDataCommonRightComparisonData (1.4s)
✔ [4921/8991] Built Iut.Foundations.SourceFunctionPointwiseFactorizationData (341ms)
✔ [4922/8991] Built Iut.Foundations.SourceFintypeFunctorFactorizationApply (1.7s)
✔ [4923/8991] Built Iut.Foundations.SourceFunctionHEqCastMapData (344ms)
✔ [4924/8991] Built Iut.Foundations.SourceFunctionPointwiseEqualityData (362ms)
✔ [4925/8991] Built Iut.Foundations.SourceFunctionHEqCongr (342ms)
✔ [4926/8991] Built Iut.Foundations.SourceCategoryPackedHEqEndpointLinkDataHiddenEndpointStorage (1.4s)
✔ [4927/8991] Built Iut.Foundations.SourceCategoryPackedHEqEndpointLinkDataOfTwoHEq (1.4s)
✔ [4928/8991] Built Iut.Foundations.SourceCategoryPackedHEqEndpointLinkDataCommonMiddleProjectionData (1.5s)
✔ [4929/8991] Built Iut.Foundations.SourceSelectedFiberComponentDomination (1.5s)
✔ [4930/8991] Built Iut.Foundations.SourceContinuousActionRestrictionComponentStability (3.4s)
✔ [4931/8991] Built Iut.Foundations.SourceHEqApply (347ms)
✔ [4932/8991] Built Iut.Foundations.SourceEtalePseudofunctorPointIdentityReconstructionNaturality (4.9s)
✔ [4933/8991] Built Iut.Foundations.SourceCategoryProjectionEndpointHEqWhisker (1.5s)
✔ [4934/8991] Built Iut.Foundations.SourceEtaleStackSchemeAtlasFiniteEtaleDescentObjectPullbackProjections (3.3s)
✔ [4935/8991] Built Iut.Foundations.SourceFiniteEtaleSignTorsorTrivialAtlasFirstSheetExt (3.6s)
✔ [4936/8991] Built Iut.Foundations.SourceOrbicurveFiniteEtaleBaseChangePointIsoToSource (3.1s)
✔ [4937/8991] Built Iut.Foundations.SourceEtaleStackSchemeAtlasFiniteEtaleDescentOverlapComparisonLeft (3.1s)
✔ [4938/8991] Built Iut.Foundations.SourceOrbicurveFiniteEtaleIteratedBaseChangeReverseLeftProjection (2.0s)
✔ [4939/8991] Built Iut.Foundations.SourceCategoryInvolutiveActionTransport (1.5s)
✔ [4940/8991] Built Iut.Foundations.SourceRegularInvolutivePullbackFiberSwap (1.0s)
✔ [4941/8991] Built Iut.Foundations.SourceEtaleStackFiniteEtaleComposition (5.7s)
✔ [4942/8991] Built Iut.Foundations.SourceCategoryProjectionEndpointLinkContext (1.3s)
✔ [4943/8991] Built Iut.Foundations.SourceCategoryDetachedHEqData (341ms)
✔ [4944/8991] Built Iut.Foundations.SourceCategoryComparisonProjectionContext (1.4s)
✔ [4945/8991] Built Iut.Foundations.SourceCategoryDetachedEqDataProjections (317ms)
✔ [4946/8991] Built Iut.Foundations.SourceProfinitePostcompositionKernelIso (4.5s)
✔ [4947/8991] Built Iut.Foundations.SourceOrbicurveFiniteEtaleCoverStabilizerExactSequence (2.0s)
✔ [4948/8991] Built Iut.Foundations.SourceProfiniteOpenSubgroupKernelIso (3.7s)
✔ [4949/8991] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalHomPointIsoNaturality (3.3s)
✔ [4950/8991] Built Iut.Foundations.SourceOrbicurveSignInvariantCategory (3.2s)
✔ [4951/8991] Built Iut.Foundations.SourcePseudofunctorStrongTransCompNaturalityInvApp (1.8s)
✔ [4952/8991] Built Iut.Foundations.SourceCategoryFunctorSquarePasting (1.5s)
✔ [4953/8992] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapPointTripleBaseInverseTailLeftHomProjection (3.2s)
✔ [4954/8992] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapPointTripleCocycleBaseInverseTerminalHom (2.0s)
✔ [4955/8992] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapPointTripleCocycleNormalizedAtlasMiddleHom (2.9s)
✔ [4956/8992] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapPointTripleEdgeConeIso (3.2s)
⚠ [4957/8992] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapPointTripleCocycleToTwoValueIsoHom (3.2s)
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`
✔ [4958/8992] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapPointTripleOverlapCompositeTargetToCocycleHom (3.1s)
✔ [4959/8992] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapPointTripleCocycleToZeroValueIsoHom (3.2s)
✔ [4960/8992] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapPointOverlapValueDirectMiddleFactor (3.3s)
✔ [4961/8992] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapPointTripleOverlapValueDirectFactorDataMapped (3.2s)
✔ [4962/8992] Built Iut.Foundations.SourceEtaleRepresentedStrongTransPointIsoWhiskerRightSymmInv (2.9s)
✔ [4963/8992] Built Iut.Foundations.SourceEtaleRepresentedStrongTransPointIsoAssociatorNaturalityMiddleInverseSolve (3.2s)
✔ [4964/8992] Built Iut.Foundations.SourceEtaleRepresentedStrongTransPointIsoAssociatorNaturalityMiddleInv (3.1s)
✔ [4965/8992] Built Iut.Foundations.SourceEtaleRepresentedStrongTransPointIsoAssociatorInvAbsorbPointTransport (3.0s)
✔ [4966/8992] Built Iut.Foundations.SourceEtaleStackSchemeAtlasSourceAtlasOverlapCanonicalComparisonLeftExpandedFirstWhiskeredHom (3.3s)
✔ [4967/8992] Built Iut.Foundations.SourceEtaleStackSchemeAtlasMapCechCocycle (3.2s)
✔ [4968/8992] Built Iut.Foundations.SourceFiniteEtaleTensorAction (3.8s)
✔ [4969/8992] Built Iut.Foundations.SourceFiniteEtaleSignQuotientAffineChartCompositionCoherence (4.1s)
✔ [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.3s)
✔ [4974/8992] Built Iut.Foundations.SourceEtalePseudofunctorTwoPullbackCancellationTwoCellYTargetToY (3.1s)
✔ [4975/8992] Built Iut.Foundations.SourceFiberFunctorComparison (2.4s)
✔ [4976/8992] Built Iut.Foundations.SourceSchemeEtaleStackPresentationReverseFiniteEtaleCover (3.0s)
✔ [4977/8992] Built Iut.Foundations.SourceEtalePseudofunctorContractiblePullbackEquivalence (3.8s)
✔ [4978/8992] Built Iut.Foundations.SourcePreGaloisFiberFunctorEquivalenceTransport (1.7s)
✔ [4979/8992] Built Iut.Foundations.SourcePseudofunctorRestrictionPullHom (2.1s)
✔ [4980/8992] Built Iut.Foundations.SourceSchemeOverFieldRestrictScalarsSliceEquivalence (4.2s)
✔ [4981/8992] Built Iut.Foundations.SourceEtaleFundamentalGroupCoverActionEquivalence (2.6s)
✔ [4983/8992] Built Iut.Foundations.SourceCategoryFourLegSquareReassociation (1.3s)
✔ [4984/8992] Built Iut.Foundations.SourcePseudofunctorStrongTransEndpointPullLeft (1.9s)
✔ [4985/8992] Built Iut.Foundations.SourcePseudofunctorStrongTransEndpointPullRight (2.3s)
✔ [4986/8992] Built Iut.Foundations.SourceEtaleStackSchemeAtlasBaseChangePointIsoSource (2.9s)
✔ [4987/8992] Built Iut.Foundations.SourceCategoryFunctorMapSubsingletonComposition (1.5s)
✔ [4988/8992] Built Iut.Foundations.SourceCategoryEndpointTransportPasting (1.5s)
✔ [4989/8992] Built Iut.Foundations.SourceCategoryMappedTwoThreePasting (1.4s)
✔ [4990/8992] Built Iut.Foundations.SourceFiniteEtaleSignQuotientAtlasPointFiberIsoNaturalityFirstSheet (5.4s)
✔ [4991/8992] Built Iut.Foundations.SourceCategoryMappedNaturalityPasting (1.5s)
✔ [4992/8992] Built Iut.Foundations.SourceCategoryPullNaturalityThroughIso (1.5s)
✔ [4993/8992] Built Iut.Foundations.SourceCategoryThreeFactorIsoRecoveryData (1.4s)
✔ [4994/8992] Built Iut.Foundations.SourceCategoryThreeMapHEq (1.4s)
✔ [4995/8992] Built Iut.Foundations.SourceCategoryRecoverFactorThroughMappedIso (1.5s)
✔ [4996/8992] Built Iut.Foundations.SourceEtalePseudofunctorYonedaIdentityBaseChange (3.4s)
✔ [4997/8992] Built Iut.Foundations.SourceInitialTheta11a1DivisionRootFiberToThirtyTorsion (3.0s)
✔ [4998/8992] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapOverlapPairWhiskeredNestedFactorization (3.0s)
✔ [4999/8992] Built Iut.Foundations.SourceEtaleRepresentedStrongTransPointIsoWhiskerLeftTargetTransportRightDataRight (2.9s)
⚠ [5001/8992] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapPointTripleNaturalityAppTransportDataEndpoints (3.7s)
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.1s)
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.SourceTensorProductAlgebraicFiniteStage (3.2s)
✔ [5004/8992] Built Iut.Foundations.SourceFiniteEtaleAffinePullbackActionReversedTensor (4.2s)
✔ [5005/8992] Built Iut.Foundations.SourceEtaleStackSchemeAtlasFiniteEtalePreDescentPullbacks (7.5s)
✔ [5006/8992] Built Iut.Foundations.SourceEtaleStackSchemeAtlasFiniteEtaleDescentTerminal (3.1s)
✔ [5007/8992] Built Iut.Foundations.SourceFiniteEtaleSchemeCoverBaseChangeFiniteCoproducts (3.5s)
✔ [5008/8992] Built Iut.Foundations.SourceInvolutiveEndofunctorEquivariantForgetReflectsLimits (1.8s)
✔ [5009/8992] Built Iut.Foundations.SourceInvolutiveEndofunctorEquivariantFreeObject (1.0s)
✔ [5010/8992] Built Iut.Foundations.SourceInvolutiveEndofunctorEquivariantForgetReflectsIsomorphisms (1.5s)
✔ [5011/8992] Built Iut.Foundations.SourceInvolutiveEndofunctorEquivariantCofreeMono (1.6s)
✔ [5012/8992] Built Iut.Foundations.SourceFiniteEtaleSchemeCoverInvolutivePostcomposition (106s)
✔ [5013/8992] Built Iut.Foundations.SourceTensorProductRightAlgEquivTmul (1.9s)
✔ [5014/8992] Built Iut.Foundations.SourceTensorProductRingHomTmulFactorization (1.8s)
✔ [5015/8992] Built Iut.Foundations.SourceEquivTransportApplyBackTarget (777ms)
✔ [5016/8992] Built Iut.Foundations.SourceSchemePullbackSectionAlongComposite (4.2s)
✔ [5017/8992] Built Iut.Foundations.SourceEtalePseudofunctorConeReplaceCommutesHomTargetIso (2.7s)
✔ [5018/8992] Built Iut.Foundations.SourceFiniteEtaleSignQuotientAtlasSecondSheetTotalSpaces (4.3s)
✔ [5019/8992] Built Iut.Foundations.SourceFiniteEtaleSignQuotientEquivariantMapIdentity (3.8s)
✔ [5020/8992] Built Iut.Foundations.SourceFiniteEtaleSignQuotientEquivariantMapComposition (4.3s)
✔ [5021/8992] Built Iut.Foundations.SourceFiniteEtaleSignTorsorInvariantEffectiveDescent (3.2s)
✔ [5022/8992] Built Iut.Foundations.SourceFiniteEtaleSignQuotientHomTripleCarrier (3.1s)
✔ [5023/8992] Built Iut.Foundations.SourceFiniteEtaleSignQuotientReindexCompInverseToTotal (3.2s)
✔ [5024/8992] Built Iut.Foundations.SourceCategoryThreeMorphismBridgePastingPackedCompletion (1.4s)
✔ [5025/8992] Built Iut.Foundations.SourceFiniteEtaleSignQuotientPointIdentityReconstructionComparison (4.3s)
✔ [5026/8992] Built Iut.Foundations.SourceGaloisFiberFunctorFiniteColimitsHeterogeneous (2.7s)
✔ [5027/8992] Built Iut.Foundations.SourceContinuousActionRestrictionConnectednessSurjectivity (3.7s)
✔ [5028/8992] Built Iut.Foundations.SourceCategoryTheoryEqToIsoFintypeMapApplyHEq (1.6s)
✔ [5029/8992] Built Iut.Foundations.SourceCategoryTheoryIndexedNatIsoTransportFintypeComponentHEq (1.5s)
✔ [5030/8992] Built Iut.Foundations.SourceFintypeDetachedNaturalityIsoExtension (1.8s)
✔ [5031/8992] Built Iut.Foundations.SourceContinuousActionClosedSubgroupAmbientEnvelope (3.8s)
✔ [5032/8992] Built Iut.Foundations.SourcePointedAnabelioidKernelFiberStability (3.1s)
✔ [5033/8992] Built Iut.Foundations.SourceEquivalenceInversePointNaturality (1.7s)
✔ [5034/8992] Built Iut.Foundations.SourceCategoryPackedHEqEndpointLinkDataCommonRightComparisonDataLeftComm (1.4s)
✔ [5035/8992] Built Iut.Foundations.SourceFunctionHEqCastMapDataPostmap (343ms)
✔ [5036/8992] Built Iut.Foundations.SourceFunctionHEqData (1.5s)
✔ [5037/8992] Built Iut.Foundations.SourceCategoryPackedHEqEndpointLinkDataHiddenEndpointStorageExplicit (1.4s)
✔ [5038/8992] Built Iut.Foundations.SourceCategoryPackedHEqEndpointLinkDataCommonMiddleProjectionDataOfExplicitMiddle (1.3s)
✔ [5039/8992] Built Iut.Foundations.SourceSelectedFiberSurjectiveMapDataComponentDomination (1.5s)
✔ [5040/8992] Built Iut.Foundations.SourceFiniteEtaleSignQuotientPointIdentityReconstructionNaturality (3.4s)
✔ [5041/8992] Built Iut.Foundations.SourceEtalePseudofunctorPointIdentityReconstructionComponent (4.2s)
✔ [5042/8992] Built Iut.Foundations.SourceRegularInvolutiveEquivariantExtension (2.5s)
✔ [5043/8992] Built Iut.Foundations.SourceCategoryProjectionEndpointLinkData (1.4s)
✔ [5044/8992] Built Iut.Foundations.SourceCategoryDetachedHEqPastingData (348ms)
✔ [5045/8992] Built Iut.Foundations.SourceCategoryDetachedHEqDataProjections (316ms)
✔ [5046/8992] Built Iut.Foundations.SourceCategoryComparisonProjectionContextLeftWhisker (1.3s)
✔ [5047/8992] Built Iut.Foundations.SourceOrbicurveFiniteEtaleCoverStabilizerProjectionSurjectivity (3.3s)
✔ [5048/8992] Built Iut.Foundations.SourceOrbicurveFiniteEtaleCoverStabilizerKernelIso (2.0s)
✔ [5049/8992] Built Iut.Foundations.SourceEtaleStackSchemeAtlasYonedaFiberNaturalityOfPointIso (3.5s)
✔ [5050/8992] Built Iut.Foundations.SourceEtaleStackSchemeAtlasPointIsoDescentComparison (5.4s)
✔ [5051/8992] Built Iut.Foundations.SourceOrbicurveSignInvariantIso (3.1s)
✔ [5052/8992] Built Iut.Foundations.SourceOrbicurveSignQuotientComparison (3.6s)
✔ [5053/8992] Built Iut.Foundations.SourceCategoryFunctorSquarePastingEvidenceFirst (1.5s)
✔ [5054/8992] Built Iut.Foundations.SourceCategoryFunctorSquarePastingContext (1.6s)
✔ [5056/8992] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapPointTripleCocycleBaseInverseTerminalProjection (3.9s)
✔ [5057/8992] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapPointTripleCocycleNormalizedAtlasMiddleIdentity (3.4s)
✔ [5058/8992] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapPointTriplePastedConeIso (3.1s)
✔ [5059/8992] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapPointTripleLongEdgeGeometricTargetAfterSourceAssociator (3.5s)
✔ [5060/8992] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapPointTripleOverlapValueDirectFactorDataMappedRight (3.2s)
✔ [5061/8992] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapPointTripleCocycleSuccessiveSecondOverlapValueFactorDataMapped (3.2s)
✔ [5062/8992] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapPointTripleCocycleSuccessiveFirstOverlapValueFactorDataMapped (2.9s)
✔ [5063/8992] Built Iut.Foundations.SourceEtaleRepresentedStrongTransPointIsoWhiskerRightWhiskerRightSymmInv (3.1s)
✔ [5064/8992] Built Iut.Foundations.SourceEtaleRepresentedStrongTransPointIsoWhiskerRightCongrIsoSymmInv (3.0s)
⚠ [5065/8992] Built Iut.Foundations.SourceEtaleStackSchemeAtlasSourceAtlasOverlapCanonicalComparisonLeftExpandedSecondWhiskerCongr (3.1s)
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.8s)
✔ [5067/8992] Built Iut.Foundations.SourceFiniteEtaleTensorFixedSubalgebra (4.1s)
✔ [5068/8992] Built Iut.Foundations.SourceFiniteEtaleSignQuotientAffineChartCompositionContext (3.5s)
✔ [5069/8992] Built Iut.Foundations.SourceFiniteEtaleSignQuotientAffineChartGluedInvolution (3.9s)
✔ [5070/8992] Built Iut.Foundations.SourceFiniteEtaleSignQuotientAtlasConeLiftTransportSchemeMap (3.2s)

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

apx-runtime-resource-v1	apx-verifier-job-1791-runtime-blueprint_build-2467169-1789160163067587605-2	946176	1376256	21474836480	0	0	0	0	0	0	11476992	113405952	21474836480	0	0	0	0	0	0

Keyboard shortcuts