-- Mathlib/Topology/Algebra/StarSubalgebra.lean
theorem starAlgHomClass_ext [T2Space B] {F : Type*} {a : A}
    [FunLike F (elemental R a) B] [AlgHomClass F R _ B] [StarHomClass F _ B]
    {φ ψ : F} (hφ : Continuous φ)
    (hψ : Continuous ψ) (h : φ ⟨a, self_mem R a⟩ = ψ ⟨a, self_mem R a⟩) : φ = ψ

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✝¹² : StarRing A
inst✝¹¹ : IsTopologicalSemiring A
inst✝¹⁰ : ContinuousStar A
inst✝⁹ : Algebra R A
inst✝⁸ : StarModule R A
inst✝⁷ : TopologicalSpace B
inst✝⁶ : Semiring B
inst✝⁵ : StarRing B
inst✝⁴ : Algebra R B
inst✝³ : T2Space B
F : Type u_4
a : A
inst✝² : FunLike F (↥(elemental R a)) B
inst✝¹ : AlgHomClass F R (↥(elemental R a)) B
inst✝ : StarHomClass F (↥(elemental R a)) B
φ ψ : F
hφ : Continuous ⇑φ
hψ : Continuous ⇑ψ
h : φ ⟨a, ⋯⟩ = ψ ⟨a, ⋯⟩
x✝ x y : ↥(adjoin R {a})
hx : φ ((inclusion ⋯) x) = ψ ((inclusion ⋯) x)
hy : φ ((inclusion ⋯) y) = ψ ((inclusion ⋯) y)
⊢ φ ((inclusion ⋯) (x + y)) = ψ ((inclusion ⋯) (x + y))

Tactic:
simp only [map_add, hx, hy]

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✝¹² : StarRing A
inst✝¹¹ : IsTopologicalSemiring A
inst✝¹⁰ : ContinuousStar A
inst✝⁹ : Algebra R A
inst✝⁸ : StarModule R A
inst✝⁷ : TopologicalSpace B
inst✝⁶ : Semiring B
inst✝⁵ : StarRing B
inst✝⁴ : Algebra R B
inst✝³ : T2Space B
F : Type u_4
a : A
inst✝² : FunLike F (↥(elemental R a)) B
inst✝¹ : AlgHomClass F R (↥(elemental R a)) B
inst✝ : StarHomClass F (↥(elemental R a)) B
φ ψ : F
hφ : Continuous ⇑φ
hψ : Continuous ⇑ψ
h : φ ⟨a, ⋯⟩ = ψ ⟨a, ⋯⟩
x✝ x y : ↥(adjoin R {a})
hx : φ ((inclusion ⋯) x) = ψ ((inclusion ⋯) x)
hy : φ ((inclusion ⋯) y) = ψ ((inclusion ⋯) y)
⊢ φ ((inclusion ⋯) (x * y)) = ψ ((inclusion ⋯) (x * y))

Tactic:
simp only [map_mul, hx, hy]

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✝¹² : StarRing A
inst✝¹¹ : IsTopologicalSemiring A
inst✝¹⁰ : ContinuousStar A
inst✝⁹ : Algebra R A
inst✝⁸ : StarModule R A
inst✝⁷ : TopologicalSpace B
inst✝⁶ : Semiring B
inst✝⁵ : StarRing B
inst✝⁴ : Algebra R B
inst✝³ : T2Space B
F : Type u_4
a : A
inst✝² : FunLike F (↥(elemental R a)) B
inst✝¹ : AlgHomClass F R (↥(elemental R a)) B
inst✝ : StarHomClass F (↥(elemental R a)) B
φ ψ : F
hφ : Continuous ⇑φ
hψ : Continuous ⇑ψ
h : φ ⟨a, ⋯⟩ = ψ ⟨a, ⋯⟩
x : ↥(adjoin R {a})
r : R
⊢ φ ((inclusion ⋯) ((algebraMap R ↥(adjoin R {a})) r)) = ψ ((inclusion ⋯) ((algebraMap R ↥(adjoin R {a})) r))

Tactic:
simp only [AlgHomClass.commutes]

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✝¹² : StarRing A
inst✝¹¹ : IsTopologicalSemiring A
inst✝¹⁰ : ContinuousStar A
inst✝⁹ : Algebra R A
inst✝⁸ : StarModule R A
inst✝⁷ : TopologicalSpace B
inst✝⁶ : Semiring B
inst✝⁵ : StarRing B
inst✝⁴ : Algebra R B
inst✝³ : T2Space B
F : Type u_4
a : A
inst✝² : FunLike F (↥(elemental R a)) B
inst✝¹ : AlgHomClass F R (↥(elemental R a)) B
inst✝ : StarHomClass F (↥(elemental R a)) B
φ ψ : F
hφ : Continuous ⇑φ
hψ : Continuous ⇑ψ
h : φ ⟨a, ⋯⟩ = ψ ⟨a, ⋯⟩
x : ↥(adjoin R {a})
y : A
hy : y ∈ {a}
⊢ φ ((inclusion ⋯) ⟨y, ⋯⟩) = ψ ((inclusion ⋯) ⟨y, ⋯⟩)

Tactic:
simpa only [Set.mem_singleton_iff.mp hy] using h

Result:
no goals

Proof state:
case refine_1
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✝¹² : StarRing A
inst✝¹¹ : IsTopologicalSemiring A
inst✝¹⁰ : ContinuousStar A
inst✝⁹ : Algebra R A
inst✝⁸ : StarModule R A
inst✝⁷ : TopologicalSpace B
inst✝⁶ : Semiring B
inst✝⁵ : StarRing B
inst✝⁴ : Algebra R B
inst✝³ : T2Space B
F : Type u_4
a : A
inst✝² : FunLike F (↥(elemental R a)) B
inst✝¹ : AlgHomClass F R (↥(elemental R a)) B
inst✝ : StarHomClass F (↥(elemental R a)) B
φ ψ : F
hφ : Continuous ⇑φ
hψ : Continuous ⇑ψ
h : φ ⟨a, ⋯⟩ = ψ ⟨a, ⋯⟩
x : ↥(adjoin R {a})
⊢ ∀ (x : A) (h : x ∈ {a}), φ ((inclusion ⋯) ⟨x, ⋯⟩) = ψ ((inclusion ⋯) ⟨x, ⋯⟩)

case refine_2
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✝¹² : StarRing A
inst✝¹¹ : IsTopologicalSemiring A
inst✝¹⁰ : ContinuousStar A
inst✝⁹ : Algebra R A
inst✝⁸ : StarModule R A
inst✝⁷ : TopologicalSpace B
inst✝⁶ : Semiring B
inst✝⁵ : StarRing B
inst✝⁴ : Algebra R B
inst✝³ : T2Space B
F : Type u_4
a : A
inst✝² : FunLike F (↥(elemental R a)) B
inst✝¹ : AlgHomClass F R (↥(elemental R a)) B
inst✝ : StarHomClass F (↥(elemental R a)) B
φ ψ : F
hφ : Continuous ⇑φ
hψ : Continuous ⇑ψ
h : φ ⟨a, ⋯⟩ = ψ ⟨a, ⋯⟩
x : ↥(adjoin R {a})
⊢ ∀ (r : R), φ ((inclusion ⋯) ((algebraMap R ↥(adjoin R {a})) r)) = ψ ((inclusion ⋯) ((algebraMap R ↥(adjoin R {a})) r))

case refine_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✝¹² : StarRing A
inst✝¹¹ : IsTopologicalSemiring A
inst✝¹⁰ : ContinuousStar A
inst✝⁹ : Algebra R A
inst✝⁸ : StarModule R A
inst✝⁷ : TopologicalSpace B
inst✝⁶ : Semiring B
inst✝⁵ : StarRing B
inst✝⁴ : Algebra R B
inst✝³ : T2Space B
F : Type u_4
a : A
inst✝² : FunLike F (↥(elemental R a)) B
inst✝¹ : AlgHomClass F R (↥(elemental R a)) B
inst✝ : StarHomClass F (↥(elemental R a)) B
φ ψ : F
hφ : Continuous ⇑φ
hψ : Continuous ⇑ψ
h : φ ⟨a, ⋯⟩ = ψ ⟨a, ⋯⟩
x : ↥(adjoin R {a})
⊢ ∀ (x y : ↥(adjoin R {a})),
    φ ((inclusion ⋯) x) = ψ ((inclusion ⋯) x) →
      φ ((inclusion ⋯) y) = ψ ((inclusion ⋯) y) → φ ((inclusion ⋯) (x + y)) = ψ ((inclusion ⋯) (x + y))

case refine_4
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✝¹² : StarRing A
inst✝¹¹ : IsTopologicalSemiring A
inst✝¹⁰ : ContinuousStar A
inst✝⁹ : Algebra R A
inst✝⁸ : StarModule R A
inst✝⁷ : TopologicalSpace B
inst✝⁶ : Semiring B
inst✝⁵ : StarRing B
inst✝⁴ : Algebra R B
inst✝³ : T2Space B
F : Type u_4
a : A
inst✝² : FunLike F (↥(elemental R a)) B
inst✝¹ : AlgHomClass F R (↥(elemental R a)) B
inst✝ : StarHomClass F (↥(elemental R a)) B
φ ψ : F
hφ : Continuous ⇑φ
hψ : Continuous ⇑ψ
h : φ ⟨a, ⋯⟩ = ψ ⟨a, ⋯⟩
x : ↥(adjoin R {a})
⊢ ∀ (x y : ↥(adjoin R {a})),
    φ ((inclusion ⋯) x) = ψ ((inclusion ⋯) x) →
      φ ((inclusion ⋯) y) = ψ ((inclusion ⋯) y) → φ ((inclusion ⋯) (x * y)) = ψ ((inclusion ⋯) (x * y))

case refine_5
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✝¹² : StarRing A
inst✝¹¹ : IsTopologicalSemiring A
inst✝¹⁰ : ContinuousStar A
inst✝⁹ : Algebra R A
inst✝⁸ : StarModule R A
inst✝⁷ : TopologicalSpace B
inst✝⁶ : Semiring B
inst✝⁵ : StarRing B
inst✝⁴ : Algebra R B
inst✝³ : T2Space B
F : Type u_4
a : A
inst✝² : FunLike F (↥(elemental R a)) B
inst✝¹ : AlgHomClass F R (↥(elemental R a)) B
inst✝ : StarHomClass F (↥(elemental R a)) B
φ ψ : F
hφ : Continuous ⇑φ
hψ : Continuous ⇑ψ
h : φ ⟨a, ⋯⟩ = ψ ⟨a, ⋯⟩
x : ↥(adjoin R {a})
⊢ ∀ (x : ↥(adjoin R {a})),
    φ ((inclusion ⋯) x) = ψ ((inclusion ⋯) x) → φ ((inclusion ⋯) (star x)) = ψ ((inclusion ⋯) (star x))

Tactic:
exacts [fun y hy => by simpa only [Set.mem_singleton_iff.mp hy] using h, fun r => by
  simp only [AlgHomClass.commutes], fun x y hx hy => by simp only [map_add, hx, hy],
  fun x y hx hy => by simp only [map_mul, hx, hy], fun x hx => by simp only [map_star, hx]]

Result:
no goals