Theorem: ContinuousAlgHom.coe_eq_id (DividedPowers/ForMathlib/Topology/Algebra/Algebra/Basic.lean)

State before:
R : Type u_1
inst✝⁶ : CommSemiring R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : TopologicalSemiring R
A : Type u_2
inst✝³ : Semiring A
inst✝² : TopologicalSpace A
inst✝¹ : TopologicalSemiring A
inst✝ : Algebra R A
f : A →A[R] A
⊢ ↑f = AlgHom.id R A ↔ f = id R A
Tactic:
rw [← coe_id, coe_inj]
State after:
no goals