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.
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
[Merged by Bors] - feat: s ∩ t * s ∪ t ⊆ s * t
#1619
Conversation
f62b054
to
121e916
Compare
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Mostly looks good, though CI is failing
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
This should fix CI
Mathlib/Data/Finset/Pointwise.lean
Outdated
@[to_additive (attr := simp)] | ||
-- Porting note: should take priority over `Finite.toFinset_singleton` | ||
@[to_additive (attr := simp high)] |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
As an explanation of what's going on here; lean reduces the definition of (1 : Set _)
because it's hidden in an implicit argument. As a mwe:
import Mathlib.Data.Set.Pointwise.Finite
import Mathlib.Data.Finset.Pointwise
namespace Set
open scoped Pointwise
variable {α : Type _} [One α]
/-- A version of `toFinset` with an explicit `s` argument. -/
noncomputable def Finite.toFinset' (s : Set α) (hs : s.Finite) : Finset α := hs.toFinset
/-- A copy of `Finite.toFinset_singleton` -/
@[simp] lemma Finite.toFinset'_singleton (a : α) (hs : Set.Finite {a} := finite_singleton _) : hs.toFinset' _ = {a} :=
Finite.toFinset_singleton _
-- ok
@[simp] theorem Finite.toFinset'_one (h : (1 : Set α).Finite := finite_one) : h.toFinset' _ = 1 :=
Finite.toFinset_singleton _
-- rejected by linter
@[simp] theorem Finite.toFinset_one (h : (1 : Set α).Finite := finite_one) : h.toFinset = 1 :=
Finite.toFinset_singleton _
end Set
#lint
I think this probably happened in Lean 3 too, but there the simp priority was automatically correct.
bors d+ Please merge once CI passes. |
✌️ YaelDillies can now approve this pull request. To approve and merge a pull request, simply reply with |
bors merge |
Match leanprover-community/mathlib#17961 Co-authored-by: Eric Wieser <wieser.eric@gmail.com> Co-authored-by: Jeremy Tan Jie Rui <reddeloostw@gmail.com> Co-authored-by: Parcly Taxel <reddeloostw@gmail.com>
Pull request successfully merged into master. Build succeeded:
|
s ∩ t * s ∪ t ⊆ s * t
s ∩ t * s ∪ t ⊆ s * t
Match leanprover-community/mathlib#17961 Co-authored-by: Eric Wieser <wieser.eric@gmail.com> Co-authored-by: Jeremy Tan Jie Rui <reddeloostw@gmail.com> Co-authored-by: Parcly Taxel <reddeloostw@gmail.com>
Match leanprover-community/mathlib#17961