Skip to content

[Merged by Bors] - feat(Topology/Algebra/Module): call eta_expand in the default tactic of ContinuousLinearEquiv#39766

Closed
gasparattila wants to merge 3 commits into
leanprover-community:masterfrom
gasparattila:CLE-dsimp
Closed

[Merged by Bors] - feat(Topology/Algebra/Module): call eta_expand in the default tactic of ContinuousLinearEquiv#39766
gasparattila wants to merge 3 commits into
leanprover-community:masterfrom
gasparattila:CLE-dsimp

Conversation

@gasparattila

@gasparattila gasparattila commented May 24, 2026 •
edited
Loading

Copy link
Copy Markdown
Contributor

This PR adds a call to eta_expand in the default tactic for the fields of ContinuousLinearEquiv, so that dsimp can also use lemmas written in applied form. This is the same default tactic that is already used for Homeomorph and ContinuousLinearMap. Most of the proofs which are solved by this default tactic are also removed.

A skip is also added to show the goal instead of "dsimp made no progress" when this default tactic fails.

Open in Gitpod

@github-actions github-actions Bot added merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) t-topology Topological spaces, uniform spaces, metric spaces, filters labels May 24, 2026
@gasparattila
feat(Topology/Algebra/Module): call eta_expand in the default tacti…
eeba2d7 
…c of `ContinuousLinearEquiv`

This PR adds a call to `eta_expand` in the default tactic for the fields of `ContinuousLinearEquiv`, so that `dsimp` can also use lemmas written in applied form. Most of the proofs which are solved by this default tactic are also removed.

A `skip` is also added to show the goal instead of "`dsimp` made no progress" when this default tactic fails.
@github-actions github-actions Bot removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label May 24, 2026
@github-actions

github-actions Bot commented May 24, 2026 •
edited
Loading

Copy link
Copy Markdown

PR summary 37b2c8b8a6

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference

Declarations diff

+ _root_.ContinuousLinearMap.continuous_postcomp_continuousMultilinearMap
+ continuous_precomp

You can run this locally as follows 
## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

## summary with just the declaration names:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.

No changes to strong technical debt.
No changes to weak technical debt.

themathqueen
themathqueen reviewed May 24, 2026
View reviewed changes
Comment thread Mathlib/Topology/Algebra/Module/Multilinear/Topology.lean Outdated
themathqueen
themathqueen reviewed May 24, 2026
View reviewed changes
Comment thread Mathlib/Topology/Algebra/Module/Multilinear/Topology.lean Outdated
themathqueen
themathqueen approved these changes May 24, 2026
View reviewed changes

@themathqueen themathqueen left a comment

Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

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

Can you say how this matches ContinuousLinearMap and Homeomorph in the description?

Thanks!

maintainer merge

@github-actions

github-actions Bot commented May 24, 2026

Copy link
Copy Markdown

🚀 Pull request has been placed on the maintainer queue by themathqueen.

@mathlib-triage mathlib-triage Bot added the maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. label May 24, 2026
themathqueen
themathqueen reviewed May 24, 2026
View reviewed changes
Comment thread Mathlib/Topology/Algebra/Module/Multilinear/Topology.lean Outdated
exact ⟨(φ '' U, V), ⟨hU.image φ, hV⟩, fun g hg ↦ hg.comp (mapsTo_image _ _)⟩ }

@[fun_prop]
theorem continuous_compContinuousLinearMap_left (f : ∀ i, E i →L[𝕜] E₁ i) :

@themathqueen themathqueen May 24, 2026

Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

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

actually, instead of _left maybe _precomp or _postcomp (I forget which is which)?

gasparattila and others added 2 commits May 24, 2026 13:51
@gasparattila @themathqueen
Apply suggestions from code review
ca179ea 
Co-authored-by: Monica Omar <23701951+themathqueen@users.noreply.github.com>
@gasparattila
Rename CMLM composition lemmas
37b2c8b
@faenuccio

faenuccio commented May 25, 2026

Copy link
Copy Markdown
Contributor

thanks

bors r+

@mathlib-triage mathlib-triage Bot added ready-to-merge This PR has been sent to bors. and removed maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. labels May 25, 2026
mathlib-bors Bot pushed a commit that referenced this pull request May 25, 2026
@gasparattila
feat(Topology/Algebra/Module): call eta_expand in the default tacti…
327a72b 
…c of `ContinuousLinearEquiv` (#39766)

This PR adds a call to `eta_expand` in the default tactic for the fields of `ContinuousLinearEquiv`, so that `dsimp` can also use lemmas written in applied form. This is the same default tactic that is already used for `Homeomorph` and `ContinuousLinearMap`. Most of the proofs which are solved by this default tactic are also removed.

A `skip` is also added to show the goal instead of "`dsimp` made no progress" when this default tactic fails.
@mathlib-bors

mathlib-bors Bot commented May 25, 2026

Copy link
Copy Markdown
Contributor

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors Bot changed the title feat(Topology/Algebra/Module): call eta_expand in the default tactic of ContinuousLinearEquiv [Merged by Bors] - feat(Topology/Algebra/Module): call eta_expand in the default tactic of ContinuousLinearEquiv May 25, 2026
@mathlib-bors mathlib-bors Bot closed this May 25, 2026
b-mehta pushed a commit to b-mehta/mathlib4 that referenced this pull request Jun 2, 2026
@gasparattila @b-mehta
feat(Topology/Algebra/Module): call eta_expand in the default tacti…
35ed2f9 
…c of `ContinuousLinearEquiv` (leanprover-community#39766)

This PR adds a call to `eta_expand` in the default tactic for the fields of `ContinuousLinearEquiv`, so that `dsimp` can also use lemmas written in applied form. This is the same default tactic that is already used for `Homeomorph` and `ContinuousLinearMap`. Most of the proofs which are solved by this default tactic are also removed.

A `skip` is also added to show the goal instead of "`dsimp` made no progress" when this default tactic fails.
Bergschaf pushed a commit to Bergschaf/mathlib4 that referenced this pull request Jun 3, 2026
@gasparattila @Bergschaf
feat(Topology/Algebra/Module): call eta_expand in the default tacti…
ef7eac5 
…c of `ContinuousLinearEquiv` (leanprover-community#39766)

This PR adds a call to `eta_expand` in the default tactic for the fields of `ContinuousLinearEquiv`, so that `dsimp` can also use lemmas written in applied form. This is the same default tactic that is already used for `Homeomorph` and `ContinuousLinearMap`. Most of the proofs which are solved by this default tactic are also removed.

A `skip` is also added to show the goal instead of "`dsimp` made no progress" when this default tactic fails.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@themathqueen themathqueen themathqueen approved these changes

Assignees

No one assigned

Labels

ready-to-merge This PR has been sent to bors. t-topology Topological spaces, uniform spaces, metric spaces, filters

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

3 participants

@gasparattila @faenuccio @themathqueen