info: mathlib: cloning https://github.com/leanprover-community/mathlib4
info: mathlib: checking out revision 'fabf563a7c95a166b8d7b6efca11c8b4dc9d911f'
info: plausible: cloning https://github.com/leanprover-community/plausible
info: plausible: checking out revision '63045536fe95024e6c18fc7b48e03f506701c5bc'
info: LeanSearchClient: cloning https://github.com/leanprover-community/LeanSearchClient
info: LeanSearchClient: checking out revision 'c5d5b8fe6e5158def25cd28eb94e4141ad97c843'
info: importGraph: cloning https://github.com/leanprover-community/import-graph
info: importGraph: checking out revision '5c7542ed018c78194f1e2b903eaf6a792b74c03d'
info: proofwidgets: cloning https://github.com/leanprover-community/ProofWidgets4
info: proofwidgets: checking out revision '24b0d9dc081c5423f8eec7e866c441e5184f29d9'
info: aesop: cloning https://github.com/leanprover-community/aesop
info: aesop: checking out revision 'e3cb2f741431ce31bf73549fb52316a57368b06f'
info: Qq: cloning https://github.com/leanprover-community/quote4
info: Qq: checking out revision 'f46324995fca5f0483b742e4eb4daec7f4ee50d2'
info: batteries: cloning https://github.com/leanprover-community/batteries
info: batteries: checking out revision 'fa08db58b30eb033edcdab331bba000827f9f785'
info: Cli: cloning https://github.com/leanprover/lean4-cli
info: Cli: checking out revision '92564e5770e4d09f2d86dfbf8ada1e9c715b384c'
✔ [5/25] Built Batteries.Data.String.Basic (290ms)
✔ [6/25] Built Cache.Lean (330ms)
✔ [7/25] Built Cache.Init (248ms)
✔ [8/25] Built Cache.Init:c.o (77ms)
✔ [9/25] Built Batteries.Data.String.Basic:c.o (141ms)
✔ [10/25] Built Cache.Lean:c.o (167ms)
✔ [11/25] Built Batteries.Data.Array.Match (593ms)
✔ [12/25] Built Batteries.Data.Array.Match:c.o (222ms)
✔ [13/25] Built Batteries.Data.String.Matcher (280ms)
✔ [14/25] Built Batteries.Tactic.OpenPrivate (849ms)
✔ [15/25] Built Batteries.Data.String.Matcher:c.o (175ms)
✔ [16/25] Built Batteries.Tactic.OpenPrivate:c.o (1.1s)
✔ [17/25] Built Cache.IO (1.3s)
✔ [18/25] Built Cache.Hashing (714ms)
✔ [19/25] Built Cache.Hashing:c.o (394ms)
✔ [20/25] Built Cache.IO:c.o (1.5s)
✔ [21/25] Built Cache.Requests (1.8s)
✔ [22/25] Built Cache.Main (893ms)
✔ [23/25] Built Cache.Main:c.o (605ms)
✔ [24/25] Built Cache.Requests:c.o (2.2s)
✔ [25/25] Built cache:exe (605ms)
⚠ [8557/8592] Built Research.BinomialBounds (1.2s)
warning: Research/BinomialBounds.lean:41:46: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice

Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false`
✔ [8559/8592] Built Research.Basic (3.0s)
✔ [8560/8592] Built Research.SupportInjective (4.3s)
⚠ [8561/8592] Built Research.Frame (4.7s)
warning: Research/Frame.lean:72:6: Try `simp at himem` instead of `simpa using himem`

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`
warning: Research/Frame.lean:86:0: automatically included section variable(s) unused in theorem `Research.frameSpike_mem`:
  [(i : Fin n) → DecidableEq (S i)]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [(i : Fin n) → DecidableEq (S i)] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
warning: Research/Frame.lean:96:0: automatically included section variable(s) unused in theorem `Research.frameSpike_not_axis`:
  [(i : Fin n) → DecidableEq (S i)]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [(i : Fin n) → DecidableEq (S i)] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
warning: Research/Frame.lean:104:0: automatically included section variable(s) unused in theorem `Research.frameSpike_private`:
  [(i : Fin n) → DecidableEq (S i)]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [(i : Fin n) → DecidableEq (S i)] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
warning: Research/Frame.lean:136:0: automatically included section variable(s) unused in theorem `Research.frameAxisPoint_on_axis`:
  [(i : Fin n) → DecidableEq (S i)]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [(i : Fin n) → DecidableEq (S i)] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
warning: Research/Frame.lean:141:0: automatically included section variable(s) unused in theorem `Research.frameAxisPoint_private`:
  [(i : Fin n) → DecidableEq (S i)]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [(i : Fin n) → DecidableEq (S i)] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
✔ [8562/8592] Built Research.Periodic (4.3s)
⚠ [8563/8592] Built Research.Squarefree (4.6s)
warning: Research/Squarefree.lean:44:0: automatically included section variable(s) unused in theorem `Research.crtFinEquiv_apply`:
  [DecidableEq ι]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [DecidableEq ι] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
warning: Research/Squarefree.lean:57:0: automatically included section variable(s) unused in theorem `Research.subsetModulus_pos`:
  [Fintype ι]
  [DecidableEq ι]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [Fintype ι] [DecidableEq ι] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
warning: Research/Squarefree.lean:89:0: automatically included section variable(s) unused in theorem `Research.subsetModulus_eq_prod`:
  [Fintype ι]
  [DecidableEq ι]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [Fintype ι] [DecidableEq ι] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
✔ [8564/8592] Built Research.UpperBound (4.6s)
⚠ [8565/8592] Built Research.SparseFrame (4.3s)
warning: Research/SparseFrame.lean:40:0: automatically included section variable(s) unused in theorem `Research.sparseFrame_covers`:
  [DecidableEq T]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [DecidableEq T] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
warning: Research/SparseFrame.lean:69:0: automatically included section variable(s) unused in theorem `Research.sparseFrame_private`:
  [DecidableEq T]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [DecidableEq T] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
⚠ [8566/8592] Built Research.Transport (4.2s)
warning: Research/Transport.lean:18:0: automatically included section variable(s) unused in theorem `Research.minimalDistinctCover_of_equiv`:
  [DecidableEq M]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [DecidableEq M] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
⚠ [8567/8592] Built Research.ArithmeticFrame (4.7s)
warning: Research/ArithmeticFrame.lean:247:4: try 'simp' instead of 'simpa'

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`
⚠ [8568/8592] Built Research.SparseArithmetic (5.1s)
warning: Research/SparseArithmetic.lean:163:37: try 'simp' instead of 'simpa'

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`
warning: Research/SparseArithmetic.lean:170:10: try 'simp' instead of 'simpa'

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`
⚠ [8569/8592] Built Research.Assignments (5.2s)
warning: Research/Assignments.lean:29:2: try 'simp' instead of 'simpa'

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`
✔ [8570/8592] Built Research.AssignmentCounting (5.5s)
⚠ [8571/8592] Built Research.PrimeConstruction (4.9s)
warning: Research/PrimeConstruction.lean:56:36: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice

Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false`
warning: Research/PrimeConstruction.lean:97:4: try 'simp' instead of 'simpa'

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`
warning: Research/PrimeConstruction.lean:158:40: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice

Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false`
warning: Research/PrimeConstruction.lean:197:40: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice

Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false`
⚠ [8572/8592] Built Research.SparseAssignments (5.1s)
warning: Research/SparseAssignments.lean:204:12: try 'simp' instead of 'simpa'

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`
⚠ [8573/8592] Built Research.ExplicitLower (4.3s)
warning: Research/ExplicitLower.lean:65:46: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice

Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false`
⚠ [8574/8592] Built Research.SparseRangeCounting (4.0s)
warning: Research/SparseRangeCounting.lean:41:8: automatically included section variable(s) unused in theorem `Research.assignmentForSparseRanges_range`:
  [(i : Fin m) → Fintype (Pool i)]
  [(i : Fin m) → DecidableEq (Pool i)]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [(i : Fin m) → Fintype (Pool i)] [(i : Fin m) → DecidableEq (Pool i)] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
warning: Research/SparseRangeCounting.lean:113:0: automatically included section variable(s) unused in theorem `Research.card_sparseRangeProfile`:
  [(i : Fin m) → DecidableEq (Pool i)]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [(i : Fin m) → DecidableEq (Pool i)] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
warning: Research/SparseRangeCounting.lean:125:0: automatically included section variable(s) unused in theorem `Research.sparseSystemForRanges_mem_counted`:
  [(i : Fin m) → Fintype (Pool i)]
  [(i : Fin m) → DecidableEq (Pool i)]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [(i : Fin m) → Fintype (Pool i)] [(i : Fin m) → DecidableEq (Pool i)] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
⚠ [8575/8592] Built Research.CrossPairPool (4.7s)
warning: Research/CrossPairPool.lean:32:13: This simp argument is unused:
  Fin.val_mk

Hint: Omit it from the simp argument list.
  simp only [̵F̵i̵n̵.̵v̵a̵l̵_̵m̵k̵]̵ ̵at hv

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Research/CrossPairPool.lean:52:10: This simp argument is unused:
  blow

Hint: Omit it from the simp argument list.
  simp only [crossPairSupport, Finset.mem_insert, Finset.mem_singleton,
  ̵  ̵ ̵ ̵alow, bl̵o̵w̵,̵ ̵b̵high] at halow

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Research/CrossPairPool.lean:52:16: This simp argument is unused:
  bhigh

Hint: Omit it from the simp argument list.
  simp only [crossPairSupport, Finset.mem_insert, Finset.mem_singleton,
  ̵  ̵ ̵ ̵alow, blow,̵ ̵b̵h̵i̵g̵h̵] at halow

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Research/CrossPairPool.lean:59:17: This simp argument is unused:
  Fin.val_mk

Hint: Omit it from the simp argument list.
  simp only [̵F̵i̵n̵.̵v̵a̵l̵_̵m̵k̵]̵ ̵at hv

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Research/CrossPairPool.lean:66:11: This simp argument is unused:
  blow

Hint: Omit it from the simp argument list.
  simp only [crossPairSupport, Finset.mem_insert, Finset.mem_singleton,
  ̵  ̵ ̵ ̵ahigh, bl̵o̵w̵,̵ ̵b̵high] at hahigh

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Research/CrossPairPool.lean:66:17: This simp argument is unused:
  bhigh

Hint: Omit it from the simp argument list.
  simp only [crossPairSupport, Finset.mem_insert, Finset.mem_singleton,
  ̵  ̵ ̵ ̵ahigh, blow,̵ ̵b̵h̵i̵g̵h̵] at hahigh

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Research/CrossPairPool.lean:70:17: This simp argument is unused:
  Fin.val_mk

Hint: Omit it from the simp argument list.
  simp only [̵F̵i̵n̵.̵v̵a̵l̵_̵m̵k̵]̵ ̵at hv

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Research/CrossPairPool.lean:75:17: This simp argument is unused:
  Fin.val_mk

Hint: Omit it from the simp argument list.
  simp only [̵F̵i̵n̵.̵v̵a̵l̵_̵m̵k̵]̵ ̵at hv

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Research/CrossPairPool.lean:144:8: This simp argument is unused:
  card_nonzeroResidue

Hint: Omit it from the simp argument list.
  simp ̵[̵c̵a̵r̵d̵_̵n̵o̵n̵z̵e̵r̵o̵R̵e̵s̵i̵d̵u̵e̵]̵

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
⚠ [8576/8592] Built Research.PrimePolynomial (6.0s)
warning: Research/PrimePolynomial.lean:115:46: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice

Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false`
⚠ [8577/8592] Built Research.SparseClosing (4.9s)
warning: Research/SparseClosing.lean:35:21: Try `simp at hab` instead of `simpa using hab`

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`
warning: Research/SparseClosing.lean:45:20: Try `simp at hab` instead of `simpa using hab`

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`
warning: Research/SparseClosing.lean:22:5: Variable name `hhpos` is not explicitly referenced.

The binding can be removed (if unused) or named `_` (if used implicitly).

Note: This linter can be disabled with `set_option linter.unusedVariables false`
warning: Research/SparseClosing.lean:149:25: Variable name `hcap` is not explicitly referenced.

The binding can be removed (if unused) or named `_` (if used implicitly).

Note: This linter can be disabled with `set_option linter.unusedVariables false`
⚠ [8578/8592] Built Research.PrimeLinearLog (5.9s)
warning: Research/PrimeLinearLog.lean:149:46: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice

Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false`
⚠ [8579/8592] Built Research.AllCutoffLower (4.4s)
warning: Research/AllCutoffLower.lean:36:38: This simp argument is unused:
  l

Hint: Omit it from the simp argument list.
  simp only [m, lowerFrameIndex, L, l,̵ ̵ll̵, D]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Research/AllCutoffLower.lean:36:41: This simp argument is unused:
  ll

Hint: Omit it from the simp argument list.
  simp only [m, lowerFrameIndex, L, l, l̵l̵,̵ ̵D]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Research/AllCutoffLower.lean:36:45: This simp argument is unused:
  D

Hint: Omit it from the simp argument list.
  simp only [m, lowerFrameIndex, L, l, ll,̵ ̵D̵]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
⚠ [8580/8592] Built Research.SparsePrimeCapacity (5.0s)
warning: Research/SparsePrimeCapacity.lean:147:9: Variable name `j` is not explicitly referenced.

The binding can be removed (if unused) or named `_` (if used implicitly).

Note: This linter can be disabled with `set_option linter.unusedVariables false`
warning: Research/SparsePrimeCapacity.lean:155:9: Variable name `j` is not explicitly referenced.

The binding can be removed (if unused) or named `_` (if used implicitly).

Note: This linter can be disabled with `set_option linter.unusedVariables false`
✔ [8581/8592] Built Research.FinalEstimate (3.0s)
⚠ [8582/8592] Built Research.SparsePrimeCount (4.8s)
warning: Research/SparsePrimeCount.lean:45:8: try 'simp' instead of 'simpa'

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`
warning: Research/SparsePrimeCount.lean:31:8: this tactic is never executed

Note: This linter can be disabled with `set_option linter.unreachableTactic false`
warning: Research/SparsePrimeCount.lean:31:8: 'simp [k]' tactic does nothing

Note: This linter can be disabled with `set_option linter.unusedTactic false`
⚠ [8583/8592] Built Research.SparseModulusBound (5.1s)
warning: Research/SparseModulusBound.lean:214:13: Variable name `j` is not explicitly referenced.

The binding can be removed (if unused) or named `_` (if used implicitly).

Note: This linter can be disabled with `set_option linter.unusedVariables false`
✔ [8584/8592] Built Research.SparseParametricLower (4.0s)
✔ [8585/8592] Built Research.SparseExponentBound (4.3s)
✔ [8586/8592] Built Research.SparseCutoffPolynomial (4.5s)
✔ [8587/8592] Built Research.SparseAllCutoff (5.3s)
✔ [8588/8592] Built Research.SparseFinalEstimate (4.1s)
✔ [8589/8592] Built Research.SparseCoarseBound (16s)
⚠ [8590/8592] Built Research.SparseAsymptotic (6.6s)
warning: Research/SparseAsymptotic.lean:129:44: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice

Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false`
warning: Research/SparseAsymptotic.lean:172:47: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice

Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false`
warning: Research/SparseAsymptotic.lean:209:15: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice

Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false`
warning: Research/SparseAsymptotic.lean:236:50: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice

Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false`
warning: Research/SparseAsymptotic.lean:309:35: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice

Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false`
warning: Research/SparseAsymptotic.lean:344:49: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice

Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false`
warning: Research/SparseAsymptotic.lean:388:39: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice

Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false`
✔ [8591/8592] Built Research (3.7s)
Build completed successfully (8592 jobs).
PASS: Lean checked log(log F(x))/log x tends to one
