⚠ [8579/8737] Replayed PrimeNumberTheoremAnd.Wiener
warning: PrimeNumberTheoremAnd/Wiener.lean:323:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/Wiener.lean:342:8: declaration uses `sorry`
ℹ [8590/8737] Replayed PrimeNumberTheoremAnd.MediumPNT
info: PrimeNumberTheoremAnd/MediumPNT.lean:4282:0: 'MediumPNT' depends on axioms: [propext, Classical.choice, Quot.sound]
⚠ [8593/8737] Replayed PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RosserSchoenfeldZeta
warning: PrimeNumberTheoremAnd/IEANTN/RosserSchoenfeld/RosserSchoenfeldZeta.lean:18:8: declaration uses `sorry`
⚠ [8597/8737] Replayed PrimeNumberTheoremAnd.IEANTN.ZetaSummary
warning: PrimeNumberTheoremAnd/IEANTN/ZetaSummary.lean:35:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/ZetaSummary.lean:48:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/ZetaSummary.lean:58:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/ZetaSummary.lean:68:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/ZetaSummary.lean:78:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/ZetaSummary.lean:88:8: declaration uses `sorry`
⚠ [8620/8737] Replayed LeanCert.Examples.Li2Bounds
warning: LeanCert/Examples/Li2Bounds.lean:40:8: declaration uses `sorry`
warning: LeanCert/Examples/Li2Bounds.lean:48:8: declaration uses `sorry`
⚠ [8692/8737] Replayed PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RosserSchoenfeldPrime
warning: PrimeNumberTheoremAnd/IEANTN/RosserSchoenfeld/RosserSchoenfeldPrime.lean:1017:8: declaration uses `sorry`
ℹ [8694/8737] Replayed Research.Basic
info: Research/Basic.lean:40:0: Erdos796.Statement : Prop
⚠ [8696/8737] Replayed Research.CoreSidon
warning: Research/CoreSidon.lean:82:8: try 'simp' instead of 'simpa'

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`
warning: Research/CoreSidon.lean:92:6: try 'simp' instead of 'simpa'

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`
⚠ [8698/8737] Replayed Research.FiberTypes
warning: Research/FiberTypes.lean:57:12: try 'simp' instead of 'simpa'

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`
warning: Research/FiberTypes.lean:78:12: try 'simp' instead of 'simpa'

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`
warning: Research/FiberTypes.lean:98:12: try 'simp' instead of 'simpa'

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`
⚠ [8702/8737] Replayed Research.SemiprimeAsymptotic
info: Research/SemiprimeAsymptotic.lean:121:2: Try this:
  [apply] ring_nf
  
  The `ring` tactic failed to close the goal. Use `ring_nf` to obtain a normal form.
    
  Note that `ring` works primarily in *commutative* rings. If you have a noncommutative ring, abelian group or module, consider using `noncomm_ring`, `abel` or `module` instead.
warning: Research/SemiprimeAsymptotic.lean:182:43: Variable name `hC` 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/SemiprimeAsymptotic.lean:917:6: 'push_cast' tactic does nothing

Note: This linter can be disabled with `set_option linter.unusedTactic false`
⚠ [8703/8737] Replayed Research.UpperCombinatorics
warning: Research/UpperCombinatorics.lean:45:18: Variable name `hu` 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/UpperCombinatorics.lean:45:45: Variable name `huW` 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/UpperCombinatorics.lean:50:24: Variable name `husS` 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/UpperCombinatorics.lean:51:5: Variable name `htpT` 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/UpperCombinatorics.lean:84:5: Variable name `h10S` 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/UpperCombinatorics.lean:85:26: Variable name `h01T` 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/UpperCombinatorics.lean:126:0: automatically included section variable(s) unused in theorem `Erdos796.bipartiteRow_offDiag_eq`:
  [Fintype α]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [Fintype α] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
warning: Research/UpperCombinatorics.lean:131:67: This simp argument is unused:
  and_assoc

Hint: Omit it from the simp argument list.
  simp [bipartiteRow, Finset.mem_offDiag, and_comm, and_left_comm,̵ ̵a̵n̵d̵_̵a̵s̵s̵o̵c̵]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Research/UpperCombinatorics.lean:326:0: automatically included section variable(s) unused in theorem `Erdos796.alphaFiber_offDiag_eq`:
  [Fintype β]
  [Fintype γ]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [Fintype β] [Fintype γ] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
warning: Research/UpperCombinatorics.lean:331:65: This simp argument is unused:
  and_assoc

Hint: Omit it from the simp argument list.
  simp [alphaFiber, Finset.mem_offDiag, and_comm, and_left_comm,̵ ̵a̵n̵d̵_̵a̵s̵s̵o̵c̵]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Research/UpperCombinatorics.lean:335:0: automatically included section variable(s) unused in theorem `Erdos796.commonSlice_rectangleFree`:
  [Fintype α]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [Fintype α] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
⚠ [8704/8737] Replayed Research.UpperStructure
warning: Research/UpperStructure.lean:112:28: Variable name `hdpos` 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`
⚠ [8705/8737] Replayed Research.UpperFiberHypergraphs
warning: Research/UpperFiberHypergraphs.lean:125:0: automatically included section variable(s) unused in theorem `Erdos796.canonicalFactorGraph_rectangleFree`:
  [DecidableEq X]
  [DecidableEq Y]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [DecidableEq X] [DecidableEq Y] in theorem ...

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

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

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
⚠ [8708/8737] Replayed Research.UpperSmooth
warning: Research/UpperSmooth.lean:33:16: This simp argument is unused:
  min_eq_left

Hint: Omit it from the simp argument list.
  simp [min_eq_l̵e̵f̵t̵,̵ ̵m̵i̵n̵_̵e̵q̵_̵right, max_eq_left, max_eq_right, h, hx₁, hy₁]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Research/UpperSmooth.lean:33:29: This simp argument is unused:
  min_eq_right

Hint: Omit it from the simp argument list.
  simp [min_eq_left, mi̵n̵_̵e̵q̵_̵r̵i̵g̵h̵t̵,̵ ̵m̵ax_eq_left, max_eq_right, h, hx₁, hy₁]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Research/UpperSmooth.lean:33:43: This simp argument is unused:
  max_eq_left

Hint: Omit it from the simp argument list.
  simp [min_eq_left, min_eq_right, max_eq_l̵e̵f̵t̵,̵ ̵m̵a̵x̵_̵e̵q̵_̵right, h, hx₁, hy₁]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Research/UpperSmooth.lean:33:56: This simp argument is unused:
  max_eq_right

Hint: Omit it from the simp argument list.
  simp [min_eq_left, min_eq_right, max_eq_left, m̵a̵x̵_̵e̵q̵_̵r̵i̵g̵h̵t̵,̵ ̵h, hx₁, hy₁]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Research/UpperSmooth.lean:39:16: This simp argument is unused:
  min_eq_left

Hint: Omit it from the simp argument list.
  simp [min_eq_l̵e̵f̵t̵,̵ ̵m̵i̵n̵_̵e̵q̵_̵right, max_eq_left, max_eq_right, h, hx₂, hy₂]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Research/UpperSmooth.lean:39:29: This simp argument is unused:
  min_eq_right

Hint: Omit it from the simp argument list.
  simp [min_eq_left, mi̵n̵_̵e̵q̵_̵r̵i̵g̵h̵t̵,̵ ̵m̵ax_eq_left, max_eq_right, h, hx₂, hy₂]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Research/UpperSmooth.lean:39:43: This simp argument is unused:
  max_eq_left

Hint: Omit it from the simp argument list.
  simp [min_eq_left, min_eq_right, max_eq_l̵e̵f̵t̵,̵ ̵m̵a̵x̵_̵e̵q̵_̵right, h, hx₂, hy₂]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Research/UpperSmooth.lean:39:56: This simp argument is unused:
  max_eq_right

Hint: Omit it from the simp argument list.
  simp [min_eq_left, min_eq_right, max_eq_left, m̵a̵x̵_̵e̵q̵_̵r̵i̵g̵h̵t̵,̵ ̵h, hx₂, hy₂]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Research/UpperSmooth.lean:45:16: This simp argument is unused:
  min_eq_left

Hint: Omit it from the simp argument list.
  simp [min_eq_l̵e̵f̵t̵,̵ ̵m̵i̵n̵_̵e̵q̵_̵right, max_eq_left, max_eq_right, h, hx₃, hy₃]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Research/UpperSmooth.lean:45:29: This simp argument is unused:
  min_eq_right

Hint: Omit it from the simp argument list.
  simp [min_eq_left, mi̵n̵_̵e̵q̵_̵r̵i̵g̵h̵t̵,̵ ̵m̵ax_eq_left, max_eq_right, h, hx₃, hy₃]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Research/UpperSmooth.lean:45:43: This simp argument is unused:
  max_eq_left

Hint: Omit it from the simp argument list.
  simp [min_eq_left, min_eq_right, max_eq_l̵e̵f̵t̵,̵ ̵m̵a̵x̵_̵e̵q̵_̵right, h, hx₃, hy₃]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Research/UpperSmooth.lean:45:56: This simp argument is unused:
  max_eq_right

Hint: Omit it from the simp argument list.
  simp [min_eq_left, min_eq_right, max_eq_left, m̵a̵x̵_̵e̵q̵_̵r̵i̵g̵h̵t̵,̵ ̵h, hx₃, hy₃]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
⚠ [8709/8737] Replayed Research.TruncatedTypes
warning: Research/TruncatedTypes.lean:19:0: automatically included section variable(s) unused in theorem `Erdos796.repeatedTypes_pairwise_compatible`:
  [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/TruncatedTypes.lean:50:0: automatically included section variable(s) unused in theorem `Erdos796.exceptionalTypeIndices_card_le_powerset`:
  [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`
ℹ [8713/8737] Replayed Research.GenericProfileAsymptotic
info: Research/GenericProfileAsymptotic.lean:500:4: Try this:
  [apply] ring_nf
  
  The `ring` tactic failed to close the goal. Use `ring_nf` to obtain a normal form.
    
  Note that `ring` works primarily in *commutative* rings. If you have a noncommutative ring, abelian group or module, consider using `noncomm_ring`, `abel` or `module` instead.
⚠ [8715/8737] Replayed Research.UpperTruncation
warning: Research/UpperTruncation.lean:222:24: This simp argument is unused:
  hR

Hint: Omit it from the simp argument list.
  simp ̵[̵h̵R̵]̵

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
⚠ [8716/8737] Replayed Research.UpperRemainder
warning: Research/UpperRemainder.lean:146:2: 'push_cast at hdecomp' tactic does nothing

Note: This linter can be disabled with `set_option linter.unusedTactic false`
info: Research/UpperRemainder.lean:179:26: Try this:
  [apply] ring_nf
  
  The `ring` tactic failed to close the goal. Use `ring_nf` to obtain a normal form.
    
  Note that `ring` works primarily in *commutative* rings. If you have a noncommutative ring, abelian group or module, consider using `noncomm_ring`, `abel` or `module` instead.
warning: Research/UpperRemainder.lean:179:22: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice

Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false`
⚠ [8719/8737] Replayed Research.SmoothExceptional
warning: Research/SmoothExceptional.lean:68:43: try 'simp' instead of 'simpa'

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`
warning: Research/SmoothExceptional.lean:71:51: try 'simp' instead of 'simpa'

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`
⚠ [8720/8737] Replayed Research.SmoothAsymptotic
warning: Research/SmoothAsymptotic.lean:296:4: 'norm_num' tactic does nothing

Note: This linter can be disabled with `set_option linter.unusedTactic false`
warning: Research/SmoothAsymptotic.lean:490:19: this tactic is never executed

Note: This linter can be disabled with `set_option linter.unreachableTactic false`
warning: Research/SmoothAsymptotic.lean:490:19: 'ring' tactic does nothing

Note: This linter can be disabled with `set_option linter.unusedTactic false`
⚠ [8722/8737] Replayed Research.IncidenceExcess
warning: Research/IncidenceExcess.lean:55:31: This simp argument is unused:
  and_assoc

Hint: Omit it from the simp argument list.
  simp [coefficientFiber, Finset.mem_offDiag, and_comm, a̵n̵d̵_̵l̵e̵f̵t̵_̵c̵o̵m̵m̵,̵ ̵a̵n̵d̵_̵a̵s̵s̵o̵c̵]̵a̲n̲d̲_̲l̲e̲f̲t̲_̲c̲o̲m̲m̲]̲

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
⚠ [8723/8737] Replayed Research.RayProjection
warning: Research/RayProjection.lean:14:0: automatically included section variable(s) unused in theorem `Erdos796.rayIncidence_cubeFree`:
  [Fintype T]
  [Fintype Q]
  [Fintype P]
  [DecidableEq T]
  [DecidableEq Q]
  [DecidableEq P]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [Fintype T] [Fintype Q] [Fintype P] [DecidableEq T] [DecidableEq Q] [DecidableEq P] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
⚠ [8724/8737] Replayed Research.HyperbolaC4
warning: Research/HyperbolaC4.lean:166:23: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice

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

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

Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false`
⚠ [8725/8737] Replayed Research.RayHyperbola
warning: Research/RayHyperbola.lean:116:19: this tactic is never executed

Note: This linter can be disabled with `set_option linter.unreachableTactic false`
warning: Research/RayHyperbola.lean:116:43: this tactic is never executed

Note: This linter can be disabled with `set_option linter.unreachableTactic false`
warning: Research/RayHyperbola.lean:123:19: this tactic is never executed

Note: This linter can be disabled with `set_option linter.unreachableTactic false`
warning: Research/RayHyperbola.lean:123:43: this tactic is never executed

Note: This linter can be disabled with `set_option linter.unreachableTactic false`
warning: Research/RayHyperbola.lean:116:19: 'exact_mod_cast hXlo' tactic does nothing

Note: This linter can be disabled with `set_option linter.unusedTactic false`
warning: Research/RayHyperbola.lean:116:43: 'exact_mod_cast hYlo' tactic does nothing

Note: This linter can be disabled with `set_option linter.unusedTactic false`
warning: Research/RayHyperbola.lean:123:19: 'exact_mod_cast hXhi' tactic does nothing

Note: This linter can be disabled with `set_option linter.unusedTactic false`
warning: Research/RayHyperbola.lean:123:43: 'exact_mod_cast hYhi' tactic does nothing

Note: This linter can be disabled with `set_option linter.unusedTactic false`
warning: Research/RayHyperbola.lean:255:0: automatically included section variable(s) unused in theorem `Erdos796.tendsto_rayPairMajorants_normalized`:
  [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/RayHyperbola.lean:275:0: automatically included section variable(s) unused in theorem `Erdos796.rayPairLimit_le_square`:
  [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`
ℹ [8726/8737] Replayed Research.RayCutoff
info: Research/RayCutoff.lean:109:4: Try this:
  [apply] ring_nf
  
  The `ring` tactic failed to close the goal. Use `ring_nf` to obtain a normal form.
    
  Note that `ring` works primarily in *commutative* rings. If you have a noncommutative ring, abelian group or module, consider using `noncomm_ring`, `abel` or `module` instead.
⚠ [8727/8737] Replayed Research.PolynomialEnvelope
warning: Research/PolynomialEnvelope.lean:155:0: automatically included section variable(s) unused in theorem `Erdos796.maxSelfCompatibleFiber_spec`:
  [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/PolynomialEnvelope.lean:171:0: automatically included section variable(s) unused in theorem `Erdos796.maxSelfCompatibleFiber_eq_empty`:
  [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`
⚠ [8728/8737] Replayed Research.CanonicalIncidence
warning: Research/CanonicalIncidence.lean:14:0: automatically included section variable(s) unused in theorem `Erdos796.canonicalIncidence_cubeFree`:
  [Fintype T]
  [Fintype Q]
  [Fintype P]
  [DecidableEq T]
  [DecidableEq Q]
  [DecidableEq P]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [Fintype T] [Fintype Q] [Fintype P] [DecidableEq T] [DecidableEq Q] [DecidableEq P] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
warning: Research/CanonicalIncidence.lean:93:5: Variable name `hcompat` 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/CanonicalIncidence.lean:94:5: Variable name `hmem` 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/CanonicalIncidence.lean:96:5: Variable name `hcanonical` 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`
⚠ [8732/8737] Replayed Research.SmoothRankin
warning: Research/SmoothRankin.lean:192:6: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice

Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false`
warning: Research/SmoothRankin.lean:222:10: this tactic is never executed

Note: This linter can be disabled with `set_option linter.unreachableTactic false`
warning: Research/SmoothRankin.lean:222:10: 'ring' tactic does nothing

Note: This linter can be disabled with `set_option linter.unusedTactic false`
⚠ [8733/8737] Replayed Research.CanonicalDyadic
warning: Research/CanonicalDyadic.lean:112:5: Variable name `hqi` 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/CanonicalDyadic.lean:178:17: Variable name `hdTail` 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/CanonicalDyadic.lean:611:56: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice

Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false`
⚠ [8734/8737] Replayed Research.CanonicalDyadicAsymptotic
warning: Research/CanonicalDyadicAsymptotic.lean:24:8: automatically included section variable(s) unused in theorem `Erdos796.mem_rotateThird_iff`:
  [Fintype T]
  [Fintype Q]
  [Fintype P]
  [DecidableEq T]
  [DecidableEq Q]
  [DecidableEq P]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [Fintype T] [Fintype Q] [Fintype P] [DecidableEq T] [DecidableEq Q] [DecidableEq P] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
warning: Research/CanonicalDyadicAsymptotic.lean:38:8: automatically included section variable(s) unused in theorem `Erdos796.rotateThird_card`:
  [Fintype T]
  [Fintype Q]
  [Fintype P]
  [DecidableEq T]
  [DecidableEq Q]
  [DecidableEq P]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [Fintype T] [Fintype Q] [Fintype P] [DecidableEq T] [DecidableEq Q] [DecidableEq P] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
warning: Research/CanonicalDyadicAsymptotic.lean:461:5: Variable name `hA` 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/CanonicalDyadicAsymptotic.lean:606:5: Variable name `hn` 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/CanonicalDyadicAsymptotic.lean:647:27: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice

Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false`
warning: Research/CanonicalDyadicAsymptotic.lean:789:5: Variable name `hn` 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/CanonicalDyadicAsymptotic.lean:823:27: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice

Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false`
warning: Research/CanonicalDyadicAsymptotic.lean:1016:5: Variable name `hn` 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/CanonicalDyadicAsymptotic.lean:1016:18: Variable name `hR` 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/CanonicalDyadicAsymptotic.lean:1016:31: Variable name `hAint` 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/CanonicalDyadicAsymptotic.lean:1048:27: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice

Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false`
warning: Research/CanonicalDyadicAsymptotic.lean:1423:6: this tactic is never executed

Note: This linter can be disabled with `set_option linter.unreachableTactic false`
warning: Research/CanonicalDyadicAsymptotic.lean:1423:6: 'ring' tactic does nothing

Note: This linter can be disabled with `set_option linter.unusedTactic false`
warning: Research/CanonicalDyadicAsymptotic.lean:1634:54: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice

Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false`
warning: Research/CanonicalDyadicAsymptotic.lean:1695:32: This simp argument is unused:
  Finset.sum_const

Hint: Omit it from the simp argument list.
  simp only [if_pos hk,̵ ̵F̵i̵n̵s̵e̵t̵.̵s̵u̵m̵_̵c̵o̵n̵s̵t̵]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Research/CanonicalDyadicAsymptotic.lean:1712:63: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice

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

Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false`
⚠ [8735/8737] Replayed Research.CanonicalTail
warning: Research/CanonicalTail.lean:263:17: This simp argument is unused:
  Prod.fst

Hint: Omit it from the simp argument list.
  simp only [̵P̵r̵o̵d̵.̵f̵s̵t̵,̵ ̵P̵r̵o̵d̵.̵s̵n̵d̵]̵[̲P̲r̲o̲d̲.̲s̲n̲d̲]̲

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Research/CanonicalTail.lean:263:27: This simp argument is unused:
  Prod.snd

Hint: Omit it from the simp argument list.
  simp only [Prod.fst,̵ ̵P̵r̵o̵d̵.̵s̵n̵d̵]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Research/CanonicalTail.lean:310:21: This simp argument is unused:
  canonicalActualRootWeight_nonneg

Hint: Omit it from the simp argument list.
  simp [h,̵ ̵c̵a̵n̵o̵n̵i̵c̵a̵l̵A̵c̵t̵u̵a̵l̵R̵o̵o̵t̵W̵e̵i̵g̵h̵t̵_̵n̵o̵n̵n̵e̵g̵]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Research/CanonicalTail.lean:677:2: 'change
  _ ≤
    (profileTailCount (2 ^ (K + 2)) n : ℝ) + canonicalPersistentSum A n (2 ^ (K + 2)) +
          canonicalLowLinearSum A n (2 ^ (K + 2)) +
        canonicalLowRootSum A n (2 ^ (K + 2)) K +
      canonicalTransientSum A n (2 ^ (K + 2))' tactic does nothing

Note: This linter can be disabled with `set_option linter.unusedTactic false`
info: Research/CanonicalTail.lean:760:55: Try this:
  [apply] ring_nf
  
  The `ring` tactic failed to close the goal. Use `ring_nf` to obtain a normal form.
    
  Note that `ring` works primarily in *commutative* rings. If you have a noncommutative ring, abelian group or module, consider using `noncomm_ring`, `abel` or `module` instead.
warning: Research/CanonicalTail.lean:760:51: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice

Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false`
Build completed successfully (8737 jobs).
PASS: authored sources are placeholder-free and Lean accepts the project
