-- Mathlib/Topology/Algebra/StarSubalgebra.lean
theorem _root_.StarAlgHom.ext_topologicalClosure [T2Space B] {S : StarSubalgebra R A}
    {φ ψ : S.topologicalClosure →⋆ₐ[R] B} (hφ : Continuous φ) (hψ : Continuous ψ)
    (h :
      φ.comp (inclusion (le_topologicalClosure S)) = ψ.comp (inclusion (le_topologicalClosure S))) :
    φ = ψ

Proof state:
case h.e'_4.h.e'_3
R : Type u_1
A : Type u_2
B : Type u_3
inst✝¹³ : CommSemiring R
inst✝¹² : StarRing R
inst✝¹¹ : TopologicalSpace A
inst✝¹⁰ : Semiring A
inst✝⁹ : Algebra R A
inst✝⁸ : StarRing A
inst✝⁷ : StarModule R A
inst✝⁶ : IsTopologicalSemiring A
inst✝⁵ : ContinuousStar A
inst✝⁴ : TopologicalSpace B
inst✝³ : Semiring B
inst✝² : Algebra R B
inst✝¹ : StarRing B
inst✝ : T2Space B
S : StarSubalgebra R A
φ ψ : ↥S.topologicalClosure →⋆ₐ[R] B
hφ : Continuous ⇑φ
hψ : Continuous ⇑ψ
h : φ.comp (inclusion ⋯) = ψ.comp (inclusion ⋯)
x : { x // x ∈ ↑S.topologicalClosure }
⊢ Subtype.val '' Set.range ⇑(inclusion ⋯) = ↑S

Tactic:
rw [← Set.range_comp]

Result:
case h.e'_4.h.e'_3
R : Type u_1
A : Type u_2
B : Type u_3
inst✝¹³ : CommSemiring R
inst✝¹² : StarRing R
inst✝¹¹ : TopologicalSpace A
inst✝¹⁰ : Semiring A
inst✝⁹ : Algebra R A
inst✝⁸ : StarRing A
inst✝⁷ : StarModule R A
inst✝⁶ : IsTopologicalSemiring A
inst✝⁵ : ContinuousStar A
inst✝⁴ : TopologicalSpace B
inst✝³ : Semiring B
inst✝² : Algebra R B
inst✝¹ : StarRing B
inst✝ : T2Space B
S : StarSubalgebra R A
φ ψ : ↥S.topologicalClosure →⋆ₐ[R] B
hφ : Continuous ⇑φ
hψ : Continuous ⇑ψ
h : φ.comp (inclusion ⋯) = ψ.comp (inclusion ⋯)
x : { x // x ∈ ↑S.topologicalClosure }
⊢ Set.range (Subtype.val ∘ ⇑(inclusion ⋯)) = ↑S

Proof state:
case h.e'_4.h.e'_3
R : Type u_1
A : Type u_2
B : Type u_3
inst✝¹³ : CommSemiring R
inst✝¹² : StarRing R
inst✝¹¹ : TopologicalSpace A
inst✝¹⁰ : Semiring A
inst✝⁹ : Algebra R A
inst✝⁸ : StarRing A
inst✝⁷ : StarModule R A
inst✝⁶ : IsTopologicalSemiring A
inst✝⁵ : ContinuousStar A
inst✝⁴ : TopologicalSpace B
inst✝³ : Semiring B
inst✝² : Algebra R B
inst✝¹ : StarRing B
inst✝ : T2Space B
S : StarSubalgebra R A
φ ψ : ↥S.topologicalClosure →⋆ₐ[R] B
hφ : Continuous ⇑φ
hψ : Continuous ⇑ψ
h : φ.comp (inclusion ⋯) = ψ.comp (inclusion ⋯)
x : { x // x ∈ ↑S.topologicalClosure }
⊢ Set.range (Subtype.val ∘ ⇑(inclusion ⋯)) = ↑S

Tactic:
exact
  Set.ext fun y =>
    ⟨by
      rintro ⟨y, rfl⟩
      exact y.prop, fun hy => ⟨⟨y, hy⟩, rfl⟩⟩

Result:
no goals

Proof state:
R : Type u_1
A : Type u_2
B : Type u_3
inst✝¹³ : CommSemiring R
inst✝¹² : StarRing R
inst✝¹¹ : TopologicalSpace A
inst✝¹⁰ : Semiring A
inst✝⁹ : Algebra R A
inst✝⁸ : StarRing A
inst✝⁷ : StarModule R A
inst✝⁶ : IsTopologicalSemiring A
inst✝⁵ : ContinuousStar A
inst✝⁴ : TopologicalSpace B
inst✝³ : Semiring B
inst✝² : Algebra R B
inst✝¹ : StarRing B
inst✝ : T2Space B
S : StarSubalgebra R A
φ ψ : ↥S.topologicalClosure →⋆ₐ[R] B
hφ : Continuous ⇑φ
hψ : Continuous ⇑ψ
h : φ.comp (inclusion ⋯) = ψ.comp (inclusion ⋯)
⊢ Dense (Set.range ⇑(inclusion ⋯))

Tactic:
refine IsInducing.subtypeVal.dense_iff.2 fun x => ?_

Result:
R : Type u_1
A : Type u_2
B : Type u_3
inst✝¹³ : CommSemiring R
inst✝¹² : StarRing R
inst✝¹¹ : TopologicalSpace A
inst✝¹⁰ : Semiring A
inst✝⁹ : Algebra R A
inst✝⁸ : StarRing A
inst✝⁷ : StarModule R A
inst✝⁶ : IsTopologicalSemiring A
inst✝⁵ : ContinuousStar A
inst✝⁴ : TopologicalSpace B
inst✝³ : Semiring B
inst✝² : Algebra R B
inst✝¹ : StarRing B
inst✝ : T2Space B
S : StarSubalgebra R A
φ ψ : ↥S.topologicalClosure →⋆ₐ[R] B
hφ : Continuous ⇑φ
hψ : Continuous ⇑ψ
h : φ.comp (inclusion ⋯) = ψ.comp (inclusion ⋯)
x : { x // x ∈ ↑S.topologicalClosure }
⊢ ↑x ∈ closure (Subtype.val '' Set.range ⇑(inclusion ⋯))

Proof state:
R : Type u_1
A : Type u_2
B : Type u_3
inst✝¹³ : CommSemiring R
inst✝¹² : StarRing R
inst✝¹¹ : TopologicalSpace A
inst✝¹⁰ : Semiring A
inst✝⁹ : Algebra R A
inst✝⁸ : StarRing A
inst✝⁷ : StarModule R A
inst✝⁶ : IsTopologicalSemiring A
inst✝⁵ : ContinuousStar A
inst✝⁴ : TopologicalSpace B
inst✝³ : Semiring B
inst✝² : Algebra R B
inst✝¹ : StarRing B
inst✝ : T2Space B
S : StarSubalgebra R A
φ ψ : ↥S.topologicalClosure →⋆ₐ[R] B
hφ : Continuous ⇑φ
hψ : Continuous ⇑ψ
h : φ.comp (inclusion ⋯) = ψ.comp (inclusion ⋯)
x : { x // x ∈ ↑S.topologicalClosure }
⊢ ↑x ∈ closure (Subtype.val '' Set.range ⇑(inclusion ⋯))

Tactic:
convert show ↑x ∈ closure (S : Set A) from x.prop

Result:
case h.e'_4.h.e'_3
R : Type u_1
A : Type u_2
B : Type u_3
inst✝¹³ : CommSemiring R
inst✝¹² : StarRing R
inst✝¹¹ : TopologicalSpace A
inst✝¹⁰ : Semiring A
inst✝⁹ : Algebra R A
inst✝⁸ : StarRing A
inst✝⁷ : StarModule R A
inst✝⁶ : IsTopologicalSemiring A
inst✝⁵ : ContinuousStar A
inst✝⁴ : TopologicalSpace B
inst✝³ : Semiring B
inst✝² : Algebra R B
inst✝¹ : StarRing B
inst✝ : T2Space B
S : StarSubalgebra R A
φ ψ : ↥S.topologicalClosure →⋆ₐ[R] B
hφ : Continuous ⇑φ
hψ : Continuous ⇑ψ
h : φ.comp (inclusion ⋯) = ψ.comp (inclusion ⋯)
x : { x // x ∈ ↑S.topologicalClosure }
⊢ Subtype.val '' Set.range ⇑(inclusion ⋯) = ↑S