fix Mathlib/Data/List/EditDistance/Estimator.lean #196089
Annotations
10 errors
|
Build:
Mathlib/Algebra/BigOperators/Group/Finset/Basic.lean#L73
@Finset.sum_image Left-hand side does not simplify, when using the simp lemma on itself.
|
|
Build:
Mathlib/Algebra/BigOperators/Group/Finset/Basic.lean#L73
@Finset.prod_image Left-hand side does not simplify, when using the simp lemma on itself.
|
|
Build:
Mathlib/Algebra/Group/Submonoid/Basic.lean#L305
@AddSubmonoid.closure_sdiff_eq_closure Left-hand side does not simplify, when using the simp lemma on itself.
|
|
Build:
Mathlib/Algebra/Group/Submonoid/Basic.lean#L305
@Submonoid.closure_sdiff_eq_closure Left-hand side does not simplify, when using the simp lemma on itself.
|
|
Build:
Mathlib/Algebra/GroupWithZero/Basic.lean#L265
@inv_mul_cancel_right₀ simp can prove this:
|
|
Build:
Mathlib/Algebra/GroupWithZero/Basic.lean#L272
@inv_mul_cancel_left₀ simp can prove this:
|
|
Build:
Mathlib/Algebra/GroupWithZero/Defs.lean#L208
@mul_inv_cancel₀ simp can prove this:
|
|
Build:
Mathlib/Algebra/GroupWithZero/Defs.lean#L235
@mul_inv_cancel_right₀ simp can prove this:
|
|
Build:
Mathlib/Algebra/GroupWithZero/Defs.lean#L241
@mul_inv_cancel_left₀ simp can prove this:
|
|
Build:
Mathlib/Algebra/GroupWithZero/NeZero.lean#L51
@inv_mul_cancel₀ simp can prove this:
|
Artifacts
Produced during runtime
| Name | Size | Digest | |
|---|---|---|---|
|
import-graph
Expired
|
225 KB |
sha256:fcc09226f916a85240607bab071744da10444c99d5a5ac080cf498d7a91b615c
|
|