case a
F : Type ?u.100208
α : Type ?u.100211
β : Type ?u.100214
R : Type u_1
S : Type u_2
S' : Type ?u.100223
inst✝² : NonAssocSemiring R
inst✝¹ : NonAssocSemiring S
inst✝ : NonAssocSemiring S'
e : R ≃+* S
x✝ : S
⊢ ↑(RingHom.comp (toRingHom e) (toRingHom (RingEquiv.symm e))) x✝ = ↑(RingHom.id S) x✝
F : Type ?u.100208
α : Type ?u.100211
β : Type ?u.100214
R : Type u_1
S : Type u_2
S' : Type ?u.100223
inst✝² : NonAssocSemiring R
inst✝¹ : NonAssocSemiring S
inst✝ : NonAssocSemiring S'
e : R ≃+* S
⊢ RingHom.comp (toRingHom e) (toRingHom (RingEquiv.symm e)) = RingHom.id S
ext
no goals
case a
F : Type ?u.100208
α : Type ?u.100211
β : Type ?u.100214
R : Type u_1
S : Type u_2
S' : Type ?u.100223
inst✝² : NonAssocSemiring R
inst✝¹ : NonAssocSemiring S
inst✝ : NonAssocSemiring S'
e : R ≃+* S
x✝ : S
⊢ ↑(RingHom.comp (toRingHom e) (toRingHom (RingEquiv.symm e))) x✝ = ↑(RingHom.id S) x✝
simp