Login

Verification run

Run 1303

promachina/iut-leanbranch mastertriggered via github_push
failedcommit 19acd7382f1atoolchain lean-v4-30-0prover leantook 2h 1m · finished 2d ago

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

Open project

Package inputs

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

Trust verification

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

(verification not run)

Manifest

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

(manifest not loaded)

Verifier log excerpt

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

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

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

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

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

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

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

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

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

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

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

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

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

Note: This linter can be disabled with `set_option linter.style.setOption false`
✔ [4608/6597] Built Iut.Foundations.SourceEtalePseudofunctorTwoPullbackCancellationLiftToYInv (2.8s)
✔ [4609/6597] Built Iut.Foundations.SourceFiniteEtaleAffineOverCoordinateAction (2.4s)
✔ [4611/6597] Built Iut.Foundations.SourceSingleObjOppositeEquivalence (1.6s)
✔ [4612/6597] Built Iut.Foundations.SourceCategoryPackedHEqEndpointLinkDataJoinProjections (1.4s)
✔ [4613/6597] Built Iut.Foundations.SourceEtalePseudofunctorStrongTransWhiskerRightIsoSymmHom (2.7s)
✔ [4614/6597] Built Iut.Foundations.SourceEtalePseudofunctorStrongTransPentagonInvPrefix (4.3s)
✔ [4615/6597] Built Iut.Foundations.SourceCategoryEqToHomTransportedEndpointDataMap (1.4s)
✔ [4616/6597] Built Iut.Foundations.SourceEtalePseudofunctorChangeFirstBaseMap (3.9s)
✔ [4617/6597] Built Iut.Foundations.SourceEtalePseudofunctorChangeSecondBaseMap (3.7s)
✔ [4618/6597] Built Iut.Foundations.SourceEtalePseudofunctorFaithfulCellAssembly (3.8s)
✔ [4619/6597] Built Iut.Foundations.SourceEtalePseudofunctorRepresentablePullbackTwoCell (117s)
✔ [4620/6597] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalHomPointValueRecovery (2.0s)
✔ [4621/6597] Built Iut.Foundations.SourceFiniteEtaleSchemeCoverClopenMono (2.8s)
⚠ [4623/6597] Built Iut.Foundations.SourceFiniteEtaleSignTorsorAffineEffectiveness (167s)
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`
✔ [4624/6597] Built Iut.Foundations.SourceFiniteEtaleSignQuotientPrestack (42s)
✔ [4625/6597] Built Iut.Foundations.SourceFiniteEtaleSignTorsorTargetStackDescent (3.0s)
✔ [4626/6597] Built Iut.Foundations.SourceFiniteEtaleSignTorsorTrivial (4.8s)
✔ [4627/6597] Built Iut.Foundations.SourceEtalePseudofunctorTwoPullbackCancellationLiftToYLawful (2.8s)
✔ [4628/6597] Built Iut.Foundations.SourceFiniteEtaleAffineOverCoordinateFiniteEtale (2.5s)
✔ [4629/6597] Built Iut.Foundations.SourceCategoryPackedHEqTwoMorphismComposition (1.4s)
✔ [4630/6597] Built Iut.Foundations.SourceEtaleStackRepresentablePropertyChangeMap (2.6s)
✔ [4631/6597] Built Iut.Foundations.SourceEtalePseudofunctorConeAfterChangeSecondBaseMap (2.0s)
✔ [4632/6597] Built Iut.Foundations.SourceEtalePseudofunctorRepresentedIsoPointLift (3.2s)
✔ [4633/6597] Built Iut.Foundations.SourceEtalePseudofunctorRepresentablePullbackWitness (2.9s)
✔ [4634/6597] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalHomYonedaPointValue (2.8s)
✔ [4635/6597] Built Iut.Foundations.SourceFiniteEtaleSchemeCoverDirectSummand (3.3s)
✔ [4636/6597] Built Iut.Foundations.SourceFiniteEtaleSchemeCoverUnderlyingEpiRange (2.8s)
⚠ [4637/6597] 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`
✔ [4638/6600] Built Iut.Foundations.SourceFiniteEtaleSignQuotientStackCriterion (3.1s)
✔ [4639/6600] Built Iut.Foundations.SourceFiniteEtaleSignQuotientAtlas (5.7s)
✔ [4640/6601] Built Iut.Foundations.SourceEtalePseudofunctorTwoPullbackCancellationLiftToYHomToX (2.9s)
✔ [4641/6601] Built Iut.Foundations.SourceEtalePseudofunctorConeAfterChangeSecondBaseMapFromConeOf (3.2s)
✔ [4642/6601] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalIsoBaseChangeOver (3.3s)
✔ [4643/6601] Built Iut.Foundations.SourceRepresentableStrongTransReconstruction (3.1s)
✔ [4644/6601] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalHomYonedaNaturality (2.9s)
✔ [4645/6601] Built Iut.Foundations.SourceFiniteEtaleSchemeCoverAffineSource (2.9s)
✔ [4646/6601] Built Iut.Foundations.SourceFiniteEtaleSchemeCoverUnderlyingEpiSurjective (7.3s)
⚠ [4647/6601] Built Iut.Foundations.SourceFiniteEtaleSignTorsorAffineCoverAssembly (892s)
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`
✔ [4649/6601] Built Iut.Foundations.SourceFiniteEtaleSignQuotientAtlasBaseChange (17s)
✔ [4650/6601] Built Iut.Foundations.SourceEtalePseudofunctorTwoPullbackCancellationLiftToYHomToY (2.7s)
✔ [4652/6601] Built Iut.Foundations.SourceEtaleStackRepresentableLocalIsoDescent (3.7s)
✔ [4653/6601] Built Iut.Foundations.SourceEtaleStackSchemeAtlasOverlapMultiplication (2.0s)
✔ [4654/6601] Built Iut.Foundations.SourceEtalePseudofunctorRepresentablePullbackAlongStrongTrans (3.8s)
✔ [4655/6601] Built Iut.Foundations.SourceFiniteEtaleSchemeCoverAffineGroupQuotient (3.1s)
✔ [4656/6601] Built Iut.Foundations.SourceFiniteEtaleSchemeCoverBalanced (2.7s)
✔ [4657/6601] Built Iut.Foundations.SourceFiniteEtaleSignTorsorAffineCoverRestriction (126s)
✔ [4659/6601] Built Iut.Foundations.SourceFiniteEtaleSignQuotientAtlasLiftApp (124s)
✔ [4660/6601] Built Iut.Foundations.SourceFiniteEtaleSignQuotientAtlasInvariant (3.7s)
✔ [4661/6602] Built Iut.Foundations.SourceEtalePseudofunctorTwoPullbackCancellationLiftCompatibility (2.8s)
✔ [4662/6604] Built Iut.Foundations.SourceEtaleStackRepresentableAtlasLocalIsoDescent (3.2s)
✔ [4663/6604] Built Iut.Foundations.SourceOrbicurveFiniteEtaleBaseChangeSchemeCoverMapReflectsLocalIso (3.5s)
✔ [4664/6604] Built Iut.Foundations.SourceEtaleStackSchemeAtlasOverlapMultiplicationRepresentedLongConeIso (2.9s)
✔ [4665/6604] Built Iut.Foundations.SourceEtaleStackSchemeAtlasOverlapConePasting (3.1s)
✔ [4666/6604] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapCechData (3.1s)
✔ [4667/6604] Built Iut.Foundations.SourceEtaleStackSchemeAtlasFiniteEtaleDescent (3.4s)
✔ [4668/6604] Built Iut.Foundations.SourceOrbicurveFiniteEtaleIteratedBaseChange (9.5s)
✔ [4669/6604] Built Iut.Foundations.SourceFiniteEtaleSchemeCoverAffineOverFullyFaithful (2.8s)
✔ [4670/6604] Built Iut.Foundations.SourceFiniteEtaleFixedSubalgebra (3.1s)
✔ [4671/6604] Built Iut.Foundations.SourceFiniteEtaleSignTorsorAffineCoverFiniteEffectivity (3.5s)
✔ [4673/6604] Built Iut.Foundations.SourceFiniteEtaleSignQuotientAtlasLiftNaturality (106s)
✔ [4674/6604] Built Iut.Foundations.SourceFiniteEtaleSignQuotientAtlasInvariantElement (3.1s)
✔ [4675/6606] Built Iut.Foundations.SourceEtalePseudofunctorTwoPullbackCancellationConeMorphismCompatibility (3.1s)
✔ [4678/6606] Built Iut.Foundations.SourceEtaleStackSchemeAtlasOverlapConePastingIso (4.1s)
✔ [4679/6606] Built Iut.Foundations.SourceEtaleStackSchemeAtlasOverlapConePastingCell (2.9s)
✔ [4680/6606] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapRestrictionCongrIsoNaturality (3.1s)
✔ [4681/6606] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapRestrictionCongrIsoWhiskerRightFactorization (3.0s)
✔ [4682/6606] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapOverlapNestedMiddleIso (2.9s)
✔ [4683/6606] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapPointObject (2.9s)
✔ [4684/6606] Built Iut.Foundations.SourceEtaleStackSchemeAtlasFiniteEtaleDescentComparison (3.2s)
✔ [4685/6606] Built Iut.Foundations.SourceEtaleStackSchemeAtlasMapCechEndpointIsos (3.0s)
✔ [4686/6606] Built Iut.Foundations.SourceEtaleStackSchemeAtlasBaseChangePointIso (3.0s)
✔ [4687/6606] Built Iut.Foundations.SourceOrbicurveFiniteEtaleIteratedBaseChangeForwardBackLiftedHom (3.4s)
✔ [4688/6606] Built Iut.Foundations.SourceEtaleStackSchemeAtlasOverlapMapIso (2.8s)
✔ [4689/6606] Built Iut.Foundations.SourceOrbicurveFiniteEtaleIteratedBaseChangeToSourceIso (2.8s)
✔ [4690/6606] Built Iut.Foundations.SourceFiniteEtaleFixedAffineQuotient (3.0s)
✔ [4691/6606] Built Iut.Foundations.SourceFiniteEtaleSignTorsorAffineRefinement (3.8s)
✔ [4692/6606] Built Iut.Foundations.SourceFiniteEtaleSignQuotientAtlasLift (3.0s)
✔ [4693/6606] Built Iut.Foundations.SourceFiniteEtaleSignQuotientAtlasInvariantComponent (25s)
✔ [4694/6607] Built Iut.Foundations.SourceEtalePseudofunctorTwoPullbackCancellationConeMorphism (3.3s)
✔ [4697/6607] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapOverlapNestedMiddleHom (3.2s)
✔ [4698/6607] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapOverlapNestedEndpointIsos (2.9s)
✔ [4699/6607] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapPointOverlap (3.2s)
✔ [4700/6607] Built Iut.Foundations.SourceEtaleStackSchemeAtlasFiniteEtaleDescentConstruction (42s)
✔ [4701/6607] Built Iut.Foundations.SourceEtaleStackSchemeAtlasMapCechPairMiddleIso (3.1s)
✔ [4702/6607] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalHomPointIsoValue (3.2s)
✔ [4703/6607] Built Iut.Foundations.SourceOrbicurveFiniteEtaleIteratedBaseChangeForwardBackLiftedHomComparison (2.9s)
✔ [4704/6607] Built Iut.Foundations.SourceFiniteEtaleOrbitConstantAlgebra (3.1s)
✔ [4705/6607] Built Iut.Foundations.SourceFiniteEtaleSignQuotientStackRefinement (3.2s)
✔ [4706/6607] Built Iut.Foundations.SourceFiniteEtaleSignQuotientAtlasLiftProjections (13s)
✔ [4707/6607] Built Iut.Foundations.SourceFiniteEtaleSignQuotientAtlasInvariantCocycle (19s)
✔ [4708/6609] Built Iut.Foundations.SourceEtalePseudofunctorTwoPullbackCancellationTwoCell (2.5s)
✔ [4711/6609] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapOverlapNestedMiddleCompositeFactorization (3.1s)
✔ [4712/6609] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapPullbackOverlapNestedFactorization (3.4s)
✔ [4713/6609] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapPointTransition (3.3s)
✔ [4714/6609] Built Iut.Foundations.SourceOrbicurveFiniteEtaleBaseChangePointIsoToSourceIso (2.9s)
✔ [4715/6609] Built Iut.Foundations.SourceEtaleStackSchemeAtlasFiniteEtaleDescentCoherence (13s)
✔ [4716/6609] Built Iut.Foundations.SourceEtaleStackSchemeAtlasMapCechPairFactorization (22s)
✔ [4717/6609] Built Iut.Foundations.SourceOrbicurveFiniteEtaleIteratedBaseChangeForwardBackStrongTransToSource (3.0s)
✔ [4718/6609] Built Iut.Foundations.SourceFiniteEtaleSplitAlgebraHom (3.3s)
✔ [4719/6609] Built Iut.Foundations.SourceFiniteEtaleSignQuotientAffineChartDescent (16s)
✔ [4720/6609] Built Iut.Foundations.SourceFiniteEtaleSignQuotientAtlasLiftTwoCell (291s)
✔ [4721/6609] Built Iut.Foundations.SourceFiniteEtaleSignQuotientAtlasLiftUnit (14s)
✔ [4722/6611] Built Iut.Foundations.SourceEtalePseudofunctorTwoPullbackCancellationTwoCellToX (2.7s)
✔ [4724/6611] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapOverlapNestedMiddleCompositeTargetCollapse (2.0s)
✔ [4725/6611] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapOverlapNestedMiddleCompositeSourceCollapse (3.1s)
✔ [4726/6611] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapOverlapNestedSpecializations (2.9s)
✔ [4727/6611] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapOverlapCompositeWhiskeredExpansion (3.1s)
✔ [4728/6611] Built Iut.Foundations.SourceEtaleRepresentedRestrictionPointIsoCongruenceTail (3.1s)
✔ [4729/6611] Built Iut.Foundations.SourceEtaleRepresentedStrongTransPointIsoWhiskerRightHom (2.9s)
✔ [4730/6611] Built Iut.Foundations.SourceEtaleRepresentedStrongTransPointIsoWhiskerLeft (3.8s)
✔ [4731/6611] Built Iut.Foundations.SourceEtaleRepresentedStrongTransPointIsoSymmHom (2.9s)
✔ [4732/6611] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapPointOverlapValueIsoRepresented (2.9s)
✔ [4733/6611] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapPointCocycleGeometry (3.4s)
✔ [4734/6611] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapCechCocyclePointValue (2.0s)
✔ [4735/6611] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapRestrictionCompositePointIsoHom (6.7s)
⚠ [4736/6611] Built Iut.Foundations.SourceEtaleRepresentedStrongTransPointIsoTransHom (2.9s)
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`
✔ [4737/6611] Built Iut.Foundations.SourceOrbicurveFiniteEtaleBaseChangePointIsoToSourceCompatibility (3.0s)
✔ [4738/6611] Built Iut.Foundations.SourceEtaleRepresentedStrongTransPointIsoCongruenceAssociator (3.2s)
✔ [4739/6611] Built Iut.Foundations.SourceEtaleStackSchemeAtlasFiniteEtaleCoverOverlapComparisonLeft (2.0s)
✔ [4740/6611] Built Iut.Foundations.SourceEtaleStackSchemeAtlasFiniteEtaleCanonicalDescentStructureComparison (2.0s)
✔ [4741/6611] Built Iut.Foundations.SourceEtaleStackSchemeAtlasMapCechPairLongFactorization (2.9s)
✔ [4742/6611] Built Iut.Foundations.SourceOrbicurveFiniteEtaleIteratedBaseChangeForwardBackRealizationToSourceExpansion (3.0s)
✔ [4743/6611] Built Iut.Foundations.SourceFiniteEtaleSplitAlgebraAutomorphism (2.7s)
✔ [4744/6611] Built Iut.Foundations.SourceFiniteEtaleSignQuotientAffineChartGluing (8.3s)
✔ [4745/6611] Built Iut.Foundations.SourceFiniteEtaleSignQuotientAtlasLiftCompatibility (18s)
✔ [4746/6612] Built Iut.Foundations.SourceEtalePseudofunctorTwoPullbackCancellationTwoCellYTarget (2.6s)
✔ [4749/6612] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapOverlapNestedMiddleTargetAssociatorNaturality (2.9s)
✔ [4750/6612] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapOverlapNestedMiddleDirectTargetNaturalityEndpoints (2.9s)
✔ [4751/6612] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapOverlapNestedMiddleAttached (2.0s)
✔ [4752/6612] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapOverlapCompositeWhiskeredEndpointIsos (2.9s)
⚠ [4753/6612] 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`
✔ [4754/6612] Built Iut.Foundations.SourceEtaleRepresentedStrongTransPointIsoWhiskerLeftInv (3.1s)
✔ [4755/6612] Built Iut.Foundations.SourceEtaleRepresentedStrongTransPointIsoWhiskerLeftSourceTransport (2.0s)
✔ [4756/6612] Built Iut.Foundations.SourceEtaleRepresentedStrongTransPointIsoSymmInv (2.8s)
✔ [4757/6612] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapPointTripleRawCompositorTailHom (2.8s)
✔ [4758/6612] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapPointTripleBaseInverseTail (4.0s)
✔ [4759/6612] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapPointLongEdgeEndpoints (3.4s)
✔ [4760/6612] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapCechCocyclePointTripleValue (2.9s)
✔ [4761/6612] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapPointOverlapValueDirectFactorData (2.0s)
⚠ [4762/6612] 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`
✔ [4763/6612] Built Iut.Foundations.SourceEtaleRepresentedStrongTransPointIsoPentagonHom (3.1s)
✔ [4764/6612] Built Iut.Foundations.SourceEtaleRepresentedStrongTransPointIsoWhiskerRightTransHom (2.0s)
✔ [4765/6612] Built Iut.Foundations.SourceEtaleRepresentedStrongTransPointIsoAssociatorEqToHom (2.9s)
✔ [4766/6612] Built Iut.Foundations.SourceEtaleRepresentedStrongTransPointIsoCongruenceSymmInvAssociator (2.0s)
✔ [4767/6637] Built Iut.Foundations.SourceEtaleStackSchemeAtlasSourceAtlasOverlapCanonicalComparisonLeftFactorIso (2.7s)
✔ [4768/6637] Built Iut.Foundations.SourceEtaleStackSchemeAtlasFiniteEtaleCanonicalDescentStructureComparisonLeft (2.9s)
✔ [4769/6637] Built Iut.Foundations.SourceEtaleStackSchemeAtlasMapCechCompositeFactorization (12s)
✔ [4770/6637] Built Iut.Foundations.SourceOrbicurveFiniteEtaleIteratedBaseChangeForwardBackToSourceExpansion (3.2s)
✔ [4771/6637] Built Iut.Foundations.SourceFiniteEtaleSplitActionFixedAlgebra (4.0s)
✔ [4772/6637] Built Iut.Foundations.SourceFiniteEtaleSignQuotientAffineChartRelativeGluing (3.7s)
✔ [4773/6637] Built Iut.Foundations.SourceFiniteEtaleSignQuotientAtlasLiftWitness (18s)
✔ [4774/6752] Built Iut.Foundations.SourceEtalePseudofunctorTwoPullbackCancellationLiftToYInvToY (2.7s)
✔ [4777/6752] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapOverlapNestedMiddleDirectTargetNaturalityEndpointExpansions (2.9s)
✔ [4778/6752] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapOverlapNestedMiddleDirectTargetNaturalityMiddleRight (2.9s)
✔ [4779/6752] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapOverlapPairWhiskeredExpansion (3.1s)
✔ [4780/6752] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapOverlapCompositeWhiskeredEndpointFactorization (3.0s)
✔ [4781/6752] Built Iut.Foundations.SourceEtaleRepresentedStrongTransPointIsoWhiskerLeftTargetTransportData (2.9s)
✔ [4782/6752] Built Iut.Foundations.SourceEtaleRepresentedStrongTransPointIsoWhiskerLeftSymmHom (2.8s)
⚠ [4783/6752] 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`
✔ [4784/6752] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapPointTripleBaseInverseTailLeftHom (2.0s)
✔ [4785/6752] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapPointTripleCocycleMiddleValueIsos (3.2s)
✔ [4786/6752] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapPointTripleEdgeIso (3.3s)
✔ [4787/6752] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapPointTripleCocycleEndpointValueIso (2.9s)
⚠ [4788/6752] 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`
✔ [4789/6752] Built Iut.Foundations.SourceEtaleRepresentedStrongTransPointIsoWhiskerLeftTransInv (2.8s)
✔ [4790/6752] Built Iut.Foundations.SourceEtaleRepresentedStrongTransPointIsoWhiskerRightTransInv (2.0s)
✔ [4791/6752] Built Iut.Foundations.SourceEtaleRepresentedStrongTransPointIsoPentagonInv (3.2s)
✔ [4792/6752] Built Iut.Foundations.SourceEtaleRepresentedStrongTransPointIsoAssociatorNaturalityLeft (3.0s)
✔ [4793/6752] Built Iut.Foundations.SourceEtaleRepresentedStrongTransPointIsoAssociatorNaturalityMiddle (3.0s)
✔ [4794/6752] Built Iut.Foundations.SourceEtaleRepresentedStrongTransPointIsoAssociatorInvEqToHom (3.0s)
✔ [4795/6752] Built Iut.Foundations.SourceEtaleRepresentedStrongTransPointIsoCongruenceSymmInvAssociatorRestrictionTail (3.1s)
✔ [4796/6752] Built Iut.Foundations.SourceEtaleStackSchemeAtlasSourceAtlasOverlapCanonicalComparisonLeftExpandedIso (2.8s)
✔ [4798/6752] Built Iut.Foundations.SourceFiniteEtaleSchemeCoverGeometricFiberFunctor (2.7s)
✔ [4799/6752] Built Iut.Foundations.SourceSpecFieldSchemeCoproductMaps (2.4s)
✔ [4800/6752] Built Iut.Foundations.SourceFiniteEtaleInvariantAlgHomOrbit (2.5s)
✔ [4801/6752] Built Iut.Foundations.SourceSingleObjTypesOrbitColimit (1.5s)
✔ [4802/7393] Built Iut.Foundations.SourceEtaleStackSchemeAtlasMapCechConeEndpointIsos (2.9s)
✔ [4803/8801] Built Iut.Foundations.SourceFiniteEtaleFixedSubalgebraBaseChange (3.3s)
✔ [4804/8801] Built Iut.Foundations.SourceFiniteEtaleSignQuotientAffineChartIdentityCoherence (549s)
✔ [4805/8801] Built Iut.Foundations.SourceFiniteEtaleSignQuotientAffineChartEffectivity (2.7s)
✔ [4806/8801] Built Iut.Foundations.SourceFiniteEtaleSignQuotientOrbicurve (198s)
✔ [4807/8801] Built Iut.Foundations.SourceEtalePseudofunctorTwoPullbackCancellationNestedWhisker (2.9s)
✔ [4809/8801] Built Iut.Foundations.SourceFiniteEtaleSchemeCoverRepresentable (3.0s)
✔ [4810/8801] Built Iut.Foundations.SourceSchemeEtaleStackPresentationFiniteEtaleCoverFunctor (2.0s)
✔ [4811/8801] Built Iut.Foundations.SourceEtalePseudofunctorContractiblePullback (3.7s)
✔ [4812/8801] Built Iut.Foundations.SourcePreGaloisCategoryEquivalenceTransport (1.8s)
✔ [4813/8801] Built Iut.Foundations.SourcePuncturedWeierstrassSchemeBaseChange (4.1s)
✔ [4814/8801] Built Iut.Foundations.SourceChosenPullbackFunctoriality (1.8s)
✔ [4815/8801] Built Iut.Foundations.SourceSchemeOverFieldRestrictScalarsEtaleSite (2.7s)
✔ [4816/8801] Built Iut.Foundations.SourceOrbicurveEtaleFundamentalGroupTransport (3.1s)
✔ [4817/8801] Built Iut.Foundations.SourceFiniteEtaleSchemeCoverSliceEquivalence (2.0s)
✔ [4818/8801] Built Iut.Foundations.SourceEquivalenceMateNaturality (1.6s)
✔ [4819/8801] Built Iut.Foundations.SourcePseudofunctorStrongTransIsoOfComponents (3.2s)
✔ [4820/8801] Built Iut.Foundations.SourceAnabelioidEquivalence (3.1s)
✔ [4821/8801] Built Iut.Foundations.SourceAnabelioidDominatingPullbackInjectivity (2.8s)
✔ [4822/8801] Built Iut.Foundations.SourceCategoryIsoConjugationInverseCancellation (1.4s)
✔ [4823/8801] Built Iut.Foundations.SourceFiniteEtalePresentedQuotientBaseChange (1.8s)
✔ [4824/8801] Built Iut.Foundations.SourceIdealQuotientEquivComparison (1.9s)
✔ [4825/8993] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapOverlapPairWhiskeredNested (3.2s)
✔ [4826/8993] Built Iut.Foundations.SourceEtaleRepresentedStrongTransPointIsoWhiskerLeftTargetTransportRightData (2.9s)
✔ [4827/8993] Built Iut.Foundations.SourceEtaleRepresentedStrongTransPointIsoWhiskerLeftSymmInv (2.9s)
⚠ [4828/8993] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapPointTripleNaturalityAppTransportData (2.8s)
warning: Iut/Foundations/SourceEtaleStackSchemeAtlasLocalMapPointTripleNaturalityAppTransportData.lean:28:0: Please, add a comment explaining the need for modifying the maxHeartbeat limit, as in
set_option maxHeartbeats 800000 in
-- reason for change
...

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

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

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

Note: This linter can be disabled with `set_option linter.style.longLine false`
✔ [5015/8994] Built Iut.Foundations.SourceEtaleStackSchemeAtlasMapLocalMapCechData (2.7s)
✔ [5016/8994] Built Iut.Foundations.SourceTensorProductAlgebraicFiniteStage (3.0s)
✔ [5017/8994] Built Iut.Foundations.SourceFiniteEtaleAffinePullbackActionReversedTensor (3.9s)
✔ [5018/8994] Built Iut.Foundations.SourceEtaleStackSchemeAtlasFiniteEtalePreDescentPullbacks (7.5s)
✔ [5019/8994] Built Iut.Foundations.SourceEtaleStackSchemeAtlasFiniteEtaleDescentTerminal (2.9s)
✔ [5020/8994] Built Iut.Foundations.SourceFiniteEtaleSchemeCoverBaseChangeFiniteCoproducts (3.3s)
✔ [5021/8994] Built Iut.Foundations.SourceInvolutiveEndofunctorEquivariantForgetReflectsLimits (1.9s)
✔ [5022/8994] Built Iut.Foundations.SourceInvolutiveEndofunctorEquivariantFreeObject (2.0s)
✔ [5023/8994] Built Iut.Foundations.SourceInvolutiveEndofunctorEquivariantForgetReflectsIsomorphisms (1.6s)
✔ [5024/8994] Built Iut.Foundations.SourceInvolutiveEndofunctorEquivariantCofreeMono (1.6s)
✔ [5025/8994] Built Iut.Foundations.SourceFiniteEtaleSchemeCoverInvolutivePostcomposition (105s)
✔ [5026/8994] Built Iut.Foundations.SourceTensorProductRightAlgEquivTmul (1.7s)
✔ [5027/8994] Built Iut.Foundations.SourceTensorProductRingHomTmulFactorization (1.9s)
✔ [5028/8994] Built Iut.Foundations.SourceEquivTransportApplyBackTarget (726ms)
✔ [5029/8994] Built Iut.Foundations.SourceSchemePullbackSectionAlongComposite (4.1s)
✔ [5030/8994] Built Iut.Foundations.SourceEtalePseudofunctorConeReplaceCommutesHomTargetIso (2.6s)
✔ [5031/8994] Built Iut.Foundations.SourceFiniteEtaleSignQuotientAtlasSecondSheetTotalSpaces (3.9s)
✔ [5032/8994] Built Iut.Foundations.SourceFiniteEtaleSignQuotientEquivariantMapIdentity (3.7s)
✔ [5033/8994] Built Iut.Foundations.SourceFiniteEtaleSignQuotientEquivariantMapComposition (4.0s)
✔ [5034/8994] Built Iut.Foundations.SourceFiniteEtaleSignTorsorInvariantEffectiveDescent (3.1s)
✔ [5035/8994] Built Iut.Foundations.SourceFiniteEtaleSignQuotientHomTripleCarrier (2.0s)
✔ [5036/8994] Built Iut.Foundations.SourceFiniteEtaleSignQuotientReindexCompInverseToTotal (2.0s)
✔ [5037/8994] Built Iut.Foundations.SourceCategoryThreeMorphismBridgePastingPackedCompletion (1.3s)
✔ [5038/8994] Built Iut.Foundations.SourceFiniteEtaleSignQuotientPointIdentityReconstructionComparison (3.9s)
✔ [5039/8994] Built Iut.Foundations.SourceGaloisFiberFunctorFiniteColimitsHeterogeneous (2.6s)
✔ [5040/8994] Built Iut.Foundations.SourceContinuousActionRestrictionConnectednessSurjectivity (3.8s)
✔ [5041/8994] Built Iut.Foundations.SourceCategoryTheoryEqToIsoFintypeMapApplyHEq (1.5s)
✔ [5042/8994] Built Iut.Foundations.SourceCategoryTheoryIndexedNatIsoTransportFintypeComponentHEq (1.5s)
✔ [5043/8994] Built Iut.Foundations.SourceFintypeDetachedNaturalityIsoExtension (1.7s)
✔ [5044/8994] Built Iut.Foundations.SourceContinuousActionClosedSubgroupAmbientEnvelope (3.7s)
✔ [5045/8994] Built Iut.Foundations.SourcePointedAnabelioidKernelFiberStability (3.1s)
✔ [5046/8994] Built Iut.Foundations.SourceEquivalenceInversePointNaturality (1.7s)
✔ [5047/8994] Built Iut.Foundations.SourceCategoryPackedHEqEndpointLinkDataCommonRightComparisonDataLeftComm (1.4s)
✔ [5048/8994] Built Iut.Foundations.SourceFunctionHEqCastMapDataPostmap (319ms)
✔ [5049/8994] Built Iut.Foundations.SourceFunctionHEqData (1.4s)
✔ [5050/8994] Built Iut.Foundations.SourceCategoryPackedHEqEndpointLinkDataHiddenEndpointStorageExplicit (1.3s)
✔ [5051/8994] Built Iut.Foundations.SourceCategoryPackedHEqEndpointLinkDataCommonMiddleProjectionDataOfExplicitMiddle (1.3s)
✔ [5052/8994] Built Iut.Foundations.SourceSelectedFiberSurjectiveMapDataComponentDomination (1.6s)
✔ [5053/8994] Built Iut.Foundations.SourceFiniteEtaleSignQuotientPointIdentityReconstructionNaturality (3.2s)
✔ [5054/8994] Built Iut.Foundations.SourceEtalePseudofunctorPointIdentityReconstructionComponent (4.1s)
✔ [5055/8994] Built Iut.Foundations.SourceRegularInvolutiveEquivariantExtension (2.5s)
✔ [5056/8994] Built Iut.Foundations.SourceCategoryProjectionEndpointLinkData (1.4s)
✔ [5057/8994] Built Iut.Foundations.SourceCategoryDetachedHEqPastingData (361ms)
✔ [5058/8994] Built Iut.Foundations.SourceCategoryDetachedHEqDataProjections (331ms)
✔ [5059/8994] Built Iut.Foundations.SourceCategoryComparisonProjectionContextLeftWhisker (1.4s)
✔ [5060/8994] Built Iut.Foundations.SourceOrbicurveFiniteEtaleCoverStabilizerProjectionSurjectivity (3.2s)
✔ [5061/8994] Built Iut.Foundations.SourceOrbicurveFiniteEtaleCoverStabilizerKernelIso (2.8s)
✔ [5062/8994] Built Iut.Foundations.SourceEtaleStackSchemeAtlasYonedaFiberNaturalityOfPointIso (3.4s)
✔ [5063/8994] Built Iut.Foundations.SourceEtaleStackSchemeAtlasPointIsoDescentComparison (5.1s)
✔ [5064/8994] Built Iut.Foundations.SourceOrbicurveSignInvariantIso (3.2s)
✔ [5065/8994] Built Iut.Foundations.SourceOrbicurveSignQuotientComparison (3.3s)
✔ [5066/8994] Built Iut.Foundations.SourceCategoryFunctorSquarePastingEvidenceFirst (1.4s)
✔ [5067/8994] Built Iut.Foundations.SourceCategoryFunctorSquarePastingContext (1.6s)
✔ [5068/8994] Built Iut.Foundations.SourceFiniteEtaleTensorFixedSubalgebra (4.1s)
✔ [5070/8994] Built Iut.Foundations.SourceFiniteEtaleSignQuotientAffineChartCompositionContext (3.5s)
✔ [5071/8994] Built Iut.Foundations.SourceFiniteEtaleSignQuotientAffineChartGluedInvolution (3.8s)
✔ [5072/8994] Built Iut.Foundations.SourceFiniteEtaleSignQuotientAtlasConeLiftTransportSchemeMap (3.1s)

stderr:
/usr/bin/podman timed out after 7200s
podman cleanup removed verifier container apx-verifier-job-1794-runtime-lean_checker-2531931-1789175636538093551-1 on attempt 1

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

apx-runtime-resource-v1	apx-verifier-job-1794-runtime-blueprint_build-2531931-1789182837263085546-2	888832	1400832	21474836480	0	0	0	0	0	0	7028736	109731840	21474836480	0	0	0	0	0	0


blueprint_build failed; continuing (non-fatal phase).

Command runs

git_cloneexit 128duration 245 ms · created 
git clone --depth 1 --branch master --single-branch https://github.com/promachina/iut-lean.git /var/lib/apodeixis/repos/job-1794-source
Cloning into '/var/lib/apodeixis/repos/job-1794-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 5s · created 
git clone (github installation auth fallback)
Cloning into '/var/lib/apodeixis/repos/job-1794-source'...
git_checkoutexit 0duration 363 ms · created 
git checkout 19acd7382f1a0af951064ce2bf36df7fa20c0aea
Note: switching to '19acd7382f1a0af951064ce2bf36df7fa20c0aea'.

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 19acd73 Merge pull request #979 from promachina/e21-929-cohomology-checkpoint
lake_cacheexit 0duration 51s · 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 (403ms)
✔ [10/25] Built Batteries.Data.Array.Match:c.o (208ms)
✔ [11/25] Built Batteries.Data.String.Basic:c.o (115ms)
✔ [12/25] Built Batteries.Data.String.Matcher:c.o (162ms)
✔ [13/25] Built Cache.Lean:c.o (136ms)
✔ [15/25] Built Cache.Init (315ms)
✔ [16/25] Built Cache.IO (1.6s)
✔ [17/25] Built Cache.Init:c.o (81ms)
✔ [18/25] Built Cache.IO:c.o (1.2s)
✔ [19/25] Built Cache.Hashing (854ms)
✔ [20/25] Built Cache.Hashing:c.o (352ms)
✔ [21/25] Built Cache.Requests (2.0s)
✔ [22/25] Built Cache.Requests:c.o (1.8s)
✔ [23/25] Built Cache.Main (918ms)
✔ [24/25] Built Cache.Main:c.o (525ms)
✔ [25/25] Built cache:exe (746ms)

Downloaded: 1 file(s) [attempted 1/8459 = 0%, 13 KB/s], Decompressed: 0
Downloaded: 15 file(s) [attempted 15/8459 = 0%, 9 KB/s], Decompressed: 9
Downloaded: 36 file(s) [attempted 36/8459 = 0%, 24 KB/s], Decompressed: 22
Downloaded: 57 file(s) [attempted 57/8459 = 0%, 45 KB/s], Decompressed: 34
Downloaded: 79 file(s) [attempted 79/8459 = 0%, 271 KB/s], Decompressed: 34
Downloaded: 103 file(s) [attempted 103/8459 = 1%, 229 KB/s], Decompressed: 57
Downloaded: 134 file(s) [attempted 134/8459 = 1%, 40 KB/s], Decompressed: 57
Downloaded: 165 file(s) [attempted 165/8459 = 1%, 346 KB/s], Decompressed: 89
Downloaded: 199 file(s) [attempted 199/8459 = 2%, 362 KB/s], Decompressed: 89
Downloaded: 230 file(s) [attempted 230/8459 = 2%, 86 KB/s], Decompressed: 141
Downloaded: 264 file(s) [attempted 264/8459 = 3%, 668 KB/s], Decompressed: 141
Downloaded: 305 file(s) [attempted 305/8459 = 3%, 536 KB/s], Decompressed: 203
Downloaded: 346 file(s) [attempted 346/8459 = 4%, 730 KB/s], Decompressed: 203
Downloaded: 384 file(s) [attempted 384/8459 = 4%, 115 KB/s], Decompressed: 203
Downloaded: 418 file(s) [attempted 418/8459 = 4%, 210 KB/s], Decompressed: 281
Downloaded: 456 file(s) [attempted 456/8459 = 5%, 198 KB/s], Decompressed: 281
Downloaded: 497 file(s) [attempted 497/8459 = 5%, 418 KB/s], Decompressed: 281
Downloaded: 541 file(s) [attempted 541/8459 = 6%, 335 KB/s], Decompressed: 387
Downloaded: 586 file(s) [attempted 586/8459 = 6%, 371 KB/s], Decompressed: 387
Downloaded: 620 file(s) [attempted 620/8459 = 7%, 59 KB/s], Decompressed: 387
Downloaded: 658 file(s) [attempted 658/8459 = 7%, 87 KB/s], Decompressed: 387
Downloaded: 699 file(s) [attempted 699/8459 = 8%, 270 KB/s], Decompressed: 387
Downloaded: 743 file(s) [attempted 743/8459 = 8%, 307 KB/s], Decompressed: 531
Downloaded: 784 file(s) [attempted 784/8459 = 9%, 458 KB/s], Decompressed: 531
Downloaded: 825 file(s) [attempted 825/8459 = 9%, 118 KB/s], Decompressed: 531
Downloaded: 867 file(s) [attempted 867/8459 = 10%, 395 KB/s], Decompressed: 531
Downloaded: 904 file(s) [attempted 904/8459 = 10%, 221 KB/s], Decompressed: 531
Downloaded: 945 file(s) [attempted 945/8459 = 11%, 206 KB/s], Decompressed: 531
Downloaded: 986 file(s) [attempted 986/8459 = 11%, 261 KB/s], Decompressed: 531
Downloaded: 1027 file(s) [attempted 1027/8459 = 12%, 929 KB/s], Decompressed: 730
Downloaded: 1068 file(s) [attempted 1068/8459 = 12%, 223 KB/s], Decompressed: 730
Downloaded: 1106 file(s) [attempted 1106/8459 = 13%, 119 KB/s], Decompressed: 730
Downloaded: 1144 file(s) [attempted 1144/8459 = 13%, 130 KB/s], Decompressed: 730
Downloaded: 1185 file(s) [attempted 1185/8459 = 14%, 191 KB/s], Decompressed: 730
Downloaded: 1222 file(s) [attempted 1222/8459 = 14%, 364 KB/s], Decompressed: 730
Downloaded: 1263 file(s) [attempted 1263/8459 = 14%, 188 KB/s], Decompressed: 730
Downloaded: 1301 file(s) [attempted 1301/8459 = 15%, 193 KB/s], Decompressed: 730
Downloaded: 1345 file(s) [attempted 1345/8459 = 15%, 224 KB/s], Decompressed: 730
Downloaded: 1386 file(s) [attempted 1386/8459 = 16%, 110 KB/s], Decompressed: 1010
Downloaded: 1427 file(s) [attempted 1427/8459 = 16%, 194 KB/s], Decompressed: 1010
Downloaded: 1465 file(s) [attempted 1465/8459 = 17%, 77 KB/s], Decompressed: 1010
Downloaded: 1503 file(s) [attempted 1503/8459 = 17%, 39 KB/s], Decompressed: 1010
Downloaded: 1547 file(s) [attempted 1547/8459 = 18%, 195 KB/s], Decompressed: 1010
Downloaded: 1588 file(s) [attempted 1588/8459 = 18%, 43 KB/s], Decompressed: 1010
Downloaded: 1633 file(s) [attempted 1633/8459 = 19%, 243 KB/s], Decompressed: 1010
Downloaded: 1670 file(s) [attempted 1670/8459 = 19%, 1608 KB/s], Decompressed: 1010
Downloaded: 1704 file(s) [attempted 1704/8459 = 20%, 152 KB/s], Decompressed: 1010
Downloaded: 1745 file(s) [attempted 1745/8459 = 20%, 98 KB/s], Decompressed: 1352
Downloaded: 1790 file(s) [attempted 1790/8459 = 21%, 399 KB/s], Decompressed: 1352
Downloaded: 1828 file(s) [attempted 1828/8459 = 21%, 549 KB/s], Decompressed: 1352
Downloaded: 1865 file(s) [attempted 1865/8459 = 22%, 1674 KB/s], Decompressed: 1352
Downloaded: 1906 file(s) [attempted 1906/8459 = 22%, 77 KB/s], Decompressed: 1352
Downloaded: 1944 file(s) [attempted 1944/8459 = 22%, 159 KB/s], Decompressed: 1352
Downloaded: 1978 file(s) [attempted 1978/8459 = 23%, 387 KB/s], Decompressed: 1352
Downloaded: 2022 file(s) [attempted 2022/8459 = 23%, 813 KB/s], Decompressed: 1352
Downloaded: 2063 file(s) [attempted 2063/8459 = 24%, 141 KB/s], Decompressed: 1352
Downloaded: 2105 file(s) [attempted 2105/8459 = 24%, 889 KB/s], Decompressed: 1352
Downloaded: 2142 file(s) [attempted 2142/8459 = 25%, 627 KB/s], Decompressed: 1352
Downloaded: 2180 file(s) [attempted 2180/8459 = 25%, 55 KB/s], Decompressed: 1352
Downloaded: 2217 file(s) [attempted 2217/8459 = 26%, 372 KB/s], Decompressed: 1352
Downloaded: 2258 file(s) [attempted 2258/8459 = 26%, 72 KB/s], Decompressed: 1352
Downloaded: 2303 file(s) [attempted 2303/8459 = 27%, 252 KB/s], Decompressed: 1739
Downloaded: 2340 file(s) [attempted 2340/8459 = 27%, 244 KB/s], Decompressed: 1739
Downloaded: 2378 file(s) [attempted 2378/8459 = 28%, 125 KB/s], Decompressed: 1739
Downloaded: 2416 file(s) [attempted 2416/8459 = 28%, 481 KB/s], Decompressed: 1739
Downloaded: 2460 file(s) [attempted 2460/8459 = 29%, 66 KB/s], Decompressed: 1739
Downloaded: 2501 file(s) [attempted 2501/8459 = 29%, 201 KB/s], Decompressed: 1739
Downloaded: 2542 file(s) [attempted 2542/8459 = 30%, 91 KB/s], Decompressed: 1739
Downloaded: 2580 file(s) [attempted 2580/8459 = 30%, 108 KB/s], Decompressed: 1739
Downloaded: 2621 file(s) [attempted 2621/8459 = 30%, 171 KB/s], Decompressed: 1739
Downloaded: 2662 file(s) [attempted 2662/8459 = 31%, 1718 KB/s], Decompressed: 1739
Downloaded: 2696 file(s) [attempted 2696/8459 = 31%, 186 KB/s], Decompressed: 1739
Downloaded: 2737 file(s) [attempted 2737/8459 = 32%, 133 KB/s], Decompressed: 1739
Downloaded: 2778 file(s) [attempted 2778/8459 = 32%, 281 KB/s], Decompressed: 1739
Downloaded: 2823 file(s) [attempted 2823/8459 = 33%, 65 KB/s], Decompressed: 1739
Downloaded: 2864 file(s) [attempted 2864/8459 = 33%, 51 KB/s], Decompressed: 2265
Downloaded: 2905 file(s) [attempted 2905/8459 = 34%, 923 KB/s], Decompressed: 2265
Downloaded: 2946 file(s) [attempted 2946/8459 = 34%, 602 KB/s], Decompressed: 2265
Downloaded: 2983 file(s) [attempted 2983/8459 = 35%, 22 KB/s], Decompressed: 2265
Downloaded: 3024 file(s) [attempted 3024/8459 = 35%, 312 KB/s], Decompressed: 2265
Downloaded: 3062 file(s) [attempted 3062/8459 = 36%, 383 KB/s], Decompressed: 2265
Downloaded: 3103 file(s) [attempted 3103/8459 = 36%, 92 KB/s], Decompressed: 2265
Downloaded: 3144 file(s) [attempted 3144/8459 = 37%, 55 KB/s], Decompressed: 2265
Downloaded: 3178 file(s) [attempted 3178/8459 = 37%, 23 KB/s], Decompressed: 2265
Downloaded: 3223 file(s) [attempted 3223/8459 = 38%, 296 KB/s], Decompressed: 2265
Downloaded: 3264 file(s) [attempted 3264/8459 = 38%, 162 KB/s], Decompressed: 2265
Downloaded: 3308 file(s) [attempted 3308/8459 = 39%, 666 KB/s], Decompressed: 2265
Downloaded: 3349 file(s) [attempted 3349/8459 = 39%, 55 KB/s], Decompressed: 2265
Downloaded: 3387 file(s) [attempted 3387/8459 = 40%, 91 KB/s], Decompressed: 2265
Downloaded: 3424 file(s) [attempted 3424/8459 = 40%, 341 KB/s], Decompressed: 2843
Downloaded: 3472 file(s) [attempted 3472/8459 = 41%, 47 KB/s], Decompressed: 2843
Downloaded: 3517 file(s) [attempted 3517/8459 = 41%, 275 KB/s], Decompressed: 2843
Downloaded: 3551 file(s) [attempted 3551/8459 = 41%, 512 KB/s], Decompressed: 2843
Downloaded: 3589 file(s) [attempted 3589/8459 = 42%, 1175 KB/s], Decompressed: 2843
Downloaded: 3626 file(s) [attempted 3626/8459 = 42%, 411 KB/s], Decompressed: 2843
Downloaded: 3674 file(s) [attempted 3674/8459 = 43%, 54 KB/s], Decompressed: 2843
Downloaded: 3719 file(s) [attempted 3719/8459 = 43%, 83 KB/s], Decompressed: 2843
Downloaded: 3760 file(s) [attempted 3760/8459 = 44%, 113 KB/s], Decompressed: 2843
Downloaded: 3794 file(s) [attempted 3794/8459 = 44%, 460 KB/s], Decompressed: 2843
Downloaded: 3838 file(s) [attempted 3838/8459 = 45%, 349 KB/s], Decompressed: 2843
Downloaded: 3879 file(s) [attempted 3879/8459 = 45%, 107 KB/s], Decompressed: 2843
Downloaded: 3920 file(s) [attempted 3920/8459 = 46%, 332 KB/s], Decompressed: 2843
Downloaded: 3961 file(s) [attempted 3961/8459 = 46%, 32 KB/s], Decompressed: 2843
Downloaded: 4002 file(s) [attempted 4002/8459 = 47%, 145 KB/s], Decompressed: 2843
Downloaded: 4043 file(s) [attempted 4043/8459 = 47%, 751 KB/s], Decompressed: 2843
Downloaded: 4081 file(s) [attempted 4081/8459 = 48%, 756 KB/s], Decompressed: 2843
Downloaded: 4125 file(s) [attempted 4125/8459 = 48%, 360 KB/s], Decompressed: 2843
Downloaded: 4163 file(s) [attempted 4163/8459 = 49%, 199 KB/s], Decompressed: 3424
Downloaded: 4207 file(s) [attempted 4207/8459 = 49%, 59 KB/s], Decompressed: 3424
Downloaded: 4245 file(s) [attempted 4245/8459 = 50%, 78 KB/s], Decompressed: 3424
Downloaded: 4286 file(s) [attempted 4286/8459 = 50%, 539 KB/s], Decompressed: 3424
Downloaded: 4324 file(s) [attempted 4324/8459 = 51%, 74 KB/s], Decompressed: 3424
Downloaded: 4365 file(s) [attempted 4365/8459 = 51%, 378 KB/s], Decompressed: 3424
Downloaded: 4406 file(s) [attempted 4406/8459 = 52%, 81 KB/s], Decompressed: 3424
Downloaded: 4450 file(s) [attempted 4450/8459 = 52%, 64 KB/s], Decompressed: 3424
Downloaded: 4495 file(s) [attempted 4495/8459 = 53%, 233 KB/s], Decompressed: 3424
Downloaded: 4532 file(s) [attempted 4532/8459 = 53%, 457 KB/s], Decompressed: 3424
Downloaded: 4577 file(s) [attempted 4577/8459 = 54%, 76 KB/s], Decompressed: 3424
Downloaded: 4618 file(s) [attempted 4618/8459 = 54%, 355 KB/s], Decompressed: 3424
Downloaded: 4662 file(s) [attempted 4662/8459 = 55%, 68 KB/s], Decompressed: 3424
Downloaded: 4710 file(s) [attempted 4710/8459 = 55%, 323 KB/s], Decompressed: 3424
Downloaded: 4751 file(s) [attempted 4751/8459 = 56%, 79 KB/s], Decompressed: 3424
Downloaded: 4789 file(s) [attempted 4789/8459 = 56%, 106 KB/s], Decompressed: 3424
Downloaded: 4826 file(s) [attempted 4826/8459 = 57%, 42 KB/s], Decompressed: 3424
Downloaded: 4874 file(s) [attempted 4874/8459 = 57%, 297 KB/s], Decompressed: 3424
Downloaded: 4919 file(s) [attempted 4919/8459 = 58%, 922 KB/s], Decompressed: 4156
Downloaded: 4960 file(s) [attempted 4960/8459 = 58%, 121 KB/s], Decompressed: 4156
Downloaded: 4994 file(s) [attempted 4994/8459 = 59%, 1064 KB/s], Decompressed: 4156
Downloaded: 5028 file(s) [attempted 5028/8459 = 59%, 231 KB/s], Decompressed: 4156
Downloaded: 5076 file(s) [attempted 5076/8459 = 60%, 86 KB/s], Decompressed: 4156
Downloaded: 5117 file(s) [attempted 5117/8459 = 60%, 91 KB/s], Decompressed: 4156
Downloaded: 5164 file(s) [attempted 5164/8459 = 61%, 54 KB/s], Decompressed: 4156
Downloaded: 5192 file(s) [attempted 5192/8459 = 61%, 224 KB/s], Decompressed: 4156
Downloaded: 5233 file(s) [attempted 5233/8459 = 61%, 911 KB/s], Decompressed: 4156
Downloaded: 5274 file(s) [attempted 5274/8459 = 62%, 233 KB/s], Decompressed: 4156
Downloaded: 5319 file(s) [attempted 5319/8459 = 62%, 457 KB/s], Decompressed: 4156
Downloaded: 5363 file(s) [attempted 5363/8459 = 63%, 424 KB/s], Decompressed: 4156
Downloaded: 5404 file(s) [attempted 5404/8459 = 63%, 242 KB/s], Decompressed: 4156
Downloaded: 5442 file(s) [attempted 5442/8459 = 64%, 730 KB/s], Decompressed: 4156
Downloaded: 5476 file(s) [attempted 5476/8459 = 64%, 68 KB/s], Decompressed: 4156
Downloaded: 5517 file(s) [attempted 5517/8459 = 65%, 407 KB/s], Decompressed: 4156
Downloaded: 5562 file(s) [attempted 5562/8459 = 65%, 169 KB/s], Decompressed: 4885
Downloaded: 5603 file(s) [attempted 5603/8459 = 66%, 301 KB/s], Decompressed: 4885
Downloaded: 5639 file(s) [attempted 5639/8459 = 66%, 140 KB/s], Decompressed: 4885
Downloaded: 5674 file(s) [attempted 5674/8459 = 67%, 51 KB/s], Decompressed: 4885
Downloaded: 5719 file(s) [attempted 5719/8459 = 67%, 168 KB/s], Decompressed: 4885
Downloaded: 5763 file(s) [attempted 5763/8459 = 68%, 410 KB/s], Decompressed: 4885
Downloaded: 5804 file(s) [attempted 5804/8459 = 68%, 195 KB/s], Decompressed: 4885
Downloaded: 5845 file(s) [attempted 5845/8459 = 69%, 131 KB/s], Decompressed: 4885
Downloaded: 5886 file(s) [attempted 5886/8459 = 69%, 95 KB/s], Decompressed: 4885
Downloaded: 5931 file(s) [attempted 5931/8459 = 70%, 110 KB/s], Decompressed: 4885
Downloaded: 5969 file(s) [attempted 5969/8459 = 70%, 586 KB/s], Decompressed: 4885
Downloaded: 6005 file(s) [attempted 6005/8459 = 70%, 97 KB/s], Decompressed: 4885
Downloaded: 6044 file(s) [attempted 6044/8459 = 71%, 100 KB/s], Decompressed: 4885
Downloaded: 6088 file(s) [attempted 6088/8459 = 71%, 741 KB/s], Decompressed: 4885
Downloaded: 6129 file(s) [attempted 6129/8459 = 72%, 83 KB/s], Decompressed: 4885
Downloaded: 6174 file(s) [attempted 6174/8459 = 72%, 611 KB/s], Decompressed: 4885
Downloaded: 6215 file(s) [attempted 6215/8459 = 73%, 315 KB/s], Decompressed: 5538
Downloaded: 6249 file(s) [attempted 6249/8459 = 73%, 501 KB/s], Decompressed: 5538
Downloaded: 6290 file(s) [attempted 6290/8459 = 74%, 142 KB/s], Decompressed: 5538
Downloaded: 6328 file(s) [attempted 6328/8459 = 74%, 104 KB/s], Decompressed: 5538
Downloaded: 6369 file(s) [attempted 6369/8459 = 75%, 193 KB/s], Decompressed: 5538
Downloaded: 6410 file(s) [attempted 6410/8459 = 75%, 342 KB/s], Decompressed: 5538
Downloaded: 6447 file(s) [attempted 6447/8459 = 76%, 38 KB/s], Decompressed: 5538
Downloaded: 6488 file(s) [attempted 6488/8459 = 76%, 65 KB/s], Decompressed: 5538
Downloaded: 6529 file(s) [attempted 6529/8459 = 77%, 516 KB/s], Decompressed: 5538
Downloaded: 6570 file(s) [attempted 6570/8459 = 77%, 146 KB/s], Decompressed: 5538
Downloaded: 6615 file(s) [attempted 6615/8459 = 78%, 53 KB/s], Decompressed: 5538
Downloaded: 6656 file(s) [attempted 6656/8459 = 78%, 1080 KB/s], Decompressed: 5538
Downloaded: 6693 file(s) [attempted 6693/8459 = 79%, 490 KB/s], Decompressed: 5538
Downloaded: 6728 file(s) [attempted 6728/8459 = 79%, 1612 KB/s], Decompressed: 6187
Downloaded: 6772 file(s) [attempted 6772/8459 = 80%, 1288 KB/s], Decompressed: 6187
Downloaded: 6813 file(s) [attempted 6813/8459 = 80%, 169 KB/s], Decompressed: 6187
Downloaded: 6854 file(s) [attempted 6854/8459 = 81%, 109 KB/s], Decompressed: 6187
Downloaded: 6892 file(s) [attempted 6892/8459 = 81%, 1850 KB/s], Decompressed: 6187
Downloaded: 6933 file(s) [attempted 6933/8459 = 81%, 45 KB/s], Decompressed: 6187
Downloaded: 6974 file(s) [attempted 6974/8459 = 82%, 619 KB/s], Decompressed: 6187
Downloaded: 7018 file(s) [attempted 7018/8459 = 82%, 218 KB/s], Decompressed: 6187
Downloaded: 7059 file(s) [attempted 7059/8459 = 83%, 212 KB/s], Decompressed: 6187
Downloaded: 7097 file(s) [attempted 7097/8459 = 83%, 95 KB/s], Decompressed: 6187
Downloaded: 7131 file(s) [attempted 7131/8459 = 84%, 84 KB/s], Decompressed: 6187
Downloaded: 7172 file(s) [attempted 7172/8459 = 84%, 135 KB/s], Decompressed: 6187
Downloaded: 7216 file(s) [attempted 7216/8459 = 85%, 662 KB/s], Decompressed: 6728
Downloaded: 7254 file(s) [attempted 7254/8459 = 85%, 63 KB/s], Decompressed: 6728
Downloaded: 7295 file(s) [attempted 7295/8459 = 86%, 423 KB/s], Decompressed: 6728
Downloaded: 7333 file(s) [attempted 7333/8459 = 86%, 70 KB/s], Decompressed: 6728
Downloaded: 7374 file(s) [attempted 7374/8459 = 87%, 67 KB/s], Decompressed: 6728
Downloaded: 7415 file(s) [attempted 7415/8459 = 87%, 132 KB/s], Decompressed: 6728
Downloaded: 7456 file(s) [attempted 7456/8459 = 88%, 253 KB/s], Decompressed: 6728
Downloaded: 7500 file(s) [attempted 7500/8459 = 88%, 96 KB/s], Decompressed: 6728
Downloaded: 7538 file(s) [attempted 7538/8459 = 89%, 121 KB/s], Decompressed: 6728
Downloaded: 7579 file(s) [attempted 7579/8459 = 89%, 887 KB/s], Decompressed: 6728
Downloaded: 7617 file(s) [attempted 7617/8459 = 90%, 515 KB/s], Decompressed: 7186
Downloaded: 7658 file(s) [attempted 7658/8459 = 90%, 1676 KB/s], Decompressed: 7186
Downloaded: 7702 file(s) [attempted 7702/8459 = 91%, 1109 KB/s], Decompressed: 7186
Downloaded: 7743 file(s) [attempted 7743/8459 = 91%, 186 KB/s], Decompressed: 7186
Downloaded: 7784 file(s) [attempted 7784/8459 = 92%, 28 KB/s], Decompressed: 7186
Downloaded: 7825 file(s) [attempted 7825/8459 = 92%, 139 KB/s], Decompressed: 7186
Downloaded: 7863 file(s) [attempted 7863/8459 = 92%, 55 KB/s], Decompressed: 7186
Downloaded: 7901 file(s) [attempted 7901/8459 = 93%, 119 KB/s], Decompressed: 7186
Downloaded: 7942 file(s) [attempted 7942/8459 = 93%, 572 KB/s], Decompressed: 7186
Downloaded: 7983 file(s) [attempted 7983/8459 = 94%, 207 KB/s], Decompressed: 7186
Downloaded: 8020 file(s) [attempted 8020/8459 = 94%, 648 KB/s], Decompressed: 7593
Downloaded: 8061 file(s) [attempted 8061/8459 = 95%, 128 KB/s], Decompressed: 7593
Downloaded: 8102 file(s) [attempted 8102/8459 = 95%, 138 KB/s], Decompressed: 7593
Downloaded: 8147 file(s) [attempted 8147/8459 = 96%, 177 KB/s], Decompressed: 7593
Downloaded: 8184 file(s) [attempted 8184/8459 = 96%, 354 KB/s], Decompressed: 7593
Downloaded: 8229 file(s) [attempted 8229/8459 = 97%, 500 KB/s], Decompressed: 7593
Downloaded: 8263 file(s) [attempted 8263/8459 = 97%, 229 KB/s], Decompressed: 7593
Downloaded: 8304 file(s) [attempted 8304/8459 = 98%, 452 KB/s], Decompressed: 7593
Downloaded: 8345 file(s) [attempted 8345/8459 = 98%, 960 KB/s], Decompressed: 7593
Downloaded: 8390 file(s) [attempted 8390/8459 = 99%, 50 KB/s], Decompressed: 7593
Downloaded: 8431 file(s) [attempted 8431/8459 = 99%, 39 KB/s], Decompressed: 8020
Downloaded: 8458 file(s) [attempted 8458/8459 = 99%, 266 KB/s], Decompressed: 8020
Downloaded: 8459 file(s) [attempted 8459/8459 = 100%, 266 KB/s], Decompressed: 8020

apx-runtime-resource-v1	apx-verifier-job-1794-runtime-lake_cache-2531931-1789175585251014580-0	888832	1409024	21474836480	0	0	0	0	0	0	8140165120	8454991872	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`
✔ [4608/6597] Built Iut.Foundations.SourceEtalePseudofunctorTwoPullbackCancellationLiftToYInv (2.8s)
✔ [4609/6597] Built Iut.Foundations.SourceFiniteEtaleAffineOverCoordinateAction (2.4s)
✔ [4611/6597] Built Iut.Foundations.SourceSingleObjOppositeEquivalence (1.6s)
✔ [4612/6597] Built Iut.Foundations.SourceCategoryPackedHEqEndpointLinkDataJoinProjections (1.4s)
✔ [4613/6597] Built Iut.Foundations.SourceEtalePseudofunctorStrongTransWhiskerRightIsoSymmHom (2.7s)
✔ [4614/6597] Built Iut.Foundations.SourceEtalePseudofunctorStrongTransPentagonInvPrefix (4.3s)
✔ [4615/6597] Built Iut.Foundations.SourceCategoryEqToHomTransportedEndpointDataMap (1.4s)
✔ [4616/6597] Built Iut.Foundations.SourceEtalePseudofunctorChangeFirstBaseMap (3.9s)
✔ [4617/6597] Built Iut.Foundations.SourceEtalePseudofunctorChangeSecondBaseMap (3.7s)
✔ [4618/6597] Built Iut.Foundations.SourceEtalePseudofunctorFaithfulCellAssembly (3.8s)
✔ [4619/6597] Built Iut.Foundations.SourceEtalePseudofunctorRepresentablePullbackTwoCell (117s)
✔ [4620/6597] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalHomPointValueRecovery (2.0s)
✔ [4621/6597] Built Iut.Foundations.SourceFiniteEtaleSchemeCoverClopenMono (2.8s)
⚠ [4623/6597] Built Iut.Foundations.SourceFiniteEtaleSignTorsorAffineEffectiveness (167s)
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`
✔ [4624/6597] Built Iut.Foundations.SourceFiniteEtaleSignQuotientPrestack (42s)
✔ [4625/6597] Built Iut.Foundations.SourceFiniteEtaleSignTorsorTargetStackDescent (3.0s)
✔ [4626/6597] Built Iut.Foundations.SourceFiniteEtaleSignTorsorTrivial (4.8s)
✔ [4627/6597] Built Iut.Foundations.SourceEtalePseudofunctorTwoPullbackCancellationLiftToYLawful (2.8s)
✔ [4628/6597] Built Iut.Foundations.SourceFiniteEtaleAffineOverCoordinateFiniteEtale (2.5s)
✔ [4629/6597] Built Iut.Foundations.SourceCategoryPackedHEqTwoMorphismComposition (1.4s)
✔ [4630/6597] Built Iut.Foundations.SourceEtaleStackRepresentablePropertyChangeMap (2.6s)
✔ [4631/6597] Built Iut.Foundations.SourceEtalePseudofunctorConeAfterChangeSecondBaseMap (2.0s)
✔ [4632/6597] Built Iut.Foundations.SourceEtalePseudofunctorRepresentedIsoPointLift (3.2s)
✔ [4633/6597] Built Iut.Foundations.SourceEtalePseudofunctorRepresentablePullbackWitness (2.9s)
✔ [4634/6597] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalHomYonedaPointValue (2.8s)
✔ [4635/6597] Built Iut.Foundations.SourceFiniteEtaleSchemeCoverDirectSummand (3.3s)
✔ [4636/6597] Built Iut.Foundations.SourceFiniteEtaleSchemeCoverUnderlyingEpiRange (2.8s)
⚠ [4637/6597] 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`
✔ [4638/6600] Built Iut.Foundations.SourceFiniteEtaleSignQuotientStackCriterion (3.1s)
✔ [4639/6600] Built Iut.Foundations.SourceFiniteEtaleSignQuotientAtlas (5.7s)
✔ [4640/6601] Built Iut.Foundations.SourceEtalePseudofunctorTwoPullbackCancellationLiftToYHomToX (2.9s)
✔ [4641/6601] Built Iut.Foundations.SourceEtalePseudofunctorConeAfterChangeSecondBaseMapFromConeOf (3.2s)
✔ [4642/6601] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalIsoBaseChangeOver (3.3s)
✔ [4643/6601] Built Iut.Foundations.SourceRepresentableStrongTransReconstruction (3.1s)
✔ [4644/6601] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalHomYonedaNaturality (2.9s)
✔ [4645/6601] Built Iut.Foundations.SourceFiniteEtaleSchemeCoverAffineSource (2.9s)
✔ [4646/6601] Built Iut.Foundations.SourceFiniteEtaleSchemeCoverUnderlyingEpiSurjective (7.3s)
⚠ [4647/6601] Built Iut.Foundations.SourceFiniteEtaleSignTorsorAffineCoverAssembly (892s)
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`
✔ [4649/6601] Built Iut.Foundations.SourceFiniteEtaleSignQuotientAtlasBaseChange (17s)
✔ [4650/6601] Built Iut.Foundations.SourceEtalePseudofunctorTwoPullbackCancellationLiftToYHomToY (2.7s)
✔ [4652/6601] Built Iut.Foundations.SourceEtaleStackRepresentableLocalIsoDescent (3.7s)
✔ [4653/6601] Built Iut.Foundations.SourceEtaleStackSchemeAtlasOverlapMultiplication (2.0s)
✔ [4654/6601] Built Iut.Foundations.SourceEtalePseudofunctorRepresentablePullbackAlongStrongTrans (3.8s)
✔ [4655/6601] Built Iut.Foundations.SourceFiniteEtaleSchemeCoverAffineGroupQuotient (3.1s)
✔ [4656/6601] Built Iut.Foundations.SourceFiniteEtaleSchemeCoverBalanced (2.7s)
✔ [4657/6601] Built Iut.Foundations.SourceFiniteEtaleSignTorsorAffineCoverRestriction (126s)
✔ [4659/6601] Built Iut.Foundations.SourceFiniteEtaleSignQuotientAtlasLiftApp (124s)
✔ [4660/6601] Built Iut.Foundations.SourceFiniteEtaleSignQuotientAtlasInvariant (3.7s)
✔ [4661/6602] Built Iut.Foundations.SourceEtalePseudofunctorTwoPullbackCancellationLiftCompatibility (2.8s)
✔ [4662/6604] Built Iut.Foundations.SourceEtaleStackRepresentableAtlasLocalIsoDescent (3.2s)
✔ [4663/6604] Built Iut.Foundations.SourceOrbicurveFiniteEtaleBaseChangeSchemeCoverMapReflectsLocalIso (3.5s)
✔ [4664/6604] Built Iut.Foundations.SourceEtaleStackSchemeAtlasOverlapMultiplicationRepresentedLongConeIso (2.9s)
✔ [4665/6604] Built Iut.Foundations.SourceEtaleStackSchemeAtlasOverlapConePasting (3.1s)
✔ [4666/6604] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapCechData (3.1s)
✔ [4667/6604] Built Iut.Foundations.SourceEtaleStackSchemeAtlasFiniteEtaleDescent (3.4s)
✔ [4668/6604] Built Iut.Foundations.SourceOrbicurveFiniteEtaleIteratedBaseChange (9.5s)
✔ [4669/6604] Built Iut.Foundations.SourceFiniteEtaleSchemeCoverAffineOverFullyFaithful (2.8s)
✔ [4670/6604] Built Iut.Foundations.SourceFiniteEtaleFixedSubalgebra (3.1s)
✔ [4671/6604] Built Iut.Foundations.SourceFiniteEtaleSignTorsorAffineCoverFiniteEffectivity (3.5s)
✔ [4673/6604] Built Iut.Foundations.SourceFiniteEtaleSignQuotientAtlasLiftNaturality (106s)
✔ [4674/6604] Built Iut.Foundations.SourceFiniteEtaleSignQuotientAtlasInvariantElement (3.1s)
✔ [4675/6606] Built Iut.Foundations.SourceEtalePseudofunctorTwoPullbackCancellationConeMorphismCompatibility (3.1s)
✔ [4678/6606] Built Iut.Foundations.SourceEtaleStackSchemeAtlasOverlapConePastingIso (4.1s)
✔ [4679/6606] Built Iut.Foundations.SourceEtaleStackSchemeAtlasOverlapConePastingCell (2.9s)
✔ [4680/6606] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapRestrictionCongrIsoNaturality (3.1s)
✔ [4681/6606] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapRestrictionCongrIsoWhiskerRightFactorization (3.0s)
✔ [4682/6606] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapOverlapNestedMiddleIso (2.9s)
✔ [4683/6606] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapPointObject (2.9s)
✔ [4684/6606] Built Iut.Foundations.SourceEtaleStackSchemeAtlasFiniteEtaleDescentComparison (3.2s)
✔ [4685/6606] Built Iut.Foundations.SourceEtaleStackSchemeAtlasMapCechEndpointIsos (3.0s)
✔ [4686/6606] Built Iut.Foundations.SourceEtaleStackSchemeAtlasBaseChangePointIso (3.0s)
✔ [4687/6606] Built Iut.Foundations.SourceOrbicurveFiniteEtaleIteratedBaseChangeForwardBackLiftedHom (3.4s)
✔ [4688/6606] Built Iut.Foundations.SourceEtaleStackSchemeAtlasOverlapMapIso (2.8s)
✔ [4689/6606] Built Iut.Foundations.SourceOrbicurveFiniteEtaleIteratedBaseChangeToSourceIso (2.8s)
✔ [4690/6606] Built Iut.Foundations.SourceFiniteEtaleFixedAffineQuotient (3.0s)
✔ [4691/6606] Built Iut.Foundations.SourceFiniteEtaleSignTorsorAffineRefinement (3.8s)
✔ [4692/6606] Built Iut.Foundations.SourceFiniteEtaleSignQuotientAtlasLift (3.0s)
✔ [4693/6606] Built Iut.Foundations.SourceFiniteEtaleSignQuotientAtlasInvariantComponent (25s)
✔ [4694/6607] Built Iut.Foundations.SourceEtalePseudofunctorTwoPullbackCancellationConeMorphism (3.3s)
✔ [4697/6607] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapOverlapNestedMiddleHom (3.2s)
✔ [4698/6607] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapOverlapNestedEndpointIsos (2.9s)
✔ [4699/6607] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapPointOverlap (3.2s)
✔ [4700/6607] Built Iut.Foundations.SourceEtaleStackSchemeAtlasFiniteEtaleDescentConstruction (42s)
✔ [4701/6607] Built Iut.Foundations.SourceEtaleStackSchemeAtlasMapCechPairMiddleIso (3.1s)
✔ [4702/6607] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalHomPointIsoValue (3.2s)
✔ [4703/6607] Built Iut.Foundations.SourceOrbicurveFiniteEtaleIteratedBaseChangeForwardBackLiftedHomComparison (2.9s)
✔ [4704/6607] Built Iut.Foundations.SourceFiniteEtaleOrbitConstantAlgebra (3.1s)
✔ [4705/6607] Built Iut.Foundations.SourceFiniteEtaleSignQuotientStackRefinement (3.2s)
✔ [4706/6607] Built Iut.Foundations.SourceFiniteEtaleSignQuotientAtlasLiftProjections (13s)
✔ [4707/6607] Built Iut.Foundations.SourceFiniteEtaleSignQuotientAtlasInvariantCocycle (19s)
✔ [4708/6609] Built Iut.Foundations.SourceEtalePseudofunctorTwoPullbackCancellationTwoCell (2.5s)
✔ [4711/6609] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapOverlapNestedMiddleCompositeFactorization (3.1s)
✔ [4712/6609] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapPullbackOverlapNestedFactorization (3.4s)
✔ [4713/6609] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapPointTransition (3.3s)
✔ [4714/6609] Built Iut.Foundations.SourceOrbicurveFiniteEtaleBaseChangePointIsoToSourceIso (2.9s)
✔ [4715/6609] Built Iut.Foundations.SourceEtaleStackSchemeAtlasFiniteEtaleDescentCoherence (13s)
✔ [4716/6609] Built Iut.Foundations.SourceEtaleStackSchemeAtlasMapCechPairFactorization (22s)
✔ [4717/6609] Built Iut.Foundations.SourceOrbicurveFiniteEtaleIteratedBaseChangeForwardBackStrongTransToSource (3.0s)
✔ [4718/6609] Built Iut.Foundations.SourceFiniteEtaleSplitAlgebraHom (3.3s)
✔ [4719/6609] Built Iut.Foundations.SourceFiniteEtaleSignQuotientAffineChartDescent (16s)
✔ [4720/6609] Built Iut.Foundations.SourceFiniteEtaleSignQuotientAtlasLiftTwoCell (291s)
✔ [4721/6609] Built Iut.Foundations.SourceFiniteEtaleSignQuotientAtlasLiftUnit (14s)
✔ [4722/6611] Built Iut.Foundations.SourceEtalePseudofunctorTwoPullbackCancellationTwoCellToX (2.7s)
✔ [4724/6611] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapOverlapNestedMiddleCompositeTargetCollapse (2.0s)
✔ [4725/6611] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapOverlapNestedMiddleCompositeSourceCollapse (3.1s)
✔ [4726/6611] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapOverlapNestedSpecializations (2.9s)
✔ [4727/6611] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapOverlapCompositeWhiskeredExpansion (3.1s)
✔ [4728/6611] Built Iut.Foundations.SourceEtaleRepresentedRestrictionPointIsoCongruenceTail (3.1s)
✔ [4729/6611] Built Iut.Foundations.SourceEtaleRepresentedStrongTransPointIsoWhiskerRightHom (2.9s)
✔ [4730/6611] Built Iut.Foundations.SourceEtaleRepresentedStrongTransPointIsoWhiskerLeft (3.8s)
✔ [4731/6611] Built Iut.Foundations.SourceEtaleRepresentedStrongTransPointIsoSymmHom (2.9s)
✔ [4732/6611] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapPointOverlapValueIsoRepresented (2.9s)
✔ [4733/6611] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapPointCocycleGeometry (3.4s)
✔ [4734/6611] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapCechCocyclePointValue (2.0s)
✔ [4735/6611] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapRestrictionCompositePointIsoHom (6.7s)
⚠ [4736/6611] Built Iut.Foundations.SourceEtaleRepresentedStrongTransPointIsoTransHom (2.9s)
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`
✔ [4737/6611] Built Iut.Foundations.SourceOrbicurveFiniteEtaleBaseChangePointIsoToSourceCompatibility (3.0s)
✔ [4738/6611] Built Iut.Foundations.SourceEtaleRepresentedStrongTransPointIsoCongruenceAssociator (3.2s)
✔ [4739/6611] Built Iut.Foundations.SourceEtaleStackSchemeAtlasFiniteEtaleCoverOverlapComparisonLeft (2.0s)
✔ [4740/6611] Built Iut.Foundations.SourceEtaleStackSchemeAtlasFiniteEtaleCanonicalDescentStructureComparison (2.0s)
✔ [4741/6611] Built Iut.Foundations.SourceEtaleStackSchemeAtlasMapCechPairLongFactorization (2.9s)
✔ [4742/6611] Built Iut.Foundations.SourceOrbicurveFiniteEtaleIteratedBaseChangeForwardBackRealizationToSourceExpansion (3.0s)
✔ [4743/6611] Built Iut.Foundations.SourceFiniteEtaleSplitAlgebraAutomorphism (2.7s)
✔ [4744/6611] Built Iut.Foundations.SourceFiniteEtaleSignQuotientAffineChartGluing (8.3s)
✔ [4745/6611] Built Iut.Foundations.SourceFiniteEtaleSignQuotientAtlasLiftCompatibility (18s)
✔ [4746/6612] Built Iut.Foundations.SourceEtalePseudofunctorTwoPullbackCancellationTwoCellYTarget (2.6s)
✔ [4749/6612] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapOverlapNestedMiddleTargetAssociatorNaturality (2.9s)
✔ [4750/6612] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapOverlapNestedMiddleDirectTargetNaturalityEndpoints (2.9s)
✔ [4751/6612] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapOverlapNestedMiddleAttached (2.0s)
✔ [4752/6612] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapOverlapCompositeWhiskeredEndpointIsos (2.9s)
⚠ [4753/6612] 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`
✔ [4754/6612] Built Iut.Foundations.SourceEtaleRepresentedStrongTransPointIsoWhiskerLeftInv (3.1s)
✔ [4755/6612] Built Iut.Foundations.SourceEtaleRepresentedStrongTransPointIsoWhiskerLeftSourceTransport (2.0s)
✔ [4756/6612] Built Iut.Foundations.SourceEtaleRepresentedStrongTransPointIsoSymmInv (2.8s)
✔ [4757/6612] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapPointTripleRawCompositorTailHom (2.8s)
✔ [4758/6612] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapPointTripleBaseInverseTail (4.0s)
✔ [4759/6612] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapPointLongEdgeEndpoints (3.4s)
✔ [4760/6612] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapCechCocyclePointTripleValue (2.9s)
✔ [4761/6612] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapPointOverlapValueDirectFactorData (2.0s)
⚠ [4762/6612] 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`
✔ [4763/6612] Built Iut.Foundations.SourceEtaleRepresentedStrongTransPointIsoPentagonHom (3.1s)
✔ [4764/6612] Built Iut.Foundations.SourceEtaleRepresentedStrongTransPointIsoWhiskerRightTransHom (2.0s)
✔ [4765/6612] Built Iut.Foundations.SourceEtaleRepresentedStrongTransPointIsoAssociatorEqToHom (2.9s)
✔ [4766/6612] Built Iut.Foundations.SourceEtaleRepresentedStrongTransPointIsoCongruenceSymmInvAssociator (2.0s)
✔ [4767/6637] Built Iut.Foundations.SourceEtaleStackSchemeAtlasSourceAtlasOverlapCanonicalComparisonLeftFactorIso (2.7s)
✔ [4768/6637] Built Iut.Foundations.SourceEtaleStackSchemeAtlasFiniteEtaleCanonicalDescentStructureComparisonLeft (2.9s)
✔ [4769/6637] Built Iut.Foundations.SourceEtaleStackSchemeAtlasMapCechCompositeFactorization (12s)
✔ [4770/6637] Built Iut.Foundations.SourceOrbicurveFiniteEtaleIteratedBaseChangeForwardBackToSourceExpansion (3.2s)
✔ [4771/6637] Built Iut.Foundations.SourceFiniteEtaleSplitActionFixedAlgebra (4.0s)
✔ [4772/6637] Built Iut.Foundations.SourceFiniteEtaleSignQuotientAffineChartRelativeGluing (3.7s)
✔ [4773/6637] Built Iut.Foundations.SourceFiniteEtaleSignQuotientAtlasLiftWitness (18s)
✔ [4774/6752] Built Iut.Foundations.SourceEtalePseudofunctorTwoPullbackCancellationLiftToYInvToY (2.7s)
✔ [4777/6752] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapOverlapNestedMiddleDirectTargetNaturalityEndpointExpansions (2.9s)
✔ [4778/6752] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapOverlapNestedMiddleDirectTargetNaturalityMiddleRight (2.9s)
✔ [4779/6752] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapOverlapPairWhiskeredExpansion (3.1s)
✔ [4780/6752] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapOverlapCompositeWhiskeredEndpointFactorization (3.0s)
✔ [4781/6752] Built Iut.Foundations.SourceEtaleRepresentedStrongTransPointIsoWhiskerLeftTargetTransportData (2.9s)
✔ [4782/6752] Built Iut.Foundations.SourceEtaleRepresentedStrongTransPointIsoWhiskerLeftSymmHom (2.8s)
⚠ [4783/6752] 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`
✔ [4784/6752] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapPointTripleBaseInverseTailLeftHom (2.0s)
✔ [4785/6752] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapPointTripleCocycleMiddleValueIsos (3.2s)
✔ [4786/6752] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapPointTripleEdgeIso (3.3s)
✔ [4787/6752] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapPointTripleCocycleEndpointValueIso (2.9s)
⚠ [4788/6752] 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`
✔ [4789/6752] Built Iut.Foundations.SourceEtaleRepresentedStrongTransPointIsoWhiskerLeftTransInv (2.8s)
✔ [4790/6752] Built Iut.Foundations.SourceEtaleRepresentedStrongTransPointIsoWhiskerRightTransInv (2.0s)
✔ [4791/6752] Built Iut.Foundations.SourceEtaleRepresentedStrongTransPointIsoPentagonInv (3.2s)
✔ [4792/6752] Built Iut.Foundations.SourceEtaleRepresentedStrongTransPointIsoAssociatorNaturalityLeft (3.0s)
✔ [4793/6752] Built Iut.Foundations.SourceEtaleRepresentedStrongTransPointIsoAssociatorNaturalityMiddle (3.0s)
✔ [4794/6752] Built Iut.Foundations.SourceEtaleRepresentedStrongTransPointIsoAssociatorInvEqToHom (3.0s)
✔ [4795/6752] Built Iut.Foundations.SourceEtaleRepresentedStrongTransPointIsoCongruenceSymmInvAssociatorRestrictionTail (3.1s)
✔ [4796/6752] Built Iut.Foundations.SourceEtaleStackSchemeAtlasSourceAtlasOverlapCanonicalComparisonLeftExpandedIso (2.8s)
✔ [4798/6752] Built Iut.Foundations.SourceFiniteEtaleSchemeCoverGeometricFiberFunctor (2.7s)
✔ [4799/6752] Built Iut.Foundations.SourceSpecFieldSchemeCoproductMaps (2.4s)
✔ [4800/6752] Built Iut.Foundations.SourceFiniteEtaleInvariantAlgHomOrbit (2.5s)
✔ [4801/6752] Built Iut.Foundations.SourceSingleObjTypesOrbitColimit (1.5s)
✔ [4802/7393] Built Iut.Foundations.SourceEtaleStackSchemeAtlasMapCechConeEndpointIsos (2.9s)
✔ [4803/8801] Built Iut.Foundations.SourceFiniteEtaleFixedSubalgebraBaseChange (3.3s)
✔ [4804/8801] Built Iut.Foundations.SourceFiniteEtaleSignQuotientAffineChartIdentityCoherence (549s)
✔ [4805/8801] Built Iut.Foundations.SourceFiniteEtaleSignQuotientAffineChartEffectivity (2.7s)
✔ [4806/8801] Built Iut.Foundations.SourceFiniteEtaleSignQuotientOrbicurve (198s)
✔ [4807/8801] Built Iut.Foundations.SourceEtalePseudofunctorTwoPullbackCancellationNestedWhisker (2.9s)
✔ [4809/8801] Built Iut.Foundations.SourceFiniteEtaleSchemeCoverRepresentable (3.0s)
✔ [4810/8801] Built Iut.Foundations.SourceSchemeEtaleStackPresentationFiniteEtaleCoverFunctor (2.0s)
✔ [4811/8801] Built Iut.Foundations.SourceEtalePseudofunctorContractiblePullback (3.7s)
✔ [4812/8801] Built Iut.Foundations.SourcePreGaloisCategoryEquivalenceTransport (1.8s)
✔ [4813/8801] Built Iut.Foundations.SourcePuncturedWeierstrassSchemeBaseChange (4.1s)
✔ [4814/8801] Built Iut.Foundations.SourceChosenPullbackFunctoriality (1.8s)
✔ [4815/8801] Built Iut.Foundations.SourceSchemeOverFieldRestrictScalarsEtaleSite (2.7s)
✔ [4816/8801] Built Iut.Foundations.SourceOrbicurveEtaleFundamentalGroupTransport (3.1s)
✔ [4817/8801] Built Iut.Foundations.SourceFiniteEtaleSchemeCoverSliceEquivalence (2.0s)
✔ [4818/8801] Built Iut.Foundations.SourceEquivalenceMateNaturality (1.6s)
✔ [4819/8801] Built Iut.Foundations.SourcePseudofunctorStrongTransIsoOfComponents (3.2s)
✔ [4820/8801] Built Iut.Foundations.SourceAnabelioidEquivalence (3.1s)
✔ [4821/8801] Built Iut.Foundations.SourceAnabelioidDominatingPullbackInjectivity (2.8s)
✔ [4822/8801] Built Iut.Foundations.SourceCategoryIsoConjugationInverseCancellation (1.4s)
✔ [4823/8801] Built Iut.Foundations.SourceFiniteEtalePresentedQuotientBaseChange (1.8s)
✔ [4824/8801] Built Iut.Foundations.SourceIdealQuotientEquivComparison (1.9s)
✔ [4825/8993] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapOverlapPairWhiskeredNested (3.2s)
✔ [4826/8993] Built Iut.Foundations.SourceEtaleRepresentedStrongTransPointIsoWhiskerLeftTargetTransportRightData (2.9s)
✔ [4827/8993] Built Iut.Foundations.SourceEtaleRepresentedStrongTransPointIsoWhiskerLeftSymmInv (2.9s)
⚠ [4828/8993] Built Iut.Foundations.SourceEtaleStackSchemeAtlasLocalMapPointTripleNaturalityAppTransportData (2.8s)
warning: Iut/Foundations/SourceEtaleStackSchemeAtlasLocalMapPointTripleNaturalityAppTransportData.lean:28:0: Please, add a comment explaining the need for modifying the maxHeartbeat limit, as in
set_option maxHeartbeats 800000 in
-- reason for change
...

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

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

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

Note: This linter can be disabled with `set_option linter.style.longLine false`
✔ [5015/8994] Built Iut.Foundations.SourceEtaleStackSchemeAtlasMapLocalMapCechData (2.7s)
✔ [5016/8994] Built Iut.Foundations.SourceTensorProductAlgebraicFiniteStage (3.0s)
✔ [5017/8994] Built Iut.Foundations.SourceFiniteEtaleAffinePullbackActionReversedTensor (3.9s)
✔ [5018/8994] Built Iut.Foundations.SourceEtaleStackSchemeAtlasFiniteEtalePreDescentPullbacks (7.5s)
✔ [5019/8994] Built Iut.Foundations.SourceEtaleStackSchemeAtlasFiniteEtaleDescentTerminal (2.9s)
✔ [5020/8994] Built Iut.Foundations.SourceFiniteEtaleSchemeCoverBaseChangeFiniteCoproducts (3.3s)
✔ [5021/8994] Built Iut.Foundations.SourceInvolutiveEndofunctorEquivariantForgetReflectsLimits (1.9s)
✔ [5022/8994] Built Iut.Foundations.SourceInvolutiveEndofunctorEquivariantFreeObject (2.0s)
✔ [5023/8994] Built Iut.Foundations.SourceInvolutiveEndofunctorEquivariantForgetReflectsIsomorphisms (1.6s)
✔ [5024/8994] Built Iut.Foundations.SourceInvolutiveEndofunctorEquivariantCofreeMono (1.6s)
✔ [5025/8994] Built Iut.Foundations.SourceFiniteEtaleSchemeCoverInvolutivePostcomposition (105s)
✔ [5026/8994] Built Iut.Foundations.SourceTensorProductRightAlgEquivTmul (1.7s)
✔ [5027/8994] Built Iut.Foundations.SourceTensorProductRingHomTmulFactorization (1.9s)
✔ [5028/8994] Built Iut.Foundations.SourceEquivTransportApplyBackTarget (726ms)
✔ [5029/8994] Built Iut.Foundations.SourceSchemePullbackSectionAlongComposite (4.1s)
✔ [5030/8994] Built Iut.Foundations.SourceEtalePseudofunctorConeReplaceCommutesHomTargetIso (2.6s)
✔ [5031/8994] Built Iut.Foundations.SourceFiniteEtaleSignQuotientAtlasSecondSheetTotalSpaces (3.9s)
✔ [5032/8994] Built Iut.Foundations.SourceFiniteEtaleSignQuotientEquivariantMapIdentity (3.7s)
✔ [5033/8994] Built Iut.Foundations.SourceFiniteEtaleSignQuotientEquivariantMapComposition (4.0s)
✔ [5034/8994] Built Iut.Foundations.SourceFiniteEtaleSignTorsorInvariantEffectiveDescent (3.1s)
✔ [5035/8994] Built Iut.Foundations.SourceFiniteEtaleSignQuotientHomTripleCarrier (2.0s)
✔ [5036/8994] Built Iut.Foundations.SourceFiniteEtaleSignQuotientReindexCompInverseToTotal (2.0s)
✔ [5037/8994] Built Iut.Foundations.SourceCategoryThreeMorphismBridgePastingPackedCompletion (1.3s)
✔ [5038/8994] Built Iut.Foundations.SourceFiniteEtaleSignQuotientPointIdentityReconstructionComparison (3.9s)
✔ [5039/8994] Built Iut.Foundations.SourceGaloisFiberFunctorFiniteColimitsHeterogeneous (2.6s)
✔ [5040/8994] Built Iut.Foundations.SourceContinuousActionRestrictionConnectednessSurjectivity (3.8s)
✔ [5041/8994] Built Iut.Foundations.SourceCategoryTheoryEqToIsoFintypeMapApplyHEq (1.5s)
✔ [5042/8994] Built Iut.Foundations.SourceCategoryTheoryIndexedNatIsoTransportFintypeComponentHEq (1.5s)
✔ [5043/8994] Built Iut.Foundations.SourceFintypeDetachedNaturalityIsoExtension (1.7s)
✔ [5044/8994] Built Iut.Foundations.SourceContinuousActionClosedSubgroupAmbientEnvelope (3.7s)
✔ [5045/8994] Built Iut.Foundations.SourcePointedAnabelioidKernelFiberStability (3.1s)
✔ [5046/8994] Built Iut.Foundations.SourceEquivalenceInversePointNaturality (1.7s)
✔ [5047/8994] Built Iut.Foundations.SourceCategoryPackedHEqEndpointLinkDataCommonRightComparisonDataLeftComm (1.4s)
✔ [5048/8994] Built Iut.Foundations.SourceFunctionHEqCastMapDataPostmap (319ms)
✔ [5049/8994] Built Iut.Foundations.SourceFunctionHEqData (1.4s)
✔ [5050/8994] Built Iut.Foundations.SourceCategoryPackedHEqEndpointLinkDataHiddenEndpointStorageExplicit (1.3s)
✔ [5051/8994] Built Iut.Foundations.SourceCategoryPackedHEqEndpointLinkDataCommonMiddleProjectionDataOfExplicitMiddle (1.3s)
✔ [5052/8994] Built Iut.Foundations.SourceSelectedFiberSurjectiveMapDataComponentDomination (1.6s)
✔ [5053/8994] Built Iut.Foundations.SourceFiniteEtaleSignQuotientPointIdentityReconstructionNaturality (3.2s)
✔ [5054/8994] Built Iut.Foundations.SourceEtalePseudofunctorPointIdentityReconstructionComponent (4.1s)
✔ [5055/8994] Built Iut.Foundations.SourceRegularInvolutiveEquivariantExtension (2.5s)
✔ [5056/8994] Built Iut.Foundations.SourceCategoryProjectionEndpointLinkData (1.4s)
✔ [5057/8994] Built Iut.Foundations.SourceCategoryDetachedHEqPastingData (361ms)
✔ [5058/8994] Built Iut.Foundations.SourceCategoryDetachedHEqDataProjections (331ms)
✔ [5059/8994] Built Iut.Foundations.SourceCategoryComparisonProjectionContextLeftWhisker (1.4s)
✔ [5060/8994] Built Iut.Foundations.SourceOrbicurveFiniteEtaleCoverStabilizerProjectionSurjectivity (3.2s)
✔ [5061/8994] Built Iut.Foundations.SourceOrbicurveFiniteEtaleCoverStabilizerKernelIso (2.8s)
✔ [5062/8994] Built Iut.Foundations.SourceEtaleStackSchemeAtlasYonedaFiberNaturalityOfPointIso (3.4s)
✔ [5063/8994] Built Iut.Foundations.SourceEtaleStackSchemeAtlasPointIsoDescentComparison (5.1s)
✔ [5064/8994] Built Iut.Foundations.SourceOrbicurveSignInvariantIso (3.2s)
✔ [5065/8994] Built Iut.Foundations.SourceOrbicurveSignQuotientComparison (3.3s)
✔ [5066/8994] Built Iut.Foundations.SourceCategoryFunctorSquarePastingEvidenceFirst (1.4s)
✔ [5067/8994] Built Iut.Foundations.SourceCategoryFunctorSquarePastingContext (1.6s)
✔ [5068/8994] Built Iut.Foundations.SourceFiniteEtaleTensorFixedSubalgebra (4.1s)
✔ [5070/8994] Built Iut.Foundations.SourceFiniteEtaleSignQuotientAffineChartCompositionContext (3.5s)
✔ [5071/8994] Built Iut.Foundations.SourceFiniteEtaleSignQuotientAffineChartGluedInvolution (3.8s)
✔ [5072/8994] Built Iut.Foundations.SourceFiniteEtaleSignQuotientAtlasConeLiftTransportSchemeMap (3.1s)

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

apx-runtime-resource-v1	apx-verifier-job-1794-runtime-blueprint_build-2531931-1789182837263085546-2	888832	1400832	21474836480	0	0	0	0	0	0	7028736	109731840	21474836480	0	0	0	0	0	0

Keyboard shortcuts