Doing simp? on the offending declaration in #3007 reveals that ring_equiv.to_fun_eq_coe is likely the lemma that should be restored, not the two already restored.

Try this: simp only [free_algebra.star_algebra_map,
 mul_opposite.algebra_map_apply,
 ring_equiv.to_fun_eq_coe,
 eq_self_iff_true,
 mul_opposite.op_inj,
 star_ring_equiv_apply,
 free_algebra.algebra_map_inj]

Can you try with squeeze_simp?

You're right though; ring_equiv.to_fun_eq_coe should be restored too edit: nevermind. Lean3's some_ring_equiv.to_fun is lean 4's some_ring_equiv.to_equiv.to_fun; so dropping ring_equiv.to_fun_eq_coe was correct

Can you try with squeeze_simp?

It returns

Try this: simp only [star_algebra_map, ring_equiv.to_fun_eq_coe, star_ring_equiv_apply, mul_opposite.algebra_map_apply]

See my edit above. ring_equiv.to_fun_eq_coe has been replaced by equiv.to_fun_eq_coe and ring_equiv.coe_to_equiv in Lean 4, since ring_equiv.to_fun no longer exists

LGTM
bors r+

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style