Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

chore: upstream classical tactic #242

Merged
merged 15 commits into from
Jan 27, 2024
Merged

chore: upstream classical tactic #242

merged 15 commits into from
Jan 27, 2024

Conversation

kim-em
Copy link
Collaborator

@kim-em kim-em commented Sep 6, 2023 •
edited
Loading

No description provided.

@kim-em kim-em added awaiting-review This PR is ready for review; the author thinks it is ready to be merged. depends on another PR This is stacked on top of another Batteries PR. labels Sep 6, 2023
@kim-em kim-em mentioned this pull request Sep 6, 2023
Closed
2 tasks
@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot added the merge-conflict This PR has merge conflicts with the `main` branch which must be resolved by the author. label Sep 13, 2023
@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot removed the merge-conflict This PR has merge conflicts with the `main` branch which must be resolved by the author. label Sep 14, 2023
@fgdorais
Copy link
Collaborator

fgdorais commented Nov 7, 2023

Does this really depend on #241? I think it could be made to do without.

@kim-em
Copy link
Collaborator Author

kim-em commented Nov 7, 2023

Does this really depend on #241? I think it could be made to do without.

I was not anticipating this being nearly as slow; I thought when I started that both of these PRs would be merged 30 minutes-hours later, but here we are 60 days later.

Yes, the only "dependence" is through a test.

@kim-em
Copy link
Collaborator Author

kim-em commented Nov 7, 2023

This PR is not essential for anything I'm doing in the short term; if you'd like to disentangle them please do!

@fgdorais fgdorais mentioned this pull request Nov 7, 2023
Merged
fgdorais
fgdorais approved these changes Nov 7, 2023
View reviewed changes
Copy link
Collaborator

@fgdorais fgdorais left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Looks good to me modulo the question about the FIXME.

Std/Tactic/Classical.lean
Comment on lines +45 to +46
-- FIXME: using ppDedent looks good in the common case, but produces the incorrect result when
-- the `classical` does not scope over the rest of the block.
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Can this be fixed in this PR?

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

No, it would require core changes, the necessary formatting combinator doesn't exist.

@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot added the merge-conflict This PR has merge conflicts with the `main` branch which must be resolved by the author. label Nov 20, 2023
@kim-em kim-em removed the merge-conflict This PR has merge conflicts with the `main` branch which must be resolved by the author. label Nov 26, 2023
@kim-em kim-em removed the depends on another PR This is stacked on top of another Batteries PR. label Dec 10, 2023
@joehendrix joehendrix removed the awaiting-review This PR is ready for review; the author thinks it is ready to be merged. label Jan 25, 2024
@joehendrix joehendrix added the will-merge-soon PR will be merged soon. Any concerns should be raised quickly. label Jan 25, 2024
@digama0 digama0 merged commit 92fb0a9 into leanprover-community:main Jan 27, 2024
1 check passed
kim-em added a commit to leanprover-community/mathlib4 that referenced this pull request Jan 29, 2024
@kim-em
chore: bump Std to leanprover-community/batteries#242
14c6661
mathlib-bors bot pushed a commit to leanprover-community/mathlib4 that referenced this pull request Jan 30, 2024
@kim-em
chore: bump Std to leanprover-community/batteries#242 (#10104)
d3a6c9f 
Co-authored-by: Scott Morrison <[email protected]>
winstonyin added a commit to leanprover-community/mathlib4 that referenced this pull request Jan 30, 2024
@winstonyin
Squashed commit of the following:
c03f829 
commit 4fcf5bd
Author: Scott Morrison <[email protected]>
Date:   Tue Jan 30 04:00:55 2024 +0000

    chore: bump Std to leanprover-community/batteries#566 (#10117)

    Co-authored-by: Scott Morrison <[email protected]>

commit 99afa84
Author: Yury G. Kudryashov <[email protected]>
Date:   Tue Jan 30 02:26:17 2024 +0000

    feat(Logic/Embedding): add a lemma (#10096)

    * Make `Function.Embedding.setValue_eq` a `simp` lemma.
    * Add `Function.Embedding.setValue_eq_iff`.

commit 41e0da3
Author: David Renshaw <[email protected]>
Date:   Tue Jan 30 02:26:16 2024 +0000

    fix: use getTransparency in librarySearch SolveByElim.Config (#10052)

commit 9cc09f6
Author: Yury G. Kudryashov <[email protected]>
Date:   Tue Jan 30 02:26:15 2024 +0000

    chore(WithTop): less abuse of defeq to `Option _` (#9986)

    Also reuse proofs here and there.

commit 15e555e
Author: Heather Macbeth <[email protected]>
Date:   Tue Jan 30 02:26:14 2024 +0000

    feat: characterize "eventually" in a subtype (#7568)

    Co-authored-by: Anatole Dedecker <[email protected]>
    Co-authored-by: ADedecker <[email protected]>

commit d3a6c9f
Author: Scott Morrison <[email protected]>
Date:   Tue Jan 30 01:07:06 2024 +0000

    chore: bump Std to leanprover-community/batteries#242 (#10104)

    Co-authored-by: Scott Morrison <[email protected]>

commit 132e511
Author: Winston Yin <[email protected]>
Date:   Tue Jan 30 00:03:21 2024 +0000

    feat: Integral curves are either injective or periodic (#9343)

    Integral curves are either injective, constant, or periodic and non-constant.

    When we have notions of submanifolds, this'll be useful for showing that the image of an integral curve is a submanifold.

    - [x] depends on: #8886

    Co-authored-by: Yury G. Kudryashov <[email protected]>
    Co-authored-by: Michael Rothgang <[email protected]>

commit b4d01dc
Author: Moritz Firsching <[email protected]>
Date:   Mon Jan 29 21:32:09 2024 +0000

    refactor(MeasureTheory/Function/L1Space): rm two porting notes (#10056)

    Co-authored-by: Moritz Firsching <[email protected]>

commit 7458f0e
Author: Yury G. Kudryashov <[email protected]>
Date:   Mon Jan 29 18:36:04 2024 +0000

    feat(Topology/Separation): define R₁ spaces, review API (#10085)

    - Define `R1Space`, a.k.a. preregular space.
    - Drop `T2OrLocallyCompactRegularSpace`.
    - Generalize all existing theorems
      about `T2OrLocallyCompactRegularSpace` to `R1Space`.
    - Drop the `[T2OrLocallyCompactRegularSpace _]` assumption
      if the space is known to be regular for other reason
      (e.g., because it's a topological group).

    - `Specializes.not_disjoint`:
      if `x ⤳ y`, then `𝓝 x` and `𝓝 y` aren't disjoint;
    - `specializes_iff_not_disjoint`, `Specializes.inseparable`,
      `disjoint_nhds_nhds_iff_not_inseparable`,
      `r1Space_iff_inseparable_or_disjoint_nhds`: basic API about `R1Space`s;
    - `Inducing.r1Space`, `R1Space.induced`, `R1Space.sInf`, `R1Space.iInf`,
      `R1Space.inf`, instances for `Subtype _`, `X × Y`, and `∀ i, X i`:
      basic instances for `R1Space`;
    - `IsCompact.mem_closure_iff_exists_inseparable`,
      `IsCompact.closure_eq_biUnion_inseparable`:
      characterizations of the closure of a compact set in a preregular space;
    - `Inseparable.mem_measurableSet_iff`: topologically inseparable points
      can't be separated by a Borel measurable set;
    - `IsCompact.closure_subset_measurableSet`, `IsCompact.measure_closure`:
      in a preregular space, a measurable superset of a compact set
      includes its closure as well;
      as a corollary, `closure K` has the same measure as `K`.
    - `exists_mem_nhds_isCompact_mapsTo_of_isCompact_mem_nhds`:
      an auxiliary lemma extracted from a `LocallyCompactPair` instance;
    - `IsCompact.isCompact_isClosed_basis_nhds`:
      if `x` admits a compact neighborhood,
      then it admits a basis of compact closed neighborhoods;
      in particular, a weakly locally compact preregular space
      is a locally compact regular space;
    - `isCompact_isClosed_basis_nhds`: a version of the previous theorem
      for weakly locally compact spaces;
    - `exists_mem_nhds_isCompact_isClosed`: in a locally compact regular space,
      each point admits a compact closed neighborhood.

    Some theorems about topological groups are true for any (pre)regular space,
    so we deprecate the special cases.

    - `exists_isCompact_isClosed_subset_isCompact_nhds_one`:
      use new `IsCompact.isCompact_isClosed_basis_nhds` instead;
    - `instLocallyCompactSpaceOfWeaklyOfGroup`,
      `instLocallyCompactSpaceOfWeaklyOfAddGroup`:
      are now implied by `WeaklyLocallyCompactSpace.locallyCompactSpace`;
    - `local_isCompact_isClosed_nhds_of_group`,
      `local_isCompact_isClosed_nhds_of_addGroup`:
      use `isCompact_isClosed_basis_nhds` instead;
    - `exists_isCompact_isClosed_nhds_one`, `exists_isCompact_isClosed_nhds_zero`:
      use `exists_mem_nhds_isCompact_isClosed` instead.

    For each renamed theorem, the old theorem is redefined as a deprecated alias.

    - `isOpen_setOf_disjoint_nhds_nhds`: moved to `Constructions`;
    - `isCompact_closure_of_subset_compact` -> `IsCompact.closure_of_subset`;
    - `IsCompact.measure_eq_infi_isOpen` -> `IsCompact.measure_eq_iInf_isOpen`;
    - `exists_compact_superset_iff` -> `exists_isCompact_superset_iff`;
    - `separatedNhds_of_isCompact_isCompact_isClosed` -> `SeparatedNhds.of_isCompact_isCompact_isClosed`;
    - `separatedNhds_of_isCompact_isCompact` -> `SeparatedNhds.of_isCompact_isCompact`;
    - `separatedNhds_of_finset_finset` -> `SeparatedNhds.of_finset_finset`;
    - `point_disjoint_finset_opens_of_t2` -> `SeparatedNhds.of_singleton_finset`;
    - `separatedNhds_of_isCompact_isClosed` -> `SeparatedNhds.of_isCompact_isClosed`;
    - `exists_open_superset_and_isCompact_closure` -> `exists_isOpen_superset_and_isCompact_closure`;
    - `exists_open_with_compact_closure` -> `exists_isOpen_mem_isCompact_closure`;

commit 7afbac6
Author: grunweg <[email protected]>
Date:   Mon Jan 29 17:52:04 2024 +0000

    chore(Topology/PartialHomeomorph): rename type variables (#9632)

    Greek letters are dead, long live X, Y and Z. Same procedure as in previous renames.

commit d883f18
Author: s1m7u <[email protected]>
Date:   Mon Jan 29 16:54:51 2024 +0000

    chore(Data/List/Rotate): add `@[simp]` to `rotate_replicate` (#10106)

commit 89f9777
Author: Scott Morrison <[email protected]>
Date:   Mon Jan 29 15:34:18 2024 +0000

    chore: fix Punit->PUnit in CommMon_ (#10089)

    Co-authored-by: Scott Morrison <[email protected]>

commit 00b71ef
Author: Moritz Firsching <[email protected]>
Date:   Mon Jan 29 14:47:04 2024 +0000

    refactor(Probability/Kernel/CondCdf): mv tendsto_of_antitone (#10046)

    Co-authored-by: Moritz Firsching <[email protected]>

commit 68c771a
Author: Pietro Monticone <[email protected]>
Date:   Mon Jan 29 13:56:07 2024 +0000

    doc: fix typos (#10100)

    Fix minor typos in the following files:

    - [x] `Mathlib/GroupTheory/GroupAction/Opposite.lean`
    - [x] `Mathlib/Init/Control/Lawful.lean`
    - [x] `Mathlib/ModelTheory/ElementarySubstructures.lean`
    - [x] `Mathlib/Algebra/Group/Defs.lean`
    - [x] `Mathlib/Algebra/Group/WithOne/Basic.lean`
    - [x] `Mathlib/Data/Int/Cast/Defs.lean`
    - [x] `Mathlib/LinearAlgebra/Dimension/Basic.lean`
    - [x] `Mathlib/NumberTheory/NumberField/CanonicalEmbedding.lean`
    - [x] `Mathlib/Algebra/Star/StarAlgHom.lean`
    - [x] `Mathlib/AlgebraicTopology/SimplexCategory.lean`
    - [x] `Mathlib/CategoryTheory/Abelian/Homology.lean`
    - [x] `Mathlib/CategoryTheory/Sites/Grothendieck.lean`
    - [x] `Mathlib/RingTheory/IsTensorProduct.lean`
    - [x] `Mathlib/AlgebraicTopology/DoldKan/Homotopies.lean`
    - [x] `Mathlib/AlgebraicTopology/ExtraDegeneracy.lean`
    - [x] `Mathlib/AlgebraicTopology/Nerve.lean`
    - [x] `Mathlib/AlgebraicTopology/SplitSimplicialObject.lean`
    - [x] `Mathlib/Analysis/ConstantSpeed.lean`
    - [x] `Mathlib/Analysis/Convolution.lean`

commit e463fbf
Author: Moritz Firsching <[email protected]>
Date:   Mon Jan 29 13:15:22 2024 +0000

    chore(Analysis/SpecialFunctions/JapaneseBracket): restore measurability (#10054)

    Co-authored-by: Moritz Firsching <[email protected]>

commit cea4f7a
Author: Scott Morrison <[email protected]>
Date:   Mon Jan 29 10:59:18 2024 +0000

    chore: cleanup some Yoneda lemma proofs (#10092)

    While thinking about simp lemmas for opposite categories (for the sake of comonoid objects, for the sake of group objects, for the sake of reductive groups), noticed some of the Yoneda lemma proofs can be golfed.

    Co-authored-by: Scott Morrison <[email protected]>

commit 197378a
Author: Adam Topaz <[email protected]>
Date:   Mon Jan 29 10:12:33 2024 +0000

    chore: Fix some porting notes and make some defs computable again. (#10062)

    These are some auxiliary definitions for the monoidal structure on a category induced by binary products and terminal objects.

commit 86ffe04
Author: Yury G. Kudryashov <[email protected]>
Date:   Mon Jan 29 07:53:36 2024 +0000

    chore(Order/Filter/ListTraverse): move from `Basic` (#10048)

commit a4c1d9d
Author: sgouezel <[email protected]>
Date:   Mon Jan 29 07:53:35 2024 +0000

    chore: split file on series of functions into two files (#9906)

    Currently, the same file contains the facts that series of functions are continuous (resp. smooth) under suitable assumption. I will need the result on continuity in a file of more topological nature. To avoid importing all calculus in this file, this PR splits the file `Analysis.Calculus.Series` into `Analysis.Calculus.SmoothSeries` and `Analysis.NormedSpace.FunctionSeries`.

    It's purely a splitting PR, no result added or removed.

commit 1fa9ebf
Author: Yury G. Kudryashov <[email protected]>
Date:   Mon Jan 29 06:37:18 2024 +0000

    feat(Algebra/InfiniteSum): drop `[T2Space _]` assumption (#10060)

    * Add `CanLift` instance for `Function.Embedding`.
    * Assume `Injective i` instead of an equivalent condition in `hasSum_iff_hasSum_of_ne_zero_bij`.
    * Add `tsum_eq_sum'`, a version of `tsum_eq_sum` that explicitly mentions `support f`.
    * Add `Function.Injective.tsum_eq`, use it to drop `[T2Space _]` assumption in
      - `Equiv.tsum_eq`;
      - `tsum_subtype_eq_of_support_subset`;
      - `tsum_subtype_support`;
      - `tsum_subtype`;
      - `tsum_univ`;
      - `tsum_image`;
      - `tsum_range`;
      - `tsum_setElem_eq_tsum_setElem_diff`;
      - `tsum_eq_tsum_diff_singleton`;
      - `tsum_eq_tsum_of_ne_zero_bij`;
      - `Equiv.tsum_eq_tsum_of_support`;
      - `tsum_extend_zero`;
    * Golf some proofs.
    * Drop `Equiv.Set.prod_singleton_left` and `Equiv.Set.prod_singleton_right` added in #10038.
      @MichaelStollBayreuth, if you need these `Equiv`s, then please

      - restore them in `Logic/Equiv/Set`, not in `Data/Set/Prod`;
      - call them `Equiv.Set.singletonProd` and `Equiv.Set.prodSingleton`, following the `lowerCamelCase` naming convention for `def`s;
      - reuse the existing `Equiv.Set.prod` and `Equiv.prodUnique`/`Equiv.uniqueProd` in the definitions.

commit 1da1e9e
Author: sgouezel <[email protected]>
Date:   Mon Jan 29 06:37:17 2024 +0000

    feat: minor topological improvements (#9908)

    * Prove that a set is a Gdelta if and only if it is an intersection of open sets indexed by `ℕ`.
    * Cleanup porting todos in the Gdelta file
    * Rename `cluster_point_of_compact` to `exists_clusterPt_of_compactSpace `
    * Generalize the class `T2Space` to `T2OrLocallyCompactRegularSpace` in the file `Support.lean`

commit 4e0ccc0
Author: technosentience <[email protected]>
Date:   Mon Jan 29 05:23:46 2024 +0000

    feat(Data/Fin/Tuple/Basic): `repeat_comp_rev` (#9845)

    Prove `repeat_comp_rev`.

    Co-authored-by: Yury G. Kudryashov <[email protected]>

commit f5a69ea
Author: Kevin Buzzard <[email protected]>
Date:   Mon Jan 29 01:14:44 2024 +0000

    docs(Algebra/Algebra/Basic): get the type right (#10055)

commit 995b1af
Author: Pietro Monticone <[email protected]>
Date:   Mon Jan 29 00:09:08 2024 +0000

    doc(Mathlib/Algebra): fix typos  (#10080)

    Fix minor typos in the `Mathlib/Algebra/CovariantAndContravariant.lean` file.

commit c38c032
Author: Yury G. Kudryashov <[email protected]>
Date:   Sun Jan 28 23:24:42 2024 +0000

    feat(Convex/Gauge): add `continuousAt_gauge` (#9911)

commit 9f35a08
Author: Oliver Nash <[email protected]>
Date:   Sun Jan 28 15:34:44 2024 +0000

    feat: add lemmas `nullMeasurableSet_lt'` and `nullMeasurableSet_le` (#10074)

    Prior to this commit the state of Mathlib was:
    ```lean
    import Mathlib
    ```

    Co-authored-by: teorth <[email protected]>

commit e975e78
Author: Yury G. Kudryashov <[email protected]>
Date:   Sun Jan 28 14:42:17 2024 +0000

    chore(Topology): fix a typo (#10070)

    There is no `NeBot` in this lemma

commit 19b5ded
Author: Moritz Firsching <[email protected]>
Date:   Sun Jan 28 09:50:58 2024 +0000

    refactor(Probability/Kernel/CondCdf): mv some theorems (#10036)

    Co-authored-by: Moritz Firsching <[email protected]>

commit e8bfb67
Author: Moritz Firsching <[email protected]>
Date:   Sun Jan 28 09:07:45 2024 +0000

    refactor(Probability/Kernel/CondCdf): mv ofReal_cinfi (#10044)

    Co-authored-by: Moritz Firsching <[email protected]>

commit d5277c9
Author: Matthew Robert Ballard <[email protected]>
Date:   Sun Jan 28 02:42:13 2024 +0000

    perf(NormedSpace/OperatorNorm): fix `simp` call and clean up porting notes (#9658)

    We clean up some porting notes and speed up this file.

commit 09b44c1
Author: Christopher Hoskin <[email protected]>
Date:   Sat Jan 27 19:32:54 2024 +0000

    feat(GroupTheory/GroupAction/Group): invOf smul lemmas (#9972)

    Give `smul` versions of some existing `mul` lemmas:

    - `invOf_smul_smul`
    - smul_invOf_smul (c.f. mul_invOf_self_assoc)
    - `invOf_smul_eq_iff` (c.f. `invOf_mul_eq_iff_eq_mul_left`) (required for #7569)
    - `smul_eq_iff_eq_invOf_smul` (c.f `mul_left_eq_iff_eq_invOf_mul`)

    Co-authored-by: Christopher Hoskin <[email protected]>
    Co-authored-by: Christopher Hoskin <[email protected]>

commit e4e10f9
Author: Michael Stoll <[email protected]>
Date:   Sat Jan 27 17:46:59 2024 +0000

    feat(Topology/Algebra/InfiniteSum/Basic): add some lemmas on `tsum`s (#10038)

    This is the fifth PR in a sequence that adds auxiliary lemmas from the [EulerProducts](https://github.com/MichaelStollBayreuth/EulerProducts) project to Mathlib.

    It adds three lemmas on `tsum`s:
    ```lean
    lemma HasSum.tsum_fiberwise {α β γ : Type*} [AddCommGroup α] [UniformSpace α] [UniformAddGroup α]
        [T2Space α] [RegularSpace α] [CompleteSpace α] {f : β → α}
        {a : α} (hf : HasSum f a) (g : β → γ) :
        HasSum (fun c : γ ↦ ∑' b : g ⁻¹' {c}, f b) a

    lemma tsum_setProd_singleton_left {α β γ : Type*} [AddCommMonoid γ] [TopologicalSpace γ] [T2Space γ]
        (a : α) (t : Set β) (f : α × β → γ) : (∑' x : {a} ×ˢ t, f x) = ∑' b : t, f (a, b)

    lemma tsum_setProd_singleton_right {α β γ : Type*} [AddCommMonoid γ] [TopologicalSpace γ] [T2Space γ]
        (s : Set α) (b : β) (f : α × β → γ) : (∑' x : s ×ˢ {b}, f x) = ∑' a : s, f (a, b)
    ```
    and the necessary equivalences
    ```lean
    def prod_singleton_left {α β : Type*} (a : α) (t : Set β) : ↑({a} ×ˢ t) ≃ ↑t

    def prod_singleton_right {α β : Type*} (s : Set α) (b : β) : ↑(s ×ˢ {b}) ≃ ↑s
    ```

commit 0bcd6be
Author: grunweg <[email protected]>
Date:   Sat Jan 27 17:21:40 2024 +0000

    feat: two lemmas about cut-off functions (#9873)

    From sphere-eversion; I'm just upstreaming this.

    The version in sphere-eversion uses an unbundled design; we provide a bundled version (for now) to match the remaining file.

    Co-authored-by: grunweg <[email protected]>

commit f1919fd
Author: Yuma Mizuno <[email protected]>
Date:   Sat Jan 27 14:51:46 2024 +0000

    feat(CategoryTheory/Monoidal): add lemmas for the whiskerings (#9995)

    Extracted from #6307.

commit c6cc35e
Author: Christian Merten <[email protected]>
Date:   Sat Jan 27 11:43:29 2024 +0000

    docs(TensorProduct/Tower): fix doc string of `AlgebraTensorModule.assoc` (#10051)

    Matches variable names in the doc string with the variables used in the type signature of `AlgebraTensorModule.assoc`.

commit ae8f621
Author: grunweg <[email protected]>
Date:   Sat Jan 27 11:43:28 2024 +0000

    feat: four small lemmas about extended charts (#10001)

    From sphere-eversion; I'm just submitting them.

commit c8818ba
Author: grunweg <[email protected]>
Date:   Sat Jan 27 11:43:27 2024 +0000

    feat(NormedSpace/Basic): add dist_smul_add_one_sub_smul_le (#9982)

    From sphere-eversion (slightly golfed); I'm just upstreaming it.

commit ca91ff1
Author: Winston Yin <[email protected]>
Date:   Sat Jan 27 11:43:26 2024 +0000

    refactor(PartialHomeomorph): make `[Nonempty s]` explicit (#9894)

    Subsets aren't going to have `Nonempty` instances on them, typically, so one would have to manually construct a term of `[Nonempty s]` whenever `PartialHomeomorph.subtypeRestr` is used. Turning this instance argument explicit, `(hs : Nonempty s)` would help us avoid `@PartialHomeomorph.subtypeRestr _ _ _ _` constructions or `haveI : Nonempty ...`.

    Its only downstream effect currently is in `ChartedSpace.lean`.

commit a1bc0ac
Author: Pietro Monticone <[email protected]>
Date:   Sat Jan 27 10:41:58 2024 +0000

      doc(docs): fix typos (#10050)

    Fix minor typos in the `docs` folder.

commit 15c33b6
Author: Frédéric Dupuis <[email protected]>
Date:   Sat Jan 27 10:41:57 2024 +0000

    fix: lemma given a wrong name by `to_additive` (#10049)

commit 7f19636
Author: sgouezel <[email protected]>
Date:   Sat Jan 27 10:41:57 2024 +0000

    chore: factor out a lemma from the proof of Steinhaus theorem (#9907)

    Given a measure in a locally compact group, and a compact set `k`, then for `g` close enough to the identity, the set `g • k \ k` has arbitrarily small measure. A slightly weaker version of this fact is used implicitly in our current proof of Steinhaus theorem that `E - E` is a neighborhood of the identity if `E` has positive measure. Since I will need this lemma later on, I extract it from the proof of Steinhaus theorem in this PR.

commit cb8ebaf
Author: Moritz Firsching <[email protected]>
Date:   Sat Jan 27 09:26:07 2024 +0000

    refactor(Probability/Kernel/CondCdf): mv prod_iInter (#10037)

    Co-authored-by: Moritz Firsching <[email protected]>

commit 62acece
Author: Ruben Van de Velde <[email protected]>
Date:   Fri Jan 26 22:26:07 2024 +0000

    feat: iteratedDeriv_const_{s,}mul, iteratedDeriv_{c,}exp_const_mul (#9767)

    Based on @CBirkbeck's work on modular forms.

commit 781af01
Author: Yury G. Kudryashov <[email protected]>
Date:   Fri Jan 26 20:18:23 2024 +0000

    feat: drop unneeded assumptions in `IsUniform.integral_eq` (#10021)

    Co-authored-by: sgouezel <[email protected]>

commit f1802b1
Author: Eric Wieser <[email protected]>
Date:   Fri Jan 26 19:09:11 2024 +0000

    feat: Add lattice lemmas about `Sub{group,monoid}.{op,unop}` (#9860)

    In fact I only need the `closure` lemma, but the others are easy enough.

    This changes the `opEquiv`s to be order isomorphisms rather than just `Equiv`s.

commit edd8f40
Author: Jireh Loreaux <[email protected]>
Date:   Fri Jan 26 18:21:29 2024 +0000

    feat: link `Dilation` to `Isometry` and `Homeomorph` (#9980)

commit ab48003
Author: grunweg <[email protected]>
Date:   Fri Jan 26 17:17:58 2024 +0000

    chore(Calculus/ParametricIntegralInterval): small clean-ups (#10005)

    - collect some very common variables
    - use refine and \mapsto instead of refine' and => (both are preferred now)

commit 1fec3c4
Author: Yury G. Kudryashov <[email protected]>
Date:   Fri Jan 26 13:55:43 2024 +0000

    chore(Filter/Ker): move from Filter.Basic to a new file (#10023)

    Start moving parts of >3K lines long `Filter.Basic` to new files.

commit 0085768
Author: Xavier Roblot <[email protected]>
Date:   Fri Jan 26 11:59:21 2024 +0000

    feat: Add `measurable_abs` (#9912)

    See [Zulip](https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there-code-for-X.3F/topic/measurable_abs/near/417230631)

    Co-authored-by: Yaël Dillies <[email protected]>

commit 5821f8c
Author: grunweg <[email protected]>
Date:   Fri Jan 26 11:20:53 2024 +0000

    feat: add LocallyFinite.smul_{left,right} (#10020)

    From sphere-eversion. Will be used to show a point-wise version of `SmoothPartitionOfUnity.contMDiff_finsum_smul`.

    Co-authored-by: Oliver Nash <[email protected]>

commit e165098
Author: Ruben Van de Velde <[email protected]>
Date:   Fri Jan 26 11:20:52 2024 +0000

    feat: add Int.le_add_one_iff (#9892)

    Co-authored-by: Yury G. Kudryashov <[email protected]>

commit 4529fc1
Author: Matthew Robert Ballard <[email protected]>
Date:   Fri Jan 26 08:58:29 2024 +0000

    chore(MetricSpace.PseudoMetric): make `PseudoEMetricSpace.toPseudoMetricSpaceOfDist` reducible  (#10012)

    `PseudoEMetricSpace.toPseudoMetricSpaceOfDist` is used in instances so needs to be reducible for unification.

commit f2b0b27
Author: Thomas Browning <[email protected]>
Date:   Fri Jan 26 08:58:28 2024 +0000

    feat(GroupTheory/GroupAction/Basic): Condition for `swap` to stabilize a set (#9945)

commit a268d11
Author: grunweg <[email protected]>
Date:   Fri Jan 26 08:58:27 2024 +0000

    feat: one lemma about LocallyFinite (#9813)

    From sphere-eversion; I'm just submitting this upstream.

commit 19ab970
Author: grunweg <[email protected]>
Date:   Fri Jan 26 08:27:37 2024 +0000

    feat: add PartialHomeomorph.extend_target' (#9977)

    Inspired by sphere-eversion; similar to `PartialEquiv.image_source_eq_target`.

commit 0500719
Author: Ruben Van de Velde <[email protected]>
Date:   Fri Jan 26 07:29:47 2024 +0000

    feat: Int.{even_sub_one,even_mul_pred_self} (#9859)

    Also rename `Nat.even_mul_self_pred` for consistency with `Nat.even_mul_succ_self`.

commit 970a1ab
Author: Oliver Nash <[email protected]>
Date:   Fri Jan 26 04:28:56 2024 +0000

    feat: the minimal polynomial is a generator of the annihilator ideal (#10008)

    More precisely, the goal of these changes is to make the following work:
    ```lean
    import Mathlib.FieldTheory.Minpoly.Field

    open Module Polynomial

    example {K V : Type*} [Field K] [AddCommGroup V] [Module K V] (f : End K V) :
        (⊤ : Submodule K[X] <| AEval K V f).annihilator = K[X] ∙ minpoly K f := by
      simp
    ```

    Co-authored-by: Johan Commelin <[email protected]>

commit 20c7b4b
Author: grunweg <[email protected]>
Date:   Fri Jan 26 03:44:15 2024 +0000

    chore(Topology/Basic): re-use variables; rename a : X to x : X (#9993)

    Co-authored-by: sgouezel <[email protected]>
    Co-authored-by: Yury G. Kudryashov <[email protected]>

commit e3b6818
Author: Yury G. Kudryashov <[email protected]>
Date:   Fri Jan 26 03:03:09 2024 +0000

    fix: `Clm` -> `CLM`, `Cle` -> `CLE` (#10018)

    Rename

    - `Complex.equivRealProdClm` → `Complex.equivRealProdCLM`;
      - [ ] TODO: should this one use `CLE`?
    - `Complex.reClm` → `Complex.reCLM`;
    - `Complex.imClm` → `Complex.imCLM`;
    - `Complex.conjLie` → `Complex.conjLIE`;
    - `Complex.conjCle` → `Complex.conjCLE`;
    - `Complex.ofRealLi` → `Complex.ofRealLI`;
    - `Complex.ofRealClm` → `Complex.ofRealCLM`;
    - `fderivInnerClm` → `fderivInnerCLM`;
    - `LinearPMap.adjointDomainMkClm` → `LinearPMap.adjointDomainMkCLM`;
    - `LinearPMap.adjointDomainMkClmExtend` → `LinearPMap.adjointDomainMkCLMExtend`;
    - `IsROrC.reClm` → `IsROrC.reCLM`;
    - `IsROrC.imClm` → `IsROrC.imCLM`;
    - `IsROrC.conjLie` → `IsROrC.conjLIE`;
    - `IsROrC.conjCle` → `IsROrC.conjCLE`;
    - `IsROrC.ofRealLi` → `IsROrC.ofRealLI`;
    - `IsROrC.ofRealClm` → `IsROrC.ofRealCLM`;
    - `MeasureTheory.condexpL1Clm` → `MeasureTheory.condexpL1CLM`;
    - `algebraMapClm` → `algebraMapCLM`;
    - `WeakDual.CharacterSpace.toClm` → `WeakDual.CharacterSpace.toCLM`;
    - `BoundedContinuousFunction.evalClm` → `BoundedContinuousFunction.evalCLM`;
    - `ContinuousMap.evalClm` → `ContinuousMap.evalCLM`;
    - `TrivSqZeroExt.fstClm` → `TrivSqZeroExt.fstClm`;
    - `TrivSqZeroExt.sndClm` → `TrivSqZeroExt.sndCLM`;
    - `TrivSqZeroExt.inlClm` → `TrivSqZeroExt.inlCLM`;
    - `TrivSqZeroExt.inrClm` → `TrivSqZeroExt.inrCLM`

    and related theorems.

commit 66439f5
Author: Matthew Robert Ballard <[email protected]>
Date:   Fri Jan 26 00:49:24 2024 +0000

    chore(UniformSpace.Basic): make `UniformSpace.comap` reducible  (#10010)

    `UniformSpace.comap` is used in instance construction so needs to be reducible for unification purposes.

commit 79a9e0e
Author: Moritz Firsching <[email protected]>
Date:   Thu Jan 25 23:16:34 2024 +0000

    refactor(Topology/Clopen): order of open and closed (#9957)

    Co-authored-by: Moritz Firsching <[email protected]>

commit f9daa98
Author: grunweg <[email protected]>
Date:   Thu Jan 25 21:01:58 2024 +0000

    chore(Data/ENNReal/Basic): split file (#9869)

    Co-authored-by: Jireh Loreaux <[email protected]>

commit 0c4ffb6
Author: Moritz Firsching <[email protected]>
Date:   Thu Jan 25 20:36:48 2024 +0000

    chore(test/toAdditive): remove commented test (#9971)

    Co-authored-by: Moritz Firsching <[email protected]>

commit b3052ec
Author: Scott Carnahan <[email protected]>
Date:   Thu Jan 25 20:09:13 2024 +0000

    feat: polynomial evaluation via SMul (#9139)

    We introduce polynomial evaluation using SMul, so polynomials can be evaluated at elements of non-associative semirings.  This is most useful in the power-associative context, but power-associativity is not implemented yet.

    We obtain a generalization of `Polynomial.eval₂`, and in particular of the specializations `Polynomial.aeval` and `Polynomial.leval`.

commit 1f2e586
Author: Alex Meiburg <[email protected]>
Date:   Thu Jan 25 16:42:45 2024 +0000

    fix doc for LinearMap.compRight (#9997)

    minor typo here. An (f : M2 -> M3) induces a linear map from (M->M2) to (M->M3). Not to (M2 -> M3).

    Co-authored-by: Alex Meiburg <[email protected]>

commit 47a9066
Author: grunweg <[email protected]>
Date:   Thu Jan 25 16:42:44 2024 +0000

    feat: add `Continuous.image_connectedComponentIn_subset` (#9983)

    and a version for homeomorphisms. From sphere-eversion; I'm just submitting things upstream.

commit e7170d3
Author: Yury G. Kudryashov <[email protected]>
Date:   Thu Jan 25 16:42:43 2024 +0000

    feat(Topology/Basic): add TopologicalSpace.ext_isClosed (#9963)

    Use it to golf `PrimeSpectrum.localization_comap_inducing`.

commit bd6616c
Author: Yury G. Kudryashov <[email protected]>
Date:   Thu Jan 25 16:42:42 2024 +0000

    chore(Integral/CircleTransform): golf (#9937)

    Motivated by @Ruben-VandeVelde's leanprover-community/mathlib3#15206

commit 941d069
Author: Oliver Nash <[email protected]>
Date:   Thu Jan 25 15:54:36 2024 +0000

    feat: the torsion submodule of an irreducible element is semisimple (#9994)

    (provided the coefficients are a principal ideal ring)

commit c27bc4e
Author: Johan Commelin <[email protected]>
Date:   Thu Jan 25 15:54:35 2024 +0000

    refactor(ZMod): remove coe out of ZMod (#9839)

    Co-authored-by: Ruben Van de Velde <[email protected]>
    Co-authored-by: Vierkantor <[email protected]>

commit fe3b2b2
Author: Yury G. Kudryashov <[email protected]>
Date:   Thu Jan 25 14:36:36 2024 +0000

    feat(Data/Sigma): add `Sigma.fst_surjective` etc (#9914)

    - Add `Sigma.fst_surjective`, `Sigma.fst_surjective_iff`,
      `Sigma.fst_injective`, and `Sigma.fst_injective_iff`.
    - Move `sigma_mk_injective` up.
    - Open `Function` namespace, drop `Function.`.
    - Fix indentation.

commit 8853442
Author: Oliver Nash <[email protected]>
Date:   Thu Jan 25 14:36:35 2024 +0000

    feat: define semisimple linear endomorphisms (#9825)

commit 0b79434
Author: Jireh Loreaux <[email protected]>
Date:   Thu Jan 25 14:02:42 2024 +0000

    chore: golf `FiniteDimensional.isROrC_to_real` (#9921)

commit ce79848
Author: Yury G. Kudryashov <[email protected]>
Date:   Thu Jan 25 13:08:16 2024 +0000

    feat(Trigonometric): add lemmas about `cos x = -1 ↔ _` etc (#9878)

commit 2b7478a
Author: Moritz Firsching <[email protected]>
Date:   Thu Jan 25 13:08:14 2024 +0000

    feat: superFactorial_two_mul, superFactorial_four_mul (#7924)

    Co-authored-by: Moritz Firsching <[email protected]>
    Co-authored-by: Yury G. Kudryashov <[email protected]>

commit c5ca57c
Author: Alex J Best <[email protected]>
Date:   Thu Jan 25 12:45:33 2024 +0000

     feat: problem matchers for tests (#9552)

    Makes it a bit easier to see which test failed and where

commit d3da7bb
Author: Yuma Mizuno <[email protected]>
Date:   Thu Jan 25 12:14:10 2024 +0000

    refactor(CategoryTheory/Monoidal): replace axioms with those more suitable for the whiskerings (#9991)

    Extracted from #6307. We replace some axioms by those more preferable when using the whiskerings instead of the tensor of morphisms.

commit 2725911
Author: Moritz Firsching <[email protected]>
Date:   Thu Jan 25 11:09:48 2024 +0000

    chore(Algebra/Algebra/Basic): remove @s to address porting note (#9969)

    Co-authored-by: Moritz Firsching <[email protected]>

commit 9a290c2
Author: grunweg <[email protected]>
Date:   Thu Jan 25 09:21:34 2024 +0000

    chore(Topology/Constructions): rename most type variables (#9863)

    Now we use letters X and Y for topological spaces, not Greek letters.

    I didn't replace all letters; some lemmas need a large number of different letters. Volunteers for the last instances welcome.

commit 2e59248
Author: Yuma Mizuno <[email protected]>
Date:   Thu Jan 25 06:29:39 2024 +0000

    refactor(CategoryTheory/Monoidal): split the naturality condition of monoidal functors (#9988)

    Extracted from #6307. We replace `μ_natural` with `μ_natural_left` and `μ_natural_right` since we prefer to use the whiskerings to the tensor of morphisms in the refactor #6307.

commit 8c661e5
Author: Jireh Loreaux <[email protected]>
Date:   Thu Jan 25 02:46:49 2024 +0000

    feat: add `Homeomorph.subtype` for lifting homeomorphisms to subtypes (#9959)

    This extends `Equiv.subtypeEquiv`, which promotes `e : α ≃ β` to `e.subtypeEquiv _ : {a : α // p a} ≃ {b : β // q b}`, to homeomorphisms.

    We also add a missing lemma linking `Equiv.subtypeEquiv` to `Subtype.map`, and update the definition to use `Subtype.map` also.

commit 0c34368
Author: grunweg <[email protected]>
Date:   Thu Jan 25 01:23:40 2024 +0000

    feat: sigma-compact measure zero sets are meagre (#7640)

    Co-authored-by: Mario Carneiro <[email protected]>

commit ad22323
Author: Eric Wieser <[email protected]>
Date:   Thu Jan 25 00:17:40 2024 +0000

    feat: two lemmas about division (#9966)

commit e88d290
Author: Oliver Nash <[email protected]>
Date:   Wed Jan 24 22:51:33 2024 +0000

    chore: remove porting note after `simp` fix (#9974)

commit a686ba8
Author: grunweg <[email protected]>
Date:   Wed Jan 24 20:52:37 2024 +0000

    feat: finite products/sums of differentiable maps into smooth commutative monoids are differentiable (#9775)

    From sphere-eversion; I'm just upstreaming this.

    Co-authored-by: Oliver Nash <[email protected]>

commit 0aa016e
Author: Matthew Robert Ballard <[email protected]>
Date:   Wed Jan 24 18:17:19 2024 +0000

    chore(Algebra.Basic): override `toFun` and `smul` in `Algebra.id` (#9949)

    The current definition of `Algebra.id` is `(RingHom.id _).toAlgebra`. The problem with this is that `RingHom.id` is a `def` and is not reducible. Thus Lean will often refuse to unfold it causing unification to fail unecessarily in typeclass searches. This overrides the data fields from `RingHom.id`.

commit 725f123
Author: Anne Baanen <[email protected]>
Date:   Wed Jan 24 15:59:29 2024 +0000

    perf: de-prioritize `Subalgebra.algebra'` and `IntermediateField.algebra'` (#9936)

    Like in #9655, these instances tend to be slow to fail, so we should assign them a low priority.

    Zulip discussions:
    https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Algebra.2Eid.20for.20IntermediateField https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Timeout.20in.20Submodule.20.28.F0.9D.93.9E.20K.29.20.28.F0.9D.93.9E.20K.29

    Co-authored-by: Anne Baanen <[email protected]>

commit 4fe0086
Author: Yury G. Kudryashov <[email protected]>
Date:   Wed Jan 24 15:59:27 2024 +0000

    feat(UpperHalfPlane): add positivity extensions (#9545)

commit 9a8dc7a
Author: Christian Merten <[email protected]>
Date:   Wed Jan 24 14:31:55 2024 +0000

    feat(CategoryTheory/Galois): finite `G`-sets are a `PreGaloisCategory` (#9879)

    We show that the category of finite `G`-sets is a `PreGaloisCategory` and the forgetful functor to finite sets is a `FibreFunctor`.

commit d1054e1
Author: grunweg <[email protected]>
Date:   Wed Jan 24 14:31:54 2024 +0000

    chore(Topology): remove autoImplicit from most remaining files (#9865)

commit 00202e4
Author: grunweg <[email protected]>
Date:   Wed Jan 24 14:31:52 2024 +0000

    feat(Topology/Support): add tsupport_smul_{left,right} (#9778)

    - rename `Function.support_smul_subset_right` to `Function.support_const_smul_subset`

    From sphere-eversion; I'm just upstreaming it.

    Co-authored-by: grunweg <[email protected]>

commit fac72bc
Author: Scott Morrison <[email protected]>
Date:   Wed Jan 24 13:11:22 2024 +0000

    chore: bump dependencies (#9962)

    Co-authored-by: Scott Morrison <[email protected]>

commit 02240d5
Author: Eric Wieser <[email protected]>
Date:   Wed Jan 24 13:11:21 2024 +0000

    refactor: move `Archimedean` instances to `Order/Archimedean` (#9950)

    We already have the instances for `ℕ`, `ℤ`, and `ℚ` in this file, so adding `NNRat` doesn't feel that out of place, as it completes this {negation,division} lattice.

    Follows on from #9917. These changes knock off 132 dependencies from `NNRat`, though adds more to `Archimedean`.
    I think this is acceptable; we need `NNRat` to be super early if we want to be able to use it in norm_num, and the depth of `Archimedean` will reduce with `NNRat` as I work towards this.

commit e61934e
Author: damiano <[email protected]>
Date:   Wed Jan 24 13:11:20 2024 +0000

    Add `Lattice ℤ` instance for computability (#9946)

    The file `Data.Int.ConditionallyCompleteOrder` defines a noncomputable instance of `ConditionallyCompleteLinearOrder` on `ℤ`.

    This noncomputable instance is picked up by the typeclass search when looking for a `Lattice` instance on `ℤ`, making, for instance, `abs` noncomputable on `ℤ`.

    This PR restores the computability of `Lattice ℤ`.

    [Zulip discussion](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/No.20more.20.60Abs.60.3F/near/417546479)

commit 6694f75
Author: Yury G. Kudryashov <[email protected]>
Date:   Wed Jan 24 10:41:24 2024 +0000

    chore(Topology/Basic): rename variables (#9956)

    Use `X`, `Y`, `Z` for topological spaces.

commit 46e6944
Author: Winston Yin <[email protected]>
Date:   Wed Jan 24 10:06:42 2024 +0000

    chore: rename `StructureGroupoid.eq_on_source'` to `StructureGroupoid.mem_of_eqOnSource'` (#9802)

    Since it refers to `PartialEquiv.EqOnSource`, the correct naming scheme should not be snake case `eq_on_source`. I also added `mem_of_` because that's the target of the lemma, while `EqOnSource` is just a hypothesis.

    There are no added lemmas or docstrings in this PR. It's all just renaming.

commit cf5ad94
Author: Scott Morrison <[email protected]>
Date:   Wed Jan 24 03:45:17 2024 +0000

    chore: bump Std and Aesop (#9948)

    Co-authored-by: Scott Morrison <[email protected]>

commit 0faddd8
Author: Yaël Dillies <[email protected]>
Date:   Wed Jan 24 02:51:10 2024 +0000

    feat: `n • v` and `v` are on the same ray (#9104)

    From LeanAPAP

commit 6219c28
Author: Jeremy Tan Jie Rui <[email protected]>
Date:   Wed Jan 24 02:24:12 2024 +0000

    feat: transfer of graph properties over maps (#9708)

    Part of #9317.
fgdorais pushed a commit to fgdorais/batteries that referenced this pull request Feb 18, 2024
@kim-em @fgdorais
chore: upstream classical tactic (leanprover-community#242)
f57cfe0
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@digama0 digama0 digama0 left review comments

@fgdorais fgdorais fgdorais approved these changes

@joehendrix joehendrix joehendrix approved these changes

Assignees
No one assigned
Labels
will-merge-soon PR will be merged soon. Any concerns should be raised quickly.
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
5 participants
@kim-em @fgdorais @digama0 @joehendrix @leanprover-community-mathlib4-bot