[Merged by Bors] - feat(data/dfinsupp): Add dfinsupp.single_eq_single_iff, and subtype.heq_iff_coe_eq #4810

eric-wieser · 2020-10-28T14:46:14Z

This ought to make working with dfinsupps over subtypes easier

With thanks to @kckennylau for pointing me in the right direction in https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Difficulty.20with.20dependent.20rewrites/near/214824136

src/data/dfinsupp.lean

…xt_iff_heq This ought to make working with dfinsupps over subtypes easier

src/data/subtype.lean

src/data/dfinsupp.lean

src/data/subtype.lean

…eq_iff_coe_eq This ought to make working with dfinsupps over subtypes easier

src/data/subtype.lean

fpvandoorn

LGTM, this seems like a fine use of heq.

bors d+

fpvandoorn · 2020-10-30T18:17:50Z

src/data/dfinsupp.lean

@@ -313,6 +313,28 @@ by simp only [single_apply, dif_neg h]
 lemma single_injective {i} : function.injective (single i : β i → Π₀ i, β i) :=
 λ x y H, congr_fun (mk_injective _ H) ⟨i, by simp⟩

+/-- Like `finsupp.single_eq_single_iff`, but with a `heq` due to dependent types -/
+lemma single_eq_single_iff (i j : ι) (xi : β i) (xj : β j) :
+  dfinsupp.single i xi = dfinsupp.single j xj ↔ i = j ∧ xi == xj ∨ xi = 0 ∧ xj = 0 :=


For a lemma like this I tend to also want a lemma of the form i = j → xi == xj → dfinsupp.single i xi = dfinsupp.single j xj (the most common case that dfinsupp.single are equal)

I found that if I want that case, I can just use congr. Is the lemma form still worthwhile?

fpvandoorn · 2020-10-30T18:18:09Z

src/data/subtype.lean

@@ -43,6 +43,10 @@ protected theorem forall' {q : ∀x, p x → Prop} :
 lemma ext_iff {a1 a2 : {x // p x}} : a1 = a2 ↔ (a1 : α) = (a2 : α) :=
 ⟨congr_arg _, subtype.ext⟩

+lemma heq_iff_coe_eq (h : ∀ x, p x ↔ q x) {a1 : {x // p x}} {a2 : {x // q x}} :


Suggested change

lemma heq_iff_coe_eq (h : ∀ x, p x ↔ q x) {a1 : {x // p x}} {a2 : {x // q x}} :

@[simp] lemma heq_iff_coe_eq (h : ∀ x, p x ↔ q x) {a1 : {x // p x}} {a2 : {x // q x}} :

If I do that then this lemma takes priority over the stronger heq_iff_eq. Note also that this is a conditional lemma, so probably shouldn't be simp

bors · 2020-10-30T18:18:51Z

✌️ eric-wieser can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

fpvandoorn · 2020-10-31T06:55:47Z

Ok, I agree with both your comments.

bors merge

Btw: you can use @[simp, priority 900] to make the lemma heq_iff_coe_eq a lower priority than heq_iff_eq (this doesn't always work, since simp always simplifies from the leaves, but in this case the lemmas would apply to the same term).

…eq_iff_coe_eq (#4810) This ought to make working with dfinsupps over subtypes easier

bors · 2020-10-31T11:35:15Z

Pull request successfully merged into master.

Build succeeded:

…eq_iff_coe_eq (leanprover-community#4810) This ought to make working with dfinsupps over subtypes easier

eric-wieser added the awaiting-review The author would like community review of the PR label Oct 28, 2020

eric-wieser commented Oct 28, 2020

View reviewed changes

src/data/dfinsupp.lean Show resolved Hide resolved

feat(data/dfinsupp): Add dfinsupp.single_eq_single_iff, and subtype.e…

2b36292

…xt_iff_heq This ought to make working with dfinsupps over subtypes easier

eric-wieser force-pushed the eric-wieser/dfinsupp.single_eq_single_iff branch from 614b31a to 2b36292 Compare October 28, 2020 15:49

eric-wieser commented Oct 28, 2020

View reviewed changes

src/data/subtype.lean Outdated Show resolved Hide resolved

eric-wieser commented Oct 28, 2020

View reviewed changes

src/data/dfinsupp.lean Show resolved Hide resolved

jcommelin reviewed Oct 30, 2020

View reviewed changes

src/data/subtype.lean Outdated Show resolved Hide resolved

feat(data/dfinsupp): Add dfinsupp.single_eq_single_iff, and subtype.h…

098e567

…eq_iff_coe_eq This ought to make working with dfinsupps over subtypes easier

eric-wieser changed the title ~~feat(data/dfinsupp): Add dfinsupp.single_eq_single_iff, and subtype.ext_iff_heq~~ feat(data/dfinsupp): Add dfinsupp.single_eq_single_iff, and subtype.heq_iff_coe_eq Oct 30, 2020

github-actions bot added the merge-conflict Please `git merge origin/master` then a bot will remove this label. label Oct 30, 2020

Merge branch 'master' into eric-wieser/dfinsupp.single_eq_single_iff

1d71564

github-actions bot removed the merge-conflict Please `git merge origin/master` then a bot will remove this label. label Oct 30, 2020

eric-wieser commented Oct 30, 2020

View reviewed changes

src/data/subtype.lean Outdated Show resolved Hide resolved

Update src/data/subtype.lean

89cd37c

eric-wieser requested a review from jcommelin October 30, 2020 13:37

fpvandoorn reviewed Oct 30, 2020

View reviewed changes

fpvandoorn added delegated The PR author may merge after reviewing final suggestions. and removed awaiting-review The author would like community review of the PR labels Oct 30, 2020

jcommelin requested a review from fpvandoorn October 31, 2020 06:32

github-actions bot added the ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.) label Oct 31, 2020

bors bot pushed a commit that referenced this pull request Oct 31, 2020

feat(data/dfinsupp): Add dfinsupp.single_eq_single_iff, and subtype.h…

17697a6

…eq_iff_coe_eq (#4810) This ought to make working with dfinsupps over subtypes easier

bors bot changed the title ~~feat(data/dfinsupp): Add dfinsupp.single_eq_single_iff, and subtype.heq_iff_coe_eq~~ [Merged by Bors] - feat(data/dfinsupp): Add dfinsupp.single_eq_single_iff, and subtype.heq_iff_coe_eq Oct 31, 2020

bors bot closed this Oct 31, 2020

bors bot deleted the eric-wieser/dfinsupp.single_eq_single_iff branch October 31, 2020 11:35

lecopivo pushed a commit to lecopivo/mathlib that referenced this pull request Oct 31, 2020

feat(data/dfinsupp): Add dfinsupp.single_eq_single_iff, and subtype.h…

308f48f

…eq_iff_coe_eq (leanprover-community#4810) This ought to make working with dfinsupps over subtypes easier

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[Merged by Bors] - feat(data/dfinsupp): Add dfinsupp.single_eq_single_iff, and subtype.heq_iff_coe_eq #4810

[Merged by Bors] - feat(data/dfinsupp): Add dfinsupp.single_eq_single_iff, and subtype.heq_iff_coe_eq #4810

eric-wieser commented Oct 28, 2020

fpvandoorn left a comment

fpvandoorn Oct 30, 2020

eric-wieser Oct 30, 2020

fpvandoorn Oct 30, 2020

eric-wieser Oct 30, 2020

bors bot commented Oct 30, 2020

fpvandoorn commented Oct 31, 2020

bors bot commented Oct 31, 2020

	lemma heq_iff_coe_eq (h : ∀ x, p x ↔ q x) {a1 : {x // p x}} {a2 : {x // q x}} :
	@[simp] lemma heq_iff_coe_eq (h : ∀ x, p x ↔ q x) {a1 : {x // p x}} {a2 : {x // q x}} :

[Merged by Bors] - feat(data/dfinsupp): Add dfinsupp.single_eq_single_iff, and subtype.heq_iff_coe_eq #4810

[Merged by Bors] - feat(data/dfinsupp): Add dfinsupp.single_eq_single_iff, and subtype.heq_iff_coe_eq #4810

Conversation

eric-wieser commented Oct 28, 2020

fpvandoorn left a comment

Choose a reason for hiding this comment

fpvandoorn Oct 30, 2020

Choose a reason for hiding this comment

eric-wieser Oct 30, 2020

Choose a reason for hiding this comment

fpvandoorn Oct 30, 2020

Choose a reason for hiding this comment

eric-wieser Oct 30, 2020

Choose a reason for hiding this comment

bors bot commented Oct 30, 2020

fpvandoorn commented Oct 31, 2020

bors bot commented Oct 31, 2020