Odd behavior of simp

Stream: new members

[Eloi Torrents]

Hi, I noticed an odd behavior of the simp tactic, and I don't know what is happening...

import ring_theory.ring_invo

variables (R: Type) [ring R] (f: ring_invo R)

#check ring_hom.map_one
-- Here simp works fine with `f.to_ring_equiv` but not with `f` alone.
example: f.to_ring_equiv 1 = 1 := by {
   simp,
   }
example : f 1 = 1 := by {
   simp, --simplify tactic failed to simplify
   sorry
   }

-- But here it works fine with `f`  but not with `f.to_ring_equiv`.
#check ring_invo.involution
example : ∀ b: R, (f (f b).unop).unop = b := by {
   simp,
   }

example : ∀ b: R, (f.to_ring_equiv (f.to_ring_equiv b).unop).unop = b := by {
   simp, --simplify tactic failed to simplify
   sorry,
   }

[Eric Wieser]

I think docs#ring_invo is quite short on lemmas

[Eloi Torrents]

Is it a good idea to make these two simp lemmas?