1695b940b1
This PR ensures `simp` does not "simplify" instances by default. The old behavior can be retrieved by using `simp +instances`. This PR is similar to #12195, but for `dsimp`. The backward compatibility flag for `dsimp` also deactivates this new feature. ``` set_option backward.dsimp.instances true ``` Applying `simp` (and `dsimp`) to instances creates non-standard instances, and this creates all sorts of problems in Mathlib. --------- Co-authored-by: Henrik Böving <hargonix@gmail.com> Co-authored-by: Sebastian Graf <sgraf1337@gmail.com> Co-authored-by: Kim Morrison <kim@tqft.net>
19 lines
701 B
Text
19 lines
701 B
Text
class MulOneClass (M : Type u) extends One M, Mul M where
|
|
one_mul : ∀ a : M, 1 * a = a
|
|
mul_one : ∀ a : M, a * 1 = a
|
|
|
|
theorem MulOneClass.ext {M : Type u} : ∀ ⦃m₁ m₂ : MulOneClass M⦄, m₁.mul = m₂.mul → m₁ = m₂ := by
|
|
intro m₁ m₂
|
|
cases m₁ with
|
|
| @mk one₁ mul₁ one_mul₁ mul_one₁ =>
|
|
cases one₁ with | mk one₁
|
|
cases mul₁ with | mk mul₁
|
|
cases m₂ with
|
|
| @mk one₂ mul₂ one_mul₂ mul_one₂ =>
|
|
cases one₂ with | mk one₂
|
|
cases mul₂ with | mk mul₂
|
|
intro h
|
|
cases h
|
|
have := (one_mul₂ one₁).symm.trans (mul_one₁ one₂) -- TODO: make sure we can apply after congr
|
|
subst this
|
|
congr
|