Theorem: ContinuousAlgHom.ext_ring (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
B : Type u_3
inst✝⁴ : Semiring B
inst✝³ : TopologicalSpace B
inst✝² : Algebra R A
inst✝¹ : Algebra R B
inst✝ : TopologicalSpace R
f g : R →A[R] A
⊢ f = g
Tactic:
apply coe_inj.1
State after:
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
B : Type u_3
inst✝⁴ : Semiring B
inst✝³ : TopologicalSpace B
inst✝² : Algebra R A
inst✝¹ : Algebra R B
inst✝ : TopologicalSpace R
f g : R →A[R] A
⊢ ↑f = ↑g

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
B : Type u_3
inst✝⁴ : Semiring B
inst✝³ : TopologicalSpace B
inst✝² : Algebra R A
inst✝¹ : Algebra R B
inst✝ : TopologicalSpace R
f g : R →A[R] A
⊢ ↑f = ↑g
Tactic:
apply Algebra.ext_id
State after:
no goals