[Merged by Bors] - chore(*): remove after the fact attribute [irreducible] at several places
#18168
Conversation
sgouezel
added
awaiting-review
sgouezel
added
WIP
sgouezel
added
the
awaiting-review
| @[simp] | ||
| theorem lift_ι_apply (f : X → A) (x) : | ||
| lift R f (ι R x) = f x := rfl | ||
| lift R f (ι R x) = f x := | ||
| by { rw [ι, lift], refl } | ||
|
|
There was a problem hiding this comment.
This is pretty unfortunate: having lift R f (ι R x) = f true feels like having sum.elim f g (sum.inl x) = f x true definitionally, in that it's effectively the recursor for the type.
This is expecially jarrying ater #18121, which only just introduced this defeq for tensor_product.
What happens if we just don't make it irreducible at all?
There was a problem hiding this comment.
In the current situation, iota is made irreducible a few lines below, so this lemma doesn't hold definitionally by the end of this file currently, and the PR doesn't change that.
We could also drop irreducibility of iota and lift, but I guess it was there for performance reasons. This would probably belong to a different PR, though.
There was a problem hiding this comment.
Ah, good point. I still think this is unfortunate, but now agree that's out of scope for this PR
| clifford_algebra.lift Q ⟨-(ι Q), λ m, by simp⟩ | ||
| begin | ||
| refine clifford_algebra.lift Q _, | ||
| exact ⟨-(ι Q), λ m, by simp only [linear_map.neg_apply, mul_neg, neg_mul, ι_sq_scalar, neg_neg]⟩ | ||
| end |
There was a problem hiding this comment.
Did squeezing the simp not work without the separate refine, or is this just a stylistic choice? If the former, a comment would be good.
There was a problem hiding this comment.
It didn't work without the separate refine when I removed the irreducible tag on clifford_algebra (I don't see how to make that irreducible in Lean 4). But since this is a can of worms, I have removed the Cliffod algebra stuff from this PR.
github-actions
bot
removed
the
awaiting-CI
sgouezel
added
mathport
|
Thanks! bors merge |
github-actions
bot
added
the
ready-to-merge
github-actions
bot
removed
the
awaiting-review
|
Build failed (retrying...): |
|
Pull request successfully merged into master. Build succeeded: |
bors
bot
changed the title
attribute [irreducible] at several placesattribute [irreducible] at several places
Part of #18164