-- Mathlib/Topology/Algebra/Algebra.lean
theorem coe_inj {f g : A →A[R] B} : (f : A →ₐ[R] B) = g ↔ f = g :=   by
  cases f; cases g; simp only [mk.injEq]; exact Eq.congr_right rfl

Proof state:
R : Type u_1
inst✝⁶ : CommSemiring R
A : Type u_2
inst✝⁵ : Semiring A
inst✝⁴ : TopologicalSpace 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
⊢ ↑f = ↑g ↔ f = g

Tactic:
cases f

Result:
case mk
R : Type u_1
inst✝⁶ : CommSemiring R
A : Type u_2
inst✝⁵ : Semiring A
inst✝⁴ : TopologicalSpace 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
⊢ ↑{ toAlgHom := toAlgHom✝, cont := cont✝ } = ↑g ↔ { toAlgHom := toAlgHom✝, cont := cont✝ } = g

Proof state:
case mk
R : Type u_1
inst✝⁶ : CommSemiring R
A : Type u_2
inst✝⁵ : Semiring A
inst✝⁴ : TopologicalSpace 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
⊢ ↑{ toAlgHom := toAlgHom✝, cont := cont✝ } = ↑g ↔ { toAlgHom := toAlgHom✝, cont := cont✝ } = g

Tactic:
cases g

Result:
case mk.mk
R : Type u_1
inst✝⁶ : CommSemiring R
A : Type u_2
inst✝⁵ : Semiring A
inst✝⁴ : TopologicalSpace 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
⊢ ↑{ toAlgHom := toAlgHom✝¹, cont := cont✝¹ } = ↑{ toAlgHom := toAlgHom✝, cont := cont✝ } ↔
    { toAlgHom := toAlgHom✝¹, cont := cont✝¹ } = { toAlgHom := toAlgHom✝, cont := cont✝ }

Proof state:
case mk.mk
R : Type u_1
inst✝⁶ : CommSemiring R
A : Type u_2
inst✝⁵ : Semiring A
inst✝⁴ : TopologicalSpace 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
⊢ ↑{ toAlgHom := toAlgHom✝¹, cont := cont✝¹ } = ↑{ toAlgHom := toAlgHom✝, cont := cont✝ } ↔ toAlgHom✝¹ = toAlgHom✝

Tactic:
exact Eq.congr_right rfl

Result:
no goals

Proof state:
case mk.mk
R : Type u_1
inst✝⁶ : CommSemiring R
A : Type u_2
inst✝⁵ : Semiring A
inst✝⁴ : TopologicalSpace 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
⊢ ↑{ toAlgHom := toAlgHom✝¹, cont := cont✝¹ } = ↑{ toAlgHom := toAlgHom✝, cont := cont✝ } ↔
    { toAlgHom := toAlgHom✝¹, cont := cont✝¹ } = { toAlgHom := toAlgHom✝, cont := cont✝ }

Tactic:
simp only [mk.injEq]

Result:
case mk.mk
R : Type u_1
inst✝⁶ : CommSemiring R
A : Type u_2
inst✝⁵ : Semiring A
inst✝⁴ : TopologicalSpace 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
⊢ ↑{ toAlgHom := toAlgHom✝¹, cont := cont✝¹ } = ↑{ toAlgHom := toAlgHom✝, cont := cont✝ } ↔ toAlgHom✝¹ = toAlgHom✝