Mathlib's nightly-testing branch (df0fcc0f5bade33d93ab84fe7f2d0f0fc30dd652 ) regression run completed .
Warning description
3
warning: Mathlib/Probability/Kernel/IonescuTulcea/Traj.lean:422:16: original tactic 'omega' failed: omega could not prove the goal:
2
warning: Mathlib/NumberTheory/LSeries/MellinEqDirichlet.lean:123:56: grind failed where linarith succeeded.
2
warning: Mathlib/NumberTheory/LSeries/HurwitzZetaEven.lean:683:24: grind failed where linarith succeeded.
2
warning: Mathlib/NumberTheory/Harmonic/ZetaAsymp.lean:162:10: grind failed where linarith succeeded.
2
warning: Mathlib/NumberTheory/Harmonic/GammaDeriv.lean:46:31: grind failed where linarith succeeded.
2
warning: Mathlib/MeasureTheory/VectorMeasure/Decomposition/Jordan.lean:278:20: original tactic 'linarith' failed: linarith failed to find a contradiction
2
warning: Mathlib/Analysis/SpecialFunctions/Trigonometric/Inverse.lean:385:6: grind failed where linarith succeeded.
2
warning: Mathlib/Analysis/SpecialFunctions/Gaussian/GaussianIntegral.lean:96:14: grind failed where linarith succeeded.
1
warning: Mathlib/Topology/TietzeExtension.lean:213:32: grind failed where linarith succeeded.
1
warning: Mathlib/Topology/TietzeExtension.lean:202:30: grind failed where linarith succeeded.
1
warning: Mathlib/Topology/MetricSpace/Pseudo/Defs.lean:375:45: grind failed where linarith succeeded.
1
warning: Mathlib/Topology/MetricSpace/Pseudo/Defs.lean:375:32: grind failed where linarith succeeded.
1
warning: Mathlib/Topology/MetricSpace/GromovHausdorff.lean:583:44: grind failed where linarith succeeded.
1
warning: Mathlib/Topology/MetricSpace/GromovHausdorff.lean:548:76: grind failed where linarith succeeded.
1
warning: Mathlib/Topology/MetricSpace/GromovHausdorff.lean:545:33: grind failed where linarith succeeded.
1
warning: Mathlib/Topology/MetricSpace/Gluing.lean:334:2: grind failed where linarith succeeded.
1
warning: Mathlib/Topology/MetricSpace/Gluing.lean:155:37: grind failed where linarith succeeded.
1
warning: Mathlib/Topology/MetricSpace/Gluing.lean:154:37: grind failed where linarith succeeded.
1
warning: Mathlib/Topology/MetricSpace/Gluing.lean:127:2: grind failed where linarith succeeded.
1
warning: Mathlib/Topology/MetricSpace/Gluing.lean:116:4: grind failed where linarith succeeded.
1
warning: Mathlib/Topology/MetricSpace/CantorScheme.lean:130:2: grind failed where linarith succeeded.
1
warning: Mathlib/Topology/MetricSpace/CantorScheme.lean:123:47: grind failed where linarith succeeded.
1
warning: Mathlib/Topology/ContinuousMap/Bounded/Normed.lean:612:2: grind failed where linarith succeeded.
1
warning: Mathlib/Topology/ContinuousMap/Bounded/Normed.lean:605:2: grind failed where linarith succeeded.
1
warning: Mathlib/RingTheory/Trace/Basic.lean:556:2: grind failed where ring succeeded.
1
warning: Mathlib/RingTheory/RootsOfUnity/Minpoly.lean:181:4: grind failed where ring succeeded.
1
warning: Mathlib/RingTheory/Polynomial/Hermite/Gaussian.lean:52:6: grind failed where ring succeeded.
1
warning: Mathlib/RingTheory/Polynomial/Eisenstein/IsIntegral.lean:183:4: grind failed where ring succeeded.
1
warning: Mathlib/RingTheory/Polynomial/Cyclotomic/Eval.lean:252:6: grind failed where linarith succeeded.
1
warning: Mathlib/RingTheory/Polynomial/Cyclotomic/Eval.lean:141:4: grind failed where linarith succeeded.
1
warning: Mathlib/RingTheory/Nilpotent/Basic.lean:140:2: grind failed where linarith succeeded.
1
warning: Mathlib/RingTheory/Localization/Ideal.lean:210:65: grind failed where ring succeeded.
1
warning: Mathlib/RingTheory/Localization/Defs.lean:483:6: grind failed where ring succeeded.
1
warning: Mathlib/RingTheory/Localization/Away/Basic.lean:247:6: grind failed where ring succeeded.
1
warning: Mathlib/RingTheory/Localization/Away/Basic.lean:246:6: grind failed where ring succeeded.
1
warning: Mathlib/RingTheory/LaurentSeries.lean:546:63: grind failed where omega succeeded.
1
warning: Mathlib/RingTheory/GradedAlgebra/HomogeneousLocalization.lean:792:23: grind failed where ring succeeded.
1
warning: Mathlib/RingTheory/GradedAlgebra/HomogeneousLocalization.lean:780:4: grind failed where ring succeeded.
1
warning: Mathlib/RingTheory/GradedAlgebra/HomogeneousLocalization.lean:773:6: grind failed where ring succeeded.
1
warning: Mathlib/Probability/StrongLaw.lean:741:79: grind failed where linarith succeeded.
1
warning: Mathlib/Probability/Kernel/IonescuTulcea/Traj.lean:422:16: grind failed where omega succeeded.
1
warning: Mathlib/Probability/Kernel/Disintegration/MeasurableStieltjes.lean:201:78: grind failed where linarith succeeded.
1
warning: Mathlib/Probability/Kernel/Disintegration/MeasurableStieltjes.lean:201:65: grind failed where linarith succeeded.
1
warning: Mathlib/Order/Interval/Finset/Box.lean:102:4: grind failed where omega succeeded.
1
warning: Mathlib/NumberTheory/WellApproximable.lean:332:8: grind failed where linarith succeeded.
1
warning: Mathlib/NumberTheory/Transcendental/Lindemann/AnalyticalPart.lean:33:2: grind failed where ring succeeded.
1
warning: Mathlib/NumberTheory/RamificationInertia/Basic.lean:163:40: grind failed where omega succeeded.
1
warning: Mathlib/NumberTheory/Pell.lean:563:33: grind failed where linarith succeeded.
1
warning: Mathlib/NumberTheory/Ostrowski.lean:382:8: grind failed where linarith succeeded.
1
warning: Mathlib/NumberTheory/Ostrowski.lean:366:2: grind failed where linarith succeeded.
1
warning: Mathlib/NumberTheory/Ostrowski.lean:212:4: grind failed where linarith succeeded.
1
warning: Mathlib/NumberTheory/NumberField/Units/DirichletTheorem.lean:101:4: grind failed where linarith succeeded.
1
warning: Mathlib/NumberTheory/NumberField/Units/Basic.lean:196:6: grind failed where linarith succeeded.
1
warning: Mathlib/NumberTheory/NumberField/Units/Basic.lean:192:4: grind failed where linarith succeeded.
1
warning: Mathlib/NumberTheory/NumberField/InfinitePlace/Basic.lean:441:32: grind failed where linarith succeeded.
1
warning: Mathlib/NumberTheory/NumberField/Discriminant/Basic.lean:236:6: grind failed where linarith succeeded.
1
warning: Mathlib/NumberTheory/NumberField/CanonicalEmbedding/NormLeOne.lean:620:2: grind failed where ring succeeded.
1
warning: Mathlib/NumberTheory/NumberField/CanonicalEmbedding/ConvexBody.lean:324:4: grind failed where linarith succeeded.
1
warning: Mathlib/NumberTheory/Multiplicity.lean:249:4: grind failed where ring succeeded.
1
warning: Mathlib/NumberTheory/ModularForms/JacobiTheta/Bounds.lean:215:61: grind failed where linarith succeeded.
1
warning: Mathlib/NumberTheory/ModularForms/DedekindEta.lean:97:2: grind failed where ring succeeded.
1
warning: Mathlib/NumberTheory/Modular.lean:221:4: grind failed where ring succeeded.
1
warning: Mathlib/NumberTheory/LSeries/ZMod.lean:450:4: grind failed where ring succeeded.
1
warning: Mathlib/NumberTheory/LSeries/Nonvanishing.lean:234:4: grind failed where ring succeeded.
1
warning: Mathlib/NumberTheory/LSeries/HurwitzZetaOdd.lean:405:2: grind failed where ring succeeded.
1
warning: Mathlib/NumberTheory/Harmonic/ZetaAsymp.lean:56:12: grind failed where linarith succeeded.
1
warning: Mathlib/NumberTheory/Harmonic/ZetaAsymp.lean:286:14: grind failed where linarith succeeded.
1
warning: Mathlib/NumberTheory/Harmonic/ZetaAsymp.lean:171:77: grind failed where linarith succeeded.
1
warning: Mathlib/NumberTheory/Harmonic/ZetaAsymp.lean:169:62: grind failed where linarith succeeded.
1
warning: Mathlib/NumberTheory/Harmonic/GammaDeriv.lean:87:40: grind failed where linarith succeeded.
1
warning: Mathlib/NumberTheory/Harmonic/GammaDeriv.lean:38:74: grind failed where linarith succeeded.
1
warning: Mathlib/NumberTheory/FLT/Three.lean:765:2: grind failed where linarith succeeded.
1
warning: Mathlib/NumberTheory/FLT/Three.lean:657:53: grind failed where ring succeeded.
1
warning: Mathlib/NumberTheory/FLT/Three.lean:647:90: grind failed where ring succeeded.
1
warning: Mathlib/NumberTheory/ClassNumber/Finite.lean:201:6: grind failed where linarith succeeded.
1
warning: Mathlib/NumberTheory/ClassNumber/Finite.lean:199:21: original tactic 'omega' failed: omega could not prove the goal:
1
warning: Mathlib/NumberTheory/ClassNumber/Finite.lean:199:21: grind failed where omega succeeded.
1
warning: Mathlib/NumberTheory/AbelSummation.lean:154:4: grind failed where ring succeeded.
1
warning: Mathlib/MeasureTheory/Measure/SeparableMeasure.lean
[message truncated]
To anyone watching: these aren't real problems, they are just a helpful way of keeping track of places where grind is still not as powerful as we'd like. Please feel free to mute this channel!
There are a couple of messages like "original tactic 'omega' failed: omega could not prove the goal" in there as well. Are those expected?
As far as I understand, these are imperfections in the tactic analysis framework. I'm not sure if @Anne Baanen wants to treat them as defects that need to be fixed, or accept them as best available approximations to the truth!
Overall the framework is going to give an approximation, since translating back and forth between tactic state and infotrees is quite complex. So bugs are expected, but that doesn't mean they are unfixable. I know how to fix a few more bugs, but it will require some more substantial work than changing a few lines of code...
Also, looks like the aggregation per warning type is not correctly stripping out the filename/position where the warning occurs...
#29712 fixes the aggregation.
Mathlib's nightly-testing branch (aa6e7675b1fea16418590ab4cc8ba3544e61489c ) regression run completed .
Oh dear. This suggests my recent refactor accidentally broke these linters.
The issue is they got renamed without updating the set that contains them. #29740 updates the set and adds a check for this issue!
Let's see if it works now:
(It timed out, and today's run seems to go towards timing out too.)
The build completed though, this timeout is all happening in string manipulation. Shellcheck suggested the use of native Bash code instead of shelling out to sed. I suspect going back to sed will make it fast again.
#29767 switches back to sed, which seems to be 3000 times faster on my machine.
Kim Morrison said :
As far as I understand, these are imperfections in the tactic analysis framework. I'm not sure if Anne Baanen wants to treat them as defects that need to be fixed, or accept them as best available approximations to the truth!
#29771 is a refactor that improves the way we reconstruct the tactic state from infotrees. There is still an issue with notation (something to do with free variables), that I haven't been able to trace down.
For example, in Mathlib/RingTheory/Trace/Quotient.lean:
local notation "pSₚ" => Ideal . map ( algebraMap Rₚ Sₚ ) ( maximalIdeal Rₚ )
...
-- error: Unknown constant `Rₚ✝`; Unknown constant `Sₚ✝`; Unknown constant `Rₚ✝`.
rw [ IsScalarTower . algebraMap_eq S Sₚ ( Sₚ ⧸ pSₚ ), Ideal . Quotient . algebraMap_eq ,
RingHom . comp_apply , ← sub_eq_zero , ← map_sub , Ideal . Quotient . eq_zero_iff_mem ]
rw [ h , IsLocalization . mem_map_algebraMap_iff
( Algebra . algebraMapSubmonoid S p . primeCompl ) Sₚ ]
Mathlib's nightly-testing branch (e9ab2793e91dde3742f495b24f8d26d92a40a5de ) regression run completed .
Warning description
234
grind failed where linarith succeeded.
54
cutsat failed where omega succeeded.
45
grind failed where ring succeeded.
5
original tactic 'omega' failed: omega could not prove the goal:
2
original tactic 'linarith' failed: linarith failed to find a contradiction
I checked out the "original tactic failed" warnings: these are all in the context of try or any_goals and similar, so failure is expected here.
Maybe we should track if the current sequence of tactics is in a try / any_goals block, and accept failure in that case?
Mathlib's nightly-testing branch (c8e4e42213c636079e09e7ca0f883386d239fd34 ) regression run completed .
Warning description
234
grind failed where linarith succeeded.
54
cutsat failed where omega succeeded.
45
grind failed where ring succeeded.
5
original tactic 'omega' failed: omega could not prove the goal:
2
original tactic 'linarith' failed: linarith failed to find a contradiction
Mathlib's nightly-testing branch (0ab22dd232a7ba67285ba69e6b31cb621469ae46 ) regression run completed .
Warning description
234
grind failed where linarith succeeded.
54
cutsat failed where omega succeeded.
45
grind failed where ring succeeded.
5
original tactic 'omega' failed: omega could not prove the goal:
2
original tactic 'linarith' failed: linarith failed to find a contradiction
Anne Baanen said :
I checked out the "original tactic failed" warnings: these are all in the context of try or any_goals and similar, so failure is expected here.
Maybe we should track if the current sequence of tactics is in a try / any_goals block, and accept failure in that case?
Sounds good. Great to know we have a diagnosis for the remaining failures!
Mathlib's nightly-testing branch (201ac84bf60583cafd1caeb9f0fc32cc8bcea48e ) regression run completed .
Warning description
232
grind failed where linarith succeeded.
47
cutsat failed where omega succeeded.
29
grind failed where ring succeeded.
5
original tactic 'omega' failed: omega could not prove the goal:
2
original tactic 'linarith' failed: linarith failed to find a contradiction
Mathlib's nightly-testing branch (0179c7b76aee422113cf560285721b2f6259d8b6 ) regression run completed .
Warning description
232
grind failed where linarith succeeded.
49
cutsat failed where omega succeeded.
29
grind failed where ring succeeded.
5
original tactic 'omega' failed: omega could not prove the goal:
2
original tactic 'linarith' failed: linarith failed to find a contradiction
Mathlib's nightly-testing branch (c530e201598ab08a1dfe57c7ee2a894b6258da91 ) regression run completed .
Warning description
232
grind failed where linarith succeeded.
49
cutsat failed where omega succeeded.
29
grind failed where ring succeeded.
5
original tactic 'omega' failed: omega could not prove the goal:
2
original tactic 'linarith' failed: linarith failed to find a contradiction
Mathlib's nightly-testing branch (1cdb73c7c473735e0cfa959109d80a719230d784 ) regression run completed .
Warning description
233
grind failed where linarith succeeded.
42
cutsat failed where omega succeeded.
29
grind failed where ring succeeded.
2
original tactic 'linarith' failed: linarith failed to find a contradiction
Mathlib's nightly-testing branch (6ad0b9e77b3bbe677c4898dfeb475ad7a64f33a5 ) regression run completed .
Warning description
233
grind failed where linarith succeeded.
42
cutsat failed where omega succeeded.
29
grind failed where ring succeeded.
2
original tactic 'linarith' failed: linarith failed to find a contradiction
Mathlib's nightly-testing branch (7d00b7f51de230e6fcb0159f413ed4241d9cc8d3 ) regression run completed .
Warning description
233
grind failed where linarith succeeded.
42
cutsat failed where omega succeeded.
29
grind failed where ring succeeded.
2
original tactic 'linarith' failed: linarith failed to find a contradiction
Mathlib's nightly-testing branch (6da53fa708b7196a725cefb032de88c4c47b4afd ) regression run completed .
Warning description
233
grind failed where linarith succeeded.
42
cutsat failed where omega succeeded.
29
grind failed where ring succeeded.
2
original tactic 'linarith' failed: linarith failed to find a contradiction
Mathlib's nightly-testing branch (b20b7ed23f231f211900ad0c59c294b073b5dfd8 ) regression run completed .
Warning description
233
grind failed where linarith succeeded.
42
cutsat failed where omega succeeded.
29
grind failed where ring succeeded.
2
original tactic 'linarith' failed: linarith failed to find a contradiction
Mathlib's nightly-testing branch (597bf947c26681388ad5ed3f4d958fd97deacada ) regression run completed .
Warning description
233
grind failed where linarith succeeded.
42
cutsat failed where omega succeeded.
29
grind failed where ring succeeded.
2
original tactic 'linarith' failed: linarith failed to find a contradiction
Mathlib's nightly-testing branch (11fa7d4a8c6f4323a3259cb4d9617131c64d653a ) regression run completed .
Warning description
235
grind failed where linarith succeeded.
35
cutsat failed where omega succeeded.
29
grind failed where ring succeeded.
2
original tactic 'linarith' failed: linarith failed to find a contradiction
Mathlib's nightly-testing branch (43c1fdcc532a0143e92b4f0be3cec14f9e5a9207 ) regression run completed .
Warning description
237
grind failed where linarith succeeded.
35
cutsat failed where omega succeeded.
29
grind failed where ring succeeded.
2
original tactic 'linarith' failed: linarith failed to find a contradiction
Mathlib's nightly-testing branch (e3a1ca33ee355432b57c5583a4997f39c70190b2 ) regression run completed .
Warning description
238
grind failed where linarith succeeded.
35
cutsat failed where omega succeeded.
29
grind failed where ring succeeded.
2
original tactic 'linarith' failed: linarith failed to find a contradiction
Mathlib's nightly-testing branch (f76e609368a08552752c8cfadfd47933128f2ce5 ) regression run completed .
Warning description
239
grind failed where linarith succeeded.
35
cutsat failed where omega succeeded.
29
grind failed where ring succeeded.
2
original tactic 'linarith' failed: linarith failed to find a contradiction
Mathlib's nightly-testing branch (153004c946eb30180b50c062c13ddc488f3ea2c0 ) regression run completed .
Warning description
239
grind failed where linarith succeeded.
35
cutsat failed where omega succeeded.
29
grind failed where ring succeeded.
2
original tactic 'linarith' failed: linarith failed to find a contradiction
Mathlib's nightly-testing branch (ac8a764b52b88ac588443dbd5adc5c7a4dd5b623 ) regression run completed .
Warning description
239
grind failed where linarith succeeded.
35
cutsat failed where omega succeeded.
29
grind failed where ring succeeded.
2
original tactic 'linarith' failed: linarith failed to find a contradiction
Mathlib's nightly-testing branch (281600fbe3d8bbc04e67750842ed1d3d3e96306e ) regression run completed .
Warning description
239
grind failed where linarith succeeded.
35
cutsat failed where omega succeeded.
30
grind failed where ring succeeded.
2
original tactic 'linarith' failed: linarith failed to find a contradiction
Mathlib's nightly-testing branch (104fa779cd9a131c1ba2fa86c9523be5fd5f9ab3 ) regression run completed .
Warning description
239
grind failed where linarith succeeded.
35
cutsat failed where omega succeeded.
30
grind failed where ring succeeded.
2
original tactic 'linarith' failed: linarith failed to find a contradiction
Mathlib's nightly-testing branch (429a4ae3f20ab74a979c0117ce54e5bb2d6b0500 ) regression run completed .
Warning description
239
grind failed where linarith succeeded.
35
cutsat failed where omega succeeded.
30
grind failed where ring succeeded.
2
original tactic 'linarith' failed: linarith failed to find a contradiction
Mathlib's nightly-testing branch (a5bfd0ed175224d30c26cda596630f19bbb4b698 ) regression run completed .
Warning description
238
grind failed where linarith succeeded.
35
cutsat failed where omega succeeded.
30
grind failed where ring succeeded.
2
original tactic 'linarith' failed: linarith failed to find a contradiction
Mathlib's nightly-testing branch (ecda81f6b653e619a992d0cbfa83b88279d76789 ) regression run completed .
Warning description
238
grind failed where linarith succeeded.
35
cutsat failed where omega succeeded.
30
grind failed where ring succeeded.
2
original tactic 'linarith' failed: linarith failed to find a contradiction
Mathlib's nightly-testing branch (824f91d5ed71e3f08b69fd50ba788a0b628c8505 ) regression run completed .
Warning description
238
grind failed where linarith succeeded.
35
cutsat failed where omega succeeded.
30
grind failed where ring succeeded.
2
original tactic 'linarith' failed: linarith failed to find a contradiction
Mathlib's nightly-testing branch (b56fe7cd4993fd2f7af49ca8cd33c2cdb6deccad ) regression run completed .
Warning description
237
grind failed where linarith succeeded.
35
cutsat failed where omega succeeded.
30
grind failed where ring succeeded.
2
original tactic 'linarith' failed: linarith failed to find a contradiction
Mathlib's nightly-testing branch (8fe43ab1bccf3e79d4857d89053e6d1348f03e5a ) regression run completed .
Warning description
237
grind failed where linarith succeeded.
35
cutsat failed where omega succeeded.
30
grind failed where ring succeeded.
2
original tactic 'linarith' failed: linarith failed to find a contradiction
Mathlib's nightly-testing branch (cda8e891afb8be29c1abd6fc2ab6ffb6ce83ff09 ) regression run completed .
Warnings: 297
Error description
1
linter Mathlib.TacticAnalysis.tacticAnalysis failed: (deterministic) timeout at isDefEq, maximum number of heartbeats (200000) has been reached
1
error: Lean exited with code 1
Warning description
231
grind failed where linarith succeeded.
35
cutsat failed where omega succeeded.
29
grind failed where ring succeeded.
2
original tactic 'linarith' failed: linarith failed to find a contradiction
Mathlib's nightly-testing branch (09c801ea5c5fd16373f8dfbd49b0d1cebe16c88d ) regression run completed .
Warnings: 298
Error description
1
linter Mathlib.TacticAnalysis.tacticAnalysis failed: (deterministic) timeout at isDefEq, maximum number of heartbeats (200000) has been reached
1
error: Lean exited with code 1
Warning description
232
grind failed where linarith succeeded.
35
cutsat failed where omega succeeded.
29
grind failed where ring succeeded.
2
original tactic 'linarith' failed: linarith failed to find a contradiction
Mathlib's nightly-testing branch (2f924cb79c413ce5cf158cf653bb8fe287622b1e ) regression run completed .
Warnings: 298
Error description
1
linter Mathlib.TacticAnalysis.tacticAnalysis failed: (deterministic) timeout at isDefEq, maximum number of heartbeats (200000) has been reached
1
error: Lean exited with code 1
Warning description
232
grind failed where linarith succeeded.
35
cutsat failed where omega succeeded.
29
grind failed where ring succeeded.
2
original tactic 'linarith' failed: linarith failed to find a contradiction
Mathlib's nightly-testing branch (1b8918e9f7d6591414d0354289cec29fa1bab47d ) regression run completed .
Warnings: 301
Error description
1
linter Mathlib.TacticAnalysis.tacticAnalysis failed: (deterministic) timeout at isDefEq, maximum number of heartbeats (200000) has been reached
1
error: Lean exited with code 1
Warning description
235
grind failed where linarith succeeded.
35
cutsat failed where omega succeeded.
29
grind failed where ring succeeded.
2
original tactic 'linarith' failed: linarith failed to find a contradiction
Mathlib's nightly-testing branch (3a09765e211bee40f7eebb7529a4b7dd90ba202a ) regression run completed .
Warnings: 301
Error description
1
linter Mathlib.TacticAnalysis.tacticAnalysis failed: (deterministic) timeout at isDefEq, maximum number of heartbeats (200000) has been reached
1
error: Lean exited with code 1
Warning description
235
grind failed where linarith succeeded.
35
cutsat failed where omega succeeded.
29
grind failed where ring succeeded.
2
original tactic 'linarith' failed: linarith failed to find a contradiction
Mathlib's nightly-testing branch (da36cf4a6eb007b201e1f5af7f3f399293461f89 ) regression run completed .
Warnings: 305
Error description
1
linter Mathlib.TacticAnalysis.tacticAnalysis failed: (deterministic) timeout at isDefEq, maximum number of heartbeats (200000) has been reached
1
error: Lean exited with code 1
Warning description
239
grind failed where linarith succeeded.
35
cutsat failed where omega succeeded.
29
grind failed where ring succeeded.
2
original tactic 'linarith' failed: linarith failed to find a contradiction
Mathlib's nightly-testing branch (9ffe5fd0791f1d271211fd961704b8f0a8d7f2af ) regression run completed .
Warnings: 159
Error description
1
unsolved goals
1
tauto failed to solve some goals.
1
error: Lean exited with code 1
Warning description
79
grind failed where tauto succeeded.
33
grind failed where linarith succeeded.
31
cutsat failed where omega succeeded.
16
grind failed where ring succeeded.
Mathlib's nightly-testing branch (b14b433fa7c95050360991bc93ea63d0ad664968 ) regression run completed .
Warnings: 159
Error description
1
unsolved goals
1
tauto failed to solve some goals.
1
error: Lean exited with code 1
Warning description
79
grind failed where tauto succeeded.
33
grind failed where linarith succeeded.
31
cutsat failed where omega succeeded.
16
grind failed where ring succeeded.
Mathlib's nightly-testing branch (5c3dd696b785d509ceafbc15ef3e36835b98e51f ) regression run completed .
Warnings: 159
Error description
1
unsolved goals
1
tauto failed to solve some goals.
1
error: Lean exited with code 1
Warning description
79
grind failed where tauto succeeded.
33
grind failed where linarith succeeded.
31
cutsat failed where omega succeeded.
16
grind failed where ring succeeded.
Mathlib's nightly-testing branch (ee8785d7e18b3537bbda7d95ea878b7766d279fe ) regression run completed .
Warnings: 159
Error description
1
unsolved goals
1
tauto failed to solve some goals.
1
error: Lean exited with code 1
Warning description
79
grind failed where tauto succeeded.
33
grind failed where linarith succeeded.
31
cutsat failed where omega succeeded.
16
grind failed where ring succeeded.
Mathlib's nightly-testing branch (7db953b1c5d3fdef287052f1cc71200abdb32fb3 ) regression run completed .
Warnings: 159
Error description
1
unsolved goals
1
tauto failed to solve some goals.
1
error: Lean exited with code 1
Warning description
79
grind failed where tauto succeeded.
33
grind failed where linarith succeeded.
31
cutsat failed where omega succeeded.
16
grind failed where ring succeeded.
Mathlib's nightly-testing branch (f01124af2f443a17b136c215639561d04b7bf876 ) regression run completed .
Warnings: 159
Error description
1
unsolved goals
1
tauto failed to solve some goals.
1
error: Lean exited with code 1
Warning description
79
grind failed where tauto succeeded.
33
grind failed where linarith succeeded.
31
cutsat failed where omega succeeded.
16
grind failed where ring succeeded.
Mathlib's nightly-testing branch (510cbb2ce097c4dc39fe834d187b1ff395c41946 ) regression run completed .
Warnings: 160
Error description
1
unsolved goals
1
tauto failed to solve some goals.
1
error: Lean exited with code 1
Warning description
79
grind failed where tauto succeeded.
33
grind failed where linarith succeeded.
31
cutsat failed where omega succeeded.
17
grind failed where ring succeeded.
Mathlib's nightly-testing branch (a05c9503a103fc75054a93ab18293b1ca3f9b736 ) regression run completed .
Warnings: 160
Error description
1
unsolved goals
1
tauto failed to solve some goals.
1
error: Lean exited with code 1
Warning description
79
grind failed where tauto succeeded.
33
grind failed where linarith succeeded.
31
cutsat failed where omega succeeded.
17
grind failed where ring succeeded.
Mathlib's nightly-testing branch (2b745e681e087431d4ed77a21223b5cf6c35180b ) regression run completed .
Warnings: 159
Error description
1
unsolved goals
1
tauto failed to solve some goals.
1
error: Lean exited with code 1
Warning description
78
grind failed where tauto succeeded.
33
grind failed where linarith succeeded.
31
cutsat failed where omega succeeded.
17
grind failed where ring succeeded.
Mathlib's nightly-testing branch (1189c522713da13a36fb82b9a07c3c64248419ee ) regression run completed .
Warnings: 159
Error description
1
unsolved goals
1
tauto failed to solve some goals.
1
error: Lean exited with code 1
Warning description
78
grind failed where tauto succeeded.
33
grind failed where linarith succeeded.
31
cutsat failed where omega succeeded.
17
grind failed where ring succeeded.
Mathlib's nightly-testing branch (1549eab285285e8070358e992655979560cbe2a8 ) regression run completed .
Warnings: 159
Error description
1
unsolved goals
1
tauto failed to solve some goals.
1
error: Lean exited with code 1
Warning description
78
grind failed where tauto succeeded.
33
grind failed where linarith succeeded.
31
cutsat failed where omega succeeded.
17
grind failed where ring succeeded.
Mathlib's nightly-testing branch (bcb82cd8c7723257a611efbc0e2ea0fbb968ac42 ) regression run completed .
Warnings: 172
Error description
1
unsolved goals
1
tauto failed to solve some goals.
1
error: Lean exited with code 1
Warning description
88
grind failed where tauto succeeded.
34
cutsat failed where omega succeeded.
33
grind failed where linarith succeeded.
17
grind failed where ring succeeded.
Mathlib's nightly-testing branch (318efa2722d9da2d9de6dfae77c32d4e2531c83a ) regression run completed .
Warnings: 172
Error description
1
unsolved goals
1
tauto failed to solve some goals.
1
error: Lean exited with code 1
Warning description
88
grind failed where tauto succeeded.
34
cutsat failed where omega succeeded.
33
grind failed where linarith succeeded.
17
grind failed where ring succeeded.
Mathlib's nightly-testing branch (9c9f6b3486a12bb0b9462cd03c4b9faff84cd238 ) regression run completed .
Warnings: 172
Info messages: 1
Error description
1
unsolved goals
1
tauto failed to solve some goals.
1
error: Lean exited with code 1
Warning description
88
grind failed where tauto succeeded.
34
cutsat failed where omega succeeded.
33
grind failed where linarith succeeded.
17
grind failed where ring succeeded.
Info message
1
Error: index out of bounds
Mathlib's nightly-testing branch (9601f1d241b59946b0119f9270bf7432f336c7cf ) regression run completed .
Warnings: 174
Info messages: 1
Error description
1
unsolved goals
1
tauto failed to solve some goals.
1
error: Lean exited with code 1
Warning description
88
grind failed where tauto succeeded.
36
cutsat failed where omega succeeded.
33
grind failed where linarith succeeded.
17
grind failed where ring succeeded.
Info message
1
Error: index out of bounds
Mathlib's nightly-testing branch (0665596f30b55957569b856b0b65bef0b811c951 ) regression run completed .
Warnings: 174
Info messages: 1
Error description
1
unsolved goals
1
tauto failed to solve some goals.
1
error: Lean exited with code 1
Warning description
88
grind failed where tauto succeeded.
36
cutsat failed where omega succeeded.
33
grind failed where linarith succeeded.
17
grind failed where ring succeeded.
Info message
1
Error: index out of bounds
Mathlib's nightly-testing branch (0c28cbcc470eba3105750fa4bb7e6330bb6e81ee ) regression run completed .
Warnings: 174
Info messages: 1
Error description
1
unsolved goals
1
tauto failed to solve some goals.
1
error: Lean exited with code 1
Warning description
88
grind failed where tauto succeeded.
36
cutsat failed where omega succeeded.
33
grind failed where linarith succeeded.
17
grind failed where ring succeeded.
Info message
1
Error: index out of bounds
Mathlib's nightly-testing branch (41b1c38179c6416d8faaa077e9293e9c0da36766 ) regression run completed .
Warnings: 174
Info messages: 1
Error description
1
unsolved goals
1
tauto failed to solve some goals.
1
error: Lean exited with code 1
Warning description
88
grind failed where tauto succeeded.
36
cutsat failed where omega succeeded.
33
grind failed where linarith succeeded.
17
grind failed where ring succeeded.
Info message
1
Error: index out of bounds
Mathlib's nightly-testing branch (8e6c7dc75a982cbbe37657574bdc8b955ebc4cb4 ) regression run completed .
Warnings: 175
Info messages: 1
Error description
1
unsolved goals
1
tauto failed to solve some goals.
1
error: Lean exited with code 1
Warning description
89
grind failed where tauto succeeded.
36
cutsat failed where omega succeeded.
33
grind failed where linarith succeeded.
17
grind failed where ring succeeded.
Info message
1
Error: index out of bounds
Mathlib's nightly-testing branch (4b309e5232be602687903b5d7eba7cdeac9c8440 ) regression run completed .
Warnings: 175
Info messages: 1
Error description
1
unsolved goals
1
tauto failed to solve some goals.
1
error: Lean exited with code 1
Warning description
89
grind failed where tauto succeeded.
36
cutsat failed where omega succeeded.
33
grind failed where linarith succeeded.
17
grind failed where ring succeeded.
Info message
1
Error: index out of bounds
Mathlib's nightly-testing branch (c05942e08bc4cc2c55dac5b7c00352c481bede99 ) regression run completed .
Warnings: 175
Info messages: 1
Error description
1
unsolved goals
1
tauto failed to solve some goals.
1
error: Lean exited with code 1
Warning description
89
grind failed where tauto succeeded.
36
cutsat failed where omega succeeded.
33
grind failed where linarith succeeded.
17
grind failed where ring succeeded.
Info message
1
Error: index out of bounds
Mathlib's nightly-testing branch (e66a7c98a6871ae2719ce08aeb613f2b45d4119d ) regression run completed .
Warnings: 175
Info messages: 1
Error description
1
unsolved goals
1
tauto failed to solve some goals.
1
error: Lean exited with code 1
Warning description
89
grind failed where tauto succeeded.
36
cutsat failed where omega succeeded.
33
grind failed where linarith succeeded.
17
grind failed where ring succeeded.
Info message
1
Error: index out of bounds
Mathlib's nightly-testing branch (69b30f6081061f8153765afc8388abc311884e58 ) regression run completed .
Warnings: 175
Info messages: 1
Error description
1
unsolved goals
1
tauto failed to solve some goals.
1
error: Lean exited with code 1
Warning description
89
grind failed where tauto succeeded.
36
cutsat failed where omega succeeded.
33
grind failed where linarith succeeded.
17
grind failed where ring succeeded.
Info message
1
Error: index out of bounds
Mathlib's nightly-testing branch (6ab3440a00cd34ee8da16d2352506f84e59dff93 ) regression run completed .
Warnings: 175
Info messages: 1
Error description
1
unsolved goals
1
tauto failed to solve some goals.
1
error: Lean exited with code 1
Warning description
89
grind failed where tauto succeeded.
36
cutsat failed where omega succeeded.
33
grind failed where linarith succeeded.
17
grind failed where ring succeeded.
Info message
1
Error: index out of bounds
Mathlib's nightly-testing branch (83359cd6f034232379715c2c70ac5a59a9ea8847 ) regression run completed .
Warnings: 175
Info messages: 1
Error description
1
unsolved goals
1
tauto failed to solve some goals.
1
error: Lean exited with code 1
Warning description
89
grind failed where tauto succeeded.
36
cutsat failed where omega succeeded.
33
grind failed where linarith succeeded.
17
grind failed where ring succeeded.
Info message
1
Error: index out of bounds
Mathlib's nightly-testing branch (22f65ecb8d8277c06aa54e12efa281e803ed1ac4 ) regression run completed .
Warnings: 175
Info messages: 1
Error description
1
unsolved goals
1
tauto failed to solve some goals.
1
error: Lean exited with code 1
Warning description
89
grind failed where tauto succeeded.
36
cutsat failed where omega succeeded.
33
grind failed where linarith succeeded.
17
grind failed where ring succeeded.
Info message
1
Error: index out of bounds
Mathlib's nightly-testing branch (95f13e57fc48ad261601c11726c1b7d964a2e679 ) regression run completed .
Warnings: 175
Info messages: 1
Error description
1
unsolved goals
1
tauto failed to solve some goals.
1
error: Lean exited with code 1
Warning description
89
grind failed where tauto succeeded.
36
cutsat failed where omega succeeded.
33
grind failed where linarith succeeded.
17
grind failed where ring succeeded.
Info message
1
Error: index out of bounds
Mathlib's nightly-testing branch (780cbe2da5302ccce8e15061c51f458e969c92dc ) regression run completed .
Warnings: 175
Info messages: 1
Error description
1
unsolved goals
1
tauto failed to solve some goals.
1
error: Lean exited with code 1
Warning description
89
grind failed where tauto succeeded.
36
cutsat failed where omega succeeded.
33
grind failed where linarith succeeded.
17
grind failed where ring succeeded.
Info message
1
Error: index out of bounds
Mathlib's nightly-testing branch (43e541b6a05faa1984fb459607d332b1b348d181 ) regression run completed .
Warnings: 175
Info messages: 1
Error description
1
unsolved goals
1
tauto failed to solve some goals.
1
error: Lean exited with code 1
Warning description
89
grind failed where tauto succeeded.
36
cutsat failed where omega succeeded.
33
grind failed where linarith succeeded.
17
grind failed where ring succeeded.
Info message
1
Error: index out of bounds
Mathlib's nightly-testing branch (8068277c3ab280502aecf3c5100d7dd55806c53a ) regression run completed .
Warnings: 175
Info messages: 1
Error description
1
unsolved goals
1
tauto failed to solve some goals.
1
error: Lean exited with code 1
Warning description
89
grind failed where tauto succeeded.
36
cutsat failed where omega succeeded.
33
grind failed where linarith succeeded.
17
grind failed where ring succeeded.
Info message
1
Error: index out of bounds
Mathlib's nightly-testing branch (1978c4df79b318f01a66d0bbe19151885f450659 ) regression run completed .
Warnings: 181
Error description
1
unsolved goals
1
tauto failed to solve some goals.
1
error: Lean exited with code 1
Warning description
92
grind failed where tauto succeeded.
37
cutsat failed where omega succeeded.
33
grind failed where linarith succeeded.
19
grind failed where ring succeeded.
Mathlib's nightly-testing branch (ef8d524f70a4ba8204224393e34203023e34f964 ) regression run completed .
Warnings: 181
Error description
1
unsolved goals
1
tauto failed to solve some goals.
1
error: Lean exited with code 1
Warning description
92
grind failed where tauto succeeded.
37
cutsat failed where omega succeeded.
33
grind failed where linarith succeeded.
19
grind failed where ring succeeded.
Mathlib's nightly-testing branch (fea3bb9371118ada7a5d092cff313b759967270d ) regression run completed .
Warnings: 181
Error description
1
unsolved goals
1
tauto failed to solve some goals.
1
error: Lean exited with code 1
Warning description
92
grind failed where tauto succeeded.
37
cutsat failed where omega succeeded.
33
grind failed where linarith succeeded.
19
grind failed where ring succeeded.
Mathlib's nightly-testing branch (544a5bad21a682c17de0b86fbab5b0a1707c0a71 ) regression run completed .
Warnings: 181
Error description
1
unsolved goals
1
tauto failed to solve some goals.
1
error: Lean exited with code 1
Warning description
92
grind failed where tauto succeeded.
37
cutsat failed where omega succeeded.
33
grind failed where linarith succeeded.
19
grind failed where ring succeeded.
Mathlib's nightly-testing branch (05ee335d6e3f03d6da5aaae2a817ce3d572fd7dc ) regression run completed .
Warnings: 181
Error description
1
unsolved goals
1
tauto failed to solve some goals.
1
error: Lean exited with code 1
Warning description
92
grind failed where tauto succeeded.
37
lia failed where omega succeeded.
33
grind failed where linarith succeeded.
19
grind failed where ring succeeded.
Mathlib's nightly-testing branch (5e416f69da92a1d2b369c5481a741ec78c6d0bc7 ) regression run completed .
Warnings: 184
Error description
1
unsolved goals
1
tauto failed to solve some goals.
1
error: Lean exited with code 1
Warning description
94
grind failed where tauto succeeded.
37
lia failed where omega succeeded.
33
grind failed where linarith succeeded.
20
grind failed where ring succeeded.
Mathlib's nightly-testing branch (9ce81b10927d4c9c4126c6b5c985064f147a6e30 ) regression run completed .
Warnings: 184
Error description
1
unsolved goals
1
tauto failed to solve some goals.
1
error: Lean exited with code 1
Warning description
94
grind failed where tauto succeeded.
37
lia failed where omega succeeded.
33
grind failed where linarith succeeded.
20
grind failed where ring succeeded.
Mathlib's nightly-testing branch (3592282fbc21a2cc2ef90d01447a3eef5ce284dd ) regression run completed .
Warnings: 181
Error description
1
unsolved goals
1
tauto failed to solve some goals.
1
error: Lean exited with code 1
Warning description
97
grind failed where tauto succeeded.
37
lia failed where omega succeeded.
27
grind failed where linarith succeeded.
20
grind failed where ring succeeded.
Mathlib's nightly-testing branch (b3687cde5b3ccbaf04e5c3b772a97465ff3949b3 ) regression run completed .
Warnings: 181
Error description
1
unsolved goals
1
tauto failed to solve some goals.
1
error: Lean exited with code 1
Warning description
97
grind failed where tauto succeeded.
37
lia failed where omega succeeded.
27
grind failed where linarith succeeded.
20
grind failed where ring succeeded.
Mathlib's nightly-testing branch (ae8e7b63aea6f3181e3a76e98a859aaf27843c3f ) regression run completed .
Warnings: 181
Error description
1
unsolved goals
1
tauto failed to solve some goals.
1
error: Lean exited with code 1
Warning description
97
grind failed where tauto succeeded.
37
lia failed where omega succeeded.
27
grind failed where linarith succeeded.
20
grind failed where ring succeeded.
Mathlib's nightly-testing branch (2bd1b8fc87246c6ddcbef2e414aad2c558edb3e4 ) regression run completed .
Warnings: 178
Error description
2
error: Lean exited with code 1
1
unsolved goals
1
tauto failed to solve some goals.
1
linter Mathlib.TacticAnalysis.tacticAnalysis failed: Unknown constant _private.Mathlib.Algebra.Module.LocalizedModule.Basic.0.LocalizedModule.mul_smul_aux._simp_1_2
Warning description
94
grind failed where tauto succeeded.
37
lia failed where omega succeeded.
27
grind failed where linarith succeeded.
20
grind failed where ring succeeded.
Mathlib's nightly-testing branch (e9941d0b3578a1b32947549e27f584f93f84727f ) regression run completed .
Warnings: 178
Error description
2
error: Lean exited with code 1
1
unsolved goals
1
tauto failed to solve some goals.
1
linter Mathlib.TacticAnalysis.tacticAnalysis failed: Unknown constant _private.Mathlib.Algebra.Module.LocalizedModule.Basic.0.LocalizedModule.mul_smul_aux._simp_1_2
Warning description
94
grind failed where tauto succeeded.
37
lia failed where omega succeeded.
27
grind failed where linarith succeeded.
20
grind failed where ring succeeded.
Mathlib's nightly-testing branch (5bfa1623542d7f245e45ac880c26cfe8f9ecc5ea ) regression run completed .
Warnings: 178
Error description
2
error: Lean exited with code 1
1
unsolved goals
1
tauto failed to solve some goals.
1
linter Mathlib.TacticAnalysis.tacticAnalysis failed: Unknown constant _private.Mathlib.Algebra.Module.LocalizedModule.Basic.0.LocalizedModule.mul_smul_aux._simp_1_2
Warning description
94
grind failed where tauto succeeded.
37
lia failed where omega succeeded.
27
grind failed where linarith succeeded.
20
grind failed where ring succeeded.
Mathlib's nightly-testing branch (47232c86ec8a757736df7a7e225fff8044ec0913 ) regression run completed .
Warnings: 178
Error description
2
error: Lean exited with code 1
1
unsolved goals
1
tauto failed to solve some goals.
1
linter Mathlib.TacticAnalysis.tacticAnalysis failed: Unknown constant _private.Mathlib.Algebra.Module.LocalizedModule.Basic.0.LocalizedModule.mul_smul_aux._simp_1_2
Warning description
94
grind failed where tauto succeeded.
37
lia failed where omega succeeded.
27
grind failed where linarith succeeded.
20
grind failed where ring succeeded.
Mathlib's nightly-testing branch (96d98dd8f37a7723fdb3f43a766a7fea4580b92b ) regression run completed .
Warnings: 178
Error description
2
error: Lean exited with code 1
1
unsolved goals
1
tauto failed to solve some goals.
1
linter Mathlib.TacticAnalysis.tacticAnalysis failed: Unknown constant _private.Mathlib.Algebra.Module.LocalizedModule.Basic.0.LocalizedModule.mul_smul_aux._simp_1_2
Warning description
94
grind failed where tauto succeeded.
37
lia failed where omega succeeded.
27
grind failed where linarith succeeded.
20
grind failed where ring succeeded.
Mathlib's nightly-testing branch (beb1a1dc8899a9b31359eb461c1562bbced8ec2a ) regression run completed .
Warnings: 177
Error description
2
error: Lean exited with code 1
1
unsolved goals
1
tauto failed to solve some goals.
1
linter Mathlib.TacticAnalysis.tacticAnalysis failed: Unknown constant _private.Mathlib.Algebra.Module.LocalizedModule.Basic.0.LocalizedModule.mul_smul_aux._simp_1_2
Warning description
94
grind failed where tauto succeeded.
37
lia failed where omega succeeded.
26
grind failed where linarith succeeded.
20
grind failed where ring succeeded.
Mathlib's nightly-testing branch (f7826d333e7f78a0636e6353ac61dd003abeb484 ) regression run completed .
Warnings: 177
Error description
2
error: Lean exited with code 1
1
unsolved goals
1
tauto failed to solve some goals.
1
linter Mathlib.TacticAnalysis.tacticAnalysis failed: Unknown constant _private.Mathlib.Algebra.Module.LocalizedModule.Basic.0.LocalizedModule.mul_smul_aux._simp_1_2
Warning description
94
grind failed where tauto succeeded.
37
lia failed where omega succeeded.
26
grind failed where linarith succeeded.
20
grind failed where ring succeeded.
Mathlib's nightly-testing branch (ba30ccc5be6e8b064adc3772b7e22119bb9f4fc4 ) regression run completed .
Warnings: 280
Error description
3
error: Lean exited with code 1
1
linter Mathlib.TacticAnalysis.tacticAnalysis failed: Unknown constant _private.Mathlib.Analysis.Normed.Operator.Basic.0.ContinuousLinearMap.uniformity_eq_seminorm._simp_1_6
1
linter Mathlib.TacticAnalysis.tacticAnalysis failed: Unknown constant _private.Mathlib.Analysis.Normed.Module.Multilinear.Basic.0.ContinuousMultilinearMap.uniformity_eq_seminorm._simp_1_8
1
linter Mathlib.TacticAnalysis.tacticAnalysis failed: Unknown constant _private.Mathlib.Algebra.Module.LocalizedModule.Basic.0.LocalizedModule.mul_smul_aux._simp_1_2
Warning description
107
grind failed where linarith succeeded.
102
grind failed where tauto succeeded.
39
lia failed where omega succeeded.
30
grind failed where ring succeeded.
2
original tactic 'linarith' failed: linarith failed to find a contradiction
Mathlib's nightly-testing branch (2d4b102baef1d6e148e0650b14e9fd32c3471d6a ) regression run completed .
Warnings: 280
Error description
3
error: Lean exited with code 1
1
linter Mathlib.TacticAnalysis.tacticAnalysis failed: Unknown constant _private.Mathlib.Analysis.Normed.Operator.Basic.0.ContinuousLinearMap.uniformity_eq_seminorm._simp_1_6
1
linter Mathlib.TacticAnalysis.tacticAnalysis failed: Unknown constant _private.Mathlib.Analysis.Normed.Module.Multilinear.Basic.0.ContinuousMultilinearMap.uniformity_eq_seminorm._simp_1_8
1
linter Mathlib.TacticAnalysis.tacticAnalysis failed: Unknown constant _private.Mathlib.Algebra.Module.LocalizedModule.Basic.0.LocalizedModule.mul_smul_aux._simp_1_2
Warning description
107
grind failed where linarith succeeded.
102
grind failed where tauto succeeded.
39
lia failed where omega succeeded.
30
grind failed where ring succeeded.
2
original tactic 'linarith' failed: linarith failed to find a contradiction
Mathlib's nightly-testing branch (03d33bda9f269145a3e31ef1971e4f7d8e922a4f ) regression run completed .
Warnings: 280
Error description
3
error: Lean exited with code 1
1
linter Mathlib.TacticAnalysis.tacticAnalysis failed: Unknown constant _private.Mathlib.Analysis.Normed.Operator.Basic.0.ContinuousLinearMap.uniformity_eq_seminorm._simp_1_6
1
linter Mathlib.TacticAnalysis.tacticAnalysis failed: Unknown constant _private.Mathlib.Analysis.Normed.Module.Multilinear.Basic.0.ContinuousMultilinearMap.uniformity_eq_seminorm._simp_1_8
1
linter Mathlib.TacticAnalysis.tacticAnalysis failed: Unknown constant _private.Mathlib.Algebra.Module.LocalizedModule.Basic.0.LocalizedModule.mul_smul_aux._simp_1_2
Warning description
107
grind failed where linarith succeeded.
102
grind failed where tauto succeeded.
39
lia failed where omega succeeded.
30
grind failed where ring succeeded.
2
original tactic 'linarith' failed: linarith failed to find a contradiction
Mathlib's nightly-testing branch (371eac11c8972082312234185a2467147004d12e ) regression run completed .
Warnings: 280
Error description
3
error: Lean exited with code 1
1
linter Mathlib.TacticAnalysis.tacticAnalysis failed: Unknown constant _private.Mathlib.Analysis.Normed.Operator.Basic.0.ContinuousLinearMap.uniformity_eq_seminorm._simp_1_6
1
linter Mathlib.TacticAnalysis.tacticAnalysis failed: Unknown constant _private.Mathlib.Analysis.Normed.Module.Multilinear.Basic.0.ContinuousMultilinearMap.uniformity_eq_seminorm._simp_1_8
1
linter Mathlib.TacticAnalysis.tacticAnalysis failed: Unknown constant _private.Mathlib.Algebra.Module.LocalizedModule.Basic.0.LocalizedModule.mul_smul_aux._simp_1_2
Warning description
107
grind failed where linarith succeeded.
102
grind failed where tauto succeeded.
39
lia failed where omega succeeded.
30
grind failed where ring succeeded.
2
original tactic 'linarith' failed: linarith failed to find a contradiction
Mathlib's nightly-testing branch (0e01e942cf77712b3c312afb0bace9fd6fc540a9 ) regression run completed .
Warnings: 280
Error description
3
error: Lean exited with code 1
1
linter Mathlib.TacticAnalysis.tacticAnalysis failed: Unknown constant _private.Mathlib.Analysis.Normed.Operator.Basic.0.ContinuousLinearMap.uniformity_eq_seminorm._simp_1_6
1
linter Mathlib.TacticAnalysis.tacticAnalysis failed: Unknown constant _private.Mathlib.Analysis.Normed.Module.Multilinear.Basic.0.ContinuousMultilinearMap.uniformity_eq_seminorm._simp_1_8
1
linter Mathlib.TacticAnalysis.tacticAnalysis failed: Unknown constant _private.Mathlib.Algebra.Module.LocalizedModule.Basic.0.LocalizedModule.mul_smul_aux._simp_1_2
Warning description
107
grind failed where linarith succeeded.
102
grind failed where tauto succeeded.
39
lia failed where omega succeeded.
30
grind failed where ring succeeded.
2
original tactic 'linarith' failed: linarith failed to find a contradiction
Mathlib's nightly-testing branch (9b2a09389fcaff1701eed8b6196c9f1402729281 ) regression run completed .
Warnings: 280
Error description
3
error: Lean exited with code 1
1
linter Mathlib.TacticAnalysis.tacticAnalysis failed: Unknown constant _private.Mathlib.Analysis.Normed.Operator.Basic.0.ContinuousLinearMap.uniformity_eq_seminorm._simp_1_6
1
linter Mathlib.TacticAnalysis.tacticAnalysis failed: Unknown constant _private.Mathlib.Analysis.Normed.Module.Multilinear.Basic.0.ContinuousMultilinearMap.uniformity_eq_seminorm._simp_1_8
1
linter Mathlib.TacticAnalysis.tacticAnalysis failed: Unknown constant _private.Mathlib.Algebra.Module.LocalizedModule.Basic.0.LocalizedModule.mul_smul_aux._simp_1_2
Warning description
107
grind failed where linarith succeeded.
102
grind failed where tauto succeeded.
39
lia failed where omega succeeded.
30
grind failed where ring succeeded.
2
original tactic 'linarith' failed: linarith failed to find a contradiction
Mathlib's nightly-testing branch (e0e4b3764f55ff95f4c6fb9dc2178cb528baafa3 ) regression run completed .
Warnings: 280
Error description
3
error: Lean exited with code 1
1
linter Mathlib.TacticAnalysis.tacticAnalysis failed: Unknown constant _private.Mathlib.Analysis.Normed.Operator.Basic.0.ContinuousLinearMap.uniformity_eq_seminorm._simp_1_6
1
linter Mathlib.TacticAnalysis.tacticAnalysis failed: Unknown constant _private.Mathlib.Analysis.Normed.Module.Multilinear.Basic.0.ContinuousMultilinearMap.uniformity_eq_seminorm._simp_1_8
1
linter Mathlib.TacticAnalysis.tacticAnalysis failed: Unknown constant _private.Mathlib.Algebra.Module.LocalizedModule.Basic.0.LocalizedModule.mul_smul_aux._simp_1_2
Warning description
107
grind failed where linarith succeeded.
102
grind failed where tauto succeeded.
39
lia failed where omega succeeded.
30
grind failed where ring succeeded.
2
original tactic 'linarith' failed: linarith failed to find a contradiction
Mathlib's nightly-testing branch (6cda3b4ae49ccfb8af631b143404895d3637bdf7 ) regression run completed .
Warnings: 267
Error description
3
error: Lean exited with code 1
1
linter Mathlib.TacticAnalysis.tacticAnalysis failed: Unknown constant _private.Mathlib.Analysis.Normed.Operator.Basic.0.ContinuousLinearMap.uniformity_eq_seminorm._simp_1_6
1
linter Mathlib.TacticAnalysis.tacticAnalysis failed: Unknown constant _private.Mathlib.Analysis.Normed.Module.Multilinear.Basic.0.ContinuousMultilinearMap.uniformity_eq_seminorm._simp_1_8
1
linter Mathlib.TacticAnalysis.tacticAnalysis failed: Unknown constant _private.Mathlib.Algebra.Module.LocalizedModule.Basic.0.LocalizedModule.mul_smul_aux._simp_1_2
Warning description
102
grind failed where tauto succeeded.
98
grind failed where linarith succeeded.
39
lia failed where omega succeeded.
26
grind failed where ring succeeded.
2
original tactic 'linarith' failed: linarith failed to find a contradiction
Mathlib's nightly-testing branch (819c9e30c119428cfd1a078fb77b44597e02e24f ) regression run completed .
Warnings: 265
Error description
3
error: Lean exited with code 1
1
linter Mathlib.TacticAnalysis.tacticAnalysis failed: Unknown constant _private.Mathlib.Analysis.Normed.Operator.Basic.0.ContinuousLinearMap.uniformity_eq_seminorm._simp_1_6
1
linter Mathlib.TacticAnalysis.tacticAnalysis failed: Unknown constant _private.Mathlib.Analysis.Normed.Module.Multilinear.Basic.0.ContinuousMultilinearMap.uniformity_eq_seminorm._simp_1_8
1
linter Mathlib.TacticAnalysis.tacticAnalysis failed: Unknown constant _private.Mathlib.Algebra.Module.LocalizedModule.Basic.0.LocalizedModule.mul_smul_aux._simp_1_2
Warning description
104
grind failed where tauto succeeded.
92
grind failed where linarith succeeded.
41
lia failed where omega succeeded.
26
grind failed where ring succeeded.
2
original tactic 'linarith' failed: linarith failed to find a contradiction
Mathlib's nightly-testing branch (1d00b4d59cb464d6d4bcb213b54f4328b743a32d ) regression run completed .
Warnings: 265
Error description
3
error: Lean exited with code 1
1
linter Mathlib.TacticAnalysis.tacticAnalysis failed: Unknown constant _private.Mathlib.Analysis.Normed.Operator.Basic.0.ContinuousLinearMap.uniformity_eq_seminorm._simp_1_6
1
linter Mathlib.TacticAnalysis.tacticAnalysis failed: Unknown constant _private.Mathlib.Analysis.Normed.Module.Multilinear.Basic.0.ContinuousMultilinearMap.uniformity_eq_seminorm._simp_1_8
1
linter Mathlib.TacticAnalysis.tacticAnalysis failed: Unknown constant _private.Mathlib.Algebra.Module.LocalizedModule.Basic.0.LocalizedModule.mul_smul_aux._simp_1_2
Warning description
104
grind failed where tauto succeeded.
92
grind failed where linarith succeeded.
41
lia failed where omega succeeded.
26
grind failed where ring succeeded.
2
original tactic 'linarith' failed: linarith failed to find a contradiction
Mathlib's nightly-testing branch (41366a77a05165b3313523d07b2e4710142426c2 ) regression run completed .
Warnings: 173
Error description
3
error: Lean exited with code 1
1
linter Mathlib.TacticAnalysis.tacticAnalysis failed: Unknown constant _private.Mathlib.Analysis.Normed.Operator.Basic.0.ContinuousLinearMap.uniformity_eq_seminorm._simp_1_6
1
linter Mathlib.TacticAnalysis.tacticAnalysis failed: Unknown constant _private.Mathlib.Analysis.Normed.Module.Multilinear.Basic.0.ContinuousMultilinearMap.uniformity_eq_seminorm._simp_1_8
1
linter Mathlib.TacticAnalysis.tacticAnalysis failed: Unknown constant _private.Mathlib.Algebra.Module.LocalizedModule.Basic.0.LocalizedModule.mul_smul_aux._simp_1_2
Warning description
104
grind failed where tauto succeeded.
41
lia failed where omega succeeded.
26
grind failed where ring succeeded.
2
grind failed where linarith succeeded.
:tada:
2 grind failed where linarith succeeded.
Almost there!
Mathlib's nightly-testing branch (581e65392b3f3c7490f7c659ed743b2fa4a669d2 ) regression run completed .
Warnings: 173
Error description
3
error: Lean exited with code 1
1
linter Mathlib.TacticAnalysis.tacticAnalysis failed: Unknown constant _private.Mathlib.Analysis.Normed.Operator.Basic.0.ContinuousLinearMap.uniformity_eq_seminorm._simp_1_6
1
linter Mathlib.TacticAnalysis.tacticAnalysis failed: Unknown constant _private.Mathlib.Analysis.Normed.Module.Multilinear.Basic.0.ContinuousMultilinearMap.uniformity_eq_seminorm._simp_1_8
1
linter Mathlib.TacticAnalysis.tacticAnalysis failed: Unknown constant _private.Mathlib.Algebra.Module.LocalizedModule.Basic.0.LocalizedModule.mul_smul_aux._simp_1_2
Warning description
104
grind failed where tauto succeeded.
41
lia failed where omega succeeded.
26
grind failed where ring succeeded.
2
grind failed where linarith succeeded.
Mathlib's nightly-testing branch (34f9d35c1e2d6467d3ecc1f42722a762a912fb67 ) regression run completed .
Warnings: 173
Error description
3
error: Lean exited with code 1
1
linter Mathlib.TacticAnalysis.tacticAnalysis failed: Unknown constant _private.Mathlib.Analysis.Normed.Operator.Basic.0.ContinuousLinearMap.uniformity_eq_seminorm._simp_1_6
1
linter Mathlib.TacticAnalysis.tacticAnalysis failed: Unknown constant _private.Mathlib.Analysis.Normed.Module.Multilinear.Basic.0.ContinuousMultilinearMap.uniformity_eq_seminorm._simp_1_8
1
linter Mathlib.TacticAnalysis.tacticAnalysis failed: Unknown constant _private.Mathlib.Algebra.Module.LocalizedModule.Basic.0.LocalizedModule.mul_smul_aux._simp_1_2
Warning description
104
grind failed where tauto succeeded.
41
lia failed where omega succeeded.
26
grind failed where ring succeeded.
2
grind failed where linarith succeeded.
Last updated: Dec 20 2025 at 21:32 UTC