Building OptimalOTS.Challenge.UpperCompressions ⚠ [2689/2689] Built OptimalOTS.Challenge.UpperCompressions (2.4s) warning: OptimalOTS/Challenge/UpperCompressions.lean:8:18: declaration uses `sorry` warning: OptimalOTS/Challenge/UpperCompressions.lean:12:8: declaration uses `sorry` warning: OptimalOTS/Challenge/UpperCompressions.lean:15:8: declaration uses `sorry` warning: OptimalOTS/Challenge/UpperCompressions.lean:18:8: declaration uses `sorry` Build completed successfully (2689 jobs). Exporting #[OptimalOTS.Challenge.UpperCompressions.admissible, OptimalOTS.Challenge.UpperCompressions.secure, OptimalOTS.Challenge.UpperCompressions.cost, propext, Quot.sound, Classical.choice, Nat.add, Nat.sub, Nat.mul, Nat.pow, Nat.gcd, Nat.div, Nat.mod, Nat.beq, Nat.ble, Nat.land, Nat.lor, Nat.xor, Nat.shiftLeft, Nat.shiftRight, String.ofList, Char.ofNat, List, eagerReduce, OptimalOTS.Challenge.UpperCompressions.scheme] from OptimalOTS.Challenge.UpperCompressions Building Submissions.UpperCompressions.Solution ✔ [8798/8850] Built ToMathlib.MeasureTheory.Measure.IndependentDraws (1.3s) ✔ [8799/8850] Built ToMathlib.MeasureTheory.Measure.Bounds (1.2s) ✔ [8800/8850] Built ToMathlib.Probability.UniformOn (1.3s) ✔ [8801/8850] Built VCVio.OracleComp.QueryTracking.RandomOracle.Simulation (2.0s) ✔ [8802/8850] Built VCVio.EvalDist.Monad.Measure (1.4s) ✔ [8803/8850] Built ToMathlib.MeasureTheory.Measure.UniformTable (1.6s) ✔ [8804/8850] Built Submissions.UpperCompressions.ProofBundle02 (3.4s) ✔ [8805/8850] Built VCVio.OracleComp.Constructions.SampleableType.MeasureCompatibility (1.3s) ✔ [8806/8850] Built VCVio.EvalDist.Monad.UniformTable (1.1s) ✔ [8807/8850] Built VCVio.OracleComp.QueryTracking.RandomOracle.EagerTable (1.4s) ⚠ [8808/8850] Built Submissions.UpperCompressions.ProofBundle00 (9.5s) warning: Submissions/UpperCompressions/ProofBundle00.lean:493:23: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false` warning: Submissions/UpperCompressions/ProofBundle00.lean:644:2: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false` warning: Submissions/UpperCompressions/ProofBundle00.lean:782:8: automatically included section variable(s) unused in theorem `_private.Submissions.UpperCompressions.ProofBundle00.0.WeightedRow.Weights.avg_new`: [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: Submissions/UpperCompressions/ProofBundle00.lean:789:8: automatically included section variable(s) unused in theorem `_private.Submissions.UpperCompressions.ProofBundle00.0.WeightedRow.Weights.avg_old`: [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: Submissions/UpperCompressions/ProofBundle00.lean:799:8: automatically included section variable(s) unused in theorem `_private.Submissions.UpperCompressions.ProofBundle00.0.WeightedRow.Weights.avg_singleton`: [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: Submissions/UpperCompressions/ProofBundle00.lean:829:0: automatically included section variable(s) unused in theorem `WeightedRow.Weights.hazard_change_rejected`: [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: Submissions/UpperCompressions/ProofBundle00.lean:884:0: automatically included section variable(s) unused in theorem `WeightedRow.Weights.rejection_nonneg`: [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: Submissions/UpperCompressions/ProofBundle00.lean:886:0: automatically included section variable(s) unused in theorem `WeightedRow.Weights.expect_one`: [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: Submissions/UpperCompressions/ProofBundle00.lean:890:0: automatically included section variable(s) unused in theorem `WeightedRow.Weights.unseenMean_nonneg`: [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: Submissions/UpperCompressions/ProofBundle00.lean:898:0: automatically included section variable(s) unused in theorem `WeightedRow.Weights.unseenMean_le_mean`: [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: Submissions/UpperCompressions/ProofBundle00.lean:906:0: automatically included section variable(s) unused in theorem `WeightedRow.Weights.singleton_le_score`: [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: Submissions/UpperCompressions/ProofBundle00.lean:988:8: automatically included section variable(s) unused in theorem `_private.Submissions.UpperCompressions.ProofBundle00.0.WeightedRow.Weights.row_ratio_bounds`: [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: Submissions/UpperCompressions/ProofBundle00.lean:989:13: Variable name `hL` is not explicitly referenced. Hint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning: [apply] _hL Note: This linter can be disabled with `set_option linter.unusedVariables false` warning: Submissions/UpperCompressions/ProofBundle00.lean:1070:0: automatically included section variable(s) unused in theorem `WeightedRow.Weights.expect_const`: [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: Submissions/UpperCompressions/ProofBundle00.lean:1074:0: automatically included section variable(s) unused in theorem `WeightedRow.Weights.expect_add`: [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: Submissions/UpperCompressions/ProofBundle00.lean:1079:0: automatically included section variable(s) unused in theorem `WeightedRow.Weights.expect_sub`: [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: Submissions/UpperCompressions/ProofBundle00.lean:1084:0: automatically included section variable(s) unused in theorem `WeightedRow.Weights.expect_smul`: [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: Submissions/UpperCompressions/ProofBundle00.lean:1214:8: automatically included section variable(s) unused in theorem `WeightedRow.Weights.mean_scoreJump`: [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: Submissions/UpperCompressions/ProofBundle00.lean:1217:8: automatically included section variable(s) unused in theorem `WeightedRow.Weights.mean_pairJump`: [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: Submissions/UpperCompressions/ProofBundle00.lean:1223:0: automatically included section variable(s) unused in theorem `WeightedRow.Weights.scoreJump_bounds`: [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: Submissions/UpperCompressions/ProofBundle00.lean:1326:8: automatically included section variable(s) unused in theorem `WeightedRow.Weights.step_not_fresh`: [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: Submissions/UpperCompressions/ProofBundle00.lean:1361:0: automatically included section variable(s) unused in theorem `WeightedPublicCounts.counts_insert_apply`: [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: Submissions/UpperCompressions/ProofBundle00.lean:1380:56: This simp argument is unused: Function.update_of_ne hij Hint: Omit it from the simp argument list. [apply] simp [counts_insert_apply, hq, he, advance, bump, hij, Ne.symm hij] Note: This linter can be disabled with `set_option linter.unusedSimpArgs false` warning: Submissions/UpperCompressions/ProofBundle00.lean:1382:0: automatically included section variable(s) unused in theorem `WeightedPublicCounts.counts_update_absent`: [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: Submissions/UpperCompressions/ProofBundle00.lean:1417:0: automatically included section variable(s) unused in theorem `WeightedCacheCounts.not_seen_of_none`: [DecidableEq D] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [DecidableEq D] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false` warning: Submissions/UpperCompressions/ProofBundle00.lean:1425:20: This simp argument is unused: Function.update_of_ne ht Hint: Omit it from the simp argument list. [apply] simp [seen, ht] Note: This linter can be disabled with `set_option linter.unusedSimpArgs false` warning: Submissions/UpperCompressions/ProofBundle00.lean:1432:20: This simp argument is unused: Function.update_of_ne ht Hint: Omit it from the simp argument list. [apply] simp [seen, ht] Note: This linter can be disabled with `set_option linter.unusedSimpArgs false` warning: Submissions/UpperCompressions/ProofBundle00.lean:1434:0: automatically included section variable(s) unused in theorem `WeightedCacheCounts.decoded_update`: [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: Submissions/UpperCompressions/ProofBundle00.lean:1467:0: automatically included section variable(s) unused in theorem `WeightedCacheCounts.seen_card_le`: [DecidableEq D] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [DecidableEq D] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false` ⚠ [8809/8850] Built Submissions.UpperCompressions.EqualityCollision91 (4.8s) warning: Submissions/UpperCompressions/EqualityCollision91.lean:26:0: automatically included section variable(s) unused in theorem `WeightedRow.Weights.collisionMass_eq`: [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: Submissions/UpperCompressions/EqualityCollision91.lean:30:6: this tactic is never executed Note: This linter can be disabled with `set_option linter.unreachableTactic false` warning: Submissions/UpperCompressions/EqualityCollision91.lean:30:6: Unused tactic linter: `ring` does nothing Note: This linter can be disabled with `set_option linter.unusedTactic false` warning: Submissions/UpperCompressions/EqualityCollision91.lean:32:0: automatically included section variable(s) unused in theorem `WeightedRow.Weights.collisionMass_nonneg`: [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: Submissions/UpperCompressions/EqualityCollision91.lean:86:0: automatically included section variable(s) unused in theorem `WeightedRow.Weights.Qrev_eq_D_add_X`: [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: Submissions/UpperCompressions/EqualityCollision91.lean:105:0: automatically included section variable(s) unused in theorem `WeightedRow.Weights.expect_xJump`: [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: Submissions/UpperCompressions/EqualityCollision91.lean:113:6: this tactic is never executed Note: This linter can be disabled with `set_option linter.unreachableTactic false` warning: Submissions/UpperCompressions/EqualityCollision91.lean:113:6: Unused tactic linter: `ring` does nothing Note: This linter can be disabled with `set_option linter.unusedTactic false` warning: Submissions/UpperCompressions/EqualityCollision91.lean:115:0: automatically included section variable(s) unused in theorem `WeightedRow.Weights.rowSquareScore_le_total`: [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: Submissions/UpperCompressions/EqualityCollision91.lean:169:0: automatically included section variable(s) unused in theorem `WeightedRow.Weights.expect_freshPiece_sq_le`: [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: Submissions/UpperCompressions/EqualityCollision91.lean:184:26: This simp argument is unused: mul_zero Hint: Omit it from the simp argument list. [apply] simp only [if_neg h0, zero_pow] Note: This linter can be disabled with `set_option linter.unusedSimpArgs false` warning: Submissions/UpperCompressions/EqualityCollision91.lean:184:36: This simp argument is unused: zero_pow Hint: Omit it from the simp argument list. [apply] simp only [if_neg h0, mul_zero] Note: This linter can be disabled with `set_option linter.unusedSimpArgs false` warning: Submissions/UpperCompressions/EqualityCollision91.lean:187:0: automatically included section variable(s) unused in theorem `WeightedRow.Weights.expect_forwardPiece_sq`: [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: Submissions/UpperCompressions/EqualityCollision91.lean:197:8: this tactic is never executed Note: This linter can be disabled with `set_option linter.unreachableTactic false` warning: Submissions/UpperCompressions/EqualityCollision91.lean:197:8: Unused tactic linter: `ring` does nothing Note: This linter can be disabled with `set_option linter.unusedTactic false` warning: Submissions/UpperCompressions/EqualityCollision91.lean:199:0: automatically included section variable(s) unused in theorem `WeightedRow.Weights.expect_reversePiece_sq_le`: [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: Submissions/UpperCompressions/EqualityCollision91.lean:209:26: This simp argument is unused: zero_pow Hint: Omit it from the simp argument list. [apply] simp only [if_neg h1, mul_zero] Note: This linter can be disabled with `set_option linter.unusedSimpArgs false` warning: Submissions/UpperCompressions/EqualityCollision91.lean:209:36: This simp argument is unused: mul_zero Hint: Omit it from the simp argument list. [apply] simp only [if_neg h1, zero_pow] Note: This linter can be disabled with `set_option linter.unusedSimpArgs false` warning: Submissions/UpperCompressions/EqualityCollision91.lean:239:10: this tactic is never executed Note: This linter can be disabled with `set_option linter.unreachableTactic false` warning: Submissions/UpperCompressions/EqualityCollision91.lean:248:10: this tactic is never executed Note: This linter can be disabled with `set_option linter.unreachableTactic false` warning: Submissions/UpperCompressions/EqualityCollision91.lean:239:10: Unused tactic linter: `ring` does nothing Note: This linter can be disabled with `set_option linter.unusedTactic false` warning: Submissions/UpperCompressions/EqualityCollision91.lean:248:10: Unused tactic linter: `ring` does nothing Note: This linter can be disabled with `set_option linter.unusedTactic false` warning: Submissions/UpperCompressions/EqualityCollision91.lean:263:0: automatically included section variable(s) unused in theorem `WeightedRow.Weights.positiveInside_eq_pieces`: [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: Submissions/UpperCompressions/EqualityCollision91.lean:273:74: This simp argument is unused: h1 Hint: Omit it from the simp argument list. [apply] simp [positiveInside, freshPiece, forwardPiece, reversePiece, h0] Note: This linter can be disabled with `set_option linter.unusedSimpArgs false` warning: Submissions/UpperCompressions/EqualityCollision91.lean:275:72: This simp argument is unused: h0 Hint: Omit it from the simp argument list. [apply] simp [positiveInside, freshPiece, forwardPiece, reversePiece, h1] Note: This linter can be disabled with `set_option linter.unusedSimpArgs false` warning: Submissions/UpperCompressions/EqualityCollision91.lean:300:0: automatically included section variable(s) unused in theorem `WeightedRow.Weights.positiveOutside_eq_pieces`: [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: Submissions/UpperCompressions/EqualityCollision91.lean:309:61: This simp argument is unused: h1 Hint: Omit it from the simp argument list. [apply] simp [positiveOutside, freshPiece, reversePiece, h0] Note: This linter can be disabled with `set_option linter.unusedSimpArgs false` warning: Submissions/UpperCompressions/EqualityCollision91.lean:311:59: This simp argument is unused: h0 Hint: Omit it from the simp argument list. [apply] simp [positiveOutside, freshPiece, reversePiece, h1] Note: This linter can be disabled with `set_option linter.unusedSimpArgs false` warning: Submissions/UpperCompressions/EqualityCollision91.lean:337:12: this tactic is never executed Note: This linter can be disabled with `set_option linter.unreachableTactic false` warning: Submissions/UpperCompressions/EqualityCollision91.lean:337:12: Unused tactic linter: `ring` does nothing Note: This linter can be disabled with `set_option linter.unusedTactic false` ⚠ [8810/8850] Built Submissions.UpperCompressions.ProofBundle01 (4.0s) warning: Submissions/UpperCompressions/ProofBundle01.lean:150:8: automatically included section variable(s) unused in theorem `WeightedRow.Weights.withScore_classMass`: [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: Submissions/UpperCompressions/ProofBundle01.lean:177:0: automatically included section variable(s) unused in theorem `WeightedCacheEvidence.mem`: [DecidableEq Q] [Fintype I] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [DecidableEq Q] [Fintype I] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false` warning: Submissions/UpperCompressions/ProofBundle01.lean:235:2: try 'simp' instead of 'simpa' Note: This linter can be disabled with `set_option linter.unnecessarySimpa false` warning: Submissions/UpperCompressions/ProofBundle01.lean:359:6: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false` warning: Submissions/UpperCompressions/ProofBundle01.lean:408:0: automatically included section variable(s) unused in theorem `WeightedRow.Weights.seen_nonneg`: [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: Submissions/UpperCompressions/ProofBundle01.lean:412:0: automatically included section variable(s) unused in theorem `WeightedRow.Weights.seen_le_score`: [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: Submissions/UpperCompressions/ProofBundle01.lean:422:0: automatically included section variable(s) unused in theorem `WeightedRow.Weights.bad_le_twice_pairScore`: [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` ✔ [8811/8850] Built Submissions.UpperCompressions.ProofBundle03 (5.3s) ⚠ [8812/8850] Built Submissions.UpperCompressions.ProofBundle04 (4.9s) warning: Submissions/UpperCompressions/ProofBundle04.lean:265:10: This simp argument is unused: Function.comp_def Hint: Omit it from the simp argument list. [apply] simp [(hc v).mpr rfl, strictRank] Note: This linter can be disabled with `set_option linter.unusedSimpArgs false` warning: Submissions/UpperCompressions/ProofBundle04.lean:281:10: This simp argument is unused: ha Hint: Omit it from the simp argument list. [apply] simp [hav] Note: This linter can be disabled with `set_option linter.unusedSimpArgs false` warning: Submissions/UpperCompressions/ProofBundle04.lean:362:28: This simp argument is unused: E_pure Hint: Omit it from the simp argument list. [apply] simp [drawList, iidMean] Note: This linter can be disabled with `set_option linter.unusedSimpArgs false` warning: Submissions/UpperCompressions/ProofBundle04.lean:402:24: This simp argument is unused: Function.comp_apply Hint: Omit it from the simp argument list. [apply] simp only [candidate, apply_ite, ENNReal.ofReal_one, ENNReal.ofReal_zero] at he ⊢ Note: This linter can be disabled with `set_option linter.unusedSimpArgs false` warning: Submissions/UpperCompressions/ProofBundle04.lean:637:50: This simp argument is unused: E_pure Hint: Omit it from the simp argument list. [apply] simp [publicHit, hybridPrefix_pure] Note: This linter can be disabled with `set_option linter.unusedSimpArgs false` warning: Submissions/UpperCompressions/ProofBundle04.lean:650:14: This simp argument is unused: E_pure Hint: Omit it from the simp argument list. [apply] simp Note: This linter can be disabled with `set_option linter.unusedSimpArgs false` ⚠ [8813/8850] Built Submissions.UpperCompressions.ProofBundle05 (3.0s) warning: Submissions/UpperCompressions/ProofBundle05.lean:42:30: This simp argument is unused: E_pure Hint: Omit it from the simp argument list. [apply] simp [run_pure] Note: This linter can be disabled with `set_option linter.unusedSimpArgs false` ⚠ [8814/8850] Built Submissions.UpperCompressions.ProofBundle06 (4.5s) warning: Submissions/UpperCompressions/ProofBundle06.lean:22:30: This simp argument is unused: E_pure Hint: Omit it from the simp argument list. [apply] simp [run_pure] Note: This linter can be disabled with `set_option linter.unusedSimpArgs false` warning: Submissions/UpperCompressions/ProofBundle06.lean:108:30: This simp argument is unused: E_pure Hint: Omit it from the simp argument list. [apply] simp [run_pure] Note: This linter can be disabled with `set_option linter.unusedSimpArgs false` warning: Submissions/UpperCompressions/ProofBundle06.lean:702:42: This simp argument is unused: Ne.symm hq Hint: Omit it from the simp argument list. [apply] simp [overwrite, Function.update, hq, hη, Ne.symm hη, hc] Note: This linter can be disabled with `set_option linter.unusedSimpArgs false` warning: Submissions/UpperCompressions/ProofBundle06.lean:702:58: This simp argument is unused: Ne.symm hη Hint: Omit it from the simp argument list. [apply] simp [overwrite, Function.update, hq, Ne.symm hq, hη, hc] Note: This linter can be disabled with `set_option linter.unusedSimpArgs false` warning: Submissions/UpperCompressions/ProofBundle06.lean:762:10: This simp argument is unused: Function.comp_def Hint: Omit it from the simp argument list. [apply] simp [hret] Note: This linter can be disabled with `set_option linter.unusedSimpArgs false` warning: Submissions/UpperCompressions/ProofBundle06.lean:816:27: Unused tactic linter: `congr 1` does nothing Note: This linter can be disabled with `set_option linter.unusedTactic false` warning: Submissions/UpperCompressions/ProofBundle06.lean:816:39: Unused tactic linter: `(try funext r)` does nothing Note: This linter can be disabled with `set_option linter.unusedTactic false` warning: Submissions/UpperCompressions/ProofBundle06.lean:816:58: Unused tactic linter: `split_ifs` does nothing Note: This linter can be disabled with `set_option linter.unusedTactic false` warning: Submissions/UpperCompressions/ProofBundle06.lean:816:72: Unused tactic linter: `rfl` does nothing Note: This linter can be disabled with `set_option linter.unusedTactic false` warning: Submissions/UpperCompressions/ProofBundle06.lean:829:27: Unused tactic linter: `congr 1` does nothing Note: This linter can be disabled with `set_option linter.unusedTactic false` warning: Submissions/UpperCompressions/ProofBundle06.lean:829:39: Unused tactic linter: `(try funext r)` does nothing Note: This linter can be disabled with `set_option linter.unusedTactic false` warning: Submissions/UpperCompressions/ProofBundle06.lean:829:58: Unused tactic linter: `split_ifs` does nothing Note: This linter can be disabled with `set_option linter.unusedTactic false` warning: Submissions/UpperCompressions/ProofBundle06.lean:829:72: Unused tactic linter: `rfl` does nothing Note: This linter can be disabled with `set_option linter.unusedTactic false` warning: Submissions/UpperCompressions/ProofBundle06.lean:816:27: this tactic is never executed Note: This linter can be disabled with `set_option linter.unreachableTactic false` warning: Submissions/UpperCompressions/ProofBundle06.lean:816:39: this tactic is never executed Note: This linter can be disabled with `set_option linter.unreachableTactic false` warning: Submissions/UpperCompressions/ProofBundle06.lean:816:58: this tactic is never executed Note: This linter can be disabled with `set_option linter.unreachableTactic false` warning: Submissions/UpperCompressions/ProofBundle06.lean:816:72: this tactic is never executed Note: This linter can be disabled with `set_option linter.unreachableTactic false` warning: Submissions/UpperCompressions/ProofBundle06.lean:829:27: this tactic is never executed Note: This linter can be disabled with `set_option linter.unreachableTactic false` warning: Submissions/UpperCompressions/ProofBundle06.lean:829:39: this tactic is never executed Note: This linter can be disabled with `set_option linter.unreachableTactic false` warning: Submissions/UpperCompressions/ProofBundle06.lean:829:58: this tactic is never executed Note: This linter can be disabled with `set_option linter.unreachableTactic false` warning: Submissions/UpperCompressions/ProofBundle06.lean:829:72: this tactic is never executed Note: This linter can be disabled with `set_option linter.unreachableTactic false` ⚠ [8815/8850] Built Submissions.UpperCompressions.ProofBundle07 (4.4s) warning: Submissions/UpperCompressions/ProofBundle07.lean:308:44: This simp argument is unused: Ne.symm hr Hint: Omit it from the simp argument list. [apply] simp [overwrite, Function.update, hr] Note: This linter can be disabled with `set_option linter.unusedSimpArgs false` warning: Submissions/UpperCompressions/ProofBundle07.lean:312:20: This simp argument is unused: hrd Hint: Omit it from the simp argument list. [apply] simp Note: This linter can be disabled with `set_option linter.unusedSimpArgs false` warning: Submissions/UpperCompressions/ProofBundle07.lean:318:12: This simp argument is unused: hrd Hint: Omit it from the simp argument list. [apply] simp [Function.update, hdd, Ne.symm hdd] Note: This linter can be disabled with `set_option linter.unusedSimpArgs false` warning: Submissions/UpperCompressions/ProofBundle07.lean:318:39: This simp argument is unused: Ne.symm hdd Hint: Omit it from the simp argument list. [apply] simp [hrd, Function.update, hdd] Note: This linter can be disabled with `set_option linter.unusedSimpArgs false` warning: Submissions/UpperCompressions/ProofBundle07.lean:733:27: This simp argument is unused: eq_comm Hint: Omit it from the simp argument list. [apply] simp [score] Note: This linter can be disabled with `set_option linter.unusedSimpArgs false` warning: Submissions/UpperCompressions/ProofBundle07.lean:735:0: automatically included section variable(s) unused in theorem `WeightedCompletion.mean_sum`: [Nonempty Ω] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [Nonempty Ω] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false` warning: Submissions/UpperCompressions/ProofBundle07.lean:740:0: automatically included section variable(s) unused in theorem `WeightedCompletion.mean_mul`: [Nonempty Ω] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [Nonempty Ω] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false` warning: Submissions/UpperCompressions/ProofBundle07.lean:762:0: automatically included section variable(s) unused in theorem `WeightedCompletion.known_score`: [Fintype D] [Nonempty D] [DecidableEq D] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [Fintype D] [Nonempty D] [DecidableEq D] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false` warning: Submissions/UpperCompressions/ProofBundle07.lean:846:0: automatically included section variable(s) unused in theorem `WeightedCompletion.referencePayoff_nonneg`: [Fintype Ω] [Nonempty Ω] [Nonempty D] [Fintype I] [DecidableEq I] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [Fintype Ω] [Nonempty Ω] [Nonempty D] [Fintype I] [DecidableEq I] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false` warning: Submissions/UpperCompressions/ProofBundle07.lean:854:25: This simp argument is unused: ht Hint: Omit it from the simp argument list. [apply] simp [score] Note: This linter can be disabled with `set_option linter.unusedSimpArgs false` warning: Submissions/UpperCompressions/ProofBundle07.lean:856:22: This simp argument is unused: ht Hint: Omit it from the simp argument list. [apply] simp only [score, Option.map_some, Option.getD_some] Note: This linter can be disabled with `set_option linter.unusedSimpArgs false` warning: Submissions/UpperCompressions/ProofBundle07.lean:906:23: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false` warning: Submissions/UpperCompressions/ProofBundle07.lean:964:0: automatically included section variable(s) unused in theorem `WeightedCompletion.selected_consistent`: [Fintype D] [Nonempty D] [DecidableEq D] [DecidableEq I] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [Fintype D] [Nonempty D] [DecidableEq D] [DecidableEq I] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false` warning: Submissions/UpperCompressions/ProofBundle07.lean:986:28: This simp argument is unused: score Hint: Omit it from the simp argument list. [apply] simp [hs] Note: This linter can be disabled with `set_option linter.unusedSimpArgs false` warning: Submissions/UpperCompressions/ProofBundle07.lean:986:35: This simp argument is unused: hs Hint: Omit it from the simp argument list. [apply] simp [score] Note: This linter can be disabled with `set_option linter.unusedSimpArgs false` warning: Submissions/UpperCompressions/ProofBundle07.lean:991:23: This simp argument is unused: hs Hint: Omit it from the simp argument list. [apply] simp [score, ht] Note: This linter can be disabled with `set_option linter.unusedSimpArgs false` warning: Submissions/UpperCompressions/ProofBundle07.lean:997:21: This simp argument is unused: hs Hint: Omit it from the simp argument list. [apply] simp [score, hn, Ne.symm hba] Note: This linter can be disabled with `set_option linter.unusedSimpArgs false` warning: Submissions/UpperCompressions/ProofBundle07.lean:997:25: This simp argument is unused: hn Hint: Omit it from the simp argument list. [apply] simp [score, hs, Ne.symm hba] Note: This linter can be disabled with `set_option linter.unusedSimpArgs false` warning: Submissions/UpperCompressions/ProofBundle07.lean:1000:0: automatically included section variable(s) unused in theorem `WeightedCompletion.iidMean_sum`: [DecidableEq D] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [DecidableEq D] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false` warning: Submissions/UpperCompressions/ProofBundle07.lean:1010:0: automatically included section variable(s) unused in theorem `WeightedCompletion.iidMean_mul_const`: [Nonempty D] [DecidableEq D] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [Nonempty D] [DecidableEq D] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false` warning: Submissions/UpperCompressions/ProofBundle07.lean:1020:0: automatically included section variable(s) unused in theorem `WeightedCompletion.iidMean_const`: [DecidableEq D] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [DecidableEq D] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false` warning: Submissions/UpperCompressions/ProofBundle07.lean:1027:0: automatically included section variable(s) unused in theorem `WeightedCompletion.iidMean_mono`: [Nonempty D] [DecidableEq D] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [Nonempty D] [DecidableEq D] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false` warning: Submissions/UpperCompressions/ProofBundle07.lean:1053:25: This simp argument is unused: ht Hint: Omit it from the simp argument list. [apply] simp [score, iidMean_const] Note: This linter can be disabled with `set_option linter.unusedSimpArgs false` warning: Submissions/UpperCompressions/ProofBundle07.lean:1055:22: This simp argument is unused: ht Hint: Omit it from the simp argument list. [apply] simp only [score, Option.map_some, Option.getD_some] Note: This linter can be disabled with `set_option linter.unusedSimpArgs false` ⚠ [8816/8850] Built Submissions.UpperCompressions.CompactSchedule91 (25s) warning: Submissions/UpperCompressions/CompactSchedule91.lean:982:46: Variable name `hx` is not explicitly referenced. Hint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning: [apply] _hx Note: This linter can be disabled with `set_option linter.unusedVariables false` ⚠ [8817/8850] Built Submissions.UpperCompressions.ProofBundle08 (3.3s) warning: Submissions/UpperCompressions/ProofBundle08.lean:52:0: automatically included section variable(s) unused in theorem `WeightedCompletion.tableKernel_reference_le`: [Fintype Ω] [Nonempty Ω] [Nonempty D] [Fintype I] [DecidableEq I] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [Fintype Ω] [Nonempty Ω] [Nonempty D] [Fintype I] [DecidableEq I] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false` warning: Submissions/UpperCompressions/ProofBundle08.lean:65:25: This simp argument is unused: ht Hint: Omit it from the simp argument list. [apply] simp [score] Note: This linter can be disabled with `set_option linter.unusedSimpArgs false` warning: Submissions/UpperCompressions/ProofBundle08.lean:67:22: This simp argument is unused: ht Hint: Omit it from the simp argument list. [apply] simp only [score, Option.map_some, Option.getD_some] Note: This linter can be disabled with `set_option linter.unusedSimpArgs false` warning: Submissions/UpperCompressions/ProofBundle08.lean:149:0: automatically included section variable(s) unused in theorem `WeightedCompletion.uniformMean_indicator`: [Nonempty W] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [Nonempty W] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false` ✔ [8818/8850] Built Submissions.UpperCompressions.LongChain91Codec (3.0s) ⚠ [8819/8850] Built Submissions.UpperCompressions.ProofBundle09 (4.1s) warning: Submissions/UpperCompressions/ProofBundle09.lean:454:0: automatically included section variable(s) unused in theorem `WeightedDirectCache.hash_count_le_one`: [Fintype B] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [Fintype B] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false` warning: Submissions/UpperCompressions/ProofBundle09.lean:650:0: automatically included section variable(s) unused in theorem `WeightedOracleExecution.state_bound_of_query_budget`: [spec.Inhabited] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [spec.Inhabited] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false` warning: Submissions/UpperCompressions/ProofBundle09.lean:698:8: automatically included section variable(s) unused in theorem `WeightedOracleExecution.firstHitRun_pure`: [spec.Inhabited] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [spec.Inhabited] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false` warning: Submissions/UpperCompressions/ProofBundle09.lean:704:8: automatically included section variable(s) unused in theorem `WeightedOracleExecution.firstHitRun_query_bind`: [spec.Inhabited] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [spec.Inhabited] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false` warning: Submissions/UpperCompressions/ProofBundle09.lean:754:19: This simp argument is unused: classify_clock Hint: Omit it from the simp argument list. [apply] simp only [classify_value, bind_assoc, pure_bind] Note: This linter can be disabled with `set_option linter.unusedSimpArgs false` warning: Submissions/UpperCompressions/ProofBundle09.lean:754:35: This simp argument is unused: classify_value Hint: Omit it from the simp argument list. [apply] simp only [classify_clock, bind_assoc, pure_bind] Note: This linter can be disabled with `set_option linter.unusedSimpArgs false` ⚠ [8820/8850] Built Submissions.UpperCompressions.ProofBundle10 (4.4s) warning: Submissions/UpperCompressions/ProofBundle10.lean:73:38: This simp argument is unused: zero_pow Hint: Omit it from the simp argument list. [apply] simp only [Nat.cast_zero, mul_zero, sub_zero] at hcomp Note: This linter can be disabled with `set_option linter.unusedSimpArgs false` warning: Submissions/UpperCompressions/ProofBundle10.lean:254:4: Unused tactic linter: `change G * w.mean * (qCount s : ℝ) ≤ G ^ 2 * N` does nothing Note: This linter can be disabled with `set_option linter.unusedTactic false` warning: Submissions/UpperCompressions/ProofBundle10.lean:442:0: automatically included section variable(s) unused in theorem `WeightedCacheCounts.classCounts_mono`: [DecidableEq D] [Fintype ι] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [DecidableEq D] [Fintype ι] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false` warning: Submissions/UpperCompressions/ProofBundle10.lean:573:6: try 'simp' instead of 'simpa' Note: This linter can be disabled with `set_option linter.unnecessarySimpa false` warning: Submissions/UpperCompressions/ProofBundle10.lean:596:0: automatically included section variable(s) unused in theorem `WeightedCacheCounts.seen_image`: [DecidableEq D] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [DecidableEq D] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false` warning: Submissions/UpperCompressions/ProofBundle10.lean:610:0: automatically included section variable(s) unused in theorem `WeightedCacheCounts.counts_image`: [Fintype I] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [Fintype I] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false` ✔ [8821/8850] Built Submissions.UpperCompressions.LongChain91SecurityData (7.3s) ⚠ [8822/8850] Built Submissions.UpperCompressions.ProofBundle11 (2.0s) warning: Submissions/UpperCompressions/ProofBundle11.lean:98:4: Try this: haveI̵ The goal is a proposition, so `have` is preferred over `haveI`. The difference between `have` and `haveI` is that `haveI` inlines the value. But this is not relevant for proofs because of proof irrelevance. Note: This linter can be disabled with `set_option linter.style.haveILetI false` ⚠ [8823/8850] Built Submissions.UpperCompressions.ProofBundle12 (3.6s) warning: Submissions/UpperCompressions/ProofBundle12.lean:41:0: automatically included section variable(s) unused in theorem `WeightedDualCache.after_comp`: [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: Submissions/UpperCompressions/ProofBundle12.lean:163:0: automatically included section variable(s) unused in theorem `WeightedDualCache.phase_steps`: [SampleableType B] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [SampleableType B] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false` ✔ [8824/8850] Built Submissions.UpperCompressions.ProofBundle13 (3.2s) ⚠ [8825/8850] Built Submissions.UpperCompressions.LongChain91Empirical (20s) warning: Submissions/UpperCompressions/LongChain91Empirical.lean:55:18: This simp argument is unused: h Hint: Omit it from the simp argument list. [apply] simp Note: This linter can be disabled with `set_option linter.unusedSimpArgs false` warning: Submissions/UpperCompressions/LongChain91Empirical.lean:56:20: This simp argument is unused: h Hint: Omit it from the simp argument list. [apply] simp Note: This linter can be disabled with `set_option linter.unusedSimpArgs false` warning: Submissions/UpperCompressions/LongChain91Empirical.lean:98:52: This simp argument is unused: hx Hint: Omit it from the simp argument list. [apply] simp [prefixLt, hr, WeightedCompletion.score] Note: This linter can be disabled with `set_option linter.unusedSimpArgs false` warning: Submissions/UpperCompressions/LongChain91Empirical.lean:112:52: This simp argument is unused: hx Hint: Omit it from the simp argument list. [apply] simp [prefixLe, hr, WeightedCompletion.score] Note: This linter can be disabled with `set_option linter.unusedSimpArgs false` warning: Submissions/UpperCompressions/LongChain91Empirical.lean:176:48: This simp argument is unused: Nat.lt_succ_iff Hint: Omit it from the simp argument list. [apply] simp Note: This linter can be disabled with `set_option linter.unusedSimpArgs false` ✔ [8826/8850] Built Submissions.UpperCompressions.LongChain91Occupancy (3.6s) ⚠ [8827/8850] Built Submissions.UpperCompressions.LongChain91CollisionCap (4.9s) warning: Submissions/UpperCompressions/LongChain91CollisionCap.lean:56:24: This simp argument is unused: ha Hint: Omit it from the simp argument list. [apply] simp Note: This linter can be disabled with `set_option linter.unusedSimpArgs false` warning: Submissions/UpperCompressions/LongChain91CollisionCap.lean:57:26: This simp argument is unused: ha Hint: Omit it from the simp argument list. [apply] simp Note: This linter can be disabled with `set_option linter.unusedSimpArgs false` warning: Submissions/UpperCompressions/LongChain91CollisionCap.lean:148:17: This simp argument is unused: hs Hint: Omit it from the simp argument list. [apply] simp only [after, expect_const] Note: This linter can be disabled with `set_option linter.unusedSimpArgs false` warning: Submissions/UpperCompressions/LongChain91CollisionCap.lean:151:17: This simp argument is unused: hs Hint: Omit it from the simp argument list. [apply] simp only [after, expect_const] Note: This linter can be disabled with `set_option linter.unusedSimpArgs false` warning: Submissions/UpperCompressions/LongChain91CollisionCap.lean:154:17: This simp argument is unused: hs Hint: Omit it from the simp argument list. [apply] simp only [after] Note: This linter can be disabled with `set_option linter.unusedSimpArgs false` warning: Submissions/UpperCompressions/LongChain91CollisionCap.lean:306:8: this tactic is never executed Note: This linter can be disabled with `set_option linter.unreachableTactic false` warning: Submissions/UpperCompressions/LongChain91CollisionCap.lean:306:8: Unused tactic linter: `ring` does nothing Note: This linter can be disabled with `set_option linter.unusedTactic false` ⚠ [8828/8850] Built Submissions.UpperCompressions.LongChain91Geometry (77s) warning: Submissions/UpperCompressions/LongChain91Geometry.lean:911:34: This simp argument is unused: stVal_cons Hint: Omit it from the simp argument list. [apply] simp only [h, ↓reduceIte, Bool.false_eq_true] Note: This linter can be disabled with `set_option linter.unusedSimpArgs false` ✔ [8829/8850] Built Submissions.UpperCompressions.LongChain91CutBridge (4.3s) ✔ [8830/8850] Built Submissions.UpperCompressions.LongChain91Scheme (4.3s) ✔ [8831/8850] Built Submissions.UpperCompressions.LongChain91SecurityClosure (3.3s) ⚠ [8832/8850] Built Submissions.UpperCompressions.LongChain91Auth (4.5s) warning: Submissions/UpperCompressions/LongChain91Auth.lean:1035:38: Variable name `ξ` is not explicitly referenced. Hint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning: [apply] _ξ Note: This linter can be disabled with `set_option linter.unusedVariables false` ⚠ [8833/8850] Built Submissions.UpperCompressions.LongChain91CachedRow (4.9s) warning: Submissions/UpperCompressions/LongChain91CachedRow.lean:105:25: This simp argument is unused: hs Hint: Omit it from the simp argument list. [apply] simp [score] Note: This linter can be disabled with `set_option linter.unusedSimpArgs false` ✔ [8834/8850] Built Submissions.UpperCompressions.LongChain91BudgetArithmetic (2.9s) ✔ [8835/8850] Built Submissions.UpperCompressions.LongChain91AuthGame (4.9s) ✔ [8836/8850] Built Submissions.UpperCompressions.LongChain91Continuation (3.1s) ✔ [8837/8850] Built Submissions.UpperCompressions.LongChain91SmallMoments (3.4s) ✔ [8838/8850] Built Submissions.UpperCompressions.LongChain91TailArithmetic (3.5s) ⚠ [8839/8850] Built Submissions.UpperCompressions.LongChain91AuthActual (3.8s) warning: Submissions/UpperCompressions/LongChain91AuthActual.lean:119:9: Variable name `xi` is not explicitly referenced. Hint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning: [apply] _xi Note: This linter can be disabled with `set_option linter.unusedVariables false` ✔ [8840/8850] Built Submissions.UpperCompressions.LongChain91CollisionArithmetic (3.5s) ⚠ [8841/8850] Built Submissions.UpperCompressions.LongChain91AuthConditional (4.1s) warning: Submissions/UpperCompressions/LongChain91AuthConditional.lean:870:32: This simp argument is unused: Finset.sum_add_distrib Hint: Omit it from the simp argument list. [apply] simp only [Finset.mul_sum] Note: This linter can be disabled with `set_option linter.unusedSimpArgs false` ✔ [8842/8850] Built Submissions.UpperCompressions.LongChain91DiagonalClock (3.2s) ⚠ [8843/8850] Built Submissions.UpperCompressions.LongChain91LargeHazard (3.7s) warning: Submissions/UpperCompressions/LongChain91LargeHazard.lean:264:47: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false` warning: Submissions/UpperCompressions/LongChain91LargeHazard.lean:467:17: This simp argument is unused: hs Hint: Omit it from the simp argument list. [apply] simp only [gain, securityWeights.expect_const, globalStep, Nat.cast_zero, mul_zero] Note: This linter can be disabled with `set_option linter.unusedSimpArgs false` warning: Submissions/UpperCompressions/LongChain91LargeHazard.lean:464:8: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false` warning: Submissions/UpperCompressions/LongChain91LargeHazard.lean:666:21: This simp argument is unused: hrow' Hint: Omit it from the simp argument list. [apply] simp [Z, hazard, WeightedRow.Weights.hazard, WeightedRow.Weights.seen, WeightedRow.Weights.bad, hq', hk', hr'] Note: This linter can be disabled with `set_option linter.unusedSimpArgs false` ⚠ [8844/8850] Built Submissions.UpperCompressions.LongChain91InitialGame (5.1s) warning: Submissions/UpperCompressions/LongChain91InitialGame.lean:233:2: Try this: letI̵ The goal is a proposition, so `let` is preferred over `letI`. The difference between `let` and `letI` is that `letI` inlines the value. But this is not relevant for proofs because of proof irrelevance. Note: This linter can be disabled with `set_option linter.style.haveILetI false` ⚠ [8845/8850] Built Submissions.UpperCompressions.LongChain91LargeTerminal (4.1s) warning: Submissions/UpperCompressions/LongChain91LargeTerminal.lean:107:45: This simp argument is unused: hh Hint: Omit it from the simp argument list. [apply] simp only [firstHitRun_query_bind, hk, hnone, exists_false, or_false, if_false, probOutput_bind_eq_expectedValue] Note: This linter can be disabled with `set_option linter.unusedSimpArgs false` ✔ [8846/8850] Built Submissions.UpperCompressions.LongChain91PayoffExpansion (3.4s) ⚠ [8847/8850] Built Submissions.UpperCompressions.LongChain91LargeSecurity (3.5s) warning: Submissions/UpperCompressions/LongChain91LargeSecurity.lean:260:2: try 'simp' instead of 'simpa' Note: This linter can be disabled with `set_option linter.unnecessarySimpa false` ⚠ [8848/8850] Built Submissions.UpperCompressions.LongChain91SmallSecurity (3.6s) warning: Submissions/UpperCompressions/LongChain91SmallSecurity.lean:337:8: try 'simp' instead of 'simpa' Note: This linter can be disabled with `set_option linter.unnecessarySimpa false` ✔ [8849/8850] Built Submissions.UpperCompressions.LongChain91Secure (2.8s) ✔ [8850/8850] Built Submissions.UpperCompressions.Solution (2.7s) Build completed successfully (8850 jobs). Exporting #[OptimalOTS.Challenge.UpperCompressions.admissible, OptimalOTS.Challenge.UpperCompressions.secure, OptimalOTS.Challenge.UpperCompressions.cost, propext, Quot.sound, Classical.choice, Nat.add, Nat.sub, Nat.mul, Nat.pow, Nat.gcd, Nat.div, Nat.mod, Nat.beq, Nat.ble, Nat.land, Nat.lor, Nat.xor, Nat.shiftLeft, Nat.shiftRight, String.ofList, Char.ofNat, List, eagerReduce, OptimalOTS.Challenge.UpperCompressions.scheme] from Submissions.UpperCompressions.Solution Running Lean default kernel on solution. Lean default kernel accepts the solution Your solution is okay!