case refine'_1
F : Type u_2
R : Type u_3
A : Type u_1
B : Type u_4
inst✝⁹ : CommSemiring R
inst✝⁸ : StarRing R
inst✝⁷ : Semiring A
inst✝⁶ : Algebra R A
inst✝⁵ : StarRing A
inst✝⁴ : StarModule R A
inst✝³ : Semiring B
inst✝² : Algebra R B
inst✝¹ : StarRing B
hF : StarAlgHomClass F R A B
f✝ g✝ : F
s : Set A
inst✝ : StarAlgHomClass F R { x // x ∈ adjoin R s } B
f g : F
h : ∀ (x : { x // x ∈ adjoin R s }), ↑x ∈ s → ↑f x = ↑g x
a : { x // x ∈ adjoin R s }
x : A
hx : x ∈ s
⊢ (fun y => ↑f y = ↑g y) { val := x, property := (_ : x ∈ ↑(adjoin R s)) }

case refine'_2
F : Type u_2
R : Type u_3
A : Type u_1
B : Type u_4
inst✝⁹ : CommSemiring R
inst✝⁸ : StarRing R
inst✝⁷ : Semiring A
inst✝⁶ : Algebra R A
inst✝⁵ : StarRing A
inst✝⁴ : StarModule R A
inst✝³ : Semiring B
inst✝² : Algebra R B
inst✝¹ : StarRing B
hF : StarAlgHomClass F R A B
f✝ g✝ : F
s : Set A
inst✝ : StarAlgHomClass F R { x // x ∈ adjoin R s } B
f g : F
h : ∀ (x : { x // x ∈ adjoin R s }), ↑x ∈ s → ↑f x = ↑g x
a : { x // x ∈ adjoin R s }
r : R
⊢ (fun y => ↑f y = ↑g y) (↑(algebraMap R { x // x ∈ adjoin R s }) r)

case refine'_3
F : Type u_2
R : Type u_3
A : Type u_1
B : Type u_4
inst✝⁹ : CommSemiring R
inst✝⁸ : StarRing R
inst✝⁷ : Semiring A
inst✝⁶ : Algebra R A
inst✝⁵ : StarRing A
inst✝⁴ : StarModule R A
inst✝³ : Semiring B
inst✝² : Algebra R B
inst✝¹ : StarRing B
hF : StarAlgHomClass F R A B
f✝ g✝ : F
s : Set A
inst✝ : StarAlgHomClass F R { x // x ∈ adjoin R s } B
f g : F
h : ∀ (x : { x // x ∈ adjoin R s }), ↑x ∈ s → ↑f x = ↑g x
a x y : { x // x ∈ adjoin R s }
hx : (fun y => ↑f y = ↑g y) x
hy : (fun y => ↑f y = ↑g y) y
⊢ (fun y => ↑f y = ↑g y) (x + y)

case refine'_4
F : Type u_2
R : Type u_3
A : Type u_1
B : Type u_4
inst✝⁹ : CommSemiring R
inst✝⁸ : StarRing R
inst✝⁷ : Semiring A
inst✝⁶ : Algebra R A
inst✝⁵ : StarRing A
inst✝⁴ : StarModule R A
inst✝³ : Semiring B
inst✝² : Algebra R B
inst✝¹ : StarRing B
hF : StarAlgHomClass F R A B
f✝ g✝ : F
s : Set A
inst✝ : StarAlgHomClass F R { x // x ∈ adjoin R s } B
f g : F
h : ∀ (x : { x // x ∈ adjoin R s }), ↑x ∈ s → ↑f x = ↑g x
a x y : { x // x ∈ adjoin R s }
hx : (fun y => ↑f y = ↑g y) x
hy : (fun y => ↑f y = ↑g y) y
⊢ (fun y => ↑f y = ↑g y) (x * y)

case refine'_5
F : Type u_2
R : Type u_3
A : Type u_1
B : Type u_4
inst✝⁹ : CommSemiring R
inst✝⁸ : StarRing R
inst✝⁷ : Semiring A
inst✝⁶ : Algebra R A
inst✝⁵ : StarRing A
inst✝⁴ : StarModule R A
inst✝³ : Semiring B
inst✝² : Algebra R B
inst✝¹ : StarRing B
hF : StarAlgHomClass F R A B
f✝ g✝ : F
s : Set A
inst✝ : StarAlgHomClass F R { x // x ∈ adjoin R s } B
f g : F
h : ∀ (x : { x // x ∈ adjoin R s }), ↑x ∈ s → ↑f x = ↑g x
a x : { x // x ∈ adjoin R s }
hx : (fun y => ↑f y = ↑g y) x
⊢ (fun y => ↑f y = ↑g y) (star x)
F : Type u_2
R : Type u_3
A : Type u_1
B : Type u_4
inst✝⁹ : CommSemiring R
inst✝⁸ : StarRing R
inst✝⁷ : Semiring A
inst✝⁶ : Algebra R A
inst✝⁵ : StarRing A
inst✝⁴ : StarModule R A
inst✝³ : Semiring B
inst✝² : Algebra R B
inst✝¹ : StarRing B
hF : StarAlgHomClass F R A B
f✝ g✝ : F
s : Set A
inst✝ : StarAlgHomClass F R { x // x ∈ adjoin R s } B
f g : F
h : ∀ (x : { x // x ∈ adjoin R s }), ↑x ∈ s → ↑f x = ↑g x
⊢ f = g
refine' FunLike.ext f g fun a =>
  adjoin_induction' (p := fun y => f y = g y) a (fun x hx => _) (fun r => _)
  (fun x y hx hy => _) (fun x y hx hy => _) fun x hx => _
no goals
case refine'_1
F : Type u_2
R : Type u_3
A : Type u_1
B : Type u_4
inst✝⁹ : CommSemiring R
inst✝⁸ : StarRing R
inst✝⁷ : Semiring A
inst✝⁶ : Algebra R A
inst✝⁵ : StarRing A
inst✝⁴ : StarModule R A
inst✝³ : Semiring B
inst✝² : Algebra R B
inst✝¹ : StarRing B
hF : StarAlgHomClass F R A B
f✝ g✝ : F
s : Set A
inst✝ : StarAlgHomClass F R { x // x ∈ adjoin R s } B
f g : F
h : ∀ (x : { x // x ∈ adjoin R s }), ↑x ∈ s → ↑f x = ↑g x
a : { x // x ∈ adjoin R s }
x : A
hx : x ∈ s
⊢ (fun y => ↑f y = ↑g y) { val := x, property := (_ : x ∈ ↑(adjoin R s)) }
exact h ⟨x, subset_adjoin R s hx⟩ hx
no goals
case refine'_2
F : Type u_2
R : Type u_3
A : Type u_1
B : Type u_4
inst✝⁹ : CommSemiring R
inst✝⁸ : StarRing R
inst✝⁷ : Semiring A
inst✝⁶ : Algebra R A
inst✝⁵ : StarRing A
inst✝⁴ : StarModule R A
inst✝³ : Semiring B
inst✝² : Algebra R B
inst✝¹ : StarRing B
hF : StarAlgHomClass F R A B
f✝ g✝ : F
s : Set A
inst✝ : StarAlgHomClass F R { x // x ∈ adjoin R s } B
f g : F
h : ∀ (x : { x // x ∈ adjoin R s }), ↑x ∈ s → ↑f x = ↑g x
a : { x // x ∈ adjoin R s }
r : R
⊢ (fun y => ↑f y = ↑g y) (↑(algebraMap R { x // x ∈ adjoin R s }) r)
simp only [AlgHomClass.commutes]
no goals
case refine'_3
F : Type u_2
R : Type u_3
A : Type u_1
B : Type u_4
inst✝⁹ : CommSemiring R
inst✝⁸ : StarRing R
inst✝⁷ : Semiring A
inst✝⁶ : Algebra R A
inst✝⁵ : StarRing A
inst✝⁴ : StarModule R A
inst✝³ : Semiring B
inst✝² : Algebra R B
inst✝¹ : StarRing B
hF : StarAlgHomClass F R A B
f✝ g✝ : F
s : Set A
inst✝ : StarAlgHomClass F R { x // x ∈ adjoin R s } B
f g : F
h : ∀ (x : { x // x ∈ adjoin R s }), ↑x ∈ s → ↑f x = ↑g x
a x y : { x // x ∈ adjoin R s }
hx : (fun y => ↑f y = ↑g y) x
hy : (fun y => ↑f y = ↑g y) y
⊢ (fun y => ↑f y = ↑g y) (x + y)
simp only [map_add, map_add, hx, hy]
no goals
case refine'_4
F : Type u_2
R : Type u_3
A : Type u_1
B : Type u_4
inst✝⁹ : CommSemiring R
inst✝⁸ : StarRing R
inst✝⁷ : Semiring A
inst✝⁶ : Algebra R A
inst✝⁵ : StarRing A
inst✝⁴ : StarModule R A
inst✝³ : Semiring B
inst✝² : Algebra R B
inst✝¹ : StarRing B
hF : StarAlgHomClass F R A B
f✝ g✝ : F
s : Set A
inst✝ : StarAlgHomClass F R { x // x ∈ adjoin R s } B
f g : F
h : ∀ (x : { x // x ∈ adjoin R s }), ↑x ∈ s → ↑f x = ↑g x
a x y : { x // x ∈ adjoin R s }
hx : (fun y => ↑f y = ↑g y) x
hy : (fun y => ↑f y = ↑g y) y
⊢ (fun y => ↑f y = ↑g y) (x * y)
simp only [map_mul, map_mul, hx, hy]
no goals
case refine'_5
F : Type u_2
R : Type u_3
A : Type u_1
B : Type u_4
inst✝⁹ : CommSemiring R
inst✝⁸ : StarRing R
inst✝⁷ : Semiring A
inst✝⁶ : Algebra R A
inst✝⁵ : StarRing A
inst✝⁴ : StarModule R A
inst✝³ : Semiring B
inst✝² : Algebra R B
inst✝¹ : StarRing B
hF : StarAlgHomClass F R A B
f✝ g✝ : F
s : Set A
inst✝ : StarAlgHomClass F R { x // x ∈ adjoin R s } B
f g : F
h : ∀ (x : { x // x ∈ adjoin R s }), ↑x ∈ s → ↑f x = ↑g x
a x : { x // x ∈ adjoin R s }
hx : (fun y => ↑f y = ↑g y) x
⊢ (fun y => ↑f y = ↑g y) (star x)
simp only [map_star, hx]