Theorem: ContinuousAlgHom.coe_injective (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
⊢ Injective toAlgHom
Tactic:
intro f g H
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
f g : A →A[R] B
H : ↑f = ↑g
⊢ 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
f g : A →A[R] B
H : ↑f = ↑g
⊢ f = g
Tactic:
cases f
State after:
case mk
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
g : A →A[R] B
toAlgHom✝ : A →ₐ[R] B
cont✝ : Continuous (↑↑toAlgHom✝.toRingHom).toFun
H : ↑{ toAlgHom := toAlgHom✝, cont := cont✝ } = ↑g
⊢ { toAlgHom := toAlgHom✝, cont := cont✝ } = g

State before:
case mk
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
g : A →A[R] B
toAlgHom✝ : A →ₐ[R] B
cont✝ : Continuous (↑↑toAlgHom✝.toRingHom).toFun
H : ↑{ toAlgHom := toAlgHom✝, cont := cont✝ } = ↑g
⊢ { toAlgHom := toAlgHom✝, cont := cont✝ } = g
Tactic:
cases g
State after:
case mk.mk
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
toAlgHom✝¹ : A →ₐ[R] B
cont✝¹ : Continuous (↑↑toAlgHom✝¹.toRingHom).toFun
toAlgHom✝ : A →ₐ[R] B
cont✝ : Continuous (↑↑toAlgHom✝.toRingHom).toFun
H : ↑{ toAlgHom := toAlgHom✝¹, cont := cont✝¹ } = ↑{ toAlgHom := toAlgHom✝, cont := cont✝ }
⊢ { toAlgHom := toAlgHom✝¹, cont := cont✝¹ } = { toAlgHom := toAlgHom✝, cont := cont✝ }

State before:
case mk.mk
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
toAlgHom✝¹ : A →ₐ[R] B
cont✝¹ : Continuous (↑↑toAlgHom✝¹.toRingHom).toFun
toAlgHom✝ : A →ₐ[R] B
cont✝ : Continuous (↑↑toAlgHom✝.toRingHom).toFun
H : ↑{ toAlgHom := toAlgHom✝¹, cont := cont✝¹ } = ↑{ toAlgHom := toAlgHom✝, cont := cont✝ }
⊢ { toAlgHom := toAlgHom✝¹, cont := cont✝¹ } = { toAlgHom := toAlgHom✝, cont := cont✝ }
Tactic:
congr
State after:
no goals