EquivLike.IsSymm

Stream: mathlib4

[Kenny Lau]

import Mathlib

namespace EquivLike

class IsSymm {α β : Type*} (E₁ E₂ : Type*) [EquivLike E₁ α β] [EquivLike E₂ β α]
    (symm : E₁ → E₂) : Prop where
  eq_symm_apply {e x y} : x = symm e y ↔ e x = y

end EquivLike

variable {α β : Type*} [Ring α] [Ring β]

instance : EquivLike.IsSymm (α ≃+* β) _ RingEquiv.symm where
  eq_symm_apply := RingEquiv.eq_symm_apply ..

theorem foo {x y} (e : α ≃+* β) (h : e x = y) : x = e.symm y := by
  rw [EquivLike.IsSymm.eq_symm_apply]
  exact h

[Kenny Lau]

I recall earlier being told that class predicate on function is bad, but it seems to work for this example?

[Kenny Lau]

basically I want to make xxx.symm into a class so that we don't have to write a new eq_symm_apply lemma every time we define a new equivlike class

[Aaron Liu]

I would make symm an outParam

[Kenny Lau]

@Riccardo Brasca since you're here do you think this is a good idea?

[Riccardo Brasca]

Honestly I am not an heavy user of IsAdjoinRoot, so we should see how it is used in practice.

[Riccardo Brasca]

wait, this is a different discussion!

[Aaron Liu]

wrong discussion

[Aaron Liu]

Kenny Lau said:

basically I want to make xxx.symm into a class so that we don't have to write a new eq_symm_apply lemma every time we define a new equivlike class

Can we also make zero_apply and add_apply etc a class

[Aaron Liu]

though there is the conflict of pointwise multiplication and composition multiplication

[Kenny Lau]

Aaron Liu said:

Can we also make zero_apply and add_apply etc a class

ZeroApplyClass :melt: