Building OptimalOTS.Challenge.UpperCompressions ⚠ [2689/2689] Built OptimalOTS.Challenge.UpperCompressions (3.2s) 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/8821] Built ToMathlib.MeasureTheory.Measure.IndependentDraws (2.1s) ✔ [8799/8821] Built ToMathlib.MeasureTheory.Measure.Bounds (2.2s) ✔ [8800/8821] Built ToMathlib.Probability.UniformOn (2.3s) ✖ [8801/8821] Building Submissions.UpperCompressions.ProofBundle02 (5.4s) trace: .> LEAN_PATH=/srv/ots-work/5f4c1c6d59a055cc053d9c4d9bbdc168/project/formal/.lake/packages/Cli/.lake/build/lib/lean:/srv/ots-work/5f4c1c6d59a055cc053d9c4d9bbdc168/project/formal/.lake/packages/cslib/.lake/build/lib/lean:/srv/ots-work/5f4c1c6d59a055cc053d9c4d9bbdc168/project/formal/.lake/packages/batteries/.lake/build/lib/lean:/srv/ots-work/5f4c1c6d59a055cc053d9c4d9bbdc168/project/formal/.lake/packages/Qq/.lake/build/lib/lean:/srv/ots-work/5f4c1c6d59a055cc053d9c4d9bbdc168/project/formal/.lake/packages/aesop/.lake/build/lib/lean:/srv/ots-work/5f4c1c6d59a055cc053d9c4d9bbdc168/project/formal/.lake/packages/proofwidgets/.lake/build/lib/lean:/srv/ots-work/5f4c1c6d59a055cc053d9c4d9bbdc168/project/formal/.lake/packages/importGraph/.lake/build/lib/lean:/srv/ots-work/5f4c1c6d59a055cc053d9c4d9bbdc168/project/formal/.lake/packages/LeanSearchClient/.lake/build/lib/lean:/srv/ots-work/5f4c1c6d59a055cc053d9c4d9bbdc168/project/formal/.lake/packages/plausible/.lake/build/lib/lean:/srv/ots-work/5f4c1c6d59a055cc053d9c4d9bbdc168/project/formal/.lake/packages/loom2/.lake/build/lib/lean:/srv/ots-work/5f4c1c6d59a055cc053d9c4d9bbdc168/project/formal/.lake/packages/PolyFun/.lake/build/lib/lean:/srv/ots-work/5f4c1c6d59a055cc053d9c4d9bbdc168/project/formal/.lake/packages/mathlib/.lake/build/lib/lean:/srv/ots-work/5f4c1c6d59a055cc053d9c4d9bbdc168/project/formal/.lake/packages/Sail/.lake/build/lib/lean:/srv/ots-work/5f4c1c6d59a055cc053d9c4d9bbdc168/project/formal/.lake/packages/VCVio/.lake/build/lib/lean:/srv/ots-work/5f4c1c6d59a055cc053d9c4d9bbdc168/project/formal/.lake/packages/riscv-zkvm/.lake/build/lib/lean:/srv/ots-work/5f4c1c6d59a055cc053d9c4d9bbdc168/project/formal/.lake/build/lib/lean /srv/ots/.elan/toolchains/leanprover--lean4---v4.33.1/bin/lean /srv/ots-work/5f4c1c6d59a055cc053d9c4d9bbdc168/project/formal/Submissions/UpperCompressions/ProofBundle02.lean -o /srv/ots-work/5f4c1c6d59a055cc053d9c4d9bbdc168/project/formal/.lake/build/lib/lean/Submissions/UpperCompressions/ProofBundle02.olean -i /srv/ots-work/5f4c1c6d59a055cc053d9c4d9bbdc168/project/formal/.lake/build/lib/lean/Submissions/UpperCompressions/ProofBundle02.ilean -c /srv/ots-work/5f4c1c6d59a055cc053d9c4d9bbdc168/project/formal/.lake/build/ir/Submissions/UpperCompressions/ProofBundle02.c --setup /srv/ots-work/5f4c1c6d59a055cc053d9c4d9bbdc168/project/formal/.lake/build/ir/Submissions/UpperCompressions/ProofBundle02.setup.json --json error: Submissions/UpperCompressions/ProofBundle02.lean:1074:69: Unknown identifier `n` Note: It is not possible to treat `n` as an implicitly bound variable here because the `autoImplicit` option is set to `false`. error: Submissions/UpperCompressions/ProofBundle02.lean:1075:43: Unknown identifier `n` Note: It is not possible to treat `n` as an implicitly bound variable here because the `autoImplicit` option is set to `false`. warning: Submissions/UpperCompressions/ProofBundle02.lean:1080:4: declaration uses `sorry` warning: Submissions/UpperCompressions/ProofBundle02.lean:1080:4: declaration uses `sorry` warning: Submissions/UpperCompressions/ProofBundle02.lean:1080:4: declaration uses `sorry` warning: Submissions/UpperCompressions/ProofBundle02.lean:1096:8: declaration uses `sorry` warning: Submissions/UpperCompressions/ProofBundle02.lean:1096:8: declaration uses `sorry` warning: Submissions/UpperCompressions/ProofBundle02.lean:1091:8: declaration uses `sorry` warning: Submissions/UpperCompressions/ProofBundle02.lean:1119:13: declaration uses `sorry` warning: Submissions/UpperCompressions/ProofBundle02.lean:1119:13: declaration uses `sorry` warning: Submissions/UpperCompressions/ProofBundle02.lean:1133:8: declaration uses `sorry` warning: Submissions/UpperCompressions/ProofBundle02.lean:1133:8: declaration uses `sorry` warning: Submissions/UpperCompressions/ProofBundle02.lean:1123:8: declaration uses `sorry` warning: Submissions/UpperCompressions/ProofBundle02.lean:1138:4: Unused tactic linter: `rw [run_loop_succ, support_bind] at hp` does nothing Note: This linter can be disabled with `set_option linter.unusedTactic false` warning: Submissions/UpperCompressions/ProofBundle02.lean:1139:4: Unused tactic linter: `simp only [Set.mem_iUnion] at hp` does nothing Note: This linter can be disabled with `set_option linter.unusedTactic false` warning: Submissions/UpperCompressions/ProofBundle02.lean:1140:4: Unused tactic linter: `obtain ⟨η, _, hp⟩ := hp` does nothing Note: This linter can be disabled with `set_option linter.unusedTactic false` warning: Submissions/UpperCompressions/ProofBundle02.lean:1141:4: Unused tactic linter: `rw [support_bind] at hp` does nothing Note: This linter can be disabled with `set_option linter.unusedTactic false` warning: Submissions/UpperCompressions/ProofBundle02.lean:1142:4: Unused tactic linter: `simp only [Set.mem_iUnion] at hp` does nothing Note: This linter can be disabled with `set_option linter.unusedTactic false` warning: Submissions/UpperCompressions/ProofBundle02.lean:1143:4: Unused tactic linter: `obtain ⟨⟨w, d⟩, hd, hp⟩ := hp` does nothing Note: This linter can be disabled with `set_option linter.unusedTactic false` warning: Submissions/UpperCompressions/ProofBundle02.lean:1144:4: Unused tactic linter: `rw [support_bind] at hp` does nothing Note: This linter can be disabled with `set_option linter.unusedTactic false` warning: Submissions/UpperCompressions/ProofBundle02.lean:1145:4: Unused tactic linter: `simp only [Set.mem_iUnion] at hp` does nothing Note: This linter can be disabled with `set_option linter.unusedTactic false` warning: Submissions/UpperCompressions/ProofBundle02.lean:1146:4: Unused tactic linter: `obtain ⟨⟨r, e⟩, hr, hp⟩ := hp` does nothing Note: This linter can be disabled with `set_option linter.unusedTactic false` warning: Submissions/UpperCompressions/ProofBundle02.lean:1147:4: Unused tactic linter: `rw [support_pure, Set.mem_singleton_iff] at hp` does nothing Note: This linter can be disabled with `set_option linter.unusedTactic false` warning: Submissions/UpperCompressions/ProofBundle02.lean:1148:4: Unused tactic linter: `subst p` does nothing Note: This linter can be disabled with `set_option linter.unusedTactic false` warning: Submissions/UpperCompressions/ProofBundle02.lean:1149:4: Unused tactic linter: `obtain ⟨hcd, hwd⟩ := Dag.Graph.hash_support (m ++ η) c (w, d) hd` does nothing Note: This linter can be disabled with `set_option linter.unusedTactic false` warning: Submissions/UpperCompressions/ProofBundle02.lean:1150:4: Unused tactic linter: `obtain ⟨hde, hret⟩ := ih d (r, e) hr` does nothing Note: This linter can be disabled with `set_option linter.unusedTactic false` warning: Submissions/UpperCompressions/ProofBundle02.lean:1151:4: Unused tactic linter: `refine ⟨hcd.trans hde, ?_⟩` does nothing Note: This linter can be disabled with `set_option linter.unusedTactic false` warning: Submissions/UpperCompressions/ProofBundle02.lean:1152:4: Unused tactic linter: `intro ζ i hi` does nothing Note: This linter can be disabled with `set_option linter.unusedTactic false` warning: Submissions/UpperCompressions/ProofBundle02.lean:1153:4: Unused tactic linter: `rcases best_some_source (fun s : Winner n M => tier s.2) (candidate decode η w) r (ζ, i) hi with hf | ht` does nothing Note: This linter can be disabled with `set_option linter.unusedTactic false` warning: Submissions/UpperCompressions/ProofBundle02.lean:1155:4: Unused tactic linter: `· cases hw : decode w with | none => simp [candidate, hw] at hf | some j => simp only [candidate, hw, Functor.map, Option.map, Option.some.injEq, Prod.mk.injEq] at hf obtain ⟨rfl, rfl⟩ := hf exact ⟨w, hde _ _ hwd, hw⟩` does nothing Note: This linter can be disabled with `set_option linter.unusedTactic false` warning: Submissions/UpperCompressions/ProofBundle02.lean:1162:4: Unused tactic linter: `· exact hret ζ i ht` does nothing Note: This linter can be disabled with `set_option linter.unusedTactic false` warning: Submissions/UpperCompressions/ProofBundle02.lean:1139:4: this tactic is never executed Note: This linter can be disabled with `set_option linter.unreachableTactic false` warning: Submissions/UpperCompressions/ProofBundle02.lean:1140:4: this tactic is never executed Note: This linter can be disabled with `set_option linter.unreachableTactic false` warning: Submissions/UpperCompressions/ProofBundle02.lean:1141:4: this tactic is never executed Note: This linter can be disabled with `set_option linter.unreachableTactic false` warning: Submissions/UpperCompressions/ProofBundle02.lean:1142:4: this tactic is never executed Note: This linter can be disabled with `set_option linter.unreachableTactic false` warning: Submissions/UpperCompressions/ProofBundle02.lean:1143:4: this tactic is never executed Note: This linter can be disabled with `set_option linter.unreachableTactic false` warning: Submissions/UpperCompressions/ProofBundle02.lean:1144:4: this tactic is never executed Note: This linter can be disabled with `set_option linter.unreachableTactic false` warning: Submissions/UpperCompressions/ProofBundle02.lean:1145:4: this tactic is never executed Note: This linter can be disabled with `set_option linter.unreachableTactic false` warning: Submissions/UpperCompressions/ProofBundle02.lean:1146:4: this tactic is never executed Note: This linter can be disabled with `set_option linter.unreachableTactic false` warning: Submissions/UpperCompressions/ProofBundle02.lean:1147:4: this tactic is never executed Note: This linter can be disabled with `set_option linter.unreachableTactic false` warning: Submissions/UpperCompressions/ProofBundle02.lean:1148:4: this tactic is never executed Note: This linter can be disabled with `set_option linter.unreachableTactic false` warning: Submissions/UpperCompressions/ProofBundle02.lean:1149:4: this tactic is never executed Note: This linter can be disabled with `set_option linter.unreachableTactic false` warning: Submissions/UpperCompressions/ProofBundle02.lean:1150:4: this tactic is never executed Note: This linter can be disabled with `set_option linter.unreachableTactic false` warning: Submissions/UpperCompressions/ProofBundle02.lean:1151:4: this tactic is never executed Note: This linter can be disabled with `set_option linter.unreachableTactic false` warning: Submissions/UpperCompressions/ProofBundle02.lean:1152:4: this tactic is never executed Note: This linter can be disabled with `set_option linter.unreachableTactic false` warning: Submissions/UpperCompressions/ProofBundle02.lean:1153:4: this tactic is never executed Note: This linter can be disabled with `set_option linter.unreachableTactic false` warning: Submissions/UpperCompressions/ProofBundle02.lean:1155:4: this tactic is never executed Note: This linter can be disabled with `set_option linter.unreachableTactic false` warning: Submissions/UpperCompressions/ProofBundle02.lean:1162:4: this tactic is never executed Note: This linter can be disabled with `set_option linter.unreachableTactic false` warning: Submissions/UpperCompressions/ProofBundle02.lean:1190:27: declaration uses `sorry` warning: Submissions/UpperCompressions/ProofBundle02.lean:1190:27: declaration uses `sorry` warning: Submissions/UpperCompressions/ProofBundle02.lean:1183:8: declaration uses `sorry` warning: Submissions/UpperCompressions/ProofBundle02.lean:1185:5: Variable name `hf` 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] _hf Note: This linter can be disabled with `set_option linter.unusedVariables false` warning: Submissions/UpperCompressions/ProofBundle02.lean:1193:4: Unused tactic linter: `rw [run_loop_succ, run_loop_succ, map_bind]` does nothing Note: This linter can be disabled with `set_option linter.unusedTactic false` warning: Submissions/UpperCompressions/ProofBundle02.lean:1194:4: Unused tactic linter: `refine bind_congr fun η => ?_` does nothing Note: This linter can be disabled with `set_option linter.unusedTactic false` warning: Submissions/UpperCompressions/ProofBundle02.lean:1195:4: Unused tactic linter: `rw [run_hash_extend _ c f (hf η)]` does nothing Note: This linter can be disabled with `set_option linter.unusedTactic false` warning: Submissions/UpperCompressions/ProofBundle02.lean:1196:4: Unused tactic linter: `simp only [map_eq_bind_pure_comp, Function.comp_def, bind_assoc, pure_bind]` does nothing Note: This linter can be disabled with `set_option linter.unusedTactic false` warning: Submissions/UpperCompressions/ProofBundle02.lean:1197:4: Unused tactic linter: `refine bind_congr fun q => ?_` does nothing Note: This linter can be disabled with `set_option linter.unusedTactic false` warning: Submissions/UpperCompressions/ProofBundle02.lean:1198:4: Unused tactic linter: `rw [ih]` does nothing Note: This linter can be disabled with `set_option linter.unusedTactic false` warning: Submissions/UpperCompressions/ProofBundle02.lean:1199:4: Unused tactic linter: `simp only [map_eq_bind_pure_comp, Function.comp_def, bind_assoc, pure_bind]` does nothing Note: This linter can be disabled with `set_option linter.unusedTactic false` warning: Submissions/UpperCompressions/ProofBundle02.lean:1194:4: this tactic is never executed Note: This linter can be disabled with `set_option linter.unreachableTactic false` warning: Submissions/UpperCompressions/ProofBundle02.lean:1195:4: this tactic is never executed Note: This linter can be disabled with `set_option linter.unreachableTactic false` warning: Submissions/UpperCompressions/ProofBundle02.lean:1196:4: this tactic is never executed Note: This linter can be disabled with `set_option linter.unreachableTactic false` warning: Submissions/UpperCompressions/ProofBundle02.lean:1197:4: this tactic is never executed Note: This linter can be disabled with `set_option linter.unreachableTactic false` warning: Submissions/UpperCompressions/ProofBundle02.lean:1198:4: this tactic is never executed Note: This linter can be disabled with `set_option linter.unreachableTactic false` warning: Submissions/UpperCompressions/ProofBundle02.lean:1199:4: this tactic is never executed Note: This linter can be disabled with `set_option linter.unreachableTactic false` error: Submissions/UpperCompressions/ProofBundle02.lean:1226:9: unsolved goals case zero M n : ℕ decode : BitVec hashBits → Option (Fin M) tier : Fin M → ℕ m : Message table : Nonce n → BitVec hashBits c : Cache hc : ∀ (η : Nonce n), c ⟨msgBits + n, m ++ η⟩ = some (table η) ⊢ none = select (fun r ↦ tier r.2) (List.replicate (sorry ()).length (sorry ())) warning: Submissions/UpperCompressions/ProofBundle02.lean:1226:18: declaration uses `sorry` warning: Submissions/UpperCompressions/ProofBundle02.lean:1226:18: declaration uses `sorry` warning: Submissions/UpperCompressions/ProofBundle02.lean:1226:34: This simp argument is unused: select Hint: Omit it from the simp argument list. [apply] simp [loop, drawList, run_pure] Note: This linter can be disabled with `set_option linter.unusedSimpArgs false` info: Submissions/UpperCompressions/ProofBundle02.lean:1234:0: 'OptimalOTS.WeightedSampling.run_loop_fixed_row' depends on axioms: [propext, sorryAx, Classical.choice, Quot.sound] info: Submissions/UpperCompressions/ProofBundle02.lean:1236:0: 'OptimalOTS.WeightedSampling.loop_support' depends on axioms: [propext, sorryAx, Classical.choice, Quot.sound] info: Submissions/UpperCompressions/ProofBundle02.lean:1237:0: 'OptimalOTS.WeightedSampling.run_loop_extend' depends on axioms: [propext, sorryAx, Classical.choice, Quot.sound] info: Submissions/UpperCompressions/ProofBundle02.lean:1239:0: 'OptimalOTS.WeightedSampling.select_source' depends on axioms: [propext] info: Submissions/UpperCompressions/ProofBundle02.lean:1240:0: 'OptimalOTS.WeightedSampling.select_none_iff' depends on axioms: [propext, Quot.sound] info: Submissions/UpperCompressions/ProofBundle02.lean:1241:0: 'OptimalOTS.WeightedSampling.select_rank_le' depends on axioms: [propext, Quot.sound] info: Submissions/UpperCompressions/ProofBundle02.lean:1242:0: 'OptimalOTS.WeightedSampling.select_first' depends on axioms: [propext] info: Submissions/UpperCompressions/ProofBundle02.lean:1243:0: 'OptimalOTS.WeightedSampling.costAtMost_loop86' depends on axioms: [propext, sorryAx, Classical.choice, Quot.sound] info: Submissions/UpperCompressions/ProofBundle02.lean:2109:0: 'OptimalOTS.WeightedConstruction.NonceCodec.decode_encode' depends on axioms: [propext, Classical.choice, Quot.sound] info: Submissions/UpperCompressions/ProofBundle02.lean:2110:0: 'OptimalOTS.WeightedConstruction.NonceCodec.encode_injective' depends on axioms: [propext, Classical.choice, Quot.sound] info: Submissions/UpperCompressions/ProofBundle02.lean:2111:0: 'OptimalOTS.WeightedConstruction.NonceCodec.encode_decode' depends on axioms: [propext, Classical.choice, Quot.sound] info: Submissions/UpperCompressions/ProofBundle02.lean:2112:0: 'OptimalOTS.WeightedConstruction.NonceCodec.canonical_of_payload_positive' depends on axioms: [propext, Classical.choice, Quot.sound] info: Submissions/UpperCompressions/ProofBundle02.lean:2113:0: 'OptimalOTS.WeightedConstruction.NonceCodec.signature86_length' depends on axioms: [propext, Quot.sound] info: Submissions/UpperCompressions/ProofBundle02.lean:2801:0: 'OptimalOTS.WeightedConstruction.GraphKeygenBridge.E_run_keygen' depends on axioms: [propext, Classical.choice, Quot.sound] info: Submissions/UpperCompressions/ProofBundle02.lean:2802:0: 'OptimalOTS.WeightedConstruction.GraphKeygenBridge.costAtMost_keygen_bind' depends on axioms: [propext, Classical.choice, Quot.sound] error: Lean exited with code 1 ✔ [8802/8821] Built VCVio.OracleComp.QueryTracking.RandomOracle.Simulation (3.1s) ✔ [8803/8821] Built VCVio.EvalDist.Monad.Measure (1.4s) ✔ [8804/8821] Built ToMathlib.MeasureTheory.Measure.UniformTable (1.6s) ✔ [8805/8821] Built VCVio.OracleComp.Constructions.SampleableType.MeasureCompatibility (1.4s) ✔ [8806/8821] Built VCVio.EvalDist.Monad.UniformTable (1.3s) ✔ [8807/8821] Built VCVio.OracleComp.QueryTracking.RandomOracle.EagerTable (1.7s) ⚠ [8808/8821] Built Submissions.UpperCompressions.ProofBundle00 (76s) info: Submissions/UpperCompressions/ProofBundle00.lean:122:0: 'OptimalOTS.ShallowResearch.single_shape_ge' depends on axioms: [propext, Classical.choice, Quot.sound] info: Submissions/UpperCompressions/ProofBundle00.lean:123:0: 'OptimalOTS.ShallowResearch.single_shape_102_ge' depends on axioms: [propext, Classical.choice, Quot.sound] info: Submissions/UpperCompressions/ProofBundle00.lean:178:0: 'OptimalOTS.WeightedResearch92.enough_classes92' depends on axioms: [propext, Classical.choice, Quot.sound] info: Submissions/UpperCompressions/ProofBundle00.lean:179:0: 'OptimalOTS.WeightedResearch92.aliases_exact' depends on axioms: [propext, Classical.choice, Quot.sound] info: Submissions/UpperCompressions/ProofBundle00.lean:180:0: 'OptimalOTS.WeightedResearch92.acceptance_fraction' depends on axioms: [propext, Classical.choice, Quot.sound] info: Submissions/UpperCompressions/ProofBundle00.lean:264:0: 'WeightedAvailability.empirical_failure' depends on axioms: [propext, Classical.choice, Quot.sound] info: Submissions/UpperCompressions/ProofBundle00.lean:364:0: 'WeightedReplacement.kernel_mono' depends on axioms: [propext, Classical.choice, Quot.sound] info: Submissions/UpperCompressions/ProofBundle00.lean:365:0: 'WeightedReplacement.kernel_scale' depends on axioms: [propext, Classical.choice, Quot.sound] info: Submissions/UpperCompressions/ProofBundle00.lean:366:0: 'WeightedReplacement.sub_mul_kernel' depends on axioms: [propext, Classical.choice, Quot.sound] info: Submissions/UpperCompressions/ProofBundle00.lean:367:0: 'WeightedReplacement.kernel_symm' depends on axioms: [propext, Classical.choice, Quot.sound] info: Submissions/UpperCompressions/ProofBundle00.lean:368:0: 'WeightedReplacement.first_minimum_sum' depends on axioms: [propext, Classical.choice, Quot.sound] info: Submissions/UpperCompressions/ProofBundle00.lean:369:0: 'WeightedReplacement.kernel_additive_envelope' depends on axioms: [propext, Classical.choice, Quot.sound] info: Submissions/UpperCompressions/ProofBundle00.lean:370:0: 'WeightedReplacement.kernel_eq_div' depends on axioms: [propext, Classical.choice, Quot.sound] info: Submissions/UpperCompressions/ProofBundle00.lean:594:0: 'WeightedReplacement.iidMean_allPass' depends on axioms: [propext, Classical.choice, Quot.sound] info: Submissions/UpperCompressions/ProofBundle00.lean:595:0: 'WeightedReplacement.iid_first_minimum_probability' depends on axioms: [propext, Classical.choice, Quot.sound] info: Submissions/UpperCompressions/ProofBundle00.lean:596:0: 'WeightedReplacement.iid_first_minimum_event_probability' depends on axioms: [propext, Classical.choice, Quot.sound] info: Submissions/UpperCompressions/ProofBundle00.lean:597:0: 'WeightedReplacement.iidMean_eq_uniform_vectors' depends on axioms: [propext, Classical.choice, Quot.sound] info: Submissions/UpperCompressions/ProofBundle00.lean:598:0: 'WeightedReplacement.uniform_vectors_first_minimum_probability' depends on axioms: [propext, Classical.choice, Quot.sound] info: Submissions/UpperCompressions/ProofBundle00.lean:717:0: 'WeightedReplacement.finite_bayes_likelihood_bound' depends on axioms: [propext, Classical.choice, Quot.sound] info: Submissions/UpperCompressions/ProofBundle00.lean:718:0: 'WeightedReplacement.coordinateLikelihood_survival' depends on axioms: [propext, Classical.choice, Quot.sound] info: Submissions/UpperCompressions/ProofBundle00.lean:719:0: 'WeightedReplacement.coordinate_posterior_bound' depends on axioms: [propext, Classical.choice, Quot.sound] warning: Submissions/UpperCompressions/ProofBundle00.lean:816:23: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false` info: Submissions/UpperCompressions/ProofBundle00.lean:892:0: 'WeightedMGF.factorial_geometric' depends on axioms: [propext, Classical.choice, Quot.sound] info: Submissions/UpperCompressions/ProofBundle00.lean:893:0: 'WeightedMGF.exp_bernstein' depends on axioms: [propext, Classical.choice, Quot.sound] info: Submissions/UpperCompressions/ProofBundle00.lean:894:0: 'WeightedMGF.centered_mgf' depends on axioms: [propext, Classical.choice, Quot.sound] info: Submissions/UpperCompressions/ProofBundle00.lean:895:0: 'WeightedMGF.nonnegative_centered_mgf' depends on axioms: [propext, Classical.choice, Quot.sound] info: Submissions/UpperCompressions/ProofBundle00.lean:896:0: 'WeightedMGF.compensated_mgf' depends on axioms: [propext, Classical.choice, Quot.sound] warning: Submissions/UpperCompressions/ProofBundle00.lean:1026:2: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false` info: Submissions/UpperCompressions/ProofBundle00.lean:1087:0: 'WeightedKernel.iterate_mono' depends on axioms: [propext, Classical.choice, Quot.sound] info: Submissions/UpperCompressions/ProofBundle00.lean:1088:0: 'WeightedKernel.iterate_one' depends on axioms: [propext, Classical.choice, Quot.sound] info: Submissions/UpperCompressions/ProofBundle00.lean:1089:0: 'WeightedKernel.iterate_supermartingale' depends on axioms: [propext, Classical.choice, Quot.sound] info: Submissions/UpperCompressions/ProofBundle00.lean:1090:0: 'WeightedKernel.exponential_step' depends on axioms: [propext, Classical.choice, Quot.sound] info: Submissions/UpperCompressions/ProofBundle00.lean:1091:0: 'WeightedKernel.exponential_tail' depends on axioms: [propext, Classical.choice, Quot.sound] info: Submissions/UpperCompressions/ProofBundle00.lean:1092:0: 'WeightedKernel.optimized_exponent' depends on axioms: [propext, Classical.choice, Quot.sound] info: Submissions/UpperCompressions/ProofBundle00.lean:1093:0: 'WeightedKernel.freedman_tail' depends on axioms: [propext, Classical.choice, Quot.sound] info: Submissions/UpperCompressions/ProofBundle00.lean:1094:0: 'WeightedKernel.finite_kernel_freedman' depends on axioms: [propext, Classical.choice, Quot.sound] info: Submissions/UpperCompressions/ProofBundle00.lean:1248:0: 'WeightedConstants.first_survival' depends on axioms: [propext, Classical.choice, Quot.sound] info: Submissions/UpperCompressions/ProofBundle00.lean:1249:0: 'WeightedConstants.penultimate_survival' depends on axioms: [propext, Classical.choice, Quot.sound] info: Submissions/UpperCompressions/ProofBundle00.lean:1250:0: 'WeightedConstants.referenceMean_le' depends on axioms: [propext, Classical.choice, Quot.sound] info: Submissions/UpperCompressions/ProofBundle00.lean:1251:0: 'WeightedConstants.relative_peak_bound' depends on axioms: [propext, Classical.choice, Quot.sound] info: Submissions/UpperCompressions/ProofBundle00.lean:1430:0: 'WeightedReference.weight_le' depends on axioms: [propext, Classical.choice, Quot.sound] info: Submissions/UpperCompressions/ProofBundle00.lean:1431:0: 'WeightedReference.reference_mean_le' depends on axioms: [propext, Classical.choice, Quot.sound] info: Submissions/UpperCompressions/ProofBundle00.lean:1432:0: 'WeightedReference.post_excess_le' depends on axioms: [propext, Classical.choice, Quot.sound] info: Submissions/UpperCompressions/ProofBundle00.lean:1433:0: 'WeightedReference.common_envelope' depends on axioms: [propext, Classical.choice, Quot.sound] warning: Submissions/UpperCompressions/ProofBundle00.lean:1543: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:1550: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:1560: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:1590: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:1646: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:1648: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:1652: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:1660: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:1668: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:1751: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:1752: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:1834: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:1838: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:1843: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:1848: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` info: Submissions/UpperCompressions/ProofBundle00.lean:1908:0: 'WeightedRow.Weights.drift_outside' depends on axioms: [propext, Classical.choice, Quot.sound] info: Submissions/UpperCompressions/ProofBundle00.lean:1909:0: 'WeightedRow.Weights.drift_inside' depends on axioms: [propext, Classical.choice, Quot.sound] info: Submissions/UpperCompressions/ProofBundle00.lean:1910:0: 'WeightedRow.Weights.drift_outside_le' depends on axioms: [propext, Classical.choice, Quot.sound] info: Submissions/UpperCompressions/ProofBundle00.lean:1911:0: 'WeightedRow.Weights.drift_inside_le' depends on axioms: [propext, Classical.choice, Quot.sound] info: Submissions/UpperCompressions/ProofBundle00.lean:1912:0: 'WeightedRow.Weights.expect_one' depends on axioms: [propext, Classical.choice, Quot.sound] info: Submissions/UpperCompressions/ProofBundle00.lean:1913:0: 'WeightedRow.Weights.positiveOutside_bounds' depends on axioms: [propext, Classical.choice, Quot.sound] info: Submissions/UpperCompressions/ProofBundle00.lean:1914:0: 'WeightedRow.Weights.positiveInside_bounds' depends on axioms: [propext, Classical.choice, Quot.sound] info: Submissions/UpperCompressions/ProofBundle00.lean:1915:0: 'WeightedRow.Weights.centered_variance_le' depends on axioms: [propext, Classical.choice, Quot.sound] info: Submissions/UpperCompressions/ProofBundle00.lean:1916:0: 'WeightedRow.Weights.centered_abs_le' depends on axioms: [propext, Classical.choice, Quot.sound] info: Submissions/UpperCompressions/ProofBundle00.lean:1917:0: 'WeightedRow.Weights.center_predictable_shift' depends on axioms: [propext, Classical.choice, Quot.sound] warning: Submissions/UpperCompressions/ProofBundle00.lean:1990: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:1993: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:2011: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:2114: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` info: Submissions/UpperCompressions/ProofBundle00.lean:2138:0: 'WeightedRow.Weights.score_bump' depends on axioms: [propext, Classical.choice, Quot.sound] info: Submissions/UpperCompressions/ProofBundle00.lean:2139:0: 'WeightedRow.Weights.pairScore_bump' depends on axioms: [propext, Classical.choice, Quot.sound] info: Submissions/UpperCompressions/ProofBundle00.lean:2140:0: 'WeightedRow.Weights.score_drift' depends on axioms: [propext, Classical.choice, Quot.sound] info: Submissions/UpperCompressions/ProofBundle00.lean:2141:0: 'WeightedRow.Weights.pair_drift' depends on axioms: [propext, Classical.choice, Quot.sound] info: Submissions/UpperCompressions/ProofBundle00.lean:2142:0: 'WeightedRow.Weights.score_variance_le' depends on axioms: [propext, Classical.choice, Quot.sound] info: Submissions/UpperCompressions/ProofBundle00.lean:2143:0: 'WeightedRow.Weights.M1_mean_next' depends on axioms: [propext, Classical.choice, Quot.sound] info: Submissions/UpperCompressions/ProofBundle00.lean:2144:0: 'WeightedRow.Weights.M2_mean_next' depends on axioms: [propext, Classical.choice, Quot.sound] info: Submissions/UpperCompressions/ProofBundle00.lean:2145:0: 'WeightedRow.Weights.M1_square_next_le' depends on axioms: [propext, Classical.choice, Quot.sound] info: Submissions/UpperCompressions/ProofBundle00.lean:2146:0: 'WeightedRow.Weights.M1_compensated_square_next_le' depends on axioms: [propext, Classical.choice, Quot.sound] info: Submissions/UpperCompressions/ProofBundle00.lean:2147:0: 'WeightedRow.Weights.uniform_decoder_expect' depends on axioms: [propext, Classical.choice, Quot.sound] info: Submissions/UpperCompressions/ProofBundle00.lean:2148:0: 'WeightedRow.Weights.M1_step_mean' depends on axioms: [propext, Classical.choice, Quot.sound] info: Submissions/UpperCompressions/ProofBundle00.lean:2149:0: 'WeightedRow.Weights.M2_step_mean' depends on axioms: [propext, Classical.choice, Quot.sound] info: Submissions/UpperCompressions/ProofBundle00.lean:2150:0: 'WeightedRow.Weights.M1_step_square_compensated' depends on axioms: [propext, Classical.choice, Quot.sound] warning: Submissions/UpperCompressions/ProofBundle00.lean:2163: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:2182: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:2184: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:2202:0: automatically included section variable(s) unused in theorem `WeightedPublicCounts.counts_cached`: [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` info: Submissions/UpperCompressions/ProofBundle00.lean:2205:0: 'WeightedPublicCounts.counts_insert_update' depends on axioms: [propext, Classical.choice, Quot.sound] info: Submissions/UpperCompressions/ProofBundle00.lean:2206:0: 'WeightedPublicCounts.counts_cached' depends on axioms: [propext, Classical.choice, Quot.sound] warning: Submissions/UpperCompressions/ProofBundle00.lean:2226: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:2234: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:2241: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:2243: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:2276: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` info: Submissions/UpperCompressions/ProofBundle00.lean:2279:0: 'WeightedCacheCounts.classCounts_update_of_mem' depends on axioms: [propext, Classical.choice, Quot.sound] info: Submissions/UpperCompressions/ProofBundle00.lean:2280:0: 'WeightedCacheCounts.classCounts_update_of_not_mem' depends on axioms: [propext, Classical.choice, Quot.sound] info: Submissions/UpperCompressions/ProofBundle00.lean:2281:0: 'WeightedCacheCounts.seen_card_update' depends on axioms: [propext, Classical.choice, Quot.sound] info: Submissions/UpperCompressions/ProofBundle00.lean:2282:0: 'WeightedCacheCounts.seen_card_le' depends on axioms: [propext, Classical.choice, Quot.sound] info: Submissions/UpperCompressions/ProofBundle00.lean:2477:0: 'WeightedFirstHit.stoppedKernel_mono' depends on axioms: [propext, Classical.choice, Quot.sound] info: Submissions/UpperCompressions/ProofBundle00.lean:2478:0: 'WeightedFirstHit.stoppedKernel_one' depends on axioms: [propext, Classical.choice, Quot.sound] info: Submissions/UpperCompressions/ProofBundle00.lean:2479:0: 'WeightedFirstHit.iterate_stopped' depends on axioms: [propext, Classical.choice, Quot.sound] info: Submissions/UpperCompressions/ProofBundle00.lean:2480:0: 'WeightedFirstHit.iterate_hit_eq' depends on axioms: [propext, Classical.choice, Quot.sound] info: Submissions/UpperCompressions/ProofBundle00.lean:2481:0: 'WeightedFirstHit.stopped_exponential_drift' depends on axioms: [propext, Classical.choice, Quot.sound] info: Submissions/UpperCompressions/ProofBundle00.lean:2482:0: 'WeightedFirstHit.firstHit_freedman' depends on axioms: [propext, Classical.choice, Quot.sound] ⚠ [8816/8821] Built Submissions.UpperCompressions.ProofBundle01 (6.3s) info: Submissions/UpperCompressions/ProofBundle01.lean:60:0: 'WeightedEmpirical.score_step_mgf' depends on axioms: [propext, Classical.choice, Quot.sound] info: Submissions/UpperCompressions/ProofBundle01.lean:112:0: 'WeightedEmpirical.lower_score_step_mgf' depends on axioms: [propext, Classical.choice, Quot.sound] warning: Submissions/UpperCompressions/ProofBundle01.lean:126:0: automatically included section variable(s) unused in theorem `WeightedEmpirical.rate_le_linear`: [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:154:4: 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:165:6: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false` info: Submissions/UpperCompressions/ProofBundle01.lean:169:0: 'WeightedEmpirical.rate_le_linear' depends on axioms: [propext, Classical.choice, Quot.sound] info: Submissions/UpperCompressions/ProofBundle01.lean:170:0: 'WeightedEmpirical.mixed_global_constants' depends on axioms: [propext, Classical.choice, Quot.sound] info: Submissions/UpperCompressions/ProofBundle01.lean:222:0: 'WeightedEmpirical.mixed_row_exponent' depends on axioms: [propext, Classical.choice, Quot.sound] info: Submissions/UpperCompressions/ProofBundle01.lean:223:0: 'WeightedEmpirical.exp_neg_pow30_le' depends on axioms: [propext, Classical.choice, Quot.sound] info: Submissions/UpperCompressions/ProofBundle01.lean:224:0: 'WeightedEmpirical.mixed_row_union_margin' depends on axioms: [propext, Classical.choice, Quot.sound] warning: Submissions/UpperCompressions/ProofBundle01.lean:245: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` info: Submissions/UpperCompressions/ProofBundle01.lean:278:0: 'WeightedRow.Weights.withScore_classMass' depends on axioms: [propext, Classical.choice, Quot.sound] info: Submissions/UpperCompressions/ProofBundle01.lean:279:0: 'WeightedRow.Weights.prefix_deficit' depends on axioms: [propext, Classical.choice, Quot.sound] warning: Submissions/UpperCompressions/ProofBundle01.lean:295: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` info: Submissions/UpperCompressions/ProofBundle01.lean:326:0: 'WeightedCacheEvidence.one' depends on axioms: [propext, Classical.choice, Quot.sound] info: Submissions/UpperCompressions/ProofBundle01.lean:327:0: 'WeightedCacheEvidence.two' depends on axioms: [propext, Classical.choice, Quot.sound] warning: Submissions/UpperCompressions/ProofBundle01.lean:356:2: try 'simp' instead of 'simpa' Note: This linter can be disabled with `set_option linter.unnecessarySimpa false` warning: Submissions/UpperCompressions/ProofBundle01.lean:480:6: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false` info: Submissions/UpperCompressions/ProofBundle01.lean:541:0: 'WeightedStopping.covariance_young' depends on axioms: [propext, Classical.choice, Quot.sound] info: Submissions/UpperCompressions/ProofBundle01.lean:542:0: 'WeightedStopping.endpoint' depends on axioms: [propext, Classical.choice, Quot.sound] info: Submissions/UpperCompressions/ProofBundle01.lean:543:0: 'WeightedStopping.stopped_payoff' depends on axioms: [propext, Classical.choice, Quot.sound] info: Submissions/UpperCompressions/ProofBundle01.lean:544:0: 'WeightedStopping.mixed72_young_coefficient' depends on axioms: [propext, Classical.choice, Quot.sound] info: Submissions/UpperCompressions/ProofBundle01.lean:545:0: 'WeightedStopping.covariance_coefficient' depends on axioms: [propext, Classical.choice, Quot.sound] info: Submissions/UpperCompressions/ProofBundle01.lean:546:0: 'WeightedStopping.mixed72_covariance' depends on axioms: [propext, Classical.choice, Quot.sound] info: Submissions/UpperCompressions/ProofBundle01.lean:547:0: 'WeightedStopping.stopped_mixed72_payoff' depends on axioms: [propext, Classical.choice, Quot.sound] info: Submissions/UpperCompressions/ProofBundle01.lean:548:0: 'WeightedStopping.pre_authentication_domination' depends on axioms: [propext, Classical.choice, Quot.sound] warning: Submissions/UpperCompressions/ProofBundle01.lean:577: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:581: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:591: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` info: Submissions/UpperCompressions/ProofBundle01.lean:618:0: 'WeightedRow.Weights.hazard_le_score_pair' depends on axioms: [propext, Classical.choice, Quot.sound] Some required targets logged failures: - Submissions.UpperCompressions.ProofBundle02 error: build failed uncaught exception: Child exited with 1