[Merged by Bors] - chore: move to v4.11.0-rc2 (new `variable` command) by kim-em · Pull Request #15726 · leanprover-community/mathlib4

kim-em · 2024-08-12T10:16:34Z

No description provided.

Co-authored-by: leanprover-community-mathlib4-bot <leanprover-community-mathlib4-bot@users.noreply.github.com> Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com>

Co-authored-by: leanprover-community-mathlib4-bot <leanprover-community-mathlib4-bot@users.noreply.github.com> Co-authored-by: Johan Commelin <johan@commelin.net> Co-authored-by: Kyle Miller <kmill31415@gmail.com> Co-authored-by: Joachim Breitner <mail@joachim-breitner.de> Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com>

jcommelin · 2024-08-12T15:01:45Z

bors merge

Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com> Co-authored-by: Tomáš Skřivan <skrivantomas@seznam.cz> Co-authored-by: mathlib-bors <150093616+mathlib-bors@users.noreply.github.com>

jcommelin · 2024-08-12T15:03:46Z

bors r-

needs merging master, @edegeltje is working on it

mathlib-bors · 2024-08-12T15:03:48Z

Canceled.

edegeltje · 2024-08-12T15:27:38Z

@jcommelin build succeeded, it should be ready to be merged

test/fun_prop_dev.lean

jcommelin · 2024-08-12T18:29:29Z

bors merge

Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com> Co-authored-by: Blizzard_inc <thrashy4inbox@gmail.com> Co-authored-by: Jeremy Tan Jie Rui <reddeloostw@gmail.com> Co-authored-by: Parcly Taxel <reddeloostw@gmail.com> Co-authored-by: Tomáš Skřivan <skrivantomas@seznam.cz> Co-authored-by: mathlib-bors <150093616+mathlib-bors@users.noreply.github.com>

mathlib-bors · 2024-08-12T19:34:12Z

Pull request successfully merged into master.

Build succeeded:

YaelDillies · 2024-08-13T19:00:05Z

Mathlib/Algebra/Homology/HomotopyCofiber.lean

 /-- If a functor inverts homotopy equivalences, it sends homotopic maps to the same map. -/
 lemma _root_.Homotopy.map_eq_of_inverts_homotopyEquivalences
-    {φ₀ φ₁ : F ⟶ G} (h : Homotopy φ₀ φ₁) (hc : ∀ j, ∃ i, c.Rel i j)
+    {φ₀ φ₁ : F ⟶ G} (h : Homotopy φ₀ φ₁)(hc : ∀ j, ∃ i, c.Rel i j)


Suggested change

{φ₀ φ₁ : F ⟶ G} (h : Homotopy φ₀ φ₁)(hc : ∀ j, ∃ i, c.Rel i j)

{φ₀ φ₁ : F ⟶ G} (h : Homotopy φ₀ φ₁) (hc : ∀ j, ∃ i, c.Rel i j)

Found by a linter in #10235 Mostly repeats #15306 accidentally reverted by #15726

@grunweg

Found by a linter in #10235 Mostly repeats @grunweg's #15306 accidentally reverted by @semorrison's #15726

Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com> Co-authored-by: Blizzard_inc <thrashy4inbox@gmail.com> Co-authored-by: Jeremy Tan Jie Rui <reddeloostw@gmail.com> Co-authored-by: Parcly Taxel <reddeloostw@gmail.com> Co-authored-by: Tomáš Skřivan <skrivantomas@seznam.cz> Co-authored-by: mathlib-bors <150093616+mathlib-bors@users.noreply.github.com>

@grunweg

Found by a linter in #10235 Mostly repeats @grunweg's #15306 accidentally reverted by @semorrison's #15726

Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com> Co-authored-by: Blizzard_inc <thrashy4inbox@gmail.com> Co-authored-by: Jeremy Tan Jie Rui <reddeloostw@gmail.com> Co-authored-by: Parcly Taxel <reddeloostw@gmail.com> Co-authored-by: Tomáš Skřivan <skrivantomas@seznam.cz> Co-authored-by: mathlib-bors <150093616+mathlib-bors@users.noreply.github.com>

@grunweg

Found by a linter in #10235 Mostly repeats @grunweg's #15306 accidentally reverted by @semorrison's #15726

Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com> Co-authored-by: Blizzard_inc <thrashy4inbox@gmail.com> Co-authored-by: Jeremy Tan Jie Rui <reddeloostw@gmail.com> Co-authored-by: Parcly Taxel <reddeloostw@gmail.com> Co-authored-by: Tomáš Skřivan <skrivantomas@seznam.cz> Co-authored-by: mathlib-bors <150093616+mathlib-bors@users.noreply.github.com>

@grunweg

Found by a linter in #10235 Mostly repeats @grunweg's #15306 accidentally reverted by @semorrison's #15726

kim-em and others added 30 commits July 31, 2024 12:57

fix

8f10520

add adaptation note

d221414

chore: backports for leanprover/lean4#4814 (part 9)

9dbbe80

unused argument

1081025

fix

92a571a

Merge master into nightly-testing

6a3f369

Apply suggestions from code review

958f26d

Merge branch 'bump/nightly-2024-07-29' into nightly-testing

d1b73dc

chore: adaptations for nightly-2024-07-29 (#15282)

f2795de

Co-authored-by: leanprover-community-mathlib4-bot <leanprover-community-mathlib4-bot@users.noreply.github.com> Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com>

Merge master into nightly-testing

8ad1f5e

adjust batteries

98f621f

adjust batteries

53e8b2a

merge master

5392584

Merge master into nightly-testing

948db9a

fix

a0929e0

fix test output

1a1947a

fix test output

793914f

fix test

69240a8

Merge remote-tracking branch 'origin/master' into variables_backports_6

ada4ab5

shake

6c957c7

tidy

0092c2a

Merge master into nightly-testing

4b15042

merge master

402b37f

chore: adaptations for nightly-2024-07-31

a4ae9d4

merge nightly-testing

71f48af

fixes

1caee5d

Trigger CI for leanprover/lean4#4814

cc43e6f

Merge master into nightly-testing

fcfba44

Merge master into nightly-testing

2c2f8fd

fix square preserving limits

e108ded

hopefully final(?) fixes

b05d2a1

Parcly-Taxel added 5 commits August 12, 2024 23:45

Merge branch 'master' into bump_to_v4.11.0-rc2

b80ee13

Merge branch 'master' into bump_to_v4.11.0-rc2

ac1c7f5

restore fun_prop_dev

2f4a409

yoink

e02119c

restore as much of this file as possible

ab82de5

jcommelin reviewed Aug 12, 2024

View reviewed changes

test/fun_prop_dev.lean Outdated Show resolved Hide resolved

test/fun_prop_dev.lean Outdated Show resolved Hide resolved

test/fun_prop_dev.lean Outdated Show resolved Hide resolved

address review comments

1fa571e

mathlib-bors bot changed the title ~~chore: move to v4.11.0-rc2 (new variable command)~~ [Merged by Bors] - chore: move to v4.11.0-rc2 (new variable command) Aug 12, 2024

mathlib-bors bot closed this Aug 12, 2024

mathlib-bors bot deleted the bump_to_v4.11.0-rc2 branch August 12, 2024 19:34

YaelDillies reviewed Aug 13, 2024

View reviewed changes

urkud added a commit that referenced this pull request Aug 23, 2024

chore(SimpleGraph): fix DecidableEq/Fintype assumptions

948aa5b

Found by a linter in #10235 Mostly repeats #15306 accidentally reverted by #15726

urkud mentioned this pull request Aug 23, 2024

[Merged by Bors] - chore(SimpleGraph): fix DecidableEq/Fintype assumptions #16079

Closed

mathlib-bors bot pushed a commit that referenced this pull request Aug 23, 2024

chore(SimpleGraph): fix DecidableEq/Fintype assumptions (#16079)

08b234f

Found by a linter in #10235 Mostly repeats @grunweg's #15306 accidentally reverted by @semorrison's #15726

bjoernkjoshanssen pushed a commit that referenced this pull request Sep 9, 2024

chore(SimpleGraph): fix DecidableEq/Fintype assumptions (#16079)

39b95f4

Found by a linter in #10235 Mostly repeats @grunweg's #15306 accidentally reverted by @semorrison's #15726

bjoernkjoshanssen pushed a commit that referenced this pull request Sep 9, 2024

chore(SimpleGraph): fix DecidableEq/Fintype assumptions (#16079)

3185f0f

Found by a linter in #10235 Mostly repeats @grunweg's #15306 accidentally reverted by @semorrison's #15726

bjoernkjoshanssen pushed a commit that referenced this pull request Sep 12, 2024

chore(SimpleGraph): fix DecidableEq/Fintype assumptions (#16079)

ef2436c

Found by a linter in #10235 Mostly repeats @grunweg's #15306 accidentally reverted by @semorrison's #15726

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[Merged by Bors] - chore: move to v4.11.0-rc2 (new `variable` command)#15726

[Merged by Bors] - chore: move to v4.11.0-rc2 (new `variable` command)#15726
kim-em wants to merge 1728 commits intomasterfrom
bump_to_v4.11.0-rc2

kim-em commented Aug 12, 2024 •

edited by mathlib-bors bot

Loading

Uh oh!

jcommelin commented Aug 12, 2024

Uh oh!

jcommelin commented Aug 12, 2024

Uh oh!

mathlib-bors bot commented Aug 12, 2024

Uh oh!

edegeltje commented Aug 12, 2024

Uh oh!

Uh oh!

Uh oh!

Uh oh!

jcommelin commented Aug 12, 2024

Uh oh!

mathlib-bors bot commented Aug 12, 2024

Uh oh!

YaelDillies Aug 13, 2024

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

12 participants

	{φ₀ φ₁ : F ⟶ G} (h : Homotopy φ₀ φ₁)(hc : ∀ j, ∃ i, c.Rel i j)
	{φ₀ φ₁ : F ⟶ G} (h : Homotopy φ₀ φ₁) (hc : ∀ j, ∃ i, c.Rel i j)

Conversation

kim-em commented Aug 12, 2024 • edited by mathlib-bors bot Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

jcommelin commented Aug 12, 2024

Uh oh!

jcommelin commented Aug 12, 2024

Uh oh!

mathlib-bors bot commented Aug 12, 2024

Uh oh!

edegeltje commented Aug 12, 2024

Uh oh!

Uh oh!

Uh oh!

Uh oh!

jcommelin commented Aug 12, 2024

Uh oh!

mathlib-bors bot commented Aug 12, 2024

Uh oh!

YaelDillies Aug 13, 2024

Choose a reason for hiding this comment

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

12 participants

kim-em commented Aug 12, 2024 •

edited by mathlib-bors bot

Loading