chore: adaptations for nightly-2024-02-26 by kim-em · Pull Request #10995 · leanprover-community/mathlib4

kim-em · 2024-02-27T02:32:31Z

No description provided.

Archive/Examples/IfNormalization/Result.lean

Co-authored-by: Patrick Massot <patrickmassot@free.fr> Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

Mathlib/Algebra/ContinuedFractions/Computation/CorrectnessTerminating.lean

Mathlib/Algebra/Homology/ShortComplex/Homology.lean

Mathlib/Algebra/Order/Group/Abs.lean

Mathlib/Analysis/BoxIntegral/Partition/Filter.lean

Mathlib/Data/Set/Finite.lean

Mathlib/Data/UnionFind.lean

Mathlib/FieldTheory/SeparableDegree.lean

Mathlib/LinearAlgebra/FreeModule/Norm.lean

Mathlib/Order/Booleanisation.lean

Mathlib/RingTheory/Polynomial/ScaleRoots.lean

Mathlib/SetTheory/Cardinal/Cofinality.lean

Mathlib/Topology/MetricSpace/Completion.lean

test/meta.lean

Mathlib/LinearAlgebra/PiTensorProduct.lean

Mathlib/Order/Booleanisation.lean

Mathlib/Order/Closure.lean

Mathlib/RingTheory/Polynomial/ScaleRoots.lean

test/FBinop.lean

Mathlib/Algebra/Homology/Augment.lean

Mathlib/Algebra/GroupWithZero/Units/Basic.lean

Mathlib/Algebra/ContinuedFractions/Computation/CorrectnessTerminating.lean

Mathlib/Algebra/Homology/HomotopyCategory/Pretriangulated.lean

Mathlib/Algebra/Order/Ring/Defs.lean

Mathlib/CategoryTheory/Category/Basic.lean

Mathlib/CategoryTheory/GradedObject/Trifunctor.lean

Mathlib/Data/Erased.lean

Mathlib/Data/Fintype/Order.lean

mattrobball · 2024-02-28T01:08:33Z

Mathlib/RingTheory/Polynomial/ScaleRoots.lean

  ext n; simp only [coeff_smul, coeff_scaleRoots, coeff_add, smul_eq_mul,
-    mul_comm (r ^ _), mul_assoc, ← pow_add, ← h, ← add_mul, add_comm (_ - n)]
+    mul_comm (r ^ _), ← pow_add, ← h, ← add_mul, add_comm (_ - n)]
+  rw [mul_assoc, ← pow_add]


Why do these not fire in simp now?

They do fire, but mul_assoc induces a max rec depth error.

I've added an "adaptation note" explaining this, but am inclined to ship.

mattrobball

Good with me

Co-authored-by: Patrick Massot <patrickmassot@free.fr> Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

chore: adaptations for nightly-2024-02-26

00d9ad8

kim-em commented Feb 27, 2024

View reviewed changes

Archive/Examples/IfNormalization/Result.lean Outdated Show resolved Hide resolved

Merge branch 'bump/v4.7.0' into bump/nightly-2024-02-26

04fe12f

kim-em changed the base branch from bump/v4.7.0 to master February 27, 2024 04:22

kim-em changed the base branch from master to bump/v4.7.0 February 27, 2024 04:23

kim-em added a commit that referenced this pull request Feb 27, 2024

chore: more backport of simp changes from #10995

0cba88b

mathlib-bors bot pushed a commit that referenced this pull request Feb 27, 2024

chore: more backporting of simp changes from #10995 (#11001)

d9589c1

Co-authored-by: Patrick Massot <patrickmassot@free.fr> Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

merge bump/v4.7.0

355aed2

kim-em commented Feb 27, 2024

View reviewed changes

Mathlib/Algebra/ContinuedFractions/Computation/CorrectnessTerminating.lean Outdated Show resolved Hide resolved

kim-em commented Feb 27, 2024

View reviewed changes

Mathlib/Algebra/Homology/ShortComplex/Homology.lean Outdated Show resolved Hide resolved

kim-em and others added 2 commits February 27, 2024 21:30

Update Mathlib/Algebra/Homology/ShortComplex/Homology.lean

9d00195

fix merge

55765ba

kim-em commented Feb 27, 2024

View reviewed changes

Mathlib/Algebra/Order/Group/Abs.lean Outdated Show resolved Hide resolved

kim-em commented Feb 27, 2024

View reviewed changes

Mathlib/Analysis/BoxIntegral/Partition/Filter.lean Outdated Show resolved Hide resolved

Update Mathlib/Analysis/BoxIntegral/Partition/Filter.lean

5406698

kim-em commented Feb 27, 2024

View reviewed changes

Mathlib/Data/Set/Finite.lean Outdated Show resolved Hide resolved

kim-em commented Feb 27, 2024

View reviewed changes

Mathlib/Data/UnionFind.lean Outdated Show resolved Hide resolved

kim-em commented Feb 27, 2024

View reviewed changes

Mathlib/FieldTheory/SeparableDegree.lean Outdated Show resolved Hide resolved

kim-em commented Feb 27, 2024

View reviewed changes

Mathlib/LinearAlgebra/FreeModule/Norm.lean Outdated Show resolved Hide resolved

kim-em commented Feb 27, 2024

View reviewed changes

Mathlib/Order/Booleanisation.lean Outdated Show resolved Hide resolved

kim-em commented Feb 27, 2024

View reviewed changes

Mathlib/RingTheory/Polynomial/ScaleRoots.lean Outdated Show resolved Hide resolved

kim-em commented Feb 27, 2024

View reviewed changes

Mathlib/SetTheory/Cardinal/Cofinality.lean Show resolved Hide resolved

kim-em commented Feb 27, 2024

View reviewed changes

Mathlib/Topology/MetricSpace/Completion.lean Outdated Show resolved Hide resolved

kim-em commented Feb 27, 2024

View reviewed changes

test/meta.lean Show resolved Hide resolved

Vierkantor added 6 commits February 27, 2024 11:36

Revert SeparableDegree changes

7fdbd6d

Revert LinearAlgebra/FreeModule/Norm.lean

a019013

Actually fix FieldTheory/SeparableDegree.lean now!

70a45c2

Fix ContinuedFractions

b730503

aesop can unfold let-definitions passed to simp rules

2530226

Fix Order/CompactlyGenerated/Basic.lean

bb1d12e

kim-em added 2 commits February 28, 2024 11:22

cleanup comment

1040153

proper fix for IfNormalization

14b1f19

kim-em commented Feb 28, 2024

View reviewed changes

Mathlib/LinearAlgebra/PiTensorProduct.lean Show resolved Hide resolved

kim-em commented Feb 28, 2024

View reviewed changes

Mathlib/Order/Booleanisation.lean Outdated Show resolved Hide resolved

kim-em commented Feb 28, 2024

View reviewed changes

Mathlib/Order/Closure.lean Outdated Show resolved Hide resolved

kim-em commented Feb 28, 2024

View reviewed changes

Mathlib/RingTheory/Polynomial/ScaleRoots.lean Outdated Show resolved Hide resolved

kim-em commented Feb 28, 2024

View reviewed changes

test/FBinop.lean Outdated Show resolved Hide resolved

kim-em added 2 commits February 28, 2024 11:37

fix

c7ed7a5

cleanuo

0828bff

kim-em commented Feb 28, 2024

View reviewed changes

Mathlib/Algebra/Homology/Augment.lean Show resolved Hide resolved

Apply suggestions from code review

487f1c6

kim-em commented Feb 28, 2024

View reviewed changes

Mathlib/Algebra/Homology/Augment.lean Show resolved Hide resolved

two fixes with spread notation

cfe5e45

mattrobball reviewed Feb 28, 2024

View reviewed changes

kim-em added 3 commits February 28, 2024 12:37

document zetaDelta in aesop_cat

ca1f686

unwrap

d853139

add note

1a58134

mattrobball approved these changes Feb 28, 2024

View reviewed changes

kmill approved these changes Feb 28, 2024

View reviewed changes

kmill added 5 commits February 27, 2024 18:36

fix

026781a

fix archive

f03d9ba

test fixes

5f2060f

test fix again

9ad98ae

shake

e35d61e

kmill merged commit b700984 into bump/v4.7.0 Feb 28, 2024

mathlib-bors bot deleted the bump/nightly-2024-02-26 branch February 28, 2024 05:08

riccardobrasca pushed a commit that referenced this pull request Mar 1, 2024

chore: more backporting of simp changes from #10995 (#11001)

052bc52

Co-authored-by: Patrick Massot <patrickmassot@free.fr> Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

kbuzzard pushed a commit that referenced this pull request Mar 12, 2024

chore: more backporting of simp changes from #10995 (#11001)

7fd0498

Co-authored-by: Patrick Massot <patrickmassot@free.fr> Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

dagurtomas pushed a commit that referenced this pull request Mar 22, 2024

chore: more backporting of simp changes from #10995 (#11001)

66c0098

Co-authored-by: Patrick Massot <patrickmassot@free.fr> Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

xgenereux pushed a commit that referenced this pull request Apr 15, 2024

chore: more backporting of simp changes from #10995 (#11001)

fbfd450

Co-authored-by: Patrick Massot <patrickmassot@free.fr> Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

Conversation

kim-em commented Feb 27, 2024

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

mattrobball Feb 28, 2024

Choose a reason for hiding this comment

Uh oh!

kim-em Feb 28, 2024

Choose a reason for hiding this comment

Uh oh!

mattrobball left a comment

Choose a reason for hiding this comment

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

5 participants